@@ -33,7 +33,9 @@ initEval = ES [] 0
3333-- | A HOAS representation of values
3434data Value = VP NameType Name Value
3535 | VV Int
36− | VBind Name (Binder Value) (Value -> Eval Value)
36+ -- True for Bool indicates safe to reduce
37+ | VBind Bool Name (Binder Value) (Value -> Eval Value)
38+ -- For frozen let bindings when simplifying
3739 | VBLet Int Name Value Value Value
3840 | VApp Value Value
3941 | VType UExp
@@ -190,10 +192,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
190192 = do t' <- ev ntimes stk top env (finalise t)
191193 v' <- ev ntimes stk top env (finalise v)
192194 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')
194196 ev ntimes stk top env (Bind n b sc)
195197 = do b' <- vbind env b
196− return $ VBind n b' (\x -> ev ntimes stk False (x:env) sc)
198+ return $ VBind (not simpl || vinstances 0 sc < 2)
199+ n b' (\x -> ev ntimes stk False (x:env) sc)
197200 where vbind env t
198201 | simpl
199202 = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)
@@ -215,10 +218,10 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
215218 evApply ntimes stk top env (a:args) f
216219 evApply ntimes stk top env args f = apply ntimes stk top env f args
217220
218− apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
219− = do a' <- sc a
220− app <- apply ntimes stk top env a' as
221− wknV (-1) app
221+ apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
222+ = do a' <- sc a
223+ app <- apply ntimes stk top env a' as
224+ wknV (-1) app
222225-- apply ntimes stk False env f args
223226-- | spec = specApply ntimes stk env f args
224227 apply ntimes_in stk top env f@(VP Ref n ty) args
@@ -352,9 +355,9 @@ class Quote a where
352355instance Quote Value where
353356 quote i (VP nt n v) = liftM (P nt n) (quote i v)
354357 quote i (VV x) = return $ V x
355− quote i (VBind n b sc) = do sc' <- sc (VTmp i)
356− b' <- quoteB b
357− liftM (Bind n b') (quote (i+1) sc')
358+ quote i (VBind _ n b sc) = do sc' <- sc (VTmp i)
359+ b' <- quoteB b
360+ liftM (Bind n b') (quote (i+1) sc')
358361 where quoteB t = fmapMB (quote i) t
359362 quote i (VBLet vd n t v sc)
360363 = do sc' <- quote i sc
@@ -387,9 +390,9 @@ instance Quote HNF where
387390
388391wknV :: Int -> Value -> Eval Value
389392wknV i (VV x) = return $ VV (x + i)
390−wknV i (VBind n b sc) = do b' <- fmapMB (wknV i) b
391− return $ VBind n b' (\x -> do x' <- sc x
392− wknV i x')
393+wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
394+ return $ VBind red n b' (\x -> do x' <- sc x
395+ wknV i x')
393396wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
394397wknV i t = return t
395398