package trs

  1. Overview
  2. Docs
package trs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module TrsSource

A library for parsing and emitting TRS.

This library provides functionality for handling the TRS format. With to_string and of_string, you can convert between a TRS string and the trs type. The specifications for the TRS format can be found here.

Types

Sourcetype trs = {
  1. var : id list option;
  2. rules : rule list;
  3. comment : string option;
}

trs is the representation of TRS format. Each record field corresponds to section if TRS: VAR, RULES, and COMMENT.

Sourceand rule = term * term

rule is a rewrite rule. (left, right) represents left -> right

Sourceand term =
  1. | Var of id
  2. | App of id * term list

A term of TRS.

Sourceand id = string

Identifier in terms.

Parsers and serialisers

Sourceval of_string : string -> (trs, exn) result

of_string s parses s into a trs value.

Sourceval of_string_exn : string -> trs

of_string s parses s into trs. Raises Invalid_argument if there is an error.

Sourceval to_string : trs -> string

to_string trs converts a trs value into a string.

Printers

Sourceval string_of_trs : trs -> string

The same as to_string.

Sourceval string_of_rule : rule -> string
Sourceval string_of_term : term -> string
Sourceval string_of_id : id -> string