3262127 · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

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

85 Idris.DataOpts, Idris.Transforms, Idris.DSL,

86 Idris.UnusedArgs, Idris.Docs, Idris.Completion,

87

88− Util.Pretty, Util.System,

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

89 Pkg.Package, Pkg.PParser,

90

91 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

src/Core/Execute.hs+4−3

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

8

9import Debug.Trace

10

11−import Foreign.LibFFI

12−import Foreign.Ptr (nullPtr)

13−import System.Posix.DynamicLinker

11+import Util.DynamicLinker

12+

14

13

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

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

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

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

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

30 Nothing -> return tm

29 Nothing -> return tm

31 Just tm' -> execute tm'

30 Just tm' -> execute tm'

32

31

32+

33+

34

35

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

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

src/Idris/AbsSyntaxTree.hs+8−4

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

10import IRTS.Lang

11import IRTS.CodegenCommon

12import Util.Pretty

13+import Util.DynamicLinker

13

14

14import Paths_idris

15import Paths_idris

15

16

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

78 idris_hdrs :: [String],

79 idris_hdrs :: [String],

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

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

80 errLine :: Maybe Int,

81 errLine :: Maybe Int,

81− lastParse :: Maybe Name,

82+ lastParse :: Maybe Name,

82 indent_stack :: [Int],

83 indent_stack :: [Int],

83 brace_stack :: [Maybe Int],

84 brace_stack :: [Maybe Int],

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

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

85 default_access :: Accessibility,

86 default_access :: Accessibility,

86 default_total :: Bool,

87 default_total :: Bool,

87 ibc_write :: [IBCWrite],

88 ibc_write :: [IBCWrite],

88− compiled_so :: Maybe String

89+ compiled_so :: Maybe String,

90+ idris_dynamic_libs :: [DynamicLib]

89 }

91 }

90

92

91data SizeChange = Smaller | Same | Bigger | Unknown

93data SizeChange = Smaller | Same | Bigger | Unknown

92 deriving (Show, Eq)

94 deriving (Show, Eq)

93−{-!

95+{-!

94deriving instance Binary SizeChange

96deriving instance Binary SizeChange

95!-}

97!-}

96

98

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

136 emptyContext emptyContext emptyContext emptyContext

138 emptyContext emptyContext emptyContext emptyContext

137 emptyContext emptyContext emptyContext emptyContext

139 emptyContext emptyContext emptyContext emptyContext

138 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

140 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

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

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

140

142

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

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

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

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

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

180 | Defn Name

182 | Defn Name

181 | Info Name

183 | Info Name

182 | Missing Name

184 | Missing Name

185+ | DynamicLink FilePath

186+ | ListDynamic

183 | Pattelab PTerm

187 | Pattelab PTerm

184 | DebugInfo Name

188 | DebugInfo Name

185 | Search PTerm

189 | Search PTerm

src/Idris/REPL.hs+17−1

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

21

22import Paths_idris

23import Util.System

24+import Util.DynamicLinker

24

25

25import Core.Evaluate

26import Core.Evaluate

26import Core.Execute (execute)

27import Core.Execute (execute)

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

52import Data.Char

53import Data.Char

53import Data.Version

54import Data.Version

54

55

56+import Debug.Trace

57+

55-- | Run the REPL

58-- | Run the REPL

56repl :: IState -- ^ The initial state

59repl :: IState -- ^ The initial state

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

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

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

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

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

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

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

378 _ -> iputStrLn $ "Ambiguous name"

381 _ -> iputStrLn $ "Ambiguous name"

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

379−process fn Metavars

395+process fn Metavars

380 = do ist <- getIState

396 = do ist <- getIState

381 let mvs = idris_metavars ist \\ primDefs

397 let mvs = idris_metavars ist \\ primDefs

382 case mvs of

398 case mvs of

src/Idris/REPLParser.hs+3−1

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

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

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

50 <|> 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))

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

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

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

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

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

57 <|> 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))

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

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

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

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

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

62 <|> 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.

3+

4+module Util.DynamicLinker where

5+

6+import Foreign.LibFFI

7+import Foreign.Ptr (nullPtr)

8+import System.Posix.DynamicLinker

9+

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+