Module Matcher.Terms

module Terms: sig .. end
Representations of expressions

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




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.

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