labels for record fields; documentation

doc/theory.bnf

@@ -11,6 +11,28 @@
     | "clone" imp-exp tqualid ("as" uident-opt)? subst? ;	   
     | "namespace" "import"? uident-opt decl* "end" ;
   \
+  type-decl ::= lident label* ("'" lident label*)* type-defn;
+  \
+  type-defn ::=                                      ; abstract type
+    | "=" type                                       ; alias type
+    | "=" "|"? type-case ("|" type-case)*            ; algebraic type
+    | "=" "{|" record-field (";" record-field)* "|}" ; record type
+  \
+  type-case ::= uident label* type-param*
+  \
+  record-field ::= lident label* ":" type
+  \
+  logic-decl ::= lident label* type-param* ":" type ;
+    | lident label* type-param* ":" type "=" term   ;
+    | lident label* type-param*                     ;
+    | lident label* type-param* "=" formula
+  \
+  type-param ::= "'" lident   ;
+   | lqualid                  ;
+   | "(" lident+ ":" type ")" ;
+   | "(" type ("," type)* ")" ;
+   | "()"
+  \
   imp-exp ::= ("import" | "export")?
   \
   uident-opt ::= uident | "_"

src/parser/parser.pre.mly

@@ -406,8 +406,8 @@ list1_record_field:
 ;
 
 record_field:
-| opt_mutable lident COLON primitive_type 
-   { loc (), $1, $2, $4 }
+| opt_mutable lident labels COLON primitive_type 
+   { loc (), $1, add_lab $2 $3, $5 }
 ;
 
 typecases: