788f800 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Record import paths in ibc

This way, an ibc contains everything needed to compile to an executable (including pointers to the other ibcs)

commit788f8007038527964f6ebe110d82a72aab6e01e5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 7 Aug 2014, 12:00 (12 years ago) parent42c694c

8 files changed+76−31

compare with master

unifiedsplit

src/IRTS/Compiler.hs+24−13 src/Idris/AbsSyntax.hs+11−1 src/Idris/AbsSyntaxTree.hs+4−1 src/Idris/Core/ProofTerm.hs+2−2 src/Idris/Core/TT.hs+10−7 src/Idris/IBC.hs+12−4 src/Idris/Parser.hs+6−1 src/Idris/REPL.hs+7−2

src/IRTS/Compiler.hs+24−13

@@ -1,6 +1,6 @@

11{-# LANGUAGE PatternGuards, TypeSynonymInstances, CPP #-}

3−module IRTS.Compiler where

3+module IRTS.Compiler(compile, generate) where

55import IRTS.Lang

66import IRTS.Defunctionalise

@@ -47,7 +47,9 @@ import System.Directory

4747import System.Environment

4848import System.FilePath ((</>), addTrailingPathSeparator)

4949

50−compile :: Codegen -> FilePath -> Term -> Idris ()

50+-- | Given a 'main' term to compiler, return the IRs which can be used to

51+-- generate code.

52+compile :: Codegen -> FilePath -> Term -> Idris CodegenInfo

5153compile codegen f tm

5254 = do checkMVs -- check for undefined metavariables

5355 checkTotality -- refuse to compile if there are totality problems

@@ -88,17 +90,17 @@ compile codegen f tm

8890 iLOG "Building output"

8991

9092 case checked of

91− OK c -> do let cginfo = CodegenInfo f outty triple cpu optimise

92− hdrs impdirs objs libs flags

93− NONE c (toAlist defuns)

94− tagged

95− runIO $ case codegen of

96− ViaC -> codegenC cginfo

97− ViaJava -> codegenJava cginfo

98− ViaJavaScript -> codegenJavaScript cginfo

99− ViaNode -> codegenNode cginfo

100− ViaLLVM -> codegenLLVM cginfo

101− Bytecode -> dumpBC c f

93+ OK c -> do return $ CodegenInfo f outty triple cpu optimise

94+ hdrs impdirs objs libs flags

95+ NONE c (toAlist defuns)

96+ tagged

97+-- runIO $ case codegen of

98+-- ViaC -> codegenC cginfo

99+-- ViaJava -> codegenJava cginfo

100+-- ViaJavaScript -> codegenJavaScript cginfo

101+-- ViaNode -> codegenNode cginfo

102+-- ViaLLVM -> codegenLLVM cginfo

103+-- Bytecode -> dumpBC c f

102104 Error e -> ierror e

103105 where checkMVs = do i <- getIState

104106 case map fst (idris_metavars i) \\ primDefs of

@@ -112,6 +114,15 @@ compile codegen f tm

112114 ex <- doesFileExist f

113115 if ex then return f else return h

114116

117+generate :: Codegen -> CodegenInfo -> IO ()

118+generate codegen ir = case codegen of

119+ ViaC -> codegenC ir

120+ ViaJava -> codegenJava ir

121+ ViaJavaScript -> codegenJavaScript ir

122+ ViaNode -> codegenNode ir

123+ ViaLLVM -> codegenLLVM ir

124+ Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)

125+

115126irMain :: TT Name -> Idris LDecl

116127irMain tm = do

117128 i <- irTerm M.empty [] tm

src/Idris/AbsSyntax.hs+11−1

@@ -82,6 +82,16 @@ addDyLib libs = do i <- getIState

8282 findDyLib (lib:libs) l | l == lib_name lib = Just lib

8383 | otherwise = findDyLib libs l

8484

85+getAutoImports :: Idris [FilePath]

86+getAutoImports = do i <- getIState

87+ return (opt_autoImport (idris_options i))

88+

89+addAutoImport :: FilePath -> Idris ()

90+addAutoImport fp = do i <- getIState

91+ let opts = idris_options i

92+ let autoimps = opt_autoImport opts

93+ put (i { idris_options = opts { opt_autoImport =

94+ fp : opt_autoImport opts } } )

8595

8696addHdr :: Codegen -> String -> Idris ()

8797addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

@@ -739,7 +749,7 @@ valIBCSubDir i = return (opt_ibcsubdir (idris_options i))

739749addImportDir :: FilePath -> Idris ()

740750addImportDir fp = do i <- getIState

741751 let opts = idris_options i

742− let opt' = opts { opt_importdirs = fp : opt_importdirs opts }

752+ let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }

743753 putIState $ i { idris_options = opt' }

744754

745755setImportDirs :: [FilePath] -> Idris ()

src/Idris/AbsSyntaxTree.hs+4−1

@@ -76,7 +76,8 @@ data IOption = IOption { opt_logLevel :: Int,

7676 opt_optLevel :: Word,

7777 opt_cmdline :: [Opt], -- remember whole command line

7878 opt_origerr :: Bool,

79− opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover

79+ opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover

80+ opt_autoImport :: [FilePath] -- ^ e.g. Builtins+Prelude

8081 }

8182 deriving (Show, Eq)

8283

@@ -100,6 +101,7 @@ defaultOpts = IOption { opt_logLevel = 0

100101 , opt_cmdline = []

101102 , opt_origerr = False

102103 , opt_autoSolve = True

104+ , opt_autoImport = []

103105 }

104106

105107data PPOption = PPOption {

@@ -247,6 +249,7 @@ data IBCWrite = IBCFix FixDecl

247249 | IBCSyntax Syntax

248250 | IBCKeyword String

249251 | IBCImport FilePath

252+ | IBCImportDir FilePath

250253 | IBCObj Codegen FilePath

251254 | IBCLib Codegen String

252255 | IBCCGFlag Codegen String

src/Idris/Core/ProofTerm.hs+2−2

@@ -133,10 +133,10 @@ updateSolvedTerm xs x = -- updateSolved' xs x where

133133 updateSolved' xs (Bind n (Hole ty) t)

134134 | Just v <- lookup n xs

135135 = case xs of

136− [_] -> (substV v $ psubst n v t, True) -- some may be Vs! Can't assume

136+ [_] -> (subst n v t, True) -- some may be Vs! Can't assume

137137 -- explicit names

138138 _ -> let (t', _) = updateSolved' xs t in

139− (substV v $ psubst n v t', True)

139+ (subst n v t', True)

140140 updateSolved' xs tm@(Bind n b t)

141141 | otherwise = let (t', ut) = updateSolved' xs t

142142 (b', ub) = updateSolvedB' xs b in

src/Idris/Core/TT.hs+10−7

@@ -969,13 +969,16 @@ subst n v tm = fst $ subst' 0 tm

969969

970970-- If there are no Vs in the term (i.e. in proof state)

971971psubst :: Eq n => n -> TT n -> TT n -> TT n

972−psubst n v tm = s' tm where

973− s' (P _ x _) | n == x = v

974− s' (Bind x b sc) | n == x = Bind x (fmap s' b) sc

975− | otherwise = Bind x (fmap s' b) (s' sc)

976− s' (App f a) = App (s' f) (s' a)

977− s' (Proj t idx) = Proj (s' t) idx

978− s' t = t

972+psubst n v tm = s' 0 tm where

973+ s' i (V x) | x > i = V (x - 1)

974+ | x == i = v

975+ | otherwise = V x

976+ s' i (P _ x _) | n == x = v

977+ s' i (Bind x b sc) | n == x = Bind x (fmap (s' i) b) sc

978+ | otherwise = Bind x (fmap (s' i) b) (s' (i+1) sc)

979+ s' i (App f a) = App (s' i f) (s' i a)

980+ s' i (Proj t idx) = Proj (s' i t) idx

981+ s' i t = t

979982

980983-- | As 'subst', but takes a list of (name, substitution) pairs instead

981984-- of a single name and substitution

src/Idris/IBC.hs+12−4

@@ -31,12 +31,13 @@ import Codec.Compression.Zlib (compress)

3131import Util.Zlib (decompressEither)

3232

3333ibcVersion :: Word8

34−ibcVersion = 75

34+ibcVersion = 76

3535

3636data IBCFile = IBCFile { ver :: Word8,

3737 sourcefile :: FilePath,

3838 symbols :: [Name],

3939 ibc_imports :: [FilePath],

40+ ibc_importdirs :: [FilePath],

4041 ibc_implicits :: [(Name, [PArg])],

4142 ibc_fixes :: [FixDecl],

4243 ibc_statics :: [(Name, [Bool])],

@@ -78,7 +79,7 @@ deriving instance Binary IBCFile

7879!-}

7980

8081initIBC :: IBCFile

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

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

8283

8384loadIBC :: FilePath -> Idris ()

8485loadIBC fp = do imps <- getImported

@@ -149,6 +150,7 @@ ibc i (IBCOpt n) f = case lookupCtxt n (idris_optimisation i) of

149150ibc i (IBCSyntax n) f = return f { ibc_syntax = n : ibc_syntax f }

150151ibc i (IBCKeyword n) f = return f { ibc_keywords = n : ibc_keywords f }

151152ibc i (IBCImport n) f = return f { ibc_imports = n : ibc_imports f }

153+ibc i (IBCImportDir n) f = return f { ibc_importdirs = n : ibc_importdirs f }

152154ibc i (IBCObj tgt n) f = return f { ibc_objs = (tgt, n) : ibc_objs f }

153155ibc i (IBCLib tgt n) f = return f { ibc_libs = (tgt, n) : ibc_libs f }

154156ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }

@@ -255,6 +257,7 @@ process i fn

255257 v <- verbose

256258 quiet <- getQuiet

257259-- when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i

260+ pImportDirs (ibc_importdirs i)

258261 pImports (ibc_imports i)

259262 pImps (ibc_implicits i)

260263 pFixes (ibc_fixes i)

@@ -307,6 +310,9 @@ pParsedSpan :: Maybe FC -> Idris ()

307310pParsedSpan fc = do ist <- getIState

308311 putIState ist { idris_parsedSpan = fc }

309312

313+pImportDirs :: [FilePath] -> Idris ()

314+pImportDirs fs = mapM_ addImportDir fs

315+

310316pImports :: [FilePath] -> Idris ()

311317pImports fs

312318 = do mapM_ (\f -> do i <- getIState

@@ -831,7 +837,7 @@ instance Binary MetaInformation where

831837 return (DataMI x1)

832838

833839instance Binary IBCFile where

834− 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)

840+ 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)

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

836842 do put x1

837843 put x2

@@ -871,6 +877,7 @@ instance Binary IBCFile where

871877 put x36

872878 put x37

873879 put x38

880+ put x39

874881

875882 get

876883 = do x1 <- get

@@ -912,7 +919,8 @@ instance Binary IBCFile where

912919 x36 <- get

913920 x37 <- get

914921 x38 <- get

915− 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)

922+ x39 <- get

923+ 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)

916924 else return (initIBC { ver = x1 })

917925

918926instance Binary DataOpt where

src/Idris/Parser.hs+6−1

@@ -1240,7 +1240,9 @@ loadSource lidr f toline

12401240 let def_total = default_total i

12411241 file_in <- runIO $ readFile f

12421242 file <- if lidr then tclift $ unlit f file_in else return file_in

1243− (mname, imports, pos) <- parseImports f file

1243+ (mname, imports_in, pos) <- parseImports f file

1244+ ai <- getAutoImports

1245+ let imports = map (\n -> (n, Just n, emptyFC)) ai ++ imports_in

12441246 ids <- allImportDirs

12451247 ibcsd <- valIBCSubDir i

12461248 mapM_ (\f -> do fp <- findImport ids ibcsd f

@@ -1264,6 +1266,9 @@ loadSource lidr f toline

12641266 i <- getIState

12651267 putIState (i { default_access = Hidden, module_aliases = modAliases })

12661268 clearIBC -- start a new .ibc file

1269+ -- record package info in .ibc

1270+ imps <- allImportDirs

1271+ mapM_ addIBC (map IBCImportDir imps)

12671272 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]

12681273 let syntax = defaultSyntax{ syn_namespace = reverse mname,

12691274 maxline = toline }

src/Idris/REPL.hs+7−2

@@ -975,7 +975,8 @@ process fn Execute

975975 (tmpn, tmph) <- runIO tempfile

976976 runIO $ hClose tmph

977977 t <- codegen

978− compile t tmpn m

978+ ir <- compile t tmpn m

979+ runIO $ generate t ir

979980 case idris_outputmode ist of

980981 RawOutput h -> do runIO $ system tmpn

981982 return ()

@@ -987,7 +988,8 @@ process fn (Compile codegen f)

987988 = do (m, _) <- elabVal recinfo ERHS

988989 (PApp fc (PRef fc (sUN "run__IO"))

989990 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

990− compile codegen f m

991+ ir <- compile codegen f m

992+ runIO $ generate codegen ir

991993 where fc = fileFC "main"

992994process fn (LogLvl i) = setLogLevel i

993995-- Elaborate as if LHS of a pattern (debug command)

@@ -1330,8 +1332,10 @@ idrisMain opts =

13301332 mapM_ addPkgDir pkgdirs

13311333 elabPrims

13321334 when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins"

1335+ addAutoImport "Builtins"

13331336 return ()

13341337 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

1338+ addAutoImport "Prelude"

13351339 return ()

13361340

13371341 when (runrepl && not idesl) initScript

@@ -1402,6 +1406,7 @@ idrisMain opts =

14021406 addPkgDir :: String -> Idris ()

14031407 addPkgDir p = do ddir <- runIO $ getDataDir

14041408 addImportDir (ddir </> p)

1409+ addIBC (IBCImportDir (ddir </> p))

14051410

14061411execScript :: String -> Idris ()

14071412execScript expr = do i <- getIState