@@ -33,7 +33,9 @@ initEval = ES [] 0
33-- | A HOAS representation of values
33-- | A HOAS representation of values
34data Value = VP NameType Name Value
34data Value = VP NameType Name Value
36+ -- True for Bool indicates safe to reduce
36− | VBind Name (Binder Value) (Value -> Eval Value)
37+ | VBind Bool Name (Binder Value) (Value -> Eval Value)
38+ -- For frozen let bindings when simplifying
37 | VBLet Int Name Value Value Value
39 | VBLet Int Name Value Value Value
38 | VApp Value Value
40 | VApp Value Value
39 | VType UExp
41 | VType UExp
@@ -190,10 +192,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
190 = do t' <- ev ntimes stk top env (finalise t)
192 = do t' <- ev ntimes stk top env (finalise t)
191 v' <- ev ntimes stk top env (finalise v)
193 v' <- ev ntimes stk top env (finalise v)
192 sc' <- ev ntimes stk top (v' : env) sc
194 sc' <- ev ntimes stk top (v' : env) sc
193− return $ VBind n (Let t' v') (\x -> return sc')
195+ return $ VBind True n (Let t' v') (\x -> return sc')
194 ev ntimes stk top env (Bind n b sc)
196 ev ntimes stk top env (Bind n b sc)
195 = do b' <- vbind env b
197 = do b' <- vbind env b
198+ return $ VBind (not simpl || vinstances 0 sc < 2)
196− return $ VBind n b' (\x -> ev ntimes stk False (x:env) sc)
199+ n b' (\x -> ev ntimes stk False (x:env) sc)
197 where vbind env t
200 where vbind env t
199 = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)
202 = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)
@@ -215,10 +218,10 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
215 evApply ntimes stk top env (a:args) f
218 evApply ntimes stk top env (a:args) f
216 evApply ntimes stk top env args f = apply ntimes stk top env f args
219 evApply ntimes stk top env args f = apply ntimes stk top env f args
218− apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
221+ apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
219− = do a' <- sc a
222+ = do a' <- sc a
220− app <- apply ntimes stk top env a' as
223+ app <- apply ntimes stk top env a' as
221− wknV (-1) app
224+ wknV (-1) app
222-- apply ntimes stk False env f args
225-- apply ntimes stk False env f args
223-- | spec = specApply ntimes stk env f args
226-- | spec = specApply ntimes stk env f args
224 apply ntimes_in stk top env f@(VP Ref n ty) args
227 apply ntimes_in stk top env f@(VP Ref n ty) args
@@ -352,9 +355,9 @@ class Quote a where
352instance Quote Value where
355instance Quote Value where
353 quote i (VP nt n v) = liftM (P nt n) (quote i v)
356 quote i (VP nt n v) = liftM (P nt n) (quote i v)
354 quote i (VV x) = return $ V x
357 quote i (VV x) = return $ V x
355− quote i (VBind n b sc) = do sc' <- sc (VTmp i)
358+ quote i (VBind _ n b sc) = do sc' <- sc (VTmp i)
356− b' <- quoteB b
359+ b' <- quoteB b
357− liftM (Bind n b') (quote (i+1) sc')
360+ liftM (Bind n b') (quote (i+1) sc')
358 where quoteB t = fmapMB (quote i) t
361 where quoteB t = fmapMB (quote i) t
359 quote i (VBLet vd n t v sc)
362 quote i (VBLet vd n t v sc)
360 = do sc' <- quote i sc
363 = do sc' <- quote i sc
@@ -387,9 +390,9 @@ instance Quote HNF where
388wknV :: Int -> Value -> Eval Value
391wknV :: Int -> Value -> Eval Value
389wknV i (VV x) = return $ VV (x + i)
392wknV i (VV x) = return $ VV (x + i)
390−wknV i (VBind n b sc) = do b' <- fmapMB (wknV i) b
393+wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
391− return $ VBind n b' (\x -> do x' <- sc x
394+ return $ VBind red n b' (\x -> do x' <- sc x
392− wknV i x')
395+ wknV i x')
393wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
396wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
394wknV i t = return t
397wknV i t = return t