% =============================================================================
% Project:	Deductive Database
% Filename:	ddb.pl
% Purpose:	Execution environment for deductive database in Datalog
% Last Change:	20.05.2012
% Language:	C++
% 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) 2010-2012 by Stefan Brass
%		Downloads and modifications for tests and scientific purposes
%		permitted, provided that some acknowledgement of my work
%		remains, and modified versions are clearly marked as such.
%		There is no warranty at all - this code may contain bugs.
%		Note that it is only a prototype for language demonstration,
%		it is not yet intended for real applications!
% =============================================================================

%==============================================================================
% Main Predicate, call this predicate to start program:
%==============================================================================

odl(File) :-
	main(File, []).

odl(File, Options) :-
	main(File, Options).

%------------------------------------------------------------------------------
% Abbreviations for calling main for example files (with all options):
%------------------------------------------------------------------------------

ex :- main('ex.odl', 'ifsd').
ex2 :- main('ex2.odl', 'ifsd').
hello :- main('hello.odl', 'ifsd').

%==============================================================================
% Dynamic Database:
%==============================================================================

 % Facts describing the input program. See example below.
:- dynamic prog/1.

 % Facts describing the current rule (not yet in prog):
:- dynamic rule/1.

% Derived facts:  derived(Fact, Partition, Order)
:- dynamic derived/3.

% derived_with_pos(Fact, RowNumber, Rank, DenseRank, Last)
:- dynamic derived_with_pos/5.

% derived_pred(Pred, Arity):
:- dynamic derived_pred/2.

% err_info(FirstLineNo, LastLineNo, Chars).
:- dynamic err_info/3.

% stratification(Level, Pred, Arity):
:- dynamic stratification/3.

% partition_value(Pred, Arity, Partition).
:- dynamic partition_value/3.

% option(Option), see option_list/3 below.
:- dynamic option/1.

%------------------------------------------------------------------------------
% Representation of the input program as prog/1 facts:
%------------------------------------------------------------------------------

% fact(RuleNo, LineNo)
% rule(RuleNo, LineNo, NumBodyLit)
%
% lit(RuleNo, LitNo, Pred, NumArgs) // LitNo == 0 means head literal
% complit(RuleNo, LitNo, Op)
%
% arg(RuleNo, LitNo, ArgNo, var,  Var)
% arg(RuleNo, LitNo, ArgNo, str,  Str)
% arg(RuleNo, LitNo, ArgNo, int,  Int)
% arg(RuleNo, LitNo, ArgNo, const, Const)
%
% negated(RuleNo, LitNo).
%
% order(RuleNo, LitNo, Pos, DescAsc, var, Var) // Order Argument in Head
%               // LitNo is always 0. Maybe later we allow order spec in body.
%
% partition(RuleNo, LitNo, ArgNo). // ArgNo is No of Last Part Arg in order().
% order_spec(RuleNo, LitNo, ArgNo). // ArgNo is No of Last Arg in order().
%
% ordered_pred(Pred, Arity).
%
% row_number(RuleNo, LitNo, ArgType, Arg). // ArgType is int or var.
% rank(RuleNo, LitNo, ArgType, Arg).
% dense_rank(RuleNo, LitNo, ArgType, Arg).
% next(RuleNo, LitNo, ArgType, Arg).

%------------------------------------------------------------------------------
% Example: emp_by_sal<Job|Sal>(EName, Sal) <- emp(EName, Sal, Job). // Rule 8
%------------------------------------------------------------------------------

%	rule(8, 12, 1).
%	lit(8, 0, emp_by_sal, 2).
%	order(8, 0, 1, asc_var, Job).
%	partition(8, 0, 1).
%	order(8, 0, 2, asc_var, Sal).
%	arg(8, 0, 1, var, EName).
%	arg(8, 0, 2, var, Sal).
%	lit(8, 1, emp, 3).
%	arg(8, 1, 1, var, EName).
%	arg(8, 1, 2, var, Sal).
%	arg(8, 1, 3, var, Job).

%------------------------------------------------------------------------------
% Example: answer(EName, Sal) <- emp_by_sal[N](EName, Sal), N <= 3. // Rule 9
%------------------------------------------------------------------------------

%	rule(9, 14, 2).
%	lit(9, 0, answer, 2).
%	arg(9, 0, 1, var, EName).
%	arg(9, 0, 2, var, Sal).
%	lit(9, 1, emp_by_sal, 2).
%	row_number(9, 1, var, N).
%	arg(9, 1, 1, var, EName).
%	arg(9, 1, 2, var, Sal).
%	complit(9, 2, le).
%	arg(9, 2, 1, var, N).
%	arg(9, 2, 2, int, 3).


%==============================================================================
% Main Program:
%==============================================================================

main(File, Options) :-
	retractall(prog(_)),
	retractall(rule(_)),
	retractall(derived(_,_,_)),
	retractall(derived_with_pos(_,_,_,_,_)),
	retractall(derived_pred(_,_)),
	retractall(stratification(_,_,_)),
	retractall(option(_)),
	atom_chars(Options, OptionList),
	process_options(OptionList),
	read_source_program(File),
	!,
	nl,
	eval_if_no_error,
	!.

%------------------------------------------------------------------------------
% eval_if_no_error:
%------------------------------------------------------------------------------

eval_if_no_error :-
	prog(error(_,_)),
	!.

eval_if_no_error :-
	stratification_error,
	!.

eval_if_no_error :-
	compute_stratification(MaxLevel),
	!,
	show_stratification(MaxLevel),
	write('Bottom-Up Evaluation starts ...\n'),
	botup(MaxLevel),
	write('done.\n'),
	show_derived_facts,
	show_output,
	show_answer,
	nl,
	!.


%==============================================================================
% Management of Options:
%==============================================================================

%------------------------------------------------------------------------------
% process_options(+OptionList):
%------------------------------------------------------------------------------

process_options([]).

process_options([' '|MoreOptions]) :-
	!,
	process_options(MoreOptions).

process_options([OptionChar|MoreOptions]) :-
	decode_option(OptionChar, OptionID),
	store_option(OptionID),
	process_options(MoreOptions).

%------------------------------------------------------------------------------
% decode_option(+OptionChar -OptionID):
%------------------------------------------------------------------------------

decode_option(OptionChar, OptionID) :-
	option_list(OptionChar, OptionID, _),
	!.

decode_option(OptionChar, _) :-
	nl,
	write('Unknown Option: \''),
	write(OptionChar),
	write('\'.'),
	nl,
	fail.

%------------------------------------------------------------------------------
% option_list(?OptionChar, ?OptionID, ?HelpText):
%------------------------------------------------------------------------------

option_list('i', show_input_chars, 'Show input rules').
option_list('f', show_input_facts, 'Show facts representing input rules').
option_list('s', show_stratification, 'Show stratification').
option_list('d', show_derived_facts, 'Show all derived facts').

%------------------------------------------------------------------------------
% store_option(+OptionID):
%------------------------------------------------------------------------------

store_option(Option) :-
	option(Option), % Already defined.
	!.

store_option(Option) :-
	assert(option(Option)).

%------------------------------------------------------------------------------
% show_option_list:
%------------------------------------------------------------------------------

show_option_list :-
	write('Possible Options:'),
	nl,
	option_list(Option, _, HelpText), % Backtracks over all options
	write('    '),
	write(Option),
	write(': '),
	write(HelpText),
	nl,
	fail.

show_option_list.

%==============================================================================
% Read Source Program:
%==============================================================================

read_source_program(File) :-
	open(File, read, Stream),
	read_source_rules(Stream, 1),
	close(Stream).

read_source_rules(Stream, RuleNo) :-
	skip_spaces(Stream),
	at_end_of_stream(Stream) -> 
		finished_reading
	;	line_count(Stream, FirstLine),
		read_source_rule(Stream, Chars, LastLineNo),
		show_source_rule(RuleNo, Chars),
		parse(Chars, RuleNo, FirstLine, LastLineNo, Facts),
		show_input_facts(Facts),
		assert_facts(Facts),
		NewRuleNo is RuleNo + 1,
		read_source_rules(Stream, NewRuleNo).

finished_reading :-
	prog(error(_,_)),
	!,
	write('Finished reading source program (with errors).\n').

finished_reading :-
	write('Finished reading source program.\n').

%------------------------------------------------------------------------------
% skip_spaces(+Stream): Position Stream on next non-space/comment character.
%------------------------------------------------------------------------------

skip_spaces(Stream) :-
	peek_char(Stream, Char),
	(is_space(Char) -> get_char(Stream, Char), skip_spaces(Stream);
	is_comment(Char) -> get_char(Stream, Char), skip_comment(Stream),
				skip_spaces(Stream);
	true).

%------------------------------------------------------------------------------
% skip_comment(+Stream): Skip to end of line or end of file.
%------------------------------------------------------------------------------

skip_comment(Stream) :-
	get_char(Stream, Char),
	(Char == end_of_file -> true;
	Char == '\n' -> true;
	skip_comment(Stream)).

%------------------------------------------------------------------------------
% read_source_rule(+Stream, -Chars, -LastLineNo): Read characters until '.'.
%------------------------------------------------------------------------------

% LastLineNo is the number of the line with the final '.':

read_source_rule(Stream, Chars, LastLineNo) :-
	get_char(Stream, Char),
	read_source_rule_cont(Stream, Char, Chars, LastLineNo).

% read_source_rule_cont(+Stream, +Char, -Chars, -LastLineNo):

read_source_rule_cont(Stream, end_of_file, [], LastLineNo) :-
	!,
	line_count(Stream, LastLineNo).

read_source_rule_cont(Stream, '.', ['.'], LastLineNo) :-
	line_count(Stream, LastLineNo),
	whitespace(Stream),
	!.

read_source_rule_cont(Stream, '\'', ['\''|Rest], LastLineNo) :-
	get_char(Stream, Next_Char),
	read_source_rule_str(Stream, Next_Char, Rest, LastLineNo).

read_source_rule_cont(Stream, '%', ['%'|Rest], LastLineNo) :-
	get_char(Stream, Next_Char),
	read_source_rule_comment(Stream, Next_Char, Rest, LastLineNo).

read_source_rule_cont(Stream, Char, [Char|Rest], LastLineNo) :-
	get_char(Stream, Next_Char),
	read_source_rule_cont(Stream, Next_Char, Rest, LastLineNo).

% There is a certain duplication with the lexical scanner here.
% We must continue reading characters if '.' occurs inside a string constant.
% The same, if it occurs inside a comment.
%
% read_source_rule_str(+Stream, +Char, -Chars, -LastLineNo):

read_source_rule_str(Stream, end_of_file, [], LastLineNo) :-
	!,
	line_count(Stream, LastLineNo).

read_source_rule_str(Stream, '\'', ['\''|Rest], LastLineNo) :-
	!,
	get_char(Stream, Next_Char),
	read_source_rule_cont(Stream, Next_Char, Rest, LastLineNo).

read_source_rule_str(Stream, Char, [Char|Rest], LastLineNo) :-
	get_char(Stream, Next_Char),
	read_source_rule_str(Stream, Next_Char, Rest, LastLineNo).

% read_source_rule_comment(+Stream, +Char, -Chars, -LastLineNo):

read_source_rule_comment(Stream, end_of_file, [], LastLineNo) :-
	!,
	line_count(Stream, LastLineNo).

read_source_rule_comment(Stream, '\n', ['\n'|Rest], LastLineNo) :-
	!,
	get_char(Stream, Next_Char),
	read_source_rule_cont(Stream, Next_Char, Rest, LastLineNo).

read_source_rule_comment(Stream, Char, [Char|Rest], LastLineNo) :-
	get_char(Stream, Next_Char),
	read_source_rule_comment(Stream, Next_Char, Rest, LastLineNo).

%------------------------------------------------------------------------------
% whitespace(+Stream):
%------------------------------------------------------------------------------

% True if at least one whitespace character in stream,
% skips all whitespace until line end.

whitespace(Stream) :-
	peek_char(Stream, C),
	is_space(C),
	!,
	skip_whitespace_to_nl(Stream).

%------------------------------------------------------------------------------
% skip_whitespace_to_nl(+Stream):
%------------------------------------------------------------------------------

skip_whitespace_to_nl(Stream) :-
	peek_char(Stream, '\n'),
	!,
	get_char(Stream, '\n').

skip_whitespace_to_nl(Stream) :-
	peek_char(Stream, C),
	is_space(C),
	get_char(Stream, C),
	!,
	skip_whitespace_to_nl(Stream).

skip_whitespace_to_nl(_).

%------------------------------------------------------------------------------
% assert_facts(+Facts):
%------------------------------------------------------------------------------

assert_facts([]).

assert_facts([Fact|MoreFacts]) :-
	assert(prog(Fact)),
	assert_facts(MoreFacts).

%==============================================================================
% Output (Unparser):
%==============================================================================

%------------------------------------------------------------------------------
% show_source_rule(+RuleNo, +Chars):
%------------------------------------------------------------------------------

show_source_rule(RuleNo, Chars) :-
	option(show_input_chars),
	!,
	write(RuleNo),
	write('. '),
	print_chars(Chars),
	nl.

show_source_rule(_, _).

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

print_chars([]) :-
	nl.

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

%------------------------------------------------------------------------------
% show_input_facts(+Facts):
%------------------------------------------------------------------------------

show_input_facts(Facts) :-
	option(show_input_facts),
	!,
	%write(Facts), nl,
	show_facts(Facts),
	!.

show_input_facts(_).

%------------------------------------------------------------------------------
% show_facts(+Facts):
%------------------------------------------------------------------------------

show_facts([]) :-
	nl.

show_facts([Fact|MoreFacts]) :-
	write('\t'),
	show_fact(Fact),
	nl,
	show_facts(MoreFacts).

%------------------------------------------------------------------------------
% show_fact(+Fact):
%------------------------------------------------------------------------------

show_fact(Fact) :-
	Fact =.. [Pred|Args],
	write(Pred),
	show_args(Args),
	write('.').

%------------------------------------------------------------------------------
% show_args(+ArgList):
%------------------------------------------------------------------------------

show_args([]).

show_args([Arg|Args]) :-
	write('('),
	show_arg(Arg),
	show_args_rest(Args),
	write(')').

%------------------------------------------------------------------------------
% show_args_rest(+Args):
%------------------------------------------------------------------------------

show_args_rest([]).

show_args_rest([Arg|Args]) :-
	write(', '),
	show_arg(Arg),
	show_args_rest(Args).

%------------------------------------------------------------------------------
% show_arg(+Arg):
%------------------------------------------------------------------------------

show_arg(Arg) :-
	number(Arg),
	!,
	write(Arg).

show_arg([]) :-
	write(''),
	!.

show_arg(Atom) :-
	atom(Atom),
	write(Atom),
	!.

show_arg([Char|Str]) :-
	write('\''),
	show_char(Char),
	show_str_rest(Str),
	write('\'').

%------------------------------------------------------------------------------
% show_str_rest(+Str):
%------------------------------------------------------------------------------

show_str_rest([]).

show_str_rest([Char|Str]) :-
	show_char(Char),
	show_str_rest(Str).

%------------------------------------------------------------------------------
% show_char(+Char):
%------------------------------------------------------------------------------

show_char('\n') :-
	!,
	write('\\'),
	write('n').

show_char('\'') :-
	!,
	write('\\\'').

show_char(Char) :-
	write(Char).

%==============================================================================
% Syntax Error Messages:
%==============================================================================

% In order not to complicate scanner and parser, we use a dynamic database
% fact for storing information about the current line:
%     err_info(FirstLineNo, LastLineNo, Chars).
% This is asserted for every line (input rule) that is read,
% before parser and scanner are called.
% If an error occurs, this information is used, and the fact is deleted
% from the dynamic database. In this way, additional error messages for
% the same rule are suppressed (an error message is only printed when the fact
% still exists in the dynamic database).
% Error handling is added to the predicates by means of an additional rule
% in the end which prints the error message and then fails.
% Only the topmost parser predicate does not fail, but produces an error fact
% error(RuleNo, LineNo), so that parsing can continue with the next rule.
% The existence of such error facts shows that there were errors, and the
% input program should not be executed.

%------------------------------------------------------------------------------
% parse(+Chars, +RuleNo, +FirstLineNo, +LastLineNo, -Facts):
%------------------------------------------------------------------------------

parse(Chars, RuleNo, FirstLineNo, LastLineNo, Facts) :-
	store_err_info(FirstLineNo, LastLineNo, Chars),
	tokenize(Chars, Tokens),
	parse_rule(Tokens, RuleNo, FirstLineNo, Facts),
	semantic_check_rule(Facts),
	!.

parse(_, RuleNo, FirstLineNo, _LastLineNo, [error(RuleNo, FirstLineNo)]) :-
	syntax_error(unhandled).

%------------------------------------------------------------------------------
% store_err_info(+FirstLineNo, +LastLineNo, +Chars):
%------------------------------------------------------------------------------

store_err_info(FirstLineNo, LastLineNo, Chars) :-
	retractall(err_info(_,_,_)),
	assert(err_info(FirstLineNo, LastLineNo, Chars)).

%------------------------------------------------------------------------------
% syntax_error(+ErrMsg):
%------------------------------------------------------------------------------

% If this is the first error in the rule, the err_info fact still exists,
% and the error message is printed:

syntax_error(ErrMsg) :-
	err_info(FirstLineNo, LastLineNo, Chars),
	!,
	retractall(err_info(_,_,_)),
	write('Syntax error '),
	print_line_no(FirstLineNo, LastLineNo),
	write(': '),
	print_errmsg_failsafe(ErrMsg),
	nl,
	print_chars(Chars),
	nl.

% Not the first error, simply ignore it:

syntax_error(_).

% print_line_no(+FirstLineNo, +LastLineNo):

print_line_no(LineNo, LineNo) :-
	!,
	write('in line '),
	write(LineNo).

print_line_no(FirstLineNo, LastLineNo) :-
	!,
	write('between line '),
	write(FirstLineNo),
	write(' and '),
	write(LastLineNo).

%------------------------------------------------------------------------------
% print_errmsg_failsafe(+ErrMsg):
%------------------------------------------------------------------------------

print_errmsg_failsafe(ErrMsg) :-
	print_errmsg(ErrMsg),
	!.

print_errmsg_failsafe(ErrMsg) :-
	nl,
	write('Sorry, no message for '),
	write(ErrMsg),
	write(' (please tell programmer).').


%------------------------------------------------------------------------------
% print_errmsg(+ErrMsg):
%------------------------------------------------------------------------------

print_errmsg(invalid_char(Char)) :-
	write('Invalid character \''),
	write(Char),
	write('\'.').

print_errmsg(string_not_closed) :-
	write('String not closed.').

print_errmsg(expect(ExpectedTokens, TokenList, Place)) :-
	nl,
	write('Expected '),
	print_expected(ExpectedTokens),
	write(' '),
	write(Place),
	write(', found '),
	print_found(TokenList),
	write('.').

print_errmsg(order_decl_after_use(Pred,Arity)) :-
	nl,
	write('Order declaration for '),
	write(Pred),
	write('/'),
	write(Arity),
	write(' must precede first use.').

print_errmsg(invalid_index_keyword(Keyword)) :-
	nl,
	write('Invalid index keyword: '),
	write(Keyword),
	write(' (must be rank, dense_rank, next, last).').

print_errmsg(unbound_var(Var)) :-
	write('Unbound Variable: '),
	write(Var),
	write('.').

print_errmsg(ospec_std_pred(Pred,Arity)) :-
	nl,
	write('Order specification used on non-ordered Predicate: '),
	write(Pred),
	write('/'),
	write(Arity),
	write('.').

print_errmsg(index_std_pred(Pred,Arity)) :-
	nl,
	write('Index used on non-ordered Predicate: '),
	write(Pred),
	write('/'),
	write(Arity),
	write('.').

print_errmsg(unhandled) :-
	write('Sorry, no specific message available.').

%------------------------------------------------------------------------------
% expect(+ExpectedTokens, +TokenList, +Place):
%------------------------------------------------------------------------------

expect(ExpectedTokens, [Token|_], _) :-
	member(Token, ExpectedTokens),
	!.

expect(ExpectedTokens, TokenList, Place) :-
	syntax_error(expect(ExpectedTokens, TokenList, Place)),
	fail.

%------------------------------------------------------------------------------
% print_expected(+Tokens):
%------------------------------------------------------------------------------

print_expected([Token]) :-
	print_token_type(Token).

print_expected([Token1, Token2]) :-
	print_token_type(Token1),
	write(', or '),
	print_token_type(Token2).

print_expected([Token1, Token2, Token3 | MoreTokens]) :-
	print_token_type(Token1),
	write(', '),
	print_expected([Token2, Token3 | MoreTokens]).

%------------------------------------------------------------------------------
% print_found(+Tokens):
%------------------------------------------------------------------------------

print_found([Token|_]) :-
	print_token(Token).

print_found([]) :-
	write('end of rule').

%------------------------------------------------------------------------------
% check_index_keyword(+Keyword):
%------------------------------------------------------------------------------

check_index_keyword(Keyword) :-
	member(Keyword, [rank, dense_rank, last, next]),
	!.

check_index_keyword(Keyword) :-
	syntax_error(invalid_index_keyword(Keyword)),
	fail.

%==============================================================================
% Lexical Scanner:
%==============================================================================

%------------------------------------------------------------------------------
%tokenize(+CharList, -TokenList).
%------------------------------------------------------------------------------

tokenize([Char|Chars], Tokens) :-
	is_space(Char),
	!,
	tokenize(Chars, Tokens).

tokenize([Char|Chars], Tokens) :-
	is_comment(Char),
	!,
	skip_to_newline(Chars, Rest),
	tokenize(Rest, Tokens).

tokenize([Char|Chars], [atom(Atom)|Tokens]) :-
	is_lower(Char),
	!,
	tokenize_word(Char, Chars, RestChars, AtomChars),
	atom_chars(Atom, AtomChars),
	tokenize(RestChars, Tokens).

tokenize([Char|Chars], [var(Atom)|Tokens]) :-
	is_upper(Char),
	!,
	tokenize_word(Char, Chars, RestChars, AtomChars),
	atom_chars(Atom, AtomChars),
	tokenize(RestChars, Tokens).

tokenize([Char|Chars], [int(Int)|Tokens]) :-
	is_digit(Char),
	!,
	tokenize_int(Char, Chars, RestChars, Digits),
	make_int(Digits, Int),
	tokenize(RestChars, Tokens).

tokenize([Char|Chars], [str(Str)|Tokens]) :-
	is_quote(Char),
	!,
	tokenize_str(Char, Chars, RestChars, Str),
	tokenize(RestChars, Tokens).

tokenize(['('|Chars], [lparen|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize([')'|Chars], [rparen|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize([','|Chars], [comma|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['.'|Chars], [fullstop|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['<', '-' |Chars], [if|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['<', '=' |Chars], [le|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['<' |Chars], [lt|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['>', '=' |Chars], [ge|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['>' |Chars], [gt|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['!', '=' |Chars], [ne|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['=' |Chars], [eq|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['/' |Chars], [slash|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['^' |Chars], [desc|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['@' |Chars], [ruleno|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['|' |Chars], [vert|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['[' |Chars], [lbrack|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize([']' |Chars], [rbrack|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize([':', '-' |Chars], [prolog_if|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize([':' |Chars], [colon|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['\\', '+' |Chars], [not|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize([InvalidChar |_], []) :-
	syntax_error(invalid_char(InvalidChar)),
	fail.

tokenize([], []).

%------------------------------------------------------------------------------
% tokenize_word(+CurrentChar, +MoreChars, -RemainingChars, -AtomChars).
%------------------------------------------------------------------------------

tokenize_word(Char, [NextChar|Chars], RestChars, [Char|AtomChars]) :-
	is_alnum(Char),
	!,
	tokenize_word(NextChar, Chars, RestChars, AtomChars).

tokenize_word(Char, Chars, [Char|Chars], []).

%------------------------------------------------------------------------------
% tokenize_int(Char, Chars, RestChars, Digits):
%------------------------------------------------------------------------------

tokenize_int(Digit, [NextChar|Chars], RestChars, [Digit|MoreDigits]) :-
	is_digit(Digit),
	!,
	tokenize_int(NextChar, Chars, RestChars, MoreDigits).

tokenize_int(Char, Chars, [Char|Chars], []).

%------------------------------------------------------------------------------
% make_int(+Digits, -Int):
%------------------------------------------------------------------------------

make_int(Digits, Int) :-
	make_int(Digits, 0, Int).

% make_int(+Digits, +IntIn, -IntOut):

make_int([], Int, Int).

make_int([Digit|RestDigits], IntIn, IntOut) :-
	digit_val(Digit, DigitVal),
	Int is IntIn * 10 + DigitVal,
	make_int(RestDigits, Int, IntOut).

%------------------------------------------------------------------------------
% tokenize_str(+Quote, +Chars, -RestChars, -Str)
%------------------------------------------------------------------------------

tokenize_str(Quote, ['\\','n'|Chars], RestChars, ['\n'|Str]) :-
	!,
	tokenize_str(Quote, Chars, RestChars, Str).

tokenize_str(Quote, [Char|Chars], RestChars, [Char|Str]) :-
	Char \= Quote,
	!,
	tokenize_str(Quote, Chars, RestChars, Str).

tokenize_str(Quote, [Quote|Chars], Chars, []) :-
	!.

tokenize_str(_, [], [], []) :-
	syntax_error(string_not_closed),
	fail.

%------------------------------------------------------------------------------
% skip_to_newline(+Chars, -Rest):
%------------------------------------------------------------------------------

skip_to_newline(['\n'|Rest], Rest) :-
	!.

skip_to_newline([], []).

skip_to_newline([Char|Chars], Rest) :-
	Char \== '\n',
	skip_to_newline(Chars, Rest).

%------------------------------------------------------------------------------
% digit_val(Digit, Int).
%------------------------------------------------------------------------------

digit_val('0', 0).
digit_val('1', 1).
digit_val('2', 2).
digit_val('3', 3).
digit_val('4', 4).
digit_val('5', 5).
digit_val('6', 6).
digit_val('7', 7).
digit_val('8', 8).
digit_val('9', 9).

%------------------------------------------------------------------------------
% is_space(Char).
%------------------------------------------------------------------------------

is_space(' ').
is_space('\t').
is_space('\n').
is_space('\r').

%------------------------------------------------------------------------------
% is_lower(Char).
%------------------------------------------------------------------------------

is_lower('a').
is_lower('b').
is_lower('c').
is_lower('d').
is_lower('e').
is_lower('f').
is_lower('g').
is_lower('h').
is_lower('i').
is_lower('j').
is_lower('k').
is_lower('l').
is_lower('m').
is_lower('n').
is_lower('o').
is_lower('p').
is_lower('q').
is_lower('r').
is_lower('s').
is_lower('t').
is_lower('u').
is_lower('v').
is_lower('w').
is_lower('x').
is_lower('y').
is_lower('z').

%------------------------------------------------------------------------------
% is_upper(Char).
%------------------------------------------------------------------------------

is_upper('A').
is_upper('B').
is_upper('C').
is_upper('D').
is_upper('E').
is_upper('F').
is_upper('G').
is_upper('H').
is_upper('I').
is_upper('J').
is_upper('K').
is_upper('L').
is_upper('M').
is_upper('N').
is_upper('O').
is_upper('P').
is_upper('Q').
is_upper('R').
is_upper('S').
is_upper('T').
is_upper('U').
is_upper('V').
is_upper('W').
is_upper('X').
is_upper('Y').
is_upper('Z').

%------------------------------------------------------------------------------
% is_digit(Char).
%------------------------------------------------------------------------------

is_digit('0').
is_digit('1').
is_digit('2').
is_digit('3').
is_digit('4').
is_digit('5').
is_digit('6').
is_digit('7').
is_digit('8').
is_digit('9').

%------------------------------------------------------------------------------
% is_alnum(Char).
%------------------------------------------------------------------------------

is_alnum(Char) :-
	is_lower(Char).

is_alnum(Char) :-
	is_upper(Char).

is_alnum(Char) :-
	is_digit(Char).

is_alnum('_').

%------------------------------------------------------------------------------
% is_comment(Char)
%------------------------------------------------------------------------------

is_comment('\%').

%------------------------------------------------------------------------------
% 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(lparen) :-
	write('(').

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

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

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

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

print_token_type(prolog_if) :-
	write(':-').

print_token_type(eq) :-
	write('=').

print_token_type(ne) :-
	write('!=').

print_token_type(lt) :-
	write('<').

print_token_type(le) :-
	write('<=').

print_token_type(gt) :-
	write('>').

print_token_type(ge) :-
	write('>=').

print_token_type(slash) :-
	write('/').

print_token_type(desc) :-
	write('^').

print_token_type(ruleno) :-
	write('@').

print_token_type(vert) :-
	write('|').

print_token_type(lbrack) :-
	write('[').

print_token_type(rbrack) :-
	write(']').

print_token_type(colon) :-
	write('\':\'').

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

%------------------------------------------------------------------------------
% 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(lparen) :-
	write('(').

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

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

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

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

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

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

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

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

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

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

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

print_token(slash) :-
	write('/').

print_token(desc) :-
	write('^').

print_token(ruleno) :-
	write('@').

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

print_token(lbrack) :-
	write('[').

print_token(rbrack) :-
	write(']').

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

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

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

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

%==============================================================================
% Parser for Source Program:
%==============================================================================

% Handling of syntax errors:
% -------------------------
%    At the start of each predicate, the next token is compared with the list
%    of possible tokens at this place (expected tokens).
%    If it is not in the list, a syntax error is written for the first such
%    error in a rule. Later messages are suppressed (see syntax_error above).
%    The is a predicate parse_N for each non-terminal N.
%    This predicate checks the token, and then calls xparse_N,
%    which does the real parsing, and often contains several rules that differ
%    in the first token.
%    Because of this treatment of syntax errors, backtracking cannot be used:
%    if one calls parse_N, one must be sure that N has to come.
%    (Actually, backtracking is ok, if after N different cases are treated.)
%    In seldom cases a specific token is expected in the middle of a rule body.
%    Then the check of the expected token is done first, to generate the
%    standard error message, in case the following unification should fail.

%------------------------------------------------------------------------------
% parse_rule(+Tokens, +RuleNo, -Facts)
%------------------------------------------------------------------------------

parse_rule(Tokens, RuleNo, LineNo, Facts) :-
	expect([atom(_),var(_),str(_),int(_)], Tokens, 'at start of rule'),
	xparse_rule(Tokens, RuleNo, LineNo, Facts).

% xparse_rule(+Tokens, +RuleNo, -Facts)

xparse_rule([atom(ordered), atom(Pred)|Tokens], _RuleNo, _LineNo,
		[ordered_pred(Pred, Arity)]) :-
	!,
	expect([slash], Tokens, 'after predicate in order declaration'),
	Tokens = [slash|Tokens1],
	expect([int(Arity)], Tokens1,
		'as predicate arity in order declaration'),
	Tokens1 = [int(Arity)|Tokens2],
	expect([fullstop], Tokens2, 'after order declaration'),
	Tokens2 = [fullstop],
	check_not_used(Pred,Arity).

xparse_rule(Tokens, RuleNo, LineNo, [fact(RuleNo,LineNo)|Facts]) :-
	parse_head_lit(Tokens, RuleNo, 0, Facts, Tokens1),
	expect([if,fullstop], Tokens1, 'after head literal'),
	Tokens1 = [fullstop],
	!.

xparse_rule(Tokens, RuleNo, LineNo, [rule(RuleNo,LineNo,NumBodyLit)|Facts]) :-
	parse_head_lit(Tokens, RuleNo, 0, HeadFacts, Tokens1),
	expect([if], Tokens1, 'after head literal'),
	Tokens1 = [if|BodyTokens],
	parse_body(BodyTokens, RuleNo, 1, BodyFacts, NumBodyLit, Tokens2),
	expect([fullstop], Tokens2, 'after body'),
	Tokens2 = [fullstop],
	append(HeadFacts, BodyFacts, Facts).

%------------------------------------------------------------------------------
% parse_body(+Tokens, +RuleNo, +LitNo, -Facts, -NumBodyLit, -RestTokens)
%------------------------------------------------------------------------------

parse_body(Tokens, RuleNo, LitNo, Facts, NumBodyLit, RestTokens) :-
	expect([not,atom(_),str(_),int(_),var(_)], Tokens, 'at start of body'),
	xparse_body(Tokens, RuleNo, LitNo, Facts, NumBodyLit, RestTokens).

% xparse_body(+Tokens, +RuleNo, +LitNo, -Facts, -NumBodyLit, -RestTokens):

xparse_body(Tokens, RuleNo, LitNo, Facts, NumBodyLit, RestTokens) :-
	parse_body_lit(Tokens, RuleNo, LitNo, LitFacts, Tokens1),
	parse_body_rest(Tokens1, RuleNo, LitNo, RestFacts, NumBodyLit,
						RestTokens),
	append(LitFacts, RestFacts, Facts).

%------------------------------------------------------------------------------
% parse_body_rest(+Tokens, +RuleNo, +LitNo, -Facts, -NumBodyLit, -RestTokens):
%------------------------------------------------------------------------------

% (begins with comma or fullstop).
parse_body_rest(Tokens, RuleNo, LitNo, Facts, NumBodyLit, RestTokens) :-
	expect([comma,fullstop], Tokens, 'after body literal'),
	xparse_body_rest(Tokens, RuleNo, LitNo, Facts, NumBodyLit, RestTokens).

% xparse_body_rest(+Tokens, +RuleNo, +LitNo, -Facts, -NumBodyLit, -RestTokens)

xparse_body_rest([comma|Tokens], RuleNo, LitNo, Facts, NumBodyLit, RestTokens)
	:-
	!,
	NextLitNo is LitNo + 1,
	parse_body(Tokens, RuleNo, NextLitNo, Facts, NumBodyLit, RestTokens).

xparse_body_rest([fullstop|Tokens], _RuleNo, LitNo, [], LitNo,
			[fullstop|Tokens]).

%------------------------------------------------------------------------------
% parse_head_lit(+Tokens, +RuleNo, +LitNo, -Facts, -RestTokens)
%------------------------------------------------------------------------------

% (from predicate to rparen)

parse_head_lit(Tokens, RuleNo, LitNo, Facts, RestTokens) :-
	expect([atom(_)], Tokens, 'at start of head literal'),
	xparse_head_lit(Tokens, RuleNo, LitNo, Facts, RestTokens).

% xparse_head_lit(+Tokens, +RuleNo, +LitNo, -Facts, -RestTokens)
xparse_head_lit([atom(Pred)|Tokens], RuleNo, LitNo,
		[lit(RuleNo,LitNo,Pred,NumArgs)|Facts], RestTokens) :-
	parse_opt_po_spec(Tokens, RuleNo, LitNo, OrderFacts, Tokens1),
	parse_opt_args(Tokens1, RuleNo, LitNo, ArgFacts, NumArgs, RestTokens),
	append(OrderFacts, ArgFacts, Facts).

%------------------------------------------------------------------------------
% parse_body_lit(+Tokens, +RuleNo, +LitNo, -Facts, -RestTokens)
%------------------------------------------------------------------------------

% from optional negation to rparen

parse_body_lit(Tokens, RuleNo, LitNo, Facts, RestTokens) :-
	expect([not,atom(_),int(_),str(_),var(_)], Tokens,
		'at start of literal'),
	xparse_body_lit(Tokens, RuleNo, LitNo, Facts, RestTokens).

% xparse_body_lit(+Tokens, +RuleNo, +LitNo, -Facts, -RestTokens)
xparse_body_lit([not|Tokens], RuleNo, LitNo,
		[negated(RuleNo,LitNo)|Facts], RestTokens) :-
	parse_pos_body_lit(Tokens, RuleNo, LitNo, Facts, RestTokens).

xparse_body_lit([Other|Tokens], RuleNo, LitNo, Facts, RestTokens) :-
	Other \= not,
	parse_pos_body_lit([Other|Tokens], RuleNo, LitNo, Facts, RestTokens).

%------------------------------------------------------------------------------
% parse_pos_body_lit(+Tokens, +RuleNo, +LitNo, -Facts, -RestTokens)
%------------------------------------------------------------------------------

% (from predicate to rparen)

parse_pos_body_lit(Tokens, RuleNo, LitNo, Facts, RestTokens) :-
	expect([atom(_),int(_),str(_),var(_)], Tokens, 'at start of literal'),
	xparse_pos_body_lit(Tokens, RuleNo, LitNo, Facts, RestTokens).

% xparse_pos_body_lit(+Tokens, +RuleNo, +LitNo, -Facts, -RestTokens)
xparse_pos_body_lit([atom(Pred)|Tokens], RuleNo, LitNo,
		[lit(RuleNo,LitNo,Pred,NumArgs)|ArgFacts], RestTokens) :-
	expect([lparen,lbrack,comma,fullstop,eq,ne,lt,le,gt,ge], Tokens,
		'after predicate or comparison term'),
	Tokens=[NextTok|_],
	member(NextTok, [lparen,comma,fullstop]),
	!,
	parse_opt_args(Tokens, RuleNo, LitNo, ArgFacts, NumArgs, RestTokens).

xparse_pos_body_lit([atom(Pred)|Tokens], RuleNo, LitNo,
		[lit(RuleNo,LitNo,Pred,NumArgs)|ArgFacts], RestTokens) :-
	Tokens=[lbrack|_],
	!,
	parse_index(Tokens, RuleNo, LitNo, IndexFacts, Tokens1),
	parse_opt_args(Tokens1, RuleNo, LitNo, ArgFacts1, NumArgs, RestTokens),
	append(IndexFacts, ArgFacts1, ArgFacts).

xparse_pos_body_lit(Tokens, RuleNo, LitNo,
		[complit(RuleNo,LitNo,Op), ArgFact1, ArgFact2], RestTokens) :-
	parse_arg(Tokens, RuleNo, LitNo, 1, ArgFact1, Tokens1),
	expect([eq,ne,lt,le,gt,ge], Tokens1, 'after term at start of literal'),
	Tokens1 = [Op|Tokens2],
	comparison_op(Op),
	parse_arg(Tokens2, RuleNo, LitNo, 2, ArgFact2, RestTokens).

%------------------------------------------------------------------------------
% parse_opt_args(+Tokens, +RuleNo, +LitNo, -Facts, -NumArgs, -RestTokens)
%------------------------------------------------------------------------------

% (from lparen to rparen) or nothing.

parse_opt_args(Tokens, RuleNo, LitNo, ArgFacts, NumArgs, RestTokens) :-
	expect([lparen,if,comma,fullstop], Tokens, 'at argument list'),
	xparse_opt_args(Tokens, RuleNo, LitNo, ArgFacts, NumArgs, RestTokens).

xparse_opt_args([lparen|Tokens], RuleNo, LitNo, ArgFacts, NumArgs,
		RestTokens) :-
	!,
	parse_args([lparen|Tokens], RuleNo, LitNo, ArgFacts, NumArgs,
		RestTokens).

xparse_opt_args(Tokens, _RuleNo, _LitNo, [], 0, Tokens).

%------------------------------------------------------------------------------
% parse_args(+Tokens, +RuleNo, +LitNo, -Facts, -NumArgs, -RestTokens)
%------------------------------------------------------------------------------

% (from lparen to rparen)

parse_args(Tokens, RuleNo, LitNo, ArgFacts, NumArgs, RestTokens) :-
	expect([lparen], Tokens, 'at start of argument list'),
	xparse_args(Tokens, RuleNo, LitNo, ArgFacts, NumArgs, RestTokens).

xparse_args([lparen|Tokens], RuleNo, LitNo, ArgFacts, NumArgs, RestTokens) :-
	parse_arg_list(Tokens, RuleNo, LitNo, 1, ArgFacts, NumArgs, Tokens1),
	Tokens1 = [rparen|RestTokens].

%------------------------------------------------------------------------------
% parse_arg_list(+Tokens, +RuleNo, +LitNo, +ArgNo, -Facts, -NumArgs, -RestTok):
%------------------------------------------------------------------------------

% (starts with term)

parse_arg_list(Tokens, RuleNo, LitNo, ArgNo, Facts, NumArgs, RestTokens) :-
	expect([var(_),atom(_),int(_),str(_)], Tokens, 'as argument'),
	xparse_arg_list(Tokens, RuleNo, LitNo, ArgNo, Facts, NumArgs,
			RestTokens).

xparse_arg_list(Tokens, RuleNo, LitNo, ArgNo,
		[Fact|MoreFacts], NumArgs, RestTokens) :-
	parse_arg(Tokens, RuleNo, LitNo, ArgNo, Fact, Tokens1),
	parse_arg_rest(Tokens1, RuleNo, LitNo, ArgNo, MoreFacts, NumArgs,
		RestTokens).

%------------------------------------------------------------------------------
% parse_arg_rest(+Tokens, +RuleNo, +LitNo, -Facts, -NumArgs, -RestTokens).
%------------------------------------------------------------------------------

% (starts with comma or rparen)

parse_arg_rest(Tokens, RuleNo, LitNo, ArgNo, ArgFacts, NumArgs, RestTokens) :-
	expect([comma, rparen], Tokens, 'after argument term'),
	xparse_arg_rest(Tokens, RuleNo, LitNo, ArgNo, ArgFacts, NumArgs,
		RestTokens).

xparse_arg_rest([comma|Tokens], RuleNo, LitNo, ArgNo, ArgFacts, NumArgs,
		RestTokens) :-
	NextArgNo is ArgNo + 1,
	parse_arg_list(Tokens, RuleNo, LitNo, NextArgNo, ArgFacts, NumArgs,
			RestTokens).

xparse_arg_rest([rparen|Tokens], _RuleNo, _LitNo, ArgNo, [], ArgNo,
		[rparen|Tokens]).

%------------------------------------------------------------------------------
% parse_arg(+Tokens, +RuleNo, +LitNo, +ArgNo, -Fact, -RestTokens):
%------------------------------------------------------------------------------

parse_arg(Tokens, RuleNo, LitNo, ArgNo, Fact, RestTokens) :-
	expect([var(_),atom(_),int(_),str(_)], Tokens, 'as argument'),
	xparse_arg(Tokens, RuleNo, LitNo, ArgNo, Fact, RestTokens).

% xparse_arg(+Tokens, +RuleNo, +LitNo, +ArgNo, -Fact, -RestTokens):

xparse_arg([atom(Const)|Tokens], RuleNo, LitNo, ArgNo,
		arg(RuleNo,LitNo,ArgNo,const,Const), Tokens).

xparse_arg([int(Int)|Tokens], RuleNo, LitNo, ArgNo,
		arg(RuleNo,LitNo,ArgNo,int,Int), Tokens).

xparse_arg([str(Str)|Tokens], RuleNo, LitNo, ArgNo,
		arg(RuleNo,LitNo,ArgNo,str,Str), Tokens).

xparse_arg([var(Var)|Tokens], RuleNo, LitNo, ArgNo,
		arg(RuleNo,LitNo,ArgNo,var,Var), Tokens).


%------------------------------------------------------------------------------
% parse_opt_po_spec(+Tokens, +RuleNo, +LitNo, -OrderFacts, -RestTokens)
%------------------------------------------------------------------------------

% partitioning and order specification, i.e. from < to > in head literal

parse_opt_po_spec(Tokens, RuleNo, LitNo, OrderFacts, RestTokens) :-
	expect([lt,lparen,if,fullstop], Tokens,
		'after predicate in head literal'),
	xparse_opt_po_spec(Tokens, RuleNo, LitNo, OrderFacts, RestTokens).

xparse_opt_po_spec([lt|Tokens], RuleNo, LitNo, OrderFacts,RestTokens) :-
	!,
	parse_po_list(Tokens, RuleNo, LitNo, 1, OrderFacts, RestTokens).

xparse_opt_po_spec(Tokens, _RuleNo, _LitNo, [], Tokens).

%------------------------------------------------------------------------------
% parse_po_list(+Tokens, +RuleNo, +LitNo, +Pos, -OrderFacts, -RestTokens)
%------------------------------------------------------------------------------

% partitioning and ordering argument list, i.e. between < and > in head.

% The difficulty is that we do not know yet whether | is used.
% If only vars, integers, or strings are used, | is still possible.
% If ^ or @ are used, we are certainly in the order part, | cannot be used.

parse_po_list(Tokens, RuleNo, LitNo, Pos, OrderFacts, RestTokens) :-
	expect([var(_),int(_),str(_),desc,ruleno], Tokens,
		'inside partioning/order specification'),
	xparse_po_list(Tokens, RuleNo, LitNo, Pos, OrderFacts, RestTokens).

xparse_po_list([var(V)|Tokens], RuleNo, LitNo, Pos, [OrderFact|OrderFacts],
		RestTokens) :-
	parse_order_arg([var(V)|Tokens], RuleNo, LitNo, Pos, OrderFact, Tokens1),
	NextPos is Pos + 1,
	parse_po_rest(Tokens1, RuleNo, LitNo, NextPos, OrderFacts,
				RestTokens).

xparse_po_list([int(I)|Tokens], RuleNo, LitNo, Pos, [OrderFact|OrderFacts],
		RestTokens) :-
	parse_order_arg([int(I)|Tokens], RuleNo, LitNo, Pos, OrderFact, Tokens1),
	NextPos is Pos + 1,
	parse_po_rest(Tokens1, RuleNo, LitNo, NextPos, OrderFacts,
				RestTokens).

xparse_po_list([str(S)|Tokens], RuleNo, LitNo, Pos, [OrderFact|OrderFacts],
		RestTokens) :-
	parse_order_arg([str(S)|Tokens], RuleNo, LitNo, Pos, OrderFact, Tokens1),
	NextPos is Pos + 1,
	parse_po_rest(Tokens1, RuleNo, LitNo, NextPos, OrderFacts,
				RestTokens).

xparse_po_list([Other|Tokens], RuleNo, LitNo, Pos, [OrderFact|OrderFacts],
		RestTokens) :-
	parse_order_arg([Other|Tokens], RuleNo, LitNo, Pos, OrderFact, Tokens1),
	NextPos is Pos + 1,
	Other \= var(_),
	Other \= int(_),
	Other \= str(_),
	parse_order_rest(Tokens1, RuleNo, LitNo, NextPos, OrderFacts,
				RestTokens).

%------------------------------------------------------------------------------
% parse_po_rest(+Tokens, +RuleNo, +LitNo, +Pos, -OrderFacts, -RestTokens)
%------------------------------------------------------------------------------

% Rest of partitioning and ordering arguments inside < and > in head literal
% Rest means after a partitioning/ordering argument,
% i.e. this starts with , or | or >
% At this point, it is still possible that | is used.
% When this is no longer possible, parse_order_rest is used instead.

parse_po_rest(Tokens, RuleNo, LitNo, Pos, OrderFacts, RestTokens) :-
	expect([comma,vert,gt], Tokens, 'after partitioning/order element'),
	xparse_po_rest(Tokens, RuleNo, LitNo, Pos, OrderFacts,
		RestTokens).

xparse_po_rest([comma|Tokens], RuleNo, LitNo, Pos, OrderFacts, RestTokens) :-
	parse_po_list(Tokens, RuleNo, LitNo, Pos, OrderFacts, RestTokens).

xparse_po_rest([vert|Tokens], RuleNo, LitNo, Pos,
		[partition(RuleNo,LitNo,PrevPos)|OrderFacts], RestTokens) :-
	PrevPos is Pos-1,
	parse_order_list(Tokens, RuleNo, LitNo, Pos, OrderFacts, RestTokens).

xparse_po_rest([gt|Tokens], RuleNo, LitNo, Pos,
		[order_spec(RuleNo, LitNo, LastPos)], Tokens) :-
	LastPos is Pos - 1.

%------------------------------------------------------------------------------
% parse_order_list(+Tokens, +RuleNo, +LitNo, +Pos, -OrderFacts, -RestTokens)
%------------------------------------------------------------------------------

% This is a suffix of the list of ordering arguments inside < > in the head.
% At this point it is clear that | can no longer be used,
% because either it was used already, or ^ or @ were used,
% which are permissible only in the ordering part.

parse_order_list(Tokens, RuleNo, LitNo, Pos, OrderFacts, RestTokens) :-
	expect([var(_),int(_),str(_),desc,ruleno], Tokens,
		'inside order specification'),
	xparse_order_list(Tokens, RuleNo, LitNo, Pos, OrderFacts, RestTokens).

xparse_order_list(Tokens, RuleNo, LitNo, Pos, [OrderFact|OrderFacts],
		RestTokens) :-
	parse_order_arg(Tokens, RuleNo, LitNo, Pos, OrderFact, Tokens1),
	NextPos is Pos + 1,
	parse_order_rest(Tokens1, RuleNo, LitNo, NextPos, OrderFacts,
				RestTokens).

%------------------------------------------------------------------------------
% parse_order_rest(+Tokens, +RuleNo, +LitNo, +Pos, -OrderFacts,-RestTokens)
%------------------------------------------------------------------------------

parse_order_rest(Tokens, RuleNo, LitNo, Pos, OrderFacts, RestTokens) :-
	expect([comma,gt], Tokens, 'after order element'),
	xparse_order_rest(Tokens, RuleNo, LitNo, Pos, OrderFacts,
		RestTokens).

xparse_order_rest([comma|Tokens], RuleNo, LitNo, Pos, OrderFacts,
		RestTokens) :-
	parse_order_list(Tokens, RuleNo, LitNo, Pos, OrderFacts, RestTokens).

xparse_order_rest([gt|Tokens], RuleNo, LitNo, Pos,
		[order_spec(RuleNo, LitNo, LastPos)], Tokens) :-
	LastPos is Pos - 1.

%------------------------------------------------------------------------------
% parse_order_arg(+Tokens, +RuleNo, +LitNo, +Pos, -OrderFact, -RestTokens)
%------------------------------------------------------------------------------

% This is a single element of the partitioning and order specification
% between < and > in the rule head.
% The predicate is called parse_order_arg and not parse_po_arg,
% because the ordering arguments are more general than the partitioning
% arguments.

parse_order_arg(Tokens, RuleNo, LitNo, Pos, OrderFact, RestTokens) :-
	expect([var(_),int(_),str(_),desc,ruleno], Tokens, 'at order element'),
	xparse_order_arg(Tokens, RuleNo, LitNo, Pos, OrderFact, RestTokens).

xparse_order_arg([var(Var)|RestTokens], RuleNo, LitNo, Pos,
		order(RuleNo,LitNo,Pos,asc_var,Var), RestTokens).

xparse_order_arg([int(Int)|RestTokens], RuleNo, LitNo, Pos,
		order(RuleNo,LitNo,Pos,asc_int,Int), RestTokens).

xparse_order_arg([str(Str)|RestTokens], RuleNo, LitNo, Pos,
		order(RuleNo,LitNo,Pos,asc_str,Str), RestTokens).

xparse_order_arg([ruleno|RestTokens], RuleNo, LitNo, Pos,
		order(RuleNo,LitNo,Pos,asc_rno,RuleNo), RestTokens).

xparse_order_arg([desc|Tokens1], RuleNo, LitNo, Pos,
		OrderFact, RestTokens) :-
		parse_order_arg_desc(Tokens1, RuleNo, LitNo, Pos, OrderFact,
					RestTokens).

%------------------------------------------------------------------------------
% parse_order_arg_desc(+Tokens, +RuleNo, +LitNo, +Pos, -OrderFact, -RestTokens)
%------------------------------------------------------------------------------

parse_order_arg_desc(Tokens, RuleNo, LitNo, Pos, OrderFact, RestTokens) :-
	expect([var(_),int(_),str(_)], Tokens, 'after ^'),
	xparse_order_arg_desc(Tokens, RuleNo, LitNo, Pos, OrderFact,
				RestTokens).

xparse_order_arg_desc([var(Var)|RestTokens], RuleNo, LitNo, Pos,
		order(RuleNo,LitNo,Pos,desc_var,Var), RestTokens).

xparse_order_arg_desc([int(Int)|RestTokens], RuleNo, LitNo, Pos,
		order(RuleNo,LitNo,Pos,desc_int,Int), RestTokens).

xparse_order_arg_desc([str(Str)|RestTokens], RuleNo, LitNo, Pos,
		order(RuleNo,LitNo,Pos,desc_str,Str), RestTokens).

%------------------------------------------------------------------------------
% parse_index(+Tokens, +RuleNo, +LitNo, -IndexFacts, -RestTokens):
%------------------------------------------------------------------------------

% Index after predicate name in body literal, from [ to ].

parse_index(Tokens, RuleNo, LitNo, IndexFacts, RestTokens) :-
	expect([lbrack], Tokens, 'after predicate name'),
	xparse_index(Tokens, RuleNo, LitNo, IndexFacts, RestTokens).

xparse_index([lbrack|Tokens], RuleNo, LitNo, IndexFacts, RestTokens) :-
	parse_index_start(Tokens, RuleNo, LitNo, IndexFacts, RestTokens).

%------------------------------------------------------------------------------
% parse_index_start(+Tokens, +RuleNo, +LitNo, -IndexFacts, -RestTokens):
%------------------------------------------------------------------------------

% After [, permits variable or integer without keyword prefix (row_number):

parse_index_start(Tokens, RuleNo, LitNo, IndexFacts, RestTokens) :-
	expect([var(_),int(_),atom(_)], Tokens, 'after ['),
	xparse_index_start(Tokens, RuleNo, LitNo, IndexFacts, RestTokens).

xparse_index_start([var(V)|Tokens], RuleNo, LitNo,
		[row_number(RuleNo,LitNo,var,V)|IndexFacts], RestTokens) :-
	!,
	parse_index_rest(Tokens, RuleNo, LitNo, IndexFacts, RestTokens).

xparse_index_start([int(I)|Tokens], RuleNo, LitNo,
		[row_number(RuleNo,LitNo,int,I)|IndexFacts], RestTokens) :-
	!,
	parse_index_rest(Tokens, RuleNo, LitNo, IndexFacts, RestTokens).

xparse_index_start([atom(Keyword)|Tokens], RuleNo, LitNo,
		IndexFacts, RestTokens) :-
	!,
	parse_index_list([atom(Keyword)|Tokens], RuleNo, LitNo,
		IndexFacts, RestTokens).

%------------------------------------------------------------------------------
% parse_index_rest(+Tokens, +RuleNo, +LitNo, -IndexFacts, -RestTokens):
%------------------------------------------------------------------------------

% Inside [  ] in body literal, starts with ',' or ']'

parse_index_rest(Tokens, RuleNo, LitNo, IndexFacts, RestTokens) :-
	expect([comma,rbrack], Tokens, 'after index in []'),
	xparse_index_rest(Tokens, RuleNo, LitNo, IndexFacts, RestTokens).

xparse_index_rest([rbrack|Tokens], _, _, [], Tokens) :-
	!.

xparse_index_rest([comma|Tokens], RuleNo, LitNo, IndexFacts, RestTokens) :-
	parse_index_list(Tokens, RuleNo, LitNo, IndexFacts, RestTokens).

%------------------------------------------------------------------------------
% parse_index_list(+Tokens, +RuleNo, +LitNo, -IndexFacts, -RestTokens):
%------------------------------------------------------------------------------

% Inside [  ] in body literal, only keywords (rank, dense_rank, next, last):

parse_index_list(Tokens, RuleNo, LitNo, IndexFacts, RestTokens) :-
	expect([atom(_)], Tokens, 'at keyword in []'),
	Tokens=[atom(Keyword)|_],
	check_index_keyword(Keyword),
	xparse_index_list(Tokens, RuleNo, LitNo, IndexFacts, RestTokens).

xparse_index_list([atom(rank)|Tokens], RuleNo, LitNo,
		[rank(RuleNo,LitNo,ArgType,Arg)|IndexFacts],
		RestTokens) :-
	!,
	parse_index_colon_arg(Tokens, ArgType, Arg, Tokens1),
	parse_index_rest(Tokens1, RuleNo, LitNo, IndexFacts, RestTokens).

xparse_index_list([atom(dense_rank)|Tokens], RuleNo, LitNo,
		[dense_rank(RuleNo,LitNo,ArgType,Arg)|IndexFacts],
		RestTokens) :-
	!,
	parse_index_colon_arg(Tokens, ArgType, Arg, Tokens1),
	parse_index_rest(Tokens1, RuleNo, LitNo, IndexFacts, RestTokens).

xparse_index_list([atom(next)|Tokens], RuleNo, LitNo,
		[next(RuleNo,LitNo,ArgType,Arg)|IndexFacts],
		RestTokens) :-
	!,
	parse_index_colon_arg(Tokens, ArgType, Arg, Tokens1),
	parse_index_rest(Tokens1, RuleNo, LitNo, IndexFacts, RestTokens).

xparse_index_list([atom(last)|Tokens], RuleNo, LitNo,
		[last(RuleNo,LitNo)|IndexFacts],
		RestTokens) :-
	!,
	parse_index_rest(Tokens, RuleNo, LitNo, IndexFacts, RestTokens).

%------------------------------------------------------------------------------
% parse_index_colon_arg(+Tokens, -ArgType, -Arg, -RestTokens):
%------------------------------------------------------------------------------

% Inside [  ] in body literal, after keyword (rank, dense_rank, next, last):

parse_index_colon_arg(Tokens, ArgType, Arg, RestTokens) :-
	expect([colon], Tokens, 'after rank/dense_rank/next'),
	xparse_index_colon_arg(Tokens, ArgType, Arg, RestTokens).

xparse_index_colon_arg([colon|Tokens], ArgType, Arg, RestTokens) :-
	!,
	parse_index_arg(Tokens, ArgType, Arg, RestTokens).

%------------------------------------------------------------------------------
% parse_index_arg(+Tokens, -ArgType, -Arg, -RestTokens):
%------------------------------------------------------------------------------

% Inside [  ] in body literal, after keyword (e.g. rank) and colon:

parse_index_arg(Tokens, ArgType, Arg, RestTokens) :-
	expect([var(_),int(_)], Tokens, 'after rank/dense_rank/next:'),
	xparse_index_arg(Tokens, ArgType, Arg, RestTokens).

xparse_index_arg([var(V)|Tokens], var, V, Tokens) :-
	!.

xparse_index_arg([int(I)|Tokens], int, I, Tokens) :-
	!.

%==============================================================================
% Semantic Checks and Application of Defaults:
%==============================================================================

%------------------------------------------------------------------------------
% check_not_used(+Pred, +Arity):
%------------------------------------------------------------------------------

% This is called in the parser when an order declaration is processed.
% Maybe it would be more consistent to do it in semantic_check_rule.
% It is no rule, though.

check_not_used(Pred, Arity) :-
	prog(lit(_,_,Pred,Arity)),
	!,
	syntax_error(order_decl_after_use(Pred,Arity)),
	fail.

check_not_used(_, _).

%------------------------------------------------------------------------------
% semantic_check_rule(+Facts):
%------------------------------------------------------------------------------

% This is called after a rule was parsed and translated to facts.
% The facts of the current rule are stored in the dynamic predicate rule.
% They are not yet in the dynamic predicate prog.

semantic_check_rule(Facts) :-
	retractall(rule(_)),
	assert_rule_facts(Facts),
	\+ err_range_restrict,
	\+ err_ospec_std_pred,
	\+ err_index_std_pred.

%------------------------------------------------------------------------------
% assert_rule_facts(+Facts):
%------------------------------------------------------------------------------

assert_rule_facts([]).

assert_rule_facts([Fact|MoreFacts]) :-
	assert(rule(Fact)),
	assert_rule_facts(MoreFacts).

%------------------------------------------------------------------------------
% err_range_restrict:
%------------------------------------------------------------------------------

err_range_restrict :-
	rule_var(Var),
	\+ bound(Var),
	syntax_error(unbound_var(Var)).

%------------------------------------------------------------------------------
% rule_var(-Var):
%------------------------------------------------------------------------------

% Variables that occur in the current rule.

rule_var(Var) :-
	rule(arg(_RuleNo, _LitNo, _ArgNo, var,  Var)).

rule_var(Var) :-
	rule(order(_RuleNo, _LitNo, _ArgNo, asc_var,  Var)).

rule_var(Var) :-
	rule(order(_RuleNo, _LitNo, _ArgNo, desc_var,  Var)).

%------------------------------------------------------------------------------
% bound(+Var):
%------------------------------------------------------------------------------

% Variables that are bound, i.e. appear in positive body literals.

bound(Var) :-
	rule(arg(RuleNo, LitNo, _ArgNo, var,  Var)),
	LitNo > 0, % Body Literal
	\+ rule(negated(RuleNo, LitNo)),
	\+ rule(complit(RuleNo, LitNo, _Op)).

bound(Var) :-
	rule(row_number(RuleNo, LitNo, var,  Var)),
	LitNo > 0, % Body Literal
	\+ rule(negated(RuleNo, LitNo)).

bound(Var) :-
	rule(rank(RuleNo, LitNo, var,  Var)),
	LitNo > 0, % Body Literal
	\+ rule(negated(RuleNo, LitNo)).

bound(Var) :-
	rule(dense_rank(RuleNo, LitNo, var,  Var)),
	LitNo > 0, % Body Literal
	\+ rule(negated(RuleNo, LitNo)).

bound(Var) :-
	rule(next(RuleNo, LitNo, var,  Var)),
	LitNo > 0, % Body Literal
	\+ rule(negated(RuleNo, LitNo)).

%------------------------------------------------------------------------------
% err_ospec_std_pred:
%------------------------------------------------------------------------------

% An order specification was used in the head,
% but the predicate is not declared as ordered.

err_ospec_std_pred :-
	rule(order(RuleNo, LitNo, _, _, _)),
	rule(lit(RuleNo, LitNo, Pred, Arity)),
	\+ prog(ordered_pred(Pred, Arity)),
	syntax_error(ospec_std_pred(Pred, Arity)).

%------------------------------------------------------------------------------
% err_index_std_pred:
%------------------------------------------------------------------------------

% An index was used on a body literal,
% but the predicate of this literal is not declared as ordered.

err_index_std_pred :-
	err_index_used(RuleNo, LitNo),
	rule(lit(RuleNo, LitNo, Pred, Arity)),
	\+ prog(ordered_pred(Pred, Arity)),
	syntax_error(index_std_pred(Pred, Arity)).

% err_index_used(-RuleNo, -LitNo):
% Check whether in the body of the current rule an index is used.

err_index_used(RuleNo, LitNo) :-
	rule(row_number(RuleNo, LitNo, _, _)).

err_index_used(RuleNo, LitNo) :-
	rule(rank(RuleNo, LitNo, _, _)).

err_index_used(RuleNo, LitNo) :-
	rule(dense_rank(RuleNo, LitNo, _, _)).

err_index_used(RuleNo, LitNo) :-
	rule(last(RuleNo, LitNo)).

%==============================================================================
% Stratification:
%==============================================================================

%------------------------------------------------------------------------------
% stratification_error:
%------------------------------------------------------------------------------

stratification_error :-
	eval_before(Pred1, Arity1, Pred2, Arity2),
	used_by(Pred2, Arity2, Pred1, Arity1),
	!,
	write('The program violates the stratification condition.'),
	nl,
	write('E.g. '),
	write(Pred1),
	write('/'),
	write(Arity1),
	write(' must be evaluated before '),
	write(Pred2),
	write('/'),
	write(Arity2),
	write(','),
	nl,
	write('but '),
	write(Pred1),
	write('/'),
	write(Arity1),
	write(' conversely depends on '),
	write(Pred2),
	write('/'),
	write(Arity2),
	write(' (possibly indirectly).'),
	nl,
	nl.

%------------------------------------------------------------------------------
% pred(-Pred, -Arity):
%------------------------------------------------------------------------------

pred(Pred, Arity) :-
	prog(lit(_Rule, _Lit, Pred, Arity)).

%------------------------------------------------------------------------------
% eval_before(-Pred1, -Arity1, -Pred2, -Arity2):
%------------------------------------------------------------------------------

% Pred1/Arity1 must be evaluated strictly before Pred2/Arity2.
% I.e. there is a rule with Pred2/Arity2 in the head,
% and Pred1/Arity1 negated or with index in the body.

eval_before(Pred1, Arity1, Pred2, Arity2) :-
	prog(lit(Rule, 0, Pred2, Arity2)),
	prog(lit(Rule, Lit, Pred1, Arity1)),
	prog(negated(Rule, Lit)).

eval_before(Pred1, Arity1, Pred2, Arity2) :-
	prog(lit(Rule, 0, Pred2, Arity2)),
	prog(lit(Rule, Lit, Pred1, Arity1)),
	prog(row_number(Rule, Lit, _, _)).

eval_before(Pred1, Arity1, Pred2, Arity2) :-
	prog(lit(Rule, 0, Pred2, Arity2)),
	prog(lit(Rule, Lit, Pred1, Arity1)),
	prog(rank(Rule, Lit, _, _)).

eval_before(Pred1, Arity1, Pred2, Arity2) :-
	prog(lit(Rule, 0, Pred2, Arity2)),
	prog(lit(Rule, Lit, Pred1, Arity1)),
	prog(dense_rank(Rule, Lit, _, _)).

eval_before(Pred1, Arity1, Pred2, Arity2) :-
	prog(lit(Rule, 0, Pred2, Arity2)),
	prog(lit(Rule, Lit, Pred1, Arity1)),
	prog(next(Rule, Lit, _, _)).

eval_before(Pred1, Arity1, Pred2, Arity2) :-
	prog(lit(Rule, 0, Pred2, Arity2)),
	prog(lit(Rule, Lit, Pred1, Arity1)),
	prog(last(Rule, Lit)).

%------------------------------------------------------------------------------
% used_by_direct(-Pred1, -Arity1, -Pred2, -Arity2):
%------------------------------------------------------------------------------

% Pred1/Arity1 is directly used by Pred2/Arity2,
% I.e. there is a rule with Pred2/Arity2 in the head,
% and Pred1/Arity1 in the body.
% In other words: Pred2/Arity2 directly depends on Pred1/Arity1.

used_by_direct(Pred1, Arity1, Pred2, Arity2) :-
	prog(lit(Rule, 0, Pred2, Arity2)),
	prog(lit(Rule, Lit, Pred1, Arity1)),
	Lit > 0.

%------------------------------------------------------------------------------
% used_by(-Pred1, -Arity1, -Pred2, -Arity2):
%------------------------------------------------------------------------------

% This is the transitive closure of used_by.

used_by(Pred1, Arity1, Pred2, Arity2) :-
	used_by(Pred1, Arity1, Pred2, Arity2, []).

% The additional argument ensures termination.

used_by(Pred1, Arity1, Pred2, Arity2, Excluded) :-
	used_by_direct(Pred1, Arity1, Pred2, Arity2),
	\+ member(excluded(Pred2,Arity2), Excluded).

used_by(Pred1, Arity1, Pred3, Arity3, Excluded) :-
	used_by_direct(Pred1, Arity1, Pred2, Arity2),
	\+ member(excluded(Pred2,Arity2), Excluded),
	used_by(Pred2, Arity2, Pred3, Arity3,
		[excluded(Pred2,Arity2)|Excluded]).

%------------------------------------------------------------------------------
% compute_stratification(-MaxLevel):
%------------------------------------------------------------------------------

compute_stratification(MaxLevel) :-
	compute_stratification(0, MaxLevel).

% compute_stratification(+Level)

compute_stratification(Level, MaxLevel) :-
	can_be_assigned(Pred, Arity, Level),
	!,
	assert(stratification(Level, Pred, Arity)),
	compute_stratification(Level, MaxLevel).

compute_stratification(Level, MaxLevel) :-
	pred_not_done(_Pred, _Arity),
	!,
	stratification(Level, _, _), % The current level is not empty
	NextLevel is Level+1,
	compute_stratification(NextLevel, MaxLevel).

compute_stratification(Level, Level).

%------------------------------------------------------------------------------
% pred_not_done(-Pred, -Arity):
%------------------------------------------------------------------------------

pred_not_done(Pred, Arity) :-
	pred(Pred, Arity),
	\+ stratification(_Level, Pred, Arity).

%------------------------------------------------------------------------------
% can_be_assigned(-Pred, -Arity, +Level):
%------------------------------------------------------------------------------

can_be_assigned(Pred, Arity, Level) :-
	pred(Pred, Arity),
	\+ stratification(_, Pred, Arity), % has no stratification level yet.
	\+ must_wait(Pred, Arity, Level).

% must_wait(+Pred, +Arity, +Level):
% i.e. depends on another predicate negatively or with index,
% and the other predicate is not yet assigned a stratification level,
% or is assigned the same level.

must_wait(Pred, Arity, _Level) :-
	eval_before(OtherPred, OtherArity, Pred, Arity),
	\+ stratification(_, OtherPred, OtherArity),
	!.

must_wait(Pred, Arity, Level) :-
	eval_before(OtherPred, OtherArity, Pred, Arity),
	stratification(Level, OtherPred, OtherArity),
	!.

% I first forgot the following rule.
% The predicate must also wait if it directly depends on another predicate
% which is not yet assigned a stratification level.
% E.g. in p <- q. q <- \+ r.
% The predicate p must not end up in level 0.
% Its level must be at least the level of q.

must_wait(Pred, Arity, _Level) :-
	used_by_direct(OtherPred, OtherArity, Pred, Arity),
	\+ stratification(_, OtherPred, OtherArity),
	!.

%------------------------------------------------------------------------------
% show_stratification(+MaxLevel):
%------------------------------------------------------------------------------

show_stratification(MaxLevel) :-
	option(show_stratification),
	!,
	nl,
	write('Stratification:'),
	nl,
	nl,
	show_stratification_levels(0, MaxLevel).

show_stratification(_).

%------------------------------------------------------------------------------
% show_stratification_levels(+StartLevel, +MaxLevel):
%------------------------------------------------------------------------------

show_stratification_levels(Level, MaxLevel) :-
	Level > MaxLevel,
	!,
	nl.

show_stratification_levels(Level, MaxLevel) :-
	Level =< MaxLevel,
	write('    Level '),
	write(Level),
	write(':'),
	nl,
	show_stratification_preds(Level),
	nl,
	NextLevel is Level + 1,
	show_stratification_levels(NextLevel, MaxLevel).

%------------------------------------------------------------------------------
% show_stratification_preds(+Level):
%------------------------------------------------------------------------------

show_stratification_preds(Level) :-
	stratification(Level, Pred, Arity),
	write('        '),
	write(Pred),
	write('/'),
	write(Arity),
	nl,
	fail.

show_stratification_preds(_).

%==============================================================================
% Naive Bottom-Up Evaluation:
%==============================================================================

%------------------------------------------------------------------------------
% Main Bottom-Up Loop:
%------------------------------------------------------------------------------

botup(MaxLevel) :-
	botup(0, MaxLevel).

% botup(+StartLevel, +MaxLevel):

botup(Level, MaxLevel) :-
	Level > MaxLevel,
	!.

botup(Level, MaxLevel) :-
	Level =< MaxLevel,
	botup_level(Level),
	NextLevel is Level + 1,
	botup(NextLevel, MaxLevel).

%------------------------------------------------------------------------------
% botup_level(+Level):
%------------------------------------------------------------------------------

botup_level(Level) :-
	derivable(Level, Fact, Partition, Order),
	\+ derived(Fact, Partition, Order),
	!,
	assert(derived(Fact, Partition, Order)),
	functor(Fact, Pred, Arity),
	store_derived_pred(Pred, Arity),
	store_partition_value(Pred, Arity, Partition),
	botup_level(Level).

botup_level(Level) :-
	compute_indexes(Level).

%------------------------------------------------------------------------------
% Keep list of predicates in derived facts:
%------------------------------------------------------------------------------

store_derived_pred(Pred, Arity) :-
	derived_pred(Pred, Arity),
	!.

store_derived_pred(Pred,Arity) :-
	\+ derived_pred(Pred, Arity),
	assert(derived_pred(Pred,Arity)).

%------------------------------------------------------------------------------
% Keep list of occuring partition values:
%------------------------------------------------------------------------------

store_partition_value(Pred, Arity, Partition) :-
	partition_value(Pred, Arity, Partition),
	!.

store_partition_value(Pred, Arity, Partition) :-
	\+ partition_value(Pred, Arity, Partition),
	assert(partition_value(Pred, Arity, Partition)).

%------------------------------------------------------------------------------
% Representation of the input program as facts:
%------------------------------------------------------------------------------

% fact(RuleNo, LineNo)
% rule(RuleNo, LineNo, NumBodyLit)
%
% lit(RuleNo, LitNo, Pred, NumArgs) // LitNo == 0 means head literal
% complit(RuleNo, LitNo, Op)
%
% arg(RuleNo, LitNo, ArgNo, var,  Var)
% arg(RuleNo, LitNo, ArgNo, str,  Str)
% arg(RuleNo, LitNo, ArgNo, int,  Int)
% arg(RuleNo, LitNo, ArgNo, const, Const)

%------------------------------------------------------------------------------d
% Finding Derivable Facts:
%------------------------------------------------------------------------------

derivable(Level, Fact, Partition, Order) :-
	prog(lit(RuleNo, 0, Pred, Arity)),
	stratification(Level, Pred, Arity),
	is_derivable(RuleNo, Fact, Partition, Order).

% is_derivable(+RuleNo, -Fact):

is_derivable(RuleNo, Fact, Partition, Order) :-
	prog(fact(RuleNo,_LineNo)),
	construct_fact(RuleNo, 0, [], Fact),
	construct_part_order(RuleNo, 0, [], Partition, Order).

is_derivable(RuleNo, Fact, Partition, Order) :-
	prog(rule(RuleNo,_LineNo,NumBodyLit)),
	solve_body(RuleNo, NumBodyLit, Subst),
	construct_fact(RuleNo, 0, Subst, Fact),
	construct_part_order(RuleNo, 0, Subst, Partition, Order).

%------------------------------------------------------------------------------d
% Construct derived fact:
%------------------------------------------------------------------------------

% construct_fact(+RuleNo, +LitNo, +Subst, -Fact):

construct_fact(RuleNo, LitNo, Subst, Fact) :-
	prog(lit(RuleNo, LitNo, Pred, NumArgs)),
	construct_arglist(RuleNo, LitNo, Subst, 0, NumArgs, ArgList),
	Fact =.. [Pred|ArgList].


% construct_arglist(+RuleNo, +LitNo, +Subst, +LastArgNo, +NumArgs, -ArgList):

construct_arglist(_, _, _, NumArgs, NumArgs, []).

construct_arglist(RuleNo, LitNo, Subst, LastArgNo, NumArgs, [Arg|ArgList]) :-
	LastArgNo < NumArgs,
	ArgNo is LastArgNo + 1,
	construct_arg(RuleNo, LitNo, ArgNo, Subst, Arg),
	construct_arglist(RuleNo, LitNo, Subst, ArgNo, NumArgs, ArgList).


% construct_arg(+RuleNo, +LitNo, +ArgNo, +Subst, -Arg):

construct_arg(RuleNo, LitNo, ArgNo, Subst, Val) :-
	prog(arg(RuleNo, LitNo, ArgNo, var, Var)),
	apply_subst(Subst, Var, Val).

construct_arg(RuleNo, LitNo, ArgNo, _, Const) :-
	prog(arg(RuleNo, LitNo, ArgNo, const, Const)).

construct_arg(RuleNo, LitNo, ArgNo, _, Int) :-
	prog(arg(RuleNo, LitNo, ArgNo, int, Int)).

construct_arg(RuleNo, LitNo, ArgNo, _, Str) :-
	prog(arg(RuleNo, LitNo, ArgNo, str, Str)).


% apply_subst(+Subst, +Var, -Val):

apply_subst([subst(Var,Val)|_], Var, Val) :- !.

apply_subst([_|Subst], Var, Val) :-
	apply_subst(Subst, Var, Val).

%------------------------------------------------------------------------------
% Construct Partition and Order Data (i.e. instanciate order specification):
%------------------------------------------------------------------------------

% construct_part_order(+RuleNo, +LitNo, +Subst, -Partition, -Order).

construct_part_order(RuleNo, LitNo, Subst, Partition, Order) :-
	prog(partition(RuleNo, LitNo, LastPartPos)),
	!,
	prog(order_spec(RuleNo, LitNo, LastOrderPos)),
	FirstOrderPos is LastPartPos + 1,
	construct_po_list(RuleNo, LitNo, Subst, 1, LastPartPos, Partition),
	construct_po_list(RuleNo, LitNo, Subst, FirstOrderPos, LastOrderPos,
								Order).
construct_part_order(RuleNo, LitNo, Subst, [], Order) :-
	prog(order_spec(RuleNo, LitNo, LastOrderPos)),
	!,
	construct_po_list(RuleNo, LitNo, Subst, 1, LastOrderPos, Order).

construct_part_order(_RuleNo, _LitNo, _Subst, [], []).

% construct_po_list(+RuleNo, +LitNo, +Subst, +FirstPos, +LastPos, -ArgList):

construct_po_list(_RuleNo, _LitNo, _Subst, FirstPos, LastPos, []) :-
	FirstPos > LastPos,
	!.

construct_po_list(RuleNo, LitNo, Subst, FirstPos, LastPos, [Arg|ArgList]) :-
	FirstPos =< LastPos,
	construct_po_arg(RuleNo, LitNo, Subst, FirstPos, Arg),
	NextPos is FirstPos + 1,
	construct_po_list(RuleNo, LitNo, Subst, NextPos, LastPos, ArgList).

% construct_po_arg(+RuleNo, +LitNo, +Subst, +Pos, -Arg):

construct_po_arg(RuleNo, LitNo, Subst, Pos, Arg) :-
	prog(order(RuleNo, LitNo, Pos, asc_var, Var)),
	member(subst(Var,Arg), Subst).

construct_po_arg(RuleNo, LitNo, _Subst, Pos, Arg) :-
	prog(order(RuleNo, LitNo, Pos, asc_int, Arg)).

construct_po_arg(RuleNo, LitNo, _Subst, Pos, Arg) :-
	prog(order(RuleNo, LitNo, Pos, asc_str, Arg)).

construct_po_arg(RuleNo, LitNo, _Subst, Pos, Arg) :-
	prog(order(RuleNo, LitNo, Pos, asc_rno, Arg)).

construct_po_arg(RuleNo, LitNo, Subst, Pos, desc(Arg)) :-
	prog(order(RuleNo, LitNo, Pos, desc_var, Var)),
	member(subst(Var,Arg), Subst).

construct_po_arg(RuleNo, LitNo, _Subst, Pos, desc(Arg)) :-
	prog(order(RuleNo, LitNo, Pos, desc_int, Arg)).

construct_po_arg(RuleNo, LitNo, _Subst, Pos, desc(Arg)) :-
	prog(order(RuleNo, LitNo, Pos, desc_str, Arg)).

%------------------------------------------------------------------------------
% Find Substitution to Make Body True:
%------------------------------------------------------------------------------

% solve_body(+RuleNo, +NumBodyLit, -Subst):

% Note: We must first solve the positive body literals to get values
%       for all variables. The range restriction ensures that all variables
%	appear in a positive body literal.
%	But the user can write the negative body literals first.
%	Therefore we simply do two loops over the body literals:
%	In the first round, the positive ones are processed,
%	in the second round, the negative ones.

solve_body(RuleNo, NumBodyLit, Subst) :-
	solve_pos_body_lits(RuleNo, 0, NumBodyLit, [], Subst),
	solve_neg_body_lits(RuleNo, 0, NumBodyLit, Subst).

%------------------------------------------------------------------------------
% solve_pos_body_lits(+RuleNo, +LastLitNo, +NumBodyLit, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

solve_pos_body_lits(_, NumBodyLit, NumBodyLit, Subst, Subst).

solve_pos_body_lits(RuleNo, LastLitNo, NumBodyLit, SubstIn, SubstOut) :-
	LastLitNo < NumBodyLit,
	LitNo is LastLitNo + 1,
	solve_pos_body_lit(RuleNo, LitNo, SubstIn, Subst),
	solve_pos_body_lits(RuleNo, LitNo, NumBodyLit, Subst, SubstOut).


%------------------------------------------------------------------------------
% solve_pos_body_lit(+RuleNo, +LitNo, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

solve_pos_body_lit(RuleNo, LitNo, SubstIn, SubstOut) :-
	\+ prog(negated(RuleNo, LitNo)),
	solve_body_lit(RuleNo, LitNo, SubstIn, SubstOut).

solve_pos_body_lit(RuleNo, LitNo, Subst, Subst) :-
	prog(negated(RuleNo,LitNo)). % skip negated literals

%------------------------------------------------------------------------------
% solve_neg_body_lits(+RuleNo, +LastLitNo, +NumBodyLit, +Subst):
%------------------------------------------------------------------------------

% Note: LastLitNo means the previous value for LitNo.

solve_neg_body_lits(_, NumBodyLit, NumBodyLit, _).

solve_neg_body_lits(RuleNo, LastLitNo, NumBodyLit, Subst) :-
	LastLitNo < NumBodyLit,
	LitNo is LastLitNo + 1,
	solve_neg_body_lit(RuleNo, LitNo, Subst),
	solve_neg_body_lits(RuleNo, LitNo, NumBodyLit, Subst).

%------------------------------------------------------------------------------
% solve_neg_body_lit(+RuleNo, +LitNo, +Subst):
%------------------------------------------------------------------------------

% Note: The parser ensures that there are no unbound variables.
% The program here would permit anonymouns variables,
% or more precisely, variables appearing only in a single negative
% body literal (the variable may appear more than once in that body literal).
% If variables are bound, the resulting substitution is simply forgotten
% after the literal is evaluated.

solve_neg_body_lit(RuleNo, LitNo, _) :-
	\+ prog(negated(RuleNo,LitNo)). % Skip positive body literal.

solve_neg_body_lit(RuleNo, LitNo, Subst) :-
	prog(negated(RuleNo,LitNo)),
	\+ solve_body_lit(RuleNo, LitNo, Subst, _SubstOut).

%------------------------------------------------------------------------------
% solve_body_lit(+RuleNo, +LitNo, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

% Note: Recursion with ordered predicates is possible,
% as long as no index is used to query the position in the sort order.
% So whether we match a body literal with derived/3 or derived_with_pos/5
% depends not on whether it has an ordered predicate or not,
% but on whether it has an index or not.

solve_body_lit(RuleNo, LitNo, SubstIn, SubstOut) :-
	prog(lit(RuleNo,LitNo,Pred,Arity)),
	\+ has_index(RuleNo, LitNo),
	functor(Lit,Pred,Arity),
	derived(Lit, _, _),
	Lit =.. [Pred|ArgList],
	match_args(RuleNo, LitNo, 1, ArgList, SubstIn, SubstOut).

solve_body_lit(RuleNo, LitNo, SubstIn, SubstOut) :-
	prog(lit(RuleNo,LitNo,Pred,Arity)),
	has_index(RuleNo, LitNo),
	functor(Lit,Pred,Arity),
	derived_with_pos(Lit, RowNumber, Rank, DenseRank, Last),
	compute_next(RowNumber, Last, Next),
	Lit =.. [Pred|ArgList],
	match_args(RuleNo, LitNo, 1, ArgList, SubstIn, Subst1),
	match_row_number(RuleNo, LitNo, RowNumber, Subst1, Subst2),
	match_rank(RuleNo, LitNo, Rank, Subst2, Subst3),
	match_dense_rank(RuleNo, LitNo, DenseRank, Subst3, Subst4),
	match_next(RuleNo, LitNo, Next, Subst4, Subst5),
	match_last(RuleNo, LitNo, Last, Subst5, SubstOut).

solve_body_lit(RuleNo, LitNo, Subst, Subst) :-
	prog(complit(RuleNo,LitNo,Op)),
	arg_val(RuleNo, LitNo, 1, Subst, Val1),
	arg_val(RuleNo, LitNo, 2, Subst, Val2),
	eval_comp_op(Op, Val1, Val2).

%------------------------------------------------------------------------------
% has_index(+RuleNo, +LitNo):
%------------------------------------------------------------------------------

has_index(RuleNo, LitNo) :-
	prog(row_number(RuleNo, LitNo, _, _)),
	!.

has_index(RuleNo, LitNo) :-
	prog(rank(RuleNo, LitNo, _, _)),
	!.

has_index(RuleNo, LitNo) :-
	prog(dense_rank(RuleNo, LitNo, _, _)),
	!.

has_index(RuleNo, LitNo) :-
	prog(next(RuleNo, LitNo, _, _)),
	!.

has_index(RuleNo, LitNo) :-
	prog(last(RuleNo, LitNo)),
	!.

%------------------------------------------------------------------------------
% match_args(+RuleNo, +LitNo, +ArgNo, +ArgList, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

match_args(_, _, _, [], Subst, Subst).

match_args(RuleNo, LitNo, ArgNo, [Arg|ArgList], SubstIn, SubstOut) :-
	match_arg(RuleNo, LitNo, ArgNo, Arg, SubstIn, Subst),
	NextArgNo is ArgNo + 1,
	match_args(RuleNo, LitNo, NextArgNo, ArgList, Subst, SubstOut).

%------------------------------------------------------------------------------
% match_arg(+RuleNo, +LitNo, +ArgNo, +Arg, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

match_arg(RuleNo, LitNo, ArgNo, Arg, Subst, Subst) :-
	prog(arg(RuleNo,LitNo,ArgNo,const,Arg)).

match_arg(RuleNo, LitNo, ArgNo, Arg, Subst, Subst) :-
	prog(arg(RuleNo,LitNo,ArgNo,str,Arg)).

match_arg(RuleNo, LitNo, ArgNo, Arg, Subst, Subst) :-
	prog(arg(RuleNo,LitNo,ArgNo,int,Arg)).

match_arg(RuleNo, LitNo, ArgNo, Arg, SubstIn, SubstOut) :-
	prog(arg(RuleNo,LitNo,ArgNo,var,Var)),
	subst_is(Var, Arg, SubstIn, SubstOut).

%------------------------------------------------------------------------------
% arg_val(+RuleNo, +LitNo, +ArgNo, +Subst, -Val):
%------------------------------------------------------------------------------

arg_val(RuleNo, LitNo, ArgNo, Subst, Val) :-
	prog(arg(RuleNo,LitNo,ArgNo,var,Var)),
	subst_val(Var, Subst, Val).

arg_val(RuleNo, LitNo, ArgNo, _Subst, Val) :-
	prog(arg(RuleNo,LitNo,ArgNo,int,Val)).

arg_val(RuleNo, LitNo, ArgNo, _Subst, Val) :-
	prog(arg(RuleNo,LitNo,ArgNo,str,Val)).

arg_val(RuleNo, LitNo, ArgNo, _Subst, Val) :-
	prog(arg(RuleNo,LitNo,ArgNo,const,Val)).

%------------------------------------------------------------------------------
% eval_comp_op(+Op, +Val1, +Val2):
%------------------------------------------------------------------------------

eval_comp_op(eq, Val1, Val2) :-
	!,
	Val1 == Val2.

eval_comp_op(ne, Val1, Val2) :-
	!,
	Val1 \= Val2.

eval_comp_op(lt, Val1, Val2) :-
	number(Val1),
	number(Val2),
	!,
	Val1 < Val2.

eval_comp_op(lt, Val1, Val2) :-
	is_string(Val1),
	is_string(Val2),
	!,
	string_before(Val1, Val2).

eval_comp_op(le, Val1, Val2) :-
	number(Val1),
	number(Val2),
	!,
	Val1 =< Val2.

eval_comp_op(le, Val1, Val2) :-
	is_string(Val1),
	is_string(Val2),
	!,
	(Val1 == Val2; string_before(Val1, Val2)).

eval_comp_op(gt, Val1, Val2) :-
	!,
	eval_comp_op(lt, Val2, Val1).

eval_comp_op(ge, Val1, Val2) :-
	!,
	eval_comp_op(le, Val2, Val1).


%------------------------------------------------------------------------------
% match_row_number(+RuleNo, +LitNo, +RowNumber, +SubstIn, SubstOut):
%------------------------------------------------------------------------------

match_row_number(RuleNo, LitNo, _, Subst, Subst) :-
	\+prog(row_number(RuleNo, LitNo, _, _)),
	!.

match_row_number(RuleNo, LitNo, RowNumber, SubstIn, SubstOut) :-
	prog(row_number(RuleNo, LitNo, var, Var)),
	subst_is(Var, RowNumber, SubstIn, SubstOut).

match_row_number(RuleNo, LitNo, RowNumber, Subst, Subst) :-
	prog(row_number(RuleNo, LitNo, int, RowNumber)).

%------------------------------------------------------------------------------
% match_rank(+RuleNo, +LitNo, +Rank, +SubstIn, SubstOut):
%------------------------------------------------------------------------------

match_rank(RuleNo, LitNo, _, Subst, Subst) :-
	\+prog(rank(RuleNo, LitNo, _, _)),
	!.

match_rank(RuleNo, LitNo, Rank, SubstIn, SubstOut) :-
	prog(rank(RuleNo, LitNo, var, Var)),
	subst_is(Var, Rank, SubstIn, SubstOut).

match_rank(RuleNo, LitNo, Rank, Subst, Subst) :-
	prog(rank(RuleNo, LitNo, int, Rank)).

%------------------------------------------------------------------------------
% match_dense_rank(+RuleNo, +LitNo, +DenseRank, +SubstIn, SubstOut):
%------------------------------------------------------------------------------

match_dense_rank(RuleNo, LitNo, _, Subst, Subst) :-
	\+prog(dense_rank(RuleNo, LitNo, _, _)),
	!.

match_dense_rank(RuleNo, LitNo, DenseRank, SubstIn, SubstOut) :-
	prog(dense_rank(RuleNo, LitNo, var, Var)),
	subst_is(Var, DenseRank, SubstIn, SubstOut).

match_dense_rank(RuleNo, LitNo, DenseRank, Subst, Subst) :-
	prog(dense_rank(RuleNo, LitNo, int, DenseRank)).

%------------------------------------------------------------------------------
% match_next(+RuleNo, +LitNo, +Next, +SubstIn, SubstOut):
%------------------------------------------------------------------------------

match_next(RuleNo, LitNo, _, Subst, Subst) :-
	\+prog(next(RuleNo, LitNo, _, _)),
	!.

match_next(RuleNo, LitNo, Next, SubstIn, SubstOut) :-
	prog(next(RuleNo, LitNo, var, Var)),
	subst_is(Var, Next, SubstIn, SubstOut).

match_next(RuleNo, LitNo, Next, Subst, Subst) :-
	prog(next(RuleNo, LitNo, int, Next)).

match_next(RuleNo, LitNo, nil, Subst, Subst) :-
	prog(next(RuleNo, LitNo, atom, nil)).

%------------------------------------------------------------------------------
% match_last(+RuleNo, +LitNo, +Last, +SubstIn, SubstOut):
%------------------------------------------------------------------------------

match_last(RuleNo, LitNo, _, Subst, Subst) :-
	\+prog(last(RuleNo, LitNo)),
	!.

match_last(RuleNo, LitNo, Last, Subst, Subst) :-
	prog(last(RuleNo, LitNo)),
	Last = 1.

%------------------------------------------------------------------------------
% compute_next(+RowNumber, +Last, -Next):
%------------------------------------------------------------------------------

compute_next(RowNumber, 0, Next) :-
	Next is RowNumber + 1.

compute_next(_, 1, nil).

%------------------------------------------------------------------------------
% Finding Derivable Facts (OLD!):
%------------------------------------------------------------------------------

derivable_old(Head) :-
	rule(Head, Body),
	is_true(Body).

is_true([]).

is_true([Lit|Rest]) :-
	check_lit(Lit),
	is_true(Rest).

check_lit(Lit) :-
	fact(Lit).

check_lit('>'(A,B)) :-
	A > B.

check_lit('>='(A,B)) :-
	A >= B.

check_lit('<'(A,B)) :-
	A < B.

check_lit('<='(A,B)) :-
	A =< B.

check_lit('='(A,B)) :-
	A = B.

check_lit('!='(A,B)) :-
	A \= B.

check_lit(inc(A,B)) :-
	B is A+1.

check_lit(concat(A,B,C)) :-
	atom_concat(A, B, C).

%==============================================================================
% Substitutions:
%==============================================================================

%------------------------------------------------------------------------------
% subst_val(+Var, +Subst, -Val):
%------------------------------------------------------------------------------

% This looks up a value of a variable in a substitution.
% It fails if the variable has no value yet.

subst_val(Var, Subst, Val) :-
	subst_contains(Subst, subst(Var,Val)).

%------------------------------------------------------------------------------
% subst_is(+Var, +Val, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

% This checks the value of a variable in a substitution.
% If the variable has a value, it must be the given value.
% If the variable has not yet a value, it is assigned the given value.

subst_is(Var, Val, Subst, Subst) :-
	subst_contains(Subst, subst(Var,Val)),
	!.

subst_is(Var, Val, SubstIn, [subst(Var,Val)|SubstIn]).


%------------------------------------------------------------------------------
% subst_contains(+Subst, +Elem):
%------------------------------------------------------------------------------

% This is an auxillary predicate, simply a version of "member"
% because the substitution is implemented as a list of subst(Var,Value) terms.
% If one uses only this predicate to access a substitution,
% one could later change the implementation.

subst_contains([Elem|_], Elem).

subst_contains([_|Rest], Elem) :-
	subst_contains(Rest, Elem).


%==============================================================================
% Compute Indexes:
%==============================================================================

%------------------------------------------------------------------------------
% compute_indexes(+Level):
%------------------------------------------------------------------------------

compute_indexes(Level) :-
	stratification(Level, Pred, Arity),
	prog(ordered_pred(Pred, Arity)),
	partition_value(Pred, Arity, Partition),
	functor(Fact, Pred, Arity),
	findall(ofact(Fact,Order), derived(Fact,Partition,Order), FactList),
	sort_facts(FactList, SortedFactList),
	assign_positions(SortedFactList),
	fail.

compute_indexes(_).

%------------------------------------------------------------------------------
% sort_facts(+ListIn, -ListOut):
%------------------------------------------------------------------------------

sort_facts(ListIn, ListOut) :-
	make_runs(ListIn, ListRuns),
	mergesort_iterate(ListRuns, ListOut).

% make_runs(+ListIn, -ListRuns):

make_runs([], []).

make_runs([Elem|RestList], [[Elem]|RestRuns]) :-
	make_runs(RestList, RestRuns).

% mergesort_iterate(+ListRuns, -SortedList):

mergesort_iterate([], []).

mergesort_iterate([Run], Run).

mergesort_iterate([Run1, Run2 | MoreRuns], SortedList) :-
	mergesort_pass([Run1, Run2 | MoreRuns], NextRunList),
	mergesort_iterate(NextRunList, SortedList).

% mergesort_pass(+RunList, -NextRunList):

mergesort_pass([], []).

mergesort_pass([Run], [Run]).

mergesort_pass([Run1, Run2 | MoreRunsIn], [Run12 | MoreRunsOut]) :-
	merge(Run1, Run2, Run12),
	mergesort_pass(MoreRunsIn, MoreRunsOut).

% merge(+Run1, +Run2, -Run):

merge([], Run, Run).

merge([E|R], [], [E|R]).

merge([E1|R1], [E2|R2], [E1|R]) :-
	before(E1, E2),
	!,
	merge(R1, [E2|R2], R).

merge([E1|R1], [E2|R2], [E2|R]) :-
	merge([E1|R1], R2, R).


%------------------------------------------------------------------------------
% before(+OFact1, +OFact2):
%------------------------------------------------------------------------------

before(ofact(_Fact1,OrderList1), ofact(_Fact2,OrderList2)) :-
	before_list(OrderList1, OrderList2).

%------------------------------------------------------------------------------
% before_list(+List1, +List2):
%------------------------------------------------------------------------------

before_list([], []).

before_list([], [_|_]).

before_list([Elem|List1], [Elem|List2]) :-
	!,
	before_list(List1, List2).

before_list([Elem1|_], [Elem2|_]) :-
	before_val(Elem1, Elem2).

%------------------------------------------------------------------------------
% before_val(+SortArg1, +SortArg2):
%------------------------------------------------------------------------------

before_val(X, Y) :-
	number(X),
	number(Y),
	!,
	X < Y.

before_val(X, Y) :-
	number(X),
	is_string(Y),
	!.

before_val(X, Y) :-
	is_string(X),
	is_string(Y),
	!,
	string_before(X, Y).

before_val(desc(X), desc(Y)) :-
	number(X),
	number(Y),
	!,
	Y < X.

before_val(desc(X), desc(Y)) :-
	is_string(X),
	number(Y),
	!.

before_val(desc(X), desc(Y)) :-
	is_string(X),
	is_string(Y),
	!,
	string_before(Y, X).

before_val(X, desc(_)) :-
	X \= desc(_),
	!.

%------------------------------------------------------------------------------
% is_string(+S):
%------------------------------------------------------------------------------

% Strings are represented as lists of atoms.
% We only have to check that it is a list,
% because the only other alternative is a number.

is_string([]).

is_string([_|_]).

%------------------------------------------------------------------------------
% string_before(+S1, +S2):
%------------------------------------------------------------------------------

string_before([], [_|_]).

string_before([C|S1], [C|S2]) :-
	!,
	string_before(S1, S2).

string_before([X|_], [Y|_]) :-
	X @< Y.

%------------------------------------------------------------------------------
% assign_positions(+SortedFactList):
%------------------------------------------------------------------------------

assign_positions(SortedFactList) :-
	assign_pos(SortedFactList, 0, 0, 0, nil).

% assign_pos(+FactList, +PrevRowNumber, +PrevRank, +PrevDenseRank, +PrevVal):

assign_pos([], _, _, _, _).

assign_pos([ofact(Fact,Val)|FactList], PrevRowNumber, PrevRank, PrevDenseRank,
		Val) :-
	!,
	RowNumber is PrevRowNumber + 1,
	Rank = PrevRank,
	DenseRank = PrevDenseRank,
	set_last(FactList, Last),
	assert(derived_with_pos(Fact, RowNumber, Rank, DenseRank, Last)),
	assign_pos(FactList, RowNumber, Rank, DenseRank, Val).

assign_pos([ofact(Fact,Val)|FactList], PrevRowNumber, _PrevRank, PrevDenseRank,
		PrevVal) :-
	Val \= PrevVal,
	!,
	RowNumber is PrevRowNumber + 1,
	Rank = RowNumber,
	DenseRank is PrevDenseRank + 1,
	set_last(FactList, Last),
	assert(derived_with_pos(Fact, RowNumber, Rank, DenseRank, Last)),
	assign_pos(FactList, RowNumber, Rank, DenseRank, Val).

% set_last(+List, -Last)

set_last([], 1).

set_last([_|_], 0).

%==============================================================================
% Show Facts:
%==============================================================================

%------------------------------------------------------------------------------
% Show derived facts:
%------------------------------------------------------------------------------

show_derived_facts :-
	option(show_derived_facts),
	derived_pred(Pred, Arity),
	nl,
	write(Pred),
	write('/'),
	write(Arity),
	write(':'),
	nl,
	show_derived_facts(Pred, Arity),
	show_sorted_facts(Pred, Arity),
	nl,
	fail.

show_derived_facts.


% show_derived_facts(+Pred, +Arity):

show_derived_facts(Pred, Arity) :-
	functor(Fact, Pred, Arity),
	derived(Fact, Partition, Order),
	write('\t'),
	show_derived_fact(Fact, Pred, Arity, Partition, Order),
	%write('.'),
	%nl,
	fail.

show_derived_facts(_, _).

% show_derived_fact(+Fact, +Pred, +Arity, +Partition, +Order)

show_derived_fact(Fact, Pred, Arity, Partition, Order) :-
	prog(ordered_pred(Pred, Arity)),
	!,
	write(Pred),
	show_part_order(Partition, Order),
	Fact =.. [Pred|Args],
	show_args(Args),
	write('.'),
	nl.

show_derived_fact(Fact, _, _, _, _) :-
	show_fact(Fact),
	nl.

% show_part_order(+Partition, +Order).

show_part_order([], Order) :-
	!,
	write('<'),
	show_po_list(Order),
	write('>').

show_part_order(Partition, Order) :-
	!,
	write('<'),
	show_po_list(Partition),
	write('|'),
	show_po_list(Order),
	write('>').

% show_po_list(+Args):

show_po_list([]).

show_po_list([Arg|Args]) :-
	show_po_arg(Arg),
	show_po_rest(Args).

% show_po_rest(+Args):

show_po_rest([]).

show_po_rest([Arg|Args]) :-
	write(','),
	show_po_arg(Arg),
	show_po_rest(Args).

% show_po_arg(+Arg):

show_po_arg(desc(Arg)) :-
	!,
	write('^'),
	show_arg(Arg).

show_po_arg(Arg) :-
	show_arg(Arg).

% show_sorted_facts(+Pred, +Arity):

show_sorted_facts(Pred, Arity) :-
	prog(ordered_pred(Pred, Arity)),
	!,
	do_show_sorted_facts(Pred, Arity).

show_sorted_facts(_, _).

% do_show_sorted_facts(+Pred, +Arity):

do_show_sorted_facts(Pred, Arity) :-
	nl,
	write('After Sorting:'),
	nl,
	functor(Fact, Pred, Arity),
	derived_with_pos(Fact, RowNumber, Rank, DenseRank, Last),
	write('\t'),
	write(Pred),
	write('['),
	write(RowNumber),
	write(',rank:'),
	write(Rank),
	write(',dense_rank:'),
	write(DenseRank),
	write(',last:'),
	write(Last),
	write(']'),
	Fact =.. [Pred|Args],
	show_args(Args),
	write('.'),
	nl,
	fail.

do_show_sorted_facts(_, _).

%==============================================================================
% Printing of Output and Answer:
%==============================================================================

%------------------------------------------------------------------------------
% show_output:
%------------------------------------------------------------------------------

%	Output is shown if there is an ordered predicate "output" of arity 1.

show_output :-
	prog(ordered_pred(output,1)),
	!,
	nl,
	write('*** Output: ***'),
	nl,
	do_show_output,
	nl.

show_output :-
	prog(lit(_,_,output,_)),
	!,
	nl,
	write('Warning: '),
	write('There is a predicate output, '),
	write('but no ordered predicate of arity 1.'),
	nl,
	write('Output is generated only after the declaration: '),
	write('ordered output/1.'),
	nl.

show_output.


% do_show_output:
%	Check whether output is empty:

do_show_output :-
	derived_with_pos(output(_),_,_,_,_),
	!,
	do_show_output(1).

do_show_output :-
	write('(Output is empty)').

% do_show_output(+RowNumber)

do_show_output(RowNumber) :-
	derived_with_pos(output(Text),RowNumber,_,_,_),
	!,
	print_text(Text),
	NextRowNumber is RowNumber+1,
	do_show_output(NextRowNumber).

do_show_output(_).
	% End of Loop. No further text piece was found.

% print_text(+CharList):

print_text([]) :-
	!.

print_text([Char|MoreChars]) :-
	!,
	write(Char),
	print_text(MoreChars).

print_text(Other) :-
	atomic(Other),
	write(Other).

%------------------------------------------------------------------------------
% show_answer:
%------------------------------------------------------------------------------

show_answer :-
	stratification(_Level, answer, Arity),
	nl,
	write('*** Answer ('),
	write(Arity),
	write(' Arguments) ***'),
	nl,
	show_answer(Arity),
	fail.

show_answer.

% show_answer(+Arity):

show_answer(0) :-
	!,
	show_boolean_answer.

show_answer(Arity) :-
	Arity > 0,
	prog(ordered_pred(answer, Arity)),
	!,
	show_ordered_answer(Arity).

show_answer(Arity) :-
	Arity > 0,
	show_unordered_answer(Arity).

% show_ordered_answer(+Arity):

show_ordered_answer(Arity) :-
	show_ordered_answer(1, Arity).

% show_ordered_answer(+RowNumber, +Arity):

show_ordered_answer(RowNumber, Arity) :-
	functor(Fact, answer, Arity),
	derived_with_pos(Fact, RowNumber, _, _, _),
	write('\t'),
	write(RowNumber),
	write('. '),
	show_answer_fact(Fact, Arity),
	NextRowNumber is RowNumber + 1,
	show_ordered_answer(NextRowNumber, Arity).

show_ordered_answer(_, _).

% show_unordered_answer(+Arity):

show_unordered_answer(Arity) :-
	functor(Fact, answer, Arity),
	derived(Fact, _, _),
	write('\t'),
	show_answer_fact(Fact, Arity),
	fail.

show_unordered_answer.

%------------------------------------------------------------------------------
% show_answer_fact(+Fact, +Arity):
%------------------------------------------------------------------------------

show_answer_fact(Fact, Arity) :-
	Fact =.. [answer|Args],
	show_answer_args(1, Arity, Args),
	nl.

% show_answer_args(+ArgNo, +Arity, +ArgList):

show_answer_args(_, _, []).

show_answer_args(ArgNo, Arity, [Arg|Args]) :-
	arg_delim(ArgNo),
	show_answer_arg(ArgNo, Arity, Arg),
	NextArgNo is ArgNo + 1,
	show_answer_args(NextArgNo, Arity, Args).

% show_answer_arg(ArgNo, Arity, Arg):

show_answer_arg(ArgNo, Arity, Arg) :-
	show_arg_name(ArgNo, Arity),
	write(' = '),
	show_arg(Arg).

% show_arg_name(+ArgNo, +Arity):

show_arg_name(ArgNo, Arity) :-
	prog(lit(RuleNo, 0, answer, Arity)),
	prog(arg(RuleNo, 0, ArgNo, var, Var)),
	!,
	write(Var).

show_arg_name(ArgNo, _Arity) :-
	write('Col_'),
	write(ArgNo).

% arg_delim(+ArgNo):

arg_delim(1) :-
	!.
	% First argument needs no comma in front

arg_delim(ArgNo) :-
	ArgNo > 1,
	write(', ').

%------------------------------------------------------------------------------
% show_boolean_answer:
%------------------------------------------------------------------------------

show_boolean_answer :-
	derived(answer, _, _),
	!,
	write('\t'),
	write('yes.'),
	nl.

show_boolean_answer :-
	\+ derived(answer, _, _),
	write('\t'),
	write('no.'),
	nl.

%==============================================================================
% Print Welcome and Short Manual:
%==============================================================================

:-	nl,
	write('Welcome to the Evaluator for Datalog with Ordered Predicates'),
	nl,
	write('    See http://www.informatik.uni-halle.de/~brass/order/'),
	nl,
	nl,
	write('Call odl(File) or odl(File,Options) to start the program, '),
	nl,
	write('    e.g. odl(\'ex.odl\',\'ifsd\').'),
	nl,
	nl,
	show_option_list,
	nl,
	write('If you find bugs, please contact '),
	write('brass@informatik.uni-halle.de'),
	nl,
	write('This program is still under development. '),
	write('This is version 0.1f [May 20, 2012]. '),
	nl,
	nl.
