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

3 files changed, 13 insertions, 1 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 46e33360cf..320bac8302 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 08a97fd221..7534ce2ca7 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 92396af590..ffd7cd007d 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))