# Extra-logical properties for typing

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

This library contains traditional Prolog predicates for testing types. They depend on the state of instantiation of their arguments, thus being of extra-logical nature.

## Usage and interface

**Library usage:**

These predicates are builtin in Ciao, so nothing special has to be done to use them.**Exports:****Imports:***System library modules:*`assertions/native_props`.*Packages:*`prelude`,`nonpure`,`assertions`,`nortchecks`,`nativeprops`,`isomodes`.

## Documentation on exports

**(True) Usage:**`var(X)`

X is a free variable.

*The following properties hold globally:*

(basic_props:native/2)This predicate is understood natively by CiaoPP as free(X).

**General properties:**

**Trust:**

*The following properties hold globally:*

(native_props:is_det/1)All calls of the form var(Arg1) are deterministic.

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

**True:**`var(X)`

*The following properties hold globally:*

(basic_props:not_further_inst/2)X is not further instantiated.

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

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

**True:**`var(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)var(X) is evaluable at compile-time.

**True:**`var(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:equiv/2)var(X) is equivalent to fail.

**True:**`var(X)`

*If the following properties hold at call time:*

(term_typing:var/1)X is a free variable.*then the following properties hold globally:*

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

**(True) Usage:**`nonvar(X)`

X is currently a term which is not a free variable.

*The following properties hold globally:*

(basic_props:native/2)This predicate is understood natively by CiaoPP as not_free(X).

**General properties:**

**Trust:**

*The following properties hold globally:*

(native_props:is_det/1)All calls of the form nonvar(Arg1) are deterministic.

**True:**`nonvar(X)`

*The following properties hold globally:*

(basic_props:not_further_inst/2)X is not further instantiated.

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

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

**True:**`nonvar(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)nonvar(X) is evaluable at compile-time.

**True:**`nonvar(T)`

*If the following properties hold at call time:*

(term_typing:var/1)T is a free variable.*then the following properties hold globally:*

(basic_props:equiv/2)nonvar(T) is equivalent to fail.

**True:**`nonvar(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:equiv/2)nonvar(T) is equivalent to true.

**(True) Usage:**`atom(X)`

X is currently instantiated to an atom.

*The following properties hold globally:*

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

**General properties:**

**Trust:**`atom(X)`

*The following properties hold upon exit:*

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

**Trust:**

*The following properties hold globally:*

(native_props:is_det/1)All calls of the form atom(Arg1) are deterministic.

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

**True:**`atom(X)`

*The following properties hold globally:*

(basic_props:not_further_inst/2)X is not further instantiated.

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

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

**True:**`atom(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)atom(X) is evaluable at compile-time.

**True:**`atom(T)`

*If the following properties hold at call time:*

(term_typing:var/1)T is a free variable.*then the following properties hold globally:*

(basic_props:equiv/2)atom(T) is equivalent to fail.

**(True) Usage:**`integer(X)`

X is currently instantiated to an integer.

*The following properties hold globally:*

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

**General properties:**

**Trust:**`integer(X)`

*The following properties hold upon exit:*

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

**Trust:**

*The following properties hold globally:*

(native_props:is_det/1)All calls of the form integer(Arg1) are deterministic.

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

**True:**`integer(X)`

*The following properties hold globally:*

(basic_props:not_further_inst/2)X is not further instantiated.

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

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

**True:**`integer(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)integer(X) is evaluable at compile-time.

**True:**`integer(T)`

*If the following properties hold at call time:*

(term_typing:var/1)T is a free variable.*then the following properties hold globally:*

(basic_props:equiv/2)integer(T) is equivalent to fail.

**(True) Usage:**`float(X)`

X is currently instantiated to a float.

*The following properties hold globally:*

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

**General properties:**

**Trust:**`float(X)`

*The following properties hold upon exit:*

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

**Trust:**

*The following properties hold globally:*

(native_props:is_det/1)All calls of the form float(Arg1) are deterministic.

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

**True:**`float(X)`

*The following properties hold globally:*

(basic_props:not_further_inst/2)X is not further instantiated.

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

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

**True:**`float(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)float(X) is evaluable at compile-time.

**True:**`float(T)`

*If the following properties hold at call time:*

(term_typing:var/1)T is a free variable.*then the following properties hold globally:*

(basic_props:equiv/2)float(T) is equivalent to fail.

**(True) Usage:**`number(X)`

X is currently instantiated to a number.

*The following properties hold globally:*

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

**General properties:**

**Trust:**`number(X)`

*The following properties hold upon exit:*

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

**Trust:**

*The following properties hold globally:*

(native_props:is_det/1)All calls of the form number(Arg1) are deterministic.

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

**True:**`number(X)`

*The following properties hold globally:*

(basic_props:not_further_inst/2)X is not further instantiated.

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

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

**True:**`number(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)number(X) is evaluable at compile-time.

**True:**`number(T)`

*If the following properties hold at call time:*

(term_typing:var/1)T is a free variable.*then the following properties hold globally:*

(basic_props:equiv/2)number(T) is equivalent to fail.

**(True) Usage:**`atomic(X)`

X is currently instantiated to an atom or a number.

*The following properties hold globally:*

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

**General properties:**

**Trust:**`atomic(T)`

*The following properties hold upon exit:*

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

**Trust:**

*The following properties hold globally:*

(native_props:is_det/1)All calls of the form atomic(Arg1) are deterministic.

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

**True:**`atomic(X)`

*The following properties hold globally:*

(basic_props:not_further_inst/2)X is not further instantiated.

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

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

**True:**`atomic(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)atomic(X) is evaluable at compile-time.

**True:**`atomic(T)`

*If the following properties hold at call time:*

(term_typing:var/1)T is a free variable.*then the following properties hold globally:*

(basic_props:equiv/2)atomic(T) is equivalent to fail.

**(True) Usage:**`ground(X)`

X is currently ground (it contains no variables).

*The following properties hold globally:*

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

**General properties:**

**Trust:**`ground(X)`

*The following properties hold upon exit:*

(basic_props:gnd/1)X is ground.

**Trust:**

*The following properties hold globally:*

(native_props:is_det/1)All calls of the form ground(Arg1) are deterministic.

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

**True:**`ground(X)`

*The following properties hold globally:*

(basic_props:not_further_inst/2)X is not further instantiated.

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

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

**True:**`ground(X)`

*If the following properties hold at call time:*

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

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

**True:**`ground(X)`

*If the following properties hold at call time:*

(term_typing:var/1)X is a free variable.*then the following properties hold globally:*

(basic_props:equiv/2)ground(X) is equivalent to fail.

**True:**`ground(X)`

*If the following properties hold at call time:*

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

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

**(True) Usage:**`type(X,Y)`

X is internally of type Y (`var`, `attv`, `float`, `integer`, `structure`, `atom` or `list`).

*The following properties hold globally:*

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

**General properties:**

**Trust:**`type(X,Y)`

*The following properties hold upon exit:*

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

**Trust:**

*The following properties hold globally:*

(native_props:is_det/1)All calls of the form type(Arg1,Arg2) are deterministic.

**True:**

*The following properties hold globally:*

(basic_props:sideff/2)type(Arg1,Arg2) is side-effect free.

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

**True:**`type(X,Y)`

*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)type(X,Y) is evaluable at compile-time.

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