Module ITM_main (.ml)

module ITM_main: sig .. end

For expanding formulas and proofs containing defined expressions, replacing each defined expression with its defining expression.

Parse

exception Parse_error of string

val items_of_file : string -> ITM_types.t_itm list

If path is the path of a file whose content conforms to the grammar specified in items.txt, then items_of_file path evaluates to a list of type ITM_types.t_itm, and otherwise raises an exception.

Print

val string_of_item : ITM_types.t_itm -> string

val string_of_items : ITM_types.t_itm list -> string

Expand

exception Invalid_definition of ITM_types.t_itm

exception Cannot_replace_var_with_term_containing_var_in_fml of FML_types.t_var * FML_types.t_term * FML_types.t_var * FML_types.t_fml

val subst_free_vars_in_fml_with_terms : (FML_types.t_var -> FML_types.t_term) -> FML_types.t_fml -> FML_types.t_fml

subst_free_vars_in_fml_with_terms subst fml evaluates to the result of simultaneously replacing every free variable in fml with a term according to the function subst: t_var -> t_term.

Raises exception Cannot_replace_var_with_term_containing_var_in_fml (var1, term, var2, fml) if term contains a variable var2 that will be bound if term replaces var1 in fml.

val expand_items : ITM_types.t_itm list -> ITM_types.t_itm list

Recursively expands each item on a list according to the definitions preceding it (with the most immediate predecessors being applied first).

For instance, if the head of the list is a definition, the last operation is to expand every element in the tail according to that definition.

Raises Invalid_definition item if item represents an invalid definition, e.g.

P(x) := ∃yQ(y,z)

val expand_file : string -> ITM_types.t_itm list

expand_file path evaluates to expand_items (items_of_file path).