(*csp*)

(*
The constraint satisfaction problem (csp). What follows is an attempt
to encode a solution to the csp in ml. First a problem description.

In the csp we have a set of variables and a set of constraints.
Variables have a finite, and discrete, domain. A variable may be
assigned a value from its domain. A constraint is a triple, that is
<Vi,r,Vj>: a relation holds between variable Vi and Vj, namely r. 
For example we may have the constraint <Vi,<,Vj> (Vi must be less than
Vj). The problem is then to assign values to the variables such that
the constraints are satisfied.

*)

datatype 'a value = empty_val|Value of 'a;
(* A value, of a variable, is an 'a or is empty. *)

exception get_val_empty_val

fun get_val empty_val = raise get_val_empty_val
   |get_val (Value(x)) = x;
(* This is an example of error detection via exception handling *)

datatype ('a,'b) variable = Variable of ('a * 'b value * 'b list);
(* A variable has a name, a value and a domain. The value may be an 'b
   value if the variable is instantiated, otherwise the value is 
   empty_val. The domain is an 'a list *)

fun get_var_val (Variable(_,v,_)) = get_val v;
(* Given a variable, get its value. Note that (Variable(_,v,_)) means
"Get me the value v. I don't care about the name or the domain." *)

fun get_domain (Variable(_,_,d)) = d;
(* Get the domain of a variable *)

fun make_var name domain = Variable(name,empty_val,domain);
(* Create a new variable, with a given name and domain *)

fun eqvar (Variable(name1,_,_)) (Variable(name2,_,_)) = name1=name2;
(* infix eqvar; *)
(* Two variables are considered to be the same variable if they have 
   the same name. The binary predicate "eqvar" has been declared to be
"infix", allowing it to be used as an operator. *)

fun instantiated (Variable(_,empty_val,_)) = false
   |instantiated (Variable(_,(Value v),_)) = true;
(* Has the variable been assigned a value? *)

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

fun make_con v1 r v2 = Constraint(v1,r,v2);
(* make a constraint. The relation r acts from variable v1 to variable
   v2 *)

fun check (Constraint((Variable(_,v1,_)),r,(Variable(_,v2,_)))) =
          r (get_val v1) (get_val v2);
(* Check if the constraint is satisfied. That is does the relation r
   hold over the current instantiations of the two variables v1 and v2. *)

fun consistent [] v = true
   |consistent (c::cs) v =
    let val Constraint(v1,_,v2) = c
        val ok = not(eqvar v v1) orelse not(instantiated v2) orelse check c
    in ok andalso consistent cs v end;
(* Given a set of constraints and a recently instantiated variable v,
   determine if that instantiation is consistent with the constraints.
   A constraint is considered as being okay (satisfied) if it (a)
   does not involve v or (b) v2 is not instantiated or (c) it checks. *)

val x = make_var "x" [1,2] and 
    y = make_var "y" [1,2] and
    z = make_var "z" [1,2];
fun eq x y = x=y;
val c1 = make_con x eq y and
    c2 = make_con x eq z and
    c3 = make_con y eq z;

(* Some trial data *)

val okay = consistent [c1,c2,c3];
(* Note that "okay" is now a "partially applied" function. *)

val x = Variable("x",(Value 1),[1,2]) and
    y = Variable("y",(Value 2),[1,2]);

okay x;   (* What happened? *)