Generalize instance declarations to any context, better name handling. Add hole kind info for topconstrs.

Derive eta_expansion from functional extensionality axiom.


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

7 files changed, 55 insertions, 30 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index bd6c15ffaa..e55024b516 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -55,7 +55,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
   let n,ro = index_and_rec_order_of_annot (fst id) bl ann in
   let ty = match tyc with
       Some ty -> ty
-    | None -> CHole loc in
+    | None -> CHole (loc, None) in
   (snd id,(n,ro),bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
@@ -65,7 +65,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
        Pp.str"Annotation forbidden in cofix expression")) (fst ann) in
   let ty = match tyc with
       Some ty -> ty
-    | None -> CHole loc in
+    | None -> CHole (loc, None) in
   (snd id,bl,ty,body)
 
 let mk_fix(loc,kw,id,dcls) =
@@ -102,7 +102,7 @@ let lpar_id_coloneq =
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
-  binder binder_let binders_let typeclass_constraint pattern;
+  binder binder_let binders_let delimited_binder_let delimited_binders_let typeclass_constraint pattern;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -222,7 +222,7 @@ GEXTEND Gram
       | s=sort -> CSort (loc,s)
       | n=INT -> CPrim (loc, Numeral (Bigint.of_string n))
       | s=string -> CPrim (loc, String s)
-      | "_" -> CHole loc
+      | "_" -> CHole (loc, None)
       | id=pattern_ident -> CPatVar(loc,(false,id)) ] ]
   ;
   fix_constr:
@@ -311,33 +311,59 @@ GEXTEND Gram
   ;
   binder_list:
     [ [ idl=LIST1 name; bl=LIST0 binder_let -> 
-          LocalRawAssum (idl,Default Explicit,CHole loc)::bl
+          LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl
       | idl=LIST1 name; ":"; c=lconstr -> 
           [LocalRawAssum (idl,Default Explicit,c)]
       | cl = binders_let -> cl
     ] ]
   ;
+  delimited_binders_let: 
+    [ [ "["; ctx = LIST1 typeclass_constraint_binder SEP ","; "]"; bl=binders_let -> 
+	  ctx @ bl
+    | b = delimited_binder_let; cl = LIST0 binder_let -> b :: cl
+    | -> [] ] ]
+  ;
   binders_let: 
     [ [ "["; ctx = LIST1 typeclass_constraint_binder SEP ","; "]"; bl=binders_let -> 
 	  ctx @ bl
-    | cl = LIST0 binder_let -> cl
-    ] ]
+    | cl = LIST0 binder_let -> cl ] ]
   ;
   binder_let:
     [ [ id=name ->
-          LocalRawAssum ([id],Default Explicit,CHole loc)
+          LocalRawAssum ([id],Default Explicit,CHole (loc, None))
       | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> 
           LocalRawAssum (id::idl,Default Explicit,c)
       | "("; id=name; ":"; c=lconstr; ")" -> 
           LocalRawAssum ([id],Default Explicit,c)
       | "`"; id=name; "`" ->
-          LocalRawAssum ([id],Default Implicit,CHole loc)
+          LocalRawAssum ([id],Default Implicit,CHole (loc, None))
+      | "`"; id=name; idl=LIST1 name; ":"; c=lconstr; "`" -> 
+          LocalRawAssum (id::idl,Default Implicit,c)
+      | "`"; id=name; ":"; c=lconstr; "`" -> 
+          LocalRawAssum ([id],Default Implicit,c)
+      | "`"; id=name; idl=LIST1 name; "`" -> 
+          LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))
+      | "("; id=name; ":="; c=lconstr; ")" ->
+          LocalRawDef (id,c)
+      | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
+          LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))
+      | "["; tc = typeclass_constraint_binder; "]" -> tc
+    ] ]
+(*     | b = delimited_binder_let -> b ] ] *)
+  ;
+  delimited_binder_let:
+    [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> 
+          LocalRawAssum (id::idl,Default Explicit,c)
+      | "("; id=name; ":"; c=lconstr; ")" -> 
+          LocalRawAssum ([id],Default Explicit,c)
+      | "`"; id=name; "`" ->
+          LocalRawAssum ([id],Default Implicit,CHole (loc, None))
       | "`"; id=name; idl=LIST1 name; ":"; c=lconstr; "`" -> 
           LocalRawAssum (id::idl,Default Implicit,c)
       | "`"; id=name; ":"; c=lconstr; "`" -> 
           LocalRawAssum ([id],Default Implicit,c)
       | "`"; id=name; idl=LIST1 name; "`" -> 
-          LocalRawAssum (id::idl,Default Implicit,CHole loc)
+          LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))
       | "("; id=name; ":="; c=lconstr; ")" ->
           LocalRawDef (id,c)
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
@@ -346,7 +372,7 @@ GEXTEND Gram
     ] ]
   ;
   binder:
-    [ [ id=name -> ([id],Default Explicit,CHole loc)
+    [ [ id=name -> ([id],Default Explicit,CHole (loc, None))
       | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) 
       | "`"; idl=LIST1 name; ":"; c=lconstr; "`" -> (idl,Default Implicit,c) 
     ] ]
@@ -358,11 +384,11 @@ GEXTEND Gram
     ] ]
   ;
   typeclass_constraint:
-    [ [ id=identref ; cl = LIST1 typeclass_param -> 
+    [ [ id=identref ; cl = LIST0 typeclass_param -> 
       (loc, Anonymous), Explicit, CApp (loc, (None, mkIdentC (snd id)), cl)
-    | "?" ; id=identref ; cl = LIST1 typeclass_param -> 
+    | "?" ; id=identref ; cl = LIST0 typeclass_param -> 
 	(loc, Anonymous), Implicit, CApp (loc, (None, mkIdentC (snd id)), cl)
-    | iid=identref ; ":" ; id=typeclass_name ; cl = LIST1 typeclass_param -> 
+    | iid=identref ; ":" ; id=typeclass_name ; cl = LIST0 typeclass_param -> 
 	(fst iid, Name (snd iid)), (fst id), CApp (loc, (None, mkIdentC (snd (snd id))), cl)
     ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 540d1aac0b..b69a6a97ac 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -286,7 +286,7 @@ GEXTEND Gram
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> c 
-      | -> CHole loc ] ]
+      | -> CHole (loc, None) ] ]
   ;
   (* Inductive schemes *)
   scheme:
@@ -314,7 +314,7 @@ GEXTEND Gram
 *)
   (* ... with coercions *)
   record_field:
-    [ [ id = name -> (false,AssumExpr(id,CHole loc))
+    [ [ id = name -> (false,AssumExpr(id,CHole (loc, None)))
       | id = name; oc = of_type_with_opt_coercion; t = lconstr ->
          (oc,AssumExpr (id,t))
       | id = name; oc = of_type_with_opt_coercion;
@@ -339,7 +339,7 @@ GEXTEND Gram
         coe = of_type_with_opt_coercion; c = lconstr ->
 	  (coe,(id,mkCProdN loc l c))
       | id = identref; l = LIST0 binder_let ->
-	  (false,(id,mkCProdN loc l (CHole loc))) ] ]
+	  (false,(id,mkCProdN loc l (CHole (loc, None)))) ] ]
   ;
   of_type_with_opt_coercion:
     [ [ ":>" -> true
@@ -479,7 +479,7 @@ GEXTEND Gram
 	   VernacClass (qid, pars, s, [], props)
 
       (* Type classes *)
-      | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
+      | IDENT "Class"; sup = OPT [ l = delimited_binders_let; "=>" -> l ];
 	 qid = identref; pars = binders_let;
 	 s = [ ":"; c = sort -> loc, c | -> (loc,Rawterm.RType None) ];
 	 props = typeclass_field_types ->
@@ -488,7 +488,7 @@ GEXTEND Gram
       | IDENT "Context"; c = typeclass_context -> 
 	  VernacContext c
 
-      | IDENT "Instance"; sup = OPT [ l = typeclass_context ; "=>" -> l ];
+      | IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ];
 	 is = typeclass_constraint ; props = typeclass_field_defs ->
 	   let sup = match sup with None -> [] | Some l -> l in
 	     VernacInstance (sup, is, props)
@@ -525,7 +525,7 @@ GEXTEND Gram
   ;
 (*   typeclass_param_type: *)
 (*     [ [ "(" ; id = identref; ":"; t = lconstr ; ")" -> id, t  *)
-(*     | id = identref -> id, CHole loc ] ] *)
+(*     | id = identref -> id, CHole (loc, None) ] ] *)
 (*   ; *)
   typeclass_field_type:
     [ [ id = identref; ":"; t = lconstr -> id, t ] ]
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 2430b88636..68ddc19292 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -434,7 +434,9 @@ module Constr =
     let lconstr_pattern = gec_constr "lconstr_pattern"
     let binder = Gram.Entry.create "constr:binder"
     let binder_let = Gram.Entry.create "constr:binder_let"
+    let delimited_binder_let = Gram.Entry.create "constr:delimited_binder_let"
     let binders_let = Gram.Entry.create "constr:binders_let"
+    let delimited_binders_let = Gram.Entry.create "constr:delimited_binders_let"
     let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
   end
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 89bdf13ebd..d5cffd35bd 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -163,7 +163,9 @@ module Constr :
     val lconstr_pattern : constr_expr Gram.Entry.e
     val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e
     val binder_let : local_binder Gram.Entry.e
+    val delimited_binder_let : local_binder Gram.Entry.e
     val binders_let : local_binder list Gram.Entry.e
+    val delimited_binders_let : local_binder list Gram.Entry.e
     val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
   end
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index ed4386ada0..8dff6dbf53 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -239,7 +239,7 @@ let pr_binder_among_many pr_c = function
   | LocalRawDef (na,c) ->
       let c,topt = match c with
         | CCast(_,c, CastConv (_,t)) -> c, t
-        | _ -> c, CHole dummy_loc in
+        | _ -> c, CHole (dummy_loc, None) in
       hov 1 (pr_lname na ++ pr_opt_type pr_c topt ++
          str":=" ++ cut() ++ pr_c c)
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0b889bf08d..e2653a9606 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -263,7 +263,7 @@ let rec pr_module_expr = function
       hov 1 (str"(" ++ pr_module_expr me2 ++ str")")
 
 let pr_type_option pr_c = function
-  | CHole loc -> mt()
+  | CHole (loc, k) -> mt()
   | _ as c -> brk(0,2) ++ str":" ++ pr_c c
 
 let pr_decl_notation prc =
@@ -399,12 +399,6 @@ let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in
 let pr_lname_lident_constr (oi,bk,a) = 
   (match snd oi with Anonymous -> mt () | Name id -> pr_lident (fst oi, id) ++ spc () ++ str":" ++ spc ()) 
   ++ pr_lconstr a in
-let pr_typeclass_context l = 
-  match l with
-      [] -> mt ()
-    | _ -> str"[" ++ spc () ++ prlist_with_sep (fun () -> str"," ++ spc()) pr_lname_lident_constr l
-	++ spc () ++ str"]" ++ spc ()
-in
 let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l 
   ++ sep ++ pr_constrarg c in
 
@@ -706,7 +700,7 @@ let rec pr_vernac = function
  | VernacInstance (sup, (instid, bk, cl), props) -> 
      hov 1 (
        str"Instance" ++ spc () ++ 
-	 pr_typeclass_context sup ++
+	 pr_and_type_binders_arg sup ++
 	 str"=>" ++ spc () ++ 
 	 (match snd instid with Name id -> pr_lident (fst instid, id) ++ spc () ++ str":" ++ spc () | Anonymous -> mt ()) ++
 	 pr_constr_expr cl ++ spc () ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6fdfba23d3..26dff3927a 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -154,7 +154,8 @@ let rec mlexpr_of_constr = function
   | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
   | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
   | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >>
+  | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >>
+  | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
   | Topconstr.CNotation(_,ntn,l) ->
       <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$
                 $mlexpr_of_list mlexpr_of_constr l$ >>