Open notation for declaring record instances.

It solves feature request 1852, makes me and Arnaud happy and 
will permit to factor some more code in typeclasses.
- Records are introduced using the syntax "{| x := t; y := foo |}" and
"with" clauses are currently parsed but not yet supported in the
elaboration. You are invited to suggest other syntaxes :)
- Missing fields are turned into holes, extra fields cause an error
message. The current implementation finds the type of the record
at pretyping time, from the typing constraint alone (and just expects
an inductive with one constructor). It is then impossible to use
scope information to parse the bodies: that may be wrong. The other
solution I see is using the fields to detect the type earlier, before
internalisation of the bodies, but then we get in name clash hell.
- In funind/contrib/interface I mostly put [assert false] everywhere to 
avoid warnings.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11496 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 23 insertions, 1 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 77b4f003c..5ecbab90e 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -25,7 +25,7 @@ let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; 
     "end"; "as"; "let"; "if"; "then"; "else"; "return";
     "Prop"; "Set"; "Type"; ".("; "_"; "..";
-    "`{"; "`("; ]
+    "`{"; "`("; "{|"; "|}" ]
 
 let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
 
@@ -125,6 +125,18 @@ let ident_colon =
               | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
+let ident_with =
+  Gram.Entry.of_parser "ident_with"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+      | [("IDENT",s)] ->
+          (match Stream.npeek 2 strm with
+          | [_; ("", "with")] ->
+              Stream.junk strm; Stream.junk strm;
+              Names.id_of_string s
+          | _ -> raise Stream.Failure)
+      | _ -> raise Stream.Failure)
+    
 let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
 
 GEXTEND Gram
@@ -205,6 +217,7 @@ GEXTEND Gram
               CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
                 CNotation(loc,"( _ )",([c],[]))
             | _ -> c)
+      | "{|"; c = record_declaration; "|}" -> c
       | "`{"; c = operconstr LEVEL "200"; "}" ->
 	  CGeneralization (loc, Implicit, None, c)
       | "`("; c = operconstr LEVEL "200"; ")" ->
@@ -221,6 +234,15 @@ GEXTEND Gram
     | IDENT "λ" -> ()
     ] ]
   ;
+  record_declaration:
+    [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs)
+      | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" ->
+	  CRecord (loc, Some c, fs)
+    ] ]
+  ;
+  record_field_declaration:
+    [ [ id = identref; ":="; c = lconstr -> (id, c) ] ]
+  ;
   binder_constr:
     [ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" ->
           mkCProdN loc bl c