ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-11 08:55:23 +03:00
Code Issues Projects Releases Wiki Activity

Added simple library packaging system

Browse Source 
Now used for the prelude (see lib/base.ipkg)
This commit is contained in:
Edwin Brady 2012-09-25 17:34:50 +01:00
parent 28325170b3
commit 1e52324008
15 changed files with 341 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
CHANGELOG
View File

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

2
Makefile
View File

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

4
idris.cabal
View File

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

18
lib/Makefile
View File

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

15
lib/base.ipkg Normal file
View File

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

2
lib/prelude/complex.idr
View File

@ -6,7 +6,7 @@
module prelude.complex
import builtins
import prelude
------------------------------ Rectangular form

1
rts/libtest.c Normal file
View File

@ -0,0 +1 @@
int main() {}

2
src/IRTS/CodegenC.hs
View File

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

11
src/Idris/AbsSyntax.hs
View File

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

7
src/Idris/AbsSyntaxTree.hs
View File

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

49
src/Idris/REPL.hs
View File

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

35
src/Main.hs
View File

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

102
src/Pkg/PParser.hs Normal file
View File

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

128
src/Pkg/Package.hs Normal file
View File

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

8
src/Util/System.hs
View File

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