Commit cb485174 authored by Robbert Krebbers's avatar Robbert Krebbers

Turn some matches into lazymatches so errors propagate properly.

parent 2da3bdf5
......@@ -86,14 +86,14 @@ Qed.
End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
match goal with
lazymatch 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) :=
match goal with
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Alloc ?e =>
......@@ -112,7 +112,7 @@ Tactic Notation "wp_alloc" ident(l) :=
let H := iFresh in wp_alloc l as H.
Tactic Notation "wp_load" :=
match goal with
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Load (Lit (LitLoc ?l)) =>
......@@ -127,7 +127,7 @@ Tactic Notation "wp_load" :=
end.
Tactic Notation "wp_store" :=
match goal with
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Store ?l ?e =>
......@@ -144,7 +144,7 @@ Tactic Notation "wp_store" :=
end.
Tactic Notation "wp_cas_fail" :=
match goal with
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| CAS ?l ?e1 ?e2 =>
......@@ -162,7 +162,7 @@ Tactic Notation "wp_cas_fail" :=
end.
Tactic Notation "wp_cas_suc" :=
match goal with
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| CAS ?l ?e1 ?e2 =>
......
......@@ -26,7 +26,7 @@ Ltac wp_finish := intros_revert ltac:(
rewrite -/of_val /= ?to_of_val; try strip_later; try wp_value_head).
Tactic Notation "wp_value" :=
match goal with
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
| _ => fail "wp_value: not a wp"
......@@ -44,7 +44,7 @@ Tactic Notation "wp_rec" :=
end.
Tactic Notation "wp_lam" :=
match goal with
lazymatch goal with
| |- _ 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 _ _ => *)
......@@ -57,7 +57,7 @@ Tactic Notation "wp_let" := wp_lam.
Tactic Notation "wp_seq" := wp_let.
Tactic Notation "wp_op" :=
match goal with
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
......@@ -72,7 +72,7 @@ Tactic Notation "wp_op" :=
end.
Tactic Notation "wp_proj" :=
match goal with
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Fst _ => wp_bind K; etrans; [|eapply wp_fst; wp_done]; wp_finish
......@@ -82,7 +82,7 @@ Tactic Notation "wp_proj" :=
end.
Tactic Notation "wp_if" :=
match goal with
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| If _ _ _ =>
......@@ -93,7 +93,7 @@ Tactic Notation "wp_if" :=
end.
Tactic Notation "wp_case" :=
match goal with
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Case _ _ _ =>
......@@ -105,7 +105,7 @@ Tactic Notation "wp_case" :=
end.
Tactic Notation "wp_focus" open_constr(efoc) :=
match goal with
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match e' with
| efoc => unify e' efoc; wp_bind K
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment