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, 54 insertions, 1 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 46e33360c..320bac830 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -212,6 +212,7 @@ let rec is_rec names =
     | RRef _ | REvar _ | RPatVar _ | RSort _ |  RHole _ | RDynamic _ -> false
     | RCast(_,b,_) -> lookup names b
     | RRec _ -> error "RRec not handled"
+    | RRecord _ -> error "Not handled RRecord"
     | RIf(_,b,_,lhs,rhs) -> 
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
     | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b)  -> 
@@ -612,6 +613,7 @@ let rec add_args id new_args b =
       CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
   | CCast(loc,b1,CastCoerce) ->
       CCast(loc,add_args id new_args b1,CastCoerce)
+  | CRecord _ -> anomaly "add_args : CRecord"
   | CNotation _ -> anomaly "add_args : CNotation"
   | CGeneralization _ -> anomaly "add_args : CGeneralization"
   | CPrim _ -> b
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 08a97fd22..7534ce2ca 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -583,6 +583,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 		*)
 		build_entry_lc env funnames avoid (mkRApp(b,args))
 	    | RRec _ -> error "Not handled RRec"
+	    | RRecord _ -> error "Not handled RRecord"
 	    | RProd _ -> error "Cannot apply a type"
 	end (* end of the application treatement *) 
 
@@ -685,6 +686,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 
 	end
     | RRec _ -> error "Not handled RRec"
+    | RRecord _ -> error "Not handled RRecord"
     | RCast(_,b,_) -> 
 	build_entry_lc env funnames  avoid b
     | RDynamic _ -> error "Not handled RDynamic"
@@ -1024,7 +1026,7 @@ let rec compute_cst_params relnames params = function
 		 discriminitation ones *)
   | RSort _ -> params
   | RHole _ -> params
-  | RIf _ | RRec _ | RCast _ | RDynamic _  ->
+  | RIf _ | RRecord _ | RRec _ | RCast _ | RDynamic _  ->
       raise (UserError("compute_cst_params", str "Not handled case"))
 and compute_cst_params_from_app acc (params,rtl) = 
   match params,rtl with 
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 92396af59..ffd7cd007 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -176,6 +176,7 @@ let change_vars =
 	      change_vars mapping lhs,
 	      change_vars mapping rhs
 	     )
+      | RRecord _ -> error "Records are not supported"
       | RRec _ -> error "Local (co)fixes are not supported"
       | RSort _ -> rt 
       | RHole _ -> rt 
@@ -358,6 +359,7 @@ let rec alpha_rt excluded rt =
 	    alpha_rt excluded rhs
 	   )
     | RRec _ -> error "Not handled RRec"
+    | RRecord _ -> error "Not handled RRecord"
     | RSort _ -> rt 
     | RHole _ -> rt 
     | RCast (loc,b,CastConv (k,t)) -> 
@@ -409,6 +411,7 @@ let is_free_in id =
 	  
     | RIf(_,cond,_,br1,br2) ->
 	is_free_in cond || is_free_in br1 || is_free_in br2
+    | RRecord _ -> raise (UserError ("", str "Not handled RRecord"))
     | RRec _ -> raise (UserError("",str "Not handled RRec"))
     | RSort _ -> false
     | RHole _ -> false
@@ -507,6 +510,7 @@ let replace_var_by_term x_id term =
 	      replace_var_by_pattern rhs
 	     )
       | RRec _ -> raise (UserError("",str "Not handled RRec"))
+      | RRecord _ -> raise (UserError("",str "Not handled RRecord"))
       | RSort _ -> rt 
       | RHole _ -> rt 
       | RCast(loc,b,CastConv(k,t)) -> 
@@ -604,6 +608,8 @@ let ids_of_rawterm c =
       | RCases (loc,sty,rtntypopt,tml,brchl) -> 
 	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
       | RRec _ -> failwith "Fix inside a constructor branch"
+      | RRecord (loc,w,l) -> Option.cata (ids_of_rawterm []) [] w @ 
+	  List.flatten (List.map (fun ((_,id), x) -> id :: ids_of_rawterm [] x) l)
       | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> []
   in
   (* build the set *)
@@ -661,6 +667,7 @@ let zeta_normalize =
 	      zeta_normalize_term lhs,
 	      zeta_normalize_term rhs
 	     )
+      | RRecord _ -> raise (UserError("",str "Not handled RRecord"))
       | RRec _ -> raise (UserError("",str "Not handled RRec"))
       | RSort _ -> rt 
       | RHole _ -> rt 
@@ -705,6 +712,7 @@ let expand_as =
       | RIf(loc,e,(na,po),br1,br2) ->
 	  RIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
+      | RRecord _ ->  error "Not handled RRecord"
       | RRec _ ->  error "Not handled RRec"
       | RDynamic _ -> error "Not handled RDynamic"
       | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 203bc9e3d..e7c6c5bcb 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -210,6 +210,8 @@ let rec depends_of_rawconstr rc acc = match rc with
   | RLambda (_, _, _, rct, rcb)
   | RProd   (_, _, _, rct, rcb)
   | RLetIn  (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc)
+  | RRecord (_, w, l) -> depends_of_rawconstr_list (List.map snd l)
+      (Option.fold_right depends_of_rawconstr w acc)
   | RCases  (_, _, rco, tmt, cc) ->
       (* LEM TODO: handle the cc *)
       (Option.fold_right depends_of_rawconstr rco
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 8201e8fdc..3c32c4068 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -501,6 +501,45 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    { uj_val = v; uj_type = p }
 
+    | RRecord (loc,w,l) ->
+	let cw = Option.map (pretype tycon env isevars 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 !isevars) cj.uj_type
+	    with Not_found ->
+	      error_case_not_inductive_loc loc env (evars_of !isevars) 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 isevars lvar constructor
+
     | RCases (loc,sty,po,tml,eqns) ->
 	Cases.compile_cases loc sty
 	  ((fun vtyc env isevars -> pretype vtyc env isevars lvar),isevars)