Merge pull request #9 from andrevidela/withfc-elab

update elab for WithFC

src/Language/LSP/Message/Derive.idr

@@ -101,15 +101,15 @@ deriveToJSON opts n = do
                    else `(JObject $ catMaybes ~rhs)
       let lhs = `(~(var funName) ~(applyBinds (var conName) (reverse bindNames)))
       pure $ patClause lhs rhs
-    let funclaim = IClaim EmptyFC MW Export [Inline] (MkTy EmptyFC EmptyFC funName `(~(var name) -> JSON))
+    let funclaim = IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Export [Inline] (MkTy EmptyFC (NoFC funName) `(~(var name) -> JSON))
     let fundecl = IDef EmptyFC funName cons
     declare [funclaim, fundecl]
     [(ifName, _)] <- getType `{ToJSON}
       | _ => fail "ToJSON interface must be in scope and unique"
     [NS _ (DN _ ifCon)] <- getCons ifName
       | _ => fail "Interface constructor error"
     let retty = `(ToJSON ~(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]
@@ -171,15 +171,15 @@ deriveFromJSON opts n = do
                      then (uncurry patClause <$> clauses)
                      else [patClause `(~(var funName) (JObject ~(bindvar $ show argName)))
                                      (foldl (\acc, x => `(~x <|> ~acc)) `(Nothing) (snd <$> clauses))]
-    let funClaim = IClaim EmptyFC MW Export [Inline] (MkTy EmptyFC EmptyFC funName `(JSON -> Maybe ~(var name)))
+    let funClaim = IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Export [Inline] (MkTy EmptyFC (NoFC funName) `(JSON -> Maybe ~(var name)))
     let funDecl = IDef EmptyFC funName (clauses ++ [patClause `(~(var funName) ~implicit') `(Nothing)])
     declare [funClaim, funDecl]
     [(ifName, _)] <- getType `{FromJSON}
       | _ => fail "FromJSON interface must be in scope and unique"
     [NS _ (DN _ ifCon)] <- getCons ifName
       | _ => fail "Interface constructor error"
     let retty = `(FromJSON ~(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]