From 7a56397ae26854df6335a3325353d0a5d6c894ea Mon Sep 17 00:00:00 2001 From: amblaf Date: Thu, 15 Jun 2017 11:34:40 +0200 Subject: Remove references to Global.env in tactics/*.ml Only in ml files that are not related to Coq commands --- tactics/class_tactics.ml | 18 +++++++++--------- tactics/eauto.ml | 6 +++--- tactics/eqdecide.ml | 3 ++- tactics/equality.ml | 40 ++++++++++++++++++---------------------- tactics/hipattern.ml | 47 ++++++++++++++++++++++------------------------- tactics/hipattern.mli | 18 +++++++++--------- tactics/tactics.ml | 21 ++++++++++++--------- 7 files changed, 75 insertions(+), 78 deletions(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3fc2fc31b..36785b15d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1342,7 +1342,7 @@ module Search = struct | Some i -> str ", with depth limit " ++ int i)); tac - let run_on_evars p evm tac = + let run_on_evars p evm tac env = match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) | Some (goals, evm') -> @@ -1357,7 +1357,7 @@ module Search = struct let pv = Proofview.unshelve goals pv in try let (), pv', (unsafe, shelved, gaveup), _ = - Proofview.apply (Global.env ()) tac pv + Proofview.apply env tac pv in if Proofview.finished pv' then let evm' = Proofview.return pv' in @@ -1374,22 +1374,22 @@ module Search = struct else raise Not_found with Logic_monad.TacticFailure _ -> raise Not_found - let evars_eauto depth only_classes unique dep st hints p evd = + let evars_eauto depth only_classes unique dep st hints p evd env = let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in - let res = run_on_evars p evd eauto_tac in + let res = run_on_evars p evd eauto_tac env in match res with | None -> evd | Some evd' -> evd' - let typeclasses_eauto ?depth unique st hints p evd = - evars_eauto depth true unique false st hints p evd + let typeclasses_eauto ?depth unique st hints p evd env = + evars_eauto depth true unique false st hints p evd env (** Typeclasses eauto is an eauto which tries to resolve only goals of typeclass type, and assumes that the initially selected evars in evd are independent of the rest of the evars *) - let typeclasses_resolve debug depth unique p evd = + let typeclasses_resolve debug depth unique p evd env = let db = searchtable_map typeclasses_db in - typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd + typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd env end (** Binding to either V85 or Search implementations. *) @@ -1534,7 +1534,7 @@ let resolve_all_evars debug depth unique env p oevd do_split fail = if get_typeclasses_legacy_resolution () then V85.resolve_all_evars_once debug depth unique p evd else - Search.typeclasses_resolve debug depth unique p evd + Search.typeclasses_resolve debug depth unique p evd env in if has_undefined p oevd evd' then raise Unresolved; docomp evd' comps diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 64d4d3135..3d073c9dc 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -86,16 +86,16 @@ let rec prolog l n gl = let prol = (prolog l (n-1)) in (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl -let out_term = function +let out_term env = function | IsConstr (c, _) -> c - | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance (Global.env ()) gr)) + | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr)) let prolog_tac l n = Proofview.V82.tactic begin fun gl -> let map c = let (sigma, c) = c (pf_env gl) (project gl) in let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in - out_term c + out_term (pf_env gl) c in let l = List.map map l in try (prolog l n gl) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index d4cad3fa8..282b020ba 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -156,8 +156,9 @@ open Proofview.Notations (* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *) let match_eqdec sigma c = + Proofview.tclENV >>= fun env -> try - let (eqonleft,_,c1,c2,ty) = match_eqdec sigma c in + let (eqonleft,_,c1,c2,ty) = match_eqdec env sigma c in let (op,eq1,noteq,eq2) = match EConstr.kind sigma c with | App (op,[|ty1;ty2|]) -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 66345ce43..d08735582 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -334,25 +334,27 @@ let (forward_general_setoid_rewrite_clause, general_setoid_rewrite_clause) = Hoo (* Do we have a JMeq instance on twice the same domains ? *) -let jmeq_same_dom gl = function +let jmeq_same_dom env sigma = function | None -> true (* already checked in Hipattern.find_eq_data_decompose *) | Some t -> - let rels, t = decompose_prod_assum (project gl) t in - let env = push_rel_context rels (Proofview.Goal.env gl) in - match decompose_app (project gl) t with - | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2 + let rels, t = decompose_prod_assum sigma t in + let env = push_rel_context rels env in + match decompose_app sigma t with + | _, [dom1; _; dom2;_] -> is_conv env sigma dom1 dom2 | _ -> false (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. *) -let find_elim hdcncl lft2rgt dep cls ot gl = +let find_elim hdcncl lft2rgt dep cls ot = + Proofview.Goal.enter_one begin fun gl -> let sigma = project gl in let is_global gr c = Termops.is_global sigma gr c in let inccl = Option.is_empty cls in + let env = Proofview.Goal.env gl in if (is_global Coqlib.glob_eq hdcncl || (is_global Coqlib.glob_jmeq hdcncl && - jmeq_same_dom gl ot)) && not dep + jmeq_same_dom env sigma ot)) && not dep then let c = match EConstr.kind sigma hdcncl with @@ -382,9 +384,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl = Logic.eq or Jmeq just before *) assert false in - let (sigma, elim) = fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in - let elim = EConstr.of_constr elim in - (sigma, (elim, Safe_typing.empty_private_constants)) + pf_constr_of_global (ConstRef c) else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) @@ -400,14 +400,12 @@ let find_elim hdcncl lft2rgt dep cls ot gl = in match EConstr.kind sigma hdcncl with | Ind (ind,u) -> + let c, eff = find_scheme scheme_name ind in - (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *) - let (sigma, elim) = - fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) - in - let elim = EConstr.of_constr elim in - (sigma, (elim, eff)) + Proofview.tclEFFECTS eff <*> + pf_constr_of_global (ConstRef c) | _ -> assert false + end let type_of_clause cls gl = match cls with | None -> Proofview.Goal.concl gl @@ -420,9 +418,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in let dep = dep_proof_ok && dep_fun evd c type_of_cls in - let (sigma, (elim, effs)) = find_elim hdcncl lft2rgt dep cls (Some t) gl in - Proofview.Unsafe.tclEVARS sigma <*> - Proofview.tclEFFECTS effs <*> + find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim -> general_elim_clause with_evars frzevars tac cls c t l (match lft2rgt with None -> false | Some b -> b) {elimindex = None; elimbody = (elim,NoBindings); elimrename = None} @@ -536,7 +532,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = let do_hyps = (* If the term to rewrite uses an hypothesis H, don't rewrite in H *) let ids gl = - let ids_in_c = Termops.global_vars_set (Global.env()) (project gl) (fst c) in + let ids_in_c = Termops.global_vars_set (Proofview.Goal.env gl) (project gl) (fst c) in let ids_of_hyps = pf_ids_of_hyps gl in Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps in @@ -988,7 +984,7 @@ let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq = let sigma, i = build_coq_I sigma in let sigma, absurd_term = build_coq_False sigma in let eq_elim, eff = ind_scheme_of_eq lbeq in - let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in + let sigma, eq_elim = Evd.fresh_global env sigma eq_elim in let eq_elim = EConstr.of_constr eq_elim in sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term), eff @@ -1536,7 +1532,7 @@ let decomp_tuple_term env sigma c t = let rec decomprec inner_code ex exty = let iterated_decomp = try - let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose sigma ex in + let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose env sigma ex in let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code]) and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in let cdrtyp = beta_applist sigma (p,[car]) in diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 4101004d4..b057cf72b 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -280,10 +280,7 @@ let coq_refl_jm_pattern = open Globnames -let is_matching sigma x y = is_matching (Global.env ()) sigma x y -let matches sigma x y = matches (Global.env ()) sigma x y - -let match_with_equation sigma t = +let match_with_equation env sigma t = if not (isApp sigma t) then raise NoEquationFound; let (hdapp,args) = destApp sigma t in match EConstr.kind sigma hdapp with @@ -302,11 +299,11 @@ let match_with_equation sigma t = let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 1 then - if is_matching sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then + if is_matching env sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) - else if is_matching sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then + else if is_matching env sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if is_matching sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then + else if is_matching env sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) else raise NoEquationFound else raise NoEquationFound @@ -335,8 +332,8 @@ let is_equality_type sigma t = op2bool (match_with_equality_type sigma t) (** X1 -> X2 **) let coq_arrow_pattern = mkPattern (mkGArrow (mkGPatVar "X1") (mkGPatVar "X2")) -let match_arrow_pattern sigma t = - let result = matches sigma coq_arrow_pattern t in +let match_arrow_pattern env sigma t = + let result = matches env sigma coq_arrow_pattern t in match Id.Map.bindings result with | [(m1,arg);(m2,mind)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind) @@ -349,13 +346,13 @@ let match_with_imp_term sigma c = let is_imp_term sigma c = op2bool (match_with_imp_term sigma c) -let match_with_nottype sigma t = +let match_with_nottype env sigma t = try - let (arg,mind) = match_arrow_pattern sigma t in + let (arg,mind) = match_arrow_pattern env sigma t in if is_empty_type sigma mind then Some (mind,arg) else None with PatternMatchingFailure -> None -let is_nottype sigma t = op2bool (match_with_nottype sigma t) +let is_nottype env sigma t = op2bool (match_with_nottype env sigma t) (* Forall *) @@ -481,7 +478,7 @@ let dest_nf_eq gls eqn = (*** Sigma-types *) -let match_sigma sigma ex = +let match_sigma env sigma ex = match EConstr.kind sigma ex with | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_exist_ref) f -> build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr) @@ -489,19 +486,19 @@ let match_sigma sigma ex = build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr) | _ -> raise PatternMatchingFailure -let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *) - match_sigma ex +let find_sigma_data_decompose env ex = (* fails with PatternMatchingFailure *) + match_sigma env ex (* Pattern "(sig ?1 ?2)" *) let coq_sig_pattern = lazy (mkPattern (mkGAppRef coq_sig_ref [mkGPatVar "X1"; mkGPatVar "X2"])) -let match_sigma sigma t = - match Id.Map.bindings (matches sigma (Lazy.force coq_sig_pattern) t) with +let match_sigma env sigma t = + match Id.Map.bindings (matches env sigma (Lazy.force coq_sig_pattern) t) with | [(_,a); (_,p)] -> (a,p) | _ -> anomaly (Pp.str "Unexpected pattern.") -let is_matching_sigma sigma t = is_matching sigma (Lazy.force coq_sig_pattern) t +let is_matching_sigma env sigma t = is_matching env sigma (Lazy.force coq_sig_pattern) t (*** Decidable equalities *) @@ -533,15 +530,15 @@ let coq_eqdec_rev_pattern = coq_eqdec ~sum:coq_or_ref ~rev:true let op_or = coq_or_ref let op_sum = coq_sumbool_ref -let match_eqdec sigma t = +let match_eqdec env sigma t = let eqonleft,op,subst = - try true,op_sum,matches sigma (Lazy.force coq_eqdec_inf_pattern) t + try true,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_pattern) t with PatternMatchingFailure -> - try false,op_sum,matches sigma (Lazy.force coq_eqdec_inf_rev_pattern) t + try false,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_rev_pattern) t with PatternMatchingFailure -> - try true,op_or,matches sigma (Lazy.force coq_eqdec_pattern) t + try true,op_or,matches env sigma (Lazy.force coq_eqdec_pattern) t with PatternMatchingFailure -> - false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in + false,op_or,matches env sigma (Lazy.force coq_eqdec_rev_pattern) t in match Id.Map.bindings subst with | [(_,typ);(_,c1);(_,c2)] -> eqonleft, Lazy.force op, c1, c2, typ @@ -551,8 +548,8 @@ let match_eqdec sigma t = let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole])) let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef coq_False_ref))) -let is_matching_not sigma t = is_matching sigma (Lazy.force coq_not_pattern) t -let is_matching_imp_False sigma t = is_matching sigma (Lazy.force coq_imp_False_pattern) t +let is_matching_not env sigma t = is_matching env sigma (Lazy.force coq_not_pattern) t +let is_matching_imp_False env sigma t = is_matching env sigma (Lazy.force coq_imp_False_pattern) t (* Remark: patterns that have references to the standard library must be evaluated lazily (i.e. at the time they are used, not a the time diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 59406e158..8ff6fe95c 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -81,8 +81,8 @@ val is_inductive_equality : inductive -> bool val match_with_equality_type : (constr * constr list) matching_function val is_equality_type : testing_function -val match_with_nottype : (constr * constr) matching_function -val is_nottype : testing_function +val match_with_nottype : Environ.env -> (constr * constr) matching_function +val is_nottype : Environ.env -> testing_function val match_with_forall_term : (Name.t * constr * constr) matching_function val is_forall_term : testing_function @@ -114,7 +114,7 @@ type equation_kind = exception NoEquationFound val match_with_equation: - evar_map -> constr -> coq_eq_data option * constr * equation_kind + Environ.env -> evar_map -> constr -> coq_eq_data option * constr * equation_kind (***** Destructing patterns bound to some theory *) @@ -132,21 +132,21 @@ val find_eq_data : evar_map -> constr -> coq_eq_data * EInstance.t * equation_ki (** Match a term of the form [(existT A P t p)] Returns associated lemmas and [A,P,t,p] *) -val find_sigma_data_decompose : evar_map -> constr -> +val find_sigma_data_decompose : Environ.env -> evar_map -> constr -> coq_sigma_data * (EInstance.t * constr * constr * constr * constr) (** Match a term of the form [{x:A|P}], returns [A] and [P] *) -val match_sigma : evar_map -> constr -> constr * constr +val match_sigma : Environ.env -> evar_map -> constr -> constr * constr -val is_matching_sigma : evar_map -> constr -> bool +val is_matching_sigma : Environ.env -> evar_map -> constr -> bool (** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns [t,u,T] and a boolean telling if equality is on the left side *) -val match_eqdec : evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr +val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr) (** Match a negation *) -val is_matching_not : evar_map -> constr -> bool -val is_matching_imp_False : evar_map -> constr -> bool +val is_matching_not : Environ.env -> evar_map -> constr -> bool +val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cb905e749..5920b344d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3074,17 +3074,17 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] *) -let warn_unused_intro_pattern = +let warn_unused_intro_pattern env = CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics" (fun names -> strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_econstr (snd (c (Global.env()) Evd.empty)))) names) + (fun c -> Printer.pr_econstr (snd (c env Evd.empty)))) names) -let check_unused_names names = +let check_unused_names names env = if not (List.is_empty names) then - warn_unused_intro_pattern names + warn_unused_intro_pattern env names let intropattern_of_name gl avoid = function | Anonymous -> IntroNaming IntroAnonymous @@ -3204,7 +3204,8 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = peel_tac ra' dests names thin) end | [] -> - check_unused_names names; + Proofview.tclENV >>= fun env -> + check_unused_names names env; Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests) in peel_tac ra dests names [] @@ -3272,7 +3273,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = | Var id -> id | _ -> let type_of = Tacmach.New.pf_unsafe_type_of gl in - id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in + id_of_name_using_hdchar env sigma (type_of c) Anonymous in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) @@ -4485,7 +4486,7 @@ let induction_gen clear_flag isrec with_evars elim declaring the induction argument as a new local variable *) let id = (* Type not the right one if partially applied but anyway for internal use*) - let x = id_of_name_using_hdchar (Global.env()) evd t Anonymous in + let x = id_of_name_using_hdchar env evd t Anonymous in new_fresh_id [] x gl in let info_arg = (is_arg_pure_hyp, not enough_applied) in pose_induction_arg_then @@ -4521,8 +4522,9 @@ let induction_gen_l isrec with_evars elim names lc = Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in let sigma = Tacmach.New.project gl in + Proofview.tclENV >>= fun env -> let x = - id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in + id_of_name_using_hdchar env sigma (type_of c) Anonymous in let id = new_fresh_id [] x gl in let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in @@ -4741,8 +4743,9 @@ let prove_symmetry hdcncl eq_kind = one_constructor 1 NoBindings ]) let match_with_equation sigma c = + Proofview.tclENV >>= fun env -> try - let res = match_with_equation sigma c in + let res = match_with_equation env sigma c in Proofview.tclUNIT res with NoEquationFound -> Proofview.tclZERO NoEquationFound -- cgit v1.2.3 From 5c7d5fce3ed1de62ff5e1528a12adce0cdf2b0d9 Mon Sep 17 00:00:00 2001 From: amblaf Date: Tue, 20 Jun 2017 09:43:11 +0200 Subject: env, sigma as first arguments of functions --- tactics/class_tactics.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 36785b15d..e8c96b7cd 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1342,7 +1342,7 @@ module Search = struct | Some i -> str ", with depth limit " ++ int i)); tac - let run_on_evars p evm tac env = + let run_on_evars env evm p tac = match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) | Some (goals, evm') -> @@ -1374,22 +1374,22 @@ module Search = struct else raise Not_found with Logic_monad.TacticFailure _ -> raise Not_found - let evars_eauto depth only_classes unique dep st hints p evd env = + let evars_eauto env evd depth only_classes unique dep st hints p = let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in - let res = run_on_evars p evd eauto_tac env in + let res = run_on_evars env evd p eauto_tac in match res with | None -> evd | Some evd' -> evd' - let typeclasses_eauto ?depth unique st hints p evd env = - evars_eauto depth true unique false st hints p evd env + let typeclasses_eauto env evd ?depth unique st hints p = + evars_eauto env evd depth true unique false st hints p (** Typeclasses eauto is an eauto which tries to resolve only goals of typeclass type, and assumes that the initially selected evars in evd are independent of the rest of the evars *) - let typeclasses_resolve debug depth unique p evd env = + let typeclasses_resolve env evd debug depth unique p = let db = searchtable_map typeclasses_db in - typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd env + typeclasses_eauto env evd ?depth unique (Hint_db.transparent_state db) [db] p end (** Binding to either V85 or Search implementations. *) @@ -1534,7 +1534,7 @@ let resolve_all_evars debug depth unique env p oevd do_split fail = if get_typeclasses_legacy_resolution () then V85.resolve_all_evars_once debug depth unique p evd else - Search.typeclasses_resolve debug depth unique p evd env + Search.typeclasses_resolve env evd debug depth unique p in if has_undefined p oevd evd' then raise Unresolved; docomp evd' comps -- cgit v1.2.3 From b84ab413f8434719dbbf5e09da9a0698b84b0106 Mon Sep 17 00:00:00 2001 From: amblaf Date: Tue, 20 Jun 2017 09:48:55 +0200 Subject: Replacing tclENV with the goal environment In functions match_eqdec and check_unused_names --- tactics/eqdecide.ml | 9 +++++---- tactics/tactics.ml | 15 +++++++++------ 2 files changed, 14 insertions(+), 10 deletions(-) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 282b020ba..e16fcec7c 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -155,8 +155,7 @@ open Proofview.Notations (* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *) -let match_eqdec sigma c = - Proofview.tclENV >>= fun env -> +let match_eqdec env sigma c = try let (eqonleft,_,c1,c2,ty) = match_eqdec env sigma c in let (op,eq1,noteq,eq2) = @@ -203,8 +202,9 @@ let solveEqBranch rectype = begin Proofview.Goal.enter begin fun gl -> let concl = pf_concl gl in + let env = Proofview.Goal.env gl in let sigma = project gl in - match_eqdec sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) -> + match_eqdec env sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in let nparams = mib.mind_nparams in let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in @@ -230,8 +230,9 @@ let decideGralEquality = begin Proofview.Goal.enter begin fun gl -> let concl = pf_concl gl in + let env = Proofview.Goal.env gl in let sigma = project gl in - match_eqdec sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) -> + match_eqdec env sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) -> let headtyp = hd_app sigma (pf_compute gl typ) in begin match EConstr.kind sigma headtyp with | Ind (mi,_) -> Proofview.tclUNIT mi diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5920b344d..b194ac5a9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3074,17 +3074,17 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] *) -let warn_unused_intro_pattern env = +let warn_unused_intro_pattern env sigma = CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics" (fun names -> strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_econstr (snd (c env Evd.empty)))) names) + (fun c -> Printer.pr_econstr (snd (c env sigma)))) names) -let check_unused_names names env = +let check_unused_names env sigma names = if not (List.is_empty names) then - warn_unused_intro_pattern env names + warn_unused_intro_pattern env sigma names let intropattern_of_name gl avoid = function | Anonymous -> IntroNaming IntroAnonymous @@ -3204,9 +3204,12 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = peel_tac ra' dests names thin) end | [] -> - Proofview.tclENV >>= fun env -> - check_unused_names names env; + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + check_unused_names env sigma names; Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests) + end in peel_tac ra dests names [] -- cgit v1.2.3 From 1c10b84c0ce5f96a3afd1fc83c738c76070958c3 Mon Sep 17 00:00:00 2001 From: amblaf Date: Tue, 27 Jun 2017 08:38:20 +0200 Subject: Correcting [build_discriminator] to make the test-suite pass --- API/API.mli | 2 +- plugins/cc/cctac.ml | 3 ++- tactics/equality.ml | 62 +++++++++++++++++++++++++++------------------------- tactics/equality.mli | 2 +- 4 files changed, 36 insertions(+), 33 deletions(-) diff --git a/API/API.mli b/API/API.mli index 19726b52f..3905843a5 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5233,7 +5233,7 @@ sig val build_selector : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types -> - EConstr.constr -> EConstr.constr -> Evd.evar_map * EConstr.constr + EConstr.constr -> EConstr.constr -> EConstr.constr val replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic val general_rewrite : orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 4934b0750..11d3a6d1f 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -231,7 +231,8 @@ let make_prb gls depth additionnal_terms = let build_projection intype (cstr:pconstructor) special default gls= let open Tacmach.New in let ci= (snd(fst cstr)) in - let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in + let sigma = project gls in + let body=Equality.build_selector (pf_env gls) sigma ci (mkRel 1) intype special default in let id=pf_get_new_id (Id.of_string "t") gls in sigma, mkLambda(Name id,intype,body) diff --git a/tactics/equality.ml b/tactics/equality.ml index d08735582..6274bca9f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -854,7 +854,8 @@ let descend_then env sigma head dirn = let IndType (indf,_) = try find_rectype env sigma (get_type_of env sigma head) with Not_found -> - user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") in + user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") + in let indp,_ = (dest_ind_family indf) in let ind, _ = check_privacy env indp in let (mib,mip) = lookup_mind_specif env ind in @@ -876,7 +877,7 @@ let descend_then env sigma head dirn = List.map build_branch (List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - sigma, Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl))) + Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl))) (* Now we need to construct the discriminator, given a discriminable position. This boils down to: @@ -921,23 +922,20 @@ let build_selector env sigma dirn c ind special default = let brl = List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - sigma, mkCase (ci, p, c, Array.of_list brl) + mkCase (ci, p, c, Array.of_list brl) -let build_coq_False sigma = Evarutil.new_global sigma (build_coq_False ()) -let build_coq_True sigma = Evarutil.new_global sigma (build_coq_True ()) -let build_coq_I sigma = Evarutil.new_global sigma (build_coq_I ()) +let build_coq_False () = pf_constr_of_global (build_coq_False ()) +let build_coq_True () = pf_constr_of_global (build_coq_True ()) +let build_coq_I () = pf_constr_of_global (build_coq_I ()) -let rec build_discriminator env sigma dirn c = function +let rec build_discriminator env sigma true_0 false_0 dirn c = function | [] -> let ind = get_type_of env sigma c in - let sigma, true_0 = build_coq_True sigma in - let sigma, false_0 = build_coq_False sigma in build_selector env sigma dirn c ind true_0 false_0 | ((sp,cnum),argnum)::l -> - let sigma, false_0 = build_coq_False sigma in let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in - let sigma, subval = build_discriminator cnum_env sigma dirn newc l in + let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in kont sigma subval (false_0,mkSort (Prop Null)) (* Note: discrimination could be more clever: if some elimination is @@ -980,14 +978,15 @@ let ind_scheme_of_eq lbeq = ConstRef c, eff -let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq = - let sigma, i = build_coq_I sigma in - let sigma, absurd_term = build_coq_False sigma in +let discrimination_pf e (t,t1,t2) discriminator lbeq = + build_coq_I () >>= fun i -> + build_coq_False () >>= fun absurd_term -> let eq_elim, eff = ind_scheme_of_eq lbeq in - let sigma, eq_elim = Evd.fresh_global env sigma eq_elim in - let eq_elim = EConstr.of_constr eq_elim in - sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term), - eff + Proofview.tclEFFECTS eff <*> + pf_constr_of_global eq_elim >>= fun eq_elim -> + Proofview.tclUNIT + (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term) + let eq_baseid = Id.of_string "e" @@ -1001,19 +1000,22 @@ let apply_on_clause (f,t) clause = clenv_fchain ~with_univs:false argmv f_clause clause let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = + build_coq_True () >>= fun true_0 -> + build_coq_False () >>= fun false_0 -> let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in - let sigma, discriminator = - build_discriminator e_env sigma dirn (mkVar e) cpath in - let sigma,(pf, absurd_term), eff = - discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in - let pf_ty = mkArrow eqn absurd_term in - let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in - let pf = Clenvtac.clenv_value_cast_meta absurd_clause in - Proofview.Unsafe.tclEVARS sigma <*> - Proofview.tclEFFECTS eff <*> - tclTHENS (assert_after Anonymous absurd_term) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] + try + let discriminator = + build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath + in + discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) -> + let pf_ty = mkArrow eqn absurd_term in + let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in + let pf = Clenvtac.clenv_value_cast_meta absurd_clause in + tclTHENS (assert_after Anonymous absurd_term) + [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] + with + UserError _ as ex -> Proofview.tclZERO ex let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1299,7 +1301,7 @@ let rec build_injrec env sigma dflt c = function let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let sigma, (subval,tuplety,dfltval) = build_injrec cnum_env sigma dflt newc l in - let sigma, res = kont sigma subval (dfltval,tuplety) in + let res = kont sigma subval (dfltval,tuplety) in sigma, (res, tuplety,dfltval) with UserError _ -> failwith "caught" diff --git a/tactics/equality.mli b/tactics/equality.mli index 421f7c7f5..a4d1c0f9b 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -126,4 +126,4 @@ val set_eq_dec_scheme_kind : mutual scheme_kind -> unit (* [build_selector env sigma i c t u v] matches on [c] of type [t] and returns [u] in branch [i] and [v] on other branches *) val build_selector : env -> evar_map -> int -> constr -> types -> - constr -> constr -> evar_map * constr + constr -> constr -> constr -- cgit v1.2.3 From 7ba6bc4554a642f78f59b996f99d9d6ca2cc2678 Mon Sep 17 00:00:00 2001 From: amblaf Date: Wed, 12 Jul 2017 15:44:37 +0200 Subject: better `try with` scope in `discr_positions` --- tactics/equality.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index 6274bca9f..ad6abfa1f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1004,18 +1004,20 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = build_coq_False () >>= fun false_0 -> let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in - try - let discriminator = - build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath - in + let discriminator = + try + Proofview.tclUNIT + (build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath) + with + UserError _ as ex -> Proofview.tclZERO ex + in + discriminator >>= fun discriminator -> discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) -> let pf_ty = mkArrow eqn absurd_term in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenvtac.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous absurd_term) [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] - with - UserError _ as ex -> Proofview.tclZERO ex let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in -- cgit v1.2.3