(* CTM Chapter #02 Examples in Alice ML *)
(* syntactic sugar for solutions using promises/futures *)
open Promise
open Future
infix 3 ?=
val op?= = fulfill
val ? = future

(* 2.1.1 Language syntax *)
fun fact 0 = 1
  | fact n = n * fact (n-1);

(* 2.3.5 Basic operations *)

(* solution using state variables *)
   let
      val x = 5
      val y = 10
      val t = (x >= y)
      val z = ref 0
   in
      if (t)
         then z := x
         else z := y
   end;

   let
      val x = 5
      val y = 10
      val z = ref 0
   in
      if (x >= y)
         then z := x
         else z := y
   end;
(* end solution using state variables *)

(* solution using promises/futures *)
   let
      val x = 5
      val y = 10
      val t = (x >= y)
      val z = promise()
   in
      if (t)
         then z ?= x
         else z ?= y
   end;

   let
      val x = 5
      val y = 10
      val z = promise()
   in
      if (x >= y)
         then z ?= x
         else z ?= y
   end;
(* end solution using promises/futures *)

(* 2.4.1 Basic concepts *)
let
   val a = 11
   val b = 2
   val c = a + b
   val d = c * c
in
   inspect d
end;

let
   val x = 1
in
   let
      val x = 2
   in
      inspect x
   end;
   inspect x
end;

(* solution using state variables *)
   val c = ref 0;
   fun max x y z =
      if (x >= y)
         then z := x
         else z := y;
   max 3 5 c;

   val c = ref 0;
   val y = 5;
   fun lb x z =
      if (x >= y)
         then z := x
         else z := y;
   lb 3 c;

   let
      val y = 10;
      fun lb x z =
         if (x >= y)
            then z := x
            else z := y
   in
      let
         val y = 15;
         val z = ref 0
      in
         lb 5 z
      end
   end;
(* end solution using state variables *)

(* solution using promises/futures *)
   val c = promise();
   fun max x y z =
      if (x >= y)
         then z ?= x
         else z ?= y;
   max 3 5 c;

   val c = promise();
   val y = 5;
   fun lb x z =
      if (x >= y)
         then z ?= x
         else z ?= y;
   lb 3 c;

   let
      val y = 10;
      fun lb x z =
         if (x >= y)
            then z ?= x
            else z ?= y
   in
      let
         val y = 15
         val z = promise()
      in
         lb 5 z
      end
   end;
(* end solution using promises/futures *)

let
   fun q x = (inspect ("stat(" ^ x ^ ")"))
   fun p x = q x
in
   let
      fun q x = (inspect ("dyn(" ^ x ^ ")"))
   in
      p "hello"
   end
end;

(* solution using state variables *)
   let
      val x = 10
      val y = spawn 99
      val z = ref 0
   in
      if (x >= y)
         then z := x
         else z := y
   end;
(* end solution using state variables *)

(* solution using promises/futures *)
   let
      val x = 10
      val y = spawn 99
      val z = promise()
   in
      if (x >= y)
         then z ?= x
         else z ?= y
   end;
(* end solution using promises/futures *)

(* 2.4.3 Nonsuspendable statements *)

(* solution using state variables *)
   local
      val res = ref (IntInf.fromInt(0))
   in
      local
         val arg1 = IntInf.fromInt(111 * 111)
         val arg2 = IntInf.fromInt(222 * 222)
         val _ = res := arg1 * arg2
      in
      end;
      val _ = inspect (!res);
   end;

   let
      val y = 10
      val z = ref 0
   in
      let
         fun lowerBound x z =
            if (x >= y)
               then z := x
               else z := y
      in
         lowerBound 5 z
      end
   end;
(* end solution using state variables *)

(* solution using promises/futures *)
   local
      val res = promise()
   in
      local
         val arg1 = IntInf.fromInt(111 * 111)
         val arg2 = IntInf.fromInt(222 * 222)
         val _ = res ?= arg1 * arg2
      in
      end;
      val _ = inspect res;
   end;

   let
      val y = 10;
      val z = promise()
   in
      let
         fun lowerBound x z =
            if (x >= y)
               then z ?= x
               else z ?= y
      in
         lowerBound 5 z
      end
   end;
(* end solution using promises/futures *)

(* 2.4.5 Basic concepts revisited *)

(* solution using state variables *)
   let
      fun max x y z =
         if (x >= y)
            then z := x
            else z := y
   in
      let
         val c = ref 0
      in
         max 3 5 c
      end
   end;

   let
      val y = 5;
      fun lowerBound x z =
         if (x >= y)
            then z := x
            else z := y
   in
      let
         val c = ref 0
      in
         lowerBound 33 c
      end
   end;

   let
      val y = 5;
      fun lowerBound x z =
         if (x >= y)
            then z := x
            else z := y
   in
      let
         val y = 10
         val c = ref 0
      in
         lowerBound 33 c
      end
   end;
(* end solution using state variables *)

(* solution using promises/futures *)
   let
      fun max x y z =
         if (x >= y)
            then z ?= x
            else z ?= y
   in
      let
         val c = promise()
      in
         max 3 5 c
      end
   end;

   let
      val y = 5
      fun lowerBound x z =
         if (x >= y)
            then z ?= x
            else z ?= y
   in
      let
         val c = promise()
      in
         lowerBound 33 c
      end
   end;

   let
      val y = 5
      fun lowerBound x z =
         if (x >= y)
            then z ?= x
            else z ?= y
   in
      let
         val y = 10
         val c = promise()
      in
         lowerBound 33 c
      end
   end;
(* end solution using state variables *)

(* 2.5.1 Last call optimization *)
fun loop10 i =
   if (i = 10)
      then
         ()
      else
         (
            inspect i;
            loop10 (i+1)
         );
val i = loop10 0;

(* 2.5.4 Garbage collection is not magic *)
fun upto m n =
   if (m > n)
      then []
      else m :: upto (m+IntInf.fromInt(1))  n;
val lst = upto (IntInf.fromInt(1)) (IntInf.fromInt(1000000));

fun sum x lst1 lst : IntInf.t =
   case lst1 of
       n::ns => sum (x+n) ns lst
     | _     => x;

(* warning: this generates tons of garbage *)
(*inspect (sum (IntInf.fromInt(0)) lst lst));*)

fun sum x lst : IntInf.t =
   case lst of
       n::ns => sum (x+n) ns
     | _     => x;

inspect (sum (IntInf.fromInt(0)) lst);

(* 2.6.1 Syntactic conveniences *)
datatype person = Person of { name:string, age:int };
Person{ name="George", age=25 };
let
   val a = "George"
   val b = 25
   val x = Person{ name=a, age=b }
in
   x
end;

datatype tree = Tree of { key:int, left:int, right:int, value:int };
val t = { key=1, left=2, right=3, value=4 };
let
   val { key=a, left=b, right=c, value=d } = t
in
   t
end;

11*11;
val x = 11*11;
Math.sqrt(5.0);

let
   val xs = [5,6]
   val ys = [3,4]
in
   case (xs, ys) of
       (nil, ys) => 1
     | (xs, nil) => 2
     | (x::xr, y::yr) if (x <= y) => 3
     | _ => 4
end;

let
   val xs = [5,6]
   val ys = [3,4]
in
   case xs of
       nil => 1
     | _   =>
         case ys of
             nil => 2
           | _ =>
               case xs of
                   x::xr => (
                     case ys of
                         y::yr =>
                           if (x <= y)
                              then 3
                              else 4
                       | _ => 4)
                 | _ => 4
end;

(2 = 2) andalso (4 = 4);
if (2 = 2) then (4 = 4) else false;

(2 = 2) orelse (4 = 4);
if (2 = 2) then true else (4 = 4);

(* don't think that alice has a correlary to nesting markers ($)
      Oz:   {Browse {Obj get($)}} *)

(* solution using state variables *)
   let
      fun obj z = z
      fun get z = z := 1234
      val x = ref 0
   in
      obj (get x);
      inspect (!x)
   end;
(* end solution using state variables *)

(* solution using promises/futures *)
   let
      fun obj z = z
      fun get z = z ?= 1234
      val x = promise()
   in
      obj (get x);
      inspect (?x)
   end;
(* end solution using promises/futures *)

(* 2.6.2 Functions *)
fun max x y =
   if (x >= y)
      then x
      else y;

(* solution using state variables *)
   val r = ref 0;
   fun max x y =
      r := (
         if (x >= y)
            then x
            else y);

   val r = ref 0;
   fun max x y =
      if (x >= y)
         then r := x
         else r := y;
(* end solution using state variables *)

(* solution using promises/futures *)
   val r = promise();
   fun max x y =
      r ?= (
         if (x >= y)
            then x
            else y);

   val r = promise();
   fun max x y =
      if (x >= y)
         then r ?= x
         else r ?= y;
(* end solution using promises/futures *)

fun f x = x*x;
val x = 2;
val xr = [1, 2, 3, 4];
val ys = f x :: map f xr;

let
   fun f x = x*x
   val x = 2
   val xr = [1, 2, 3, 4]
in
   let
      val y = f x
      val yr = map f xr
   in
      y::yr
   end
end;

fun map' f xs =
   case xs of
       nil => nil
     | x::xr => (f x)::(map f xr);
inspect (map (fn (x) => (x * x)) [1, 2, 3, 4]);

let
   fun f x = x*x
   val x = 2
   val xr = [1, 2, 3, 4]
   val p = promise()
   fun map' f xs p =
      case xs of
          nil => fulfill(p, nil)
        | x::xs =>
            let
               val p' = promise()
               val y  = f x
               val yr = future p'
            in
               fulfill(p, y::yr);
               map' f xs p'
            end
in
   map' f xr p;
   future p
end;

(* 2.6.3 Interactive interface *)
val px = promise()
and py = promise();
val x = future(px)
and y = future(py);

val px = promise()
and py = promise();
val x = future(px)
and y = future(py);
fulfill(px, 25);
datatype person = Person of { name:string, age:int };
val pa = promise();
val a = promise();
fulfill(pa, Person{ name="", age=25 });
val px = promise()
and py = promise();
val x = future(px)
and y = future(py);

let
   val px = promise()
   and py = promise()
   val x = future(px)
   and y = future(py)
in
   ()
end;

inspect 1;

let
   val py = promise()
   val y = future(py)
in
   inspect y
end;

let
   val pa = promise()
   and pb = promise()
   and pc = promise()
   val a = future(pa)
   and b = future(pb)
   and c = future(pc)
in
   spawn fulfill(pa, 10);
   spawn fulfill(pb, 200);
   fulfill(pc, a + b);
   inspect c
end;

(* 2.7.1 Exceptions - Motivation and basic concepts *)
datatype 'a expression = Number of 'a
                       | Plus  of 'a expression * 'a expression
                       | Minus of 'a expression * 'a expression
                       | Times of 'a expression * 'a expression;
exception IllFormedExpr of string;
fun toString(Number(x))   = "Number(" ^ Int.toString(x) ^ ")"
  | toString(Plus(x, y))  = "Plus("  ^ toString(x) ^ ", " ^ toString(y) ^ ")"
  | toString(Minus(x, y)) = "Minus(" ^ toString(x) ^ ", " ^ toString(y) ^ ")"
  | toString(Times(x, y)) = "Times(" ^ toString(x) ^ ", " ^ toString(y) ^ ")";
fun isNumber(Number(x)) = true
  | isNumber(_) = false;
fun getNumber(Number(x)) = x
  | getNumber(e) = raise IllFormedExpr(toString(e));

fun eval e =
   if (isNumber(e))
      then getNumber(e)
      else
         case e of
             Plus  (x, y) => (eval x) + (eval y)
           | Times (x, y) => (eval x) * (eval y)
           | _            => raise IllFormedExpr(toString(e));

(
   inspect (eval(Plus(Plus(Number(5), Number(5)), Number(10))));
   inspect (eval(Times(Number(6), Number(11))));
   inspect (eval(Minus(Number(7), Number(10))))
) handle IllFormedExpr(e) => inspect ("*** Illegal Expression: '" ^ e ^ "' ***");

(* 2.7.3 Exceptions - Full syntax *)
exception FileNotFound;
fun processFile f = raise FileNotFound;
fun closeFile f = ();
fun toString(FileNotFound) = "FileNotFound"
  | toString(_) = "Unknown";

processFile "myfile"
   handle failure => ()
   finally closeFile "myfile";

processFile "myfile"
   handle failure => inspect ("*** Exception '" ^ toString(failure) ^ "' when Processing File")
   finally closeFile "myfile";

(* 2.7.4 Exceptions - Full syntax *)
fun one() = 1;
fun two() = 2;
(* compiler catches bind type errors *)
(* ({one} = {two}) handle failure => inspect ("caughtFailure"); *)

(* 2.8.1 Functional programming languages *)
fun $ x = x * x;

fun isNil x = (x = nil);
fun isCons (h::t) = true
  | isCons nil = false;
fun car (h::t) = h
  | car nil = nil;
fun cdr (h::t) = t
  | cdr nil = nil;
fun cons (h, t) = h::t;

val rec append = fn (xs, ys) =>
   if (isNil xs)
      then ys
      else cons(car xs, append((cdr xs), ys));

(* 2.8.2.1 Unification (the = operator) *)

(* Unify functions for Alice *)
exception Unify
fun isFulfilled p = not(Future.isFuture(future p))
fun known x =
   let
      val p = promise()
   in
      fulfill(p, x); p
   end
fun unifyPromise unifyContent (p1, p2) =
   if (p1 = p2)
      then ()
      else
         case (isFulfilled p1, isFulfilled p2)
          of (false, _) => fulfill(p1, future p2)
           | (_, false) => fulfill(p2, future p1)
           | (true, true) => unifyContent(future p1, future p2)
fun unifySimple(x, y) = if x = y then () else raise Unify
fun unifyList unifyElem (nil, nil) = ()
  | unifyList unifyElem (x::xs, y::ys) =
      (unifyElem(x,y); unifyList unifyElem (xs,ys))
  | unifyList unifyElem _ = raise Unify;
unifyList unifySimple ([1,2,3], [1,2,3]);    (* example usage *)

(* Person datatype used in the examples *)
datatype person = Person of {name : string promise, age : int promise}
fun unifyPerson(Person{name, age}, Person{name=name', age=age'}) = (
   unifyPromise unifySimple (name, name');
   unifyPromise unifySimple (age, age'))

(* Bindings to values *)
val x = Person{name=promise(), age=promise()}
val y = x

(* Unification is symetric *)
val x1 = promise()
val x2 = promise()
val x = Person{name=x1, age=x2};
unifyPerson(x, Person{name=x1, age=x2});

(* Any two partial values can be unified *)
unifyPerson(Person{name=promise(), age=promise()},
            Person{name=known "George", age=known 25});

(* If partial values are already equal, then unification does nothing *)
unifyPerson(Person{name=known "George", age=known 25},
            Person{name=known "George", age=known 25});

(* If partial values are incompatible, then they cannot be unified *)
unifyPerson(Person{name=promise(), age=known 26},
            Person{name=known "George", age=known 25})
   handle Unify => ();

(* Unification is symmetric in the arguments *)
unifyPerson(Person{name=known "George", age=promise()},
            Person{name=promise(), age=known 25});

(* Unification can create cyclic structures *)
datatype person' = Person' of {grandfather : person' promise}
fun unifyPerson'(Person'{grandfather}, Person'{grandfather=grandfather'}) =
      unifyPromise unifyPerson' (grandfather, grandfather')
val x = promise();
unifyPromise unifyPerson' (x, known(Person'{grandfather=x}));

(* Unification can bind cyclic structures *)
datatype t = F of {a : t promise, b : t promise}
fun unifyF (F{a, b}, F{a=a', b=b'}) =
      (unifyPromise unifyF (a,a');
       unifyPromise unifyF (b,b'))
val x = promise();
unifyPromise unifyF (x, known(F{a=x, b=promise()}));
val y = promise();
unifyPromise unifyF (y, known(F{a=promise(), b=y}));
unifyPromise unifyF (x, y);

(* 2.8.2.2 The unification algorithm *)
datatype foo = Foo of {a : int promise}
fun unifyFoo(Foo{a}, Foo{a=a'}) = (unifyPromise unifySimple (a, a'))

val x8 = promise()
val x7 = x8
val x6 = promise()
val x5 = promise()
val x4 = x5
val x3 = x4
val x2 = known 25;
val x1 = known (Foo{a=x2});

val x1 = promise()
val x2 = promise()
val x3 = promise()
val x4 = promise()
val x5 = promise()
val x6 = promise()
val x7 = promise()
val x8 = promise();

unifyPromise unifySimple (x1, known(Foo{a=x2}));
unifyPromise unifySimple (x2, known(25));
unifyPromise unifyFoo (x3, x6);
unifyPromise unifyFoo (x4, x6);
unifyPromise unifyFoo (x5, x6);
unifyPromise unifyFoo (x7, known(Foo{a=x2}));
unifyPromise unifyFoo (x8, known(Foo{a=x2}));

datatype foo = Foo of {a : foo promise}
fun unifyFoo(Foo{a}, Foo{a=a'}) = (unifyPromise unifySimple (a, a'))

datatype t = F of {a : t promise}
fun unifyF (F{a}, F{a=a'}) = unifyPromise unifyF (a,a')
val x = promise();
val y = promise();
unifyPromise unifyF (x, known(F{a=x}));
unifyPromise unifyF (y, known(F{a=y}));
(* loops forever on unify *)
(* unifyPromise unifyF (x, y); *)

(* 2.8.2.3 Displaying cyclic structures *)

(* ctm plays fast and loose with types in this section *)
(* not gonna spend much time getting these correct     *)
datatype t = F of {a : t promise, b : t promise}
fun unifyF (F{a, b}, F{a=a', b=b'}) =
      (unifyPromise unifyF (a,a');
       unifyPromise unifyF (b,b'))
val x = promise();
val y = promise();
val z = promise();
unifyPromise unifyF (known(F{a=x, b=promise()}), known(F{a=promise(), b=y}));
unifyPromise unifyF (z, known(F{a=z, b=promise()}));
inspect [x, y, z];

datatype t = A of {a : t promise, b : t promise, c : t promise}
fun unifyA (A{a, b, c}, A{a=a', b=b', c=c'}) =
      (unifyPromise unifyA (a,a');
       unifyPromise unifyA (b,b');
       unifyPromise unifyA (c,c'))
val x = promise();
val y = promise();
val z = promise();
(*unifyPromise unifyA (known(A{a=x, b=z, c=z}), known(A{a=y, b=y, c=x}));*)
inspect [x, y, z];

(* 2.8.2.4 Entailment and disentailment checks (the == and \= operations *)

val head = 1;
val tail = 2::nil;
val l1 = known(head::tail);
val l2 = known([1,2]);
val l3 = known(1::2::nil);
inspect (future(l1) = future(l2));
inspect (future(l1) = future(l3));

val x  = promise();
val l1 = known([1]);
val l2 = known([future(x)]);
fulfill(x, 1);  (* will wait if this line removed *)
inspect (future(l1) = future(l2));

val x  = promise();
val l1 = known([future(x)]);
val l2 = known([future(x)]);
fulfill(x, 1);  (* will wait if this line removed *)
inspect (future(l1) = future(l2));

val x  = promise();
val l1 = known([1, future(promise())]);
val l2 = known([future(x), future(promise())]);
(*inspect (future(l1) = future(l2));*)

(* Alternate implementation of Unify *)
(* first stab at Unify in Alice - Andreas provided the cleaner solutions listed above *)

   (* Unify functions for Alice *)
   signature UNIFY =
      sig
         exception Unify
         val clear      : unit -> unit
         val unify      : unit -> unit
         val bind       : 'a Promise.promise * 'a -> unit
         val predicate  : 'a
                        * ('a * 'a -> bool)
                        * 'a
                        * 'a Promise.promise option
                        * 'a Promise.promise option
                        -> unit
      end
   structure Unify :> UNIFY =
      struct
         open Promise
         open Future
         exception Unify
         val store =  ref []
         fun addStore(f) = store := f::(!store)
         fun clear() = store := [];
         fun unify() =
            let
               fun unifyStore (f::fs) =
                     let
                        val _ = f()
                     in
                        unifyStore(fs)
                     end
                 | unifyStore nil = ()
            in
               unifyStore(!store)
            end
         fun bind(px:'a promise, x:'a) =
            let
               val _ = fulfill(px, x) handle failure => raise Unify
            in
               unify()
            end
         fun predicate(
            x   : 'a,
            opn : 'a * 'a -> bool,
            y   : 'a,
            px  : 'a promise option,
            py  : 'a promise option) = (
            if (op= = opn)
               then addStore(
                  fn () => (
                     if (not(isFuture(x)) orelse isFuture(y) orelse not(isSome(px)))
                        then ()
                        else bind(valOf(px), y);
                     if (isFuture(x) orelse not(isFuture(y)) orelse not(isSome(py)))
                        then ()
                        else bind(valOf(py), x);
                     if (isFuture(x) orelse isFuture(y))
                        then ()
                        else
                           if (x = y)
                              then ( (* can remove this function from store here *) )
                              else raise Unify))
               else addStore(
                  fn () =>
                     if (isFuture(x) orelse isFuture(y))
                        then ()
                        else
                           if opn(x, y)
                              then ( (* can remove this function from store here *) )
                              else raise Unify))
      end

   (* example usage of Unify *)
   val px = promise();
   val x  = future(px);
   val py = promise();
   val y  = future(py);
   Unify.predicate(x, op=, y, SOME px, SOME py);
   Unify.predicate(x, op<, 125, NONE, NONE);
   Unify.predicate(x, op>, 100, NONE, NONE);
   Unify.predicate(x, op=, y, NONE, NONE);
   Unify.bind(px, 123);
   Unify.predicate(x, op<>, y, NONE, NONE);
   Unify.unify() handle Unify.Unify => Unify.clear();

   (* Person datatype used for examples *)
   datatype person = Person of {name:string, age:int}
   fun unifyPerson(
      Person{name=name1, age=age1},
      Person{name=name2, age=age2},
      pname1,
      page1,
      pname2,
      page2) = (
         Unify.predicate(name1, op=, name2, pname1, pname2);
         Unify.predicate(age1,  op=, age2,  page1,  page2);
         Unify.unify()
      );

   (* bindings to values *)
   val px1 = promise();
   val px2 = promise();
   val x1  = future(px1);
   val x2  = future(px2);
   val x = Person{name=x1, age=x2};
   val y = x;

   (* Unification is symetric *)
   val px1 = promise();
   val px2 = promise();
   val x1  = future(px1);
   val x2  = future(px2);
   val x = Person{name=x1, age=x2};
   unifyPerson(x, Person{name=x1, age=x2}, SOME px1, SOME px2, NONE, NONE);

   (* Any two partial values can be unified *)
   val px1 = promise();
   val x1  = future(px1);
   val px2 = promise();
   val x2  = future(px2);
   unifyPerson(
      Person{name=x1, age=x2},
      Person{name="George", age=25}, SOME px1, SOME px2, NONE, NONE);

   (* If partial values are already equal, then unification does nothing *)
   val x = Person{name="George", age=25};
   val y = Person{name="George", age=25};
   unifyPerson(x, y, NONE, NONE, NONE, NONE);

   (* If partial values are incompatible, then they cannot be unified *)
   val px1 = promise();
   val x1  = future(px1);
   unifyPerson(
      Person{name=x1, age=26},
      Person{name="George", age=25}, SOME px1, NONE, NONE, NONE)
      handle Unify.Unify => Unify.clear();

   (* Unification is symetric in the arguments *)
   val px1 = promise();
   val px2 = promise();
   val x1  = future(px1);
   val x2  = future(px2);
   unifyPerson(
      Person{name=x1, age=25},
      Person{name="George", age=x2}, SOME px1, NONE, NONE, SOME px2);

   (* Unification can create cyclic structures *)
   datatype person_cyclic = PersonCyclic of {grandfather:person_cyclic}
   val px = promise();
   val x = future(px);
   Unify.bind(px, PersonCyclic{grandfather=x});
   (* note: this one was tricksie. the following causes grief. *)
   val px = promise();
   val x  = future(px);
   Unify.predicate(x, op=, PersonCyclic{grandfather=x}, SOME px, NONE);
   (* Unify.unify(); *)  (* uncomment this code see effect *)
   Unify.clear();

   (* Unification can bind cyclic structures *)
   datatype person_cyclic = PersonCyclic of {a:person_cyclic, b:person_cyclic}
   val px = promise();
   val py = promise();
   val x  = future(px);
   val y  = future(py);
   Unify.bind(px, PersonCyclic{a=x, b=y});
   (* Unify.bind(py, PersonCyclic{a=x, b=y}); *)      (* Causes grief in Alice 1.2 *)
(* end first stab at Unify in Alice *)