Loosely closed terms.

Non-structural, machine dependent, but fast comparison and efficient merges

Non-structural, machine dependent, but fast comparison and efficient merges

Structuraly ordered, but less efficient access and non-linear merges

Structuraly ordered, but less efficient access and non-linear merges

Return true if and only the term is e_true. Constant time.

Constant time.

Constant time.

Boolean or Property

Integer sort

Real sort

Integer or Real sort

Computes equality

Same as are_equal is Yes

Same as are_equal is No

Same as e_lt is e_true

Same as e_leq is e_true

Constant time

Constant time

Constant time

position of a subterm in a term.

• raises Invalid_argument

  on Bvar and Bind

Bind the given variable if it appears free in the term, or return the term unchanged.

Opens the top-most bound variable with a (fresh) variable. Can be only applied on top-most lc-term from `Bind(_,_,_)`, thanks to typing.

Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default). The pool must contain all free variables of the term.

Closes all specified binders

The environment sigma must be prepared with the desired substitution. Its pool of fresh variables must covers the entire domain and co-domain of the substitution, and the transformed values.

All bound variables are under their binder

Calling this function is unsafe unless the term is lc_closed

Similar to f_iter but exposes non-closed sub-terms of `Bind` as regular term values instead of lc_term ones.

Pass and open binders, maps its direct sub-terms and then close then opened binders Raises Invalid_argument in case of a bind-term without pool. The optional pool must contain all free variables of the term.

Iterates over its direct sub-terms (pass and open binders) Raises Invalid_argument in case of a bind-term without pool. The optional pool must contain all free variables of the term.

Try to extract a type of term. Parameterized by optional extractors for field and functions. Extractors may raise Not_found ; however, they are only used when the provided kinds for fields and functions are not precise enough.

• parameter field

  type of a field value

• parameter record

  type of the record containing a field

• parameter call

  type of the values returned by the function

• raises Not_found

  if no type is found.

Register a simplifier for function f. The computation code may raise Not_found, in which case the symbol is not interpreted.

If f is an operator with algebraic rules (see type operator), the children are normalized before builtin call.

Highest priority is 0. Recursive calls must be performed on strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

• before 22.0-Titanium

  the optional force parameter does not exist

Register a builtin for rewriting f a1..an into f b1..bm.

This is short cut for set_builtin, where the head application of f avoids to run into an infinite loop.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

• before 22.0-Titanium

  the optional force parameter does not exist

set_builtin_get f rewrite register a builtin for rewriting (f a1..an)[k1]..[km] into rewrite (a1..an) (k1..km).

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

• before 22.0-Titanium

  the optional force parameter does not exist

• before 28.0-Nickel

  one-dimensional access only

Register a builtin for simplifying (f e…).fd expressions. Must only use recursive comparison for strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

• since 28.0-Nickel

Register a builtin equality for comparing any term with head-symbol. Must only use recursive comparison for strictly smaller terms. The recognized term with head function symbol is passed first.

Highest priority is 0. Recursive calls must be performed on strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

• before 22.0-Titanium

  the optional force parameter does not exist

Register a builtin for comparing any term with head-symbol. Must only use recursive comparison for strictly smaller terms. The recognized term with head function symbol can be on both sides. Strict comparison is automatically derived from the non-strict one.

Highest priority is 0. Recursive calls must be performed on strictly smaller terms.

The force parameters defaults to false, when it is true, if there exist another builtin, it is replaced with the new one. Use with care.

• before 22.0-Titanium

  the optional force parameter does not exist

Knowing h, consequence h a returns b such that h -> (a<->b)

unique identifier (stored in t)

constant access (stored in t)

physical equality

atoms are lower than complex terms ; otherwise, sorted by id.

Informal size

No bound variables

Constants, variables, functions of arity 0

Constants and variables

Constants only

internal id

head symbol with children id's

head symbol with children id's

Occurrence check. is_subterm a b returns true iff a is a subterm of b. Optimized wrt shared subterms, term size, and term variables.

Computes the sub-terms that appear several times. shared marked linked e returns the shared subterms of e.

The list of shared subterms is consistent with order of definition: each trailing terms only depend on heading ones.

The traversal is controlled by two optional arguments:

• shared those terms are not traversed (considered as atomic, default to none)
• shareable those terms (is_simple excepted) that can be shared (default to all)
• subterms those sub-terms a term to be considered during traversal (lc_iter by default)

Mark a term to be printed

Mark a term to be explicitly shared

Returns a list of terms to be shared among all shared or marked subterms. The order of terms is consistent with definition order: head terms might be used in tail ones.