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

git.iko.soy/Idris-dev

on master help sign in

Record import paths in ibc

788f800Edwin Brady12 years ago

src/IRTS/Compiler.hs+24−13

compare with master

unifiedsplit

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

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

3−module IRTS.Compiler where

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

5import IRTS.Lang

6import IRTS.Defunctionalise

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

47import System.Environment

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

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

51+-- generate code.

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

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

51compile codegen f tm

53compile codegen f tm

52 = do checkMVs -- check for undefined metavariables

54 = do checkMVs -- check for undefined metavariables

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

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

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

88 iLOG "Building output"

90 iLOG "Building output"

90 case checked of

92 case checked of

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

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

92− hdrs impdirs objs libs flags

94+ hdrs impdirs objs libs flags

93− NONE c (toAlist defuns)

95+ NONE c (toAlist defuns)

94− tagged

96+ tagged

95− runIO $ case codegen of

97+-- runIO $ case codegen of

96− ViaC -> codegenC cginfo

98+-- ViaC -> codegenC cginfo

97− ViaJava -> codegenJava cginfo

99+-- ViaJava -> codegenJava cginfo

98− ViaJavaScript -> codegenJavaScript cginfo

100+-- ViaJavaScript -> codegenJavaScript cginfo

99− ViaNode -> codegenNode cginfo

101+-- ViaNode -> codegenNode cginfo

100− ViaLLVM -> codegenLLVM cginfo

102+-- ViaLLVM -> codegenLLVM cginfo

101− Bytecode -> dumpBC c f

103+-- Bytecode -> dumpBC c f

102 Error e -> ierror e

104 Error e -> ierror e

103 where checkMVs = do i <- getIState

105 where checkMVs = do i <- getIState

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

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

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

112 ex <- doesFileExist f

114 ex <- doesFileExist f

113 if ex then return f else return h

115 if ex then return f else return h

114

116

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+

115irMain :: TT Name -> Idris LDecl

126irMain :: TT Name -> Idris LDecl

116irMain tm = do

127irMain tm = do

117 i <- irTerm M.empty [] tm

128 i <- irTerm M.empty [] tm

src/Idris/AbsSyntax.hs+11−1

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

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

83 | otherwise = findDyLib libs l

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

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

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

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

97addHdr 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))

739addImportDir :: FilePath -> Idris ()

749addImportDir :: FilePath -> Idris ()

740addImportDir fp = do i <- getIState

750addImportDir fp = do i <- getIState

741 let opts = idris_options i

751 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 }

743 putIState $ i { idris_options = opt' }

753 putIState $ i { idris_options = opt' }

744

754

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

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

src/Idris/AbsSyntaxTree.hs+4−1

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

76 opt_optLevel :: Word,

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

78 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

80 }

81 }

81 deriving (Show, Eq)

82 deriving (Show, Eq)

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

100 , opt_cmdline = []

101 , opt_cmdline = []

101 , opt_origerr = False

102 , opt_origerr = False

102 , opt_autoSolve = True

103 , opt_autoSolve = True

104+ , opt_autoImport = []

103 }

105 }

104

106

105data PPOption = PPOption {

107data PPOption = PPOption {

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

247 | IBCSyntax Syntax

249 | IBCSyntax Syntax

248 | IBCKeyword String

250 | IBCKeyword String

249 | IBCImport FilePath

251 | IBCImport FilePath

252+ | IBCImportDir FilePath

250 | IBCObj Codegen FilePath

253 | IBCObj Codegen FilePath

251 | IBCLib Codegen String

254 | IBCLib Codegen String

252 | IBCCGFlag Codegen String

255 | IBCCGFlag Codegen String

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

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

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

134 | Just v <- lookup n xs

135 = 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

137 -- explicit names

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

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

139+ (subst n v t', True)

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

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

142 (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

969

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

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

972−psubst n v tm = s' tm where

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

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

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

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

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

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

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

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

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

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

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

978− s' t = t

981+ s' i t = t

979

982

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

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

981-- of a single name and substitution

984-- of a single name and substitution

src/Idris/IBC.hs+12−4

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

31import Util.Zlib (decompressEither)

33ibcVersion :: Word8

34−ibcVersion = 75

34+ibcVersion = 76

36data IBCFile = IBCFile { ver :: Word8,

37 sourcefile :: FilePath,

38 symbols :: [Name],

39 ibc_imports :: [FilePath],

40+ ibc_importdirs :: [FilePath],

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

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

41 ibc_fixes :: [FixDecl],

42 ibc_fixes :: [FixDecl],

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

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

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

78!-}

79!-}

80initIBC :: IBCFile

81initIBC :: IBCFile

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

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

83loadIBC :: FilePath -> Idris ()

84loadIBC :: FilePath -> Idris ()

84loadIBC fp = do imps <- getImported

85loadIBC fp = do imps <- getImported

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

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

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

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

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

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

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

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

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

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

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

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

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

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

255 v <- verbose

257 v <- verbose

256 quiet <- getQuiet

258 quiet <- getQuiet

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

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

260+ pImportDirs (ibc_importdirs i)

258 pImports (ibc_imports i)

261 pImports (ibc_imports i)

259 pImps (ibc_implicits i)

262 pImps (ibc_implicits i)

260 pFixes (ibc_fixes i)

263 pFixes (ibc_fixes i)

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

307pParsedSpan fc = do ist <- getIState

310pParsedSpan fc = do ist <- getIState

308 putIState ist { idris_parsedSpan = fc }

311 putIState ist { idris_parsedSpan = fc }

309

312

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

314+pImportDirs fs = mapM_ addImportDir fs

315+

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

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

311pImports fs

317pImports fs

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

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

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

831 return (DataMI x1)

837 return (DataMI x1)

832

838

833instance Binary IBCFile where

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

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

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

836 do put x1

842 do put x1

837 put x2

843 put x2

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

871 put x36

877 put x36

872 put x37

878 put x37

873 put x38

879 put x38

880+ put x39

874

881

875 get

882 get

876 = do x1 <- get

883 = do x1 <- get

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

912 x36 <- get

919 x36 <- get

913 x37 <- get

920 x37 <- get

914 x38 <- get

921 x38 <- get

922+ x39 <- 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)

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)

916 else return (initIBC { ver = x1 })

924 else return (initIBC { ver = x1 })

917

925

918instance Binary DataOpt where

926instance Binary DataOpt where

src/Idris/Parser.hs+6−1

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

1240 let def_total = default_total i

1241 file_in <- runIO $ readFile f

1242 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

1244 ids <- allImportDirs

1246 ids <- allImportDirs

1245 ibcsd <- valIBCSubDir i

1247 ibcsd <- valIBCSubDir i

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

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

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

1264 i <- getIState

1266 i <- getIState

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

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

1266 clearIBC -- start a new .ibc file

1268 clearIBC -- start a new .ibc file

1269+ -- record package info in .ibc

1270+ imps <- allImportDirs

1271+ mapM_ addIBC (map IBCImportDir imps)

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

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

1268 let syntax = defaultSyntax{ syn_namespace = reverse mname,

1273 let syntax = defaultSyntax{ syn_namespace = reverse mname,

1269 maxline = toline }

1274 maxline = toline }

src/Idris/REPL.hs+7−2

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

975 (tmpn, tmph) <- runIO tempfile

976 runIO $ hClose tmph

977 t <- codegen

978− compile t tmpn m

978+ ir <- compile t tmpn m

979+ runIO $ generate t ir

979 case idris_outputmode ist of

980 case idris_outputmode ist of

980 RawOutput h -> do runIO $ system tmpn

981 RawOutput h -> do runIO $ system tmpn

981 return ()

982 return ()

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

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

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

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

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

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

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

990− compile codegen f m

991+ ir <- compile codegen f m

992+ runIO $ generate codegen ir

991 where fc = fileFC "main"

993 where fc = fileFC "main"

992process fn (LogLvl i) = setLogLevel i

994process fn (LogLvl i) = setLogLevel i

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

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

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

1330 mapM_ addPkgDir pkgdirs

1332 mapM_ addPkgDir pkgdirs

1331 elabPrims

1333 elabPrims

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

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

1335+ addAutoImport "Builtins"

1333 return ()

1336 return ()

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

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

1338+ addAutoImport "Prelude"

1335 return ()

1339 return ()

1336

1340

1337 when (runrepl && not idesl) initScript

1341 when (runrepl && not idesl) initScript

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

1402 addPkgDir :: String -> Idris ()

1406 addPkgDir :: String -> Idris ()

1403 addPkgDir p = do ddir <- runIO $ getDataDir

1407 addPkgDir p = do ddir <- runIO $ getDataDir

1404 addImportDir (ddir </> p)

1408 addImportDir (ddir </> p)

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

1405

1410

1406execScript :: String -> Idris ()

1411execScript :: String -> Idris ()

1407execScript expr = do i <- getIState

1412execScript expr = do i <- getIState