diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml | 2 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 115 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 5 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 84 | ||||
| -rw-r--r-- | tactics/tactics.mli | 6 |
8 files changed, 163 insertions, 60 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 28b5ed5811..7b323ee0ed 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -485,7 +485,7 @@ let unfold_head env sigma (ids, csts) c = true, EConstr.of_constr (Environ.constant_value_in env (cst, u)) | App (f, args) -> (match aux f with - | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args)) + | true, f' -> true, Reductionops.whd_betaiota env sigma (mkApp (f', args)) | false, _ -> let done_, args' = Array.fold_left_i (fun i (done_, acc) arg -> diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 7c702eab3a..6da2248cc3 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -653,7 +653,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p) (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp) (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind) - (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma + (EConstr.Unsafe.to_constr (Reductionops.whd_beta env sigma (EConstr.of_constr (applist (c, Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))))) in c', ctx' diff --git a/tactics/equality.ml b/tactics/equality.ml index f3073acb0a..58345ac253 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -423,7 +423,8 @@ let type_of_clause cls gl = match cls with let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = Proofview.Goal.enter begin fun gl -> let evd = Proofview.Goal.sigma gl in - let isatomic = isProd evd (whd_zeta evd hdcncl) in + let env = Proofview.Goal.env gl in + let isatomic = isProd evd (whd_zeta env evd hdcncl) in 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 @@ -458,7 +459,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in - let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in + let rels, t = decompose_prod_assum sigma (whd_betaiotazeta env sigma ctype) in match match_with_equality_type env sigma t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in @@ -475,7 +476,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac Proofview.tclEVARMAP >>= fun sigma -> let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) - match match_with_equality_type env sigma t' with + match match_with_equality_type env' sigma t' with | Some (hdcncl,args) -> let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c @@ -1043,7 +1044,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = 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 false_0) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))] + [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1214,7 +1215,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = with Evarconv.UnableToUnify _ -> user_err Pp.(str "Cannot solve a unification problem.") else - let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with + let (a,p_i_minus_1) = match whd_beta_stack env sigma p_i with | (_sigS,[a;p]) -> (a, p) | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in let sigma, ev = Evarutil.new_evar env sigma a in @@ -1360,8 +1361,8 @@ let inject_if_homogenous_dependent_pair ty = tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar sigma hyp]; Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 -> - Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr - (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))) + Refiner.refiner ~check:true EConstr.Unsafe.(to_constr + (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) ])] with Exit -> Proofview.tclUNIT () @@ -1406,7 +1407,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (Proofview.tclIGNORE (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) [inject_if_homogenous_dependent_pair ty; - Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))]) + Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) @@ -1707,12 +1708,42 @@ let is_eq_x gl x d = with Constr_matching.PatternMatchingFailure -> () +exception FoundDepInGlobal of Id.t option * GlobRef.t + +let test_non_indirectly_dependent_section_variable gl x = + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let hyps = Proofview.Goal.hyps gl in + let concl = Proofview.Goal.concl gl in + List.iter (fun decl -> + NamedDecl.iter_constr (fun c -> + match occur_var_indirectly env sigma x c with + | Some gr -> raise (FoundDepInGlobal (Some (NamedDecl.get_id decl), gr)) + | None -> ()) decl) hyps; + match occur_var_indirectly env sigma x concl with + | Some gr -> raise (FoundDepInGlobal (None, gr)) + | None -> () + +let check_non_indirectly_dependent_section_variable gl x = + try test_non_indirectly_dependent_section_variable gl x + with FoundDepInGlobal (pos,gr) -> + let where = match pos with + | Some id -> str "hypothesis " ++ Id.print id + | None -> str "the conclusion of the goal" in + user_err ~hdr:"Subst" + (strbrk "Section variable " ++ Id.print x ++ + strbrk " occurs implicitly in global declaration " ++ Printer.pr_global gr ++ + strbrk " present in " ++ where ++ strbrk ".") + +let is_non_indirectly_dependent_section_variable gl z = + try test_non_indirectly_dependent_section_variable gl z; true + with FoundDepInGlobal (pos,gr) -> false + (* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and erase hyp and x; proceed by generalizing all dep hyps *) let subst_one dep_proof_ok x (hyp,rhs,dir) = Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in @@ -1721,7 +1752,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> let id = NamedDecl.get_id dcl in if not (Id.equal id hyp) - && List.exists (fun y -> occur_var_in_decl env sigma y dcl) deps + && List.exists (fun y -> local_occur_var_in_decl sigma y dcl) deps then let id_dest = if !regular_subst_tactic then dest else MoveLast in (dest,id::deps,(id_dest,id)::allhyps) @@ -1730,7 +1761,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = hyps (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *) (* Decides if x appears in conclusion *) - let depconcl = occur_var env sigma x concl in + let depconcl = local_occur_var sigma x concl in let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then @@ -1761,6 +1792,8 @@ let subst_one_var dep_proof_ok x = (str "Cannot find any non-recursive equality over " ++ Id.print x ++ str".") with FoundHyp res -> res in + if is_section_variable x then + check_non_indirectly_dependent_section_variable gl x; subst_one dep_proof_ok x res end @@ -1794,53 +1827,37 @@ let subst_all ?(flags=default_subst_tactic_flags) () = if !regular_subst_tactic then - (* First step: find hypotheses to treat in linear time *) - let find_equations gl = - let env = Proofview.Goal.env gl in - let sigma = project gl in - let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in - let select_equation_name decl = + (* Find hypotheses to treat in linear time *) + let process hyp = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = project gl in + let c = pf_get_hyp hyp gl |> NamedDecl.get_type in try - let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in + let lbeq,u,(_,x,y) = pf_apply find_eq_data_decompose gl c in let u = EInstance.kind sigma u in let eq = Constr.mkRef (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match EConstr.kind sigma x, EConstr.kind sigma y with - | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> - Some (NamedDecl.get_id decl) - | _, Var z when not (is_evaluable env (EvalVarRef z)) -> - Some (NamedDecl.get_id decl) + | Var x, Var y when Id.equal x y -> + Proofview.tclUNIT () + | Var x', _ when not (Termops.local_occur_var sigma x' y) && + not (is_evaluable env (EvalVarRef x')) && + is_non_indirectly_dependent_section_variable gl x' -> + subst_one flags.rewrite_dependent_proof x' (hyp,y,true) + | _, Var y' when not (Termops.local_occur_var sigma y' x) && + not (is_evaluable env (EvalVarRef y')) && + is_non_indirectly_dependent_section_variable gl y' -> + subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> - None - with Constr_matching.PatternMatchingFailure -> None + Proofview.tclUNIT () + with Constr_matching.PatternMatchingFailure -> + Proofview.tclUNIT () + end in - let hyps = Proofview.Goal.hyps gl in - List.rev (List.map_filter select_equation_name hyps) - in - - (* Second step: treat equations *) - let process hyp = Proofview.Goal.enter begin fun gl -> - let sigma = project gl in - let env = Proofview.Goal.env gl in - let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in - let c = pf_get_hyp hyp gl |> NamedDecl.get_type in - let _,_,(_,x,y) = find_eq_data_decompose c in - (* J.F.: added to prevent failure on goal containing x=x as an hyp *) - if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else - match EConstr.kind sigma x, EConstr.kind sigma y with - | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) -> - subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) -> - subst_one flags.rewrite_dependent_proof y' (hyp,x,false) - | _ -> - Proofview.tclUNIT () + tclMAP process (List.rev (List.map NamedDecl.get_id (Proofview.Goal.hyps gl))) end - in - Proofview.Goal.enter begin fun gl -> - let ids = find_equations gl in - tclMAP process ids - end else diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 76b1c94759..5338e0eef5 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -88,9 +88,9 @@ let is_lax_conjunction = function let prod_assum sigma t = fst (decompose_prod_assum sigma t) (* whd_beta normalize the types of arguments in a product *) -let rec whd_beta_prod sigma c = match EConstr.kind sigma c with - | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta sigma t,whd_beta_prod sigma c) - | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c) +let rec whd_beta_prod env sigma c = match EConstr.kind sigma c with + | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta env sigma t,whd_beta_prod env sigma c) + | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod env sigma c) | _ -> c let match_with_one_constructor env sigma style onlybinary allow_rec t = @@ -119,7 +119,7 @@ let match_with_one_constructor env sigma style onlybinary allow_rec t = else let ctx, cty = mip.mind_nf_lc.(0) in let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in - let ctyp = whd_beta_prod sigma + let ctyp = whd_beta_prod env sigma (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod env sigma ctyp then diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 8f6844079b..374706c8f9 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -29,6 +29,8 @@ module NamedDecl = Context.Named.Declaration type tactic = Proofview.V82.tac +[@@@ocaml.warning "-3"] + let tclIDTAC = Refiner.tclIDTAC let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE let tclORELSE0 = Refiner.tclORELSE0 @@ -368,6 +370,9 @@ module New = struct Proofview.Unsafe.tclNEWGOALS tl <*> Proofview.tclUNIT ans + let tclTHENSLASTn t1 repeat l = + tclTHENS3PARTS t1 [||] repeat l + let tclTHENLASTn t1 l = tclTHENS3PARTS t1 [||] (tclUNIT()) l let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|] diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 9ec558f1ad..01565169ca 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -180,6 +180,7 @@ module New : sig middle. Raises an error if the number of resulting subgoals is strictly less than [n+m] *) val tclTHENS3PARTS : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic + val tclTHENSLASTn : unit tactic -> unit tactic -> unit tactic array -> unit tactic val tclTHENSFIRSTn : unit tactic -> unit tactic array -> unit tactic -> unit tactic val tclTHENFIRSTn : unit tactic -> unit tactic array -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0df4f5b207..378b6c7418 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1319,7 +1319,7 @@ let cut c = let r = Sorts.relevance_of_sort s in let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in (* Backward compat: normalize [c]. *) - let c = if normalize_cut then local_strong whd_betaiota sigma c else c in + let c = if normalize_cut then strong whd_betaiota env sigma c else c in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun h -> let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in @@ -1368,7 +1368,7 @@ let clenv_refine_in with_evars targetid id sigma0 clenv tac = if not with_evars && occur_meta clenv.evd new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in - let exact_tac = Proofview.V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf)) in + let exact_tac = Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in let naming = NamingMustBe (CAst.make targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN @@ -1607,7 +1607,7 @@ let make_projection env sigma params cstr sign elim i n c u = noccur_between sigma 1 (n-i-1) t (* to avoid surprising unifications, excludes flexible projection types or lambda which will be instantiated by Meta/Evar *) - && not (isEvar sigma (fst (whd_betaiota_stack sigma t))) + && not (isEvar sigma (fst (whd_betaiota_stack env sigma t))) && (accept_universal_lemma_under_conjunctions () || not (isRel sigma t)) then let t = lift (i+1-n) t in @@ -1670,7 +1670,7 @@ let descend_in_conjunctions avoid tac (err, info) c = | Some (p,pt) -> Tacticals.New.tclTHENS (assert_before_gen false (NamingAvoid avoid) pt) - [Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p)); + [refiner ~check:true EConstr.Unsafe.(to_constr p); (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] end))) @@ -3025,7 +3025,7 @@ let specialize (c,lbind) ipat = let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let sigma = clause.evd in - let (thd,tstack) = whd_nored_stack sigma (clenv_value clause) in + let (thd,tstack) = whd_nored_stack env sigma (clenv_value clause) in (* The completely applied term is (thd tstack), but tstack may contain unsolved metas, so now we must reabstract them args with there name to have @@ -5045,6 +5045,80 @@ let unify ?(state=TransparentState.full) x y = Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None))) end +(** [tclWRAPFINALLY before tac finally] runs [before] before each + entry-point of [tac] and passes the result of [before] to + [finally], which is then run at each exit-point of [tac], + regardless of whether it succeeds or fails. Said another way, if + [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun + ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with + [e], it behaves as [before >>= fun v -> finally v <*> tclZERO + e]. Note that if [tac] succeeds [n] times before finally failing, + [before] and [finally] are both run [n+1] times (once around each + succuess, and once more around the final failure). *) +(* We should probably export this somewhere, but it's not clear + where. As per + https://github.com/coq/coq/pull/12197#discussion_r418480525 and + https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef, we don't + export it from Proofview, because it seems somehow not primitive + enough. We don't export it from this file because it is more of a + tactical than a tactic. But we also don't export it from Tacticals + because all of the non-New tacticals there operate on `tactic`, not + `Proofview.tactic`, and all of the `New` tacticals that deal with + multi-success things are focussing, i.e., apply their arguments on + each goal separately (and it even says so in the comment on `New`), + whereas it's important that `tclWRAPFINALLY` doesn't introduce + extra focussing. *) +let rec tclWRAPFINALLY before tac finally = + let open Proofview in + let open Proofview.Notations in + before >>= fun v -> tclCASE tac >>= function + | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e + | Next (ret, tac') -> tclOR + (finally v >>= fun () -> tclUNIT ret) + (fun e -> tclWRAPFINALLY before (tac' e) finally) + +let with_set_strategy lvl_ql k = + let glob_key r = + match r with + | GlobRef.ConstRef sp -> ConstKey sp + | GlobRef.VarRef id -> VarKey id + | _ -> user_err Pp.(str + "cannot set an inductive type or a constructor as transparent") in + let kl = List.concat (List.map (fun (lvl, ql) -> List.map (fun q -> (lvl, glob_key q)) ql) lvl_ql) in + tclWRAPFINALLY + (Proofview.tclENV >>= fun env -> + let orig_kl = List.map (fun (_lvl, k) -> + (Conv_oracle.get_strategy (Environ.oracle env) k, k)) + kl in + (* Because the global env might be desynchronized from the + proof-local env, we need to update the global env to have this + tactic play nicely with abstract. + TODO: When abstract no longer depends on Global, delete this + let orig_kl_global = ... in *) + let orig_kl_global = List.map (fun (_lvl, k) -> + (Conv_oracle.get_strategy (Environ.oracle (Global.env ())) k, k)) + kl in + let env = List.fold_left (fun env (lvl, k) -> + Environ.set_oracle env + (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env kl in + Proofview.Unsafe.tclSETENV env <*> + (* TODO: When abstract no longer depends on Global, remove this + [Proofview.tclLIFT] block *) + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + List.iter (fun (lvl, k) -> Global.set_strategy k lvl) kl)) <*> + Proofview.tclUNIT (orig_kl, orig_kl_global)) + k + (fun (orig_kl, orig_kl_global) -> + (* TODO: When abstract no longer depends on Global, remove this + [Proofview.tclLIFT] block *) + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + List.iter (fun (lvl, k) -> Global.set_strategy k lvl) orig_kl_global)) <*> + Proofview.tclENV >>= fun env -> + let env = List.fold_left (fun env (lvl, k) -> + Environ.set_oracle env + (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env orig_kl in + Proofview.Unsafe.tclSETENV env) + module Simple = struct (** Simplified version of some of the above tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c84ba17f23..b6eb48a3d9 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -435,6 +435,12 @@ val declare_intro_decomp_eq : (types * constr * constr) -> constr * types -> unit Proofview.tactic) -> unit +(** Tactic analogous to the [Strategy] vernacular, but only applied + locally to the tactic argument *) +val with_set_strategy : + (Conv_oracle.level * Names.GlobRef.t list) list -> + 'a Proofview.tactic -> 'a Proofview.tactic + (** {6 Simple form of basic tactics. } *) module Simple : sig |