Predicate declaration examples

• append/3
• Simplification of declarations
• member/2 and '='/2 and insert_uniq/3
• reverse/2
• fibonacci/2
• partially ordered set
• overlap/2 and disjoint/2
• DCG grammars

append/3

Concatenation of two lists.
Comparison with results of conventional type-checkers (marked with "old").

:- pred append_old(list(T),list(T),list(T)).
% is identical with
% :- pred append_old(list(@T1),list(@T2),list(@T)) with (T1=<T, T2=<T, T3=<T).

:- pred append(list(T),list(T),list(@T)).
% is identical with
% :- pred append(list(@T1),list(@T2),list(@T3)) with (T1=<T3, T2=<T3).

File app
Output of type checking (app.tap)

Simplification of declarations

Use of anchored type parameters ("@T").

File simpdecl
Internal data of the declarations (simpdecl.all)

member/2 and '='/2 and insert_uniq/3

• Checking for membership in a list
• Unification
• Unique insertion of an element into a list

Comparison with results of conventional type-checkers (marked with "old").

File member
Output of type checking (member.tap)

reverse/2

Predicate reverse/2 reverses the order of a given list.

File reverse
Output of type checking (reverse.tap)

fibonacci/2

Fibonacci numbers.

File fibonacci
Output of type checking (fibonacci.tap)

partially ordered set

Predicate declarations with a type parameter (a partially ordered set).

% a partially ordered set is internally represented by a structure

Example: poset([a,b,c,d,e,f], [a=<b, c=<d, e=<d, b=<d, b=<f, c=<f])

File poset
Output of type checking (poset.tap)

overlap/2 and disjoint/2

• Checking if two given lists are overlapping (overlap/2)
• Checking it two given lists are disjunc (disjoint/2)

disjoint/2 is the negation of the predicate overlap/2 and is therfore negatively declared ("pred_neg").

:- pred overlap(list(@S),list(@T)) with U=<S, U=<T.
:- pred_neg disjoint(list(@S),list(@T)) with U=<S, U=<T.

:- disjoint([-1,-2],[2,3]). % now useless atom "false"

File overlap
Output of type checking (overlap.tap)

DCG grammars

As a convenience for declaring grammar rules,

:- rule p(T1,...,Tk).

has the same effect as

:- predl p(T1,...,Tk, list(@T), list(@T)).

where T is a new type parameter.

The predicate 'C'/3 is predeclared in TYPICAL library prolog_dcg.pl as

:- pred 'C'(list(@T),T,list(T)).

File dcg
Output of type checking (dcg.tap)

PREV: Predicate declaration

NEXT: Case-study: Complex list structures