567b1be · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev

commit567b1be59653af496767da0afceb81bd01d0e466 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 18 Jan 2014, 18:15 (13 years ago) parentd7b2913 970c833

4 files changed+106−32

compare with master

unifiedsplit

main/Main.hs+57−30 src/Idris/AbsSyntaxTree.hs+1 src/Idris/REPL.hs+7 src/Pkg/Package.hs+41−2

main/Main.hs+57−30

@@ -53,6 +53,10 @@ runIdris opts = do

5353 when (ShowIncs `elem` opts) $ runIO showIncs

5454 when (ShowLibs `elem` opts) $ runIO showLibs

5555 when (ShowLibdir `elem` opts) $ runIO showLibdir

56+ case opt getPkgCheck opts of

57+ [] -> return ()

58+ fs -> do runIO $ mapM_ (checkPkg (WarnOnly `elem` opts)) fs

59+ runIO $ exitWith ExitSuccess

5660 case opt getPkgClean opts of

5761 [] -> return ()

5862 fs -> do runIO $ mapM_ cleanPkg fs

@@ -79,34 +83,57 @@ showIncs = do incFlags <- getIncFlags

7983 putStrLn incFlags

8084 exitWith ExitSuccess

8185

82−usagemsg = "Idris version " ++ ver ++ "\n" ++

83− "--------------" ++ map (\x -> '-') ver ++ "\n" ++

84− "Usage: idris [input file] [options]\n" ++

85− "Options:\n" ++

86− "\t--quiet Quiet mode (for editors)\n" ++

87− "\t--[no]colour Control REPL colour highlighting\n" ++

88− "\t--check Type check only\n" ++

89− "\t-o [file] Specify output filename\n" ++

90− "\t-i [dir] Add directory to the list of import paths\n" ++

91− "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++

92− "\t--noprelude Don't import the prelude\n" ++

93− "\t--total Require functions to be total by default\n" ++

94− "\t--warnpartial Warn about undeclared partial functions\n" ++

95− "\t--typeintype Disable universe checking\n" ++

96− "\t--log [level] Type debugging log level\n" ++

97− "\t-S Do no further compilation of code generator output\n" ++

98− "\t-c Compile to object files rather than an executable\n" ++

99− "\t--mvn Create a maven project (for Java codegen)\n" ++

100− "\t--exec [expr] Execute the expression expr in the interpreter,\n" ++

101− "\t defaulting to Main.main if none provided, and exit.\n" ++

102− "\t--ideslave Ideslave mode (for editors; in/ouput wrapped in \n" ++

103− "\t s-expressions)\n" ++

104− "\t--libdir Show library install directory and exit\n" ++

105− "\t--link Show C library directories and exit (for C linking)\n" ++

106− "\t--include Show C include directories and exit (for C linking)\n" ++

107− "\t--codegen [cg] Select code generator: C, Java, bytecode, javascript,\n" ++

108− "\t node or llvm\n" ++

109− "\t--target [triple] Select target triple (for LLVM codegen)\n" ++

110− "\t--cpu [cpu] Select target CPU (e.g. corei7 or cortex-m3) (for LLVM codegen)\n"

111−

86+usagemsghdr = "Idris version " ++ ver ++ ", (C) The Idris Community 2014"

87+

88+usagemsg = usagemsghdr ++ "\n" ++

89+ map (\x -> '-') usagemsghdr ++ "\n" ++

90+ "idris [OPTIONS] [FILE]\n\n" ++

91+ "Common flags:\n" ++

92+ "\t --install=IPKG Install Package\n" ++

93+ "\t --clean=IPKG Clean Package\n" ++

94+ "\t --build=IPKG Build Package\n" ++

95+ "\t --exec=EXPR Execute as Idris\n" ++

96+ "\t --libdir Display library directory\n" ++

97+ "\t --link Display link directory\n" ++

98+ "\t --include Display the includes directory\n" ++

99+ "\t --nobanner Suppress the banner\n" ++

100+ "\t --color Force colored output\n" ++

101+ "\t --colour Force coloured output\n" ++

102+ "\t --nocolor Disable colored output\n" ++

103+ "\t --nocolour Disable coloured output\n" ++

104+ "\t --errorcontent Undocumented\n" ++

105+ "\t --nocoverage Undocumented\n" ++

106+ "\t -o --output=FILE Specify output file\n" ++

107+ "\t --check Undocumented\n" ++

108+ "\t --total Require functions to be total by default\n" ++

109+ "\t --partial Undocumented\n" ++

110+ "\t --warnpartial Warn about undeclared partial functions.\n" ++

111+ "\t --warn Undocumented\n" ++

112+ "\t --typecase Undocumented\n" ++

113+ "\t --typeintype Undocumented\n" ++

114+ "\t --nobasepkgs Undocumented\n" ++

115+ "\t --noprelude Undocumented\n" ++

116+ "\t --nobuiltins Undocumented\n" ++

117+ "\t -O --level=LEVEL Undocumented\n" ++

118+ "\t -i --idrispath=DIR Add directory to the list of import paths\n" ++

119+ "\t --package=ITEM Undocumented\n" ++

120+ "\t --ibcsubdir=FILE Write IBC files into sub directory\n" ++

121+ "\t --codegen=TARGET Select code generator: C, Java, bytecode," ++

122+ "\t javascript, node, or llvm\n" ++

123+ "\t --mvn Create a maven project (for Java codegen)\n" ++

124+ "\t --cpu=CPU Select tartget CPU e.g. corei& or cortex-m3" ++

125+ "\t (for LLVM codegen)\n" ++

126+ "\t --target=TRIPLE Select target triple (for llvm codegen)\n" ++

127+ "\t -S --codegenonly Do no further compilation of code generator output\n" ++

128+ "\t -c --compileonly Compile to object fules rather than an executable\n" ++

129+ "\t -X --extension=ITEM undocumented\n" ++

130+ "\t --dumpdefuns Undocumented\n" ++

131+ "\t --dumpcases Undocumented\n" ++

132+ "\t --log=LEVEL --loglevel Type Debugging log level\n" ++

133+ "\t --ideslave Undocumented\n" ++

134+ "\t --client Undocumented\n" ++

135+ "\t -h --help Display help message\n" ++

136+ "\t -v --version Print version information\n" ++

137+ "\t -V --Verbose Loud verbosity\n" ++

138+ "\t -q --quiet Quiet verbosity\n"

112139

src/Idris/AbsSyntaxTree.hs+1

@@ -295,6 +295,7 @@ data Opt = Filename String

295295 | PkgBuild String

296296 | PkgInstall String

297297 | PkgClean String

298+ | PkgCheck String

298299 | WarnOnly

299300 | Pkg String

300301 | BCAsm String

src/Idris/REPL.hs+7

@@ -1008,11 +1008,14 @@ parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)

10081008parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)

10091009parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)

10101010parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)

1011+-- Package Related options

10111012parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)

10121013parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)

10131014parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)

10141015parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

10151016parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

1017+parseArgs ("--checkpkg":n:ns) = PkgCheck n : (parseArgs ns)

1018+-- Misc Options

10161019parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

10171020parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

10181021parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

@@ -1327,6 +1330,10 @@ getPkgClean :: Opt -> Maybe String

13271330getPkgClean (PkgClean str) = Just str

13281331getPkgClean _ = Nothing

13291332

1333+getPkgCheck :: Opt -> Maybe String

1334+getPkgCheck (PkgCheck str) = Just str

1335+getPkgCheck _ = Nothing

1336+

13301337getCodegen :: Opt -> Maybe Codegen

13311338getCodegen (UseCodegen x) = Just x

13321339getCodegen _ = Nothing

src/Pkg/Package.hs+41−2

@@ -24,13 +24,14 @@ import Pkg.PParser

2424

2525import Paths_idris (getDataDir)

2626

27+-- | Run the package through the idris compiler.

28+--

2729-- To build a package:

2830-- * read the package description

2931-- * check all the library dependencies exist

3032-- * invoke the makefile if there is one

3133-- * invoke idris on each module, with idris_opts

3234-- * install everything into datadir/pname, if install flag is set

33−

3435buildPkg :: Bool -> (Bool, FilePath) -> IO ()

3536buildPkg warnonly (install, fp)

3637 = do pkgdesc <- parseDesc fp

@@ -63,7 +64,33 @@ buildPkg warnonly (install, fp)

6364 putStrLn $ "\t" ++ show ms

6465 exitWith (ExitFailure 1)

6566

66−cleanPkg :: FilePath -> IO ()

67+-- | Type check packages only

68+--

69+-- This differs from build in that executables are not built, if the

70+-- package contains an executable.

71+checkPkg :: Bool -- ^ Show Warnings

72+ -> FilePath -- ^ Path to ipkg file.

73+ -> IO ()

74+checkPkg warnonly fpath

75+ = do pkgdesc <-parseDesc fpath

76+ ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)

77+ when (and ok) $

78+ do dir <- getCurrentDirectory

79+ setCurrentDirectory $ dir </> sourcedir pkgdesc

80+ make (makefile pkgdesc)

81+ res <- buildMods (NoREPL : Verbose : idris_opts pkgdesc)

82+ (modules pkgdesc)

83+ setCurrentDirectory dir

84+ case res of

85+ Nothing -> exitWith (ExitFailure 1)

86+ Just res' -> do

87+ case errLine res' of

88+ Just _ -> exitWith (ExitFailure 1)

89+ _ -> return ()

90+

91+-- | Clean Package build files

92+cleanPkg :: FilePath -- ^ Path to ipkg file.

93+ -> IO ()

6794cleanPkg fp

6895 = do pkgdesc <- parseDesc fp

6996 dir <- getCurrentDirectory

@@ -74,6 +101,7 @@ cleanPkg fp

74101 Nothing -> return ()

75102 Just s -> rmFile $ dir </> s

76103

104+-- | Install package

77105installPkg :: PkgDesc -> IO ()

78106installPkg pkgdesc

79107 = do dir <- getCurrentDirectory

@@ -83,6 +111,11 @@ installPkg pkgdesc

83111 Just o -> return () -- do nothing, keep executable locally, for noe

84112 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

85113

114+

115+-- ---------------------------------------------------------- [ Helper Methods ]

116+-- Methods for building, testing, installing, and removal of idris

117+-- packages.

118+

86119buildMods :: [Opt] -> [Name] -> IO (Maybe IState)

87120buildMods opts ns = do let f = map (toPath . showCG) ns

88121-- putStrLn $ "MODULE: " ++ show f

@@ -122,6 +155,7 @@ installIBC p m = do let f = toIBCFile m

122155 where getDest (UN n) = ""

123156 getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))

124157

158+

125159installObj :: String -> String -> IO ()

126160installObj p o = do d <- getTargetDir

127161 let destdir = addTrailingPathSeparator (d </> p)

@@ -136,12 +170,17 @@ mkDirCmd = "mkdir "

136170mkDirCmd = "mkdir -p "

137171#endif

138172

173+-- ------------------------------------------------------- [ Makefile Commands ]

174+-- | Invoke a Makefile's default target.

139175make :: Maybe String -> IO ()

140176make Nothing = return ()

141177make (Just s) = do system $ "make -f " ++ s

142178 return ()

143179

180+-- | Invoke a Makefile's clean target.

144181clean :: Maybe String -> IO ()

145182clean Nothing = return ()

146183clean (Just s) = do system $ "make -f " ++ s ++ " clean"

147184 return ()

185+

186+-- --------------------------------------------------------------------- [ EOF ]