/tmp/mosstmp/csu00112/comp-proof.sml
(* gaurav bansal 2000112 group-4*)
open Char;
signature EXPRESSION =
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;
type env = (var*int)list;
type pair = IExpr*IExpr;
type rule = pair*pair*string;
type proof = rule list;
val giveproof : IExpr -> unit
end;
structure smallsteps:EXPRESSION =
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;
type env = (var*int)list;
type pair = IExpr*IExpr;
type rule = pair*pair*string;
type proof = rule list;
exception let_requires_var;
fun undec_var(INT(_),_) = (true,"")
|undec_var(VAR(x),[]) = (false,x)
|undec_var(VAR(x),(y,_)::L) = if x=y then (true,"")
else undec_var(VAR(x),L)
|undec_var(PLUS(e1,e2),L) = let
val (a,b) = undec_var(e1,L);
val (c,d) = undec_var(e2,L)
in
if not(a) then (false,b)
else if not(c) then (false,d)
else (true,"")
end
|undec_var(MINUS(e1,e2),L) = let
val (a,b) = undec_var(e1,L);
val (c,d) = undec_var(e2,L)
in
if not(a) then (false,b)
else if not(c) then (false,d)
else (true,"")
end
|undec_var(MULT(e1,e2),L) = let
val (a,b) = undec_var(e1,L);
val (c,d) = undec_var(e2,L)
in
if not(a) then (false,b)
else if not(c) then (false,d)
else (true,"")
end
|undec_var(DIV(e1,e2),L) = let
val (a,b) = undec_var(e1,L);
val (c,d) = undec_var(e2,L)
in
if not(a) then (false,b)
else if not(c) then (false,d)
else (true,"")
end
|undec_var(MOD(e1,e2),L) = let
val (a,b) = undec_var(e1,L);
val (c,d) = undec_var(e2,L)
in
if not(a) then (false,b)
else if not(c) then (false,d)
else (true,"")
end
|undec_var(LET(VAR(x),e2,e3),L) = let
val (a,b) = undec_var(e2,L)
in
if not(a) then (false,b)
else undec_var(e3,(x,0)::L)
end
|undec_var(LET(e1,e2,e3),L) = raise let_requires_var
|undec_var(ERR(e),L) = undec_var(e,L);
exception undeclaredvariable;
fun lookvalue(v :var,[] :env) = raise undeclaredvariable
|lookvalue(v,(a,b)::g) = if v=a then b
else lookvalue(v,g);
val emp = (INT 0 , INT 0 );
fun pf(PLUS(ERR(e),e2),_ :env) :proof*IExpr =
([(emp,(PLUS(ERR(e),e2),ERR(e)),"errorl")],ERR(e))
|pf(PLUS(INT(n1),ERR(e)),_) =
([(emp,(PLUS(INT(n1),ERR(e)),ERR(e)),"errorr")],ERR(e))
|pf(PLUS(INT(n1),INT(n2)),_) =
let
val n3 = n1 + n2
in
([(emp,(PLUS(INT(n1),INT(n2)),INT(n3)),"add0")],INT(n3))
end
|pf(PLUS(INT n1,e2),g) = let
val (L,e22) = pf(e2,g);
in
(L@[((e2,e22),(PLUS(INT n1,e2),PLUS(INT n1,e22)),"addr")],PLUS(INT n1,e22))
end
|pf(PLUS(e1,e2),g) = let
val (L,e11) = pf(e1,g);
in
(L@[((e1,e11),(PLUS(e1,e2),PLUS(e11,e2)),"addl")],PLUS(e11,e2))
end
|pf(MINUS(ERR(e),e2),_ :env) :proof*IExpr =
([(emp,(MINUS(ERR(e),e2),ERR(e)),"errorl")],ERR(e))
|pf(MINUS(INT(n1),ERR(e)),_) =
([(emp,(MINUS(INT(n1),ERR(e)),ERR(e)),"errorr")],ERR(e))
|pf(MINUS(INT(n1),INT(n2)),_) =
let
val n3 = n1 - n2
in
([(emp,(MINUS(INT(n1),INT(n2)),INT(n3)),"sub0")],INT(n3))
end
|pf(MINUS(INT n1,e2),g) = let
val (L,e22) = pf(e2,g);
in
(L@[((e2,e22),(MINUS(INT n1,e2),MINUS(INT n1,e22)),"subr")],MINUS(INT
n1,e22))
end
|pf(MINUS(e1,e2),g) = let
val (L,e11) = pf(e1,g);
in
(L@[((e1,e11),(MINUS(e1,e2),MINUS(e11,e2)),"subl")],MINUS(e11,e2))
end
|pf(MULT(ERR(e),e2),_ :env) :proof*IExpr =
([(emp,(MULT(ERR(e),e2),ERR(e)),"errorl")],ERR(e))
|pf(MULT(INT(n1),ERR(e)),_) =
([(emp,(MULT(INT(n1),ERR(e)),ERR(e)),"errorr")],ERR(e))
|pf(MULT(INT(n1),INT(n2)),_) =
let
val n3 = n1 * n2
in
([(emp,(MULT(INT(n1),INT(n2)),INT(n3)),"mult0")],INT(n3))
end
|pf(MULT(INT n1,e2),g) = let
val (L,e22) = pf(e2,g);
in
(L@[((e2,e22),(MULT(INT n1,e2),MULT(INT n1,e22)),"multr")],MULT(INT
n1,e22))
end
|pf(MULT(e1,e2),g) = let
val (L,e11) = pf(e1,g);
in
(L@[((e1,e11),(MULT(e1,e2),MULT(e11,e2)),"multl")],MULT(e11,e2))
end
|pf(MOD(ERR(e),e2),_ :env) :proof*IExpr =
([(emp,(MOD(ERR(e),e2),ERR(e)),"errorl")],ERR(e))
|pf(MOD(INT(n1),ERR(e)),_) =
([(emp,(MOD(INT(n1),ERR(e)),ERR(e)),"errorr")],ERR(e))
|pf(MOD(INT n1,INT 0),_) =
([(emp,(MOD(INT n1,INT 0),ERR(MOD(INT n1,INT
0))),"moderr")],ERR(MOD(INT n1,INT 0)))
|pf(MOD(INT(n1),INT(n2)),_) =
let
val n3 = n1 mod n2
in
([(emp,(MOD(INT(n1),INT(n2)),INT(n3)),"mod0")],INT(n3))
end
|pf(MOD(INT n1,e2),g) = let
val (L,e22) = pf(e2,g);
in
(L@[((e2,e22),(MOD(INT n1,e2),MOD(INT n1,e22)),"modr")],MOD(INT
n1,e22))
end
|pf(MOD(e1,e2),g) = let
val (L,e11) = pf(e1,g);
in
(L@[((e1,e11),(MOD(e1,e2),MOD(e11,e2)),"modl")],MOD(e11,e2))
end
|pf(DIV(ERR(e),e2),_ :env) :proof*IExpr =
([(emp,(DIV(ERR(e),e2),ERR(e)),"errorl")],ERR(e))
|pf(DIV(INT(n1),ERR(e)),_) =
([(emp,(DIV(INT(n1),ERR(e)),ERR(e)),"errorr")],ERR(e))
|pf(DIV(INT n1,INT 0),_) =
([(emp,(DIV(INT n1,INT 0),ERR(DIV(INT n1,INT
0))),"diverr")],ERR(DIV(INT n1,INT 0)))
|pf(DIV(INT(n1),INT(n2)),_) =
let
val n3 = n1 div n2
in
([(emp,(DIV(INT(n1),INT(n2)),INT(n3)),"div0")],INT(n3))
end
|pf(DIV(INT n1,e2),g) = let
val (L,e22) = pf(e2,g);
in
(L@[((e2,e22),(DIV(INT n1,e2),DIV(INT n1,e22)),"divr")],DIV(INT
n1,e22))
end
|pf(DIV(e1,e2),g) = let
val (L,e11) = pf(e1,g);
in
(L@[((e1,e11),(DIV(e1,e2),DIV(e11,e2)),"divl")],DIV(e11,e2))
end
|pf(LET(VAR v,ERR e,e2),_) =
([(emp,(LET(VAR v,ERR(e),e2),ERR(e)),"errorl")],ERR(e))
|pf(LET(VAR v,INT(n1),ERR(e)),_) =
([(emp,(LET(VAR v,INT(n1),ERR(e)),ERR(e)),"errorr")],ERR(e))
|pf(LET(VAR v,INT(n1),INT n2),_) =
([(emp,(LET(VAR v,INT(n1),INT n2),INT n2),"let2")],INT n2)
|pf(LET(VAR v,INT(n1),e2),g) = let
val (L,e22) = pf(e2,(v,n1)::g);
in
(L@[((e2,e22),(LET(VAR v,INT n1,e2),LET(VAR v,INT
n1,e22)),"let1")],LET(VAR v,INT n1,e22))
end
|pf(LET(VAR v,e1,e2),g) = let
val (L,e11) = pf(e1,g);
in
(L@[((e1,e11),(LET(VAR v,e1,e2),LET(VAR
v,e11,e2)),"let0")],LET(VAR v,e11,e2))
end
|pf(VAR v,g) = let
val a = lookvalue(v,g)
in
([(emp,(VAR v,INT a),"vbl")],INT a)
end
|pf(INT n,_) = ([],INT n)
|pf(ERR e,_) = ([],ERR e);
fun pf2(INT n) = []
|pf2(ERR e) = []
|pf2(e) = let
val (u,v) = pf(e,[])
in
u@pf2(v)
end;
fun f_help(n) = let
val a = n div 10;
val b = n mod 10
in
if (a=0) then toString(chr(b+48))
else f_help(a)^ toString(chr(b+48))
end;
fun f(INT n) = f_help(n)
|f(VAR v) = v
|f(MINUS(e1,e2)) = "("^f(e1)^"-"^f(e2)^")"
|f(PLUS(e1,e2)) = "("^f(e1)^"+"^f(e2)^")"
|f(MULT(e1,e2)) = "("^f(e1)^"*"^f(e2)^")"
|f(DIV(e1,e2)) = "("^f(e1)^"/"^f(e2)^")"
|f(MOD(e1,e2)) = "("^f(e1)^"%"^f(e2)^")"
|f(LET(e1,e2,e3)) = "("^"let "^f(e1)^"="^f(e2)^" in "^f(e3)^")"
|f(ERR e) = "("^"ERR"^f(e)^")";
fun g([]) = []
|g(((a,b),(c,d),e)::L) =if a=INT(0) then
("_________________"^e^"____"^f(c)^"->"^f(d))::g(L)
else
(f(a)^"->"^f(b)^"____"^e^"____"^f(c)^"->"^f(d))::g(L);
fun pp([]) = print("done \n")
|pp(x::L) = (print(x^"\n\n");pp(L));
fun giveproof(e) = let
val (x,y) = undec_var(e,[])
in
if not(x) then print("\nUNDECLARED VARIABLE : "^y^"\n")
else
pp(g(pf2(e)))
end
end;
open smallsteps;