mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
[ perf ] make Core.Normalise.Eval.evalDef stack safety
This commit is contained in:
Asafov Alexander
CodingCellist
parent
9bfa04921a
commit
f93c927952
@ -83,6 +83,12 @@ data CaseResult a
|
||||
| NoMatch -- case alternative didn't match anything
|
||||
| GotStuck -- alternative matched, but got stuck later
|
||||
|
||||
record TermWithEnv (free : List Name) where
|
||||
constructor MkTermEnv
|
||||
varsEnv : List Name
|
||||
locEnv : LocalEnv free varsEnv
|
||||
term : Term $ varsEnv ++ free
|
||||
|
||||
parameters (defs : Defs, topopts : EvalOpts)
|
||||
mutual
|
||||
eval : {auto c : Ref Ctxt Defs} ->
|
||||
@ -316,7 +322,7 @@ parameters (defs : Defs, topopts : EvalOpts)
|
||||
getCaseBound (arg :: args) [] loc = Nothing -- mismatched arg length
|
||||
getCaseBound (arg :: args) (n :: ns) loc = (arg ::) <$> getCaseBound args ns loc
|
||||
|
||||
evalConAlt : {auto c : Ref Ctxt Defs} ->
|
||||
conAltTerm : {auto c : Ref Ctxt Defs} ->
|
||||
{more, free : _} ->
|
||||
Env Term free ->
|
||||
LocalEnv free more -> EvalOpts -> FC ->
|
||||
@ -324,59 +330,59 @@ parameters (defs : Defs, topopts : EvalOpts)
|
||||
(args : List Name) ->
|
||||
List (Closure free) ->
|
||||
CaseTree (args ++ more) ->
|
||||
Core (CaseResult (NF free))
|
||||
evalConAlt env loc opts fc stk args args' sc
|
||||
Core (CaseResult (TermWithEnv free))
|
||||
conAltTerm env loc opts fc stk args args' sc
|
||||
= do let Just bound = getCaseBound args' args loc
|
||||
| Nothing => pure GotStuck
|
||||
evalTree env bound opts fc stk sc
|
||||
caseTermTree env bound opts fc stk sc
|
||||
|
||||
tryAlt : {auto c : Ref Ctxt Defs} ->
|
||||
{free, more : _} ->
|
||||
Env Term free ->
|
||||
LocalEnv free more -> EvalOpts -> FC ->
|
||||
Stack free -> NF free -> CaseAlt more ->
|
||||
Core (CaseResult (NF free))
|
||||
Core (CaseResult (TermWithEnv free))
|
||||
-- Dotted values should still reduce at compile time
|
||||
tryAlt {more} env loc opts fc stk (NErased _ (Dotted tm)) alt
|
||||
= tryAlt {more} env loc opts fc stk tm alt
|
||||
-- Ordinary constructor matching
|
||||
tryAlt {more} env loc opts fc stk (NDCon _ nm tag' arity args') (ConCase x tag args sc)
|
||||
= if tag == tag'
|
||||
then evalConAlt env loc opts fc stk args (map snd args') sc
|
||||
then conAltTerm env loc opts fc stk args (map snd args') sc
|
||||
else pure NoMatch
|
||||
-- Type constructor matching, in typecase
|
||||
tryAlt {more} env loc opts fc stk (NTCon _ nm tag' arity args') (ConCase nm' tag args sc)
|
||||
= if nm == nm'
|
||||
then evalConAlt env loc opts fc stk args (map snd args') sc
|
||||
then conAltTerm env loc opts fc stk args (map snd args') sc
|
||||
else pure NoMatch
|
||||
-- Primitive type matching, in typecase
|
||||
tryAlt env loc opts fc stk (NPrimVal _ c) (ConCase nm tag args sc)
|
||||
= case args of -- can't just test for it in the `if` for typing reasons
|
||||
[] => if UN (Basic $ show c) == nm
|
||||
then evalTree env loc opts fc stk sc
|
||||
then caseTermTree env loc opts fc stk sc
|
||||
else pure NoMatch
|
||||
_ => pure NoMatch
|
||||
-- Type of type matching, in typecase
|
||||
tryAlt env loc opts fc stk (NType _ _) (ConCase (UN (Basic "Type")) tag [] sc)
|
||||
= evalTree env loc opts fc stk sc
|
||||
= caseTermTree env loc opts fc stk sc
|
||||
-- Arrow matching, in typecase
|
||||
tryAlt {more}
|
||||
env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase (UN (Basic "->")) tag [s,t] sc)
|
||||
= evalConAlt {more} env loc opts fc stk [s,t]
|
||||
= conAltTerm {more} env loc opts fc stk [s,t]
|
||||
[aty,
|
||||
MkNFClosure opts env (NBind pfc x (Lam fc' r e aty) scty)]
|
||||
sc
|
||||
-- Delay matching
|
||||
tryAlt env loc opts fc stk (NDelay _ _ ty arg) (DelayCase tyn argn sc)
|
||||
= evalTree env (ty :: arg :: loc) opts fc stk sc
|
||||
= caseTermTree env (ty :: arg :: loc) opts fc stk sc
|
||||
-- Constant matching
|
||||
tryAlt env loc opts fc stk (NPrimVal _ c') (ConstCase c sc)
|
||||
= if c == c' then evalTree env loc opts fc stk sc
|
||||
= if c == c' then caseTermTree env loc opts fc stk sc
|
||||
else pure NoMatch
|
||||
-- Default case matches against any *concrete* value
|
||||
tryAlt env loc opts fc stk val (DefaultCase sc)
|
||||
= if concrete val
|
||||
then evalTree env loc opts fc stk sc
|
||||
then caseTermTree env loc opts fc stk sc
|
||||
else pure GotStuck
|
||||
where
|
||||
concrete : NF free -> Bool
|
||||
@ -394,12 +400,12 @@ parameters (defs : Defs, topopts : EvalOpts)
|
||||
Env Term free ->
|
||||
LocalEnv free args -> EvalOpts -> FC ->
|
||||
Stack free -> NF free -> List (CaseAlt args) ->
|
||||
Core (CaseResult (NF free))
|
||||
Core (CaseResult (TermWithEnv free))
|
||||
findAlt env loc opts fc stk val [] = do
|
||||
log "eval.casetree.stuck" 2 "Ran out of alternatives"
|
||||
pure GotStuck
|
||||
findAlt env loc opts fc stk val (x :: xs)
|
||||
= do Result val <- tryAlt env loc opts fc stk val x
|
||||
= do (Result (MkTermEnv vars newLoc val)) <- tryAlt env loc opts fc stk val x
|
||||
| NoMatch => findAlt env loc opts fc stk val xs
|
||||
| GotStuck => do
|
||||
logC "eval.casetree.stuck" 5 $ do
|
||||
@ -407,14 +413,14 @@ parameters (defs : Defs, topopts : EvalOpts)
|
||||
x <- toFullNames x
|
||||
pure $ "Got stuck matching \{show val} against \{show x}"
|
||||
pure GotStuck
|
||||
pure (Result val)
|
||||
pure (Result (MkTermEnv vars newLoc val))
|
||||
|
||||
evalTree : {auto c : Ref Ctxt Defs} ->
|
||||
caseTermTree : {auto c : Ref Ctxt Defs} ->
|
||||
{args, free : _} -> Env Term free -> LocalEnv free args ->
|
||||
EvalOpts -> FC ->
|
||||
Stack free -> CaseTree args ->
|
||||
Core (CaseResult (NF free))
|
||||
evalTree env loc opts fc stk (Case {name} idx x _ alts)
|
||||
Core (CaseResult (TermWithEnv free))
|
||||
caseTermTree env loc opts fc stk (Case {name} idx x _ alts)
|
||||
= do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc
|
||||
-- we have not defined quote yet (it depends on eval itself) so we show the NF
|
||||
-- i.e. only the top-level constructor.
|
||||
@ -423,16 +429,9 @@ parameters (defs : Defs, topopts : EvalOpts)
|
||||
pure "Evaluated \{show name} to \{show xval}"
|
||||
let loc' = updateLocal opts env idx (varExtend x) loc xval
|
||||
findAlt env loc' opts fc stk xval alts
|
||||
evalTree env loc opts fc stk (STerm _ tm)
|
||||
= case fuel opts of
|
||||
Nothing => do res <- evalWithOpts defs opts env loc (embed tm) stk
|
||||
pure (Result res)
|
||||
Just Z => pure GotStuck
|
||||
Just (S k) =>
|
||||
do let opts' = { fuel := Just k } opts
|
||||
res <- evalWithOpts defs opts' env loc (embed tm) stk
|
||||
pure (Result res)
|
||||
evalTree env loc opts fc stk _ = pure GotStuck
|
||||
caseTermTree env loc opts fc stk (STerm _ tm)
|
||||
= pure (Result $ MkTermEnv _ loc $ embed tm)
|
||||
caseTermTree env loc opts fc stk _ = pure GotStuck
|
||||
|
||||
-- Take arguments from the stack, as long as there's enough.
|
||||
-- Returns the arguments, and the rest of the stack
|
||||
@ -507,12 +506,18 @@ parameters (defs : Defs, topopts : EvalOpts)
|
||||
pure "Cannot reduce under-applied \{show def}"
|
||||
pure def
|
||||
Just (locs', stk') =>
|
||||
do Result res <- evalTree env locs' opts fc stk' tree
|
||||
do (Result (MkTermEnv _ newLoc res)) <- caseTermTree env locs' opts fc stk' tree
|
||||
| _ => do logC "eval.def.stuck" 50 $ do
|
||||
def <- toFullNames def
|
||||
pure "evalTree failed on \{show def}"
|
||||
pure "caseTermTree failed on \{show def}"
|
||||
pure def
|
||||
pure res
|
||||
case fuel opts of
|
||||
Nothing => evalWithOpts defs opts env newLoc res stk'
|
||||
Just Z => log "eval.def.stuck" 50 "Recursion depth limit exceeded"
|
||||
>> pure def
|
||||
Just (S k) =>
|
||||
do let opts' = { fuel := Just k } opts
|
||||
evalWithOpts defs opts' env newLoc res stk'
|
||||
else do -- logC "eval.def.stuck" 50 $ do
|
||||
-- def <- toFullNames def
|
||||
-- pure $ unlines [ "Refusing to reduce \{show def}:"
|
||||
|
||||
Loading…
Reference in New Issue
Block a user