Commit 1d8edc89 authored by Joseph Tassarotti's avatar Joseph Tassarotti

Fix error message regression, add new test cases.

Also fixes pre-existing bug in iCombine error messages.
parent 2c01bead
...@@ -456,16 +456,47 @@ The command has indeed failed with message: ...@@ -456,16 +456,47 @@ The command has indeed failed with message:
In nested Ltac calls to "iIntros ( (intropattern) )", In nested Ltac calls to "iIntros ( (intropattern) )",
"iIntro ( (intropattern) )" and "intros x", last call failed. "iIntro ( (intropattern) )" and "intros x", last call failed.
x is already used. x is already used.
"iSplit_one_of_many" "iSplitL_one_of_many"
: string : string
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iSplitL (constr)" and "iMissingHyps", last call Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
"iSplitR_one_of_many"
: string
The command has indeed failed with message:
Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
"iCombine_fail"
: string
The command has indeed failed with message:
Ltac call to "iCombine (constr) as (constr)" failed.
Tactic failure: iCombine: hypotheses ["HP3"] not found.
"iSpecialize_bad_name1_fail"
: string
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed. failed.
No matching clauses for match. Tactic failure: iSpecialize: "H" not found.
"iSpecialize_bad_name2_fail"
: string
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iSplitL (constr)" and "iMissingHyps", last call In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed. failed.
No matching clauses for match. Tactic failure: iSpecialize: "H" not found.
"iExact_fail" "iExact_fail"
: string : string
The command has indeed failed with message: The command has indeed failed with message:
......
...@@ -777,13 +777,41 @@ Proof. ...@@ -777,13 +777,41 @@ Proof.
iIntros "HQ" (x). Fail iIntros (x). iIntros "HQ" (x). Fail iIntros (x).
Abort. Abort.
Check "iSplit_one_of_many". Check "iSplitL_one_of_many".
Lemma iSplit_one_of_many P : Lemma iSplitL_one_of_many P :
P - P - P P. P - P - P P.
Proof. Proof.
iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1". iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
Abort. Abort.
Check "iSplitR_one_of_many".
Lemma iSplitR_one_of_many P :
P - P - P P.
Proof.
iIntros "HP1 HP2". Fail iSplitR "HP1 HPx". Fail iSplitR "HPx HP1".
Abort.
Check "iCombine_fail".
Lemma iCombine_fail P:
P - P - P P.
Proof.
iIntros "HP1 HP2". Fail iCombine "HP1 HP3" as "HP".
Abort.
Check "iSpecialize_bad_name1_fail".
Lemma iSpecialize_bad_name1_fail P Q:
(P - Q) - P - Q.
Proof.
iIntros "HW HP". Fail iSpecialize ("H" with "HP").
Abort.
Check "iSpecialize_bad_name2_fail".
Lemma iSpecialize_bad_name2_fail P Q:
(P - Q) - P - Q.
Proof.
iIntros "HW HP". Fail iSpecialize ("HW" with "H").
Abort.
Check "iExact_fail". Check "iExact_fail".
Lemma iExact_fail P Q : Lemma iExact_fail P Q :
<affine> P - Q - <affine> P. <affine> P - Q - <affine> P.
......
...@@ -39,15 +39,20 @@ Ltac pretty_ident H := ...@@ -39,15 +39,20 @@ Ltac pretty_ident H :=
(** * Misc *) (** * Misc *)
Ltac iMissingHyps Hs := Ltac iGetCtx :=
let Δ := lazymatch goal with
lazymatch goal with | |- envs_entails ?Δ _ => Δ
| |- envs_entails ?Δ _ => Δ | |- context[ envs_split _ _ ?Δ ] => Δ
| |- context[ envs_split _ _ ?Δ ] => Δ end.
end in
Ltac iMissingHypsCore Δ Hs :=
let Hhyps := pm_eval (envs_dom Δ) in let Hhyps := pm_eval (envs_dom Δ) in
eval vm_compute in (list_difference Hs Hhyps). eval vm_compute in (list_difference Hs Hhyps).
Ltac iMissingHyps Hs :=
let Δ := iGetCtx in
iMissingHypsCore Δ Hs.
Ltac iTypeOf H := Ltac iTypeOf H :=
let Δ := match goal with |- envs_entails ?Δ _ => Δ end in let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
pm_eval (envs_lookup H Δ). pm_eval (envs_lookup H Δ).
...@@ -1125,13 +1130,14 @@ Tactic Notation "iSplitL" constr(Hs) := ...@@ -1125,13 +1130,14 @@ Tactic Notation "iSplitL" constr(Hs) :=
iStartProof; iStartProof;
let Hs := words Hs in let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in let Hs := eval vm_compute in (INamed <$> Hs) in
let Δ := iGetCtx in
eapply tac_sep_split with Left Hs _ _; (* (js:=Hs) *) eapply tac_sep_split with Left Hs _ _; (* (js:=Hs) *)
[iSolveTC || [iSolveTC ||
let P := match goal with |- FromSep _ ?P _ _ => P end in let P := match goal with |- FromSep _ ?P _ _ => P end in
fail "iSplitL:" P "not a separating conjunction" fail "iSplitL:" P "not a separating conjunction"
|pm_reduce; |pm_reduce;
lazymatch goal with lazymatch goal with
|- False => let Hs := iMissingHyps Hs in |- False => let Hs := iMissingHypsCore Δ Hs in
fail "iSplitL: hypotheses" Hs "not found" fail "iSplitL: hypotheses" Hs "not found"
| _ => split; [(* subgoal 1 *)|(* subgoal 2 *)] | _ => split; [(* subgoal 1 *)|(* subgoal 2 *)]
end]. end].
...@@ -1140,14 +1146,15 @@ Tactic Notation "iSplitR" constr(Hs) := ...@@ -1140,14 +1146,15 @@ Tactic Notation "iSplitR" constr(Hs) :=
iStartProof; iStartProof;
let Hs := words Hs in let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in let Hs := eval vm_compute in (INamed <$> Hs) in
let Δ := iGetCtx in
eapply tac_sep_split with Right Hs _ _; (* (js:=Hs) *) eapply tac_sep_split with Right Hs _ _; (* (js:=Hs) *)
[iSolveTC || [iSolveTC ||
let P := match goal with |- FromSep _ ?P _ _ => P end in let P := match goal with |- FromSep _ ?P _ _ => P end in
fail "iSplitR:" P "not a separating conjunction" fail "iSplitR:" P "not a separating conjunction"
|pm_reduce; |pm_reduce;
lazymatch goal with lazymatch goal with
|- False => let Hs := iMissingHyps Hs in |- False => let Hs := iMissingHypsCore Δ Hs in
fail "iSplitL: hypotheses" Hs "not found" fail "iSplitR: hypotheses" Hs "not found"
| _ => split; [(* subgoal 1 *)|(* subgoal 2 *)] | _ => split; [(* subgoal 1 *)|(* subgoal 2 *)]
end]. end].
...@@ -1358,9 +1365,10 @@ Tactic Notation "iCombine" constr(Hs) "as" constr(pat) := ...@@ -1358,9 +1365,10 @@ Tactic Notation "iCombine" constr(Hs) "as" constr(pat) :=
let Hs := words Hs in let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in let Hs := eval vm_compute in (INamed <$> Hs) in
let H := iFresh in let H := iFresh in
let Δ := iGetCtx in
eapply tac_combine with _ _ Hs _ _ H _; eapply tac_combine with _ _ Hs _ _ H _;
[pm_reflexivity || [pm_reflexivity ||
let Hs := iMissingHyps Hs in let Hs := iMissingHypsCore Δ Hs in
fail "iCombine: hypotheses" Hs "not found" fail "iCombine: hypotheses" Hs "not found"
|iSolveTC |iSolveTC
|pm_reflexivity || |pm_reflexivity ||
......
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