@@ -58,20 +58,20 @@ data ExecVal = EP NameType Name ExecVal
59 | EConstant Const
59 | EConstant Const
60 | forall a. EPtr (Ptr a)
60 | forall a. EPtr (Ptr a)
61− | EThunk ExecEnv Term
61+ | EThunk Context ExecEnv Term
62 | EHandle Handle
62 | EHandle Handle
64instance Show ExecVal where
64instance Show ExecVal where
65− show (EP _ n _) = show n
65+ show (EP _ n _) = show n
66− show (EV i) = "!!V" ++ show i ++ "!!"
66+ show (EV i) = "!!V" ++ show i ++ "!!"
67− show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
67+ show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
68− show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
68+ show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
69− show (EType _) = "Type"
69+ show (EType _) = "Type"
70− show EErased = "[__]"
70+ show EErased = "[__]"
71− show (EConstant c) = show c
71+ show (EConstant c) = show c
72− show (EPtr p) = "<<ptr " ++ show p ++ ">>"
72+ show (EPtr p) = "<<ptr " ++ show p ++ ">>"
73− show (EThunk env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"
73+ show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"
74− show (EHandle h) = "<<handle " ++ show h ++ ">>"
74+ show (EHandle h) = "<<handle " ++ show h ++ ">>"
76toTT :: ExecVal -> Exec Term
76toTT :: ExecVal -> Exec Term
77toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
77toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
@@ -79,22 +79,25 @@ toTT (EV i) = return $ V i
79toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
79toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
80 b' <- fixBinder b
80 b' <- fixBinder b
81 Bind n b' <$> toTT body'
81 Bind n b' <$> toTT body'
82− where fixBinder (Lam t) = Lam <$> toTT t
82+ where fixBinder (Lam t) = Lam <$> toTT t
83− fixBinder (Pi t) = Pi <$> toTT t
83+ fixBinder (Pi t) = Pi <$> toTT t
84− fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
84+ fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
85− fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
85+ fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
86− fixBinder (Hole t) = Hole <$> toTT t
86+ fixBinder (Hole t) = Hole <$> toTT t
87 fixBinder (GHole i t) = GHole i <$> toTT t
87 fixBinder (GHole i t) = GHole i <$> toTT t
88− fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
88+ fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
89− fixBinder (PVar t) = PVar <$> toTT t
89+ fixBinder (PVar t) = PVar <$> toTT t
90− fixBinder (PVTy t) = PVTy <$> toTT t
90+ fixBinder (PVTy t) = PVTy <$> toTT t
91toTT (EApp e1 e2) = do e1' <- toTT e1
91toTT (EApp e1 e2) = do e1' <- toTT e1
92 e2' <- toTT e2
92 e2' <- toTT e2
93 return $ App e1' e2'
93 return $ App e1' e2'
94toTT (EType u) = return $ TType u
94toTT (EType u) = return $ TType u
95toTT EErased = return Erased
95toTT EErased = return Erased
96toTT (EConstant c) = return (Constant c)
96toTT (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')
98toTT (EHandle _) = return Erased
101toTT (EHandle _) = return Erased
100unApplyV :: ExecVal -> (ExecVal, [ExecVal])
103unApplyV :: ExecVal -> (ExecVal, [ExecVal])
@@ -181,7 +184,7 @@ doExec env ctxt a@(App _ _) =
181 case args of
184 case args of
182 [t,a,tm] -> do t' <- doExec env ctxt t
185 [t,a,tm] -> do t' <- doExec env ctxt t
183 a' <- doExec env ctxt a
186 a' <- doExec env ctxt a
184− return [t', a', EThunk env tm]
187+ return [t', a', EThunk ctxt env tm]
185 _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate
188 _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate
186 fun' -> do mapM (doExec env ctxt) args
189 fun' -> do mapM (doExec env ctxt) args
187 execApp env ctxt f' args'
190 execApp env ctxt f' args'
@@ -197,8 +200,8 @@ execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
197execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls
200execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls
198execApp env ctxt (EP _ f _) (t:a:delayed:rest)
201execApp env ctxt (EP _ f _) (t:a:delayed:rest)
199 | f == force
202 | f == force
200− , (_, [_, _, EThunk tmEnv tm]) <- unApplyV delayed =
203+ , (_, [_, _, EThunk tmCtxt tmEnv tm]) <- unApplyV delayed =
201− do tm' <- doExec tmEnv ctxt tm
204+ do tm' <- doExec tmEnv tmCtxt tm
202 execApp env ctxt tm' rest
205 execApp env ctxt tm' rest
203execApp env ctxt (EP _ fp _) (ty:action:rest)
206execApp env ctxt (EP _ fp _) (ty:action:rest)
204 | fp == upio,
207 | fp == upio,