Add --directive cli option

It sends a codegen directive to the current codegen. It's useful
for sending options you don't want to hard code in the source. Examples
include enabling profiling or setting a target.

src/Core/Context.idr

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

src/Core/Options.idr

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

src/Idris/CommandLine.idr

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

src/Idris/IDEMode/Commands.idr

@@ -34,6 +34,7 @@ data IDECommand
      | MakeCase Integer String
      | MakeWith Integer String
      | DocsFor String (Maybe DocMode)
+     | Directive String
      | Apropos String
      | Metavariables Integer
      | WhoCalls String
@@ -108,6 +109,8 @@ getIDECommand (SExpList (SymbolAtom "docs-for" ::  StringAtom n :: modeTail))
          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])
@@ -167,6 +170,7 @@ putIDECommand (HideTermImplicits tm)          = (SExpList [SymbolAtom "hide-term
 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"
 

src/Idris/IDEMode/REPL.idr

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

src/Idris/Parser.idr

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

src/Idris/REPL.idr

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

src/Idris/SetOptions.idr

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

src/Idris/Syntax.idr

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