@@ -55,7 +55,7 @@ import System.IO
5555-- Nothing -> return tm
5656-- Just tm' -> execute' tm'
5757
58−data Lazy = Delayed Term | Forced Term
58+data Lazy = Delayed Env Context Term | Forced Term
5959
6060data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs
6161 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
@@ -89,21 +89,40 @@ execIO = lift . lift
8989thunk :: Name
9090thunk = MN 0 "__execThunk"
9191
92−delay :: Term -> Exec Term
93−delay tm = do st <- getExecState
94− let i = exec_next_thunk st
95− putExecState $ st { exec_thunks = M.insert i (Delayed tm) (exec_thunks st)
96− , exec_next_thunk = exec_next_thunk st + 1
97− }
98− return $ App (P Ref thunk Erased) (Constant (I i))
92+delay :: Env -> Context -> Term -> Exec Term
93+delay env ctxt tm =
94+ do st <- getExecState
95+ let i = exec_next_thunk st
96+ putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)
97+ , exec_next_thunk = exec_next_thunk st + 1
98+ }
99+ return $ App (P (DCon 1 0) thunk Erased) (Constant (I i))
99100
100101force :: Int -> Exec Term
101102force i = do st <- getExecState
102− let thunk = M.lookup i (exec_thunks st)
103− case thunk of
104− Just (Delayed tm) -> return tm -- FIXME DO THE EXEC
103+ case M.lookup i (exec_thunks st) of
104+ Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm
105+ case tm' of
106+ App (P _ thnk _) (Constant (I i)) | thnk == thunk ->
107+ do res <- force i
108+ update res i
109+ return res
110+ _ -> do update tm' i
111+ return tm'
105112 Just (Forced tm) -> return tm
106113 Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"
114+ where update :: Term -> Int -> Exec ()
115+ update tm i = do est <- getExecState
116+ putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }
117+
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+
107126
108127execute :: Term -> Idris Term
109128execute tm = do est <- initState
@@ -114,7 +133,7 @@ execute tm = do est <- initState
114133 Right tm' -> return tm'
115134
116135ioWrap :: Term -> Term
117−ioWrap = App (P Ref (UN "prim__IO") Erased)
136+ioWrap tm = mkApp (P Ref (UN "prim__IO") Erased) [Erased, tm]
118137
119138ioUnit :: Term
120139ioUnit = ioWrap (P Ref unitCon Erased)
@@ -132,11 +151,12 @@ doExec env ctxt p@(P Ref n ty) =
132151 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
133152 doExec env ctxt tm
134153 [CaseOp _ _ _ _ _ ns sc _ _] -> return p
135− thing -> trace ("got to " ++ show thing) $ undefined
136−doExec env ctxt p@(P Bound n ty) = case (lookupDef n ctxt) of -- bound vars must be Function
137− [Function ty tm] -> doExec env ctxt tm
138− [] -> return p
139− x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
154+ thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
155+doExec 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)
140160doExec env ctxt p@(P (DCon _ _) n _) = return p
141161doExec env ctxt p@(P (TCon _ _) n _) = return p
142162doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
@@ -159,30 +179,48 @@ doExec env ctxt Impossible = fail "Tried to execute an impossible case"
159179doExec env ctxt (TType u) = return (TType u)
160180
161181execApp :: 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)
162184execApp env ctxt (f, args) = do newF <- doExec env ctxt f
163− laziness <- getLaziness newF
164− newArgs <- mapM (doExec env ctxt) args
165− -- trace (show newF ++ show (zip args laziness)) $ return ()
185+ laziness <- (getLaziness newF) >>= return . (++ repeat False)
186+ newArgs <- mapM argExec (zip args laziness)
187+ trace ((take 40 (show newF)) ++ " " ++ show (map (take 100 . show) (zip args laziness))) $ return ()
166188 execApp' env ctxt newF newArgs
167− where getLaziness (P _ (UN "lazy") _) = return [True]
189+ where getLaziness (P _ (UN "io_bind") _) = return [False, False, False, True]
190+ getLaziness (P _ (UN "lazy") _) = return [True]
168191 getLaziness (P _ n _) = do est <- getExecState
169192 let argInfo = exec_implicits est
193+ trace ("Looking for laziness of " ++ show n ++ ", found " ++ (take 1000 . show $ lookupCtxtName n argInfo)) $ return ()
170194 case lookupCtxtName n argInfo of
171195 [] -> return (repeat False)
172196 [ps] -> return $ map lazyarg (snd ps)
173− many -> fail $ "Ambiguous " ++ show n ++ ", found " ++ show many
197+ many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
174198 getLaziness x = return (repeat False) -- ok due to zip above
199+ argExec :: (Term, Bool) -> Exec Term
200+ argExec (tm, False) = doExec env ctxt tm
201+ argExec (tm, True) = delay env ctxt tm
175202
176203
177204execApp' :: Env -> Context -> Term -> [Term] -> Exec Term
178205execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
179−execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
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)
180217
181218-- Special cases arising from not having access to the C RTS in the interpreter
182219
183−execApp' env ctxt (P _ (UN "mkForeign") _) [_, fn, Constant (Str arg)]
184− | Just (FFun "putStr" _ _) <- foreignFromTT fn = execIO (putStr arg) >> return ioUnit
185−execApp' env ctxt (P _ (UN "mkForeign") _) [_, fn, Constant (Str f), Constant (Str mode)]
220+execApp' env ctxt (P _ (UN "mkForeign") _) (_:fn:Constant (Str arg):rest)
221+ | 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)
186224 | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do trace ("Opening " ++ f ++ " with " ++ mode) $ return ()
187225 m <- case mode of
188226 "r" -> return ReadMode
@@ -194,17 +232,24 @@ execApp' env ctxt (P _ (UN "mkForeign") _) [_, fn, Constant (Str f), Constant (S
194232 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
195233 h <- execIO $ openFile f m
196234 h' <- handle h
197− return (ioWrap h')
235+ trace ("Got " ++ (take 100 (show h') ++ " and " ++ (take 100 (show rest)))) (return ())
236+ doExec env ctxt (mkApp (ioWrap h') rest)
237+
238+execApp' env ctxt (P _ (UN "mkForeign") _) (_:fn:fh:rest)
239+ | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = trace ("feof") $
240+ do h <- unHandle fh
241+ eofp <- execIO $ hIsEOF h
242+ let res = ioWrap (Constant (I $ if eofp then 1 else 0))
243+ doExec env ctxt (mkApp res rest)
198244
199245
200−execApp' env ctxt (P _ (UN "mkForeign") _) args =
201− do res <- stepForeign args
246+execApp' env ctxt f@(P _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn
247+ , length xs >= length argTs =
248+ do res <- stepForeign (ty:fn:take (length argTs) xs)
202249 case res of
203250 Nothing -> fail "Could not call foreign function"
204− Just r -> return r
205−execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
206− do line <- execIO getLine
207− return (Constant (Str line))
251+ Just r -> return (mkApp r (drop (length argTs) xs))
252+ | otherwise = return (mkApp f args)
208253
209254execApp' env ctxt (P _ (UN "prim__concat") _) [Constant (Str s1), Constant (Str s2)] =
210255 return $ Constant (Str (s1 ++ s2))
@@ -218,7 +263,16 @@ execApp' env ctxt (P _ (UN "prim__ltInt") _) [Constant (I i1), Constant (I i2)]
218263execApp' env ctxt (P _ (UN "prim__subInt") _) [Constant (I i1), Constant (I i2)] =
219264 return . Constant . I $ i1 - i2
220265
221−execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] = trace "readString" $ undefined
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))
222276
223277execApp' env ctxt f@(P _ n _) args =
224278 do let val = lookupDef n ctxt
@@ -240,10 +294,12 @@ execApp' env ctxt bnd@(Bind n b body) (arg:args) = let ctxt' = addToCtxt n arg E
240294execApp' env ctxt f args = return (mkApp f args)
241295
242296execCase :: Env -> Context -> [Name] -> SC -> [Term] -> Exec (Maybe Term)
243−execCase env ctxt ns sc args =
297+execCase env ctxt ns sc args = trace ("Case execution, args are " ++ take 100 (show (zip ns args))) $
244298 let arity = length ns in
245299 if arity <= length args
246− then do let amap = (zip ns (take arity 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'
247303 caseRes <- execCase' env ctxt amap sc
248304 case caseRes of
249305 Just res-> Just <$> doExec env ctxt (mkApp res (drop arity args))
@@ -294,6 +350,9 @@ unPtr (App (P _ con _) (Constant (I addr))) | con == ptrCon = Just (unAddr addr)
294350 where unAddr a = nullPtr `plusPtr` a
295351unPtr _ = Nothing
296352
353+handleCon :: Name
354+handleCon = MN 0 "__Handle"
355+
297356-- | Convert a Haskell file handle to a handle term in TT (an int)
298357handle :: Handle -> Exec Term
299358handle h = do est <- getExecState
@@ -301,10 +360,10 @@ handle h = do est <- getExecState
301360 putExecState $ est { exec_next_handle = exec_next_handle est + 1
302361 , exec_handles = M.insert i h (exec_handles est)
303362 }
304− return $ Constant (I i)
363+ return $ App (P (DCon 1 0) handleCon Erased) (Constant (I i))
305364
306365unHandle :: Term -> Exec Handle
307−unHandle (Constant (I i)) =
366+unHandle (App (P _ hc _) (Constant (I i))) | hc == handleCon =
308367 do est <- getExecState
309368 case M.lookup i (exec_handles est) of
310369 Just h -> return h
@@ -343,7 +402,7 @@ call (FFun name argTypes retType) args =
343402 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
344403 prepArg (Constant (Str s)) = argString s
345404 prepArg ptr | Just p <- unPtr ptr = argPtr p
346− prepArg other = trace ("Could not use " ++ show other ++ " as FFI arg.") undefined
405+ prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
347406
348407
349408