summaryrefslogtreecommitdiff
path: root/rewrite.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'rewrite.ml4')
-rw-r--r--rewrite.ml495
1 files changed, 27 insertions, 68 deletions
diff --git a/rewrite.ml4 b/rewrite.ml4
index 383d706..b3e52e0 100644
--- a/rewrite.ml4
+++ b/rewrite.ml4
@@ -8,6 +8,7 @@
(** aac_rewrite -- rewriting modulo *)
+DECLARE PLUGIN "aac"
module Control = struct
let debug = false
@@ -26,16 +27,15 @@ let tac_or_exn tac exn msg = fun gl ->
pr_constr "last goal" (Tacmach.pf_concl gl);
exn msg e
+
+let retype = Coq.retype
+
(* helper to be used with the previous function: raise a new anomaly
except if a another one was previously raised *)
let push_anomaly msg = function
- | Util.Anomaly _ as e -> raise e
+ | e when Errors.is_anomaly e -> raise e
| _ -> Coq.anomaly msg
-
-
-
-
module M = Matcher
open Term
@@ -184,14 +184,14 @@ let by_aac_reflexivity zero
(* This convert is required to deal with evars in a proper
way *)
let convert_to = mkApp (r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in
- let convert = Tactics.convert_concl convert_to Term.VMcast in
- let apply_tac = Tactics.apply decision_thm in
+ let convert = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Term.VMcast) in
+ let apply_tac = Proofview.V82.of_tactic (Tactics.apply decision_thm) in
(Tacticals.tclTHENLIST
- [
+ [ retype decision_thm; retype convert_to;
convert ;
tac_or_exn apply_tac Coq.user_error "unification failure";
tac_or_exn (time_tac "vm_norm" (Tactics.normalise_in_concl)) Coq.anomaly "vm_compute failure";
- Tacticals.tclORELSE Tactics.reflexivity
+ Tacticals.tclORELSE (Proofview.V82.of_tactic Tactics.reflexivity)
(Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC"))
])
)
@@ -215,10 +215,10 @@ let by_aac_normalise zero lift ir t t' =
(* This convert is required to deal with evars in a proper
way *)
let convert_to = mkApp (rlt.Coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in
- let convert = Tactics.convert_concl convert_to Term.VMcast in
- let apply_tac = Tactics.apply normalise_thm in
+ let convert = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Term.VMcast) in
+ let apply_tac = Proofview.V82.of_tactic (Tactics.apply normalise_thm) in
(Tacticals.tclTHENLIST
- [
+ [ retype normalise_thm; retype convert_to;
convert ;
apply_tac;
])
@@ -260,6 +260,7 @@ let aac_normalise = fun goal ->
Tacticals.tclTHENLIST
[
aac_conclude by_aac_normalise;
+ Proofview.V82.of_tactic begin
Tacinterp.interp (
<:tactic<
intro x;
@@ -270,8 +271,8 @@ let aac_normalise = fun goal ->
unfold y;
compute [Internal.eval Internal.fold_map Internal.copy Prect]; simpl
>>
- );
- Tactics.keep ids
+ )end;
+ Proofview.V82.of_tactic (Tactics.keep ids)
] goal
let aac_reflexivity = fun goal ->
@@ -293,7 +294,8 @@ let aac_reflexivity = fun goal ->
|])
in
Tacticals.tclTHEN
- (Tactics.apply lift_reflexivity)
+
+ (Tacticals.tclTHEN (retype lift_reflexivity) (Proofview.V82.of_tactic (Tactics.apply lift_reflexivity)))
(fun goal ->
let concl = Tacmach.pf_concl goal in
let _ = pr_constr "concl "concl in
@@ -330,8 +332,8 @@ let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equ
|])
in
Tacticals.tclTHENLIST
- [
- Tactics.apply lift_transitivity
+ [ retype lift_transitivity;
+ Proofview.V82.of_tactic (Tactics.apply lift_transitivity)
] goal
@@ -439,41 +441,6 @@ let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict
) goal
-(** [aac_match eq (fun x1 ... xn => p) t H] match the term [t] against
- the pattern, and introduces an hypothesis H of type p = t. (Note
- that we have performed the substitution in p).
-*)
-
-let aac_match ~eq pattern term h = fun gl ->
- let env = Tacmach.pf_env gl in
- let evar_map = Tacmach.project gl in
- let carrier = Typing.type_of env evar_map term in
- let rel = Coq.Relation.make carrier eq in
- let equiv,gl = Coq.Equivalence.from_relation gl rel in
- (* first, we decompose the pattern as an arity. *)
- let x_args, pat = Term.decompose_lam pattern in
- (* then, we reify the pattern and the term, using the provided equality *)
- let envs = Theory.Trans.empty_envs () in
- let left, right,gl = Theory.Trans.t_of_constr gl rel envs (pat,term) in
- let gl,ir = Theory.Trans.ir_of_envs gl rel envs in
- let solutions = Matcher.matcher (Theory.Trans.ir_to_units ir) left right in
- (* then, we pick the first solution to the matching problem *)
- let sigma = match Search_monad.choose solutions with
- | None -> Coq.user_error "no solution to the matching problem"
- | Some sigma -> sigma
- in
- let p_sigma = Matcher.Subst.instantiate sigma left in
- let args = List.map (fun (x,t) -> x,Theory.Trans.raw_constr_of_t ir rel [] t) (Matcher.Subst.to_list sigma) in
- (* Then, we have to assert the fact that p_sigma is equal to term *)
- let equation = mkApp (eq, [| Theory.Trans.raw_constr_of_t ir rel [] p_sigma ; term |]) in
- let evar_map = Tacmach.project gl in
- Tacticals.tclTHENLIST
- [
- Refiner.tclEVARS evar_map;
- Tactics.assert_by h equation (by_aac_reflexivity term equiv ir p_sigma right);
- ] gl
-
-
open Coq.Rewrite
open Tacmach
open Tacticals
@@ -525,47 +492,39 @@ PRINTED BY pr_constro
END
TACTIC EXTEND _aac_reflexivity_
-| [ "aac_reflexivity" ] -> [ aac_reflexivity ]
+| [ "aac_reflexivity" ] -> [ Proofview.V82.tactic aac_reflexivity ]
END
TACTIC EXTEND _aac_normalise_
-| [ "aac_normalise" ] -> [ aac_normalise ]
+| [ "aac_normalise" ] -> [ Proofview.V82.tactic aac_normalise ]
END
TACTIC EXTEND _aac_rewrite_
| [ "aac_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
- [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl ]
+ [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl) ]
END
TACTIC EXTEND _aac_pattern_
| [ "aac_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
- [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl ]
+ [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl) ]
END
TACTIC EXTEND _aac_instances_
| [ "aac_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
- [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~show:true c gl ]
+ [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~show:true c gl) ]
END
TACTIC EXTEND _aacu_rewrite_
| [ "aacu_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
- [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl ]
+ [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl) ]
END
TACTIC EXTEND _aacu_pattern_
| [ "aacu_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
- [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl ]
+ [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl) ]
END
TACTIC EXTEND _aacu_instances_
| [ "aacu_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
- [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl ]
-END
-
-TACTIC EXTEND _aac_match_
-| [ "aac_match" constr(p) constr(t) ident(h)] ->
- [ fun gl ->
- let ty = Tacmach.pf_type_of gl t in
- let eq = Coq.Leibniz.eq ty in
- aac_match ~eq p t (Names.Name h) gl]
+ [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl) ]
END
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 08:20:39 +0000