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

git.iko.soy/Idris-dev

on master help sign in

%dynamic now works from IBC files

3a80954David Christiansen14 years ago

src/Core/Execute.hs+1−1

compare with master

unifiedsplit

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

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

src/Idris/AbsSyntax.hs+10−1

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

9import Core.Typecheck

10import Idris.AbsSyntaxTree

11import IRTS.CodegenCommon

12+import Util.DynamicLinker

13import Paths_idris

14import Paths_idris

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

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 }

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

352

361

353allImportDirs :: IState -> Idris [FilePath]

362allImportDirs :: IState -> Idris [FilePath]

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

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

355− return ("." : optdirs)

364+ return ("." : reverse optdirs)

356

365

357impShow :: Idris Bool

366impShow :: Idris Bool

358impShow = do i <- getIState

367impShow = do i <- getIState

src/Idris/AbsSyntaxTree.hs+1

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

124 | IBCImport FilePath

125 | IBCObj FilePath

126 | IBCLib String

127+ | IBCDyLib String

127 | IBCHeader String

128 | IBCHeader String

128 | IBCAccess Name Accessibility

129 | IBCAccess Name Accessibility

129 | IBCTotal Name Totality

130 | IBCTotal Name Totality

src/Idris/IBC.hs+12−4

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

21import Paths_idris

23ibcVersion :: Word8

24−ibcVersion = 27

24+ibcVersion = 28

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!-}

54initIBC :: IBCFile

55initIBC :: IBCFile

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

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

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

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

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

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

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

1492− return [PDirective (do i <- getIState

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

1493− handle <- lift $ tryLoadLib lib

1493+ addDyLib 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 })])

1500

1494

1501pProvider :: SyntaxInfo -> IParser [PDecl]

1495pProvider :: SyntaxInfo -> IParser [PDecl]

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

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