f7648db · Idris-dev · git.iko.soy

idris.cabal+1

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

723723 , IRTS.CodegenC

724724 , IRTS.CodegenCommon

725725 , IRTS.CodegenJavaScript

726+ , IRTS.Exports

726727 , IRTS.JavaScript.AST

727728 , IRTS.Compiler

728729 , IRTS.Defunctionalise

libs/prelude/IO.idr+42

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

199199JS_IO : Type -> Type

200200JS_IO = IO' FFI_JS

201201

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,

3333 debugLevel :: DbgLevel,

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

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

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

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

37+ exportDecls :: [ExportIFace]

3738 }

3839

3940type CodeGenerator = CodegenInfo -> IO ()

src/IRTS/Compiler.hs+3−1

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

1111import IRTS.DumpBC

1212import IRTS.CodegenJavaScript

1313import IRTS.Inliner

14+import IRTS.Exports

1415

1516import Idris.AbsSyntax

1617import Idris.AbsSyntaxTree

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

8990 triple <- Idris.AbsSyntax.targetTriple

9091 cpu <- Idris.AbsSyntax.targetCPU

9192 iLOG "Building output"

93+ exports <- findExports

9294

9395 case checked of

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

9597 hdrs impdirs objs libs flags

9698 NONE c (toAlist defuns)

97− tagged

99+ tagged exports

98100-- runIO $ case codegen of

99101-- ViaC -> codegenC cginfo

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

2929 Int Name [LExp]

3030 | LCase CaseType LExp [LAlt]

3131 | LConst Const

32− | LForeign FDesc -- Function descriptor

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

3333 FDesc -- Return type descriptor

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

3535 | LOp PrimFn [LExp]

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

4343 | FApp Name [FDesc]

4444 deriving (Show, Eq)

4545

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+

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

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

4861

src/Idris/AbsSyntax.hs+13−5

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

129129addErasureUsage n i = do ist <- getIState

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

131131

132+addExport :: Name -> Idris ()

133+addExport n = do ist <- getIState

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

135+

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

133137addUsedName fc n arg

134138 = do ist <- getIState

135139 case lookupTyName n (tt_ctxt ist) of

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

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

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

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

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

140− addErasureUsage n i

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

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

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

144+ addErasureUsage n i

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

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

143147

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

145149getErasureUsage = do ist <- getIState;

146150 return (idris_erasureUsed ist)

147151

152+getExports :: Idris [Name]

153+getExports = do ist <- getIState

154+ return (idris_exports ist)

155+

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

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

150158

src/Idris/AbsSyntaxTree.hs+4−2

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

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

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

227227 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

229230 }

230231

231232-- Required for parsers library, and therefore trifecta

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

297298 | IBCParsedRegion FC

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

299300 | IBCUsage (Name, Int)

301+ | IBCExport Name

300302 deriving Show

301303

302304-- | The initial state for the compiler

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

309311 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

310312 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

311313 (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 []

313315

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

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

181181 addIBC (IBCErrorHandler n)

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

183183 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 ()

184190 return usety

185191 where

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

191197 | otherwise = mergeTy sc sc'

192198 mergeTy _ sc = sc

193199

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

201+

194202 err = txt "Err"

195203 maybe = txt "Maybe"

196204 lst = txt "List"

src/Idris/Erasure.hs+18−14

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

6868performUsageAnalysis :: Idris [Name]

6969performUsageAnalysis = do

7070 ctx <- tt_ctxt <$> getIState

71− mainName <- getMainName <$> getIState

71+ startNames <- getStartNames <$> getIState

7272

73− case mainName of

73+ case startNames of

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

7575 Right main -> do

7676 ci <- idris_classes <$> getIState

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

106106

107107 return $ S.toList reachableNames

108108 where

109− getMainName :: IState -> Either Err Name

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

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

112− [] -> Left (NoSuchVariable n)

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

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

110+ getStartNames ist

111+ = do let es = idris_exports ist

112+ case lookupCtxtName n (idris_implicits ist) of

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

114+ [] -> if null es

115+ then Left (NoSuchVariable n)

116+ else Right es

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

114118 where

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

116120

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

171175

172176-- Build the dependency graph,

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

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

175−buildDepMap ci used ctx mainName = addPostulates used $

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

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

179+buildDepMap ci used ctx startNames = addPostulates used $

180+ dfs S.empty M.empty startNames

177181 where

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

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

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

191195

192196 postulates used =

193197 [ [] ==> concat

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

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

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

196− [ [(mainName, Result)]

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

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

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

198202

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

201205

202206 -- MkIO is read by run__IO,

203207 -- 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)

3737import Util.Zlib (decompressEither)

3838

3939ibcVersion :: Word8

40−ibcVersion = 98

40+ibcVersion = 99

4141

4242data IBCFile = IBCFile { ver :: Word8,

4343 sourcefile :: FilePath,

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

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

8181 ibc_postulates :: ![Name],

8282 ibc_parsedSpan :: !(Maybe FC),

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

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

84+ ibc_exports :: ![Name]

8485 }

8586 deriving Show

8687{-!

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

8889!-}

8990

9091initIBC :: IBCFile

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

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

9293

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

9495 -> FilePath -> Idris ()

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

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

234235 _ -> ifail "IBC write failed"

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

236238

237239process :: Bool -- ^ Reexporting

238240 -> IBCFile -> FilePath -> Idris ()

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

290292 pPostulates $ force (ibc_postulates i)

291293 pParsedSpan $ force (ibc_parsedSpan i)

292294 pUsage $ force (ibc_usage i)

295+ pExports $ force (ibc_exports i)

293296

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

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

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

311314pUsage ns = do ist <- getIState

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

313316

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

318+pExports ns = do ist <- getIState

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

320+

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

315322pImportDirs fs = mapM_ addImportDir fs

316323

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

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

928935

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

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

932939 do put x1

933940 put x2

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

971978 put x40

972979 put x41

973980 put x42

981+ put x43

974982

975983 get

976984 = do x1 <- get

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

10161024 x40 <- get

10171025 x41 <- get

10181026 x42 <- 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)

1027+ x43 <- get

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)

10201029 else return (initIBC { ver = x1 })

10211030

10221031instance Binary DataOpt where