# Term checking utilities

**Author(s):**The CLIP Group.

This module implements a basic set of term checking utilities.

## Usage and interface

**Library usage:**`:- use_module(library(terms_check)).`**Exports:***Predicates:*`ask/2`,`subsumes_term/2`,`variant/2`,`most_general_instance/3`,`most_specific_generalization/3`,`unifiable/3`.*Properties:*`instance/2`.*Regular Types:*`unifier/1`.

**Imports:***Packages:*`prelude`,`nonpure`,`condcomp`,`assertions`,`regtypes`,`nortchecks`.

## Documentation on exports

PREDICATE

`ask(Term1,Term2)`

Term1 and Term2 unify without producing bindings for the variables of Term1. I.e., `instance(Term1,Term2)` holds.

PROPERTY

**(True) Usage:**`instance(Term1,Term2)`

Term1 is an instance of Term2.

*The following properties hold globally:*

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

PREDICATE

`most_general_instance(Term1,Term2,Term)`

Term satisfies `instance(Term,Term1)` and `instance(Term,Term2)` and there is no term more general than Term (modulo variants) that satisfies it.

PREDICATE

`most_specific_generalization(Term1,Term2,Term)`

Term satisfies `instance(Term1,Term)` and `instance(Term2,Term)` and there is no term less general than Term (modulo variants) that satisfies it.

PREDICATE

**(True) Usage:**`unifiable(X,Y,Unifier)`

Unifies Unifier with the most general unifier between the terms X and Y. Fails if such unifier does not exit.

*The following properties should hold at call time:*

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

(basic_props:term/1)Y is any term.*The following properties hold upon exit:*

(terms_check:unifier/1)Unifier is a unifier.

## Documentation on internals

REGTYPE

A regular type, defined as follows:

unifier_elem(X=Term) :- var(X), term(Term).

## Other information

Currently,`ask/2`and

`instance/2`are exactly the same. However,

`ask/2`is intended to be more general, since it is also applicable to constraint domains (although not yet implemented): i.e., for the particular case of Herbrand terms,

`ask/2`is just

`instance/2`.

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