(* ref-csp*)

fun deref x = !x;
(* Dereference a variable *)

val DEFAULT = ~999;

datatype ('a,'b,'c,'d) variable = Variable of ('a * 'b * 'c * 'd list);
(* A variable has a reference to a value ('a), a reference to a boolean
   ('b), a reference to a domain ('c) and a domain ('d list). 
   When the variable is bound to a value the boolean is set to true *);

fun make_var domain = Variable((ref DEFAULT),(ref false),(ref domain),domain);
(* Make a variable, with an initial value and a domain
   Note: we can now change attributes of the object, rather than
         create anew. *)

fun bind V x = let val Variable(v,s,_,_)=V in v:=x; s:=true; V end;
(* Bind the value x to the variable V. 
   Note: the use of multiple expressions delimited by ";"
   Note: the use of the assignment statement ":=" to change
         attributes.
   Note: the variable is instantiated with the value x and the status
         s is set to true, showing that the variable is instantiated
   Note: Delivers variable V as a result   *)

fun free V = let val Variable(v,s,_,_)=V in v:=DEFAULT; s:=false; V end;
(* Uninstantiate the variable V *)

fun boundp (Variable(_,s,_,_)) = !s;
(* Is the variable V assigned a value? 
   Note: !s means "dereference s and deliver its result *)

fun freep V = not(boundp V);
(* Is the variable V uninstantiated? *)

exception unbound_variable;
fun get_val V = 
    if freep V 
    then raise unbound_variable 
    else let val Variable(v,_,_,_) = V in !v end;
(* The value of the variable is dereferenced *)

fun get_current_domain (Variable(_,_,d,_)) = !d;
(* Get the current domain of the variable. Note use of "don't care"
    and dereferencing *)

datatype ('a,'b,'c,'d) constraint = 
        Constraint of (('a,'b,'c,'d)variable * 
                       ('d -> 'd -> bool) * 
                       ('a,'b,'c,'d)variable);
(* A constraint is composed of two ('a,'b,'c,'d)variables and a 
   binary predicate. The binary predicate takes as arguments a 'd and
   a 'd and delivers true or false. *);

fun make_con v1 r v2 = Constraint(v1,r,v2);
(* Make a constraint, from v1 to v2 over relation r *)

fun check (Constraint(v1,r,v2)) =
          r (get_val v1) (get_val v2);
(* Given a constraint, are the values assigned to the two
   variables consistent with the relation r *)

fun consistent [] v = true
   |consistent (c::cs) v = 
    let val (Constraint(v1,r,v2))=c
        val okay = not(v1=v) orelse freep v2 orelse check c
        in okay andalso consistent cs v end;
(* Given a variable v that has been asssigned a value, and a 
   set of constraints is v consistent *)


val x = make_var [1,2,3,4] and
    y = make_var [1,2,3,4] and
    z = make_var [1,2,3,4];

fun eq x y = x=y;
fun lt x y = x-y<0;
fun gt x y = y-x<0;

val c1 = make_con x eq y and
    c2 = make_con y eq x and
    c3 = make_con y gt z and
    c4 = make_con z lt y;

val okay = consistent [c1,c2,c3,c4];
(* partially applied function. *)

fun fm (p,f,s) =                     (*0*)
    let val c = hd f                 (*1*)
        val Variable(_,_,cd,_) = c   (*2*)
    in bind c (hd(!cd));             (*3*)
       cd := (tl(!cd));              (*4*)
       if okay c                     (*5*)
       then (c::p,tl f,true)         (*6*)
       else (p,f,false) end;         (*7*)
(* Make a forward move
   (0) p is the set of past variables, f is the set of future variables and s
       is a state. If s is true then all past variables are consistently 
       instantiated.
   (1) c is the current variable, that is the most recent future variable.
   (2) cd is the current domain of the current variable c.
   (3) the current variable is assigned the first value from 
       its current domain.
   (4) This value is removed from current domain.
   (5) If this assignment checks okay then do 6 otherwise do 7
   (6) c becomes a past variable and s is true.
   (7) s is false      *)

fun bm (p,f,s) =                     (*0*)
    let val c = hd f                 (*1*)
        val n = hd p                 (*2*)
        val Variable(_,_,cd,od) = c  (*3*)
    in free c;                       (*4*)
       cd:=od;                       (*5*)
       (tl p,n::f,s) end;            (*6*)
(* Make a backwards move 
   (1) c is current variable
   (2) n is the most recent past variable
   (3) cd is the current domain of c and o_d is the original domain of c
   (4) uninstantiate c
   (5) current domain of c becomed original domain of c.
   (6) n becomes the current variable.  *)

fun bt (p,[],s) = p                       (*0*)
   |bt (p,f,true) = bt(fm(p,f,true))      (*1*)
   |bt (p,f,false) =                      (*2*)
    let val c = hd f                      (*3*)
        val Variable(_,_,cd,_) = c        (*4*)
        in if !cd = []                    (*5*)
           then if p = []                 (*6*)
                then p                    (*7*)
                else bt(bm(p,f,false))    (*8*)
           else bt(fm(p,f,false)) end;    (*9*)
(* Backtracking
   (0) If there are no future variables then deliver the set of past
       variables as a result.
   (1) The state s is true, that is all past variables are
       consistently instantiated wrt the current variable. 
       Therefore make a forward move.
   (2) s is false. The instantiation of the current variable was
       inconsistent wrt the past variables.
   (3) c is the current variable
   (4) cd is the current domain of the current variable
   (7) current domain of c is empty and there are no past variables.
       Deliver [], there is no solution.
   (8) current domain of c is empty and there are past variables.
       Make a backwards move, uninstantiating the most recent past
       variable.
   (9) current domain of c is not empty, therefore try another
       instantiation of c  *)


(* Conclusions
   
Imperatives have been used, that is references and assignment
statements. This allows objects to be modified rather than created
anew. If this was not done it would have been necessary to perform
sequential searchers through the set of constraints and the set of
past variables to check for consistency. This would be wasteful in
both time and space. 

It may be argued that imperatives result in a less elegant
implementation. This may be so, but compare it to the implementation
that does not use imperatives! 

My view: the above problem can be encoded without references and
assignment statements (for example refer back to the graph search
algorithms). But ... I believe such an implementation is inefficient
(space and time) and more confused! I believe that you cannot go far
without :=
*)

(* Exercises:
   (1) Create a new problem and convince yourself that the above algorithm
       works. For example give it a problem that has no solution.
   (2) Create some data structure that allows you to implement 
       circular lists and some functions for stepping round this list.
   (3) Re-implement the graph search algorithms to use imperatives.
*)