@@ -1,4 +1,4 @@
1−{-# LANGUAGE PatternGuards #-}
1+{-# LANGUAGE PatternGuards, ExistentialQuantification #-}
22module Core.Execute (execute) where
33
44import Idris.AbsSyntax
@@ -35,8 +35,6 @@ data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the res
3535 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
3636 , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad
3737 , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
38− , exec_handles :: M.Map Int Handle -- ^ Opened files
39− , exec_next_handle :: Int -- ^ Ensure opened file key uniqueness
4038 }
4139
4240data ExecVal = EP NameType Name ExecVal
@@ -46,20 +44,21 @@ data ExecVal = EP NameType Name ExecVal
4644 | EType UExp
4745 | EErased
4846 | EConstant Const
49−-- | ETmp Int
47+ | forall a. EPtr (Ptr a)
5048 | EThunk Int
51− | EHandle Int
49+ | EHandle Handle
5250
5351instance Show ExecVal where
54− show (EP _ n _) = show n
55− show (EV i) = "!!V" ++ show i ++ "!!"
52+ show (EP _ n _) = show n
53+ show (EV i) = "!!V" ++ show i ++ "!!"
5654 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>> "
57− show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
58− show (EType _) = "Type"
59− show EErased = "[__]"
60− show (EConstant c) = show c
61− show (EThunk i) = "<<thunk " ++ show i ++ ">>"
62− show (EHandle i) = "<<handle " ++ show i ++ ">>"
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 ++ ">>"
6362
6463toTT :: ExecVal -> Exec Term
6564toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
@@ -96,7 +95,7 @@ mkEApp f (a:args) = mkEApp (EApp f a) args
9695
9796initState :: Idris ExecState
9897initState = do ist <- getIState
99− return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist) M.empty 0
98+ return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
10099
101100type Exec = ErrorT String (StateT ExecState IO)
102101
@@ -241,18 +240,15 @@ execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (S
241240 "r+" -> return ReadWriteMode
242241 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
243242 h <- execIO $ openFile f m
244− h' <- handle h
245− execApp' env ctxt (ioWrap h') rest
243+ execApp' env ctxt (ioWrap (EHandle h)) rest
246244
247−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:fh:rest)
248− | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do h <- unHandle fh
249− eofp <- execIO $ hIsEOF h
245+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
246+ | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h
250247 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
251248 execApp' env ctxt res rest
252249
253−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:fh:rest)
254− | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do h <- unHandle fh
255− execIO $ hClose h
250+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
251+ | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h
256252 execApp' env ctxt ioUnit rest
257253
258254
@@ -293,9 +289,8 @@ execApp' env ctxt f@(EP _ n _) args =
293289 getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
294290 Just $ do line <- execIO getLine
295291 return (EConstant (Str line))
296− getOp (UN "prim__readString") [ptr] =
297− Just $ do h <- unHandle ptr
298− contents <- execIO $ hGetLine h
292+ getOp (UN "prim__readString") [EHandle h] =
293+ Just $ do contents <- execIO $ hGetLine h
299294 return (EConstant (Str contents))
300295 getOp _ _ = Nothing
301296execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
@@ -355,40 +350,6 @@ idrisType ft = EConstant (idr ft)
355350
356351data Foreign = FFun String [FTy] FTy deriving Show
357352
358−-- | A representation of Ptr values, which otherwise don't work in TT
359−ptrCon :: Name
360−ptrCon = MN 0 "__Ptr"
361−
362−-- | Convert a Haskell pointer to a Ptr term in TT
363−ptr :: Ptr a -> ExecVal
364−ptr p = EApp (EP (DCon 0 1) ptrCon EErased) (EConstant (I (addr p)))
365− where addr p = p `minusPtr` nullPtr
366−
367−-- | Convert a Ptr term in TT to a Haskell pointer
368−unPtr :: ExecVal -> Maybe (Ptr a)
369−unPtr (EApp (EP _ con _) (EConstant (I addr))) | con == ptrCon = Just (unAddr addr)
370− where unAddr a = nullPtr `plusPtr` a
371−unPtr _ = Nothing
372−
373−handleCon :: Name
374−handleCon = MN 0 "__Handle"
375−
376−-- | Convert a Haskell file handle to a handle term in TT (an int)
377−handle :: Handle -> Exec ExecVal
378−handle h = do est <- getExecState
379− let i = exec_next_handle est
380− putExecState $ est { exec_next_handle = exec_next_handle est + 1
381− , exec_handles = M.insert i h (exec_handles est)
382− }
383− return $ EHandle i
384−
385−unHandle :: ExecVal -> Exec Handle
386−unHandle (EHandle i) =
387− do est <- getExecState
388− case M.lookup i (exec_handles est) of
389− Just h -> return h
390− Nothing -> execFail "Bad handle ID"
391−unHandle _ = execFail "Not a handle"
392353
393354call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
394355call (FFun name argTypes retType) args =
@@ -410,7 +371,7 @@ call (FFun name argTypes retType) args =
410371 return (EConstant (Str hStr))
411372
412373 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
413− return (ptr res)
374+ return (EPtr res)
414375 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
415376 return (EP Ref unitCon EErased)
416377-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
@@ -421,7 +382,7 @@ call (FFun name argTypes retType) args =
421382 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
422383 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
423384 prepArg (EConstant (Str s)) = argString s
424− prepArg ptr | Just p <- unPtr ptr = argPtr p
385+ prepArg (EPtr p) = argPtr p
425386 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
426387
427388