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, 13 insertions, 70 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 301f9bf2a..4e8710918 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -270,17 +270,6 @@ let type_ctx_instance isevars env ctx inst subst =
       (subst, []) (List.rev ctx) inst
   in s
 
-(* let type_ctx_instance isevars env ctx inst subst = *)
-(*   let (s, _, _) =  *)
-(*     List.fold_left2 *)
-(*       (fun (s, env, n) (na, _, t) ce -> *)
-(* 	let t' = substnl subst n t in *)
-(* 	let c = interp_casted_constr_evars isevars env ce t' in *)
-(* 	let d = na, Some c, t' in *)
-(* 	  (substl s c :: s, push_rel d env, succ n)) *)
-(*       ([], env, 0) (List.rev ctx) inst *)
-(*   in s @ subst *)
-
 let refine_ref = ref (fun _ -> assert(false))
 
 let id_of_class cl =
@@ -294,23 +283,6 @@ let id_of_class cl =
 open Pp
 
 let ($$) g f = fun x -> g (f x)
-
-let default_on_free_vars =
-  Flags.if_verbose
-    (fun fvs ->
-      match fvs with
-	  [] -> ()
-	| l -> msgnl (str"Implicitly generalizing " ++ 
-			 prlist_with_sep (fun () -> str", ") Nameops.pr_id l ++ str"."))
-
-let fail_on_free_vars = function
-    [] -> ()
-  | [fv] ->
-      errorlabstrm "Classes" 
-	(str"Unbound variable " ++ Nameops.pr_id fv ++ str".")
-  | fvs -> errorlabstrm "Classes" 
-      (str"Unbound variables " ++
-	  prlist_with_sep (fun () -> str", ") Nameops.pr_id fvs ++ str".")
 	
 let instance_hook k pri global imps ?hook cst = 
   let inst = Typeclasses.new_instance k pri global cst in
@@ -333,47 +305,24 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
     instance_hook k pri global imps ?hook kn;
     id
 
-let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars) 
+let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
     ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
-  let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
-  let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in
   let tclass = 
     match bk with
-      | Implicit ->
-	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
-	  let k = class_info (Nametab.global id) in
-	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
-	  let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 (fst k.cl_context) in
-	    if needlen <> applen then 
-	      mismatched_params env (List.map fst par) (snd k.cl_context);
-	    let (ci, rd) = k.cl_context in
-	    let pars = List.rev (List.combine ci rd) in
-	    let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *)
-	      (fun avoid (clname, (id, _, t)) -> 
-		match clname with 
-		    Some (cl, b) -> 
-		      let t = 
-			if b then 
-			  let _k = class_info cl in
-			    CHole (Util.dummy_loc, Some (Evd.ImplicitArg (k.cl_impl, (1, None))))
-			else CHole (Util.dummy_loc, None)
-		      in t, avoid
-		  | None -> failwith ("new instance: under-applied typeclass"))
-	      par pars
-	    in Topconstr.CAppExpl (loc, (None, id), pars)
-
-      | Explicit -> cl
+    | Implicit ->
+	Implicit_quantifiers.implicit_application Idset.empty
+	  (fun avoid (clname, (id, _, t)) -> 
+	    match clname with 
+	    | Some (cl, b) -> 
+		let t = CHole (Util.dummy_loc, None) in
+		  t, avoid
+	    | None -> failwith ("new instance: under-applied typeclass"))
+	  cl
+    | Explicit -> cl
   in
-  let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in
-  let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in
-  on_free_vars (List.rev fvs @ List.rev gen_ids);
-  let gen_idset = Implicit_quantifiers.ids_of_list gen_ids in
-  let bound = Idset.union gen_idset ctx_bound in
-  let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in
-  let ctx, avoid = name_typeclass_binders bound ctx in
-  let ctx = List.append ctx (List.rev gen_ctx) in
+  let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, ctx', imps, subst = 
     let c = Command.generalize_constr_expr tclass ctx in
     let imps, c' = interp_type_evars isevars env c in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 970f3e2ab..4f20f1649 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -47,12 +47,6 @@ val new_class : identifier located ->
   local_binder list ->
   binder_list -> unit
 
-(* By default, print the free variables that are implicitely generalized. *)
-
-val default_on_free_vars : identifier list -> unit
-
-val fail_on_free_vars : identifier list -> unit
-
 (* Instance declaration *)
 
 val declare_instance : bool -> identifier located -> unit
@@ -73,7 +67,7 @@ val new_instance :
   local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
-  ?on_free_vars:(identifier list -> unit) ->
+  ?generalize:bool ->
   ?tac:Proof_type.tactic  ->
   ?hook:(constant -> unit) ->
   int option ->