This library contains the set of basic properties used by the builtin predicates, and which constitute the basic data types and properties of the language. They are intented to be used as properties in assertions (for both runtime and compile time checking).
Note that most of those properties can be used directly from goals as type testing builtins, and they should be correct when terms are sufficiently instantiated. Calling with uninstantiated terms have undefined behaviour (failure or non termination, depending on the type). Please use the run-time checking facilities (inst/2 and compat/2) to ensure well-defined behaviour. For low-level instantiation checks we encourage the use term_typing builtins.
X is any term.
T is an integer.
T is a non-negative integer.
T is a float.
T is a number.
T is an atom.
T is a compound term.
T is ground.
T is a ground compound term.
T is an atomic term (an atom or a number).
T is a term which represents a goal, i.e., an atom or a structure.
M is an internal module identifier
X specifies the type and associativity of an operator.
list(). list([_1|L]) :- list(L).
L is a list.
L is a list, and for all its elements, T holds.
L is a list of Ts.
L is T or a nested list of Ts. Note that if T is term, this type is equivalent to term, this fact explain why we do not have a nlist/1 type.
X is an element of L.
S is a sequence of Ts.
S is a sequence or list of Ts.
T is an integer which is a character code.
T is a string (a list of character codes).
P is a Name/Arity structure denoting a predicate name:
predname(P/A) :- atm(P), nnegint(A).
P is a predicate name.
T is an atom or a list of atoms.
Term is compatible with Prop.
Term is instantiated enough to satisfy Prop.
Complies with the ISO-Prolog standard.
V is not further instantiated.
Declares that G is side-effect free (if its execution has no observable result other than its success, its failure, or its abortion), soft (if its execution may have other observable results which, however, do not affect subsequent execution, e.g., input/output), or hard (e.g., assert/retract).
G is side-effect X.
Defines a regular type.
This predicate is understood natively by CiaoPP.
This predicate is understood natively by CiaoPP as Key.
Equivalent to rtcheck(G, complete).
The runtime check of this property is Status.
G is not checked during run-time checking.
Goal is evaluable at compile-time.
Goal1 is equivalent to Goal2.
Goal is binding insensitive.
Goal is error free.
Goal should be memoized (not unfolded).
Vars should be filtered during global control).
Define the valid flag values
Goal will be filtered in partial evaluation time according to the PE types defined in the assertion.