mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2025-01-02 17:52:09 +03:00
Don't allow nested delays
This makes the rules for ambiguous names a lot more restrictive (but I think that's probably good...)
This commit is contained in:
Edwin Brady
parent
f3c31f3089
commit
2536b03e84
@ -66,14 +66,16 @@ record UState where
|
||||
constraints : IntMap Constraint -- map for finding constraints by ID
|
||||
nextName : Int
|
||||
nextConstraint : Int
|
||||
delayedElab : IntMap (Core ClosedTerm)
|
||||
delayedElab : List (Int, Core ClosedTerm)
|
||||
-- Elaborators which we need to try again later, because
|
||||
-- we didn't have enough type information to elaborate
|
||||
-- successfully yet
|
||||
-- successfully yet.
|
||||
-- The 'Int' is the resolved name. Delays can't be nested,
|
||||
-- so we just process them in order.
|
||||
|
||||
export
|
||||
initUState : UState
|
||||
initUState = MkUState empty empty empty empty 0 0 empty
|
||||
initUState = MkUState empty empty empty empty 0 0 []
|
||||
|
||||
export
|
||||
data UST : Type where
|
||||
@ -335,8 +337,8 @@ newDelayed : {auto u : Ref UST UState} ->
|
||||
newDelayed {vars} fc rig env n ty
|
||||
= do let hty = abstractEnvType fc env ty
|
||||
let hole = newDef fc n rig hty Public Delayed
|
||||
log 10 $ "Added delayed elaborator " ++ show n
|
||||
idx <- addDef n hole
|
||||
log 10 $ "Added delayed elaborator " ++ show (n, idx)
|
||||
addHoleName fc n idx
|
||||
pure (idx, Meta fc n idx envArgs)
|
||||
where
|
||||
|
||||
@ -17,6 +17,15 @@ getRigNeeded InType = Rig0 -- unrestricted usage in types
|
||||
getRigNeeded (InLHS Rig0) = Rig0
|
||||
getRigNeeded _ = Rig1
|
||||
|
||||
data ElabOpts
|
||||
= HolesOkay
|
||||
| InCase
|
||||
|
||||
Eq ElabOpts where
|
||||
HolesOkay == HolesOkay = True
|
||||
InCase == InCase = True
|
||||
_ == _ = False
|
||||
|
||||
export
|
||||
elabTerm : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
@ -40,7 +49,10 @@ elabTerm defining mode env tm ty
|
||||
solveConstraints solvemode Normal
|
||||
solveConstraints solvemode Normal
|
||||
logTerm 5 "Looking for delayed in " chktm
|
||||
retryDelayedIn env chktm
|
||||
ust <- get UST
|
||||
retryDelayed (delayedElab ust)
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab = [] } ust)
|
||||
-- As long as we're not in a case block, finish off constraint solving
|
||||
when (not incase) $
|
||||
-- resolve any default hints
|
||||
|
||||
@ -87,13 +87,14 @@ record EState (vars : List Name) where
|
||||
allPatVars : List Name
|
||||
-- Holes standing for pattern variables, which we'll delete
|
||||
-- once we're done elaborating
|
||||
allowDelay : Bool -- Delaying elaborators is okay. We can't nest delays.
|
||||
|
||||
export
|
||||
data EST : Type where
|
||||
|
||||
export
|
||||
initEStateSub : Int -> Env Term outer -> SubVars outer vars -> EState vars
|
||||
initEStateSub n env sub = MkEState n env sub [] [] [] [] []
|
||||
initEStateSub n env sub = MkEState n env sub [] [] [] [] [] True
|
||||
|
||||
export
|
||||
initEState : Int -> Env Term vars -> EState vars
|
||||
@ -111,7 +112,8 @@ weakenedEState {e}
|
||||
(map wknTms (toBind est))
|
||||
(bindIfUnsolved est)
|
||||
(lhsPatVars est)
|
||||
(allPatVars est))
|
||||
(allPatVars est)
|
||||
(allowDelay est))
|
||||
pure eref
|
||||
where
|
||||
wknTms : (Name, ImplBinding vs) ->
|
||||
@ -138,7 +140,8 @@ strengthenedEState {n} {vars} c e fc env
|
||||
todo
|
||||
(bindIfUnsolved est)
|
||||
(lhsPatVars est)
|
||||
(allPatVars est))
|
||||
(allPatVars est)
|
||||
(allowDelay est))
|
||||
where
|
||||
dropSub : SubVars xs (y :: ys) -> Core (SubVars xs ys)
|
||||
dropSub (DropCons sub) = pure sub
|
||||
@ -187,6 +190,7 @@ updateEnv env sub bif st
|
||||
(boundNames st) (toBind st) bif
|
||||
(lhsPatVars st)
|
||||
(allPatVars st)
|
||||
(allowDelay st)
|
||||
|
||||
export
|
||||
addBindIfUnsolved : Name -> RigCount -> Env Term vars -> Term vars -> Term vars ->
|
||||
@ -198,6 +202,7 @@ addBindIfUnsolved hn r env tm ty st
|
||||
((hn, r, (_ ** (env, tm, ty, subEnv st))) :: bindIfUnsolved st)
|
||||
(lhsPatVars st)
|
||||
(allPatVars st)
|
||||
(allowDelay st)
|
||||
|
||||
clearBindIfUnsolved : EState vars -> EState vars
|
||||
clearBindIfUnsolved st
|
||||
@ -206,6 +211,7 @@ clearBindIfUnsolved st
|
||||
(boundNames st) (toBind st) []
|
||||
(lhsPatVars st)
|
||||
(allPatVars st)
|
||||
(allowDelay st)
|
||||
|
||||
-- Clear the 'toBind' list, except for the names given
|
||||
export
|
||||
|
||||
@ -53,7 +53,8 @@ delayOnFailure : {auto c : Ref Ctxt Defs} ->
|
||||
delayOnFailure fc rig env expected pred elab
|
||||
= handle (elab False)
|
||||
(\err =>
|
||||
do if pred err
|
||||
do est <- get EST
|
||||
if pred err && allowDelay est
|
||||
then
|
||||
do nm <- genName "delayed"
|
||||
(ci, dtm) <- newDelayed fc rig env nm !(getTerm expected)
|
||||
@ -61,52 +62,29 @@ delayOnFailure fc rig env expected pred elab
|
||||
" for") env expected
|
||||
log 10 ("Due to error " ++ show err)
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab $= insert ci
|
||||
(mkClosedElab fc env (elab True)) }
|
||||
put UST (record { delayedElab $=
|
||||
((ci, mkClosedElab fc env
|
||||
(do est <- get EST
|
||||
put EST (record { allowDelay = False } est)
|
||||
tm <- elab True
|
||||
put EST (record { allowDelay = True } est)
|
||||
pure tm)) :: ) }
|
||||
ust)
|
||||
pure (dtm, expected)
|
||||
else throw err)
|
||||
|
||||
export
|
||||
retryDelayedIn : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
Env Term vars -> Term vars ->
|
||||
Core ()
|
||||
retryDelayedIn env (Meta fc n i args)
|
||||
= do traverse (retryDelayedIn env) args
|
||||
defs <- get Ctxt
|
||||
case !(lookupDefExact (Resolved i) (gamma defs)) of
|
||||
Just Delayed =>
|
||||
do ust <- get UST
|
||||
log 10 $ "Retrying " ++ show n
|
||||
let Just elab = lookup i (delayedElab ust)
|
||||
| Nothing => pure ()
|
||||
tm <- elab
|
||||
-- On success, look for delayed holes in the result
|
||||
retryDelayedIn env (embed tm)
|
||||
updateDef (Resolved i) (const (Just
|
||||
(PMDef [] (STerm tm) (STerm tm) [])))
|
||||
logTerm 5 ("Resolved delayed hole " ++ show n) tm
|
||||
removeHole i
|
||||
-- Also look for delayed names inside guarded definitions.
|
||||
-- This helps with error messages because it shows any
|
||||
-- problems in delayed elaborators before the constraint
|
||||
-- failure, and it might also solve some constraints
|
||||
Just (Guess g cs) => retryDelayedIn env (embed g)
|
||||
_ => pure ()
|
||||
retryDelayedIn env (Bind fc x b sc)
|
||||
= do traverse (retryDelayedIn env) b
|
||||
inScope fc (b :: env)
|
||||
(\e' => retryDelayedIn {e=e'} (b :: env) sc)
|
||||
retryDelayedIn env (App fc fn p arg)
|
||||
= do retryDelayedIn env fn
|
||||
retryDelayedIn env arg
|
||||
retryDelayedIn env (As fc as pat)
|
||||
= do retryDelayedIn env as
|
||||
retryDelayedIn env pat
|
||||
retryDelayedIn env (TDelayed fc r tm) = retryDelayedIn env tm
|
||||
retryDelayedIn env (TDelay fc r tm) = retryDelayedIn env tm
|
||||
retryDelayedIn env (TForce fc tm) = retryDelayedIn env tm
|
||||
retryDelayedIn env tm = pure ()
|
||||
retryDelayed : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
List (Int, Core ClosedTerm) ->
|
||||
Core ()
|
||||
retryDelayed [] = pure ()
|
||||
retryDelayed ((i, elab) :: ds)
|
||||
= do tm <- elab
|
||||
updateDef (Resolved i) (const (Just
|
||||
(PMDef [] (STerm tm) (STerm tm) [])))
|
||||
logTerm 5 ("Resolved delayed hole " ++ show i) tm
|
||||
removeHole i
|
||||
retryDelayed ds
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user