From 96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 00:43:01 +0200 Subject: Move transparent_state to its own module. --- tactics/auto.ml | 8 ++++---- tactics/auto.mli | 2 +- tactics/btermdn.mli | 9 ++++----- tactics/class_tactics.ml | 12 ++++++------ tactics/class_tactics.mli | 4 ++-- tactics/eauto.ml | 6 +++--- tactics/equality.ml | 16 ++++++++-------- tactics/hints.ml | 16 ++++++++-------- tactics/hints.mli | 10 +++++----- tactics/tactics.ml | 8 ++++---- tactics/tactics.mli | 2 +- 11 files changed, 46 insertions(+), 47 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 65b2615b6b..07b9bac2c7 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -45,7 +45,7 @@ let auto_core_unif_flags_of st1 st2 = { use_metas_eagerly_in_conv_on_closed_terms = false; use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = st2; - modulo_delta_types = full_transparent_state; + modulo_delta_types = TranspState.full; check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; @@ -59,13 +59,13 @@ let auto_unif_flags_of st1 st2 = let flags = auto_core_unif_flags_of st1 st2 in { core_unify_flags = flags; merge_unify_flags = flags; - subterm_unify_flags = { flags with modulo_delta = empty_transparent_state }; + subterm_unify_flags = { flags with modulo_delta = TranspState.empty }; allow_K_in_toplevel_higher_order_unification = false; resolve_evars = true } let auto_unif_flags = - auto_unif_flags_of full_transparent_state empty_transparent_state + auto_unif_flags_of TranspState.full TranspState.empty (* Try unification with the precompiled clause, then use registered Apply *) @@ -291,7 +291,7 @@ let flags_of_state st = auto_unif_flags_of st st let auto_flags_of_state st = - auto_unif_flags_of full_transparent_state st + auto_unif_flags_of TranspState.full st let hintmap_of sigma secvars hdc concl = match hdc with diff --git a/tactics/auto.mli b/tactics/auto.mli index a835c1ed95..c7acbd4bfb 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -22,7 +22,7 @@ val compute_secvars : Proofview.Goal.t -> Id.Pred.t val default_search_depth : int ref -val auto_flags_of_state : transparent_state -> Unification.unify_flags +val auto_flags_of_state : TranspState.t -> Unification.unify_flags val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> Proofview.Goal.t -> clausenv * constr diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 861c9b6250..6af5012def 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -9,7 +9,6 @@ (************************************************************************) open Pattern -open Names (** Discrimination nets with bounded depth. *) @@ -19,7 +18,7 @@ open Names order in such a way patterns having the same prefix have this common prefix shared and the seek for the action associated to the patterns that a term matches are found in time proportional to the maximal -number of nodes of the patterns matching the term. The [transparent_state] +number of nodes of the patterns matching the term. The [TranspState.t] indicates which constants and variables can be considered as rigid. These dnets are able to cope with existential variables as well, which match [Everything]. *) @@ -31,10 +30,10 @@ sig val empty : t - val add : transparent_state option -> t -> (constr_pattern * Z.t) -> t - val rmv : transparent_state option -> t -> (constr_pattern * Z.t) -> t + val add : TranspState.t option -> t -> (constr_pattern * Z.t) -> t + val rmv : TranspState.t option -> t -> (constr_pattern * Z.t) -> t - val lookup : Evd.evar_map -> transparent_state option -> t -> EConstr.constr -> Z.t list + val lookup : Evd.evar_map -> TranspState.t option -> t -> EConstr.constr -> Z.t list val app : (Z.t -> unit) -> t -> unit end diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 81cf9289d1..f27e5e281a 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -585,9 +585,9 @@ module Search = struct (** Local hints *) let autogoal_cache = Summary.ref ~name:"autogoal_cache" (DirPath.empty, true, Context.Named.empty, - Hint_db.empty full_transparent_state true) + Hint_db.empty TranspState.full true) - let make_autogoal_hints only_classes ?(st=full_transparent_state) g = + let make_autogoal_hints only_classes ?(st=TranspState.full) g = let open Proofview in let open Tacmach.New in let sign = Goal.hyps g in @@ -605,7 +605,7 @@ module Search = struct in autogoal_cache := (cwd, only_classes, sign, hints); hints - let make_autogoal ?(st=full_transparent_state) only_classes dep cut i g = + let make_autogoal ?(st=TranspState.full) only_classes dep cut i g = let hints = make_autogoal_hints only_classes ~st g in { search_hints = hints; search_depth = [i]; last_tac = lazy (str"none"); @@ -843,7 +843,7 @@ module Search = struct let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in search_tac hints depth 1 info - let search_tac ?(st=full_transparent_state) only_classes dep hints depth = + let search_tac ?(st=TranspState.full) only_classes dep hints depth = let open Proofview in let tac sigma gls i = Goal.enter @@ -873,7 +873,7 @@ module Search = struct | (e,ie) -> Proofview.tclZERO ~info:ie e) in aux 1 - let eauto_tac ?(st=full_transparent_state) ?(unique=false) + let eauto_tac ?(st=TranspState.full) ?(unique=false) ~only_classes ?strategy ~depth ~dep hints = let open Proofview in let tac = @@ -985,7 +985,7 @@ end (** Binding to either V85 or Search implementations. *) -let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) +let typeclasses_eauto ?(only_classes=false) ?(st=TranspState.full) ?strategy ~depth dbs = let dbs = List.map_filter (fun db -> try Some (searchtable_map db) diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 9ba69a0584..9e2b0d26b5 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -25,7 +25,7 @@ type search_strategy = Dfs | Bfs val set_typeclasses_strategy : search_strategy -> unit -val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> ?strategy:search_strategy -> +val typeclasses_eauto : ?only_classes:bool -> ?st:TranspState.t -> ?strategy:search_strategy -> depth:(Int.t option) -> Hints.hint_db_name list -> unit Proofview.tactic @@ -39,7 +39,7 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic module Search : sig val eauto_tac : - ?st:Names.transparent_state -> + ?st:TranspState.t -> (** The transparent_state used when working with local hypotheses *) ?unique:bool -> (** Should we force a unique solution *) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 5067315d08..c18b7bb214 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -29,7 +29,7 @@ open Locusops open Hints open Proofview.Notations -let eauto_unif_flags = auto_flags_of_state full_transparent_state +let eauto_unif_flags = auto_flags_of_state TranspState.full let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter begin fun gl -> @@ -307,7 +307,7 @@ module SearchProblem = struct let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in let hyps' = pf_hyps gls in if hyps' == hyps then List.hd s.localdb - else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true s.local_lemmas) + else make_local_hint_db (pf_env gls) (project gls) ~ts:TranspState.full true s.local_lemmas) (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls)) in { depth = pred s.depth; priority = cost; tacres = lgls; @@ -388,7 +388,7 @@ let make_initial_state dbg n gl dblist localdb lems = } let e_search_auto debug (in_depth,p) lems db_list gl = - let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:full_transparent_state true lems in + let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:TranspState.full true lems in let d = mk_eauto_dbg debug in let tac = match in_depth,d with | (true,Debug) -> Search.debug_depth_first diff --git a/tactics/equality.ml b/tactics/equality.ml index c4a6b1605d..8377cd5c75 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -101,8 +101,8 @@ let rewrite_core_unif_flags = { modulo_conv_on_closed_terms = None; use_metas_eagerly_in_conv_on_closed_terms = true; use_evars_eagerly_in_conv_on_closed_terms = false; - modulo_delta = empty_transparent_state; - modulo_delta_types = empty_transparent_state; + modulo_delta = TranspState.empty; + modulo_delta_types = TranspState.empty; check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; @@ -169,7 +169,7 @@ let instantiate_lemma gl c ty l l2r concl = [eqclause] let rewrite_conv_closed_core_unif_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; + modulo_conv_on_closed_terms = Some TranspState.full; (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) @@ -178,8 +178,8 @@ let rewrite_conv_closed_core_unif_flags = { (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *) (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *) - modulo_delta = empty_transparent_state; - modulo_delta_types = full_transparent_state; + modulo_delta = TranspState.empty; + modulo_delta_types = TranspState.full; check_applied_meta_types = true; use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) @@ -204,7 +204,7 @@ let rewrite_conv_closed_unif_flags = { } let rewrite_keyed_core_unif_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; + modulo_conv_on_closed_terms = Some TranspState.full; (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) @@ -213,8 +213,8 @@ let rewrite_keyed_core_unif_flags = { (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *) (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *) - modulo_delta = full_transparent_state; - modulo_delta_types = full_transparent_state; + modulo_delta = TranspState.full; + modulo_delta_types = TranspState.full; check_applied_meta_types = true; use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 2f2d32e887..5f0d3a2503 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -497,7 +497,7 @@ type hint_db_name = string module Hint_db : sig type t -val empty : ?name:hint_db_name -> transparent_state -> bool -> t +val empty : ?name:hint_db_name -> TranspState.t -> bool -> t val find : GlobRef.t -> t -> search_entry val map_none : secvars:Id.Pred.t -> t -> full_hint list val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list @@ -513,8 +513,8 @@ val remove_one : GlobRef.t -> t -> t val remove_list : GlobRef.t list -> t -> t val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool -val transparent_state : t -> transparent_state -val set_transparent_state : t -> transparent_state -> t +val transparent_state : t -> TranspState.t +val set_transparent_state : t -> TranspState.t -> t val add_cut : hints_path -> t -> t val add_mode : GlobRef.t -> hint_mode array -> t -> t val cut : t -> hints_path @@ -526,7 +526,7 @@ end = struct type t = { - hintdb_state : Names.transparent_state; + hintdb_state : TranspState.t; hintdb_cut : hints_path; hintdb_unfolds : Id.Set.t * Cset.t; hintdb_max_id : int; @@ -740,8 +740,8 @@ let typeclasses_db = "typeclass_instances" let rewrite_db = "rewrite" let auto_init_db = - Hintdbmap.add typeclasses_db (Hint_db.empty full_transparent_state true) - (Hintdbmap.add rewrite_db (Hint_db.empty cst_full_transparent_state true) + Hintdbmap.add typeclasses_db (Hint_db.empty TranspState.full true) + (Hintdbmap.add rewrite_db (Hint_db.empty TranspState.cst_full true) Hintdbmap.empty) let searchtable = Summary.ref ~name:"searchtable" auto_init_db @@ -977,7 +977,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let get_db dbname = try searchtable_map dbname - with Not_found -> Hint_db.empty ~name:dbname empty_transparent_state false + with Not_found -> Hint_db.empty ~name:dbname TranspState.empty false let add_hint dbname hintlist = let check (_, h) = @@ -1015,7 +1015,7 @@ let remove_hint dbname grs = searchtable_add (dbname, db') type hint_action = - | CreateDB of bool * transparent_state + | CreateDB of bool * TranspState.t | AddTransparency of evaluable_global_reference hints_transparency_target * bool | AddHints of hint_entry list | RemoveHints of GlobRef.t list diff --git a/tactics/hints.mli b/tactics/hints.mli index 6db8feccd0..43cfb6a059 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -122,7 +122,7 @@ val glob_hints_path : module Hint_db : sig type t - val empty : ?name:hint_db_name -> transparent_state -> bool -> t + val empty : ?name:hint_db_name -> TranspState.t -> bool -> t val find : GlobRef.t -> t -> search_entry (** All hints which have no pattern. @@ -155,8 +155,8 @@ module Hint_db : hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool - val transparent_state : t -> transparent_state - val set_transparent_state : t -> transparent_state -> t + val transparent_state : t -> TranspState.t + val set_transparent_state : t -> TranspState.t -> t val add_cut : hints_path -> t -> t val cut : t -> hints_path @@ -191,7 +191,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit [use_dn] switches the use of the discrimination net for all hints and patterns. *) -val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit +val create_hint_db : bool -> hint_db_name -> TranspState.t -> bool -> unit val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit @@ -273,7 +273,7 @@ val repr_hint : hint -> (raw_hint * clausenv) hint_ast Useful to take the current goal hypotheses as hints; Boolean tells if lemmas with evars are allowed *) -val make_local_hint_db : env -> evar_map -> ?ts:transparent_state -> bool -> delayed_open_constr list -> hint_db +val make_local_hint_db : env -> evar_map -> ?ts:TranspState.t -> bool -> delayed_open_constr list -> hint_db val make_db_list : hint_db_name list -> hint_db list diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 03ad1b4c4f..2601b5fd84 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1660,7 +1660,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars let sigma = Tacmach.New.project gl in let ts = if respect_opaque then Conv_oracle.get_transp_state (oracle env) - else full_transparent_state + else TranspState.full in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in @@ -1826,7 +1826,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta let sigma = Tacmach.New.project gl in let ts = if respect_opaque then Conv_oracle.get_transp_state (oracle env) - else full_transparent_state + else TranspState.full in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in @@ -4909,7 +4909,7 @@ let constr_eq ~strict x y = | None -> fail end -let unify ?(state=full_transparent_state) x y = +let unify ?(state=TranspState.full) x y = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -4922,7 +4922,7 @@ let unify ?(state=full_transparent_state) x y = let flags = { (default_unify_flags ()) with core_unify_flags = core_flags; merge_unify_flags = core_flags; - subterm_unify_flags = { core_flags with modulo_delta = empty_transparent_state } } + subterm_unify_flags = { core_flags with modulo_delta = TranspState.empty } } in let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in Proofview.Unsafe.tclEVARS sigma diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b298524ff8..1db65fc1aa 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -419,7 +419,7 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - are added to the evar map. *) val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic -val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic +val unify : ?state:TranspState.t -> constr -> constr -> unit Proofview.tactic val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic val specialize_eqs : Id.t -> unit Proofview.tactic -- cgit v1.2.3 From ad5aea737ecc639c31dda84322b3550a4d380b47 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 21:06:01 +0200 Subject: Proper record type and accessors for transparent states. This is documented in dev/doc/changes.md. --- tactics/auto.ml | 4 ++-- tactics/btermdn.ml | 14 +++++++------- tactics/hints.ml | 34 +++++++++++++++++++--------------- 3 files changed, 28 insertions(+), 24 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 07b9bac2c7..a23a085db5 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -358,12 +358,12 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = let flags = flags_of_state (Hint_db.transparent_state db) in List.map (fun x -> (Some flags, x)) (f db) else - let (ids, csts as st) = Hint_db.transparent_state db in + let st = Hint_db.transparent_state db in let flags, l = let l = match hdc with None -> Hint_db.map_none ~secvars db | Some hdc -> - if (Id.Pred.is_empty ids && Cpred.is_empty csts) + if TranspState.is_empty st then Hint_db.map_auto sigma ~secvars hdc concl db else Hint_db.map_existential sigma ~secvars hdc concl db in auto_flags_of_state st, l diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index bfee0422e7..04fe6a9fa7 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -69,13 +69,13 @@ let constr_pat_discr t = | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args) | _ -> None -let constr_val_discr_st sigma (idpred,cpred) t = +let constr_val_discr_st sigma ts t = let c, l = decomp sigma t in match EConstr.kind sigma c with - | Const (c,u) -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l) + | Const (c,u) -> if TranspState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l) | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l) | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id when not (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l) + | Var id when not (TranspState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l) | Prod (n, d, c) -> Label(ProdLabel, [d; c]) | Lambda (n, d, c) -> if List.is_empty l then @@ -85,15 +85,15 @@ let constr_val_discr_st sigma (idpred,cpred) t = | Evar _ -> Everything | _ -> Nothing -let constr_pat_discr_st (idpred,cpred) t = +let constr_pat_discr_st ts t = match decomp_pat t with | PRef ((IndRef _) as ref), args | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) - | PRef ((VarRef v) as ref), args when not (Id.Pred.mem v idpred) -> + | PRef ((VarRef v) as ref), args when not (TranspState.is_transparent_variable ts v) -> Some(GRLabel ref,args) - | PVar v, args when not (Id.Pred.mem v idpred) -> + | PVar v, args when not (TranspState.is_transparent_variable ts v) -> Some(GRLabel (VarRef v),args) - | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) -> + | PRef ((ConstRef c) as ref), args when not (TranspState.is_transparent_constant ts c) -> Some (GRLabel ref, args) | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c]) | PLambda (_, d, c), [] -> Some (LambdaLabel, [d ; c]) diff --git a/tactics/hints.ml b/tactics/hints.ml index 5f0d3a2503..287e289c2f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -290,9 +290,9 @@ let lookup_tacs sigma concl st se = module Constr_map = Map.Make(GlobRef.Ordered) -let is_transparent_gr (ids, csts) = function - | VarRef id -> Id.Pred.mem id ids - | ConstRef cst -> Cpred.mem cst csts +let is_transparent_gr ts = function + | VarRef id -> TranspState.is_transparent_variable ts id + | ConstRef cst -> TranspState.is_transparent_constant ts cst | IndRef _ | ConstructRef _ -> false let strip_params env sigma c = @@ -663,10 +663,13 @@ struct let st',db,rebuild = match v.code.obj with | Unfold_nth egr -> - let addunf (ids,csts) (ids',csts') = + let addunf ts (ids, csts) = + let open TranspState in match egr with - | EvalVarRef id -> (Id.Pred.add id ids, csts), (Id.Set.add id ids', csts') - | EvalConstRef cst -> (ids, Cpred.add cst csts), (ids', Cset.add cst csts') + | EvalVarRef id -> + { ts with tr_var = Id.Pred.add id ts.tr_var }, (Id.Set.add id ids, csts) + | EvalConstRef cst -> + { ts with tr_cst = Cpred.add cst ts.tr_cst }, (ids, Cset.add cst csts) in let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in state, { db with hintdb_unfolds = unfs }, true @@ -995,18 +998,19 @@ let add_hint dbname hintlist = searchtable_add (dbname,db') let add_transparency dbname target b = + let open TranspState in let db = get_db dbname in - let (ids, csts as st) = Hint_db.transparent_state db in + let st = Hint_db.transparent_state db in let st' = match target with - | HintsVariables -> (if b then Id.Pred.full else Id.Pred.empty), csts - | HintsConstants -> ids, if b then Cpred.full else Cpred.empty + | HintsVariables -> { st with tr_var = (if b then Id.Pred.full else Id.Pred.empty) } + | HintsConstants -> { st with tr_cst = (if b then Cpred.full else Cpred.empty) } | HintsReferences grs -> - List.fold_left (fun (ids, csts) gr -> - match gr with - | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts) - | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts) - st grs + List.fold_left (fun st gr -> + match gr with + | EvalConstRef c -> { st with tr_cst = (if b then Cpred.add else Cpred.remove) c st.tr_cst } + | EvalVarRef v -> { st with tr_var = (if b then Id.Pred.add else Id.Pred.remove) v st.tr_var }) + st grs in searchtable_add (dbname, Hint_db.set_transparent_state db st') let remove_hint dbname grs = @@ -1543,7 +1547,7 @@ let pr_hint_db_env env sigma db = in Hint_db.fold fold db (mt ()) in - let (ids, csts) = Hint_db.transparent_state db in + let { TranspState.tr_var = ids; tr_cst = csts } = Hint_db.transparent_state db in hov 0 ((if Hint_db.use_dn db then str"Discriminated database" else str"Non-discriminated database")) ++ fnl () ++ -- cgit v1.2.3 From 733cb74a2038ff92156b7209713fc2ea741ccca6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 19 Nov 2018 08:12:28 +0100 Subject: Rename TranspState into TransparentState. --- tactics/auto.ml | 10 +++++----- tactics/auto.mli | 2 +- tactics/btermdn.ml | 10 +++++----- tactics/btermdn.mli | 8 ++++---- tactics/class_tactics.ml | 12 ++++++------ tactics/class_tactics.mli | 4 ++-- tactics/eauto.ml | 6 +++--- tactics/equality.ml | 16 ++++++++-------- tactics/hints.ml | 26 +++++++++++++------------- tactics/hints.mli | 10 +++++----- tactics/tactics.ml | 8 ++++---- tactics/tactics.mli | 2 +- 12 files changed, 57 insertions(+), 57 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index a23a085db5..81e487b77d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -45,7 +45,7 @@ let auto_core_unif_flags_of st1 st2 = { use_metas_eagerly_in_conv_on_closed_terms = false; use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = st2; - modulo_delta_types = TranspState.full; + modulo_delta_types = TransparentState.full; check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; @@ -59,13 +59,13 @@ let auto_unif_flags_of st1 st2 = let flags = auto_core_unif_flags_of st1 st2 in { core_unify_flags = flags; merge_unify_flags = flags; - subterm_unify_flags = { flags with modulo_delta = TranspState.empty }; + subterm_unify_flags = { flags with modulo_delta = TransparentState.empty }; allow_K_in_toplevel_higher_order_unification = false; resolve_evars = true } let auto_unif_flags = - auto_unif_flags_of TranspState.full TranspState.empty + auto_unif_flags_of TransparentState.full TransparentState.empty (* Try unification with the precompiled clause, then use registered Apply *) @@ -291,7 +291,7 @@ let flags_of_state st = auto_unif_flags_of st st let auto_flags_of_state st = - auto_unif_flags_of TranspState.full st + auto_unif_flags_of TransparentState.full st let hintmap_of sigma secvars hdc concl = match hdc with @@ -363,7 +363,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = let l = match hdc with None -> Hint_db.map_none ~secvars db | Some hdc -> - if TranspState.is_empty st + if TransparentState.is_empty st then Hint_db.map_auto sigma ~secvars hdc concl db else Hint_db.map_existential sigma ~secvars hdc concl db in auto_flags_of_state st, l diff --git a/tactics/auto.mli b/tactics/auto.mli index c7acbd4bfb..72d2292ffb 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -22,7 +22,7 @@ val compute_secvars : Proofview.Goal.t -> Id.Pred.t val default_search_depth : int ref -val auto_flags_of_state : TranspState.t -> Unification.unify_flags +val auto_flags_of_state : TransparentState.t -> Unification.unify_flags val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> Proofview.Goal.t -> clausenv * constr diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 04fe6a9fa7..2f2bd8d2bc 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -72,10 +72,10 @@ let constr_pat_discr t = let constr_val_discr_st sigma ts t = let c, l = decomp sigma t in match EConstr.kind sigma c with - | Const (c,u) -> if TranspState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l) + | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l) | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l) | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id when not (TranspState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l) + | Var id when not (TransparentState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l) | Prod (n, d, c) -> Label(ProdLabel, [d; c]) | Lambda (n, d, c) -> if List.is_empty l then @@ -89,11 +89,11 @@ let constr_pat_discr_st ts t = match decomp_pat t with | PRef ((IndRef _) as ref), args | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) - | PRef ((VarRef v) as ref), args when not (TranspState.is_transparent_variable ts v) -> + | PRef ((VarRef v) as ref), args when not (TransparentState.is_transparent_variable ts v) -> Some(GRLabel ref,args) - | PVar v, args when not (TranspState.is_transparent_variable ts v) -> + | PVar v, args when not (TransparentState.is_transparent_variable ts v) -> Some(GRLabel (VarRef v),args) - | PRef ((ConstRef c) as ref), args when not (TranspState.is_transparent_constant ts c) -> + | PRef ((ConstRef c) as ref), args when not (TransparentState.is_transparent_constant ts c) -> Some (GRLabel ref, args) | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c]) | PLambda (_, d, c), [] -> Some (LambdaLabel, [d ; c]) diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 6af5012def..cc31fb0599 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -18,7 +18,7 @@ open Pattern order in such a way patterns having the same prefix have this common prefix shared and the seek for the action associated to the patterns that a term matches are found in time proportional to the maximal -number of nodes of the patterns matching the term. The [TranspState.t] +number of nodes of the patterns matching the term. The [TransparentState.t] indicates which constants and variables can be considered as rigid. These dnets are able to cope with existential variables as well, which match [Everything]. *) @@ -30,10 +30,10 @@ sig val empty : t - val add : TranspState.t option -> t -> (constr_pattern * Z.t) -> t - val rmv : TranspState.t option -> t -> (constr_pattern * Z.t) -> t + val add : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t + val rmv : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t - val lookup : Evd.evar_map -> TranspState.t option -> t -> EConstr.constr -> Z.t list + val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list val app : (Z.t -> unit) -> t -> unit end diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index f27e5e281a..1bb33f2a23 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -585,9 +585,9 @@ module Search = struct (** Local hints *) let autogoal_cache = Summary.ref ~name:"autogoal_cache" (DirPath.empty, true, Context.Named.empty, - Hint_db.empty TranspState.full true) + Hint_db.empty TransparentState.full true) - let make_autogoal_hints only_classes ?(st=TranspState.full) g = + let make_autogoal_hints only_classes ?(st=TransparentState.full) g = let open Proofview in let open Tacmach.New in let sign = Goal.hyps g in @@ -605,7 +605,7 @@ module Search = struct in autogoal_cache := (cwd, only_classes, sign, hints); hints - let make_autogoal ?(st=TranspState.full) only_classes dep cut i g = + let make_autogoal ?(st=TransparentState.full) only_classes dep cut i g = let hints = make_autogoal_hints only_classes ~st g in { search_hints = hints; search_depth = [i]; last_tac = lazy (str"none"); @@ -843,7 +843,7 @@ module Search = struct let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in search_tac hints depth 1 info - let search_tac ?(st=TranspState.full) only_classes dep hints depth = + let search_tac ?(st=TransparentState.full) only_classes dep hints depth = let open Proofview in let tac sigma gls i = Goal.enter @@ -873,7 +873,7 @@ module Search = struct | (e,ie) -> Proofview.tclZERO ~info:ie e) in aux 1 - let eauto_tac ?(st=TranspState.full) ?(unique=false) + let eauto_tac ?(st=TransparentState.full) ?(unique=false) ~only_classes ?strategy ~depth ~dep hints = let open Proofview in let tac = @@ -985,7 +985,7 @@ end (** Binding to either V85 or Search implementations. *) -let typeclasses_eauto ?(only_classes=false) ?(st=TranspState.full) +let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full) ?strategy ~depth dbs = let dbs = List.map_filter (fun db -> try Some (searchtable_map db) diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 9e2b0d26b5..46dff34f89 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -25,7 +25,7 @@ type search_strategy = Dfs | Bfs val set_typeclasses_strategy : search_strategy -> unit -val typeclasses_eauto : ?only_classes:bool -> ?st:TranspState.t -> ?strategy:search_strategy -> +val typeclasses_eauto : ?only_classes:bool -> ?st:TransparentState.t -> ?strategy:search_strategy -> depth:(Int.t option) -> Hints.hint_db_name list -> unit Proofview.tactic @@ -39,7 +39,7 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic module Search : sig val eauto_tac : - ?st:TranspState.t -> + ?st:TransparentState.t -> (** The transparent_state used when working with local hypotheses *) ?unique:bool -> (** Should we force a unique solution *) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index c18b7bb214..9a6bdab7b9 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -29,7 +29,7 @@ open Locusops open Hints open Proofview.Notations -let eauto_unif_flags = auto_flags_of_state TranspState.full +let eauto_unif_flags = auto_flags_of_state TransparentState.full let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter begin fun gl -> @@ -307,7 +307,7 @@ module SearchProblem = struct let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in let hyps' = pf_hyps gls in if hyps' == hyps then List.hd s.localdb - else make_local_hint_db (pf_env gls) (project gls) ~ts:TranspState.full true s.local_lemmas) + else make_local_hint_db (pf_env gls) (project gls) ~ts:TransparentState.full true s.local_lemmas) (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls)) in { depth = pred s.depth; priority = cost; tacres = lgls; @@ -388,7 +388,7 @@ let make_initial_state dbg n gl dblist localdb lems = } let e_search_auto debug (in_depth,p) lems db_list gl = - let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:TranspState.full true lems in + let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:TransparentState.full true lems in let d = mk_eauto_dbg debug in let tac = match in_depth,d with | (true,Debug) -> Search.debug_depth_first diff --git a/tactics/equality.ml b/tactics/equality.ml index 8377cd5c75..969f539d1f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -101,8 +101,8 @@ let rewrite_core_unif_flags = { modulo_conv_on_closed_terms = None; use_metas_eagerly_in_conv_on_closed_terms = true; use_evars_eagerly_in_conv_on_closed_terms = false; - modulo_delta = TranspState.empty; - modulo_delta_types = TranspState.empty; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.empty; check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; @@ -169,7 +169,7 @@ let instantiate_lemma gl c ty l l2r concl = [eqclause] let rewrite_conv_closed_core_unif_flags = { - modulo_conv_on_closed_terms = Some TranspState.full; + modulo_conv_on_closed_terms = Some TransparentState.full; (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) @@ -178,8 +178,8 @@ let rewrite_conv_closed_core_unif_flags = { (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *) (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *) - modulo_delta = TranspState.empty; - modulo_delta_types = TranspState.full; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.full; check_applied_meta_types = true; use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) @@ -204,7 +204,7 @@ let rewrite_conv_closed_unif_flags = { } let rewrite_keyed_core_unif_flags = { - modulo_conv_on_closed_terms = Some TranspState.full; + modulo_conv_on_closed_terms = Some TransparentState.full; (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) @@ -213,8 +213,8 @@ let rewrite_keyed_core_unif_flags = { (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *) (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *) - modulo_delta = TranspState.full; - modulo_delta_types = TranspState.full; + modulo_delta = TransparentState.full; + modulo_delta_types = TransparentState.full; check_applied_meta_types = true; use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 287e289c2f..6aa021543d 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -291,8 +291,8 @@ let lookup_tacs sigma concl st se = module Constr_map = Map.Make(GlobRef.Ordered) let is_transparent_gr ts = function - | VarRef id -> TranspState.is_transparent_variable ts id - | ConstRef cst -> TranspState.is_transparent_constant ts cst + | VarRef id -> TransparentState.is_transparent_variable ts id + | ConstRef cst -> TransparentState.is_transparent_constant ts cst | IndRef _ | ConstructRef _ -> false let strip_params env sigma c = @@ -497,7 +497,7 @@ type hint_db_name = string module Hint_db : sig type t -val empty : ?name:hint_db_name -> TranspState.t -> bool -> t +val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t val find : GlobRef.t -> t -> search_entry val map_none : secvars:Id.Pred.t -> t -> full_hint list val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list @@ -513,8 +513,8 @@ val remove_one : GlobRef.t -> t -> t val remove_list : GlobRef.t list -> t -> t val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool -val transparent_state : t -> TranspState.t -val set_transparent_state : t -> TranspState.t -> t +val transparent_state : t -> TransparentState.t +val set_transparent_state : t -> TransparentState.t -> t val add_cut : hints_path -> t -> t val add_mode : GlobRef.t -> hint_mode array -> t -> t val cut : t -> hints_path @@ -526,7 +526,7 @@ end = struct type t = { - hintdb_state : TranspState.t; + hintdb_state : TransparentState.t; hintdb_cut : hints_path; hintdb_unfolds : Id.Set.t * Cset.t; hintdb_max_id : int; @@ -664,7 +664,7 @@ struct match v.code.obj with | Unfold_nth egr -> let addunf ts (ids, csts) = - let open TranspState in + let open TransparentState in match egr with | EvalVarRef id -> { ts with tr_var = Id.Pred.add id ts.tr_var }, (Id.Set.add id ids, csts) @@ -743,8 +743,8 @@ let typeclasses_db = "typeclass_instances" let rewrite_db = "rewrite" let auto_init_db = - Hintdbmap.add typeclasses_db (Hint_db.empty TranspState.full true) - (Hintdbmap.add rewrite_db (Hint_db.empty TranspState.cst_full true) + Hintdbmap.add typeclasses_db (Hint_db.empty TransparentState.full true) + (Hintdbmap.add rewrite_db (Hint_db.empty TransparentState.cst_full true) Hintdbmap.empty) let searchtable = Summary.ref ~name:"searchtable" auto_init_db @@ -980,7 +980,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let get_db dbname = try searchtable_map dbname - with Not_found -> Hint_db.empty ~name:dbname TranspState.empty false + with Not_found -> Hint_db.empty ~name:dbname TransparentState.empty false let add_hint dbname hintlist = let check (_, h) = @@ -998,7 +998,7 @@ let add_hint dbname hintlist = searchtable_add (dbname,db') let add_transparency dbname target b = - let open TranspState in + let open TransparentState in let db = get_db dbname in let st = Hint_db.transparent_state db in let st' = @@ -1019,7 +1019,7 @@ let remove_hint dbname grs = searchtable_add (dbname, db') type hint_action = - | CreateDB of bool * TranspState.t + | CreateDB of bool * TransparentState.t | AddTransparency of evaluable_global_reference hints_transparency_target * bool | AddHints of hint_entry list | RemoveHints of GlobRef.t list @@ -1547,7 +1547,7 @@ let pr_hint_db_env env sigma db = in Hint_db.fold fold db (mt ()) in - let { TranspState.tr_var = ids; tr_cst = csts } = Hint_db.transparent_state db in + let { TransparentState.tr_var = ids; tr_cst = csts } = Hint_db.transparent_state db in hov 0 ((if Hint_db.use_dn db then str"Discriminated database" else str"Non-discriminated database")) ++ fnl () ++ diff --git a/tactics/hints.mli b/tactics/hints.mli index 43cfb6a059..dd2c63d351 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -122,7 +122,7 @@ val glob_hints_path : module Hint_db : sig type t - val empty : ?name:hint_db_name -> TranspState.t -> bool -> t + val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t val find : GlobRef.t -> t -> search_entry (** All hints which have no pattern. @@ -155,8 +155,8 @@ module Hint_db : hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool - val transparent_state : t -> TranspState.t - val set_transparent_state : t -> TranspState.t -> t + val transparent_state : t -> TransparentState.t + val set_transparent_state : t -> TransparentState.t -> t val add_cut : hints_path -> t -> t val cut : t -> hints_path @@ -191,7 +191,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit [use_dn] switches the use of the discrimination net for all hints and patterns. *) -val create_hint_db : bool -> hint_db_name -> TranspState.t -> bool -> unit +val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit @@ -273,7 +273,7 @@ val repr_hint : hint -> (raw_hint * clausenv) hint_ast Useful to take the current goal hypotheses as hints; Boolean tells if lemmas with evars are allowed *) -val make_local_hint_db : env -> evar_map -> ?ts:TranspState.t -> bool -> delayed_open_constr list -> hint_db +val make_local_hint_db : env -> evar_map -> ?ts:TransparentState.t -> bool -> delayed_open_constr list -> hint_db val make_db_list : hint_db_name list -> hint_db list diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2601b5fd84..349cfce205 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1660,7 +1660,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars let sigma = Tacmach.New.project gl in let ts = if respect_opaque then Conv_oracle.get_transp_state (oracle env) - else TranspState.full + else TransparentState.full in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in @@ -1826,7 +1826,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta let sigma = Tacmach.New.project gl in let ts = if respect_opaque then Conv_oracle.get_transp_state (oracle env) - else TranspState.full + else TransparentState.full in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in @@ -4909,7 +4909,7 @@ let constr_eq ~strict x y = | None -> fail end -let unify ?(state=TranspState.full) x y = +let unify ?(state=TransparentState.full) x y = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -4922,7 +4922,7 @@ let unify ?(state=TranspState.full) x y = let flags = { (default_unify_flags ()) with core_unify_flags = core_flags; merge_unify_flags = core_flags; - subterm_unify_flags = { core_flags with modulo_delta = TranspState.empty } } + subterm_unify_flags = { core_flags with modulo_delta = TransparentState.empty } } in let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in Proofview.Unsafe.tclEVARS sigma diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 1db65fc1aa..4e91a9a728 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -419,7 +419,7 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - are added to the evar map. *) val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic -val unify : ?state:TranspState.t -> constr -> constr -> unit Proofview.tactic +val unify : ?state:TransparentState.t -> constr -> constr -> unit Proofview.tactic val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic val specialize_eqs : Id.t -> unit Proofview.tactic -- cgit v1.2.3