mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 11:05:17 +03:00
Don't calculate blocked metavariable set
With the new representation of postponed problems, this is now either not worth doing, or much more expensive than just having another crack at the problem anyway. So let's not calculate it. This makes the libraries built a couple of seconds quicker for me, and I have one example where a program that previously took minutes now type checks in seconds... Might revisit this later, if it turns out to be a potential source of optimisations, but it'll need to be done an entirely different way.
This commit is contained in:
Edwin Brady
parent
5ac441ac05
commit
e3fa0711e3
@ -210,10 +210,9 @@ getMetaNames tm
|
||||
postpone : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
(blockedMeta : Bool) ->
|
||||
FC -> UnifyInfo -> String ->
|
||||
Env Term vars -> NF vars -> NF vars -> Core UnifyResult
|
||||
postpone blockedMetas loc mode logstr env x y
|
||||
postpone loc mode logstr env x y
|
||||
= do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
logC "unify.postpone" 10 $
|
||||
@ -226,19 +225,9 @@ postpone blockedMetas loc mode logstr env x y
|
||||
checkDefined defs x
|
||||
checkDefined defs y
|
||||
|
||||
-- Need to find all the metas in the constraint since solving any one
|
||||
-- of them might stop the constraint being blocked.
|
||||
metas <-
|
||||
if blockedMetas
|
||||
then do let xmetas = getMetas x
|
||||
let ymetas = addMetas xmetas y
|
||||
chaseMetas (keys ymetas) NameMap.empty
|
||||
else pure []
|
||||
blocked <- filterM undefinedN metas
|
||||
c <- addConstraint (MkConstraint loc (atTop mode) blocked env x y)
|
||||
c <- addConstraint (MkConstraint loc (atTop mode) env x y)
|
||||
log "unify.postpone" 10 $
|
||||
show c ++ " NEW CONSTRAINT " ++ show loc ++
|
||||
" blocked on " ++ show metas
|
||||
show c ++ " NEW CONSTRAINT " ++ show loc
|
||||
logNF "unify.postpone" 10 "X" env x
|
||||
logNF "unify.postpone" 10 "Y" env y
|
||||
pure (constrain c)
|
||||
@ -262,12 +251,12 @@ postpone blockedMetas loc mode logstr env x y
|
||||
postponeS : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Bool -> Bool -> FC -> UnifyInfo -> String -> Env Term vars ->
|
||||
Bool -> FC -> UnifyInfo -> String -> Env Term vars ->
|
||||
NF vars -> NF vars ->
|
||||
Core UnifyResult
|
||||
postponeS b s loc mode logstr env x y
|
||||
= if s then postpone b loc (lower mode) logstr env y x
|
||||
else postpone b loc mode logstr env x y
|
||||
postponeS s loc mode logstr env x y
|
||||
= if s then postpone loc (lower mode) logstr env y x
|
||||
else postpone loc mode logstr env x y
|
||||
|
||||
unifyArgs : (Unify tm, Quote tm) =>
|
||||
{vars : _} ->
|
||||
@ -661,8 +650,7 @@ mutual
|
||||
if !(convert defs env x y)
|
||||
then pure success
|
||||
else if post
|
||||
then postpone True
|
||||
loc mode ("Postponing unifyIfEq " ++
|
||||
then postpone loc mode ("Postponing unifyIfEq " ++
|
||||
show (atTop mode)) env x y
|
||||
else convertError loc env x y
|
||||
|
||||
@ -743,14 +731,14 @@ mutual
|
||||
(con (reverse fargs))
|
||||
(NApp fc (NMeta mname mref margs) (reverse $ map (EmptyFC,) hargs))
|
||||
pure (union ures uargs))
|
||||
(postponeS True swap fc mode "Postponing hole application [1]" env
|
||||
(postponeS swap fc mode "Postponing hole application [1]" env
|
||||
(NApp fc (NMeta mname mref margs) $ map (EmptyFC,) margs')
|
||||
(con args'))
|
||||
_ => postponeS True swap fc mode "Postponing hole application [2]" env
|
||||
_ => postponeS swap fc mode "Postponing hole application [2]" env
|
||||
(NApp fc (NMeta mname mref margs) (map (EmptyFC,) margs'))
|
||||
(con args')
|
||||
else -- TODO: Cancellable function applications
|
||||
postpone True fc mode "Postponing hole application [3]" env
|
||||
postpone fc mode "Postponing hole application [3]" env
|
||||
(NApp fc (NMeta mname mref margs) (map (EmptyFC,) margs')) (con args')
|
||||
|
||||
-- Unify a hole application - we have already checked that the hole is
|
||||
@ -785,7 +773,7 @@ mutual
|
||||
if inv
|
||||
then unifyInvertible swap (lower mode) loc env mname mref margs margs' Nothing
|
||||
(NApp nfc (NMeta n i margs2)) args2'
|
||||
else postponeS True swap loc mode "Postponing hole application" env
|
||||
else postponeS swap loc mode "Postponing hole application" env
|
||||
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') tm
|
||||
where
|
||||
isPatName : Name -> Bool
|
||||
@ -793,7 +781,7 @@ mutual
|
||||
isPatName _ = False
|
||||
|
||||
unifyHoleApp swap mode loc env mname mref margs margs' tm
|
||||
= postponeS True swap loc mode "Postponing hole application" env
|
||||
= postponeS swap loc mode "Postponing hole application" env
|
||||
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') tm
|
||||
|
||||
postponePatVar : {auto c : Ref Ctxt Defs} ->
|
||||
@ -811,8 +799,7 @@ mutual
|
||||
defs <- get Ctxt
|
||||
if !(convert defs env x tm)
|
||||
then pure success
|
||||
else postponeS False -- it's not the metavar that's blocked
|
||||
swap loc mode "Not in pattern fragment" env
|
||||
else postponeS swap loc mode "Not in pattern fragment" env
|
||||
x tm
|
||||
|
||||
solveHole : {auto c : Ref Ctxt Defs} ->
|
||||
@ -885,7 +872,7 @@ mutual
|
||||
do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs)
|
||||
| _ => postponePatVar swap mode loc env mname mref margs margs' tmnf
|
||||
let Hole _ _ = definition hdef
|
||||
| _ => postponeS True swap loc mode "Delayed hole" env
|
||||
| _ => postponeS swap loc mode "Delayed hole" env
|
||||
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
|
||||
tmnf
|
||||
tmq <- quote empty env tmnf
|
||||
@ -895,7 +882,7 @@ mutual
|
||||
then quote defs env tmnf
|
||||
else pure tmq
|
||||
Just tm <- occursCheck loc env mode mname tm
|
||||
| _ => postponeS True swap loc mode "Occurs check failed" env
|
||||
| _ => postponeS swap loc mode "Occurs check failed" env
|
||||
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
|
||||
tmnf
|
||||
|
||||
@ -906,7 +893,7 @@ mutual
|
||||
Nothing =>
|
||||
do tm' <- quote defs env tmnf
|
||||
case shrinkTerm tm' submv of
|
||||
Nothing => postponeS True swap loc mode "Can't shrink" env
|
||||
Nothing => postponeS swap loc mode "Can't shrink" env
|
||||
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
|
||||
tmnf
|
||||
Just stm => solveHole fc mode env mname mref
|
||||
@ -936,7 +923,7 @@ mutual
|
||||
unifyApp swap mode loc env xfc (NLocal rx x xp) [] (NApp yfc (NLocal ry y yp) [])
|
||||
= do gam <- get Ctxt
|
||||
if x == y then pure success
|
||||
else postponeS True swap loc mode "Postponing var"
|
||||
else postponeS swap loc mode "Postponing var"
|
||||
env (NApp xfc (NLocal rx x xp) [])
|
||||
(NApp yfc (NLocal ry y yp) [])
|
||||
-- A local against something canonical (binder or constructor) is bad
|
||||
@ -956,13 +943,13 @@ mutual
|
||||
= do gam <- get Ctxt
|
||||
if !(convert gam env (NApp fc hd args) tm)
|
||||
then pure success
|
||||
else postponeS True False loc mode "Postponing constraint"
|
||||
else postponeS False loc mode "Postponing constraint"
|
||||
env (NApp fc hd args) tm
|
||||
unifyApp True mode loc env fc hd args tm
|
||||
= do gam <- get Ctxt
|
||||
if !(convert gam env tm (NApp fc hd args))
|
||||
then pure success
|
||||
else postponeS True True loc mode "Postponing constraint"
|
||||
else postponeS True loc mode "Postponing constraint"
|
||||
env (NApp fc hd args) tm
|
||||
|
||||
unifyBothApps : {auto c : Ref Ctxt Defs} ->
|
||||
@ -982,7 +969,7 @@ mutual
|
||||
unifyBothApps mode@(MkUnifyInfo p InTerm) loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
|
||||
= if x == y
|
||||
then unifyArgs mode loc env (map snd xargs) (map snd yargs)
|
||||
else postpone True loc mode "Postponing local app"
|
||||
else postpone loc mode "Postponing local app"
|
||||
env (NApp xfc (NLocal xr x xp) xargs)
|
||||
(NApp yfc (NLocal yr y yp) yargs)
|
||||
unifyBothApps mode loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
|
||||
@ -1279,8 +1266,7 @@ mutual
|
||||
= if isHoleApp tmy && not (umode mode == InMatch)
|
||||
-- given type delayed, expected unknown, so let's wait and see
|
||||
-- what the expected type turns out to be
|
||||
then postpone True
|
||||
loc mode "Postponing in lazy" env x tmy
|
||||
then postpone loc mode "Postponing in lazy" env x tmy
|
||||
else do vs <- unify (lower mode) loc env tmx tmy
|
||||
pure (record { addLazy = AddForce r } vs)
|
||||
unifyWithLazyD _ _ mode loc env tmx (NDelayed _ r tmy)
|
||||
@ -1355,37 +1341,28 @@ retry mode c
|
||||
case lookup c (constraints ust) of
|
||||
Nothing => pure success
|
||||
Just Resolved => pure success
|
||||
Just (MkConstraint loc withLazy blocked env xold yold)
|
||||
Just (MkConstraint loc withLazy env xold yold)
|
||||
=> do defs <- get Ctxt
|
||||
x <- continueNF defs env xold
|
||||
y <- continueNF defs env yold
|
||||
if umode mode /= InTerm ||
|
||||
!(anyM definedN blocked) || isNil blocked
|
||||
-- only go if any of the blocked names are defined now
|
||||
then
|
||||
catch
|
||||
(do logNF "unify.retry" 5 ("Retrying " ++ show c ++ " " ++ show (umode mode)) env x
|
||||
logNF "unify.retry" 5 "....with" env y
|
||||
log "unify.retry" 5 $ if withLazy
|
||||
then "(lazy allowed)"
|
||||
else "(no lazy)"
|
||||
cs <- ifThenElse withLazy
|
||||
(unifyWithLazy mode loc env x y)
|
||||
(unify (lower mode) loc env x y)
|
||||
case constraints cs of
|
||||
[] => do log "unify.retry" 5 $ "Success " ++ show (addLazy cs)
|
||||
deleteConstraint c
|
||||
pure cs
|
||||
_ => do log "unify.retry" 5 $ "Constraints " ++ show (addLazy cs)
|
||||
pure cs)
|
||||
(\err => do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
throw (WhenUnifying loc env !(quote empty env x) !(quote empty env y) err))
|
||||
else
|
||||
do log "unify.retry" 10 $ show c ++ " still blocked on " ++ show blocked
|
||||
logNF "unify.retry" 10 "X" env x
|
||||
logNF "unify.retry" 10 "Y" env y
|
||||
pure (constrain c)
|
||||
catch
|
||||
(do logNF "unify.retry" 5 ("Retrying " ++ show c ++ " " ++ show (umode mode)) env x
|
||||
logNF "unify.retry" 5 "....with" env y
|
||||
log "unify.retry" 5 $ if withLazy
|
||||
then "(lazy allowed)"
|
||||
else "(no lazy)"
|
||||
cs <- ifThenElse withLazy
|
||||
(unifyWithLazy mode loc env x y)
|
||||
(unify (lower mode) loc env x y)
|
||||
case constraints cs of
|
||||
[] => do log "unify.retry" 5 $ "Success " ++ show (addLazy cs)
|
||||
deleteConstraint c
|
||||
pure cs
|
||||
_ => do log "unify.retry" 5 $ "Constraints " ++ show (addLazy cs)
|
||||
pure cs)
|
||||
(\err => do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
throw (WhenUnifying loc env !(quote empty env x) !(quote empty env y) err))
|
||||
Just (MkSeqConstraint loc env xsold ysold)
|
||||
=> do defs <- get Ctxt
|
||||
xs <- traverse (continueNF defs env) xsold
|
||||
@ -1593,7 +1570,7 @@ checkDots
|
||||
pure (Just n')
|
||||
|
||||
checkConstraint : (Name, DotReason, Constraint) -> Core ()
|
||||
checkConstraint (n, reason, MkConstraint fc wl blocked env xold yold)
|
||||
checkConstraint (n, reason, MkConstraint fc wl env xold yold)
|
||||
= do defs <- get Ctxt
|
||||
x <- continueNF defs env xold
|
||||
y <- continueNF defs env yold
|
||||
|
||||
@ -28,7 +28,6 @@ data Constraint : Type where
|
||||
MkConstraint : {vars : _} ->
|
||||
FC ->
|
||||
(withLazy : Bool) ->
|
||||
(blockedOn : List Name) ->
|
||||
(env : Env Term vars) ->
|
||||
(x : NF vars) -> (y : NF vars) ->
|
||||
Constraint
|
||||
@ -279,7 +278,7 @@ addDot fc env dotarg x reason y
|
||||
xnf <- nf defs env x
|
||||
ynf <- nf defs env y
|
||||
put UST (record { dotConstraints $=
|
||||
((dotarg, reason, MkConstraint fc False [] env xnf ynf) ::)
|
||||
((dotarg, reason, MkConstraint fc False env xnf ynf) ::)
|
||||
} ust)
|
||||
|
||||
mkConstantAppArgs : {vars : _} ->
|
||||
@ -562,7 +561,7 @@ checkValidHole base (idx, (fc, n))
|
||||
let Just c = lookup con (constraints ust)
|
||||
| Nothing => pure ()
|
||||
case c of
|
||||
MkConstraint fc l blocked env x y =>
|
||||
MkConstraint fc l env x y =>
|
||||
do put UST (record { guesses = empty } ust)
|
||||
empty <- clearDefs defs
|
||||
xnf <- quote empty env x
|
||||
@ -672,7 +671,7 @@ dumpHole' lvl hole
|
||||
case lookup n (constraints ust) of
|
||||
Nothing => pure ()
|
||||
Just Resolved => log' lvl "\tResolved"
|
||||
Just (MkConstraint _ lazy _ env x y) =>
|
||||
Just (MkConstraint _ lazy env x y) =>
|
||||
do log' lvl $ "\t " ++ show !(toFullNames !(quote defs env x))
|
||||
++ " =?= " ++ show !(toFullNames !(quote defs env y))
|
||||
empty <- clearDefs defs
|
||||
|
||||
@ -100,64 +100,6 @@ ntCon fc n tag Z [] = case isConstantType n of
|
||||
Nothing => NTCon fc n tag Z []
|
||||
ntCon fc n tag arity args = NTCon fc n tag arity args
|
||||
|
||||
-- Look for metavariables which, if later defined, will help unblock
|
||||
-- reduction
|
||||
mutual
|
||||
export
|
||||
addMetas : NameMap Bool -> NF vars -> NameMap Bool
|
||||
addMetas ns (NBind fc x b sc)
|
||||
= addMetas ns (binderType b) -- we won't be blocked on the scope
|
||||
-- Arguments might be the cause of the blockage here
|
||||
addMetas ns (NApp fc (NMeta n i args) xs)
|
||||
= addMetaArgs (insert n False ns) (args ++ map snd xs)
|
||||
addMetas ns (NApp fc x xs)
|
||||
= addMetaArgs ns (map snd xs)
|
||||
addMetas ns (NDCon fc x tag arity xs)
|
||||
= addMetaArgs ns (map snd xs)
|
||||
addMetas ns (NTCon fc x tag arity xs)
|
||||
= addMetaArgs ns (map snd xs)
|
||||
addMetas ns (NAs fc _ p t)
|
||||
= addMetas (addMetas ns p) t
|
||||
addMetas ns (NDelayed fc x tm)
|
||||
= addMetas ns tm
|
||||
addMetas ns (NDelay fc x t y)
|
||||
= addMetaC (addMetaC ns t) y
|
||||
addMetas ns (NForce fc x t xs)
|
||||
= addMetas (addMetaArgs ns (map snd xs)) t
|
||||
addMetas ns (NPrimVal fc x) = ns
|
||||
addMetas ns (NErased fc imp) = ns
|
||||
addMetas ns (NType fc) = ns
|
||||
|
||||
addEnvMetas : NameMap Bool -> Env Term vars -> NameMap Bool
|
||||
addEnvMetas ns [] = ns
|
||||
addEnvMetas ns (Let _ _ val _ :: env) = addEnvMetas (addMetas ns val) env
|
||||
addEnvMetas ns (_ :: env) = addEnvMetas ns env
|
||||
|
||||
addMetaC : NameMap Bool -> Closure vars ->
|
||||
NameMap Bool
|
||||
addMetaC ns (MkClosure {vars=tvars} opts locs env' tm) = addMetas ns tm
|
||||
addMetaC ns (MkNFClosure x) = addMetas ns x
|
||||
|
||||
addMetaLocalEnv : NameMap Bool -> List (Closure vars) -> NameMap Bool
|
||||
addMetaLocalEnv ns (MkClosure _ locs _ _ :: _)
|
||||
= addMetaArgs ns (getClosures locs)
|
||||
where
|
||||
getClosures : LocalEnv f vs -> List (Closure f)
|
||||
getClosures [] = []
|
||||
getClosures (c :: ls) = c :: getClosures ls
|
||||
addMetaLocalEnv ns (_ :: cs) = addMetaLocalEnv ns cs
|
||||
addMetaLocalEnv ns [] = ns
|
||||
|
||||
addMetaArgs : NameMap Bool -> List (Closure vars) ->
|
||||
NameMap Bool
|
||||
addMetaArgs ns [] = ns
|
||||
addMetaArgs ns (c :: xs)
|
||||
= addMetaLocalEnv (addMetaArgs (addMetaC ns c) xs) (c :: xs)
|
||||
|
||||
export
|
||||
getMetas : NF vars -> NameMap Bool
|
||||
getMetas tm = addMetas empty tm
|
||||
|
||||
export
|
||||
getLoc : NF vars -> FC
|
||||
getLoc (NBind fc _ _ _) = fc
|
||||
|
||||
Loading…
Reference in New Issue
Block a user