Better error messages for wp tactics.

heap_lang/proofmode.v

@@ -88,6 +88,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     wp_bind K; iApply lem; try iNext)
+  | _ => fail "wp_apply: not a 'wp'"
   end.
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
@@ -103,9 +104,11 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
          |intros l; eexists; split;
            [env_cbv; reflexivity || fail 2 "wp_alloc:" H "not fresh"
            |wp_finish]]
-    end)
+    end) || fail "wp_alloc: cannot find 'Alloc' in" e
+  | _ => 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_alloc" ident(l) :=
+  let H := iFresh in wp_alloc l as H.
 
 Tactic Notation "wp_load" :=
   match goal with
@@ -118,7 +121,8 @@ Tactic Notation "wp_load" :=
          |apply _
          |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
          |wp_finish]
-    end)
+    end) || fail "wp_load: cannot find 'Load' in" e
+  | _ => fail "wp_load: not a 'wp'"
   end.
 
 Tactic Notation "wp_store" :=
@@ -134,14 +138,15 @@ Tactic Notation "wp_store" :=
          |iAssumptionCore || fail 2 "wp_store: cannot find" l "↦ ?"
          |env_cbv; reflexivity
          |wp_finish]
-    end)
+    end) || fail "wp_store: cannot find 'Store' in" e
+  | _ => fail "wp_store: not a 'wp'"
   end.
 
 Tactic Notation "wp_cas_fail" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
-    | CAS (Lit (LitLoc ?l)) ?e1 ?e2 =>
+    | 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"
@@ -151,14 +156,15 @@ Tactic Notation "wp_cas_fail" :=
          |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
          |try discriminate
          |wp_finish]
-    end)
+    end) || fail "wp_cas_fail: cannot find 'CAS' in" e
+  | _ => fail "wp_cas_fail: not a 'wp'"
   end.
 
 Tactic Notation "wp_cas_suc" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
-    | CAS (Lit (LitLoc ?l)) ?e1 ?e2 =>
+    | 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"
@@ -168,5 +174,6 @@ Tactic Notation "wp_cas_suc" :=
          |iAssumptionCore || fail 2 "wp_cas_suc: cannot find" l "↦ ?"
          |env_cbv; reflexivity
          |wp_finish]
-    end)
+    end) || fail "wp_cas_suc: cannot find 'CAS' in" e
+  | _ => fail "wp_cas_suc: not a 'wp'"
   end.

heap_lang/wp_tactics.v

@@ -28,7 +28,8 @@ Ltac wp_finish := intros_revert ltac:(
 Tactic Notation "wp_value" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind K; wp_value_head)
+    wp_bind K; wp_value_head) || fail "wp_value: cannot find value in" e
+  | _ => fail "wp_value: not a wp"
   end.
 
 Tactic Notation "wp_rec" :=
@@ -38,8 +39,9 @@ Tactic Notation "wp_rec" :=
 (* 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
-(*      end *) end)
-   end.
+(*      end *) end) || fail "wp_rec: cannot find 'Rec' in" e
+  | _ => fail "wp_rec: not a 'wp'"
+  end.
 
 Tactic Notation "wp_lam" :=
   match goal with
@@ -47,7 +49,8 @@ Tactic Notation "wp_lam" :=
     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
-(*    end *) end)
+(*    end *) end) || fail "wp_lam: cannot find 'Lam' in" e
+  | _ => fail "wp_lam: not a 'wp'"
   end.
 
 Tactic Notation "wp_let" := wp_lam.
@@ -64,7 +67,8 @@ Tactic Notation "wp_op" :=
        wp_bind K; etrans; [|eapply wp_bin_op; try fast_done]; wp_finish
     | UnOp _ _ =>
        wp_bind K; etrans; [|eapply wp_un_op; try fast_done]; wp_finish
-    end)
+    end) || fail "wp_op: cannot find 'BinOp' or 'UnOp' in" e
+  | _ => fail "wp_op: not a 'wp'"
   end.
 
 Tactic Notation "wp_proj" :=
@@ -73,30 +77,38 @@ Tactic Notation "wp_proj" :=
     match eval hnf in e' with
     | Fst _ => wp_bind K; etrans; [|eapply wp_fst; wp_done]; wp_finish
     | Snd _ => wp_bind K; etrans; [|eapply wp_snd; wp_done]; wp_finish
-    end)
+    end) || fail "wp_proj: cannot find 'Fst' or 'Snd' in" e
+  | _ => fail "wp_proj: not a 'wp'"
   end.
 
 Tactic Notation "wp_if" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with If _ _ _ =>
-    wp_bind K;
-    etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
-    end)
+    match eval hnf in e' with
+    | If _ _ _ =>
+      wp_bind K;
+      etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
+    end) || fail "wp_if: cannot find 'If' in" e
+  | _ => fail "wp_if: not a 'wp'"
   end.
 
 Tactic Notation "wp_case" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with Case _ _ _ =>
+    match eval hnf in e' with
+    | Case _ _ _ =>
       wp_bind K;
       etrans; [|first[eapply wp_case_inl; wp_done|eapply wp_case_inr; wp_done]];
       wp_finish
-    end)
+    end) || fail "wp_case: cannot find 'Case' in" e
+  | _ => fail "wp_case: not a 'wp'"
   end.
 
 Tactic Notation "wp_focus" open_constr(efoc) :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match e' with efoc => unify e' efoc; wp_bind K end)
+    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'"
   end.