Merge pull request #1712 from edwinb/MarcelineVQ-elab-name-changes

Add more name reflections

libs/base/Language/Reflection/TT.idr

@@ -102,6 +102,9 @@ data Name = UN String -- user defined name
           | NS Namespace Name -- name in a namespace
           | DN String Name -- a name and how to display it
           | RF String -- record field name
+          | 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
@@ -110,6 +113,10 @@ Show Name where
   show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
   show (DN str y) = str
   show (RF n) = "." ++ n
+  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

@@ -291,8 +291,22 @@ Reify Name where
              (NS _ (UN "RF"), [(_, str)])
                  => do str' <- reify defs !(evalClosure defs str)
                        pure (RF str')
-             _ => cantReify val "Name"
-  reify defs val = cantReify val "Name"
+             (NS _ (UN "Nested"), [(_, ix), (_, n)])
+                 => do ix' <- reify defs !(evalClosure defs ix)
+                       n' <- reify defs !(evalClosure defs n)
+                       pure (Nested ix' n')
+             (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
@@ -314,11 +328,25 @@ Reflect Name where
   reflect fc defs lhs env (RF x)
       = do x' <- reflect fc defs lhs env x
            appCon fc defs (reflectiontt "RF") [x']
+  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 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 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

@@ -186,7 +186,7 @@ idrisTests = MkTestPool "Misc" [] Nothing
        -- Quotation and reflection
        "reflection001", "reflection002", "reflection003", "reflection004",
        "reflection005", "reflection006", "reflection007", "reflection008",
-       "reflection009",
+       "reflection009","reflection010",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008", "total009", "total010",

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.2963:747:foo
+LOG declare.type:1: Processing Main.cased
+LOG declare.type:1: Processing Main.test
+LOG 1: nested: ((Main.MkIdentity [a = Int]) Main.2963:747: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