%%%% Propositional Dynamic Logic in -*-Prolog-*-

%%% REPL
parse(E) :- scan(Tokens), !, expr(E, Tokens, [eol]).
pdl :- parse(E) -> eval(E, X), write(' => '), write(X), nl, pdl.

%%% Semantics

% Set union & intersection.
cup(S1, S2, S) :- setof(X, (member(X, S1); member(X, S2)), S).
cap([], _, []).
cap(_, [], []).
cap(S1, S2, S) :- setof(X, (member(X, S1), member(X, S2)), S).
bigcup(Ss, U) :- bigcup(Ss, U, []).
bigcup([], U, U).
bigcup([S|Ss], U, Acc) :- cup(S, Acc, X), bigcup(Ss, U, X).

% PDL semantics: based on Kripke semantics for modal logic.
eval(0, []).
eval(P, W) :- prop(P), setof(X, m(P, X), W).
eval(eq(P,Q), W) :- eval(P, X), eval(Q, Y), (X=Y -> k(W) ; W=[]).
eval(not(P), W) :-
	k(K), eval(P, X),
	(setof(Z, (member(Z, K), \+member(Z, X)), W) -> true ; W=[]).
eval(or(P,Q), W) :- eval(P, X), eval(Q, Y),  cup(X, Y, W).
eval(and(P,Q), W) :- eval(P, X), eval(Q, Y),  cap(X, Y, W).
eval(imply(P,Q), W) :- eval(or(not(P),Q), W).

eval(A, W) :- prog(A), setof([X|Y], m(A, [X|Y]), W).
eval(nec(A,P), W) :- eval(not(pos(A,not(P))),W).
eval(pos(A,P), W) :-
	k(K), eval(A, X), eval(P, Y),
	(setof(U, V^(member(V, K), member([U|V], X), member(V, Y)), W)
	 -> true ; W=[]).
eval(seq(A,B), W) :-
	k(K), eval(A, X), eval(B, Y),
	setof([U|V], Z^(member(Z, K), member([U|Z], X), member([Z|V], Y)), W).
eval(choice(A,B), W) :- eval(A, X), eval(B, Y), cup(X, Y, W).
eval(test(P), W) :- setof([X|X], Z^(eval(P, Z), member(X, Z)), W).
eval(star(A), W) :- setof(X, closure(A, X, []), Y), bigcup(Y, W).

% Reflexive transitive closure with loop detection.
closure(_, W, _) :- k(K), setof([V|V], member(V, K), W).
closure(A, W, _) :- eval(A, W).
closure(A, W, Seen) :-
	eval(seq(A,A), X), \+member(X, Seen), closure(seq(A,A), W, [X|Seen]).

%%% Syntax

expr(E) --> formula(E).
expr(eq(P,Q)) --> formula(P), ['='], formula(Q).
expr(E) --> program(E).

formula(F) --> prop(T),  rest_formula(T, F).
rest_formula(X, X) --> [].
rest_formula(X, F) --> ['&'], prop(Y), rest_formula(and(X,Y), F).
rest_formula(X, F) --> ['+'], prop(Y), rest_formula(or(X,Y), F).
rest_formula(X, F) --> ['-', '>'], prop(Y), rest_formula(imply(X,Y), F).

prop(P) --> [P], {prop(P)}.
prop(nec(A,P)) --> ['['], program(A), [']'], formula(P).
prop(pos(A,P)) --> ['<'], program(A), ['>'], formula(P).
prop(not(P)) --> ['-'], formula(P).
prop(P) --> ['('], formula(P), [')'].

program(A) --> sequence(X), rest_program(X, A).
program(A) --> prop(P), ['?'], rest_program(test(P), A).
rest_program(X, X) --> [].
rest_program(X, A) --> ['|'], sequence(Y), rest_program(choice(X,Y), A).

sequence(A) --> stmt(S), rest_sequence(S, A).
rest_sequence(X, X) --> [].
rest_sequence(X, A) --> [';'], stmt(Y), rest_sequence(seq(X,Y), A).
rest_sequence(X, A) --> stmt(Y), rest_sequence(seq(X,Y), A).

stmt(S) --> atomic_prog(X), rest_stmt(X, S).
rest_stmt(X, X) --> [].
rest_stmt(X, S) --> ['*'], rest_stmt(star(X), S).

atomic_prog(T) --> [T], {prog(T)}.
atomic_prog(T) --> ['('], program(T), [')'].

%%% Lexer

scan([Token|Rest]) :-
	get_char(Char),
	get_token(Char, Token, NextChar), !,
	scan_rest(Token, NextChar, Rest).
scan_rest(eol, _, []).
scan_rest(_, Char, [Token|Rest]) :-
	get_token(Char, Token, NextChar), !,
	scan_rest(Token, NextChar, Rest).

% char_range(+Char, +Start, +End).
char_range(Char, Start, End) :-
	atom(Char), atom_length(Char, 1),
	char_code(Char, Code),
	char_code(Start, StartCode),
	char_code(End, EndCode),
	Code >= StartCode, Code =< EndCode.

digit(Char) :- char_range(Char, '0', '9').
upper(Char) :- char_range(Char, 'A', 'Z').
lower(Char) :- char_range(Char, 'a', 'z').
alpha(Char) :- upper(Char) ; lower(Char).
alnum(Char) :- alpha(Char) ; digit(Char).
whitespace(Char) :- Char = ' ' ; Char = '\t' ; Char = '\n'.

prop(0).
prop(X) :- char_range(X, 'p', 't').	% atomic propositions
prog(X) :- char_range(X, 'a', 'o').	% atomic programs
world(X) :- char_range(X, 'u', 'z').	% worlds

% Characters recognized as tokens & parts of multi-character tokens.
token(';').		% composition
token('|').		% choice
token('*').		% iteration
token('?').		% test
token('-').		% logical negation, implication ("->")
token('&').		% logical and
token('+').		% logical or
token('=').		% logical equivalence
token('['). token(']').	% necessity
token('<'). token('>').	% possibility
token('('). token(')').	% grouping

% get_token(+Lookahead, -Token, -NextChar).
get_token('\n', eol, _).			% end-of-line
get_token(Lookahead, Token, NextChar) :-	% ignore whitespace
	whitespace(Lookahead),
	get_char(Char),
	get_token(Char, Token, NextChar).
get_token('0', 0, NextChar) :-			% falsity
	get_char(NextChar).
get_token(Lookahead, Lookahead, NextChar) :-	% atomic proposition or program
	alpha(Lookahead),
	get_char(NextChar).
get_token(Lookahead, Lookahead, NextChar) :-	% other token
	token(Lookahead),
	get_char(NextChar).