idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #1424 from edwinb/micro-optimise

Browse Source 
A couple of small optimisations
This commit is contained in:
Edwin Brady 2021-05-16 21:44:06 +01:00 committed by GitHub
commit 11761daa76
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 56 additions and 131 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Core/CaseBuilder.idr
View File

@ -194,6 +194,10 @@ Weaken ArgType where
weaken (Stuck fty) = Stuck (weaken fty) weaken (Stuck fty) = Stuck (weaken fty)
weaken Unknown = Unknown weaken Unknown = Unknown
weakenNs s (Known c ty) = Known c (weakenNs s ty)
weakenNs s (Stuck fty) = Stuck (weakenNs s fty)
weakenNs s Unknown = Unknown
Weaken (PatInfo p) where Weaken (PatInfo p) where
weaken (MkInfo p el fty) = MkInfo p (Later el) (weaken fty) weaken (MkInfo p el fty) = MkInfo p (Later el) (weaken fty)

7
src/Core/Normalise.idr
View File

@ -216,8 +216,11 @@ parameters (defs : Defs, topopts : EvalOpts)
FC -> Name -> Int -> List (Closure free) -> FC -> Name -> Int -> List (Closure free) ->
Stack free -> Core (NF free) Stack free -> Core (NF free)
evalMeta env fc nm i args stk evalMeta env fc nm i args stk
= evalRef env True fc Func (Resolved i) (map (EmptyFC,) args ++ stk) = let args' = if isNil stk then map (EmptyFC,) args
(NApp fc (NMeta nm i args) stk) else map (EmptyFC,) args ++ stk
in
evalRef env True fc Func (Resolved i) args'
(NApp fc (NMeta nm i args) stk)
-- The commented out logging here might still be useful one day, but -- The commented out logging here might still be useful one day, but
-- evalRef is used a lot and even these tiny checks turn out to be -- evalRef is used a lot and even these tiny checks turn out to be

109
src/Core/Unify.idr
View File

@ -210,10 +210,9 @@ getMetaNames tm
postpone : {vars : _} -> postpone : {vars : _} ->
{auto c : Ref Ctxt Defs} -> {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
(blockedMeta : Bool) ->
FC -> UnifyInfo -> String -> FC -> UnifyInfo -> String ->
Env Term vars -> NF vars -> NF vars -> Core UnifyResult 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 = do defs <- get Ctxt
empty <- clearDefs defs empty <- clearDefs defs
logC "unify.postpone" 10 $ logC "unify.postpone" 10 $
@ -226,19 +225,9 @@ postpone blockedMetas loc mode logstr env x y
checkDefined defs x checkDefined defs x
checkDefined defs y checkDefined defs y
-- Need to find all the metas in the constraint since solving any one c <- addConstraint (MkConstraint loc (atTop mode) env x y)
-- 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)
log "unify.postpone" 10 $ log "unify.postpone" 10 $
show c ++ " NEW CONSTRAINT " ++ show loc ++ show c ++ " NEW CONSTRAINT " ++ show loc
" blocked on " ++ show metas
logNF "unify.postpone" 10 "X" env x logNF "unify.postpone" 10 "X" env x
logNF "unify.postpone" 10 "Y" env y logNF "unify.postpone" 10 "Y" env y
pure (constrain c) pure (constrain c)
@ -262,12 +251,12 @@ postpone blockedMetas loc mode logstr env x y
postponeS : {vars : _} -> postponeS : {vars : _} ->
{auto c : Ref Ctxt Defs} -> {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
Bool -> Bool -> FC -> UnifyInfo -> String -> Env Term vars -> Bool -> FC -> UnifyInfo -> String -> Env Term vars ->
NF vars -> NF vars -> NF vars -> NF vars ->
Core UnifyResult Core UnifyResult
postponeS b s loc mode logstr env x y postponeS s loc mode logstr env x y
= if s then postpone b loc (lower mode) logstr env y x = if s then postpone loc (lower mode) logstr env y x
else postpone b loc mode logstr env x y else postpone loc mode logstr env x y
unifyArgs : (Unify tm, Quote tm) => unifyArgs : (Unify tm, Quote tm) =>
{vars : _} -> {vars : _} ->
@ -661,8 +650,7 @@ mutual
if !(convert defs env x y) if !(convert defs env x y)
then pure success then pure success
else if post else if post
then postpone True then postpone loc mode ("Postponing unifyIfEq " ++
loc mode ("Postponing unifyIfEq " ++
show (atTop mode)) env x y show (atTop mode)) env x y
else convertError loc env x y else convertError loc env x y
@ -743,14 +731,14 @@ mutual
(con (reverse fargs)) (con (reverse fargs))
(NApp fc (NMeta mname mref margs) (reverse $ map (EmptyFC,) hargs)) (NApp fc (NMeta mname mref margs) (reverse $ map (EmptyFC,) hargs))
pure (union ures uargs)) 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') (NApp fc (NMeta mname mref margs) $ map (EmptyFC,) margs')
(con args')) (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')) (NApp fc (NMeta mname mref margs) (map (EmptyFC,) margs'))
(con args') (con args')
else -- TODO: Cancellable function applications 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') (NApp fc (NMeta mname mref margs) (map (EmptyFC,) margs')) (con args')
-- Unify a hole application - we have already checked that the hole is -- Unify a hole application - we have already checked that the hole is
@ -785,7 +773,7 @@ mutual
if inv if inv
then unifyInvertible swap (lower mode) loc env mname mref margs margs' Nothing then unifyInvertible swap (lower mode) loc env mname mref margs margs' Nothing
(NApp nfc (NMeta n i margs2)) args2' (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 (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') tm
where where
isPatName : Name -> Bool isPatName : Name -> Bool
@ -793,7 +781,7 @@ mutual
isPatName _ = False isPatName _ = False
unifyHoleApp swap mode loc env mname mref margs margs' tm 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 (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') tm
postponePatVar : {auto c : Ref Ctxt Defs} -> postponePatVar : {auto c : Ref Ctxt Defs} ->
@ -811,8 +799,7 @@ mutual
defs <- get Ctxt defs <- get Ctxt
if !(convert defs env x tm) if !(convert defs env x tm)
then pure success then pure success
else postponeS False -- it's not the metavar that's blocked else postponeS swap loc mode "Not in pattern fragment" env
swap loc mode "Not in pattern fragment" env
x tm x tm
solveHole : {auto c : Ref Ctxt Defs} -> solveHole : {auto c : Ref Ctxt Defs} ->
@ -865,7 +852,7 @@ mutual
unifyHole swap mode loc env fc mname mref margs margs' tmnf unifyHole swap mode loc env fc mname mref margs margs' tmnf
= do defs <- get Ctxt = do defs <- get Ctxt
empty <- clearDefs defs empty <- clearDefs defs
let args = margs ++ margs' let args = if isNil margs' then margs else margs ++ margs'
logC "unify.hole" 10 logC "unify.hole" 10
(do args' <- traverse (evalArg empty) args (do args' <- traverse (evalArg empty) args
qargs <- traverse (quote empty env) args' qargs <- traverse (quote empty env) args'
@ -885,7 +872,7 @@ mutual
do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs) do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs)
| _ => postponePatVar swap mode loc env mname mref margs margs' tmnf | _ => postponePatVar swap mode loc env mname mref margs margs' tmnf
let Hole _ _ = definition hdef 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') (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
tmnf tmnf
tmq <- quote empty env tmnf tmq <- quote empty env tmnf
@ -895,7 +882,7 @@ mutual
then quote defs env tmnf then quote defs env tmnf
else pure tmq else pure tmq
Just tm <- occursCheck loc env mode mname tm 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') (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
tmnf tmnf
@ -906,7 +893,7 @@ mutual
Nothing => Nothing =>
do tm' <- quote defs env tmnf do tm' <- quote defs env tmnf
case shrinkTerm tm' submv of 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') (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
tmnf tmnf
Just stm => solveHole fc mode env mname mref 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) []) unifyApp swap mode loc env xfc (NLocal rx x xp) [] (NApp yfc (NLocal ry y yp) [])
= do gam <- get Ctxt = do gam <- get Ctxt
if x == y then pure success 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) []) env (NApp xfc (NLocal rx x xp) [])
(NApp yfc (NLocal ry y yp) []) (NApp yfc (NLocal ry y yp) [])
-- A local against something canonical (binder or constructor) is bad -- A local against something canonical (binder or constructor) is bad
@ -956,13 +943,13 @@ mutual
= do gam <- get Ctxt = do gam <- get Ctxt
if !(convert gam env (NApp fc hd args) tm) if !(convert gam env (NApp fc hd args) tm)
then pure success then pure success
else postponeS True False loc mode "Postponing constraint" else postponeS False loc mode "Postponing constraint"
env (NApp fc hd args) tm env (NApp fc hd args) tm
unifyApp True mode loc env fc hd args tm unifyApp True mode loc env fc hd args tm
= do gam <- get Ctxt = do gam <- get Ctxt
if !(convert gam env tm (NApp fc hd args)) if !(convert gam env tm (NApp fc hd args))
then pure success then pure success
else postponeS True True loc mode "Postponing constraint" else postponeS True loc mode "Postponing constraint"
env (NApp fc hd args) tm env (NApp fc hd args) tm
unifyBothApps : {auto c : Ref Ctxt Defs} -> 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 unifyBothApps mode@(MkUnifyInfo p InTerm) loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
= if x == y = if x == y
then unifyArgs mode loc env (map snd xargs) (map snd yargs) 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) env (NApp xfc (NLocal xr x xp) xargs)
(NApp yfc (NLocal yr y yp) yargs) (NApp yfc (NLocal yr y yp) yargs)
unifyBothApps mode loc env xfc (NLocal xr x xp) xargs 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) = if isHoleApp tmy && not (umode mode == InMatch)
-- given type delayed, expected unknown, so let's wait and see -- given type delayed, expected unknown, so let's wait and see
-- what the expected type turns out to be -- what the expected type turns out to be
then postpone True then postpone loc mode "Postponing in lazy" env x tmy
loc mode "Postponing in lazy" env x tmy
else do vs <- unify (lower mode) loc env tmx tmy else do vs <- unify (lower mode) loc env tmx tmy
pure (record { addLazy = AddForce r } vs) pure (record { addLazy = AddForce r } vs)
unifyWithLazyD _ _ mode loc env tmx (NDelayed _ r tmy) unifyWithLazyD _ _ mode loc env tmx (NDelayed _ r tmy)
@ -1355,37 +1341,28 @@ retry mode c
case lookup c (constraints ust) of case lookup c (constraints ust) of
Nothing => pure success Nothing => pure success
Just Resolved => 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 => do defs <- get Ctxt
x <- continueNF defs env xold x <- continueNF defs env xold
y <- continueNF defs env yold y <- continueNF defs env yold
if umode mode /= InTerm || catch
!(anyM definedN blocked) || isNil blocked (do logNF "unify.retry" 5 ("Retrying " ++ show c ++ " " ++ show (umode mode)) env x
-- only go if any of the blocked names are defined now logNF "unify.retry" 5 "....with" env y
then log "unify.retry" 5 $ if withLazy
catch then "(lazy allowed)"
(do logNF "unify.retry" 5 ("Retrying " ++ show c ++ " " ++ show (umode mode)) env x else "(no lazy)"
logNF "unify.retry" 5 "....with" env y cs <- ifThenElse withLazy
log "unify.retry" 5 $ if withLazy (unifyWithLazy mode loc env x y)
then "(lazy allowed)" (unify (lower mode) loc env x y)
else "(no lazy)" case constraints cs of
cs <- ifThenElse withLazy [] => do log "unify.retry" 5 $ "Success " ++ show (addLazy cs)
(unifyWithLazy mode loc env x y) deleteConstraint c
(unify (lower mode) loc env x y) pure cs
case constraints cs of _ => do log "unify.retry" 5 $ "Constraints " ++ show (addLazy cs)
[] => do log "unify.retry" 5 $ "Success " ++ show (addLazy cs) pure cs)
deleteConstraint c (\err => do defs <- get Ctxt
pure cs empty <- clearDefs defs
_ => do log "unify.retry" 5 $ "Constraints " ++ show (addLazy cs) throw (WhenUnifying loc env !(quote empty env x) !(quote empty env y) err))
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)
Just (MkSeqConstraint loc env xsold ysold) Just (MkSeqConstraint loc env xsold ysold)
=> do defs <- get Ctxt => do defs <- get Ctxt
xs <- traverse (continueNF defs env) xsold xs <- traverse (continueNF defs env) xsold
@ -1593,7 +1570,7 @@ checkDots
pure (Just n') pure (Just n')
checkConstraint : (Name, DotReason, Constraint) -> Core () 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 = do defs <- get Ctxt
x <- continueNF defs env xold x <- continueNF defs env xold
y <- continueNF defs env yold y <- continueNF defs env yold

7
src/Core/UnifyState.idr
View File

@ -28,7 +28,6 @@ data Constraint : Type where
MkConstraint : {vars : _} -> MkConstraint : {vars : _} ->
FC -> FC ->
(withLazy : Bool) -> (withLazy : Bool) ->
(blockedOn : List Name) ->
(env : Env Term vars) -> (env : Env Term vars) ->
(x : NF vars) -> (y : NF vars) -> (x : NF vars) -> (y : NF vars) ->
Constraint Constraint
@ -279,7 +278,7 @@ addDot fc env dotarg x reason y
xnf <- nf defs env x xnf <- nf defs env x
ynf <- nf defs env y ynf <- nf defs env y
put UST (record { dotConstraints $= put UST (record { dotConstraints $=
((dotarg, reason, MkConstraint fc False [] env xnf ynf) ::) ((dotarg, reason, MkConstraint fc False env xnf ynf) ::)
} ust) } ust)
mkConstantAppArgs : {vars : _} -> mkConstantAppArgs : {vars : _} ->
@ -562,7 +561,7 @@ checkValidHole base (idx, (fc, n))
let Just c = lookup con (constraints ust) let Just c = lookup con (constraints ust)
| Nothing => pure () | Nothing => pure ()
case c of case c of
MkConstraint fc l blocked env x y => MkConstraint fc l env x y =>
do put UST (record { guesses = empty } ust) do put UST (record { guesses = empty } ust)
empty <- clearDefs defs empty <- clearDefs defs
xnf <- quote empty env x xnf <- quote empty env x
@ -672,7 +671,7 @@ dumpHole' lvl hole
case lookup n (constraints ust) of case lookup n (constraints ust) of
Nothing => pure () Nothing => pure ()
Just Resolved => log' lvl "\tResolved" 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)) do log' lvl $ "\t " ++ show !(toFullNames !(quote defs env x))
++ " =?= " ++ show !(toFullNames !(quote defs env y)) ++ " =?= " ++ show !(toFullNames !(quote defs env y))
empty <- clearDefs defs empty <- clearDefs defs

58
src/Core/Value.idr
View File

@ -100,64 +100,6 @@ ntCon fc n tag Z [] = case isConstantType n of
Nothing => NTCon fc n tag Z [] Nothing => NTCon fc n tag Z []
ntCon fc n tag arity args = NTCon fc n tag arity args 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 export
getLoc : NF vars -> FC getLoc : NF vars -> FC
getLoc (NBind fc _ _ _) = fc getLoc (NBind fc _ _ _) = fc

2
src/TTImp/Elab/App.idr
View File

@ -69,7 +69,7 @@ getNameType rigc env fc x
[(pname, i, def)] <- lookupCtxtName x (gamma defs) [(pname, i, def)] <- lookupCtxtName x (gamma defs)
| [] => undefinedName fc x | [] => undefinedName fc x
| ns => throw (AmbiguousName fc (map fst ns)) | ns => throw (AmbiguousName fc (map fst ns))
checkVisibleNS fc !(getFullName pname) (visibility def) checkVisibleNS fc (fullname def) (visibility def)
rigSafe (multiplicity def) rigc rigSafe (multiplicity def) rigc
let nt = case definition def of let nt = case definition def of
PMDef _ _ _ _ _ => Func PMDef _ _ _ _ _ => Func