/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)|
other		    	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;