WithFC elab (#3423)

* add WithFC to reflection

* implement IClaimData reflection

* Add Ord,Eq instance to WithFC

CHANGELOG_NEXT.md

@@ -98,6 +98,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * `min` was renamed to `leftMost` in `Libraries.Data.Sorted{Map|Set}` in order
   to be defined as in `base`.
 
+* Reflected trees now make use of WithFC to replicate the new location tracking
+  in the compiler.
+
 ### Backend changes
 
 #### RefC Backend

libs/base/Deriving/Foldable.idr

@@ -371,7 +371,7 @@ namespace Foldable
     let b = un $ freshName paramNames "b"
     let va = IVar fc a
     let vb = IVar fc b
-    let ty = MkTy fc fc foldMapName $ withParams fc (paramConstraints ns) params
+    let ty = MkTy fc (NoFC foldMapName) $ withParams fc (paramConstraints ns) params
            $ IPi fc M0 ImplicitArg (Just a) (IType fc)
            $ IPi fc M0 ImplicitArg (Just b) (IType fc)
            $ `(Monoid ~(vb) => (~(va) -> ~(vb)) -> ~(t) ~(va) -> ~(vb))
@@ -381,7 +381,7 @@ namespace Foldable
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc foldMapName cls
       ] `(fromFoldMap ~(t) ~(IVar fc foldMapName))
 

libs/base/Deriving/Functor.idr

@@ -382,7 +382,7 @@ namespace Functor
       , "Bifunctors: \{show ns.asBifunctors}"
       , "Parameters: \{show (map (mapFst unArg) params)}"
       ]
-    let ty = MkTy fc fc mapName $ withParams fc (paramConstraints ns) params
+    let ty = MkTy fc (NoFC mapName) $ withParams fc (paramConstraints ns) params
            $ IPi fc M0 ImplicitArg (Just a) (IType fc)
            $ IPi fc M0 ImplicitArg (Just b) (IType fc)
            $ `((~(va) -> ~(vb)) -> ~(t) ~(va) -> ~(t) ~(vb))
@@ -392,7 +392,7 @@ namespace Functor
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc mapName cls
       ] `(MkFunctor {f = ~(t)} ~(IVar fc mapName))
 

libs/base/Deriving/Show.idr

@@ -264,15 +264,15 @@ namespace Show
             ])
 
     -- Generate the type of the show function
-    let ty = MkTy fc fc showName $ withParams fc (paramConstraints ns) params
+    let ty = MkTy fc (NoFC showName) $ withParams fc (paramConstraints ns) params
            $ `(Prec -> ~(t) -> String)
     logMsg "derive.show.clauses" 1 $
       joinBy "\n" ("" :: ("  " ++ show (mapITy cleanup ty))
                       :: map (("  " ++) . showClause InDecl . mapClause cleanup) cls)
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc showName cls
       ] `(fromShowPrec ~(IVar fc showName))
 

libs/base/Deriving/Traversable.idr

@@ -395,7 +395,7 @@ namespace Traversable
     let va = IVar fc a
     let vb = IVar fc b
     let vf = IVar fc f
-    let ty = MkTy fc fc traverseName $ withParams fc (paramConstraints ns) params
+    let ty = MkTy fc (NoFC traverseName) $ withParams fc (paramConstraints ns) params
            $ IPi fc M0 ImplicitArg (Just a) (IType fc)
            $ IPi fc M0 ImplicitArg (Just b) (IType fc)
            $ IPi fc M0 ImplicitArg (Just f) (IPi fc MW ExplicitArg Nothing (IType fc) (IType fc))
@@ -406,7 +406,7 @@ namespace Traversable
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc traverseName cls
       ] `(MkTraversable {t = ~(t)} ~(IVar fc traverseName))
 

libs/base/Language/Reflection/TT.idr

@@ -68,6 +68,41 @@ public export
 emptyFC : FC
 emptyFC = EmptyFC
 
+------------------------------------------------------------------------
+||| A wrapper for a value with a file context.
+public export
+record WithFC (ty : Type) where
+  constructor MkFCVal
+  fc : FC
+  value : ty
+
+||| Smart constructor for WithFC that uses EmptyFC as location
+%inline export
+NoFC : a -> WithFC a
+NoFC = MkFCVal EmptyFC
+
+export
+Functor WithFC where
+  map f = { value $= f}
+
+export
+Foldable WithFC where
+  foldr f i v = f v.value i
+
+export
+Traversable WithFC where
+  traverse f (MkFCVal fc val) = map (MkFCVal fc) (f val)
+
+||| Locations are not taken into account when comparing reflected trees
+export
+Eq a => Eq (WithFC a) where
+  x == y = x.value == y.value
+
+||| Locations are not taken into account when comparing reflected trees
+export
+Ord a => Ord (WithFC a) where
+  compare x y = compare x.value y.value
+
 public export
 data NameType : Type where
      Bound   : NameType

libs/base/Language/Reflection/TTImp.idr

@@ -123,7 +123,7 @@ mutual
 
   public export
   data ITy : Type where
-       MkTy : FC -> (nameFC : FC) -> (n : Name) -> (ty : TTImp) -> ITy
+       MkTy : FC -> (n : WithFC Name) -> (ty : TTImp) -> ITy
 
   %name ITy sig
 
@@ -202,10 +202,17 @@ mutual
   onWithDefault defHandler _ DefaultedValue     = defHandler
   onWithDefault _ valHandler (SpecifiedValue v) = valHandler v
 
+  public export
+  record IClaimData where
+    constructor MkIClaimData
+    rig : Count
+    vis : Visibility
+    opts : List FnOpt
+    type : ITy
+
   public export
   data Decl : Type where
-       IClaim : FC -> Count -> Visibility -> List FnOpt ->
-                ITy -> Decl
+       IClaim : WithFC IClaimData -> Decl
        IData : FC -> WithDefault Visibility Private -> Maybe TotalReq -> Data -> Decl
        IDef : FC -> Name -> (cls : List Clause) -> Decl
        IParameters : FC -> (params : List (Name, Count, PiInfo TTImp, TTImp)) ->
@@ -408,7 +415,7 @@ parameters {auto eqTTImp : Eq TTImp}
 
   public export
   Eq ITy where
-    MkTy _ _ n ty == MkTy _ _ n' ty' = n == n' && ty == ty'
+    MkTy _ n ty == MkTy _ n' ty' = n.value == n'.value && ty == ty'
 
   public export
   Eq Data where
@@ -429,9 +436,13 @@ parameters {auto eqTTImp : Eq TTImp}
       n == n' && ps == ps' && opts == opts' && cn == cn' && fs == fs'
 
   public export
-  Eq Decl where
-    IClaim _ c v fos t == IClaim _ c' v' fos' t' =
+  Eq IClaimData where
+    MkIClaimData c v fos t == MkIClaimData c' v' fos' t' =
       c == c' && v == v' && fos == fos' && t == t'
+
+  public export
+  Eq Decl where
+    IClaim c == IClaim c' = c.value == c'.value
     IData _ v t d == IData _ v' t' d' =
       v == v' && t == t' && d == d'
     IDef _ n cs == IDef _ n' cs' =
@@ -541,13 +552,16 @@ mutual
 
   public export
   Show ITy where
-    show (MkTy fc nameFC n ty) = "\{show n} : \{show ty}"
+    show (MkTy fc n ty) = "\{show n.value} : \{show ty}"
 
-  public export
-  Show Decl where
-    show (IClaim fc rig vis xs sig)
+  Show IClaimData where
+    show (MkIClaimData rig vis xs sig)
       = unwords [ show vis
                 , showCount rig (show sig) ]
+
+  public export
+  Show Decl where
+    show (IClaim claim) = show claim.value
     show (IData fc vis treq dt)
       = unwords [ show vis
                 , showTotalReq treq (show dt)
@@ -774,7 +788,7 @@ parameters (f : TTImp -> TTImp)
 
   public export
   mapITy : ITy -> ITy
-  mapITy (MkTy fc nameFC n ty) = MkTy fc nameFC n (mapTTImp ty)
+  mapITy (MkTy fc n ty) = MkTy fc n (mapTTImp ty)
 
   public export
   mapFnOpt : FnOpt -> FnOpt
@@ -807,10 +821,13 @@ parameters (f : TTImp -> TTImp)
   mapRecord (MkRecord fc n params opts conName fields)
     = MkRecord fc n (map (map $ map $ bimap mapPiInfo mapTTImp) params) opts conName (map mapIField fields)
 
+  mapIClaimData : IClaimData -> IClaimData
+  mapIClaimData (MkIClaimData rig vis opts ty)
+    = MkIClaimData rig vis (map mapFnOpt opts) (mapITy ty)
+
   public export
   mapDecl : Decl -> Decl
-  mapDecl (IClaim fc rig vis opts ty)
-    = IClaim fc rig vis (map mapFnOpt opts) (mapITy ty)
+  mapDecl (IClaim claim) = IClaim $ map mapIClaimData claim
   mapDecl (IData fc vis mtreq dat) = IData fc vis mtreq (mapData dat)
   mapDecl (IDef fc n cls) = IDef fc n (map mapClause cls)
   mapDecl (IParameters fc params xs) = IParameters fc params (assert_total $ map mapDecl xs)
@@ -895,7 +912,7 @@ parameters {0 m : Type -> Type} {auto apl : Applicative m} (f : (original : TTIm
 
   public export
   mapMITy : ITy -> m ITy
-  mapMITy (MkTy fc nameFC n ty) = MkTy fc nameFC n <$> mapATTImp' ty
+  mapMITy (MkTy fc n ty) = MkTy fc n <$> mapATTImp' ty
 
   public export
   mapMFnOpt : FnOpt -> m FnOpt
@@ -933,10 +950,13 @@ parameters {0 m : Type -> Type} {auto apl : Applicative m} (f : (original : TTIm
     <*> pure conName
     <*> traverse mapMIField fields
 
+  mapMIClaimData : IClaimData -> m IClaimData
+  mapMIClaimData (MkIClaimData rig vis opts ty)
+    = MkIClaimData rig vis <$> traverse mapMFnOpt opts <*> mapMITy ty
+
   public export
   mapMDecl : Decl -> m Decl
-  mapMDecl (IClaim fc rig vis opts ty)
-    = IClaim fc rig vis <$> traverse mapMFnOpt opts <*> mapMITy ty
+  mapMDecl (IClaim claim) = IClaim <$> traverse mapMIClaimData claim
   mapMDecl (IData fc vis mtreq dat) = IData fc vis mtreq <$> mapMData dat
   mapMDecl (IDef fc n cls) = IDef fc n <$> traverse mapMClause cls
   mapMDecl (IParameters fc params xs) = IParameters fc params <$> assert_total (traverse mapMDecl xs)

src/Core/Reflect.idr

@@ -12,6 +12,7 @@ import Libraries.Data.WithDefault
 
 %default covering
 
+
 public export
 interface Reify a where
   reify : {auto c : Ref Ctxt Defs} ->
@@ -863,6 +864,28 @@ Reflect FC where
            appCon fc defs (reflectiontt "MkFC") [fn', start', end']
   reflect fc defs lhs env EmptyFC = getCon fc defs (reflectiontt "EmptyFC")
 
+export
+Reify a => Reify (WithFC a) where
+  reify defs val@(NDCon _ n _ _ args)
+      = case (dropAllNS !(full (gamma defs) n), map snd args) of
+             (UN (Basic "MkFCVal"), [fcterm, nestedVal]) => do
+                 fc <- reify defs !(evalClosure defs fcterm)
+                 val <- reify defs !(evalClosure defs nestedVal)
+                 pure $ MkFCVal fc val
+             (UN (Basic "MkFCVal"), [_, fc, l2]) => do
+                 fc' <- reify defs !(evalClosure defs fc)
+                 val' <- reify defs !(evalClosure defs l2)
+                 pure $ MkFCVal fc' val'
+             (t, l) => cantReify val "WithFC constructor: \{show t}, args: \{show (length l)}"
+  reify defs val = cantReify val "Expected WithFC, found something else"
+
+export
+Reflect a => Reflect (WithFC a) where
+  reflect fc defs lhs env (MkFCVal loc val)
+      = do loc' <- reflect fc defs lhs env loc
+           val' <- reflect fc defs lhs env val
+           appCon fc defs (reflectiontt "MkFCVal") [loc', val']
+
 {-
 -- Reflection of well typed terms: We don't reify terms because that involves
 -- type checking, but we can reflect them

src/TTImp/Reflect.idr

@@ -310,12 +310,11 @@ mutual
   Reify ImpTy where
     reify defs val@(NDCon _ n _ _ args)
         = case (dropAllNS !(full (gamma defs) n), map snd args) of
-               (UN (Basic "MkTy"), [w, x, y, z])
+               (UN (Basic "MkTy"), [w, y, z])
                     => do w' <- reify defs !(evalClosure defs w)
-                          x' <- reify defs !(evalClosure defs x)
                           y' <- reify defs !(evalClosure defs y)
                           z' <- reify defs !(evalClosure defs z)
-                          pure (MkImpTy w' (MkFCVal x' y') z')
+                          pure (MkImpTy w' y' z')
                _ => cantReify val "ITy"
     reify defs val = cantReify val "ITy"
 
@@ -416,16 +415,25 @@ mutual
     reify defs val = cantReify val "Clause"
 
   export
-  Reify ImpDecl where
+  Reify (IClaimData Name) where
     reify defs val@(NDCon _ n _ _ args)
         = case (dropAllNS !(full (gamma defs) n), map snd args) of
-               (UN (Basic "IClaim"), [v,w,x,y,z])
-                    => do v' <- reify defs !(evalClosure defs v)
-                          w' <- reify defs !(evalClosure defs w)
+               (UN (Basic "MkIClaimData"), [w, x, y, z])
+                    => do w' <- reify defs !(evalClosure defs w)
                           x' <- reify defs !(evalClosure defs x)
                           y' <- reify defs !(evalClosure defs y)
                           z' <- reify defs !(evalClosure defs z)
-                          pure (IClaim (MkFCVal v' $ MkIClaimData w' x' y' z'))
+                          pure (MkIClaimData w' x' y' z')
+               _ => cantReify val "IClaimData"
+    reify defs val = cantReify val "IClaimData"
+
+  export
+  Reify ImpDecl where
+    reify defs val@(NDCon _ n _ _ args)
+        = case (dropAllNS !(full (gamma defs) n), map snd args) of
+               (UN (Basic "IClaim"), [v])
+                    => do v' <- reify defs !(evalClosure defs v)
+                          pure (IClaim v')
                (UN (Basic "IData"), [x,y,z,w])
                     => do x' <- reify defs !(evalClosure defs x)
                           y' <- reify defs !(evalClosure defs y)
@@ -685,12 +693,11 @@ mutual
 
   export
   Reflect ImpTy where
-    reflect fc defs lhs env (MkImpTy w (MkFCVal x y) z)
+    reflect fc defs lhs env (MkImpTy w x z)
         = do w' <- reflect fc defs lhs env w
              x' <- reflect fc defs lhs env x
-             y' <- reflect fc defs lhs env y
              z' <- reflect fc defs lhs env z
-             appCon fc defs (reflectionttimp "MkTy") [w', x', y', z']
+             appCon fc defs (reflectionttimp "MkTy") [w', x', z']
 
   export
   Reflect DataOpt where
@@ -765,14 +772,19 @@ mutual
              appCon fc defs (reflectionttimp "ImpossibleClause") [x', y']
 
   export
-  Reflect ImpDecl where
-    reflect fc defs lhs env (IClaim (MkFCVal v $ MkIClaimData w x y z))
-        = do v' <- reflect fc defs lhs env v
-             w' <- reflect fc defs lhs env w
+  Reflect (IClaimData Name) where
+    reflect fc defs lhs env (MkIClaimData w x y z)
+        = do w' <- reflect fc defs lhs env w
              x' <- reflect fc defs lhs env x
              y' <- reflect fc defs lhs env y
              z' <- reflect fc defs lhs env z
-             appCon fc defs (reflectionttimp "IClaim") [v', w', x', y', z']
+             appCon fc defs (reflectionttimp "MkIClaimData") [w', x', y', z']
+
+  export
+  Reflect ImpDecl where
+    reflect fc defs lhs env (IClaim v)
+        = do v' <- reflect fc defs lhs env v
+             appCon fc defs (reflectionttimp "IClaim") [v']
     reflect fc defs lhs env (IData x y z w)
         = do x' <- reflect fc defs lhs env x
              y' <- reflect fc defs lhs env y

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:13933} = eq} a -> f (EqMap key {{conArg:13933} = eq} b)
+  traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13937} = eq} a -> f (EqMap key {{conArg:13937} = 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)