%lab 11
move((K,M),[N|Ns],[N|Ns1]):-K>1,K1 is K-1,move((K1,M),Ns,Ns1).
move((1,N),[N|Ns],Ns).
move((1,M),[N|Ns],[N1|Ns]):-M<N,N1 is N-M.


initialize(nim,[1,3,5,7],opponent).

play(Game,Result) :-initialize(Game,Position,Player),display_game(Position,Player),
play(Position,Player,Result).
play(Position,Player,Result) :-game_over(Position,Player,Result), !,announce(Result).
play(Position,Player,Result) :-choose_move(Position,Player,Move),move(Move,Position,Position1),display_game(Position1,Player),next_player(Player,Player1),!, play(Position1,Player1,Result).

choose_move(Position,opponent,Move) :-write(['Please make move (pile,matches)']), nl,read(Move),legal(Move,Position).
choose_move(Ns,computer,Move):-unsafe(Ns,Sum),safe_move(Ns,Sum,Move).
choose_move(Ns,computer,(1,1)):-safe(Ns).

nim_sum([N|Ns],Bs,Sum) :-binary(N,Ds),nim_add(Ds,Bs,Bs1),nim_sum(Ns,Bs1,Sum).

safe_move(Piles,NimSum,Move) :-safe_move(Piles,NimSum,1,Move).
safe_move([Pile|_],NimSum,K,(K,M)) :-binary(Pile,Bs),can_zero(Bs,NimSum,Ds,0),
decimal(Ds,M).
safe_move([_|Piles],NimSum,K,Move) :-K1 is K+1,safe_move(Piles,NimSum,K1,Move).

can_zero([],NimSum,[],0) :-zero(NimSum).
can_zero([_|Bs],[0|NimSum],[C|Ds],C) :-can_zero(Bs,NimSum,Ds,C).
can_zero([B|Bs],[1|NimSum],[D|Ds],C) :-D is 1-B*C, C1 is 1-B, can_zero(Bs,NimSum,Ds,C1).
decimal(0,'0').
decimal(1,'1').
decimal(N,B) :-
	N > 1,
	X is N mod 2,
	Y is N//2,
	decimal(Y,B1),
	atom_concat(B1, X, B).

next_player(opponent,computer).
next_player(computer,opponent).

display_game(Position,Player):-write(Player),write(''),write(Position),nl.

game_over([],_,_).
announce(result):-write('Game over:').
legal((N,M),Position):-nth1(N,Position,Pile),Pile>=M,M>0.
unsafe(Ns,Sum):-nim_sum(Ns,Sum,S),zero(S).
safe(Ns):-not(unsafe(Ns,_)).
nim_sum([N|Ns],Bs,Sum):-binary(N,Ds),nim_add(Ds,Bs,Bs1),nim_sum(Ns,Bs1,Sum).
zero([]).
zero([X|NimSum]):-X=:=0,zero(NimSum).

suma(0,0,0).
suma(1,1,0).
suma(1,0,1).
suma(0,1,1).

nim_add([],[],[]).
nim_add([X|Ns],[Y|Bs],[S|Bs1]):-suma(X,Y,S),nim_add(Ns,Bs,Bs1).

bin(0,[]).
bin(N,[M|R]):-M is Nmod2,C is N // 2,(C,M)/=(0,0),bin(C,R).

binary(N,D):-bin(N,D).
pow(A,N,R):-R is A**N.

decimal([],0).
decimal(L,X):-deci(L,X,0,0).

deci([],X,X,_).
deci([H|T],X,Xi,N):-pow(2,N,S),S1 is H*S+Xi,N1 is N+1,deci(T,X,S1,N1).



decimal(0,'0').
decimal(1,'1').
decimal(N,B) :-
	N > 1,
	X is N mod 2,
	Y is N//2,
	decimal(Y,B1),
	atom_concat(B1, X, B).

next_player(opponent, computer).
next_player(computer, opponent).

display_game(Position, Player):-
    write(Player),
    write(''),
    write(Position),
    nl.

game_over([],_,_).

announce(result):- write('Game over').

safe(Ns):-not(unsafe(Ns,_)).
unsafe(Ns,Sum):-nim_sum(Ns, Sum, S), zero(S).

legal((N,M),Position):-nth1(N, Position, Pile), Pile >= M, M > 0.


zero([]).
zero([X|NimSum]):-X=:=0,zero(NimSum).

sum(0,0,0).
sum(1,1,1).
sum(1,0,1).
sum(0,1,1).

nim_add([], [], []).
nim_add([X|Ns], [Y|Bs], [S|Bs1]):-
    sum(X,Y,S),
    nim_add(Ns,Bs,Bs1).

bin(0,[]).
bin(N,[M|R]):-M is N mod 2, C is N//2, (C,M) \= (0,0), bin(C,R).
binary(N,D):-bin(N, D).

pow(A,N,R):-R is A**N.




%lab10


start:- write('Input the formula (ex: [p, and, [not, q]]) ='),
read(Formula), write('Input the variables list'), read(Var),
table(Formula, Var).

liste_variables([p,q,r,s,t,u,v,z]).
bienforme(X):-liste_variables(L),member(X,L).
bienforme([not,F]):-bienforme(F).
bienforme([X,O,Y]):-bienforme(X),
	member(O,[and,or,->,<->]),
	bienforme(Y).

combiner(L,0,[[]]):-!.
combiner(L,N,R):-N1 is N-1,combiner(L,N1,R1),ajouter(L,R1,R).
ajouter(_,[],[]).
ajouter([],_,[]).

ajouter([H|T],[H1|T1],[[H|H1]|R]):-
	ajouter([H],T1,R1),ajouter(T,[H1|T1],R2),append(R1,R2,R).

subst(N,V,[],[]).
subst(N,V,[V|T],[N|R]):-subst(N,V,T,R).
subst(N,V,[A|T],[A|R]):-A\=V,atom(A),subst(N,V,T,R).
subst(N,V,[A|T],[R1|R]):-A\=V,not(atom(A)),subst(N,V,A,R1),subst(N,V,T,R).

sub([],[],L,L).
sub([Val|T1],[Var,T2],F,R):-
	subst(Val,Var,F,S),sub(T1,T2,S,R).

table(Formula, Lvar):- length(Lvar, Lung),
combiner([true, false], Lung, Comb),
member(C, Comb),
line(C, Lvar, Formula, Rez), fail.
line(C, Lvar, Formula, Rez):- write(C), tab(2),
sub(C, Lvar, Formula, Rez),
write(Rez), tab(3),
(eval(Rez), write(true), !; write(false), !), nl.
eval(true):- true.
eval(false):- false.
eval([X, and, Y]):-eval(X), eval(Y).
eval([X, or, Y]):- eval(X); eval(Y).
eval([not, X]):- not(eval(X)).
eval([X, ->, Y]):- not(eval(X)); eval(Y).
eval([X, <->, Y]):- (not(eval(X)); eval(Y)),(not(eval(Y)); eval(X)).