From 970bbeabd7efbc9417773d18b0308bdaaf03cc07 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 25 Oct 2016 22:04:11 +0200
Subject: [PATCH] Rename wp_bind.
---
proofmode.v | 8 ++++----
wp_tactics.v | 24 ++++++++++++------------
2 files changed, 16 insertions(+), 16 deletions(-)
diff --git a/proofmode.v b/proofmode.v
index 3c93028b..579dcd8f 100644
--- a/proofmode.v
+++ b/proofmode.v
@@ -76,7 +76,7 @@ End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- wp_bind K; iApply lem; try iNext)
+ wp_bind_core K; iApply lem; try iNext)
| _ => fail "wp_apply: not a 'wp'"
end.
@@ -85,7 +85,7 @@ Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
| |- _ ⊢ wp ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with Alloc _ => wp_bind K end)
+ match eval hnf in e' with Alloc _ => wp_bind_core K end)
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
eapply tac_wp_alloc with _ _ H Hf;
[iAssumption || fail "wp_alloc: cannot find heap_ctx"
@@ -107,7 +107,7 @@ Tactic Notation "wp_read" :=
| |- _ ⊢ wp ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with Read _ _ => wp_bind K end)
+ match eval hnf in e' with Read _ _ => wp_bind_core K end)
|fail 1 "wp_read: cannot find 'Read' in" e];
eapply tac_wp_read;
[iAssumption || fail "wp_read: cannot find heap_ctx"
@@ -126,7 +126,7 @@ Tactic Notation "wp_write" :=
| |- _ ⊢ wp ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with Write _ _ _ => wp_bind K end)
+ match eval hnf in e' with Write _ _ _ => wp_bind_core K end)
|fail 1 "wp_write: cannot find 'Write' in" e];
eapply tac_wp_write;
[let e' := match goal with |- to_val ?e' = _ => e' end in
diff --git a/wp_tactics.v b/wp_tactics.v
index c7bc61af..df840ba7 100644
--- a/wp_tactics.v
+++ b/wp_tactics.v
@@ -3,7 +3,7 @@ From lrust Require Export tactics derived.
Import uPred.
(** wp-specific helper tactics *)
-Ltac wp_bind K :=
+Ltac wp_bind_core K :=
lazymatch eval hnf in K with
| [] => idtac
| _ => etrans; [|fast_by apply (wp_bind K)]; simpl
@@ -53,7 +53,7 @@ Ltac wp_finish := intros_revert ltac:(
Tactic Notation "wp_value" :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- wp_bind K; wp_value_head) || fail "wp_value: cannot find value in" e
+ wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
| _ => fail "wp_value: not a wp"
end.
@@ -63,7 +63,7 @@ Tactic Notation "wp_rec" :=
match eval hnf in e' with App ?e1 _ =>
(* hnf does not reduce through an of_val *)
(* match eval hnf in e1 with Rec _ _ _ => *)
- wp_bind K; etrans; [|eapply wp_rec; wp_done]; simpl_subst; wp_finish
+ wp_bind_core K; etrans; [|eapply wp_rec; wp_done]; simpl_subst; wp_finish
(* end *) end) || fail "wp_rec: cannot find 'Rec' in" e
| _ => fail "wp_rec: not a 'wp'"
end.
@@ -73,7 +73,7 @@ Tactic Notation "wp_lam" :=
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* match eval hnf in e1 with Rec BAnon _ _ => *)
- wp_bind K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
+ wp_bind_core K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
(* end *) end) || fail "wp_lam: cannot find 'Lam' in" e
| _ => fail "wp_lam: not a 'wp'"
end.
@@ -85,9 +85,9 @@ Tactic Notation "wp_op" :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
- | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
+ | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
| BinOp _ _ _ =>
- wp_bind K; etrans; [|eapply wp_bin_op; try fast_done]; wp_finish
+ wp_bind_core K; etrans; [|eapply wp_bin_op; try fast_done]; wp_finish
end) || fail "wp_op: cannot find 'BinOp' in" e
| _ => fail "wp_op: not a 'wp'"
end.
@@ -97,7 +97,7 @@ Tactic Notation "wp_if" :=
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| If _ _ _ =>
- wp_bind K;
+ wp_bind_core K;
etrans; [|eapply wp_if]; wp_finish
end) || fail "wp_if: cannot find 'If' in" e
| _ => fail "wp_if: not a 'wp'"
@@ -108,18 +108,18 @@ Tactic Notation "wp_case" :=
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Case _ _ _ =>
- wp_bind K;
+ wp_bind_core K;
etrans; [|eapply wp_case; wp_done];
simpl_subst; wp_finish
end) || fail "wp_case: cannot find 'Case' in" e
| _ => fail "wp_case: not a 'wp'"
end.
-Tactic Notation "wp_focus" open_constr(efoc) :=
+Tactic Notation "wp_bind" open_constr(efoc) :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match e' with
- | efoc => unify e' efoc; wp_bind K
- end) || fail "wp_focus: cannot find" efoc "in" e
- | _ => fail "wp_focus: not a 'wp'"
+ | efoc => unify e' efoc; wp_bind_core K
+ end) || fail "wp_bind: cannot find" efoc "in" e
+ | _ => fail "wp_bind: not a 'wp'"
end.
--
GitLab