% ----------------------------------
% Skolem Euler Machine -- Jos De Roo
% ----------------------------------

:- op(1200,xfx,':=').
:- op(1199,xfx,'=>').

:- dynamic(pfx/2).
:- dynamic(flag/1).
:- dynamic(brake/0).
:- dynamic(limit/1).
:- dynamic(scope/1).
:- dynamic(graph/1).
:- dynamic(tuple/2).
:- dynamic(fact/1).
:- dynamic(bset/0).
:- dynamic(bcnd/2).
:- dynamic(bref/2).
:- dynamic(bvar/1).
:- dynamic(bgot/3).
:- dynamic(fset/0).
:- dynamic(fm/1).
:- dynamic(fs/1).
:- dynamic(pi/3).
:- dynamic(tabs/1).
:- dynamic(goal/0).
:- dynamic(false/1).
:- dynamic(steps/3).
:- dynamic(answers/2).
:- dynamic('e:tactic'/2).

:- set_prolog_flag(float_format,'%.15g').
:- use_module(library(lists)).
:- use_module(library(regexp)).
:- use_module(library(charsio)).
:- use_module(library(system)).

main :-
	write('#Processed by $Id: sem.yap 2706 2009-02-27 12:34:50Z josd $ '),
	consult(user), nl,
	(flag(keywords) -> write('@keywords is, of, a.'), nl, nl; nl),
	forall(pfx(A,B), (write('@prefix '), write(A), write(' '), write(B), write('.\n'))),
	(pfx('e:',_) -> true; write('@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.\n')),
	(pfx('r:',_) -> true; write('@prefix r: <http://www.w3.org/2000/10/swap/reason#>.\n')), nl,
	catch(sem(0),Exc,(write('#'), write(Exc), nl, fail)),
	write('#ENDS '), statistics(cputime,[_,T]), Z is T, write(Z), write(' msec\n\n').

sem(Scp) :-
	(Src := Prem => Conc),
	\+'e:tactic'(lf('log:implies'(lf(Prem),lf(Conc))),_), nonvar(Prem),
	Prem, \+Conc,									% ----- euler path detection -----
	ground(Conc), Conc \= (_;_), Conc \= goal, Conc \= false,
	astep(Src,Prem,Conc), retract(brake), fail
	; brake, (limit(N), Scp < N, Sc is Scp+1, assert(scope(Sc)), sem(Sc); w3(trunk), sem([],0,[],[]); true), !
	; assert(brake), sem(Scp).

% ----- Coherent Logic inspired by http://www.cs.vu.nl/~diem/research/ht/CL.pl -----
sem(Grd,Pnum,Stack,Env) :-
	(Src := Prem => Conc),
	(\+'e:tactic'(lf('log:implies'(lf(Prem),lf(Conc))),_) -> Gnew = Grd;
	'e:tactic'(lf('log:implies'(lf(Prem),lf(Conc))),[Grd,Gnew])), nonvar(Prem),
	Prem, \+Conc,									% ----- euler path detection -----
	(Conc \= false; \+false(lf(Prem))),
	(Conc = false -> C = false(lf(Prem)); C = Conc),
	((C = goal; C = false(_), flag(quick)) -> end(C,Env)
	; (C = (E;D) -> split(Src,Prem,Gnew,Pnum,[D|Stack],E,Env); memo(Src,Prem,Gnew,Pnum,Stack,C,Env))).

split(Src,Prem,Grd,Pnum,[T|Stack],C,Env) :-
	memo(Src,Prem,Grd,Pnum,[T|Stack],C,[C|Env]),
	(T = (E;D) -> split(Src,Prem,Grd,Pnum,[D|Stack],E,Env); memo(Src,Prem,Grd,Pnum,Stack,T,[T|Env])).

memo(Src,Prem,Grd,Pnum,Stack,Conc,Env) :-
	(Conc = answer('log:implies'(_,_)) -> Q = all; Q = sk), numbervars(Conc,Pnum,Pnew,Q),
	astep(Src,Prem,Conc), (sem(Grd,Pnew,Stack,Env) -> true; end(countermodel,Env)), dstep(Src,Prem,Conc).

astep(A,B,C) :-
	C = (D,E) -> assert(D), assert(steps(A,B,D)), astep(A,B,E); assert(C), assert(steps(A,B,C)).

dstep(A,B,C) :-
	C = (D,E) -> retract(D), retract(steps(A,B,D)), dstep(A,B,E); retract(C), retract(steps(A,B,C)).

ancestor(A,B) :-
	steps(_,C,B), cmember(D,C), (unif(A,D); ancestor(A,D)).

decendent(A,B) :-
	steps(_,C,A), cmember(D,C), (unif(B,D); decendent(D,B)).

cgives(A,B) :-
	\+steps(_,_,B), !; steps(_,C,B), \+((cmember(D,C), cmember(E,A), (unif(E,D); \+cgives(E,D)))).

end(goal,Env) :-
	\+false(_), !,
	(Env = [] -> w3(trunk); write('[ e:possibleModel '), clist(Env,G), wt(lf(G)), nl,
	write('; r:gives {'), nl, retractall(answers(_,branch)), w3(branch), write('}].'), nl, nl).
end(countermodel,Env) :-
	\+false(_), !,
	write('[ e:counterModel '), clist(Env,G), wt(lf(G)), write('].'), nl, nl.
end(_,Env) :-
	write('[ e:falseModel '), clist(Env,G), wt(lf(G)), nl, (false(lf(F)),
	write('; e:because [ e:integrityConstraint '), write('{'), wt(lf(F)), write(' => false}'),
	(flag(quiet) -> true; (cmember(A,F), nl,
	write('  ; e:selected [ e:triple '), wt(lf(A)), nl,
	findall(X,(ancestor(X,A), X \= true, X \= atom(_), \+unif(X,_=.._)),L), clist(L,U),
	findall(X,(decendent(X,A), X \= false(_), X \= answer(_)),M), clist(M,V),
	findall(X,(false(lf(Y)), cmember(X,Y)),I), remove_duplicates(I,P), clist(P,Q),
	findall(X,(cmember(X,U), cmember(Y,Q), unif(X,Y)),J), clist(J,R),
	write('    ; e:falseAncestors '), wt(lf(R)), nl,
	findall(X,(cmember(X,V), cmember(Y,Q), unif(X,Y)),K), clist(K,S),
	write('    ; e:falseDecendents '), wt(lf(S)), nl,
	(flag(think) -> findall(X,(steps(_,_,X), X \= false(_), X \= answer(_), \+unif(X,A), cgives(A,X)),N), clist(N,W),
	write('    ; e:consistentGives '), wt(lf(W)), nl; true),
	write('    ]'), fail; true)), nl, write('  ]'), nl, fail; true),
	write('; r:gives {'), nl, retractall(answers(_,branch)), w3(branch), write('}].'), nl, nl.


% ------------
% proof output
% ------------

w3(U) :-
	flag(nope), !,
	(steps(_,_,answer(C)), \+answers(C,_), assert(answers(C,U)), wn(C), fail; nl).
w3(U) :-
	steps(A,B,answer(C)), \+answers(C,_), assert(answers(C,U)), redent,
	write('[ a r:Proof, r:Conjunction;'), indent, ws,
	wc(A,B,C), write('r:gives {'), indent, ws, wt(C), write('.'), write('}].'), nl, nl, fail; true.

wc(A,B,(C,D)) :- !,
	write('r:component '), wi(A,B,C), write(';'), ws, wc(A,B,D).
wc(A,B,C) :-
	write('r:component '), wi(A,B,C), write(';'), ws.

wi(A,true,C) :- !,
	write('[ a r:Extraction; r:gives {'), numbervars((A,C),0,_,var), wt(C),
	write('}; r:because [ a r:Parsing; r:source '), wt(A), write(']]').
wi(A,B,C) :-
	write('[ a r:Inference; r:gives {'), numbervars((A,B,C),0,_,var), wt(C),
	write('}; r:evidence ('), indent, wr(B), write(');'), ws, dedent,
	write('r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source '), wt(A), write(']]]'), fail; true.

wr(varpred(S,P,O)) :- !,
	U =.. [P,S,O], wr(U).
wr((atom(_),_)) :- !.
wr((X,Y)) :- !,
	wr(X), wr(Y).
wr('='(X,Y)) :- !,
	ws, write('[ a r:Fact; r:gives '), wt(lf('='(X,Y))), write(']').
wr(Z) :-
	steps(X,Y,Z), !, ws, wi(X,Y,Z).
wr(Y) :-
	auri(Y,Z), ws, write('[ a r:Fact; r:gives '), numbervars(Z,0,_,var), wt(lf(Z)), write(']').

wt(X) :-
	number(X), !, write(X).
wt((X,Y)) :- !,
	wt(X), write('. '), wt(Y).
wt([]) :- !,
	write('()').
wt([X|Y]) :- !,
	write('('), wt(X), wl(Y), write(')').
wt(X) :-
	functor(X,_,A), (A = 0, !, wt0(X); A = 1, !, wt1(X); A = 2, !, wt2(X); wtn(X)).

wt0(empty) :- !.
wt0(a) :- !,
	write(':a').
wt0('rdf:type') :- !,
	write('a').
wt0('owl:sameAs') :- !,
	write('=').
wt0('log:implies') :- !,
	write('=>').
wt0(X) :-
	atom_concat('var:',Y,X), !, write('_:'), write(Y).
wt0(X) :-
	fact(curi(X,Y)) -> write(Y); write(X).

wt1(sk(X)) :- !,
	write('_:sk'), write(X).
wt1(all(X)) :- !,
	write('?U'), write(X).
wt1(var(X)) :- !,
	write('var:x'), write(X).
wt1(lf(true)) :- !,
	write('{}').
wt1(lf(X)) :- !,
	write('{'), wt(X), write('}').
wt1(X) :-
	X =.. [B|C], write('_: '), wt0(B), write(' '), wt(C).

wt2(fpath(X,Y)) :- !,
	wt(X), write('!'), wt(Y).
wt2(bpath(X,Y)) :- !,
	wt(X), write('^'), wt(Y).
wt2(tlit(X,Y)) :- !,
	wt(X), write('^^'), wt(Y).
wt2(plit(X,Y)) :- !,
	wt(X), write('@'), wt(Y).
wt2('e:biconditional'([X|Y],Z)) :-
	flag(tquery), !, write('{'), wb(Y), write('_: e:true '), wt(Z), write('} => '), wt(X).
wt2('e:conditional'([X|Y],Z)) :-
	flag(tquery), !, write('{'), wb(Y), write('_: e:true '), wt(Z), write('} => '), wt(X).
wt2(X) :-
	X =.. [P,S,O], wt(S), write(' '), wt0(P), write(' '), wt(O).

wtn(varpred(S,P,O)) :- !,
	wt(S), write(' '), wt(P), write(' '), wt(O).
wtn(X) :-
	X =.. [B|C], write('_: '), wt0(B), write(' '), wt(C).

wn('{}') :- !.
wn(lf(X)) :- !,
	wt(X), write('.'), nl.
wn(X) :-
	wt(X), write('.'), nl.

wb([]) :- !.
wb([lf(X)|Y]) :-
	wt(X), write('. '), wb(Y).

wl([]) :- !.
wl([X|Y]) :-
	write(' '), wt(X), wl(Y).

ws:-
	nl, tabs(A), tab(A).

redent :-
	retractall(tabs(_)), assert(tabs(0)).

indent :-
	retract(tabs(A)), B is A+1, assert(tabs(B)).

dedent :-
	retract(tabs(A)), B is A-1, assert(tabs(B)).


% --------
% builtins
% --------

'e:biconditional'([lf('e:boolean'(A,B))|C],D) :-
	within_scope(1), (\+bset, assert(bset), bcln, bnet; true), bvar(A), bval(B),
	(flag(quick) -> qb(lf('e:boolean'(A,B)),C,D); bcon([lf('e:boolean'(A,B))],C,D)).

'e:binaryEntropy'(A,B) :-
	getnumber(A,C), (C =:= 0.0 -> B is 0.0; (C =:= 1.0 -> B is 0.0; B is -(C*log(C)+(1-C)*log(1-C))/log(2))).

'e:distinct'(A,B) :-
	when(nonvar(A),remove_duplicates(A,B)).

'e:findall'([_,S],[A,lf(B),C]) :-
	(var(S) -> S = 1; true), within_scope(S), findall(A,B,C).

'e:graphDifference'(X,Y) :-
	nonvar(X), difference(X,Y).

'e:graphIntersection'(X,Y) :-
	nonvar(X), intersection(X,Y).

'e:label'(A,B) :-
	when(nonvar(A),(atom(A) -> sub_atom(A,0,4,_,'var:'), sub_atom(A,4,_,0,C), atom_concat(['"',C,'"'],B);
	A = sk(C), atom_number(D,C), atom_concat(['"sk',D,'"'],B))).

'e:length'(A,B) :-
	when(nonvar(A),length(A,B)).

'e:max'(A,B) :-
	when(nonvar(A),bmax(A,B)).

'e:min'(A,B) :-
	when(nonvar(A),bmin(A,B)).

'e:notLabel'(A,B) :-
	when(nonvar(A),\+'e:label'(A,B)).

'e:optional'(_,lf(A)) :-
	A -> true; true.

'e:pair'(A,[B,C]) :-
	'e:sublist'(A,[B,C]); 'e:sublist'(A,[C,B]).

'e:reflexive'(_,A) :-
	B =.. [A,C,C], (\+B -> assert(B); true).

'e:reverse'(A,B) :-
	reverse(A,B).

'e:sigmoid'(A,B) :-
	getnumber(A,C), B is 1/(1+exp(-C)).

'e:sort'(A,B) :-
	when(nonvar(A),sort(A,B)).

'e:sublist'(A,B) :-
	when(nonvar(A),(append(C,_,A), append(_,B,C))).

'e:trace'(_,X) :-
	write('#TRACE '), wt(X), nl.

'e:true'(_,A) :-
	when(nonvar(A),A =:= 1.0).

'e:tuple'(X,Y) :-
	(tuple(X,Y) -> true
	; findall(Z,tuple(Z,_),L), length(L,N), atom_number(A,N), atom_concat(['var:e',A],X), assert(tuple(X,Y))).

'e:wwwFormEncode'(X,Y) :-
	ground(X), unquote(X,U), www_form_encode(U,V), atom_concat(['"',V,'"'],Y), !
	; ground(Y), unquote(Y,V), www_form_encode(U,V), atom_concat(['"',U,'"'],X).

'fl:pi'([A,B],C) :-
	within_scope(1), (fset -> true; findall(_,('fl:mu'([X,Y],Z), (fm(X) -> true; assert(fm(X))), assert(pi(X,Y,Z))),_),
	findall(_,('fl:sigma'([X,Y],_), (fs(X) -> true; assert(fs(X))), (fs(Y) -> true; assert(fs(Y)))),_), fnet, assert(fset)), pi(A,B,C).

'fn:resolve-uri'([A,B],C) :-
	when(ground([A,B]),(unquote(A,U), unquote(B,V), resolve_uri(U,V,W), atom_concat(['"',W,'"'],C))).

'fn:substring'([A,B|C],D) :-
	when(ground([A,B,C]),(sub_atom(A,1,E,1,U), (C = [] -> F is E-B; C = [F]), sub_atom(U,B,F,_,V), atom_concat(['"',V,'"'],D))).

'fn:substring-after'([A,B],C) :-
	when(ground([A,B]),(unquote(A,U), unquote(B,V), sub_atom(U,_,_,W,V), sub_atom(U,_,W,Z,X), Z = 0, atom_concat(['"',X,'"'],C))).

'fn:substring-before'([A,B],C) :-
	when(ground([A,B]),(unquote(A,U), unquote(B,V), sub_atom(U,W,_,_,V), sub_atom(U,0,W,_,X), atom_concat(['"',X,'"'],C))).

'list:append'([A,B],C) :-
	when((nonvar(A), nonvar(B)),append(A,B,C)).

'list:first'([A|_],A).

'list:in'(A,B) :-
	when(nonvar(B),member(A,B)).

'list:last'(A,B) :-
	when(nonvar(A),last(A,B)).

'list:member'(A,B) :-
	when(nonvar(A),member(B,A)).

'list:rest'([_|B],B).

'log:conjunction'(X,Y) :-
	when(nonvar(X),(conjoin(X), findall(Z,graph(Z),L), clist(L,C), (C = true -> Y = '{}'; Y = lf(C)), retractall(graph(_)))).

'log:equalTo'(X,X).

'log:implies'(lf(X),lf(Y)) :-
	(_ := X => Y), X \= true, Y \= answer(_), Y \= goal.

'log:includes'(X,Y) :-
	when((nonvar(X), nonvar(Y)),includes(X,Y)).

'log:notEqualTo'(X,Y) :-
	X \= Y.

'log:notIncludes'(X,Y) :-
	when((nonvar(X), nonvar(Y)),\+'log:includes'(X,Y)).

'log:semantics'(X,Y) :-
	when((nonvar(X); nonvar(Y)),(nonvar(X), quri(X,Q), (fact('log:semantics'(Q,Y)), !;
	findall(U,(pfx(X1,X2), atom_concat(['@prefix ',X1,' ',X2,'. '],U)),L), atom_concat(L,W),
	base(B), sub_atom(Q,1,_,1,Z), atom_concat(['.context ',W],C1), www_form_encode(C1,C2),
	tmpnam(F), atom_concat(['euler --semterm ',B,C2,' ',Z,' > ',F],V),
	system(V), open(F,read,S), catch(read(S,Y),_,Y = fail), close(S), delete_file(F), assert(fact('log:semantics'(Q,Y))))
	; nonvar(Y), X = Y, assert(fact('log:semantics'(X,Y))))).

'log:uri'(X,Y) :-
	when((nonvar(X); ground(Y)),(quri(X,Q), !, sub_atom(Q,1,_,1,U), atom_concat(['"',U,'"'],Y);
	unquote(Y,U), atom_concat(['<',U,'>'],X))).

'math:absoluteValue'(X,Z) :-
	when(ground(X),(getnumber(X,U), Z is abs(U))).

'math:cos'(X,Z) :-
	when((ground(X); ground(Z)),(getnumber(X,U), Z is cos(U), !; getnumber(Z,W), X is acos(W))).

'math:degrees'(X,Z) :-
	when((ground(X); ground(Z)),(getnumber(X,U), Z is U*180/pi, !; getnumber(Z,W), X is W*pi/180)).

'math:difference'([X,Y],Z) :-
	when(ground([X,Y]),(getnumber(X,U), getnumber(Y,V), Z is U-V)).

'math:equalTo'(X,Y) :-
	when(ground([X,Y]),(getnumber(X,U), getnumber(Y,V), U =:= V)).

'math:exponentiation'([X,Y],Z) :-
	when((ground([X,Y]); ground([X,Z])),(getnumber(X,U), (getnumber(Y,V), Z is U**V, !;
	getnumber(Z,W), Y is log(W)/log(U)))).

'math:greaterThan'(X,Y) :-
	when(ground([X,Y]),(getnumber(X,U), getnumber(Y,V), U > V)).

'math:integerQuotient'([X,Y],Z) :-
	when(ground([X,Y]),(getnumber(X,U), getnumber(Y,V), Z is U//V)).

'math:lessThan'(X,Y) :-
	when(ground([X,Y]),(getnumber(X,U), getnumber(Y,V), U < V)).

'math:memberCount'(X,Y) :-
	when(nonvar(X),length(X,Y)).

'math:negation'(X,Z) :-
	when((ground(X); ground(Z)),(getnumber(X,U), Z is -U, !; getnumber(Z,W), X is -W)).

'math:notEqualTo'(X,Y) :-
	when(ground([X,Y]),(getnumber(X,U), getnumber(Y,V), U =\= V)).

'math:notGreaterThan'(X,Y) :-
	when(ground([X,Y]),(getnumber(X,U), getnumber(Y,V), U =< V)).

'math:notLessThan'(X,Y) :-
	when(ground([X,Y]),(getnumber(X,U), getnumber(Y,V), U >= V)).

'math:product'(X,Z) :-
	when(ground(X),product(X,Z)).

'math:quotient'([X,Y],Z) :-
	when(ground([X,Y]),(getnumber(X,U), getnumber(Y,V), Z is U/V)).

'math:remainder'([X,Y],Z) :-
	when(ground([X,Y]),(getnumber(X,U), getnumber(Y,V), Z is U mod V)).

'math:rounded'(X,Z) :-
	when(ground(X),(getnumber(X,U), Z is round(U))).

'math:sin'(X,Z) :-
	when((ground(X); ground(Z)),(getnumber(X,U), Z is sin(U), !; getnumber(Z,W), X is asin(W))).

'math:sum'(X,Z) :-
	when(ground(X),sum(X,Z)).

'math:tan'(X,Z) :-
	when((ground(X); ground(Z)),(getnumber(X,U), Z is tan(U), !; getnumber(Z,W), X is atan(W))).

'rdf:first'([X|Y],X) :-
	'rdf:type'([X|Y],'rdf:List').

'rdf:rest'([X|Y],Y) :-
	'rdf:type'([X|Y],'rdf:List').

'str:concatenation'([X,Y],Z) :-
	when(ground([X,Y]),(unquote(X,S), unquote(Y,T), atom_concat(['"',S,T,'"'],Z))).

'str:contains'(X,Y) :-
	when(ground([X,Y]),(unquote(X,S), unquote(Y,T), sub_atom(S,_,_,_,T))).

'str:containsIgnoringCase'(X,Y) :-
	when(ground([X,Y]),(unquote(X,S), unquote(Y,T), atom_codes(S,U), atom_codes(T,V), regexp(V,U,[nocase]))).

'str:endsWith'(X,Y) :-
	when(ground([X,Y]),(unquote(X,S), unquote(Y,T), sub_atom(S,_,_,0,T))).

'str:equalIgnoringCase'(X,Y) :-
	when(ground([X,Y]),(unquote(X,S), unquote(Y,T), atom_codes(S,U), atom_codes(T,V), regexp(V,U,[nocase],[W]), W == U)).

'str:greaterThan'(X,Y) :-
	when(ground([X,Y]),X @> Y).

'str:lessThan'(X,Y) :-
	when(ground([X,Y]),X @< Y).

'str:matches'(X,Y) :-
	when(ground([X,Y]),(unquote(X,S), unquote(Y,T), atom_codes(S,U), atom_codes(T,V), regexp(V,U,[],[W]), W == U)).

'str:notEqualIgnoringCase'(X,Y) :-
	when(ground([X,Y]),\+'str:equalIgnoringCase'(X,Y)).

'str:notGreaterThan'(X,Y) :-
	when(ground([X,Y]),X @=< Y).

'str:notLessThan'(X,Y) :-
	when(ground([X,Y]),X @>= Y).

'str:notMatches'(X,Y) :-
	when(ground([X,Y]),\+'str:matches'(X,Y)).

'str:startsWith'(X,Y) :-
	when(ground([X,Y]),(unquote(X,S), unquote(Y,T), sub_atom(S,0,_,_,T))).

'time:day'(tlit(X,_),Y) :-
	when(ground(X),(sub_atom(X,9,2,_,Z), atom_concat(['"',Z,'"'],Y))).

'time:month'(tlit(X,_),Y) :-
	when(ground(X),(sub_atom(X,6,2,_,Z), atom_concat(['"',Z,'"'],Y))).

'time:year'(tlit(X,_),Y) :-
	when(ground(X),(sub_atom(X,1,4,_,Z), atom_concat(['"',Z,'"'],Y))).


% -------
% support
% -------

base(A) :-
	flag(port(B)), !, atom_concat(['http://localhost:',B,'/'],A).
base('http://localhost/').

auri('log:semantics'(A,B),'log:semantics'(D,B)) :-
	quri(A,D), !.
auri('log:uri'(A,B),'log:uri'(D,B)) :-
	quri(A,D), !.
auri(A,A).

quri(A,A) :-
	atom(A), sub_atom(A,1,_,1,U), atom_concat(['<',U,'>'],A), !.
quri(A,B) :-
	atom(A), pfx(A,B), !.
quri(A,B) :-
	atom(A), pfx(U,V), sub_atom(A,0,X,Y,U), sub_atom(V,0,_,1,W), sub_atom(A,X,Y,_,Q), atom_concat([W,Q,'>'],B), !.
quri(lf(A),lf(A)) :-
	nonvar(A).

within_scope(A) :-
	(limit(B) -> (B < A -> retract(limit(B)), assert(limit(A)); true); assert(limit(A))), scope(A), brake.

varpred(S,P,O) :-
	atom(P) -> U =.. [P,S,O], U; steps(_,_,U), U =.. [P,S,O], P \= false.

unif(varpred(S,P,O),A) :-
	A =.. [P,S,O], !.
unif(A,varpred(S,P,O)) :-
	A =.. [P,S,O], !.
unif(A,A).

clist([],true) :- !.
clist([A],A) :- !.
clist([A|B],(A,C)) :-
	clist(B,C).

cmember(A,(A,_)).
cmember(A,(_,B)) :-
	cmember(A,B).
cmember(A,A) :-
	A \= (_,_).

conjoin([]) :- !.
conjoin(['{}'|Y]) :- !,
	conjoin(Y).
conjoin([lf(true)|Y]) :- !,
	conjoin(Y).
conjoin([lf(X)|Y]) :-
	agraph(X), conjoin(Y).

agraph((X,Y)) :- !,
	(\+graph(X) -> assert(graph(X)); true), agraph(Y).
agraph(X) :-
	\+graph(X) -> assert(graph(X)); true.

includes('{}','{}') :- !.
includes(lf(_),'{}') :- !.
includes(lf(X),lf(Y)) :-
	unif(X,Y), !.
includes(lf((X,Y)),lf(Z)) :-
	unif(X,Z); includes(lf(Y),lf(Z)).
includes(lf(X),lf((Y,Z))) :-
	includes(lf(X),lf(Y)), includes(lf(X),lf(Z)).

difference(['{}',_],'{}') :- !.
difference([X,'{}'],X) :- !.
difference([lf(X),lf(Y)],Z) :-
	findall(U,(cmember(U,X), \+((cmember(V,Y), unif(U,V)))),W), (W = [] -> Z = '{}'; clist(W,G), Z = lf(G)).

intersection([X],X) :- !.
intersection(['{}'|_],'{}') :- !.
intersection([_|Y],'{}') :-
	intersection(Y,'{}'), !.
intersection([lf(X)|Y],lf(Z)) :-
	intersection(Y,lf(I)), findall(U,(cmember(U,X), cmember(V,I), unif(U,V)),W), clist(W,Z).

sum([],0) :- !.
sum([A|B],C) :-
	getnumber(A,X), sum(B,D), C is X+D.

product([],1) :- !.
product([A|B],C) :-
	getnumber(A,X), product(B,D), C is X*D.

bmax([A|B],C) :-
	bmax(B,A,C).

bmax([],A,A).
bmax([A|B],C,D) :-
	(A > C -> bmax(B,A,D); bmax(B,C,D)).

bmin([A|B],C) :-
	bmin(B,A,C).

bmin([],A,A).
bmin([A|B],C,D) :-
	(A < C -> bmin(B,A,D); bmin(B,C,D)).

inconsistent([lf('e:boolean'(A,'e:T'))|B]) :-
	memberchk(lf('e:boolean'(A,'e:F')),B), !.
inconsistent([lf('e:boolean'(A,'e:F'))|B]) :-
	memberchk(lf('e:boolean'(A,'e:T')),B), !.
inconsistent([_|B]) :-
	inconsistent(B).

inverse(lf('e:boolean'(A,'e:T')),lf('e:boolean'(A,'e:F'))) :- !.
inverse(lf('e:boolean'(A,'e:F')),lf('e:boolean'(A,'e:T'))).

bcln :-
	'e:conditional'([A|B],U), (flag(quick) -> Z = U; sort(B,C), findall(Y,('e:conditional'([A|X],Y), sort(X,C)),L),
	sum(L,S), length(L,N), Z is S/N), \+bcnd([A|B],_), assert(bcnd([A|B],Z)),
	inverse(A,D), \+bcnd([D|B],_), E is 1-Z, assert(bcnd([D|B],E)), fail; true.

bnet :-
	bcnd([lf('e:boolean'(A,_))|B],_), (\+bvar(A), assert(bvar(A)); true),
	member(lf('e:boolean'(C,_)),B), \+bref(C,A), assert(bref(C,A)), \+bvar(C), assert(bvar(C)), fail; true.

bval('e:T').
bval('e:F').

brel(lf('e:boolean'(A,_)),lf('e:boolean'(B,_))) :-
	bref(A,B), !.
brel(A,lf('e:boolean'(B,_))) :-
	bref(C,B), brel(A,lf('e:boolean'(C,_))).

bpar([],[]) :- !.
bpar([lf('e:boolean'(A,_))|B],[A|C]) :-
	bpar(B,C).

bget(A,B,1.0) :-
	memberchk(A,B), !.
bget(lf('e:boolean'(A,'e:T')),B,0.0) :-
	memberchk(lf('e:boolean'(A,'e:F')),B), !.
bget(lf('e:boolean'(A,'e:F')),B,C) :-
	memberchk(lf('e:boolean'(A,'e:T')),B), !, C is 0.0; !, bget(lf('e:boolean'(A,'e:T')),B,D), C is 1-D.
bget(A,B,C) :-
	bgot(A,B,C) -> true; (member(X,B), brel(A,X), member(G,B),
	findall(Y,(member(Z,[A|B]), brel(G,Z)),[]), delete(B,G,H), !,
	bget(G,[A|H],U), bget(A,H,V), bget(G,H,W), (W =:= 0.0 -> C is V; E is U*V/W, bmin([E,1.0],C));
	findall([Z,Y],(bcnd([A|O],P), bcon(O,B,Q), Z is P*Q, bpar(O,Y)),L),
	findall(Z,(member([_,Z],L)),N), remove_duplicates(N,I),
	findall(Z,(member(Y,I), findall(P,(member([P,Y],L)),Q), sum(Q,R), length(Q,S), length(Y,T),
		(Q = [] -> Z is 0.0; D is 2**(T-ceiling(log(S)/log(2))), (D < 1 -> Z is R*D; Z is R))),J),
	(J = [] -> C is 0.0; bmax(J,C))), assert(bgot(A,B,C)).

bcon([],_,1.0) :- !.
bcon(_,B,0.5) :-
	inconsistent(B), !.
bcon([A|B],C,D) :-
	bget(A,C,E), bcon(B,[A|C],F), D is E*F.

qc(_,[],0.0) :- !.
qc(A,[B|C],D) :-
	(bcnd([B,A],E); inverse(B,F), bcnd([F,A],G), E is 1-G; E is 1.0), !, (E =:= 0.0 -> I = 1e-16; I = E),
	qc(A,C,H), D is log(I)/log(2)+H.

qb(A,B,1.0) :-
	memberchk(A,B), !.
qb(lf('e:boolean'(A,'e:T')),B,0.0) :-
	memberchk(lf('e:boolean'(A,'e:F')),B), !.
qb(lf('e:boolean'(A,'e:F')),B,C) :-
	memberchk(lf('e:boolean'(A,'e:T')),B), !, C is 0.0; !, qb(lf('e:boolean'(A,'e:T')),B,D), C is 1-D.
qb(A,B,C) :-
	bcnd([A,D],E), !, qb(D,B,F), inverse(D,G), bcnd([A,G],H), C is F*E+(1-F)*H
	; qc(A,B,D), !, inverse(A,E), qc(E,B,F), C is 1/(1+2**(F-D)).

fnet :-
	repeat(20), fm(X), fs(Y), findall(I,('fl:sigma'([P,Y],W), pi(X,P,M), I is W*M),L),
	(L = [] -> true; sum(L,A), Z is 1/(1+exp(-5*A)), retractall(pi(X,Y,_)), assert(pi(X,Y,Z))), fail; true.

repeat(_).
repeat(N) :- N > 1, N1 is N-1, repeat(N1).	

numbervars(sk(A),A,B,sk) :- !,
	B is A+1.
numbervars(all(A),A,B,all) :- !,
	B is A+1.
numbervars(var(A),A,B,var) :- !,
	B is A+1.
numbervars(A,B,B,_) :-
	atomic(A), !.
numbervars([A|B],C,D,Q) :- !,
	numbervars(A,C,E,Q), numbervars(B,E,D,Q).
numbervars((A,B),C,D,Q) :- !,
	numbervars(A,C,E,Q), numbervars(B,E,D,Q).
numbervars(A,B,C,Q) :-
	functor(A,_,D), numbervars(0,D,A,B,C,Q).

numbervars(A,A,_,B,B,_) :- !.
numbervars(A,B,C,D,E,Q) :-
	F is A+1, arg(F,C,G), numbervars(G,D,H,Q), numbervars(F,B,C,H,E,Q).

getnumber(A,A) :-
	ground(A), number(A), !.
getnumber(tlit(A,'xsd:dateTime'),B) :- !,
	ground(A), fact(datetime(A,B)).
getnumber(tlit(A,'xsd:duration'),B) :- !,
	ground(A), fact(duration(A,B)).
getnumber(tlit(A,_),B) :- !,
	ground(A), unquote(A,C), atom_number(C,B).
getnumber(plit(A,_),B) :- !,
	ground(A), unquote(A,C), atom_number(C,B).
getnumber(A,B) :-
	ground(A), unquote(A,C), atom_number(C,B).

unquote(A,B) :-
	ground(A), sub_atom(A,0,1,_,'"'), sub_atom(A,_,1,0,'"'), sub_atom(A,1,_,1,B).	

unreserved(C) :-
	1 =< C, C =< 128, code_type(C,alnum).
unreserved(0'-).
unreserved(0'.).
unreserved(0'_).
unreserved(0'~).

www_form_encode(A,B) :-
	atomic(A), atom_codes(A,C), phrase(www_encode(C,""),D), !, atom_codes(B,D).
www_form_encode(A,B) :-
	atom_codes(B,C), phrase(www_decode(D),C), !, atom_codes(A,D).

resolve_uri(A,_,A) :-
	sub_atom(A,_,_,_,':'), !.
resolve_uri(A,B,C) :-
	sub_atom(A,0,_,_,'/'),
	sub_atom(B,0,_,D,'http://'),
	sub_atom(B,7,D,_,E),
	sub_atom(E,F,_,_,'/'), !,
	sub_atom(E,0,F,_,G),
	atom_concat(['http://',G,A],C).
resolve_uri(A,B,C) :-
	sub_atom(B,0,_,D,'http://'),
	sub_atom(B,7,D,_,E),
	sub_atom(E,F,_,G,'/'),
	sub_atom(E,_,G,0,H),
	\+sub_atom(H,_,_,_,'/'),
	sub_atom(E,0,F,_,I),
	atom_concat(['http://',I,'/',A],C).

% DCG thanks to SWI-Prolog url.pl and utf8.pl
www_encode([0'\r, 0'\n|T], Extra) --> !,
	"%0D%0A",
	www_encode(T, Extra).
www_encode([0'\n|T], Extra) --> !,
	"%0D%0A",
	www_encode(T, Extra).
www_encode([H|T], Extra) -->
	percent_encode(H, Extra),
	www_encode(T, Extra).
www_encode([], _) -->
	"".

percent_encode(C, _Extra) -->
	{ unreserved(C) }, !,
	[C].
percent_encode(C, Extra) -->
	{ memberchk(C, Extra) }, !,
	[C].
percent_encode(C, _) -->
	{ C =< 128 }, !,
	percent_byte(C).
percent_encode(C, _) --> !,
	{ phrase(utf8_codes([C]), Bytes)},
	percent_bytes(Bytes).
percent_encode(C, _) -->
	percent_byte(C).

percent_bytes([]) -->
	"".
percent_bytes([H|T]) -->
	percent_byte(H),
	percent_bytes(T).

percent_byte(C) -->
	[0'%, D1, D2],
	{   nonvar(C)
	->  Dv1 is (C>>4 /\ 0xf),
	    Dv2 is (C /\ 0xf),
	    code_type(D1, xdigit(Dv1)),
	    code_type(D2, xdigit(Dv2))
	;   code_type(D1, xdigit(Dv1)),
	    code_type(D2, xdigit(Dv2)),
	    C is ((Dv1)<<4) + Dv2
	}.

percent_coded(C) -->
	percent_byte(C0), !,
	(   { C0 == 13
	    },
	    "%0",
	    ( "A" ; "a" )
	->  { C = 10
	    }
	;   { C0 >= 0xc0 },
	    utf8_con(Cs),
	    { phrase(utf8_codes([C]), [C0|Cs]) }
	->  []
	;   { C = C0
	    }
	).

www_decode([0' |T]) -->
	"+", !,
        www_decode(T).
www_decode([C|T]) -->
	percent_coded(C), !,
	www_decode(T).
www_decode([C|T]) -->
	[C], !,
	www_decode(T).
www_decode([]) -->
	[].

utf8_con([H|T]) -->
	percent_byte(H),
	{ 0x80 =< H, H =< 0xbf }, !,
	utf8_con(T).
utf8_con([]) -->
	[].

utf8_codes([H|T]) -->
	utf8_code(H), !,
	utf8_codes(T).
utf8_codes([]) -->
	[].

utf8_code(C) -->
	[C0],
	{ nonvar(C0) }, !,
	(   {C0 < 0x80}
	->  {C = C0}
	;   {C0/\0xe0 =:= 0xc0}
	->  utf8_cont(C1, 0),
	    {C is (C0/\0x1f)<<6\/C1}
	;   {C0/\0xf0 =:= 0xe0}
	->  utf8_cont(C1, 6),
	    utf8_cont(C2, 0),
	    {C is ((C0/\0xf)<<12)\/C1\/C2}
	;   {C0/\0xf8 =:= 0xf0}
	->  utf8_cont(C1, 12),
	    utf8_cont(C2, 6),
	    utf8_cont(C3, 0),
	    {C is ((C0/\0x7)<<18)\/C1\/C2\/C3}
	;   {C0/\0xfc =:= 0xf8}
	->  utf8_cont(C1, 18),
	    utf8_cont(C2, 12),
	    utf8_cont(C3, 6),
	    utf8_cont(C4, 0),
	    {C is ((C0/\0x3)<<24)\/C1\/C2\/C3\/C4}
	;   {C0/\0xfe =:= 0xfc}
	->  utf8_cont(C1, 24),
	    utf8_cont(C2, 18),
	    utf8_cont(C3, 12),
	    utf8_cont(C4, 6),
	    utf8_cont(C5, 0),
	    {C is ((C0/\0x1)<<30)\/C1\/C2\/C3\/C4\/C5}
	).
utf8_code(C) -->
	{ nonvar(C) }, !,
	(   { C < 0x80 }
	->  [C]
	;   { C < 0x800 }
	->  { C0 is 0xc0\/((C>>6)/\0x1f),
	      C1 is 0x80\/(C/\0x3f)
	    },
	    [C0,C1]
	;   { C < 0x10000 }
	->  { C0 is 0xe0\/((C>>12)/\0x0f),
	      C1 is 0x80\/((C>>6)/\0x3f),
	      C2 is 0x80\/(C/\0x3f)
	    },
	    [C0,C1,C2]
	;   { C < 0x200000 }
	->  { C0 is 0xf0\/((C>>18)/\0x07),
	      C1 is 0x80\/((C>>12)/\0x3f),
	      C2 is 0x80\/((C>>6)/\0x3f),
	      C3 is 0x80\/(C/\0x3f)
	    },
	    [C0,C1,C2,C3]
	;   { C < 0x4000000 }
	->  { C0 is 0xf8\/((C>>24)/\0x03),
	      C1 is 0x80\/((C>>18)/\0x3f),
	      C2 is 0x80\/((C>>12)/\0x3f),
	      C3 is 0x80\/((C>>6)/\0x3f),
	      C4 is 0x80\/(C/\0x3f)
	    },
	    [C0,C1,C2,C3,C4]
	;   { C < 0x80000000 }
	->  { C0 is 0xfc\/((C>>30)/\0x01),
	      C1 is 0x80\/((C>>24)/\0x3f),
	      C2 is 0x80\/((C>>18)/\0x3f),
	      C3 is 0x80\/((C>>12)/\0x3f),
	      C4 is 0x80\/((C>>6)/\0x3f),
	      C5 is 0x80\/(C/\0x3f)
	    },
	    [C0,C1,C2,C3,C4,C5]
	).
	     
utf8_cont(Val, Shift) -->
	[C],
	{ C/\0xc0 =:= 0x80,
	  Val is (C/\0x3f)<<Shift
	}.