Functor Acsym.Make


module Make: functor (Sig : SIG) -> TERM
Canonizer for a theory with one AC symbol, say *. A term a is said to be in in canonical form if it is of the form x1 * (x2 * (x3 * ... (xn-1 * xn)...)) with xi either variables or terms with a top-level symbol disequal from *. Furthermore, xi << xj for i < j.

For canonical terms a, b it is the case that Term.eqa b iff AC |= a = b, that is a and b are valid in the theory AC.

Parameters:
Sig : Acsym.SIG

val d_interp : Term.t -> Term.t * Term.t
If a is of the form b*c, then d_interp a returns (b, c).
Parameters:
? : Term.t
val is_interp : Term.t -> bool
is_interp a holds iff a is of the form b*c.
Parameters:
? : Term.t
val make : Term.t -> Term.t -> Term.t
For canonical a, b, make a b returns a canonical term c with AC |= c = a * b.
Parameters:
? : Term.t
? : Term.t
val iterate : Term.t -> int -> Term.t
For n>=1, iterate a n iterates make a n-1 times. We sometimes write a^n to denote this term.
Parameters:
? : Term.t
? : int
val multiplicity : Term.t -> Term.t -> int
multiplicity x a counts the number of interpreted occurrences of x in a.
Parameters:
? : Term.t
? : Term.t
val decompose : Term.t -> (Term.t * int) * Term.t option
Decompose x*x*...*x*y*.... into (x, n) with n the multiplicity of x in a and y*....
Parameters:
? : Term.t
val fold : (Term.t -> int -> 'a -> 'a) -> Term.t -> 'a -> 'a
If a is of the form x1^m1*(x2^m2*...*xn^mn), then fold f a e is f x1 m1 (f x2 m2 (... (f xn mn e)...)).
Parameters:
? : Term.t -> int -> 'a -> 'a
? : Term.t
? : 'a
val iter : (Term.t -> int -> unit) -> Term.t -> unit
If a is of the form x1^m1*(x2^m2*...*xn^mn), then iter f a is f x1 m1; f x2 m2; ...; f xn mn.
Parameters:
? : Term.t -> int -> unit
? : Term.t
val sigma : Sym.t -> Term.t list -> Term.t
If f equals *, then sigma f [a1; a2] reduces to make a1 a2; otherwise the uninterpreted application f(a1, a2) is built.
Parameters:
? : Sym.t
? : Term.t list
val map : (Term.t -> Term.t) -> Term.t -> Term.t
map f a applies f at uninterpreted positions and recanonizes the result.
Parameters:
? : Term.t -> Term.t
? : Term.t