f7648db · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

@@ -723,6 +723,7 @@ Library

723 , IRTS.CodegenC

724 , IRTS.CodegenCommon

725 , IRTS.CodegenJavaScript

726+ , IRTS.Exports

726 , IRTS.JavaScript.AST

727 , IRTS.JavaScript.AST

727 , IRTS.Compiler

728 , IRTS.Compiler

728 , IRTS.Defunctionalise

729 , IRTS.Defunctionalise

libs/prelude/IO.idr+42

@@ -199,3 +199,45 @@ FFI_JS = MkFFI JS_Types String

199JS_IO : Type -> Type

200JS_IO = IO' FFI_JS

201

202+

203+--------- Foreign Exports

204+

205+namespace FFI_Export

206+-- It's just like Data.List.Elem, but we don't need all the other stuff

207+-- that comes with it, just a proof that a data type is defined.

208+ data DataDefined : Type -> List (Type, String) -> String -> Type where

209+ DHere : DataDefined x ((x, t) :: xs) t

210+ DThere : DataDefined x xs t -> DataDefined x (y :: xs) t

211+

212+ data FFI_Base : FFI -> List (Type, String) -> Type -> Type where

213+ FFI_ExpType : (def : DataDefined t xs n) -> FFI_Base f xs t

214+ FFI_Prim : (prim : ffi_types f t) -> FFI_Base f xs t

215+

216+ %used FFI_ExpType n

217+ %used FFI_ExpType def

218+ %used FFI_Prim prim

219+

220+ data FFI_Exportable : FFI -> List (Type, String) -> Type -> Type where

221+ FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t)

222+ FFI_Fun : (b : FFI_Base f xs s) -> FFI_Exportable f xs t -> FFI_Exportable f xs (s -> t)

223+ FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t

224+

225+ %used FFI_IO b

226+ %used FFI_Fun b

227+ %used FFI_Ret b

228+

229+ data FFI_Export : FFI -> String -> List (Type, String) -> Type where

230+ Data : (x : Type) -> (n : String) ->

231+ (es : FFI_Export f h ((x, n) :: xs)) -> FFI_Export f h xs

232+ Fun : (fn : t) -> (n : String) -> {auto prf : FFI_Exportable f xs t} ->

233+ (es : FFI_Export f h xs) -> FFI_Export f h xs

234+ End : FFI_Export f h xs

235+

236+%used Data x

237+%used Data n

238+%used Data es

239+%used Fun fn

240+%used Fun n

241+%used Fun es

242+%used Fun prf

243+

src/IRTS/CodegenCommon.hs+2−1

@@ -33,7 +33,8 @@ data CodegenInfo = CodegenInfo { outputFile :: String,

33 debugLevel :: DbgLevel,

34 simpleDecls :: [(Name, SDecl)],

35 defunDecls :: [(Name, DDecl)],

36− liftDecls :: [(Name, LDecl)]

36+ liftDecls :: [(Name, LDecl)],

37+ exportDecls :: [ExportIFace]

37 }

38 }

38

39

39type CodeGenerator = CodegenInfo -> IO ()

40type CodeGenerator = CodegenInfo -> IO ()

src/IRTS/Compiler.hs+3−1

@@ -11,6 +11,7 @@ import IRTS.CodegenC

11import IRTS.DumpBC

12import IRTS.CodegenJavaScript

13import IRTS.Inliner

14+import IRTS.Exports

14

15

15import Idris.AbsSyntax

16import Idris.AbsSyntax

16import Idris.AbsSyntaxTree

17import Idris.AbsSyntaxTree

@@ -89,12 +90,13 @@ compile codegen f tm

89 triple <- Idris.AbsSyntax.targetTriple

90 triple <- Idris.AbsSyntax.targetTriple

90 cpu <- Idris.AbsSyntax.targetCPU

91 cpu <- Idris.AbsSyntax.targetCPU

91 iLOG "Building output"

92 iLOG "Building output"

93+ exports <- findExports

92

94

93 case checked of

95 case checked of

94 OK c -> do return $ CodegenInfo f outty triple cpu

96 OK c -> do return $ CodegenInfo f outty triple cpu

95 hdrs impdirs objs libs flags

97 hdrs impdirs objs libs flags

96 NONE c (toAlist defuns)

98 NONE c (toAlist defuns)

97− tagged

99+ tagged exports

98-- runIO $ case codegen of

100-- runIO $ case codegen of

99-- ViaC -> codegenC cginfo

101-- ViaC -> codegenC cginfo

100-- ViaJava -> codegenJava cginfo

102-- ViaJava -> codegenJava cginfo

src/IRTS/Exports.hsnew file+9

@@ -0,0 +1,9 @@

1+module IRTS.Exports(findExports) where

2+

3+import Idris.AbsSyntax

4+import IRTS.Lang

5+

6+findExports :: Idris [ExportIFace]

7+findExports = do exps <- getExports

8+ return []

9+

src/IRTS/Lang.hs+14−1

@@ -29,7 +29,7 @@ data LExp = LV LVar

29 Int Name [LExp]

30 | LCase CaseType LExp [LAlt]

31 | LConst Const

32− | LForeign FDesc -- Function descriptor

32+ | LForeign FDesc -- Function descriptor (usually name as string)

33 FDesc -- Return type descriptor

34 [(FDesc, LExp)] -- first LExp is the FFI type description

35 | LOp PrimFn [LExp]

@@ -43,6 +43,19 @@ data FDesc = FCon Name

43 | FApp Name [FDesc]

44 deriving (Show, Eq)

45

46+data Export = ExportData Name -- Idris name

47+ FDesc -- Exported function descriptor (usually string)

48+ | ExportFun Name -- Idris name

49+ FDesc -- Exported function descriptor

50+ FDesc -- Return type descriptor

51+ [FDesc] -- Argument types

52+ deriving (Show, Eq)

53+

54+data ExportIFace = Export Name -- FFI descriptor

55+ String -- interface file

56+ [Export]

57+ deriving (Show, Eq)

58+

46-- Primitive operators. Backends are not *required* to implement all

59-- Primitive operators. Backends are not *required* to implement all

47-- of these, but should report an error if they are unable

60-- of these, but should report an error if they are unable

48

61

src/Idris/AbsSyntax.hs+13−5

@@ -129,22 +129,30 @@ addErasureUsage :: Name -> Int -> Idris ()

129addErasureUsage n i = do ist <- getIState

130 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }

131

132+addExport :: Name -> Idris ()

133+addExport n = do ist <- getIState

134+ putIState $ ist { idris_exports = n : idris_exports ist }

135+

132addUsedName :: FC -> Name -> Name -> Idris ()

136addUsedName :: FC -> Name -> Name -> Idris ()

133addUsedName fc n arg

137addUsedName fc n arg

134 = do ist <- getIState

138 = do ist <- getIState

135 case lookupTyName n (tt_ctxt ist) of

139 case lookupTyName n (tt_ctxt ist) of

136− [(_, ty)] -> addUsage 0 ty

140+ [(n', ty)] -> addUsage n' 0 ty

137 [] -> throwError (At fc (NoSuchVariable n))

141 [] -> throwError (At fc (NoSuchVariable n))

138 xs -> throwError (At fc (CantResolveAlts (map fst xs)))

142 xs -> throwError (At fc (CantResolveAlts (map fst xs)))

139− where addUsage i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))

143+ where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))

140− addErasureUsage n i

144+ addErasureUsage n i

141− | otherwise = addUsage (i + 1) sc

145+ | otherwise = addUsage n (i + 1) sc

142− addUsage _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))

146+ addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))

143

147

144getErasureUsage :: Idris [(Name, Int)]

148getErasureUsage :: Idris [(Name, Int)]

145getErasureUsage = do ist <- getIState;

149getErasureUsage = do ist <- getIState;

146 return (idris_erasureUsed ist)

150 return (idris_erasureUsed ist)

147

151

152+getExports :: Idris [Name]

153+getExports = do ist <- getIState

154+ return (idris_exports ist)

155+

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

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

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

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

150

158

src/Idris/AbsSyntaxTree.hs+4−2

@@ -225,7 +225,8 @@ data IState = IState {

225 idris_callswho :: Maybe (M.Map Name [Name]),

226 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined

227 elab_stack :: [Name], -- ^ Stack of names currently being elaborated

228− idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)

228+ idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)

229+ idris_exports :: [Name] -- ^ Functions with ExportList

229 }

230 }

230

231

231-- Required for parsers library, and therefore trifecta

232-- Required for parsers library, and therefore trifecta

@@ -297,6 +298,7 @@ data IBCWrite = IBCFix FixDecl

297 | IBCParsedRegion FC

298 | IBCParsedRegion FC

298 | IBCModDocs Name -- ^ The name is the special name used to track module docs

299 | IBCModDocs Name -- ^ The name is the special name used to track module docs

299 | IBCUsage (Name, Int)

300 | IBCUsage (Name, Int)

301+ | IBCExport Name

300 deriving Show

302 deriving Show

301

303

302-- | The initial state for the compiler

304-- | The initial state for the compiler

@@ -309,7 +311,7 @@ idrisInit = IState initContext [] []

309 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

311 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

310 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

312 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

311 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

313 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

312− AutomaticWidth S.empty [] Nothing Nothing [] [] M.empty

314+ AutomaticWidth S.empty [] Nothing Nothing [] [] M.empty []

313

315

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

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

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

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

src/Idris/Elab/Type.hs+8

@@ -181,6 +181,12 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

181 addIBC (IBCErrorHandler n)

182 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

183 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

184+ -- if it's an export list type, make a note of it

185+ case (unApply usety) of

186+ (P _ ut _, _)

187+ | ut == ffiexport -> do addIBC (IBCExport n)

188+ addExport n

189+ _ -> return ()

184 return usety

190 return usety

185 where

191 where

186 -- for making an internalapp, we only want the explicit ones, and don't

192 -- for making an internalapp, we only want the explicit ones, and don't

@@ -191,6 +197,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

191 | otherwise = mergeTy sc sc'

197 | otherwise = mergeTy sc sc'

192 mergeTy _ sc = sc

198 mergeTy _ sc = sc

193

199

200+ ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]

201+

194 err = txt "Err"

202 err = txt "Err"

195 maybe = txt "Maybe"

203 maybe = txt "Maybe"

196 lst = txt "List"

204 lst = txt "List"

src/Idris/Erasure.hs+18−14

@@ -68,9 +68,9 @@ type Vars = Map Name VarInfo

68performUsageAnalysis :: Idris [Name]

69performUsageAnalysis = do

70 ctx <- tt_ctxt <$> getIState

71− mainName <- getMainName <$> getIState

71+ startNames <- getStartNames <$> getIState

72

73− case mainName of

73+ case startNames of

74 Left reason -> return [] -- no main -> not compiling -> reachability irrelevant

75 Right main -> do

76 ci <- idris_classes <$> getIState

@@ -106,11 +106,15 @@ performUsageAnalysis = do

106

107 return $ S.toList reachableNames

108 where

109− getMainName :: IState -> Either Err Name

109+ getStartNames :: IState -> Either Err [Name]

110+ getStartNames ist

111+ = do let es = idris_exports ist

110− getMainName ist = case lookupCtxtName n (idris_implicits ist) of

112+ case lookupCtxtName n (idris_implicits ist) of

111− [(n', _)] -> Right n'

113+ [(n', _)] -> Right (n' : es)

114+ [] -> if null es

112− [] -> Left (NoSuchVariable n)

115+ then Left (NoSuchVariable n)

116+ else Right es

113− more -> Left (CantResolveAlts (map fst more))

117+ more -> Left (CantResolveAlts (map fst more))

114 where

118 where

115 n = sNS (sUN "main") ["Main"]

119 n = sNS (sUN "main") ["Main"]

116

120

@@ -171,9 +175,9 @@ forwardChain deps

171

175

172-- Build the dependency graph,

176-- Build the dependency graph,

173-- starting the depth-first search from a list of Names.

177-- starting the depth-first search from a list of Names.

174−buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> Name -> Deps

178+buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> [Name] -> Deps

175−buildDepMap ci used ctx mainName = addPostulates used $

179+buildDepMap ci used ctx startNames = addPostulates used $

176− dfs S.empty M.empty [mainName]

180+ dfs S.empty M.empty startNames

177 where

181 where

178 -- mark the result of Main.main as used with the empty assumption

182 -- mark the result of Main.main as used with the empty assumption

179 addPostulates :: [(Name, Int)] -> Deps -> Deps

183 addPostulates :: [(Name, Int)] -> Deps -> Deps

@@ -191,13 +195,13 @@ buildDepMap ci used ctx mainName = addPostulates used $

191

195

192 postulates used =

196 postulates used =

193 [ [] ==> concat

197 [ [] ==> concat

194− -- These two, Main.main and run__IO, are always evaluated

198+ -- Main.main ( + export lists) and run__IO, are always evaluated

195 -- but they elude analysis since they come from the seed term.

199 -- but they elude analysis since they come from the seed term.

196− [ [(mainName, Result)]

200+ [(map (\n -> (n, Result)) startNames),

197− , [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

201+ [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

198

202

199 -- Explicit usage declarations from a %used pragma

203 -- Explicit usage declarations from a %used pragma

200− , map (\(n, i) -> (n, Arg i)) used

204+ , trace (show used) $ map (\(n, i) -> (n, Arg i)) used

201

205

202 -- MkIO is read by run__IO,

206 -- MkIO is read by run__IO,

203 -- but this cannot be observed in the source code of programs.

207 -- but this cannot be observed in the source code of programs.

src/Idris/IBC.hs+14−5

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

37import Util.Zlib (decompressEither)

38

39ibcVersion :: Word8

40−ibcVersion = 98

40+ibcVersion = 99

41

42data IBCFile = IBCFile { ver :: Word8,

43 sourcefile :: FilePath,

@@ -80,7 +80,8 @@ data IBCFile = IBCFile { ver :: Word8,

80 ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],

81 ibc_postulates :: ![Name],

82 ibc_parsedSpan :: !(Maybe FC),

83− ibc_usage :: ![(Name, Int)]

83+ ibc_usage :: ![(Name, Int)],

84+ ibc_exports :: ![Name]

84 }

85 }

85 deriving Show

86 deriving Show

86{-!

87{-!

@@ -88,7 +89,7 @@ deriving instance Binary IBCFile

88!-}

89!-}

89

90

90initIBC :: IBCFile

91initIBC :: IBCFile

91−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing []

92+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] []

92

93

93loadIBC :: Bool -- ^ True = reexport, False = make everything private

94loadIBC :: Bool -- ^ True = reexport, False = make everything private

94 -> FilePath -> Idris ()

95 -> FilePath -> Idris ()

@@ -233,6 +234,7 @@ ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

233 Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }

234 Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }

234 _ -> ifail "IBC write failed"

235 _ -> ifail "IBC write failed"

235ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

236ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

237+ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

236

238

237process :: Bool -- ^ Reexporting

239process :: Bool -- ^ Reexporting

238 -> IBCFile -> FilePath -> Idris ()

240 -> IBCFile -> FilePath -> Idris ()

@@ -290,6 +292,7 @@ process reexp i fn

290 pPostulates $ force (ibc_postulates i)

292 pPostulates $ force (ibc_postulates i)

291 pParsedSpan $ force (ibc_parsedSpan i)

293 pParsedSpan $ force (ibc_parsedSpan i)

292 pUsage $ force (ibc_usage i)

294 pUsage $ force (ibc_usage i)

295+ pExports $ force (ibc_exports i)

293

296

294timestampOlder :: FilePath -> FilePath -> Idris ()

297timestampOlder :: FilePath -> FilePath -> Idris ()

295timestampOlder src ibc = do srct <- runIO $ getModificationTime src

298timestampOlder src ibc = do srct <- runIO $ getModificationTime src

@@ -311,6 +314,10 @@ pUsage :: [(Name, Int)] -> Idris ()

311pUsage ns = do ist <- getIState

314pUsage ns = do ist <- getIState

312 putIState ist { idris_erasureUsed = ns ++ idris_erasureUsed ist }

315 putIState ist { idris_erasureUsed = ns ++ idris_erasureUsed ist }

313

316

317+pExports :: [Name] -> Idris ()

318+pExports ns = do ist <- getIState

319+ putIState ist { idris_exports = ns ++ idris_exports ist }

320+

314pImportDirs :: [FilePath] -> Idris ()

321pImportDirs :: [FilePath] -> Idris ()

315pImportDirs fs = mapM_ addImportDir fs

322pImportDirs fs = mapM_ addImportDir fs

316

323

@@ -927,7 +934,7 @@ instance Binary MetaInformation where

927 _ -> error "Corrupted binary data for MetaInformation"

934 _ -> error "Corrupted binary data for MetaInformation"

928

935

929instance Binary IBCFile where

936instance Binary IBCFile where

930− put x@(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 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42)

937+ put x@(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 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43)

931 = {-# SCC "putIBCFile" #-}

938 = {-# SCC "putIBCFile" #-}

932 do put x1

939 do put x1

933 put x2

940 put x2

@@ -971,6 +978,7 @@ instance Binary IBCFile where

971 put x40

978 put x40

972 put x41

979 put x41

973 put x42

980 put x42

981+ put x43

974

982

975 get

983 get

976 = do x1 <- get

984 = do x1 <- get

@@ -1016,7 +1024,8 @@ instance Binary IBCFile where

1016 x40 <- get

1024 x40 <- get

1017 x41 <- get

1025 x41 <- get

1018 x42 <- get

1026 x42 <- get

1027+ x43 <- get

1019− 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 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42)

1028+ 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 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43)

1020 else return (initIBC { ver = x1 })

1029 else return (initIBC { ver = x1 })

1021

1030

1022instance Binary DataOpt where

1031instance Binary DataOpt where