f387ef0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Code cleanups

f387ef0David Christiansen14 years ago

src/Core/Execute.hs+22−61

compare with master

unifiedsplit

@@ -1,4 +1,4 @@

1−{-# LANGUAGE PatternGuards #-}

1+{-# LANGUAGE PatternGuards, ExistentialQuantification #-}

2module Core.Execute (execute) where

4import Idris.AbsSyntax

@@ -35,8 +35,6 @@ data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the res

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− , exec_handles :: M.Map Int Handle -- ^ Opened files

39− , exec_next_handle :: Int -- ^ Ensure opened file key uniqueness

40 }

38 }

42data ExecVal = EP NameType Name ExecVal

40data ExecVal = EP NameType Name ExecVal

@@ -46,20 +44,21 @@ data ExecVal = EP NameType Name ExecVal

46 | EType UExp

44 | EType UExp

47 | EErased

45 | EErased

48 | EConstant Const

46 | EConstant Const

49−-- | ETmp Int

47+ | forall a. EPtr (Ptr a)

50 | EThunk Int

48 | EThunk Int

51− | EHandle Int

49+ | EHandle Handle

53instance Show ExecVal where

51instance Show ExecVal where

54− show (EP _ n _) = show n

52+ show (EP _ n _) = show n

55− show (EV i) = "!!V" ++ show i ++ "!!"

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

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

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

57− show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"

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

58− show (EType _) = "Type"

56+ show (EType _) = "Type"

59− show EErased = "[__]"

57+ show EErased = "[__]"

60− show (EConstant c) = show c

58+ show (EConstant c) = show c

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

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

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

62− show (EHandle i) = "<<handle " ++ show i ++ ">>"

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

64toTT :: ExecVal -> Exec Term

63toTT :: ExecVal -> Exec Term

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

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

@@ -96,7 +95,7 @@ mkEApp f (a:args) = mkEApp (EApp f a) args

97initState :: Idris ExecState

96initState :: Idris ExecState

98initState = do ist <- getIState

97initState = 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)

100

101type Exec = ErrorT String (StateT ExecState IO)

100type Exec = ErrorT String (StateT ExecState IO)

102

101

@@ -241,18 +240,15 @@ execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (S

241 "r+" -> return ReadWriteMode

240 "r+" -> return ReadWriteMode

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

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

243 h <- execIO $ openFile f m

242 h <- execIO $ openFile f m

244− h' <- handle h

245− execApp' env ctxt (ioWrap h') rest

243+ execApp' env ctxt (ioWrap (EHandle h)) rest

246

244

247−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:fh:rest)

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

248− | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do h <- unHandle fh

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

249− eofp <- execIO $ hIsEOF h

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

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

251 execApp' env ctxt res rest

248 execApp' env ctxt res rest

252

249

253−execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:fh:rest)

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

254− | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do h <- unHandle fh

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

255− execIO $ hClose h

256 execApp' env ctxt ioUnit rest

252 execApp' env ctxt ioUnit rest

257

253

258

254

@@ -293,9 +289,8 @@ execApp' env ctxt f@(EP _ n _) args =

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

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

294 Just $ do line <- execIO getLine

290 Just $ do line <- execIO getLine

295 return (EConstant (Str line))

291 return (EConstant (Str line))

296− getOp (UN "prim__readString") [ptr] =

292+ getOp (UN "prim__readString") [EHandle h] =

297− Just $ do h <- unHandle ptr

298− contents <- execIO $ hGetLine h

293+ Just $ do contents <- execIO $ hGetLine h

299 return (EConstant (Str contents))

294 return (EConstant (Str contents))

300 getOp _ _ = Nothing

295 getOp _ _ = Nothing

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

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

@@ -355,40 +350,6 @@ idrisType ft = EConstant (idr ft)

355

350

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

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

357

352

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"

392

353

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

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

394call (FFun name argTypes retType) args =

355call (FFun name argTypes retType) args =

@@ -410,7 +371,7 @@ call (FFun name argTypes retType) args =

410 return (EConstant (Str hStr))

371 return (EConstant (Str hStr))

411

372

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

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

413− return (ptr res)

374+ return (EPtr res)

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

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

415 return (EP Ref unitCon EErased)

376 return (EP Ref unitCon EErased)

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

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

@@ -421,7 +382,7 @@ call (FFun name argTypes retType) args =

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

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

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

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

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

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

424− prepArg ptr | Just p <- unPtr ptr = argPtr p

385+ prepArg (EPtr p) = argPtr p

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

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

426

387

427

388