@@ -28,34 +28,8 @@ import Foreign.Ptr
2828
2929import System.IO
3030
31−-- | Attempt to perform a side effect. Return either Just the next step in
32−-- evaluation (after performing the side effect through IO), or Nothing if no
33−-- IO was performed.
34−--
35−-- This function is exceedingly generous about what it will accept in order to
36−-- enable convenient testing at the REPL.
37−-- step :: TT Name -> Idris (Maybe (TT Name))
38−-- step tm = step' (unApply tm)
39−-- where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped
40−-- step' (P _ (UN "mkForeign") _, args) = stepForeign args
41−-- step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)
42−-- step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =
43−-- do line <- lift $ getLine
44−-- return . Just . Constant . Str $ line
45−-- step' _ = return Nothing
46−
47−-- | Perform side effects until no more can be performed, then return the
48−-- resulting term (possibly the argument).
49−-- execute :: TT Name -> Idris (TT Name)
50−-- execute tm = case unApply tm of
51−-- (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg
52−-- _ -> return tm
53−-- where execute' tm = do stepped <- step tm
54−-- case stepped of
55−-- Nothing -> return tm
56−-- Just tm' -> execute' tm'
57−
58−data Lazy = Delayed Env Context Term | Forced Term
31+
32+data Lazy = Delayed ExecEnv Context Term | Forced ExecVal
5933
6034data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs
6135 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
@@ -65,6 +39,51 @@ data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the res
6539 , exec_next_handle :: Int -- ^ Ensure opened file key uniqueness
6640 }
6741
42+data ExecVal = EP NameType Name ExecVal
43+ | EV Int
44+ | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
45+ | EApp ExecVal ExecVal
46+ | EType UExp
47+ | EErased
48+ | EConstant Const
49+-- | ETmp Int
50+ | EThunk Int
51+ | EHandle Int
52+ deriving Show
53+
54+toTT :: ExecVal -> Exec Term
55+toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
56+toTT (EV i) = return $ V i
57+toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
58+ b' <- fixBinder b
59+ Bind n b' <$> toTT body'
60+ where fixBinder (Lam t) = Lam <$> toTT t
61+ fixBinder (Pi t) = Pi <$> toTT t
62+ fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
63+ fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
64+ fixBinder (Hole t) = Hole <$> toTT t
65+ fixBinder (GHole t) = GHole <$> toTT t
66+ fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
67+ fixBinder (PVar t) = PVar <$> toTT t
68+ fixBinder (PVTy t) = PVTy <$> toTT t
69+toTT (EApp e1 e2) = do e1' <- toTT e1
70+ e2' <- toTT e2
71+ return $ App e1' e2'
72+toTT (EType u) = return $ TType u
73+toTT EErased = return Erased
74+toTT (EConstant c) = return (Constant c)
75+toTT (EThunk _) = return Erased
76+toTT (EHandle _) = return Erased
77+
78+unApplyV :: ExecVal -> (ExecVal, [ExecVal])
79+unApplyV tm = ua [] tm
80+ where ua args (EApp f a) = ua (a:args) f
81+ ua args t = (t, args)
82+
83+mkEApp :: ExecVal -> [ExecVal] -> ExecVal
84+mkEApp f [] = f
85+mkEApp f (a:args) = mkEApp (EApp f a) args
86+
6887initState :: Idris ExecState
6988initState = do ist <- getIState
7089 return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist) M.empty 0
@@ -86,143 +105,121 @@ execFail = throwError
86105execIO :: IO a -> Exec a
87106execIO = lift . lift
88107
89−thunk :: Name
90−thunk = MN 0 "__execThunk"
91−
92−delay :: Env -> Context -> Term -> Exec Term
108+delay :: ExecEnv -> Context -> Term -> Exec ExecVal
93109delay env ctxt tm =
94110 do st <- getExecState
95111 let i = exec_next_thunk st
96112 putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)
97113 , exec_next_thunk = exec_next_thunk st + 1
98114 }
99− return $ App (P (DCon 1 0) thunk Erased) (Constant (I i))
115+ return $ EThunk i
100116
101−force :: Int -> Exec Term
117+force :: Int -> Exec ExecVal
102118force i = do st <- getExecState
103119 case M.lookup i (exec_thunks st) of
104120 Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm
105121 case tm' of
106− App (P _ thnk _) (Constant (I i)) | thnk == thunk ->
107− do res <- force i
108− update res i
109− return res
122+ EThunk i ->
123+ do res <- force i
124+ update res i
125+ return res
110126 _ -> do update tm' i
111127 return tm'
112128 Just (Forced tm) -> return tm
113129 Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"
114− where update :: Term -> Int -> Exec ()
130+ where update :: ExecVal -> Int -> Exec ()
115131 update tm i = do est <- getExecState
116132 putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }
117133
118−unLazy :: Env -> Context -> Term -> Exec Term
119−unLazy env ctxt tm = trace ("unLazy " ++ take 100 (show (unApply tm))) $
120− do res <- unLazy' (unApply tm)
121− trace ("unLazy res is " ++ take 100 (show res)) $ return res
122− where unLazy' (P _ thnk _, (Constant (I i)):rest) | thnk == thunk = do tm <- force i
123− doExec env ctxt (mkApp tm rest)
124− unLazy' (tm, xs) = return $ mkApp tm xs
125−
134+tryForce :: ExecVal -> Exec ExecVal
135+tryForce (EThunk i) = force i
136+tryForce tm = return tm
126137
127138execute :: Term -> Idris Term
128139execute tm = do est <- initState
129140 ctxt <- getContext
130− res <- lift $ runExec (doExec [] ctxt tm) est
141+ res <- lift $ runExec (doExec [] ctxt tm >>= toTT) est
131142 case res of
132143 Left err -> fail err
133144 Right tm' -> return tm'
134145
135−ioWrap :: Term -> Term
136−ioWrap tm = mkApp (P Ref (UN "prim__IO") Erased) [Erased, tm]
146+ioWrap :: ExecVal -> ExecVal
147+ioWrap tm = mkEApp (EP Ref (UN "prim__IO") EErased) [EErased, tm]
148+
149+ioUnit :: ExecVal
150+ioUnit = ioWrap (EP Ref unitCon EErased)
137151
138−ioUnit :: Term
139−ioUnit = ioWrap (P Ref unitCon Erased)
152+type ExecEnv = [(Name, Binder ExecVal)]
140153
141−doExec :: Env -> Context -> Term -> Exec Term
154+doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
142155doExec env ctxt p@(P Ref n ty) =
143156 do let val = lookupDef n ctxt
144157 case val of
145− [Function _ tm] ->
146− do val <- doExec env ctxt tm
147− return val
148− [TyDecl nt ty] -> return p -- abstract def
149− [Operator tp arity op] -> do ty' <- doExec env ctxt ty
150− return (P Ref n ty')
158+ [Function _ tm] -> doExec env ctxt tm
159+ [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
160+ [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
151161 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
152162 doExec env ctxt tm
153− [CaseOp _ _ _ _ _ ns sc _ _] -> return p
163+ [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)
154164 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
155165doExec env ctxt p@(P Bound n ty) =
156− case (lookupDef n ctxt) of -- bound vars must be Function
157− [Function ty tm] -> doExec env ctxt tm
158− [] -> return p
159− x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
160−doExec env ctxt p@(P (DCon _ _) n _) = return p
161−doExec env ctxt p@(P (TCon _ _) n _) = return p
166+ case lookup n env of
167+ Nothing -> execFail "not found"
168+ Just (Let _ tm) -> return tm
169+ Just b -> execFail $ "Unknown binder " ++ show b
170+doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)
171+doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
162172doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
163173 case binder of
164174 (_, (Let t v)) -> return v
165175 (_, (NLet t v)) -> return v
166− (n, b) -> doExec env ctxt (P Bound n (binderTy b))
167− | otherwise = return $ V i
176+ (n, b) -> doExec env ctxt (P Bound n Erased)
177+ | otherwise = execFail "env too small"
168178doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
169− let ctxt' = addToCtxt n v' t ctxt
170− doExec ((n, Let t v'):env) ctxt' body
179+ doExec ((n, Let EErased v'):env) ctxt body
171180doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
172−doExec env ctxt tm@(Bind n b body) = return tm -- don't eval under lambda!
181+doExec env ctxt tm@(Bind n b body) = return $
182+ EBind n (fmap (\_->EErased) b)
183+ (\arg -> doExec ((n, Let EErased arg):env) ctxt body)
173184doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
174−doExec env ctxt (Constant c) = return (Constant c)
185+doExec env ctxt (Constant c) = return (EConstant c)
175186doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
176− return ((x:xs) !! i)
177−doExec env ctxt Erased = return Erased
187+ doExec env ctxt ((x:xs) !! i)
188+doExec env ctxt Erased = return EErased
178189doExec env ctxt Impossible = fail "Tried to execute an impossible case"
179−doExec env ctxt (TType u) = return (TType u)
190+doExec env ctxt (TType u) = return (EType u)
180191
181−execApp :: Env -> Context -> (Term, [Term]) -> Exec Term
182−execApp env ctxt ((P _ n _), (Constant (I i)):args) | n == thunk = do x <- force i
183− doExec env ctxt (mkApp x args)
192+execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
184193execApp env ctxt (f, args) = do newF <- doExec env ctxt f
185194 laziness <- (getLaziness newF) >>= return . (++ repeat False)
186195 newArgs <- mapM argExec (zip args laziness)
187− trace ((take 40 (show newF)) ++ " " ++ show (map (take 100 . show) (zip args laziness))) $ return ()
196+ trace (take 1000 (show newF) ++ " " ++ take 2000 (show newArgs)) $ return ()
188197 execApp' env ctxt newF newArgs
189− where getLaziness (P _ (UN "io_bind") _) = return [False, False, False, True]
190− getLaziness (P _ (UN "lazy") _) = return [True]
191− getLaziness (P _ n _) = do est <- getExecState
192− let argInfo = exec_implicits est
193− trace ("Looking for laziness of " ++ show n ++ ", found " ++ (take 1000 . show $ lookupCtxtName n argInfo)) $ return ()
194− case lookupCtxtName n argInfo of
195− [] -> return (repeat False)
196− [ps] -> return $ map lazyarg (snd ps)
197− many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
198− getLaziness x = return (repeat False) -- ok due to zip above
199− argExec :: (Term, Bool) -> Exec Term
198+ where getLaziness (EP _ (UN "lazy") _) = return [True]
199+ getLaziness (EP _ n _) = do est <- getExecState
200+ let argInfo = exec_implicits est
201+ case lookupCtxtName n argInfo of
202+ [] -> return (repeat False)
203+ [ps] -> return $ map lazyarg (snd ps)
204+ many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
205+ getLaziness _ = return (repeat False) -- ok due to zip above
206+ argExec :: (Term, Bool) -> Exec ExecVal
200207 argExec (tm, False) = doExec env ctxt tm
201208 argExec (tm, True) = delay env ctxt tm
202209
203210
204−execApp' :: Env -> Context -> Term -> [Term] -> Exec Term
211+execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
205212execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
206−execApp' env ctxt (P _ (UN "io_bind") _) (_:_:x:k:rest) =
207− trace ("x="++(take 150 (show x)) ++ " and\nk=" ++ (take 150 (show k))) $
208− do x' <- doExec env ctxt x
209− trace ("Arg x in io_bind from " ++ (take 150 (show x)) ++ "\n to ==> " ++ take 150 (show x')) $ return ()
210− case unApply x' of
211− (P _ (UN "prim__IO") _, [_, x'']) ->
212− trace ("Calling " ++ take 100 (show k)) $
213− doExec env ctxt (mkApp k (x'':rest))
214− _ -> execFail $ "Did not get an IO object out of " ++ take 100 (show x)
215−execApp' env ctxt (P _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [ty', v]) <- unApply action =
216− doExec env ctxt (mkApp v rest)
213+execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [ty', v]) <- unApplyV action =
214+ execApp' env ctxt v rest
217215
218216-- Special cases arising from not having access to the C RTS in the interpreter
219217
220−execApp' env ctxt (P _ (UN "mkForeign") _) (_:fn:Constant (Str arg):rest)
218+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
221219 | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
222− doExec env ctxt (mkApp ioUnit rest)
223−execApp' env ctxt (P _ (UN "mkForeign") _) (_:fn:Constant (Str f):Constant (Str mode):rest)
224− | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do trace ("Opening " ++ f ++ " with " ++ mode) $ return ()
225− m <- case mode of
220+ execApp' env ctxt ioUnit rest
221+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
222+ | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of
226223 "r" -> return ReadMode
227224 "w" -> return WriteMode
228225 "a" -> return AppendMode
@@ -232,101 +229,105 @@ execApp' env ctxt (P _ (UN "mkForeign") _) (_:fn:Constant (Str f):Constant (Str
232229 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
233230 h <- execIO $ openFile f m
234231 h' <- handle h
235− trace ("Got " ++ (take 100 (show h') ++ " and " ++ (take 100 (show rest)))) (return ())
236− doExec env ctxt (mkApp (ioWrap h') rest)
232+ execApp' env ctxt (ioWrap h') rest
237233
238−execApp' env ctxt (P _ (UN "mkForeign") _) (_:fn:fh:rest)
239− | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = trace ("feof") $
240− do h <- unHandle fh
234+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:fh:rest)
235+ | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do h <- unHandle fh
241236 eofp <- execIO $ hIsEOF h
242− let res = ioWrap (Constant (I $ if eofp then 1 else 0))
243− doExec env ctxt (mkApp res rest)
237+ let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
238+ trace ("feof was " ++ show eofp) $ return ()
239+ execApp' env ctxt res rest
244240
245241
246−execApp' env ctxt f@(P _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn
247− , length xs >= length argTs =
242+execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn
243+ , length xs >= length argTs =
248244 do res <- stepForeign (ty:fn:take (length argTs) xs)
249245 case res of
250246 Nothing -> fail "Could not call foreign function"
251− Just r -> return (mkApp r (drop (length argTs) xs))
252− | otherwise = return (mkApp f args)
253−
254−execApp' env ctxt (P _ (UN "prim__concat") _) [Constant (Str s1), Constant (Str s2)] =
255− return $ Constant (Str (s1 ++ s2))
256−
257−execApp' env ctxt (P _ (UN "prim__eqInt") _) [Constant (I i1), Constant (I i2)] =
258− return $ if i1 == i2 then Constant (I 1) else Constant (I 0)
259−
260−execApp' env ctxt (P _ (UN "prim__ltInt") _) [Constant (I i1), Constant (I i2)] =
261− return $ if i1 < i2 then Constant (I 1) else Constant (I 0)
262−
263−execApp' env ctxt (P _ (UN "prim__subInt") _) [Constant (I i1), Constant (I i2)] =
264− return . Constant . I $ i1 - i2
247+ Just r -> return (mkEApp r (drop (length argTs) xs))
248+ | otherwise = return (mkEApp f args)
265249
266−execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
267− do line <- execIO getLine
268− return (Constant (Str line))
269−
270−execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] =
271− trace ("prim__readStr of file") $
272− do h <- unHandle ptr
273−
274− contents <- execIO $ hGetLine h
275− return $ ioWrap (Constant (Str contents))
276−
277−execApp' env ctxt f@(P _ n _) args =
250+execApp' env ctxt f@(EP _ n _) args =
278251 do let val = lookupDef n ctxt
279252 case val of
280253 [Function _ tm] -> fail "should already have been eval'd"
281− [TyDecl nt ty] -> return $ mkApp f args
282− [Operator tp arity op] -> fail $ "Can't apply operator " ++ show n ++ " which needs special-casing"
254+ [TyDecl nt ty] -> return $ mkEApp f args
255+ [Operator tp arity op] ->
256+ case getOp n (take arity args) of
257+ Just res -> do r <- res
258+ execApp' env ctxt r (drop arity args)
259+ Nothing -> return (mkEApp f args)
283260 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
284261 do rhs <- doExec env ctxt tm
285− doExec env ctxt (mkApp tm args)
262+ execApp' env ctxt rhs args
286263 [CaseOp _ _ _ _ _ ns sc _ _] ->
287264 do res <- execCase env ctxt ns sc args
288− return $ fromMaybe (mkApp f args) res
289− thing -> return $ mkApp f args
290−
291−execApp' env ctxt bnd@(Bind n b body) (arg:args) = let ctxt' = addToCtxt n arg Erased ctxt in
292− doExec ((n, b):env) ctxt' body
293−
294−execApp' env ctxt f args = return (mkApp f args)
295−
296−execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Exec (Maybe Term)
297−execCase env ctxt ns sc args = trace ("Case execution, args are " ++ take 100 (show (zip ns args))) $
265+ return $ fromMaybe (mkEApp f args) res
266+ thing -> return $ mkEApp f args
267+ where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
268+ getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =
269+ Just . return . EConstant . Str $ s1 ++ s2
270+ getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =
271+ Just . return . EConstant . I $ if i1 == i2 then 1 else 0
272+ getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =
273+ Just . return . EConstant . I $ if i1 < i2 then 1 else 0
274+ getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
275+ Just . return . EConstant . I $ i1 - i2
276+ getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
277+ Just $ do line <- execIO getLine
278+ return (EConstant (Str line))
279+ getOp (UN "prim__readString") [ptr] =
280+ Just $ do h <- unHandle ptr
281+ contents <- execIO $ hGetLine h
282+ return $ ioWrap (EConstant (Str contents))
283+ getOp _ _ = Nothing
284+execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
285+ execApp' env ctxt ret args
286+
287+execApp' env ctxt f args = return (mkEApp f args)
288+
289+
290+-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
291+-- evaluates them, then begins the checks for matching cases.
292+execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
293+execCase env ctxt ns sc args =
298294 let arity = length ns in
299295 if arity <= length args
300− then do args' <- mapM (unLazy env ctxt) (take arity args)
301− trace ("Unlazied args are " ++ take 100 (show args')) $ return ()
302− let amap = zip ns args'
296+ then do -- args' <- mapM tryForce (take arity args)
297+ let amap = zip ns args
303298 caseRes <- execCase' env ctxt amap sc
304299 case caseRes of
305− Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
300+ Just res -> Just <$> execApp' (map (\(n, tm) -> (n, Let EErased tm)) amap ++ env) ctxt res (drop arity args)
306301 Nothing -> return Nothing
307302 else return Nothing
308303
309−execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Exec (Maybe Term)
304+-- | Take bindings and a case tree and examines them, executing the matching case if possible.
305+execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
306+execCase' env ctxt amap (UnmatchedCase _) = trace "Unmatched" $ return Nothing
310307execCase' env ctxt amap (STerm tm) =
311− Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
312−execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap
313− , Just (newCase, newBindings) <- chooseAlt tm alts =
314− execCase' env ctxt (amap ++ newBindings) newCase
315− | otherwise = return Nothing
308+ Just <$> doExec (map (\(n, v) -> (n, Let EErased v)) amap ++ env) ctxt tm
309+execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
310+ do tm' <- tryForce tm
311+ case chooseAlt tm alts of
312+ Just (newCase, newBindings) ->
313+ let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
314+ execCase' env ctxt amap' newCase
315+ Nothing -> return Nothing
316316
317−chooseAlt :: Term -> [CaseAlt] -> Maybe (SC, [(Name, Term)])
317+chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
318318chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
319−chooseAlt (Constant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
320−chooseAlt tm (ConCase n i ns sc : alts) | ((P _ cn _), args) <- unApply tm, cn == n = Just (sc, zip ns args)
319+chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
320+chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
321+ , cn == n = Just (sc, zip ns args)
321322 | otherwise = chooseAlt tm alts
322323chooseAlt tm (_:alts) = chooseAlt tm alts
323324chooseAlt _ [] = Nothing
324325
325326data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
326327
327−idrisType :: FTy -> Type
328−idrisType FUnit = P Ref unitTy (TType (UVal 0))
329−idrisType ft = Constant (idr ft)
328+idrisType :: FTy -> ExecVal
329+idrisType FUnit = EP Ref unitTy EErased
330+idrisType ft = EConstant (idr ft)
330331 where idr FInt = IType
331332 idr FFloat = FlType
332333 idr FChar = ChType
@@ -340,13 +341,13 @@ ptrCon :: Name
340341ptrCon = MN 0 "__Ptr"
341342
342343-- | Convert a Haskell pointer to a Ptr term in TT
343−ptr :: Ptr a -> Term
344−ptr p = App (P (DCon 1 0) ptrCon Erased) (Constant (I (addr p)))
344+ptr :: Ptr a -> ExecVal
345+ptr p = EApp (EP (DCon 1 0) ptrCon EErased) (EConstant (I (addr p)))
345346 where addr p = p `minusPtr` nullPtr
346347
347348-- | Convert a Ptr term in TT to a Haskell pointer
348−unPtr :: Term -> Maybe (Ptr a)
349−unPtr (App (P _ con _) (Constant (I addr))) | con == ptrCon = Just (unAddr addr)
349+unPtr :: ExecVal -> Maybe (Ptr a)
350+unPtr (EApp (EP _ con _) (EConstant (I addr))) | con == ptrCon = Just (unAddr addr)
350351 where unAddr a = nullPtr `plusPtr` a
351352unPtr _ = Nothing
352353
@@ -354,76 +355,77 @@ handleCon :: Name
354355handleCon = MN 0 "__Handle"
355356
356357-- | Convert a Haskell file handle to a handle term in TT (an int)
357−handle :: Handle -> Exec Term
358+handle :: Handle -> Exec ExecVal
358359handle h = do est <- getExecState
359360 let i = exec_next_handle est
360361 putExecState $ est { exec_next_handle = exec_next_handle est + 1
361362 , exec_handles = M.insert i h (exec_handles est)
362363 }
363− return $ App (P (DCon 1 0) handleCon Erased) (Constant (I i))
364+ return $ EHandle i
364365
365−unHandle :: Term -> Exec Handle
366−unHandle (App (P _ hc _) (Constant (I i))) | hc == handleCon =
366+unHandle :: ExecVal -> Exec Handle
367+unHandle (EHandle i) =
367368 do est <- getExecState
368369 case M.lookup i (exec_handles est) of
369370 Just h -> return h
370371 Nothing -> execFail "Bad handle ID"
371372unHandle _ = execFail "Not a handle"
372373
373−call :: Foreign -> [Term] -> Exec (Maybe Term)
374+call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
374375call (FFun name argTypes retType) args =
375376 do fn <- findForeign name
376377 case fn of
377378 Nothing -> return Nothing
378379 Just f -> do res <- call' f args retType
379− return . Just $ mkApp (P Ref (UN "prim__IO") Erased) [idrisType retType, res]
380− where call' :: ForeignFun -> [Term] -> FTy -> Exec Term
380+ return . Just $ mkEApp (EP Ref (UN "prim__IO") EErased) [idrisType retType, res]
381+ where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal
381382 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
382− return (Constant (I (fromIntegral res)))
383+ return (EConstant (I (fromIntegral res)))
383384 call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)
384− return (Constant (Fl (realToFrac res)))
385+ return (EConstant (Fl (realToFrac res)))
385386 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)
386− return (Constant (Ch (castCCharToChar res)))
387+ return (EConstant (Ch (castCCharToChar res)))
387388 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
388389 hStr <- execIO $ peekCString res
389390-- lift $ free res
390− return (Constant (Str hStr))
391+ return (EConstant (Str hStr))
391392
392393 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
393394 return (ptr res)
394395 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
395− return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
396+ return (EP Ref unitCon EErased)
396397-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
397398
398399
399400 prepArgs = map prepArg
400− prepArg (Constant (I i)) = argCInt (fromIntegral i)
401− prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
402− prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
403− prepArg (Constant (Str s)) = argString s
401+ prepArg (EConstant (I i)) = argCInt (fromIntegral i)
402+ prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
403+ prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
404+ prepArg (EConstant (Str s)) = argString s
404405 prepArg ptr | Just p <- unPtr ptr = argPtr p
405406 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
406407
407408
408409
409−foreignFromTT :: Term -> Maybe Foreign
410−foreignFromTT t = case (unApply t) of
411− (_, [(Constant (Str name)), args, ret]) ->
412− do argTy <- unList args
410+foreignFromTT :: ExecVal -> Maybe Foreign
411+foreignFromTT t = case (unApplyV t) of
412+ (_, [(EConstant (Str name)), args, ret]) ->
413+ do argTy <- unEList args
413414 argFTy <- sequence $ map getFTy argTy
414415 retFTy <- getFTy ret
415416 return $ FFun name argFTy retFTy
416417 _ -> trace "failed to construct ffun" Nothing
417418
418−getFTy :: Term -> Maybe FTy
419−getFTy (P _ (UN t) _) = case t of
420− "FInt" -> Just FInt
421− "FFloat" -> Just FFloat
422− "FChar" -> Just FChar
423− "FString" -> Just FString
424− "FPtr" -> Just FPtr
425− "FUnit" -> Just FUnit
426− _ -> Nothing
419+getFTy :: ExecVal -> Maybe FTy
420+getFTy (EP _ (UN t) _) =
421+ case t of
422+ "FInt" -> Just FInt
423+ "FFloat" -> Just FFloat
424+ "FChar" -> Just FChar
425+ "FString" -> Just FString
426+ "FPtr" -> Just FPtr
427+ "FUnit" -> Just FUnit
428+ _ -> Nothing
427429getFTy _ = Nothing
428430
429431unList :: Term -> Maybe [Term]
@@ -434,11 +436,20 @@ unList tm = case unApply tm of
434436 return $ x:rest
435437 (f, args) -> Nothing
436438
439+unEList :: ExecVal -> Maybe [ExecVal]
440+unEList tm = case unApplyV tm of
441+ (nil, [_]) -> Just []
442+ (cons, ([_, x, xs])) ->
443+ do rest <- unEList xs
444+ return $ x:rest
445+ (f, args) -> Nothing
446+
447+
437448toConst :: Term -> Maybe Const
438449toConst (Constant c) = Just c
439450toConst _ = Nothing
440451
441−stepForeign :: [Term] -> Exec (Maybe Term)
452+stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
442453stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
443454 f' <- case (call <$> ffun) of
444455 Just f -> f args