3a80954 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

%dynamic now works from IBC files

commit3a809543c297628f78b3230664dd24105bd51304 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 15 Mar 2013, 16:07 (14 years ago) parent70c9bd5

5 files changed+26−14

compare with master

unifiedsplit

src/Core/Execute.hs+1−1 src/Idris/AbsSyntax.hs+10−1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/IBC.hs+12−4 src/Idris/Parser.hs+2−8

src/Core/Execute.hs+1−1

@@ -31,7 +31,7 @@ execute tm = do stepped <- step tm

3131

3232

3333

3535

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

3737

src/Idris/AbsSyntax.hs+10−1

@@ -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,6 +41,14 @@ 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

@@ -352,7 +361,7 @@ setImportDirs fps = do i <- getIState

352361

353362allImportDirs :: IState -> Idris [FilePath]

354363allImportDirs i = do let optdirs = opt_importdirs (idris_options i)

355− return ("." : optdirs)

364+ return ("." : reverse optdirs)

356365

357366impShow :: Idris Bool

358367impShow = do i <- getIState

src/Idris/AbsSyntaxTree.hs+1

@@ -124,6 +124,7 @@ data IBCWrite = IBCFix FixDecl

124124 | IBCImport FilePath

125125 | IBCObj FilePath

126126 | IBCLib String

127+ | IBCDyLib String

127128 | IBCHeader String

128129 | IBCAccess Name Accessibility

129130 | IBCTotal Name Totality

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+2−8

@@ -1489,14 +1489,8 @@ pDirective syn = try (do lchar '%'; reserved "lib"; lib <- strlit;

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

14901490 return [PDirective (setLogLevel (fromInteger i))])

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

1492− return [PDirective (do i <- getIState

1493− handle <- lift $ tryLoadLib lib

1494− case handle of

1495− Nothing ->

1496− fail $ "Could not load dynamic lib \"" ++ lib ++ "\""

1497− Just x ->

1498− do let libs = idris_dynamic_libs i

1499− putIState $ i { idris_dynamic_libs = x:libs })])

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

1493+ addDyLib lib)])

15001494

15011495pProvider :: SyntaxInfo -> IParser [PDecl]

15021496pProvider syn = do lchar '%'; reserved "provide";