[ new ] add --show-implicits flag (#3484)

idris-lang · Feb 4, 2025 · 80c4ca1 · 80c4ca1
1 parent 0751a91
commit 80c4ca1
Show file tree

Hide file tree

Showing 5 changed files with 27 additions and 0 deletions.
diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr
@@ -103,6 +103,8 @@ data CLOpt
   NoBanner |
    ||| Run Idris 2 in quiet mode
   Quiet |
+   ||| Show implicits when pretty printing
+  ShowImplicits |
    ||| Show machine names when pretty printing
   ShowMachineNames |
    ||| Show namespaces when pretty printing
@@ -336,6 +338,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
               (Just "Quiet mode; display fewer messages"),
            MkOpt ["--console-width"] [AutoNat "console width"] (\l => [ConsoleWidth l])
               (Just "Width for console output (0 for unbounded) (auto by default)"),
+          MkOpt ["--show-implicits"] [] [ShowImplicits]
+              (Just "Show implicits when pretty printing"),
            MkOpt ["--show-machine-names"] [] [ShowMachineNames]
               (Just "Show machine names when pretty printing"),
            MkOpt ["--show-namespaces"] [] [ShowNamespaces]

diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr
@@ -490,6 +490,10 @@ preOptions (Logging n :: opts)
 preOptions (ConsoleWidth n :: opts)
     = do setConsoleWidth n
          preOptions opts
+preOptions (ShowImplicits :: opts)
+    = do pp <- getPPrint
+         setPPrint ({ showImplicits := True } pp)
+         preOptions opts
 preOptions (ShowMachineNames :: opts)
     = do pp <- getPPrint
          setPPrint ({ showMachineNames := True } pp)

diff --git a/tests/idris2/interactive/interactive047/Missing.idr b/tests/idris2/interactive/interactive047/Missing.idr
@@ -0,0 +1,4 @@
+import Data.Vect
+
+foo : {n : Nat} -> Vect n Nat -> Nat
+foo {n=Z} _ = 42
diff --git a/tests/idris2/interactive/interactive047/expected b/tests/idris2/interactive/interactive047/expected
@@ -0,0 +1,12 @@
+1/1: Building Missing (Missing.idr)
+Error: foo is not covering.
+
+Missing:3:1--3:37
+ 1 | import Data.Vect
+ 2 | 
+ 3 | foo : {n : Nat} -> Vect n Nat -> Nat
+     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    foo {n = S _} _
+
diff --git a/tests/idris2/interactive/interactive047/run b/tests/idris2/interactive/interactive047/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 --check --show-implicits Missing.idr
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		. ../../../testutils.sh

		idris2 --check --show-implicits Missing.idr