(*** ANALYZE.SML ***)

(* Analysis Types: Expressions either have type integer, boolean or
   a bad type *)
datatype atp = aint | abool | bad

(* A Context is a mapping from variables to analysis types *)
datatype context = Context of (variable -> atp);

(* Initial Context gives every variable a bad type *)
val init_cxt = Context(fn x => bad);

(* Cupdate is just like update for stores *)
fun Cupdate(Context C,v,t) = 
    Context(fn x=> if x=v then t else C x);

(* Cfetch is just like fetch for stores *)
fun Cfetch(v,Context C) = C v;


(*** TYPEOF - returns the type of an expression with respect to a context *)
fun typeof(IConstant n, Cxt) = aint
   |typeof(BConstant b, Cxt) = abool
   |typeof(Contents v, Cxt) = Cfetch(v,Cxt)
   |typeof(Minus(e1,e2), Cxt) = typeofBinaryArith(e1,e2, Cxt)
   |typeof(Plus(e1,e2), Cxt) = typeofBinaryArith(e1,e2, Cxt)
   |typeof(Times(e1,e2), Cxt) = typeofBinaryArith(e1,e2, Cxt)
   |typeof(Divide(e1,e2), Cxt) = typeofBinaryArith(e1,e2, Cxt)
   |typeof(Greater(e1,e2), Cxt)=typeofBinaryRelation(e1,e2,Cxt)
   |typeof(Less(e1,e2), Cxt) = typeofBinaryRelation(e1,e2, Cxt)
   |typeof(Equal(e1,e2), Cxt) = typeofBinaryRelation(e1,e2, Cxt)
   |typeof(And(e1,e2), Cxt) = typeofBinaryLogical(e1,e2, Cxt)
   |typeof(Or(e1,e2), Cxt) = typeofBinaryLogical(e1,e2, Cxt)
   |typeof(Not e1, Cxt) = typeofUnaryLogical(e1, Cxt)

and typeofBinaryArith(e1,e2, Cxt) = 
	let val t1 = typeof(e1, Cxt);
	    val t2 = typeof(e2, Cxt)
	in if (t1=aint andalso t2=aint) then aint else bad end

and typeofBinaryRelation(e1,e2, Cxt) = 
	let val t1 = typeof(e1, Cxt);
	    val t2 = typeof(e2, Cxt)
	in if (t1=aint andalso t2=aint) then abool else bad end

and typeofBinaryLogical(e1,e2, Cxt) = 
	let val t1 = typeof(e1, Cxt);
	    val t2 = typeof(e2, Cxt)
	in if (t1=abool andalso t2=abool) 
		then abool else bad end

and typeofUnaryLogical(e1, Cxt) = 
	let val t1 = typeof(e1, Cxt)
	in if t1=abool then abool else bad end

(*** ANALYZE: takes a program (command) and returns true if it is ***)
(***          properly formed					  ***)
fun analyze(Assign(V,E), Cxt) =
	let val Vtype = Cfetch(V,Cxt)
	    val te = typeof(E, Cxt)
	in not(te=bad) andalso (te = Vtype) end

   |analyze(Sequence(C1,C2), Cxt) =
	analyze(C1, Cxt) andalso analyze(C2, Cxt)

   |analyze(Conditional(E,C1,C2), Cxt) =
	typeof(E, Cxt) = abool andalso 
	analyze(C1, Cxt) andalso analyze(C2, Cxt)

   |analyze(While(E,C), Cxt) =
	typeof(E, Cxt) = abool andalso analyze(C, Cxt)

   |analyze(Print(Args), Cxt) =
	let fun checkargs nil = true
	       |checkargs (E::Es) =
		if typeof(E,Cxt) = bad 
		  then false else checkargs Es
	in checkargs Args end;