remove record let

src/Core/Core.idr

@@ -830,7 +830,7 @@ traverseList1_ f xxs
          ignore (f x)
          traverse_ f xs
 
-export
+%inline export
 traverseFC : (a -> Core b) -> WithFC a -> Core (WithFC b)
 traverseFC f (MkFCVal fc x) = MkFCVal fc <$> f x
 

src/Core/Reflect.idr

@@ -863,7 +863,6 @@ Reflect FC where
            appCon fc defs (reflectiontt "MkFC") [fn', start', end']
   reflect fc defs lhs env EmptyFC = getCon fc defs (reflectiontt "EmptyFC")
 
-
 {-
 -- Reflection of well typed terms: We don't reify terms because that involves
 -- type checking, but we can reflect them

src/Idris/Desugar.idr

@@ -976,7 +976,7 @@ mutual
                       tycon <- desugar AnyExpr ps tycon
                       bindTypeNames fc (usingImpl syn) ps tycon)
                    opts
-                   (concat mm) -- !(traverse (desugarType ps) datacons)
+                   (concat mm)
   desugarData ps doc (MkPLater fc n tycon)
       = do addDocString n doc
            syn <- get Syn
@@ -990,21 +990,18 @@ mutual
                  {auto o : Ref ROpts REPLOpts} ->
                  List Name -> Namespace -> PField ->
                  Core (List IField)
-  desugarField ps ns (MkField fc doc rig p names ty)
+  desugarField ps ns (MkFCVal fc $ MkRecordField doc rig p names ty)
       = flip Core.traverse names $ \n : Name => do
            addDocStringNS ns n doc
            addDocStringNS ns (toRF n) doc
            syn <- get Syn
-
            pure (MkIField fc rig !(traverse (desugar AnyExpr ps) p )
                           n !(bindTypeNames fc (usingImpl syn)
                           ps !(desugar AnyExpr ps ty)))
         where
           toRF : Name -> Name
           toRF (UN (Basic n)) = UN (Field n)
           toRF n = n
-  desugarField ps ns (MkRecordLet (MkFCVal fc let_))
-      = ?whu
 
   export
   desugarFnOpt : {auto s : Ref Syn SyntaxInfo} ->
@@ -1215,8 +1212,7 @@ mutual
                          vis mbtot (MkImpRecord fc tn paramsb opts conname (concat fields'))]
     where
       getfname : PField -> List Name
-      getfname (MkField _ _ _ _ n _) = n
-      getfname (MkRecordLet let_) = []
+      getfname x = x.val.names
 
       mkConName : Name -> Name
       mkConName (NS ns (UN n))

src/Idris/Parser.idr

@@ -1803,24 +1803,19 @@ fieldDecl fname indents
           RecordClaim <$> localClaim fname idents
       <|> do b <- bounds (clause 0 Nothing fname idents)
              pure $ RecordClause (b.withFC {o = fname})
+
     fieldBody : String -> PiInfo PTerm -> Rule (PField)
     fieldBody doc p
         = do b <- bounds (do
-                    col <- column
-                    decoratedKeyword fname "let"
-                    nonEmptyBlockAfter col (parseRecordLet fname)
-                    )
-             pure $ MkRecordLet b.withFC
-      <|> do b <- bounds (do
                     rig <- multiplicity fname
                     ns <- sepBy1 (decoratedSymbol fname ",")
                             (decorate fname Function name
                                <|> (do b <- bounds (symbol "_")
                                        fatalLoc {c = True} b.bounds "Fields have to be named"))
                     decoratedSymbol fname ":"
                     ty <- typeExpr pdef fname indents
-                    pure (\fc : FC => MkField fc doc rig p (forget ns) ty))
-             pure (b.val b.toFC)
+                    pure (MkRecordField doc rig p (forget ns) ty))
+             pure b.withFC
 
 typedArg : OriginDesc -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
 typedArg fname indents

src/Idris/Resugar.idr

@@ -491,7 +491,7 @@ mutual
   toPField (MkIField fc c p n ty)
       = do ty' <- toPTerm startPrec ty
            p' <- traverse (toPTerm startPrec) p
-           pure (MkField fc "" c p' [n] ty')
+           pure (MkFCVal fc $ MkRecordField "" c p' [n] ty')
 
   toPRecord : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->

src/Idris/Syntax.idr

@@ -10,7 +10,6 @@ import public Core.TT
 
 import TTImp.TTImp
 
-import Data.Choice
 import Data.List
 import Data.Maybe
 import Data.SnocList
@@ -394,15 +393,23 @@ mutual
        -- There is no nm on Directive
        ForeignImpl : Name -> List PTerm -> Directive
 
+
+  public export
+  record RecordField' (nm : Type) where
+    constructor MkRecordField
+    doc : String
+    rig : RigCount
+    piInfo : PiInfo (PTerm' nm)
+    names : List Name -- Those names should be `WithFC`
+    type : PTerm' nm
+
   public export
   PField : Type
   PField = PField' Name
 
   public export
-  data PField' : Type -> Type where
-       MkField : FC -> (doc : String) -> RigCount -> PiInfo (PTerm' nm) ->
-                 List Name -> (ty : PTerm' nm) -> PField' nm
-       MkRecordLet : WithFC (List1 (PRecordDeclLet' nm)) -> PField' nm
+  PField' : Type -> Type
+  PField' nm = WithFC (RecordField' nm)
 
   public export
   0 PRecordDeclLet : Type

src/Idris/Syntax/Traversals.idr

@@ -312,13 +312,11 @@ mapPTermM f = goPTerm where
                    <*> goPTypeDecls tdecls
     goPDataDecl (MkPLater fc n t) = MkPLater fc n <$> goPTerm t
 
-    goPField : PField' nm -> Core (PField' nm)
-    goPField (MkField fc doc c info n t) =
-      MkField fc doc c <$> goPiInfo info
-                       <*> pure n
-                       <*> goPTerm t
-    goPField (MkRecordLet decls) =
-      MkRecordLet <$> traverseFC (traverseList1 goPRecordDeclLet) decls
+    goRecordField : RecordField' nm -> Core (RecordField' nm)
+    goRecordField (MkRecordField doc c info n t) =
+      MkRecordField doc c <$> goPiInfo info
+                          <*> pure n
+                          <*> goPTerm t
 
     goPiInfo : PiInfo (PTerm' nm) -> Core (PiInfo (PTerm' nm))
     goPiInfo (DefImplicit t) = DefImplicit <$> goPTerm t
@@ -402,7 +400,7 @@ mapPTermM f = goPTerm where
 
     goPFields : List (PField' nm) -> Core (List (PField' nm))
     goPFields []        = pure []
-    goPFields (f :: fs) = (::) <$> goPField f <*> goPFields fs
+    goPFields (f :: fs) = (::) <$> traverseFC goRecordField f <*> goPFields fs
 
     goPFnOpts : List (PFnOpt' nm) -> Core (List (PFnOpt' nm))
     goPFnOpts []        = pure []
@@ -563,7 +561,8 @@ mapPTerm f = goPTerm where
       = PImplementation fc v opts p (goImplicits is) (goPairedPTerms cs)
            n (goPTerm <$> ts) mn ns (map (goPDecl <$>) mps)
     goPDecl (PRecord fc doc v tot (MkPRecord n nts opts mn fs))
-      = PRecord fc doc v tot (MkPRecord n (go4TupledPTerms nts) opts mn (goPField <$> fs))
+      = PRecord fc doc v tot
+          (MkPRecord n (go4TupledPTerms nts) opts mn (map (mapFC goRecordField) fs))
     goPDecl (PRecord fc doc v tot (MkPRecordLater n nts))
       = PRecord fc doc v tot (MkPRecordLater n (go4TupledPTerms nts))
     goPDecl (PFail fc msg ps) = PFail fc msg $ goPDecl <$> ps
@@ -588,11 +587,9 @@ mapPTerm f = goPTerm where
     goPRecordDeclLet (RecordClaim claim) = RecordClaim $ mapFC goPClaim claim
     goPRecordDeclLet (RecordClause clause) = RecordClause $ mapFC goPClause clause
 
-    goPField : PField' nm -> PField' nm
-    goPField (MkField fc doc c info n t)
-      = MkField fc doc c (goPiInfo info) n (goPTerm t)
-    goPField (MkRecordLet decls)
-      = MkRecordLet $ mapFC (map goPRecordDeclLet) decls
+    goRecordField : RecordField' nm -> RecordField' nm
+    goRecordField (MkRecordField doc c info n t)
+      = MkRecordField doc c (goPiInfo info) n (goPTerm t)
 
     goPiInfo : PiInfo (PTerm' nm) -> PiInfo (PTerm' nm)
     goPiInfo (DefImplicit t) = DefImplicit $ goPTerm t