idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 02:07:25 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #485 from melted/directive_arg

Browse Source 
Add `--directive` cli option
This commit is contained in:
Niklas Larsson 2020-07-23 14:50:53 +02:00 committed by GitHub
commit 57f89ccd9a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 52 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/Core/Context.idr
View File

@ -1719,7 +1719,8 @@ getDirectives : {auto c : Ref Ctxt Defs} ->
CG -> Core (List String)
getDirectives cg
= do defs <- get Ctxt
pure (mapMaybe getDir (cgdirectives defs))
pure $ defs.options.session.directives ++
mapMaybe getDir (cgdirectives defs)
where
getDir : (CG, String) -> Maybe String
getDir (x', str) = if cg == x' then Just str else Nothing

6
src/Core/Options.idr
View File

@ -123,6 +123,7 @@ record Session where
nobanner : Bool
findipkg : Bool
codegen : CG
directives : List String
logLevel : Nat
logTimings : Bool
debugElabCheck : Bool -- do conversion check to verify results of elaborator
@ -174,8 +175,9 @@ defaultPPrint = MkPPOpts False True False
export
defaultSession : Session
defaultSession = MkSessionOpts False False False Chez 0 False False
Nothing Nothing Nothing Nothing
defaultSession = MkSessionOpts False False False Chez [] 0
False False Nothing Nothing
Nothing Nothing
export
defaultElab : ElabDirectives

4
src/Idris/CommandLine.idr
View File

@ -51,6 +51,8 @@ data CLOpt
ExecFn String |
||| Use a specific code generator
SetCG String |
||| Pass a directive to the code generator
Directive String |
||| Don't implicitly import Prelude
NoPrelude |
||| Set source directory
@ -160,6 +162,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
(Just "Don't implicitly import Prelude"),
MkOpt ["--codegen", "--cg"] [Required "backend"] (\f => [SetCG f])
(Just $ "Set code generator " ++ showDefault (codegen defaultSession)),
MkOpt ["--directive"] [Required "directive"] (\d => [Directive d])
(Just $ "Pass a directive to the current code generator"),
MkOpt ["--package", "-p"] [Required "package"] (\f => [PkgPath f])
(Just "Add a package as a dependency"),
MkOpt ["--source-dir"] [Required "dir"] (\d => [SourceDir d])

22
src/Idris/IDEMode/Commands.idr
View File

@ -34,6 +34,7 @@ data IDECommand
| MakeCase Integer String
| MakeWith Integer String
| DocsFor String (Maybe DocMode)
| Directive String
| Apropos String
| Metavariables Integer
| WhoCalls String
@ -75,7 +76,7 @@ getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, StringAtom n])
= Just $ CaseSplit l 0 n
getIDECommand (SExpList [SymbolAtom "add-clause", IntegerAtom l, StringAtom n])
= Just $ AddClause l n
getIDECommand (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
getIDECommand (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
= Just $ AddMissing line n
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n])
= Just $ ExprSearch l n [] False
@ -105,9 +106,11 @@ getIDECommand (SExpList (SymbolAtom "docs-for" :: StringAtom n :: modeTail))
[SymbolAtom "overview"] => Just $ Just Overview
[SymbolAtom "full" ] => Just $ Just Full
_ => Nothing
Just $ DocsFor n modeOpt
Just $ DocsFor n modeOpt
getIDECommand (SExpList [SymbolAtom "apropos", StringAtom n])
= Just $ Apropos n
getIDECommand (SExpList [SymbolAtom "directive", StringAtom n])
= Just $ Directive n
getIDECommand (SExpList [SymbolAtom "metavariables", IntegerAtom n])
= Just $ Metavariables n
getIDECommand (SExpList [SymbolAtom "who-calls", StringAtom n])
@ -116,13 +119,13 @@ getIDECommand (SExpList [SymbolAtom "calls-who", StringAtom n])
= Just $ CallsWho n
getIDECommand (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
= Just $ BrowseNamespace ns
getIDECommand (SExpList [SymbolAtom "normalise-term", StringAtom tm])
getIDECommand (SExpList [SymbolAtom "normalise-term", StringAtom tm])
= Just $ NormaliseTerm tm
getIDECommand (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
= Just $ ShowTermImplicits tm
getIDECommand (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
= Just $ HideTermImplicits tm
getIDECommand (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
getIDECommand (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
= Just $ ElaborateTerm tm
getIDECommand (SExpList [SymbolAtom "print-definition", StringAtom n])
= Just $ PrintDefinition n
@ -151,7 +154,7 @@ putIDECommand (GenerateDef line n) = (SExpList [SymbolAtom "generate-
putIDECommand (MakeLemma line n) = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n])
putIDECommand (MakeCase line n) = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])
putIDECommand (MakeWith line n) = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])
putIDECommand (DocsFor n modeOpt) = let modeTail = case modeOpt of
putIDECommand (DocsFor n modeOpt) = let modeTail = case modeOpt of
Nothing => []
Just Overview => [SymbolAtom "overview"]
Just Full => [SymbolAtom "full"] in
@ -161,12 +164,13 @@ putIDECommand (Metavariables n) = (SExpList [SymbolAtom "metavaria
putIDECommand (WhoCalls n) = (SExpList [SymbolAtom "who-calls", StringAtom n])
putIDECommand (CallsWho n) = (SExpList [SymbolAtom "calls-who", StringAtom n])
putIDECommand (BrowseNamespace ns) = (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
putIDECommand (NormaliseTerm tm) = (SExpList [SymbolAtom "normalise-term", StringAtom tm])
putIDECommand (ShowTermImplicits tm) = (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
putIDECommand (HideTermImplicits tm) = (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
putIDECommand (ElaborateTerm tm) = (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
putIDECommand (NormaliseTerm tm) = (SExpList [SymbolAtom "normalise-term", StringAtom tm])
putIDECommand (ShowTermImplicits tm) = (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
putIDECommand (HideTermImplicits tm) = (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
putIDECommand (ElaborateTerm tm) = (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
putIDECommand (PrintDefinition n) = (SExpList [SymbolAtom "print-definition", StringAtom n])
putIDECommand (ReplCompletions n) = (SExpList [SymbolAtom "repl-completions", StringAtom n])
putIDECommand (Directive n) = (SExpList [SymbolAtom "directive", StringAtom n])
putIDECommand GetOptions = (SExpList [SymbolAtom "get-options"])
putIDECommand Version = SymbolAtom "version"

3
src/Idris/IDEMode/REPL.idr
View File

@ -182,6 +182,9 @@ process (DocsFor n modeOpt)
process (Apropos n)
= do todoCmd "apropros"
pure $ REPL $ Printed []
process (Directive n)
= do todoCmd "directive"
pure $ REPL $ Printed []
process (WhoCalls n)
= do todoCmd "who-calls"
pure $ NameList []

18
src/Idris/Parser.idr
View File

@ -1764,6 +1764,9 @@ data CmdArg : Type where
||| The command takes a module.
ModuleArg : CmdArg
||| The command takes a string
StringArg : CmdArg
||| The command takes multiple arguments.
Args : List CmdArg -> CmdArg
@ -1777,6 +1780,7 @@ Show CmdArg where
show OptionArg = "<option>"
show FileArg = "<file>"
show ModuleArg = "<module>"
show StringArg = "<module>"
show (Args args) = showSep " " (map show args)
export
@ -1826,6 +1830,19 @@ nameArgCmd parseCmd command doc = (names, NameArg, doc, parse)
n <- name
pure (command n)
stringArgCmd : ParseCmd -> (String -> REPLCmd) -> String -> CommandDefinition
stringArgCmd parseCmd command doc = (names, StringArg, doc, parse)
where
names : List String
names = extractNames parseCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
s <- strLit
pure (command s)
moduleArgCmd : ParseCmd -> (List String -> REPLCmd) -> String -> CommandDefinition
moduleArgCmd parseCmd command doc = (names, ModuleArg, doc, parse)
where
@ -1918,6 +1935,7 @@ parserCommandsForHelp =
, optArgCmd (ParseIdentCmd "unset") SetOpt False "Unset an option"
, compileArgsCmd (ParseREPLCmd ["c", "compile"]) Compile "Compile to an executable"
, exprArgCmd (ParseIdentCmd "exec") Exec "Compile to an executable and run"
, stringArgCmd (ParseIdentCmd "directive") CGDirective "Set a codegen-specific directive"
, noArgCmd (ParseREPLCmd ["r", "reload"]) Reload "Reload current file"
, noArgCmd (ParseREPLCmd ["e", "edit"]) Edit "Edit current file using $EDITOR or $VISUAL"
, nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing "Show missing clauses"

3
src/Idris/REPL.idr
View File

@ -727,6 +727,9 @@ process (Editing cmd)
res <- processEdit cmd
setPPrint ppopts
pure $ Edited res
process (CGDirective str)
= do setSession (record { directives $= (str::) } !getSession)
pure Done
process Quit
= pure Exited
process NOP

3
src/Idris/SetOptions.idr
View File

@ -71,6 +71,9 @@ preOptions (SetCG e :: opts)
coreLift $ putStrLn $ "Code generators available: " ++
showSep ", " (map fst (availableCGs (options defs)))
coreLift $ exitWith (ExitFailure 1)
preOptions (Directive d :: opts)
= do setSession (record { directives $= (d::) } !getSession)
preOptions opts
preOptions (PkgPath p :: opts)
= do addPkgDir p
preOptions opts

3
src/Idris/Syntax.idr
View File

@ -392,7 +392,7 @@ data EditCmd : Type where
public export
data REPLCmd : Type where
NewDefn : List PDecl -> REPLCmd
NewDefn : List PDecl -> REPLCmd
Eval : PTerm -> REPLCmd
Check : PTerm -> REPLCmd
PrintDef : Name -> REPLCmd
@ -407,6 +407,7 @@ data REPLCmd : Type where
DebugInfo : Name -> REPLCmd
SetOpt : REPLOpt -> REPLCmd
GetOpts : REPLCmd
CGDirective : String -> REPLCmd
CD : String -> REPLCmd
CWD: REPLCmd
Missing : Name -> REPLCmd