[ base ] Show example of using the last change + allow holes in isType

libs/base/Deriving/Common.idr

@@ -70,10 +70,12 @@ isType = go Z [] where
     -- Unqualified: that's a local variable
     UN (Basic _) => go (S idx) ((Arg emptyFC nm, idx) :: acc) t
     _ => go (S idx) acc t
+  go idx acc (INamedApp _ t nm (IHole _ _)) = go (S idx) acc t
   go idx acc (INamedApp _ t nm (IVar _ nm')) = case nm' of
     -- Unqualified: that's a local variable
     UN (Basic _) => go (S idx) ((NamedArg emptyFC nm nm', idx) :: acc) t
     _ => go (S idx) acc t
+  go idx acc (IAutoApp _ t (IHole _ _)) = go (S idx) acc t
   go idx acc (IAutoApp _ t (IVar _ nm)) = case nm of
     -- Unqualified: that's a local variable
     UN (Basic _) => go (S idx) ((AutoArg emptyFC nm, idx) :: acc) t

libs/base/Language/Reflection/TTImp.idr

@@ -664,6 +664,12 @@ Traversable Argument where
   traverse f (NamedArg fc nm x) = NamedArg fc nm <$> f x
   traverse f (AutoArg fc x)     = AutoArg fc <$> f x
 
+export
+Show a => Show (Argument a) where
+  showPrec d (Arg fc x)         = showPrec d x
+  showPrec _ (NamedArg fc nm x) = "{\{show nm} = \{show x}}"
+  showPrec _ (AutoArg fc x)     = "@{\show x}"
+
 public export
 iApp : TTImp -> Argument TTImp -> TTImp
 iApp f (Arg fc t) = IApp fc f t

tests/base/deriving_common001/ConView.idr

@@ -0,0 +1,29 @@
+module ConView
+
+import Data.Fin
+
+import Deriving.Common
+
+import Language.Reflection
+
+%default total
+
+%language ElabReflection
+
+data X : Fin n -> Type where
+  MkX1 : (fn : _) -> X fn
+  MkX2 : (fn : Fin n) -> X {n} fn
+  MkX3 : (fn : Fin n) -> X fn {n}
+
+consParams : a -> Elab ()
+consParams t = do
+  t <- isType !(quote t)
+  logMsg "elab" 0 "the type \{show t.typeConstructor}"
+  for_ t.dataConstructors $ \(conName, conTy) => do
+    let Just conView = constructorView conTy
+      | Nothing => failAt (getFC conTy) "cannot intepret as a constructor"
+    logMsg "elab" 0 "- constructor \{show conName}"
+    for_ conView.params $ \(conParam, conIdx) => do
+      logMsg "elab" 0 "  - param (arg #\{show conIdx}): \{show conParam}"
+
+%runElab consParams X

tests/base/deriving_common001/expected

@@ -0,0 +1,21 @@
+1/1: Building ConView (ConView.idr)
+LOG elab:0: the type ConView.X
+LOG elab:0: - constructor ConView.MkX1
+LOG elab:0:   - param (arg #0): {n = {n:3537}}
+LOG elab:0:   - param (arg #1): fn
+LOG elab:0: - constructor ConView.MkX2
+LOG elab:0:   - param (arg #0): {n = n}
+LOG elab:0:   - param (arg #1): fn
+LOG elab:0: - constructor ConView.MkX3
+LOG elab:0:   - param (arg #0): {n = n}
+LOG elab:0:   - param (arg #1): fn
+Error: Unsolved holes:
+ConView.{n:3773} introduced at: 
+ConView:29:21--29:22
+ 25 |     logMsg "elab" 0 "- constructor \{show conName}"
+ 26 |     for_ conView.params $ \(conParam, conIdx) => do
+ 27 |       logMsg "elab" 0 "  - param (arg #\{show conIdx}): \{show conParam}"
+ 28 | 
+ 29 | %runElab consParams X
+                          ^
+

tests/base/deriving_common001/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+check ConView.idr

tests/base/deriving_common001/test.ipkg

@@ -0,0 +1 @@
+package a-test

tests/base/deriving_traversable/expected

@@ -65,7 +65,7 @@ LOG derive.traversable.clauses:1:
   traverseIVect : {0 m : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> IVect {n = m} a -> f (IVect {n = m} b)
   traverseIVect f (MkIVect x2) = MkIVect <$> (traverse f x2)
 LOG derive.traversable.clauses:1: 
-  traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13951} = eq} a -> f (EqMap key {{conArg:13951} = eq} b)
+  traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13967} = eq} a -> f (EqMap key {{conArg:13967} = eq} b)
   traverseEqMap f (MkEqMap x3) = MkEqMap <$> (traverse (traverse f) x3)
 LOG derive.traversable.clauses:1: 
   traverseTree : {0 l : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tree l a -> f (Tree l b)