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

5 files changed, 55 insertions, 2 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6854a4a7c5..eb4c737914 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -603,6 +603,12 @@ let rec subst_rawconstr subst raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  RLetIn (loc,n,r1',r2')
 
+  | RRecord (loc,w,rl) ->
+      let w' = Option.smartmap (subst_rawconstr subst) w 
+      and rl' = list_smartmap (fun (id, x) -> (id, subst_rawconstr subst x)) rl in
+	if w == w' && rl == rl' then raw else
+	  RRecord (loc,w',rl')
+
   | RCases (loc,sty,rtno,rl,branches) -> 
       let rtno' = Option.smartmap (subst_rawconstr subst) rtno
       and rl' = list_smartmap (fun (a,x as y) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 08ecae12e8..c114a922c0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -587,6 +587,45 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    { uj_val = v; uj_type = p }
 	
+    | RRecord (loc,w,l) ->
+	let cw = Option.map (pretype tycon env evdref lvar) w in
+	let cj = match cw with
+	  | None -> 
+	      (match tycon with
+	      | None -> user_err_loc (loc,"pretype",(str "Unnable to infer the record type."))
+	      | Some (_, ty) -> {uj_val=ty;uj_type=ty})
+	  | Some cj -> cj
+	in
+	let constructor = 
+	  let (IndType (indf,realargs)) = 
+	    try find_rectype env (evars_of !evdref) cj.uj_type
+	    with Not_found ->
+	      error_case_not_inductive_loc loc env (evars_of !evdref) cj
+	  in
+	  let cstrs = get_constructors env indf in 
+	    if Array.length cstrs <> 1 then 
+	      user_err_loc (loc,"pretype",(str "Inductive is not a singleton."))
+	    else
+	      let info = cstrs.(0) in
+	      let fields, rest = 
+		List.fold_left (fun (args, rest as acc) (na, b, t) ->
+		  if b = None then 
+		    try 
+		      let id = out_name na in
+		      let _, t = List.assoc id rest in
+			t :: args, List.remove_assoc id rest
+		    with _ -> RHole (loc, Evd.QuestionMark (Evd.Define false)) :: args, rest
+		  else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) l) info.cs_args
+	      in
+		if rest <> [] then 
+		  let id, (loc, t) = List.hd rest in
+		    user_err_loc (loc,"pretype",(str "Unknown field name " ++ pr_id id))
+		else
+		  RApp (loc,
+		       RDynamic (loc, constr_in (applistc (mkConstruct info.cs_cstr) info.cs_params)),
+		       fields)
+	in pretype tycon env evdref lvar constructor
+	  
     | RCases (loc,sty,po,tml,eqns) ->
 	Cases.compile_cases loc sty
 	  ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index ea622de7f4..b2e770f65a 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -62,6 +62,7 @@ type rawconstr =
   | RLambda of loc * name * binding_kind * rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
+  | RRecord of loc * rawconstr option * ((loc * identifier) * rawconstr) list
   | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
@@ -114,6 +115,7 @@ let map_rawconstr f = function
   | RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c)
   | RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c)
   | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
+  | RRecord (loc,c,l) -> RRecord (loc,Option.map f c,List.map (fun (id,c) -> id, f c) l)
   | RCases (loc,sty,rtntypopt,tml,pl) ->
       RCases (loc,sty,Option.map f rtntypopt,
         List.map (fun (tm,x) -> (f tm,x)) tml,
@@ -174,6 +176,8 @@ let occur_rawconstr id =
     | RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
+    | RRecord (loc,w,l) -> Option.cata occur false w
+	or List.exists (fun (_, c) -> occur c) l
     | RCases (loc,sty,rtntypopt,tml,pl) ->
 	(occur_option rtntypopt)
         or (List.exists (fun (tm,_) -> occur tm) tml)
@@ -219,7 +223,9 @@ let free_rawvars  =
     | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) -> 
 	let vs' = vars bounded vs ty in 
 	let bounded' = add_name_to_ids bounded na in 
-	vars bounded' vs' c
+       vars bounded' vs' c
+    | RRecord (loc,f,args) -> 
+	List.fold_left (vars bounded) vs (Option.List.cons f (List.map snd args))
     | RCases (loc,sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bounded vs rtntypopt in 
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in 
@@ -280,6 +286,7 @@ let loc_of_rawconstr = function
   | RLambda (loc,_,_,_,_) -> loc
   | RProd (loc,_,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
+  | RRecord (loc,_,_) -> loc
   | RCases (loc,_,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
   | RIf (loc,_,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 3628e2a503..5115e2d59b 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -66,6 +66,7 @@ type rawconstr =
   | RLambda of loc * name * binding_kind *  rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
+  | RRecord of loc * rawconstr option * ((loc * identifier) * rawconstr) list
   | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 97fbae075b..c437d9eab2 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -25,7 +25,7 @@ open Util
 (* This module defines type-classes *)
 type typeclass = {
   (* The class implementation: a record parameterized by the context with defs in it or a definition if 
-     the class is a singleton. This acts as the classe's global identifier. *)
+     the class is a singleton. This acts as the class' global identifier. *)
   cl_impl : global_reference; 
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses.