diff options
Diffstat (limited to 'tactics/equality.ml')
-rw-r--r-- | tactics/equality.ml | 102 |
1 files changed, 51 insertions, 51 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 66345ce43..ad6abfa1f 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 @@ -858,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 @@ -880,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: @@ -925,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 @@ -984,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 (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" @@ -1005,19 +1000,24 @@ 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))] + 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))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1303,7 +1303,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" @@ -1536,7 +1536,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 |