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.