A much better implementation of implicit generalization:

- Do it after internalisation (esp. after notation expansion)
- Generalize it to any constr, not just typeclasses
- Prepare for having settings on the implicit status of generalized
variables (currently only impl,impl and expl,expl are supported).
- Simplified implementation! (Still some refactoring needed in
typeclasses parsing code).
This patch contains a fix for bug #1964 as well.


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

4 files changed, 25 insertions, 17 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 740ba0b343..5f729762f0 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -399,11 +399,11 @@ GEXTEND Gram
     | "{"; id=name; idl=LIST1 name; "}" -> 
         List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
     | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Explicit, b), t)) tc
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Explicit, Explicit, b), t)) tc
     | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
-    | "["; tc = LIST1 typeclass_constraint SEP ","; "]" -> 
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+    | "["; tc = LIST1 typeclass_constraint SEP ","; "]" ->
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
     ] ]
   ;
   binder:
@@ -413,13 +413,13 @@ GEXTEND Gram
     ] ]
   ;
   typeclass_constraint:
-    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c
-      | "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), true, c
+      | "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
 	  id, expl, c
-      | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+      | iid=ident_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
 	  (loc, Name iid), expl, c
       | c = operconstr LEVEL "200" ->
-	  (loc, Anonymous), Implicit, c
+	  (loc, Anonymous), false, c
     ] ]
   ;
   
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d1c062e117..fa8c2a6f5a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -166,7 +166,7 @@ module Constr :
     val binder_let : local_binder list Gram.Entry.e
     val binders_let : local_binder list Gram.Entry.e
     val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
-    val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
+    val typeclass_constraint : (name located * bool * constr_expr) Gram.Entry.e
     val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
   end
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index e906fb3983..239d3772f0 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -205,17 +205,23 @@ let begin_of_binders = function
   | b::_ -> begin_of_binder b
   | _ -> 0
 
-let surround_binder k p = 
+let surround_impl k p = 
   match k with
-      Default Explicit -> hov 1 (str"(" ++ p ++ str")")
-    | Default Implicit -> hov 1 (str"{" ++ p ++ str"}")
-    | TypeClass _ -> hov 1 (str"[" ++ p ++ str"]")
+  | Explicit -> str"(" ++ p ++ str")"
+  | Implicit -> str"{" ++ p ++ str"}"
 
+let surround_binder k p = 
+  match k with
+  | Default b -> hov 1 (surround_impl b p)
+  | Generalized (b, b', t) -> 
+      hov 1 (surround_impl b' (surround_impl b p))
+	
 let surround_implicit k p =
   match k with
-      Default Explicit -> p
-    | Default Implicit -> (str"{" ++ p ++ str"}")
-    | TypeClass _ -> (str"[" ++ p ++ str"]")
+  | Default Explicit -> p
+  | Default Implicit -> (str"{" ++ p ++ str"}")
+  | Generalized (b, b', t) -> 
+      surround_impl b' (surround_impl b p)
 
 let pr_binder many pr (nal,k,t) =
   match t with
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 8407211f10..1a5e7fb726 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -140,7 +140,9 @@ let mlexpr_of_binding_kind = function
 
 let mlexpr_of_binder_kind = function
   | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >>
-  | Topconstr.TypeClass (b,b') -> <:expr< Topconstr.TypeClass $mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_binding_kind (b,b')$ >>
+  | Topconstr.Generalized (b,b',b'') -> 
+      <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$
+	$mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >>
 
 let rec mlexpr_of_constr = function
   | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->