Merge pull request #2192 from mateuszbujalski/matbuj_record_field_att…

…ributes

Allow attributes on record fields

CHANGES.md

@@ -147,6 +147,10 @@ Guidelines for the changelog:
      a semicolon separated list of terms. The old syntax will soon
      be deprecated.
 
+   * Attributes on binders are now using a different syntax `[@@@ a1; ... ; an]` i.e., 
+     @@@ instead of @@. This is a breaking change that enables 
+     using attributes on explicit binders, record fields and more. See 
+     https://github.com/FStarLang/FStar/pull/2192 for more details. 
 
 ## Extraction
 

src/parser/FStar.Parser.AST.fs

@@ -139,7 +139,7 @@ type expr = term
 type tycon =
   | TyconAbstract of ident * list<binder> * option<knd>
   | TyconAbbrev   of ident * list<binder> * option<knd> * term
-  | TyconRecord   of ident * list<binder> * option<knd> * list<(ident * term)>
+  | TyconRecord   of ident * list<binder> * option<knd> * list<(ident * aqual * attributes_ * term)>
   | TyconVariant  of ident * list<binder> * option<knd> * list<(ident * option<term> * bool)> (* bool is whether it's using 'of' notation *)
 
 type qualifier =

src/parser/FStar.Parser.Dep.fs

@@ -776,7 +776,10 @@ let collect_one
         | TyconRecord (_, binders, k, identterms) ->
             collect_binders binders;
             iter_opt k collect_term;
-            List.iter (fun (_, t) -> collect_term t) identterms
+            List.iter (fun (_, aq, attrs, t) -> 
+                collect_aqual aq;
+                attrs |> List.iter collect_term;
+                collect_term t) identterms
         | TyconVariant (_, binders, k, identterms) ->
             collect_binders binders;
             iter_opt k collect_term;

src/parser/FStar.Parser.ToDocument.fs

@@ -787,9 +787,9 @@ and p_typeDecl pre = function
     let comm, doc = p_typ_sep false false t in
     comm, p_typeDeclPrefix pre true lid bs typ_opt, doc, jump2
   | TyconRecord (lid, bs, typ_opt, record_field_decls) ->
-    let p_recordField (ps: bool) (lid, t) =
+    let p_recordField (ps: bool) (lid, aq, attrs, t) =
       let comm, field =
-        with_comment_sep (p_recordFieldDecl ps) (lid, t)
+        with_comment_sep (p_recordFieldDecl ps) (lid, aq, attrs, t)
                          (extend_to_end_of_line t.range) in
       let sep = if ps then semi else empty in
       inline_comment_or_above comm field sep
@@ -829,8 +829,8 @@ and p_typeDeclPrefix kw eq lid bs typ_opt =
     let binders = p_binders_list true bs in
     with_kw (fun n -> prefix2 (prefix2 n (flow break1 binders)) typ)
 
-and p_recordFieldDecl ps (lid, t) =
-  group (p_lident lid ^^ colon ^^ p_typ ps false t)
+and p_recordFieldDecl ps (lid, aq, attrs, t) =
+  group (optional p_aqual aq ^^ p_attributes attrs ^^ p_lident lid ^^ colon ^^ p_typ ps false t)
 
 and p_constructorBranch (uid, t_opt, use_of) =
   let sep = if use_of then str "of" else colon in

src/parser/lex.fsl

@@ -354,6 +354,7 @@ rule token args = parse
      }
 
  | "///[@"
+ | "[@@@"       { LBRACK_AT_AT_AT }  
  | "[@@"       { LBRACK_AT_AT } 
  | "[@"        { LBRACK_AT }
  | "//"  [^'\n''\r']*

src/parser/ml/FStar_Parser_LexFStar.ml

@@ -168,6 +168,7 @@ let () =
    "=", EQUALS;
    "%[", PERCENT_LBRACK;
    "!{", BANG_LBRACE;
+   "[@@@", LBRACK_AT_AT_AT;
    "[@@", LBRACK_AT_AT;
    "[@", LBRACK_AT;
    "[", LBRACK;
@@ -383,7 +384,7 @@ let regexp op_token =
   "u#" | "&" | "()" | "(" | ")" | "," | "~>" | "->" | "<--" |
   "<-" | "<==>" | "==>" | "." | "?." | "?" | ".[|" | ".[" | ".(|" | ".(" |
   "$" | "{:pattern" | ":" | "::" | ":=" | ";;" | ";" | "=" | "%[" |
-  "!{" | "[@@" | "[@" | "[|" | "{|" | "[" | "|>" | "]" | "|]" | "|}" | "{" | "|" | "}"
+  "!{" | "[@@@" | "[@@" | "[@" | "[|" | "{|" | "[" | "|>" | "]" | "|]" | "|}" | "{" | "|" | "}"
 
 (* -------------------------------------------------------------------- *)
 let regexp xinteger =