[ upstream ] Update elab for WithFC (#77)

* fix elab for WithFC

* Fix elab-doc

Author: andrevidela

src/Doc/Enum1.md

@@ -68,7 +68,7 @@ enumDecl1 name cons = IData EmptyFC (specified Public) Nothing dat
     enumName = UN $ Basic name
 
     mkCon : String -> ITy
-    mkCon n = MkTy EmptyFC EmptyFC (UN $ Basic n) (IVar EmptyFC enumName)
+    mkCon n = MkTy EmptyFC (NoFC $ UN $ Basic n) (IVar EmptyFC enumName)
 
     dat : Data
     dat = MkData EmptyFC enumName (Just (IType EmptyFC)) [] (map mkCon cons)

src/Doc/Generic4.md

@@ -246,6 +246,7 @@ deriveGeneral ns fs = do
   , "Record"
   , "Clause"
   , "Decl"
+  , "IClaimData"
   ] [Generic', Eq', Ord']
 ```
 

src/Language/Reflection/Pretty.idr

@@ -109,6 +109,10 @@ export
 Pretty FC where
   prettyPrec _ _ = line "emptyFC"
 
+export
+Pretty a => Pretty (WithFC a) where
+  prettyPrec n x = prettyPrec n x.value
+
 export
 Pretty a => Pretty (WithDefault a def') where
   prettyPrec p withDef =
@@ -155,10 +159,11 @@ prettyImplITy : Pretty ITy
   , "IField"
   , "Record"
   , "Decl"
+  , "IClaimData"
   ] [Pretty]
 
 prettyImplITy = MkPretty $ \p,v => case v of
-  (MkTy _ _ n ty) => recordH p "mkTy" [("name", n), ("type", ty)]
+  (MkTy _ n ty) => recordH p "mkTy" [("name", n.value), ("type", ty)]
 
 prettyImplArg = MkPretty $ \p,v =>
   conH p "MkArg" [v.count, v.piInfo, v.name, v.type]

src/Language/Reflection/Syntax.idr

@@ -474,7 +474,7 @@ as = IAs EmptyFC EmptyFC UseLeft
 ||| This is an alias for `MkTyp EmptyFC`.
 public export %inline
 mkTy : (name : Name) -> (type : TTImp) -> ITy
-mkTy = MkTy EmptyFC EmptyFC
+mkTy = MkTy EmptyFC . MkFCVal EmptyFC
 
 ||| Type declaration of a function.
 |||
@@ -488,7 +488,7 @@ claim :
   -> (name  : Name)
   -> (type  : TTImp)
   -> Decl
-claim c v opts n tp = IClaim EmptyFC c v opts (mkTy n tp)
+claim c v opts n tp = IClaim $ MkFCVal EmptyFC $ MkIClaimData c v opts (mkTy n tp)
 
 ||| `simpleClaim v n t` is an alias for `claim MW v [] (mkTy n t)`
 public export %inline

src/Language/Reflection/Types.idr

@@ -667,3 +667,4 @@ getParamInfo' n = do
 export %macro
 getParamInfo : Name -> Elab ParamTypeInfo
 getParamInfo = getParamInfo'
+

src/Test/Enum2.idr

@@ -8,8 +8,7 @@ import Language.Reflection.Util
 
 ex1 : List Decl
 ex1 =
-  [ IClaim
-      emptyFC
+  [ IClaim $ NoFC $ MkIClaimData
       MW
       Private
       []

src/Test/Inspect.idr

@@ -73,15 +73,13 @@ ex9 =
 
 ex10 : List Decl
 ex10 =
-  [ IClaim
-      emptyFC
+  [ IClaim $ NoFC $ MkIClaimData
       MW
       Export
       [Inline]
       (MkTy
          emptyFC
-         emptyFC
-         "test"
+         (NoFC "test")
          (    MkArg MW ExplicitArg Nothing (primVal (PrT IntType))
           .-> primVal (PrT IntType)))
   , IDef
@@ -103,10 +101,9 @@ ex11 =
          []
          [ MkTy
              emptyFC
-             emptyFC
-             "A"
+             (NoFC "A")
              (    MkArg MW ExplicitArg Nothing (bindVar "t")
               .-> var "Foo" .$ bindVar "t")
-         , MkTy emptyFC emptyFC "B" (var "Foo" .$ bindVar "t")
+         , MkTy emptyFC (NoFC "B") (var "Foo" .$ bindVar "t")
          ])
   ]