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, 8 insertions, 0 deletions

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))