7e3df2f · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -7,6 +7,8 @@ User visible changes:

7* Renamed EFF to EFFECT in Effect package

8* Experimental Java backend

9* Tab completion in REPL

10+* Dynamic loading of C libraries in the interpreter

11+* Testing IO actions at the REPL with :x command

10

12

11Internal changes:

13Internal changes:

12

14

idris.cabal+3−3

@@ -79,7 +79,7 @@ Flag Java

79Executable idris

80 Main-is: Main.hs

81 hs-source-dirs: src

82− Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,

82+ Other-modules: Core.TT, Core.Evaluate, Core.Execute, Core.Typecheck,

83 Core.ProofShell, Core.ProofState, Core.CoreParser,

84 Core.ShellParser, Core.Unify, Core.Elaborate,

85 Core.CaseTree, Core.Constraints,

@@ -93,7 +93,7 @@ Executable idris

93 Idris.DataOpts, Idris.Transforms, Idris.DSL,

94 Idris.UnusedArgs, Idris.Docs, Idris.Completion,

95

96− Util.Pretty, Util.System,

96+ Util.Pretty, Util.System, Util.DynamicLinker,

97 Pkg.Package, Pkg.PParser,

98

99 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

@@ -108,7 +108,7 @@ Executable idris

108 haskeline>=0.7, split, directory,

109 containers, process, transformers, filepath,

110 directory, binary, bytestring, text, pretty,

111− language-java>=0.2.2

111+ language-java>=0.2.2, libffi, unix

112

113 Extensions: MultiParamTypeClasses, FunctionalDependencies,

114 FlexibleInstances, TemplateHaskell

lib/Providers.idrnew file+8

@@ -0,0 +1,8 @@

1+module Providers

2+

3+public

4+data Provider a = Provide (IO a) | Error (IO String)

5+

6+partial public

7+unProv : Provider a -> a

8+unProv (Provide x) = unsafePerformIO x

lib/base.ipkg+2

@@ -17,6 +17,8 @@ modules = Builtins, Prelude, IO, System,

17

18 Uninhabited,

19

20+ Providers,

21+

20 Language.Reflection,

22 Language.Reflection,

21

23

22 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,

24 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,

src/Core/Execute.hsnew file+144

@@ -0,0 +1,144 @@

1+module Core.Execute (execute) where

2+

3+import Idris.AbsSyntax

4+import Idris.AbsSyntaxTree

5+

6+import Core.TT

7+import Core.Evaluate

8+

9+import Debug.Trace

10+

11+import Util.DynamicLinker

12+

13+import Control.Applicative hiding (Const)

14+import Control.Monad.Trans

15+import Control.Monad

16+import Data.Maybe

17+

18+import Foreign.LibFFI

19+import Foreign.C.String

20+import Foreign.Marshal.Alloc (free)

21+

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

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

24+-- IO was performed.

25+--

26+-- This function is exceedingly generous about what it will accept in order to

27+-- enable convenient testing at the REPL.

28+step :: TT Name -> Idris (Maybe (TT Name))

29+step tm = step' (unApply tm)

30+ where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped

31+ step' (P _ (UN "mkForeign") _, args) = stepForeign args

32+ step' (P _ (UN "prim__IO") _, [_, arg]) = step arg

33+ step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =

34+ do line <- lift $ getLine

35+ return . Just . Constant . Str $ line

36+ step' _ = return Nothing

37+

38+-- | Perform side effects until no more can be performed, then return the

39+-- resulting term (possibly the argument).

40+execute :: TT Name -> Idris (TT Name)

41+execute tm = case unApply tm of

42+ (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg

43+ _ -> return tm

44+ where execute' tm = do stepped <- step tm

45+ case stepped of

46+ Nothing -> return tm

47+ Just tm' -> execute' tm'

48+

49+

50+

52+

53+data Foreign = FFun String [FTy] FTy deriving Show

54+

55+call :: Foreign -> [TT Name] -> Idris (Maybe (TT Name))

56+call (FFun name argTypes retType) args = do fn <- findForeign name

57+ case fn of

58+ Nothing -> return Nothing

59+ Just f -> return . Just =<< call' f args retType

60+ where call' :: ForeignFun -> [TT Name] -> FTy -> Idris (TT Name)

61+ call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)

62+ return (Constant (I (fromIntegral res)))

63+ call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)

64+ return (Constant (Fl (realToFrac res)))

65+ call' (Fun _ h) args FChar = do res <- lift $ callFFI h retCChar (prepArgs args)

66+ return (Constant (Ch (castCCharToChar res)))

67+ call' (Fun _ h) args FString = do res <- lift $ callFFI h retCString (prepArgs args)

68+ hStr <- lift $ peekCString res

69+-- lift $ free res

70+ return (Constant (Str hStr))

71+-- awaiting Const constructor for pointers

72+-- call' (Fun _ h) args FPtr = do res <- lift $ callFFI h retPtr (prepArgs args)

73+-- return (Constant (Ch (castCCharToChar res)))

74+ call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)

75+ return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level

76+

77+ prepArgs = map prepArg

78+ prepArg (Constant (I i)) = argCInt (fromIntegral i)

79+ prepArg (Constant (Fl f)) = argCDouble (realToFrac f)

80+ prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

81+ prepArg (Constant (Str s)) = argString s

82+

83+

84+

85+foreignFromTT :: TT Name -> Maybe Foreign

86+foreignFromTT t = case (unApply t) of

87+ (_, [(Constant (Str name)), args, ret]) ->

88+ do argTy <- unList args

89+ argFTy <- sequence $ map getFTy argTy

90+ retFTy <- getFTy ret

91+ return $ FFun name argFTy retFTy

92+ _ -> Nothing

93+

94+getFTy :: TT Name -> Maybe FTy

95+getFTy (P _ (UN t) _) = case t of

96+ "FInt" -> Just FInt

97+ "FFloat" -> Just FFloat

98+ "FChar" -> Just FChar

99+ "FString" -> Just FString

100+ "FPtr" -> Just FPtr

101+ "FUnit" -> Just FUnit

102+ _ -> Nothing

103+getFTy _ = Nothing

104+

105+unList :: TT Name -> Maybe [TT Name]

106+unList tm = case unApply tm of

107+ (nil, [_]) -> Just []

108+ (cons, ([_, x, xs])) ->

109+ do rest <- unList xs

110+ return $ x:rest

111+ (f, args) -> Nothing

112+

113+toConst :: TT Name -> Maybe Const

114+toConst (Constant c) = Just c

115+toConst _ = Nothing

116+

117+stepForeign :: [TT Name] -> Idris (Maybe (TT Name))

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

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

120+ Just f -> f args

121+ Nothing -> return Nothing

122+ return f'

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

124+

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

126+mapMaybeM f [] = return []

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

128+ x' <- f x

129+ case x' of

130+ Just x'' -> return (x'':rest)

131+ Nothing -> return rest

132+

133+findForeign :: String -> Idris (Maybe ForeignFun)

134+findForeign fn = do i <- getIState

135+ let libs = idris_dynamic_libs i

136+ fns <- mapMaybeM (lift . tryLoadFn fn) libs

137+ case fns of

138+ [f] -> return (Just f)

139+ [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"

140+ return Nothing

141+ fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++

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

143+ return Nothing

144+

src/Idris/AbsSyntax.hs+12

@@ -9,6 +9,7 @@ import Core.Elaborate hiding (Tactic(..))

9import Core.Typecheck

10import Idris.AbsSyntaxTree

11import IRTS.CodegenCommon

12+import Util.DynamicLinker

12

13

13import Paths_idris

14import Paths_idris

14

15

@@ -40,9 +41,20 @@ getLibs = do i <- getIState; return (idris_libs i)

40addLib :: String -> Idris ()

41addLib :: String -> Idris ()

41addLib f = do i <- getIState; putIState $ i { idris_libs = f : idris_libs i }

42addLib f = do i <- getIState; putIState $ i { idris_libs = f : idris_libs i }

42

43

44+addDyLib :: String -> Idris ()

45+addDyLib lib = do i <- getIState

46+ handle <- lift $ tryLoadLib lib

47+ case handle of

48+ Nothing -> fail $ "Could not load dynamic lib \"" ++ lib ++ "\""

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

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

51+

43addHdr :: String -> Idris ()

52addHdr :: String -> Idris ()

44addHdr f = do i <- getIState; putIState $ i { idris_hdrs = f : idris_hdrs i }

53addHdr f = do i <- getIState; putIState $ i { idris_hdrs = f : idris_hdrs i }

45

54

55+addLangExt :: LanguageExt -> Idris ()

56+addLangExt TypeProviders = do i <- getIState ; putIState $ i { idris_language_extensions = [TypeProviders] }

57+

46totcheck :: (FC, Name) -> Idris ()

58totcheck :: (FC, Name) -> Idris ()

47totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

59totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

48

60

src/Idris/AbsSyntaxTree.hs+24−5

@@ -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

@@ -42,6 +43,8 @@ data IOption = IOption { opt_logLevel :: Int,

42

43

43defaultOpts = IOption 0 False False True False False True True False ViaC Executable "" [] []

44defaultOpts = IOption 0 False False True False False True True False ViaC Executable "" [] []

44

45

46+data LanguageExt = TypeProviders deriving (Show, Eq, Read, Ord)

47+

45-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

48-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

46-- without typechecking).

49-- without typechecking).

47-- This will include all the functions and data declarations, plus fixity declarations

50-- This will include all the functions and data declarations, plus fixity declarations

@@ -79,19 +82,21 @@ data IState = IState {

79 idris_hdrs :: [String],

82 idris_hdrs :: [String],

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

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

81 errLine :: Maybe Int,

84 errLine :: Maybe Int,

82− lastParse :: Maybe Name,

85+ lastParse :: Maybe Name,

83 indent_stack :: [Int],

86 indent_stack :: [Int],

84 brace_stack :: [Maybe Int],

87 brace_stack :: [Maybe Int],

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

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

86 default_access :: Accessibility,

89 default_access :: Accessibility,

87 default_total :: Bool,

90 default_total :: Bool,

88 ibc_write :: [IBCWrite],

91 ibc_write :: [IBCWrite],

89− compiled_so :: Maybe String

92+ compiled_so :: Maybe String,

93+ idris_dynamic_libs :: [DynamicLib],

94+ idris_language_extensions :: [LanguageExt]

90 }

95 }

91

96

92data SizeChange = Smaller | Same | Bigger | Unknown

97data SizeChange = Smaller | Same | Bigger | Unknown

93 deriving (Show, Eq)

98 deriving (Show, Eq)

94−{-!

99+{-!

95deriving instance Binary SizeChange

100deriving instance Binary SizeChange

96!-}

101!-}

97

102

@@ -123,6 +128,7 @@ data IBCWrite = IBCFix FixDecl

123 | IBCImport FilePath

128 | IBCImport FilePath

124 | IBCObj FilePath

129 | IBCObj FilePath

125 | IBCLib String

130 | IBCLib String

131+ | IBCDyLib String

126 | IBCHeader String

132 | IBCHeader String

127 | IBCAccess Name Accessibility

133 | IBCAccess Name Accessibility

128 | IBCTotal Name Totality

134 | IBCTotal Name Totality

@@ -137,7 +143,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

137 emptyContext emptyContext emptyContext emptyContext

143 emptyContext emptyContext emptyContext emptyContext

138 emptyContext emptyContext emptyContext emptyContext

144 emptyContext emptyContext emptyContext emptyContext

139 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

145 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

140− [] Nothing Nothing [] [] [] Hidden False [] Nothing

146+ [] Nothing Nothing [] [] [] Hidden False [] Nothing [] []

141

147

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

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

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

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

@@ -181,6 +187,8 @@ data Command = Quit

181 | Defn Name

187 | Defn Name

182 | Info Name

188 | Info Name

183 | Missing Name

189 | Missing Name

190+ | DynamicLink FilePath

191+ | ListDynamic

184 | Pattelab PTerm

192 | Pattelab PTerm

185 | DebugInfo Name

193 | DebugInfo Name

186 | Search PTerm

194 | Search PTerm

@@ -222,6 +230,7 @@ data Opt = Filename String

222 | FOVM String

230 | FOVM String

223 | UseTarget Target

231 | UseTarget Target

224 | OutputTy OutputType

232 | OutputTy OutputType

233+ | Extension LanguageExt

225 deriving (Show, Eq)

234 deriving (Show, Eq)

226

235

227-- Parsed declarations

236-- Parsed declarations

@@ -332,12 +341,22 @@ data PDecl' t

332 | PSyntax FC Syntax -- ^ Syntax definition

341 | PSyntax FC Syntax -- ^ Syntax definition

333 | PMutual FC [PDecl' t] -- ^ Mutual block

342 | PMutual FC [PDecl' t] -- ^ Mutual block

334 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

343 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

344+ | PProvider SyntaxInfo FC Name t t -- ^ Type provider. The first t is the type, the second is the term

335 deriving Functor

345 deriving Functor

336{-!

346{-!

337deriving instance Binary PDecl'

347deriving instance Binary PDecl'

338!-}

348!-}

339

349

350+-- | One clause of a top-level definition. Term arguments to constructors are:

351+--

352+-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)

353+--

354+-- 2. The list of patterns

355+--

356+-- 3. The right-hand side

357+--

358+-- 4. The where block (PDecl' t)

340−data PClause' t = PClause FC Name t [t] t [PDecl' t]

359+data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.

341 | PWith FC Name t [t] t [PDecl' t]

360 | PWith FC Name t [t] t [PDecl' t]

342 | PClauseR FC [t] t [PDecl' t]

361 | PClauseR FC [t] t [PDecl' t]

343 | PWithR FC [t] t [PDecl' t]

362 | PWithR FC [t] t [PDecl' t]

src/Idris/ElabDecls.hs+32

@@ -11,11 +11,13 @@ import Idris.Imports

11import Idris.ElabTerm

12import Idris.Coverage

13import Idris.DataOpts

14+import Idris.Providers

14import Paths_idris

15import Paths_idris

15

16

16import Core.TT

17import Core.TT

17import Core.Elaborate hiding (Tactic(..))

18import Core.Elaborate hiding (Tactic(..))

18import Core.Evaluate

19import Core.Evaluate

20+import Core.Execute

19import Core.Typecheck

21import Core.Typecheck

20import Core.CaseTree

22import Core.CaseTree

21

23

@@ -38,6 +40,7 @@ checkDef fc ns = do ctxt <- getContext

38 mapM (\(n, t) -> do (t', _) <- recheckC fc [] t

40 mapM (\(n, t) -> do (t', _) <- recheckC fc [] t

39 return (n, t')) ns

41 return (n, t')) ns

40

42

43+-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

41elabType :: ElabInfo -> SyntaxInfo -> String ->

44elabType :: ElabInfo -> SyntaxInfo -> String ->

42 FC -> FnOpts -> Name -> PTerm -> Idris ()

45 FC -> FnOpts -> Name -> PTerm -> Idris ()

43elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

46elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

@@ -185,6 +188,29 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

185 = (mn, False) : updateParamsA ns args (p : all)

188 = (mn, False) : updateParamsA ns args (p : all)

186 updateParamsA ps args all = ps

189 updateParamsA ps args all = ps

187

190

191+-- | Elaborate a type provider

192+elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()

193+elabProvider info syn fc n ty tm

194+ = do i <- getIState

195+ if not (TypeProviders `elem` idris_language_extensions i)

196+ then fail $ "Failed to define type provider \"" ++ show n ++

197+ "\".\nYou must turn on TypeProviders extension."

198+ else do let expected = providerTy fc ty

199+ let using = unProv fc tm

200+ logLvl 1 $ "** Providing " ++

201+ show n ++ " : " ++ show expected ++

202+ " as " ++ show using

203+ (e', et) <- elabVal toplevel False using

204+ ctxt <- getContext

205+ let e'' = normaliseAll ctxt [] e'

206+ logLvl 1 $ "Term is " ++ show e''

207+ let et' = normaliseAll ctxt [] et

208+ elabType info syn "" fc [] n ty

209+ rhs <- execute e''

210+ elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i rhs) []]

211+ logLvl 1 $ "** Elaborated: " ++ show e' ++ " :as: " ++ show et

212+ logLvl 1 $ "** Evaluated: " ++ show rhs ++ " :as: " ++ show et'

213+

188elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

214elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

189 PTerm -> String -> Name -> PTerm -> Idris ()

215 PTerm -> String -> Name -> PTerm -> Idris ()

190elabRecord info syn doc fc tyn ty cdoc cn cty

216elabRecord info syn doc fc tyn ty cdoc cn cty

@@ -329,6 +355,8 @@ elabCon info syn tn codata (doc, n, t_in, fc)

329 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)

355 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)

330 mkLazy t = t

356 mkLazy t = t

331

357

358+-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

359+-- top-level definition.

332elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

360elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

333elabClauses info fc opts n_in cs = let n = liftname info n_in in

361elabClauses info fc opts n_in cs = let n = liftname info n_in in

334 do ctxt <- getContext

362 do ctxt <- getContext

@@ -1263,6 +1291,10 @@ elabDecl' _ info (PDSL n dsl)

1263 addIBC (IBCDSL n)

1291 addIBC (IBCDSL n)

1264elabDecl' what info (PDirective i)

1292elabDecl' what info (PDirective i)

1265 | what /= EDefns = i

1293 | what /= EDefns = i

1294+elabDecl' what info (PProvider syn fc n tp tm)

1295+ | what /= EDefns

1296+ = do iLOG $ "Elaborating type provider " ++ show n

1297+ elabProvider info syn fc n tp tm

1266elabDecl' _ _ _ = return () -- skipped this time

1298elabDecl' _ _ _ = return () -- skipped this time

1267

1299

1268elabCaseBlock info d@(PClauses f o n ps)

1300elabCaseBlock info d@(PClauses f o n ps)

src/Idris/Help.hs+4−1

@@ -8,7 +8,7 @@ data CmdArg = ExprArg -- ^ The command takes an expression

8 | MetaVarArg -- ^ The command takes a metavariable

9 | NoArg -- ^ No completion yet

10

11−

11+-- TODO: Merge the second and fourth elements of the following tuples

12help :: [([String], String, String, CmdArg)]

13help =

14 [ (["<expr>"], "", "Evaluate an expression", NoArg),

@@ -26,9 +26,12 @@ help =

26 ([":rmproof"], "<name>", "Remove proof from proof stack", NameArg),

27 ([":showproof"], "<name>", "Show proof", NameArg),

28 ([":proofs"], "", "Show available proofs", NoArg),

29+ ([":x"], "<expr>", "Execute IO actions resulting from an expression using the interpreter", ExprArg),

29 ([":c",":compile"], "<filename>", "Compile to an executable <filename>", FileArg),

30 ([":c",":compile"], "<filename>", "Compile to an executable <filename>", FileArg),

30 ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>", FileArg),

31 ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>", FileArg),

31 ([":exec",":execute"], "", "Compile to an executable and run", NoArg),

32 ([":exec",":execute"], "", "Compile to an executable and run", NoArg),

33+ ([":dynamic"], "<filename>", "Dynamically load a C library (similar to %dynamic)", FileArg),

34+ ([":dynamic"], "", "List dynamically loaded C libraries", NoArg),

32 ([":?",":h",":help"], "", "Display this help text", NoArg),

35 ([":?",":h",":help"], "", "Display this help text", NoArg),

33 ([":set"], "<option>", "Set an option (errorcontext, showimplicits)", OptionArg),

36 ([":set"], "<option>", "Set an option (errorcontext, showimplicits)", OptionArg),

34 ([":unset"], "<option>", "Unset an option", OptionArg),

37 ([":unset"], "<option>", "Unset an option", OptionArg),

src/Idris/IBC.hs+12−4

@@ -21,7 +21,7 @@ import System.Directory

21import Paths_idris

22

23ibcVersion :: Word8

24−ibcVersion = 27

24+ibcVersion = 28

25

26data IBCFile = IBCFile { ver :: Word8,

27 sourcefile :: FilePath,

@@ -38,6 +38,7 @@ data IBCFile = IBCFile { ver :: Word8,

38 ibc_keywords :: [String],

39 ibc_objs :: [FilePath],

40 ibc_libs :: [String],

41+ ibc_dynamic_libs :: [String],

41 ibc_hdrs :: [String],

42 ibc_hdrs :: [String],

42 ibc_access :: [(Name, Accessibility)],

43 ibc_access :: [(Name, Accessibility)],

43 ibc_total :: [(Name, Totality)],

44 ibc_total :: [(Name, Totality)],

@@ -52,7 +53,7 @@ deriving instance Binary IBCFile

52!-}

53!-}

53

54

54initIBC :: IBCFile

55initIBC :: IBCFile

55−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

56+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

56

57

57loadIBC :: FilePath -> Idris ()

58loadIBC :: FilePath -> Idris ()

58loadIBC fp = do iLOG $ "Loading ibc " ++ fp

59loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -110,6 +111,7 @@ ibc i (IBCKeyword n) f = return f { ibc_keywords = n : ibc_keywords f }

110ibc i (IBCImport n) f = return f { ibc_imports = n : ibc_imports f }

111ibc i (IBCImport n) f = return f { ibc_imports = n : ibc_imports f }

111ibc i (IBCObj n) f = return f { ibc_objs = n : ibc_objs f }

112ibc i (IBCObj n) f = return f { ibc_objs = n : ibc_objs f }

112ibc i (IBCLib n) f = return f { ibc_libs = n : ibc_libs f }

113ibc i (IBCLib n) f = return f { ibc_libs = n : ibc_libs f }

114+ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

113ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }

115ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }

114ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

116ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

115 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

117 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

@@ -147,6 +149,7 @@ process i fn

147 pKeywords (ibc_keywords i)

149 pKeywords (ibc_keywords i)

148 pObjs (ibc_objs i)

150 pObjs (ibc_objs i)

149 pLibs (ibc_libs i)

151 pLibs (ibc_libs i)

152+ pDyLibs (ibc_dynamic_libs i)

150 pHdrs (ibc_hdrs i)

153 pHdrs (ibc_hdrs i)

151 pDefs (ibc_defs i)

154 pDefs (ibc_defs i)

152 pAccess (ibc_access i)

155 pAccess (ibc_access i)

@@ -242,6 +245,9 @@ pObjs os = mapM_ addObjectFile os

242pLibs :: [String] -> Idris ()

245pLibs :: [String] -> Idris ()

243pLibs ls = mapM_ addLib ls

246pLibs ls = mapM_ addLib ls

244

247

248+pDyLibs :: [String] -> Idris ()

249+pDyLibs ls = mapM_ addDyLib ls

250+

245pHdrs :: [String] -> Idris ()

251pHdrs :: [String] -> Idris ()

246pHdrs hs = mapM_ addHdr hs

252pHdrs hs = mapM_ addHdr hs

247

253

@@ -744,7 +750,7 @@ instance Binary Totality where

744 _ -> error "Corrupted binary data for Totality"

750 _ -> error "Corrupted binary data for Totality"

745

751

746instance Binary IBCFile where

752instance Binary IBCFile where

747− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23)

753+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24)

748 = do put x1

754 = do put x1

749 put x2

755 put x2

750 put x3

756 put x3

@@ -768,6 +774,7 @@ instance Binary IBCFile where

768 put x21

774 put x21

769 put x22

775 put x22

770 put x23

776 put x23

777+ put x24

771 get

778 get

772 = do x1 <- get

779 = do x1 <- get

773 if x1 == ibcVersion then

780 if x1 == ibcVersion then

@@ -793,7 +800,8 @@ instance Binary IBCFile where

793 x21 <- get

800 x21 <- get

794 x22 <- get

801 x22 <- get

795 x23 <- get

802 x23 <- get

803+ x24 <- get

796− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23)

804+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24)

797 else return (initIBC { ver = x1 })

805 else return (initIBC { ver = x1 })

798

806

799instance Binary FnOpt where

807instance Binary FnOpt where

src/Idris/Parser.hs+46−29

@@ -11,8 +11,11 @@ import Idris.ElabTerm

11import Idris.Coverage

12import Idris.IBC

13import Idris.Unlit

14+import Idris.Providers

14import Paths_idris

15import Paths_idris

15

16

17+import Util.DynamicLinker

18+

16import Core.CoreParser

19import Core.CoreParser

17import Core.TT

20import Core.TT

18import Core.Evaluate

21import Core.Evaluate

@@ -339,7 +342,8 @@ pDecl syn = do notEndBlock

339 <|> pClass syn

342 <|> pClass syn

340 <|> pInstance syn

343 <|> pInstance syn

341 <|> do d <- pDSL syn; return [d]

344 <|> do d <- pDSL syn; return [d]

342− <|> pDirective

345+ <|> pDirective syn

346+ <|> pProvider syn

343 <|> try (do reserved "import"; fp <- identifier

347 <|> try (do reserved "import"; fp <- identifier

344 fail "imports must be at the top of file")

348 fail "imports must be at the top of file")

345

349

@@ -1465,34 +1469,47 @@ pWhereblock n syn

1465 closeBlock

1469 closeBlock

1466 return (concat ds, map (\x -> (x, decoration syn x)) dns)

1470 return (concat ds, map (\x -> (x, decoration syn x)) dns)

1467

1471

1468−pDirective :: IParser [PDecl]

1472+pDirective :: SyntaxInfo -> IParser [PDecl]

1469−pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

1473+pDirective syn = try (do lchar '%'; reserved "lib"; lib <- strlit;

1470− return [PDirective (do addLib lib

1474+ return [PDirective (do addLib lib

1471− addIBC (IBCLib lib))])

1475+ addIBC (IBCLib lib))])

1472− <|> try (do lchar '%'; reserved "link"; obj <- strlit;

1476+ <|> try (do lchar '%'; reserved "link"; obj <- strlit;

1473− return [PDirective (do datadir <- liftIO getDataDir

1477+ return [PDirective (do datadir <- liftIO getDataDir

1474− o <- liftIO $ findInPath [".", datadir] obj

1478+ o <- liftIO $ findInPath [".", datadir] obj

1475− addIBC (IBCObj o)

1479+ addIBC (IBCObj o)

1476− addObjectFile o)])

1480+ addObjectFile o)])

1477− <|> try (do lchar '%'; reserved "include"; hdr <- strlit;

1481+ <|> try (do lchar '%'; reserved "include"; hdr <- strlit;

1478− return [PDirective (do addHdr hdr

1482+ return [PDirective (do addHdr hdr

1479− addIBC (IBCHeader hdr))])

1483+ addIBC (IBCHeader hdr))])

1480− <|> try (do lchar '%'; reserved "hide"; n <- iName []

1484+ <|> try (do lchar '%'; reserved "hide"; n <- iName []

1481− return [PDirective (do setAccessibility n Hidden

1485+ return [PDirective (do setAccessibility n Hidden

1482− addIBC (IBCAccess n Hidden))])

1486+ addIBC (IBCAccess n Hidden))])

1483− <|> try (do lchar '%'; reserved "freeze"; n <- iName []

1487+ <|> try (do lchar '%'; reserved "freeze"; n <- iName []

1484− return [PDirective (do setAccessibility n Frozen

1488+ return [PDirective (do setAccessibility n Frozen

1485− addIBC (IBCAccess n Frozen))])

1489+ addIBC (IBCAccess n Frozen))])

1486− <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'

1490+ <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'

1487− return [PDirective (do i <- getIState

1491+ return [PDirective (do i <- getIState

1488− putIState (i { default_access = acc }))])

1492+ putIState (i { default_access = acc }))])

1489− <|> try (do lchar '%'; reserved "default"; tot <- pTotality

1493+ <|> try (do lchar '%'; reserved "default"; tot <- pTotality

1490− i <- getState

1494+ i <- getState

1491− setState (i { default_total = tot } )

1495+ setState (i { default_total = tot } )

1492− return [PDirective (do i <- getIState

1496+ return [PDirective (do i <- getIState

1493− putIState (i { default_total = tot }))])

1497+ putIState (i { default_total = tot }))])

1494− <|> try (do lchar '%'; reserved "logging"; i <- natural;

1498+ <|> try (do lchar '%'; reserved "logging"; i <- natural;

1495− return [PDirective (setLogLevel (fromInteger i))])

1499+ return [PDirective (setLogLevel (fromInteger i))])

1500+ <|> try (do lchar '%'; reserved "dynamic"; lib <- strlit;

1501+ return [PDirective (do addIBC (IBCDyLib lib)

1502+ addDyLib lib)])

1503+ <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";

1504+ return [PDirective (addLangExt TypeProviders)])

1505+

1506+pProvider :: SyntaxInfo -> IParser [PDecl]

1507+pProvider syn = do lchar '%'; reserved "provide";

1508+ lchar '('; n <- pfName; t <- pTSig syn; lchar ')'

1509+ fc <- pfc

1510+ reserved "with"

1511+ e <- pExpr syn

1512+ return [PProvider syn fc n t e]

1496

1513

1497pTactic :: SyntaxInfo -> IParser PTactic

1514pTactic :: SyntaxInfo -> IParser PTactic

1498pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

1515pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

src/Idris/Providers.hsnew file+14

@@ -0,0 +1,14 @@

1+module Idris.Providers where

2+

3+import Core.TT

4+import Core.Evaluate

5+import Idris.AbsSyntax

6+import Idris.AbsSyntaxTree

7+

8+-- | Wrap a type provider in the type of type providers

9+providerTy :: FC -> PTerm -> PTerm

10+providerTy fc tm = PApp fc (PRef fc $ UN "Provider") [PExp 0 False tm ""]

11+

12+-- | Wrap the RHS of a type provider definition

13+unProv :: FC -> PTerm -> PTerm

14+unProv fc tm = PApp fc (PRef fc $ NS (UN "unProv") ["Providers"]) [PExp 0 False tm ""]

src/Idris/REPL.hs+70−47

@@ -21,8 +21,10 @@ import Idris.Completion

21

22import Paths_idris

23import Util.System

24+import Util.DynamicLinker

24

25

25import Core.Evaluate

26import Core.Evaluate

27+import Core.Execute (execute)

26import Core.ProofShell

28import Core.ProofShell

27import Core.TT

29import Core.TT

28import Core.Constraints

30import Core.Constraints

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

51import Data.Char

53import Data.Char

52import Data.Version

54import Data.Version

53

55

56+import Debug.Trace

57+

54-- | Run the REPL

58-- | Run the REPL

55repl :: IState -- ^ The initial state

59repl :: IState -- ^ The initial state

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

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

@@ -185,17 +189,17 @@ process fn (Eval t)

185 imp <- impShow

189 imp <- impShow

186 iputStrLn (showImp imp (delab ist tm') ++ " : " ++

190 iputStrLn (showImp imp (delab ist tm') ++ " : " ++

187 showImp imp (delab ist ty'))

191 showImp imp (delab ist ty'))

188−process fn (ExecVal t)

192+process fn (ExecVal t)

193+ = do ctxt <- getContext

194+ ist <- getIState

189− = do (tm, ty) <- elabVal toplevel False t

195+ (tm, ty) <- elabVal toplevel False t

190−-- (PApp fc (PRef fc (NS (UN "print") ["Prelude"]))

196+ let tm' = normaliseAll ctxt [] tm

191−-- [pexp t])

197+ let ty' = normaliseAll ctxt [] ty

192− (tmpn, tmph) <- liftIO tempfile

198+ res <- execute tm'

193− liftIO $ hClose tmph

199+ imp <- impShow

194− t <- target

200+ iputStrLn (showImp imp (delab ist res) ++ " : " ++

195− compile t tmpn tm

201+ showImp imp (delab ist ty'))

196− liftIO $ system tmpn

197− return ()

202+ return ()

198− where fc = FC "(input)" 0

199process fn (Check (PRef _ n))

203process fn (Check (PRef _ n))

200 = do ctxt <- getContext

204 = do ctxt <- getContext

201 ist <- getIState

205 ist <- getIState

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

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

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

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

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

382 _ -> iputStrLn $ "Ambiguous name"

386 _ -> iputStrLn $ "Ambiguous name"

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

388+ let lib = trim l

389+ handle <- lift $ tryLoadLib lib

390+ case handle of

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

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

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

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

395+process fn ListDynamic = do i <- getIState

396+ iputStrLn "Dynamic libraries:"

397+ showLibs $ idris_dynamic_libs i

398+ where showLibs [] = return ()

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

383−process fn Metavars

400+process fn Metavars

384 = do ist <- getIState

401 = do ist <- getIState

385 let mvs = idris_metavars ist \\ primDefs

402 let mvs = idris_metavars ist \\ primDefs

386 case mvs of

403 case mvs of

@@ -441,41 +458,42 @@ parseTarget _ = error "unknown target" -- FIXME: partial function

441

458

442parseArgs :: [String] -> [Opt]

459parseArgs :: [String] -> [Opt]

443parseArgs [] = []

460parseArgs [] = []

444−parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)

461+parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)

445−parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

462+parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

446−parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

463+parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

447−parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

464+parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

448−parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)

465+parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)

449−parseArgs ("-no":n:ns) = NoREPL : NewOutput n : (parseArgs ns)

466+parseArgs ("-no":n:ns) = NoREPL : NewOutput n : (parseArgs ns)

450−parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)

467+parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)

451−parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)

468+parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)

452−parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)

469+parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)

453−parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)

470+parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)

454−parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)

471+parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)

455−parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)

472+parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)

456−parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)

473+parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)

457−parseArgs ("--help":ns) = Usage : (parseArgs ns)

474+parseArgs ("--help":ns) = Usage : (parseArgs ns)

458−parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)

475+parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)

459−parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)

476+parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)

460−parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)

477+parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)

461−parseArgs ("--version":ns) = Ver : (parseArgs ns)

478+parseArgs ("--version":ns) = Ver : (parseArgs ns)

462−parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)

479+parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)

463−parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)

480+parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)

464−parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)

481+parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)

465−parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)

482+parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)

466−parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)

483+parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)

467−parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)

484+parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)

468−parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)

485+parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)

469−parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

486+parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

470−parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

487+parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

471−parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

488+parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

472−parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)

489+parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)

473−parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

490+parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

474−parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

491+parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

475−parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

492+parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

476−parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

493+parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

477−parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

494+parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

495+parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)

478−parseArgs (n:ns) = Filename n : (parseArgs ns)

496+parseArgs (n:ns) = Filename n : (parseArgs ns)

479

497

480helphead =

498helphead =

481 [ (["Command"], "Arguments", "Purpose", ""),

499 [ (["Command"], "Arguments", "Purpose", ""),

@@ -510,6 +528,7 @@ idrisMain opts =

510 xs -> last xs

528 xs -> last xs

511 when (DefaultTotal `elem` opts) $ do i <- getIState

529 when (DefaultTotal `elem` opts) $ do i <- getIState

512 putIState (i { default_total = True })

530 putIState (i { default_total = True })

531+ mapM_ addLangExt (opt getLanguageExt opts)

513 setREPL runrepl

532 setREPL runrepl

514 setQuiet quiet

533 setQuiet quiet

515 setVerbose runrepl

534 setVerbose runrepl

@@ -609,6 +628,10 @@ getOutputTy :: Opt -> Maybe OutputType

609getOutputTy (OutputTy t) = Just t

628getOutputTy (OutputTy t) = Just t

610getOutputTy _ = Nothing

629getOutputTy _ = Nothing

611

630

631+getLanguageExt :: Opt -> Maybe LanguageExt

632+getLanguageExt (Extension e) = Just e

633+getLanguageExt _ = Nothing

634+

612opt :: (Opt -> Maybe a) -> [Opt] -> [a]

635opt :: (Opt -> Maybe a) -> [Opt] -> [a]

613opt = mapMaybe

636opt = mapMaybe

614

637

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+28

@@ -0,0 +1,28 @@

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

2+-- through conditional compilation.

3+{-# LANGUAGE ExistentialQuantification #-}

4+module Util.DynamicLinker where

5+

6+import Foreign.LibFFI

7+import Foreign.Ptr (nullPtr, FunPtr, nullFunPtr)

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+

20+data ForeignFun = forall a. Fun { fun_name :: String

21+ , fun_handle :: FunPtr a

22+ }

23+

24+tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)

25+tryLoadFn fn (Lib _ h) = do cFn <- dlsym h fn

26+ if cFn == nullFunPtr

27+ then return Nothing

28+ else return . Just $ Fun fn cFn

test/README+1

@@ -21,5 +21,6 @@ Tests:

21019: magic with

22020: implicit conversions

23021: effects

24+022: dynamic C library loading and interpreter IO

24

25

25regxxx: various regression tests

26regxxx: various regression tests

test/test022/expectednew file+2

@@ -0,0 +1,2 @@

1+Type checking ./test022.idr

2+0.9995736030415051 : Float

test/test022/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+echo ":x x" | idris --quiet test022.idr

3+rm -f test021 test021a *.ibc

test/test022/test022.idrnew file+6

@@ -0,0 +1,6 @@

1+module Main

2+

3+%dynamic "libm.so"

4+

5+x : Float

6+x = unsafePerformIO (mkForeign (FFun "sin" [FFloat] FFloat) 1.6)

tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/miscellany.tex+16

@@ -228,8 +228,24 @@ This is made possible through the following directives:

228\texttt{-lx} option to \texttt{gcc}.

229\item \texttt{\%include "x.h"} --- use the header file \texttt{x.h}.

230\item \texttt{\%link "x.o"} --- link with the object file \texttt{x.o}.

231+\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.

231\end{itemize}

232\end{itemize}

232

233

234+\subsubsection*{Testing foreign function calls}

235+Normally, the Idris interpreter (used for typechecking and at the REPL) will

236+not perform IO actions. Additionally, as it neither generates C code nor

237+compiles to machine code, the \texttt{\%lib}, \texttt{\%include} and

238+\texttt{\%link} directives have no effect. IO actions and FFI calls can be

239+tested using the special REPL command \texttt{:x EXPR}, and C libraries can be

240+dynamically loaded in the interpreter by using the \texttt{:dynamic} command

241+or the \texttt{\%dynamic} directive. For example:

242+

243+\begin{SaveVerbatim}{xdynamic}

244+Idris> :dynamic libm.so

245+Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)

246+0.9995736030415051 : Float

247+\end{SaveVerbatim}

248+\useverb{xdynamic}

233\subsection{Cumulativity}

249\subsection{Cumulativity}

234

250

235Since values can appear in types and \emph{vice versa}, it is natural that types themselves

251Since values can appear in types and \emph{vice versa}, it is natural that types themselves