(* File cont/backtrack.sml 

   Towards modelling micro-Icon, a language where an expression can
   produce more than one result.  This version has no variables.
   sestoft@dina.kvl.dk * 2003-03-27

   The evaluation of an expression may fail (producing no value), or
   may succeed once (producing one value), or may succeed several
   times (producing many values), or indeed, infinitely many times.

   The constant expression 5 succeeds once with the value 5.

   The range expression 

      1 to 3

   succeeds three times, with the values 1 2 3.

   The expression 
   
      write(1 to 3) 

   succeeds three times, printing 1 2 3.

   Evaluating 

      write(1 to 3)

   just prints 1.  To force it to produce (and print) all its success
   values, evaluate

      every(write(1 to 3))     

   The expression 

      (1 to 3) + (4 to 6) 

   succeeds 9 times, with values 5 6 7 6 7 8 7 8 9.

   The expression 

      (1 to 3) & (4 to 6) 

   succeeds 9 times, with the values 4 5 6 4 5 6 4 5 6.  It produces
   all values of the second expression for each value of the first
   expression.

   The expression 

      (1 to 3) | (4 to 6) 

   succeeds 6 times, with the values 1 2 3 4 5 6.  It produces all
   values of the first expression, followed by all values of the
   second expression.

   The expression 

      (1 to 3) ; (4 to 6) 

   succeeds 3 times, with the values 4 5 6.  It does not backtrack
   into the expression before the semicolon.

   The expression 

      (1 to 0) ; (4 to 6) 

   succeeds 3 times, with the values 4 5 6.

   The expression 

      (4 < 3) 

   fails.  Icon does not have Boolean values, instead a failing
   expression is considered false, and a successful expression is
   considered true.  The operators `&' (and) and `|' (or) agree with
   this interpretation, and behave like the `&&' and `||' operators
   known from C/C++/Java/C#.

   The expression 

      (3 < 4) 

   succeeds once, with the value 4.

   The expression 

      (3 < (1 to 5)) 

   succeeds twice, with the values 4 5.

   This language can be implemented by evaluating expressions with two
   continuations:

      * A normal (or success) continuation which is given the
        expression's result in case of success, and a failure
        continuation to use in case of future failures.

      * A failure continuation that is invoked in case of failure.
        This continuation may also be called the backtracking
        continuation, or a resumption (it resumes the execution of a
        multi-result expression).

   Thus in 
   
      write(1 to 3) & ...

   the success continuation of (1 to 3) will print 1, but that success
   continuation also takes as argument a failure continuation, so that
   if the evaluation of ... fails, then it will go back to (1 to 3) to
   produce 2 and then print 2, and so on.  After the value 3 has been
   produced, further attempts to backtrack should fail (by calling the
   failure continuation of the entire expression).  
*)

app load ["Int"];

datatype expr = 
    CstI of int                         (* i                     *)
  | Write of expr                       (* write(e)              *)
  | Prim2 of string * expr * expr       (* e1+e2, e1*e2, e1<e2   *)
  | FromTo of int * int                 (* i to j                *)
  | And of expr * expr                  (* e1 & e2               *)
  | Or  of expr * expr                  (* e1 | e2               *)
  | Seq of expr * expr                  (* e1 ; e2               *)
  | If of expr * expr * expr            (* if e1 then e2 else e3 *)
  | Every of expr                       (* every(e)              *)
  | Fail                                (* &fail                 *)

(* Failure continuation and normal continuation *)

datatype answer =
    Success 
  | Failure of string;

type fcont = unit -> answer

type cont = int -> fcont -> answer

fun write i = (print (Int.toString i); print " ")

fun eval (e : expr) (cont : cont) (fcont : fcont) = 
    case e of
        CstI i       => cont i fcont
      | FromTo(i1, i2) => 
            let fun loop i = 
                    if i <= i2 then 
                        cont i (fn () => loop (i+1))
                    else 
                        fcont ()
            in loop i1 end
      | Write e      => 
            eval e (fn v => fn fcont1 => (write v; cont v fcont1))
                   fcont
      | If(e1, e2, e3) => 
            eval e1 (fn _ => fn fcont1 => eval e2 cont fcont1)
                    (fn () => eval e3 cont fcont)
      | Prim2(ope, e1, e2) => 
            eval e1 (fn v1 => fn fcont1 =>
                     eval e2 (fn v2 => fn fcont2 => 
                              case ope of
                                  "+" => cont (v1+v2) fcont2 
                                | "*" => cont (v1*v2) fcont2
                                | "<" => 
                                      if v1<v2 then 
                                          cont v2 fcont2
                                      else
                                          fcont2 ()
                                | _ => Failure "unknown prim2")
                          fcont1)
                    fcont
      | And(e1, e2) => 
            eval e1 (fn _ => fn fcont1 => eval e2 cont fcont1)
                    fcont
      | Or(e1, e2) => 
            eval e1 cont
                    (fn () => eval e2 cont fcont)
      | Seq(e1, e2) => 
            eval e1 (fn _ => fn fcont1 => eval e2 cont fcont)
                    (fn () => eval e2 cont fcont)
      | Every e => 
            eval e (fn _ => fn fcont1 => fcont1 ())
                   (fn () => cont 0 fcont)
      | Fail => fcont ()

fun run e = 
    eval e (fn v => fn _ => Success) (fn () => Failure "no result");

val ex1 = Seq(Write (FromTo(1, 3)), Fail);

val ex2 = And(Write (FromTo(1, 3)), Fail);

val ex3and = And(Write(And(FromTo(1, 3), FromTo(4, 6))), Fail);

val ex3or  = And(Write(Or(FromTo(1, 3), FromTo(4, 6))), Fail);

val ex3seq = And(Write(Seq(FromTo(1, 3), FromTo(4, 6))), Fail);

val ex4 = Write(And(FromTo(1, 3), And(FromTo(4, 6), CstI 666)));

val ex5 = Every (Write (FromTo(1, 3)));

val ex6 = And(Every (Write (FromTo(1, 3))), FromTo(4, 6));

val ex7 = Every(Write(Prim2("+", FromTo(1,3), FromTo(4, 6))));

val ex8 = Write(Prim2("<", CstI 4, FromTo(1, 10)));

val ex9 = Write(If(Prim2("<", CstI 5, CstI 4), CstI 11, CstI 22));