@@ -1,3 +1,4 @@
1+{-# LANGUAGE PatternGuards, ExistentialQuantification #-}
12module Core.Execute (execute) where
23
34import Idris.AbsSyntax
@@ -5,104 +6,456 @@ import Idris.AbsSyntaxTree
56
67import Core.TT
78import Core.Evaluate
9+import Core.CaseTree
810
911import Debug.Trace
1012
1113import Util.DynamicLinker
14+import Util.System
1215
1316import Control.Applicative hiding (Const)
1417import Control.Monad.Trans
18+import Control.Monad.Trans.State.Strict
19+import Control.Monad.Trans.Error
1520import Control.Monad
1621import Data.Maybe
22+import qualified Data.Map as M
1723
1824import Foreign.LibFFI
1925import Foreign.C.String
2026import Foreign.Marshal.Alloc (free)
27+import Foreign.Ptr
28+
29+import System.IO
30+
31+
32+data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
33+
34+data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs
35+ , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
36+ , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad
37+ , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
38+ }
39+
40+data ExecVal = EP NameType Name ExecVal
41+ | EV Int
42+ | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
43+ | EApp ExecVal ExecVal
44+ | EType UExp
45+ | EErased
46+ | EConstant Const
47+ | forall a. EPtr (Ptr a)
48+ | EThunk Int
49+ | EHandle Handle
50+
51+instance Show ExecVal where
52+ show (EP _ n _) = show n
53+ show (EV i) = "!!V" ++ show i ++ "!!"
54+ show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
55+ show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
56+ show (EType _) = "Type"
57+ show EErased = "[__]"
58+ show (EConstant c) = show c
59+ show (EPtr p) = "<<ptr " ++ show p ++ ">>"
60+ show (EThunk i) = "<<thunk " ++ show i ++ ">>"
61+ show (EHandle h) = "<<handle " ++ show h ++ ">>"
62+
63+toTT :: ExecVal -> Exec Term
64+toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
65+toTT (EV i) = return $ V i
66+toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
67+ b' <- fixBinder b
68+ Bind n b' <$> toTT body'
69+ where fixBinder (Lam t) = Lam <$> toTT t
70+ fixBinder (Pi t) = Pi <$> toTT t
71+ fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
72+ fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
73+ fixBinder (Hole t) = Hole <$> toTT t
74+ fixBinder (GHole t) = GHole <$> toTT t
75+ fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
76+ fixBinder (PVar t) = PVar <$> toTT t
77+ fixBinder (PVTy t) = PVTy <$> toTT t
78+toTT (EApp e1 e2) = do e1' <- toTT e1
79+ e2' <- toTT e2
80+ return $ App e1' e2'
81+toTT (EType u) = return $ TType u
82+toTT EErased = return Erased
83+toTT (EConstant c) = return (Constant c)
84+toTT (EThunk i) = return (P (DCon 0 0) (MN i "THUNK") Erased) --(force i) >>= toTT
85+toTT (EHandle _) = return Erased
86+
87+unApplyV :: ExecVal -> (ExecVal, [ExecVal])
88+unApplyV tm = ua [] tm
89+ where ua args (EApp f a) = ua (a:args) f
90+ ua args t = (t, args)
91+
92+mkEApp :: ExecVal -> [ExecVal] -> ExecVal
93+mkEApp f [] = f
94+mkEApp f (a:args) = mkEApp (EApp f a) args
95+
96+initState :: Idris ExecState
97+initState = do ist <- getIState
98+ return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
99+
100+type Exec = ErrorT String (StateT ExecState IO)
101+
102+runExec :: Exec a -> ExecState -> IO (Either String a)
103+runExec ex st = fst <$> runStateT (runErrorT ex) st
104+
105+getExecState :: Exec ExecState
106+getExecState = lift get
107+
108+putExecState :: ExecState -> Exec ()
109+putExecState = lift . put
110+
111+execFail :: String -> Exec a
112+execFail = throwError
113+
114+execIO :: IO a -> Exec a
115+execIO = lift . lift
116+
117+delay :: ExecEnv -> Context -> Term -> Exec ExecVal
118+delay env ctxt tm =
119+ do st <- getExecState
120+ let i = exec_next_thunk st
121+ putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)
122+ , exec_next_thunk = exec_next_thunk st + 1
123+ }
124+ return $ EThunk i
125+
126+force :: Int -> Exec ExecVal
127+force i = do st <- getExecState
128+ case M.lookup i (exec_thunks st) of
129+ Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm
130+ case tm' of
131+ EThunk i ->
132+ do res <- force i
133+ update res i
134+ return res
135+ _ -> do update tm' i
136+ return tm'
137+ Just (Forced tm) -> return tm
138+ Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"
139+ where update :: ExecVal -> Int -> Exec ()
140+ update tm i = do est <- getExecState
141+ putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }
142+
143+tryForce :: ExecVal -> Exec ExecVal
144+tryForce (EThunk i) = force i
145+tryForce tm = return tm
146+
147+debugThunks :: Exec ()
148+debugThunks = do st <- getExecState
149+ execIO $ putStrLn (take 4000 (show (exec_thunks st)))
150+
151+execute :: Term -> Idris Term
152+execute tm = do est <- initState
153+ ctxt <- getContext
154+ res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm
155+ toTT res
156+ case res of
157+ Left err -> fail err
158+ Right tm' -> return tm'
159+
160+ioWrap :: ExecVal -> ExecVal
161+ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]
162+
163+ioUnit :: ExecVal
164+ioUnit = ioWrap (EP Ref unitCon EErased)
165+
166+type ExecEnv = [(Name, ExecVal)]
167+
168+doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
169+doExec env ctxt p@(P Ref n ty) =
170+ do let val = lookupDef n ctxt
171+ case val of
172+ [Function _ tm] -> doExec env ctxt tm
173+ [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
174+ [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
175+ [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
176+ doExec env ctxt tm
177+ [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)
178+ thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
179+doExec env ctxt p@(P Bound n ty) =
180+ case lookup n env of
181+ Nothing -> execFail "not found"
182+ Just tm -> return tm
183+doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)
184+doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
185+doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
186+ | otherwise = execFail "env too small"
187+doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
188+ doExec ((n, v'):env) ctxt body
189+doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
190+doExec env ctxt tm@(Bind n b body) = return $
191+ EBind n (fmap (\_->EErased) b)
192+ (\arg -> doExec ((n, arg):env) ctxt body)
193+doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
194+doExec env ctxt (Constant c) = return (EConstant c)
195+doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
196+ doExec env ctxt ((x:xs) !! i)
197+doExec env ctxt Erased = return EErased
198+doExec env ctxt Impossible = fail "Tried to execute an impossible case"
199+doExec env ctxt (TType u) = return (EType u)
200+
201+execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
202+execApp env ctxt (f, args) = do newF <- doExec env ctxt f
203+ laziness <- (++ repeat False) <$> (getLaziness newF)
204+ newArgs <- mapM argExec (zip args laziness)
205+ execApp' env ctxt newF newArgs
206+ where getLaziness (EP _ (UN "lazy") _) = return [False, True]
207+ getLaziness (EP _ n _) = do est <- getExecState
208+ let argInfo = exec_implicits est
209+ case lookupCtxtName n argInfo of
210+ [] -> return (repeat False)
211+ [ps] -> return $ map lazyarg (snd ps)
212+ many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
213+ getLaziness _ = return (repeat False) -- ok due to zip above
214+ argExec :: (Term, Bool) -> Exec ExecVal
215+ argExec (tm, False) = doExec env ctxt tm
216+ argExec (tm, True) = delay env ctxt tm
217+
218+
219+execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
220+execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
221+execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
222+ execApp' env ctxt v rest
223+
224+execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
225+ do v'' <- tryForce v'
226+ res <- execApp' env ctxt k [v''] >>= tryForce
227+ execApp' env ctxt res rest
228+execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =
229+ do v' <- tryForce v
230+ execApp' env ctxt (mkEApp con [tp, v']) rest
231+
232+-- Special cases arising from not having access to the C RTS in the interpreter
233+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
234+ | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
235+ execApp' env ctxt ioUnit rest
236+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
237+ | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of
238+ "r" -> return ReadMode
239+ "w" -> return WriteMode
240+ "a" -> return AppendMode
241+ "rw" -> return ReadWriteMode
242+ "wr" -> return ReadWriteMode
243+ "r+" -> return ReadWriteMode
244+ _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
245+ h <- execIO $ openFile f m
246+ execApp' env ctxt (ioWrap (EHandle h)) rest
247+
248+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
249+ | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h
250+ let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
251+ execApp' env ctxt res rest
252+
253+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
254+ | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h
255+ execApp' env ctxt ioUnit rest
256+
257+
258+execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn
259+ , length xs >= length argTs =
260+ do res <- stepForeign (ty:fn:take (length argTs) xs)
261+ case res of
262+ Nothing -> fail "Could not call foreign function"
263+ Just r -> return (mkEApp r (drop (length argTs) xs))
264+ | otherwise = return (mkEApp f args)
265+
266+execApp' env ctxt f@(EP _ n _) args =
267+ do let val = lookupDef n ctxt
268+ case val of
269+ [Function _ tm] -> fail "should already have been eval'd"
270+ [TyDecl nt ty] -> return $ mkEApp f args
271+ [Operator tp arity op] ->
272+ if length args >= arity
273+ then do args' <- mapM tryForce $ take arity args
274+ case getOp n args' of
275+ Just res -> do r <- res
276+ execApp' env ctxt r (drop arity args)
277+ Nothing -> return (mkEApp f args)
278+ else return (mkEApp f args)
279+ [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
280+ do rhs <- doExec env ctxt tm
281+ execApp' env ctxt rhs args
282+ [CaseOp _ _ _ _ _ ns sc _ _] ->
283+ do res <- execCase env ctxt ns sc args
284+ return $ fromMaybe (mkEApp f args) res
285+ thing -> return $ mkEApp f args
286+ where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
287+ getOp (UN "prim__addInt") [EConstant (I i1), EConstant (I i2)] =
288+ primRes I (i1 + i2)
289+ getOp (UN "prim__charToInt") [EConstant (Ch c)] =
290+ primRes I (fromEnum c)
291+ getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =
292+ primRes Str (s1 ++ s2)
293+ getOp (UN "prim__eqChar") [EConstant (Ch c1), EConstant (Ch c2)] =
294+ primResBool (c1 == c2)
295+ getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =
296+ primResBool (i1 == i2)
297+ getOp (UN "prim__eqString") [EConstant (Str s1), EConstant (Str s2)] =
298+ primResBool (s1 == s2)
299+ getOp (UN "prim__intToFloat") [EConstant (I i)] =
300+ primRes Fl (fromRational (toRational i))
301+ getOp (UN "prim__intToStr") [EConstant (I i)] =
302+ primRes Str (show i)
303+ getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =
304+ primResBool (i1 < i2)
305+ getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =
306+ primRes BI (i1 * i2)
307+ getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
308+ primRes Fl (i1 * i2)
309+ getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =
310+ primRes I (i1 * i2)
311+ getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
312+ Just $ do line <- execIO getLine
313+ return (EConstant (Str line))
314+ getOp (UN "prim__readString") [EHandle h] =
315+ Just $ do contents <- execIO $ hGetLine h
316+ return (EConstant (Str contents))
317+ getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =
318+ primRes Str (c:s)
319+ getOp (UN "prim__strHead") [EConstant (Str (c:s))] =
320+ primRes Ch c
321+ getOp (UN "prim__strRev") [EConstant (Str s)] =
322+ primRes Str (reverse s)
323+ getOp (UN "prim__strTail") [EConstant (Str (c:s))] =
324+ primRes Str s
325+ getOp (UN "prim__subFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
326+ primRes Fl (i1 - i2)
327+ getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
328+ primRes I (i1 - i2)
329+ getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing
330+
331+ primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)
332+ primRes constr = Just . return . EConstant . constr
333+
334+ primResBool :: Bool -> Maybe (Exec ExecVal)
335+ primResBool b = primRes I (if b then 1 else 0)
336+
337+execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
338+ let (f', as) = unApplyV ret
339+ execApp' env ctxt f' (as ++ args)
340+execApp' env ctxt (EThunk i) args = do f <- force i
341+ execApp' env ctxt f args
342+execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)
343+execApp' env ctxt f args = return (mkEApp f args)
344+
345+
346+
347+
348+
349+-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
350+-- evaluates them, then begins the checks for matching cases.
351+execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
352+execCase env ctxt ns sc args =
353+ let arity = length ns in
354+ if arity <= length args
355+ then do let amap = zip ns args
356+ caseRes <- execCase' env ctxt amap sc
357+ case caseRes of
358+ Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
359+ Nothing -> return Nothing
360+ else return Nothing
361+
362+-- | Take bindings and a case tree and examines them, executing the matching case if possible.
363+execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
364+execCase' env ctxt amap (UnmatchedCase _) = return Nothing
365+execCase' env ctxt amap (STerm tm) =
366+ Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
367+execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
368+ do tm' <- tryForce tm
369+ case chooseAlt tm' alts of
370+ Just (newCase, newBindings) ->
371+ let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
372+ execCase' env ctxt amap' newCase
373+ Nothing -> return Nothing
374+
375+chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
376+chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
377+chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
378+chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
379+ , cn == n = Just (sc, zip ns args)
380+ | otherwise = chooseAlt tm alts
381+chooseAlt tm (_:alts) = chooseAlt tm alts
382+chooseAlt _ [] = Nothing
21383
22−-- | Attempt to perform a side effect. Return either Just the next step in
23−-- evaluation (after performing the side effect through IO), or Nothing if no
24−-- IO was performed.
25−--
26−-- This function is exceedingly generous about what it will accept in order to
27−-- enable convenient testing at the REPL.
28−step :: TT Name -> Idris (Maybe (TT Name))
29−step tm = step' (unApply tm)
30− where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped
31− step' (P _ (UN "mkForeign") _, args) = stepForeign args
32− step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)
33− step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =
34− do line <- lift $ getLine
35− return . Just . Constant . Str $ line
36− step' _ = return Nothing
37−
38−-- | Perform side effects until no more can be performed, then return the
39−-- resulting term (possibly the argument).
40−execute :: TT Name -> Idris (TT Name)
41−execute tm = case unApply tm of
42− (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg
43− _ -> return tm
44− where execute' tm = do stepped <- step tm
45− case stepped of
46− Nothing -> return tm
47− Just tm' -> execute' tm'
48384
49385
50386
51387data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
52388
389+idrisType :: FTy -> ExecVal
390+idrisType FUnit = EP Ref unitTy EErased
391+idrisType ft = EConstant (idr ft)
392+ where idr FInt = IType
393+ idr FFloat = FlType
394+ idr FChar = ChType
395+ idr FString = StrType
396+ idr FPtr = PtrType
397+
53398data Foreign = FFun String [FTy] FTy deriving Show
54399
55−call :: Foreign -> [TT Name] -> Idris (Maybe (TT Name))
56−call (FFun name argTypes retType) args = do fn <- findForeign name
57− case fn of
58− Nothing -> return Nothing
59− Just f -> return . Just =<< call' f args retType
60− where call' :: ForeignFun -> [TT Name] -> FTy -> Idris (TT Name)
61− call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
62− return (Constant (I (fromIntegral res)))
63− call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)
64− return (Constant (Fl (realToFrac res)))
65− call' (Fun _ h) args FChar = do res <- lift $ callFFI h retCChar (prepArgs args)
66− return (Constant (Ch (castCCharToChar res)))
67− call' (Fun _ h) args FString = do res <- lift $ callFFI h retCString (prepArgs args)
68− hStr <- lift $ peekCString res
400+
401+call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
402+call (FFun name argTypes retType) args =
403+ do fn <- findForeign name
404+ case fn of
405+ Nothing -> return Nothing
406+ Just f -> do res <- call' f args retType
407+ return . Just . ioWrap $ res
408+ where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal
409+ call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
410+ return (EConstant (I (fromIntegral res)))
411+ call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)
412+ return (EConstant (Fl (realToFrac res)))
413+ call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)
414+ return (EConstant (Ch (castCCharToChar res)))
415+ call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
416+ hStr <- execIO $ peekCString res
69417-- lift $ free res
70− return (Constant (Str hStr))
71−-- awaiting Const constructor for pointers
72−-- call' (Fun _ h) args FPtr = do res <- lift $ callFFI h retPtr (prepArgs args)
73−-- return (Constant (Ch (castCCharToChar res)))
74− call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)
75− return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
418+ return (EConstant (Str hStr))
419+
420+ call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
421+ return (EPtr res)
422+ call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
423+ return (EP Ref unitCon EErased)
424+-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
425+
76426
77427 prepArgs = map prepArg
78− prepArg (Constant (I i)) = argCInt (fromIntegral i)
79− prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
80− prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
81− prepArg (Constant (Str s)) = argString s
428+ prepArg (EConstant (I i)) = argCInt (fromIntegral i)
429+ prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
430+ prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
431+ prepArg (EConstant (Str s)) = argString s
432+ prepArg (EPtr p) = argPtr p
433+ prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
82434
83435
84436
85−foreignFromTT :: TT Name -> Maybe Foreign
86−foreignFromTT t = case (unApply t) of
87− (_, [(Constant (Str name)), args, ret]) ->
88− do argTy <- unList args
437+foreignFromTT :: ExecVal -> Maybe Foreign
438+foreignFromTT t = case (unApplyV t) of
439+ (_, [(EConstant (Str name)), args, ret]) ->
440+ do argTy <- unEList args
89441 argFTy <- sequence $ map getFTy argTy
90442 retFTy <- getFTy ret
91443 return $ FFun name argFTy retFTy
92− _ -> Nothing
93−
94−getFTy :: TT Name -> Maybe FTy
95−getFTy (P _ (UN t) _) = case t of
96− "FInt" -> Just FInt
97− "FFloat" -> Just FFloat
98− "FChar" -> Just FChar
99− "FString" -> Just FString
100− "FPtr" -> Just FPtr
101− "FUnit" -> Just FUnit
102− _ -> Nothing
444+ _ -> trace "failed to construct ffun" Nothing
445+
446+getFTy :: ExecVal -> Maybe FTy
447+getFTy (EP _ (UN t) _) =
448+ case t of
449+ "FInt" -> Just FInt
450+ "FFloat" -> Just FFloat
451+ "FChar" -> Just FChar
452+ "FString" -> Just FString
453+ "FPtr" -> Just FPtr
454+ "FUnit" -> Just FUnit
455+ _ -> Nothing
103456getFTy _ = Nothing
104457
105−unList :: TT Name -> Maybe [TT Name]
458+unList :: Term -> Maybe [Term]
106459unList tm = case unApply tm of
107460 (nil, [_]) -> Just []
108461 (cons, ([_, x, xs])) ->
@@ -110,11 +463,20 @@ unList tm = case unApply tm of
110463 return $ x:rest
111464 (f, args) -> Nothing
112465
113−toConst :: TT Name -> Maybe Const
466+unEList :: ExecVal -> Maybe [ExecVal]
467+unEList tm = case unApplyV tm of
468+ (nil, [_]) -> Just []
469+ (cons, ([_, x, xs])) ->
470+ do rest <- unEList xs
471+ return $ x:rest
472+ (f, args) -> Nothing
473+
474+
475+toConst :: Term -> Maybe Const
114476toConst (Constant c) = Just c
115477toConst _ = Nothing
116478
117−stepForeign :: [TT Name] -> Idris (Maybe (TT Name))
479+stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
118480stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
119481 f' <- case (call <$> ffun) of
120482 Just f -> f args
@@ -130,15 +492,15 @@ mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
130492 Just x'' -> return (x'':rest)
131493 Nothing -> return rest
132494
133−findForeign :: String -> Idris (Maybe ForeignFun)
134−findForeign fn = do i <- getIState
135− let libs = idris_dynamic_libs i
136− fns <- mapMaybeM (lift . tryLoadFn fn) libs
495+findForeign :: String -> Exec (Maybe ForeignFun)
496+findForeign fn = do est <- getExecState
497+ let libs = exec_dynamic_libs est
498+ fns <- mapMaybeM getFn libs
137499 case fns of
138500 [f] -> return (Just f)
139− [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"
501+ [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
140502 return Nothing
141− fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
142− show (length fs) ++ " occurrences."
503+ fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
504+ show (length fs) ++ " occurrences."
143505 return Nothing
144−
506+ where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)