From 57cb1648fcf7da18d74c28a4d63d59ea129ab136 Mon Sep 17 00:00:00 2001 From: msozeau Date: Thu, 23 Oct 2008 12:49:34 +0000 Subject: 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 --- toplevel/classes.ml | 75 +++++++++------------------------------------------- toplevel/classes.mli | 8 +----- 2 files changed, 13 insertions(+), 70 deletions(-) (limited to 'toplevel') diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 301f9bf2a4..4e87109187 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 970f3e2abd..4f20f1649c 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 -> -- cgit v1.2.3