%==============================================================================
% Project:	Microcontroller Programming in Datalog
% Version:	0.4
% Filename:	types.pl
% Purpose:	Data types, e.g. for pieces of formulas.
% Last Change:	29.03.2021
% Language:	Prolog (tested with SWI Prolog)
% Author:	Stefan Brass
% Email:	brass@informatik.uni-halle.de
% WWW:		http://www.informatik.uni-halle.de/~brass/
% Address:	Univ. Halle, Von-Seckendorff-Platz 1, D-06120 Halle, GERMANY
% Copyright:	(c) 2020-2021 by Stefan Brass
%==============================================================================

% For more information, see the main file: ctest.pl


%******************************************************************************
% Types:
%******************************************************************************


% Each type T has a predicate is_T to check whether a Prolog term satisfies
% the structural constraints of type T
% and a predicate print_T to show a value of type T on standard output.

% Currently, basically no type checking is done
% (only in the make_T predicates which import data into the internal format).
% I am planning to add type assertions with the is_T predicates
% to do at least runtime type checking (with the possibility to switch it off
% for increased performance).

% However, the types are helpful to understand the program structure
% and they are an abstraction layer over the Prolog data structures.
% When the types are used later, the internal functors should not be used,
% only the official interface predicates defined in this "Types" section.

% The print_T predicates usually fail if the value should not be of type T.


%==============================================================================
% Type "Chars" (List of One-Character Atoms):
%==============================================================================


%------------------------------------------------------------------------------
% is_chars(+Chars):
%------------------------------------------------------------------------------

is_chars([]).

is_chars([Char|Chars]) :-
	atom(Char), % Maybe I should check that only one character.
	is_chars(Chars).

%------------------------------------------------------------------------------
% print_chars(+Chars):
%------------------------------------------------------------------------------

% Print list of characters (encoded as one-character Prolog atoms).

print_chars([]).

print_chars([Char|Rest]) :-
	put_char(Char),
	print_chars(Rest).


%==============================================================================
% Type "Const" (Constants in Terms):
%==============================================================================


%------------------------------------------------------------------------------
% is_const(+Term):
%------------------------------------------------------------------------------

is_const(Term) :-
	atomic(Term).

is_const(str(Chars)) :-
	is_chars(Chars).

is_const(cconst(Name)) :-
	atom(Name).

%------------------------------------------------------------------------------
% print_const(+Const):
%------------------------------------------------------------------------------

print_const(cconst(Name)) :-
	!,
	write('#'),
	write(Name).

print_const(str(Chars)) :-
	!,
	write('\''),
	print_chars(Chars),
	write('\'').

print_const(Const) :-
	is_const(Const),
	write(Const).

%------------------------------------------------------------------------------
% const_number(+Const, -Number):
%------------------------------------------------------------------------------

% This can also be called for constants that are not numbers,
% then it should fail.

const_number(Const, Const) :-
	number(Const).


%==============================================================================
% Type "Var" (Variables in Terms):
%==============================================================================


%------------------------------------------------------------------------------
% is_var(+Term):
%------------------------------------------------------------------------------

is_var(v(_)).

is_var(v(_,_)).

%------------------------------------------------------------------------------
% print_var(+Var):
%------------------------------------------------------------------------------

print_var(v(VarName)) :-
	write(VarName).

print_var(v(VarName,No)) :-
	write(VarName),
	write('_'),
	write(No).


%==============================================================================
% Type "Term" (Terms Formulas and Rules):
%==============================================================================

% Terms in Datalog are Constants or Variables.

%------------------------------------------------------------------------------
% is_term(+Term):
%------------------------------------------------------------------------------

is_term(Term) :-
	is_const(Term).

is_term(Term) :-
	is_var(Term).

%------------------------------------------------------------------------------
% print_term(+Term):
%------------------------------------------------------------------------------

print_term(Var) :-
	is_var(Var),
	!,
	print_var(Var).

print_term(Const) :-
	is_const(Const),
	!,
	print_const(Const).


%==============================================================================
% Type "Pred" (Predicates that can be used in Rules):
%==============================================================================


%------------------------------------------------------------------------------
% is_pred(+Pred):
%------------------------------------------------------------------------------

is_pred(Pred) :-
	atom(Pred).

%------------------------------------------------------------------------------
% print_pred(+Pred):
%------------------------------------------------------------------------------

print_pred(Pred) :-
	write(Pred).

%------------------------------------------------------------------------------
% is_return_pred(+Pred):
%------------------------------------------------------------------------------

% TODO: This is simplified, only what is used in the example.

is_return_pred(ret_millis).


%==============================================================================
% Type "Atomic Formula" (with Comparison Operator or Built-In Predicate):
%==============================================================================


% This means only comparisons and built-in predicate calls
% that can occur in "Formulas",
% not the standard Datalog literals.

%------------------------------------------------------------------------------
% is_atomic_formula(+Formula):
%------------------------------------------------------------------------------

is_atomic_formula(true).
is_atomic_formula(false).
is_atomic_formula(eq(_,_)).
is_atomic_formula(ne(_,_)).
is_atomic_formula(lt(_,_)).
is_atomic_formula(le(_,_)).
is_atomic_formula(gt(_,_)).
is_atomic_formula(ge(_,_)).
is_atomic_formula(plus_lt(_,_,_)).
is_atomic_formula(plus_ge(_,_,_)).
is_atomic_formula(succ(_,_)).
is_atomic_formula(not_succ(_,_)).
is_atomic_formula(ret_millis(_,_)).
is_atomic_formula(not_ret_millis(_,_)).

%------------------------------------------------------------------------------
% complement_atomic_formula(+FormulaIn, -FormulaOut):
%------------------------------------------------------------------------------

complement_atomic_formula(true, false).
complement_atomic_formula(false, true).
complement_atomic_formula(eq(Term1,Term2), ne(Term1,Term2)).
complement_atomic_formula(ne(Term1,Term2), eq(Term1,Term2)).
complement_atomic_formula(lt(Term1,Term2), ge(Term1,Term2)).
complement_atomic_formula(le(Term1,Term2), gt(Term1,Term2)).
complement_atomic_formula(gt(Term1,Term2), le(Term1,Term2)).
complement_atomic_formula(ge(Term1,Term2), lt(Term1,Term2)).
complement_atomic_formula(plus_lt(T1,T2,T3), plus_ge(T1,T2,T3)).
complement_atomic_formula(plus_ge(T1,T2,T3), plus_lt(T1,T2,T3)).
complement_atomic_formula(succ(Term1,Term2), not_succ(Term1,Term2)).
complement_atomic_formula(not_succ(Term1,Term2), succ(Term1,Term2)).
complement_atomic_formula(ret_millis(Term1,Term2), not_ret_millis(Term1,Term2)).
complement_atomic_formula(not_ret_millis(Term1,Term2), ret_millis(Term1,Term2)).


%------------------------------------------------------------------------------
% print_atomic_formula(+Formula):
%------------------------------------------------------------------------------

print_atomic_formula(true) :-
	write('true').

print_atomic_formula(false) :-
	write('false').

print_atomic_formula(ne(Term1,Term2)) :-
	print_term(Term1),
	write('!='),
	print_term(Term2).

print_atomic_formula(eq(Term1,Term2)) :-
	print_term(Term1),
	write('='),
	print_term(Term2).

print_atomic_formula(lt(Term1,Term2)) :-
	print_term(Term1),
	write('<'),
	print_term(Term2).

print_atomic_formula(le(Term1,Term2)) :-
	print_term(Term1),
	write('<='),
	print_term(Term2).

print_atomic_formula(gt(Term1,Term2)) :-
	print_term(Term1),
	write('>'),
	print_term(Term2).

print_atomic_formula(ge(Term1,Term2)) :-
	print_term(Term1),
	write('>='),
	print_term(Term2).

print_atomic_formula(plus_lt(Term1,Term2,Term3)) :-
	print_term(Term1),
	write('+'),
	print_term(Term2),
	write('<'),
	print_term(Term3).

print_atomic_formula(plus_ge(Term1,Term2,Term3)) :-
	print_term(Term1),
	write('+'),
	print_term(Term2),
	write('>='),
	print_term(Term3).

print_atomic_formula(succ(Term1,Term2)) :-
	write('succ('),
	print_term(Term1),
	write(','),
	print_term(Term2),
	write(')').

print_atomic_formula(not_succ(Term1,Term2)) :-
	write('not_succ('),
	print_term(Term1),
	write(','),
	print_term(Term2),
	write(')').

print_atomic_formula(ret_millis(Term1,Term2)) :-
	write('ret_millis('),
	print_term(Term1),
	write(','),
	print_term(Term2),
	write(')').

print_atomic_formula(not_ret_millis(Term1,Term2)) :-
	write('not_ret_millis('),
	print_term(Term1),
	write(','),
	print_term(Term2),
	write(')').

%------------------------------------------------------------------------------
% eval_obvious_atomic(+AtomicFormula):
%------------------------------------------------------------------------------

% This predicate replaces atomic formulas with obvious truth values
% by true or false.
% If the truth value cannot be determined, the formula is left unchanged.
% This is only part of an optional simplification of the formula,
% so it is not absolutely essential to catch all cases.

% The logical constants cannot be further simplified:

eval_obvious_atomic(true, true) :-
	!.

eval_obvious_atomic(false, false) :-
	!.

% eq(Term1, Term2):

eval_obvious_atomic(eq(Term,Term), true) :-
	!.

eval_obvious_atomic(eq(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	Const1 \= Const2,
	!.

eval_obvious_atomic(eq(Term1,Term2), eq(Term1,Term2)) :-
	!.

% ne(Term1, Term2):

eval_obvious_atomic(ne(Term,Term), false) :-
	!.

eval_obvious_atomic(ne(Const1,Const2), true) :-
	is_const(Const1),
	is_const(Const2),
	Const1 \= Const2,
	!.

eval_obvious_atomic(ne(Term1,Term2), ne(Term1,Term2)) :-
	!.

% lt(Term1, Term2):

eval_obvious_atomic(lt(Term,Term), false) :-
	!.

eval_obvious_atomic(lt(Const1,Const2), true) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 < Num2,
	!.

eval_obvious_atomic(lt(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 >= Num2,
	!.

eval_obvious_atomic(lt(Term1,Term2), lt(Term1,Term2)) :-
	!.

% le(Term1, Term2):

eval_obvious_atomic(le(Term,Term), true) :-
	!.

eval_obvious_atomic(le(Const1,Const2), true) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 =< Num2,
	!.

eval_obvious_atomic(le(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 > Num2,
	!.

eval_obvious_atomic(le(Term1,Term2), le(Term1,Term2)) :-
	!.

% gt(Term1, Term2):

eval_obvious_atomic(gt(Term,Term), false) :-
	!.

eval_obvious_atomic(gt(Const1,Const2), true) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 > Num2,
	!.

eval_obvious_atomic(gt(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 =< Num2,
	!.

eval_obvious_atomic(gt(Term1,Term2), gt(Term1,Term2)) :-
	!.

% ge(Term1, Term2):

eval_obvious_atomic(ge(Term,Term), true) :-
	!.

eval_obvious_atomic(ge(Const1,Const2), true) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 >= Num2,
	!.

eval_obvious_atomic(ge(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 < Num2,
	!.

eval_obvious_atomic(ge(Term1,Term2), ge(Term1,Term2)) :-
	!.

% succ(Term1, Term2):

eval_obvious_atomic(succ(Term,Term), false) :-
	!.

eval_obvious_atomic(succ(_Term,0), false) :-
	!.

eval_obvious_atomic(succ(0,1), true) :-
	!.

eval_obvious_atomic(succ(Term1,Term2), succ(Term1,Term2)) :-
	!.

% not_succ(Term1, Term2):

eval_obvious_atomic(not_succ(Term,Term), true) :-
	!.

eval_obvious_atomic(not_succ(_Term,0), true) :-
	!.

eval_obvious_atomic(not_succ(0,1), false) :-
	!.

eval_obvious_atomic(not_succ(Term1,Term2), not_succ(Term1,Term2)) :-
	!.

% TODO: Cound do more here:

eval_obvious_atomic(plus_lt(T1,T2,T3), plus_lt(T1,T2,T3)) :-
	!.

eval_obvious_atomic(plus_ge(T1,T2,T3), plus_ge(T1,T2,T3)) :-
	!.

% ret_millis(Term1,Term2):

eval_obvious_atomic(ret_millis(0,_), false) :-
	!.

eval_obvious_atomic(ret_millis(Term1,Term2), ret_millis(Term1,Term2)) :-
	!.

% not_ret_millis(Term1,Term2):

eval_obvious_atomic(not_ret_millis(0,_), true) :-
	!.

eval_obvious_atomic(not_ret_millis(Term1,Term2), not_ret_millis(Term1,Term2)) :-
	!.

% We should be informed if we forgot a new kind of atomic formula:

eval_obvious_atomic(F1, F1) :-
	nl,
	write('***** eval_obvious_atomic: Unhandled Formula: '),
	write(F1),
	nl.


%==============================================================================
% Type "Formula" (and/or/nor-connection of Comparisons or Built-In Literals):
%==============================================================================


% Only comparisons and built-in predicate calls can occur in "Formulas",
% not the standard Datalog literals.

%------------------------------------------------------------------------------
% is_formula(+Formula):
%------------------------------------------------------------------------------

is_formula(Formula) :-
	is_atomic_formula(Formula),
	!.

is_formula(and(Formula1,Formula2)) :-
	!,
	is_formula(Formula1),
	is_formula(Formula2).

is_formula(or(Formula1,Formula2)) :-
	!,
	is_formula(Formula1),
	is_formula(Formula2).

is_formula(not(Formula1)) :-
	!,
	is_formula(Formula1).

%------------------------------------------------------------------------------
% print_formula(+Formula):
%------------------------------------------------------------------------------

print_formula(Formula) :-
	print_formula_not(Formula).

% The suffix indicates the priority that can be printed without (...).

% print_formula_atomic(+Formula):

print_formula_atomic(Formula) :-
	is_atomic_formula(Formula),
	!,
	print_atomic_formula(Formula).

print_formula_atomic(Formula) :-
	write('('),
	print_formula_or(Formula),
	write(')').

% We treat "and" and "or" as right-associative (fits better with lists).
% I.e. "p1 and p2 and p3" is and(p1, and(p2, p3)).

% print_formula_or(+Formula):

print_formula_or(or(Formula1,Formula2)) :-
	!,
	print_formula_and(Formula1),
	write(' | '),
	print_formula_or(Formula2).

print_formula_or(Formula) :-
	print_formula_and(Formula).

% print_formula_and(+Formula):

print_formula_and(and(Formula1,Formula2)) :-
	!,
	print_formula_not(Formula1),
	write(' & '),
	print_formula_and(Formula2).

print_formula_and(Formula) :-
	print_formula_not(Formula).

% print_formula_not(+Formula):

print_formula_not(not(Formula)) :-
	!,
	write('! '),
	print_formula_not(Formula).

print_formula_not(Formula) :-
	print_formula_atomic(Formula).

%------------------------------------------------------------------------------
% simplify_formula(+FormulaIn, -FormulaOut):
%------------------------------------------------------------------------------

% unused?
simplify_formula(FormulaIn, FormulaOut) :-
	eval_obvious(FormulaIn, FormulaOut).

%------------------------------------------------------------------------------
% eval_obvious(+FormulaIn, -FormulaOut):
%------------------------------------------------------------------------------

eval_obvious(FormulaIn, FormulaOut) :-
	is_atomic_formula(FormulaIn),
	!,
	eval_obvious_atomic(FormulaIn, FormulaOut).

eval_obvious(and(FIn1,FIn2), FOut) :-
	!,
	eval_obvious(FIn1, F1),
	eval_obvious(FIn2, F2),
	eval_obvious_and(F1, F2, FOut).

eval_obvious(or(FIn1,FIn2), FOut) :-
	!,
	eval_obvious(FIn1, F1),
	eval_obvious(FIn2, F2),
	eval_obvious_or(F1, F2, FOut).

eval_obvious(not(FIn1), FOut) :-
	!,
	eval_obvious(FIn1, F1),
	eval_obvious_not(F1, FOut).

eval_obvious(F1, F1) :-
	nl,
	write('***** eval_obvious: Unhandled Formula: '),
	write(F1),
	nl.

% eval_obvious_and(+F1, +F2, -F):

eval_obvious_and(true, F, F) :-
	!.

eval_obvious_and(false, _F, false) :-
	!.

eval_obvious_and(F, true, F) :-
	!.

eval_obvious_and(_F, false, false) :-
	!.

eval_obvious_and(F1, F2, and(F1,F2)).

% eval_obvious_or(+F1, +F2, -F):

eval_obvious_or(true, _F, true) :-
	!.

eval_obvious_or(false, F, F) :-
	!.

eval_obvious_or(_F, true, true) :-
	!.

eval_obvious_or(F, false, F) :-
	!.

eval_obvious_or(F1, F2, or(F1,F2)).

% eval_obvious_not(+F1, -F):

eval_obvious_not(true, false) :-
	!.

eval_obvious_not(false, true) :-
	!.

eval_obvious_not(F1, not(F1)).

%------------------------------------------------------------------------------
% normalize_and(+FormulaIn, -FormulaOut):
%------------------------------------------------------------------------------

% Make and-trees right-deep (corresponding to list).
% Note that we cannot use and_to_conj and conj_to_and,
% because the formulas might contain or and not.
% Here, we look only at the top part of the tree consisting of and.
% Subtrees with other operators are left untouched.

normalize_and(FormulaIn, FormulaOut) :-
	and_to_list(FormulaIn, List),
	list_to_and(List, FormulaOut).

% list_to_and(+List, -Formula):

list_to_and([Fo], Fo) :-
	!.

list_to_and([Fo1|Rest], and(Fo1,FoRest)) :-
	list_to_and(Rest, FoRest).

% and_to_list(+FormulaIn, -FormulaList):

and_to_list(and(Fo1, Fo2), List) :-
	!,
	and_to_list(Fo1, List1),
	and_to_list(Fo2, List2),
	list_append(List1, List2, List).

and_to_list(Fo, [Fo]).


%==============================================================================
% Type "Conj" (Conjunction as List of Atomic Formulas with Builtin Literals):
%==============================================================================

% The type "Conj" is a list of atomic formulas with built-in literals,
% especially
% false,
% true,
% eq(Term1,Term2),
% ne(Term1,Term2),
% succ(Term1,Term2),
% plus_lt(Term1,Term2,Term3),
% plus_ge(Term1,Term2,Term3).
% This type is the input to the consistency checker.

% In contrast, "Body" is also a list of (positive) literals (atomic formulas),
% but it includes literals with user-defined predicates.

%------------------------------------------------------------------------------
% is_conj(+Conj):
%------------------------------------------------------------------------------

is_conj([]).

is_conj([AtomicFormula|Rest]) :-
	is_atomic_formula(AtomicFormula),
	is_conj(Rest).

%------------------------------------------------------------------------------
% print_conj(+ListOfAtomicFormulas):
%------------------------------------------------------------------------------

% print_conj(+Conj):

print_conj([]) :-
	write('true').

print_conj([AtomicFormula|Rest]) :-
	is_atomic_formula(AtomicFormula),
	print_formula(AtomicFormula),
	print_conj_rest(Rest).

% print_conj_rest(+Conj):

print_conj_rest([]).

print_conj_rest([AtomicFormula|Rest]) :-
	write(', '),
	is_atomic_formula(AtomicFormula),
	print_formula(AtomicFormula),
	print_conj_rest(Rest).

%------------------------------------------------------------------------------
% print_conj_prover(+ListOfAtomicFormulas):
%------------------------------------------------------------------------------

% This is used for printing the derived atomic formulas of the prover.
% We print in inverse order, and one formula per line, doubly indented.

print_conj_prover([]).

print_conj_prover([AtomicFormula|Rest]) :-
	print_conj_prover(Rest),
	write('\t\t'),
	print_atomic_formula(AtomicFormula),
	nl.

%------------------------------------------------------------------------------
% conj_length(+ListOfAtomicFormulas, -Length):
%------------------------------------------------------------------------------

conj_length(Conj, Length) :-
	list_length(Conj, Length).

%------------------------------------------------------------------------------
% conj_contains_false(+Conj):
%------------------------------------------------------------------------------

% Check whether Conj contains false as a member (surely inconsistent).

conj_contains_false([false|_]) :-
	!.

conj_contains_false([_|Rest]) :-
	conj_contains_false(Rest).

%------------------------------------------------------------------------------
% conj_to_and(+List, -Formula):
%------------------------------------------------------------------------------

conj_to_and([], true).

conj_to_and([Fo], Fo) :-
	!.

conj_to_and([Fo1|Rest], and(Fo1,FoRest)) :-
	conj_to_and(Rest, FoRest).

%------------------------------------------------------------------------------
% and_to_conj(+FormulaIn, -FormulaList):
%------------------------------------------------------------------------------

% unused?

and_to_conj(and(Fo1, Fo2), List) :-
	!,
	and_to_conj(Fo1, List1),
	and_to_conj(Fo2, List2),
	list_append(List1, List2, List).

and_to_conj(Fo, [Fo]) :-
	is_atomic_formula(Fo).


%==============================================================================
% Type "DNF" (List of Conj-Lists interpreted as Disjunction of Conjunctions):
%==============================================================================


%------------------------------------------------------------------------------
% is_dnf(+DNF):
%------------------------------------------------------------------------------

is_dnf([]).

is_dnf([Conj|Rest]) :-
	is_conj(Conj),
	is_dnf(Rest).

%------------------------------------------------------------------------------
% print_dnf(+DNF):
%------------------------------------------------------------------------------

print_dnf([]) :-
	write('false').

print_dnf([Conj|Rest]) :-
	print_conj(Conj),
	print_dnf_rest(Rest).

% print_dnf_rest(+DNF):

print_dnf_rest([]).

print_dnf_rest([Conj|Rest]) :-
	write(' | '),
	print_conj(Conj),
	print_dnf_rest(Rest).

%------------------------------------------------------------------------------
% eliminate_not(+FormulaIn, -FormulaOut):
%------------------------------------------------------------------------------

% This is part of the translation of a formula to DNF.

eliminate_not(and(FIn1,FIn2), and(FOut1,FOut2)) :-
	!,
	eliminate_not(FIn1, FOut1),
	eliminate_not(FIn2, FOut2).

eliminate_not(or(FIn1,FIn2), or(FOut1,FOut2)) :-
	!,
	eliminate_not(FIn1, FOut1),
	eliminate_not(FIn2, FOut2).

eliminate_not(not(FIn1), FOut1) :-
	!,
	eliminate_not_negated(FIn1, FOut1).

eliminate_not(AtomicFormula, AtomicFormula) :-
	is_atomic_formula(AtomicFormula).

% eliminate_not_negated(+FormulaIn, -FormulaOut):

eliminate_not_negated(and(FIn1,FIn2), or(FOut1,FOut2)) :-
	!,
	eliminate_not_negated(FIn1, FOut1),
	eliminate_not_negated(FIn2, FOut2).

eliminate_not_negated(or(FIn1,FIn2), and(FOut1,FOut2)) :-
	!,
	eliminate_not_negated(FIn1, FOut1),
	eliminate_not_negated(FIn2, FOut2).

eliminate_not_negated(not(FIn1), FOut1) :-
	!,
	eliminate_not(FIn1, FOut1).

eliminate_not_negated(FIn, FOut) :-
	is_atomic_formula(FIn),
	complement_atomic_formula(FIn, FOut).

%------------------------------------------------------------------------------
% dnf(+FormulaIn, -DNF):
%------------------------------------------------------------------------------

% The input to DNF computation is a formula without negation.
% The output is a list of lists of atomic formulas.
% The inner lists are conjunctions, the outer one corresonds to a disjunction.

dnf(false, []) :-
	!.

dnf(true, [[]]) :-
	!.

dnf(AtomicFormula, [[AtomicFormula]]) :-
	is_atomic_formula(AtomicFormula).

dnf(and(F1,F2), DNF) :-
	dnf(F1, DNF1),
	dnf(F2, DNF2),
	dnf_multiply(DNF1, DNF2, DNF).

dnf(or(F1,F2), DNF) :-
	dnf(F1, DNF1),
	dnf(F2, DNF2),
	list_append(DNF1, DNF2, DNF).

% dnf_multiply(+DNFIn1, +DNFIn2, -DNFOut):

dnf_multiply([Conj1|Rest1], DNFIn2, DNFOut) :-
	dnf_and_all(Conj1, DNFIn2, DNFOut1),
	dnf_multiply(Rest1, DNFIn2, DNFOut2),
	list_append(DNFOut1, DNFOut2, DNFOut).

dnf_multiply([], _, []).

% dnf_and_all(+Conj, +DNFIn, -DNFOut):

dnf_and_all(_, [], []) :-
	!.

dnf_and_all(Conj1, [Conj2|Rest2], [ConjOut|RestOut]) :-
	list_append(Conj1, Conj2, ConjOut),
	dnf_and_all(Conj1, Rest2, RestOut).


%==============================================================================
% Type "Args" (List of Terms):
%==============================================================================


%------------------------------------------------------------------------------
% is_args(+Args):
%------------------------------------------------------------------------------

is_args([]).

is_args([Term|Args]) :-
	is_term(Term),
	is_args(Args).


%------------------------------------------------------------------------------
% print_args(+Args):
%------------------------------------------------------------------------------

print_args([]).

print_args([Arg|Rest]) :-
	write('('),
	print_term(Arg),
	print_args_rest(Rest),
	write(')').

% print_args_rest(+Args):

print_args_rest([]).

print_args_rest([Arg|Rest]) :-
	write(', '),
	print_term(Arg),
	print_args_rest(Rest).


%==============================================================================
% Type "Lit" (Literal in Rules):
%==============================================================================


%------------------------------------------------------------------------------
% is_lit(+Lit):
%------------------------------------------------------------------------------

is_lit(Lit) :-
	Lit =.. [Pred|Args],
	is_pred(Pred),
	is_args(Args).

%------------------------------------------------------------------------------
% print_lit(+Lit):
%------------------------------------------------------------------------------

% TODO: Introduce Type for Lits with Builtin Preds!

print_lit(plus_lt(X,Y,Z)) :-
	!,
	print_term(X),
	write(' + '),
	print_term(Y),
	write(' < '),
	print_term(Z).

print_lit(plus_ge(X,Y,Z)) :-
	!,
	print_term(X),
	write(' + '),
	print_term(Y),
	write(' >= '),
	print_term(Z).

print_lit(Lit) :-
	Lit =.. [Pred|Terms],
	print_pred(Pred),
	print_args(Terms).

%------------------------------------------------------------------------------
% lit_statearg(+Lit, -Arg):
%------------------------------------------------------------------------------

% ?unused

% The state/time argument is the first argument of standard literals.

lit_statearg(Lit, Arg) :-
	Lit =.. [_Pred, Arg|_].

% TODO: Check that Pred is not a built-in Predicate.


%------------------------------------------------------------------------------
% lit_pred(+Lit, -Pred):
%------------------------------------------------------------------------------

lit_pred(Lit, Pred) :-
	Lit =.. [Pred|_].

%==============================================================================
% Type "LitList" (List of Literals, e.g. Rule Body):
%==============================================================================


%------------------------------------------------------------------------------
% is_litlist(+LitList):
%------------------------------------------------------------------------------

is_litlist([]).

is_litlist([Lit|LitList]) :-
	is_lit(Lit),
	is_litlist(LitList).

%------------------------------------------------------------------------------
% print_litlist(+LitList):
%------------------------------------------------------------------------------

% One literal (indented by a TAB) is printed per line.

print_litlist([]).

print_litlist([Lit|Rest]) :-
	write('\t'),
	print_lit(Lit),
	print_litlist_rest(Rest).

% print_litlist_rest(+LitList):

print_litlist_rest([]).

print_litlist_rest([Lit|Rest]) :-
	write(', '),
	nl,
	write('\t'),
	print_lit(Lit),
	print_litlist_rest(Rest).


%==============================================================================
% Type "RID" (Rule Identifier):
%==============================================================================

% Typical rule identifiers are 1, 2, 3.

%------------------------------------------------------------------------------
% is_rid(+RID):
%------------------------------------------------------------------------------

is_rid(RID) :-
	integer(RID),
	RID > 0.

%------------------------------------------------------------------------------
% print_rid(+RID):
%------------------------------------------------------------------------------

print_rid(RID) :-
	write('('),
	write(RID),
	write(')').

%------------------------------------------------------------------------------
% make_rid(+No, -RID):
%------------------------------------------------------------------------------

make_rid(No, No) :-
	integer(No),
	No >= 1.


%==============================================================================
% Type "Rule":
%==============================================================================


%------------------------------------------------------------------------------
% is_rule(+Rule):
%------------------------------------------------------------------------------

is_rule(rule(No, Head, Body)) :-
	is_rid(No),
	is_lit(Head),
	is_litlist(Body).

% TODO: Should check that head does not contain built-in predicate!

%------------------------------------------------------------------------------
% print_rule(+Rule):
%------------------------------------------------------------------------------

print_rule(rule(No, Head, Body)) :-
	print_rid(No),
	write(' '),
	print_lit(Head),
	print_rule_body(Body),
	write('.'),
	nl.

% print_rule_body(+LitList): Handles facts specially (empty body).

print_rule_body([]).

print_rule_body([Lit|Rest]) :-
	write(' :- '),
	nl,
	print_litlist([Lit|Rest]).

%------------------------------------------------------------------------------
% rule_data(+Rule, -No, -Head, -Body):
%------------------------------------------------------------------------------

rule_data(rule(No, Head, Body), No, Head, Body).

%------------------------------------------------------------------------------
% make_rule(+No, +Head, +Body, -Rule):
%------------------------------------------------------------------------------

make_rule(No, Head, Body, rule(No, Head, Body)) :-
	is_rid(No),
	is_lit(Head),
	is_litlist(Body).


%==============================================================================
% Type "CID" (Constraint Identifier):
%==============================================================================

% Typical constraint identifiers are 'A', 'B', 'C'.

%------------------------------------------------------------------------------
% is_cid(+CID):
%------------------------------------------------------------------------------

is_cid(CID) :-
	atom(CID).

%------------------------------------------------------------------------------
% print_cid(+CID):
%------------------------------------------------------------------------------

print_cid(CID) :-
	write('('),
	write(CID),
	write(')').

%------------------------------------------------------------------------------
% make_cid(+No, -CID):
%------------------------------------------------------------------------------

make_cid(No, CID) :-
	integer(No),
	No >= 1,
	make_cid_cases(No, CID).

% make_cid_cases(+No, -CID):

make_cid_cases(No, CID) :-
	make_cid_letter(No, CID),
	!.

make_cid_cases(No, CID) :-
	number_chars(No, Chars),
	atom_chars(CID, ['C'|Chars]).

% make_cid_letter(+No, -CID):

make_cid_letter( 1, 'A').
make_cid_letter( 2, 'B').
make_cid_letter( 3, 'C').
make_cid_letter( 4, 'D').
make_cid_letter( 5, 'E').
make_cid_letter( 6, 'F').
make_cid_letter( 7, 'G').
make_cid_letter( 8, 'H').
make_cid_letter( 9, 'I').
make_cid_letter(10, 'J').
make_cid_letter(11, 'K').
make_cid_letter(12, 'L').
make_cid_letter(13, 'M').
make_cid_letter(14, 'N').
make_cid_letter(15, 'O').
make_cid_letter(16, 'P').
make_cid_letter(17, 'Q').
make_cid_letter(18, 'R').
make_cid_letter(19, 'S').
make_cid_letter(20, 'T').
make_cid_letter(21, 'U').
make_cid_letter(22, 'V').
make_cid_letter(23, 'W').
make_cid_letter(24, 'X').
make_cid_letter(25, 'Y').
make_cid_letter(26, 'Z').

%==============================================================================
% Type "Constraint":
%==============================================================================

% These are the generalized exclusion constraints from our paper.
% They have the form <- Lit1, Lit2, Formula
% where Formula is either true or a disjunction of disequations Term1 <> Term2
% between a term from Lit1 and a Term from Lit2.

%------------------------------------------------------------------------------
% is_constraint(+Constraint):
%------------------------------------------------------------------------------

is_constraint(constraint(ID, Lit1, Lit2, Formula)) :-
	is_cid(ID),
	is_lit(Lit1),
	is_lit(Lit2),
	is_formula(Formula).

% TODO: Should check that Lit1 and Lit2 have no built-in predicate.

%------------------------------------------------------------------------------
% print_constraint(+Constraint):
%------------------------------------------------------------------------------

print_constraint(constraint(ID, Lit1, Lit2, Formula)) :-
	print_cid(ID),
	write(' '),
	write('<- '),
	print_lit(Lit1),
	write(', '),
	print_lit(Lit2),
	print_opt_formula(Formula),
	write('.'),
	nl.

% print_opt_formula(+Formula):

print_opt_formula(true) :-
	!.

print_opt_formula(Formula) :-
	write(','),
	nl,
	write('       '),
	print_formula(Formula).

%------------------------------------------------------------------------------
% constraint_data(+Constraint, -ID, -Lit1, -Lit2, -Formula):
%------------------------------------------------------------------------------

constraint_data(constraint(ID,Lit1,Lit2,Formula), ID, Lit1, Lit2, Formula).


%------------------------------------------------------------------------------
% make_constraint(+ID, +Lit1, +Lit2, +Formula, +Constraint):
%------------------------------------------------------------------------------

make_constraint(ID, Lit1, Lit2, Formula, constraint(ID,Lit1,Lit2,Formula)) :-
	is_cid(ID),
	is_lit(Lit1),
	is_lit(Lit2),
	is_formula(Formula).


%==============================================================================
% Type "IDGen" (Generator for Rule and Constraint IDs):
%==============================================================================

% idgen(RNo,CNo) contains the number of rules and the number of constraints
% read so far.

%------------------------------------------------------------------------------
% is_idgen(+IDGen):
%------------------------------------------------------------------------------

is_idgen(idgen(RNo,CNo)) :-
	integer(RNo),
	RNo >= 0,
	integer(CNo),
	CNo >= 0.

%------------------------------------------------------------------------------
% print_idgen(+IDGen):
%------------------------------------------------------------------------------

print_idgen(idgen(RNo,CNo)) :-
	write('IDGen('),
	write(RNo),
	write(','),
	write(CNo),
	write(')').

%------------------------------------------------------------------------------
% idgen_init(-IDGen):
%------------------------------------------------------------------------------

idgen_init(idgen(0,0)).

%------------------------------------------------------------------------------
% idgen_next_rid(+IDGenIn, -RID, -IDGenOut):
%------------------------------------------------------------------------------

idgen_next_rid(idgen(RNo,CNo), RID, idgen(NextRNo,CNo)) :-
	NextRNo is RNo + 1,
	make_rid(NextRNo, RID).

%------------------------------------------------------------------------------
% idgen_next_cid(+IDGenIn, -CID, -IDGenOut):
%------------------------------------------------------------------------------

idgen_next_cid(idgen(RNo,CNo), CID, idgen(RNo,NextCNo)) :-
	NextCNo is CNo + 1,
	make_cid(NextCNo, CID).


%==============================================================================
% Type "VioCond" (Violation Conditions):
%==============================================================================


%------------------------------------------------------------------------------
% is_viocond(+VioCond):
%------------------------------------------------------------------------------

is_viocond(viocond(ID, No1, No2, LitList, Formula)) :-
	is_cid(ID),
	is_rid(No1),
	is_rid(No2),
	is_litlist(LitList),
	is_formula(Formula).

%------------------------------------------------------------------------------
% print_viocond(+VioCond):
%------------------------------------------------------------------------------

print_viocond(viocond(ID, No1, No2, LitList, Formula)) :-
	write('Constraint '),
	print_cid(ID),
	write(' with Rule '),
	print_rid(No1),
	write(' and Rule '),
	print_rid(No2),
	write(':'),
	nl,
	print_viocond_cases(LitList, Formula),
	write('.'),
	nl,
	nl.

% print_viocond_cases(+LitList, +Formula):

print_viocond_cases([], true) :-
	!,
	write('true').

print_viocond_cases([Lit|Rest], true) :-
	!,
	print_litlist([Lit|Rest]).

print_viocond_cases([], Formula) :-
	!,
	write('\t'),
	print_formula(Formula).

print_viocond_cases([Lit|Rest], Formula) :-
	print_litlist([Lit|Rest]),
	write(','),
	nl,
	write('\t'),
	print_formula(Formula).

%------------------------------------------------------------------------------
% make_viocond(+ID, +No1, +No2, +LitList, +Formula, -VioCond):
%------------------------------------------------------------------------------

make_viocond(ID, No1, No2, LitList, Formula,
		viocond(ID, No1, No2, LitList, Formula)).

%------------------------------------------------------------------------------
% viocond_lits(+VioCond, -LitList):
%------------------------------------------------------------------------------

viocond_lits(viocond(_ID, _No1, _No2, LitList, _Formula), LitList).

%------------------------------------------------------------------------------
% viocond_formula(+VioCond, -Formula):
%------------------------------------------------------------------------------

viocond_formula(viocond(_ID, _No1, _No2, _LitList, Formula), Formula).


%==============================================================================
% Type "VCList" (List of Violation Conditions):
%==============================================================================


%------------------------------------------------------------------------------
% is_vclist(+VCList):
%------------------------------------------------------------------------------

is_vclist([]).

is_vclist([VioCond|VCList]) :-
	is_viocond(VioCond),
	is_vclist(VCList).

%------------------------------------------------------------------------------
% print_vclist(+VCList):
%------------------------------------------------------------------------------

print_vclist([]).

print_vclist([VioCond|Rest]) :-
	print_viocond(VioCond),
	print_vclist(Rest).


%==============================================================================
% Type "VCStat" (Statistics for Violation Conditions):
%==============================================================================


%------------------------------------------------------------------------------
% is_vcstat(+VCStat):
%------------------------------------------------------------------------------

is_vcstat(vcstat(NumVCond,NumRefuted,NonRefutedList)) :-
	integer(NumVCond),
	NumVCond >= 0,
	integer(NumRefuted),
	NumRefuted >= 0,
	NumVCond >= NumRefuted,
	is_vclist(NonRefutedList),
	list_length(NonRefutedList, L),
	L is NumVCond - NumRefuted.

%------------------------------------------------------------------------------
% print_vcstat(+VCStat):
%------------------------------------------------------------------------------

print_vcstat(vcstat(NumVCond,NumRefuted,_)) :-
	write('Total Number of Violation Conditions: '),
	write(NumVCond),
	nl,
	write('Refuted:     '),
	write(NumRefuted),
	nl,
	NotRefuted is NumVCond - NumRefuted,
	write('Not Refuted: '),
	write(NotRefuted),
	nl.

%------------------------------------------------------------------------------
% print_vcstat(+VCStat):
%------------------------------------------------------------------------------

print_vcstat_long(vcstat(NumVCond,NumRefuted,NonRefutedList)) :-
	print_vcstat(vcstat(NumVCond,NumRefuted,NonRefutedList)),
	nl,
	print_opt_nonrefuted(NonRefutedList).

% print_opt_nonrefuted(+VCList):

print_opt_nonrefuted([]) :-
	write('*** All Violation conditions refuted, constraints proven ***'),
	nl.

print_opt_nonrefuted([VioCond|VCList]) :-
	write('Non Refuted Violation Conditions:'),
	nl,
	write('================================'),
	nl,
	nl,
	print_vclist([VioCond|VCList]).

%------------------------------------------------------------------------------
% init_vcstat(-VCStat):
%------------------------------------------------------------------------------

init_vcstat(vcstat(0,0,[])).

%------------------------------------------------------------------------------
% inc_refuted(+VCStatIn, -VCStatOut):
%------------------------------------------------------------------------------

inc_refuted(vcstat(NumVCondIn,NumRefutedIn,VCList),
		vcstat(NumVCondOut,NumRefutedOut,VCList)) :-
	NumVCondOut is NumVCondIn + 1,
	NumRefutedOut is NumRefutedIn + 1.

%------------------------------------------------------------------------------
% inc_nonrefuted(+VCStatIn, +VioCond, -VCStatOut):
%------------------------------------------------------------------------------

inc_nonrefuted(vcstat(NumVCondIn,NumRefuted,VCListIn),
		VioCond,
		vcstat(NumVCondOut,NumRefuted,VCListOut)) :-
	NumVCondOut is NumVCondIn + 1,
	list_append(VCListIn, [VioCond], VCListOut).


%==============================================================================
% Type "Refute" (Reason why Violation Condition is not Satisfiable):
%==============================================================================


%------------------------------------------------------------------------------
% is_refute(+Refute):
%------------------------------------------------------------------------------

is_refute(retfute0(VFormula)) :-
	is_formula(VFormula).

is_refute(refute1(Lit1,Lit2,ID,VFormula)) :-
	is_lit(Lit1),
	is_lit(Lit2),
	is_cid(ID),
	is_formula(VFormula).

%------------------------------------------------------------------------------
% print_refute(+Refute):
%------------------------------------------------------------------------------

print_refute(refute0(VFormula)) :-
	write('\tViolation condition is inconsistent:'),
	nl,
	write('\tVForm: '),
	print_formula(VFormula),
	nl.

print_refute(refute1(Lit1,Lit2,ID,VFormula)) :-
	write('\tViolation condition is inconsistent with constraint '),
	print_cid(ID),
	nl,
	write('\tLit 1: '),
	print_lit(Lit1),
	nl,
	write('\tLit 2: '),
	print_lit(Lit2),
	nl,
	write('\tVForm: '),
	print_formula(VFormula),
	nl.

%------------------------------------------------------------------------------
% make_refute0(+VFormula, -Refute):
%------------------------------------------------------------------------------

% The built-in literals together with the formula from the constraint
% of the violation were already inconsistent.
% It was not necessary to apply a constraint.

make_refute0(VFormula, refute0(VFormula)).

%------------------------------------------------------------------------------
% make_refute1(+Lit1, +Lit2, +ID, +VFormula, -Refute):
%------------------------------------------------------------------------------

% Violation condition was refuted by applying constraint ID
% to literals Lit1 and Lit2 of the violation condition.
% The resulting violation formula Cond was inconsistent.

make_refute1(Lit1, Lit2, ID, VFormula, refute1(Lit1,Lit2,ID,VFormula)).


%==============================================================================
% Type "Subst" (Substitutions):
%==============================================================================

% Substitutions are represented as lists of variable->Term mappings.
% However, it is necessary to repeatedly apply the mapping.
% E.g. [subst(X,Y), subst(Y,Z)] represents {X/Z, Y/Z}.
% In order to avoid cycles, we check that when X/T is added (at the end),
% there is no substitution for T. And of course, no substition for X.
% The unification algorithm guarantees this property.

%------------------------------------------------------------------------------
% is_subst(+Subst):
%------------------------------------------------------------------------------

is_subst([]).

is_subst([subst(Var,Term)|Rest]) :-
	is_var(Var),
	is_term(Term),
	is_subst(Rest).

%------------------------------------------------------------------------------
% empty_subst(-Subst):
%------------------------------------------------------------------------------

empty_subst([]).

%------------------------------------------------------------------------------
% subst_one(+Var, +Term, -Subst):
%------------------------------------------------------------------------------

subst_one(v(Var), Term, [subst(v(Var),Term)]) :-
	Term \= v(Var).

subst_one(v(Var,No), Term, [subst(v(Var,No),Term)]) :-
	Term \= v(Var,No).

%------------------------------------------------------------------------------
% subst_add(+SubstIn, +Var, +Term, -SubstOut):
%------------------------------------------------------------------------------

% SubstIn must not contain a mapping for Var alreay.

%subst_add(SubstIn, Var, Term, [subst(Var,Term)|SubstOut]) :-
%	no_subst_for(SubstIn, Var).

subst_add([], v(Var), Term, [subst(v(Var),Term)]) :-
	Term \= v(Var).

subst_add([], v(Var,No), Term, [subst(v(Var,No),Term)]) :-
	Term \= v(Var,No).

subst_add([subst(OtherVar,OtherTerm)|RestIn], Var, Term, 
		[subst(OtherVar,OtherTerm)|RestOut]) :-
	Var \= OtherVar,
	Term \= OtherVar,
	subst_add(RestIn, Var, Term, RestOut).

%------------------------------------------------------------------------------
% no_subst_for(+SubstIn, +Var):
%------------------------------------------------------------------------------

% unused?

no_subst_for([], _Var).

no_subst_for([subst(OtherVar,_)|Rest], Var) :-
	OtherVar \= Var,
	no_subst_for(Rest, Var).

%------------------------------------------------------------------------------
% do_subst_var(+Var, +Subst, -Term):
%------------------------------------------------------------------------------

do_subst_var(Var, Subst, Term) :-
	do_subst_var_search(Subst, Var, Subst, Term).

% do_subst_var_search(+RestSubst, +Var, +OriginalSubst, -Term):
do_subst_var_search([subst(Var,Term)|_], Var, Subst, TermOut) :-
	% If substitution was done, apply Subst again to result:
	do_subst_term(Term, Subst, TermOut).

do_subst_var_search([subst(OtherVar,_)|RestSubst], Var, Subst, Term) :-
	Var \= OtherVar,
	do_subst_var_search(RestSubst, Var, Subst, Term).

do_subst_var_search([], Var, _Subst, Var).
	% If no substitution was done, we are done.

%------------------------------------------------------------------------------
% do_subst_term(+TermIn, +Subst, -TermOut):
%------------------------------------------------------------------------------

do_subst_term(v(Var), Subst, TermOut) :-
	do_subst_var(v(Var), Subst, TermOut).

do_subst_term(v(Var,No), Subst, TermOut) :-
	do_subst_var(v(Var,No), Subst, TermOut).

do_subst_term(Const, _Subst, Const) :-
	is_const(Const).

%------------------------------------------------------------------------------
% do_subst_termlist(+TermsIn, +Subst, -TermsOut):
%------------------------------------------------------------------------------

do_subst_termlist([], _Subst, []).

do_subst_termlist([TermIn|RestIn], Subst, [TermOut|RestOut]) :-
	do_subst_term(TermIn, Subst, TermOut),
	do_subst_termlist(RestIn, Subst, RestOut).

%------------------------------------------------------------------------------
% do_subst_lit(+LitIn, +Subst, -LitOut):
%------------------------------------------------------------------------------

do_subst_lit(LitIn, Subst, LitOut) :-
	LitIn =.. [Pred|ArgsIn],
	do_subst_termlist(ArgsIn, Subst, ArgsOut),
	LitOut =.. [Pred|ArgsOut].

%------------------------------------------------------------------------------
% do_subst_litlist(+LitsIn, +Subst, -LitsOut):
%------------------------------------------------------------------------------

do_subst_litlist([], _Subst, []).

do_subst_litlist([LitIn|RestIn], Subst, [LitOut|RestOut]) :-
	do_subst_lit(LitIn, Subst, LitOut),
	do_subst_litlist(RestIn, Subst, RestOut).

%------------------------------------------------------------------------------
% do_subst_formula(+FormulaIn, +Subst, -FormulaOut):
%------------------------------------------------------------------------------

do_subst_formula(or(FormulaIn1,FormulaIn2), Subst,
			or(FormulaOut1,FormulaOut2)) :-
	!,
	do_subst_formula(FormulaIn1, Subst, FormulaOut1),
	do_subst_formula(FormulaIn2, Subst, FormulaOut2).

do_subst_formula(and(FormulaIn1,FormulaIn2), Subst,
			and(FormulaOut1,FormulaOut2)) :-
	!,
	do_subst_formula(FormulaIn1, Subst, FormulaOut1),
	do_subst_formula(FormulaIn2, Subst, FormulaOut2).

do_subst_formula(not(FormulaIn1), Subst,
			not(FormulaOut1)) :-
	!,
	do_subst_formula(FormulaIn1, Subst, FormulaOut1).

do_subst_formula(LitIn, Subst, LitOut) :-
	do_subst_lit(LitIn, Subst, LitOut).

%------------------------------------------------------------------------------
% print_subst(+Subst):
%------------------------------------------------------------------------------

% This prints the real substitution, as defined in theory,
% where variables are replaced once in parallel.
% Since the list contains only single replacement steps,
% we use do_subst_term to get the final version of the replacement term.

print_subst([]) :-
	write('{}').

print_subst([subst(Var,Term)|Rest]) :-
	write('{'),
	print_subst_pair(Var, Term, [subst(Var,Term)|Rest]),
	print_subst_rest(Rest, [subst(Var,Term)|Rest]),
	write('}').

% print_subst_pair(+Var, +Term, +Subst):

print_subst_pair(Var, Term, Subst) :-
	print_var(Var),
	write('/'),
	do_subst_term(Term, Subst, FinalTerm),
	print_term(FinalTerm).

% print_subst_rest(+PairList, +Subst):

print_subst_rest([], _Subst).

print_subst_rest([subst(Var,Term)|Rest], Subst) :-
	write(', '),
	print_subst_pair(Var, Term, Subst),
	print_subst_rest(Rest, Subst).

%==============================================================================
% Type "Token":
%==============================================================================

% The lexical scanner returns a list of tokens.

%------------------------------------------------------------------------------
% is_token(+Token):
%------------------------------------------------------------------------------

			% E.g.:
is_token(atom(_)).	% ab    (alphanumeric, starts with lowercase letter).
is_token(var(_)).	% X     (alphanumeric, starts with uppercase letter).
is_token(int(_)).	% 123   (sequence of digits).
is_token(str(_)).	% 'abc' (any characters enclosed in '...')
is_token(cconst(_)).	% #LOW  (alphanumeric after #, first must be letter)
is_token(lparen).	% (
is_token(rparen).	% )
is_token(comma).	% ,
is_token(fullstop) :-	% .     (followed by whitespace)
is_token(if).		% <- or :-
is_token(comp(eq)).	% =
is_token(comp(ne)).	% != or \=
is_token(comp(lt)).	% <
is_token(comp(le)).	% <= or =<
is_token(comp(gt)).	% >
is_token(comp(ge)).	% >=
is_token(plus).		% +
is_token(at(AtKeyword)) :-	% @next, @init, @start, @setup, @call, @ret
	at_keyword(AtKeyword).
is_token(or).		% |
is_token(and).		% &
is_token(param).	% ?
is_token(not).		% \+ or !

%------------------------------------------------------------------------------
% at_keyword(+Keyword):
%------------------------------------------------------------------------------

% Possible Keywords after @:
at_keyword(next).
at_keyword(this).
at_keyword(init).
at_keyword(start).
at_keyword(setup).
at_keyword(call).
at_keyword(ret).

%------------------------------------------------------------------------------
% comparison_op(+Op):
%------------------------------------------------------------------------------

% ? unused

comparison_op(eq).
comparison_op(ne).
comparison_op(lt).
comparison_op(le).
comparison_op(gt).
comparison_op(ge).

%------------------------------------------------------------------------------
% print_token(Token):
%------------------------------------------------------------------------------

print_token(atom(Atom)) :-
	write(Atom).

print_token(var(Var)) :-
	write(Var).

print_token(int(Int)) :-
	write(Int).

print_token(str(Str)) :-
	write('\''),
	print_chars(Str),
	write('\'').

print_token(cconst(Const)) :-
	write('#'),
	write(Const).

print_token(lparen) :-
	write('(').

print_token(rparen) :-
	write(')').

print_token(comma) :-
	write('\',\'').

print_token(fullstop) :-
	write('\'.\'').

print_token(if) :-
	write('<-').

print_token(comp(eq)) :-
	write('=').

print_token(comp(ne)) :-
	write('!=').

print_token(comp(lt)) :-
	write('<').

print_token(comp(le)) :-
	write('<=').

print_token(comp(gt)) :-
	write('>').

print_token(comp(ge)) :-
	write('>=').

print_token(at(AtKeyword)) :-
	at_keyword(AtKeyword),
	!,
	write('@'),
	write(AtKeyword).

print_token(plus) :-
	write('+').

print_token(or) :-
	write('|').

print_token(and) :-
	write('&').

print_token(not) :-
	write('\\+').

print_token(param) :-
	write('?').

%------------------------------------------------------------------------------
% print_token_list(+TokenList):
%------------------------------------------------------------------------------

print_token_list([]).

print_token_list([Token|Rest]) :-
	write('\t'),
	print_token(Token),
	nl,
	print_token_list(Rest).

%------------------------------------------------------------------------------
% print_token_type(Token):
%------------------------------------------------------------------------------

print_token_type(atom(_)) :-
	!,
	write('Atom').

print_token_type(var(_)) :-
	!,
	write('Variable').

print_token_type(int(_)) :-
	!,
	write('Integer').

print_token_type(str(_)) :-
	!,
	write('String').

print_token_type(cconst(_)) :-
	!,
	write('#-Const').

print_token_type(at(_)) :-
	!,
	write('@').

print_token_type(comp(_)) :-
	!,
	write('Comparison operator').

print_token_type(OtherToken) :-
	print_token(OtherToken),
	!.

print_token_type(Unknown) :-
	write('token type '),
	write(Unknown),
	write(' (??? Please inform programmer)').
