From 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Nov 2016 20:35:01 +0100 Subject: Equality API using EConstr. --- plugins/funind/functional_principles_proofs.ml | 10 +++++----- plugins/funind/indfun_common.ml | 1 + plugins/funind/invfun.ml | 10 +++++----- plugins/funind/recdef.ml | 12 ++++++------ 4 files changed, 17 insertions(+), 16 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 940f1669a..2e3992be9 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -401,7 +401,7 @@ let rewrite_until_var arg_num eq_ids : tactic = | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property"); | eq_id::eq_ids -> tclTHEN - (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id)))) + (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar eq_id)))) (do_rewrite eq_ids) g in @@ -1060,7 +1060,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a let just_introduced = nLastDecls nb_intro_to_do g' in let open Context.Named.Declaration in let just_introduced_id = List.map get_id just_introduced in - tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) + tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr equation_lemma))) (revert just_introduced_id) g' ) g @@ -1425,7 +1425,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = let backtrack_eqs_until_hrec hrec eqs : tactic = fun gls -> - let eqs = List.map mkVar eqs in + let eqs = List.map EConstr.mkVar eqs in let rewrite = tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs ) in @@ -1453,7 +1453,7 @@ let rec rewrite_eqs_in_eqs eqs = observe_tac (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id)) (tclTRY (Proofview.V82.of_tactic (Equality.general_rewrite_in true Locus.AllOccurrences - true (* dep proofs also: *) true id (mkVar eq) false))) + true (* dep proofs also: *) true id (EConstr.mkVar eq) false))) gl ) eqs @@ -1659,7 +1659,7 @@ let prove_principle_for_gen (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); - Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); + Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_ref))); (* observe_tac "finish" *) (fun gl' -> let body = let _,args = destApp (pf_concl gl') in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a45effb16..08b40a1f7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -502,6 +502,7 @@ let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (G | _ -> assert false;; let list_rewrite (rev:bool) (eqs: (constr*bool) list) = + let eqs = List.map (Util.on_fst EConstr.of_constr) eqs in tclREPEAT (List.fold_right (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 36fb6dad3..d29d4694f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -385,7 +385,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (* introducing the the result of the graph and the equality hypothesis *) observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]); (* replacing [res] with its value *) - observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); + observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar hres))); (* Conclusion *) observe_tac "exact" (fun g -> Proofview.V82.of_tactic (exact_check (EConstr.of_constr (app_constructor g))) g) @@ -520,7 +520,7 @@ and intros_with_rewrite_aux : tactic = let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); generalize_dependent_of (destVar args.(1)) id; - tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); + tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id))); intros_with_rewrite ] g @@ -529,7 +529,7 @@ and intros_with_rewrite_aux : tactic = let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); generalize_dependent_of (destVar args.(2)) id; - tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id))); + tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar id))); intros_with_rewrite ] g @@ -538,7 +538,7 @@ and intros_with_rewrite_aux : tactic = let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ[ Proofview.V82.of_tactic (Simple.intro id); - tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); + tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id))); intros_with_rewrite ] g end @@ -709,7 +709,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = in tclTHENSEQ[ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids; - Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma)); + Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_lemma))); (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) Proofview.V82.of_tactic (reduce diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 74affa396..5cee3cb20 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -871,10 +871,10 @@ let rec make_rewrite_list expr_info max = function in Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true - (mkVar hp, + (EConstr.mkVar hp, ExplicitBindings[Loc.ghost,NamedHyp def, - expr_info.f_constr;Loc.ghost,NamedHyp k, - (f_S max)]) false) g) ) + EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k, + EConstr.of_constr (f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *) @@ -898,10 +898,10 @@ let make_rewrite expr_info l hp max = observe_tac (str "general_rewrite_bindings") (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true - (mkVar hp, + (EConstr.mkVar hp, ExplicitBindings[Loc.ghost,NamedHyp def, - expr_info.f_constr;Loc.ghost,NamedHyp k, - (f_S (f_S max))]) false)) g) + EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k, + EConstr.of_constr (f_S (f_S max))]) false)) g) [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (str "make_rewrite")[ -- cgit v1.2.3