@@ -11,6 +11,7 @@ import Core.CaseTree
11import Debug.Trace
11import Debug.Trace
13import Util.DynamicLinker
13import Util.DynamicLinker
15import Control.Applicative hiding (Const)
16import Control.Applicative hiding (Const)
16import Control.Monad.Trans
17import Control.Monad.Trans
@@ -102,6 +103,7 @@ execApp env ctxt (f, args) = do newF <- doExec env ctxt f
103execApp' :: Env -> Context -> Term -> [Term] -> Idris Term
104execApp' :: Env -> Context -> Term -> [Term] -> Idris Term
104execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
105execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
106+execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
105execApp' env ctxt (P _ (UN "mkForeign") _) args =
107execApp' env ctxt (P _ (UN "mkForeign") _) args =
106 do res <- stepForeign args
108 do res <- stepForeign args
107 case res of
109 case res of
@@ -147,28 +149,39 @@ execCase env ctxt ns sc args =
147execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Idris (Maybe Term)
149execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Idris (Maybe Term)
148execCase' env ctxt amap (STerm tm) =
150execCase' env ctxt amap (STerm tm) =
149 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
151 Just <$> doExec env (foldl (\c (n, t) -> addToCtxt n t Erased c) ctxt amap) tm
150−execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
152+execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap
151− let (newCase, newBindings) = chooseAlt tm alts in
153+ , Just (newCase, newBindings) <- chooseAlt tm alts =
152 execCase' env ctxt (amap ++ newBindings) newCase
154 execCase' env ctxt (amap ++ newBindings) newCase
155+ | otherwise = return Nothing
154−chooseAlt :: Term -> [CaseAlt] -> (SC, [(Name, Term)])
157+chooseAlt :: Term -> [CaseAlt] -> Maybe (SC, [(Name, Term)])
155−chooseAlt _ (DefaultCase sc : alts) = (sc, [])
158+chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
156−chooseAlt (Constant c) (ConstCase c' sc : alts) | c == c' = (sc, [])
159+chooseAlt (Constant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
157−chooseAlt tm (ConCase n i ns sc : alts) | ((P _ cn _), args) <- unApply tm, cn == n = (sc, zip ns args)
160+chooseAlt tm (ConCase n i ns sc : alts) | ((P _ cn _), args) <- unApply tm, cn == n = Just (sc, zip ns args)
158 | otherwise = chooseAlt tm alts
161 | otherwise = chooseAlt tm alts
159chooseAlt tm (_:alts) = chooseAlt tm alts
162chooseAlt tm (_:alts) = chooseAlt tm alts
160−chooseAlt _ [] = trace "bad pattern match" undefined
163+chooseAlt _ [] = Nothing
162data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
165data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
167+idrisType :: FTy -> Type
168+idrisType FUnit = P Ref unitTy (TType (UVal 0))
169+idrisType ft = Constant (idr ft)
170+ where idr FInt = IType
173+ idr FString = StrType
164data Foreign = FFun String [FTy] FTy deriving Show
176data Foreign = FFun String [FTy] FTy deriving Show
166call :: Foreign -> [Term] -> Idris (Maybe Term)
178call :: Foreign -> [Term] -> Idris (Maybe Term)
167−call (FFun name argTypes retType) args = do fn <- findForeign name
179+call (FFun name argTypes retType) args =
180+ do fn <- findForeign name
168− case fn of
181+ case fn of
169− Nothing -> return Nothing
182+ Nothing -> return Nothing
170− Just f -> do res <- call' f args retType
183+ Just f -> do res <- call' f args retType
171− return . Just $ App (P Ref (UN "prim__IO") Erased) res
184+ return . Just $ mkApp (P Ref (UN "prim__IO") Erased) [idrisType retType, res]
172 where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
185 where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
173 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
186 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
174 return (Constant (I (fromIntegral res)))
187 return (Constant (I (fromIntegral res)))
@@ -246,7 +259,7 @@ mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
246findForeign :: String -> Idris (Maybe ForeignFun)
259findForeign :: String -> Idris (Maybe ForeignFun)
247findForeign fn = do i <- getIState
260findForeign fn = do i <- getIState
248 let libs = idris_dynamic_libs i
261 let libs = idris_dynamic_libs i
249− fns <- mapMaybeM (lift . tryLoadFn fn) libs
262+ fns <- mapMaybeM getFn libs
250 case fns of
263 case fns of
251 [f] -> return (Just f)
264 [f] -> return (Just f)
252 [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"
265 [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"
@@ -254,4 +267,6 @@ findForeign fn = do i <- getIState
254 fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
267 fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
255 show (length fs) ++ " occurrences."
268 show (length fs) ++ " occurrences."
256 return Nothing
269 return Nothing
270+ where getFn lib = lift $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)