# Basic data types and properties

**Author(s):**Daniel Cabeza, Manuel Hermenegildo.

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 can be used both as type testing builtins within programs (by calling them explicitly) and as properties in assertions.

## Usage and interface

**Library usage:**

These predicates are builtin in Ciao, so nothing special has to be done to use them.**Exports:***Properties:*`member/2`,`compat/2`,`inst/2`,`iso/1`,`deprecated/1`,`not_further_inst/2`,`sideff/2`,`regtype/1`,`native/1`,`native/2`,`no_rtcheck/1`,`eval/1`,`equiv/2`,`bind_ins/1`,`error_free/1`,`memo/1`,`filter/2`,`pe_type/1`.*Regular Types:*`term/1`,`int/1`,`nnegint/1`,`flt/1`,`num/1`,`atm/1`,`struct/1`,`gnd/1`,`gndstr/1`,`constant/1`,`callable/1`,`operator_specifier/1`,`list/1`,`list/2`,`nlist/2`,`sequence/2`,`sequence_or_list/2`,`character_code/1`,`string/1`,`num_code/1`,`predname/1`,`atm_or_atm_list/1`,`flag_values/1`.

**Other modules used:***System library modules:*`assertions/native_props`,`terms_check`.

## Documentation on exports

**General properties:**

`term(X)`

*The following properties hold globally:*

(basic_props:sideff/2)term(X) is side-effect free.

`term(X)`

*The following properties hold globally:*

(basic_props:eval/1)term(X) is evaluable at compile-time.

`term(X)`

*The following properties hold globally:*

(basic_props:equiv/2)term(X) is equivalent to true.

**Usage:** `term(X)`

*Description:*X is any term.*The following properties hold globally:*

(basic_props:native/1)This predicate is understood natively by CiaoPP.

`[-2^2147483616, 2^2147483616)`. Thus for all practical purposes, the range of integers can be considered infinite.

**General properties:**

`int(T)`

*The following properties hold globally:*

(basic_props:sideff/2)int(T) is side-effect free.

`int(T)`

*If the following properties hold at call time:*

(term_typing:nonvar/1)T is currently a term which is not a free variable.*then the following properties hold globally:*

(basic_props:eval/1)int(T) is evaluable at compile-time.

(native_props:is_det/1)All calls of the form int(T) are deterministic.

`int(T)`

*The following properties hold upon exit:*

(basic_props:int/1)T is an integer.

*The following properties hold globally:*

(native_props:test_type/2)Indicates the type of test that a predicate performs. Required by the nonfailure analyisis.

**Usage:** `int(T)`

*Description:*T is an integer.*The following properties hold globally:*

(basic_props:native/1)This predicate is understood natively by CiaoPP.

**General properties:**

`nnegint(T)`

*The following properties hold globally:*

(basic_props:sideff/2)nnegint(T) is side-effect free.

`nnegint(T)`

*If the following properties hold at call time:*

(term_typing:nonvar/1)T is currently a term which is not a free variable.*then the following properties hold globally:*

(basic_props:eval/1)nnegint(T) is evaluable at compile-time.

`nnegint(T)`

*The following properties hold upon exit:*

(basic_props:nnegint/1)T is a non-negative integer.

*The following properties hold globally:*

(native_props:test_type/2)Indicates the type of test that a predicate performs. Required by the nonfailure analyisis.

**Usage:** `nnegint(T)`

*Description:*T is a non-negative integer.*The following properties hold globally:*

(basic_props:native/1)This predicate is understood natively by CiaoPP.

`double`type, typically

`[4.9e-324, 1.8e+308]`(plus or minus). There are also three special values: Infinity, either positive or negative, represented as

`1.0e1000`and

`-1.0e1000`; and Not-a-number, which arises as the result of indeterminate operations, represented as

`0.Nan`

**General properties:**

`flt(T)`

*The following properties hold globally:*

(basic_props:sideff/2)flt(T) is side-effect free.

`flt(T)`

*If the following properties hold at call time:*

(term_typing:nonvar/1)T is currently a term which is not a free variable.*then the following properties hold globally:*

(basic_props:eval/1)flt(T) is evaluable at compile-time.

(native_props:is_det/1)All calls of the form flt(T) are deterministic.

`flt(T)`

*The following properties hold upon exit:*

(basic_props:flt/1)T is a float.

*The following properties hold globally:*

(native_props:test_type/2)Indicates the type of test that a predicate performs. Required by the nonfailure analyisis.

**Usage:** `flt(T)`

*Description:*T is a float.*The following properties hold globally:*

(basic_props:native/1)This predicate is understood natively by CiaoPP.

**General properties:**

`num(T)`

*The following properties hold globally:*

(basic_props:sideff/2)num(T) is side-effect free.

(basic_props:bind_ins/1)num(T) is binding insensitive.

`num(T)`

*If the following properties hold at call time:*

(term_typing:nonvar/1)T is currently a term which is not a free variable.*then the following properties hold globally:*

(basic_props:eval/1)num(T) is evaluable at compile-time.

(native_props:is_det/1)All calls of the form num(T) are deterministic.

`num(T)`

*The following properties hold upon exit:*

(basic_props:num/1)T is a number.

*The following properties hold globally:*

(native_props:test_type/2)Indicates the type of test that a predicate performs. Required by the nonfailure analyisis.

**Usage:** `num(T)`

*Description:*T is a number.*The following properties hold globally:*

(basic_props:native/1)This predicate is understood natively by CiaoPP.

**General properties:**

`atm(T)`

*The following properties hold globally:*

(basic_props:sideff/2)atm(T) is side-effect free.

`atm(T)`

*If the following properties hold at call time:*

(term_typing:nonvar/1)T is currently a term which is not a free variable.*then the following properties hold globally:*

(basic_props:eval/1)atm(T) is evaluable at compile-time.

(native_props:is_det/1)All calls of the form atm(T) are deterministic.

`atm(T)`

*The following properties hold upon exit:*

(basic_props:atm/1)T is an atom.

*The following properties hold globally:*

(native_props:test_type/2)Indicates the type of test that a predicate performs. Required by the nonfailure analyisis.

**Usage:** `atm(T)`

*Description:*T is an atom.*The following properties hold globally:*

(basic_props:native/1)This predicate is understood natively by CiaoPP.

**General properties:**

`struct(T)`

*The following properties hold globally:*

(basic_props:sideff/2)struct(T) is side-effect free.

`struct(T)`

*If the following properties hold at call time:*

(term_typing:nonvar/1)T is currently a term which is not a free variable.*then the following properties hold globally:*

(basic_props:eval/1)struct(T) is evaluable at compile-time.

`struct(T)`

*The following properties hold upon exit:*

(basic_props:struct/1)T is a compound term.

**Usage:** `struct(T)`

*Description:*T is a compound term.*The following properties hold globally:*

(basic_props:native/1)This predicate is understood natively by CiaoPP.

**General properties:**

`gnd(T)`

*The following properties hold globally:*

(basic_props:sideff/2)gnd(T) is side-effect free.

`gnd(T)`

*If the following properties hold at call time:*

(term_typing:ground/1)T is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)gnd(T) is evaluable at compile-time.

(native_props:is_det/1)All calls of the form gnd(T) are deterministic.

`gnd(T)`

*The following properties hold upon exit:*

(basic_props:gnd/1)T is ground.

*The following properties hold globally:*

(native_props:test_type/2)Indicates the type of test that a predicate performs. Required by the nonfailure analyisis.

**Usage:** `gnd(T)`

*Description:*T is ground.*The following properties hold globally:*

(basic_props:native/1)This predicate is understood natively by CiaoPP.

**General properties:**

`gndstr(T)`

*The following properties hold globally:*

(basic_props:sideff/2)gndstr(T) is side-effect free.

`gndstr(T)`

*If the following properties hold at call time:*

(term_typing:ground/1)T is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)gndstr(T) is evaluable at compile-time.

(native_props:is_det/1)All calls of the form gndstr(T) are deterministic.

`gndstr(T)`

*The following properties hold upon exit:*

(basic_props:gndstr/1)T is a ground compound term.

**Usage:** `gndstr(T)`

*Description:*T is a ground compound term.*The following properties hold globally:*

(basic_props:native/1)This predicate is understood natively by CiaoPP.

**General properties:**

`constant(T)`

*The following properties hold globally:*

(basic_props:sideff/2)constant(T) is side-effect free.

`constant(T)`

*If the following properties hold at call time:*

(term_typing:nonvar/1)T is currently a term which is not a free variable.*then the following properties hold globally:*

(basic_props:eval/1)constant(T) is evaluable at compile-time.

(native_props:is_det/1)All calls of the form constant(T) are deterministic.

`constant(T)`

*The following properties hold upon exit:*

(basic_props:constant/1)T is an atomic term (an atom or a number).

**Usage:** `constant(T)`

*Description:*T is an atomic term (an atom or a number).

**General properties:**

`callable(T)`

*The following properties hold globally:*

(basic_props:sideff/2)callable(T) is side-effect free.

`callable(T)`

*If the following properties hold at call time:*

(term_typing:nonvar/1)T is currently a term which is not a free variable.*then the following properties hold globally:*

(basic_props:eval/1)callable(T) is evaluable at compile-time.

(native_props:is_det/1)All calls of the form callable(T) are deterministic.

`callable(T)`

*The following properties hold upon exit:*

(term_typing:nonvar/1)T is currently a term which is not a free variable.

**Usage:** `callable(T)`

*Description:*T is a term which represents a goal, i.e., an atom or a structure.

`xfx`- Infix, non-associative: it is a requirement that both of the two subexpressions which are the arguments of the operator must be of
*lower*precedence than the operator itself. `xfy`- Infix, right-associative: only the first (left-hand) subexpression must be of lower precedence; the right-hand subexpression can be of the
*same*precedence as the main operator. `yfx`- Infix, left-associative: same as above, but the other way around.
`fx`- Prefix, non-associative: the subexpression must be of
*lower*precedence than the operator. `fy`- Prefix, associative: the subexpression can be of the
*same*precedence as the operator. `xf`- Postfix, non-associative: the subexpression must be of
*lower*precedence than the operator. `yf`- Postfix, associative: the subexpression can be of the
*same*precedence as the operator.

**General properties:**

`operator_specifier(X)`

*The following properties hold globally:*

(basic_props:sideff/2)operator_specifier(X) is side-effect free.

`operator_specifier(X)`

*If the following properties hold at call time:*

(term_typing:nonvar/1)X is currently a term which is not a free variable.*then the following properties hold globally:*

(basic_props:eval/1)operator_specifier(X) is evaluable at compile-time.

(native_props:is_det/1)All calls of the form operator_specifier(X) are deterministic.

(native_props:relations/2)Goal operator_specifier(X) produces 7 solutions.

`operator_specifier(T)`

*The following properties hold upon exit:*

(basic_props:operator_specifier/1)T specifies the type and associativity of an operator.

**Usage:** `operator_specifier(X)`

*Description:*X specifies the type and associativity of an operator.

`'.'/2`, and its end is the atom

`[]`. Defined as

list([]). list([_1|L]) :- list(L).

**General properties:**

`list(L)`

*The following properties hold globally:*

(basic_props:sideff/2)list(L) is side-effect free.

`list(L)`

*If the following properties hold at call time:*

(term_typing:ground/1)L is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)list(L) is evaluable at compile-time.

(native_props:is_det/1)All calls of the form list(L) are deterministic.

`list(T)`

*The following properties hold upon exit:*

(basic_props:list/1)T is a list.

**Usage:** `list(L)`

*Description:*L is a list.

`list(L,T)`

L is a list, and for all its elements, T holds.

*Meta-predicate* with arguments: `list(?,(pred 1))`.

**General properties:** `list(L,T)`

*The following properties hold globally:*

(basic_props:sideff/2)list(L,T) is side-effect free.

`list(L,T)`

*If the following properties hold at call time:*

(term_typing:ground/1)L is currently ground (it contains no variables).

(term_typing:ground/1)T is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)list(L,T) is evaluable at compile-time.

`list(X,T)`

*The following properties hold upon exit:*

(basic_props:list/1)X is a list.

**Usage:** `list(L,T)`

*Description:*L is a list of Ts.

*Meta-predicate*with arguments:

`nlist(?,(pred 1))`.

**General properties:**

`nlist(L,T)`

*The following properties hold globally:*

(basic_props:sideff/2)nlist(L,T) is side-effect free.

`nlist(L,T)`

*If the following properties hold at call time:*

(term_typing:ground/1)L is currently ground (it contains no variables).

(term_typing:ground/1)T is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)nlist(L,T) is evaluable at compile-time.

`nlist(X,T)`

*The following properties hold upon exit:*

(basic_props:term/1)X is any term.

**Usage:** `nlist(L,T)`

*Description:*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

**General properties:**

`member(X,L)`

*The following properties hold globally:*

(basic_props:sideff/2)member(X,L) is side-effect free.

(basic_props:bind_ins/1)member(X,L) is binding insensitive.

`member(X,L)`

*If the following properties hold at call time:*

(basic_props:list/1)L is a list.*then the following properties hold globally:*

(basic_props:eval/1)member(X,L) is evaluable at compile-time.

`member(_X,L)`

*The following properties hold upon exit:*

(basic_props:list/1)L is a list.

`member(X,L)`

*If the following properties hold at call time:*

(term_typing:ground/1)L is currently ground (it contains no variables).*then the following properties hold upon exit:*

(term_typing:ground/1)X is currently ground (it contains no variables).

**Usage:** `member(X,L)`

*Description:*X is an element of L.

`','/2`. For example,

`a, b, c`is a sequence of three atoms,

`a`is a sequence of one atom.

*Meta-predicate*with arguments:

`sequence(?,(pred 1))`.

**General properties:**

`sequence(S,T)`

*The following properties hold globally:*

(basic_props:sideff/2)sequence(S,T) is side-effect free.

`sequence(S,T)`

*If the following properties hold at call time:*

(term_typing:ground/1)S is currently ground (it contains no variables).

(term_typing:ground/1)T is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)sequence(S,T) is evaluable at compile-time.

`sequence(E,T)`

*The following properties hold upon exit:*

(term_typing:nonvar/1)E is currently a term which is not a free variable.

(term_typing:ground/1)T is currently ground (it contains no variables).

**Usage:** `sequence(S,T)`

*Description:*S is a sequence of Ts.

*Meta-predicate*with arguments:

`sequence_or_list(?,(pred 1))`.

**General properties:**

`sequence_or_list(S,T)`

*The following properties hold globally:*

(basic_props:sideff/2)sequence_or_list(S,T) is side-effect free.

`sequence_or_list(S,T)`

*If the following properties hold at call time:*

(term_typing:ground/1)S is currently ground (it contains no variables).

(term_typing:ground/1)T is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)sequence_or_list(S,T) is evaluable at compile-time.

`sequence_or_list(E,T)`

*The following properties hold upon exit:*

(term_typing:nonvar/1)E is currently a term which is not a free variable.

(term_typing:ground/1)T is currently ground (it contains no variables).

**Usage:** `sequence_or_list(S,T)`

*Description:*S is a sequence or list of Ts.

**General properties:**

`character_code(T)`

*The following properties hold globally:*

(basic_props:sideff/2)character_code(T) is side-effect free.

`character_code(T)`

*If the following properties hold at call time:*

(term_typing:nonvar/1)T is currently a term which is not a free variable.*then the following properties hold globally:*

(basic_props:eval/1)character_code(T) is evaluable at compile-time.

`character_code(I)`

*The following properties hold upon exit:*

(basic_props:character_code/1)I is an integer which is a character code.

**Usage:** `character_code(T)`

*Description:*T is an integer which is a character code.

`"string"`is allowed, which is equivalent to

`[0's,0't,0'r,0'i,0'n,0'g]`or

`[115,116,114,105,110,103]`. There is also a special Ciao syntax when the list is not complete:

`"st"||R`is equivalent to

`[0's,0't|R]`.

**General properties:**

`string(T)`

*The following properties hold globally:*

(basic_props:sideff/2)string(T) is side-effect free.

`string(T)`

*If the following properties hold at call time:*

(term_typing:ground/1)T is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)string(T) is evaluable at compile-time.

`string(T)`

*The following properties hold upon exit:*

(basic_props:string/1)T is a string (a list of character codes).

**Usage:** `string(T)`

*Description:*T is a string (a list of character codes).

**General properties:**

`predname(P)`

*The following properties hold globally:*

(basic_props:sideff/2)predname(P) is side-effect free.

`predname(P)`

*If the following properties hold at call time:*

(term_typing:ground/1)P is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)predname(P) is evaluable at compile-time.

`predname(P)`

*The following properties hold upon exit:*

(basic_props:predname/1)P is a Name/Arity structure denoting a predicate name:predname(P/A) :- atm(P), nnegint(A).

**Usage:** `predname(P)`

*Description:*P is a Name/Arity structure denoting a predicate name:predname(P/A) :- atm(P), nnegint(A).

**General properties:**

`atm_or_atm_list(T)`

*The following properties hold globally:*

(basic_props:sideff/2)atm_or_atm_list(T) is side-effect free.

`atm_or_atm_list(T)`

*If the following properties hold at call time:*

(term_typing:ground/1)T is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)atm_or_atm_list(T) is evaluable at compile-time.

`atm_or_atm_list(T)`

*The following properties hold upon exit:*

(basic_props:atm_or_atm_list/1)T is an atom or a list of atoms.

**Usage:** `atm_or_atm_list(T)`

*Description:*T is an atom or a list of atoms.

`X`(i.e., a free variable),

`[Y|Z]`, and

`[Y,Z]`are all compatible with the regular type

`list/1`, whereas the terms

`f(a)`and

`[1|2]`are not.

*Meta-predicate*with arguments:

`compat(?,(pred 1))`.

**General properties:**

`compat(Term,Prop)`

*If the following properties hold at call time:*

(term_typing:ground/1)Term is currently ground (it contains no variables).

(term_typing:ground/1)Prop is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)compat(Term,Prop) is evaluable at compile-time.

**Usage:** `compat(Term,Prop)`

*Description:*Term is*compatible*with Prop

*Meta-predicate*with arguments:

`inst(?,(pred 1))`.

**General properties:**

`inst(Term,Prop)`

*The following properties hold globally:*

(basic_props:sideff/2)inst(Term,Prop) is side-effect free.

`inst(Term,Prop)`

*If the following properties hold at call time:*

(term_typing:ground/1)Term is currently ground (it contains no variables).

(term_typing:ground/1)Prop is currently ground (it contains no variables).*then the following properties hold globally:*

(basic_props:eval/1)inst(Term,Prop) is evaluable at compile-time.

**Usage:** `inst(Term,Prop)`

*Description:*Term is instantiated enough to satisfy Prop.

*Meta-predicate*with arguments:

`iso(goal)`.

**General properties:**

`iso(G)`

*The following properties hold globally:*

(basic_props:sideff/2)iso(G) is side-effect free.

**Usage:** `iso(G)`

*Description:**Complies with the ISO-Prolog standard.*

*Meta-predicate*with arguments:

`deprecated(goal)`.

**General properties:**

`deprecated(G)`

*The following properties hold globally:*

(basic_props:sideff/2)deprecated(G) is side-effect free.

**Usage:** `deprecated(G)`

*Description:***DEPRECATED.**

*Meta-predicate*with arguments:

`not_further_inst(goal,?)`.

**General properties:**

`not_further_inst(G,V)`

*The following properties hold globally:*

(basic_props:sideff/2)not_further_inst(G,V) is side-effect free.

**Usage:** `not_further_inst(G,V)`

*Description:*V is not further instantiated.

`sideff(G,X)`

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).

*Meta-predicate* with arguments: `sideff(goal,?)`.

**General properties:** `sideff(G,X)`

*The following properties hold globally:*

(basic_props:native/1)This predicate is understood natively by CiaoPP.

(basic_props:sideff/2)sideff(G,X) is side-effect free.

**Usage:** `sideff(G,X)`

*Description:*G is side-effect X.*If the following properties hold at call time:*

(basic_props:member/2)X is an element of [free,soft,hard].

*Meta-predicate*with arguments:

`regtype goal`.

**General properties:**

`regtype G`

*The following properties hold globally:*

(basic_props:sideff/2)regtype G is side-effect free.

**Usage:** `regtype G`

*Description:*Defines a regular type.

*Meta-predicate*with arguments:

`native(goal)`.

**General properties:**

`native(P)`

*The following properties hold globally:*

(basic_props:sideff/2)native(P) is side-effect free.

**Usage:** `native(Pred)`

*Description:*This predicate is understood natively by CiaoPP.

*Meta-predicate*with arguments:

`native(goal,?)`.

**General properties:**

`native(P,K)`

*The following properties hold globally:*

(basic_props:sideff/2)native(P,K) is side-effect free.

**Usage:** `native(Pred,Key)`

*Description:*This predicate is understood natively by CiaoPP as Key.

*Meta-predicate*with arguments:

`no_rtcheck(goal)`.

**General properties:**

`no_rtcheck(G)`

*The following properties hold globally:*

(basic_props:sideff/2)no_rtcheck(G) is side-effect free.

**Usage:** `no_rtcheck(G)`

*Description:*Declares that the assertion in which this comp property appears must not be checked at run-time.

*Meta-predicate*with arguments:

`eval(goal)`.

**Usage:** `eval(Goal)`

*Description:*Goal is evaluable at compile-time.

*Meta-predicate*with arguments:

`equiv(goal,goal)`.

**Usage:** `equiv(Goal1,Goal2)`

*Description:*Goal1 is equivalent to Goal2.

*Meta-predicate*with arguments:

`bind_ins(goal)`.

**Usage:** `bind_ins(Goal)`

*Description:*Goal is binding insensitive.

*Meta-predicate*with arguments:

`error_free(goal)`.

**Usage:** `error_free(Goal)`

*Description:*Goal is error free.

*Meta-predicate*with arguments:

`memo(goal)`.

**Usage:** `memo(Goal)`

*Description:*Goal should be memoized (not unfolded).

**Usage:** `filter(Vars,Goal)`

*Description:*Vars should be filtered during global control).

*Meta-predicate*with arguments:

`pe_type(goal)`.

**Usage:** `pe_type(Goal)`

*Description:*Goal will be filtered in partial evaluation time according to the PE types defined in the assertion.

## Known bugs and planned improvements

- Run-time checks have been reported not to work with this code. That means that either the assertions here, or the code that implements the run-time checks are erroneous.