Merge pull request #109 from andrevidela/withfc-elab

update elab for WithFC
alexhumphreys · Dec 1, 2024 · c169165 · c169165
2 parents 6deee64 + 9220019
commit c169165
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/Idrall/Derive.idr b/Idrall/Derive.idr
@@ -97,7 +97,7 @@ deriveFromDhall it {options} n =
 
      clauses <- genClauses it funName argName cons
 
-     let funClaim = IClaim EmptyFC MW Export [Inline] (MkTy EmptyFC EmptyFC funName `(Expr Void -> Either Error ~(var name)))
+     let funClaim = IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Export [Inline] (MkTy EmptyFC (NoFC funName) `(Expr Void -> Either Error ~(var name)))
      -- add a catch all pattern
      let funDecl = IDef EmptyFC funName (clauses ++ [patClause `(~(var funName) ~(varStr "expr")) `(Left $ FromDhallError (getFC ~(varStr "expr")) "\{show expr}")])
 
@@ -110,7 +110,7 @@ deriveFromDhall it {options} n =
 
      -- created interface for Example, and use function we already declared
      let retty = `(FromDhall ~(var name))
-     let objClaim = IClaim EmptyFC MW Export [Hint True, Inline] (MkTy EmptyFC EmptyFC objName retty)
+     let objClaim = IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Export [Hint True, Inline] (MkTy EmptyFC (NoFC objName) retty)
      let objrhs = `(~(var ifCon) ~(var funName))
      let objDecl = IDef EmptyFC objName [(PatClause EmptyFC (var objName) objrhs)]
      declare [objClaim, objDecl]

diff --git a/Idrall/Derive/Common.idr b/Idrall/Derive/Common.idr
@@ -17,7 +17,7 @@ import public Data.String
 ||| This is an alias for `MkTyp EmptyFC`.
 export
 mkTy : (n : Name) -> (ty : TTImp) -> ITy
-mkTy = MkTy EmptyFC EmptyFC
+mkTy = MkTy EmptyFC . MkFCVal EmptyFC
 
 ||| Creates a variable from the given name
 |||

diff --git a/Idrall/Derive/ToDhall.idr b/Idrall/Derive/ToDhall.idr
@@ -186,12 +186,12 @@ toDhallImpl typeName =
       toDhallLitClause = patClause toDhall $ var rhsToDhallLit
 
       impl = ILocal EmptyFC
-          [ IClaim EmptyFC MW Private [] (MkTy EmptyFC EmptyFC toDhallName `(~(typeNameImp) -> Expr Void))
+          [ IClaim $ NoFC $ MkIClaimData MW Private [] (MkTy EmptyFC (NoFC toDhallName) `(~(typeNameImp) -> Expr Void))
           , IDef EmptyFC toDhallName [toDhallLitClause]
           ]
           `(~(var mkToDhall) ~(var rhsToDhallType) ~(var rhsToDhallLit))
 
-  in [ IClaim EmptyFC MW Public [Hint True] $ MkTy EmptyFC EmptyFC functionName `(ToDhall ~(typeNameImp))
+  in [ IClaim $ NoFC $ MkIClaimData MW Public [Hint True] $ MkTy EmptyFC (NoFC functionName) `(ToDhall ~(typeNameImp))
      , IDef EmptyFC functionName [patClause function impl]
      ]
 
@@ -222,8 +222,8 @@ deriveToDhall it {options} n = do
   -- logCons cons
 
   -- create the function type signatures
-  let funClaimType = IClaim EmptyFC MW Export [Inline] (MkTy EmptyFC EmptyFC funNameType `(Expr Void))
-  let funClaimLit = IClaim EmptyFC MW Export [Inline] (MkTy EmptyFC EmptyFC funNameLit `(~(var name) -> Expr Void))
+  let funClaimType = IClaim $ NoFC $ MkIClaimData MW Export [Inline] (MkTy EmptyFC (NoFC funNameType) `(Expr Void))
+  let funClaimLit = IClaim $ NoFC $ MkIClaimData MW Export [Inline] (MkTy EmptyFC (NoFC funNameLit) `(~(var name) -> Expr Void))
 
   -- declare the function type signatures in the env
   declare [funClaimType, funClaimLit]