diff options
Diffstat (limited to 'plugins/cc/cctac.ml')
| -rw-r--r-- | plugins/cc/cctac.ml | 49 |
1 files changed, 32 insertions, 17 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 8884aef1..068cb25c 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -46,7 +46,7 @@ let whd_delta env= (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = family_of_sort (sort_of env (ref sigma) c) +let sf_of env sigma c = sort_of env (ref sigma) c let rec decompose_term env sigma t= match kind_of_term (whd env t) with @@ -253,9 +253,15 @@ let new_app_global f args k = let new_refine c = Proofview.V82.tactic (refine c) +let assert_before n c = + Proofview.Goal.enter begin fun gl -> + let evm, _ = Tacmach.New.pf_apply type_of gl c in + Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) + end + let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.nf_enter begin fun gl -> - let type_of t = Tacmach.New.pf_type_of gl t in + let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check c @@ -302,9 +308,9 @@ let rec proof_tac p : unit Proofview.tactic = Tacticals.New.tclFIRST [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2); reflexivity; - Proofview.tclZERO (UserError ("Congruence" , + Tacticals.New.tclZEROMSG (Pp.str - "I don't know how to handle dependent equality")))]] + "I don't know how to handle dependent equality")]] | Inject (prf,cstr,nargs,argind) -> let ti=constr_of_term prf.p_lhs in let tj=constr_of_term prf.p_rhs in @@ -325,7 +331,7 @@ let refute_tac c t1 t2 p = Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl in let neweq= new_app_global _eq [|intype;tt1;tt2|] in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in @@ -335,14 +341,14 @@ let refute_tac c t1 t2 p = end let refine_exact_check c gl = - let evm, _ = pf_apply e_type_of gl c in + let evm, _ = pf_apply type_of gl c in Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl let convert_to_goal_tac c t1 t2 p = Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl in let neweq= new_app_global _eq [|sort;tt1;tt2|] in let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in @@ -367,7 +373,7 @@ let discriminate_tac (cstr,u as cstru) p = Proofview.Goal.nf_enter begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl in let concl = Proofview.Goal.concl gl in (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *) @@ -376,7 +382,7 @@ let discriminate_tac (cstr,u as cstru) p = (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) let identity = Universes.constr_of_global (Lazy.force _I) in - (* let trivial=pf_type_of gls identity in *) + (* let trivial=pf_unsafe_type_of gls identity in *) let trivial = Universes.constr_of_global (Lazy.force _True) in let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in let outtype = mkSort outtype in @@ -476,19 +482,28 @@ let congruence_tac depth l = This isn't particularly related with congruence, apart from the fact that congruence is called internally. *) - + +let mk_eq f c1 c2 k = + Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> + Proofview.Goal.enter begin + fun gl -> + let open Tacmach.New in + let evm, ty = pf_apply type_of gl c1 in + let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in + let term = mkApp (fc, [| ty; c1; c2 |]) in + let evm, _ = type_of (pf_env gl) evm term in + Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) + (k term) + end) + let f_equal = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let type_of = Tacmach.New.pf_type_of gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) - let ty = (* Termops.refresh_universes *) (type_of c1) in - if eq_constr_nounivs c1 c2 then Proofview.tclUNIT () - else - Tacticals.New.tclTRY (Tacticals.New.tclTHEN - ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut) - (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))) + Tacticals.New.tclTHEN + (mk_eq _eq c1 c2 Tactics.cut) + (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE |