From 09611c068c930656bdf0759c22296f53f39536da Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Fri, 11 Feb 2022 12:27:26 +0100
Subject: [PATCH] Replaced 'try cont' with 'cont', should avoid TC search on
sideconditions when hints are not found.
---
theories/biabd/search.v | 45 ++++++++++++++++++++-----------------
theories/biabd/search_abd.v | 25 +++++++++++----------
2 files changed, 38 insertions(+), 32 deletions(-)
diff --git a/theories/biabd/search.v b/theories/biabd/search.v
index 48ebe972..575414fc 100644
--- a/theories/biabd/search.v
+++ b/theories/biabd/search.v
@@ -444,46 +444,46 @@ Ltac biabd_step_sep P :=
Ltac biabd_step_hyp_exist cont :=
notypeclasses refine (biabdhyp_exist' _ _ _ _ _ _ _ _ _ _ _ _ _ _); [iSolveTC |
- intros?; do 3 eexists; split; [ try cont | simple notypeclasses refine (ex_intro _ _ _); last cbn beta ] | ].
+ intros?; do 3 eexists; split; [ cont | simple notypeclasses refine (ex_intro _ _ _); last cbn beta ] | ].
Ltac biabd_step_hyp_mod cont :=
- notypeclasses refine (biabdhyp_mod_intro_l _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); [iSolveTC | iSolveTC | try cont | ].
+ notypeclasses refine (biabdhyp_mod_intro_l _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); [iSolveTC | iSolveTC | cont | ].
Ltac biabd_step_wand :=
notypeclasses refine (biabdhyp_wand _ _ _ _ _ _ _ _ _ _ _ _); [iSolveTC| ].
Ltac biabd_step_forall cont :=
notypeclasses refine (biabdhyp_forall_postpone _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); [ iSolveTC |
- intros ?; do 4 eexists; split; [ try cont | split; [ | simple notypeclasses refine (ex_intro _ _ _); last cbn beta ] ] | ].
+ intros ?; do 4 eexists; split; [ cont | split; [ | simple notypeclasses refine (ex_intro _ _ _); last cbn beta ] ] | ].
Ltac biabd_step_from_goal p P :=
assert_fails (assert (AtomAndConnective p P) as _ by (iSolveTC));
simple eapply biabdhyp_from_unfold_goal.
Ltac biabd_step_hyp_naive p P cont :=
- (biabd_step_atom_shortcut; try cont) + (
- (biabd_step_later_mono; try cont) ||
- (biabd_step_sep P; try cont) ||
+ (biabd_step_atom_shortcut; cont) + (
+ tryif biabd_step_later_mono then cont else (* ensures ⊳ (P ∗ Q) is not also tried as ⊳P ∗ ⊳ Q *)
+ tryif biabd_step_sep P then cont else
(biabd_step_hyp_exist cont) ||
(biabd_step_hyp_mod cont) ||
- (biabd_step_wand; try cont) ||
+ (biabd_step_wand; cont) ||
(biabd_step_forall cont) ||
- (biabd_step_from_goal p P; try cont)
+ (biabd_step_from_goal p P; cont)
).
Ltac connective_as_atom_shortcut := fail.
(* this keeps open the option of seeing all wands also as atoms *)
Ltac biabd_step_hyp p P cont :=
- (connective_as_atom_shortcut; try cont) +
+ (connective_as_atom_shortcut; cont) +
lazymatch P with
- | bi_later _ => biabd_step_later_mono; try cont
- | bi_laterN _ _ => biabd_step_later_mono; try cont
- | bi_sep _ _ => biabd_step_sep P; try cont
+ | bi_later _ => biabd_step_later_mono; cont
+ | bi_laterN _ _ => biabd_step_later_mono; cont
+ | bi_sep _ _ => biabd_step_sep P; cont
| bi_exist _ => biabd_step_hyp_exist cont
| fupd _ _ _ => biabd_step_hyp_mod cont
| bupd _ => biabd_step_hyp_mod cont
- | bi_wand _ _ => biabd_step_wand; try cont
+ | bi_wand _ _ => biabd_step_wand; cont
| bi_forall _ => biabd_step_forall cont
| _ => biabd_step_hyp_naive p P cont
end.
@@ -494,7 +494,7 @@ Ltac biabd_step_goal_mod :=
Ltac biabd_step_goal_exist cont :=
notypeclasses refine (biabdgoal_witness_both_v3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);
[ intros; do 4 (notypeclasses refine (ex_intro _ _ _)); split;
- [ try cont
+ [ cont
| simple notypeclasses refine (ex_intro _ _ _);
[
| simpl; simple notypeclasses refine (ex_intro _ _ _); last simpl ] ]
@@ -503,19 +503,24 @@ Ltac biabd_step_goal_exist cont :=
Ltac diaframe_hint_search := iSolveTC.
Ltac biabd_step_goal cont :=
- (solve [eapply unfoldgoal_from_base; [diaframe_hint_search | iSolveTC]]) ||
- (biabd_step_goal_mod; try cont) ||
- (biabd_step_goal_exist cont).
+ (solve [eapply unfoldgoal_from_base; [diaframe_hint_search | iSolveTC]]) || (
+ tryif biabd_step_goal_mod then cont else
+ biabd_step_goal_exist cont
+ ).
Ltac pre_step := idtac.
Ltac find_biabd_steps :=
- let cont := ltac:(pre_step; find_biabd_steps) in
+ let cont := ltac:(pre_step; find_biabd_steps) in
+ (* if you want to inspect the goal after applying all recursive rules, use
+ cont := ltac:(pre_step; try find_biabd_steps) *)
lazymatch goal with
| |- BiAbdUnfoldHypMod ?p ?P _ _ _ _ _ _ => biabd_step_hyp p P cont
| |- BiAbdUnfoldGoalMod _ _ _ _ _ _ _ _ => biabd_step_goal cont
end.
- (* this CPS version ensures we don't start (possibly costly) TC search until we are sure all recursive rules have been applied.
- TODO: maybe this can be improved even further, by not doing 'try cont' *)
+ (* this CPS version ensures we don't start (possibly costly) TC search until we are sure all recursive rules have been applied.
+ Note that find_biabd_steps intentionally FAILS if it cannot find a hint.
+ this means it fails before initiating TC search, as desired. If it does succeed, it only leaves sideconditions for TC search
+ *)
Ltac find_biabd_initial_step :=
notypeclasses refine (biabd_from_unfold_hyp _ _ _ _ _ _ _ _ _).
diff --git a/theories/biabd/search_abd.v b/theories/biabd/search_abd.v
index 2414f42b..93dbdc1f 100644
--- a/theories/biabd/search_abd.v
+++ b/theories/biabd/search_abd.v
@@ -274,32 +274,32 @@ Ltac abd_step_sep P :=
Ltac abd_step_hyp_exist cont :=
simple eapply abdhyp_exist; [iSolveTC |
- cbn [tforall tele_fold tele_bind tele_app tele_appd_dep]; intros; try cont | idtac..].
+ cbn [tforall tele_fold tele_bind tele_app tele_appd_dep]; intros; cont | idtac..].
(* TODO: this might be broken like it was for BiAbd, in the case of nested exists *)
Ltac abd_step_hyp_mod cont :=
- notypeclasses refine (abdhyp_mod_intro_l _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); [iSolveTC | iSolveTC | try cont | ].
+ notypeclasses refine (abdhyp_mod_intro_l _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); [iSolveTC | iSolveTC | cont | ].
Ltac abd_step_wand cont :=
- notypeclasses refine (abdhyp_wand _ _ _ _ _ _ _ _ _ _ _ _ _); [iSolveTC| try cont | ].
+ notypeclasses refine (abdhyp_wand _ _ _ _ _ _ _ _ _ _ _ _ _); [iSolveTC| cont | ].
Ltac abd_step_forall cont :=
notypeclasses refine (abdhyp_forall_both _ _ _ _ _ _ _ _ _ _ _ _ _); [ iSolveTC |
- intros ?; do 2 eexists; split; [try cont | ] | ].
+ intros ?; do 2 eexists; split; [cont | ] | ].
Ltac abd_step_from_goal p P :=
assert_fails (assert (AtomAndConnective p P) as _ by (iSolveTC));
simple eapply abdhyp_from_unfold_goal.
Ltac abd_step_hyp p P cont :=
- (abd_step_atom_shortcut; try cont) + (
- (abd_step_later_mono; try cont) ||
- (abd_step_sep P; try cont) ||
+ (abd_step_atom_shortcut; cont) + (
+ tryif abd_step_later_mono then cont else
+ tryif abd_step_sep P then cont else
(abd_step_hyp_exist cont) ||
(abd_step_hyp_mod cont) ||
(abd_step_wand cont) ||
(abd_step_forall cont) ||
- (abd_step_from_goal p P; try cont)
+ (abd_step_from_goal p P; cont)
).
Ltac abd_step_goal_mod :=
@@ -307,12 +307,13 @@ Ltac abd_step_goal_mod :=
Ltac abd_step_goal_exist cont :=
notypeclasses refine (abdgoal_witness_both _ _ _ _ _ _ _ _ _ _);
- [ intros ?; do 2 (notypeclasses refine (ex_intro _ _ _)); split; [try cont | ] | ].
+ [ intros ?; do 2 (notypeclasses refine (ex_intro _ _ _)); split; [cont | ] | ].
Ltac abd_step_goal cont :=
- (solve [eapply abd_unfoldgoal_from_base; [diaframe_hint_search | iSolveTC]]) ||
- (abd_step_goal_mod; try cont) ||
- (abd_step_goal_exist cont).
+ (solve [eapply abd_unfoldgoal_from_base; [diaframe_hint_search | iSolveTC]]) || (
+ tryif abd_step_goal_mod then cont else
+ abd_step_goal_exist cont
+ ).
Ltac find_abd_steps :=
let cont := ltac:(pre_step; find_abd_steps) in
--
GitLab