mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-25 13:54:55 +03:00
Don't keep running delayed elaborators
Also fix a bug where the elaborator state wasn't updated on completing the delayed elaborator, which could cause issues with implicitly bound names in particular.
This commit is contained in:
Edwin Brady
parent
8d6b990157
commit
ecb5cb1e40
@ -883,7 +883,7 @@ public export
|
||||
isHexDigit : Char -> Bool
|
||||
isHexDigit x = elem (toUpper x) hexChars where
|
||||
hexChars : List Char
|
||||
hexChars
|
||||
hexChars
|
||||
= ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
|
||||
'A', 'B', 'C', 'D', 'E', 'F']
|
||||
|
||||
@ -983,7 +983,7 @@ showLitChar c
|
||||
else strCons c
|
||||
where
|
||||
asciiTab : List String
|
||||
asciiTab
|
||||
asciiTab
|
||||
= ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",
|
||||
"BS", "HT", "LF", "VT", "FF", "CR", "SO", "SI",
|
||||
"DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",
|
||||
|
||||
@ -381,15 +381,12 @@ export
|
||||
traverse : (a -> Core b) -> List a -> Core (List b)
|
||||
traverse f xs = traverse' f xs []
|
||||
|
||||
traverse_' : (a -> Core b) -> List a -> Core ()
|
||||
traverse_' f [] = pure ()
|
||||
traverse_' f (x :: xs)
|
||||
= do f x
|
||||
traverse_' f xs
|
||||
|
||||
export
|
||||
traverse_ : (a -> Core b) -> List a -> Core ()
|
||||
traverse_ f xs = traverse_' f xs
|
||||
traverse_ f [] = pure ()
|
||||
traverse_ f (x :: xs)
|
||||
= do f x
|
||||
traverse_ f xs
|
||||
|
||||
namespace Binder
|
||||
export
|
||||
|
||||
@ -295,7 +295,6 @@ patternEnvTm {vars} env args
|
||||
-- and returning the term
|
||||
-- If the type of the metavariable doesn't have enough arguments, fail, because
|
||||
-- this wasn't valid for pattern unification
|
||||
export
|
||||
instantiate : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{newvars : _} ->
|
||||
@ -379,6 +378,28 @@ instantiate {newvars} loc env mname mref mdef locs otm tm
|
||||
pure (Bind bfc x (Lam c Explicit (Erased bfc)) sc')
|
||||
mkDef got (vs ++ [v]) (Snoc rec) cvs locs tm ty
|
||||
= ufail loc $ "Can't make solution for " ++ show mname
|
||||
|
||||
export
|
||||
solveIfUndefined : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Env Term vars -> Term vars -> Term vars -> Core Bool
|
||||
solveIfUndefined env (Meta fc mname idx args) soln
|
||||
= do defs <- get Ctxt
|
||||
Just (Hole _ _) <- lookupDefExact (Resolved idx) (gamma defs)
|
||||
| pure False
|
||||
case !(patternEnvTm env args) of
|
||||
Nothing => pure False
|
||||
Just (newvars ** (locs, submv)) =>
|
||||
case shrinkTerm soln submv of
|
||||
Nothing => pure False
|
||||
Just stm =>
|
||||
do Just hdef <- lookupCtxtExact (Resolved idx) (gamma defs)
|
||||
| Nothing => throw (InternalError "Can't happen: no definition")
|
||||
instantiate fc env mname idx hdef locs soln stm
|
||||
pure True
|
||||
solveIfUndefined env metavar soln
|
||||
= pure False
|
||||
|
||||
isDefInvertible : {auto c : Ref Ctxt Defs} ->
|
||||
Int -> Core Bool
|
||||
@ -945,14 +966,18 @@ mutual
|
||||
then do log 10 $ "Skipped unification (equal already): "
|
||||
++ show x ++ " and " ++ show y
|
||||
pure success
|
||||
else unify mode loc env !(nf defs env x) !(nf defs env y)
|
||||
else do xnf <- nf defs env x
|
||||
ynf <- nf defs env y
|
||||
unify mode loc env xnf ynf
|
||||
unifyWithLazyD _ _ mode loc env x y
|
||||
= do defs <- get Ctxt
|
||||
if x == y
|
||||
then do log 10 $ "Skipped unification (equal already): "
|
||||
++ show x ++ " and " ++ show y
|
||||
pure success
|
||||
else unifyWithLazy mode loc env !(nf defs env x) !(nf defs env y)
|
||||
else do xnf <- nf defs env x
|
||||
ynf <- nf defs env y
|
||||
unifyWithLazy mode loc env xnf ynf
|
||||
|
||||
export
|
||||
Unify Closure where
|
||||
|
||||
@ -177,27 +177,6 @@ mutual
|
||||
checkAppWith rig elabinfo nest env fc
|
||||
fntm fnty expargs impargs kr expty
|
||||
|
||||
solveIfUndefined : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Env Term vars -> Term vars -> Term vars -> Core Bool
|
||||
solveIfUndefined env (Meta fc mname idx args) soln
|
||||
= do defs <- get Ctxt
|
||||
Just (Hole _ _) <- lookupDefExact (Resolved idx) (gamma defs)
|
||||
| pure False
|
||||
case !(patternEnvTm env args) of
|
||||
Nothing => pure False
|
||||
Just (newvars ** (locs, submv)) =>
|
||||
case shrinkTerm soln submv of
|
||||
Nothing => pure False
|
||||
Just stm =>
|
||||
do Just hdef <- lookupCtxtExact (Resolved idx) (gamma defs)
|
||||
| Nothing => throw (InternalError "Can't happen: no definition")
|
||||
instantiate fc env mname idx hdef locs soln stm
|
||||
pure True
|
||||
solveIfUndefined env metavar soln
|
||||
= pure False
|
||||
|
||||
-- Defer elaborating anything which will be easier given a known target
|
||||
-- type (ambiguity, cases, etc)
|
||||
needsDelay : {auto c : Ref Ctxt Defs} ->
|
||||
|
||||
@ -259,7 +259,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
|
||||
|
||||
est <- get EST
|
||||
fullImps_in <- getToBind fc (elabMode elabinfo)
|
||||
(implicitMode elabinfo) env [] scrtm
|
||||
(implicitMode elabinfo) env []
|
||||
let fullImps = mapMaybe (shrinkImp (subEnv est)) fullImps_in
|
||||
log 5 $ "Doing a case under unbound implicits " ++ show fullImps
|
||||
|
||||
|
||||
@ -68,6 +68,7 @@ delayOnFailure fc rig env expected pred elab
|
||||
(do est <- get EST
|
||||
put EST (record { allowDelay = False } est)
|
||||
tm <- elab True
|
||||
est <- get EST
|
||||
put EST (record { allowDelay = True } est)
|
||||
pure tm)) :: ) }
|
||||
ust)
|
||||
@ -82,7 +83,10 @@ retryDelayed : {auto c : Ref Ctxt Defs} ->
|
||||
Core ()
|
||||
retryDelayed [] = pure ()
|
||||
retryDelayed ((i, elab) :: ds)
|
||||
= do tm <- elab
|
||||
= do defs <- get Ctxt
|
||||
Just Delayed <- lookupDefExact (Resolved i) (gamma defs)
|
||||
| _ => retryDelayed ds
|
||||
tm <- elab
|
||||
updateDef (Resolved i) (const (Just
|
||||
(PMDef [] (STerm tm) (STerm tm) [])))
|
||||
logTerm 5 ("Resolved delayed hole " ++ show i) tm
|
||||
|
||||
@ -318,11 +318,11 @@ export
|
||||
getToBind : {auto c : Ref Ctxt Defs} -> {auto e : Ref EST (EState vars)} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> ElabMode -> BindMode ->
|
||||
Env Term vars -> (excepts : List Name) -> Term vars ->
|
||||
Env Term vars -> (excepts : List Name) ->
|
||||
Core (List (Name, ImplBinding vars))
|
||||
getToBind fc elabmode NONE env excepts toptom
|
||||
getToBind fc elabmode NONE env excepts
|
||||
= pure [] -- We should probably never get here, but for completeness...
|
||||
getToBind {vars} fc elabmode impmode env excepts toptm
|
||||
getToBind {vars} fc elabmode impmode env excepts
|
||||
= do solveConstraints (case elabmode of
|
||||
InLHS _ => InLHS
|
||||
_ => InTerm) Normal
|
||||
@ -504,16 +504,19 @@ checkBindHere rig elabinfo nest env fc bindmode tm exp
|
||||
throw err)
|
||||
checkDots -- Check dot patterns unifying with the claimed thing
|
||||
-- before binding names
|
||||
|
||||
logTerm 5 "Binding names" tmv
|
||||
logTermNF 5 "Normalised" env tmv
|
||||
argImps <- getToBind fc (elabMode elabinfo)
|
||||
bindmode env dontbind tmv
|
||||
bindmode env dontbind
|
||||
clearToBind dontbind
|
||||
defs <- get Ctxt
|
||||
est <- get EST
|
||||
put EST (updateEnv oldenv oldsub oldbif
|
||||
(record { boundNames = [] } est))
|
||||
ty <- getTerm tmt
|
||||
defs <- get Ctxt
|
||||
(bv, bt) <- bindImplicits fc bindmode
|
||||
defs env argImps
|
||||
defs env argImps
|
||||
!(normaliseHoles defs env tmv)
|
||||
!(normaliseHoles defs env ty)
|
||||
traverse_ implicitBind (map fst argImps)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user