collapsing positives in tau set operations

IDNI · Dec 21, 2023 · 83579ce · 83579ce
1 parent 8feb40d
commit 83579ce
Show file tree

Hide file tree

Showing 4 changed files with 294 additions and 253 deletions.
diff --git a/parser/tau.tgf b/parser/tau.tgf
@@ -82,9 +82,9 @@ in				=> "?i_" chars. # instead of '<', easy to remember
 out				=> "?o_" chars. # instead of '>', easy to remember
 
 # tau
-tau_rule			=> tau_matcher definition tau_body dot.
+tau_rule	=> tau_matcher definition tau_body dot.
 tau_matcher	=> tau.
-tau_body	=> tau.
+tau_body	=> tau | tau_collapse_positives_cb | tau_positives_upwards_cb.
 
 
 # TODO (HIGH) check programatically that we do not have inappropriated element from wff in tau
@@ -262,6 +262,12 @@ wff_has_clashing_subformulas_cb_sym		=> ws "wff_has_clashing_subformulas_cb" ws.
 wff_has_subformula_cb_sym				=> ws "wff_has_subformula_cb" ws.
 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_positives_upwards_cb	=> tau_positives_upwards_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg.
+tau_cb_arg	=> capture | tau.
+
 # input definition
 input			=> in colon open_brace source_binding close_brace.