replacing bf_subs_cb with bf_remove_existential_cb and bf_remove_funi…

…versal_cb
IDNI · Jan 9, 2024 · 2b92cd5 · 2b92cd5
1 parent 001454c
commit 2b92cd5
Show file tree

Hide file tree

Showing 7 changed files with 267 additions and 239 deletions.
diff --git a/parser/tau.tgf b/parser/tau.tgf
@@ -163,12 +163,9 @@ bf_rec_relation	=> bf_ref definition bf dot.
 
 bf_matcher	=> bf.
 bf_body 	=> bf | bf_is_zero_cb | bf_is_one_cb | bf_has_clashing_subformulas_cb
-				| bf_has_subformula_cb.
-
-# TODO (MEDIUM) remove bf_subs_cb and add a callback to eliminate fall and fex
+				| bf_has_subformula_cb | bf_remove_funiversal_cb | bf_remove_fexistential_cb.
 bf			=> bf_ref | bf_constant | bf_and | bf_neg | bf_xor | bf_or
-				| bf_all | bf_ex
-				| bf_subs_cb | bf_t | bf_f | variable | capture.
+				| bf_all | bf_ex | bf_t | bf_f | variable | capture.
 bf_ref 		=> sym offsets bf_ref_args.
 bf_ref_args	=> open_parenthesis (variable)* close_parenthesis.
 bf_and		=> open_parenthesis bf bf_and_sym bf close_parenthesis.
@@ -232,28 +229,33 @@ bf_and_cb			=> bf_cb_arg bf_and_cb_sym bf_cb_arg.
 bf_or_cb			=> bf_cb_arg bf_or_cb_sym bf_cb_arg.
 bf_xor_cb			=> bf_cb_arg bf_xor_cb_sym bf_cb_arg.
 bf_neg_cb			=> bf_neg_cb_sym bf_cb_arg.
-bf_subs_cb			=> bf_subs_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required bf_cb_arg.
 bf_eq_cb			=> bf_eq_cb_sym bf_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
 bf_neq_cb			=> bf_neq_cb_sym bf_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
 bf_is_zero_cb		=> bf_is_zero_cb_sym bf_cb_arg ws_required bf_cb_arg.
 bf_is_one_cb		=> bf_is_one_cb_sym bf_cb_arg ws_required bf_cb_arg.
 
+bf_remove_funiversal_cb		=> bf_remove_funiversal_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required bf_cb_arg ws_required bf_cb_arg.
+bf_remove_fexistential_cb	=> bf_remove_fexistential_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required bf_cb_arg ws_required bf_cb_arg.
+wff_remove_existential_cb	=> wff_remove_existential_cb_sym wff_cb_arg ws_required wff_cb_arg.
+wff_remove_bexistential_cb	=> wff_remove_bexistential_cb_sym wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
+wff_remove_buniversal_cb	=> wff_remove_buniversal_cb_sym wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
+
 # extra callbacks to speed up computations
 bf_has_clashing_subformulas_cb	=> bf_has_clashing_subformulas_cb_sym bf_cb_arg ws_required bf_cb_arg.
 wff_has_clashing_subformulas_cb	=> wff_has_clashing_subformulas_cb_sym wff_cb_arg ws_required wff_cb_arg.
 bf_has_subformula_cb 			=> bf_has_subformula_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required bf_cb_arg.
 wff_has_subformula_cb 			=> wff_has_subformula_cb_sym wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
-wff_remove_existential_cb		=> wff_remove_existential_cb_sym wff_cb_arg ws_required wff_cb_arg.
-wff_remove_bexistential_cb		=> wff_remove_bexistential_cb_sym wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
-wff_remove_buniversal_cb		=> wff_remove_buniversal_cb_sym wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
-# IDEA we could reuse the same symbol
+
+# callback symbols
 bf_has_clashing_subformulas_cb_sym		=> ws "bf_has_clashing_subformulas_cb" ws.
 bf_has_subformula_cb_sym				=> ws "bf_has_subformula_cb" ws.
 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.
 wff_remove_bexistential_cb_sym			=> ws "wff_remove_bexistential_cb" ws.
 wff_remove_buniversal_cb_sym			=> ws "wff_remove_buniversal_cb" ws.
+bf_remove_fexistential_cb_sym			=> ws "bf_remove_fexistential_cb" ws.
+bf_remove_funiversal_cb_sym				=> ws "bf_remove_funiversal_cb" ws.
 
 # bultin_args
 bf_cb_arg	=> capture | bf.
@@ -264,7 +266,6 @@ bf_and_cb_sym			=> ws "bf_and_cb" ws.
 bf_or_cb_sym			=> ws "bf_or_cb" ws.
 bf_xor_cb_sym			=> ws "bf_xor_cb" ws.
 bf_neg_cb_sym			=> ws "bf_neg_cb" ws.
-bf_subs_cb_sym			=> ws "bf_subs_cb" ws.
 bf_eq_cb_sym			=> ws "bf_eq_cb" ws.
 bf_neq_cb_sym			=> ws "bf_neq_cb" ws.
 bf_is_zero_cb_sym		=> ws "bf_is_zero_cb" ws.