From 02f8a5fc7d445ee093bc80663646cfea0a915e6d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Apr 2017 17:36:35 +0200 Subject: Removing tactic compatibility layer in congruence. --- plugins/cc/cctac.ml | 128 ++++++++++++++++++++++++++++++--------------------- plugins/cc/cctac.mli | 2 +- 2 files changed, 76 insertions(+), 54 deletions(-) (limited to 'plugins/cc') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index b2c609dcb..00b31ccce 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -239,21 +239,43 @@ let build_projection intype (cstr:pconstructor) special default gls= (* generate an adhoc tactic following the proof tree *) -let _M =mkMeta - let app_global f args k = - Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) - -let new_app_global f args k = Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args)) -let new_refine c = Proofview.V82.tactic (refine c) -let refine c = refine c +let rec gen_holes env sigma t n accu = + let open Sigma in + if Int.equal n 0 then (sigma, List.rev accu) + else match EConstr.kind sigma t with + | Prod (_, u, t) -> + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma u in + let sigma = Sigma.to_evar_map sigma in + let t = EConstr.Vars.subst1 ev t in + gen_holes env sigma t (pred n) (ev :: accu) + | _ -> assert false + +let app_global_with_holes f args n = + Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + Refine.refine { Sigma.run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let t = Tacmach.New.pf_get_type_of gl fc in + let t = Termops.prod_applist sigma t (Array.to_list args) in + let ans = mkApp (fc, args) in + let (sigma, holes) = gen_holes env sigma t n [] in + let ans = applist (ans, holes) in + let evdref = ref sigma in + let () = Typing.e_check env evdref ans concl in + Sigma.Unsafe.of_pair (ans, !evdref) + end } + end } let assert_before n c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.s_enter { s_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) + Sigma.Unsafe.of_pair (assert_before n c, evm) end } let refresh_type env evm ty = @@ -281,18 +303,18 @@ let rec proof_tac p : unit Proofview.tactic = let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in refresh_universes (type_of l) (fun typ -> - new_app_global _sym_eq [|typ;r;l;c|] exact_check) + app_global _sym_eq [|typ;r;l;c|] exact_check) | Refl t -> let lr = constr_of_term t in refresh_universes (type_of lr) (fun typ -> - new_app_global _refl_equal [|typ;constr_of_term t|] exact_check) + app_global _refl_equal [|typ;constr_of_term t|] exact_check) | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and t3 = constr_of_term p2.p_rhs in refresh_universes (type_of t2) (fun typ -> - let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in - Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]) + let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in + Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)]) | Congr (p1,p2)-> let tf1=constr_of_term p1.p_lhs and tx1=constr_of_term p2.p_lhs @@ -303,18 +325,18 @@ let rec proof_tac p : unit Proofview.tactic = refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in - let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in - let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in + let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in + let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in let prf = - app_global _trans_eq + app_global_with_holes _trans_eq [|typfx; mkApp(tf1,[|tx1|]); mkApp(tf2,[|tx1|]); - mkApp(tf2,[|tx2|]);_M 2;_M 3|] in - Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine)) - [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1); + mkApp(tf2,[|tx2|])|] 2 in + Tacticals.New.tclTHENS prf + [Tacticals.New.tclTHEN lemma1 (proof_tac p1); Tacticals.New.tclFIRST - [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2); + [Tacticals.New.tclTHEN lemma2 (proof_tac p2); reflexivity; Tacticals.New.tclZEROMSG (Pp.str @@ -330,8 +352,8 @@ let rec proof_tac p : unit Proofview.tactic = build_projection intype cstr special default gl in let injt= - app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in - Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf))) + app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in + Tacticals.New.tclTHEN injt (proof_tac prf))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end } @@ -341,27 +363,29 @@ let refute_tac c t1 t2 p = let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let false_t=mkApp (c,[|mkVar hid|]) in let k intype = - let neweq= new_app_global _eq [|intype;tt1;tt2|] in + let neweq= app_global _eq [|intype;tt1;tt2|] in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k end } -let refine_exact_check c gl = - let evm, _ = pf_apply type_of gl c in - Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl +let refine_exact_check c = + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let evm, _ = Tacmach.New.pf_apply type_of gl c in + Sigma.Unsafe.of_pair (exact_check c, evm) + end } let convert_to_goal_tac c t1 t2 p = Proofview.Goal.enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let k sort = - let neweq= new_app_global _eq [|sort;tt1;tt2|] in + let neweq= app_global _eq [|sort;tt1;tt2|] in let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in let identity=mkLambda (Name x,sort,mkRel 1) in - let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in + let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) - [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] + [proof_tac p; endt refine_exact_check] in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k end } @@ -392,27 +416,25 @@ let discriminate_tac (cstr,u as cstru) p = let pred = mkLambda(Name xid,outtype,mkRel 1) in let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let proj = build_projection intype cstru trivial concl gl in - let injt=app_global _f_equal + let injt = app_global _f_equal [|intype;outtype;proj;t1;t2;mkVar hid|] in let endt k = injt (fun injt -> app_global _eq_rect [|outtype;trivial;pred;identity;concl;injt|] k) in - let neweq=new_app_global _eq [|intype;t1;t2|] in + let neweq = app_global _eq [|intype;t1;t2|] in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) - [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) + [proof_tac p; endt refine_exact_check]) end } (* wrap everything *) -let build_term_to_complete uf meta pac = +let build_term_to_complete uf pac = let cinfo = get_constructor_info uf pac.cnode in - let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in - let dummy_args = List.rev (List.init pac.arity meta) in - let all_args = List.rev_append real_args dummy_args in + let real_args = List.rev_map (fun i -> constr_of_term (term uf i)) pac.args in let (kn, u) = cinfo.ci_constr in - applist (mkConstructU (kn, EInstance.make u), all_args) + (applist (mkConstructU (kn, EInstance.make u), real_args), pac.arity) let cc_tactic depth additionnal_terms = Proofview.Goal.enter { enter = begin fun gl -> @@ -434,16 +456,17 @@ let cc_tactic depth additionnal_terms = let cstr=(get_constructor_info uf ipac.cnode).ci_constr in discriminate_tac cstr p | Incomplete -> + let open Glob_term in let env = Proofview.Goal.env gl in - let metacnt = ref 0 in - let newmeta _ = incr metacnt; _M !metacnt in - let terms_to_complete = - List.map - (build_term_to_complete uf newmeta) - (epsilons uf) in + let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in + let hole = GHole (Loc.ghost, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let pr_missing (c, missing) = + let c = Detyping.detype ~lax:true false [] env sigma c in + let holes = List.init missing (fun _ -> hole) in + Printer.pr_glob_constr_env env (GApp (Loc.ghost, c, holes)) + in Feedback.msg_info - (Pp.str "Goal is solvable by congruence but \ - some arguments are missing."); + (Pp.str "Goal is solvable by congruence but some arguments are missing."); Feedback.msg_info (Pp.str " Try " ++ hov 8 @@ -451,7 +474,7 @@ let cc_tactic depth additionnal_terms = str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(") - (Termops.print_constr_env env sigma) + pr_missing terms_to_complete ++ str ")\"," end ++ @@ -472,13 +495,13 @@ let cc_tactic depth additionnal_terms = convert_to_hyp_tac ida ta idb tb p end } -let cc_fail gls = - user_err ~hdr:"Congruence" (Pp.str "congruence failed.") +let cc_fail = + Tacticals.New.tclZEROMSG (Pp.str "congruence failed.") let congruence_tac depth l = Tacticals.New.tclORELSE (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l)) - (Proofview.V82.tactic cc_fail) + cc_fail (* Beware: reflexivity = constructor 1 = apply refl_equal might be slow now, let's rather do something equivalent @@ -493,14 +516,13 @@ let congruence_tac depth l = let mk_eq f c1 c2 k = Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.s_enter { s_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) + Sigma.Unsafe.of_pair (k term, evm) end } let f_equal = @@ -511,7 +533,7 @@ let f_equal = try (* type_of can raise an exception *) Tacticals.New.tclTHENS (mk_eq _eq c1 c2 Tactics.cut) - [Proofview.tclUNIT ();Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)] + [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)] with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index de6eb982e..5099d847b 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -14,7 +14,7 @@ val proof_tac: Ccproof.proof -> unit Proofview.tactic val cc_tactic : int -> constr list -> unit Proofview.tactic -val cc_fail : tactic +val cc_fail : unit Proofview.tactic val congruence_tac : int -> constr list -> unit Proofview.tactic -- cgit v1.2.3