Dynamic Predicates: non_det_constants/2 deferred_set_constant/3 section_header_generated/1 print_additional_machine_info/0 latex_mode/0 unicode_mode/0 atelierb_mode/1 force_eventb_rodin_mode/0 bugly_scramble_id_cache/2 bugly_count/1 comment_level/1

5896 Lines

645 Predicates

Imported Modules: tools module_information lists codesio terms avl debug error_manager self_check b_global_sets bsyntaxtree bmachine_structure ordsets preferences clpfd

126 Exports

36 specified Imports

Imports	Exports
Name: is_list_simple/1 Module: tools_lists Name: csp_with_bz_mode/0 Module: specfile Name: process_algebra_mode/0 Module: specfile Name: animation_minor_mode/1 Module: specfile Name: set_animation_minor_mode/1 Module: specfile Name: remove_animation_minor_mode/0 Module: specfile Name: animation_mode/1 Module: specfile Name: set_animation_mode/1 Module: specfile Name: csp_mode/0 Module: specfile Name: translate_operation_name/2 Module: specfile Name: get_preference/2 Module: preferences Name: set_preference/2 Module: preferences Name: eclipse_preference/2 Module: preferences Name: check_is_non_empty_avl/1 Module: avl_tools Name: b_get_machine_operation_parameter_types/2 Module: bmachine Name: b_is_operation_name/1 Module: bmachine Name: translate_term_into_atom_with_max_depth/3 Module: tools_meta Name: get_specification_description/2 Module: specfile Name: quick_avl_approximate_size/2 Module: avl_tools Name: is_recursive_closure/3 Module: closures Name: register_event_listener/3 Module: eventhandling Name: put_codes/2 Module: tools_files Name: create_type_set/3 Module: typing_tools Name: get_terminal_colour_code/2 Module: tools_printing Name: no_color/0 Module: tools_printing Name: classical_b_keyword/1 Module: translate_keywords Name: translate_keyword_id/2 Module: translate_keywords Name: is_simple_classical_b_identifier/1 Module: tools_strings Name: latex_escape_atom/2 Module: tools Name: b_string_escape_codes/2 Module: tools Name: convert_atom_to_number/2 Module: tools_strings Name: gensym/2 Module: gensym Name: synonym_for_external_predicate/2 Module: external_function_declarations Name: datime/1 Module: system Name: currently_opened_file/1 Module: specfile Name: format_prob_version/1 Module: version	Name: print_bexpr_or_subst/1 Name: l_print_bexpr_or_subst/1 Name: print_bexpr/1 Name: debug_print_bexpr/1 Name: nested_print_bexpr/1 Name: nested_print_bexpr_as_classicalb/1 Name: print_bexpr_stream/2 Name: print_components/1 Name: print_bexpr_with_limit/2 Name: print_unwrapped_bexpr_with_limit/1 Name: print_bvalue/1 Name: l_print_bvalue/1 Name: print_bvalue_stream/2 Name: translate_params_for_dot/2 Name: translate_params_for_dot_nl/2 Name: print_machine/1 Name: translate_machine/3 Name: set_unicode_mode/0 Name: unset_unicode_mode/0 Name: unicode_mode/0 Name: unicode_translation/2 Name: set_latex_mode/0 Name: unset_latex_mode/0 Name: latex_mode/0 Name: set_atelierb_mode/1 Name: unset_atelierb_mode/0 Name: set_force_eventb_mode/0 Name: unset_force_eventb_mode/0 Name: get_translation_mode/1 Name: set_translation_mode/1 Name: unset_translation_mode/1 Name: with_translation_mode/2 Name: get_language_mode/1 Name: set_language_mode/1 Name: with_language_mode/2 Name: translate_bexpression_to_unicode/2 Name: translate_bexpression/2 Name: translate_subst_or_bexpr_in_mode/3 Name: translate_bexpression_with_limit/3 Name: translate_bexpression_with_limit/2 Name: translate_bexpression_to_codes/2 Name: translate_bexpr_to_parseable/2 Name: translate_predicate_into_machine/3 Name: nested_print_sequent_as_classicalb/6 Name: get_bexpression_column_template/4 Name: translate_subst_or_bexpr/2 Name: translate_subst_or_bexpr_with_limit/3 Name: translate_substitution/2 Name: print_subst/1 Name: translate_bvalue/2 Name: translate_bvalue_to_codes/2 Name: translate_bvalue_to_codes_with_limit/3 Name: translate_bvalue_to_parseable_classicalb/2 Name: translate_bvalue_for_dot/2 Name: translate_bvalue_with_limit/3 Name: translate_bvalue_with_type/3 Name: translate_bvalue_with_type_and_limit/4 Name: translate_bvalue_for_expression/3 Name: translate_bvalue_for_expression_with_limit/4 Name: translate_bvalue_with_tlatype/3 Name: translate_bvalue_kind/2 Name: print_state/1 Name: translate_bstate/2 Name: translate_bstate_limited/2 Name: translate_bstate_limited/3 Name: print_bstate/1 Name: print_bstate_limited/3 Name: translate_b_state_to_comma_list/3 Name: translate_context/2 Name: print_context/1 Name: translate_any_state/2 Name: print_value_variable/1 Name: print_cspm_state/1 Name: translate_cspm_state/2 Name: print_csp_value/1 Name: translate_csp_value/2 Name: translate_cspm_expression/2 Name: translate_properties_with_limit/2 Name: translate_event/2 Name: translate_events/2 Name: translate_event_with_target_id/4 Name: translate_event_with_src_and_target_id/4 Name: translate_event_with_src_and_target_id/5 Name: get_non_det_modified_vars_in_target_id/3 Name: translate_event_with_limit/3 Name: translate_state_errors/2 Name: translate_state_error/2 Name: translate_event_error/2 Name: translate_call_stack/2 Name: translate_prolog_constructor/2 Name: translate_prolog_constructor_in_mode/2 Name: get_texpr_top_level_symbol/4 Name: pretty_type/2 Name: explain_state_error/3 Name: get_state_error_span/2 Name: explain_event_trace/3 Name: generate_typing_predicates/2 Name: print_raw_machine_terms/1 Name: print_raw_bexpr/1 Name: l_print_raw_bexpr/1 Name: translate_raw_bexpr_with_limit/3 Name: print_span/1 Name: print_span_nl/1 Name: translate_span/2 Name: translate_span_with_filename/2 Name: get_definition_context_from_span/2 Name: translate_error_term/2 Name: translate_error_term/3 Name: translate_prolog_exception/2 Name: set_translation_constants/1 Name: set_translation_context/1 Name: clear_translation_constants/0 Name: set_print_type_infos/1 Name: suppress_rodin_positions/1 Name: reset_suppress_rodin_positions/1 Name: add_normal_typing_predicates/3 Name: install_b_portray_hook/0 Name: remove_b_portray_hook/0 Name: translate_eventb_to_classicalb/3 Name: translate_eventb_direct_definition_header/3 Name: translate_eventb_direct_definition_body/2 Name: return_csp_closure_value/2 Name: latex_to_unicode/2 Name: get_latex_keywords/1 Name: get_latex_keywords_with_backslash/1 Name: ascii_to_unicode/2

Imports

Exports

Name: is_list_simple/1

Module: tools_lists

Name: csp_with_bz_mode/0

Module: specfile

Name: process_algebra_mode/0

Module: specfile

Name: animation_minor_mode/1

Module: specfile

Name: set_animation_minor_mode/1

Module: specfile

Name: remove_animation_minor_mode/0

Module: specfile

Name: animation_mode/1

Module: specfile

Name: set_animation_mode/1

Module: specfile

Name: csp_mode/0

Module: specfile

Name: translate_operation_name/2

Module: specfile

Name: get_preference/2

Module: preferences

Name: set_preference/2

Module: preferences

Name: eclipse_preference/2

Module: preferences

Name: check_is_non_empty_avl/1

Module: avl_tools

Name: b_get_machine_operation_parameter_types/2

Module: bmachine

Name: b_is_operation_name/1

Module: bmachine

Name: translate_term_into_atom_with_max_depth/3

Module: tools_meta

Name: get_specification_description/2

Module: specfile

Name: quick_avl_approximate_size/2

Module: avl_tools

Name: is_recursive_closure/3

Module: closures

Name: register_event_listener/3

Module: eventhandling

Name: put_codes/2

Module: tools_files

Name: create_type_set/3

Module: typing_tools

Name: get_terminal_colour_code/2

Module: tools_printing

Name: no_color/0

Module: tools_printing

Name: classical_b_keyword/1

Module: translate_keywords

Name: translate_keyword_id/2

Module: translate_keywords

Name: is_simple_classical_b_identifier/1

Module: tools_strings

Name: latex_escape_atom/2

Module: tools

Name: b_string_escape_codes/2

Module: tools

Name: convert_atom_to_number/2

Module: tools_strings

Name: gensym/2

Module: gensym

Name: synonym_for_external_predicate/2

Module: external_function_declarations

Name: datime/1

Module: system

Name: currently_opened_file/1

Module: specfile

Name: format_prob_version/1

Module: version

Name: print_bexpr_or_subst/1

Name: l_print_bexpr_or_subst/1

Name: print_bexpr/1

Name: debug_print_bexpr/1

Name: nested_print_bexpr/1

Name: nested_print_bexpr_as_classicalb/1

Name: print_bexpr_stream/2

Name: print_components/1

Name: print_bexpr_with_limit/2

Name: print_unwrapped_bexpr_with_limit/1

Name: print_bvalue/1

Name: l_print_bvalue/1

Name: print_bvalue_stream/2

Name: translate_params_for_dot/2

Name: translate_params_for_dot_nl/2

Name: print_machine/1

Name: translate_machine/3

Name: set_unicode_mode/0

Name: unset_unicode_mode/0

Name: unicode_mode/0

Name: unicode_translation/2

Name: set_latex_mode/0

Name: unset_latex_mode/0

Name: latex_mode/0

Name: set_atelierb_mode/1

Name: unset_atelierb_mode/0

Name: set_force_eventb_mode/0

Name: unset_force_eventb_mode/0

Name: get_translation_mode/1

Name: set_translation_mode/1

Name: unset_translation_mode/1

Name: with_translation_mode/2

Name: get_language_mode/1

Name: set_language_mode/1

Name: with_language_mode/2

Name: translate_bexpression_to_unicode/2

Name: translate_bexpression/2

Name: translate_subst_or_bexpr_in_mode/3

Name: translate_bexpression_with_limit/3

Name: translate_bexpression_with_limit/2

Name: translate_bexpression_to_codes/2

Name: translate_bexpr_to_parseable/2

Name: translate_predicate_into_machine/3

Name: nested_print_sequent_as_classicalb/6

Name: get_bexpression_column_template/4

Name: translate_subst_or_bexpr/2

Name: translate_subst_or_bexpr_with_limit/3

Name: translate_substitution/2

Name: print_subst/1

Name: translate_bvalue/2

Name: translate_bvalue_to_codes/2

Name: translate_bvalue_to_codes_with_limit/3

Name: translate_bvalue_to_parseable_classicalb/2

Name: translate_bvalue_for_dot/2

Name: translate_bvalue_with_limit/3

Name: translate_bvalue_with_type/3

Name: translate_bvalue_with_type_and_limit/4

Name: translate_bvalue_for_expression/3

Name: translate_bvalue_for_expression_with_limit/4

Name: translate_bvalue_with_tlatype/3

Name: translate_bvalue_kind/2

Name: print_state/1

Name: translate_bstate/2

Name: translate_bstate_limited/2

Name: translate_bstate_limited/3

Name: print_bstate/1

Name: print_bstate_limited/3

Name: translate_b_state_to_comma_list/3

Name: translate_context/2

Name: print_context/1

Name: translate_any_state/2

Name: print_value_variable/1

Name: print_cspm_state/1

Name: translate_cspm_state/2

Name: print_csp_value/1

Name: translate_csp_value/2

Name: translate_cspm_expression/2

Name: translate_properties_with_limit/2

Name: translate_event/2

Name: translate_events/2

Name: translate_event_with_target_id/4

Name: translate_event_with_src_and_target_id/4

Name: translate_event_with_src_and_target_id/5

Name: get_non_det_modified_vars_in_target_id/3

Name: translate_event_with_limit/3

Name: translate_state_errors/2

Name: translate_state_error/2

Name: translate_event_error/2

Name: translate_call_stack/2

Name: translate_prolog_constructor/2

Name: translate_prolog_constructor_in_mode/2

Name: get_texpr_top_level_symbol/4

Name: pretty_type/2

Name: explain_state_error/3

Name: get_state_error_span/2

Name: explain_event_trace/3

Name: generate_typing_predicates/2

Name: print_raw_machine_terms/1

Name: print_raw_bexpr/1

Name: l_print_raw_bexpr/1

Name: translate_raw_bexpr_with_limit/3

Name: print_span/1

Name: print_span_nl/1

Name: translate_span/2

Name: translate_span_with_filename/2

Name: get_definition_context_from_span/2

Name: translate_error_term/2

Name: translate_error_term/3

Name: translate_prolog_exception/2

Name: set_translation_constants/1

Name: set_translation_context/1

Name: clear_translation_constants/0

Name: set_print_type_infos/1

Name: suppress_rodin_positions/1

Name: reset_suppress_rodin_positions/1

Name: add_normal_typing_predicates/3

Name: install_b_portray_hook/0

Name: remove_b_portray_hook/0

Name: translate_eventb_to_classicalb/3

Name: translate_eventb_direct_definition_header/3

Name: translate_eventb_direct_definition_body/2

Name: return_csp_closure_value/2

Name: latex_to_unicode/2

Name: get_latex_keywords/1

Name: get_latex_keywords_with_backslash/1

Name: ascii_to_unicode/2

Predicates

Predicates:

adapt_machine_name/2

adapt_state/3

adapt_value_according_to_type/3

add_normal_typing_predicates/3

add_optional_typing_predicates/3

add_outer_paren/6

add_span_label/5

add_typing_predicates/3

always_surround_by_parentheses/1

and_symbol-->/2

ascii_to_unicode/2

asharing_csp_op/8

atelierb_pp_translation/2

binary_infix_in_mode/4

binary_infix_symbol/2

binary_pred/4

block_set_up_limit_reached/3

bynary_numeric_operation/4

call_pp_with_no_limit_and_parseable/1

call_stack_arrow_atom_symbol/1

can_indent_expr/1

can_indent_texpr/1

check_info/3

clear_translation_constants/0

colour_construct/2

colour_translation/3

combine_span_pred/5

compute_non_det_constants2/2

constants/2

constants_in_mode/2

conversion_check/1

convert_and_ajoin_ids/2

convert_avlset_into_sequence/2

convert_avlset_into_sequence2/3

convert_event/3

convert_event2/4

convert_eventb_classicalb/2

convert_eventop/2

convert_id/2

convert_set_into_sequence/2

convert_set_into_sequence1/2

convert_set_into_sequence2/5

create_assign/3

create_label/4

create_tvalue/3

dcg_set_up_limit_reached/4

decrease_indentation_level/3

decrease_indentation_level-->/2

def_description/2

definition_decl_from_library/2

detect_lambda_comprehension/5

do_indention/3

dot_bullet_symbol-->/2

dot_symbol-->/2

dummy_def_body/2

empty_set_symbol-->/2

end_size/4

enter_comment-->/2

eventb_integer_mapping/2

eventb_translation_mode/0

exctract_span_pred_from_subst/2

exists_symbol-->/2

exit_comment-->/2

explain_abort_error_type/3

explain_action_not_executable/4

explain_error_context1/3

explain_error_context2/3

explain_event_step/3

explain_event_step4/4

explain_event_trace/3

explain_event_trace/4

explain_event_trace4/6

explain_local_state/3

explain_predicate/4

explain_simulation_error/4

explain_simulation_errors/4

explain_span/3

explain_span2/3

explain_span_context/3

explain_span_file/3

explain_state_error/3

explain_state_error2/4

expression_has_tla_type/2

external_call/4

extract_def_calls/3

extract_def_context_msg/2

extract_equality/4

extract_vartype_names/2

field_value_present/3

forall_symbol-->/2

format_proof_infos/2

function_like/2

function_like_in_mode/2

gen_bugly_id/2

gen_bugly_id_codes/2

genbuglynr/1

generate_typed_int_set/2

generate_typing_predicate/3

generate_typing_predicates/2

generate_typing_predicates/3

get_all_ids/3

get_bexpression_column_template/4

get_binary_connective/5

get_call_stack_span/2

get_cs_avl_limit/1

get_cs_limit/1

get_definition_context_from_span/2

get_error_span_for_value/2

get_eventb_default_label/2

get_function_from_span/4

get_latex_keywords_with_backslash/1

get_non_det_constant/2

get_non_det_modified_vars_in_target_id/3

get_pp_state_limit/1

get_sep_prio/2

get_span_context_span/2

get_span_from_context/2

get_specification_description_codes/2

get_state_error_span/2

get_texpr_top_level_symbol/4

get_translation_mode/1

get_type/2

get_variables/2

get_was_identifier/2

greek_or_math_symbol/1

greek_symbol/2

hash_card_symbol-->/2

id_requires_escaping/1

in_parallel/2

inc_indent/4

inc_lvl/4

increase_indentation_level/3

increase_indentation_level-->/2

indent/3

indent-->/2

indent2/4

indent_binary_predicate/4

init_machine_translation/0

insert_library_usages/3

install_b_portray_hook/0

integer_set_mapping/2

integer_set_mapping/3

invisible_external_pred/1

is_duplicate_predicate/2

is_init/1

is_lambda_result_id/2

is_lambda_result_name/2

is_nontrivial_negation/4

is_printable_set/2

is_projection/2

is_set_pref/1

is_set_pref_def_name/3

is_subst_type/1

is_top_level_function_call/1

is_typing_predicate/2

l_adapt_value_according_to_type/3

l_print_bexpr_or_subst/1

l_print_bvalue/1

l_print_frozen_info/1

l_print_raw_bexpr/1

lambda_symbol-->/2

latex_integer_set_translation/2

left_set_bracket-->/2

my_greek_latex_escape_atom/3

nested_print_bexpr2/2

nested_print_bexpr_as_classicalb/1

nested_print_bexpr_as_classicalb2/2

nested_print_sequent_as_classicalb/6

nested_print_sequent_as_classicalb_aux/6

non_det_modified_var/2

pp_all_disjoint_aux/5

pp_annotations/4

pp_any_state/4

pp_any_state_with_limit/4

pp_argument/3

pp_atom_indent/3

pp_atom_opt_latex/3

pp_atom_opt_latex_mathit/3

pp_atom_opt_mathit/3

pp_b_context/3

pp_b_state/4

pp_b_state_comma_list/5

pp_b_state_list/4

pp_backquoted_id_codes/3

pp_backquoted_identifier/3

pp_begin_sequence-->/2

pp_bugly_composed_string/3

pp_bugly_composed_string_codes/4

pp_codes_opt_scramble/3

pp_colour_code/3

pp_comprehension_set/6

pp_comprehension_set5/7

pp_cur_context_state-->/2

pp_current_state-->/2

pp_description_pragma_of/3

pp_disjoint/5

pp_empty_sequence-->/2

pp_end_label_pragma-->/2

pp_end_sequence-->/2

pp_event_b_comprehension_set/6

pp_eventb_direct_definition_header/4

pp_eventb_operator_args/3

pp_expr_ids_in_mode/4

pp_expr_ids_in_mode_indent/3

pp_expr_ids_no_parentheses/4

pp_expr_l_pair_in_mode/4

pp_expr_let_pred_exprs/5

pp_function_left_bracket-->/2

pp_function_right_bracket-->/2

pp_functor/3

pp_identifier/3

pp_identifier_for_atelierb/3

pp_ids_indent/3

pp_important_infos/4

pp_inner_value/4

pp_is_important_info_field/3

pp_label/4

pp_lambda_identifiers/4

pp_property_without_plugin/3

pp_rodin_label_indent/3

pp_separator_sequence/1

pp_sequence/4

pp_sequence_with_limit/4

pp_single_csp_value/2

pp_space-->/2

pp_start_label_pragma-->/2

pp_such_that_bar/3

pp_such_that_bar-->/2

pp_theory_operator/5

pp_tla_value/4

pp_tla_with_sep/7

pp_tla_with_sep_aux/6

pp_value_l_with_limit/5

pp_value_l_with_types/6

ppatom_opt_scramble/3

ppatoms/3

ppatoms_opt_latex/3

ppcodes/3

ppcodes_with_limit_reached/4

ppnumber/3

ppstring_opt_scramble/3

ppterm/3

ppterm_with_limit_reached/4

pretty_normalized_type/2

print_additional_machine_info/0

print_bexpr/1

print_bexpr_or_subst/1

print_bexpr_stream/2

print_bexpr_with_limit/2

print_bracket/3

print_bstate/1

print_bstate_limited/3

print_bvalue/1

print_bvalue_stream/2

print_clpfd_variable/1

print_raw_machine_terms/1

print_raw_machine_terms_sep/2

print_unwrapped_bexpr_with_limit/1

print_unwrapped_bexpr_with_limit/2

print_value_variable/1

remove_already_typed_ids/3

remove_already_typed_ids2/3

remove_b_portray_hook/0

remove_duplicate_predicates/3

render_function_call/4

render_function_name/3

render_negation_context/3

render_nr/6

render_operator_arg/3

render_operator_args/3

render_prob_command/3

reset_suppress_rodin_positions/1

reset_translate/0

return_csp_closure_value/2

right_set_bracket-->/2

section_pred_over_lines/5

select_membership/4

set_atelierb_mode/1

set_brackets/2

set_force_eventb_mode/0

set_language_mode/1

set_latex_mode/0

set_pref_used/1

set_print_type_infos/1

set_suppress_rodin_positions/2

set_translation_constants/1

set_translation_context/1

set_translation_mode/1

set_unicode_mode/0

set_up_limit_reached/3

show_parameter_value/4

show_parameter_values/4

size_is_in_set_limit/1

standard_library_required/2

start_size/3

status_string/2

string_end_symbol-->/2

string_start_symbol-->/2

strip_code/3

strip_illegal_id_codes/3

strip_illegal_id_codes2/3

subst_needs_begin_end/1

suppress_rodin_positions/1

symbolic_raw/2

transform_raw/2

transform_raw_list/2

transform_raw_list_to_conjunct/2

transform_raw_list_to_couple/2

translate_additional_description/2

translate_any_state/2

translate_b_operation_call/4

translate_b_state_to_comma_list/3

translate_b_state_to_comma_list_codes/4

translate_bexpr_for_call_stack/2

translate_bexpr_to_parseable/2

translate_bexpression/2

translate_bexpression_to_codes/2

translate_bexpression_to_unicode/2

translate_bexpression_with_limit/2

translate_bexpression_with_limit/3

translate_bexpression_with_limit/4

translate_bstate/2

translate_bstate_limited/2

translate_bstate_limited/3

translate_bstate_limited/4

translate_bvalue/2

translate_bvalue_for_dot/2

translate_bvalue_for_expression/3

translate_bvalue_for_expression_with_limit/4

translate_bvalue_kind/2

translate_bvalue_to_codes/2

translate_bvalue_to_codes_with_limit/3

translate_bvalue_to_parseable_aux/2

translate_bvalue_to_parseable_classicalb/2

translate_bvalue_with_limit/3

translate_bvalue_with_limit_aux/3

translate_bvalue_with_tlatype/3

translate_bvalue_with_type/3

translate_bvalue_with_type_and_limit/4

translate_bvalue_with_type_and_limit2/4

translate_bvalues/2

translate_bvalues_with_limit/3

translate_bvalues_with_types/3

translate_call_stack/2

translate_cases/3

translate_channel_values/3

translate_context/2

translate_csp_value/2

translate_cspm_expression/2

translate_cspm_state/2

translate_error_context/2

translate_error_context2/3

translate_error_term/2

translate_error_term/3

translate_event/2

translate_event2/3

translate_event_error/2

translate_event_error2/2

translate_event_with_limit/3

translate_event_with_src_and_target_id/4

translate_event_with_src_and_target_id/5

translate_event_with_target_id/4

translate_event_with_target_id2/5

translate_eventb_direct_definition_body/2

translate_eventb_direct_definition_header/3

translate_eventb_operator/4

translate_eventb_operator2/7

translate_eventb_operators/3

translate_eventb_to_classicalb/3

translate_events/2

translate_freetype/3

translate_freetype_cases/3

translate_freetypes/3

translate_op_params/3

translate_op_results/3

translate_operation/6

translate_ops/3

translate_other_defpart/3

translate_params_for_dot/2

translate_params_for_dot/4

translate_params_for_dot_nl/2

translate_predicate_into_machine/3

translate_pref_val/2

translate_prolog_constructor/2

translate_prolog_constructor_in_mode/2

translate_prolog_error/3

translate_prolog_exception/2

translate_properties_with_limit/2

translate_property_with_limit/3

translate_raw_bexpr_with_limit/3

translate_section_list/2

translate_set_pref_def/3

translate_set_pref_defs/3

translate_set_pref_defs1/3

translate_span/2

translate_span/4

translate_span_file/4

translate_span_file_opt/4

translate_span_with_filename/2

translate_state_error/2

translate_state_errors/2

translate_subst/3

translate_subst2/3

translate_subst_begin_end/3

translate_subst_check/3

translate_subst_or_bexpr/2

translate_subst_or_bexpr_in_mode/3

translate_subst_or_bexpr_with_limit/3

translate_subst_or_bexpr_with_limit/4

translate_subst_with_indention/4

translate_subst_with_indention_and_label/4

translate_subst_with_label/3

translate_substitution/2

translate_substitution/3

translate_used/3

translate_used2/3

translate_whens/4

translated_identifier/2

treat_constants/1

try_get_identifier/2

try_pp_b_state/4

type_infos_in_subst/3

type_infos_in_subst2/3

unary_postfix/3

unary_postfix_in_mode/3

unary_prefix/3

unary_prefix_parentheses/2

underscore_symbol-->/2

unicode_translation/2

unset_atelierb_mode/0

unset_force_eventb_mode/0

unset_latex_mode/0

unset_translation_mode/1

unset_unicode_mode/0

use_colour_codes/0

var_not_really_modified/2

was_eventb_destructor/4

with_language_mode/2

with_translation_mode/2

witness_intro/5

write_goal_with_max_depth/3

write_with_max_depth/4

adapt_machine_name/2

adapt_state/3

adapt_value_according_to_type/3

add_normal_typing_predicates/3

add_optional_typing_predicates/3

add_outer_paren/6

Block: add_outer_paren(-,?,?,?,?,?)

add_span_label/5

add_typing_predicates/3

always_surround_by_parentheses/1

and_symbol-->/2

ascii_to_unicode/2

asharing_csp_op/8

atelierb_pp_translation/2

binary_infix(composition,';',20,left).

binary_infix(overwrite,'<+',160,left).

binary_infix(direct_product,'><',160,left). % Rodin requires parentheses

binary_infix(parallel_product,'||',20,left).

binary_infix(concat,'^',160,left).

binary_infix(relations,'<->',125,left).

binary_infix(partial_function,'+->',125,left).

binary_infix(total_function,'-->',125,left).

binary_infix(partial_injection,'>+>',125,left).

binary_infix(total_injection,'>->',125,left).

binary_infix(partial_surjection,'+->>',125,left).

binary_infix(total_surjection,Symbol,125,left) :-
(eventb_translation_mode -> Symbol = '->>'; Symbol = '-->>').

binary_infix(total_bijection,'>->>',125,left).

binary_infix(partial_bijection,'>+>>',125,left).

binary_infix(total_relation,'<<->',125,left). % only in Event-B

binary_infix(surjection_relation,'<->>',125,left). % only in Event-B

binary_infix(total_surjection_relation,'<<->>',125,left). % only in Event-B

binary_infix(insert_front,'->',160,left).

binary_infix(insert_tail,'<-',160,left).

binary_infix(domain_restriction,'<|',160,left).

binary_infix(domain_subtraction,'<<|',160,left).

binary_infix(range_restriction,'|>',160,left).

binary_infix(range_subtraction,'|>>',160,left).

binary_infix(intersection,'/\\',160,left).

binary_infix(union,'\\/',160,left).

binary_infix(restrict_front,'/|\\',160,left).

binary_infix(restrict_tail,'\\|/',160,left).

binary_infix(couple,'|->',160,left).

binary_infix(interval,'..',170,left).

binary_infix(add,+,180,left).

binary_infix(add_real,+,180,left).

binary_infix(minus,-,180,left).

binary_infix(minus_real,-,180,left).

binary_infix(set_subtraction,'\\',180,left) :- eventb_translation_mode,!. % symbol is not allowed by Atelier-B

binary_infix(set_subtraction,-,180,left).

binary_infix(minus_or_set_subtract,-,180,left).

binary_infix(multiplication,*,190,left).

binary_infix(multiplication_real,*,190,left).

binary_infix(cartesian_product,**,190,left) :- eventb_translation_mode,!.

binary_infix(cartesian_product,*,190,left).

binary_infix(mult_or_cart,*,190,left). % in case type checker not yet run

binary_infix(div,/,190,left).

binary_infix(div_real,/,190,left).

binary_infix(floored_div,div,190,left) :- animation_minor_mode(tla).

binary_infix(modulo,mod,190,left).

binary_infix(power_of,**,200,right).

binary_infix(power_of_real,**,200,right).

binary_infix(typeof,oftype,120,right). % Event-B oftype operator; usually removed by btypechecker, technically has no associativity in our parser, but right associativity matches better

binary_infix(ring,'\x2218\',160,left). % our B Parser gives ring same priority as direct_product or overwrite

binary_infix(implication,'=>',30,left).

binary_infix(conjunct,'&',40,left).

binary_infix(disjunct,or,40,left).

binary_infix(equivalence,'<=>',Prio,left) :- % in Rodin this has the same priority as implication
(eventb_translation_mode -> Prio=30 ; Prio=60).

binary_infix(equal,=,60,left).

binary_infix(not_equal,'/=',160,left).

binary_infix(less_equal,'<=',160,left).

binary_infix(less,'<',160,left).

binary_infix(less_equal_real,'<=',160,left).

binary_infix(less_real,'<',160,left).

binary_infix(greater_equal,'>=',160,left).

binary_infix(greater,'>',160,left).

binary_infix(member,':',60,left).

binary_infix(not_member,'/:',160,left).

binary_infix(subset,'<:',110,left).

binary_infix(subset_strict,'<<:',110,left).

binary_infix(not_subset,'/<:',110,left).

binary_infix(not_subset_strict,'/<<:',110,left).

binary_infix(values_entry,'=',60,left).

binary_infix_in_mode/4

binary_infix_symbol/2

binary_pred/4

block_set_up_limit_reached/3

Block: block_set_up_limit_reached(-,?,?)

Dynamic: true

bynary_numeric_operation/4

call_pp_with_no_limit_and_parseable/1

Meta: call_pp_with_no_limit_and_parseable(0)

call_stack_arrow_atom_symbol/1

can_indent_expr/1

can_indent_texpr/1

check_info/3

clear_translation_constants/0

colour_construct/2

colour_translation/3

combine_span_pred/5

compute_non_det_constants2/2

constants/2

constants_in_mode/2

conversion_check/1

convert_and_ajoin_ids/2

convert_avlset_into_sequence/2

convert_avlset_into_sequence2/3

convert_event/3

convert_event2/4

convert_eventb_classicalb/2

convert_eventop/2

convert_id/2

convert_set_into_sequence/2

convert_set_into_sequence1/2

convert_set_into_sequence2/5

create_assign/3

create_label/4

create_tvalue/3

dcg_set_up_limit_reached/4

decrease_indentation_level/3

decrease_indentation_level-->/2

def_description/2

definition_decl_from_library/2

detect_lambda_comprehension/5

do_indention/3

dot_bullet_symbol-->/2

dot_symbol-->/2

dummy_def_body/2

empty_set_symbol-->/2

end_size/4

enter_comment-->/2

eventb_integer_mapping/2

eventb_translation_mode/0

exctract_span_pred_from_subst/2

exists_symbol-->/2

exit_comment-->/2

explain_abort_error_type/3

explain_action_not_executable/4

explain_error_context1/3

explain_error_context2/3

explain_event_step/3

explain_event_step(variant_checked_pre(CType,Variant,Value)) -->
    " ",ppatom(CType)," event: checking if the variant is non-negative:\n",
    " variant: ",pp_expr(Variant,_,_LR),"\n",
    " its value: ",pp_value(Value),"\n".

explain_event_step(variant_negative(CType,Variant,Value)) -->
    explain_event_step(variant_checked_pre(CType,Variant,Value)),
    " ERROR: variant is negative\n".

explain_event_step(variant_checked_post(CType,Variant,EntryValue,ExitValue)) -->
    " ",ppatom(CType)," event: checking if the variant is ",
    ( {CType==convergent} -> "decreased:\n" ; "not increased:\n"),
    " variant: ", pp_expr(Variant,_,_LR), "\n",
    " its value before: ", pp_value(EntryValue),"\n",
    " its value after: ", pp_value(ExitValue),"\n".

explain_event_step(invalid_variant(CType,Variant,EntryValue,ExitValue)) -->
    explain_event_step(variant_checked_post(CType,Variant,EntryValue,ExitValue)),
    " ERROR: variant has ",
    ({CType==convergent} -> "not been decreased\n"; "has been increased\n").

explain_event_step(no_witness_found(Type,Id,Predicate)) -->
    witness_intro(Id,Predicate,Type),
    " ERROR: no solution for witness predicate found!\n".

explain_event_step(action(Lhs,_Rhs,Values)) -->
    " executing an action:\n",
    show_assignments(Lhs,Values).

explain_event_step(action_set(Lhs,_Rhs,ValueSet,Values)) -->
    " executing an action:\n ",
    pp_expr_l(Lhs,_LR)," :: ",pp_value(ValueSet),"\n choosing\n",
    show_assignments(Lhs,Values).

explain_event_step(action_pred(Ids,Pred,Values)) -->
    " executing an action:\n ",
    pp_expr_l(Ids,_LR1)," :| ",pp_expr(Pred,_,_LR2),"\n choosing\n",
    show_assignments(Ids,Values).

explain_event_step(error(Error,_Id)) -->
    % the error marker serves to link to a stored state-error by its ID
    explain_event_step(Error).

explain_event_step(event_wd_error(TExpr,Source)) -->
    " Well-Definedness ERROR for ", ppatom(Source), "\n",
    " ", pp_expr(TExpr,_,_LR), "\n".

explain_event_step(event_other_error(Msg)) --> ppatom(Msg).

explain_event_step4/4

explain_event_trace/3

explain_event_trace/4

explain_event_trace4/6

explain_local_state/3

explain_predicate/4

explain_simulation_error/4

explain_simulation_errors/4

explain_span/3

explain_span2/3

explain_span_context/3

explain_span_file/3

explain_state_error/3

explain_state_error2/4

expression_has_tla_type/2

external_call/4

extract_def_calls/3

extract_def_context_msg/2

extract_equality/4

extract_vartype_names/2

field_value_present/3

forall_symbol-->/2

format_proof_infos/2

function_like/2

function_like(convert_bool,bool).

function_like(convert_real,real). % cannot be used on its own: dom(real) is not accepted by Atelier-B

function_like(convert_int_floor,floor). % ditto

function_like(convert_int_ceiling,ceiling). % ditto

function_like(successor,succ). % can also be used on its own; e.g., dom(succ)=INTEGER is ok

function_like(predecessor,pred). % ditto

function_like(max,max).

function_like(max_real,max).

function_like(min,min).

function_like(min_real,min).

function_like(card,card).

function_like(pow_subset,'POW').

function_like(pow1_subset,'POW1').

function_like(fin_subset,'FIN').

function_like(fin1_subset,'FIN1').

function_like(identity,id).

function_like(first_projection,prj1).

function_like(first_of_pair,'prj1'). % used to be __first_of_pair, will be dealt with separately to generate parsable representation

function_like(second_projection,prj2).

function_like(second_of_pair,'prj2'). % used to be __second_of_pair, will be dealt with separately to generate parsable representation

function_like(iteration,iterate).

function_like(event_b_first_projection_v2,prj1).

function_like(event_b_second_projection_v2,prj2).

function_like(reflexive_closure,closure).

function_like(closure,closure1).

function_like(domain,dom).

function_like(range,ran).

function_like(seq,seq).

function_like(seq1,seq1).

function_like(iseq,iseq).

function_like(iseq1,iseq1).

function_like(perm,perm).

function_like(size,size).

function_like(first,first).

function_like(last,last).

function_like(front,front).

function_like(tail,tail).

function_like(rev,rev).

function_like(general_concat,conc).

function_like(general_union,union).

function_like(general_intersection,inter).

function_like(trans_function,fnc).

function_like(trans_relation,rel).

function_like(tree,tree).

function_like(btree,btree).

function_like(const,const).

function_like(top,top).

function_like(sons,sons).

function_like(prefix,prefix).

function_like(postfix,postfix).

function_like(sizet,sizet).

function_like(mirror,mirror).

function_like(rank,rank).

function_like(father,father).

function_like(son,son).

function_like(subtree,subtree).

function_like(arity,arity).

function_like(bin,bin).

function_like(left,left).

function_like(right,right).

function_like(infix,infix).

function_like(rec,rec).

function_like(struct,struct).

function_like(negation,not).

function_like(bag_items,items).

function_like(finite,finite). % from Event-B, TO DO: if \+ eventb_translation_mode then print as S:FIN(S)

function_like(witness,'@witness'). % from Event-B

function_like(floored_div,'FDIV') :- \+ animation_minor_mode(tla). % using external function

function_like_in_mode/2

gen_bugly_id/2

gen_bugly_id_codes/2

genbuglynr/1

generate_typed_int_set/2

generate_typing_predicate/3

generate_typing_predicates/2

generate_typing_predicates/3

get_all_ids/3

get_bexpression_column_template/4

get_binary_connective/5

get_call_stack_span/2

get_cs_avl_limit/1

get_cs_limit/1

get_definition_context_from_span/2

get_error_span_for_value/2

get_eventb_default_label/2

get_function_from_span/4

get_latex_keywords_with_backslash/1

get_non_det_constant/2

get_non_det_modified_vars_in_target_id/3

get_pp_state_limit/1

get_sep_prio/2

get_span_context_span/2

get_span_from_context/2

get_specification_description_codes/2

get_state_error_span/2

get_texpr_top_level_symbol/4

get_translation_mode/1

get_type/2

get_variables/2

get_was_identifier/2

greek_or_math_symbol/1

greek_or_math_symbol(Symbol) :- greek_symbol(Symbol,_).

greek_or_math_symbol('varepsilon').

greek_or_math_symbol('varphi').

greek_or_math_symbol('varpi').

greek_or_math_symbol('varrho').

greek_or_math_symbol('varsigma').

greek_or_math_symbol('vartheta').

greek_or_math_symbol('vdash').

greek_or_math_symbol('models').

Calls:

Name: greek_symbol/2

Module: translate

Called:

Name: my_greek_latex_escape_atom/3

Module: translate

greek_symbol/2

hash_card_symbol-->/2

id_requires_escaping/1

in_parallel/2

inc_indent/4

inc_lvl/4

increase_indentation_level/3

increase_indentation_level-->/2

indent/3

indent-->/2

indent2/4

indent_binary_predicate/4

init_machine_translation/0

insert_library_usages/3

install_b_portray_hook/0

integer_set_mapping/2

integer_set_mapping/3

invisible_external_pred/1

is_duplicate_predicate/2

is_init/1

is_lambda_result_id/2

is_lambda_result_name/2

is_nontrivial_negation/4

is_printable_set/2

is_projection/2

is_set_pref/1

is_set_pref_def_name/3

is_subst_type/1

is_top_level_function_call/1

is_typing_predicate/2

l_adapt_value_according_to_type/3

l_print_bexpr_or_subst/1

l_print_bvalue/1

l_print_frozen_info/1

l_print_raw_bexpr/1

lambda_symbol-->/2

latex_integer_set_translation/2

latex_to_b_ast/2

latex_to_b_ast(and,conjunct).

latex_to_b_ast(bcomp,ring). % bsymb: backwards composition

latex_to_b_ast(bigcap,quantified_intersection).

latex_to_b_ast(bigcup,quantified_union).

latex_to_b_ast(cap,intersection).

latex_to_b_ast(cart,cartesian_product).

latex_to_b_ast(cprod,cartesian_product).

latex_to_b_ast(cdot,dot_symbol).

latex_to_b_ast(cup,union).

latex_to_b_ast(dprod,direct_product).

latex_to_b_ast(dres,domain_restriction).

latex_to_b_ast(dsub,domain_subtraction).

latex_to_b_ast(emptyset,empty_set).

latex_to_b_ast(exp,power_of).

latex_to_b_ast(geq,greater_equal).

latex_to_b_ast(implies,implication).

latex_to_b_ast(in,member).

latex_to_b_ast(int,'INTEGER').

latex_to_b_ast(intg,'INTEGER'). % from bsymb

latex_to_b_ast(lambda,lambda).

latex_to_b_ast(land,conjunct).

latex_to_b_ast(leq,less_equal).

latex_to_b_ast(leqv,equivalence).

latex_to_b_ast(lhd,domain_restriction).

latex_to_b_ast(limp,implication).

latex_to_b_ast(lor,disjunct).

latex_to_b_ast(lnot,negation).

latex_to_b_ast(mapsto,couple).

latex_to_b_ast(nat,'NATURAL').

latex_to_b_ast(natn,'NATURAL1').

latex_to_b_ast(neg,negation).

latex_to_b_ast(neq,not_equal).

latex_to_b_ast(nin,not_member).

latex_to_b_ast(not,negation).

latex_to_b_ast(nsubseteq,not_subset).

latex_to_b_ast(nsubset,not_subset_strict).

latex_to_b_ast(or,disjunct).

latex_to_b_ast(pfun,partial_function).

latex_to_b_ast(pinj,partial_injection).

latex_to_b_ast(psur,partial_surjection).

latex_to_b_ast(pow,pow_subset).

latex_to_b_ast(pown,pow1_subset).

latex_to_b_ast(pprod,parallel_product).

latex_to_b_ast(qdot,dot_symbol).

latex_to_b_ast(real,'REAL').

latex_to_b_ast(rel,relations).

latex_to_b_ast(rhd,range_restriction).

latex_to_b_ast(rres,range_restriction).

latex_to_b_ast(rsub,range_subtraction).

latex_to_b_ast(srel,surjection_relation).

latex_to_b_ast(subseteq,subset).

latex_to_b_ast(subset,subset_strict).

latex_to_b_ast(tbij,total_bijection).

latex_to_b_ast(tfun,total_function).

latex_to_b_ast(tinj,total_injection).

latex_to_b_ast(trel,total_relation).

latex_to_b_ast(tsrel,total_surjection_relation).

latex_to_b_ast(tsur,total_surjection).

latex_to_b_ast(upto,interval).

latex_to_b_ast(vee,disjunct).

latex_to_b_ast(wedge,conjunct).

latex_to_b_ast('INT','INTEGER').

latex_to_b_ast('NAT','NATURAL').

latex_to_b_ast('N','NATURAL').

latex_to_b_ast('Pi',general_product).

latex_to_b_ast('POW',pow_subset).

latex_to_b_ast('REAL','REAL').

latex_to_b_ast('Rightarrow',implication).

latex_to_b_ast('Sigma',general_sum).

latex_to_b_ast('Leftrightarrow',equivalence).

latex_to_b_ast('Inter',quantified_intersection).

latex_to_b_ast('Union',quantified_union).

latex_to_b_ast('Z','INTEGER').

latex_to_unicode/2

latex_translation/2

latex_translation(empty_set, '\\emptyset ').

latex_translation(implication, '\\mathbin\\Rightarrow ').

latex_translation(conjunct,'\\wedge ').

latex_translation(disjunct,'\\vee ').

latex_translation(equivalence,'\\mathbin\\Leftrightarrow ').

latex_translation(negation,'\\neg ').

latex_translation(not_equal,'\\neq ').

latex_translation(less_equal,'\\leq ').

latex_translation(less_equal_real,'\\leq ').

latex_translation(greater_equal,'\\geq ').

latex_translation(member,'\\in ').

latex_translation(not_member,'\\not\\in ').

latex_translation(subset,'\\subseteq ').

latex_translation(subset_strict,'\\subset ').

latex_translation(not_subset,'\\not\\subseteq ').

latex_translation(not_subset_strict,'\\not\\subset ').

latex_translation(union,'\\cup ').

latex_translation(intersection,'\\cap ').

latex_translation(couple,'\\mapsto ').

latex_translation(cartesian_product,'\\times').

latex_translation(rec,'\\mathit{rec}').

latex_translation(struct,'\\mathit{struct}').

latex_translation(convert_bool,'\\mathit{bool}').

latex_translation(max,'\\mathit{max}').

latex_translation(max_real,'\\mathit{max}').

latex_translation(min,'\\mathit{min}').

latex_translation(min_real,'\\mathit{min}').

latex_translation(modulo,'\\mod ').

latex_translation(card,'\\mathit{card}').

latex_translation(successor,'\\mathit{succ}').

latex_translation(predecessor,'\\mathit{pred}').

latex_translation(domain,'\\mathit{dom}').

latex_translation(range,'\\mathit{ran}').

latex_translation(size,'\\mathit{size}').

latex_translation(first,'\\mathit{first}').

latex_translation(last,'\\mathit{last}').

latex_translation(front,'\\mathit{front}').

latex_translation(tail,'\\mathit{tail}').

latex_translation(rev,'\\mathit{rev}').

latex_translation(seq,'\\mathit{seq}').

latex_translation(seq1,'\\mathit{seq}_{1}').

latex_translation(perm,'\\mathit{perm}').

latex_translation(fin_subset,'\\mathit{FIN}').

latex_translation(fin1_subset,'\\mathit{FIN}_{1}').

latex_translation(first_projection,'\\mathit{prj}_{1}').

latex_translation(second_projection,'\\mathit{prj}_{2}').

latex_translation(pow_subset,'\\mathbb P\\hbox{}'). % POW \pow would require bsymb.sty

latex_translation(pow1_subset,'\\mathbb P_1'). % POW1 \pown would require bsymb.sty

latex_translation(concat,'\\stackrel{\\frown}{~}'). % was '\\hat{~}').

latex_translation(relations,'\\mathbin\\leftrightarrow'). % <->, \rel requires bsymb.sty

latex_translation(total_relation,'\\mathbin{\\leftarrow\\mkern-14mu\\leftrightarrow}'). % <<-> \trel requires bsymb.sty

latex_translation(total_surjection_relation,'\\mathbin{\\leftrightarrow\\mkern-14mu\\leftrightarrow}'). % <<->> \strel requires bsymb.sty

latex_translation(surjection_relation,'\\mathbin{\\leftrightarrow\\mkern-14mu\\rightarrow}'). % <->> \srel requires bsymb.sty

latex_translation(partial_function,'\\mathbin{\\mkern6mu\\mapstochar\\mkern-6mu\\rightarrow}'). % +-> \pfun requires bsymb.sty, but \mapstochar is not supported by Mathjax

latex_translation(partial_injection,'\\mathbin{\\mkern9mu\\mapstochar\\mkern-9mu\\rightarrowtail}'). % >+> \pinj requires bsymb.sty

latex_translation(partial_surjection,'\\mathbin{\\mkern6mu\\mapstochar\\mkern-6mu\\twoheadrightarrow}'). % >+> \psur requires bsymb.sty

latex_translation(total_function,'\\mathbin\\rightarrow'). % --> \tfun would require bsymb.sty

latex_translation(total_surjection,'\\mathbin\\twoheadrightarrow'). % -->> \tsur requires bsymb.sty

latex_translation(total_injection,'\\mathbin\\rightarrowtail'). % >-> \tinj requires bsymb.sty

latex_translation(total_bijection,'\\mathbin{\\rightarrowtail\\mkern-18mu\\twoheadrightarrow}'). % >->> \tbij requires bsymb.sty

latex_translation(domain_restriction,'\\mathbin\\lhd'). % <| domres requires bsymb.sty

latex_translation(range_restriction,'\\mathbin\\rhd'). % |> ranres requires bsymb.sty

latex_translation(domain_subtraction,'\\mathbin{\\lhd\\mkern-14mu-}'). % <<| domsub requires bsymb.sty

latex_translation(range_subtraction,'\\mathbin{\\rhd\\mkern-14mu-}'). % |>> ransub requires bsymb.sty

latex_translation(overwrite,'\\mathbin{\\lhd\\mkern-9mu-}'). % <+ \ovl requires bsymb.sty

latex_translation(ring,'\\circ '). % not tested

latex_translation(general_sum,'\\Sigma ').

latex_translation(general_product,'\\Pi ').

latex_translation(lambda,'\\lambda ').

latex_translation(quantified_union,'\\bigcup\\nolimits'). % \Union requires bsymb.sty

latex_translation(quantified_intersection,'\\bigcap\\nolimits'). % \Inter requires bsymb.sty

latex_translation(truth,'{\\color{olive} \\top}'). % requires \usepackage{xcolor} in Latex

latex_translation(falsity,'{\\color{red} \\bot}').

latex_translation(boolean_true,'{\\color{olive} \\mathit{TRUE}}').

latex_translation(boolean_false,'{\\color{red} \\mathit{FALSE}}').

latex_translation(pred_true,'{\\color{olive} \\mathit{TRUE}}').

latex_translation(pred_false,'{\\color{red} \\mathit{FALSE}}').

latex_translation(reverse,'^{-1}').

ldots-->/2

left_set_bracket-->/2

my_greek_latex_escape_atom/3

name_variables/3

nbp/3

nbp2/4

nbp2(E,Type,_Info,Indent) :- get_binary_connective(E,NewType,Ascii,LHS,RHS),!,
    inc_indent(NewType,Type,Indent,NIndent),
    print_bracket(Indent,NIndent,'('),
    nbp(LHS,NewType,NIndent),
    print_indent(NIndent),
    translate_in_mode(NewType,Ascii,Symbol), print(Symbol),nl,
    (is_associative(NewType) -> NewTypeR=NewType % no need for parentheses if same operator on right
    ; NewTypeR=right(NewType)),
    nbp(RHS,NewTypeR,NIndent),
    print_bracket(Indent,NIndent,')').

nbp2(lazy_let_pred(TID,LHS,RHS),Type,_Info,Indent) :-
    def_get_texpr_id(TID,ID),!,
    NewType=lazy_let_pred(TID),
    inc_indent(NewType,Type,Indent,NIndent),
    print_indent(Indent), format('LET ~w = (~n',[ID]),
    nbp(LHS,NewType,NIndent),
    print_indent(NIndent), print(') IN ('),nl,
    nbp(RHS,NewType,NIndent),
    print_indent(NIndent),print(')'),nl.

nbp2(negation(LHS),_Type,_Info,Indent) :- !,
    inc_indent(negation,false,Indent,NIndent),
    print_indent(Indent),
    translate_in_mode(negation,'not',Symbol), format('~s(~n',[Symbol]),
    nbp(LHS,negation,NIndent),
    print_indent(Indent), print(')'),nl.

nbp2(let_predicate(Ids,Exprs,Pred),_Type,_Info,Indent) :- !,
    inc_indent(let_predicate,false,Indent,NIndent),
    pp_expr_ids_in_mode(Ids,_LR,Codes,[]),
    print_indent(Indent),format('#~s.( /* LET */~n',[Codes]),
    pp_expr_let_pred_exprs(Ids,Exprs,_LimitReached,Codes2,[]),
    print_indent(Indent), format('~s~n',[Codes2]),
    print_indent(NIndent), print('&'),nl,
    nbp(Pred,let_predicate,NIndent),
    print_indent(Indent), print(')'),nl.

nbp2(exists(Ids,Pred),_Type,_Infos,Indent) :- !,
    inc_indent(exists,false,Indent,NIndent),
    pp_expr_ids_in_mode(Ids,_LR,Codes,[]),
    print_indent(Indent),
    %(member(allow_to_lift_exists,_Infos) -> write('/* LIFT */ ') ; true),
    exists_symbol(ExistsSymbol,[]), format('~s~s.(~n',[ExistsSymbol,Codes]),
    nbp(Pred,exists,NIndent),
    print_indent(Indent), print(')'),nl.

nbp2(forall(Ids,LHS,RHS),_Type,_Info,Indent) :- !,
    inc_indent(forall,false,Indent,NIndent),
    pp_expr_ids_in_mode(Ids,_LR,Codes,[]),
    print_indent(Indent),
    forall_symbol(ForallSymbol,[]), format('~s~s.(~n',[ForallSymbol,Codes]),
    nbp(LHS,forall,NIndent),
    print_indent(NIndent),
    translate_in_mode(implication,'=>',Symbol),print(Symbol),nl,
    nbp(RHS,forall,NIndent),
    print_indent(Indent), print(')'),nl.

nbp2(if_then_else(Test,LHS,RHS),_Type,_Info,Indent) :- !,
    inc_indent(if_then_else,false,Indent,NIndent),
    print_indent(Indent), print('IF'),nl,
    nbp(Test,if_then_else,NIndent),
    print_indent(Indent), print('THEN'),nl,
    nbp(LHS,if_then_else,NIndent),
    print_indent(Indent), print('ELSE'),nl,
    nbp(RHS,if_then_else,NIndent),
    print_indent(Indent), print('END'),nl.

nbp2(value(V),_,Info,Indent) :- !,
    print_indent(Indent), print_bexpr(b(value(V),any,Info)),nl.

nbp2(E,_,Info,Indent) :- print_indent(Indent), print_bexpr(b(E,pred,Info)),nl.

nested_print_bexpr/1

nested_print_bexpr2/2

nested_print_bexpr_as_classicalb/1

nested_print_bexpr_as_classicalb2/2

nested_print_sequent_as_classicalb/6

nested_print_sequent_as_classicalb_aux/6

nested_print_sequent_as_classicalb_aux(Stream,HypsList,Goal,AllHypsList,MchName,ProofInfos) :-
    conjunct_predicates(HypsList,HypsPred),
    conjunct_predicates([Goal|HypsList],Pred),
    get_global_identifiers(Ignored,ignore_promoted_constants), % the sets section below will not print the promoted enumerated set constants, they may also not be valid for the selected hyps only
    find_typed_identifier_uses(Pred, Ignored, TUsedIds),
    get_texpr_ids(TUsedIds,UsedIds),
    convert_and_ajoin_ids(UsedIds,AllIds),
    bmachine:get_full_b_machine(_Name,BMachine),
    include(relevant_section,BMachine,RelevantSections),
    % TO DO: we could filter out enumerate/deferred sets not occuring in Pred
    translate_section_list(RelevantSections,SetsParas),
    set_print_type_infos(all),
    datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
    format(Stream,'MACHINE ~w~n /* Exported: ~w/~w/~w ~w:~w */~n',[MchName,Day,Mon,Yr,Hr,Min]),
    (currently_opened_file(File), bmachine:b_machine_name(Name)
    -> format(Stream,' /* Origin: ~w : ~w */~n',[Name,File]) ; true),
    write(Stream,' /* '),format_prob_version(Stream), format(Stream,' */~n',[]),
    format(Stream,' /* Use static asssertion checking (probcli -cbc_assertions) to look for counter examples */~n',[]),
    maplist(format_proof_infos(Stream),ProofInfos),
    format(Stream,'~sCONSTANTS~n ~w~nPROPERTIES /* Selected Hypotheses: */~n',[SetsParas,AllIds]),
    add_typing_predicates(TUsedIds,HypsPred,HypsT),
    current_output(OldStream),
    set_output(Stream),
    nested_print_bexpr_as_classicalb2(HypsT,s(0)), % TODO: pass stream to this predicate
    format(Stream,'~nASSERTIONS /* Proof Goal: */~n',[]),
    nested_print_bexpr_as_classicalb2(Goal,s(0)), % TODO: pass stream to this predicate
    (AllHypsList = [] -> true
    ; sort(AllHypsList,SAL), sort(HypsList,SL),
    ord_subtract(SAL,SL,RemainingHypsList), % TODO: we could preserve order
    conjunct_predicates(RemainingHypsList,AllHypsPred),
    find_typed_identifier_uses(AllHypsPred, Ignored, TAllUsedIds),
    get_texpr_ids(TAllUsedIds,AllUsedIds),
    ord_subtract(AllUsedIds,UsedIds,NewIds), % compute new ids not used in selected hyps and goal
    (NewIds = []
    -> format(Stream,'OPERATIONS~n CheckRemainingHypotheses = SELECT~n',[])
    ; ajoin_with_sep(NewIds,', ',NIdLst),
    format(Stream,'OPERATIONS~n CheckRemainingHypotheses(~w) = SELECT~n',[NIdLst])
    ),
    nested_print_bexpr_as_classicalb2(AllHypsPred,s(0)), % TODO: pass stream to this predicate
    format(Stream,' THEN skip~n END /* CheckRemainingHypotheses */~n',[])
    ),
    set_output(OldStream),
    set_print_type_infos(none),
    format(Stream,'DEFINITIONS~n SET_PREF_DISPROVER_MODE == TRUE~n ; SET_PREF_TRY_FIND_ABORT == FALSE~n',[]),
    format(Stream,' ; SET_PREF_ALLOW_REALS == FALSE~n',[]),
    % The Rodin DisproverCommand.java usually enables CHR;
    % TODO: we could also look for options(List) in ProofInfos and check use_chr_solver/true in List, ...
    (get_preference(use_clpfd_solver,false) -> format(Stream,' ; SET_PREF_CHR == FALSE~n',[]) ; true),
    (get_preference(use_chr_solver,true) -> format(Stream,' ; SET_PREF_CHR == TRUE~n',[]) ; true),
    (get_preference(use_smt_mode,true) -> format(Stream,' ; SET_PREF_SMT == TRUE~n',[]) ; true),
    (get_preference(use_smt_mode,true) -> format(Stream,' ; SET_PREF_SMT == TRUE~n',[]) ; true),
    (get_preference(use_common_subexpression_elimination,true) -> format(Stream,' ; SET_PREF_CSE == TRUE~n',[]) ; true),
    (get_preference(smt_supported_interpreter,true) -> format(Stream,' ; SET_PREF_SMT_SUPPORTED_INTERPRETER == TRUE~n',[]) ; true),
    format(Stream,'END~n',[]).

non_det_modified_var/2

pp_all_disjoint_aux/5

pp_annotations/4

pp_any_state/4

pp_any_state_with_limit/4

pp_argument/3

pp_atom_indent/3

pp_atom_opt_latex/3

pp_atom_opt_latex_mathit/3

pp_atom_opt_latex_mathit(Name) --> {latex_mode},!,
{latex_escape_atom(Name,EscName)},
"\\mathit{",ppatom(EscName),"}".

pp_atom_opt_latex_mathit(Name) --> ppatom(Name).

Calls:

Name: ppatom/3	Module: translate
Name: =/2
Name: latex_escape_atom/2	Module: tools
Name: !
Name: latex_mode	dynamic predicate

Called:

Name: pp_expr2/5

Module: translate

pp_atom_opt_mathit/3

pp_atom_opt_mathit(EscName) --> {latex_mode},!,
% we assume already escaped
"\\mathit{",ppatom(EscName),"}".

pp_atom_opt_mathit(Name) --> ppatom(Name).

Calls:

Name: ppatom/3	Module: translate
Name: =/2
Name: !
Name: latex_mode	dynamic predicate

Called:

Name: pp_expr2/5

Module: translate

pp_b_context/3

pp_b_state/4

pp_b_state_comma_list/5

pp_b_state_list/4

pp_backquoted_id_codes/3

pp_backquoted_identifier/3

pp_begin_sequence-->/2

pp_bugly_composed_string/3

pp_bugly_composed_string_codes/4

pp_codes_opt_scramble/3

pp_colour_code/3

pp_comprehension_set/6

pp_comprehension_set5/7

pp_comprehension_set5([TID1,TID2,TID3],Body,_Info,LimitReached,special(Proj)) -->
    /* This comprehension set was a projection function (prj1/prj2) */
    % %(z_,z__).(z__ : NATURAL|z_) -> prj1(INTEGER,NATURAL)
    {get_texpr_id(TID1,ID1), % sometimes _zzzz_unary or _prj_arg1__
    get_texpr_id(TID2,ID2), % sometimes _zzzz_binary or _prj_arg2__
    get_texpr_id(TID3,LambdaID),
    get_lambda_equality(Body,LambdaID,RestBody,ResultExpr),
    get_texpr_id(ResultExpr,ResultID),
    (ResultID = ID1 -> Proj = prj1 ; ResultID = ID2, Proj = prj2),
    flatten_conjunctions(RestBody,Rest1),
    select_membership(Rest1,TID1,Rest2,Set1),
    select_membership(Rest2,TID2,[],Set2)},
    !,
    pp_prj12(Proj,Set1,Set2,LimitReached).

pp_comprehension_set5([ID1|T],Body,Info,LimitReached,special(disjunct)) --> {is_a_disjunct(Body,B1,B2),
    get_last(T,ID1,_FrontIDs,LastID),
    is_lambda_result_id(LastID,_Suffix)},!, % we seem to have the union of two lambda expressions
    "(", pp_comprehension_set([ID1|T],B1,Info,LimitReached),
    " \\/ ", pp_comprehension_set([ID1|T],B2,Info,LimitReached), ")".

pp_comprehension_set5([b(identifier('_pred_'),integer,_),
    b(identifier(LAMBDARES),integer,_)],Body,_,_,special(pred)) --> % '_lambda_result_'
    {Body = b(equal(LR,T),pred,_),
    LR = b(identifier(LAMBDARES),integer,_),
    T = b(minus(ARG,One),integer,_),
    get_integer(One,1),
    ARG = b(identifier('_pred_'),integer,_)},
    !,
    "pred".

pp_comprehension_set5([b(identifier('_succ_'),integer,_),
    b(identifier(LAMBDARES),integer,_)],Body,_,_,special(succ)) --> % '_lambda_result_'
    {Body = b(equal(LR,T),pred,_),
    LR = b(identifier(LAMBDARES),integer,_),
    T = b(add(ARG,One),integer,_),
    get_integer(One,1),
    ARG = b(identifier('_succ_'),integer,_)},
    !,
    "succ".

pp_comprehension_set5(Paras,Body,Info,LimitReached,special(lambda)) -->
    {detect_lambda_comprehension(Paras,Body, FrontIDs,LambdaBody,ToExpr)},
    !,
    {add_normal_typing_predicates(FrontIDs,LambdaBody,TLambdaBody)},
    ({eventb_translation_mode} -> "(" ; ""), % put brackets around the lambda in Rodin
    pp_annotations(Info,Body),
    lambda_symbol, % "%"
    pp_lambda_identifiers(FrontIDs,LimitReached),
    ".",
    ({eventb_translation_mode} -> {IPrio=30} ; {IPrio=11}, "("), % In Rodin it is not ok to write (P|E)
    pp_expr_m(TLambdaBody,IPrio,LimitReached), % Check 11 against prio of . and |
    pp_such_that_bar(ToExpr),
    pp_expr_m(ToExpr,IPrio,LimitReached),
    ")".

pp_comprehension_set5(TIds,Body,Info,LimitReached,special(event_b_comprehension_set)) -->
    % detect Event-B style set comprehensions and use bullet • or Event-B notation such as {x·x ∈ 1 ‥ 3|x * 10}
    % gets translated to {`__comp_result__`|∃x·(x ∈ 1 ‥ 3 ∧ `__comp_result__` = x * 10)}
    {is_eventb_comprehension_set(TIds,Body,Info,Ids,P1,EXPR)},!,
    pp_annotations(Info,P1),
    left_set_bracket,
    pp_expr_l_pair_in_mode(Ids,LimitReached),
    {add_normal_typing_predicates(Ids,P1,P)},
    dot_bullet_symbol,
    pp_expr_m(P,11,LimitReached),
    pp_such_that_bar(P),
    pp_expr_m(EXPR,11,LimitReached),
    right_set_bracket.

pp_comprehension_set5(Ids,P1,Info,LimitReached,normal) -->
    pp_annotations(Info,P1),
    left_set_bracket,
    pp_expr_l_pair_in_mode(Ids,LimitReached),
    {add_normal_typing_predicates(Ids,P1,P)},
    pp_such_that_bar(P),
    pp_expr_m(P,11,LimitReached),
    right_set_bracket.

pp_csp_process(skip(_Span),S,T) :- !, S=['SKIP'|T].

pp_csp_process(stop(_Span),S,T) :- !, S=['STOP'|T].

pp_csp_process('CHAOS'(_Span,Set),['CHAOS('|S],T) :- !,
    pp_csp_value(Set,S,[')'|T]).

pp_csp_process(val_of(Agent,_Span),S,T) :- !,
    pp_csp_value(Agent,S,T).

pp_csp_process(builtin_call(X),S,T) :- !,pp_csp_process(X,S,T).

pp_csp_process(agent(F,Body,_Span),S,T) :- !,
    F =.. [Agent|Parameters],
    pp_csp_value(Agent,S,S1),
    pp_csp_args(Parameters,S1,[' = '|S2],'(',')'),
    pp_csp_value(Body,S2,T).

pp_csp_process(agent_call(_Span,Agent,Parameters),S,T) :- !,
    pp_csp_value(Agent,S,S1),
    pp_csp_args(Parameters,S1,T,'(',')').

pp_csp_process(agent_call_curry(Agent,Parameters),S,T) :- !,
    pp_csp_value(Agent,S,S1),
    pp_csp_curry_args(Parameters,S1,T).

pp_csp_process(lambda(Parameters,Body),['\\ '|S],T) :- !,
    pp_csp_args(Parameters,S,[' @ '|S1],'',''),
    pp_csp_value(Body,S1,T).

pp_csp_process('\\'(B,C,S),S1,T) :- !, pp_csp_process(ehide(B,C,S),S1,T).

pp_csp_process(ehide(Body,ChList,_Span),['('|S],T) :- !,
    pp_csp_process(Body,S,[')\\('|S1]),
    pp_csp_value(ChList,S1,[')'|T]).

pp_csp_process(let(Decls,P),['let '| S],T) :- !,
    maplist(translate_cspm_state,Decls,Texts),
    ajoin_with_sep(Texts,' ',Text),
    S=[Text,' within '|S1],
    pp_csp_process(P,S1,T).

pp_csp_process(Expr,['('|S],T) :- binary_csp_op(Expr,X,Y,Op),!,
    pp_csp_process(X,S,[') ',Op,' ('|S1]),
    pp_csp_process(Y,S1,[')'|T]).

pp_csp_process(Expr,S,T) :- sharing_csp_op(Expr,X,Middle,Y,Op1,Op2),!,
    pp_csp_process(X,S,[Op1|S1]),
    pp_csp_value(Middle,S1,[Op2|S2]),
    pp_csp_process(Y,S2,T).

pp_csp_process(Expr,S,T) :- asharing_csp_op(Expr,X,MiddleX,MiddleY,Y,Op1,MOp,Op2),!,
    pp_csp_process(X,S,[Op1|S1]),
    pp_csp_value(MiddleX,S1,[MOp|S2]),
    pp_csp_value(MiddleY,S2,[Op2|S3]),
    pp_csp_process(Y,S3,T).

pp_csp_process(Expr,S,T) :- renaming_csp_op(Expr,X,RList,Op1,Op2),!,
    pp_csp_process(X,S,[Op1|S1]),
    pp_csp_value_l(RList,',',S1,[Op2|T],10).

pp_csp_process(prefix(_SPAN1,Values,ChannelExpr,CSP,_SPAN2),S,T) :- !,
    pp_csp_value_l([ChannelExpr|Values],'',S,['->'|S2],20),
    pp_csp_process(CSP,S2,T).

pp_csp_process('&'(Test,Then),S,T) :- !,
    pp_csp_bool_expr(Test,S,['&'|S2]),
    pp_csp_process(Then,S2,T).

pp_csp_process(ifte(Test,Then,Else,_SPAN1,_SPAN2,_SPAN3),[' if '|S],T) :- !,
    pp_csp_bool_expr(Test,S,[' then '|S2]),
    pp_csp_process(Then,S2,[' else '|S3]),
    pp_csp_process(Else,S3,T).

pp_csp_process(head(A),[head,'('|S],T) :- !, pp_csp_process(A,S,[')'|T]).

pp_csp_process(X,[X|T],T).

pp_csp_value/3

pp_csp_value(X,[A|S],S) :- pp_single_csp_value(X,A),!.

pp_csp_value(setValue(L),['{'|S],T) :- !,pp_csp_value_l(L,',',S,['}'|T],inf).

pp_csp_value(setExp(rangeEnum(L)),['{'|S],T) :- !,pp_csp_value_l(L,',',S,['}'|T],inf).

pp_csp_value(setExp(rangeEnum(L),Gen),['{'|S],T) :- !,
    copy_term((L,Gen),(L2,Gen2)), numbervars((L2,Gen2),1,_),
    pp_csp_value_l(L2,',',S,['|'|S2],inf),
    pp_csp_value_l(Gen2,',',S2,['}'|T],inf).

pp_csp_value(avl_set(A),['{'|S],T) :- !, check_is_non_empty_avl(A),
    avl_domain(A,L),pp_csp_value_l(L,',',S,['}'|T],inf).

pp_csp_value(setExp(rangeClosed(L,U)),['{'|S],T) :- !, pp_csp_value(L,S,['..'|S2]),pp_csp_value(U,S2,['}'|T]).

pp_csp_value(setExp(rangeOpen(L)),['{'|S],T) :- !, pp_csp_value(L,S,['..}'|T]).

pp_csp_value(comprehensionGenerator(Var,Body),S,T) :- !, pp_csp_value(Var,S,['<-'|S1]),
    pp_csp_value(Body,S1,T).

pp_csp_value(listExp(rangeEnum(L)),['<'|S],T) :- !,pp_csp_value_l(L,',',S,['>'|T],inf).

pp_csp_value(listExp(rangeClosed(L,U)),['<'|S],T) :- !, pp_csp_value(L,S,['..'|S2]),pp_csp_value(U,S2,['>'|T]).

pp_csp_value(listExp(rangeOpen(L)),['<'|S],T) :- !, pp_csp_value(L,S,['..>'|T]).

pp_csp_value(setFromTo(L,U),['{'|S],T) :- !,
    pp_csp_value(L,S,['..'|S2]),pp_csp_value(U,S2,['}'|T]).

pp_csp_value(setFrom(L),['{'|S],T) :- !,
    pp_csp_value(L,S,['..}'|T]).

pp_csp_value(closure(L), ['{|'|S],T) :- !,pp_csp_value_l(L,',',S,['|}'|T],inf).

pp_csp_value(list(L),['<'|S],T) :- !,pp_csp_value_l(L,',',S,['>'|T],inf).

pp_csp_value(listFromTo(L,U),['<'|S],T) :- !,
    pp_csp_value(L,S,['..'|S2]),pp_csp_value(U,S2,['>'|T]).

pp_csp_value(listFrom(L),['<'|S],T) :- !,
    pp_csp_value(L,S,['..>'|T]).

pp_csp_value('#'(L),['#'|S],T) :- !,pp_csp_value(L,S,T).

pp_csp_value('^'(X,Y),S,T) :- !,pp_csp_value(X,S,['^'|S1]), pp_csp_value(Y,S1,T).

pp_csp_value(linkList(L),S,T) :- !,pp_csp_value_l(L,',',S,T,inf).

pp_csp_value(in(X),['?'|S],T) :- !,pp_csp_value(X,S,T).

pp_csp_value(inGuard(X,Set),['?'|S],T) :- !,pp_csp_value(X,S,[':'|S1]),
    pp_csp_value(Set,S1,T).

pp_csp_value(out(X),['!'|S],T) :- !,pp_csp_value(X,S,T).

pp_csp_value(alsoPat(X,_Y),S,T) :- !,pp_csp_value(X,S,T).

pp_csp_value(appendPat(X,_Fun),S,T) :- !,pp_csp_value(X,S,T).

pp_csp_value(tuple(vclosure),S,T) :- !, S=T.

pp_csp_value(tuple([X]),S,T) :- !,pp_csp_value_in(X,S,T).

pp_csp_value(tuple([X|vclosure]),S,T) :- !,pp_csp_value_in(X,S,T).

pp_csp_value(tuple([H|TT]),S,T) :- !,pp_csp_value_in(H,S,['.'|S1]),pp_csp_value(tuple(TT),S1,T).

pp_csp_value(dotTuple([]),['unit_channel'|S],S) :- ! .

pp_csp_value(dotTuple([H]),S,T) :- !, pp_csp_value_in(H,S,T).

pp_csp_value(dotTuple([H|TT]),S,T) :- !, pp_csp_value_in(H,S,['.'|S1]),
    pp_csp_value(dotTuple(TT),S1,T).

pp_csp_value(tupleExp(Args),S,T) :- !,pp_csp_args(Args,S,T,'(',')').

pp_csp_value(na_tuple(Args),S,T) :- !,pp_csp_args(Args,S,T,'(',')').

pp_csp_value(record(Name,Args),['('|S],T) :- !,pp_csp_value(tuple([Name|Args]),S,[')'|T]).

pp_csp_value(val_of(Name,_Span),S,T) :- !, pp_csp_value(Name,S,T).

pp_csp_value(builtin_call(X),S,T) :- !,pp_csp_value(X,S,T).

pp_csp_value(seq_to_set(X),['set('|S],T) :- !,pp_csp_value(X,S,[')'|T]).

pp_csp_value(set_to_seq(X),['seq('|S],T) :- !,pp_csp_value(X,S,[')'|T]).

pp_csp_value(agent_call(_Span,Agent,Parameters),['('|S],T) :- !,
    pp_csp_value(Agent,S,S1),
    pp_csp_args(Parameters,S1,[')'|T],'(',')').

pp_csp_value(agent_call_curry(Agent,Parameters),S,T) :- !,
    pp_csp_value(Agent,S,S1),
    pp_csp_curry_args(Parameters,S1,T).

pp_csp_value(lambda(Parameters,Body),['\\ '|S],T) :- !,
    pp_csp_args(Parameters,S,[' @ '|S1],'',''),
    pp_csp_value(Body,S1,T).

pp_csp_value(rename(X,Y),S,T) :- !,pp_csp_value(X,S,[' <- '|S1]),
    pp_csp_value(Y,S1,T).

pp_csp_value(link(X,Y),S,T) :- !,pp_csp_value(X,S,[' <-> '|S1]),
    pp_csp_value(Y,S1,T).

pp_csp_value(Expr,['('|S],T) :- bynary_numeric_operation(Expr,E1,E2,OP),!,
    pp_csp_value(E1,S,[OP|S2]),
    pp_csp_value(E2,S2,[')'|T]).

pp_csp_value(empty(A),[empty,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).

pp_csp_value(card(A),[card,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).

pp_csp_value('Set'(A),['Set','('|S],T) :- !, pp_csp_value(A,S,[')'|T]).

pp_csp_value('Inter'(A1),['Inter','('|S],T) :- !,pp_csp_value(A1,S,[')'|T]).

pp_csp_value('Union'(A1),['Union','('|S],T) :- !,pp_csp_value(A1,S,[')'|T]).

pp_csp_value(diff(A1,A2),[diff,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').

pp_csp_value(inter(A1,A2),[inter,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').

pp_csp_value(union(A1,A2),[union,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').

pp_csp_value(member(A1,A2),[member,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').

pp_csp_value(null(A),[null,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).

pp_csp_value(length(A),[length,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).

pp_csp_value(head(A),[head,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).

pp_csp_value(tail(A),[tail,'('|S],T) :- !, pp_csp_value(A,S,[')'|T]).

pp_csp_value(elem(A1,A2),[elem,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').

pp_csp_value(concat(A1,A2),[concat,'('|S],T) :- !,pp_csp_args([A1,A2],S,[')'|T],'','').

pp_csp_value('Seq'(A),['Seq','('|S],T) :- !, pp_csp_value(A,S,[')'|T]).

pp_csp_value(Expr,S,T) :- is_list(Expr),!,pp_csp_value(closure(Expr),S,T).

pp_csp_value(dotTupleType([H]),S,T) :- !, pp_csp_value_in(H,S,T).

pp_csp_value(dotTupleType([H|TT]),S,T) :- !,pp_csp_value_in(H,S,['.'|S1]), pp_csp_value(dotTupleType(TT),S1,T).

pp_csp_value(typeTuple(Args),S,T) :- !, pp_csp_args(Args,S,T,'(',')').

pp_csp_value(dataType(T),[T|S],S) :- ! .

pp_csp_value(boolType,['Bool'|S],S) :- ! .

pp_csp_value(intType,['Int'|S],S) :- ! .

pp_csp_value(dataTypeDef([H]),S,T) :- !, pp_csp_value(H,S,T).

pp_csp_value(dataTypeDef([H|TT]),S,T) :- !, pp_csp_value(H,S,['|'|S1]),
    pp_csp_value(dataTypeDef(TT),S1,T).

pp_csp_value(constructor(Name),[Name|S],S) :- ! .

pp_csp_value(constructorC(C,Type),[C,'('|S],T) :- !, pp_csp_value(Type,S,[')'|T]).

pp_csp_value(Expr,S,T) :- pp_csp_process(Expr,S,T),!. % pp_csp_process has a catch-all !!! TO DO: look at this

pp_csp_value(Expr,S,T) :- csp_with_bz_mode,!,pp_value(Expr,S,T).

pp_csp_value(X, [A|S], S) :- % ['<< ',A,' >>'|S],S) :- % the << >> pose problems when checking against FDR
    write_to_codes(X,Codes),atom_codes_with_limit(A,Codes).

pp_csp_value_in/3

pp_csp_value_l/5

pp_csp_value_l1/2

pp_cur_context_state-->/2

pp_current_state-->/2

pp_description_pragma_of/3

pp_disjoint/5

pp_empty_sequence-->/2

pp_end_label_pragma-->/2

pp_end_sequence-->/2

pp_event_b_comprehension_set/6

pp_eventb_direct_definition_header/4

pp_eventb_operator_args/3

pp_expr1(Expr,_,_,Prio,_) --> {var(Expr)},!,"_",{Prio=500}.

pp_expr1(event_b_comprehension_set(Ids,E,P),Type,_Info,Prio,LimitReached) -->
    {b_ast_cleanup:rewrite_event_b_comprehension_set(Ids,E,P,Type, NewExpression)},!,
    pp_expr(NewExpression,Prio,LimitReached).

pp_expr1(union(b(event_b_identity,Type,_), b(closure(Rel),Type,_)),_,Info,500,LimitReached) -->
    /* closure(Rel) = id \/ closure1(Rel) */
    {member_in_info(was(reflexive_closure),Info)},!,
    "closure(",pp_expr(Rel,_,LimitReached),")".

pp_expr1(comprehension_set([_],_),_,Info,500,_LimitReached) -->
    {memberchk_in_info(freetype(P),Info),!},ppatom(P).

pp_expr1(greater_equal(A,Y),Type,Info,Prio,LimitReached) --> % x:NATURAL was rewritten to x>=0, see test 499, 498
    {memberchk_in_info(was(member(A,B)),Info), get_integer(Y,_)},
    pp_expr1(member(A,B),Type,Info,Prio,LimitReached).

pp_expr1(comprehension_set([TID],b(B,_,_)),Type,Info,Prio,LimitReached) -->
    {memberchk_in_info(was(integer_set(S)),Info)},
    {S='INTEGER' -> B=truth
    ; get_texpr_id(TID,ID),
    B=greater_equal(TID2,Y), get_integer(Y,I),
    get_texpr_id(TID2,ID),
    (I=0 -> S='NATURAL' ; I=1,S='NATURAL1')}, % TO DO: check bounds
    !,
    pp_expr1(integer_set(S),Type,Info,Prio,LimitReached).

pp_expr1(interval(b(A,_,_),B),Type,Info,Prio,LimitReached) -->
    {memberchk_in_info(was(integer_set(S)),Info)},
    {B=b(max_int,integer,_)}, % TO DO ? allow value(int(Mx))
    {A=min_int -> S='INT' ; A=integer(0) -> S='NAT' ; A=integer(1),S='NAT1'},
    !,
    pp_expr1(integer_set(S),Type,Info,Prio,LimitReached).

pp_expr1(falsity,_,Info,Prio,LimitReached) --> {memberchk_in_info(was(Pred),Info)},!,
    ({(unicode_mode ; latex_mode)}
    -> {translate_in_mode(falsity,'falsity',Symbol)},
    ppatom(Symbol),
    ({get_preference(pp_propositional_logic_mode,true)} -> {true}
    ; " ", enter_comment, " ", pp_expr2(Pred,Prio,LimitReached), " ", exit_comment)
    ; enter_comment, " falsity ",exit_comment, " ",
    pp_expr2(Pred,Prio,LimitReached)). % Pred is not wrapped

pp_expr1(truth,_,Info,Prio,LimitReached) --> {memberchk_in_info(was(Pred),Info)},!,
    ({(unicode_mode ; latex_mode)}
    -> {translate_in_mode(truth,'truth',Symbol)},
    ppatom(Symbol),
    ({get_preference(pp_propositional_logic_mode,true)} -> {true}
    ; " ",enter_comment, " ", pp_expr2(Pred,Prio,LimitReached), " ", exit_comment)
    ; enter_comment, " truth ", exit_comment, " ",
    pp_expr2(Pred,Prio,LimitReached)). % Pred is not wrapped

pp_expr1(event_b_identity,Type,_Info,500,_LimitReached) -->
    {\+ eventb_translation_mode}, %{atelierb_mode(Mode), Mode == pp},
    {is_set_type(Type,couple(ElType,ElType))},
    !,
    "id(", {pretty_normalized_type(ElType,S)},ppatom(S), ")".

pp_expr1(typeset,SType,_Info,500,_LimitReached) --> % normally removed by ast_cleanup
    {is_set_type(SType,Type)},
    !,
    "(", {pretty_normalized_type(Type,S)},ppatom(S), ")".

pp_expr1(Expr,Type,Info,Prio,LimitReached) --> {member_in_info(sharing(ID,Count,_,_),Info),number(Count),Count>1},!,
    "( ",enter_comment," CSE ",ppnumber(ID), ":#", ppnumber(Count),
    ({member_in_info(negated_cse,Info)} -> " (neg) " ; " "),
    ({member_in_info(contains_wd_condition,Info)} -> " (wd) " ; " "),
    exit_comment, " ",
    {delete(Info,sharing(_,_,_,_),Info2)},
    pp_expr1(Expr,Type,Info2,Prio,LimitReached), ")".

pp_expr1(value(V),Type,_,Prio,LimitReached) --> !,
    {(nonvar(V),V=closure(_,_,_) -> Prio=300 ; Prio=500)}, pp_value_with_type(V,Type,LimitReached).

pp_expr1(comprehension_set(Ids,P1),_,Info,500,LimitReached) --> !,
    pp_comprehension_set(Ids,P1,Info,LimitReached).

pp_expr1(first_of_pair(X),_,Info,500,LimitReached) --> {was_eventb_destructor(Info,X,Op,Arg)},!,
    ppatom(Op), "(",pp_expr(Arg,_,LimitReached), ")".

pp_expr1(second_of_pair(X),_,Info,500,LimitReached) --> {was_eventb_destructor(Info,X,Op,Arg)},!,
    ppatom(Op), "(",pp_expr(Arg,_,LimitReached), ")".

pp_expr1(Expr,_,_Info,Prio,LimitReached) --> pp_expr2(Expr,Prio,LimitReached).

pp_expr2/5

pp_expr2(Expr,_,_LimitReached) --> {var(Expr)},!,"_".

pp_expr2(_,_,LimitReached) --> {LimitReached==limit_reached},!,"...".

pp_expr2(atom_string(V),500,_) --> !,pp_atom_opt_latex_mathit(V). % hardwired_atom

pp_expr2(global_set(V),500,_) --> !, pp_identifier(V).

pp_expr2(freetype_set(V),500,_) --> !,{pretty_freetype(V,P)},ppatom_opt_scramble(P).

pp_expr2(lazy_lookup_expr(I),500,_) --> !, pp_identifier(I).

pp_expr2(lazy_lookup_pred(I),500,_) --> !, pp_identifier(I).

pp_expr2(identifier(I),500,_) --> !,
    {( I=op(Id) -> true; I=Id)},
    ( {atomic(Id)} -> ({translated_identifier(Id,TId)},
    ({latex_mode} -> ppatom(TId) ; pp_identifier(TId)))
    ;
    "'",ppterm(Id), "'").

pp_expr2(integer(N),500,_) --> !, ppnumber(N).

pp_expr2(real(N),500,_) --> !, ppatom(N).

pp_expr2(integer_set(S),500,_) --> !,
    {integer_set_mapping(S,T)},ppatom(T).

pp_expr2(string(S),500,_) --> !, string_start_symbol, ppstring_opt_scramble(S), string_end_symbol.

pp_expr2(set_extension(Ext),500,LimitReached) --> !, {set_brackets(L,R)},
    pp_expr_wrap_l(L,Ext,R,LimitReached).

pp_expr2(sequence_extension(Ext),500,LimitReached) --> !,
    pp_begin_sequence,
    ({get_preference(translate_print_cs_style_sequences,true)} -> pp_expr_l_sep(Ext,"",LimitReached)
    ; pp_expr_l_sep(Ext,",",LimitReached)),
    pp_end_sequence.

pp_expr2(assign(LHS,RHS),10,LimitReached) --> !,
    pp_expr_wrap_l(',',LHS,'',LimitReached), ":=", pp_expr_wrap_l(',',RHS,'',LimitReached).

pp_expr2(assign_single_id(LHS,RHS),10,LimitReached) --> !, pp_expr2(assign([LHS],[RHS]),10,LimitReached).

pp_expr2(parallel(RHS),10,LimitReached) --> !,
    pp_expr_wrap_l('||',RHS,'',LimitReached).

pp_expr2(sequence(RHS),10,LimitReached) --> !,
    pp_expr_wrap_l(';',RHS,'',LimitReached).

pp_expr2(event_b_comprehension_set(Ids,E,P1),500,LimitReached) --> !, % normally conversion above should trigger; this is if we call pp_expr for untyped expressions
    pp_event_b_comprehension_set(Ids,E,P1,LimitReached).

pp_expr2(recursive_let(Id,S),500,LimitReached) --> !,
    ({eventb_translation_mode} -> "" % otherwise we get strange characters in Rodin
    ; enter_comment," recursive ID ", pp_expr(Id,_,LimitReached), " ", exit_comment),
    pp_expr(S,_,LimitReached).

pp_expr2(image(A,B),300,LimitReached) --> !,
    pp_expr_m(A,249,LimitReached),"[", % was 0; but we may have to bracket A; e.g., f <| {2} [{2}] is not ok; 250 is priority of lambda
    pp_expr_m(B,0,LimitReached),"]". % was 500, now set to 0: we never need an outer pair of () !?

pp_expr2(function(A,B),300,LimitReached) --> !,
    pp_expr_m(A,249,LimitReached), % was 0; but we may have to bracket A; e.g., f <| {2} (2) is not ok; 250 is priority of lambda
    pp_function_left_bracket,
    pp_expr_m(B,0,LimitReached), % was 500, now set to 0: we never need an outer pair of () !?
    pp_function_right_bracket.

pp_expr2(definition(A,B),300,LimitReached) --> !, % definition call; usually inlined,...
    ppatom(A),
    pp_function_left_bracket,
    pp_expr_l_sep(B,",",LimitReached),
    pp_function_right_bracket.

pp_expr2(operation_call_in_expr(A,B),300,LimitReached) --> !,
    pp_expr_m(A,249,LimitReached),
    pp_function_left_bracket,
    pp_expr_l_sep(B,",",LimitReached),
    pp_function_right_bracket.

pp_expr2(enumerated_set_def(GS,ListEls),200,LimitReached) --> !, % for pretty printing enumerate set defs
    {reverse(ListEls,RLE)}, /* they have been inserted in inverse order */
    pp_identifier(GS), "=", pp_expr_wrap_l('{',RLE,'}',LimitReached).

pp_expr2(forall(Ids,D1,P),Prio,LimitReached) --> !,
    ({eventb_translation_mode} -> {Prio=60} ; {Prio=250}), % in Rodin forall/exists cannot be mixed with &, or, <=>, ...
    forall_symbol,pp_expr_ids_in_mode(Ids,LimitReached),
    {add_normal_typing_predicates(Ids,D1,D)},
    dot_symbol,pp_expr_m(b(implication(D,P),pred,[]),221,LimitReached).

pp_expr2(exists(Ids,P1),Prio,LimitReached) --> !,
    ({eventb_translation_mode} -> {Prio=60} ; {Prio=250}), % exists has Prio 250, but dot has 220
    exists_symbol,pp_expr_ids_in_mode(Ids,LimitReached),
    {add_normal_typing_predicates(Ids,P1,P)},
    dot_symbol,
    ({eventb_translation_mode} -> {MinPrio=29} ; {MinPrio=500}),
    % used to be 221, but #x.x>7 or #x.not(...) are not parsed by Atelier-B or ProB, x.x and x.not are parsed as composed identifiers
    % In Event-B ∃y·y>x ∧ (y=x+1 ∨ y=x+2) is valid and requires no outer parenthesis
    pp_expr_m(P,MinPrio,LimitReached).

pp_expr2(record_field(R,I),250,LimitReached) --> !,
    pp_expr_m(R,251,LimitReached),"'",pp_identifier(I).

pp_expr2(rec(Fields),500,LimitReached) --> !,
    {function_like_in_mode(rec,Symbol)},
    ppatom(Symbol), "(",pp_expr_fields(Fields,LimitReached),")".

pp_expr2(struct(Rec),500,LimitReached) -->
    {get_texpr_expr(Rec,rec(Fields)),Val=false ; get_texpr_expr(Rec,value(rec(Fields)))},!,
    {function_like_in_mode(struct,Symbol)},
    ppatom(Symbol), "(",
    ({Val==false} -> pp_expr_fields(Fields,LimitReached)
    ; pp_value_l(Fields,',',LimitReached)),
    ")".

pp_expr2(freetype_case(FT,L,Expr),500,LimitReached) --> !,
    pp_freetype_term('__is_ft_case',FT,L,Expr,LimitReached).

pp_expr2(freetype_constructor(_FT,L,Expr),500,LimitReached) --> !,
    ppatom_opt_scramble(L),ppatom('('),pp_expr(Expr,_,LimitReached),ppatom(')').

pp_expr2(freetype_destructor(FT,Case,Expr),500,LimitReached) --> !,
    ({unicode_mode}
    -> {unicode_translation(reverse,PowMinus1Symbol)},
    ppatom(Case),ppatom(PowMinus1Symbol), % Note: we do not print the freetype's name FT
    "(",pp_expr_m(Expr,0,LimitReached),")"
    ; pp_freetype_term('__ft~',FT,Case,Expr,LimitReached) % TODO: maybe find better print
).

pp_expr2(let_predicate(Ids,Exprs,P),1,LimitReached) --> !,
    pp_expr_let_exists(Ids,Exprs,P,LimitReached). % instead of pp_expr_let

pp_expr2(let_expression(Ids,Exprs,P),1,LimitReached) --> !,
    pp_expr_let(Ids,Exprs,P,LimitReached).

pp_expr2(let_expression_global(Ids,Exprs,P),1,LimitReached) --> !, " /", "* global *", "/ ",
    pp_expr_let(Ids,Exprs,P,LimitReached).

pp_expr2(lazy_let_pred(Id,Expr,P),Pr,LimitReached) --> !, pp_expr2(lazy_let_expr(Id,Expr,P),Pr,LimitReached).

pp_expr2(lazy_let_subst(Id,Expr,P),Pr,LimitReached) --> !, pp_expr2(lazy_let_expr(Id,Expr,P),Pr,LimitReached).

pp_expr2(lazy_let_expr(Id,Expr,P),1,LimitReached) --> !,
    pp_expr_let([Id],[Expr],P,LimitReached).

pp_expr2(norm_conjunct(Cond,[]),1,LimitReached) --> !, % norm_conjunct: flattened version generated by b_interpreter_check,...
    "( ",pp_expr(Cond,_,LimitReached), ")".

pp_expr2(norm_conjunct(Cond,[H|T]),1,LimitReached) --> !,
    "( ",pp_expr(Cond,_,LimitReached), ") ", and_symbol, " (", pp_expr2(norm_conjunct(H,T),_,LimitReached), ")".

pp_expr2(assertion_expression(Cond,Msg,Expr),1,LimitReached) --> !,
    " ASSERT_EXPR (",
    pp_expr_m(b(convert_bool(Cond),pred,[]),30,LimitReached), ",",
    pp_expr_m(string(Msg),30,LimitReached), ",",
    pp_expr_m(Expr,30,LimitReached),
    " )".

pp_expr2(partition(S,Elems),500,LimitReached) -->
    {eventb_translation_mode ;
    \+ atelierb_mode(_), length(Elems,Len), Len>50 % we need to print a quadratic number of disjoints
    },!,
    "partition(",pp_expr(S,_,LimitReached),
    ({Elems=[]} -> ")" ; pp_expr_wrap_l(',',Elems,')',LimitReached)).

pp_expr2(partition(S,Elems),500,LimitReached) --> !,
    "(",pp_expr(S,_,LimitReached), " = ",
    ({Elems=[]} -> "{})"
    ; pp_expr_l_sep(Elems,"\\/",LimitReached), pp_all_disjoint(Elems,LimitReached),")").

pp_expr2(finite(S),Prio,LimitReached) --> {\+ eventb_translation_mode}, %{atelierb_mode(_)},
    !,
    pp_expr2(member(S,b(fin_subset(S),set(any),[])),Prio,LimitReached).

pp_expr2(if_then_else(If,Then,Else),1,LimitReached) --> {animation_minor_mode(z)},!,
    "\\IF ",pp_expr_m(If,30,LimitReached),
    " \\THEN ",pp_expr_m(Then,30,LimitReached),
    " \\ELSE ",pp_expr_m(Else,30,LimitReached).

pp_expr2(if_then_else(If,Then,Else),Prio,LimitReached) --> {atelierb_mode(_)},!,
    % print IF-THEN-ELSE using a translation that Atelier-B can understand:
    {rewrite_if_then_else_expr_to_b(if_then_else(If,Then,Else), NExpr),
    get_texpr_type(Then,Type),
    NAst = b(NExpr,Type,[])},
    % construct {d,x| If => x=Then & not(if) => x=Else}(TRUE)
    pp_expr(NAst,Prio,LimitReached).

pp_expr2(if_then_else(If,Then,Else),1,LimitReached) --> !,
    pp_atom_opt_mathit('IF'),pp_space, % "IF ",
    pp_expr_m(If,30,LimitReached),
    pp_space, pp_atom_opt_mathit('THEN'),pp_space, " THEN ",
    pp_expr_m(Then,30,LimitReached),
    pp_space, pp_atom_opt_mathit('ELSE'),pp_space, " ELSE ",
    pp_expr_m(Else,30,LimitReached),
    pp_space, pp_atom_opt_mathit('END'). " END"

pp_expr2(kodkod(Id,Identifiers),300,LimitReached) --> !,
    "KODKOD_CALL(",ppnumber(Id),": ",pp_expr_ids(Identifiers,LimitReached),")".

pp_expr2(Expr,500,_) -->
    {constants_in_mode(Expr,Symbol)},!,ppatom(Symbol).

pp_expr2(equal(A,B),Prio,LimitReached) -->
    {get_preference(pp_propositional_logic_mode,true), % a mode for printing propositional logic formuli
    is_boolean_value(B,BV),
    get_texpr_id(A,_)},!,
    ({BV=pred_true} -> pp_expr(A,Prio,LimitReached)
    ; pp_expr2(negation(b(equal(A,b(boolean_true,boolean,[])),pred,[])),Prio,LimitReached)).

pp_expr2(Expr,Prio,LimitReached) -->
    {functor(Expr,F,1),
    unary_prefix(F,Symbol,Prio),!,
    arg(1,Expr,Arg),APrio is Prio+1},
    ppatom(Symbol), " ",
    pp_expr_m(Arg,APrio,LimitReached).

pp_expr2(Expr,500,LimitReached) -->
    {functor(Expr,F,1),
    unary_prefix_parentheses(F,Symbol),!,
    arg(1,Expr,Arg)},
    pp_atom_opt_latex(Symbol), "(", pp_expr(Arg,_,LimitReached), ")".

pp_expr2(Expr,Prio,LimitReached) -->
    {functor(Expr,F,1),
    unary_postfix_in_mode(F,Symbol,Prio),!,
    arg(1,Expr,Arg),APrio is Prio+1},
    pp_expr_m(Arg,APrio,LimitReached),ppatom(Symbol).

pp_expr2(power_of(Left,Right),Prio,LimitReached) --> {latex_mode},!, % special case, as we need to put {} around RHS
    {Prio=200, LPrio is Prio+1, RPrio = Prio},
    pp_expr_m(Left,LPrio,LimitReached),
    "^{",
    pp_expr_m(Right,RPrio,LimitReached),
    "}".

pp_expr2(power_of_real(Left,Right),Prio,LimitReached) --> !,
    ({get_texpr_expr(Right,convert_real(RI))}
    -> pp_expr2(power_of(Left,RI),Prio,LimitReached) % the Atelier-B power_of expects integer exponent
    ; pp_external_call('RPOW',[Left,Right],expression,Prio,LimitReached)
).

pp_expr2(Expr,OPrio,LimitReached) -->
    {functor(Expr,F,2),
    binary_infix_in_mode(F,Symbol,Prio,Ass),!,
    arg(1,Expr,Left),
    arg(2,Expr,Right),
    ( Ass = left, binary_infix_symbol(Left,Symbol) -> LPrio is Prio-1, RPrio is Prio+1
    ; Ass = right, binary_infix_symbol(Right,Symbol) -> LPrio is Prio+1, RPrio is Prio-1
    ; LPrio is Prio+1, RPrio is Prio+1)},
    % Note: Prio+1 is actually not necessary, Prio would be sufficient, as pp_expr_m uses a strict comparison <
    ({always_surround_by_parentheses(F)} -> "(",{OPrio=1000} ; {OPrio=Prio}),
    pp_expr_m(Left,LPrio,LimitReached),
    " ", ppatom(Symbol), " ",
    pp_expr_m(Right,RPrio,LimitReached),
    ({always_surround_by_parentheses(F)} -> ")" ; []).

pp_expr2(first_of_pair(X),500,LimitReached) --> {get_texpr_type(X,couple(From,To))},!,
    "prj1(", % TO DO: Latex version
    ({\+ atelierb_mode(_)} % eventb_translation_mode
    -> "" % no need to print types in Event-B or with new parser;
    % TODO: also with new parser no longer required; only print in Atelier-B mode
    ; {pretty_normalized_type(From,FromT),
    pretty_normalized_type(To,ToT)},
    pp_atom_opt_latex(FromT), ",", pp_atom_opt_latex(ToT),
    ")("
    ),
    pp_expr(X,_,LimitReached),")".

pp_expr2(second_of_pair(X),500,LimitReached) --> {get_texpr_type(X,couple(From,To))},!,
    "prj2(", % TO DO: Latex version
    ({\+ atelierb_mode(_)} -> "" % no need to print types in Event-B or with new parser
    ; {pretty_normalized_type(From,FromT),
    pretty_normalized_type(To,ToT)},
    pp_atom_opt_latex(FromT), ",", pp_atom_opt_latex(ToT),
    ")("
    ),
    pp_expr(X,_,LimitReached),")".

pp_expr2(Call,Prio,LimitReached) --> {external_call(Call,Kind,Symbol,Args)},!,
    pp_external_call(Symbol,Args,Kind,Prio,LimitReached).

pp_expr2(card(A),500,LimitReached) --> {latex_mode, get_preference(latex_pp_greek_ids,true)},!,
    "|",pp_expr_m(A,0,LimitReached),"|".

pp_expr2(Expr,500,LimitReached) -->
    {functor(Expr,F,_),
    function_like_in_mode(F,Symbol),!,
    Expr =.. [F|Args]},
    ppatom(Symbol),
    ({Args=[]}
    -> "" % some operators like pred and succ do not expect arguments
    ; pp_expr_wrap_l('(',Args,')',LimitReached)).

pp_expr2(Expr,250,LimitReached) -->
    {functor(Expr,F,3),
    quantified_in_mode(F,Symbol),
    Expr =.. [F,Ids,P1,E],
    !,
    add_normal_typing_predicates(Ids,P1,P)},
    ppatom(Symbol),pp_expr_ids(Ids,LimitReached),".(",
    pp_expr_m(P,11,LimitReached),pp_such_that_bar(E),
    pp_expr_m(E,11,LimitReached),")".

pp_expr2(Expr,Prio,LimitReached) -->
    {functor(Expr,F,N),
    (debug_mode(on)
    -> format('**** Unknown functor ~w/~w in pp_expr2~n expression: ~w~n',[F,N,Expr])
    ; format('**** Unknown functor ~w/~w in pp_expr2~n',[F,N])
    ),
    %add_internal_error('Unknown Expression: ',pp_expr2(Expr,Prio)),
    Prio=20},
    ppterm_with_limit_reached(Expr,LimitReached).

pp_expr_ids_in_mode/4

pp_expr_ids_in_mode_indent/3

pp_expr_ids_no_parentheses/4

pp_expr_l_pair_in_mode/4

pp_expr_let_pred_exprs/5

pp_function_left_bracket-->/2

pp_function_right_bracket-->/2

pp_functor/3

pp_identifier/3

pp_identifier_for_atelierb/3

pp_ids_indent/3

pp_important_infos/4

pp_inner_value/4

pp_is_important_info_field/3

pp_label/4

pp_lambda_identifiers/4

pp_pred_nested(TExpr,CurrentType,_) --> {TExpr = b(E,pred,_)},
    {get_binary_connective(E,NewType,Ascii,LHS,RHS), binary_infix(NewType,Ascii,Prio,left)},
    !,
    pp_rodin_label_indent(TExpr), % print any label
    inc_lvl(CurrentType,NewType),
    pp_pred_nested(LHS,NewType,Prio),
    {translate_in_mode(NewType,Ascii,Symbol)},
    indent(' '),pp_atom_indent(Symbol),
    indent(' '),
    {(is_associative(NewType) -> NewTypeR=NewType % no need for parentheses if same operator on right
    ; NewTypeR=right(NewType))},
    pp_pred_nested(RHS,NewTypeR,Prio),
    dec_lvl(CurrentType,NewType).

pp_pred_nested(TExpr,_,_) --> {is_nontrivial_negation(TExpr,NExpr,InnerType,Prio)},
    !,
    pp_rodin_label_indent(TExpr), % print any label
    {translate_in_mode(negation,'not',Symbol)},
    pp_atom_indent(Symbol),
    inc_lvl(other,negation), % always need parentheses for negation
    pp_pred_nested(NExpr,InnerType,Prio),
    dec_lvl(other,negation).

pp_pred_nested(TExpr,_,_) --> {TExpr = b(exists(Ids,RHS),pred,_)},
    !,
    pp_rodin_label_indent(TExpr), % print any label
    {translate_in_mode(exists,'#',FSymbol)},
    %indent(' '),
    pp_atom_indent(FSymbol),
    pp_expr_ids_in_mode_indent(Ids),pp_atom_indent('.'),
    inc_lvl(other,conjunct), % always need parentheses here
    {add_normal_typing_predicates(Ids,RHS,RHST), Prio=40}, % Prio of conjunction
    pp_pred_nested(RHST,conjunct,Prio),
    dec_lvl(other,conjunct).

pp_pred_nested(TExpr,_,_) --> {TExpr = b(forall(Ids,LHS,RHS),pred,_)},
    !,
    pp_rodin_label_indent(TExpr), % print any label
    {translate_in_mode(forall,'!',FSymbol)},
    %indent(' '),
    pp_atom_indent(FSymbol),
    pp_expr_ids_in_mode_indent(Ids),pp_atom_indent('.'),
    inc_lvl(other,implication), % always need parentheses here
    {add_normal_typing_predicates(Ids,LHS,LHST), Prio=30}, % Prio of implication
    pp_pred_nested(LHST,implication,Prio),
    {translate_in_mode(implication,'=>',Symbol)},
    indent(' '),pp_atom_indent(Symbol),
    indent(' '),
    pp_pred_nested(RHS,right(implication),Prio),
    dec_lvl(other,implication).

pp_pred_nested(TExpr,_,_) -->
    {\+ eventb_translation_mode,
    TExpr = b(let_predicate(Ids,Exprs,Body),pred,_)
    }, %Ids=[_]}, % TODO: enable printing with more than one id; see below
    !,
    pp_let_nested(Ids,Exprs,Body).

pp_pred_nested(b(BOP,pred,_),_CurrentType,CurMinPrio) -->
    {indent_binary_predicate(BOP,LHS,RHS,OpStr),
    get_texpr_id(LHS,_),can_indent_texpr(RHS)},!,
    pp_expr_m_indent(LHS,CurMinPrio),
    insertstr(OpStr),
    increase_indentation_level(2),
    indent(''),
    pp_expr_indent(RHS), % only supports %, {}, bool which do not need parentheses
    decrease_indentation_level(2).

pp_pred_nested(Expr,_CurrentType,CurMinPrio) --> {can_indent_texpr(Expr)},!,
    pp_expr_m_indent(Expr,CurMinPrio).

pp_pred_nested(Expr,_CurrentType,CurMinPrio) --> pp_expr_m_indent(Expr,CurMinPrio).

pp_prj12/6

pp_property/3

pp_property_without_plugin/3

pp_rodin_label_indent/3

pp_separator_sequence/1

pp_sequence/4

pp_sequence_with_limit/4

pp_single_csp_value/2

pp_space-->/2

pp_start_label_pragma-->/2

pp_such_that_bar/3

pp_such_that_bar-->/2

pp_theory_operator/5

pp_tla_value/4

pp_tla_with_sep/7

pp_tla_with_sep_aux/6

pp_value/4

Description:
,"TRUE". % TO DO: in latex_mode: surround by mathit
,"FALSE".

pp_value(_,LimitReached) --> {LimitReached==limit_reached},!, "...".

pp_value(V,_) --> {var(V)},!, pp_variable(V).

pp_value('$VAR'(N),_) --> !,pp_numberedvar(N).

pp_value(X,_) --> {cyclic_term(X)},!,underscore_symbol,"cyclic",underscore_symbol.

pp_value(fd(X,GSet),_) --> {var(X)},!,
    ppatom(GSet),":", ppnumber(X). ":??".

pp_value(fd(X,GSet),_) -->
    {b_global_sets:is_b_global_constant_hash(GSet,X,Res)},!,
    pp_identifier(Res).

pp_value(fd(X,GSet),_) --> {deferred_set_constant(GSet,X,Cst)},!,
    pp_identifier(Cst).

pp_value(fd(X,M),_) --> !,ppatom_opt_scramble(M),ppnumber(X).

pp_value(int(X),_) --> !,ppnumber(X).

pp_value(term(floating(X)),_) --> !,ppnumber(X).

pp_value(string(X),_) --> !,string_start_symbol,ppstring_opt_scramble(X),string_end_symbol.

pp_value(global_set(X),_) --> {atomic(X),integer_set_mapping(X,Kind,Y)},!,
    ({Kind=integer_set} -> ppatom(Y) ; ppatom_opt_scramble(X)).

pp_value(term(X),_) --> {var(X)},!,"term(",pp_variable(X),")".

pp_value(freetype(X),_) --> {pretty_freetype(X,P)},!,ppatom_opt_scramble(P).

pp_value(pred_true /* bool_true */,_) --> %!,"TRUE". % TO DO: in latex_mode: surround by mathit
    {constants_in_mode(pred_true,Symbol)},!,ppatom(Symbol).

pp_value(pred_false /* bool_false */,_) --> %!,"FALSE".
    {constants_in_mode(pred_false,Symbol)},!,ppatom(Symbol).

pp_value([],_) --> !,empty_set_symbol.

pp_value(sequence(List),LimitReached) --> !,
    ({List=[]} -> pp_empty_sequence ; pp_sequence_with_limit(List,LimitReached)).

pp_value([Head|Tail],LimitReached) --> {get_preference(translate_print_all_sequences,true),
    convert_set_into_sequence([Head|Tail],Elements)},
    !,
    pp_sequence(Elements,LimitReached).

pp_value([Head|Tail],LimitReached) --> !, {set_brackets(L,R)},
    ppatom(L),
    pp_value_l_with_limit([Head|Tail],',',LimitReached),
    ppatom(R).

pp_value( (A,B) ,LimitReached) --> !,
    "(",pp_inner_value(A,LimitReached),
    maplet_symbol,
    pp_value(B,LimitReached),")".

pp_value(avl_set(A),LimitReached) --> !,
    {check_is_non_empty_avl(A),avl_size(A,Sz)},
    {set_brackets(LBrace,RBrace)},
    ( {size_is_in_set_limit(Sz),
    %(Sz>2 ; get_preference(translate_print_all_sequences,true)),
    get_preference(translate_print_all_sequences,true), % no longer try and convert any sequence longer than 2 to sequence notation
    avl_max(A,(int(Sz),_)), % a sequence has minimum int(1) and maximum int(Sz)
    convert_avlset_into_sequence(A,Seq)} ->
    pp_sequence(Seq,LimitReached)
    ;
    ( {Sz=0} -> left_set_bracket," /* empty avl_set */ ",right_set_bracket
    ; {(size_is_in_set_limit(Sz) ; Sz < 3)} -> % if Sz 3 we will print at least two elements anyway
    {avl_domain(A,List)},
    ppatom(LBrace),pp_value_l(List,',',LimitReached),ppatom(RBrace)
    ; {(Sz<5 ; \+ size_is_in_set_limit(4))} ->
    {avl_min(A,Min),avl_max(A,Max)},
    hash_card_symbol, % "#"
    ppnumber(Sz),":", left_set_bracket,
    pp_value(Min,LimitReached),",",ldots,",",pp_value(Max,LimitReached),right_set_bracket
    ;
    {avl_min(A,Min),avl_next(Min,A,Nxt),avl_max(A,Max),avl_prev(Max,A,Prev)},
    hash_card_symbol, % "#",
    ppnumber(Sz),":", left_set_bracket,
    pp_value(Min,LimitReached),",",pp_value(Nxt,LimitReached),",",ldots,",",
    pp_value(Prev,LimitReached),",",pp_value(Max,LimitReached),right_set_bracket )).

pp_value(field(Name,Value),LimitReached) --> !,
    pp_identifier(Name),":",pp_value(Value,LimitReached). % : for fields has priority 120 in French manual

pp_value(rec(Rec),LimitReached) --> !,
    {function_like_in_mode(rec,Symbol)},
    ppatom(Symbol), "(",pp_value_l(Rec,',',LimitReached),")".

pp_value(struct(Rec),LimitReached) --> !,
    {function_like_in_mode(struct,Symbol)},
    ppatom(Symbol), "(", pp_value_l(Rec,',',LimitReached),")".

pp_value(term(no_value_for(Id)),_) --> !,
    "undefined ",ppatom(Id).

pp_value(closure(Variables,Types,Predicate),LimitReached) --> !,
    pp_closure_value(Variables,Types,Predicate,LimitReached).

pp_value(freeval(Freetype,Case,Value),LimitReached) --> !,
    ({ground(Case),ground(Value),Value=term(Case)} -> ppatom_opt_scramble(Case)
    ; {ground(Case)} -> ppatom_opt_scramble(Case),"(",pp_value(Value,LimitReached),")"
    ; {pretty_freetype(Freetype,P)},
    "FREEVALUE[",ppatom_opt_scramble(P),
    ",",write_to_codes(Case),
    "](",pp_value(Value,LimitReached),")"
).

pp_value(X,_) --> {animation_mode(xtl)},!,
    write_to_codes(X).

pp_value(X,_) --> % the << >> pose problems when checking against FDR
    "<< ",write_to_codes(X)," >>".

pp_value/3

pp_value_l/5

pp_value_l/6

pp_value_l_with_limit/5

pp_value_l_with_types/6

ppatom_opt_scramble/3

ppatoms/3

ppatoms_opt_latex/3

ppcodes/3

ppcodes_with_limit_reached/4

ppnumber/3

ppstring_opt_scramble/3

ppterm/3

ppterm_with_limit_reached/4

pretty_normalized_type/2

pretty_type/2

pretty_type2/4

pretty_type2(X,names(Vars,Names),_,Name) :- var(X),!,exact_member_lookup(X,Name,Vars,Names).

pretty_type2(any,_,_,'?').

pretty_type2(set(T),N,_,Text) :- nonvar(T),T=couple(A,B),!,
    pretty_type2(A,N,paren,AT), pretty_type2(B,N,paren,BT),
    binary_infix_in_mode(relations,Symbol,_,_), % <->
    ajoin(['(',AT,Symbol,BT,')'],Text).

pretty_type2(set(T),N,_,Text) :-
    pretty_type2(T,N,noparen,TT), function_like_in_mode(pow_subset,POW),
    ajoin([POW,'(',TT,')'],Text).

pretty_type2(seq(T),N,_,Text) :-
    pretty_type2(T,N,noparen,TT), ajoin(['seq(',TT,')'],Text).

pretty_type2(couple(A,B),N,Paren,Text) :-
    pretty_type2(A,N,paren,AT),pretty_type2(B,N,paren,BT),
    binary_infix_in_mode(cartesian_product,Cart,_,_),
    ajoin([AT,Cart,BT],Prod),
    ( Paren == noparen ->
    Text = Prod
    ;
    ajoin(['(',Prod,')'],Text)).

pretty_type2(string,_,_,'STRING').

pretty_type2(integer,_,_,Atom) :- integer_set_mapping('INTEGER',Atom).

pretty_type2(real,_,_,Atom) :- real_set_mapping('REAL',Atom).

pretty_type2(boolean,_,_,'BOOL').

pretty_type2(global(G_Id),_,_,A) :- opt_scramble_id(G_Id,G), ajoin([G],A).

pretty_type2(freetype(Id),N,_,A) :- pretty_freetype2(Id,N,A).

pretty_type2(pred,_,_,predicate).

pretty_type2(subst,_,_,substitution).

pretty_type2(constant(List),_,_,A) :-
    (var(List) -> ['{??VAR??...}'] % should not happen
    ; ajoin_with_sep(List,',',P), ajoin(['{',P,'}'],A)).

pretty_type2(record(Fields),N,_,Text) :-
    pretty_type_fields(Fields,N,FText),
    ajoin(['struct(',FText,')'],Text).

pretty_type2(op(Params,Results),N,_,Text) :-
    pretty_type_l(Params,N,PText),
    ( nonvar(Results),Results=[] ->
    ajoin(['operation(',PText,')'],Text)
    ;
    pretty_type_l(Results,N,RText),
    ajoin([RText,'<--operation(',PText,')'],Text) ).

pretty_type2(definition(DefType,_,_),_,_,DefType).

pretty_type2(witness,_,_,witness).

pretty_type2([],_,_,'[]') :- add_error(pretty_type,'Illegal list in type:','[]').

pretty_type2([H|T],_,_,'[_]') :- add_error(pretty_type,'Illegal list in type:',[H|T]).

pretty_type2(b(E,T,I),_,_,'?') :- add_error(pretty_type,'Illegal b/3 term in type:',b(E,T,I)).

print_additional_machine_info/0

Dynamic: true

print_bexpr/1

print_bexpr_or_subst/1

print_bexpr_stream/2

print_bexpr_with_limit/2

print_bracket/3

print_bstate/1

print_bstate_limited/3

print_bvalue/1

print_bvalue_stream/2

print_clpfd_variable/1

print_raw_machine_terms/1

print_raw_machine_terms_sep/2

print_unwrapped_bexpr_with_limit/1

print_unwrapped_bexpr_with_limit/2

print_value_variable/1

remove_already_typed_ids/3

remove_already_typed_ids2/3

remove_b_portray_hook/0

remove_duplicate_predicates/3

renaming_csp_op/5

render_b_expr/3

render_call/4

render_call(definition_call(Name,Pos),Opts) --> !,
    ['within DEFINITION call '],[Name],
    render_span(Pos,Opts).

render_call(operation_call(Op,Paras,Pos),Opts) --> !,
    translate_b_operation_call(Op,Paras), % TODO: limit size?
    render_span(Pos,Opts).

render_call(using_state(Name,State),_Opts) --> !,
    [Name], [' with state: '],
    {get_cs_limit(Limit),translate_bstate_limited(State,Limit,Str)},
    [Str].

render_call(after_event(OpTerm),_Opts) --> !,
    ['after event: '],
    {get_cs_limit(Limit),translate_event_with_limit(OpTerm,Limit,Str)},
    [Str].

render_call(function_call(Fun,Paras,Pos),Opts) --> !,
    render_function_call(Fun,Paras),
    render_span(Pos,Opts).

render_call(b_operator_call(OP,Paras,Pos),Opts) --> !,
    render_operator_arg(b_operator(OP,Paras)),
    render_span(Pos,Opts).

render_call(id_equality_evaluation(ID,Kind,Pos),Opts) --> !,
    ['equality for '],[Kind],[' '],[ID],
    render_span(Pos,Opts).

render_call(b_operator_arg_evaluation(OP,PosNr,Args,Pos),Opts) --> !,
    ['arg '],[PosNr],[' of '],
    render_operator_arg(b_operator(OP,Args)),
    render_span(Pos,Opts).

render_call(external_call(Name,Paras,Pos),Opts) --> !,
    ['external call '], [Name],['('],
    {get_cs_limit(Limit),translate_bvalues_with_limit(Paras,Limit,PS)},[PS], [')'],
    render_span(Pos,Opts).

render_call(prob_command_context(Name,Pos),Opts) --> !,
    ['checking '], render_prob_command(Name),
    render_span(Pos,Opts).

render_call(quantifier_call(comprehension_set,ParaNames,ParaValues,Pos),Opts) --> % special case for lambda
    {nth1(LPos,ParaNames,LambdaRes,RestParaNames),
    is_lambda_result_name(LambdaRes,_),
    nth1(LPos,ParaValues,LambdaVal,RestParaValues)},!, % we have found '_lambda_res_' amongst paras
    render_quantifier(lambda), ['('],
    render_paras(RestParaNames,RestParaValues),
    ['|'], render_para_val(LambdaVal),
    [')'],
    render_span(Pos,Opts).

render_call(quantifier_call(Kind,ParaNames,ParaValues,Pos),Opts) --> !,
    render_quantifier(Kind), ['('],
    render_paras(ParaNames,ParaValues), [')'],
    render_span(Pos,Opts).

render_call(top_level_call(SpanPred),Opts) -->
    render_call(SpanPred,Opts).

render_call(b_expr_call(Context,Expr),Opts) --> !,
    [Context],[': '],
    render_b_expr(Expr),
    render_span(Expr,Opts).

render_call(span_predicate(Pred,LS,S),Opts) --> % Pred can also be an expression like function/2
    % infos could contain was(extended_expr(Op)); special case for: assertion_expression
    {Pred=b(_,_,Pos),
    b_compiler:b_compile(Pred,[],LS,S,CPred,no_wf_available) % inline actual parameters
    },
    !,
    render_b_expr(CPred),
    render_function_name(Pred), % try show function name from uncompiled Expr
    render_span(Pos,Opts).

render_call(Other,_) --> [Other].

render_call_stack/5

render_function_call/4

render_function_name/3

render_negation_context/3

render_nr/6

render_operator_arg/3

render_operator_args/3

render_prob_command/3

reset_suppress_rodin_positions/1

reset_translate/0

return_csp_closure_value/2

right_set_bracket-->/2

section_pred_over_lines/5

select_membership/4

set_atelierb_mode/1

set_brackets/2

set_force_eventb_mode/0

set_language_mode/1

set_latex_mode/0

set_pref_used/1

set_print_type_infos/1

set_suppress_rodin_positions/2

set_translation_constants/1

Description:
print_message(setting_constants(ConstID)),%%

set_translation_context/1

Description:
print_message(setting_translation_constants(ConstID)),

set_translation_mode/1

set_unicode_mode/0

set_up_limit_reached/3

show_parameter_value/4

show_parameter_values/4

size_is_in_set_limit/1

standard_library_required/2

start_size/3

status_string/2

string_end_symbol-->/2

string_start_symbol-->/2

strip_code/3

strip_illegal_id_codes/3

strip_illegal_id_codes2/3

subst_needs_begin_end/1

suppress_rodin_positions/1

symbolic_raw/2

transform_raw/2

transform_raw(Var,Res) :- %print(raw(Var)),nl,
    var(Var), !, add_internal_error('Var raw expression:',transform_raw(Var,Res)),
    Res= b(identifier('$$VARIABLE$$'),any,[raw]).

transform_raw(precondition(_,Pre,Body),Res) :- !, Res= b(precondition(TP,TB),subst,[raw]),
    transform_raw(Pre,TP),
    transform_raw(Body,TB).

transform_raw(typeof(_,E,_Type),Res) :- !, transform_raw(E,Res). % remove typeof operator; TODO: transform

transform_raw(identifier(_,M),Res) :- !, Res= b(identifier(M),any,[raw]).

transform_raw(integer(_,M),Res) :- !, Res= b(integer(M),integer,[raw]).

transform_raw(integer_set(_),Res) :- !, generate_typed_int_set('INTEGER',Res).

transform_raw(natural_set(_),Res) :- !, generate_typed_int_set('NATURAL',Res).

transform_raw(natural1_set(_),Res) :- !, generate_typed_int_set('NATURAL1',Res).

transform_raw(nat_set(_),Res) :- !, generate_typed_int_set('NAT',Res).

transform_raw(nat1_set(_),Res) :- !, generate_typed_int_set('NAT1',Res).

transform_raw(int_set(_),Res) :- !, generate_typed_int_set('INT',Res).

transform_raw(let_expression(_,_Ids,Eq,Body),Res) :- !,
    transform_raw(conjunct(_,Eq,Body),Res). % TO DO: fix and generate let_expression(Ids,ListofExprs,Body)

transform_raw(let_predicate(_,_Ids,Eq,Body),Res) :- !,
    transform_raw(conjunct(_,Eq,Body),Res). % ditto

transform_raw(forall(_,Ids,Body),Res) :- !,
    (Body=implication(_,LHS,RHS) -> true ; LHS=truth,RHS=Body),
    transform_raw(forall(_,Ids,LHS,RHS),Res).

transform_raw(record_field(_,Rec,identifier(_,Field)),Res) :- !, Res = b(record_field(TRec,Field),any,[]),
    transform_raw(Rec,TRec).

transform_raw(rec_entry(_,identifier(_,Field),Rec),Res) :- !, Res = field(Field,TRec),
    transform_raw(Rec,TRec).

transform_raw(conjunct(_,List),Res) :- !,
    transform_raw_list_to_conjunct(List,Res). % sometimes conjunct/1 with list is used (e.g., .eventb files)

transform_raw(couple(_,L),Res) :- !, transform_raw_list_to_couple(L,Res). % couples are represented by lists

transform_raw(extended_expr(Pos,Op,L,_TypeParas),Res) :- !,
    (L=[] -> transform_raw(identifier(none,Op),Res) % no arguments
    ; transform_raw(function(Pos,identifier(none,Op),L),Res)).

transform_raw(extended_pred(Pos,Op,L,_TypeParas),Res) :- !,
    transform_raw(function(Pos,identifier(none,Op),L),Res). % not of correct type pred, but seems to work

transform_raw(external_function_call_auto(Pos,Name,Para),Res) :- !,
    transform_raw(external_function_call(Pos,Name,Para),Res). % we assume expr rather than pred and hope for the best

transform_raw(function(_,F,L),Res) :- !, transform_raw(F,TF),
    Res = b(function(TF,Args),any,[]),
    transform_raw_list_to_couple(L,Args). % args are represented by lists

transform_raw(Atom,Res) :- atomic(Atom),!,Res=Atom.

transform_raw([H|T],Res) :- !, maplist(transform_raw,[H|T],Res).

transform_raw(Symbolic,Res) :- symbolic_raw(Symbolic,Body),!,
    transform_raw(Body,Res).

transform_raw(OtherOp,b(Res,Type,[])) :- OtherOp =..[F,_Pos|Rest],
    maplist(transform_raw,Rest,TRest),
    (get_type(F,FT) -> Type=FT ; Type=any),
    Res =.. [F|TRest].

transform_raw_list/2

transform_raw_list_to_conjunct/2

transform_raw_list_to_couple/2

translate_additional_description/2

translate_any_state/2

translate_b_operation_call/4

translate_b_state_to_comma_list/3

translate_b_state_to_comma_list_codes/4

translate_bexpr_for_call_stack/2

translate_bexpr_to_parseable/2

translate_bexpression/2

translate_bexpression_to_codes/2

translate_bexpression_to_unicode/2

translate_bexpression_with_limit/2

translate_bexpression_with_limit/3

translate_bexpression_with_limit/4

translate_bstate/2

translate_bstate_limited/2

translate_bstate_limited/3

translate_bstate_limited/4

translate_bvalue/2

translate_bvalue_for_dot/2

translate_bvalue_for_expression/3

translate_bvalue_for_expression_with_limit/4

translate_bvalue_kind/2

translate_bvalue_to_codes/2

translate_bvalue_to_codes_with_limit/3

translate_bvalue_to_parseable_aux/2

translate_bvalue_to_parseable_classicalb/2

translate_bvalue_with_limit/3

translate_bvalue_with_limit_aux/3

translate_bvalue_with_tlatype/3

translate_bvalue_with_type/3

translate_bvalue_with_type_and_limit/4

translate_bvalue_with_type_and_limit2/4

translate_bvalues/2

translate_bvalues_with_limit/3

translate_bvalues_with_types/3

translate_call_stack/2

translate_cases/3

translate_channel_values/3

translate_context/2

translate_csp_value/2

translate_cspm_expression/2

translate_cspm_state/2

translate_error_context/2

translate_error_context2/3

translate_error_term/2

translate_error_term/3

translate_error_term(Var,_,S) :- var(Var),!,
    translate_term_into_atom_with_max_depth(Var,5,S).

translate_error_term('@fun'(X,F),Span,S) :-
    translate_bvalue(X,TX),
    (get_function_from_span(Span,Fun,LocState,State),
    translate_bexpression_with_limit(Fun,200,TSF)
    -> % we managed to extract the function from the span_predicate
    (is_compiled_value(Fun)
    -> (get_was_identifier(Fun,WasFunId) -> Rest = [', function: ',WasFunId | Rest1]
    ; Rest = Rest1
    ),
    TVal=TSF % use as value
    ; Rest = [', function: ',TSF | Rest1],
    % try and extract value from span_predicate (often F=[] after traversing avl)
    (get_texpr_id(Fun,FID),
    (member(bind(FID,FVal),LocState) ; member(bind(FID,FVal),State))
    -> translate_bvalue(FVal,TVal)
    ; translate_bvalue(F,TVal)
    )
    )
    ; Rest=[], translate_bvalue(F,TVal)
    ),!,
    % translate_term_into_atom_with_max_depth('@fun'(TX,TVal),5,S).
    (get_error_span_for_value(F,NewSpanTxt) % triggers in test 953
    -> Rest1 = [' defined at ',NewSpanTxt]
    ; Rest1 = []
    ),
    ajoin(['Function argument: ',TX, ', function value: ',TVal | Rest],S).

translate_error_term('@rel'(Arg,Res1,Res2),_,S) :-
    translate_bvalue(Arg,TA), translate_bvalue(Res1,R1),
    translate_bvalue(Res2,R2),!,
    ajoin(['Function argument: ',TA, ', two possible values: ',R1,', ',R2],S).

translate_error_term([operation(Name,Env)],_,S) :-
    translate_any_state(Env,TEnv), !,
    translate_term_into_atom_with_max_depth(operation(Name,TEnv),10,S).

translate_error_term(error(E1,E2),_,S) :- !, translate_prolog_error(E1,E2,S).

translate_error_term(b(B,T,I),_,S) :-
    translate_subst_or_bexpr_with_limit(b(B,T,I),1000,do_not_report_errors,S),!. % do not report errors, otherwise we end in an infinite loop of adding errors while adding errors

translate_error_term([H|T],_,S) :- nonvar(H), H=b(_,_,_), % typically a list of typed ids
    E=b(sequence_extension([H|T]),any,[]),
    translate_subst_or_bexpr_with_limit(E,1000,do_not_report_errors,S),!.

translate_error_term([H|T],_,S) :- nonvar(H), H=bind(_,_), % a store
    translate_bstate_limited([H|T],1000,S),!.

translate_error_term(Term,_,S) :-
    is_bvalue(Term),
    translate_bvalue_with_limit(Term,1000,S),!.

translate_error_term(T,_,S) :-
    (debug_mode(on) -> Depth = 20 ; Depth = 5),
    translate_term_into_atom_with_max_depth(T,Depth,S).

translate_event/2

translate_event2/3

Description:
translate_event2(i(_Span),['i'|T],T) :- process_algebra_mode,!. / CSP */ %% deprecated

translate_event_error/2

translate_event_error2/2

translate_event_with_limit/3

translate_event_with_src_and_target_id/4

translate_event_with_src_and_target_id/5

translate_event_with_target_id/4

translate_event_with_target_id2/5

translate_event_with_target_id2(Term,_,Dst,Limit,Str) :-
    functor(Term,Functor,_),
    setup_cst_functor(Functor,UI_Name),
    get_preference(show_initialisation_arguments,true),
    state_space:visited_expression(Dst,concrete_constants(State)),
    get_non_det_constant(State,NonDetState),
    !,
    translate_b_state_to_comma_list_codes(UI_Name,NonDetState,Limit,Codes),
    atom_codes_with_limit(Str,Limit,Codes).

translate_event_with_target_id2(Term,_,Dst,Limit,Str) :-
    functor(Term,'$initialise_machine',_),
    get_preference(show_initialisation_arguments,true),
    bmachine:b_get_operation_non_det_modifies('$initialise_machine',NDModVars),
    state_space:visited_expression(Dst,State), get_variables(State,VarsState),
    (NDModVars \= []
    ->
    include(non_det_modified_var(NDModVars),VarsState,ModVarsState) % first show non-det variables
    % we could add a preference for whether to show the deterministicly assigned variables at all
    %exclude(non_det_modified_var(NDModVars),VarsState,ModVarsState2),
    %append(ModVarsState1,ModVarsState2,ModVarsState)
    ; ModVarsState = VarsState),
    !,
    translate_b_state_to_comma_list_codes("INITIALISATION",ModVarsState,Limit,Codes),
    atom_codes_with_limit(Str,Limit,Codes).

translate_event_with_target_id2(Term,Src,Dst,Limit,Str) :-
    atomic(Term), % only applied to operations without parameters
    specfile:b_mode,
    get_non_det_modified_vars_in_target_id(Term,Dst,ModVarsState0), % only show non-det variables
    (Src \= unknown,
    state_space:visited_expression(Src,SrcState), get_variables(SrcState,PriorVarsState)
    -> exclude(var_not_really_modified(PriorVarsState),ModVarsState0,ModVarsState)
    % we could also optionally filter out vars which have the same value for all outgoing transitions of Src
    ; ModVarsState = ModVarsState0
    ),
    !,
    atom_codes(Term,TermCodes),
    translate_b_state_to_comma_list_codes(TermCodes,ModVarsState,Limit,Codes),
    atom_codes_with_limit(Str,Limit,Codes).

translate_event_with_target_id2(Term,_,_,Limit,Str) :- translate_event_with_limit(Term,Limit,Str).

translate_eventb_direct_definition_body/2

translate_eventb_direct_definition_header/3

translate_eventb_operator/4

translate_eventb_operator2/7

translate_eventb_operators/3

translate_eventb_to_classicalb/3

translate_events/2

translate_freetype/3

translate_freetype_cases/3

translate_freetypes/3

translate_mpart2(deferred_sets,I,_) -->
    mpstart_section(sets,'SETS /* deferred */',' ; /* deferred */',P),
    indent_expr_l_sep(I,';'),mpend(P).

translate_mpart2(enumerated_sets,_I,_) --> []. % these are now pretty printed below

translate_mpart2(enumerated_elements,I,_) --> %{print(enum_els(I)),nl},
    {translate_enums(I,[],Res)},
    mpstart_section(sets,'SETS /* enumerated */',' ; /* enumerated */',P),
    indent_expr_l_sep(Res,';'),mpend(P).

translate_mpart2(parameters,I,_) --> mpstart('PARAMETERS',P),indent_expr_l_sep(I,','),mpend(P).

translate_mpart2(internal_parameters,I,_) --> {print_additional_machine_info},!,
    mpstart('/* INTERNAL_PARAMETERS',P),indent_expr_l_sep(I,','),insertstr(' */'),mpend(P).

translate_mpart2(internal_parameters,_I,_) --> [].

translate_mpart2(abstract_variables,I,_) --> mpstart('ABSTRACT_VARIABLES',P),indent_exprs(I),mpend(P).

translate_mpart2(concrete_variables,I,_) --> mpstart('CONCRETE_VARIABLES',P),indent_exprs(I),mpend(P).

translate_mpart2(abstract_constants,I,_) --> mpstart('ABSTRACT_CONSTANTS',P),indent_exprs(I),mpend(P).

translate_mpart2(concrete_constants,I,_) --> mpstart('CONCRETE_CONSTANTS',P),indent_exprs(I),mpend(P).

translate_mpart2(promoted,I,_) --> {print_additional_machine_info},!,
    mpstart('/* PROMOTED OPERATIONS',P),indent_expr_l_sep(I,','),insertstr(' */'),mpend(P).

translate_mpart2(promoted,_I,_) --> [].

translate_mpart2(unpromoted,I,_) --> {print_additional_machine_info},!,
    mpstart('/* NOT PROMOTED OPERATIONS',P),indent_expr_l_sep(I,','),insertstr(' */'),mpend(P).

translate_mpart2(unpromoted,_I,_) --> [].

translate_mpart2(constraints,I,All) --> mpart_typing(constraints,[parameters],All,I).

translate_mpart2(invariant,I,All) --> mpart_typing(invariant, [abstract_variables,concrete_variables],All,I).

translate_mpart2(linking_invariant,_I,_) --> [].

translate_mpart2(properties,I,All) --> mpart_typing(properties,[abstract_constants,concrete_constants],All,I).

translate_mpart2(assertions,I,_) -->
    mpstart_spec_desc(assertions,P),
    %indent_expr_l_sep(I,';'),
    preds_over_lines(1,'@thm','; ',I),
    mpend(P). % TO DO:

translate_mpart2(initialisation,S,_) --> mpstart_spec_desc(initialisation,P),translate_inits(S),mpend(P).

translate_mpart2(definitions,Defs,_) --> {(standard_library_required(Defs,_) ; set_pref_used(Defs))},!,
    mpstart('DEFINITIONS',P),
    insertstr('\n'),
    {findall(Lib,standard_library_required(Defs,Lib),Libs)},
    insert_library_usages(Libs),
    translate_set_pref_defs(Defs),
    mpend(P),
    translate_other_defpart(Defs).

translate_mpart2(definitions,Defs,_) --> !, translate_other_defpart(Defs).

translate_mpart2(operation_bodies,Ops,_) --> mpstart_spec_desc(operations,P),translate_ops(Ops),mpend(P).

translate_mpart2(used,Used,_) --> {print_additional_machine_info},!,
    mpstart('/* USED',P),translate_used(Used),insertstr(' */'),mpend(P).

translate_mpart2(used,_Used,_) --> [].

translate_mpart2(freetypes,Freetypes,_) -->
    mpstart('FREETYPES',P),translate_freetypes(Freetypes),mpend(P).

translate_mpart2(meta,_Infos,_) --> [].

translate_mpart2(operators,Operators,_) -->
    insertstr('\n/* Event-B operators:'), % */
    indention_level(I,I2), {I2 is I+2},
    translate_eventb_operators(Operators),
    indention_level(I2,I),
    insertstr('\n*/').

translate_mpart2(values,Values,_) -->
    mpstart('VALUES',P),indent_expr_l_sep(Values,';'),mpend(P).

translate_op/3

translate_op_params/3

translate_op_results/3

translate_operation/6

translate_ops/3

translate_other_defpart/3

translate_params_for_dot/2

translate_params_for_dot/4

translate_params_for_dot_nl/2

translate_predicate_into_machine/3

translate_pref_val/2

translate_prolog_constructor/2

translate_prolog_constructor_in_mode/2

translate_prolog_error/3

translate_prolog_error(existence_error(procedure,Pred),_,S) :- !,
    translate_term_into_atom_with_max_depth('Unknown Prolog predicate:'(Pred),8,S).

translate_prolog_error(existence_error(source_sink,File),_,S) :- !,
    translate_term_into_atom_with_max_depth('File does not exist:'(File),8,S).

translate_prolog_error(permission_error(Action,source_sink,File),_,S) :- !, % Action = open, ...
    ajoin(['Permission denied to ',Action,' the file: ',File],S).

translate_prolog_error(permission_error(Action,past_end_of_stream,File),_,S) :- !, % Action = open, ...
    ajoin(['Permission denied to ',Action,' past end of file: ',File],S).

translate_prolog_error(system_error,system_error('SPIO_E_NET_CONNRESET'),S) :- !,
    S = 'System error: connection to process lost (SPIO_E_NET_CONNRESET)'.

translate_prolog_error(system_error,system_error('SPIO_E_ENCODING_UNMAPPABLE'),S) :- !,
    S = 'System error: illegal character or encoding encountered (SPIO_E_ENCODING_UNMAPPABLE)'.

translate_prolog_error(system_error,system_error('SPIO_E_NET_HOST_NOT_FOUND'),S) :- !,
    S = 'System error: could not find host (SPIO_E_NET_HOST_NOT_FOUND)'.

translate_prolog_error(system_error,system_error('SPIO_E_CHARSET_NOT_FOUND'),S) :- !,
    S = 'System error: could not find character set encoding'.

translate_prolog_error(system_error,system_error('SPIO_E_OS_ERROR'),S) :- !,
    S = 'System error due to some OS/system call (SPIO_E_OS_ERROR)'.

translate_prolog_error(system_error,system_error('SPIO_E_END_OF_FILE'),S) :- !,
    S = 'System error: end of file (SPIO_E_END_OF_FILE)'.

translate_prolog_error(system_error,system_error('SPIO_E_TOO_MANY_OPEN_FILES'),S) :- !,
    S = 'System error: too many open files (SPIO_E_TOO_MANY_OPEN_FILES)'.

translate_prolog_error(system_error,system_error(dlopen(Msg)),S) :- !,
    translate_term_into_atom_with_max_depth(Msg,4,MS),
    ajoin(['System error: could not load dynamic library (you may have to right-click on the library and open it in the macOS Finder): ', MS],S).

translate_prolog_error(system_error,system_error(Err),S) :- !,
    % or Err is an atom dlopen( mach-o file, but is an incompatible architecture ...)
    % E.g., SPIO_E_NOT_SUPPORTED when doing open('/usr',r,S)
    translate_term_into_atom_with_max_depth('System error:'(Err),8,S).

translate_prolog_error(existence_error(procedure,Module:Pred/Arity),_,S) :- !,
    ajoin(['Prolog predicate does not exist: ',Module,':', Pred, '/',Arity],S).

translate_prolog_error(instantiation_error,instantiation_error(Call,_ArgNo),S) :- !,
    translate_term_into_atom_with_max_depth('Prolog instantiation error:'(Call),8,S).

translate_prolog_error(uninstantiation_error(_),uninstantiation_error(Call,_ArgNo,_Culprit),S) :- !,
    translate_term_into_atom_with_max_depth('Prolog uninstantiation error:'(Call),8,S).

translate_prolog_error(evaluation_error(zero_divisor),evaluation_error(Call,_,_,_),S) :- !,
    translate_term_into_atom_with_max_depth('Division by zero error:'(Call),8,S).

translate_prolog_error(evaluation_error(float_overflow),evaluation_error(Call,_,_,_),S) :- !,
    translate_term_into_atom_with_max_depth('Float overflow:'(Call),8,S).

translate_prolog_error(representation_error(Err),representation_error(Call,_,_),S) :-
    memberchk(Err, ['CLPFD integer overflow','max_clpfd_integer','min_clpfd_integer']),!,
    translate_term_into_atom_with_max_depth('Prolog CLP(FD) overflow:'(Call),8,S).

translate_prolog_error(syntax_error(Err),_,S) :- !,
    translate_term_into_atom_with_max_depth('Prolog syntax error:'(Err),8,S).

translate_prolog_error(_,resource_error(open(File,Mode,_),Kind),S) :- !, % Kind e.g. file_handle
    ajoin(['Resource error (',Kind,
    '), could not open file ',File,' in mode ',Mode],S).

translate_prolog_error(E1,_,S) :- translate_term_into_atom_with_max_depth(E1,8,S).

translate_prolog_exception/2

translate_properties_with_limit/2

translate_property_with_limit/3

translate_raw_bexpr_with_limit/3

translate_section_list/2

translate_set_pref_def/3

translate_set_pref_defs/3

translate_set_pref_defs1/3

translate_span/2

translate_span/4

translate_span_file/4

translate_span_file_opt/4

translate_span_with_filename/2

translate_state_error/2

translate_state_errors/2

translate_subst/3

translate_subst2/3

translate_subst2(Var) --> {var(Var)}, !, "_", {add_warning(translate_subst,'Variable subst:',Var)}.

translate_subst2(skip) -->
    indent(skip).

translate_subst2(operation(Id,Res,Params,Body)) --> translate_operation(Id,Res,Params,Body). % not really a substition that can appear normally

translate_subst2(precondition(P,S)) -->
    indent('PRE '), pred_over_lines(2,'@grd',P), indent('THEN'), insert_subst(S), indent('END').

translate_subst2(assertion(P,S)) -->
    indent('ASSERT '), pp_expr_indent(P), indent('THEN'), insert_subst(S), indent('END').

translate_subst2(witness_then(P,S)) -->
    indent('WITNESS '), pp_expr_indent(P), indent('THEN'), insert_subst(S), indent('END').

translate_subst2(block(S)) -->
    indent('BEGIN'), insert_subst(S), indent('END').

translate_subst2(assign([L],[R])) --> !,
    indent,pp_expr_indent(L),insertstr(' := '),pp_expr_indent(R).

translate_subst2(assign(L,R)) -->
    {(member(b(E,_,_),R), can_indent_expr(E)
    -> maplist(create_assign,L,R,ParAssigns))},!, % split into parallel assignments so that we can indent
    translate_subst2(parallel(ParAssigns)).

translate_subst2(assign(L,R)) -->
    indent,pp_expr_indent_l(L),insertstr(' := '),pp_expr_indent_l(R).

translate_subst2(assign_single_id(L,R)) -->
    translate_subst2(assign([L],[R])).

translate_subst2(becomes_element_of(L,R)) -->
    indent,pp_expr_indent_l(L),insertstr(' :: '),pp_expr_indent(R).

translate_subst2(becomes_such(L,R)) -->
    indent,pp_expr_indent_l(L),insertstr(' : '), insertstr('('),
    { add_optional_typing_predicates(L,R,R1) },
    pp_expr_indent(R1), insertstr(')').

translate_subst2(evb2_becomes_such(L,R)) --> translate_subst2(becomes_such(L,R)).

translate_subst2(if([Elsif|Rest])) -->
    { get_if_elsif(Elsif,P,S) },
    indent('IF '), pp_expr_indent(P), insertstr(' THEN'),
    insert_subst(S),
    translate_ifs(Rest).

translate_subst2(if_elsif(P,S)) --> % not a legal top-level construct; but can be called in b_portray_hook
    indent('IF '), pp_expr_indent(P), insertstr(' THEN'),
    insert_subst(S),
    indent('END').

translate_subst2(choice(Ss)) --> indent(' CHOICE'),
    split_over_lines(Ss,'OR'),
    indent('END'). % indentation seems too far

translate_subst2(parallel(Ss)) -->
    split_over_lines(Ss,'||').

translate_subst2(init_statement(S)) --> insert_subst(S).

translate_subst2(sequence(Ss)) -->
    split_over_lines(Ss,';').

translate_subst2(operation_call(Id,Rs,As)) -->
    indent,translate_op_results(Rs),
    pp_expr_indent(Id),
    translate_op_params(As).

translate_subst2(identifier(op(Id))) --> % shouldn't normally appear
    indent,pp_expr_indent(identifier(Id)).

translate_subst2(external_subst_call(Symbol,Args)) -->
    indent,
    pp_expr_indent(identifier(Symbol)),
    translate_op_params(Args).

translate_subst2(any(Ids,Pred,Subst)) -->
    indent('ANY '), pp_expr_indent_l(Ids),
    indent('WHERE '),
    {add_optional_typing_predicates(Ids,Pred,Pred2)},
    pred_over_lines(2,'@grd',Pred2), indent('THEN'),
    insert_subst(Subst),
    indent('END').

translate_subst2(select(Whens)) -->
    translate_whens(Whens,'SELECT '),
    indent('END').

translate_subst2(select_when(Cond,Then)) --> % not a legal top-level construct; but can be called in b_portray_hook
    indent('WHEN'),
    pp_expr_indent(Cond),
    indent('THEN'),
    insert_subst(Then),
    indent('END').

translate_subst2(select(Whens,Else)) -->
    translate_whens(Whens,'SELECT '),
    indent('ELSE'), insert_subst(Else),
    indent('END').

translate_subst2(var(Ids,S)) -->
    indent('VAR '),
    pp_expr_indent_l(Ids),
    indent('IN'),insert_subst(S),
    indent('END').

translate_subst2(let(Ids,P,S)) -->
    indent('LET '),
    pp_expr_indent_l(Ids),
    insertstr(' BE '), pp_expr_indent(P),
    indent('IN'), insert_subst(S),
    indent('END').

translate_subst2(lazy_let_subst(TID,P,S)) -->
    indent('LET '),
    pp_expr_indent_l([TID]),
    insertstr(' BE '), pp_expr_indent(P), % could be expr or pred
    indent('IN'), insert_subst(S),
    indent('END').

translate_subst2(case(Expression,Cases,ELSE)) -->
    % CASE E OF EITHER m THEN G OR n THEN H ... ELSE I END END
    indent('CASE '),
    pp_expr_indent(Expression), insertstr(' OF'),
    indent('EITHER '), translate_cases(Cases),
    indent('ELSE '), insert_subst(ELSE), % we could drop this if ELSE is skip ?
    indent('END END').

translate_subst2(while(Pred,Subst,Inv,Var)) -->
    indent('WHILE '), pp_expr_indent(Pred),
    indent('DO'),insert_subst(Subst),
    indent('INVARIANT '),pp_expr_indent(Inv),
    indent('VARIANT '),pp_expr_indent(Var),
    indent('END').

translate_subst2(while1(Pred,Subst,Inv,Var)) -->
    indent('WHILE /* 1 */ '), pp_expr_indent(Pred),
    indent('DO'),insert_subst(Subst),
    indent('INVARIANT '),pp_expr_indent(Inv),
    indent('VARIANT '),pp_expr_indent(Var),
    indent('END').

translate_subst2(rlevent(Id,Section,Status,Parameters,Guard,Theorems,Actions,VWitnesses,PWitnesses,_Unmod,Refines)) -->
    indent,
    insert_status(Status),
    insertstr('EVENT '),
    ({Id = 'INITIALISATION'}
    -> [] % avoid BLexer error in ProB2-UI, BLexerException: Invalid combination of symbols: 'INITIALISATION' and '='.
    ; insertstr(Id), insertstr(' = ')),
    insertstr('/'), insertstr('* of machine '),
    insertstr(Section),insertstr(' */'),
    insert_variant(Status),
    ( {Parameters=[], get_texpr_expr(Guard,truth)} ->
    {NoGuard=true} % indent('BEGIN ')
    ; {Parameters=[]} ->
    indent('WHEN '),
    pred_over_lines(2,'@grd',Guard)
    ;
    indent('ANY '),pp_expr_indent_l(Parameters),
    indent('WHERE '),
    pred_over_lines(2,'@grd',Guard)
    ),
    ( {VWitnesses=[],PWitnesses=[]} ->
    []
    ;
    {append(VWitnesses,PWitnesses,Witnesses)},
    indent('WITH '),pp_witness_l(Witnesses)
    ),
    {( Actions=[] ->
    create_texpr(skip,subst,[],Subst)
    ;
    create_texpr(parallel(Actions),subst,[],Subst)
    )},
    ( {Theorems=[]} -> {true}
    ;
    indent('THEOREMS '),
    preds_over_lines(2,'@thm',Theorems)
    ),
    ({NoGuard==true}
    -> indent('BEGIN ') % avoid BLexer errors in ProB2-UI Syntax highlighting
    ; indent('THEN ')
    ),
    insert_subst(Subst),
    pp_refines_l(Refines,Id),
    indent('END').

translate_subst_begin_end/3

translate_subst_check/3

translate_subst_or_bexpr/2

translate_subst_or_bexpr_in_mode/3

translate_subst_or_bexpr_with_limit/3

translate_subst_or_bexpr_with_limit/4

translate_subst_with_indention/4

translate_subst_with_indention_and_label/4

translate_subst_with_label/3

translate_substitution/2

translate_substitution/3

translate_used/3

translate_used2/3

translate_whens/4

translated_identifier/2

treat_constants/1

try_get_identifier/2

try_pp_b_state/4

type_infos_in_subst/3

type_infos_in_subst2/3

unary_postfix/3

unary_postfix_in_mode/3

unary_prefix/3

unary_prefix_parentheses/2

underscore_symbol-->/2

unicode_translation/2

unicode_translation(implication, '\x21D2\').

unicode_translation(conjunct,'\x2227\').

unicode_translation(disjunct,'\x2228\').

unicode_translation(negation,'\xAC\').

unicode_translation(equivalence,'\x21D4\').

unicode_translation(not_equal,'\x2260\').

unicode_translation(less_equal,'\x2264\').

unicode_translation(less_equal_real,'\x2264\').

unicode_translation(greater_equal,'\x2265\').

unicode_translation(member,'\x2208\').

unicode_translation(not_member,'\x2209\').

unicode_translation(subset,'\x2286\').

unicode_translation(subset_strict,'\x2282\').

unicode_translation(not_subset,'\x2288\').

unicode_translation(not_subset_strict,'\x2284\').

unicode_translation(supseteq,'\x2287\'). % ProB parser supports unicode symbol by reversing arguments

unicode_translation(supset_strict,'\x2283\'). % ditto

unicode_translation(not_supseteq,'\x2289\'). % ditto

unicode_translation(not_supset_strict,'\x2285\'). % ditto

unicode_translation(union,'\x222A\').

unicode_translation(intersection,'\x2229\').

unicode_translation(cartesian_product,'\xD7\'). % also 0x2217 in Camille or 0x2A2F (vector or cross product) in IDP

unicode_translation(couple,'\x21A6\').

unicode_translation(div,'\xF7\').

unicode_translation(dot_symbol,'\xB7\'). % not a B AST operator, cf dot_symbol 183

unicode_translation(floored_div,'\xF7\') :-
animation_minor_mode(tla). % should we provide another Unicode character here for B?

unicode_translation(power_of,'\x02C4\'). % version of ^, does not exist in Rodin ?!, upwards arrow x2191 used below for restrict front

unicode_translation(power_of_real,'\x02C4\').

unicode_translation(interval,'\x2025\').

unicode_translation(domain_restriction,'\x25C1\').

unicode_translation(domain_subtraction,'\x2A64\').

unicode_translation(range_restriction,'\x25B7\').

unicode_translation(range_subtraction,'\x2A65\').

unicode_translation(relations,'\x2194\').

unicode_translation(partial_function,'\x21F8\').

unicode_translation(total_function,'\x2192\').

unicode_translation(partial_injection,'\x2914\').

unicode_translation(partial_surjection,'\x2900\').

unicode_translation(total_injection,'\x21A3\').

unicode_translation(total_surjection,'\x21A0\').

unicode_translation(total_bijection,'\x2916\').

unicode_translation('INTEGER','\x2124\').

unicode_translation('NATURAL','\x2115\').

unicode_translation('NATURAL1','\x2115\\x2081\'). % \x2115\ is subscript 1

unicode_translation('REAL','\x211D\'). % 8477 in decimal

unicode_translation(real_set,'\x211D\').

unicode_translation(pow_subset,'\x2119\').

unicode_translation(pow1_subset,'\x2119\\x2081\'). % \x2115\ is subscript 1

unicode_translation(lambda,'\x3BB\').

unicode_translation(general_product,'\x220F\').

unicode_translation(general_sum,'\x2211\').

unicode_translation(quantified_union,'\x22C3\'). % 8899 in decimal

unicode_translation(quantified_intersection,'\x22C2\'). % 8898 in decimal

unicode_translation(empty_set,'\x2205\').

unicode_translation(truth,'\x22A4\'). % 8868 in decimal

unicode_translation(falsity,'\x22A5\'). % 8869 in decimal

unicode_translation(direct_product,'\x2297\').

unicode_translation(parallel_product,'\x2225\').

unicode_translation(reverse,'\x207B\\xB9\') :- \+ force_eventb_rodin_mode. % the one ¹ is ASCII 185

unicode_translation(concat,'\x2312\'). % Arc character

unicode_translation(insert_front,'\x21FE\').

unicode_translation(insert_tail,'\x21FD\').

unicode_translation(restrict_front,'\x2191\'). % up arrow

unicode_translation(restrict_tail,'\x2192\').

unicode_translation(forall, '\x2200\'). % usually forall_symbol used

unicode_translation(exists, '\x2203\'). % usually exists_symbol used

unicode_translation(eqeq,'\x225c\').

unicode_translation(ring,'\x2218\'). % from Event-B

unicode_translation(typeof,'\x2982\'). % Event-B oftype operator

unset_atelierb_mode/0

unset_force_eventb_mode/0

unset_latex_mode/0

unset_translation_mode/1

unset_unicode_mode/0

use_colour_codes/0

var_not_really_modified/2

was_eventb_destructor/4

with_language_mode/2

Meta: with_language_mode(+,0)

with_translation_mode/2

Meta: with_translation_mode(+,0)

witness_intro/5

write_goal_with_max_depth/3

write_with_max_depth/4

Determinacy Checker

Determinacy Checker:

! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file extension('dll_path/dll_path') does not exist
! goal: absolute_file_name(extension('dll_path/dll_path'),_43503,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_terminal_colors,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_enter_debugger_upon_error,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_src_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_74345,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes_lib.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_43503,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(plspec_patch_libraries,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_53707,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_52043,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(json_parser) does not exist
! goal: absolute_file_name(extrasrc(json_parser),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/translate.pl')])

Name: =/2
Name: nl
Name: print/1
Name: !
Name: l_adapt_value_according_to_type/3	Module: translate
Name: convert_set_into_sequence/2	Module: translate
Name: ->/3
Name: maplist/3	Module: foo_error
Name: expand_custom_set_to_list/2	Module: custom_explicit_sets
Name: </2
Name: quick_avl_approximate_size/2	Module: avl_tools
Name: check_is_non_empty_avl/1	Module: avl_tools
Name: RECURSIVE_CALL/3	Module: translate
Name: add_internal_error/2	Module: foo_error
Name: var/1

Name: =/2
Name: add_internal_error/2	Module: foo_error
Name: true
Name: add_optional_typing_predicates/3	Module: translate
Name: ->/3

Name: pp_event_b_comprehension_set/6	Module: translate
Name: pp_expr2/5	Module: translate
Name: fuzz_list/2	Module: dev.pl
Name: pp_comprehension_set5/7	Module: translate
Name: pp_expr_indent/3	Module: translate
Name: translate_bexpr_typed/2	Module: banditfuzz
Name: pp_pred_nested/5	Module: translate
Name: report_ast/2	Module: banditfuzz

Name: add_labels_to_texpr/3	Module: foo_error
Name: create_label/4	Module: translate
Name: true
Name: =/2
Name: ->/3

Name: conjunct_predicates/2	Module: foo_error
Name: append/3
Name: remove_duplicate_predicates/3	Module: translate
Name: conjunction_to_list/2	Module: foo_error
Name: generate_typing_predicates/3	Module: translate
Name: =/2
Name: remove_already_typed_ids/3	Module: translate
Name: !

Name: pp_value_with_type/5	Module: translate
Name: translate_bvalue_with_type_and_limit2/4	Module: translate
Name: l_adapt_value_according_to_type/3	Module: translate
Name: translate_bvalue_with_type/3	Module: translate

Name: =/2
Name: add_typing_predicates/3	Module: translate
Name: is_truth/1	Module: foo_error
Name: ->/3
Name: get_preference/2	Module: preferences

Name: translate_subst2/3	Module: translate
Name: add_normal_typing_predicates/3	Module: translate

Name: combine_span_pred/5	Module: translate
Name: explain_simulation_error/4	Module: translate

Name: translate_in_mode/3	Module: translate
Name: integer_set_mapping/3	Module: translate

Name: RECURSIVE_CALL/3	Module: translate
Name: ppterm/3	Module: translate
Name: =/2

Name: format/2
Name: =/2
Name: ->/2
Name: write/1
Name: print_bvalue/1	Module: translate
Name: ground/1
Name: ->/3
Name: print_bexpr_or_subst/1	Module: translate
Name: is_texpr/1	Module: foo_error
Name: nonvar/1

Name: =/2
Name: eventb_translation_mode/0	Module: translate
Name: ->/3
Name: animation_minor_mode/1	Module: specfile
Name: !

Name: pp_pred_nested/5	Module: translate
Name: binary_infix_in_mode/4	Module: translate
Name: is_nontrivial_negation/4	Module: translate
Name: kernel_predicate/7	Module: kernel_mappings

Name: translate_in_mode/3	Module: translate
Name: binary_infix/4	Module: translate

Name: pretty_type2/4	Module: translate
Name: binary_infix_symbol/2	Module: translate
Name: pp_expr2/5	Module: translate
Name: render_operator_arg/3	Module: translate
Name: translate_prolog_constructor/2	Module: translate

Name: binary_infix_in_mode/4	Module: translate
Name: functor/3

Name: RECURSIVE_CALL/3	Module: translate
Name: is/2
Name: =/2
Name: </2
Name: ->/3

Name: =/2
Name: assertz/1
Name: gen_bugly_id/2	Module: translate
Name: genbuglynr/1	Module: translate
Name: !
Name: bugly_scramble_id_cache/2	dynamic predicate
Name: add_internal_error/2	Module: foo_error
Name: var/1

Name: pp_bugly_string/3	Module: translate
Name: opt_scramble_id/2	Module: translate
Name: ppatom_opt_scramble/3	Module: translate

Name: call_cleanup/2
Name: temporary_set_preference/3	Module: foo_error

Name: translate_bexpr_to_parseable/2	Module: translate
Name: translate_bvalue_to_parseable_aux/2	Module: translate
Name: translate_machine/3	Module: translate

Name: translate_subst2/3	Module: translate
Name: can_indent_texpr/1	Module: translate

Name: try_pp_b_state/4	Module: translate
Name: set_translation_constants/1	Module: translate

Name: ajoin/2	Module: foo_error
Name: get_terminal_colour_code/2	Module: tools_printing
Name: !
Name: colour_construct/2	Module: translate
Name: use_colour_codes/0	Module: translate

prob_prolog/src/translate.pl

Modules

Predicates of translate

Module Information

Dynamic Predicates: non_det_constants/2 deferred_set_constant/3 section_header_generated/1 print_additional_machine_info/0 latex_mode/0 unicode_mode/0 atelierb_mode/1 force_eventb_rodin_mode/0 bugly_scramble_id_cache/2 bugly_count/1 comment_level/1

5896 Lines

645 Predicates

Imported Modules: tools module_information lists codesio terms avl debug error_manager self_check b_global_sets bsyntaxtree bmachine_structure ordsets preferences clpfd

126 Exports

36 specified Imports

Predicates:

Name: RECURSIVE_CALL/2	Module: translate
Name: lub_state/3	Module: translate
Name: visited_expression/2	Module: state_space
Name: assertz/1
Name: =/2
Name: ->/3
Name: adapt_state/3	Module: translate

Name: translate_in_mode/3	Module: translate
Name: constants/2	Module: translate

Name: get_texpr_expr/2	Module: foo_error
Name: get_section/3	Module: foo_error
Name: animation_minor_mode/1	Module: specfile
Name: animation_mode/1	Module: specfile

Name: ajoin_with_sep/3	Module: foo_error
Name: maplist/3	Module: foo_error

Name: convert_avlset_into_sequence2/3	Module: translate
Name: eventb_translation_mode/0	Module: translate
Name: not/1

Name: pp_value/4	Module: translate
Name: convert_set_into_sequence1/2	Module: translate
Name: pp_tla_value/4	Module: translate

Name: convert_event2/4	Module: translate
Name: in_parallel/2	Module: translate
Name: get_texpr_expr/2	Module: foo_error

Name: convert_eventop/2	Module: translate
Name: convert_eventb_classicalb/2	Module: translate

Name: create_texpr/4	Module: foo_error
Name: !
Name: is_truth/1	Module: foo_error

Name: convert_event/3	Module: translate
Name: select_section/5	Module: foo_error
Name: maplist/3	Module: foo_error