Commit 211dc7ca authored by Robbert Krebbers's avatar Robbert Krebbers

Optimize wp_apply and improve its error reporting.

We now first iPoseProof the lemma and instantiate its premises before trying
to search for the sub-term where to apply. As a result, instantiation of the
premises of the applied lemmas happens only once, instead of it being done for
each sub-term as obtained by reshape_expr.
parent c5e7fc1a
...@@ -219,12 +219,16 @@ Qed. ...@@ -219,12 +219,16 @@ Qed.
End heap. End heap.
Tactic Notation "wp_apply" open_constr(lem) := Tactic Notation "wp_apply" open_constr(lem) :=
iStartProof; iPoseProofCore lem as false true (fun H =>
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q =>
wp_bind_core K; iApply lem; try iNext; simpl) reshape_expr e ltac:(fun K e' =>
| _ => fail "wp_apply: not a 'wp'" wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
end. lazymatch iTypeOf H with
| Some (_,?P) => fail "wp_apply: cannot apply" P
end
| _ => fail "wp_apply: not a 'wp'"
end).
Tactic Notation "wp_alloc" ident(l) "as" constr(H) := Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
iStartProof; iStartProof;
......
...@@ -564,19 +564,21 @@ Tactic Notation "iPoseProofCore" open_constr(lem) ...@@ -564,19 +564,21 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
end. end.
(** * Apply *) (** * Apply *)
Tactic Notation "iApply" open_constr(lem) := Tactic Notation "iApplyHyp" constr(H) :=
let rec go H := first let rec go H := first
[eapply tac_apply with _ H _ _ _; [eapply tac_apply with _ H _ _ _;
[env_reflexivity [env_reflexivity
|apply _ |apply _
|lazy beta (* reduce betas created by instantiation *)] |lazy beta (* reduce betas created by instantiation *)]
|iSpecializePat H "[]"; last go H] in |iSpecializePat H "[]"; last go H] in
iPoseProofCore lem as false true (fun H => first iExact H ||
[iExact H go H ||
|go H lazymatch iTypeOf H with
|lazymatch iTypeOf H with | Some (_,?Q) => fail "iApply: cannot apply" Q
| Some (_,?Q) => fail 1 "iApply: cannot apply" Q end.
end]).
Tactic Notation "iApply" open_constr(lem) :=
iPoseProofCore lem as false true (fun H => iApplyHyp H).
(** * Revert *) (** * Revert *)
Local Tactic Notation "iForallRevert" ident(x) := Local Tactic Notation "iForallRevert" ident(x) :=
......
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