Module TRS

module TRS: sig .. end
Get syntax definitions from a TRS.

type trs 
val syntax_defs_of_sys : trs -> (string * SyntaxDef.syntax_def) list
Get syntax definitions from a TRS.
val set_vals_of_sys : trs -> (string * Term.term * Term.term) list
Get set values (chronologically) from a TRS.

Operating on the TRS


val update_on_term : string -> Term.term -> trs -> trs
val normalise_with_sys : trs -> Term.term -> Term.term
val parse_with_sys : trs -> string -> Term.term list
val parse_disambiguate_with_sys : bool -> trs -> string -> Term.term list
val message_for_term : Term.decls_set ->
(string * SyntaxDef.syntax_def) list ->
string -> bool -> bool -> Term.term * Term.term -> string
exception FAILED_PARSE_OR_EXN of string
val process_with_system : string ->
bool ->
trs ->
string -> bool -> (string -> unit) -> trs * Term.term list * string
val basic_system : (unit -> trs) Pervasives.ref
val step_shell : string ->
bool ->
trs ->
(unit -> char) ->
bool -> Term.term list Pervasives.ref -> (string -> unit) -> trs
A full one step of the computation. The channel (unit -> char) argument should raise End_of_file on end of channel, as does input_char.
val run_shell : string ->
bool ->
trs Pervasives.ref ->
(unit -> char) ->
bool -> Term.term list Pervasives.ref -> (string -> unit) -> unit
A full run of the TRS computation. The channel (unit -> char) argument should raise End_of_file on end of channel, as does input_char. The trs reference gets updated to the result, and the term list reference to the list of parsed terms.
val run_shell_str : ?libpath:string ->
?sys:trs -> string -> string * trs * Term.term list
Simplified interface to TRS computation, returns the messages, resulting system and the list of parsed terms, chronologically.