Module Export.HrsSource

This module provides a function to translate a signature to the HRS format used in the confluence competition.

print_sym ppf s outputs the fully qualified name of s to ppf. The name is prefixed by "c_", and modules are separated with "_", not ".".

Sourceval print_term : bool -> Core.Term.term Lplib.Base.pp

print_patt ppf p outputs TPDB format corresponding to the pattern p, to ppf.

print_rule ppf lhs rhs outputs the rule declaration lhs->rhs to ppf

Sourceval print_sym_rule : Format.formatter -> Core.Term.sym -> Core.Term.rule -> unit

print_sym_rule ppf s r outputs the rule declaration corresponding r (on the symbol s), to ppf.

Sourceval to_HRS : Format.formatter -> Core.Sign.t -> unit

to_HRS ppf sign outputs a TPDB representation of the rewriting system of the signature sign to ppf.