% test...

% reseni testu...

% z minula
model(V,F,B):-variable(F),(member(F/B,V);B=0).
model(V,F,B):-F=..[Sym|SubForm],modellist(V,SubForm,Bs),F2=..[tt,Sym,B|Bs],call(F2),!.

modellist(_,[],[]).
modellist(V,[F|SubForm],[B|Bs]):-model(V,F,B),modellist(V,SubForm,Bs).

variable(A):-var(A);atom(A).

% logicke spojky
:- op(300,fx,~).
:- op(400,xfy,/\).
:- op(350,xfy,\/).
:- op(600,xfx,=>).
:- op(650,xfx,<=>).

% operator valuace
:- op(500,xfx,/).

% not
tt(~,0,1).
tt(~,1,0).
% or
tt(\/,0,0,0).
tt(\/,1,0,1).
tt(\/,1,1,0).
tt(\/,1,1,1).
% and
tt(/\,1,1,1).
tt(/\,0,0,1).
tt(/\,0,1,0).
tt(/\,0,0,0).
% eq
tt(<=>,1,0,0).
tt(<=>,0,0,1).
tt(<=>,0,1,0).
tt(<=>,1,1,1).
% impl
tt(=>,1,0,0).
tt(=>,1,0,1).
tt(=>,0,1,0).
tt(=>,1,1,1).

wff(A):-(var(A);atom(A)),!.
wff(~A):-wff(A).
wff(A):-(A=B \/ C;A=B /\ C;A=B => C;A=B <=> C),wff(B),wff(C),!.

% rozmyslet si predikat model(F,V,B), ktery unifikuje B=1, pokud V je modelem F a B=0 jinak
% napiste tuto metodu obecne pro libovolne log. funkce (tj. pres operator dekompozice)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Predikaty vyssiho radu
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% maplist/2 a maplist/3 - aplikace predikatu na seznam

% maplist(P,L) - aplikuje unární predikát P na L
% ?- maplist(odd,[1,3,5]).
% true.
% maplist(P,L1,L2) - aplikuje predikat P na prvky L1 a vystup ulozi do L2
% ?- maplist(plus(1), [0, 1, 2], X).
% X = [1, 2, 3]

% bagof(Var,Goal,Bag) - nasbira predikaty majici nejakou vlastnost
% bagof(X,tt(X,1,0,1),L). - L je seznam symbolu, ktere vraci true pri parametrech 0 a 1
% setof(Var,Goal,Bag) - jako bagof, ale vraci to jako mnozinu (tj. bez duplicit)

p(1,3,5).
p(1,4,5).
p(2,4,1).
p(3,5,2).
p(4,3,1).
p(5,2,4).
q(3).

% u bagof apod. je druhy argument konjunkce podminek, kterou musi bindovana promena splnit
% napr: ?- bagof(X,(p(X,Y,_),q(Y)),Bag).
% toto pri spusteni vrati pouze Bag=[4] a pri odmitnuti Bag=[1]. Promenna Y se totiz namatchuje na data z databaze. 
% muzeme prologu rict, ze namisto namatchovani Y ma najit vsechny vyskyty, kde za Y jde neco namatchvoat (existencni kvantifikator)
% vyuzijeme operatoru ^/2
% ?- bagof(X,Y^Z^(p(X,Y,Z),q(Y)),Bag).
% Bag=[1,4].

% rozdíl mezi findall a setof

dite(mama1,dite1).
dite(mama1,dite2). 

dite(mama2,dite1). 
dite(mama2,dite2).  
dite(mama2,dite3).   

% nyní při dotazu findall(X,dite(M,X),L). to vrátí L = [dite1, dite2, dite1, dite2, dite3].
% To je nic moc neříkající, setof vrátí
% ?- setof(X,dite(M,X),L).
% M = mama1,
% L = [dite1, dite2] ;
% M = mama2,
% L = [dite1, dite2, dite3].
%
% vidime tady lepe, ktere dite patri ktere matce

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Prace s databazi
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% assert(K) - prida klauzuli na konec databaze
% asserta(K) - prida klauzuli na zacatek databaze
% retract(K) - vymaze z databaze prvni vyskyt klauzule unifikovatelny s K
% retractall(K) - vymaze z databaze vsechny vyskyty, jejichz hlava se da unifikovat s K

% :-dynamic tt/3
% toto rika, ze definice tt se bdue za behu menit
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% findall pomoci assert
%findall(X,Cil,Bag):- zapis(X,Cil),
%                     seber([],Bag).
%zapis(X,Cil):- call(Cil),
%               asserta(data999(X)),
%               fail.
%zapis(_,_).
%seber(B,Bag) :- data999(X),
%                retract(data999(X)),
%                seber([X|B],Bag), !.
%seber(Bag,Bag).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% jak se da vyuzit cerveneho rezu
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% roznasob(X,Y) - roznasobi vyraz v X
roznasob(X,Y):-roznasob2(X,Z),!,roznasob(Z,Y).
roznasob(X,X).

% nechame prolog backtrackovat a nedeterministicky upravovat
roznasob2(A *(B + C),(A * B) + (A * C)).
roznasob2((A + B) * C,(A * C) + (B * C)).
roznasob2( A + B,A + Bd):-roznasob2(B,Bd).
roznasob2( A + B,Ad + B):-roznasob2(A,Ad).
roznasob2( A * B,A * Bd):-roznasob2(B,Bd).
roznasob2( A * B,Ad * B):-roznasob2(A,Ad).