Module Matcher.Terms

module Terms: sig .. end

Representations of expressions

The module Matcher.Terms defines two different types for expressions.

a public type Matcher.Terms.t that represents abstract syntax trees of expressions with binary associative and commutative operators
a private type Matcher.Terms.nf_term, corresponding to a canonical representation for the above terms modulo AACU. The construction functions on this type ensure that these terms are in normal form (that is, no sum can appear as a subterm of the same sum, no trailing units, lists corresponding to multisets are sorted, etc...).

Abstract syntax tree of terms and patterns

We represent both terms and patterns using the following datatype.

Values of type symbol are used to index symbols. Typically, given two associative operations (^) and ( * ), and two morphisms f and g, the term f (a^b) (a*g b) is represented by the following value Sym(0,[| Dot(1, Sym(2,[||]), Sym(3,[||])); Dot(4, Sym(2,[||]), Sym(5,[|Sym(3,[||])|])) |]) where the implicit symbol environment associates f to 0, (^) to 1, a to 2, b to 3, ( * ) to 4, and g to 5,

Accordingly, the following value, that contains "variables" Sym(0,[| Dot(1, Var x, Unit (1); Dot(4, Var x, Sym(5,[|Sym(3,[||])|])) |]) represents the pattern forall x, f (x^1) (x*g b). The relationship between 1 and ( * ) is only mentionned in the units table.

type t =

`\|`	`Dot of (Matcher.symbol * t * t)`
`\|`	`Plus of (Matcher.symbol * t * t)`
`\|`	`Sym of (Matcher.symbol * t array)`
`\|`	`Var of Matcher.var`
`\|`	`Unit of Matcher.symbol`

val equal_aac : Matcher.units -> t -> t -> bool

Test for equality of terms modulo AACU (relies on the following canonical representation of terms). Note than two different units of a same operator are not considered equal.

val map_syms : (Matcher.symbol -> Matcher.symbol) -> t -> t

Normalised terms (canonical representation)

A term in normal form is the canonical representative of the equivalence class of all the terms that are equal modulo AACU. This representation is only used internally; it is exported here for the sake of completeness

type nf_term

Comparisons

val nf_term_compare : nf_term -> nf_term -> int

val nf_equal : nf_term -> nf_term -> bool

Printing function

val sprint_nf_term : nf_term -> string

Conversion functions

val term_of_t : Matcher.units -> t -> nf_term

we have the following property: a and b are equal modulo AACU iif nf_equal (term_of_t a) (term_of_t b) = true

val t_of_term : nf_term -> t