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.
- Predicates:
- Imports:
- Packages:
prelude, nonpure, condcomp, assertions, regtypes, nortchecks.
- Packages:
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.
