From 7e0bca23fdcbcd01f59bd98f29a90c2f4880c50f Mon Sep 17 00:00:00 2001
From: Niklas Larsson <niklas@mm.st>
Date: Sat, 18 Jul 2020 17:10:13 +0200
Subject: [PATCH] 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           |  3 ++-
 src/Core/Options.idr           |  6 ++++--
 src/Idris/CommandLine.idr      |  4 ++++
 src/Idris/IDEMode/Commands.idr | 22 +++++++++++++---------
 src/Idris/IDEMode/REPL.idr     |  3 +++
 src/Idris/Parser.idr           | 18 ++++++++++++++++++
 src/Idris/REPL.idr             |  3 +++
 src/Idris/SetOptions.idr       |  3 +++
 src/Idris/Syntax.idr           |  3 ++-
 9 files changed, 52 insertions(+), 13 deletions(-)

diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index a7ddfd95f..546833550 100644
--- a/src/Core/Context.idr
+++ b/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
diff --git a/src/Core/Options.idr b/src/Core/Options.idr
index 777c9b137..1d1ace735 100644
--- a/src/Core/Options.idr
+++ b/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
diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr
index 2b5cfad93..2bdcd7c51 100644
--- a/src/Idris/CommandLine.idr
+++ b/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])
diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr
index 6d6c0b3ca..ebccc8097 100644
--- a/src/Idris/IDEMode/Commands.idr
+++ b/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
@@ -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"
 
diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr
index cfafc45db..6fa6fd9d3 100644
--- a/src/Idris/IDEMode/REPL.idr
+++ b/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 []
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 0dd5de298..a1575a100 100644
--- a/src/Idris/Parser.idr
+++ b/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"
diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr
index cc2010090..80470634d 100644
--- a/src/Idris/REPL.idr
+++ b/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
diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr
index 7b0ed9fbd..d1de37335 100644
--- a/src/Idris/SetOptions.idr
+++ b/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
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index 25ef189df..34903d131 100644
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@@ -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