diff options
author | 2015-07-31 18:45:41 +0200 | |
---|---|---|
committer | 2015-09-23 18:23:04 +0200 | |
commit | 13716dc6561a3379ba130f07ce7ecd1df379475c (patch) | |
tree | bcb347d50031561d16afa8430208d5deaf9cfdf8 | |
parent | 6459c0e8c240f0997873c50d4ec749effaba2f44 (diff) |
Give a way to control if the decidable-equality schemes are built like
in 8.4 with the schemes of the subcomponent of an inductive added to
the environment or discharged as let-ins over the main scheme.
As of today, decidable-equality schemes are built when calling
vernacular command (Inductive with option Set Dedicable Equality
Schemes, or Scheme Equality), so there is no need to discharge the
sub-schemes as let-ins. But if ever the schemes are built from within
an opaque proof and one would not like the schemes and a fortiori the
subschemes to appear in the env, the new addition of a parameter
internal_flag to "find_scheme" allows this possibility (then to be set
to KernelSilent).
-rw-r--r-- | tactics/elimschemes.ml | 20 | ||||
-rw-r--r-- | tactics/eqschemes.ml | 18 | ||||
-rw-r--r-- | toplevel/auto_ind_decl.ml | 42 | ||||
-rw-r--r-- | toplevel/ind_tables.ml | 32 | ||||
-rw-r--r-- | toplevel/ind_tables.mli | 15 |
5 files changed, 65 insertions, 62 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index e1c9c2de5..e6a8cbe3a 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -21,7 +21,7 @@ open Ind_tables (* Induction/recursion schemes *) -let optimize_non_type_induction_scheme kind dep sort ind = +let optimize_non_type_induction_scheme kind dep sort _ ind = let env = Global.env () in let sigma = Evd.from_env env in if check_scheme kind ind then @@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind = let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) let ind_scheme_kind_from_type = declare_individual_scheme_object "_ind_nodep" @@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 8643fe10f..f7d3ad5d0 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -191,7 +191,7 @@ let build_sym_scheme env ind = let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" - (fun ind -> + (fun _ ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in (c, ctx), Declareops.no_seff) @@ -262,7 +262,7 @@ let build_sym_involutive_scheme env ind = let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" - (fun ind -> + (fun _ ind -> build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind) (**********************************************************************) @@ -650,7 +650,7 @@ let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme (**********************************************************************) let rew_l2r_dep_scheme_kind = declare_individual_scheme_object "_rew_r_dep" - (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType) + (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType) (**********************************************************************) (* Dependent rewrite from right-to-left in conclusion *) @@ -660,7 +660,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -670,7 +670,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -680,7 +680,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -693,7 +693,7 @@ let rew_l2r_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" - (fun ind -> fix_r2l_forward_rew_scheme + (fun _ ind -> fix_r2l_forward_rew_scheme (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff) (**********************************************************************) @@ -704,7 +704,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) (* End of rewriting schemes *) @@ -780,6 +780,6 @@ let build_congr env (eq,refl,ctx) ind = in c, Evd.evar_universe_context_of ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" - (fun ind -> + (fun _ ind -> (* May fail if equality is not defined *) build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff) diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 16683d243..118ffb3e8 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -111,7 +111,7 @@ let check_bool_is_defined () = let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let build_beq_scheme kn = +let build_beq_scheme mode kn = check_bool_is_defined (); (* fetching global env *) let env = Global.env() in @@ -188,7 +188,7 @@ let build_beq_scheme kn = else begin try let eq, eff = - let c, eff = find_scheme (!beq_scheme_kind_aux()) (kn',i) in + let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in mkConst c, eff in let eqa, eff = let eqa, effs = List.split (List.map aux a) in @@ -330,7 +330,7 @@ let destruct_ind c = so from Ai we can find the the correct eq_Ai bl_ai or lb_ai *) (* used in the leib -> bool side*) -let do_replace_lb lb_scheme_key aavoid narg p q = +let do_replace_lb mode lb_scheme_key aavoid narg p q = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -360,7 +360,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = let u,v = destruct_ind type_of_pq in let lb_type_of_p = try - let c, eff = find_scheme lb_scheme_key (out_punivs u) (*FIXME*) in + let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in Proofview.tclUNIT (mkConst c, eff) with Not_found -> (* spiwack: the format of this error message should probably @@ -388,7 +388,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = end (* used in the bool -> leib side *) -let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = +let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -551,7 +551,7 @@ let compute_bl_goal ind lnamesparrec nparrec = (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|])) ))), eff -let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec = +let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -608,7 +608,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). if eq_gr (IndRef indeq) Coqlib.glob_eq then Tacticals.New.tclTHEN - (do_replace_bl bl_scheme_key ind + (do_replace_bl mode bl_scheme_key ind (!avoid) nparrec (ca.(2)) (ca.(1))) @@ -625,7 +625,12 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let make_bl_scheme mind = +let side_effect_of_mode = function + | Declare.KernelVerbose -> false + | Declare.KernelSilent -> true + | Declare.UserVerbose -> false + +let make_bl_scheme mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -637,8 +642,9 @@ let make_bl_scheme mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx bl_goal - (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal + (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -688,7 +694,7 @@ let compute_lb_goal ind lnamesparrec nparrec = (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) ))), eff -let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = +let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -732,7 +738,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = | App(c,ca) -> (match (kind_of_term ca.(1)) with | App(c',ca') -> let n = Array.length ca' in - do_replace_lb lb_scheme_key + do_replace_lb mode lb_scheme_key (!avoid) nparrec ca'.(n-2) ca'.(n-1) @@ -747,7 +753,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") -let make_lb_scheme mind = +let make_lb_scheme mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -759,8 +765,9 @@ let make_lb_scheme mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx lb_goal - (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal + (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in ([|ans|], ctx (* FIXME *)), eff @@ -919,7 +926,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ] end -let make_eq_decidability mind = +let make_eq_decidability mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then raise DecidabilityMutualNotSupported; @@ -930,7 +937,8 @@ let make_eq_decidability mind = let ctx = Evd.empty_evar_universe_context (* FIXME *)in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx (compute_dec_goal (ind,u) lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec) in diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 0d39466ed..b59d6fc8a 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -28,11 +28,10 @@ open Pp (**********************************************************************) (* Registering schemes in the environment *) - type mutual_scheme_object_function = - mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects type individual_scheme_object_function = - inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects type 'a scheme_kind = string @@ -141,32 +140,31 @@ let define internal id c p univs = in kn -let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) = - let (c, ctx), eff = f ind in +let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = + let (c, ctx), eff = f mode ind in let mib = Global.lookup_mind mind in let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define internal id c mib.mind_polymorphic ctx in + let const = define mode id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; const, Declareops.cons_side_effects (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff -let define_individual_scheme kind internal names (mind,i as ind) = +let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with | _,MutualSchemeFunction f -> assert false | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f internal names ind + define_individual_scheme_base kind s f mode names ind -let define_mutual_scheme_base kind suff f internal names mind = - let (cl, ctx), eff = f mind in +let define_mutual_scheme_base kind suff f mode names mind = + let (cl, ctx), eff = f mode mind in let mib = Global.lookup_mind mind in let ids = Array.init (Array.length mib.mind_packets) (fun i -> try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in - let consts = Array.map2 (fun id cl -> - define internal id cl mib.mind_polymorphic ctx) ids cl in + define mode id cl mib.mind_polymorphic ctx) ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, @@ -175,11 +173,11 @@ let define_mutual_scheme_base kind suff f internal names mind = kind (Global.safe_env()) (Array.to_list schemes)) eff -let define_mutual_scheme kind internal names mind = +let define_mutual_scheme kind mode names mind = match Hashtbl.find scheme_object_table kind with | _,IndividualSchemeFunction _ -> assert false | s,MutualSchemeFunction f -> - define_mutual_scheme_base kind s f internal names mind + define_mutual_scheme_base kind s f mode names mind let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in @@ -188,14 +186,14 @@ let find_scheme_on_env_too kind ind = kind (Global.safe_env()) [ind, s]) Declareops.no_seff -let find_scheme kind (mind,i as ind) = +let find_scheme ?(mode=KernelSilent) kind (mind,i as ind) = try find_scheme_on_env_too kind ind with Not_found -> match Hashtbl.find scheme_object_table kind with | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f KernelSilent None ind + define_individual_scheme_base kind s f mode None ind | s,MutualSchemeFunction f -> - let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in + let ca, eff = define_mutual_scheme_base kind s f mode [] mind in ca.(i), eff let check_scheme kind ind = diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index 98eaac092..d0844dd94 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -8,6 +8,7 @@ open Term open Names +open Declare (** This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand *) @@ -19,9 +20,9 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects type individual_scheme_object_function = - inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects (** Main functions to register a scheme builder *) @@ -32,21 +33,17 @@ val declare_individual_scheme_object : string -> ?aux:string -> individual_scheme_object_function -> individual scheme_kind -(* -val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit -*) - (** Force generation of a (mutually) scheme with possibly user-level names *) val define_individual_scheme : individual scheme_kind -> - Declare.internal_flag (** internal *) -> + internal_flag (** internal *) -> Id.t option -> inductive -> constant * Declareops.side_effects -val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) -> +val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects val check_scheme : 'a scheme_kind -> inductive -> bool |