add more Name reflections

broaden what Names can be reflected and refied
I did not add the Names I wasn't sure how to test but have put placeholders
that produce clearer error messages.

libs/base/Language/Reflection/TT.idr

@@ -64,6 +64,9 @@ data Name = UN String -- user defined name
           | MN String Int -- machine generated name
           | NS Namespace Name -- name in a namespace
           | DN String Name -- a name and how to display it
+          | Nested (Int, Int) Name -- nested function name
+          | CaseBlock Int Int -- case block nested in (resolved) name
+          | WithBlock Int Int -- with block nested in (resolved) name
 
 export
 Show Name where
@@ -71,6 +74,10 @@ Show Name where
   show (UN x) = x
   show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
   show (DN str y) = str
+  show (Nested (outer, idx) inner)
+      = show outer ++ ":" ++ show idx ++ ":" ++ show inner
+  show (CaseBlock outer i) = "case block in " ++ show outer
+  show (WithBlock outer i) = "with block in " ++ show outer
 
 public export
 data Count = M0 | M1 | MW

src/Core/Reflect.idr

@@ -272,8 +272,22 @@ Reify Name where
                  => do str' <- reify defs !(evalClosure defs str)
                        n' <- reify defs !(evalClosure defs n)
                        pure (DN str' n')
-             _ => cantReify val "Name"
-  reify defs val = cantReify val "Name"
+             (NS _ (UN "Nested"), [ix,str])
+                 => do ix' <- reify defs !(evalClosure defs ix)
+                       str' <- reify defs !(evalClosure defs str)
+                       pure (Nested ix' str')
+             (NS _ (UN "CaseBlock"), [outer,i])
+                 => do outer' <- reify defs !(evalClosure defs outer)
+                       i' <- reify defs !(evalClosure defs i)
+                       pure (CaseBlock outer' i')
+             (NS _ (UN "WithBlock"), [outer,i])
+                 => do outer' <- reify defs !(evalClosure defs outer)
+                       i' <- reify defs !(evalClosure defs i)
+                       pure (WithBlock outer' i')
+             (NS _ (UN _), _)
+                 => cantReify val "Name, reifying it is unimplemented or intentionally internal"
+             _ => cantReify val "Name, the name was not found in context"
+  reify defs val = cantReify val "Name, value is not an NDCon interally"
 
 export
 Reflect Name where
@@ -292,11 +306,31 @@ Reflect Name where
       = do str' <- reflect fc defs lhs env str
            n' <- reflect fc defs lhs env n
            appCon fc defs (reflectiontt "DN") [str', n']
+  reflect fc defs lhs env (Nested ix n)
+      = do ix' <- reflect fc defs lhs env ix
+           n'  <- reflect fc defs lhs env n
+           appCon fc defs (reflectiontt "Nested") [ix',n']
+  reflect fc defs lhs env (CaseBlock outer i)
+      = do Resolved _ <- full (gamma defs) (Resolved i)
+             | _ => cantReflect fc
+                      "Name inside CaseBlock, it is not a Resolved name"
+           outer' <- reflect fc defs lhs env outer
+           i' <- reflect fc defs lhs env i
+           appCon fc defs (reflectiontt "CaseBlock") [outer',i']
+  reflect fc defs lhs env (WithBlock outer i)
+      = do Resolved _ <- full (gamma defs) (Resolved i)
+             | _ => cantReflect fc
+                      "Name inside WithBlock, it is not a Resolved name"
+           outer' <- reflect fc defs lhs env outer
+           i' <- reflect fc defs lhs env i
+           appCon fc defs (reflectiontt "WithBlock") [outer',i']
   reflect fc defs lhs env (Resolved i)
       = case !(full (gamma defs) (Resolved i)) of
-             Resolved _ => cantReflect fc "Name"
+             Resolved _ => cantReflect fc
+                      "Name directly, Resolved is intentionally internal"
              n => reflect fc defs lhs env n
-  reflect fc defs lhs env val = cantReflect fc "Name"
+  reflect fc defs lhs env n = cantReflect fc
+    "Name, reflecting it is unimplemented or intentionally internal"
 
 export
 Reify NameType where

tests/Main.idr

@@ -105,7 +105,7 @@ idrisTests
        -- Quotation and reflection
        "reflection001", "reflection002", "reflection003", "reflection004",
        "reflection005", "reflection006", "reflection007", "reflection008",
-       "reflection009",
+       "reflection009","reflection010",
        -- Miscellaneous regressions
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",

tests/idris2/reflection010/Name.idr

@@ -0,0 +1,40 @@
+import Language.Reflection
+
+%language ElabReflection
+
+%logging 1
+
+-- This test is for checking changes to how Names are reflected and reified.
+-- It currently tests Names that refer to nested functions and Names that refer
+-- to nested cases.
+
+-- Please add future tests for Names here if they would fit in. There's plenty
+-- of room.
+
+data Identity a = MkIdentity a
+
+nested : Identity Int
+nested = MkIdentity foo
+  where
+    foo : Int
+    foo = 12
+
+-- a pattern matching lambda is really a case
+cased : Identity Int -> Int
+cased = \(MkIdentity x) => x
+
+test : Elab ()
+test = do
+    n <- quote nested
+    logTerm "" 1 "nested" n
+    MkIdentity n' <- check {expected=Identity Int} n
+    logMsg "" 1 $ show (n' == 12)
+
+    c <- quote cased
+    logTerm "" 1 "cased" c
+    c' <- check {expected=Identity Int -> Int} c
+    logMsg "" 1 $ show (c' (MkIdentity 10))
+
+    pure ()
+
+%runElab test

tests/idris2/reflection010/expected

@@ -0,0 +1,10 @@
+1/1: Building Name (Name.idr)
+LOG declare.data:1: Processing Main.Identity
+LOG declare.type:1: Processing Main.nested
+LOG declare.type:1: Processing Main.2091:3813:foo
+LOG declare.type:1: Processing Main.cased
+LOG declare.type:1: Processing Main.test
+LOG 1: nested: ((Main.MkIdentity [Just a = Int]) Main.2091:3813:foo)
+LOG 1: True
+LOG 1: cased: (%lam RigW Explicit (Just {lamc:0}) (Main.Identity Int) (Main.case block in cased {lamc:0}))
+LOG 1: 10

tests/idris2/reflection010/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner --check Name.idr
+
+rm -rf build