diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr new file mode 100644 index 0000000..d5ed807 --- /dev/null +++ b/src/Idris/CommandLine.idr @@ -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 + diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr new file mode 100644 index 0000000..89a8ccb --- /dev/null +++ b/src/Idris/Package.idr @@ -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 + diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr new file mode 100644 index 0000000..b1c053b --- /dev/null +++ b/src/Idris/SetOptions.idr @@ -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 + diff --git a/yaffle.ipkg b/yaffle.ipkg index 60d3f3d..6770e1c 100644 --- a/yaffle.ipkg +++ b/yaffle.ipkg @@ -43,7 +43,10 @@ modules = Data.NameMap, Data.StringMap, + Idris.CommandLine, Idris.Desugar, + Idris.Elab.Implementation, + Idris.Elab.Interface, Idris.Error, Idris.IDEMode.CaseSplit, Idris.IDEMode.Commands, @@ -51,12 +54,14 @@ modules = Idris.IDEMode.Parser, Idris.IDEMode.TokenLine, Idris.ModTree, + Idris.Package, Idris.Parser, Idris.ProcessIdr, Idris.REPL, Idris.REPLCommon, Idris.REPLOpts, Idris.Resugar, + Idris.SetOptions, Idris.Socket, Idris.Socket.Data, Idris.Socket.Raw,