/tmp/mosstmp/csd00378/comp-proof.sml

```signature Exp =
sig
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
val Reduce : IExpr -> unit
end;

structure Let:Exp  =
struct
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;
datatype rule  = EX of IExpr| RULE of string;

fun Exist([],X) = false|
Exist((A,Y)::L,X) = if Y = X then true else Exist(L,X);

fun Gamma (Env,X:var)=
let
fun gamma_((A:int,Y)::L,X) = if Y = X then A else gamma_(L,X)
in	gamma_(Env,X) end;

fun value(X:int,B:bool,M:string) = X;

fun bool1(X:int,B:bool,M:string) = B;

fun message(X:int,Y:bool,S:string) = S;

fun Scan(LET(VAR(A),B,C)) = Scan(B)^Scan(C)|
Scan(LET(A,B,C)) = "\nIllegal use of LET. \n"|
Scan(PLUS(A,B)) = Scan(A)^Scan(B)|
Scan(MULT(A,B)) = Scan(A)^Scan(B)|
Scan(ERR(A)) = Scan(A)|
Scan(DIV(A,B)) = Scan(A)^Scan(B)|
Scan(MINUS(A,B)) = Scan(A)^Scan(B)|
Scan(MOD(A,B)) = Scan(A)^Scan(B)|
Scan(VAR(A)) = ""|
Scan(INT(A)) = "";

fun Parse(E,INT(A)) = ""|
Parse(E,VAR(A)) = if Exist(E,A) then "" else "\n"^A^" is not defined.\n"|
Parse(E,PLUS(A,B)) = Parse(E,A)^Parse(E,B)|
Parse(E,MINUS(A,B)) = Parse(E,A)^Parse(E,B)|
Parse(E,MULT(A,B)) = Parse(E,A)^Parse(E,B)|
Parse(E,DIV(A,B)) = Parse(E,A)^Parse(E,B)|
Parse(E,MOD(A,B)) = Parse(E,A)^Parse(E,B)|
Parse(E,ERR(A)) = ""|
Parse(E,LET(VAR(A),B,C)) = Parse(E,B)^Parse(((1,A)::E),C);

fun exp(E:IExpr,R:string) = E;
fun rule(E:IExpr,R:string) = R;

fun red(E,INT(A)) = (INT(A),"")|
red(E,VAR(A)) = let val Y = INT(Gamma(E,A)) in (Y," Variable Rule : ") end|
red(E,PLUS(INT(A),INT(B))) = let val Y = (A + B); val Z = INT(Y) in (Z,"Add Rule 0 : ") end|
red(E,PLUS(INT(A),ERR(B))) = (ERR(B),"Add Rule Right & Error Rule : ")|
red(E,PLUS(INT(A),B)) = let val Y = red(E,B) in (PLUS(INT(A),exp(Y)), "Add Rule Right &"^rule(Y)) end|
red(E,PLUS(ERR(A),B)) = (ERR(A),"Add Rule Left & Error Rule : ")|
red(E,PLUS(A,B)) = let val Y = red(E,A) in (PLUS(exp(Y),B),"Add Rule Left &"^rule(Y)) end|
red(E,MINUS(INT(A),INT(B))) = let val Y = (A - B); val Z = INT(Y) in (Z,"Sub Rule 0 : ") end|
red(E,MINUS(INT(A),ERR(B))) = (ERR(B)," Sub Rule Right & Error Rule : ")|
red(E,MINUS(INT(A),B)) = let val Y = red(E,B) in (MINUS(INT(A),exp(Y)), "Sub Rule Right &"^rule(Y)) end|
red(E,MINUS(ERR(A),B)) = (ERR(A),"Sub Rule Left & Error Rule : ")|
red(E,MINUS(A,B)) = let val Y = red(E,A) in (MINUS(exp(Y),B),"Sub Rule Left &"^rule(Y)) end|
red(E,MULT(INT(A),INT(B))) = let val Y = (A * B); val Z = INT(Y) in (Z," Mul Rule 0 : ") end|
red(E,MULT(INT(A),ERR(B))) = (ERR(B)," Mul Rule Right & Error Rule : ")|
red(E,MULT(INT(A),B)) = let val Y = red(E,B) in (MULT(INT(A),exp(Y)), "Mul Rule Right &"^rule(Y)) end|
red(E,MULT(ERR(A),B)) = (ERR(A)," Mul Rule Left & Error Rule : ")|
red(E,MULT(A,B)) = let val Y = red(E,A) in (MULT(exp(Y),B),"Mul Rule Left &"^rule(Y)) end|
red(E,DIV(INT(A),INT(B))) = if B=0 then (ERR(DIV(INT(A),INT(B)))," Error Rule (Division By Zero) : " ) else (INT(A div B)," Div Rule 0 : ")|
red(E,DIV(INT(A),ERR(B))) = (ERR(B)," Div Rule Right & Error Rule : ")|
red(E,DIV(INT(A),B)) = let val Y = red(E,B) in (DIV(INT(A),exp(Y)), "Div Rule Right &"^rule(Y)) end|
red(E,DIV(ERR(A),B)) = (ERR(A)," Div Rule Left & Error Rule : ")|
red(E,DIV(A,B)) = let val Y = red(E,A) in (DIV(exp(Y),B),"Div Rule Left &"^rule(Y)) end|
red(E,MOD(INT(A),INT(B))) = if B=0 then (ERR(MOD(INT(A),INT(B)))," Error Rule (Division By Zero) : " ) else (INT(A mod B)," Mod Rule 0 : ")|
red(E,MOD(INT(A),ERR(B))) = (ERR(B)," Mod Rule Right & Error Rule : ")|
red(E,MOD(INT(A),B)) = let val Y = red(E,B) in (MOD(INT(A),exp(Y)), "Mod Rule Right &"^rule(Y)) end|
red(E,MOD(ERR(A),B)) = (ERR(A)," Mod Rule Left & Error Rule : ")|
red(E,MOD(A,B)) = let val Y = red(E,A) in (MOD(exp(Y),B),"Mod Rule Left &"^rule(Y)) end|
red(E,LET(VAR(A),INT(B),INT(C))) = (INT(C),"Let Rule 0 : ")|
red(E,LET(VAR(A),INT(B),ERR(C))) = (ERR(C),"Let Rule Right & Error Rule : ") |
red(E,LET(VAR(A),INT(B),C)) = let val Y = red((B,A)::E,C) in (LET(VAR(A),INT(B),exp(Y)),"Let Rule Right &"^rule(Y)) end|
red(E,LET(VAR(A),ERR(B),C)) = (ERR(B),"Let Rule Left & Error Rule : ")|
red(E,LET(VAR(A),B,C)) = let val Y = red(E,B) in (LET(VAR(A),exp(Y),C),"Let Rule Left &"^rule(Y)) end;

local

fun toString(INT(A)) = Int.toString(A)|
toString(VAR(A)) = A|
toString(PLUS(A,B)) = "("^toString(A)^" + "^toString(B)^")"|
toString(MINUS(A,B)) = "("^toString(A)^" - "^toString(B)^")"|
toString(MULT(A,B)) = "("^toString(A)^"*"^toString(B)^")"|
toString(DIV(A,B)) = "("^toString(A)^"/"^toString(B)^")"|
toString(MOD(A,B)) = "("^toString(A)^"%"^toString(B)^")"|
toString(ERR(A)) = "ERR("^toString(A)^")"|
toString(LET(A,B,C))= "(let "^toString(A)^" := "^toString(B)^" in "^toString(C)^")";
in

fun small(E,INT(A)) = print(" This is Result you were looking for!\n\n ")|
small(E,ERR(X)) = (print( "Error rule : "); print("\n"); print(toString(ERR(X))); print("\n You got airthmetic error \n\n"))|
small(E,Ex) = let val Y = red(E,Ex) in (print(rule(Y)); print("\n"); print(toString(Ex)); print( " ----> "); print(toString(exp(Y))); print("\n\n"); small(E,exp(Y)))
end;

fun Reduce(I) = if Scan(I)^Parse([],I) = "" then (print("\n\n"); small([],I)) else print(Scan(I)^Parse([],I)) end;

end;```