3262127 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Dynamically load C libraries in REPL

commit3262127f01274edf7ddcd9fecf43d8e5da1f7605 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 15 Mar 2013, 11:45 (14 years ago) parentf5e4128

6 files changed+52−10

compare with master

unifiedsplit

idris.cabal+1−1 src/Core/Execute.hs+4−3 src/Idris/AbsSyntaxTree.hs+8−4 src/Idris/REPL.hs+17−1 src/Idris/REPLParser.hs+3−1 src/Util/DynamicLinker.hs+19

idris.cabal+1−1

@@ -85,7 +85,7 @@ Executable idris

8585 Idris.DataOpts, Idris.Transforms, Idris.DSL,

8686 Idris.UnusedArgs, Idris.Docs, Idris.Completion,

8787

88− Util.Pretty, Util.System,

88+ Util.Pretty, Util.System, Util.DynamicLinker,

8989 Pkg.Package, Pkg.PParser,

9090

9191 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

src/Core/Execute.hs+4−3

@@ -8,9 +8,8 @@ import Core.Evaluate

99import Debug.Trace

1010

11−import Foreign.LibFFI

12−import Foreign.Ptr (nullPtr)

13−import System.Posix.DynamicLinker

11+import Util.DynamicLinker

12+

1413

1514-- | Attempt to perform a side effect. Return either Just the next step in

1615-- evaluation (after performing the side effect through IO), or Nothing if no

@@ -30,6 +29,8 @@ execute tm = do stepped <- step tm

3029 Nothing -> return tm

3130 Just tm' -> execute tm'

3231

32+

33+

3435

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

src/Idris/AbsSyntaxTree.hs+8−4

@@ -10,6 +10,7 @@ import Core.Typecheck

1010import IRTS.Lang

1111import IRTS.CodegenCommon

1212import Util.Pretty

13+import Util.DynamicLinker

1314

1415import Paths_idris

1516

@@ -78,19 +79,20 @@ data IState = IState {

7879 idris_hdrs :: [String],

7980 proof_list :: [(Name, [String])],

8081 errLine :: Maybe Int,

81− lastParse :: Maybe Name,

82+ lastParse :: Maybe Name,

8283 indent_stack :: [Int],

8384 brace_stack :: [Maybe Int],

8485 hide_list :: [(Name, Maybe Accessibility)],

8586 default_access :: Accessibility,

8687 default_total :: Bool,

8788 ibc_write :: [IBCWrite],

88− compiled_so :: Maybe String

89+ compiled_so :: Maybe String,

90+ idris_dynamic_libs :: [DynamicLib]

8991 }

9092

9193data SizeChange = Smaller | Same | Bigger | Unknown

9294 deriving (Show, Eq)

93−{-!

95+{-!

9496deriving instance Binary SizeChange

9597!-}

9698

@@ -136,7 +138,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

136138 emptyContext emptyContext emptyContext emptyContext

137139 emptyContext emptyContext emptyContext emptyContext

138140 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

139− [] Nothing Nothing [] [] [] Hidden False [] Nothing

141+ [] Nothing Nothing [] [] [] Hidden False [] Nothing []

140142

141143-- | The monad for the main REPL - reading and processing files and updating

142144-- global state (hence the IO inner monad).

@@ -180,6 +182,8 @@ data Command = Quit

180182 | Defn Name

181183 | Info Name

182184 | Missing Name

185+ | DynamicLink FilePath

186+ | ListDynamic

183187 | Pattelab PTerm

184188 | DebugInfo Name

185189 | Search PTerm

src/Idris/REPL.hs+17−1

@@ -21,6 +21,7 @@ import Idris.Completion

2121

2222import Paths_idris

2323import Util.System

24+import Util.DynamicLinker

2425

2526import Core.Evaluate

2627import Core.Execute (execute)

@@ -52,6 +53,8 @@ import Data.List

5253import Data.Char

5354import Data.Version

5455

56+import Debug.Trace

57+

5558-- | Run the REPL

5659repl :: IState -- ^ The initial state

5760 -> [FilePath] -- ^ The loaded modules

@@ -376,7 +379,20 @@ process fn (Missing n) = do i <- getIState

376379 iputStrLn (showSep "\n" (map (showImp True) tms))

377380 [] -> iputStrLn $ show n ++ " undefined"

378381 _ -> iputStrLn $ "Ambiguous name"

379−process fn Metavars

382+process fn (DynamicLink l) = do i <- getIState

383+ let lib = trim l

384+ handle <- lift $ tryLoadLib lib

385+ case handle of

386+ Nothing -> iputStrLn $ "Could not load dynamic lib \"" ++ l ++ "\""

387+ Just x -> do let libs = idris_dynamic_libs i

388+ putIState $ i { idris_dynamic_libs = x:libs }

389+ where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

390+process fn ListDynamic = do i <- getIState

391+ iputStrLn "Dynamic libraries:"

392+ showLibs $ idris_dynamic_libs i

393+ where showLibs [] = return ()

394+ showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls

395+process fn Metavars

380396 = do ist <- getIState

381397 let mvs = idris_metavars ist \\ primDefs

382398 case mvs of

src/Idris/REPLParser.hs+3−1

@@ -48,13 +48,15 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

4848 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

4949 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

5050 <|> try (do cmd ["doc"]; n <- pfName; eof; return (DocStr n))

51− <|> try (do cmd ["d", "def"]; n <- pfName; eof; return (Defn n))

51+ <|> try (do cmd ["d", "def"]; many1 (char ' ') ; n <- pfName; eof; return (Defn n))

5252 <|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))

5353 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

5454 <|> try (do cmd ["u", "universes"]; eof; return Universes)

5555 <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))

5656 <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))

5757 <|> try (do cmd ["miss", "missing"]; n <- pfName; eof; return (Missing n))

58+ <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

59+ <|> try (do cmd ["dynamic"]; l <- getInput; return (DynamicLink l))

5860 <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))

5961 <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

6062 <|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t))

src/Util/DynamicLinker.hsnew file+19

@@ -0,0 +1,19 @@

1+-- | Platform-specific dynamic linking support. Add new platforms to this file

2+-- through conditional compilation.

4+module Util.DynamicLinker where

6+import Foreign.LibFFI

7+import Foreign.Ptr (nullPtr)

8+import System.Posix.DynamicLinker

10+data DynamicLib = Lib { lib_name :: String

11+ , lib_handle :: DL

12+ }

13+

14+tryLoadLib :: String -> IO (Maybe DynamicLib)

15+tryLoadLib lib = do handle <- dlopen lib [RTLD_NOW]

16+ if undl handle == nullPtr

17+ then return Nothing

18+ else return . Just $ Lib lib handle

19+