From bfbe974254ce88052bb01fb5f443379f5d4cfd30 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Tue, 13 Jul 2021 17:52:40 +0200
Subject: [PATCH] [ doc ] Add topics (#1498) for pragmas. Implements `--help
 pragma`.

This adds the ability to do `idris2 --help pragma` and get a list of the
various pragmas and their options, similar to `idris2 --help logging`.
---
 src/Idris/CommandLine.idr | 10 +++++---
 src/Idris/Driver.idr      |  3 +++
 src/Idris/Syntax.idr      | 51 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 60 insertions(+), 4 deletions(-)

diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr
index 6fa0e8c66..a326afbf9 100644
--- a/src/Idris/CommandLine.idr
+++ b/src/Idris/CommandLine.idr
@@ -51,12 +51,14 @@ Show DirCommand where
 ||| Help topics
 public export
 data HelpTopic
-  =
-    ||| Interactive debugging topics
-   HelpLogging
+  = ||| Interactive debugging topics
+    HelpLogging
+  | ||| The various pragmas
+    HelpPragma
 
 recogniseHelpTopic : String -> Maybe HelpTopic
-recogniseHelpTopic "logging" = pure HelpLogging
+recogniseHelpTopic "logging"   = pure HelpLogging
+recogniseHelpTopic "pragma" = pure HelpPragma
 recogniseHelpTopic _ = Nothing
 
 ||| CLOpt - possible command line options
diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr
index 5609b7772..868d7d672 100644
--- a/src/Idris/Driver.idr
+++ b/src/Idris/Driver.idr
@@ -265,6 +265,9 @@ quitOpts (Help Nothing :: _)
 quitOpts (Help (Just HelpLogging) :: _)
     = do putStrLn helpTopics
          pure False
+quitOpts (Help (Just HelpPragma) :: _)
+    = do putStrLn pragmaTopics
+         pure False
 quitOpts (ShowPrefix :: _)
     = do putStrLn yprefix
          pure False
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index 44dfa31c8..879c45a50 100644
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@@ -20,6 +20,7 @@ import Libraries.Data.String.Extra
 import Libraries.Data.StringMap
 import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Text.PrettyPrint.Prettyprinter.Render.String
 
 import Parser.Lexer.Source
 
@@ -269,6 +270,56 @@ mutual
        NFMetavarThreshold : Nat -> Directive
        SearchTimeout : Integer -> Directive
 
+  directiveList : List Directive
+  directiveList =
+      [ (Hide (UN "")), (Logging Nothing), (LazyOn False)
+      , (UnboundImplicits False), (AmbigDepth 0)
+      , (PairNames (UN "") (UN "") (UN "")), (RewriteName (UN "") (UN ""))
+      , (PrimInteger (UN "")), (PrimString (UN "")), (PrimChar (UN ""))
+      , (PrimDouble (UN "")), (CGAction "" ""), (Names (UN "") [])
+      , (StartExpr (PRef EmptyFC (UN ""))), (Overloadable (UN ""))
+      , (Extension ElabReflection), (DefaultTotality PartialOK)
+      , (PrefixRecordProjections True), (AutoImplicitDepth 0)
+      , (NFMetavarThreshold 0), (SearchTimeout 0)
+      ]
+
+  isPragma : Directive -> Bool
+  isPragma (CGAction _ _) = False
+  isPragma _              = True
+
+  export
+  pragmaTopics : String
+  pragmaTopics =
+    show $ vsep $ map (((<++>) "+") . pretty {ann=()} . showDirective) $ filter isPragma directiveList
+    where
+      showDirective : Directive -> String
+      showDirective (Hide _)             = "%hide term"
+      showDirective (Logging _)          = "%logging [topic] lvl"
+      showDirective (LazyOn _)           = "%auto_lazy on|off"
+      showDirective (UnboundImplicits _) = "%unbound_implicits"
+      showDirective (AmbigDepth _)       = "%ambiguity_depth n"
+      showDirective (PairNames _ _ _)    = "%pair ty f s"
+      showDirective (RewriteName _ _)    = "%rewrite eq rw"
+      showDirective (PrimInteger _)      = "%integerLit n"
+      showDirective (PrimString _)       = "%stringLit n"
+      showDirective (PrimChar _)         = "%charLit n"
+      showDirective (PrimDouble _)       = "%doubleLit n"
+      showDirective (CGAction _ _)       = "--directive d"
+      showDirective (Names _ _)          = "%name ty ns"
+      showDirective (StartExpr _)        = "%start expr"
+      showDirective (Overloadable _)     = "%allow_overloads"
+      showDirective (Extension _)        = "%language"
+      showDirective (DefaultTotality _)  =
+        "%default partial|total|covering"
+      showDirective (PrefixRecordProjections _) =
+        "%prefix_record_projections on|off"
+      showDirective (AutoImplicitDepth _) =
+        "%auto_implicit_depth n"
+      showDirective (NFMetavarThreshold _) =
+        "%nf_metavar_threshold n"
+      showDirective (SearchTimeout _) =
+        "%search_timeout ms"
+
   public export
   data PField : Type where
        MkField : FC -> (doc : String) -> RigCount -> PiInfo PTerm ->