Generalized implementation of generalization.

- New constr_expr construct [CGeneralization of loc * binding_kind *
abstraction_kind option * constr_expr] to generalize the free vars of
the [constr_expr], binding these using [binding_kind] and making
a lambda or a pi (or deciding from the scope) using [abstraction_kind
option] (abstraction_kind = AbsLambda | AbsPi)
- Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{
... }" for implicit bindings (both "..(" and "_(" seem much more
difficult to implement). Subject to discussion! A few examples added
in a test-suite file.
- Also add missing syntax for implicit/explicit combinations for
_binders_: "{( )}" means implicit for the generalized (outer) vars,
explicit for the (inner) variable itself. Subject to discussion as well :)
- Factor much typeclass instance declaration code. We now just have to
force generalization of the term after the : in instance declarations.
One more step to using Instance for records.


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

2 files changed, 21 insertions, 2 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 5f729762f0..77b4f003cd 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -24,7 +24,8 @@ open Util
 let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; 
     "end"; "as"; "let"; "if"; "then"; "else"; "return";
-    "Prop"; "Set"; "Type"; ".("; "_"; ".." ]
+    "Prop"; "Set"; "Type"; ".("; "_"; "..";
+    "`{"; "`("; ]
 
 let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
 
@@ -203,7 +204,12 @@ GEXTEND Gram
           (match c with
               CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
                 CNotation(loc,"( _ )",([c],[]))
-            | _ -> c) ] ]
+            | _ -> c)
+      | "`{"; c = operconstr LEVEL "200"; "}" ->
+	  CGeneralization (loc, Implicit, None, c)
+      | "`("; c = operconstr LEVEL "200"; ")" ->
+	  CGeneralization (loc, Explicit, None, c)
+      ] ]
   ;
   forall: 
     [ [ "forall" -> () 
@@ -400,8 +406,12 @@ GEXTEND Gram
         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], Generalized (Explicit, Explicit, b), t)) tc
+    | "{"; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; "}" ->
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
     | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" ->
 	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 (Explicit, Implicit, b), t)) tc
     | "["; tc = LIST1 typeclass_constraint SEP ","; "]" ->
 	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
     ] ]
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 239d3772f0..a2cad8e170 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -92,6 +92,14 @@ let pr_notation pr s env =
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
+let pr_generalization bk ak c =
+  let hd, tl =
+    match bk with 
+    | Implicit -> "{", "}"
+    | Explicit -> "(", ")"
+  in (* TODO: syntax Abstraction Kind *) 
+    str "`" ++ str hd ++ c ++ str tl
+
 let pr_com_at n =
   if Flags.do_translate() && n <> 0 then comment n 
   else mt()
@@ -597,6 +605,7 @@ let rec pr sep inherited a =
   | CNotation (_,"( _ )",([t],[])) ->
       pr (fun()->str"(") (max_int,L) t ++ str")", latom
   | CNotation (_,s,env) -> pr_notation (pr mt) s env
+  | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom
   | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
   | CDynamic _ -> str "<dynamic>", latom