diff --git a/idris.cabal b/idris.cabal index 6b6efc8da..78ba49897 100644 --- a/idris.cabal +++ b/idris.cabal @@ -723,6 +723,7 @@ Library , IRTS.CodegenC , IRTS.CodegenCommon , IRTS.CodegenJavaScript + , IRTS.Exports , IRTS.JavaScript.AST , IRTS.Compiler , IRTS.Defunctionalise diff --git a/libs/prelude/IO.idr b/libs/prelude/IO.idr index 53f0089d8..210af52b9 100644 --- a/libs/prelude/IO.idr +++ b/libs/prelude/IO.idr @@ -199,3 +199,45 @@ FFI_JS = MkFFI JS_Types String JS_IO : Type -> Type JS_IO = IO' FFI_JS + +--------- Foreign Exports + +namespace FFI_Export +-- It's just like Data.List.Elem, but we don't need all the other stuff +-- that comes with it, just a proof that a data type is defined. + data DataDefined : Type -> List (Type, String) -> String -> Type where + DHere : DataDefined x ((x, t) :: xs) t + DThere : DataDefined x xs t -> DataDefined x (y :: xs) t + + data FFI_Base : FFI -> List (Type, String) -> Type -> Type where + FFI_ExpType : (def : DataDefined t xs n) -> FFI_Base f xs t + FFI_Prim : (prim : ffi_types f t) -> FFI_Base f xs t + + %used FFI_ExpType n + %used FFI_ExpType def + %used FFI_Prim prim + + data FFI_Exportable : FFI -> List (Type, String) -> Type -> Type where + FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t) + FFI_Fun : (b : FFI_Base f xs s) -> FFI_Exportable f xs t -> FFI_Exportable f xs (s -> t) + FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t + + %used FFI_IO b + %used FFI_Fun b + %used FFI_Ret b + + data FFI_Export : FFI -> String -> List (Type, String) -> Type where + Data : (x : Type) -> (n : String) -> + (es : FFI_Export f h ((x, n) :: xs)) -> FFI_Export f h xs + Fun : (fn : t) -> (n : String) -> {auto prf : FFI_Exportable f xs t} -> + (es : FFI_Export f h xs) -> FFI_Export f h xs + End : FFI_Export f h xs + +%used Data x +%used Data n +%used Data es +%used Fun fn +%used Fun n +%used Fun es +%used Fun prf + diff --git a/src/IRTS/CodegenCommon.hs b/src/IRTS/CodegenCommon.hs index a15bbb8cb..8d3e01a11 100644 --- a/src/IRTS/CodegenCommon.hs +++ b/src/IRTS/CodegenCommon.hs @@ -33,7 +33,8 @@ data CodegenInfo = CodegenInfo { outputFile :: String, debugLevel :: DbgLevel, simpleDecls :: [(Name, SDecl)], defunDecls :: [(Name, DDecl)], - liftDecls :: [(Name, LDecl)] + liftDecls :: [(Name, LDecl)], + exportDecls :: [ExportIFace] } type CodeGenerator = CodegenInfo -> IO () diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs index eef3777f1..0df74ae75 100644 --- a/src/IRTS/Compiler.hs +++ b/src/IRTS/Compiler.hs @@ -11,6 +11,7 @@ import IRTS.CodegenC import IRTS.DumpBC import IRTS.CodegenJavaScript import IRTS.Inliner +import IRTS.Exports import Idris.AbsSyntax import Idris.AbsSyntaxTree @@ -89,12 +90,13 @@ compile codegen f tm triple <- Idris.AbsSyntax.targetTriple cpu <- Idris.AbsSyntax.targetCPU iLOG "Building output" + exports <- findExports case checked of OK c -> do return $ CodegenInfo f outty triple cpu hdrs impdirs objs libs flags NONE c (toAlist defuns) - tagged + tagged exports -- runIO $ case codegen of -- ViaC -> codegenC cginfo -- ViaJava -> codegenJava cginfo diff --git a/src/IRTS/Exports.hs b/src/IRTS/Exports.hs new file mode 100644 index 000000000..84e0d2b69 --- /dev/null +++ b/src/IRTS/Exports.hs @@ -0,0 +1,9 @@ +module IRTS.Exports(findExports) where + +import Idris.AbsSyntax +import IRTS.Lang + +findExports :: Idris [ExportIFace] +findExports = do exps <- getExports + return [] + diff --git a/src/IRTS/Lang.hs b/src/IRTS/Lang.hs index 6bdc3a256..2231864cc 100644 --- a/src/IRTS/Lang.hs +++ b/src/IRTS/Lang.hs @@ -29,7 +29,7 @@ data LExp = LV LVar Int Name [LExp] | LCase CaseType LExp [LAlt] | LConst Const - | LForeign FDesc -- Function descriptor + | LForeign FDesc -- Function descriptor (usually name as string) FDesc -- Return type descriptor [(FDesc, LExp)] -- first LExp is the FFI type description | LOp PrimFn [LExp] @@ -43,6 +43,19 @@ data FDesc = FCon Name | FApp Name [FDesc] deriving (Show, Eq) +data Export = ExportData Name -- Idris name + FDesc -- Exported function descriptor (usually string) + | ExportFun Name -- Idris name + FDesc -- Exported function descriptor + FDesc -- Return type descriptor + [FDesc] -- Argument types + deriving (Show, Eq) + +data ExportIFace = Export Name -- FFI descriptor + String -- interface file + [Export] + deriving (Show, Eq) + -- Primitive operators. Backends are not *required* to implement all -- of these, but should report an error if they are unable diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs index fd41cf88f..d71b4e1e1 100644 --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -129,22 +129,30 @@ addErasureUsage :: Name -> Int -> Idris () addErasureUsage n i = do ist <- getIState putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist } +addExport :: Name -> Idris () +addExport n = do ist <- getIState + putIState $ ist { idris_exports = n : idris_exports ist } + addUsedName :: FC -> Name -> Name -> Idris () addUsedName fc n arg = do ist <- getIState case lookupTyName n (tt_ctxt ist) of - [(_, ty)] -> addUsage 0 ty + [(n', ty)] -> addUsage n' 0 ty [] -> throwError (At fc (NoSuchVariable n)) xs -> throwError (At fc (CantResolveAlts (map fst xs))) - where addUsage i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i)) - addErasureUsage n i - | otherwise = addUsage (i + 1) sc - addUsage _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg))) + where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i)) + addErasureUsage n i + | otherwise = addUsage n (i + 1) sc + addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg))) getErasureUsage :: Idris [(Name, Int)] getErasureUsage = do ist <- getIState; return (idris_erasureUsed ist) +getExports :: Idris [Name] +getExports = do ist <- getIState + return (idris_exports ist) + totcheck :: (FC, Name) -> Idris () totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] } diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs index 9a731fcac..1056a5d48 100644 --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -225,7 +225,8 @@ data IState = IState { idris_callswho :: Maybe (M.Map Name [Name]), idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined elab_stack :: [Name], -- ^ Stack of names currently being elaborated - idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names) + idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names) + idris_exports :: [Name] -- ^ Functions with ExportList } -- Required for parsers library, and therefore trifecta @@ -297,6 +298,7 @@ data IBCWrite = IBCFix FixDecl | IBCParsedRegion FC | IBCModDocs Name -- ^ The name is the special name used to track module docs | IBCUsage (Name, Int) + | IBCExport Name deriving Show -- | The initial state for the compiler @@ -309,7 +311,7 @@ idrisInit = IState initContext [] [] [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] [] [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] [] (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty - AutomaticWidth S.empty [] Nothing Nothing [] [] M.empty + AutomaticWidth S.empty [] Nothing Nothing [] [] M.empty [] -- | The monad for the main REPL - reading and processing files and updating -- global state (hence the IO inner monad). diff --git a/src/Idris/Elab/Type.hs b/src/Idris/Elab/Type.hs index 884945f83..5d457e400 100644 --- a/src/Idris/Elab/Type.hs +++ b/src/Idris/Elab/Type.hs @@ -181,6 +181,12 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params addIBC (IBCErrorHandler n) else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler" else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled." + -- if it's an export list type, make a note of it + case (unApply usety) of + (P _ ut _, _) + | ut == ffiexport -> do addIBC (IBCExport n) + addExport n + _ -> return () return usety where -- 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 | otherwise = mergeTy sc sc' mergeTy _ sc = sc + ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"] + err = txt "Err" maybe = txt "Maybe" lst = txt "List" diff --git a/src/Idris/Erasure.hs b/src/Idris/Erasure.hs index 0af150f18..58fe7ccf5 100644 --- a/src/Idris/Erasure.hs +++ b/src/Idris/Erasure.hs @@ -68,9 +68,9 @@ type Vars = Map Name VarInfo performUsageAnalysis :: Idris [Name] performUsageAnalysis = do ctx <- tt_ctxt <$> getIState - mainName <- getMainName <$> getIState + startNames <- getStartNames <$> getIState - case mainName of + case startNames of Left reason -> return [] -- no main -> not compiling -> reachability irrelevant Right main -> do ci <- idris_classes <$> getIState @@ -106,11 +106,15 @@ performUsageAnalysis = do return $ S.toList reachableNames where - getMainName :: IState -> Either Err Name - getMainName ist = case lookupCtxtName n (idris_implicits ist) of - [(n', _)] -> Right n' - [] -> Left (NoSuchVariable n) - more -> Left (CantResolveAlts (map fst more)) + getStartNames :: IState -> Either Err [Name] + getStartNames ist + = do let es = idris_exports ist + case lookupCtxtName n (idris_implicits ist) of + [(n', _)] -> Right (n' : es) + [] -> if null es + then Left (NoSuchVariable n) + else Right es + more -> Left (CantResolveAlts (map fst more)) where n = sNS (sUN "main") ["Main"] @@ -171,9 +175,9 @@ forwardChain deps -- Build the dependency graph, -- starting the depth-first search from a list of Names. -buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> Name -> Deps -buildDepMap ci used ctx mainName = addPostulates used $ - dfs S.empty M.empty [mainName] +buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> [Name] -> Deps +buildDepMap ci used ctx startNames = addPostulates used $ + dfs S.empty M.empty startNames where -- mark the result of Main.main as used with the empty assumption addPostulates :: [(Name, Int)] -> Deps -> Deps @@ -191,13 +195,13 @@ buildDepMap ci used ctx mainName = addPostulates used $ postulates used = [ [] ==> concat - -- These two, Main.main and run__IO, are always evaluated + -- Main.main ( + export lists) and run__IO, are always evaluated -- but they elude analysis since they come from the seed term. - [ [(mainName, Result)] - , [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)] + [(map (\n -> (n, Result)) startNames), + [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)] -- Explicit usage declarations from a %used pragma - , map (\(n, i) -> (n, Arg i)) used + , trace (show used) $ map (\(n, i) -> (n, Arg i)) used -- MkIO is read by run__IO, -- but this cannot be observed in the source code of programs. diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs index 804837d72..ca7087f54 100644 --- a/src/Idris/IBC.hs +++ b/src/Idris/IBC.hs @@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress) import Util.Zlib (decompressEither) ibcVersion :: Word8 -ibcVersion = 98 +ibcVersion = 99 data IBCFile = IBCFile { ver :: Word8, sourcefile :: FilePath, @@ -80,7 +80,8 @@ data IBCFile = IBCFile { ver :: Word8, ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))], ibc_postulates :: ![Name], ibc_parsedSpan :: !(Maybe FC), - ibc_usage :: ![(Name, Int)] + ibc_usage :: ![(Name, Int)], + ibc_exports :: ![Name] } deriving Show {-! @@ -88,7 +89,7 @@ deriving instance Binary IBCFile !-} initIBC :: IBCFile -initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] +initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] loadIBC :: Bool -- ^ True = reexport, False = make everything private -> FilePath -> Idris () @@ -233,6 +234,7 @@ ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f } _ -> ifail "IBC write failed" ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f } +ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f } process :: Bool -- ^ Reexporting -> IBCFile -> FilePath -> Idris () @@ -290,6 +292,7 @@ process reexp i fn pPostulates $ force (ibc_postulates i) pParsedSpan $ force (ibc_parsedSpan i) pUsage $ force (ibc_usage i) + pExports $ force (ibc_exports i) timestampOlder :: FilePath -> FilePath -> Idris () timestampOlder src ibc = do srct <- runIO $ getModificationTime src @@ -311,6 +314,10 @@ pUsage :: [(Name, Int)] -> Idris () pUsage ns = do ist <- getIState putIState ist { idris_erasureUsed = ns ++ idris_erasureUsed ist } +pExports :: [Name] -> Idris () +pExports ns = do ist <- getIState + putIState ist { idris_exports = ns ++ idris_exports ist } + pImportDirs :: [FilePath] -> Idris () pImportDirs fs = mapM_ addImportDir fs @@ -927,7 +934,7 @@ instance Binary MetaInformation where _ -> error "Corrupted binary data for MetaInformation" instance Binary IBCFile where - 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) + 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) = {-# SCC "putIBCFile" #-} do put x1 put x2 @@ -971,6 +978,7 @@ instance Binary IBCFile where put x40 put x41 put x42 + put x43 get = do x1 <- get @@ -1016,7 +1024,8 @@ instance Binary IBCFile where x40 <- get x41 <- get x42 <- get - 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 <- get + 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) else return (initIBC { ver = x1 }) instance Binary DataOpt where