src/Core/Execute.hs · Idris-dev

git.iko.soy/Idris-dev

on 4ed62cc help sign in

Idris-dev/src/Core/Execute.hs

547 lines 26 kB history raw

1{-# LANGUAGE PatternGuards, ExistentialQuantification #-}

2module Core.Execute (execute) where

4import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

7import Core.TT

8import Core.Evaluate

9import Core.CaseTree

11import Debug.Trace

13import Util.DynamicLinker

14import Util.System

16import Control.Applicative hiding (Const)

17import Control.Monad.Trans

18import Control.Monad.Trans.State.Strict

19import Control.Monad.Trans.Error

20import Control.Monad

21import Data.Maybe

22import Data.Bits

23import qualified Data.Map as M

25import Foreign.LibFFI

26import Foreign.C.String

27import Foreign.Marshal.Alloc (free)

28import Foreign.Ptr

30import System.IO

33data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show

35data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs

36 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness

37 , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad

38 , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

39 }

41data ExecVal = EP NameType Name ExecVal

42 | EV Int

43 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)

44 | EApp ExecVal ExecVal

45 | EType UExp

46 | EErased

47 | EConstant Const

48 | forall a. EPtr (Ptr a)

49 | EThunk Int

50 | EHandle Handle

52instance Show ExecVal where

53 show (EP _ n _) = show n

54 show (EV i) = "!!V" ++ show i ++ "!!"

55 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"

56 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"

57 show (EType _) = "Type"

58 show EErased = "[__]"

59 show (EConstant c) = show c

60 show (EPtr p) = "<<ptr " ++ show p ++ ">>"

61 show (EThunk i) = "<<thunk " ++ show i ++ ">>"

62 show (EHandle h) = "<<handle " ++ show h ++ ">>"

64toTT :: ExecVal -> Exec Term

65toTT (EP nt n ty) = (P nt n) <$> (toTT ty)

66toTT (EV i) = return $ V i

67toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

68 b' <- fixBinder b

69 Bind n b' <$> toTT body'

70 where fixBinder (Lam t) = Lam <$> toTT t

71 fixBinder (Pi t) = Pi <$> toTT t

72 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

73 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

74 fixBinder (Hole t) = Hole <$> toTT t

75 fixBinder (GHole t) = GHole <$> toTT t

76 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

77 fixBinder (PVar t) = PVar <$> toTT t

78 fixBinder (PVTy t) = PVTy <$> toTT t

79toTT (EApp e1 e2) = do e1' <- toTT e1

80 e2' <- toTT e2

81 return $ App e1' e2'

82toTT (EType u) = return $ TType u

83toTT EErased = return Erased

84toTT (EConstant c) = return (Constant c)

85toTT (EThunk i) = return (P (DCon 0 0) (MN i "THUNK") Erased) --(force i) >>= toTT

86toTT (EHandle _) = return Erased

88unApplyV :: ExecVal -> (ExecVal, [ExecVal])

89unApplyV tm = ua [] tm

90 where ua args (EApp f a) = ua (a:args) f

91 ua args t = (t, args)

93mkEApp :: ExecVal -> [ExecVal] -> ExecVal

94mkEApp f [] = f

95mkEApp f (a:args) = mkEApp (EApp f a) args

97initState :: Idris ExecState

98initState = do ist <- getIState

99 return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)

100

101type Exec = ErrorT String (StateT ExecState IO)

102

103runExec :: Exec a -> ExecState -> IO (Either String a)

104runExec ex st = fst <$> runStateT (runErrorT ex) st

105

106getExecState :: Exec ExecState

107getExecState = lift get

108

109putExecState :: ExecState -> Exec ()

110putExecState = lift . put

111

112execFail :: String -> Exec a

113execFail = throwError

114

115execIO :: IO a -> Exec a

116execIO = lift . lift

117

118delay :: ExecEnv -> Context -> Term -> Exec ExecVal

119delay env ctxt tm =

120 do st <- getExecState

121 let i = exec_next_thunk st

122 putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)

123 , exec_next_thunk = exec_next_thunk st + 1

124 }

125 return $ EThunk i

126

127force :: Int -> Exec ExecVal

128force i = do st <- getExecState

129 case M.lookup i (exec_thunks st) of

130 Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm

131 case tm' of

132 EThunk i ->

133 do res <- force i

134 update res i

135 return res

136 _ -> do update tm' i

137 return tm'

138 Just (Forced tm) -> return tm

139 Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"

140 where update :: ExecVal -> Int -> Exec ()

141 update tm i = do est <- getExecState

142 putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }

143

144tryForce :: ExecVal -> Exec ExecVal

145tryForce (EThunk i) = force i

146tryForce tm = return tm

147

148debugThunks :: Exec ()

149debugThunks = do st <- getExecState

150 execIO $ putStrLn (take 4000 (show (exec_thunks st)))

151

152execute :: Term -> Idris Term

153execute tm = do est <- initState

154 ctxt <- getContext

155 res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm

156 toTT res

157 case res of

158 Left err -> fail err

159 Right tm' -> return tm'

160

161ioWrap :: ExecVal -> ExecVal

162ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]

163

164ioUnit :: ExecVal

165ioUnit = ioWrap (EP Ref unitCon EErased)

166

167type ExecEnv = [(Name, ExecVal)]

168

169doExec :: ExecEnv -> Context -> Term -> Exec ExecVal

170doExec env ctxt p@(P Ref n ty) | Just v <- lookup n env = return v

171doExec env ctxt p@(P Ref n ty) =

172 do let val = lookupDef n ctxt

173 case val of

174 [Function _ tm] -> doExec env ctxt tm

175 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def

176 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later

177 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

178 doExec env ctxt tm

179 [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)

180 [] -> execFail $ "Could not find " ++ show n ++ " in definitions."

181 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined

182doExec env ctxt p@(P Bound n ty) =

183 case lookup n env of

184 Nothing -> execFail "not found"

185 Just tm -> return tm

186doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)

187doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)

188doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

189 | otherwise = execFail "env too small"

190doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v

191 doExec ((n, v'):env) ctxt body

192doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

193doExec env ctxt tm@(Bind n b body) = return $

194 EBind n (fmap (\_->EErased) b)

195 (\arg -> doExec ((n, arg):env) ctxt body)

196doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)

197doExec env ctxt (Constant c) = return (EConstant c)

198doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

199 doExec env ctxt ((x:xs) !! i)

200doExec env ctxt Erased = return EErased

201doExec env ctxt Impossible = fail "Tried to execute an impossible case"

202doExec env ctxt (TType u) = return (EType u)

203

204execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal

205execApp env ctxt (f, args) = do newF <- doExec env ctxt f

206 laziness <- (++ repeat False) <$> (getLaziness newF)

207 newArgs <- mapM argExec (zip args laziness)

208 execApp' env ctxt newF newArgs

209 where getLaziness (EP _ (UN "lazy") _) = return [False, True]

210 getLaziness (EP _ n _) = do est <- getExecState

211 let argInfo = exec_implicits est

212 case lookupCtxtName n argInfo of

213 [] -> return (repeat False)

214 [ps] -> return $ map lazyarg (snd ps)

215 many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)

216 getLaziness _ = return (repeat False) -- ok due to zip above

217 argExec :: (Term, Bool) -> Exec ExecVal

218 argExec (tm, False) = doExec env ctxt tm

219 argExec (tm, True) = delay env ctxt tm

220

221

222execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

223execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls

224execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =

225 execApp' env ctxt v rest

226

227execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =

228 do v'' <- tryForce v'

229 res <- execApp' env ctxt k [v''] >>= tryForce

230 execApp' env ctxt res rest

231execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =

232 do v' <- tryForce v

233 execApp' env ctxt (mkEApp con [tp, v']) rest

234

235-- Special cases arising from not having access to the C RTS in the interpreter

236execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)

237 | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)

238 execApp' env ctxt ioUnit rest

239execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

240 | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of

241 "r" -> return ReadMode

242 "w" -> return WriteMode

243 "a" -> return AppendMode

244 "rw" -> return ReadWriteMode

245 "wr" -> return ReadWriteMode

246 "r+" -> return ReadWriteMode

247 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)

248 h <- execIO $ openFile f m

249 execApp' env ctxt (ioWrap (EHandle h)) rest

250

251execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)

252 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h

253 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

254 execApp' env ctxt res rest

255

256execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)

257 | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h

258 execApp' env ctxt ioUnit rest

259

260execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EPtr p):rest)

261 | Just (FFun "isNull" _ _) <- foreignFromTT fn = let res = ioWrap . EConstant . I $

262 if p == nullPtr then 1 else 0

263 in execApp' env ctxt res rest

264

265execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun f argTs retT) <- foreignFromTT fn

266 , length xs >= length argTs =

267 do res <- stepForeign (ty:fn:take (length argTs) xs)

268 case res of

269 Nothing -> fail $ "Could not call foreign function \"" ++ f ++

270 "\" with args " ++ show (take (length argTs) xs)

271 Just r -> return (mkEApp r (drop (length argTs) xs))

272 | otherwise = return (mkEApp f args)

273

274execApp' env ctxt f@(EP _ n _) args =

275 do let val = lookupDef n ctxt

276 case val of

277 [Function _ tm] -> fail "should already have been eval'd"

278 [TyDecl nt ty] -> return $ mkEApp f args

279 [Operator tp arity op] ->

280 if length args >= arity

281 then do args' <- mapM tryForce $ take arity args

282 case getOp n args' of

283 Just res -> do r <- res

284 execApp' env ctxt r (drop arity args)

285 Nothing -> return (mkEApp f args)

286 else return (mkEApp f args)

287 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

288 do rhs <- doExec env ctxt tm

289 execApp' env ctxt rhs args

290 [CaseOp _ _ _ _ _ ns sc _ _] ->

291 do res <- execCase env ctxt ns sc args

292 return $ fromMaybe (mkEApp f args) res

293 thing -> return $ mkEApp f args

294 where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

295 getOp (UN "prim__addInt") [EConstant (I i1), EConstant (I i2)] =

296 primRes I (i1 + i2)

297 getOp (UN "prim__andInt") [EConstant (I i1), EConstant (I i2)] =

298 primRes I (i1 .&. i2)

299 getOp (UN "prim__charToInt") [EConstant (Ch c)] =

300 primRes I (fromEnum c)

301 getOp (UN "prim__complInt") [EConstant (I i)] =

302 primRes I (complement i)

303 getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =

304 primRes Str (s1 ++ s2)

305 getOp (UN "prim__divInt") [EConstant (I i1), EConstant (I i2)] =

306 primRes I (i1 `div` i2)

307 getOp (UN "prim__eqChar") [EConstant (Ch c1), EConstant (Ch c2)] =

308 primResBool (c1 == c2)

309 getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =

310 primResBool (i1 == i2)

311 getOp (UN "prim__eqString") [EConstant (Str s1), EConstant (Str s2)] =

312 primResBool (s1 == s2)

313 getOp (UN "prim__gtChar") [EConstant (Ch i1), EConstant (Ch i2)] =

314 primResBool (i1 > i2)

315 getOp (UN "prim__gteChar") [EConstant (Ch i1), EConstant (Ch i2)] =

316 primResBool (i1 >= i2)

317 getOp (UN "prim__gtInt") [EConstant (I i1), EConstant (I i2)] =

318 primResBool (i1 > i2)

319 getOp (UN "prim__gteInt") [EConstant (I i1), EConstant (I i2)] =

320 primResBool (i1 >= i2)

321 getOp (UN "prim__intToFloat") [EConstant (I i)] =

322 primRes Fl (fromRational (toRational i))

323 getOp (UN "prim__intToStr") [EConstant (I i)] =

324 primRes Str (show i)

325 getOp (UN "prim_lenString") [EConstant (Str s)] =

326 primRes I (length s)

327 getOp (UN "prim__ltChar") [EConstant (Ch i1), EConstant (Ch i2)] =

328 primResBool (i1 < i2)

329 getOp (UN "prim__lteChar") [EConstant (Ch i1), EConstant (Ch i2)] =

330 primResBool (i1 <= i2)

331 getOp (UN "prim__lteInt") [EConstant (I i1), EConstant (I i2)] =

332 primResBool (i1 <= i2)

333 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =

334 primResBool (i1 < i2)

335 getOp (UN "prim__modInt") [EConstant (I i1), EConstant (I i2)] =

336 primRes I (i1 `mod` i2)

337 getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =

338 primRes BI (i1 * i2)

339 getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =

340 primRes Fl (i1 * i2)

341 getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =

342 primRes I (i1 * i2)

343 getOp (UN "prim__orInt") [EConstant (I i1), EConstant (I i2)] =

344 primRes I (i1 .|. i2)

345 getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =

346 Just $ do line <- execIO getLine

347 return (EConstant (Str line))

348 getOp (UN "prim__readString") [EHandle h] =

349 Just $ do contents <- execIO $ hGetLine h

350 return (EConstant (Str contents))

351 getOp (UN "prim__shLInt") [EConstant (I i1), EConstant (I i2)] =

352 primRes I (shiftL i1 i2)

353 getOp (UN "prim__shRInt") [EConstant (I i1), EConstant (I i2)] =

354 primRes I (shiftR i1 i2)

355 getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =

356 primRes Str (c:s)

357 getOp (UN "prim__strHead") [EConstant (Str (c:s))] =

358 primRes Ch c

359 getOp (UN "prim__strRev") [EConstant (Str s)] =

360 primRes Str (reverse s)

361 getOp (UN "prim__strTail") [EConstant (Str (c:s))] =

362 primRes Str s

363 getOp (UN "prim__subFloat") [EConstant (Fl i1), EConstant (Fl i2)] =

364 primRes Fl (i1 - i2)

365 getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =

366 primRes I (i1 - i2)

367 getOp (UN "prim__xorInt") [EConstant (I i1), EConstant (I i2)] =

368 primRes I (i1 `xor` i2)

369 getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing

370

371 primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)

372 primRes constr = Just . return . EConstant . constr

373

374 primResBool :: Bool -> Maybe (Exec ExecVal)

375 primResBool b = primRes I (if b then 1 else 0)

376

377execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

378 let (f', as) = unApplyV ret

379 execApp' env ctxt f' (as ++ args)

380execApp' env ctxt (EThunk i) args = do f <- force i

381 execApp' env ctxt f args

382execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)

383execApp' env ctxt f args = return (mkEApp f args)

389-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,

390-- evaluates them, then begins the checks for matching cases.

391execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)

392execCase env ctxt ns sc args =

393 let arity = length ns in

394 if arity <= length args

395 then do let amap = zip ns args

396-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()

397 caseRes <- execCase' env ctxt amap sc

398 case caseRes of

399 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

400 Nothing -> return Nothing

401 else return Nothing

402

403-- | Take bindings and a case tree and examines them, executing the matching case if possible.

404execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)

405execCase' env ctxt amap (UnmatchedCase _) = return Nothing

406execCase' env ctxt amap (STerm tm) =

407 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

408execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

409 do tm' <- tryForce tm

410 case chooseAlt tm' alts of

411 Just (newCase, newBindings) ->

412 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

413 execCase' env ctxt amap' newCase

414 Nothing -> return Nothing

415

416chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])

417chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])

418chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])

419chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm

420 , cn == n = Just (sc, zip ns args)

421 | otherwise = chooseAlt tm alts

422chooseAlt tm (_:alts) = chooseAlt tm alts

423chooseAlt _ [] = Nothing

430idrisType :: FTy -> ExecVal

431idrisType FUnit = EP Ref unitTy EErased

432idrisType ft = EConstant (idr ft)

433 where idr FInt = IType

434 idr FFloat = FlType

435 idr FChar = ChType

436 idr FString = StrType

437 idr FPtr = PtrType

438

439data Foreign = FFun String [FTy] FTy deriving Show

440

441

442call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)

443call (FFun name argTypes retType) args =

444 do fn <- findForeign name

445 case fn of

446 Nothing -> return Nothing

447 Just f -> do res <- call' f args retType

448 return . Just . ioWrap $ res

449 where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal

450 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)

451 return (EConstant (I (fromIntegral res)))

452 call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)

453 return (EConstant (Fl (realToFrac res)))

454 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)

455 return (EConstant (Ch (castCCharToChar res)))

456 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)

457 hStr <- execIO $ peekCString res

458-- lift $ free res

459 return (EConstant (Str hStr))

460

461 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)

462 return (EPtr res)

463 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)

464 return (EP Ref unitCon EErased)

465-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)

466

467

468 prepArgs = map prepArg

469 prepArg (EConstant (I i)) = argCInt (fromIntegral i)

470 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)

471 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

472 prepArg (EConstant (Str s)) = argString s

473 prepArg (EPtr p) = argPtr p

474 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined

475

476

477

478foreignFromTT :: ExecVal -> Maybe Foreign

479foreignFromTT t = case (unApplyV t) of

480 (_, [(EConstant (Str name)), args, ret]) ->

481 do argTy <- unEList args

482 argFTy <- sequence $ map getFTy argTy

483 retFTy <- getFTy ret

484 return $ FFun name argFTy retFTy

485 _ -> trace "failed to construct ffun" Nothing

486

487getFTy :: ExecVal -> Maybe FTy

488getFTy (EP _ (UN t) _) =

489 case t of

490 "FInt" -> Just FInt

491 "FFloat" -> Just FFloat

492 "FChar" -> Just FChar

493 "FString" -> Just FString

494 "FPtr" -> Just FPtr

495 "FUnit" -> Just FUnit

496 _ -> Nothing

497getFTy _ = Nothing

498

499unList :: Term -> Maybe [Term]

500unList tm = case unApply tm of

501 (nil, [_]) -> Just []

502 (cons, ([_, x, xs])) ->

503 do rest <- unList xs

504 return $ x:rest

505 (f, args) -> Nothing

506

507unEList :: ExecVal -> Maybe [ExecVal]

508unEList tm = case unApplyV tm of

509 (nil, [_]) -> Just []

510 (cons, ([_, x, xs])) ->

511 do rest <- unEList xs

512 return $ x:rest

513 (f, args) -> Nothing

514

515

516toConst :: Term -> Maybe Const

517toConst (Constant c) = Just c

518toConst _ = Nothing

519

520stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)

521stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn

522 f' <- case (call <$> ffun) of

523 Just f -> f args

524 Nothing -> return Nothing

525 return f'

526stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"

527

528mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]

529mapMaybeM f [] = return []

530mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs

531 x' <- f x

532 case x' of

533 Just x'' -> return (x'':rest)

534 Nothing -> return rest

535

536findForeign :: String -> Exec (Maybe ForeignFun)

537findForeign fn = do est <- getExecState

538 let libs = exec_dynamic_libs est

539 fns <- mapMaybeM getFn libs

540 case fns of

541 [f] -> return (Just f)

542 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"

543 return Nothing

544 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++

545 show (length fs) ++ " occurrences."

546 return Nothing

547 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)