Skip to content

Commit 9fbdf56

Browse files
edwinbedwinb
committed
Add CBV mode to the evaluator
I'm not sure how useful this is going to be, but I set it as the default for evaluation at the REPL, since it can save duplicating work. It's not a good choice for evaluation during type checking, since we want to avoid evaluation when we don't need it. Also when we resume suspended unification problems, the context may be different due to solved metavariables, so even if we evaluate early we might still have to evaluate again.
1 parent ff9725b commit 9fbdf56

File tree

3 files changed

+82
-48
lines changed

3 files changed

+82
-48
lines changed

‎src/Core/Normalise.idr

Lines changed: 63 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,10 @@ parameters (defs : Defs, topopts : EvalOpts)
117117
(\defs', arg => evalWithOpts defs' topopts
118118
env (arg :: locs) scope stk)
119119
eval env locs (App fc fn arg) stk
120-
= eval env locs fn ((fc, MkClosure topopts locs env arg) :: stk)
120+
= case strategy topopts of
121+
CBV => do arg' <- eval env locs arg []
122+
eval env locs fn ((fc, MkNFClosure topopts env arg') :: stk)
123+
CBN => eval env locs fn ((fc, MkClosure topopts locs env arg) :: stk)
121124
eval env locs (As fc s n tm) stk
122125
= if removeAs topopts
123126
then eval env locs tm stk
@@ -144,53 +147,57 @@ parameters (defs : Defs, topopts : EvalOpts)
144147
-- to a stack
145148
applyToStack : {auto c : Ref Ctxt Defs} ->
146149
{free : _} ->
147-
Env Term free -> NF free -> Stack free -> Core (NF free)
148-
applyToStack env (NBind fc _ (Lam _ _ _ _) sc) (arg :: stk)
149-
= do defs' <- get Ctxt
150-
arg' <- sc defs' $ snd arg
151-
applyToStack env arg' stk
152-
applyToStack env (NBind fc x b@(Let _ r val ty) sc) stk
150+
Env Term free -> Bool ->
151+
NF free -> Stack free -> Core (NF free)
152+
applyToStack env cont (NBind fc _ (Lam _ _ _ _) sc) (arg :: stk)
153+
= do arg' <- sc defs $ snd arg
154+
applyToStack env cont arg' stk
155+
applyToStack env cont (NBind fc x b@(Let _ r val ty) sc) stk
153156
= if (holesOnly topopts || argHolesOnly topopts) && not (tcInline topopts)
154-
then do b' <- traverse (\t => applyToStack env t []) b
157+
then do b' <- if cont
158+
then traverse (\t => applyToStack env cont t []) b
159+
else pure b
155160
pure (NBind fc x b'
156-
(\defs', arg => applyToStack env !(sc defs' arg) stk))
157-
else do val' <- applyToStack env val []
158-
applyToStack env !(sc defs (MkNFClosure val')) stk
159-
applyToStack env (NBind fc x b sc) stk
160-
= do b' <- traverse (\t => applyToStack env t []) b
161+
(\defs', arg => applyToStack env cont !(sc defs' arg) stk))
162+
else do val' <- applyToStack env cont val []
163+
applyToStack env cont !(sc defs (MkNFClosure topopts env val')) stk
164+
applyToStack env cont (NBind fc x b sc) stk
165+
= do b' <- if cont
166+
then traverse (\t => applyToStack env cont t []) b
167+
else pure b
161168
pure (NBind fc x b'
162-
(\defs', arg => applyToStack env !(sc defs' arg) stk))
163-
applyToStack env (NApp fc (NRef nt fn) args) stk
169+
(\defs', arg => applyToStack env cont !(sc defs' arg) stk))
170+
applyToStack env cont (NApp fc (NRef nt fn) args) stk
164171
= evalRef env False fc nt fn (args ++ stk)
165172
(NApp fc (NRef nt fn) (args ++ stk))
166-
applyToStack env (NApp fc (NLocal mrig idx p) args) stk
173+
applyToStack env cont (NApp fc (NLocal mrig idx p) args) stk
167174
= evalLocal env fc mrig _ p (args ++ stk) []
168-
applyToStack env (NApp fc (NMeta n i args) args') stk
175+
applyToStack env cont (NApp fc (NMeta n i args) args') stk
169176
= evalMeta env fc n i args (args' ++ stk)
170-
applyToStack env (NDCon fc n t a args) stk
177+
applyToStack env cont (NDCon fc n t a args) stk
171178
= pure $ NDCon fc n t a (args ++ stk)
172-
applyToStack env (NTCon fc n t a args) stk
179+
applyToStack env cont (NTCon fc n t a args) stk
173180
= pure $ NTCon fc n t a (args ++ stk)
174-
applyToStack env (NAs fc s p t) stk
181+
applyToStack env cont (NAs fc s p t) stk
175182
= if removeAs topopts
176-
then applyToStack env t stk
177-
else do p' <- applyToStack env p []
178-
t' <- applyToStack env t stk
183+
then applyToStack env cont t stk
184+
else do p' <- applyToStack env cont p []
185+
t' <- applyToStack env cont t stk
179186
pure (NAs fc s p' t')
180-
applyToStack env (NDelayed fc r tm) stk
181-
= do tm' <- applyToStack env tm stk
187+
applyToStack env cont (NDelayed fc r tm) stk
188+
= do tm' <- applyToStack env cont tm stk
182189
pure (NDelayed fc r tm')
183-
applyToStack env nf@(NDelay fc r ty tm) stk
190+
applyToStack env cont nf@(NDelay fc r ty tm) stk
184191
= pure nf -- stack should always be empty here!
185-
applyToStack env (NForce fc r tm args) stk
186-
= do tm' <- applyToStack env tm []
192+
applyToStack env cont (NForce fc r tm args) stk
193+
= do tm' <- applyToStack env cont tm []
187194
case tm' of
188195
NDelay fc r _ arg =>
189196
eval env [arg] (Local {name = UN "fvar"} fc Nothing _ First) stk
190197
_ => pure (NForce fc r tm' (args ++ stk))
191-
applyToStack env nf@(NPrimVal fc _) _ = pure nf
192-
applyToStack env nf@(NErased fc _) _ = pure nf
193-
applyToStack env nf@(NType fc) _ = pure nf
198+
applyToStack env cont nf@(NPrimVal fc _) _ = pure nf
199+
applyToStack env cont nf@(NErased fc _) _ = pure nf
200+
applyToStack env cont nf@(NType fc) _ = pure nf
194201

195202
evalLocClosure : {auto c : Ref Ctxt Defs} ->
196203
{free : _} ->
@@ -201,8 +208,8 @@ parameters (defs : Defs, topopts : EvalOpts)
201208
Core (NF free)
202209
evalLocClosure env fc mrig stk (MkClosure opts locs' env' tm')
203210
= evalWithOpts defs opts env' locs' tm' stk
204-
evalLocClosure {free} env fc mrig stk (MkNFClosure nf)
205-
= applyToStack env nf stk
211+
evalLocClosure {free} env fc mrig stk (MkNFClosure opts env' nf)
212+
= applyToStack env' False nf stk
206213

207214
evalLocal : {auto c : Ref Ctxt Defs} ->
208215
{free : _} ->
@@ -229,12 +236,15 @@ parameters (defs : Defs, topopts : EvalOpts)
229236
env fc mrig (S idx) (Later p) stk (_ :: locs)
230237
= evalLocal {vars = xs} env fc mrig idx p stk locs
231238

232-
updateLocal : (idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) ->
239+
updateLocal : EvalOpts -> Env Term free ->
240+
(idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) ->
233241
LocalEnv free vars -> NF free ->
234242
LocalEnv free vars
235-
updateLocal Z First (x :: locs) nf = MkNFClosure nf :: locs
236-
updateLocal (S idx) (Later p) (x :: locs) nf = x :: updateLocal idx p locs nf
237-
updateLocal _ _ locs nf = locs
243+
updateLocal opts env Z First (x :: locs) nf
244+
= MkNFClosure opts env nf :: locs
245+
updateLocal opts env (S idx) (Later p) (x :: locs) nf
246+
= x :: updateLocal opts env idx p locs nf
247+
updateLocal _ _ _ _ locs nf = locs
238248

239249
evalMeta : {auto c : Ref Ctxt Defs} ->
240250
{free : _} ->
@@ -345,8 +355,8 @@ parameters (defs : Defs, topopts : EvalOpts)
345355
tryAlt {more}
346356
env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase (UN "->") tag [s,t] sc)
347357
= evalConAlt {more} env loc opts fc stk [s,t]
348-
[MkNFClosure aty,
349-
MkNFClosure (NBind pfc x (Lam fc' r e aty) scty)]
358+
[MkNFClosure opts env aty,
359+
MkNFClosure opts env (NBind pfc x (Lam fc' r e aty) scty)]
350360
sc
351361
-- Delay matching
352362
tryAlt env loc opts fc stk (NDelay _ _ ty arg) (DelayCase tyn argn sc)
@@ -398,7 +408,7 @@ parameters (defs : Defs, topopts : EvalOpts)
398408
-- we have not defined quote yet (it depends on eval itself) so we show the NF
399409
-- i.e. only the top-level constructor.
400410
log "eval.casetree" 5 $ "Evaluated " ++ show name ++ " to " ++ show xval
401-
let loc' = updateLocal idx (varExtend x) loc xval
411+
let loc' = updateLocal opts env idx (varExtend x) loc xval
402412
findAlt env loc' opts fc stk xval alts
403413
evalTree env loc opts fc stk (STerm _ tm)
404414
= case fuel opts of
@@ -497,7 +507,17 @@ evalWithOpts {vars} defs opts = eval {vars} defs opts
497507

498508
evalClosure defs (MkClosure opts locs env tm)
499509
= eval defs opts env locs tm []
500-
evalClosure defs (MkNFClosure nf) = pure nf
510+
evalClosure defs (MkNFClosure opts env nf)
511+
= applyToStack defs opts env True nf []
512+
513+
export
514+
evalClosureWithOpts : {auto c : Ref Ctxt Defs} ->
515+
{free : _} ->
516+
Defs -> EvalOpts -> Closure free -> Core (NF free)
517+
evalClosureWithOpts defs opts (MkClosure _ locs env tm)
518+
= eval defs opts env locs tm []
519+
evalClosureWithOpts defs opts (MkNFClosure _ env nf)
520+
= applyToStack defs opts env True nf []
501521

502522
export
503523
nf : {auto c : Ref Ctxt Defs} ->
@@ -740,7 +760,8 @@ export
740760
continueNF : {auto c : Ref Ctxt Defs} ->
741761
{vars : _} ->
742762
Defs -> Env Term vars -> NF vars -> Core (NF vars)
743-
continueNF defs env stuck = applyToStack defs defaultOpts env stuck []
763+
continueNF defs env stuck
764+
= applyToStack defs defaultOpts env True stuck []
744765

745766
export
746767
glueBack : {auto c : Ref Ctxt Defs} ->

‎src/Core/Value.idr

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,9 @@ import Libraries.Data.NameMap
1010

1111
%default covering
1212

13+
public export
14+
data EvalOrder = CBV | CBN
15+
1316
public export
1417
record EvalOpts where
1518
constructor MkEvalOpts
@@ -21,22 +24,23 @@ record EvalOpts where
2124
fuel : Maybe Nat -- Limit for recursion depth
2225
reduceLimit : List (Name, Nat) -- reduction limits for given names. If not
2326
-- present, no limit
27+
strategy : EvalOrder
2428

2529
export
2630
defaultOpts : EvalOpts
27-
defaultOpts = MkEvalOpts False False True False False Nothing []
31+
defaultOpts = MkEvalOpts False False True False False Nothing [] CBN
2832

2933
export
3034
withHoles : EvalOpts
31-
withHoles = MkEvalOpts True True False False False Nothing []
35+
withHoles = MkEvalOpts True True False False False Nothing [] CBN
3236

3337
export
3438
withAll : EvalOpts
35-
withAll = MkEvalOpts False False True True False Nothing []
39+
withAll = MkEvalOpts False False True True False Nothing [] CBN
3640

3741
export
3842
withArgHoles : EvalOpts
39-
withArgHoles = MkEvalOpts False True False False False Nothing []
43+
withArgHoles = MkEvalOpts False True False False False Nothing [] CBN
4044

4145
export
4246
tcOnly : EvalOpts
@@ -46,6 +50,14 @@ export
4650
onLHS : EvalOpts
4751
onLHS = record { removeAs = False } defaultOpts
4852

53+
export
54+
cbn : EvalOpts
55+
cbn = defaultOpts
56+
57+
export
58+
cbv : EvalOpts
59+
cbv = record { strategy = CBV } defaultOpts
60+
4961
mutual
5062
public export
5163
data LocalEnv : List Name -> List Name -> Type where
@@ -59,7 +71,7 @@ mutual
5971
LocalEnv free vars ->
6072
Env Term free ->
6173
Term (vars ++ free) -> Closure free
62-
MkNFClosure : NF free -> Closure free
74+
MkNFClosure : EvalOpts -> Env Term free -> NF free -> Closure free
6375

6476
-- The head of a value: things you can apply arguments to
6577
public export

‎src/Idris/REPL.idr

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ import Core.Options
2626
import Core.TT
2727
import Core.Termination
2828
import Core.Unify
29+
import Core.Value
2930

3031
import Parser.Unlit
3132

@@ -661,7 +662,7 @@ loadMainFile f
661662
replEval : {auto c : Ref Ctxt Defs} ->
662663
{vs : _} ->
663664
REPLEval -> Defs -> Env Term vs -> Term vs -> Core (Term vs)
664-
replEval NormaliseAll = normaliseAll
665+
replEval NormaliseAll = normaliseOpts (record { strategy = CBV } withAll)
665666
replEval _ = normalise
666667

667668
record TermWithType where

0 commit comments

Comments
 (0)