Did you know ... Search Documentation:
Pack onepointfour_basics -- prolog/doc/README_checks.md

checks.pl

A more powerful replacement for the venerable must_be/2 to perform type and domain checks on predicate entry (among others).

  • ../checks.pl (MIT license)
  • [checks.plt](../checks.plt) (0BSD license) This documentation is out of sync with the latest update

Synopsis

Check that term X fulfills all the conditions in the list Conditions. Conditions that are marked tuned will preferentially fail instead of throwing if the condition is not fulfilled:

check_that(+X,@Conditions)

Check that term X fulfills all the conditions in the list Conditions. If Tuned is instantiated to hard, conditions that are marked tuned will throw if the condition is not fulfilled. If Tuned is instantiated to soft, conditions that are marked tuned will fail if the condition is not fulfilled.

check_that(+X,@Conditions,@Tuned)

Same as check_that/2, but a Name for X is given. This name will be used when the message for an excpetion is constructed:

check_that_named(X,Conditions,Name)

Same as check_that/3, but a Name for X is given. This name will be used when the message for an excpetion is constructed:

check_that_named(X,Conditions,Name,Tuned)

Exception terms

The exception terms thrown by check_that/N and check_that_named/N are not ISO exception terms, although they still retain the outer error(Formal,Context) structure. They are structured as follows:

error(check(Type,Expected,Msg,Culprit),_).

Where Type is an exception-identifying atom that is generally one of:

  • type - the culprit is of the wrong type to pass the check
  • domain - the culprit is of the correct type but of the wrong domain to pass the check
  • uninstantiation - the culprit is too instantiated (generally, fully instantiated when it shouldn't be)
  • instantiation - the culprit is not instantiated enough (generally, fully uninstantiated when it shouldn't be) and
  • Expected - either an uninstantiated term or a string that explains what is expected
  • Msg - either an uninstantaited term or a string giving additional information
  • Culprit - the term that caused the exception to be thrown; may be large or contain sensitive information! A hook into error_message/1 formats the exception for the toplevel printer.

Description

check_that/3 and friends: a replacement for the must_be/2 predicate of (SWI-)Prolog. must_be/2 is used to check preconditions on predicate entry, but is not very flexible. Can we change that?

A call to check_that/3 looks as follows:

check_that(X,Conditions,Tuned)

where

  • X is the term that is subject to being checked.
  • Conditions is a proper list of conditions to be evaluated left-to-right
  • Tuned is a flag that determines whether to, in certain settings, preferentially throw (if it is hard) or fail (if it is soft; actually anything other than hard)

    The simpler

    check_that(X,Conditions)

    assumes that Tuned is soft.

    The more extensive

    check_that_named(X,Conditions,Name)
    check_that_named(X,Conditions,Name,Tuned)

    also take a Name to designate the X that is being checked. This Name can then be inserted into exception messages. Generally one would not bother with this.

    TODO:

    I seems one sometimes wants to provide an explicit error message instead of having check_that construct a confusing one. Make that possible!

The list of conditions

The list of conditions in the call check_that(X,Conditions) behaves like a "conditional and" (aka. "short-circuiting and") of verifications.

A condition is a compound term, a tagged check. The functor name of the condition specifies what to do depending on the outcome of the check.

The behaviour is as given below for the various tags allowed in conditions.

The "check precondition fails" generally means that the actual check cannot determine from the current state of X whether to reasonably succeed or fail because X is not instantiated enough. The check would then raise an instantiation exception (in the current implementation, a non-ISO exception term error(check(instantiation,_,_,_),_).

The Prolog default checks like atom/1 take the high way and fail if an uninstantaited term is passed. However, atom(_) failing means that either it pretends to know something about _ that it doesn't (namely that this is not an atom) or it is actually a second-order predicate like var/1 that can analyze the momentary state of the computation and say that a term is indeed uninstantiated. In either case, we have something dubious.

break/1

  • Precondition fails: An exception (generally a 'uninstantiated error' exception) is thrown.
  • Verification fails: The condition succeeds, leading to examination of the next condition to the right.
  • Verification succeeds: Condition processing stops and check_that succeeds overall smooth/1
  • Precondition fails: The condition fails, leading to the whole of check_that/N failing. This is like the behaviour of prolog predicates like atom/N when they are given an uninstantiated term: They just fail.
  • Verification fails: The condition fails, leading to the whole of check_that/N failing.
  • Verification succeeds: The condition succeeds, leading to examination of the next condition to the right. soft/1
  • Precondition fails: An exception (generally a 'uninstantiated error' exception) is thrown.
  • Verification fails: The condition fails, leading to the whole of check_that/N failing.
  • Verification succeeds: The condition succeeds, leading to examination of the next condition to the right. tuned/1 and the Tuned flag is soft: behaves like soft/1
  • Precondition fails: An exception (generally a 'uninstantiated error' exception) is thrown.
  • Verification fails: The condition fails, leading to the whole of check_that/N failing.
  • Verification succeeds: The condition succeeds, leading to examination of the next condition to the right. tuned/1 and the Tuned flag is hard: behaves like hard/1
  • Precondition fails: An exception (generally a 'uninstantiated error' exception) is thrown.
  • Verification fails: An exception (generally a 'type error' if X is out-of-type, and a domain error if X is 'out of domain') is thrown.
  • Verification succeeds: The condition succeeds, leading to examination of the next condition to the right. hard/1
  • Check precondition fails: An exception (generally a 'uninstantiated error' exception) is thrown.
  • Check verification fails: An exception (generally a 'type error' if X is out-of-type, and a domain error if X is 'out of domain') is thrown.
  • Verification succeeds: The condition succeeds, leading to examination of the next condition to the right.

How would one use this

 client code                     circumspect                       "logical"
      |                          client code                      client code
      |                      (in particular if                         |
      |                    it calls predicate_x/N+1                    |
      |                       with Throw = true)                       |
      |                               |                                |
      |                               |                                |
      |                               |                                |
      V                               |                                V
predicate_x/N                         |                        predicate_x_smooth/N
      |                               |                       - - - - - - - - - - -
      |                               |                     captures all the argument
      |                               |                 subdomains where predicate_x/N+1
      +----------------------------+  |                    would throw and *fails them*
               Calls               |  |               (using appropriate check_that/2 calls)
          predicate_x/N+1          |  |                                |
               with                |  |                                |
           Throw = false           |  |                                |
          - - - - - - - -          |  |  +-----------------------------+
      As a consequence, some       |  |  |                Calls
      domains of problematic       |  |  |           predicate_x/N+1
      arguments subdomains will    |  |  |                with
      just cause failure instead   |  |  |            Throw = false
      of exceptions.               |  |  |
                                   |  |  |
                                   |  |  |
                                   |  |  |
                                   V  V  V
                                predicate_x/N+1
                               - - - - - - - - -
                             takes an additional
                       "Throw" argument that determines
                      what check_that/3 conditions tagged
                       as "tuned/1" will do: throw or fail
                                      |
                                      |
                                      |
                                      V
                          explicitly allow the cases
                            of unbound arguments
                          - - - - - - - - - - - - -
                       This is done with calls that break        | Note that checks generally throw if they
                         if the argument is unbound:             | are given an unbound argument, which is why
                       check_that(X,[break(var),...])            | "break" is needed. Contrariwise, Prolog's atom(_) fails
                                      |                          | but check_that(_,[soft(atom)]) throws "instantiation error".
                                      |                          | Alternatively, check_that(_,[smooth(atom)]) fails.
                                      |
                                      V
                            underspecified problem? ------------> throw "instantion error"
                            - - - - - - - - - - - -               Conditions checking this should be tagged with hard/1
                               some arguments or                  so that they always throw. If you want
                            tuples of arguments are               to see failure, you should catch-and-fail
                            not instantiated enough               in a wrapping predicate.
                                      |
                                      |
                                      |
                                      V
                                  wrong type? ------------------> These conditions should be tagged with hard/1
                               - - - - - - - -                    as such an error smells like a programming error.
                              some arguments are                  In a "smooth" setting, one may want these to fail,
                              of the wrong type                   in that case, you should catch-and-fail
                       (e.g. passing 'foo' as integer arg)        in a wrapping predicate.
                                      |
                                      |
                                      |
                                      V
                                wrong domain? ------------------> These conditions should be tagged with tuned/1
                                - - - - - - -                     so that they throw if member(Throw,[true,throw]) but only
                       some arguments or argument tuples          fail otherwise, thus causing predicate_x/N+1 to
                         are out of the allowed domain            appear more relaxed regarding some problems.
                        (such a test can become complex)
                                      |
                                      |
                                      |
                                      V
                         cross-argument correlations -----------> Generally the same as domain errors.
                         - - - - - - - - - - - - - -
                  complex conditions may need to be checked;
                  for these, use passany, passall, passnone
                          checks. This can be costly.
                                      |
                                      |
                                      |
                                      V
                               "BUSINESS CODE" ------------------------> Throw or fail? It depends, but if a problem is
                  actual processing can more easily and cheaply          detected "after the entry checks" on would
                  check additional conditions at certain points          probably want to throw.
                      and should not refrain from doing so.
                                                    |
                                                    +------------------> Augment with assertion/1 calls according to taste.
                                                                         These can be considered "live documentation" and
                                                                         can always be compiled-out later.

Check keywords implemented so far

"TBC" stands for "The term to be checked".

KeywordIf TBC is varTBC must be a/an ....
:--:--:--
truedoesn't careThis check always succeeds, whatever TBC is.
false,faildoesn't careThis check always fails, whatever TBC is.
random(Probability)doesn't careThis check randomly fails with probability 0 =< Probability =< 1.<br>Useful for playing chaos monkey.
varcovered by testuninstantiated term.
nonvarcovered by testinstantiated term.
nongroundcovered by testnonground term (and thus may be uninstantiated).
groundcovered by testground term (and thus will be instantiated).
atom,symbolthrowsatom.
atomic,constantthrowsatomic term.
compoundthrowscompound term.
booleanthrowsone of the atoms true or false.
pairthrowscompound term with functor name - and arity 2.
stringthrowsSWI-Prolog string.
stringythrowseither an atom or an SWI-Prolog string.
nonempty_stringythrowsnonempty stringy: a stringy that is different from '' and "".
charthrowsatom of length 1. This is the traditional Prolog char type.
char_list,charsthrowsproper list of 0 or more chars. Unbound elements are not allowed.
codethrowsinteger between 0 and 0x10FFFF (a Unicode code point).<br>Detailed range checks are not done.
code_list,codesthrowsproper list of 0 or more codes. Unbound elements are not allowed.
charythrowschar or a code.
chary_list,charysthrowsproper list of 0 or more chars or codes (but consistently only one of those).<br>Unbound list elements cause an exception.
stringy_typeidthrowsone of the atoms string or atom. Compare with the check boolean.
chary_typeidthrowsone of the atoms char or code. Compare with the check boolean.
numberthrowsnumber (encompasses float, rational, integer).
floatthrowsfloat (64 bit double precision), including +1.0Inf, -1.0Inf, NaN, -0.0.
float_not_nanthrowsfloat, excluding NaN.
float_not_infthrowsfloat, excluding +1.0Inf, -1.0Inf.
float_not_neginfthrowsfloat, excluding -1.0Inf.
float_not_posinfthrowsfloat, excluding +1.0Inf.
int/integerthrowsinteger.
rationalthrowsSWI-Prolog _rational, which encompasses integer.
nonint_rational,proper_rationalthrowsSWI-Prolog rational that is not an integer.
negnum,negnumberthrowsstrictly negative number.
posnum,posnumberthrowsstrictly positive number.
neg0num,neg0numberthrowsnegative-or-zero number.
pos0num,pos0numberthrowspositive-or-zero number.
non0num,non0numberthrowsnon-zero number.
negint,negative_integerthrowsstrictly negative integer.
posint,positive_integerthrowsstrictly positive integer.
neg0intthrowsnegative-or-zero integer.
pos0int,nonnegthrowspositive-or-zero integer.
negfloat,throwsstrictly negative float.
posfloatthrowsstrictly positive float.
neg0floatthrowsnegative-or-zero float.
pos0floatthrowspositive-or-zero float.
intythrowsinteger or a float that represents an integer, e.g 1.0.
negintythrowsstrictly negative inty.
posintythrowsstrictly positive inty.
neg0intythrowsnegative-or-0 inty.
pos0intythrowspositive-or-0 inty.
list,proper_listthrowsproper list, including the empty list. (TODO: open lists)
nonempty_listthrowsproper list that is not empty.
dictthrowsSWI-Prolog dict (which is a compound term following some special requirements).
dict_has_key(Key)throwsterm must be a dict, and it must contain an entry for Key.
cyclicthrowsterm for which one can unambiguously decide whether it is cyclic.
cyclic_nowcovered by testterm that has a cyclic structure now.<br>check_that(_,soft(cyclic_now)) fails.
acyclic_nowcovered by testterm that has no cyclic structure now, but may acquire it later, unless the term is ground.<br>check_that(_,soft(acyclic_now)). succeeds.
acyclic_forevercovered by testterm that is both ground and acyclic and will never become cyclic.<br>check_that(_,soft(acyclic_forever)). fails.
streamthrowsterm that is either "stream name" (certain atoms) or a valid stream handle (certain blobs).<br>The known stream names are user_input, user_output, user_error, current_input, current_output.
unifies(Z)covered by testterm that unifies with Z. Unification is rolled back by use \+ \+.
member(ListOfValues)throwsterm that is member of the ListOfValues. Membership test is unification, as for member/2.
forall(ListOfChecks)dependsTBC must pass all checks in ListOfChecks. Recursive. Same as writing the checks down normally, thus not really useful.
forany(ListOfChecks)dependsTBC must pass at least one check in ListOfChecks. Recursive. Useful for implementing an or.
fornone(ListOfChecks)dependsTBC must pass no check in ListOfChecks. Recursive. Useful for negation.
passall(Check)throwsCheck is one of the check keywords. TBC must be a proper list. All the terms in that list must pass Check. Useful for terse code.
passany(Check)throwsCheck is one of the check keywords. TBC must be a proper list. At least one terms in that list must pass Check.
passnone(Check)throwsCheck is one of the check keywords. TBC must be a proper list. None of the terms in that list must pass Check.

Keywords provided by must_be/2 not yet implemented

  • between(FloatL,FloatU): if FloatL is float, all other values may be float or integer (FIXME?); the limits are both INCLUSIVE; limits may be equal but NOT reversed
  • between(IntL,IntU): if IntL is integer, all other values must be integer; the limits are both INCLUSIVE; limits may be equal but NOT reversed. FIXME: there should be specific between_int/2 and between_float/2 if one goes that way.
  • text: atom or string or chars or codes (but not numbers even though some predicates "textify" those)
  • list(Type): proper list with elements of type Type (must_be/2(Type,_) is called on elements); empty list is allowed; on error the index is not indicated. A type like "list(list(integer))" is ok! Actually corresponds to passall(Type)
  • list_or_partial_list: A partial list (one ending in a variable: [x|_]). This includes an unbound variable.
  • callable: passes callable/1. Relatively usesless, as "callable" is ill-defined. Basically (atom(X);compound(X))
  • encoding: valid name for a character encoding; see current_encoding/1, e.g. utf8 (but not "utf8" or 'utf-8'; also fails for 'iso_8859_1')
  • type: Meta: Term is a valid type specification for must_be/2. This is done by looking up whether a clause has_type(Type,_) :- .... exists. Example: must_be(type,list(integer)). However, "must_be(type,list(grofx))": OK, but "must_be(type,grofx)": NOT OK. Possible extension:
  • predicate_indicator: A Name/Arity predicate indicator
  • list_length_X: Tests for length of lists (larger, smaller, equal)
  • subsumes
  • does_not_unify / dif A note on cyclic/acyclic

    Consider the "instantiation career" of a term, going from "most uninstantiated" to "ground":

                           uninstantiated
                                 |
                                 V
                  +--------------+-------------+
                  |                            |
                  V                            |
          nonground noncyclic                  |
                  |                            |
                  +----------------------------+
                  |                            |
                  |                            V
                  |                     nonground cyclic
                  |                            |
                  V                            V
            ground acylic                ground cyclic

    For example

                                 X=_
                       not "cyclic", "acyclic"
                                 |
                                 V
                  +--------------+-------------+
                  |                            |
                  V                            |
                X=s(_)                         |
       not "cyclic", "acyclic"                 |
                  |                            |
                  +----------------------------+
                  |                            |
                  |                            V
                  |                         X=s(X,_)
                  |                 "cyclic", not "acyclic"
                  |                            |
                  V                            V
                X=s(a)                       X=s(X)
        not "cyclic", "acyclic"      "cyclic", not "acyclic"
    

    We would like to see a predicate which throws unless it can be sure, which is not the case with the builtins cyclic_term/1 and acyclic_term/1.

    The predicates cyclic_term/1 and acyclic_term/1 are in fact "second order": They say something about the current state of computation, not about the term they are examining.

    We define the following four checks, where acyclic_now corresponds exactly to acyclic_term/1 and cyclic_now corresponds exactly to cyclic_term/1. Conditions using those check never throw.

    cycliccyclic_now<br>(cyclic_term/1)acyclic_now<br>(acyclic_term/1)acyclic_forever
    :--:--:--:--:--
    uninstantiatedthrow (hard mode)false (could change)true (could change)false
    nonground acyclicthrow (hard mode)false (could change)true (could change)false
    ground acylicfalse (for sure)false (for sure)true (for sure)true
    nonground cyclictrue (for sure)true (for sure)false (for sure)false
    ground cyclictrue (for sure)true (for sure)false (for sure)false

Examples

Fail if X is not a string (but throw if X is unbound): check_that(X,[soft(string)])

?- check_that(foo,[soft(string)]).
false.

Throw if X is not a string (or unbound): check_that(X,[hard(string)])

?- check_that(foo,[hard(string)]).
ERROR: check failed : type error (the culprit is not of the required type)
ERROR:    message   : the value should fulfill 'string-ness'
ERROR:    culprit   : foo

Throw if X is not an integer and then fail if X is not a positive integer: check_that(X,[hard(int),soft(posint)])

?- check_that(foo,[hard(int),soft(posint)]).
ERROR: check failed : type error (the culprit is not of the required type)
ERROR:    message   : the value should fulfill 'integer-ness'
ERROR:    culprit   : foo
?- check_that(-1,[hard(int),soft(posint)]).
false.
?- check_that(1,[hard(int),soft(posint)]).
true.

A type of test often done on predicate entry: break off with success if X is unbound, but otherwise it must absolutely be stringy, and even a nonempty stringy (for example): check_that(X,[break(var),hard(stringy),soft(nonempty_stringy)]).

?- check_that(X,[break(var),hard(stringy),soft(nonempty_stringy)]).
true.
?- check_that(12,[break(var),hard(stringy),soft(nonempty_stringy)]).
ERROR: check failed : type error (the culprit is not of the required type)
ERROR:    message   : the value should fulfill 'stringy-ness'
ERROR:    culprit   : 12
?- check_that("",[break(var),hard(stringy),soft(nonempty_stringy)]).
false.
?- check_that("foo",[break(var),hard(stringy),soft(nonempty_stringy)]).
true.

Smooth, soft, tuned, hard failure modes

Using the tuned/1 tag, you can switch from "hard" to "soft" behaviour:

This behaves as if you had written hard(posint):

check_that(X,[hard(int),tuned(posint)],throw)

This behaves as if you had written soft(posint):

check_that(X,[hard(int),tuned(posint)],false)

Succeed if X is unbound, and then fail or throw depending on Throw if X is not a member of the given list:

check_that(X,[break(var),tuned(member([alpha,bravo,charlie]))],Throw).

Running it:

?- check_that(X,[break(var),tuned(member([alpha,bravo,charlie]))],throw).
true.
?- check_that(bar,[break(var),tuned(member([alpha,bravo,charlie]))],throw).
ERROR: check failed : domain error (the culprit is outside the required domain)
ERROR:    message   : the value should fulfill 'list_membership-ness'
ERROR:    culprit   : bar
?- check_that(bar,[break(var),tuned(member([alpha,bravo,charlie]))],false).
false.

Usage scenarios:

  • Use check_that/2 to verify predicate entry preconditions
    • Expecting to switch them off at "production time" (assertions) to gain performance
    • They are also goo "live documentation" saying exactly what parts of the input space are covered by throws and which ones by fails One can rely on "implicitly building" that space via the behaviour of the predicates called in turn, but may become unclear what that space is. (This may be ok depending on coding style)
    • Using check_that/2 "normally" as a guard to make the predicate
      • throw on extremely bad arguments (i.e. badly typed ones)
      • fail on bad arguments (i.e. out-of-domain ones)
      • Logic/Search parts of the program will preferentially fail (or only enter the situation where a fail makes sense)
      • Functional programming parts of the program will preferentially throw (or only enter the situation where a throw makes sense)
  • Use check_that/2 to verify invariants inside of predicates (generally not needed as this is done by checking pre/postconditions in Prolog)
    • Expecting to switch them off at "production time" (assertions) to gain performance
    • TODO: Such cases must be marked as "this is not expected to be violated in running code" (throwing a really nasty exception) And then the test must be switch-offable using a specific hierarchical key, just like you switch logging on or off that way.
  • Use check_that/2 normally in code, as just a particular form of a guard, i.e. it is not expected that they will be switched off
  • (There is no easy way to perform postconditions-on-success in Prolog except by wrapping a predicate with another predicate. Annoying.)

Assertions

  • Assertions are basically the subset of conditions that one does not expect to fail or throw at runtime. The idea is to remove those tests because they "never fail" and the insurance will pick up the slack if they do. Prolog is special in that "failing" is an integral part of its approach, so switching off checks wholesale is not an option (Unless one wants to really have separate instructions for "necessary checks" and "assertion checks") To "remove unnecessary checks" it must both be possible to: 1) identify them. This can be done my giving them a special name, e.g. lenient_assert instead of just lenient 2) be able to "remove them" cheaply; this can be done during compilation phase: the marked conditions can be written out 3) select those which should be removed based on program structure: eg. all those in module XY should be removed this also seems a case for the compilation phase

Design question especially clear in case of complex checking of lists:

  • The structure to test may have multiple layers of testing. For example, for a "proper list of char":
    • X is a var -> fail or exception
    • X is not a proper list -> fail or exception
    • X contains vars -> fail or exception
    • X contains non-chars -> fails or exception
    • and finally success A caller could demand throwing down to any level of the above (and possibly accept var) The proper way to have this flexibility is exactly to use check_that/2 with the detailed more-and-more-precise check sequence, going from strictness to leniency depending on taste, for example check_that(X,[break(var),hard(list),hard(list(nonvar)),tuned(list(char))]) instead of a single monolitic check_that(X,[break(var),hard(chars)]) However, in that case the "rightmost checks" may perform wasteful checks against that we already know will succeed. So there is a need for doing bare-bones checks (maybe?). Probably not worth it. Note that what exception to throw is generally made in this order: X uninstantiated -> throw instantiation error X instantiated but not of the correct type (e.g. expecting integer but it's a float) -> throw type error X of the correct type but not in the correct domain (e.g. expecting positive integer but it's negative) -> throw domain error

Bugs

Good:

?- check_that([a,_,b],hard(chars)).
ERROR: check failed : instantiation error (the culprit is not instantiated (enough))
ERROR:    message   : the value should be instantiated. Can't check for 'atom-ness'
?- check_that([a,_,b],soft(chars)).
ERROR: check failed : instantiation error (the culprit is not instantiated (enough))
ERROR:    message   : the value should be instantiated. Can't check for 'atom-ness'

But:

?- check_that([1,_,b],soft(chars)).
false.

because the above fails at 1. It should throw.