module Term: sig end
Datatype of terms
Author(s): Harald Ruess
A term is either a
- an injection of a variable
x (Var.t) or an
- application of a function symbol
f (Sym.t) to a list of
argument terms l.
Each term a has an integer value hash a associated with it.
type t =
Notice: all terms should be build using the constructors below.
This type definition is only visible for convenience to allow for
pattern matching on terms.
type trm = t
Synonym for avoiding name clashes
val hash : t -> int
hash a returns a hash value such that
Term.eqa b implies
hash a = hash b. Furthermore,
hash restricted to variables is
injective.
val pp : t Pretty.printer
Pretty-printing of terms. The exact outcome depends on the
value
Pretty.flag.
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
a |
: |
t
|
|
val to_string : t -> string
Pretty-printing a term to a string.
to_string a is synonymous
with
Pretty.to_stringpp a.
module Var: sig end
Operations on term variables.
module App: sig end
Operations on term applications.
val is_var : t -> bool
is_var a holds iff a is of the form Var _.
val is_app : t -> bool
is_app a holds iff a is of the form App _.
val is_const : t -> bool
is_const a holds iff a is of the form App(_,[], _).
val is_pure : Th.t -> t -> bool
is_pure i a holds iff all function symbols in
a are of
theory
i (see
Th.t).
type status =
| |
Variable |
| |
Pure of Th.t |
| |
Mixed of Th.t * t |
Facts are partitioned into
- facts over variable terms
- facts over pure terms with all function symbols drawn
from a single theory
i
- facts over mixed terms.
val status : t -> status
status a classifies term
a into one of:
- variables
- pure terms with all function symbols drawn from a single theory
i
- mixed terms. In this case, a maximal pure term is retured.
val is_equal : t -> t -> Three.t
is_equal a b returns
Three.Yes if Term.eqa b holds,Three.No is a and b are two distinct constants in some theory th, andThree.X if none of the above holds.
val eq : t -> t -> bool
eq a b holds iff a and b are syntactically equal.
This comparison is linear in the size of a and b.
val eql : t list -> t list -> bool
eql al bl holds iff al and bl are of the
form a1;...;an and b1;...;bn, respectively, and
if eq ai bi holds for all i.
val cmp : t -> t -> int
cmp a b realizes a total ordering on terms. It returns
0 if
eq a b holds. Values less than
0 are interpreted
as '
a is less than
b' and values greater than
0 as
'
a is greater than
b'. Variables are greater than
applications, variables
Var(x) and
Var(y) are ordered
according to
Var.cmpx y
(in particular, internal variables are always greater than
external ones), and function applications
App(f, al) and
App(g, bl) are ordered using a lexicographic ordering
on the function symbols
f and
g as given by
Sym.cmpf g
and the orderings on respective terms in the argument lists
al
and
bl.
val compare : t -> t -> int
Total comparison on term which is designed to be fast.
Does not necessarily coincide with
Term.cmp.
val (<<<) : t -> t -> bool
a <<< b iff cmp a b <= 0.
val orient : t * t -> t * t
orient (a, b) is (b, a) if b is greater than a,
and (a, b) otherwise.
val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
Fold operator fold f a e on terms applies
argument function f to all variables in a
and accumulates the results starting with e.
Thus, if vars_of a is of the form {x1,...,xn}
with the order of variables unspecified,
then fold f a e reduces to f x1 (f x2 ... (f xn e)).
| Parameters: |
|
f |
: |
t -> 'a -> 'a
|
|
a |
: |
t
|
|
acc |
: |
'a
|
|
val iter : (t -> unit) -> t -> unit
Iteration operator on terms.
val for_all : (t -> bool) -> t -> bool
forall p a holds if p x for all variables in a.
val mapl : (t -> t) -> t list -> t list
Mapping over list of terms. Avoids unnecessary consing.
val choose : (t -> bool) -> t -> t
choose p a chooses a variable of a which satisfies predicate p.
val subterm : t -> t -> bool
subterm a b holds if a is a subterm of b.
val occurs : t -> t -> bool
occurs a b holds if term a occurs in b.
val assq : t -> (t * 'a) list -> 'a
Association lists for terms.
module Set2: sig end
Set of pair of terms.
module Set: sig end
Set of terms.
module Map: sig end
Maps with terms as keys.
val vars_of : t -> Var.Set.t
Return set of variables.
module Equal: sig end
Following to be deprecated.
type apply = t * t -> t -> t
type map = (t -> t) -> t -> t
module Subst: sig end
Term Substitutions