type var = string;

datatype IExpr = INT of int
                |VAR of var
                |PLUS of IExpr*IExpr
                |MINUS of IExpr*IExpr
                |MULT of IExpr*IExpr
                |DIV of IExpr*IExpr
                |MOD of IExpr*IExpr
                |LET of IExpr*IExpr*IExpr
                |ERR of IExpr

signature Env = 
sig
type env;
val varval : env*IExpr -> IExpr;
val upd    : env*(IExpr*IExpr) -> env;
end;

structure env:Env = 
struct
type env = (IExpr*IExpr) list

fun upd([],(VAR(x),y:IExpr)) = (VAR(x),y)::[]
   |upd((VAR(a),b)::L,(VAR(x),y)) = if a=x then (VAR(a),y)::L
                                 else (VAR(a),b)::upd(L,(VAR(x),y))

fun varval((VAR(a),b)::L,VAR(x)) = if x = a then b
                                  else varval(L,VAR(x))

end


signature rules =
sig
type rules;
val defrules : env.env*IExpr -> (IExpr*string)
end; 

structure r:rules = 
struct

type rules = IExpr*env.env*IExpr*string
 
 fun defrules(G:env.env,INT(a)) = (INT(a),"Integer")
    |defrules(G,VAR(a)) = (env.varval(G,VAR(a)),"Variable Substitution")
    
    |defrules(G,PLUS(x,ERR(a))) = (ERR(a)," PlusError")
    |defrules(G,PLUS(ERR(a),x)) = (ERR(a),"PlusError")
    |defrules(G,PLUS(INT(a),INT(b))) = (INT(a+b),"PLUS0")
    |defrules(G,PLUS(INT(a),x)) = (PLUS(INT(a),#1(defrules(G,x))),"PLUSRightEval"^"\n"^(#2(defrules(G,x))))
    |defrules(G,PLUS(x,y)) = (PLUS(#1(defrules(G,x)),y),"PLUSLeftEval"^"\n"^(#2(defrules(G,x))))

    |defrules(G,MINUS(x,ERR(a))) = (ERR(a),"MinusError")
    |defrules(G,MINUS(ERR(a),x)) = (ERR(a),"MinusError")
    |defrules(G,MINUS(INT(a),INT(b))) = (INT(a-b),"MINUS0")
    |defrules(G,MINUS(INT(a),x)) = (MINUS(INT(a),#1(defrules(G,x))),"MINUSRightEval"^"\n"^(#2(defrules(G,x))))
    |defrules(G,MINUS(x,y)) = (MINUS(#1(defrules(G,x)),y),"MINUSLeftEval"^"\n"^(#2(defrules(G,x))))

    |defrules(G,MULT(x,ERR(a))) = (ERR(a),"MultError")
    |defrules(G,MULT(ERR(a),x)) = (ERR(a),"MultError")
    |defrules(G,MULT(INT(a),INT(b))) = (INT(a*b),"MULT0")
    |defrules(G,MULT(INT(a),x)) = (MULT(INT(a),#1(defrules(G,x))),"MULTRightEval"^"\n"^(#2(defrules(G,x))))
    |defrules(G,MULT(x,y)) = (MULT(#1(defrules(G,x)),y),"MULTLeftEval"^"\n"^(#2(defrules(G,x))))

    |defrules(G,DIV(x,ERR(a))) = (ERR(a),"DivError")
    |defrules(G,DIV(ERR(a),x)) = (ERR(a),"DivError")
    |defrules(G,DIV(x,INT(0))) = (ERR(DIV(x,INT(0))),"DivError")
    |defrules(G,DIV(INT(a),INT(b))) = (INT(a div b),"DIV0")
    |defrules(G,DIV(INT(a),x)) = (DIV(INT(a),#1(defrules(G,x))),"DIVRightEval"^"\n"^(#2(defrules(G,x))))
    |defrules(G,DIV(x,y)) = (DIV(#1(defrules(G,x)),y),"DIVLeftEval"^"\n"^(#2(defrules(G,x))))

    |defrules(G,MOD(x,ERR(a))) = (ERR(a),"ModError")
    |defrules(G,MOD(ERR(a),x)) = (ERR(a),"ModError")
    |defrules(G,MOD(x,INT(0))) = (ERR(MOD(x,INT(0))),"ModError")
    |defrules(G,MOD(INT(a),INT(b))) = (INT(a mod b),"MOD0")
    |defrules(G,MOD(INT(a),x)) = (MOD(INT(a),#1(defrules(G,x))),"MODRightEval"^"\n"^(#2(defrules(G,x))))
    |defrules(G,MOD(x,y)) = (MOD(#1(defrules(G,x)),y),"MODLeftEval"^"\n"^(#2(defrules(G,x))))


    
    |defrules(G,LET(VAR(x),y,INT(b))) = (INT(b),"LET0")
    |defrules(G,LET(VAR(x),y,ERR(a))) = (ERR(a),"LetError")
    |defrules(G,LET(VAR(x),INT(a),y)) = 
     (LET(VAR(x),INT(a),#1(defrules(env.upd(G,(VAR(x),INT(a))),y))),"LETRightEval"^"\n"^(#2(defrules(env.             upd(G,(VAR(x),INT(a))),y))))
    |defrules(G,LET(VAR(x),ERR(a),y)) = 
     (LET(VAR(x),ERR(a),#1(defrules(env.upd(G,(VAR(x),ERR(a))),y))),"LETRightEval"^"\n"^(#2(defrules(env.             upd(G,(VAR(x),ERR(a))),y))))
    |defrules(G,LET(VAR(x),y,z)) = (LET(VAR(x),#1(defrules(G,y)),z),"LETLeftEval"^"\n"^(#2(defrules(G,y))))
    |defrules(G,LET(x,y,z)) = (ERR(LET(x,y,z)),"No Var in LET")


 
end



signature proofs =
sig

type proofs;
val evaluate : IExpr -> unit;
end;

structure Proofs:proofs = 
struct

type proofs = unit

fun rm(x,[]) = []
    |rm(x,a::L:string list) = if x=a then rm(x,L) 
                         else a::rm(x,L)

fun findvars(INT(a),L:string list) = L
   |findvars(VAR(x),L) = L@x::[]
   |findvars(ERR(a),L) = findvars(a,L)
   |findvars(PLUS(a,b),L) = findvars(a,L)@findvars(b,L)
   |findvars(MINUS(a,b),L) = findvars(a,L)@findvars(b,L)
   |findvars(MULT(a,b),L) = findvars(a,L)@findvars(b,L)
   |findvars(DIV(a,b),L) = findvars(a,L)@findvars(b,L)
   |findvars(MOD(a,b),L) = findvars(a,L)@findvars(b,L)
   |findvars(LET(VAR(x),y,z),L) = findvars(y,L)@rm(x,findvars(z,L))
   |findvars(LET(x,y,z),L) = findvars(y,L)@findvars(z,L)

fun p([]) = ""
    |p(a::[]) = a^"."
    |p(L:string list) = hd(L)^","^p(tl(L))   


fun eval(x:IExpr) = 
 let 
   fun a(INT(x),G:env.env,L) = L@(INT(x),"Normal Form")::[]
      |a(ERR(x),G,L) = L@(ERR(x),"Normal Form")::[]
      |a(x,G,L) = a(#1(r.defrules(G,x)),G,L@r.defrules(G,x)::[])
 in
  a(x,[],[])
 end

fun write(INT(a)) = "INT("^Int.toString(a)^")"
   |write(VAR(x)) = "VAR("^x^")"
   |write(ERR(x)) = "ERR("^write(x)^")"
   |write(PLUS(a,b)) = "PLUS("^write(a)^","^write(b)^")"
   |write(MINUS(a,b)) = "MINUS("^write(a)^","^write(b)^")"
   |write(MULT(a,b)) = "MULT("^write(a)^","^write(b)^")"
   |write(DIV(a,b)) = "DIV("^write(a)^","^write(b)^")"
   |write(MOD(a,b)) = "MOD("^write(a)^","^write(b)^")"
   |write(LET(x,y,z)) = "LET("^write(x)^","^write(y)^","^write(z)^")"

fun wp((x,y)) = "\n"^write(x)^"\n"^y^"\n"

fun wpr([]) = []
    |wpr(a::L) = wp(a)::wpr(L)

fun pr([]) = ()
    |pr(L) = print("\nThe Proof is :\n"^String.concat(L)^"\n")


 
fun evaluate(x:IExpr) = if findvars(x,[]) = [] then pr(wpr(eval(x)))
                                               else print("\nUNDECLARED VARIABLES : "^p(findvars(x,[]))^"\n")

   
end

open Proofs;

val l = print("Please use the function 'evaluate'\n");