Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Added simple library packaging system

Now used for the prelude (see lib/base.ipkg)
  • Loading branch information...
commit 1e523240084951f9729912ad8560081b59e85f3b 1 parent 2832517
Edwin Brady authored
View
6 CHANGELOG
@@ -1,7 +1,13 @@
New in 0.9.4:
-------------
+User visible changes:
+
+* Simple packaging system
+
+Internal changes:
+* Improve overloading resolution (especially where this is a type error)
New in 0.9.3:
-------------
View
2  Makefile
@@ -15,7 +15,7 @@ test : .PHONY
make -C test
relib: .PHONY
- make -C lib clean
+ make -C lib IDRIS=../dist/build/idris/idris clean
make -C lib IDRIS=../dist/build/idris/idris
linecount : .PHONY
View
4 idris.cabal
@@ -1,5 +1,5 @@
Name: idris
-Version: 0.9.3.1
+Version: 0.9.4
License: BSD3
License-file: LICENSE
Author: Edwin Brady
@@ -42,6 +42,7 @@ Build-type: Custom
Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h
rts/idris_stdfgn.h rts/idris_main.c rts/idris_gmp.h
+ rts/libtest.c
Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr
lib/control/monad/*.idr lib/language/*.idr
tutorial/examples/*.idr
@@ -69,6 +70,7 @@ Executable idris
Idris.DataOpts, Idris.Transforms, Idris.DSL,
Util.Pretty, Util.System,
+ Pkg.Package, Pkg.PParser,
IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,
IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Compiler,
View
18 lib/Makefile
@@ -1,26 +1,14 @@
check: .PHONY
- $(IDRIS) --noprelude --verbose --check checkall.idr
+ $(IDRIS) --build base.ipkg
recheck: clean check
install: check
- mkdir -p $(TARGET)/prelude
- mkdir -p $(TARGET)/network
- mkdir -p $(TARGET)/language
- mkdir -p $(TARGET)/control/monad
- install *.ibc $(TARGET)
- install prelude/*.ibc $(TARGET)/prelude
- install network/*.ibc $(TARGET)/network
- install language/*.ibc $(TARGET)/language
- install control/monad/*.ibc $(TARGET)/control/monad
+ $(IDRIS) --install base.ipkg
clean: .PHONY
- rm -f *.ibc
- rm -f prelude/*.ibc
- rm -f network/*.ibc
- rm -f language/*.ibc
- rm -f control/monad/*.ibc
+ $(IDRIS) --clean base.ipkg
linecount: .PHONY
wc -l *.idr network/*.idr language/*.idr prelude/*.idr control/monad/*.idr
View
15 lib/base.ipkg
@@ -0,0 +1,15 @@
+package base
+
+opts = "--noprelude"
+modules = builtins, prelude, io, system,
+
+ prelude.algebra, prelude.cast, prelude.nat, prelude.fin,
+ prelude.list, prelude.maybe, prelude.monad, prelude.applicative,
+ prelude.either, prelude.vect, prelude.strings, prelude.char,
+ prelude.heap, prelude.complex,
+
+ network.cgi,
+
+ language.reflection,
+
+ control.monad.identity, control.monad.state
View
2  lib/prelude/complex.idr
@@ -6,7 +6,7 @@
module prelude.complex
import builtins
-
+import prelude
------------------------------ Rectangular form
View
1  rts/libtest.c
@@ -0,0 +1 @@
+int main() {}
View
2  src/IRTS/CodegenC.hs
@@ -38,7 +38,7 @@ codegenC defs out exec incs objs libs dbg
hFlush tmph
hClose tmph
let useclang = False
- let comp = if useclang then "clang" else "gcc"
+ comp <- getCC
let gcc = comp ++ " -I. " ++ objs ++ " -x c " ++
(if exec then "" else " - c ") ++
gccDbg dbg ++
View
11 src/Idris/AbsSyntax.hs
@@ -257,6 +257,12 @@ setIBCSubDir fp = do i <- get
valIBCSubDir :: IState -> Idris FilePath
valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
+addImportDir :: FilePath -> Idris ()
+addImportDir fp = do i <- get
+ let opts = idris_options i
+ let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
+ put (i { idris_options = opt' })
+
setImportDirs :: [FilePath] -> Idris ()
setImportDirs fps = do i <- get
let opts = idris_options i
@@ -264,9 +270,8 @@ setImportDirs fps = do i <- get
put (i { idris_options = opt' })
allImportDirs :: IState -> Idris [FilePath]
-allImportDirs i = do datadir <- liftIO $ getDataDir
- let optdirs = opt_importdirs (idris_options i)
- return ("." : (optdirs ++ [datadir]))
+allImportDirs i = do let optdirs = opt_importdirs (idris_options i)
+ return ("." : optdirs)
impShow :: Idris Bool
impShow = do i <- get
View
7 src/Idris/AbsSyntaxTree.hs
@@ -165,9 +165,14 @@ data Opt = Filename String
| Verbose
| IBCSubDir String
| ImportDir String
+ | PkgBuild String
+ | PkgInstall String
+ | PkgClean String
+ | WarnOnly
+ | Pkg String
| BCAsm String
| FOVM String
- deriving Eq
+ deriving (Show, Eq)
-- Parsed declarations
View
49 src/Idris/REPL.hs
@@ -365,6 +365,35 @@ displayHelp = let vstr = showVersion version in
l ++ take (c1 - length l) (repeat ' ') ++
m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
+parseArgs :: [String] -> [Opt]
+parseArgs [] = []
+parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
+parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
+parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
+parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)
+parseArgs ("-no":n:ns) = NoREPL : NewOutput n : (parseArgs ns)
+parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)
+parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)
+parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)
+parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)
+parseArgs ("--help":ns) = Usage : (parseArgs ns)
+parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)
+parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)
+parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)
+parseArgs ("--version":ns) = Ver : (parseArgs ns)
+parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)
+parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)
+parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)
+parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)
+parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)
+parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)
+parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)
+parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)
+parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)
+parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)
+parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)
+parseArgs (n:ns) = Filename n : (parseArgs ns)
+
help =
[ (["Command"], "Arguments", "Purpose"),
([""], "", ""),
@@ -402,6 +431,7 @@ idrisMain opts =
let importdirs = opt getImportDir opts
let bcs = opt getBC opts
let vm = opt getFOVM opts
+ let pkgdirs = opt getPkgDir opts
setREPL runrepl
setVerbose runrepl
when (Verbose `elem` opts) $ setVerbose True
@@ -418,6 +448,8 @@ idrisMain opts =
[] -> setIBCSubDir ""
(d:_) -> setIBCSubDir d
setImportDirs importdirs
+ addPkgDir "base"
+ mapM_ addPkgDir pkgdirs
elabPrims
when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"
return ()
@@ -442,6 +474,10 @@ idrisMain opts =
makeOption ErrContext = setErrContext True
makeOption _ = return ()
+ addPkgDir :: String -> Idris ()
+ addPkgDir p = do ddir <- liftIO $ getDataDir
+ addImportDir (ddir ++ "/" ++ p)
+
getFile :: Opt -> Maybe String
getFile (Filename str) = Just str
getFile _ = Nothing
@@ -470,6 +506,19 @@ getImportDir :: Opt -> Maybe String
getImportDir (ImportDir str) = Just str
getImportDir _ = Nothing
+getPkgDir :: Opt -> Maybe String
+getPkgDir (Pkg str) = Just str
+getPkgDir _ = Nothing
+
+getPkg :: Opt -> Maybe (Bool, String)
+getPkg (PkgBuild str) = Just (False, str)
+getPkg (PkgInstall str) = Just (True, str)
+getPkg _ = Nothing
+
+getPkgClean :: Opt -> Maybe String
+getPkgClean (PkgClean str) = Just str
+getPkgClean _ = Nothing
+
opt :: (Opt -> Maybe a) -> [Opt] -> [a]
opt = mapMaybe
View
35 src/Main.hs
@@ -25,13 +25,15 @@ import Idris.Primitives
import Idris.Imports
import Idris.Error
+import Pkg.Package
+
import Paths_idris
-- Main program reads command line options, parses the main program, and gets
-- on with the REPL.
main = do xs <- getArgs
- opts <- parseArgs xs
+ let opts = parseArgs xs
runInputT defaultSettings $ execStateT (runIdris opts) idrisInit
runIdris :: [Opt] -> Idris ()
@@ -41,7 +43,13 @@ runIdris opts = do
when (ShowIncs `elem` opts) $ liftIO showIncs
when (ShowLibs `elem` opts) $ liftIO showLibs
when (ShowLibdir `elem` opts) $ liftIO showLibdir
- idrisMain opts -- in Idris.REPL
+ case opt getPkgClean opts of
+ [] -> return ()
+ fs -> do liftIO $ mapM_ cleanPkg fs
+ liftIO $ exitWith ExitSuccess
+ case opt getPkg opts of
+ [] -> idrisMain opts -- in Idris.REPL
+ fs -> liftIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs
usage = do putStrLn usagemsg
exitWith ExitSuccess
@@ -61,29 +69,6 @@ showIncs = do dir <- getDataDir
putStrLn $ "-I" ++ dir ++ "/rts"
exitWith ExitSuccess
-parseArgs :: [String] -> IO [Opt]
-parseArgs [] = return []
-parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
-parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)
-parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
-parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)
-parseArgs ("-no":n:ns) = liftM (\x -> NoREPL : NewOutput n : x) (parseArgs ns)
-parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
-parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)
-parseArgs ("--nocoverage":ns) = liftM (NoCoverage : ) (parseArgs ns)
-parseArgs ("--errorcontext":ns) = liftM (ErrContext : ) (parseArgs ns)
-parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)
-parseArgs ("--link":ns) = liftM (ShowLibs : ) (parseArgs ns)
-parseArgs ("--libdir":ns) = liftM (ShowLibdir : ) (parseArgs ns)
-parseArgs ("--include":ns) = liftM (ShowIncs : ) (parseArgs ns)
-parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)
-parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)
-parseArgs ("--ibcsubdir":n:ns) = liftM (IBCSubDir n : ) (parseArgs ns)
-parseArgs ("-i":n:ns) = liftM (ImportDir n : ) (parseArgs ns)
-parseArgs ("--bytecode":n:ns) = liftM (\x -> NoREPL : BCAsm n : x) (parseArgs ns)
-parseArgs ("--fovm":n:ns) = liftM (\x -> NoREPL : FOVM n : x) (parseArgs ns)
-parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
-
usagemsg = "Idris version " ++ ver ++ "\n" ++
"--------------" ++ map (\x -> '-') ver ++ "\n" ++
"Usage: idris [input file] [options]\n" ++
View
102 src/Pkg/PParser.hs
@@ -0,0 +1,102 @@
+module Pkg.PParser where
+
+import Core.CoreParser
+import Core.TT
+import Idris.REPL
+import Idris.AbsSyntaxTree
+
+import Paths_idris
+
+import Text.ParserCombinators.Parsec
+import Text.ParserCombinators.Parsec.Error
+import Text.ParserCombinators.Parsec.Expr
+import Text.ParserCombinators.Parsec.Language
+import qualified Text.ParserCombinators.Parsec.Token as PTok
+
+type TokenParser a = PTok.TokenParser a
+
+type PParser = GenParser Char PkgDesc
+
+lexer :: TokenParser PkgDesc
+lexer = PTok.makeTokenParser idrisDef
+
+whiteSpace= PTok.whiteSpace lexer
+lexeme = PTok.lexeme lexer
+symbol = PTok.symbol lexer
+natural = PTok.natural lexer
+parens = PTok.parens lexer
+semi = PTok.semi lexer
+comma = PTok.comma lexer
+identifier= PTok.identifier lexer
+reserved = PTok.reserved lexer
+operator = PTok.operator lexer
+reservedOp= PTok.reservedOp lexer
+integer = PTok.integer lexer
+float = PTok.float lexer
+strlit = PTok.stringLiteral lexer
+chlit = PTok.charLiteral lexer
+lchar = lexeme.char
+
+data PkgDesc = PkgDesc { pkgname :: String,
+ libdeps :: [String],
+ objs :: [String],
+ makefile :: Maybe String,
+ idris_opts :: [Opt],
+ sourcedir :: String,
+ modules :: [Name],
+ idris_main :: Name,
+ execout :: Maybe String
+ }
+ deriving Show
+
+defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (UN "") Nothing
+
+parseDesc :: FilePath -> IO PkgDesc
+parseDesc fp = do p <- readFile fp
+ case runParser pPkg defaultPkg fp p of
+ Left err -> fail (show err)
+ Right x -> return x
+
+pPkg :: PParser PkgDesc
+pPkg = do reserved "package"; p <- identifier
+ st <- getState
+ setState (st { pkgname = p })
+ many1 pClause
+ st <- getState
+ return st
+
+pClause :: PParser ()
+pClause = do reserved "executable"; lchar '=';
+ exec <- iName []
+ st <- getState
+ setState (st { execout = Just (show exec) })
+ <|> do reserved "main"; lchar '=';
+ main <- iName []
+ st <- getState
+ setState (st { idris_main = main })
+ <|> do reserved "sourcedir"; lchar '=';
+ src <- identifier
+ st <- getState
+ setState (st { sourcedir = src })
+ <|> do reserved "opts"; lchar '=';
+ opts <- strlit
+ st <- getState
+ let args = parseArgs (words opts)
+ setState (st { idris_opts = args })
+ <|> do reserved "modules"; lchar '=';
+ ms <- sepBy1 (iName []) (lchar ',')
+ st <- getState
+ setState (st { modules = modules st ++ ms })
+ <|> do reserved "libs"; lchar '=';
+ ls <- sepBy1 identifier (lchar ',')
+ st <- getState
+ setState (st { libdeps = libdeps st ++ ls })
+ <|> do reserved "objs"; lchar '=';
+ ls <- sepBy1 identifier (lchar ',')
+ st <- getState
+ setState (st { objs = libdeps st ++ ls })
+ <|> do reserved "makefile"; lchar '=';
+ mk <- iName []
+ st <- getState
+ setState (st { makefile = Just (show mk) })
+
View
128 src/Pkg/Package.hs
@@ -0,0 +1,128 @@
+module Pkg.Package where
+
+import System.Process
+import System.Directory
+import System.Exit
+import System.IO
+
+import Util.System
+
+import Control.Monad
+import Data.List
+
+import Core.TT
+import Idris.REPL
+import Idris.AbsSyntax
+
+import Pkg.PParser
+
+import Paths_idris
+
+-- To build a package:
+-- * read the package description
+-- * check all the library dependencies exist
+-- * invoke the makefile if there is one
+-- * invoke idris on each module, with idris_opts
+-- * install everything into datadir/pname, if install flag is set
+
+buildPkg :: Bool -> (Bool, FilePath) -> IO ()
+buildPkg warnonly (install, fp)
+ = do pkgdesc <- parseDesc fp
+ ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
+ when (and ok) $
+ do make (makefile pkgdesc)
+ dir <- getCurrentDirectory
+ setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc
+ case (execout pkgdesc) of
+ Nothing -> buildMods (NoREPL : Verbose : idris_opts pkgdesc)
+ (modules pkgdesc)
+ Just o -> do let exec = dir ++ "/" ++ o
+ buildMod
+ (NoREPL : Verbose : Output exec : idris_opts pkgdesc)
+ (idris_main pkgdesc)
+ setCurrentDirectory dir
+ when install $ installPkg pkgdesc
+
+cleanPkg :: FilePath -> IO ()
+cleanPkg fp
+ = do pkgdesc <- parseDesc fp
+ clean (makefile pkgdesc)
+ dir <- getCurrentDirectory
+ setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc
+ mapM_ rmIBC (modules pkgdesc)
+ case execout pkgdesc of
+ Nothing -> return ()
+ Just s -> do let exec = dir ++ "/" ++ s
+ putStrLn $ "Removing " ++ exec
+ system $ "rm -f " ++ exec
+ return ()
+
+installPkg :: PkgDesc -> IO ()
+installPkg pkgdesc
+ = do dir <- getCurrentDirectory
+ setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc
+ case (execout pkgdesc) of
+ Nothing -> mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)
+ Just o -> return () -- do nothing, keep executable locally, for noe
+
+buildMod :: [Opt] -> Name -> IO ()
+buildMod opts n = do let f = map slash $ show n
+ idris (Filename f : opts)
+ return ()
+ where slash '.' = '/'
+ slash x = x
+
+buildMods :: [Opt] -> [Name] -> IO ()
+buildMods opts ns = do let f = map ((map slash) . show) ns
+ idris (map Filename f ++ opts)
+ return ()
+ where slash '.' = '/'
+ slash x = x
+
+testLib :: Bool -> String -> String -> IO Bool
+testLib warn p f
+ = do d <- getDataDir
+ gcc <- getCC
+ (tmpf, tmph) <- tempfile
+ hClose tmph
+ e <- system $ gcc ++ " " ++ d ++ "/rts/libtest.c -l" ++ f ++ " -o " ++ tmpf
+ case e of
+ ExitSuccess -> return True
+ _ -> do if warn
+ then do putStrLn $ "Not building " ++ p ++
+ " due to missing library " ++ f
+ return False
+ else fail $ "Missing library " ++ f
+
+rmIBC :: Name -> IO ()
+rmIBC m = do let f = toIBCFile m
+ putStrLn $ "Removing " ++ f
+ system $ "rm -f " ++ f
+ return ()
+
+toIBCFile (UN n) = n ++ ".ibc"
+toIBCFile (NS n ns) = concat (intersperse "/" (reverse ns)) ++ "/" ++ toIBCFile n
+
+installIBC :: String -> Name -> IO ()
+installIBC p m = do let f = toIBCFile m
+ d <- getDataDir
+ let destdir = d ++ "/" ++ p ++ "/" ++ getDest m
+ putStrLn $ "Installing " ++ f ++ " to " ++ destdir
+ system $ "mkdir -p " ++ destdir
+ system $ "install " ++ f ++ " " ++ destdir
+ return ()
+ where getDest (UN n) = ""
+ getDest (NS n ns) = concat (intersperse "/" (reverse ns)) ++ "/" ++ getDest n
+
+make :: Maybe String -> IO ()
+make Nothing = return ()
+make (Just s) = do system $ "make -f " ++ s
+ return ()
+
+clean :: Maybe String -> IO ()
+clean Nothing = return ()
+clean (Just s) = do system $ "make -f " ++ s ++ " clean"
+ return ()
+
+
+
View
8 src/Util/System.hs
@@ -1,5 +1,5 @@
{-# LANGUAGE CPP #-}
-module Util.System(tempfile,environment) where
+module Util.System(tempfile,environment,getCC) where
-- System helper functions.
@@ -16,6 +16,12 @@ catchIO = CE.catch
catchIO = catch
#endif
+getCC :: IO String
+getCC = do env <- environment "IDRIS_CC"
+ case env of
+ Nothing -> return "gcc"
+ Just cc -> return cc
+
tempfile :: IO (FilePath, Handle)
tempfile = do env <- environment "TMPDIR"
let dir = case env of
Please sign in to comment.
Something went wrong with that request. Please try again.