ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-15 01:25:05 +03:00
Code Issues Projects Releases Wiki Activity

Foreign export lists in IO

Browse Source 
Not yet used, but this patch adds types in IO.idr, and treats them as
always reachable in erasure analysis.
This commit is contained in:
Edwin Brady 2015-03-06 12:18:05 +00:00
parent 49fffbcf5c
commit f7648db74e
11 changed files with 128 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
idris.cabal
View File

@ -723,6 +723,7 @@ Library
, IRTS.CodegenC
, IRTS.CodegenCommon
, IRTS.CodegenJavaScript
, IRTS.Exports
, IRTS.JavaScript.AST
, IRTS.Compiler
, IRTS.Defunctionalise

42
libs/prelude/IO.idr
View File

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

3
src/IRTS/CodegenCommon.hs
View File

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

4
src/IRTS/Compiler.hs
View File

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

9
src/IRTS/Exports.hs Normal file
View File

@ -0,0 +1,9 @@
module IRTS.Exports(findExports) where
import Idris.AbsSyntax
import IRTS.Lang
findExports :: Idris [ExportIFace]
findExports = do exps <- getExports
return []

15
src/IRTS/Lang.hs
View File

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

18
src/Idris/AbsSyntax.hs
View File

@ -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] }

6
src/Idris/AbsSyntaxTree.hs
View File

@ -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).

8
src/Idris/Elab/Type.hs
View File

@ -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"

32
src/Idris/Erasure.hs
View File

@ -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.

19
src/Idris/IBC.hs
View File

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