% Prolog program til: 
%
%  - indlæsning og syntakscheck af simple engelske sætninger: {translate(_)}
%  - transformation til logisk prædikat, og
%  - transformation til Prolog clauses {clausal_form(_)}
%
%    Eksempel på acceptabel sætning: every man that lives likes a woman
%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Definér operatorprioriteter
:- op(400,xfy,&).
:- op(700,xfy,->).
:- op(200, fx,~).
:- op(400,xfy,#).
:- op(700,xfy,<->).


% SYNTAKS-Check:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

sentence(P) -->
	noun_phrase(X,P1,P), verb_phrase(X,P1).

noun_phrase(X,P1,P) -->
	determiner(X,P2,P1,P),
	noun(X,P3),
	rel_clause(X,P3,P2).
noun_phrase(X,P,P) --> proper_noun(X).

verb_phrase(X,P) --> trans_verb(X,Y,P1), noun_phrase(Y,P1,P).
verb_phrase(X,P) --> intrans_verb(X,P).

rel_clause(X,P1,(P1 & P2)) --> [that], verb_phrase(X,P2).
rel_clause(_,P,P) --> [].

determiner(X,P1,P2, all(X,(P1 -> P2))) --> [every].
determiner(X,P1,P2, exists(X,(P1 & P2))) --> [a].

noun(X,man(X)) --> [man].
noun(X,woman(X)) --> [woman].
noun(X,martian(X)) --> [martian].

proper_noun(john) --> [john].
proper_noun(alice) --> [alice].

trans_verb(X,Y,loves(X,Y)) --> [loves].
trans_verb(X,Y,likes(X,Y)) --> [likes].

intrans_verb(X,lives(X)) --> [lives].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% INDLÆSNING:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
read_list(L) :-
        nl, write('INPUT > '),
        read_line(CL),
        wordlist(L,CL,[]), !.

read_line(L) :-
        get0(C),
        buildlist(C,L).

buildlist(10,[]) :- !.
buildlist(C,[C|X]) :-
        get0(C2),
        buildlist(C2,X).
 
wordlist([X|Y]) --> word(X), whitespace, wordlist(Y).
wordlist([X|Y]) --> whitespace, word(X), whitespace, wordlist(Y).
wordlist([X]) --> whitespace, wordlist(X).
wordlist([X]) --> word(X).
wordlist([X]) --> word(X), whitespace.

word(W) --> charlist(X), {name(W,X)}.

charlist([X|Y]) --> chr(X), charlist(Y).
charlist([X]) --> chr(X).

chr(X) --> [X],{X>=48}.

whitespace --> whsp, whitespace.
whitespace --> whsp.

whsp --> [X], {X<48}.


translate(X) :- 
	read_list(L),
	sentence(X,L,[]),!.
translate(_) :-
	write('I don''t understand'), nl, fail.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% TRANSFORMATION TIL CLAUSAL FORM:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

clausal_form(X) :-
	translate(X),         nl,write('translated: '),write(X),nl,nl,
	implout(X,X1),           write('implout: '),write(X1),nl,nl,
	negin(X1,X2),            write('negin: '),write(X2),nl,nl,
	skolem(X2,X3,[]),        write('skolem: '),write(X3),nl,nl,
	univout(X3,X4),          write('univout: '),write(X4),nl,nl,
	conjnf(X4,X5),           write('conjnf: '),write(X5),nl,nl,
	clausify(X5,Clauses,_),  write('clausify: '),write(Clauses),nl,nl,
	pclauses(Clauses),       write('finished!!').

implout((P <-> Q), ((P1 & Q1) # (~P1 & ~Q1))) :-
	!, implout(P,P1), implout(Q,Q1).
implout((P -> Q), (~P1 # Q1)) :-
	!, implout(P,P1), implout(Q,Q1).
implout(all(X,P), all(X,P1)) :- 
	!, implout(P,P1).
implout(exists(X,P), exists(X,P1)) :- 
	!, implout(P,P1).
implout((P & Q), (P1 & Q1)) :-
	!, implout(P,P1), implout(Q,Q1).
implout((P # Q), (P1 # Q1)) :-
	!, implout(P,P1), implout(Q,Q1).
implout((~P),(~P1)) :- implout(P,P1).
implout(P,P).

negin((~P),P1) :- !, neg(P,P1).
negin(all(X,P),all(X,P1)) :- !, negin(P,P1).
negin(exists(X,P),exists(X,P1)) :- !,negin(P,P1).
negin((P & Q), (P1 & Q1))  :-
	!, negin(P,P1), negin(Q,Q1).
negin((P # Q), (P1 # Q1))  :-
	!, negin(P,P1), negin(Q,Q1).
negin(P,P).

neg((~P),P1) :- !, negin(P,P1).
neg(all(X,P),exists(X,P1)) :- !, neg(P,P1).
neg(exists(X,P),all(X,P1)) :- !, neg(P,P1).
neg((P & Q), (P1 # Q1))  :- 
	!, neg(P,P1), neg(Q,Q1).
neg((P # Q), (P1 & Q1))  :-
	!, neg(P,P1), neg(Q,Q1).
neg(P,(~P)).


skolem(all(X,P),all(X,P1),Vars) :-
	!, skolem(P,P1,[X|Vars]).
skolem(exists(X,P), P2, Vars) :-
	!,
	gensym(f,F),
	Sk =..[F|Vars],
	subst(Sk,X,P,P1),
	skolem(P1,P2,Vars).
skolem((P # Q), (P1 # Q1), Vars) :-
	!, skolem(P, P1, Vars), skolem(Q, Q1, Vars).
skolem((P & Q), (P1 & Q1), Vars) :-
	!, skolem(P, P1, Vars), skolem(Q, Q1, Vars).
skolem(P, P, _).


univout(all(_,P),P1) :- !, univout(P,P1).
univout((P & Q), (P1 & Q1)) :- 
	!, univout(P,P1), univout(Q,Q1).
univout((P # Q), (P1 # Q1)) :- 
	!, univout(P,P1), univout(Q,Q1).
univout(P,P).


conjnf((P # Q), R) :-
	!,
	conjnf(P,P1),conjnf(Q,Q1),
	conjnf1((P1 # Q1),R).
conjnf((P & Q), (P1 & Q1)) :-
	!,conjnf(P,P1), conjnf(Q,Q1).
conjnf(P,P).

conjnf1(((P & Q) # R), (P1 & Q1)) :-
	!, conjnf((P # R), P1), conjnf((Q # R), Q1).
conjnf1((P # (Q & R)), (P1 & Q1)) :-
	!, conjnf((P # Q), P1), conjnf((P # R), Q1).
conjnf1(P,P).


clausify((P & Q), C1, C2) :- 
	!, clausify(P, C1, C3), clausify(Q, C3, C2).
clausify(P, [cl(A,B)|Cs],Cs) :- 
	inclause(P, A, [], B, []),!.
clausify(_, C, C).


inclause((P # Q), A, A1, B, B1) :- 
	!, 
	inclause(P, A2, A1, B2, B1), 
	inclause(Q, A, A2, B, B2).
inclause((~P), A, A, B1, B) :-
	!, notin(P, A), putin(P, B, B1).
inclause(P, A1, A, B, B) :-
	notin(P, B), putin(P, A, A1).

notin(X, [X|_]) :- !, fail.
notin(X, [_|L]) :- !, notin(X,L).
notin(_,[]).

putin(X, [],[X]) :- !.
putin(X, [X|L], [X|L]) :- !.
putin(X, [Y|L], [Y|L1]) :- putin(X, L, L1).

pclauses([]) :- !, nl, nl.
pclauses([cl(A, B)|Cs]) :-
	pclause(A, B), nl, pclauses(Cs).

pclause(L,[]) :- !, pdisj(L), write('.').
pclause([], L) :- !, write(':- '), pconj(L), write('.').
pclause(L1,L2) :-
	pdisj(L1),
	write(' :- '), pconj(L2), write('.').

pdisj([L]) :- !, write(L).
pdisj([L|Ls]) :- write(L), write('; '), pdisj(Ls).

pconj([L]) :- !, write(L).
pconj([L|Ls]) :- write(L), write(', '), pconj(Ls).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% HJÆLPERUTINER:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%

gensym(Root,Atom) :-
	get_num(Root,Num),
	name(Root,Name1),
	integer_name(Num,Name2),
	append(Name1,Name2,Name),
	name(Atom,Name).

get_num(Root,Num) :-
	retract(current_num(Root,Num1)), !,
	Num is Num1+1,
	asserta(current_num(Root,Num)).
get_num(Root,1) :- asserta(current_num(Root,1)).

integer_name(Int,List) :- integer_name(Int,[],List).
integer_name(I,Sofar,[C|Sofar]) :-  
	I < 10, !, C is (I + 48).
integer_name(I,Sofar,List) :-
	Tophalf is I // 10,
	Bothalf is I mod 10,
	C is Bothalf + 48,
	integer_name(Tophalf,[C|Sofar],List).

subst(New,O,Old,New) :- (O==Old),!.
subst(_,_,Val,Val) :-   var(Val),!.
subst(New,Old,Val,NewVal) :- 
	var(Old),
	functor(Val,Fn,N),
	functor(NewVal,Fn,N),
	subst_args(N,New,Old,Val,NewVal).

subst_args(0,_,_,_,_) :- !.
subst_args(N,New,Old,Val,NewVal) :- 
	var(Old),
	arg(N,Val,OldArg),
	arg(N,NewVal,NewArg),
	subst(New,Old,OldArg,NewArg),
	N1 is N - 1,
	subst_args(N1,New,Old,Val,NewVal).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%