From 6d43651e90b83d670eecc4da0e6b0da5c8b15de5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 May 2016 19:41:41 +0200
Subject: [PATCH] Better errors messages for wp heap tactics.
---
heap_lang/proofmode.v | 139 ++++++++++++++++++++++++------------------
1 file changed, 78 insertions(+), 61 deletions(-)
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 584384035..b57a9ea5c 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -94,88 +94,105 @@ Tactic Notation "wp_apply" open_constr(lem) :=
Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with
- | Alloc ?e =>
- wp_bind K; eapply tac_wp_alloc with _ _ H _;
- [wp_done || fail 2 "wp_alloc:" e "not a value"
- |iAssumption || fail 2 "wp_alloc: cannot find heap_ctx"
- |done || eauto with ndisj
- |apply _
- |intros l; eexists; split;
- [env_cbv; reflexivity || fail 2 "wp_alloc:" H "not fresh"
- |wp_finish]]
- end) || fail "wp_alloc: cannot find 'Alloc' in" e
+ | |- _ ⊢ wp ?E ?e ?Q =>
+ first
+ [reshape_expr e ltac:(fun K e' =>
+ match eval hnf in e' with Alloc _ => wp_bind K end)
+ |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+ eapply tac_wp_alloc with _ _ H _;
+ [let e' := match goal with |- to_val ?e' = _ => e' end in
+ wp_done || fail "wp_alloc:" e' "not a value"
+ |iAssumption || fail "wp_alloc: cannot find heap_ctx"
+ |done || eauto with ndisj
+ |apply _
+ |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
+ eexists; split;
+ [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
+ |wp_finish]]
| _ => fail "wp_alloc: not a 'wp'"
end.
+
Tactic Notation "wp_alloc" ident(l) :=
let H := iFresh in wp_alloc l as H.
Tactic Notation "wp_load" :=
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with
- | Load ?l =>
- wp_bind K; eapply tac_wp_load;
- [iAssumption || fail 2 "wp_load: cannot find heap_ctx"
- |done || eauto with ndisj
- |apply _
- |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
- |wp_finish]
- end) || fail "wp_load: cannot find 'Load' in" e
+ | |- _ ⊢ wp ?E ?e ?Q =>
+ first
+ [reshape_expr e ltac:(fun K e' =>
+ match eval hnf in e' with Load _ => wp_bind K end)
+ |fail 1 "wp_load: cannot find 'Load' in" e];
+ eapply tac_wp_load;
+ [iAssumption || fail "wp_load: cannot find heap_ctx"
+ |done || eauto with ndisj
+ |apply _
+ |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
+ |wp_finish]
| _ => fail "wp_load: not a 'wp'"
end.
Tactic Notation "wp_store" :=
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with
- | Store ?l ?e =>
- wp_bind K; eapply tac_wp_store;
- [wp_done || fail 2 "wp_store:" e "not a value"
- |iAssumption || fail 2 "wp_store: cannot find heap_ctx"
- |done || eauto with ndisj
- |apply _
- |iAssumptionCore || fail 2 "wp_store: cannot find" l "↦ ?"
- |env_cbv; reflexivity
- |wp_finish]
- end) || fail "wp_store: cannot find 'Store' in" e
+ | |- _ ⊢ wp ?E ?e ?Q =>
+ first
+ [reshape_expr e ltac:(fun K e' =>
+ match eval hnf in e' with Store _ _ => wp_bind K end)
+ |fail 1 "wp_store: cannot find 'Store' in" e];
+ eapply tac_wp_store;
+ [let e' := match goal with |- to_val ?e' = _ => e' end in
+ wp_done || fail "wp_store:" e' "not a value"
+ |iAssumption || fail "wp_store: cannot find heap_ctx"
+ |done || eauto with ndisj
+ |apply _
+ |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
+ |env_cbv; reflexivity
+ |wp_finish]
| _ => fail "wp_store: not a 'wp'"
end.
Tactic Notation "wp_cas_fail" :=
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with
- | CAS ?l ?e1 ?e2 =>
- wp_bind K; eapply tac_wp_cas_fail;
- [wp_done || fail 2 "wp_cas_fail:" e1 "not a value"
- |wp_done || fail 2 "wp_cas_fail:" e2 "not a value"
- |iAssumption || fail 2 "wp_cas_fail: cannot find heap_ctx"
- |done || eauto with ndisj
- |apply _
- |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
- |try congruence
- |wp_finish]
- end) || fail "wp_cas_fail: cannot find 'CAS' in" e
+ | |- _ ⊢ wp ?E ?e ?Q =>
+ first
+ [reshape_expr e ltac:(fun K e' =>
+ match eval hnf in e' with CAS _ _ _ => wp_bind K end)
+ |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
+ eapply tac_wp_cas_fail;
+ [let e' := match goal with |- to_val ?e' = _ => e' end in
+ wp_done || fail "wp_cas_fail:" e' "not a value"
+ |let e' := match goal with |- to_val ?e' = _ => e' end in
+ wp_done || fail "wp_cas_fail:" e' "not a value"
+ |iAssumption || fail "wp_cas_fail: cannot find heap_ctx"
+ |done || eauto with ndisj
+ |apply _
+ |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
+ |try congruence
+ |wp_finish]
| _ => fail "wp_cas_fail: not a 'wp'"
end.
Tactic Notation "wp_cas_suc" :=
lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- match eval hnf in e' with
- | CAS ?l ?e1 ?e2 =>
- wp_bind K; eapply tac_wp_cas_suc;
- [wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
- |wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
- |iAssumption || fail 2 "wp_cas_suc: cannot find heap_ctx"
- |done || eauto with ndisj
- |apply _
- |iAssumptionCore || fail 2 "wp_cas_suc: cannot find" l "↦ ?"
- |try congruence
- |env_cbv; reflexivity
- |wp_finish]
- end) || fail "wp_cas_suc: cannot find 'CAS' in" e
+ | |- _ ⊢ wp ?E ?e ?Q =>
+ first
+ [reshape_expr e ltac:(fun K e' =>
+ match eval hnf in e' with CAS _ _ _ => wp_bind K end)
+ |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
+ eapply tac_wp_cas_suc;
+ [let e' := match goal with |- to_val ?e' = _ => e' end in
+ wp_done || fail "wp_cas_suc:" e' "not a value"
+ |let e' := match goal with |- to_val ?e' = _ => e' end in
+ wp_done || fail "wp_cas_suc:" e' "not a value"
+ |iAssumption || fail "wp_cas_suc: cannot find heap_ctx"
+ |done || eauto with ndisj
+ |apply _
+ |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+ iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
+ |try congruence
+ |env_cbv; reflexivity
+ |wp_finish]
| _ => fail "wp_cas_suc: not a 'wp'"
end.
--
GitLab