Commit 3147b08a authored by Robbert Krebbers's avatar Robbert Krebbers

Explicitly thunk tactic argument of `iPoseProofCoreLem`.

This avoids weird Ltac behaviors like those in !272.

Also, change `before_tc` keyword into `as` to be consistent with other tactics.
parent 2471db29
Pipeline #17677 passed with stage
in 19 minutes and 19 seconds
......@@ -554,17 +554,16 @@ Tactic failure: iStartProof: not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)" and
"iPoseProofCoreLem (constr) as (tactic3)" and
"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
Tactic failure: iPoseProof: not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)",
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iRename (constr) into (constr)", last call failed.
......@@ -581,11 +580,10 @@ Tactic failure: iPoseProof: "Hx" not found.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)",
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
"spec_tac" (bound to
fun _ =>
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "spec_tac" (bound to
fun Htmp =>
lazymatch lem with
| {| itrm := _; itrm_vars := ?xs; itrm_hyps := ?pat |} => iSpecializeCore
{| itrm := Htmp; itrm_vars := xs; itrm_hyps := pat |} as p
......
......@@ -725,8 +725,8 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
| _ => idtac
end.
Tactic Notation "iPoseProofCoreLem"
constr(lem) "as" constr(Hnew) "before_tc" tactic3(tac) :=
Tactic Notation "iPoseProofCoreLem" constr(lem) "as" tactic3(tac) :=
let Hnew := iFresh in
eapply tac_pose_proof with Hnew _; (* (j:=H) *)
[iIntoEmpValid lem
|pm_reduce;
......@@ -734,7 +734,7 @@ Tactic Notation "iPoseProofCoreLem"
| |- False =>
let Hnew := pretty_ident Hnew in
fail "iPoseProof:" Hnew "not fresh"
| _ => tac
| _ => tac Hnew
end];
(* Solve all remaining TC premises generated by [iIntoEmpValid] *)
try iSolveTC.
......@@ -1002,17 +1002,18 @@ whether the conclusion of the specialized term [lem] is persistent. *)
Tactic Notation "iPoseProofCore" open_constr(lem)
"as" constr(p) tactic3(tac) :=
iStartProof;
let Htmp := iFresh in
let t := lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
let t := lazymatch type of t with string => constr:(INamed t) | _ => t end in
let spec_tac _ :=
let spec_tac Htmp :=
lazymatch lem with
| ITrm _ ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
| _ => idtac
end in
lazymatch type of t with
| ident => iPoseProofCoreHyp t as Htmp; spec_tac (); [..|tac Htmp]
| _ => iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
| ident =>
let Htmp := iFresh in
iPoseProofCoreHyp t as Htmp; spec_tac Htmp; [..|tac Htmp]
| _ => iPoseProofCoreLem t as (fun Htmp => spec_tac Htmp; [..|tac Htmp])
end.
(** * The apply tactic *)
......
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