% -*- mercury -*-
%##############################################################################
% Types
%##############################################################################
#ifdef PM_TYPES
% TODO use a special CLP, over norvegian, ... DSL CHR :))
% TODO dont use around, use or plus minus plusbol (need NF)
% TODO to do with use of element
% TODO do it in prolog normal, possible ?? 
% TODO cf constraint in sicp (AC ?)
% TODO use bool
%  type plusbol  (var int) -> (var int) -> (var int) -> (var int) -> constraint.
% TODO can we generalise the bolstuff ??
%  "plusbol1" @@ [plusbol X Y Z R]

type in  (var int) -> int -> int -> constraint. %TODO can do also vint -> vint -> vint !!!
type ins (var int) -> (list int)-> constraint. %TODO can do also vint -> vint -> vint !!!
type domain (list (var int)) -> int -> int -> constraint. 
type neq (var int) -> (var int) -> constraint. %TODO generalise
type all_different (list (var int)) -> constraint.
type around (var int) -> (var int) -> constraint.
op 700 xfx neq .


% X + 1 = Y, if X in 1..5 and y in 1..5 => X in 1..4, Y in 2..5
type ac_plus (list int) -> (list int) -> int -> (list int) -> (list int) -> o.
ac_plus XS YS V XSbis YSbis :-
	filter (x\ (sigma y\ (member y YS, y is x + V ))  ) XS XSbis,
	filter (x\ (sigma y\ (member y XS, y is x - V ))  ) YS YSbis,
	% to not loop in chr !!!
	not (XS = XSbis, YS = YSbis).

type ac_around (list int) -> (list int) -> (list int) -> (list int) -> o.
%dont work: ac_around XS YS XSbis YSbis :- ac_plus XS YS 1 XSbis YSbis ; ac_plus YS XS 1 ...
ac_around XS YS XSbis YSbis :-
	filter (x\ (sigma y\ (member y YS, (y is x + 1; y is x - 1)))) XS XSbis,
	filter (x\ (sigma y\ (member y XS, (y is x + 1; y is x - 1)))) YS YSbis,
	not (XS = XSbis, YS = YSbis).


#endif
%##############################################################################
% Rules
%##############################################################################
#ifdef PM_RULES

%"in"       @@ [in (cc X) Y Z]      <=> [ccall_g (X >= Y, X =< Z)].
%"in2"      @@ [in X Y Y]           <=> [X eq (cc Y)].
%"in3"      @@ [in X Y Z]           <=> [cfalse] if Y > Z.
%"label"    @@ [in X Y Z] with [labeling] <=>[cchoice (X eq (cc Y)) (in X Y2 Z)] if Y2 is Y+1, Y =< Z.
% cant do
%"label"    @@ [in X Y Z, labeling] ==> [X eq (cc Y)]. %a ==>cos must keep the in constraint to check
%"label2"   @@ [in X Y Z] with [labeling] <=> [in X Y2 Z] if Y2 is Y+1.
% cos my engine cut !! TODO?

% prefer ins cos more general
"in"  @@ [in X Y Z] <=> [ins X L] if generate Y Z L.

"ins1"  @@ [ins (cc X) L] <=> [ccall_g (member X L)].
"ins2"  @@ [ins X [Y]]    <=> [X eq (cc Y)].
"ins3"  @@ [ins X []]     <=> [cfalse].
"label" @@ [ins X [Y|YS]] with [labeling] <=> [cchoice (X eq (cc Y)) (ins X YS)].

"domain"     @@ [domain [] Y Z]     <=> [].
"domain2"    @@ [domain [X|XS] Y Z] <=> [in X Y Z, domain XS Y Z].

"neq"        @@ [(cc X) neq (cc Y)] <=> [ccall_g (X =\= Y)].
"neq2"       @@ [X neq X] <=> [cfalse].
"neq3"       @@ [X neq Y] ==> [Y neq X]. %PB comm !! can loop ??

"all_different1" @@ [all_different []] <=> [].
"all_different2" @@ [all_different [X|XS]] <=> [(all_different XS)|YS]
  if mapfun (x\ (X neq x)) XS YS.

%delete do a member needed ? yes cos avoid to be fired twice
"neq and ins" @@ [ins X L] with [X neq (cc Y)] <=> [ins X L2] if delete Y L L2.
"ins and eq"  @@ [ins X L1, ins X L2] <=> [ins X L3] if intersection L1 L2 L3.

% TODO generalise, plus cv cv cc, plus cc cv cv,
%  how ?? make ac a constraint ?? or make binary constraint = arc ?? 
% arc consistency technique
"plus and ins" @@ [ins X1 L1, ins X2 L2] with [(plus X1 (cc Y) X2)] <=> [ins X1 L1bis, ins X2 L2bis]
   if ac_plus L1 L2 Y L1bis L2bis.

%((X #= Y+1) #\/ (X #= Y-1)),
"around"  @@ [around (cc X) (cc Y)] <=> [ccall_g(X is Y+1; X is Y-1)].
"around2" @@ [ins X1 L1, ins X2 L2] with [around X1 X2] <=> [ins X1 L1bis, ins X2 L2bis]
   if ac_around L1 L2 L1bis L2bis.
"around3" @@ [ins X L] with [around (cc Y) X] <=> [ins X L2]
   if (filter (x\ (x is Y + 1; x is Y - 1)) L L2, not (L = L2)).
"around4" @@ [around X Y] ==> [around Y X].
"around5" @@ [around X X] <=> [cfalse].
   
	      
% always same:
%  first rule = when instantiated,
%  then the other case (when <, =, >, ...) or when first = instantiated, snd not, ...
%  then labeling (many rules of label cos have to enumerate
% try to see what sicstus do !! what constraint he inferered from some constraints
%  and mimic what he do, then add constraint, see what he do, mimic, ...

% must go to a normal form !!! otherwise too many combination to test

% test incrementally !! use label !! quite early to test
% use debug !! in common.pm
% engine first use simpagation ! so can lead to surprise
					
#endif
%##############################################################################
% Tests
%##############################################################################
#ifdef PM_TESTS

test "zebre1"  :-
	newvar A, 
	(in A 1 5) #=> soluce (true).

test "zebre2"  :-
	newvar A, 
	((in A 1 5) #=> labeling #=> soluce (format "A = ~p\n" [~A])), fail.

test "zebre3"  :-
	newvar A, newvar B,
	((domain [A,B] 1 5) #=> labeling #=> soluce (format "A = ~p B = ~p\n" [~A,~B])), fail.

test "zebre4"  :-
	newvar A, newvar B,
	((domain [A,B] 1 5) #=> A neq B #=> labeling #=>
	soluce (format "A = ~p B = ~p\n" [~A,~B])), fail.

test "zebre5"  :-
	newvar A, newvar B, newvar C,
	((domain [A,B,C] 1 5) #=> all_different [A,B,C] #=> labeling #=>
	soluce (format "A = ~p B = ~p C = ~p\n" [~A,~B,~C])), fail.

test "acplus1" :- ac_plus [1,2,3,4] [1,2,3,4] 1 XS YS,
	format "XS = ~p, YS = ~p" [~XS,~YS].

test "acaround" :- ac_around [1,2,3,4] [1,2,3,4] XS YS,
	format "XS = ~p, YS = ~p" [~XS,~YS].

% take only 5sec4 (yes sicstus take 0,1 but C++ take 6 hour !!!)
% try comment labeling to see how ac can be powerful to reduce a search space
test "ultime" :-
	%TODO a newvars
	newvar Red, newvar Green, newvar Yellow, newvar Blue, newvar White,
	Colors        = [Red, Green, Yellow, Blue, White],
	newvar Brit, newvar Sweed, newvar Dane, newvar Norvegian, newvar German,
	Nationalities = [Brit, Sweed, Dane, Norvegian, German],
	newvar Tea, newvar Coffee, newvar Milk, newvar Beer, newvar Water,
	Drinks        = [Tea, Coffee, Milk, Beer, Water],
	newvar Pall_mall, newvar Dunhill, newvar Blends, newvar Bluemaster, newvar Prince,
	Smokes        = [Pall_mall, Dunhill, Blends, Bluemaster, Prince],
	newvar Dogs, newvar Birds, newvar Cats, newvar Fish, newvar Horse,
	Pets          = [Dogs, Birds, Cats, Fish, Horse],
	
	X = [Colors, Nationalities, Drinks, Smokes, Pets],
	concat X All,
	%TODO do a flattern
	(domain Colors 1 5) #=>
	(domain Nationalities  1 5) #=>
	(domain Drinks  1 5) #=>
	(domain Smokes  1 5) #=>
	(domain Pets  1 5) #=>
	
	(all_different Colors) #=>
	(all_different Nationalities) #=>
	(all_different Drinks) #=>
	(all_different Smokes) #=>
	(all_different Pets) #=>
	(Brit eq Red) #=>
	(Sweed eq Dogs) #=>
	(Dane eq Tea) #=>
	(plus Green (cc 1) White) #=>
	(Green eq Coffee) #=>
	(Pall_mall eq Birds) #=>
	(Yellow eq Dunhill) #=>
	(Milk  eq (cc 3)) #=>
	(Norvegian eq (cc 1)) #=>
	(around Blends Cats) #=>
	(around Horse Dunhill) #=>
	(Bluemaster eq Beer) #=>
	(German eq Prince) #=>
 	(around Norvegian Blue) #=>
	(around Blends  Water) #=>
	labeling #=>
	(chr_store (store Store),
	 mappred (x\y\(sigma L\(member (ins x L) Store ?
			        format "Value: ~p\n" [~L]
			      ; format "Value: ~p\n" [~x]))
		) All _,
	soluce(true),
	fail).

#endif