@@ -11,6 +11,7 @@ import Core.CaseTree
1111import Debug.Trace
1212
1313import Util.DynamicLinker
14+import Util.System
1415
1516import Control.Applicative hiding (Const)
1617import Control.Monad.Trans
@@ -102,6 +103,7 @@ execApp env ctxt (f, args) = do newF <- doExec env ctxt f
102103
103104execApp' :: Env -> Context -> Term -> [Term] -> Idris Term
104105execApp' 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
105107execApp' env ctxt (P _ (UN "mkForeign") _) args =
106108 do res <- stepForeign args
107109 case res of
@@ -147,28 +149,39 @@ execCase env ctxt ns sc args =
147149execCase' :: Env -> Context -> [(Name, Term)] -> SC -> Idris (Maybe Term)
148150execCase' env ctxt amap (STerm tm) =
149151 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 =
151− let (newCase, newBindings) = chooseAlt tm alts in
152+execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap
153+ , Just (newCase, newBindings) <- chooseAlt tm alts =
152154 execCase' env ctxt (amap ++ newBindings) newCase
155+ | otherwise = return Nothing
153156
154−chooseAlt :: Term -> [CaseAlt] -> (SC, [(Name, Term)])
155−chooseAlt _ (DefaultCase sc : alts) = (sc, [])
156−chooseAlt (Constant c) (ConstCase c' sc : alts) | c == c' = (sc, [])
157−chooseAlt tm (ConCase n i ns sc : alts) | ((P _ cn _), args) <- unApply tm, cn == n = (sc, zip ns args)
157+chooseAlt :: Term -> [CaseAlt] -> Maybe (SC, [(Name, Term)])
158+chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
159+chooseAlt (Constant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
160+chooseAlt tm (ConCase n i ns sc : alts) | ((P _ cn _), args) <- unApply tm, cn == n = Just (sc, zip ns args)
158161 | otherwise = chooseAlt tm alts
159162chooseAlt tm (_:alts) = chooseAlt tm alts
160−chooseAlt _ [] = trace "bad pattern match" undefined
163+chooseAlt _ [] = Nothing
161164
162165data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
163166
167+idrisType :: FTy -> Type
168+idrisType FUnit = P Ref unitTy (TType (UVal 0))
169+idrisType ft = Constant (idr ft)
170+ where idr FInt = IType
171+ idr FFloat = FlType
172+ idr FChar = ChType
173+ idr FString = StrType
174+ idr FPtr = PtrType
175+
164176data Foreign = FFun String [FTy] FTy deriving Show
165177
166178call :: Foreign -> [Term] -> Idris (Maybe Term)
167−call (FFun name argTypes retType) args = do fn <- findForeign name
168− case fn of
169− Nothing -> return Nothing
170− Just f -> do res <- call' f args retType
171− return . Just $ App (P Ref (UN "prim__IO") Erased) res
179+call (FFun name argTypes retType) args =
180+ do fn <- findForeign name
181+ case fn of
182+ Nothing -> return Nothing
183+ Just f -> do res <- call' f args retType
184+ return . Just $ mkApp (P Ref (UN "prim__IO") Erased) [idrisType retType, res]
172185 where call' :: ForeignFun -> [Term] -> FTy -> Idris Term
173186 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
174187 return (Constant (I (fromIntegral res)))
@@ -246,7 +259,7 @@ mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
246259findForeign :: String -> Idris (Maybe ForeignFun)
247260findForeign fn = do i <- getIState
248261 let libs = idris_dynamic_libs i
249− fns <- mapMaybeM (lift . tryLoadFn fn) libs
262+ fns <- mapMaybeM getFn libs
250263 case fns of
251264 [f] -> return (Just f)
252265 [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"
@@ -254,4 +267,6 @@ findForeign fn = do i <- getIState
254267 fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
255268 show (length fs) ++ " occurrences."
256269 return Nothing
270+ where getFn lib = lift $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
271+
257272