/tmp/mosstmp/csu00118/comp-proof.sml
type var=string;
datatype IExpr= INT of int
| VAR of var
| PLUS of IExpr*IExpr
| MINUS of IExpr*IExpr
| DIV of IExpr*IExpr
| MOD of IExpr*IExpr
| MULT of IExpr*IExpr
| LET of IExpr*IExpr*IExpr
| ERR of IExpr;
signature enviro=
sig
type Env
val make : (int * var) list -> Env
val get_val : Env * var -> int * bool
val update : int * var * Env -> Env
end;
structure EE:enviro=
struct
datatype Env = ENV of (int*var) list
fun make(L) = ENV(L)
fun get_val(ENV([]),v)=(0,false)
|get_val(ENV((h_i,h_v)::t),v) = if v = h_v then (h_i,true) else get_val(ENV(t),v)
fun update(i,v,ENV(L)) = ENV((i,v)::L)
end;
signature rule=
sig
type rules;
val ext : rules -> IExpr;
val extract : rules -> IExpr * string * IExpr;
val apply : EE.Env * IExpr -> (rules list);
end;
structure RULES:rule=
struct
datatype rules = RUL of IExpr * string * IExpr;
fun extract(RUL(a,b,c))= (a,b,c);
fun add_fun(n1,n2) = INT(n1+n2);
fun sub_fun(n1,n2) = INT(n1-n2);
fun div_fun(n1,n2) = if (n2=0) then ERR(DIV(INT n1,INT n2)) else INT(n1 div n2);
fun mod_fun(n1,n2) = if (n2=0) then ERR(MOD(INT n1,INT n2)) else INT(n1 mod n2);
fun mult_fun(n1,n2) = INT(n1*n2);
fun ext(RUL(a,b,c))=c;
fun apply(e,VAR(v)) = let val (x,tmp)=EE.get_val(e,v) in RUL(VAR(v),"vbl",INT(x))::[] end
|apply(e,PLUS(INT(n1),INT(n2))) = RUL(PLUS(INT(n1),INT(n2)),"ADD_0",add_fun(n1,n2))::[]
|apply(e,PLUS(ERR(e1),e2))=RUL(PLUS(ERR(e1),e2),"ADD_ERR_l",ERR(PLUS(e1,e2)))::[]
|apply(e,PLUS(e1,ERR(e2)))=RUL(PLUS(e1,ERR(e2)),"ADD_ERR_2",ERR(PLUS(e1,e2)))::[]
|apply(e,PLUS(INT(n1),e2))=RUL(PLUS(INT(n1),e2),"ADD_r",PLUS(INT(n1),ext(List.hd(apply(e,e2)))))::apply(e,e2)
|apply(e,PLUS(e1,e2))=RUL(PLUS(e1,e2),"ADD_l",PLUS(ext(List.hd(apply(e,e1))),e2))::apply(e,e1)
|apply(e,MINUS(INT(n1),INT(n2))) = RUL(MINUS(INT(n1),INT(n2)),"SUB_0",sub_fun(n1,n2))::[]
|apply(e,MINUS(ERR(e1),e2))=RUL(MINUS(ERR(e1),e2),"SUB_ERR_l",ERR(MINUS(e1,e2)))::[]
|apply(e,MINUS(e1,ERR(e2)))=RUL(MINUS(e1,ERR(e2)),"SUB_ERR_2",ERR(MINUS(e1,e2)))::[]
|apply(e,MINUS(INT(n1),e2))=RUL(MINUS(INT(n1),e2),"SUB_r",MINUS(INT(n1),ext(List.hd(apply(e,e2)))))::apply(e,e2)
|apply(e,MINUS(e1,e2))=RUL(MINUS(e1,e2),"SUB_l",MINUS(ext(List.hd(apply(e,e1))),e2))::apply(e,e1)
|apply(e,MULT(INT(n1),INT(n2))) = RUL(MULT(INT(n1),INT(n2)),"MULT_0",mult_fun(n1,n2))::[]
|apply(e,MULT(ERR(e1),e2))=RUL(MULT(ERR(e1),e2),"MULT_ERR_l",ERR(MULT(e1,e2)))::[]
|apply(e,MULT(e1,ERR(e2)))=RUL(MULT(e1,ERR(e2)),"MULT_ERR_2",ERR(MULT(e1,e2)))::[]
|apply(e,MULT(INT(n1),e2))=RUL(MULT(INT(n1),e2),"MULT_r",MULT(INT(n1),ext(List.hd(apply(e,e2)))))::apply(e,e2)
|apply(e,MULT(e1,e2))=RUL(MULT(e1,e2),"MULT_l",MULT(ext(List.hd(apply(e,e1))),e2))::apply(e,e1)
|apply(e,DIV(INT(n),INT(0)))=RUL(DIV(INT(n),INT(0)),"DIV_ERR_0",ERR(DIV(INT(n),INT(0))))::[]
|apply(e,DIV(INT(n1),INT(n2)))=RUL(DIV(INT(n1),INT(n2)),"DIV_0",div_fun(n1,n2))::[]
|apply(e,DIV(ERR(e1),e2))=RUL(DIV(ERR(e1),e2),"DIV_ERR_l",ERR(DIV(e1,e2)))::[]
|apply(e,DIV(e1,ERR(e2)))=RUL(DIV(e1,ERR(e2)),"DIV_ERR_2",ERR(DIV(e1,e2)))::[]
|apply(e,DIV(INT(n1),e2))=RUL(DIV(INT(n1),e2),"DIV_r",DIV(INT(n1),ext(List.hd(apply(e,e2)))))::apply(e,e2)
|apply(e,DIV(e1,e2))=RUL(DIV(e1,e2),"DIV_l",DIV(ext(List.hd(apply(e,e1))),e2))::apply(e,e1)
|apply(e,MOD(INT(n),INT(0)))=RUL(MOD(INT(n),INT(0)),"MOD_ERR_0",ERR(MOD(INT(n),INT(0))))::[]
|apply(e,MOD(INT(n1),INT(n2)))=RUL(MOD(INT(n1),INT(n2)),"MOD_0",mod_fun(n1,n2))::[]
|apply(e,MOD(ERR(e1),e2))=RUL(MOD(ERR(e1),e2),"MOD_ERR_l",ERR(MOD(e1,e2)))::[]
|apply(e,MOD(e1,ERR(e2)))=RUL(MOD(e1,ERR(e2)),"MOD_ERR_2",ERR(MOD(e1,e2)))::[]
|apply(e,MOD(INT(n1),e2))=RUL(MOD(INT(n1),e2),"MOD_r",MOD(INT(n1),ext(List.hd(apply(e,e2)))))::apply(e,e2)
|apply(e,MOD(e1,e2))=RUL(MOD(e1,e2),"MOD_l",MOD(ext(List.hd(apply(e,e1))),e2))::apply(e,e1)
|apply(e,LET(VAR(x),INT(n1),INT(n2)))=RUL(LET(VAR(x),INT(n1),INT(n2)),"LET_0",INT(n2))::[]
|apply(e,LET(VAR(x),e1,ERR(e2)))=RUL(LET(VAR(x),e1,ERR(e2)),"LET_ERR_1",ERR(LET(VAR(x),e1,ERR(e2))))::[]
|apply(e,LET(VAR(x),ERR(e1),e2))=RUL(LET(VAR(x),ERR(e1),e2),"LET_ERR_2",ERR(LET(VAR(x),ERR(e1),e2)))::[]
|apply(e,LET(VAR(x),INT(n1),e2))=RUL(LET(VAR(x),INT(n1),e2),"LET_r",LET(VAR(x),INT(n1),ext(List.hd(apply(EE.update(n1,x,e),e2)))))::apply(EE.update(n1,x,e),e2)
|apply(e,LET(VAR(x),e1,e2))=RUL(LET(VAR(x),e1,e2),"LET_l",LET(VAR(x),ext(List.hd(apply(e,e1))),e2))::apply(e,e1)
|apply(_,_)=[]
end;
signature PROOF = sig
type proof;
val printproof : RULES.rules list list -> unit;
end;
structure PP:PROOF =
struct
datatype proof = proofify of RULES.rules list list;
fun exp2string(INT(n))=Int.toString(n)
|exp2string(VAR(x))=x
|exp2string(PLUS(e1,e2))="("^exp2string(e1)^" + "^exp2string(e2)^")"
|exp2string(MINUS(e1,e2))="("^exp2string(e1)^" - "^exp2string(e2)^")"
|exp2string(MULT(e1,e2))="("^exp2string(e1)^" * "^exp2string(e2)^")"
|exp2string(DIV(e1,e2))="("^exp2string(e1)^" / "^exp2string(e2)^")"
|exp2string(MOD(e1,e2))="("^exp2string(e1)^" % "^exp2string(e2)^")"
|exp2string(LET(VAR(x),e1,e2))= "let("^x^" := "^exp2string(e1)^" in "^exp2string(e2)^")"
|exp2string(ERR(e))= "error("^exp2string(e)^")"
|exp2string(_)=""
fun prhelp([])=""
|prhelp(a::ls)= let val (x,y,z)= RULES.extract(a) in (print( y^" : "^exp2string(x)^" --> "^exp2string(z));print("\n");prhelp(ls))
end;
fun printproof([])=print("")
|printproof(a::ls)=(prhelp(a);print("\n\n");printproof(ls));
end;
fun syn_chk(e,INT(n))= true
|syn_chk(e,VAR(x))= let val (a,b)= EE.get_val(e,x)
in if b=true then true
else (print("\n UNDECLARED VARIABLE :");print(x);false)
end
|syn_chk(e,PLUS(e1,e2))= syn_chk(e,e1) andalso syn_chk(e,e2)
|syn_chk(e,MINUS(e1,e2))= syn_chk(e,e1) andalso syn_chk(e,e2)
|syn_chk(e,MULT(e1,e2))= syn_chk(e,e1) andalso syn_chk(e,e2)
|syn_chk(e,DIV(e1,e2))= syn_chk(e,e1) andalso syn_chk(e,e2)
|syn_chk(e,MOD(e1,e2))= syn_chk(e,e1) andalso syn_chk(e,e2)
|syn_chk(e,LET(VAR(x),e1,e2))= let val en=EE.update(0,x,e)
in
syn_chk(e,e1) andalso syn_chk(en,e2)
end
|syn_chk(_,LET(_,_,_))=(print("\n SYNTAX ERROR");false)
|syn_chk(_,ERR(_))=(print("\n input error ");false);
fun red_help(INT(A)) = []|
red_help(ERR(A)) = []|
red_help(e)= let val a=RULES.apply(EE.make([]),e) in
a::red_help(RULES.ext(List.hd(a))) end;
fun reduction_proof(e)= if syn_chk(EE.make([]),e) then PP.printproof(red_help(e))
else print("");
(*
LET(VAR "x",LET(VAR "y",INT 4,PLUS(INT 4,MULT(INT 6,INT 5))),DIV (VAR "x",INT 9))
LET(VAR "x",INT 4,DIV (VAR "x",INT 9))
PLUS(INT 9,MULT(INT 4,INT 7))
*)