@@ -1,7 +1,7 @@
11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
22 PatternGuards #-}
33
4−module Core.Evaluate(normalise, normaliseC, normaliseAll,
4+module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
55 simplify, specialise, hnf, convEq, convEq',
66 Def(..), Accessibility(..), Totality(..), PReason(..),
77 Context, initContext, ctxtAlist, uconstraints, next_tvar,
@@ -83,22 +83,25 @@ threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typech
8383-- Normalise fully type checked terms (so, assume all names/let bindings resolved)
8484normaliseC :: Context -> Env -> TT Name -> TT Name
8585normaliseC ctxt env t
86− = evalState (do val <- eval ctxt threshold [] env t []
86+ = evalState (do val <- eval False ctxt threshold [] env t []
8787 quote 0 val) initEval
8888
8989normaliseAll :: Context -> Env -> TT Name -> TT Name
9090normaliseAll ctxt env t
91− = evalState (do val <- eval ctxt threshold [] env t [AtREPL]
91+ = evalState (do val <- eval False ctxt threshold [] env t [AtREPL]
9292 quote 0 val) initEval
9393
9494normalise :: Context -> Env -> TT Name -> TT Name
95−normalise ctxt env t
96− = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) []
95+normalise = normaliseTrace False
96+
97+normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
98+normaliseTrace tr ctxt env t
99+ = evalState (do val <- eval tr ctxt threshold [] (map finalEntry env) (finalise t) []
97100 quote 0 val) initEval
98101
99102specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
100103specialise ctxt env limits t
101− = evalState (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) []
104+ = evalState (do val <- eval False ctxt threshold limits (map finalEntry env) (finalise t) []
102105 quote 0 val) (initEval { limited = limits })
103106
104107-- Like normalise, but we only reduce functions that are marked as okay to
@@ -106,13 +109,13 @@ specialise ctxt env limits t
106109
107110simplify :: Context -> Env -> TT Name -> TT Name
108111simplify ctxt env t
109− = evalState (do val <- eval ctxt threshold []
112+ = evalState (do val <- eval False ctxt threshold []
110113 (map finalEntry env) (finalise t) [Simplify]
111114 quote 0 val) initEval
112115
113116hnf :: Context -> Env -> TT Name -> TT Name
114117hnf ctxt env t
115− = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
118+ = evalState (do val <- eval False ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
116119 quote 0 val) initEval
117120
118121
@@ -144,8 +147,9 @@ reduction = do ES ns s <- get
144147-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
145148-- such as we might have during construction of a proof)
146149
147−eval :: Context -> Int -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value
148−eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
150+eval :: Bool -> Context -> Int -> [(Name, Int)] -> Env -> TT Name ->
151+ [EvalOpt] -> Eval Value
152+eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
149153 spec = Spec `elem` opts
150154 simpl = Simplify `elem` opts
151155 atRepl = AtREPL `elem` opts
@@ -216,7 +220,7 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
216220-- | spec = specApply ntimes stk env f args
217221 apply ntimes_in stk top env f@(VP Ref n ty) args
218222 | (True, ntimes) <- usable n ntimes_in
219− = -- trace (show n) $
223+ = traceWhen traceon (show stk) $
220224 do let val = lookupDefAcc Nothing n atRepl ctxt
221225 case val of
222226 [(CaseOp inl _ _ ns tree _ _, Public)] ->
@@ -629,7 +633,7 @@ initContext = MkContext [] 0 emptyContext
629633ctxtAlist :: Context -> [(Name, Def)]
630634ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
631635
632−veval ctxt env t = evalState (eval ctxt threshold [] env t []) initEval
636+veval ctxt env t = evalState (eval False ctxt threshold [] env t []) initEval
633637
634638addToCtxt :: Name -> Term -> Type -> Context -> Context
635639addToCtxt n tm ty uctxt