PROLOG-REQUEST@SUSHI.STANFORD.EDU (Chuck Restivo, The Moderator) (11/13/87)
PROLOG Digest Saturday, 14 Nov 1987 Volume 5 : Issue 86
Today's Topics:
Announcement - Final CADE9 Call,
Implementation - Types,
LP Library - List Package & Type Checker
----------------------------------------------------------------------
Date: Wed, 4 Nov 87 12:45:07 cst
From: stevens@anl-mcs.ARPA (Rick L. Stevens)
Subject: Final CADE-9 Call for Papers
Final Call for Papers
9th International Conference on Automated
Deduction
May 23-26, 1988
CADE-9 will be held at Argonne National Laboratory (near
Chicago) in celebration of the 25th anniversary of the
discovery of the resolution principle at Argonne in the sum-
mer of 1963. Papers are invited in the following or related
fields:
Theorem Proving Logic Programming
Unification Deductive Databases
Term Rewriting ATP for Non-Standard Logics
Program Verification Inference Systems
Papers are solicited in three categories:
Long papers: 20 pages, about 5000 words
Short papers: 10 pages, about 2500 words
Extended Abstracts of Working Systems: 2 pages
Problem sets: 5 pages
Long papers are expected to present substantial research
results. Short papers are a forum for briefer presentations
of the results of ongoing research. Extended abstracts are
descriptions of existing automated reasoning systems and
their areas of application. Problem sets should present a
complete, formal representation of some collection of
interesting problems for automated systems to attack. The
problems should currently unavailable in the existing
literature. Three copies should be sent to arrive before
November 23rd, 1987 to
Ewing Lusk and Ross Overbeek, chairmen
CADE-9
Mathematics and Computer Science Division
Argonne National Laboratory
9700 South Cass Avenue
Argonne, IL 60439
Schedule:
November 23, 1987: papers due
January 25, 1988: notification of authors
February 21, 1988: final manuscripts due
Questions should be directed to E. L. Lusk (lusk@anl-
mcs.arpa, phone 312-972-7852) or Ross Overbeek
(overbeek@anl-mcs.arpa, phone 312-972-7856)
------------------------------
Date: 31 Oct 87 16:19:00 GMT
From: reddy@b.cs.uiuc.edu
Subject: Types Utilizations in Prolog
I don't know if Lee's message got cut off in the middle somewhere on
the net. But, I didn't see an important reference mentioned in his
list.
Mycroft and O'Keefe, A polymorphic type system for Prolog,
Artificial Intelligence, 23:295-307 (1984).
An implementation of this system exists. But, it needs lots of
declarations. You can probably ask O'Keefe for a copy of the system.
For an early reference on the theory of type "inference", see
Mishra, Towards a theory of types in Prolog, IEEE Intl. Symp
on Logic Programming, 1984, 289-298.
------------------------------
Date: 3 Nov 87 03:02:00 GMT
From: munnari!mulga!philip@uunet.uu.net (Philip Dart)
Subject: Doubly-linked list package
% Following the comments about Fortran as an AI language,
% Melbourne University Department of Artificial Intelligence
% has decided to convert all of its Fortran AI programs to NU-Prolog.
% This package has been written as an aid to this conversion.
% For non-NU-Prolog users, simply comment out the when declarations.
% Doubly-linked list package.
% Why use boring old single-linked lists when doubly-linked
% list could make your list processing applications
% run as never before.
% ?- dAdj(L, R) when L and R. % Are these adjacent nodes?
% ?- dPrev(D, _) when D. % Get previous node.
% ?- dNext(D, _) when D. % Get next node.
% ?- dHead(D, _) when D. % Get head of list
% ?- dTail(D, _) when D. % Get tail of list
% ?- isD(D) when D. % Is this a doubly-linked list?
% ?- portray(D) when ever. % Portray doubly-linked list
% ?- dAppend(X, Y, Z) when X or Z. % Append for doubly-linked lists
test :-
L1 = [1, 2, 3],
listToD(L1, D1),
write(L1), write(' <=> '), portray(D1), nl,
L2 = [4, 5, 6, 7],
listToD(L2, D2),
write(L2), write(' <=> '), portray(D2), nl,
dAppend(D1, D2, D3),
listToD(L3, D3),
isD(D3),
write(L3), write(' <=> '), portray(D3), nl.
?- dAdj(L, R) when L and R. % Are these adjacent nodes?
dAdj(L, R) :-
L = d(_, _, R),
R = d(L, _, _).
?- dPrev(D, _) when D. % Get previous node.
dPrev(d(L, _, _), L).
?- dNext(D, _) when D. % Get next node.
dNext(d(_, _, R), R).
?- dHead(D, _) when D. % Get head of list
dHead([], []).
dHead(d([], D, R), d([], D, R)).
dHead(d(d(L, D, R), _, _), H) :-
dHead(d(L, D, R), H).
?- dTail(D, _) when D. % Get tail of list
dTail([], []).
dTail(d(L, D, []), d(L, D, [])).
dTail(d(_, _, d(L, D, R)), T) :-
dTail(d(L, D, R), T).
?- listToD(List, D) when List or D. % Convert single to doubly-linked list
listToD([], []).
listToD(H.T, D) :-
D = d([], H, R),
$listToD(T, D, R).
?- $listToD(List, _, D) when List or D.
$listToD([], _, []).
$listToD(H.T, L, D) :-
D = d(L, H, R),
$listToD(T, D, R).
?- isD(D) when D. % Is this a doubly-linked list?
isD([]).
isD(D) :-
D = d([], _, R),
$isD(D, R).
?- $isD(_, D) when D.
$isD(_, []).
$isD(L, D) :-
D = d(L, V, R),
$isD(D, R).
?- portray(D) when ever. % Portray doubly-linked list
portray(D) :-
nonvar(D),
D = d([], _, _),
display('[]:'),
$dPrint(D).
?- $dPrint(D) when D.
$dPrint([]) :-
display('[]').
$dPrint(d(_, V, R)) :-
display(V),
display(':'),
$dPrint(R).
?- dAppend(X, Y, Z) when X or Z. % Append for doubly-linked lists
dAppend(X, [], X).
dAppend([], d([], D, R), d([], D, R)).
dAppend(d(L, X, R), d([], Y, RY), Z) :-
$dAppend([], d(L, X, R), Y, RY, Z).
?- $dAppend(X, _, _, Z) when X or Z.
$dAppend(L, d(_, X, []), Y, R, Z) :-
Z = d(L, X, H),
H = d(Z, Y, R1),
$dAppend1(H, R, R1).
$dAppend(L, d(_, X, d(L1, X1, R1)), Y, RY, d(L, X, RZ)) :-
Z = d(L, X, RZ),
$dAppend(Z, d(L1, X1, R1), Y, RY, RZ).
?- $dAppend(_, Y, Z) when Y or Z.
$dAppend1(_, [], []).
$dAppend1(L, d(_, D, R), Z) :-
Z = d(L, D, R1),
$dAppend1(Z, R, R1).
% P.S. Don't forget to turn off the occur-check in your version of Prolog!
------------------------------
Date: Sun, 8 Nov 87 17:35:58 PST
From: quintus!ok@Sun.COM (Richard A. O'Keefe)
Subject: Type checker
Disclaimer:
the timestamps on the following two files are
correct. This is the type-checker as it stood
in 1984 for DEC-10 Prolog + Edinburgh library
(pretty much the code that was handed out at the
Albufeira Workshop in '83, in fact). It has not
been upgraded to Quintus Prolog; it doesn't
handle modules, and it was never considered to
be particularly good code. Comments and
improvements welcome.
------------------------------------------------------------------------
% File : TYPECH.PL
% Author : Alan Mycroft & R.A.O'Keefe
% Updated: 8 June 1984
% Purpose: Prolog type-checker
:- public
load/1, % for users
type_check/5. % for setof/3
%>> This module uses unify/2 from Util:MetUtl.Pl .
%>> It also uses append/3 from the utilities.
% This program defines a "type-checked consult" operation
% load(Files)
% where Files is an atom or a list of atoms. There is no
% analogue of the reconsult operation. In the Files type
% declarations may be given in addition to the usual sort
% of commands, questions, clauses, and declarations. You
% can put the type declarations in separate files, so that
% load(['foo.typ','foo.pl']) can be used to type-check and
% load the interpreted version, and compile('foo.pl') can
% be used to compile the same code. Note that declarations
% have to be processed before clauses using the things
% declared.
% There are two new declarations:
% type <type term> --> <constr>{| <constr>}.. .
% e.g. type tree(T) --> empty | tree(T,tree(T),tree(T)).
% and
% pred <pred decl>{, <pred decl>}.. .
% e.g. pred append(list(T), list(T), list(T)).
% You may use a semicolon instead of a vertical bar if you like.
% As a convenience for defining grammar rules,
% rule p(T1,...,Tk).
% has the same effect as
% pred p(T1,...,Tk,list(T_),list(T_)).
% where T_ is not further specified. 'C'/3 is predefined as
% pred 'C'(list(X), X, list(X)).
:- op(1199, fx, [(type), (pred), (rule)]).
:- op(1198, xfy, (-->)).
:- op( 999, xfy, (:)).
% load/1 is defined in the usual way. The juggling with (no)fileerrors
% is to determine whether failure to find a file causes an error message
% and abort, or just (as here) a failure. expandterm/2 is where grammar
% rules are translated to ordinary Prolog. In Dec-10 Prolog, the style
% of programming which uses failure-driven loops is nearly obsolete,
% thanks to the introduction of TRO to the compiler, and it was never
% considered to be anything other than a hack. However, this stuff has
% to be useful in C Prolog and other Prologs which still lack TRO, so
% the hack remains.
load(Files) :-
recorded(void, (type), _),
!, % the definitions have been loaded
load1(Files).
load(Files) :-
recordz(void, (type), _),
recordz(any, (type), _),
recordz((_:-_), type((void:-void), void), _), % for assert
load1(['util:prolog.typ'|Files]).
load1(Var) :-
var(Var),
!,
write('! load: argument contains a variable'), nl,
fail.
load1([Head|Tail]) :- !,
load1(Head), !, % discard this cut on non-TRO systems
load1(Tail).
load1(File) :-
atom(File),
!,
nofileerrors,
seeing(Old),
load2(File),
fileerrors,
see(Old).
load1(File) :-
write('! load: argument not list or atom: '),
write(File), nl,
fail.
load2(File) :-
see(File),
repeat,
read(Term),
expand_term(Term, Expanded),
process_term(Expanded, File),
Expanded = end_of_file,
!,
seen,
write(File), write(' loaded.'), nl.
load2(File) :-
write('! load: can''t see '),
write(File), nl,
fail.
% process_term(Expansion, File)
% handles a command, question, clause, or declaration.
% Questions are treated as if they were commands, which is just plain
% wrong, but only in Prolog-X is a version of 'read' standardly
% available which gives you a name->variable list so that you can
% print the answers. Type checking wants to be built into a Prolog
% system top level from the word go, not added on as an afterthought.
process_term(end_of_file, File) :- !.
process_term((:- Command), File) :- !,
process_command(Command, File).
process_term((?- Question), File) :- !,
process_command(Question, File).
process_term({Unchecked}, File) :- !,
assertz(Unchecked).
process_term((Head :- Body), File) :- !,
type_check((Head:-Body), Clause),
assertz(Clause).
process_term(Head, File) :-
type_check((Head:-true), Clause),
assertz(Clause).
% process_command(Command, File)
% mainly handles declarations.
process_command((type Type --> Constructors), File) :- !,
process_type(Type, Constructors).
process_command((pred Predicates), File) :- !,
process_pred(Predicates, (pred)).
process_command((rule GrammarRules), File) :- !,
process_pred(GrammarRules, (rule)).
process_command([Files], File) :- !,
load1(Files).
process_command((mode Modes), File) :- !,
true. % could maybe note that we expect a type?
process_command((public PublicDeclarations), File) :- !,
true. % could maybe note that we expect a type?
process_command(Question, user) :- !,
( type_check(Question, Checked)
; write('! ill-typed '), nl, fail
),
( call(Checked),
write(Checked), nl, write('more? '), ttyflush,
read(no)
; write('no (more) answers'), nl
).
process_command(Command, File) :-
( type_check(Command, Checked)
; write('! ill-typed '), write(Command),
write(' in '), write(File), nl, fail
),
( call(Checked), !
; write('! failed command '), write(Command),
write(' in '), write(File), nl, fail
).
% The "typed premise" described in Mycroft & O'Keefe is stored two
% ways. The types of variables are held in a dynamic data structure
% used only within a single clause. The types of predicates and
% functors are held in the data base. We use the Dec-10 "recorded"
% data base here to reduce clashes with user clauses and make access
% a little bit faster, but ordinary clauses could just as easily be
% used. There are three cases:
%
% recorded(Key, (type), _)
% - use type_def(Key) as clauses
% means that the Key is a type constructor. E.g. after
% processing the declaration :- type tree(T) --> ... .
% recorded(tree(T), (type), _)
% would be true.
%
% recorded(Key, type(Pat,void), _)
% - use has_type(Key, Pat, void) as clauses
% means that the Key is defined as a predicate. The Pat looks like
% the Key, but has type terms for its arguments. E.g. after
% processing the declaration :- pred elem(T, tree(T)).
% recorded(elem(_,_), type(elem(T,tree(T)),void), _)
% would be true.
%
% recorded(Key, type(Pat,Val), _)
% - use has_type(Key, Pat, Val) as clauses
% means that the Key is defined as a function. The Pat looks like
% the Key, but has type terms for its arguments. E.g. after
% processing the declaration
% :- type tree(T) --> empty | t(T,tree(T),tree(T)).
% recorded(empty, type(empty,tree(T)), _) and
% recorded(t(_,_,_), type(t(T,tree(T),tree(T)),tree(T)), _)
% would both be true.
%
% These declarations are the only way that data of the given forms
% are recorded.
% process_type(<type head>, <type body>)
% checks that its arguments are well formed, and if they are,
% records the type information about the <type head> and the
% constructors.
process_type(Head, Body) :-
check_type_head(Head),
recordz(Head, (type), _), % recorded here for recursive types
check_type_body(Head, Body, Constructors),
process_type_body(Constructors, Head).
process_type_body([Constructor|Constructors], Head) :-
recordz(Constructor, type(Constructor,Head), _), !,
process_type_body(Constructors, Head).
process_type_body([], _).
check_type_head(Head) :-
var(Head),
!,
write('! Type head is a variable.'), nl,
fail.
check_type_head(Head) :-
recorded(Head, (type), _),
!,
write('! Already a type: '), write(Head), nl,
fail.
check_type_head(Head) :-
functor(Head, _, N),
check_type_head(N, Head),
!,
fail.
check_type_head(_).
check_type_head(N, Head) :-
arg(N, Head, Arg),
nonvar(Arg),
write('! Type head argument '), write(N),
write(' is bad.'), nl.
check_type_head(N, Head) :-
arg(N, Head, N),
M is N-1,
check_type_head(M, Head).
% is_type_expr(Term)
% succeeds when Term is a type expression, that is, when all the
% constructors it is made from are type constructors. If we had
% type macros (:- type Lhs = Rhs) this is where we would expand
% them. That will come later.
is_type_expr(Type) :-
var(Type),
!.
is_type_expr(Type) :-
recorded(Type, (type), _),
!,
functor(Type, _, N),
is_type_expr(N, Type).
is_type_expr(Type) :-
write('! not a type: '),
write(Type), nl,
fail.
is_type_expr(0, Type) :- !.
is_type_expr(N, Type) :-
arg(N, Type, Arg),
is_type_expr(Arg),
M is N-1,
!,
is_type_expr(M, Type).
check_type_body(Head, Body, _) :-
numbervars(Head, 0, M),
numbervars(Body, M, N),
N > M,
!,
write('! Rhs of type def contains variables not in lhs.'), nl,
fail.
check_type_body(Head, Body, Constructors) :-
check_type_body_(Body, Constructors, []).
check_type_body_(( Constr1 ; Constr2 ), CL, CR) :- !,
check_type_body_(Constr1, CL, CM),
check_type_body_(Constr2, CM, CR).
check_type_body_({Constructor}, [Constructor|CR], CR) :-
nonvar(Constructor),
functor(Constructor, _, N),
is_type_expr(N, Constructor),
!.
check_type_body_({Constructor}, _, _) :- !,
write('! Dud constructor : '),
write(Constructor), nl,
fail.
check_type_body_(Constructor, CL, CR) :-
check_type_body_({Constructor}, CL, CR).
% process_pred(Preds, Sort)
% processes pred (Sort=pred) and rule (Sort=rule) declarations.
% Several predicates may be declared in one declaration, and they
% may be separated by any mixture of commas and semicolons. To
% declare comma or semicolon as a predicate, you have to put it
% inside braces { }, e.g. :- pred {void,void}. The same escape
% convention is used to let you define these symbols as constructors
% in type declarations.
process_pred(Var, Sort) :-
var(Var),
!,
write('! variable in '), write(Sort),
write(' declaration.'), nl,
fail.
process_pred((Preds1 , Preds2), Sort) :- !,
process_pred(Preds1, Sort),
process_pred(Preds2, Sort).
process_pred((Preds1 ; Preds2), Sort) :- !,
process_pred(Preds1, Sort),
process_pred(Preds2, Sort).
process_pred({Pred}, (pred)) :-
recorded(Pred, type(_,void), _),
!,
write('! already declared: '), write(Pred), nl,
fail.
process_pred({Pred}, (pred)) :- !,
functor(Pred, _, N),
is_type_expr(N, Pred),
recordz(Pred, type(Pred,void), _).
process_pred({Rule}, (rule)) :- !,
Rule =.. List,
append(List, [list(T),list(T)], Full),
Pred =.. Full,
process_pred({Pred}, (pred)).
process_pred(Other, Sort) :-
process_pred({Other}, Sort).
% To perform type checking we use the Milner algorithm with overloading.
% The idea is that we consider (via backtracking) all the type resolutions
% possible, and accept the typing if exactly one type assignment exists.
% For this (second order) operation we use 'setof'. The typed premise
% is in two parts. The predicate and functor assignments are held in the
% data base, the variable assignments (which only have significance within
% the current clause) in held in Tenv (type environment) variables.
% type tenv --> var | var(variable,type,tenv).
type_check(Given, Pruned) :-
setof(P, To^type_check(Given, P, var, To, void), PP),
( PP = [Pruned], !
; write('! ambiguous overloaded functor.'), nl, !, fail
).
type_check(:-(Head,Body), _) :-
write('% no type can be assigned to the rule'), nl, !,
pp_explicit(:-(Head,Body), Head).
type_check(Head, _) :-
write('% no type can be assigned to the fact'), nl, !,
pp_explicit(Head, Head).
% type_check(Given, Pruned, TenvIn, TenvOut, Expected)
% checks a Given term which is expected to have type Expected.
% It may extend the type environment, as well as further specifying
% existing variable assignments, and it returns the Given term
% Pruned of ":Type" annotations. The point of the latter is to
% help the type system when it comes across an overloaded term that
% it is otherwise unable to resolve.
type_check(X, X, Ti, Ti, Expected) :-
Expected == any,
!. % X had better not contain :annotations!
type_check(Var, Var, Ti, To, Context) :-
var(Var),
!,
type_check(Var, Ti, To, Context).
type_check((Given:Type), Pruned, Ti, To, Expected) :- !,
unify(Type, Expected),
type_check(Given, Pruned, Ti, To, Expected).
type_check((Head:-Body), (Lhs:-Rhs), Ti, To, void) :- !,
recorded(Head, type(HeadT,void), _),
numbervars(HeadT, 0, _), % crucial
functor(Head, F, N),
functor(Lhs, F, N),
type_check(N, Head, Lhs, Ti, Tm, HeadT),
type_check(Body, Rhs, Tm, To, void).
type_check(Int, Int, Ti, Ti, integer) :-
integer(Int),
!. % special hack for numbers
type_check(Given, Pruned, Ti, To, Expected) :-
recorded(Given, type(GivenT, ResultT), _),
unify(ResultT, Expected),
functor(Given, F, N),
functor(Pruned, F, N),
type_check(N, Given, Pruned, Ti, To, GivenT).
% Type check a variable
type_check(Var, Ti, Ti, Expected) :-
varassoc(Ti, Var, VarT),
!,
unify(VarT, Expected).
type_check(Var, Ti, var(Var,Expected,Ti), Expected).
varassoc(var(V,T,_), Var, T) :-
V == Var, !.
varassoc(var(_,_,R), Var, T) :-
varassoc(R, Var, T).
% Type check the arguments of a term. The Given, Pruned, and Expected
% arguments all have the same principal functor, and N is the number
% of arguments still to be checked.
type_check(0, _, _, Ti, Ti, _) :- !.
type_check(N, Given, Pruned, Ti, To, Expected) :-
arg(N, Given, Agiven),
arg(N, Expected, Aexpected),
type_check(Agiven, Apruned, Ti, Tm, Aexpected),
arg(N, Pruned, Apruned),
M is N-1,
% There *MUSTN'T* be a cut here, as we want type_check/5
% to be able to back-track and try another assignment.
type_check(M, Given, Pruned, Tm, To, Expected).
------------------------------------------------------------------------
% File : PROLOG.TYP
% Author : R.A.O'Keefe
% Updated: 23 June 1983
% Purpose: Type definitions for Prolog & utilities
% the two built in types are
% void -- type of goals, truth values
% any -- matches anything at all
:- type integer --> % integers and expressions
integer + integer
| integer - integer
| integer * integer
| integer //integer % was /, should be div
| integer mod integer
| integer /\ integer % bitwise and
| integer \/ integer % bitwise or
| integer << integer % left shift
| integer >> integer % right shift
| + integer
| - integer
| [integer|any].
:- type list(T) --> [] | [T|list(T)].
:- type dbref --> ''. % this is a sort of abstract data type
:- type op --> xf | yf | yfx | xfx | xfy | fy | fx.
:- type order --> < | = | > . % for compare
:- type pair(X,Y) --> X-Y. % for keysort
:- pred {void,void}, % , = conjunction
{void;void}, % ; = disjunction
{void->void}. % -> = if-then
:- pred abolish(any, integer).
:- pred revive(any, integer).
:- pred incore(void).
:- pred asserta(void, dbref).
:- pred asserta(void).
:- pred assertz(void, dbref).
:- pred assertz(void).
:- pred retract(void).
:- pred clause(void, void, dbref).
:- pred clause(void, void).
:- pred recorda(any, any, dbref).
:- pred recordz(any, any, dbref).
:- pred recorded(any, any, dbref).
:- pred instance(dbref, any).
:- pred erase(dbref).
:- pred true.
:- pred length(list(_), integer).
:- pred name(any, list(integer)).
:- pred op(integer, op, any).
:- pred var(any).
:- pred atom(any).
:- pred !.
:- pred statistics.
:- pred statistics(any, any).
:- pred functor(any, any, integer).
:- pred call(void).
:- pred expand_term(any, any).
:- pred debug.
:- pred debugging.
:- pred display(any).
:- pred get(integer).
:- pred get0(integer).
:- pred leash(any).
:- pred nl.
:- pred nodebug.
:- pred print(any).
:- pred put(integer).
:- pred skip(integer).
:- pred tab(integer).
:- pred trace.
:- pred ttyflush.
:- pred ttyget(integer).
:- pred ttyget0(integer).
:- pred ttynl.
:- pred ttyput(integer).
:- pred ttyskip(integer).
:- pred ttytab(integer).
:- pred write(any).
:- pred writeq(any).
:- pred ancestors(list(void)).
:- pred depth(integer).
:- pred maxdepth(integer).
:- pred subgoal_of(void).
:- pred abort.
:- pred arg(integer, any, any).
:- pred assert(void).
:- pred atomic(any).
:- pred bagof(T, void, list(T)).
:- pred break.
:- pred close(any).
:- pred compare(order, any, any).
:- pred compile(any).
:- pred consult(any).
:- pred current_atom(any).
:- pred current_functor(any,any).
:- pred current_predicate(any,any).
:- pred current_op(integer, op, any).
:- pred fail.
:- pred fileerrors.
:- pred gc.
:- pred gcguide(any).
:- pred halt.
:- pred integer(any).
:- pred keysort(list(pair(X,Y)), list(pair(X,Y))).
:- pred listing.
:- pred listing(any).
:- pred log.
:- pred nofileerrors.
:- pred nogc.
:- pred nolog.
:- pred nonvar(any).
:- pred numbervars(any, integer, integer).
:- pred phrase(any, list(_)).
:- pred prompt(any, any).
:- pred read(any).
:- pred reconsult(any).
:- pred rename(any, any).
:- pred repeat.
:- pred restore(any).
:- pred save(any).
:- pred see(any).
:- pred seeing(any).
:- pred seen.
:- pred setof(T, void, list(T)).
:- pred sort(list(T), list(T)).
:- pred tell(any).
:- pred telling(any).
:- pred told.
:- pred trimcore.
:- pred plsys(any).
:- pred 'LC'.
:- pred 'NOLC'.
:- pred spy void.
:- pred nospy void.
:- pred \+ void.
:- pred T = T.
:- pred integer is integer.
:- pred T == T.
:- pred T \== T.
:- pred any =.. list(any).
:- pred integer < integer.
:- pred integer > integer.
:- pred integer =< integer.
:- pred integer >= integer.
:- pred any @< any.
:- pred any @=< any.
:- pred any @>= any.
:- pred any @> any.
:- pred any^void.
:- pred integer =\= integer.
:- pred integer =:= integer.
% From here on belong to UTIL.
:- pred &(void, void).
:- pred \=(T, T).
:- pred \\(void, void).
:- pred any(list(void)).
:- pred append(list(T), list(T), list(T)).
:- pred apply(any, list(any)).
:- pred binding(any, void).
:- pred casserta(void).
:- pred cassertz(void).
:- pred cgensym(any, any).
:- pred check_exists(any).
:- pred checkand(any, any).
:- pred checklist(any, list(_)).
:- pred clean.
:- pred close(any, any).
:- pred concat(any, any, any).
:- pred continue.
:- pred convlist(any, list(_), list(_)).
:- pred delete(any).
:- pred diff(T, T).
:- pred disjoint(list(_)).
:- pred edit(any).
:- pred error(any, any, any).
:- pred eval(void).
:- pred eval(integer, integer).
:- pred file_exists(any).
:- pred findall(T, void, list(T)).
:- pred flag(any, T, T).
:- pred for(integer, void).
:- pred forall(void, void).
:- pred gcc(void).
:- pred gensym(any, any).
:- pred intersect(list(T), list(T), list(T)).
:- pred last(T, list(T)).
:- pred listtoset(list(T), list(T)).
:- pred mapand(any, any, any).
:- pred maplist(any, list(_), list(_)).
:- pred member(T, list(T)).
:- pred nextto(T, T, list(T)).
:- pred nmember(T, list(T), integer).
:- pred nobt(void).
:- pred not(void).
:- pred number(any).
:- pred numlist(integer, integer, list(integer)).
:- pred occ(any, any, integer).
:- pred open(any).
:- pred open(any, any).
:- pred pairfrom(list(T), T, T, list(T)).
:- pred perm(list(T), list(T)).
:- pred perm2(T, T, T, T).
:- pred read_in(list(T)).
:- pred redo(any).
:- pred remove_dups(list(T), list(T)).
:- pred rev(list(T), list(T)).
:- pred select(T, list(T), list(T)).
:- pred seteq(list(T), list(T)).
:- pred some(any, list(_)).
:- pred subgoal(any, void).
:- pred subset(list(T), list(T)).
:- pred subst(any, T, T).
:- pred subtract(list(T), list(T), list(T)).
:- pred sumlist(list(integer), integer).
:- pred thnot(void).
:- pred tidy(any, any).
:- pred tlim(integer).
:- pred ton(any).
:- pred toff.
:- pred toff(any).
:- pred trace(any, integer).
:- pred trace(any, any, integer).
:- pred union(list(T), list(T), list(T)).
:- pred variables(any, list(T)).
:- pred writef(any).
:- pred writef(any, any).
------------------------------
End of PROLOG Digest
********************