Merge pull request #249 from edwinb/refl-names

Reflect 'display names' and record field names

libs/base/Language/Reflection/TT.idr

@@ -47,9 +47,11 @@ data Constant
     | WorldType
 
 public export
-data Name = UN String
-          | MN String Int
-          | NS (List String) Name
+data Name = UN String -- user defined name
+          | MN String Int -- machine generated name
+          | NS (List String) Name -- name in a namespace
+          | DN String Name -- a name and how to display it
+          | RF String -- record field name
 
 export
 Show Name where
@@ -61,6 +63,8 @@ Show Name where
       showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
   show (UN x) = x
   show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
+  show (DN str y) = str
+  show (RF n) = "." ++ n
 
 public export
 data Count = M0 | M1 | MW

src/Core/Reflect.idr

@@ -228,6 +228,13 @@ Reify Name where
                  => do ns' <- reify defs !(evalClosure defs ns)
                        n' <- reify defs !(evalClosure defs n)
                        pure (NS ns' n')
+             (NS _ (UN "DN"), [str, n])
+                 => do str' <- reify defs !(evalClosure defs str)
+                       n' <- reify defs !(evalClosure defs n)
+                       pure (DN str' n')
+             (NS _ (UN "RF"), [str])
+                 => do str' <- reify defs !(evalClosure defs str)
+                       pure (RF str')
              _ => cantReify val "Name"
   reify defs val = cantReify val "Name"
 
@@ -244,6 +251,13 @@ Reflect Name where
       = do ns' <- reflect fc defs lhs env ns
            n' <- reflect fc defs lhs env n
            appCon fc defs (reflectiontt "NS") [ns', n']
+  reflect fc defs lhs env (DN str n)
+      = 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 (RF x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "RF") [x']
   reflect fc defs lhs env (Resolved i)
       = case !(full (gamma defs) (Resolved i)) of
              Resolved _ => cantReflect fc "Name"