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.
- System library modules:
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).
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).
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.
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.
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.
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.
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.
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.
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.
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.