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

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


%******************************************************************************
% Input Data, Parsing, Preprocessing:
%******************************************************************************


%==============================================================================
% Input Data:
%==============================================================================


%------------------------------------------------------------------------------
% input_rule(-Rule):
%------------------------------------------------------------------------------

:- dynamic(input_rule/1).

%------------------------------------------------------------------------------
% input_constraint(-Constraint):
%------------------------------------------------------------------------------

:- dynamic(input_constraint/1).

%------------------------------------------------------------------------------
% clear_input:
%------------------------------------------------------------------------------

clear_input :-
	delete_all(input_rule, 1),
	delete_all(input_constraint, 1).

%------------------------------------------------------------------------------
% blink1:
%------------------------------------------------------------------------------

% Set input_rule and input_constraint to the data of the example "Blink1".

blink1 :-
	clear_input,
	store_blink1_rules,
	store_blink1_constraints.

store_blink1_rules :-
	blink1_rule(No, Head, Body),
	make_rule(No, Head, Body, Rule),
	assert(input_rule(Rule)),
	fail.
store_blink1_rules.

store_blink1_constraints :-
	blink1_constraint(ID, Lit1, Lit2, Formula),
	make_constraint(ID, Lit1, Lit2, Formula, Constraint),
	assert(input_constraint(Constraint)),
	fail.
store_blink1_constraints.


%------------------------------------------------------------------------------
% blink0:
%------------------------------------------------------------------------------

% Set input_rule and input_constraint to the data of the example "Blink1".

blink0 :-
	clear_input,
	store_blink0_rules,
	store_blink0_constraints.

store_blink0_rules :-
	blink0_rule(No, Head, Body),
	make_rule(No, Head, Body, Rule),
	assert(input_rule(Rule)),
	fail.
store_blink0_rules.

store_blink0_constraints :-
	blink0_constraint(ID, Lit1, Lit2, Formula),
	make_constraint(ID, Lit1, Lit2, Formula, Constraint),
	assert(input_constraint(Constraint)),
	fail.
store_blink0_constraints.


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


%------------------------------------------------------------------------------
% load(+FileName, +OptChars):
%------------------------------------------------------------------------------

load(FileName, OptChars) :-
	set_opt(OptChars),
	load(FileName).

%------------------------------------------------------------------------------
% load(+FileName):
%------------------------------------------------------------------------------

load(FileName) :-
	write('Loading input program \"'),
	write(FileName),
	write('\" ...'),
	nl,
	open_file_with_errmsg(FileName, Stream),
	idgen_init(IDGen),
	read_source_rules(Stream, IDGen),
	file_close(Stream).

%------------------------------------------------------------------------------
% open_file_with_errmsg(+FileName, -Stream):
%------------------------------------------------------------------------------

open_file_with_errmsg(FileName, Stream) :-
	file_ropen(FileName, Stream),
	!.

% Try to add extension '.mlg' to solve the problem:
open_file_with_errmsg(FileName, Stream) :-
	atom_chars(FileName, FileChars),
	atom_chars('.mlg', ExtChars),
	list_append(FileChars, ExtChars, Chars),
	atom_chars(FileWithExt, Chars),
	file_ropen(FileWithExt, Stream),
	!.

open_file_with_errmsg(FileName, _) :-
	write('Cannot open input file: \"'),
	write(FileName),
	write('\"!'),
	nl,
	fail.

%------------------------------------------------------------------------------
% read_source_rules(+Stream, +IDGen):
%------------------------------------------------------------------------------

read_source_rules(Stream, IDGen) :-
	skip_spaces(Stream),
	file_eof(Stream) -> 
		finished_reading
	;	file_lineno(Stream, FirstLine),
		read_source_rule(Stream, Chars, LastLineNo),
		!,
		show_source_rule(FirstLine, LastLineNo, Chars),
		parse(Chars, FirstLine, LastLineNo, IDGen, NextIDGen),
		read_source_rules(Stream, NextIDGen).

% finished_reading:

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

finished_reading :-
	write('Program successfully loaded.\n').

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

skip_spaces(Stream) :-
	file_peekc(Stream, Char),
	(is_space(Char) -> file_getc(Stream, Char), skip_spaces(Stream);
	is_comment(Char) -> file_getc(Stream, Char), skip_comment(Stream),
				skip_spaces(Stream);
	true).

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

skip_comment(Stream) :-
	file_getc(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) :-
	file_getc(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) :-
	file_getc(Stream, Next_Char),
	read_source_rule_str(Stream, Next_Char, Rest, LastLineNo).

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

read_source_rule_cont(Stream, Char, [Char|Rest], LastLineNo) :-
	file_getc(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) :-
	!,
	file_getc(Stream, Next_Char),
	read_source_rule_cont(Stream, Next_Char, Rest, LastLineNo).

read_source_rule_str(Stream, Char, [Char|Rest], LastLineNo) :-
	file_getc(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) :-
	!,
	file_getc(Stream, Next_Char),
	read_source_rule_cont(Stream, Next_Char, Rest, LastLineNo).

read_source_rule_comment(Stream, Char, [Char|Rest], LastLineNo) :-
	file_getc(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) :-
	file_peekc(Stream, C),
	is_space(C),
	!,
	skip_whitespace_to_nl(Stream).

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

skip_whitespace_to_nl(Stream) :-
	file_peekc(Stream, '\n'),
	!,
	file_getc(Stream, '\n').

skip_whitespace_to_nl(Stream) :-
	file_peekc(Stream, C),
	is_space(C),
	file_getc(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).

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

show_source_rule(FirstLineNo, LastLineNo, Chars) :-
	opt(show_input_chars),
	!,
	nl,
	write('Rule '),
	print_line_no(FirstLineNo, LastLineNo),
	write(':'),
	nl,
	print_chars(Chars),
	nl,
	nl.

show_source_rule(_, _, _).


%==============================================================================
% 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
% err(FirstLineNo, LastLineNo), 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.

%------------------------------------------------------------------------------
% err(-FirstLineNo, -LastLineNo): Error occurred.
%------------------------------------------------------------------------------

:- dynamic(err/2).

%------------------------------------------------------------------------------
% err_info(-FirstLineNo, -LastLineNo, -Chars):
%------------------------------------------------------------------------------

% This predicate stores information about the rule that is currently being
% parsed to be used in a possible error message.

:- dynamic(err_info/3).

%------------------------------------------------------------------------------
% clear_err:
%------------------------------------------------------------------------------

clear_err :-
	delete_all(err, 2),
	delete_all(err_info, 3).

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

store_err_info(FirstLineNo, LastLineNo, Chars) :-
	delete_all(err_info, 3),
	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),
	!,
	delete_all(err_info, 3),
	assert(err(FirstLineNo,LastLineNo)),
	nl,
	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(invalid_char_after_at(Char)) :-
	write('Invalid character \''),
	write(Char),
	write('\' after @.').

print_errmsg(missing_keyword_after_at) :-
	write('Missing keyword after @.').

print_errmsg(invalid_at_keyword(Keyword)) :-
	write('Invalid keyword \''),
	write(Keyword),
	write('\' after @.').

print_errmsg(invalid_char_after_hash(Char)) :-
	write('Invalid character \''),
	write(Char),
	write('\' after # (must be letter).').

print_errmsg(missing_const_after_hash) :-
	write('Missing constant after #.').

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

print_errmsg(expect_end(TokenList, Place)) :-
	nl,
	write('Expected end of rule '),
	write(Place),
	write(','),
	nl,
	write('    found '),
	print_found(TokenList),
	write('.').

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

print_errmsg(unknown_type(Type)) :-
	write('Unknown data type: '),
	write(Type),
	write('.').

print_errmsg(db_pred_in_head(Pred)) :-
	write('Database predicate in rule head: '),
	write(Pred),
	write('.').

print_errmsg(db_pred_already_in_head(Pred,Line)) :-
	write('DB predicate '),
	write(Pred),
	write(' already defined by rule in line '),
	write(Line),
	write('.').

print_errmsg(db_pred_already_declared(Pred,Line)) :-
	write('DB predicate '),
	write(Pred),
	write(' already declared in line '),
	write(Line),
	write('.').

print_errmsg(db_arg_name_undeclared(ArgName,Pred)) :-
	write('Argument '),
	write(ArgName),
	write(' of '),
	write(Pred),
	write('is not declared.').

print_errmsg(db_invalid_arg_no(ArgNo,Pred)) :-
	write('Argument number '),
	write(ArgNo),
	write(' of '),
	write(Pred),
	write('is invalid.').

print_errmsg(only_one_at) :-
	write('@ can only be used once per literal, '),
	write('either before or after the arguments.').

print_errmsg(invalid_at_in_constraint(At)) :-
	write('@'),
	write(At),
	write('cannot be used in constraint literals.').

print_errmsg(ret_forbidden_in_head) :-
	write('@ret cannot be used in the rule head').

print_errmsg(unknown_at_in_head(At)) :-
	write('Unknown @-keyword \''),
	write(At),
	write('\' in rule head').

print_errmsg(invalid_at_in_body(At)) :-
	write('@'),
	write(At),
	write('cannot be used in body literals.').

print_errmsg(params_only_in_head) :-
	write('The parameter marker ? can be used only in @call-literals '),
	write('in rule heads.').

print_errmsg(params_only_in_calls) :-
	write('The parameter marker ? can be used only in @call-literals.').

print_errmsg(negation_not_yet_supported) :-
	write('Negation of body literals is not yet supported.').

print_errmsg(invalid_plus_comp_op(Op)) :-
	write('Currently, only < and >= can be used with +, not '),
	print_token(comp(Op)),
	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.

%------------------------------------------------------------------------------
% expect_end(+TokenList, +Place):
%------------------------------------------------------------------------------

expect_end([], _) :-
	!.

expect_end(TokenList, Place) :-
	syntax_error(expect_end(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_token_info(Token),
	!.

print_found([Token|_]) :-
	write('invalid token: '),
	write(Token).

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


%------------------------------------------------------------------------------
% print_token_info(+Token):
%------------------------------------------------------------------------------

% Additional information about offending token in syntax error message:
%print_token_info(Keyword) :-
%	keyword(Keyword),
%	!,
%	write(' (keyword)').
%
%print_token_info(_).

%==============================================================================
% 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], [Token|Tokens]) :-
	is_lower(Char),
	!,
	tokenize_word(Char, Chars, RestChars, AtomChars),
	atom_chars(Atom, AtomChars),
	keyword_or_atom(Atom, Token),
	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], [if|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

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

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

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

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

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

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

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

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

tokenize(['@' |Chars], [at(Keyword)|Tokens]) :-
	!,
	tokenize_at(Chars, RestChars, Keyword),
	tokenize(RestChars, Tokens).

tokenize(['#' |Chars], [cconst(Const)|Tokens]) :-
	!,
	tokenize_cconst(Chars, RestChars, Const),
	tokenize(RestChars, Tokens).

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

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

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

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

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

tokenize([':', '-' |Chars], [prolog_if|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.

%------------------------------------------------------------------------------
% tokenize_at(+Chars, -RestChars, -Keyword):
%------------------------------------------------------------------------------

tokenize_at(Chars, RestChars, Keyword) :-
	tokenize_at_first(Chars, RestChars1, FirstChar),
	tokenize_at_rest(RestChars1, RestChars, MoreChars),
	atom_chars(Keyword, [FirstChar|MoreChars]),
	check_at_keyword(Keyword).

%------------------------------------------------------------------------------
% tokenize_at_first(+Chars, -RestChars, -FirstChar):
%------------------------------------------------------------------------------

tokenize_at_first([FirstChar|RestChars], RestChars, FirstChar) :-
	is_lower(FirstChar),
	!.

tokenize_at_first([FirstChar|RestChars], RestChars, FirstChar) :-
	is_upper(FirstChar),
	!.

tokenize_at_first([FirstChar|RestChars], RestChars, FirstChar) :-
	syntax_error(invalid_char_after_at(FirstChar)),
	!,
	fail.

tokenize_at_first([], [], '.') :-
	syntax_error(missing_keyword_after_at),
	fail.

%------------------------------------------------------------------------------
% tokenize_at_rest(+Chars, -RestChars, -KeywordChars):
%------------------------------------------------------------------------------

tokenize_at_rest([Char|Chars], RestChars, [Char|KeywordChars]) :-
	is_lower(Char),
	!,
	tokenize_at_rest(Chars, RestChars, KeywordChars).

tokenize_at_rest([Char|Chars], RestChars, [Char|KeywordChars]) :-
	is_upper(Char),
	!,
	tokenize_at_rest(Chars, RestChars, KeywordChars).

tokenize_at_rest(RestChars, RestChars, []).

%------------------------------------------------------------------------------
% check_at_keyword(+Keyword):
%------------------------------------------------------------------------------

check_at_keyword(Keyword) :-
	at_keyword(Keyword),
	!.

check_at_keyword(Keyword) :-
	syntax_error(invalid_at_keyword(Keyword)),
	fail.
%------------------------------------------------------------------------------
% tokenize_cconst(+Chars, -RestChars, -Const):
%------------------------------------------------------------------------------

tokenize_cconst(Chars, RestChars, Const) :-
	tokenize_cconst_first(Chars, RestChars1, FirstChar),
	tokenize_word(FirstChar, RestChars1, RestChars, ConstChars),
	atom_chars(Const, ConstChars).

%------------------------------------------------------------------------------
% tokenize_cconst_first(+Chars, -RestChars, -FirstChar):
%------------------------------------------------------------------------------

tokenize_cconst_first([FirstChar|RestChars], RestChars, FirstChar) :-
	is_lower(FirstChar),
	!.

tokenize_cconst_first([FirstChar|RestChars], RestChars, FirstChar) :-
	is_upper(FirstChar),
	!.

tokenize_cconst_first([FirstChar|RestChars], RestChars, FirstChar) :-
	syntax_error(invalid_char_after_hash(FirstChar)),
	!,
	fail.

tokenize_cconst_first([], [], '.') :-
	syntax_error(missing_const_after_hash),
	fail.

%------------------------------------------------------------------------------
% keyword_or_atom(+Atom, -Token):
%------------------------------------------------------------------------------

%keyword_or_atom(Keyword, Keyword) :-
%	keyword(Keyword),
%	!.

keyword_or_atom(Atom, atom(Atom)).

%------------------------------------------------------------------------------
% keyword(+Keyword):
%------------------------------------------------------------------------------

% List of keywords (reserved words):
%keyword(db).
%keyword(type).
%keyword(fd).

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

%------------------------------------------------------------------------------
% is_whitespace(Char)
%------------------------------------------------------------------------------

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

%------------------------------------------------------------------------------
% show_input_tokens(+FirstLine, +LastLine, +Tokens):
%------------------------------------------------------------------------------

show_input_tokens(FirstLine, LastLine, Tokens) :-
	opt(show_input_tokens),
	!,
	write('Input Tokens '),
	print_line_no(FirstLine, LastLine),
	write(':'),
	nl,
	print_token_list(Tokens),
	nl.

show_input_tokens(_, _, _).

%==============================================================================
% Main Parser Predicate:
%==============================================================================

%------------------------------------------------------------------------------
% parse(+Chars, +FirstLineNo, +LastLineNo, +IDGenIn, -IDGenOut):
%------------------------------------------------------------------------------

parse(Chars, FirstLineNo, LastLineNo, IDGenIn, IDGenOut) :-
	store_err_info(FirstLineNo, LastLineNo, Chars),
	tokenize(Chars, Tokens),
	show_input_tokens(FirstLineNo, LastLineNo, Tokens),
	parse_rule_or_cons(Tokens, IDGenIn, IDGenOut),
	!.

parse(_, _FirstLineNo, _LastLineNo, IDGen, IDGen) :-
	syntax_error(unhandled).

%==============================================================================
% 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).
%    There 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_or_cons(+Tokens, +IDGenIn, -IDGenOut)
%------------------------------------------------------------------------------

parse_rule_or_cons(Tokens, IDGenIn, IDGenOut) :-
	dbg_parser(parse_rule_or_cons, Tokens),
	expect([atom(_),if], Tokens, 'at start of rule or constraint'),
	xparse_rule_or_cons(Tokens, IDGenIn, IDGenOut).

% xparse_rule_or_cons(+Tokens, +IDGenIn, -IDGenOut):

% Constraint:
xparse_rule_or_cons([if|Tokens], IDGenIn, IDGenOut) :-
	!,
	parse_con_lit(Tokens, Lit1, Tokens1),
	expect([comma], Tokens1, 'after first literal in constraint'),
	Tokens1 = [comma|Tokens2],
	parse_con_lit(Tokens2, Lit2, Tokens3), 
	parse_opt_formula(Tokens3, Formula, Tokens4),
	expect([fullstop], Tokens4, 'after constraint literals'),
	Tokens4 = [fullstop|Tokens5],
	!,
	expect_end(Tokens5, 'after constraint'),
% TODO: Semantic Check!
	idgen_next_cid(IDGenIn, CID, IDGenOut),
	make_constraint(CID, Lit1, Lit2, Formula, Constraint),
	assert(input_constraint(Constraint)).

% Fact:
xparse_rule_or_cons(Tokens, IDGenIn, IDGenOut) :-
	parse_head_lit(Tokens, HeadLit, _At, Tokens1),
	expect([if,fullstop], Tokens1, 'after head literal'),
	Tokens1 = [fullstop|RestTokens],
	!,
	expect_end(RestTokens, 'after fact'),
% TODO: Semantic Check!
	idgen_next_rid(IDGenIn, RID, IDGenOut),
	make_rule(RID, HeadLit, [], Rule),
	assert(input_rule(Rule)).

% TODO: Duplizierung Head literal parsen besser vermeiden!

% Rule:
xparse_rule_or_cons(Tokens, IDGenIn, IDGenOut) :-
	parse_head_lit(Tokens, HeadLit, At, Tokens1),
	expect([if], Tokens1, 'after head literal'),
	Tokens1 = [if|BodyTokens],
	parse_body(BodyTokens, BodyLits, Tokens2),
	expect([fullstop], Tokens2, 'after body'),
	Tokens2 = [fullstop|RestTokens],
	expect_end(RestTokens, 'after rule'),
	gen_body(At, BodyLits, FullBody),
% TODO: Semantic Check!
	idgen_next_rid(IDGenIn, RID, IDGenOut),
	make_rule(RID, HeadLit, FullBody, Rule),
	assert(input_rule(Rule)).


%==============================================================================
% >>> Parsing Predicates for Rule Body <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_body(+Tokens, -Body, -RestTokens)
%------------------------------------------------------------------------------

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

% xparse_body(+Tokens, -Body, -RestTokens):

xparse_body(Tokens, [Lit|Body], RestTokens) :-
	parse_body_lit(Tokens, Lit, Tokens1),
	parse_body_rest(Tokens1, Body, RestTokens).

%------------------------------------------------------------------------------
% parse_body_rest(+Tokens, -Body, -RestTokens):
%------------------------------------------------------------------------------

% (begins with comma or fullstop).

parse_body_rest(Tokens, Body, RestTokens) :-
	dbg_parser(parse_body_rest, Tokens),
	expect([comma,fullstop], Tokens, 'after body literal'),
	xparse_body_rest(Tokens, Body, RestTokens).

% xparse_body_rest(+Tokens, -Body, -RestTokens):

xparse_body_rest([comma|Tokens], Body, RestTokens) :-
	!,
	parse_body(Tokens, Body, RestTokens).

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


%==============================================================================
% >>> Parsing Predicates for Literals <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_con_lit(+Tokens, -Lit, -RestTokens):
%------------------------------------------------------------------------------

% Standard literal in a constraint.
% (from predicate to rparen)

parse_con_lit(Tokens, Lit, RestTokens) :-
	dbg_parser(parse_con_lit, Tokens),
	expect([atom(_)], Tokens, 'at start of constraint literal'),
	xparse_con_lit(Tokens, Lit, RestTokens).

% xparse_con_lit(+Tokens, -Lit, -RestTokens):

xparse_con_lit([atom(Pred)|Tokens1], Lit, RestTokens) :-
	parse_opt_at(Tokens1, [lparen,comma,fullstop],
			"after predicate in constraint literal",
			At1, Tokens2),
	parse_opt_args(Tokens2, Args, Tokens3),
	parse_opt_at(Tokens3, [comma,fullstop], "after constraint literal",
			At2, RestTokens),
	only_one_at(At1, At2, At),
	gen_con_lit(Pred, At, Args, Lit).

%------------------------------------------------------------------------------
% parse_head_lit(+Tokens, -Lit, -At, -RestTokens)
%------------------------------------------------------------------------------

% (from predicate to rparen)

parse_head_lit(Tokens, Lit, At, RestTokens) :-
	dbg_parser(parse_head_lit, Tokens),
	expect([atom(_)], Tokens, 'at start of head literal'),
	xparse_head_lit(Tokens, Lit, At, RestTokens).

% xparse_head_lit(+Tokens, -Lit, -At, -RestTokens):

xparse_head_lit([atom(Pred)|Tokens1], Lit, At, RestTokens) :-
	parse_opt_at(Tokens1, [lparen,if,fullstop],
			"after predicate in head literal",
			At1, Tokens2),
	parse_opt_head_args(Tokens2, Args, NumParams, Tokens3),
	parse_opt_at(Tokens3, [if,fullstop], "after head literal",
			At2, RestTokens),
	only_one_at(At1, At2, At),
	gen_head_lit(Pred, At, Args, NumParams, Lit).

%------------------------------------------------------------------------------
% parse_opt_at(+Tokens, +Follow, +Place, -At, -RestTokens)
%------------------------------------------------------------------------------

% This can appear in the head or body of a rule,
% and in the literals of a constraint.
% Currently, it is allowed immediately after the predicate
% and alternatively after the argument list.
% To handle all these options, the caller must specify a list of tokens that
% might follow this nonterminal, and also a Place text that is printed in
% the error message if the current token is not at(_) or an element of Follow.

parse_opt_at(Tokens, Follow, Place, At, RestTokens) :-
	dbg_parser(parse_opt_at, Tokens),
	expect([at(_)|Follow], Tokens, Place),
	xparse_opt_at(Tokens, At, RestTokens).

xparse_opt_at([at(At)|Tokens], At, Tokens) :-
	!.

xparse_opt_at(Tokens, none, Tokens).

%------------------------------------------------------------------------------
% only_one_at(+At1, +At2, -At)
%------------------------------------------------------------------------------

only_one_at(none, At, At) :-
	!.

only_one_at(At, none, At) :-
	!.

only_one_at(_, At, At) :-
	syntax_error(only_one_at),
	fail.

%------------------------------------------------------------------------------
% parse_body_lit(+Tokens, -Lit, -RestTokens)
%------------------------------------------------------------------------------

% from optional negation to rparen

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

% xparse_body_lit(+Tokens, -Lit, -RestTokens):

xparse_body_lit([not|Tokens], negated(Lit), RestTokens) :-
	syntax_error(negation_not_yet_supported),
	parse_pos_body_lit(Tokens, Lit, RestTokens).

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

%------------------------------------------------------------------------------
% parse_pos_body_lit(+Tokens, -Lit, -RestTokens)
%------------------------------------------------------------------------------

% (from predicate to rparen)

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

% xparse_pos_body_lit(+Tokens, -Lit, -RestTokens):

xparse_pos_body_lit([atom(Pred)|Tokens], Lit, RestTokens) :-
	expect([at(_),lparen,comma,fullstop,comp(_)], Tokens,
		'after predicate or comparison term'),
	Tokens=[NextTok|_],
	member(NextTok, [at(_),lparen,comma,fullstop]),
	!,
	parse_opt_at(Tokens, [lparen,comma,fullstop],
			"after predicate in body literal", At1, Tokens1),
	parse_opt_args(Tokens1, Args, Tokens2),
	parse_opt_at(Tokens2, [comma,fullstop],
			"after arguments in body literal", At2, RestTokens),
	only_one_at(At1, At2, At),
	gen_body_lit(Pred, At, Args, Lit).

xparse_pos_body_lit(Tokens, Lit, RestTokens) :-
	parse_arg(Tokens, Arg1, Tokens1),
	parse_comparison_rest(Tokens1, Arg1, Lit, RestTokens).

%------------------------------------------------------------------------------
% parse_comparison_rest(+Tokens, +Arg1, -Lit, -RestTokens)
%------------------------------------------------------------------------------

parse_comparison_rest(Tokens, Arg1, Lit, RestTokens) :-
	dbg_parser(parse_comparison_rest, Tokens),
	expect([comp(_),plus], Tokens, 'after first term of comparison'),
	xparse_comparison_rest(Tokens, Arg1, Lit, RestTokens).

% xparse_comparison_rest(+Tokens, +Arg1, -Lit, -RestTokens):

xparse_comparison_rest([comp(Op)|Tokens], Arg1, Lit, RestTokens) :-
	parse_arg(Tokens, Arg2, RestTokens),
	gen_comp_lit(Op, Arg1, Arg2, Lit).

xparse_comparison_rest([plus|Tokens], Arg1, Lit, RestTokens) :-
	parse_arg(Tokens, Arg2, Tokens1),
	expect([comp(_)], Tokens1, 'after sum in comparison'),
	Tokens1 = [comp(Op)|Tokens2],
	parse_arg(Tokens2, Arg3, RestTokens),
	gen_sum_comp_lit(Op, Arg1, Arg2, Arg3, Lit).

%==============================================================================
% >>> Parsing Predicates for Argument Lists of Literals <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_opt_head_args(+Tokens, -Args, -NumParams, -RestTokens)
%------------------------------------------------------------------------------

% (from lparen to rparen) or nothing.
% NumParams is the number of ? at the end of the argument list (only in @call).

parse_opt_head_args(Tokens, Args, NumParams, RestTokens) :-
	dbg_parser(parse_opt_head_args, Tokens),
	expect([lparen,at(_),if,fullstop], Tokens, 'at head argument list'),
	xparse_opt_head_args(Tokens, Args, NumParams, RestTokens).

xparse_opt_head_args([lparen|Tokens], Args, NumParams, RestTokens) :-
	!,
	parse_args([lparen|Tokens], Args, NumParams, RestTokens).

xparse_opt_head_args(Tokens, [], 0, Tokens).

%------------------------------------------------------------------------------
% parse_args(+Tokens, -Args, -NumParams, -RestTokens)
%------------------------------------------------------------------------------

% (from lparen to rparen)

parse_args(Tokens, Args, NumParams, RestTokens) :-
	dbg_parser(parse_args, Tokens),
	expect([lparen], Tokens, 'at start of argument list'),
	xparse_head_args(Tokens, Args, NumParams, RestTokens).

xparse_head_args([lparen|Tokens], Args, NumParams, RestTokens) :-
	parse_arg_list(Tokens, Args, NumParams, Tokens1),
	Tokens1 = [rparen|RestTokens].

%------------------------------------------------------------------------------
% parse_arg_list(+Tokens, -Args, -NumParams, -RestTokens):
%------------------------------------------------------------------------------

% (starts with term - i.e. '(' was already read, ')' will be read afterwards)

parse_arg_list(Tokens, Args, NumParams, RestTokens) :-
	dbg_parser(parse_arg_list, Tokens),
	expect([var(_),atom(_),int(_),str(_),cconst(_),param], Tokens,
		'as argument'),
	xparse_arg_list(Tokens, Args, NumParams, RestTokens).

xparse_arg_list([param|RestTokens], [], NumParams, RestTokens) :-
	!,
	parse_par_list([param|RestTokens], NumParams, RestTokens).

xparse_arg_list(Tokens, [Term|Args], NumParams, RestTokens) :-
	parse_arg(Tokens, Term, Tokens1),
	parse_args_rest(Tokens1, Args, NumParams, RestTokens).

%------------------------------------------------------------------------------
% parse_args_rest(+Tokens, -Args, -NumParams, -RestTokens).
%------------------------------------------------------------------------------

% (starts with comma or rparen)

parse_args_rest(Tokens, Args, NumParams, RestTokens) :-
	dbg_parser(parse_args_rest, Tokens),
	expect([comma, rparen], Tokens, 'after argument term'),
	xparse_args_rest(Tokens, Args, NumParams, RestTokens).

xparse_args_rest([comma|Tokens], Args, NumParams, RestTokens) :-
	parse_arg_list(Tokens, Args, NumParams, RestTokens).

xparse_args_rest([rparen|Tokens], [], 0, [rparen|Tokens]).


%==============================================================================
% >>> Parsing Predicates for ? Suffix of Argument List <<<
%==============================================================================

% This is allowed only for @call literals, but this is checked later.
% When this predicate is called, it can be any head or body literal
% with an argument list in (...).

%------------------------------------------------------------------------------
% parse_par_list(+Tokens, -NumParams, -RestTokens):
%------------------------------------------------------------------------------

% Called when ? appears in argument list.

parse_par_list(Tokens, NumParams, RestTokens) :-
	dbg_parser(parse_par_list, Tokens),
	expect([param], Tokens, 'in ?-suffix of argument list'),
	xparse_par_list(Tokens, NumParams, RestTokens).

xparse_par_list([param|Tokens], NumParams1, RestTokens) :-
	!,
	parse_par_rest(Tokens, NumParams, RestTokens),
	NumParams1 is NumParams + 1.

%------------------------------------------------------------------------------
% parse_par_rest(+Tokens, -NumParams, -RestTokens):
%------------------------------------------------------------------------------

% Called after ? in argument list

parse_par_rest(Tokens, NumParams, RestTokens) :-
	dbg_parser(parse_par_rest, Tokens),
	expect([comma,rparen], Tokens, 'after ? in argument list'),
	xparse_par_rest(Tokens, NumParams, RestTokens).

xparse_par_rest([comma|Tokens], NumParams, RestTokens) :-
	!,
	parse_par_list(Tokens, NumParams, RestTokens).

xparse_par_rest([rparen|Tokens], 0, [rparen|Tokens]).


%==============================================================================
% >>> Parsing Predicates for Argument List of Body Literals <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_opt_args(+Tokens, -Args, -RestTokens)
%------------------------------------------------------------------------------

% (from lparen to rparen) or nothing.

parse_opt_args(Tokens, Args, RestTokens) :-
	dbg_parser(parse_opt_args, Tokens),
	expect([lparen,comma,fullstop], Tokens, 'at argument list'),
	xparse_opt_args(Tokens, Args, RestTokens).

xparse_opt_args([lparen|Tokens], Args, RestTokens) :-
	!,
	parse_args([lparen|Tokens], Args, NumParams, RestTokens),
	check_params_only_in_head(NumParams).

xparse_opt_args(Tokens, [], Tokens).

%------------------------------------------------------------------------------
% check_params_only_in_head(+NumParams)
%------------------------------------------------------------------------------

check_params_only_in_head(0) :-
	!.

check_params_only_in_head(_) :-
	syntax_error(params_only_in_head).


%==============================================================================
% >>> Parsing Predicates for Single Argument (Term) - Used in Head and Body <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_arg(+Tokens, -Term, -RestTokens):
%------------------------------------------------------------------------------

parse_arg(Tokens, Term, RestTokens) :-
	dbg_parser(parse_arg, Tokens),
	expect([var(_),atom(_),int(_),str(_),cconst(_)], Tokens, 'as argument'),
	xparse_arg(Tokens, Term, RestTokens).

% xparse_arg(+Tokens, -Term, -RestTokens):

xparse_arg([atom(Atom)|Tokens], Atom, Tokens).

xparse_arg([int(Int)|Tokens], Int, Tokens).

xparse_arg([str(Str)|Tokens], str(Str), Tokens).

xparse_arg([cconst(Const)|Tokens], cconst(Const), Tokens).

xparse_arg([var(Var)|Tokens], v(Var), Tokens).


%==============================================================================
% >>> Parsing Predicates for Additional Formula in Constraints <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_opt_formula(+Tokens, -Formula, -RestTokens):
%------------------------------------------------------------------------------

% Currently, only disjunctions of disequalities are accepted (as in the paper).

parse_opt_formula(Tokens, Formula, RestTokens) :-
	dbg_parser(parse_opt_formula, Tokens),
	expect([comma,fullstop], Tokens, 'after literals in constraint'),
	xparse_opt_formula(Tokens, Formula, RestTokens).

xparse_opt_formula([comma|Tokens], Formula, RestTokens) :-
	!,
	parse_formula(Tokens, Formula, RestTokens).

xparse_opt_formula(Tokens, true, Tokens).


%------------------------------------------------------------------------------
% parse_formula(+Tokens, -Formula, -RestTokens):
%------------------------------------------------------------------------------

parse_formula(Tokens, Formula, RestTokens) :-
	dbg_parser(parse_formula, Tokens),
	expect([lparen,var(_),atom(_),int(_),str(_),cconst(_)], Tokens,
		'at start of constraint formula'),
	xparse_formula(Tokens, Formula, RestTokens).

xparse_formula([lparen|Tokens], Formula, RestTokens) :-
	!,
	parse_formula_disj(Tokens, Formula, Tokens1),
	expect([rparen], Tokens1, 'at end of parenthesized formula'),
	Tokens1 = [rparen|RestTokens].

xparse_formula(Tokens, Formula, RestTokens) :-
	parse_formula_atomic(Tokens, Formula, RestTokens).

%------------------------------------------------------------------------------
% parse_formula_disj(+Tokens, -Formula, -RestTokens):
%------------------------------------------------------------------------------

parse_formula_disj(Tokens, Formula, RestTokens) :-
	dbg_parser(parse_formula_disj, Tokens),
	expect([lparen,var(_),atom(_),int(_),str(_),cconst(_)], Tokens,
		'in constraint formula'),
	xparse_formula_disj(Tokens, Formula, RestTokens).

xparse_formula_disj([lparen|Tokens], Formula, RestTokens) :-
	!,
	parse_formula_disj(Tokens, Formula, Tokens1),
	expect([rparen], Tokens1, 'at end of parenthesized formula'),
	Tokens1 = [rparen|RestTokens].

xparse_formula_disj(Tokens, Formula, RestTokens) :-
	parse_formula_atomic(Tokens, Formula1, Tokens1),
	parse_formula_disj_rest(Tokens1, Formula1, Formula, RestTokens).

%------------------------------------------------------------------------------
% parse_formula_disj_rest(+Tokens, +LeftFormula, -Formula, -RestTokens):
%------------------------------------------------------------------------------

parse_formula_disj_rest(Tokens, LeftFormula, Formula, RestTokens) :-
	dbg_parser(parse_formula_disj_rest, Tokens),
	expect([or,rparen], Tokens, 'in constraint formula (disjunction)'),
	xparse_formula_disj_rest(Tokens, LeftFormula, Formula, RestTokens).

xparse_formula_disj_rest([or|Tokens], LeftFormula, Formula, RestTokens) :-
	!,
	parse_formula_disj(Tokens, RightFormula, RestTokens),
	Formula = or(LeftFormula,RightFormula).

xparse_formula_disj_rest(Tokens, Formula, Formula, Tokens).

%------------------------------------------------------------------------------
% parse_formula_atomic(+Tokens, -Formula, -RestTokens):
%------------------------------------------------------------------------------

parse_formula_atomic(Tokens, Formula, RestTokens) :-
	dbg_parser(parse_formula_atomic, Tokens),
	expect([var(_),atom(_),int(_),str(_),cconst(_)], Tokens,
		'at start of atomic constraint formula'),
	xparse_formula_atomic(Tokens, Formula, RestTokens).

xparse_formula_atomic(Tokens, Formula, RestTokens) :-
	!,
	parse_arg(Tokens, Term1, Tokens1),
	expect([comp(_)], Tokens1, 'in atomic constraint formula'),
	Tokens1 = [comp(Op)|Tokens2],
	parse_arg(Tokens2, Term2, RestTokens),
	gen_comp_lit(Op, Term1, Term2, Formula).


%==============================================================================
% Debug Output for Parser:
%==============================================================================


%------------------------------------------------------------------------------
% dbg_parser(+Pred, +Tokens):
%------------------------------------------------------------------------------

dbg_parser(Pred, Tokens) :-
	opt(dbg_out_parser),
	!,
	print_dbg_out_parser(Pred, Tokens).

dbg_parser(_, _).

%------------------------------------------------------------------------------
% print_dbg_out_parser(+Pred, +Tokens):
%------------------------------------------------------------------------------

print_dbg_out_parser(Pred, Tokens) :-
	write('\tParser: '),
	print_dbg_out_parser_pred(Pred),
	write(' '),
	print_dbg_out_parser_tokens(Tokens),
	nl.

%------------------------------------------------------------------------------
% print_dbg_out_parser_pred(+Pred):
%------------------------------------------------------------------------------

% To print parser predicate and token in columns, add spaces to width 20+1:

print_dbg_out_parser_pred(Pred) :-
	write(Pred),
	write(':'),
	atom_chars(Pred, PredChars),
	list_length(PredChars, Length),
	Spaces is 20 - Length,
	print_spaces(Spaces).

%------------------------------------------------------------------------------
% print_spaces(+NumSpaces):
%------------------------------------------------------------------------------

print_spaces(0) :-
	!.

print_spaces(N) :-
	N > 0,
	write(' '),
	NextN is N - 1,
	print_spaces(NextN).

%------------------------------------------------------------------------------
% print_dbg_out_parser_tokens(+Pred, +Tokens):
%------------------------------------------------------------------------------

print_dbg_out_parser_tokens([]) :-
	write('end of statement').

print_dbg_out_parser_tokens([Token|Rest]) :-
	print_token(Token),
	list_length(Rest, Length),
	write('   [+ '),
	write(Length),
	write(' more tokens]').

%==============================================================================
% Semantic Check:
%==============================================================================

%------------------------------------------------------------------------------
% gen_con_lit(+Pred, +At, +Args, -Lit):
%------------------------------------------------------------------------------

gen_con_lit(Pred, none, Args, Lit) :-
	!,
	Lit =.. [Pred,v('T')|Args].

gen_con_lit(Pred, call, Args, Lit) :-
	gen_call_pred(Pred, CallPred),
	!,
	Lit =.. [CallPred,v('T')|Args].

gen_con_lit(Pred, ret, Args, Lit) :-
	gen_ret_pred(Pred, RetPred),
	!,
	Lit =.. [RetPred,v('T')|Args].

gen_con_lit(_Pred, At, _Args, error) :-
	syntax_error(invalid_at_in_constraint(At)),
	fail.

%------------------------------------------------------------------------------
% gen_comp_lit(+Op, +Term1, +Term2, -Lit):
%------------------------------------------------------------------------------

gen_comp_lit(Op, Term1, Term2, Lit) :-
	Lit =.. [Op, Term1, Term2].

%------------------------------------------------------------------------------
% gen_sum_comp_lit(Op, Arg1, Arg2, Arg3, Lit):
%------------------------------------------------------------------------------

gen_sum_comp_lit(lt, Arg1, Arg2, Arg3, plus_lt(Arg1,Arg2,Arg3)) :-
	!,
	is_term(Arg1),
	is_term(Arg2),
	is_term(Arg3).

gen_sum_comp_lit(ge, Arg1, Arg2, Arg3, plus_ge(Arg1,Arg2,Arg3)) :-
	!,
	is_term(Arg1),
	is_term(Arg2),
	is_term(Arg3).

gen_sum_comp_lit(Op, _Arg1, _Arg2, _Arg3, error) :-
	syntax_error(invalid_plus_comp_op(Op)),
	fail.

%------------------------------------------------------------------------------
% gen_head_lit(+Pred, +At, +Args, +NumParams, -Lit):
%------------------------------------------------------------------------------

gen_head_lit(Pred, none, Args, NumParams, Lit) :-
	!,
	check_no_params(NumParams),
	Lit =.. [Pred,v('T')|Args].

gen_head_lit(Pred, next, Args, NumParams, Lit) :-
	!,
	check_no_params(NumParams),
	Lit =.. [Pred,v('S')|Args].

gen_head_lit(Pred, init, Args, NumParams, Lit) :-
	!,
	check_no_params(NumParams),
	Lit =.. [Pred,0|Args].

gen_head_lit(Pred, start, Args, NumParams, Lit) :-
	!,
	check_no_params(NumParams),
	Lit =.. [Pred,1|Args].

gen_head_lit(Pred, call, Args, _NumParams, Lit) :-
	gen_call_pred(Pred, CallPred),
	!,
	Lit =.. [CallPred,v('T')|Args].

gen_head_lit(Pred, setup, Args, _NumParams, Lit) :-
	gen_call_pred(Pred, CallPred),
	!,
	Lit =.. [CallPred,0|Args].

gen_head_lit(_Pred, ret, _Args, _NumParams, error) :-
	!,
	syntax_error(ret_forbidden_in_head),
	fail.

gen_head_lit(_Pred, At, _Args, _NumParams, error) :-
	syntax_error(unknown_at_in_head(At)),
	fail.

%------------------------------------------------------------------------------
% check_no_params(+NumArgs):
%------------------------------------------------------------------------------

check_no_params(0) :-
	!.

check_no_params(_) :-
	syntax_error(params_only_in_calls).

%------------------------------------------------------------------------------
% gen_body_lit(+Pred, +At, +Args, -Lit):
%------------------------------------------------------------------------------

gen_body_lit(Pred, none, Args, Lit) :-
	!,
	Lit =.. [Pred,v('T')|Args].

gen_body_lit(Pred, ret, Args, Lit) :-
	gen_ret_pred(Pred, RetPred),
	!,
	Lit =.. [RetPred,v('T')|Args].

gen_body_lit(_Pred, At, _Args, error) :-
	syntax_error(invalid_at_in_body(At)),
	fail.

%------------------------------------------------------------------------------
% gen_call_pred(+Pred, -CallPred):
%------------------------------------------------------------------------------

gen_call_pred(Pred, CallPred) :-
	atom_chars('call_', PrefixChars),
	atom_chars(Pred, PredChars),
	list_append(PrefixChars, PredChars, Chars),
	atom_chars(CallPred, Chars).

%------------------------------------------------------------------------------
% gen_ret_pred(+Pred, -RetPred):
%------------------------------------------------------------------------------

gen_ret_pred(Pred, RetPred) :-
	atom_chars('ret_', PrefixChars),
	atom_chars(Pred, PredChars),
	list_append(PrefixChars, PredChars, Chars),
	atom_chars(RetPred, Chars).

%------------------------------------------------------------------------------
% gen_body(+At, +BodyLits, -FullBody):
%------------------------------------------------------------------------------

% This adds the succ-Literal to the body for @next rules:

gen_body(next, BodyLits, FullBody) :-
	!,
	list_append(BodyLits, [succ(v('T'),v('S'))], FullBody).

gen_body(_, BodyLits, BodyLits).
