# Meta-properties

**Author(s):**Francisco Bueno.

This library allows the use of some meta-constructs which provide for specifying properties of terms which are unknown at the time of the specification, or expressed with a shorthand for the property definition, i.e., without really defining it.

An example of such use is an assertion which specifies that any property holding upon call will also hold upon exit:

:- pred p(X) : Prop(X) => Prop(X).

Another example is using shorthands for properties when documenting:

:- pred p(X) : regtype(X,(^(list;list);list)).

(See below for an explanation of such a regular type.)

## Usage and interface

**Library usage:**`:- use_module(library(assertions(meta_props)))`or also as a package

`:- use_package(metaprops)`.Note the different names of the library and the package.

**Exports:****Imports:***Internal (engine) modules:*`term_basic`,`arithmetic`,`atomic_basic`,`basic_props`,`basiccontrol`,`data_facts`,`exceptions`,`io_aux`,`io_basic`,`prolog_flags`,`streams_basic`,`system_info`,`term_compare`,`term_typing`,`hiord_rt`,`debugger_support`.*Packages:*`prelude`,`nonpure`,`assertions`,`hiord`.

## Documentation on exports

`call(P,A)`

A has property P (provided that P is a property). Equivalent to `P(A)`.

**(True) Usage:**`call(P,A)`

A has property P.

*If the following properties hold at call time:*

(`callable/1`)P is a term which represents a goal, i.e., an atom or a structure.

**(True) Usage:**`A prop P`

A has property P.

*If the following properties hold at call time:*

(`(prop)/2`)P has property ^ (callable;prop_abs).

**(True) Usage:**`A regtype T`

A is of type T.

*If the following properties hold at call time:*

(`(prop)/2`)T has property ^ ((regtype);prop_abs).

## Documentation on multifiles

`callme(P,X):- P(X), !.`in the program that uses this library. This is done automatically if the package is used instead of the library module (but then you

*should not*define

`callme/2`in your program).

**(Trust) Usage:**`callme(A,B)`

*The following properties should hold at call time:*

(`callable/1`)A is a term which represents a goal, i.e., an atom or a structure.

*multifile*.

## Documentation on internals

`prop_abs(Prop)`

Prop is a *property abstraction*, i.e., a *parametric property*, or a term formed of property abstractions, where the functors used in the term are escaped by `^`.

One particular case of property abstractions are *parametric regular type abstractions*, i.e., a parametric type functor or a `^`-escaped term formed of regular type abstractions.

Such abstractions are a short-hand for a corresponding regular type (correspondingly, property). For example, the following abstraction:

^(list;list);listdenotes terms of the form

`(X;Y)`where

`list(X)`and

`list(Y)`hold and also terms

`T`such that

`list(T)`holds. It is equivalent to the regular type:

abstract_type((X;Y)):- list(X), list(Y). abstract_type(T):- list(T).

**Usage:**`prop_abs(Prop)`

Prop is a property abstraction.