@@ -58,20 +58,20 @@ data ExecVal = EP NameType Name ExecVal
5858 | EErased
5959 | EConstant Const
6060 | forall a. EPtr (Ptr a)
61− | EThunk ExecEnv Term
61+ | EThunk Context ExecEnv Term
6262 | EHandle Handle
6363
6464instance Show ExecVal where
65− show (EP _ n _) = show n
66− show (EV i) = "!!V" ++ show i ++ "!!"
67− show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
68− show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
69− show (EType _) = "Type"
70− show EErased = "[__]"
71− show (EConstant c) = show c
72− show (EPtr p) = "<<ptr " ++ show p ++ ">>"
73− show (EThunk env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"
74− show (EHandle h) = "<<handle " ++ show h ++ ">>"
65+ show (EP _ n _) = show n
66+ show (EV i) = "!!V" ++ show i ++ "!!"
67+ show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
68+ show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
69+ show (EType _) = "Type"
70+ show EErased = "[__]"
71+ show (EConstant c) = show c
72+ show (EPtr p) = "<<ptr " ++ show p ++ ">>"
73+ show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"
74+ show (EHandle h) = "<<handle " ++ show h ++ ">>"
7575
7676toTT :: ExecVal -> Exec Term
7777toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
@@ -79,22 +79,25 @@ toTT (EV i) = return $ V i
7979toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
8080 b' <- fixBinder b
8181 Bind n b' <$> toTT body'
82− where fixBinder (Lam t) = Lam <$> toTT t
83− fixBinder (Pi t) = Pi <$> toTT t
84− fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
85− fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
86− fixBinder (Hole t) = Hole <$> toTT t
82+ where fixBinder (Lam t) = Lam <$> toTT t
83+ fixBinder (Pi t) = Pi <$> toTT t
84+ fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
85+ fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
86+ fixBinder (Hole t) = Hole <$> toTT t
8787 fixBinder (GHole i t) = GHole i <$> toTT t
88− fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
89− fixBinder (PVar t) = PVar <$> toTT t
90− fixBinder (PVTy t) = PVTy <$> toTT t
88+ fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
89+ fixBinder (PVar t) = PVar <$> toTT t
90+ fixBinder (PVTy t) = PVTy <$> toTT t
9191toTT (EApp e1 e2) = do e1' <- toTT e1
9292 e2' <- toTT e2
9393 return $ App e1' e2'
9494toTT (EType u) = return $ TType u
9595toTT EErased = return Erased
9696toTT (EConstant c) = return (Constant c)
97−toTT (EThunk env tm) = return tm
97+toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env
98+ return $ normalise ctxt env' tm
99+ where toBinder (n, v) = do v' <- toTT v
100+ return (n, Let Erased v')
98101toTT (EHandle _) = return Erased
99102
100103unApplyV :: ExecVal -> (ExecVal, [ExecVal])
@@ -181,7 +184,7 @@ doExec env ctxt a@(App _ _) =
181184 case args of
182185 [t,a,tm] -> do t' <- doExec env ctxt t
183186 a' <- doExec env ctxt a
184− return [t', a', EThunk env tm]
187+ return [t', a', EThunk ctxt env tm]
185188 _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate
186189 fun' -> do mapM (doExec env ctxt) args
187190 execApp env ctxt f' args'
@@ -197,8 +200,8 @@ execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
197200execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls
198201execApp env ctxt (EP _ f _) (t:a:delayed:rest)
199202 | f == force
200− , (_, [_, _, EThunk tmEnv tm]) <- unApplyV delayed =
201− do tm' <- doExec tmEnv ctxt tm
203+ , (_, [_, _, EThunk tmCtxt tmEnv tm]) <- unApplyV delayed =
204+ do tm' <- doExec tmEnv tmCtxt tm
202205 execApp env ctxt tm' rest
203206execApp env ctxt (EP _ fp _) (ty:action:rest)
204207 | fp == upio,