/tmp/mosstmp/csd00391/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 Isdefine(X,[]) = false|
Isdefine(X,(Y,_)::L) = if Y = X then true else Isdefine(X,L);
fun Lexical(INT(A:int)) = ""|
Lexical(VAR(X)) = ""|
Lexical(PLUS(X,Y)) = if Lexical(X)= ""
then Lexical(Y) else Lexical(X)|
Lexical(MINUS(X,Y)) = if Lexical(X)= ""
then Lexical(Y) else Lexical(X)|
Lexical(MULT(X,Y)) = if Lexical(X)= ""
then Lexical(Y) else Lexical(X)|
Lexical(DIV(X,Y)) = if Lexical(X)= ""
then Lexical(Y) else Lexical(X)|
Lexical(MOD(X,Y)) = if Lexical(X)= ""
then Lexical(Y) else Lexical(X)|
Lexical(ERR(X)) = ""|
Lexical(LET(VAR(X),Y,Z)) = if Lexical(Y) = "" then Lexical(Z)
else Lexical(Y)|
Lexical(LET(X,Y,Z)) = "Syntax Error in LET\n\n";
local
fun gamma_(X,(Y,A:int)::L) = if Y = X then A else gamma_(X,L)
in
fun Gamma (X:string,Env)= gamma_(X,Env) end;
local
fun value(_,_,X:int) = X;
fun bool1(Y:bool,_,_) = Y;
fun parse_(INT(X),Env) = (true,"",X)|
parse_(VAR(X),Env) = if Isdefine(X,Env) then (true,"",Gamma(X,Env)) else (false,"Variable "^X^" not declared\n\n",0)|
parse_(PLUS(X,Y),Env) = if bool1(parse_(X,Env)) andalso bool1(parse_(Y,Env)) then (true,"",(value(parse_(X,Env))+ value(parse_(Y,Env))))
else if bool1(parse_(X,Env)) then parse_(Y,Env) else parse_(X,Env)|
parse_(MINUS(X,Y),Env) = if bool1(parse_(X,Env)) andalso bool1(parse_(Y,Env)) then (true,"",value(parse_(X,Env))-value(parse_(Y,Env)))
else if bool1(parse_(X,Env)) then parse_(Y,Env) else parse_(X,Env)|
parse_(MULT(X,Y),Env) = if bool1(parse_(X,Env)) andalso bool1(parse_(Y,Env)) then (true,"",value(parse_(X,Env))*value(parse_(Y,Env)))
else if bool1(parse_(X,Env)) then parse_(Y,Env) else parse_(X,Env)|
parse_(DIV(X,INT(0)),Env) = parse_(ERR(DIV(X,INT(0))),Env)|
parse_(DIV(X,Y),Env) = if bool1(parse_(X,Env)) andalso bool1(parse_(Y,Env)) then (true,"",value(parse_(X,Env)) * value(parse_(Y,Env)))
else if bool1(parse_(X,Env)) then parse_(Y,Env) else parse_(X,Env)|
parse_(MOD(X,INT(0)),Env) = parse_(ERR(MOD(X,INT(0))),Env)|
parse_(MOD(X,Y),Env) = if bool1(parse_(X,Env)) andalso bool1(parse_(Y,Env)) then (true,"",value(parse_(X,Env)) - value(parse_(Y,Env)))
else if bool1(parse_(X,Env)) then parse_(Y,Env) else parse_(X,Env)|
parse_(ERR(A),Env) = (true,"",0)|
parse_(LET(VAR(V),INT(X),Z),Env) = parse_(Z,(V,X)::Env)|
(*parse_(LET(VAR(V1),VAR(V2),Z),Env) = if Isdefine(V2,Env) then parse_(Z,(V1,Gamma(V2,Env))::Env) else (false,"Variable "^V2^" not declared",0)|*)
parse_(LET(VAR(V),Z,Z2),Env) =
let val s = parse_(Z,Env)
in if bool1(s) then parse_(Z2,(V,value(s))::Env)
else s end;
fun message(_,S:string,_) = S
in
fun Parse(I) =
let val A = parse_(I,[])
in if bool1(A) then "" else message(A)
end
end;
fun red(INT(A),Env) = INT(A)|
red(VAR(A),Env) = INT(Gamma(A,Env))|
red(PLUS(INT(A),INT(B)),Env) = INT(A + B)|
red(PLUS(INT(A),ERR(B)),Env) = ERR(B)|
red(PLUS(INT(A),B),Env) = PLUS(INT(A),red(B,Env))|
red(PLUS(ERR(A),B),Env) = ERR(A)|
red(PLUS(A,B),Env) = PLUS(red(A,Env),B)|
red(MINUS(INT(A),INT(B)),Env) = INT(A - B)|
red(MINUS(INT(A),ERR(B)),Env) = ERR(B)|
red(MINUS(INT(A),B),Env) = MINUS(INT(A),red(B,Env))|
red(MINUS(ERR(A),B),Env) = ERR(A)|
red(MINUS(A,B),Env) = MINUS(red(A,Env),B)|
red(MULT(INT(A),INT(B)),Env) = INT(A * B)|
red(MULT(INT(A),ERR(B)),Env) = ERR(B)|
red(MULT(INT(A),B),Env) = MULT(INT(A),red(B,Env))|
red(MULT(ERR(A),B),Env) = ERR(A)|
red(MULT(A,B),Env) = MULT(red(A,Env),B)|
red(DIV(INT(A),INT(B)),Env) = if B = 0 then ERR(DIV(INT(A),INT(B))) else INT(A div B)|
red(DIV(INT(A),ERR(B)),Env) = ERR(B)|
red(DIV(INT(A),B),Env) = DIV(INT(A),red(B,Env))|
red(DIV(ERR(A),B),Env) = ERR(A)|
red(DIV(A,B),Env) = DIV(red(A,Env),B)|
red(MOD(INT(A),INT(B)),Env) = if B = 0 then ERR(MOD(INT(A),INT(B))) else INT(A mod B)|
red(MOD(INT(A),ERR(B)),Env) = ERR(B)|
red(MOD(INT(A),B),Env) = MOD(INT(A),red(B,Env))|
red(MOD(ERR(A),B),Env) = ERR(A)|
red(MOD(A,B),Env) = MOD(red(A,Env),B)|
red(LET(VAR(A),INT(B),INT(C)),Env) = INT(C)|
red(LET(VAR(A),INT(B),ERR(C)),Env) = ERR(C)|
red(LET(VAR(A),INT(B),C),Env) = LET(VAR(A),INT(B),red(C,(A,B)::Env))|
red(LET(VAR(A),ERR(B),C),Env) = ERR(B)|
red(LET(VAR(A),B,C),Env) = LET(VAR(A),red(B,Env),C);
fun rule(INT(A)) = " This is Final Result!\n"|
rule(VAR(A)) = " Vrb rule : "|
rule(PLUS(INT(A),INT(B))) = " Add-0 rule : "|
rule(PLUS(INT(A),B)) = " Add-R rule &"^rule(B)|
rule(PLUS(A,B)) = " Add-L rule &"^rule(A)|
rule(MINUS(INT(A),INT(B))) = " Sub-0 rule : "|
rule(MINUS(INT(A),B)) = " Sub-R rule &"^rule(B)|
rule(MINUS(A,B)) = " Sub-L rule &"^rule(A)|
rule(MULT(INT(A),INT(B))) = " Mul-0 rule : "|
rule(MULT(INT(A),B)) = " Mul-R rule &"^rule(B)|
rule(MULT(A,B)) = " Mul-L rule &"^rule(A)|
rule(DIV(INT(A),INT(B))) = " Div-0 rule : "|
rule(DIV(INT(A),B)) = " Div-R rule &"^rule(B)|
rule(DIV(A,B)) = " Div-L rule &"^rule(A)|
rule(MOD(INT(A),INT(B))) = " Mod-0 rule : "|
rule(MOD(INT(A),B)) = " Mod-R rule &"^rule(B)|
rule(MOD(A,B)) = " Mod-L rule &"^rule(A)|
rule(ERR(A)) = " Err rule : "|
rule(LET(VAR(A),INT(B),INT(C))) = " Let-0 rule : "|
rule(LET(VAR(A),INT(B),C)) = " Let-R rule &"^rule(C)|
rule(LET(VAR(A),B,C)) = " Let-L rule &"^rule(B);
fun toString(INT(A)) = "INT("^Int.toString(A)^")"|
toString(VAR(A)) = "VAR("^A^")"|
toString(PLUS(A,B)) = "PLUS("^toString(A)^","^toString(B)^")"|
toString(MINUS(A,B)) = "MINUS("^toString(A)^","^toString(B)^")"|
toString(MULT(A,B)) = "MULT("^toString(A)^","^toString(B)^")"|
toString(DIV(A,B)) = "DIV("^toString(A)^","^toString(B)^")"|
toString(MOD(A,B)) = "MOD("^toString(A)^","^toString(B)^")"|
toString(ERR(A)) = "ERR("^toString(A)^")"|
toString(LET(A,B,C))= "LET("^toString(A)^","^toString(B)^","^toString(C)^")";
fun small(INT(A),Env) = print(" This is Final Result!\n\n You gotta your answer \n\n")|
small(VAR(X),Env) = (print(rule(VAR(X))); print("\n"); print(toString(VAR(X))); print(" ----> "); print(toString(red(VAR(X),Env)));print("\n\n"))|
small(ERR(X),Env) = (print(rule(ERR(X))); print("\n"); print(toString(ERR(X))); print("\n You gotta an error \n\n"))|
small(E,Env) = (print(rule(E)); print("\n"); print(toString(E)); print( " ----> "); print(toString(red(E,Env))); print("\n\n"); small(red(E,Env),Env));
fun Reduce(I) = if Lexical(I) = "" then if Parse(I) = "" then (print("\n\n"); small(I,[])) else print(Parse(I)) else print(Lexical(I));
end;