improvements in tau_collapse_positives cb

IDNI · Dec 26, 2023 · 1f2bed9 · 1f2bed9
1 parent 7e94288
commit 1f2bed9
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 5 deletions.
diff --git a/parser/tau.tgf b/parser/tau.tgf
@@ -264,7 +264,7 @@ wff_remove_existential_cb_sym			=> ws "wff_remove_existential_cb" ws.
 
 
 # cb for tau
-tau_collapse_positives_cb	=> tau_collapse_positives_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg ws_required tau_cb_arg.
+tau_collapse_positives_cb	=> tau_collapse_positives_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg.
 tau_positives_upwards_cb	=> tau_positives_upwards_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg.
 tau_cb_arg	=> capture | tau.
 

diff --git a/parser/tau_parser.generated.h b/parser/tau_parser.generated.h
@@ -701,8 +701,8 @@ struct tau_parser {
 		q(nt(186), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(44)+t(18)+t(16)+nt(13)));
 		// wff_remove_existential_cb_sym => ws 'w' 'f' 'f' '_' 'r' 'e' 'm' 'o' 'v' 'e' '_' 'e' 'x' 'i' 's' 't' 'e' 'n' 't' 'i' 'a' 'l' '_' 'c' 'b' ws.
 		q(nt(187), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(20)+t(24)+t(13)+t(25)+t(59)+t(24)+t(44)+t(24)+t(5)+t(22)+t(28)+t(19)+t(24)+t(12)+t(19)+t(22)+t(10)+t(11)+t(44)+t(18)+t(16)+nt(13)));
-		// tau_collapse_positives_cb => tau_collapse_positives_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg ws_required tau_cb_arg.
-		q(nt(72), (nt(188)+nt(12)+nt(189)+nt(12)+nt(189)+nt(12)+nt(189)));
+		// tau_collapse_positives_cb => tau_collapse_positives_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg.
+		q(nt(72), (nt(188)+nt(12)+nt(189)+nt(12)+nt(189)));
 		// tau_positives_upwards_cb => tau_positives_upwards_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg.
 		q(nt(73), (nt(190)+nt(12)+nt(189)+nt(12)+nt(189)));
 		// tau_cb_arg => capture.

diff --git a/src/formula.h b/src/formula.h
@@ -1424,7 +1424,10 @@ struct callback_applier {
 	sp_tau_node<BAs...> apply_tau_collapse_positives(const sp_tau_node<BAs...>& n) {
 		auto args = n || tau_parser::tau_cb_arg || only_child_extractor<BAs...>;
 		if (auto check_1eft = args[0] | tau_parser::wff; check_1eft)
-			if (auto check_right = args[1] | tau_parser::wff; check_right) return args[2];
+			if (auto check_right = args[1] | tau_parser::wff; check_right) {
+				auto wff = build_wff_and<BAs...>(check_1eft.value(), check_right.value());
+				return make_node<tau_sym<BAs...>>(tau_parser::tau, { wff });
+			}
 		return n;
 	}
 };

diff --git a/src/tau.h b/src/tau.h
@@ -54,7 +54,7 @@ RULE(TAU_SIMPLIFY_SELF_3, "( $X ||| % $X ) := T.")
 RULE(TAU_SIMPLIFY_SELF_4, "( % $X &&& $X ) := F.")
 RULE(TAU_SIMPLIFY_SELF_5, "( % $X ||| $X ) := T.")
 
-RULE(TAU_COLLAPSE_POSITIVES_0, "($X &&& $Y) := tau_collapse_positives $X $Y ($X && $Y).")
+RULE(TAU_COLLAPSE_POSITIVES_0, "($X &&& $Y) := tau_collapse_positives $X $Y.")
 RULE(TAU_PUSH_POSITIVES_UPWARDS_0, "($X &&& ($Y &&& $Z) := tau_positives_upwards $Y ($Y &&& ($X &&& $Z).")
 RULE(TAU_PUSH_POSITIVES_UPWARDS_1, "($X &&& ($Y &&& $Z) := tau_positives_upwards $Z ($Z &&& ($X &&& $Y).")
 RULE(TAU_PUSH_POSITIVES_UPWARDS_2, "(($X &&& $Y) &&& $Z) := tau_positives_upwards $X ($X &&& ($Y &&& $Z).")