diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 81 |
1 files changed, 35 insertions, 46 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 96b61b6994..7393454ba9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -72,7 +72,6 @@ let use_injection_in_context = function let () = declare_bool_option { optdepr = false; - optname = "injection in context"; optkey = ["Structural";"Injection"]; optread = (fun () -> !injection_in_context) ; optwrite = (fun b -> injection_in_context := b) } @@ -356,7 +355,7 @@ let find_elim hdcncl lft2rgt dep cls ot = Proofview.Goal.enter_one begin fun gl -> let sigma = project gl in let is_global_exists gr c = - Coqlib.has_ref gr && Termops.is_global sigma (Coqlib.lib_ref gr) c + Coqlib.has_ref gr && isRefX sigma (Coqlib.lib_ref gr) c in let inccl = Option.is_empty cls in let env = Proofview.Goal.env gl in @@ -734,7 +733,6 @@ let keep_proof_equalities_for_injection = ref false let () = declare_bool_option { optdepr = false; - optname = "injection on prop arguments"; optkey = ["Keep";"Proof";"Equalities"]; optread = (fun () -> !keep_proof_equalities_for_injection) ; optwrite = (fun b -> keep_proof_equalities_for_injection := b) } @@ -1062,14 +1060,14 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let onEquality with_evars tac (c,lbindc) = Proofview.Goal.enter begin fun gl -> - let type_of = pf_unsafe_type_of gl in let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in - let t = type_of c in + let t = pf_get_type_of gl c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in let eqn = clenv_type eq_clause' in - let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in + (* FIXME evar leak *) + let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) (tac (eq,eqn,eq_args) eq_clause') @@ -1165,7 +1163,7 @@ let minimal_free_rels_rec env sigma = let rec minimalrec_free_rels_rec prev_rels (c,cty) = let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in let combined_rels = Int.Set.union prev_rels direct_rels in - let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i))) + let folder rels i = snd (minimalrec_free_rels_rec rels (c, get_type_of env sigma (mkRel i))) in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels))) in minimalrec_free_rels_rec Int.Set.empty @@ -1210,7 +1208,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let rec sigrec_clausal_form sigma siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) - let dflt_typ = unsafe_type_of env sigma dflt in + let sigma, dflt_typ = type_of env sigma dflt in try let sigma = Evarconv.unify_leq_delay env sigma dflt_typ p_i in let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in @@ -1224,29 +1222,21 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigma, ev = Evarutil.new_evar env sigma a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in - let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in - match evopt with - | Some w -> - let w_type = unsafe_type_of env sigma w in - begin match Evarconv.unify_leq_delay env sigma w_type a with - | sigma -> - let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in - sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) - | exception Evarconv.UnableToUnify _ -> - user_err Pp.(str "Cannot solve a unification problem.") - end - | None -> - (* This at least happens if what has been detected as a - dependency is not one; use an evasive error message; - even if the problem is upwards: unification should be - tried in the first place in make_iterated_tuple instead - of approximatively computing the free rels; then - unsolved evars would mean not binding rel *) - user_err Pp.(str "Cannot solve a unification problem.") + if EConstr.isEvar sigma ev then + (* This at least happens if what has been detected as a + dependency is not one; use an evasive error message; + even if the problem is upwards: unification should be + tried in the first place in make_iterated_tuple instead + of approximatively computing the free rels; then + unsolved evars would mean not binding rel *) + user_err Pp.(str "Cannot solve a unification problem.") + else + let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in + sigma, applist(exist_term,[a;p_i_minus_1;ev;tuple_tail]) in let sigma = Evd.clear_metas sigma in let sigma, scf = sigrec_clausal_form sigma siglen ty in - sigma, Evarutil.nf_evar sigma scf + sigma, Evarutil.nf_evar sigma scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors @@ -1319,7 +1309,7 @@ let make_iterated_tuple env sigma dflt (z,zty) = sigma, (tuple,tuplety,dfltval) let rec build_injrec env sigma dflt c = function - | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c) + | [] -> make_iterated_tuple env sigma dflt (c,get_type_of env sigma c) | ((sp,cnum),argnum)::l -> try let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in @@ -1341,17 +1331,17 @@ let inject_if_homogenous_dependent_pair ty = Proofview.Goal.enter begin fun gl -> try let sigma = Tacmach.New.project gl in - let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in + let eq,u,(t,t1,t2) = pf_apply find_this_eq_data_decompose gl ty in (* fetch the informations of the pair *) let sigTconstr = Coqlib.(lib_ref "core.sigT.type") in let existTconstr = Coqlib.lib_ref "core.sigT.intro" in (* check whether the equality deals with dep pairs or not *) let eqTypeDest = fst (decompose_app sigma t) in - if not (Termops.is_global sigma sigTconstr eqTypeDest) then raise Exit; + if not (isRefX sigma sigTconstr eqTypeDest) then raise Exit; let hd1,ar1 = decompose_app_vect sigma t1 and hd2,ar2 = decompose_app_vect sigma t2 in - if not (Termops.is_global sigma existTconstr hd1) then raise Exit; - if not (Termops.is_global sigma existTconstr hd2) then raise Exit; + if not (isRefX sigma existTconstr hd1) then raise Exit; + if not (isRefX sigma existTconstr hd2) then raise Exit; let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in (* check if the user has declared the dec principle *) (* and compare the fst arguments of the dep pair *) @@ -1360,7 +1350,7 @@ let inject_if_homogenous_dependent_pair ty = if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; check_required_library ["Coq";"Logic";"Eqdep_dec"]; - let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in + let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in (* cut with the good equality and prove the requested goal *) @@ -1603,7 +1593,7 @@ let cutSubstInConcl l2r eqn = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in + let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in let typ = pf_concl gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in @@ -1620,7 +1610,7 @@ let cutSubstInHyp l2r eqn id = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in + let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in let typ = pf_get_hyp_typ id gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in @@ -1694,14 +1684,13 @@ let regular_subst_tactic = ref true let () = declare_bool_option { optdepr = false; - optname = "more regular behavior of tactic subst"; optkey = ["Regular";"Subst";"Tactic"]; optread = (fun () -> !regular_subst_tactic); optwrite = (:=) regular_subst_tactic } let restrict_to_eq_and_identity eq = (* compatibility *) - if not (is_global (lib_ref "core.eq.type") eq) && - not (is_global (lib_ref "core.identity.type") eq) + if not (Constr.isRefX (lib_ref "core.eq.type") eq) && + not (Constr.isRefX (lib_ref "core.identity.type") eq) then raise Constr_matching.PatternMatchingFailure exception FoundHyp of (Id.t * constr * bool) @@ -1715,7 +1704,7 @@ let is_eq_x gl x d = | _ -> false in let c = pf_nf_evar gl (NamedDecl.get_type d) in - let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in + let (_,lhs,rhs) = pi3 (pf_apply find_eq_data_decompose gl c) in if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true)); if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false)) with Constr_matching.PatternMatchingFailure -> @@ -1812,7 +1801,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let find_equations gl = let env = Proofview.Goal.env gl in let sigma = project gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let select_equation_name decl = try let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in @@ -1837,7 +1826,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = Proofview.Goal.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in - let find_eq_data_decompose = find_eq_data_decompose 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 *) @@ -1863,7 +1852,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let-ins *) Proofview.Goal.enter begin fun gl -> let sigma = project gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let test (_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in @@ -1887,19 +1876,19 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let cond_eq_term_left c t gl = try - let (_,x,_) = pi3 (find_eq_data_decompose gl t) in + let (_,x,_) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else failwith "not convertible" with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term_right c t gl = try - let (_,_,x) = pi3 (find_eq_data_decompose gl t) in + let (_,_,x) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then false else failwith "not convertible" with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term c t gl = try - let (_,x,y) = pi3 (find_eq_data_decompose gl t) in + let (_,x,y) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else if pf_conv_x gl c y then false else failwith "not convertible" |