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

CHANGELOG+2

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

77* Renamed EFF to EFFECT in Effect package

88* Experimental Java backend

99* Tab completion in REPL

10+* Dynamic loading of C libraries in the interpreter

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

1012

1113Internal changes:

1214

idris.cabal+3−3

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

7979Executable idris

8080 Main-is: Main.hs

8181 hs-source-dirs: src

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

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

8383 Core.ProofShell, Core.ProofState, Core.CoreParser,

8484 Core.ShellParser, Core.Unify, Core.Elaborate,

8585 Core.CaseTree, Core.Constraints,

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

9393 Idris.DataOpts, Idris.Transforms, Idris.DSL,

9494 Idris.UnusedArgs, Idris.Docs, Idris.Completion,

9595

96− Util.Pretty, Util.System,

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

9797 Pkg.Package, Pkg.PParser,

9898

9999 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

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

108108 haskeline>=0.7, split, directory,

109109 containers, process, transformers, filepath,

110110 directory, binary, bytestring, text, pretty,

111− language-java>=0.2.2

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

112112

113113 Extensions: MultiParamTypeClasses, FunctionalDependencies,

114114 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,

1717

1818 Uninhabited,

1919

20+ Providers,

21+

2022 Language.Reflection,

2123

2224 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(..))

99import Core.Typecheck

1010import Idris.AbsSyntaxTree

1111import IRTS.CodegenCommon

12+import Util.DynamicLinker

1213

1314import Paths_idris

1415

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

4041addLib :: String -> Idris ()

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

4243

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+

4352addHdr :: String -> Idris ()

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

4554

55+addLangExt :: LanguageExt -> Idris ()

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

57+

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

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

4860

src/Idris/AbsSyntaxTree.hs+24−5

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

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

4243

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

4445

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

47+

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

4649-- without typechecking).

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

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

7982 idris_hdrs :: [String],

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

8184 errLine :: Maybe Int,

82− lastParse :: Maybe Name,

85+ lastParse :: Maybe Name,

8386 indent_stack :: [Int],

8487 brace_stack :: [Maybe Int],

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

8689 default_access :: Accessibility,

8790 default_total :: Bool,

8891 ibc_write :: [IBCWrite],

89− compiled_so :: Maybe String

92+ compiled_so :: Maybe String,

93+ idris_dynamic_libs :: [DynamicLib],

94+ idris_language_extensions :: [LanguageExt]

9095 }

9196

9297data SizeChange = Smaller | Same | Bigger | Unknown

9398 deriving (Show, Eq)

94−{-!

99+{-!

95100deriving instance Binary SizeChange

96101!-}

97102

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

123128 | IBCImport FilePath

124129 | IBCObj FilePath

125130 | IBCLib String

131+ | IBCDyLib String

126132 | IBCHeader String

127133 | IBCAccess Name Accessibility

128134 | IBCTotal Name Totality

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

137143 emptyContext emptyContext emptyContext emptyContext

138144 emptyContext emptyContext emptyContext emptyContext

139145 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

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

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

141147

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

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

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

181187 | Defn Name

182188 | Info Name

183189 | Missing Name

190+ | DynamicLink FilePath

191+ | ListDynamic

184192 | Pattelab PTerm

185193 | DebugInfo Name

186194 | Search PTerm

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

222230 | FOVM String

223231 | UseTarget Target

224232 | OutputTy OutputType

233+ | Extension LanguageExt

225234 deriving (Show, Eq)

226235

227236-- Parsed declarations

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

332341 | PSyntax FC Syntax -- ^ Syntax definition

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

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

335345 deriving Functor

336346{-!

337347deriving instance Binary PDecl'

338348!-}

339349

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

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)

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

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

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

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

src/Idris/ElabDecls.hs+32

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

1111import Idris.ElabTerm

1212import Idris.Coverage

1313import Idris.DataOpts

14+import Idris.Providers

1415import Paths_idris

1516

1617import Core.TT

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

1819import Core.Evaluate

20+import Core.Execute

1921import Core.Typecheck

2022import Core.CaseTree

2123

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

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

3941 return (n, t')) ns

4042

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

4144elabType :: ElabInfo -> SyntaxInfo -> String ->

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

4346elabType 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)

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

186189 updateParamsA ps args all = ps

187190

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+

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

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

190216elabRecord info syn doc fc tyn ty cdoc cn cty

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

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

330356 mkLazy t = t

331357

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

359+-- top-level definition.

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

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

334362 do ctxt <- getContext

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

12631291 addIBC (IBCDSL n)

12641292elabDecl' what info (PDirective i)

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

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

12671299

12681300elabCaseBlock 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

88 | MetaVarArg -- ^ The command takes a metavariable

99 | NoArg -- ^ No completion yet

1010

11−

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

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

1313help =

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

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

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

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

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

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

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

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

3132 ([":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),

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

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

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

src/Idris/IBC.hs+12−4

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

2121import Paths_idris

2222

2323ibcVersion :: Word8

24−ibcVersion = 27

24+ibcVersion = 28

2525

2626data IBCFile = IBCFile { ver :: Word8,

2727 sourcefile :: FilePath,

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

3838 ibc_keywords :: [String],

3939 ibc_objs :: [FilePath],

4040 ibc_libs :: [String],

41+ ibc_dynamic_libs :: [String],

4142 ibc_hdrs :: [String],

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

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

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

5253!-}

5354

5455initIBC :: IBCFile

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

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

5657

5758loadIBC :: FilePath -> Idris ()

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

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

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

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

112113ibc 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 }

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

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

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

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

147149 pKeywords (ibc_keywords i)

148150 pObjs (ibc_objs i)

149151 pLibs (ibc_libs i)

152+ pDyLibs (ibc_dynamic_libs i)

150153 pHdrs (ibc_hdrs i)

151154 pDefs (ibc_defs i)

152155 pAccess (ibc_access i)

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

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

243246pLibs ls = mapM_ addLib ls

244247

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

249+pDyLibs ls = mapM_ addDyLib ls

250+

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

246252pHdrs hs = mapM_ addHdr hs

247253

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

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

745751

746752instance 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)

748754 = do put x1

749755 put x2

750756 put x3

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

768774 put x21

769775 put x22

770776 put x23

777+ put x24

771778 get

772779 = do x1 <- get

773780 if x1 == ibcVersion then

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

793800 x21 <- get

794801 x22 <- get

795802 x23 <- 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)

803+ x24 <- get

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)

797805 else return (initIBC { ver = x1 })

798806

799807instance Binary FnOpt where

src/Idris/Parser.hs+46−29

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

1111import Idris.Coverage

1212import Idris.IBC

1313import Idris.Unlit

14+import Idris.Providers

1415import Paths_idris

1516

17+import Util.DynamicLinker

18+

1619import Core.CoreParser

1720import Core.TT

1821import Core.Evaluate

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

339342 <|> pClass syn

340343 <|> pInstance syn

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

342− <|> pDirective

345+ <|> pDirective syn

346+ <|> pProvider syn

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

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

345349

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

14651469 closeBlock

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

14671471

1468−pDirective :: IParser [PDecl]

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

1470− return [PDirective (do addLib lib

1471− addIBC (IBCLib lib))])

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

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

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

1475− addIBC (IBCObj o)

1476− addObjectFile o)])

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

1478− return [PDirective (do addHdr hdr

1479− addIBC (IBCHeader hdr))])

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

1481− return [PDirective (do setAccessibility n Hidden

1482− addIBC (IBCAccess n Hidden))])

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

1484− return [PDirective (do setAccessibility n Frozen

1485− addIBC (IBCAccess n Frozen))])

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

1487− return [PDirective (do i <- getIState

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

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

1490− i <- getState

1491− setState (i { default_total = tot } )

1492− return [PDirective (do i <- getIState

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

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

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

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

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

1474+ return [PDirective (do addLib lib

1475+ addIBC (IBCLib lib))])

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

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

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

1479+ addIBC (IBCObj o)

1480+ addObjectFile o)])

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

1482+ return [PDirective (do addHdr hdr

1483+ addIBC (IBCHeader hdr))])

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

1485+ return [PDirective (do setAccessibility n Hidden

1486+ addIBC (IBCAccess n Hidden))])

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

1488+ return [PDirective (do setAccessibility n Frozen

1489+ addIBC (IBCAccess n Frozen))])

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

1491+ return [PDirective (do i <- getIState

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

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

1494+ i <- getState

1495+ setState (i { default_total = tot } )

1496+ return [PDirective (do i <- getIState

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

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

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]

14961513

14971514pTactic :: SyntaxInfo -> IParser PTactic

14981515pTactic 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

2121

2222import Paths_idris

2323import Util.System

24+import Util.DynamicLinker

2425

2526import Core.Evaluate

27+import Core.Execute (execute)

2628import Core.ProofShell

2729import Core.TT

2830import Core.Constraints

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

5153import Data.Char

5254import Data.Version

5355

56+import Debug.Trace

57+

5458-- | Run the REPL

5559repl :: IState -- ^ The initial state

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

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

185189 imp <- impShow

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

187191 showImp imp (delab ist ty'))

188−process fn (ExecVal t)

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

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

191−-- [pexp t])

192− (tmpn, tmph) <- liftIO tempfile

193− liftIO $ hClose tmph

194− t <- target

195− compile t tmpn tm

196− liftIO $ system tmpn

197− return ()

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

192+process fn (ExecVal t)

193+ = do ctxt <- getContext

194+ ist <- getIState

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

196+ let tm' = normaliseAll ctxt [] tm

197+ let ty' = normaliseAll ctxt [] ty

198+ res <- execute tm'

199+ imp <- impShow

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

201+ showImp imp (delab ist ty'))

202+ return ()

199203process fn (Check (PRef _ n))

200204 = do ctxt <- getContext

201205 ist <- getIState

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

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

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

382386 _ -> iputStrLn $ "Ambiguous name"

383−process fn Metavars

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

400+process fn Metavars

384401 = do ist <- getIState

385402 let mvs = idris_metavars ist \\ primDefs

386403 case mvs of

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

441458

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

443460parseArgs [] = []

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

479497

480498helphead =

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

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

510528 xs -> last xs

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

512530 putIState (i { default_total = True })

531+ mapM_ addLangExt (opt getLanguageExt opts)

513532 setREPL runrepl

514533 setQuiet quiet

515534 setVerbose runrepl

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

609628getOutputTy (OutputTy t) = Just t

610629getOutputTy _ = Nothing

611630

631+getLanguageExt :: Opt -> Maybe LanguageExt

632+getLanguageExt (Extension e) = Just e

633+getLanguageExt _ = Nothing

634+

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

613636opt = mapMaybe

614637

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

2121019: magic with

2222020: implicit conversions

2323021: effects

24+022: dynamic C library loading and interpreter IO

2425

2526regxxx: 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:

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

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

230230\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}.

231232\end{itemize}

232233

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}

233249\subsection{Cumulativity}

234250

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