mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-25 22:06:33 +03:00
Add package files
This commit is contained in:
Edwin Brady
parent
b9e67db95d
commit
2afad1f13c
170
src/Idris/CommandLine.idr
Normal file
170
src/Idris/CommandLine.idr
Normal file
@ -0,0 +1,170 @@
|
|||||||
|
module Idris.CommandLine
|
||||||
|
|
||||||
|
%default total
|
||||||
|
|
||||||
|
public export
|
||||||
|
data PkgCommand
|
||||||
|
= Build
|
||||||
|
| Install
|
||||||
|
| REPL
|
||||||
|
|
||||||
|
|
||||||
|
export
|
||||||
|
Show PkgCommand where
|
||||||
|
show Build = "--build"
|
||||||
|
show Install = "--install"
|
||||||
|
show REPL = "--repl"
|
||||||
|
|
||||||
|
||| CLOpt - possible command line options
|
||||||
|
public export
|
||||||
|
data CLOpt
|
||||||
|
=
|
||||||
|
||| Only typecheck the given file
|
||||||
|
CheckOnly |
|
||||||
|
||| Execute a given function after checking the source file
|
||||||
|
ExecFn String |
|
||||||
|
||| Use a specific code generator (default chez)
|
||||||
|
SetCG String |
|
||||||
|
||| Don't implicitly import Prelude
|
||||||
|
NoPrelude |
|
||||||
|
||| Show the installation prefix
|
||||||
|
ShowPrefix |
|
||||||
|
||| Display blodwen version
|
||||||
|
Version |
|
||||||
|
||| Display help text
|
||||||
|
Help |
|
||||||
|
||| Run Blodwen in quiet mode
|
||||||
|
Quiet |
|
||||||
|
||| Add a package as a dependency
|
||||||
|
PkgPath String |
|
||||||
|
||| Build or install a given package, depending on PkgCommand
|
||||||
|
Package PkgCommand String |
|
||||||
|
||| The input Blodwen file
|
||||||
|
InputFile String |
|
||||||
|
||| Whether or not to run in IdeMode (easily parsable for other tools)
|
||||||
|
IdeMode |
|
||||||
|
||| Whether or not to run IdeMode (using a socket instead of stdin/stdout)
|
||||||
|
IdeModeSocket |
|
||||||
|
BlodwenPaths
|
||||||
|
|
||||||
|
|
||||||
|
ActType : List String -> Type
|
||||||
|
ActType [] = List CLOpt
|
||||||
|
ActType (a :: as) = String -> ActType as
|
||||||
|
|
||||||
|
record OptDesc where
|
||||||
|
constructor MkOpt
|
||||||
|
flags : List String
|
||||||
|
argdescs : List String
|
||||||
|
action : ActType argdescs
|
||||||
|
help : Maybe String
|
||||||
|
|
||||||
|
options : List OptDesc
|
||||||
|
options = [MkOpt ["--check", "-c"] [] [CheckOnly]
|
||||||
|
(Just "Exit after checking source file"),
|
||||||
|
MkOpt ["--exec", "-x"] ["name"] (\f => [ExecFn f, Quiet])
|
||||||
|
(Just "Execute function after checking source file"),
|
||||||
|
MkOpt ["--no-prelude"] [] [NoPrelude]
|
||||||
|
(Just "Don't implicitly import Prelude"),
|
||||||
|
MkOpt ["--codegen", "--cg"] ["backend"] (\f => [SetCG f])
|
||||||
|
(Just "Set code generator (default chez)"),
|
||||||
|
MkOpt ["--package", "-p"] ["package"] (\f => [PkgPath f])
|
||||||
|
(Just "Add a package as a dependency"),
|
||||||
|
|
||||||
|
MkOpt ["--ide-mode"] [] [IdeMode]
|
||||||
|
(Just "Run the REPL with machine-readable syntax"),
|
||||||
|
|
||||||
|
MkOpt ["--ide-mode-socket"] [] [IdeModeSocket]
|
||||||
|
(Just "Run the ide socket mode"),
|
||||||
|
|
||||||
|
MkOpt ["--prefix"] [] [ShowPrefix]
|
||||||
|
(Just "Show installation prefix"),
|
||||||
|
MkOpt ["--paths"] [] [BlodwenPaths]
|
||||||
|
(Just "Show paths"),
|
||||||
|
MkOpt ["--build"] ["package file"] (\f => [Package Build f])
|
||||||
|
(Just "Build modules/executable for the given package"),
|
||||||
|
MkOpt ["--install"] ["package file"] (\f => [Package Install f])
|
||||||
|
(Just "Install the given package"),
|
||||||
|
|
||||||
|
MkOpt ["--quiet", "-q"] [] [Quiet]
|
||||||
|
(Just "Quiet mode; display fewer messages"),
|
||||||
|
MkOpt ["--version", "-v"] [] [Version]
|
||||||
|
(Just "Display version string"),
|
||||||
|
MkOpt ["--help", "-h", "-?"] [] [Help]
|
||||||
|
(Just "Display help text")
|
||||||
|
]
|
||||||
|
|
||||||
|
optUsage : OptDesc -> String
|
||||||
|
optUsage d
|
||||||
|
= maybe "" -- Don't show anything if there's no help string (that means
|
||||||
|
-- it's an internal option)
|
||||||
|
(\h =>
|
||||||
|
let optshow = showSep "," (flags d) ++ " " ++
|
||||||
|
showSep " " (map (\x => "<" ++ x ++ ">") (argdescs d)) in
|
||||||
|
optshow ++ pack (List.replicate (minus 26 (length optshow)) ' ')
|
||||||
|
++ h ++ "\n") (help d)
|
||||||
|
where
|
||||||
|
showSep : String -> List String -> String
|
||||||
|
showSep sep [] = ""
|
||||||
|
showSep sep [x] = x
|
||||||
|
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
|
||||||
|
|
||||||
|
export
|
||||||
|
version : String
|
||||||
|
version = "0.1"
|
||||||
|
|
||||||
|
export
|
||||||
|
versionMsg : String
|
||||||
|
versionMsg = "Blodwen, a prototype successor to Idris, version " ++ version
|
||||||
|
|
||||||
|
export
|
||||||
|
usage : String
|
||||||
|
usage = versionMsg ++ "\n" ++
|
||||||
|
"Usage: blodwen [options] [input file]\n\n" ++
|
||||||
|
"Available options:\n" ++
|
||||||
|
concatMap (\u => " " ++ optUsage u) options
|
||||||
|
|
||||||
|
processArgs : String -> (args : List String) -> List String -> ActType args ->
|
||||||
|
Either String (List CLOpt, List String)
|
||||||
|
processArgs flag [] xs f = Right (f, xs)
|
||||||
|
processArgs flag (a :: as) [] f
|
||||||
|
= Left $ "Missing argument <" ++ a ++ "> for flag " ++ flag
|
||||||
|
processArgs flag (a :: as) (x :: xs) f
|
||||||
|
= processArgs flag as xs (f x)
|
||||||
|
|
||||||
|
matchFlag : (d : OptDesc) -> List String ->
|
||||||
|
Either String (Maybe (List CLOpt, List String))
|
||||||
|
matchFlag d [] = Right Nothing -- Nothing left to match
|
||||||
|
matchFlag d (x :: xs)
|
||||||
|
= if x `elem` flags d
|
||||||
|
then do args <- processArgs x (argdescs d) xs (action d)
|
||||||
|
Right (Just args)
|
||||||
|
else Right Nothing
|
||||||
|
|
||||||
|
findMatch : List OptDesc -> List String ->
|
||||||
|
Either String (List CLOpt, List String)
|
||||||
|
findMatch [] [] = Right ([], [])
|
||||||
|
findMatch [] (f :: args) = Right ([InputFile f], args)
|
||||||
|
findMatch (d :: ds) args
|
||||||
|
= case !(matchFlag d args) of
|
||||||
|
Nothing => findMatch ds args
|
||||||
|
Just res => Right res
|
||||||
|
|
||||||
|
parseOpts : List OptDesc -> List String -> Either String (List CLOpt)
|
||||||
|
parseOpts opts [] = Right []
|
||||||
|
parseOpts opts args
|
||||||
|
= do (cl, rest) <- findMatch opts args
|
||||||
|
cls <- assert_total (parseOpts opts rest) -- 'rest' smaller than 'args'
|
||||||
|
pure (cl ++ cls)
|
||||||
|
|
||||||
|
export
|
||||||
|
getOpts : List String -> Either String (List CLOpt)
|
||||||
|
getOpts opts = parseOpts options opts
|
||||||
|
|
||||||
|
|
||||||
|
export covering
|
||||||
|
getCmdOpts : IO (Either String (List CLOpt))
|
||||||
|
getCmdOpts = do (_ :: opts) <- getArgs
|
||||||
|
| pure (Left "Invalid command line")
|
||||||
|
pure $ getOpts opts
|
||||||
|
|
||||||
287
src/Idris/Package.idr
Normal file
287
src/Idris/Package.idr
Normal file
@ -0,0 +1,287 @@
|
|||||||
|
module Idris.Package
|
||||||
|
|
||||||
|
import Core.Context
|
||||||
|
import Core.Core
|
||||||
|
import Core.Directory
|
||||||
|
import Core.Options
|
||||||
|
import Core.Unify
|
||||||
|
|
||||||
|
import Idris.CommandLine
|
||||||
|
import Idris.ModTree
|
||||||
|
import Idris.ProcessIdr
|
||||||
|
import Idris.REPLOpts
|
||||||
|
import Idris.SetOptions
|
||||||
|
import Idris.Syntax
|
||||||
|
import Parser.Lexer
|
||||||
|
import Parser.Support
|
||||||
|
import Utils.Binary
|
||||||
|
|
||||||
|
import System
|
||||||
|
import Text.Parser
|
||||||
|
|
||||||
|
%default covering
|
||||||
|
|
||||||
|
record PkgDesc where
|
||||||
|
constructor MkPkgDesc
|
||||||
|
name : String
|
||||||
|
version : String
|
||||||
|
authors : String
|
||||||
|
depends : List String -- packages to add to search path
|
||||||
|
modules : List (List String, String) -- modules to install (namespace, filename)
|
||||||
|
mainmod : Maybe (List String, String) -- main file (i.e. file to load at REPL)
|
||||||
|
executable : Maybe String -- name of executable
|
||||||
|
options : Maybe (FC, String)
|
||||||
|
prebuild : Maybe (FC, String) -- Script to run before building
|
||||||
|
postbuild : Maybe (FC, String) -- Script to run after building
|
||||||
|
preinstall : Maybe (FC, String) -- Script to run after building, before installing
|
||||||
|
postinstall : Maybe (FC, String) -- Script to run after installing
|
||||||
|
|
||||||
|
Show PkgDesc where
|
||||||
|
show pkg = "Package: " ++ name pkg ++ "\n" ++
|
||||||
|
"Version: " ++ version pkg ++ "\n" ++
|
||||||
|
"Authors: " ++ authors pkg ++ "\n" ++
|
||||||
|
"Depends: " ++ show (depends pkg) ++ "\n" ++
|
||||||
|
"Modules: " ++ show (map snd (modules pkg)) ++ "\n" ++
|
||||||
|
maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++
|
||||||
|
maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++
|
||||||
|
maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++
|
||||||
|
maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++
|
||||||
|
maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++
|
||||||
|
maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++
|
||||||
|
maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg)
|
||||||
|
|
||||||
|
initPkgDesc : String -> PkgDesc
|
||||||
|
initPkgDesc pname
|
||||||
|
= MkPkgDesc pname "0" "Anonymous" [] []
|
||||||
|
Nothing Nothing Nothing Nothing Nothing Nothing Nothing
|
||||||
|
|
||||||
|
data DescField : Type where
|
||||||
|
PVersion : FC -> String -> DescField
|
||||||
|
PAuthors : FC -> String -> DescField
|
||||||
|
PDepends : List String -> DescField
|
||||||
|
PModules : List (FC, List String) -> DescField
|
||||||
|
PMainMod : FC -> List String -> DescField
|
||||||
|
PExec : String -> DescField
|
||||||
|
POpts : FC -> String -> DescField
|
||||||
|
PPrebuild : FC -> String -> DescField
|
||||||
|
PPostbuild : FC -> String -> DescField
|
||||||
|
PPreinstall : FC -> String -> DescField
|
||||||
|
PPostinstall : FC -> String -> DescField
|
||||||
|
|
||||||
|
field : String -> Rule DescField
|
||||||
|
field fname
|
||||||
|
= strField PVersion "version"
|
||||||
|
<|> strField PAuthors "authors"
|
||||||
|
<|> strField POpts "options"
|
||||||
|
<|> strField POpts "opts"
|
||||||
|
<|> strField PPrebuild "prebuild"
|
||||||
|
<|> strField PPostbuild "postbuild"
|
||||||
|
<|> strField PPreinstall "preinstall"
|
||||||
|
<|> strField PPostinstall "postinstall"
|
||||||
|
<|> do exactIdent "depends"; symbol "="
|
||||||
|
ds <- sepBy1 (symbol ",") unqualifiedName
|
||||||
|
pure (PDepends ds)
|
||||||
|
<|> do exactIdent "modules"; symbol "="
|
||||||
|
ms <- sepBy1 (symbol ",")
|
||||||
|
(do start <- location
|
||||||
|
ns <- namespace_
|
||||||
|
end <- location
|
||||||
|
pure (MkFC fname start end, ns))
|
||||||
|
pure (PModules ms)
|
||||||
|
<|> do exactIdent "main"; symbol "="
|
||||||
|
start <- location
|
||||||
|
m <- namespace_
|
||||||
|
end <- location
|
||||||
|
pure (PMainMod (MkFC fname start end) m)
|
||||||
|
<|> do exactIdent "executable"; symbol "="
|
||||||
|
e <- unqualifiedName
|
||||||
|
pure (PExec e)
|
||||||
|
where
|
||||||
|
getStr : (FC -> String -> DescField) -> FC ->
|
||||||
|
String -> Constant -> EmptyRule DescField
|
||||||
|
getStr p fc fld (Str s) = pure (p fc s)
|
||||||
|
getStr p fc fld _ = fail $ fld ++ " field must be a string"
|
||||||
|
|
||||||
|
strField : (FC -> String -> DescField) -> String -> Rule DescField
|
||||||
|
strField p f
|
||||||
|
= do start <- location
|
||||||
|
exactIdent f
|
||||||
|
symbol "="
|
||||||
|
c <- constant
|
||||||
|
end <- location
|
||||||
|
getStr p (MkFC fname start end) f c
|
||||||
|
|
||||||
|
parsePkgDesc : String -> Rule (String, List DescField)
|
||||||
|
parsePkgDesc fname
|
||||||
|
= do exactIdent "package"
|
||||||
|
name <- unqualifiedName
|
||||||
|
fields <- many (field fname)
|
||||||
|
pure (name, fields)
|
||||||
|
|
||||||
|
addField : {auto c : Ref Ctxt Defs} ->
|
||||||
|
DescField -> PkgDesc -> Core PkgDesc
|
||||||
|
addField (PVersion fc n) pkg = pure (record { version = n } pkg)
|
||||||
|
addField (PAuthors fc a) pkg = pure (record { authors = a } pkg)
|
||||||
|
addField (PDepends ds) pkg = pure (record { depends = ds } pkg)
|
||||||
|
addField (PModules ms) pkg
|
||||||
|
= pure (record { modules = !(traverse toSource ms) } pkg)
|
||||||
|
where
|
||||||
|
toSource : (FC, List String) -> Core (List String, String)
|
||||||
|
toSource (loc, ns) = pure (ns, !(nsToSource loc ns))
|
||||||
|
addField (PMainMod loc n) pkg
|
||||||
|
= pure (record { mainmod = Just (n, !(nsToSource loc n)) } pkg)
|
||||||
|
addField (PExec e) pkg = pure (record { executable = Just e } pkg)
|
||||||
|
addField (POpts fc e) pkg = pure (record { options = Just (fc, e) } pkg)
|
||||||
|
addField (PPrebuild fc e) pkg = pure (record { prebuild = Just (fc, e) } pkg)
|
||||||
|
addField (PPostbuild fc e) pkg = pure (record { postbuild = Just (fc, e) } pkg)
|
||||||
|
addField (PPreinstall fc e) pkg = pure (record { preinstall = Just (fc, e) } pkg)
|
||||||
|
addField (PPostinstall fc e) pkg = pure (record { postinstall = Just (fc, e) } pkg)
|
||||||
|
|
||||||
|
addFields : {auto c : Ref Ctxt Defs} ->
|
||||||
|
List DescField -> PkgDesc -> Core PkgDesc
|
||||||
|
addFields [] desc = pure desc
|
||||||
|
addFields (x :: xs) desc = addFields xs !(addField x desc)
|
||||||
|
|
||||||
|
runScript : Maybe (FC, String) -> Core ()
|
||||||
|
runScript Nothing = pure ()
|
||||||
|
runScript (Just (fc, s))
|
||||||
|
= do res <- coreLift $ system s
|
||||||
|
when (res /= 0) $
|
||||||
|
throw (GenericMsg fc "Script failed")
|
||||||
|
|
||||||
|
addDeps : {auto c : Ref Ctxt Defs} ->
|
||||||
|
PkgDesc -> Core ()
|
||||||
|
addDeps pkg
|
||||||
|
= do defs <- get Ctxt
|
||||||
|
traverse addPkgDir (depends pkg)
|
||||||
|
pure ()
|
||||||
|
|
||||||
|
processOptions : {auto c : Ref Ctxt Defs} ->
|
||||||
|
{auto o : Ref ROpts REPLOpts} ->
|
||||||
|
Maybe (FC, String) -> Core ()
|
||||||
|
processOptions Nothing = pure ()
|
||||||
|
processOptions (Just (fc, opts))
|
||||||
|
= do let Right clopts = getOpts (words opts)
|
||||||
|
| Left err => throw (GenericMsg fc err)
|
||||||
|
preOptions clopts
|
||||||
|
|
||||||
|
build : {auto c : Ref Ctxt Defs} ->
|
||||||
|
{auto s : Ref Syn SyntaxInfo} ->
|
||||||
|
{auto o : Ref ROpts REPLOpts} ->
|
||||||
|
PkgDesc -> Core (List Error)
|
||||||
|
build pkg
|
||||||
|
= do defs <- get Ctxt
|
||||||
|
addDeps pkg
|
||||||
|
processOptions (options pkg)
|
||||||
|
runScript (prebuild pkg)
|
||||||
|
let toBuild = maybe (map snd (modules pkg))
|
||||||
|
(\m => snd m :: map snd (modules pkg))
|
||||||
|
(mainmod pkg)
|
||||||
|
[] <- buildAll toBuild
|
||||||
|
| errs => pure errs
|
||||||
|
runScript (postbuild pkg)
|
||||||
|
pure []
|
||||||
|
|
||||||
|
copyFile : String -> String -> IO (Either FileError ())
|
||||||
|
copyFile src dest
|
||||||
|
= do Right buf <- readFromFile src
|
||||||
|
| Left err => pure (Left err)
|
||||||
|
writeToFile dest buf
|
||||||
|
|
||||||
|
installFrom : {auto c : Ref Ctxt Defs} ->
|
||||||
|
String -> String -> String -> List String -> Core ()
|
||||||
|
installFrom _ _ _ [] = pure ()
|
||||||
|
installFrom pname builddir destdir ns@(m :: dns)
|
||||||
|
= do defs <- get Ctxt
|
||||||
|
let modname = showSep "." (reverse ns)
|
||||||
|
let ttcfile = showSep "/" (reverse ns)
|
||||||
|
let ttcPath = builddir ++ dirSep ++ ttcfile ++ ".ttc"
|
||||||
|
let destPath = destdir ++ dirSep ++ showSep "/" (reverse dns)
|
||||||
|
let destFile = destdir ++ dirSep ++ ttcfile ++ ".ttc"
|
||||||
|
Right _ <- coreLift $ mkdirs (reverse dns)
|
||||||
|
| Left err => throw (FileErr pname err)
|
||||||
|
coreLift $ putStrLn $ "Installing " ++ ttcPath ++ " to " ++ destPath
|
||||||
|
Right _ <- coreLift $ copyFile ttcPath destFile
|
||||||
|
| Left err => throw (FileErr pname err)
|
||||||
|
pure ()
|
||||||
|
|
||||||
|
-- Install all the built modules in prefix/package/
|
||||||
|
-- We've already built and checked for success, so if any don't exist that's
|
||||||
|
-- an internal error.
|
||||||
|
install : {auto c : Ref Ctxt Defs} ->
|
||||||
|
{auto o : Ref ROpts REPLOpts} ->
|
||||||
|
PkgDesc -> Core ()
|
||||||
|
install pkg
|
||||||
|
= do defs <- get Ctxt
|
||||||
|
let build = build_dir (dirs (options defs))
|
||||||
|
runScript (preinstall pkg)
|
||||||
|
let toInstall = maybe (map fst (modules pkg))
|
||||||
|
(\m => fst m :: map fst (modules pkg))
|
||||||
|
(mainmod pkg)
|
||||||
|
srcdir <- coreLift currentDir
|
||||||
|
-- Make the package installation directory
|
||||||
|
let installPrefix = dir_prefix (dirs (options defs)) ++ dirSep ++ "blodwen"
|
||||||
|
True <- coreLift $ changeDir installPrefix
|
||||||
|
| False => throw (FileErr (name pkg) FileReadError)
|
||||||
|
Right _ <- coreLift $ mkdirs [name pkg]
|
||||||
|
| Left err => throw (FileErr (name pkg) err)
|
||||||
|
True <- coreLift $ changeDir (name pkg)
|
||||||
|
| False => throw (FileErr (name pkg) FileReadError)
|
||||||
|
|
||||||
|
-- We're in that directory now, so copy the files from
|
||||||
|
-- srcdir/build into it
|
||||||
|
traverse (installFrom (name pkg)
|
||||||
|
(srcdir ++ dirSep ++ build)
|
||||||
|
(installPrefix ++ dirSep ++ name pkg)) toInstall
|
||||||
|
coreLift $ changeDir srcdir
|
||||||
|
runScript (postinstall pkg)
|
||||||
|
|
||||||
|
-- Just load the 'Main' module, if it exists, which will involve building
|
||||||
|
-- it if necessary
|
||||||
|
runRepl : {auto c : Ref Ctxt Defs} ->
|
||||||
|
{auto o : Ref ROpts REPLOpts} ->
|
||||||
|
PkgDesc -> Core ()
|
||||||
|
runRepl pkg
|
||||||
|
= do addDeps pkg
|
||||||
|
processOptions (options pkg)
|
||||||
|
throw (InternalError "Not implemented")
|
||||||
|
|
||||||
|
processPackage : {auto c : Ref Ctxt Defs} ->
|
||||||
|
{auto s : Ref Syn SyntaxInfo} ->
|
||||||
|
{auto o : Ref ROpts REPLOpts} ->
|
||||||
|
PkgCommand -> String -> Core ()
|
||||||
|
processPackage cmd file
|
||||||
|
= do Right (pname, fs) <- coreLift $ parseFile file
|
||||||
|
(do desc <- parsePkgDesc file
|
||||||
|
eoi
|
||||||
|
pure desc)
|
||||||
|
| Left err => throw (ParseFail (getParseErrorLoc file err) err)
|
||||||
|
pkg <- addFields fs (initPkgDesc pname)
|
||||||
|
case cmd of
|
||||||
|
Build => do [] <- build pkg
|
||||||
|
| errs => coreLift (exit 1)
|
||||||
|
pure ()
|
||||||
|
Install => do [] <- build pkg
|
||||||
|
| errs => coreLift (exit 1)
|
||||||
|
install pkg
|
||||||
|
REPL => runRepl pkg
|
||||||
|
|
||||||
|
rejectPackageOpts : List CLOpt -> Core Bool
|
||||||
|
rejectPackageOpts (Package cmd f :: _)
|
||||||
|
= do coreLift $ putStrLn ("Package commands (--build, --install --repl) must be the only option given")
|
||||||
|
pure True -- Done, quit here
|
||||||
|
rejectPackageOpts (_ :: xs) = rejectPackageOpts xs
|
||||||
|
rejectPackageOpts [] = pure False
|
||||||
|
|
||||||
|
-- If there's a package option, it must be the only option, so reject if
|
||||||
|
-- it's not
|
||||||
|
export
|
||||||
|
processPackageOpts : {auto c : Ref Ctxt Defs} ->
|
||||||
|
{auto s : Ref Syn SyntaxInfo} ->
|
||||||
|
{auto o : Ref ROpts REPLOpts} ->
|
||||||
|
List CLOpt -> Core Bool
|
||||||
|
processPackageOpts [Package cmd f]
|
||||||
|
= do processPackage cmd f
|
||||||
|
pure True
|
||||||
|
processPackageOpts opts = rejectPackageOpts opts
|
||||||
|
|
||||||
79
src/Idris/SetOptions.idr
Normal file
79
src/Idris/SetOptions.idr
Normal file
@ -0,0 +1,79 @@
|
|||||||
|
module Idris.SetOptions
|
||||||
|
|
||||||
|
import Core.Context
|
||||||
|
import Core.Directory
|
||||||
|
import Core.Metadata
|
||||||
|
import Core.Options
|
||||||
|
import Core.Unify
|
||||||
|
|
||||||
|
import Idris.CommandLine
|
||||||
|
import Idris.REPL
|
||||||
|
import Idris.Syntax
|
||||||
|
|
||||||
|
import System
|
||||||
|
|
||||||
|
-- TODO: Version numbers on dependencies
|
||||||
|
export
|
||||||
|
addPkgDir : {auto c : Ref Ctxt Defs} ->
|
||||||
|
String -> Core ()
|
||||||
|
addPkgDir p
|
||||||
|
= do defs <- get Ctxt
|
||||||
|
addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++
|
||||||
|
"blodwen" ++ dirSep ++ p)
|
||||||
|
|
||||||
|
-- Options to be processed before type checking
|
||||||
|
export
|
||||||
|
preOptions : {auto c : Ref Ctxt Defs} ->
|
||||||
|
{auto o : Ref ROpts REPLOpts} ->
|
||||||
|
List CLOpt -> Core ()
|
||||||
|
preOptions [] = pure ()
|
||||||
|
preOptions (Quiet :: opts)
|
||||||
|
= do setOutput (REPL True)
|
||||||
|
preOptions opts
|
||||||
|
preOptions (NoPrelude :: opts)
|
||||||
|
= do setSession (record { noprelude = True } !getSession)
|
||||||
|
preOptions opts
|
||||||
|
preOptions (SetCG e :: opts)
|
||||||
|
= case getCG e of
|
||||||
|
Just cg => do setCG cg
|
||||||
|
preOptions opts
|
||||||
|
Nothing =>
|
||||||
|
do coreLift $ putStrLn "No such code generator"
|
||||||
|
coreLift $ putStrLn $ "Code generators available: " ++
|
||||||
|
showSep ", " (map fst availableCGs)
|
||||||
|
coreLift $ exit 1
|
||||||
|
preOptions (PkgPath p :: opts)
|
||||||
|
= do addPkgDir p
|
||||||
|
preOptions opts
|
||||||
|
preOptions (_ :: opts) = preOptions opts
|
||||||
|
|
||||||
|
-- Options to be processed after type checking. Returns whether execution
|
||||||
|
-- should continue (i.e., whether to start a REPL)
|
||||||
|
export
|
||||||
|
postOptions : {auto c : Ref Ctxt Defs} ->
|
||||||
|
{auto u : Ref UST UState} ->
|
||||||
|
{auto s : Ref Syn SyntaxInfo} ->
|
||||||
|
{auto m : Ref MD Metadata} ->
|
||||||
|
List CLOpt -> Core Bool
|
||||||
|
postOptions [] = pure True
|
||||||
|
postOptions (ExecFn str :: rest)
|
||||||
|
= do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str))
|
||||||
|
postOptions rest
|
||||||
|
pure False
|
||||||
|
postOptions (CheckOnly :: rest)
|
||||||
|
= do postOptions rest
|
||||||
|
pure False
|
||||||
|
postOptions (_ :: rest) = postOptions rest
|
||||||
|
|
||||||
|
export
|
||||||
|
ideMode : List CLOpt -> Bool
|
||||||
|
ideMode [] = False
|
||||||
|
ideMode (IdeMode :: _) = True
|
||||||
|
ideMode (_ :: xs) = ideMode xs
|
||||||
|
|
||||||
|
export
|
||||||
|
ideModeSocket : List CLOpt -> Bool
|
||||||
|
ideModeSocket [] = False
|
||||||
|
ideModeSocket (IdeModeSocket :: _) = True
|
||||||
|
ideModeSocket (_ :: xs) = ideModeSocket xs
|
||||||
|
|
||||||
@ -43,7 +43,10 @@ modules =
|
|||||||
Data.NameMap,
|
Data.NameMap,
|
||||||
Data.StringMap,
|
Data.StringMap,
|
||||||
|
|
||||||
|
Idris.CommandLine,
|
||||||
Idris.Desugar,
|
Idris.Desugar,
|
||||||
|
Idris.Elab.Implementation,
|
||||||
|
Idris.Elab.Interface,
|
||||||
Idris.Error,
|
Idris.Error,
|
||||||
Idris.IDEMode.CaseSplit,
|
Idris.IDEMode.CaseSplit,
|
||||||
Idris.IDEMode.Commands,
|
Idris.IDEMode.Commands,
|
||||||
@ -51,12 +54,14 @@ modules =
|
|||||||
Idris.IDEMode.Parser,
|
Idris.IDEMode.Parser,
|
||||||
Idris.IDEMode.TokenLine,
|
Idris.IDEMode.TokenLine,
|
||||||
Idris.ModTree,
|
Idris.ModTree,
|
||||||
|
Idris.Package,
|
||||||
Idris.Parser,
|
Idris.Parser,
|
||||||
Idris.ProcessIdr,
|
Idris.ProcessIdr,
|
||||||
Idris.REPL,
|
Idris.REPL,
|
||||||
Idris.REPLCommon,
|
Idris.REPLCommon,
|
||||||
Idris.REPLOpts,
|
Idris.REPLOpts,
|
||||||
Idris.Resugar,
|
Idris.Resugar,
|
||||||
|
Idris.SetOptions,
|
||||||
Idris.Socket,
|
Idris.Socket,
|
||||||
Idris.Socket.Data,
|
Idris.Socket.Data,
|
||||||
Idris.Socket.Raw,
|
Idris.Socket.Raw,
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user