idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 12:42:02 +03:00
Code Issues Projects Releases Wiki Activity

Improve inference of linearity in let

Browse Source 
This involves a bit of backtracking in linearity checking, which I'd
prefer to avoid, but it won't hurt in the normal case. If checking a
binder fails due to linearity misuse, try again at linear multiplicity.
This commit is contained in:
Edwin Brady 2020-06-12 13:47:15 +01:00
parent c9b20911e1
commit b2c7029b6b
3 changed files with 27 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Core/LinearCheck.idr
View File

@ -247,7 +247,13 @@ mutual
unusedHoleArgs _ ty = ty
lcheck rig_in erase env (Bind fc nm b sc)
= do (b', bt, usedb) <- lcheckBinder rig erase env b
= do (b', bt, usedb) <- handleUnify (lcheckBinder rig erase env b)
(\err =>
case err of
LinearMisuse _ _ r _ =>
lcheckBinder rig erase env
(setMultiplicity b linear)
_ => throw err)
-- Anything linear can't be used in the scope of a lambda, if we're
-- checking in general context
let env' = if rig_in == top

30
src/TTImp/Elab/Binders.idr
View File

@ -201,17 +201,17 @@ checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty {vars}
(record { preciseInf = True } elabinfo)
nest env nVal (Just (gnf env tyv))
pure (fst c, snd c, rigl |*| rigc))
(\err => case err of
(LinearMisuse _ _ r _)
=> branchOne
(do c <- runDelays 0 $ check linear elabinfo
nest env nVal (Just (gnf env tyv))
pure (fst c, snd c, linear))
(do c <- check (rigl |*| rigc)
elabinfo -- without preciseInf
nest env nVal (Just (gnf env tyv))
pure (fst c, snd c, rigMult rigl rigc))
r
(\err => case linearErr err of
Just r
=> do branchOne
(do c <- runDelays 0 $ check linear elabinfo
nest env nVal (Just (gnf env tyv))
pure (fst c, snd c, linear))
(do c <- check (rigl |*| rigc)
elabinfo -- without preciseInf
nest env nVal (Just (gnf env tyv))
pure (fst c, snd c, rigMult rigl rigc))
r
_ => do c <- check (rigl |*| rigc)
elabinfo -- without preciseInf
nest env nVal (Just (gnf env tyv))
@ -229,3 +229,11 @@ checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty {vars}
-- build the term directly
pure (Bind fc n (Let rigb valv tyv) scopev,
gnf env (Bind fc n (Let rigb valv tyv) scopet))
where
linearErr : Error -> Maybe RigCount
linearErr (LinearMisuse _ _ r _) = Just r
linearErr (InType _ _ e) = linearErr e
linearErr (InCon _ _ e) = linearErr e
linearErr (InLHS _ _ e) = linearErr e
linearErr (InRHS _ _ e) = linearErr e
linearErr _ = Nothing

1
src/TTImp/Elab/Delayed.idr
View File

@ -179,6 +179,7 @@ recoverable (CantSolveEq _ env l r)
= do defs <- get Ctxt
pure $ not !(contra defs !(nf defs env l) !(nf defs env r))
recoverable (UndefinedName _ _) = pure False
recoverable (LinearMisuse _ _ _ _) = pure False
recoverable (InType _ _ err) = recoverable err
recoverable (InCon _ _ err) = recoverable err
recoverable (InLHS _ _ err) = recoverable err