(* CTM Chapter #09 Examples in Alice ML *)
import structure Space from "x-alice:/lib/gecode/Space"
import structure FS from "x-alice:/lib/gecode/FS"
import structure FD from "x-alice:/lib/gecode/FD"
import structure Search from "x-alice:/lib/gecode/Search"
import structure Linear from "x-alice:/lib/gecode/Linear"
import structure Explorer from "x-alice:/lib/tools/Explorer";

(* syntactic sugar for solutions using promises/futures *)
open Linear
open Promise
open Future
infix 3 ?=
val op?= = fulfill
val ? = future

(* Note:  I haven't figured out how to get a choice type statement in Alice ML.
In the meantime, I show how to use constraint programming (ala chapter #12)
to translate the examples *)

(* 9.1.1 The relational computation model - The choice and fail statements *)

(* Encoding: beige=0 coral=1 mauve=2 ochre=3 *)
fun suit sp =
   let
      val soft = FD.intvar(sp, #[(0,1)])
      val hard = FD.intvar(sp, #[(2,3)])
      val shirt = FD.intvar(sp, #[(0,3)])
      val pants = FD.intvar(sp, #[(0,3)])
      val socks = FD.intvar(sp, #[(0,3)])
   in
      Linear.distinct (sp, #[FD(shirt),FD(pants),FD(socks)], FD.BND);
      (* Need to figure out how to use FD.conj and FD.disj???
         FD.disj(sp, `true,
            FD.conj(sp, `true, shirt'>=hard, FD.conj(sp, `true, pants'>=soft, socks'<=hard)),
            FD.conj(sp, `true, shirt'<=soft, FD.conj(sp, `true, pants'<=hard, socks'>=soft))); *)
      branch (sp, #[FD(shirt),FD(pants),FD(socks)], FD.B_SIZE_MIN, FD.B_MIN);
      {shirt,pants,socks}
   end;
Explorer.exploreAll suit;
(* 8 Solutions
      suit(0 2 1)  suit(beige mauve coral)
      suit(0 3 1)  suit(beige ochre coral)
      suit(1 2 0)  suit(coral mauve beige)
      suit(1 3 0)  suit(coral ochre beige)
      suit(2 0 3)  suit(mauve beige ochre)
      suit(2 1 3)  suit(mauve coral ochre)
      suit(3 0 2)  suit(ochre beige mauve)
      suit(3 1 2)  suit(ochre coral mauve)
 *)

(* 9.1.4 The relational computation model - The Solve function *)
fun nrange sp =
   let
      val x = fdterm(sp, [``1, ``2, ``3])
   in
      branch (sp, #[x], FD.B_SIZE_MIN, FD.B_MIN);
      {x}
   end;
Explorer.exploreAll nrange;

(* 9.2.1 Further examples - Numeric examples *)
fun digit sp =
   let
      val x = fdterm(sp, [0 `# 9])
   in
      branch (sp, #[x], FD.B_SIZE_MIN, FD.B_MIN);
      {x}
   end;
Explorer.exploreAll digit;

fun twodigit sp =
   let
      val x = fdterm(sp, [0 `# 9])
      val y = fdterm(sp, [0 `# 9])
      val a = fdterm(sp, [0 `# 99])
   in
      post (sp, a `= x `+ `10 `* y, FD.DOM);
      branch (sp, #[a], FD.B_SIZE_MIN, FD.B_MIN);
      {a}
   end;
Explorer.exploreAll twodigit;

fun palindrome sp =
   let
      val a = FD.intvar(sp, #[(0,9999)])
      val b = FD.intvar(sp, #[(0,99)])
      val c = FD.intvar(sp, #[(0,99)])
      val x = FD.intvar(sp, #[(0,9)])
      val y = FD.intvar(sp, #[(0,9)])
   in
      (* post (sp, FD(a) `= FD(b) `* FD(c), FD.DOM); *)
      FD.mult (sp, b, c, a, FD.DOM);
      post (sp, FD(a) `= (FD(x) `* `1000) `+
                         (FD(y) `* `100) `+
                         (FD(y) `* `10) `+
                         FD(x), FD.DOM);
      post (sp, FD(a) `> `1000, FD.DOM);
      branch (sp, #[FD(x),FD(y),FD(b),FD(c)], FD.B_SIZE_MIN, FD.B_MIN);
      {a,x,y}
   end;
Explorer.exploreOne palindrome;

(* 9.2.1 Further examples - Puzzles and the n-queens problem *)

(* Alice ML code for queens was lifted from the lecture notes from
   Guido Tack and Marco Kuhlmann.  See:
      http://www.ps.uni-sb.de/courses/cp-ss05/
      http://www.ps.uni-sb.de/courses/cp-ss05/services.html *)

(* triangle n computes the upper triangular matrix with elements 0 <= i < j <= n *)
fun loop i n f = if i >= n then nil else f i :: loop (i + 1) n f
fun upperTriangle n = List.concat (loop 0 n (fn i => loop (i + 1) n (fn j => (i, j))))

(* n-queens problem *)
fun queens n sp =
   let
      val row = Linear.fdtermVec (sp, n, [0`#(n - 1)])
   in
      Linear.distinct (sp, row, FD.BND);
      List.app (fn (i, j) =>
         let
            val rowi = Vector.sub (row, i)
            val rowj = Vector.sub (row, j)
         in
            post (sp, rowi `+ (`j `- `i) `<> rowj, FD.BND);
            post (sp, rowi `- (`j `- `i) `<> rowj, FD.BND)
         end) (upperTriangle n);
      Linear.branch (sp, row, FD.B_SIZE_MIN, FD.B_MED);
      row
   end;
Explorer.exploreOne (queens 8);

(* n-queens problem, more efficient *)
fun betterqueens n sp =
   let
      val row = FD.rangeVec (sp, n, (0, n - 1))
      val add = Vector.tabulate (n, fn i => 0 + i)
      val sub = Vector.tabulate (n, fn i => 0 - i)
   in
      FD.distinct (sp, row, FD.BND);
      FD.distinctOffset (sp, VectorPair.zip (add, row), FD.BND);
      FD.distinctOffset (sp, VectorPair.zip (sub, row), FD.BND);
      FD.branch (sp, row, FD.B_SIZE_MIN, FD.B_MED);
      row
  end;
Explorer.exploreOne (betterqueens 8);