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 mapping = var * int;
type env  = mapping list;
type confi= env * IExpr;
type label= string;
type rule = confi * confi * label;
type proof = string list;

val evaluate:IExpr -> unit;
end;

structure smallstep : 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 DECLARATIONS------------------*)
type mapping = var * int;
type env  = mapping list;
type confi= env * IExpr;
type label= string;
type rule = confi * confi * label;
type proof = string list;

(*-----------ENVIRONMENTS--------------------------*)
fun searchv([]:env,v)=(false,0)
   |searchv((v1,i1)::x,v)=if (v1=v) then (true,i1) else searchv(x,v);

fun rem((v1,i1)::x,v)=if (v1=v) then x else (v1,i1)::rem(x,v)
   |rem([],v)=[] ;
fun update(r1,[]:env)=r1
   |update(r1,(v,i)::x)= if #1(searchv(r1,v)) 
                        then update((v,i)::rem(r1,v),x)
                        else (v,i)::update(r1,x)  ;
(*----------------------------------------------------------------*)

fun ss(G:env,VAR(x),z,z1) = if #1(searchv(G,x)) then (G,INT(#2(searchv(G,x))),"vbl"::z,z1)
                                     else (G,INT(#2(searchv(G,x))),z,"undeclared variable"::z1)
   |ss(G,PLUS(INT(n1),INT(n2)),z,z1) = (G,INT(n1+n2),"add0"::z,z1)
   |ss(G,PLUS(INT(n1),ERR(e2)),z,z1) = (G,ERR(PLUS(INT n1,e2)),"addr"::z,z1) 
   |ss(G,PLUS(INT(n1),e2),z,z1) =  (G,PLUS(INT(n1),#2(ss(G,e2,z,z1))),"addr"::(#3(ss(G,e2,z,z1))),z1)
   |ss(G,PLUS(ERR(e1),e2),z,z1) =  (G,ERR(PLUS(e1,e2)),"addl"::z,z1) 
   |ss(G,PLUS(e1,e2),z,z1) =  (G,PLUS(#2(ss(G,e1,z,z1)),e2),"addl"::(#3(ss(G,e1,z,z1))),z1)

   |ss(G,MINUS(INT(n1),INT(n2)),z,z1) = (G,INT(n1-n2),"sub0"::z,z1)
   |ss(G,MINUS(INT(n1),ERR(e2)),z,z1) = (G,ERR(MINUS(INT n1,e2)),"subr"::z,z1) 
   |ss(G,MINUS(INT(n1),e2),z,z1) =  (G,MINUS(INT(n1),#2(ss(G,e2,z,z1))),"subr"::(#3(ss(G,e2,z,z1))),z1)
   |ss(G,MINUS(ERR(e1),e2),z,z1) =  (G,ERR(MINUS(e1,e2)),"subl"::z,z1) 
   |ss(G,MINUS(e1,e2),z,z1) =  (G,MINUS(#2(ss(G,e1,z,z1)),e2),"subl"::(#3(ss(G,e1,z,z1))),z1)

   |ss(G,MULT(INT(n1),INT(n2)),z,z1) = (G,INT(n1*n2),"mult0"::z,z1)
   |ss(G,MULT(INT(n1),ERR(e2)),z,z1) = (G,ERR(MULT(INT n1,e2)),"multr"::z,z1) 
   |ss(G,MULT(INT(n1),e2),z,z1) =  (G,MULT(INT(n1),#2(ss(G,e2,z,z1))),"multr"::(#3(ss(G,e2,z,z1))),z1)
   |ss(G,MULT(ERR(e1),e2),z,z1) =  (G,ERR(MULT(e1,e2)),"multl"::z,z1) 
   |ss(G,MULT(e1,e2),z,z1) =  (G,MULT(#2(ss(G,e1,z,z1)),e2),"multl"::(#3(ss(G,e1,z,z1))),z1)

   |ss(G,MOD(INT(n1),INT(n2)),z,z1) = if not(n2=0) then (G,INT(n1 mod n2),"mod0"::z,z1) else (G,ERR(MOD(INT n1,INT n2)),"mod0"::z,z1)
   |ss(G,MOD(INT(n1),ERR(e2)),z,z1) = (G,ERR(MOD(INT n1,e2)),"modr"::z,z1) 
   |ss(G,MOD(INT(n1),e2),z,z1) =  (G,MOD(INT(n1),#2(ss(G,e2,z,z1))),"modr"::(#3(ss(G,e2,z,z1))),z1)
   |ss(G,MOD(ERR(e1),e2),z,z1) =  (G,ERR(MOD(e1,e2)),"modl"::z,z1) 
   |ss(G,MOD(e1,e2),z,z1) =  (G,MOD(#2(ss(G,e1,z,z1)),e2),"modl"::(#3(ss(G,e1,z,z1))),z1)

   |ss(G,DIV(INT(n1),INT(n2)),z,z1) = if not(n2=0) then (G,INT(n1 div n2),"div0"::z,z1) else (G,ERR(DIV(INT n1,INT n2)),"div0"::z,z1)
   |ss(G,DIV(INT(n1),ERR(e2)),z,z1) = (G,ERR(DIV(INT n1,e2)),"divr"::z,z1) 
   |ss(G,DIV(INT(n1),e2),z,z1) =  (G,DIV(INT(n1),#2(ss(G,e2,z,z1))),"divr"::(#3(ss(G,e2,z,z1))),z1)
   |ss(G,DIV(ERR(e1),e2),z,z1) =  (G,ERR(DIV(e1,e2)),"divl"::z,z1) 
   |ss(G,DIV(e1,e2),z,z1) =  (G,DIV(#2(ss(G,e1,z,z1)),e2),"divl"::(#3(ss(G,e1,z,z1))),z1)

   |ss(G,LET(VAR(x),INT(n1),INT(n2)),z,z1)=(G,INT(n2),"let0"::z,z1)    
   |ss(G,LET(VAR(x),INT(n1),ERR(e2)),z,z1)=(G,ERR(LET(VAR(x),INT(n1),e2)),"letr"::z,z1) 
   |ss(G,LET(VAR(x),INT(n1),e2),z,z1)= (G,LET( VAR(x),INT(n1),#2(ss(update(G,[(x,n1)]),e2,z,z1)) ),"letr"::(#3(ss(update(G,[(x,n1)]),e2,z,z1))),z1)
   |ss(G,LET(VAR(x),ERR(e1),e2),z,z1)=(G,ERR(LET(VAR(x),e1,e2)),"letl"::z,z1)                 
   |ss(G,LET(VAR(x),e1,e2),z,z1)= (G,LET(VAR(x),#2(ss(G,e1,z,z1)),e2),"letl"::(#3(ss(G,e1,z,z1))),z1)                  
;


fun cvstr(INT(n))="INT "^Int.toString(n)
   |cvstr(VAR(v))="VAR "^v
   |cvstr(PLUS(e1,e2))="PLUS ("^cvstr(e1)^","^cvstr(e2)^")"
   |cvstr(MINUS(e1,e2))="MINUS ("^cvstr(e1)^","^cvstr(e2)^")"
   |cvstr(MULT(e1,e2))="MULT ("^cvstr(e1)^","^cvstr(e2)^")"
   |cvstr(DIV(e1,e2))="DIV ("^cvstr(e1)^","^cvstr(e2)^")"
   |cvstr(MOD(e1,e2))="MOD ("^cvstr(e1)^","^cvstr(e2)^")"
   |cvstr(LET(e1,e2,e3))="LET ("^cvstr(e1)^","^cvstr(e2)^","^cvstr(e3)^")"
   |cvstr(ERR(e))="ERR ("^cvstr(e)^")"
;


(*fun comp(INT(n))=print(cvstr(INT(n)))
   |comp(E)=print( cvstr(#2(ss([],E,[]))) );
*)

fun exist([],a)=false
    |exist(b::z,a)=if a=b then true else exist(z,a)
;

fun stlst([])=""
   |stlst(a::z)=a^","^stlst(z)
;

fun eval(_,_,_,s::z1)=["undeclared variable \n"]
   |eval(_,ERR(e),z,[])=z@[cvstr(ERR(e))]
   |eval(_,INT(n),z,[]):proof= z@[cvstr(INT(n))]
   |eval(G,E,z,[])=eval( #1(ss(G,E,[],[])),#2(ss(G,E,[],[])),z@["-->"^cvstr(#2(ss(G,E,[],[])))^"\n\t\t : rule  "^stlst(#3(ss(G,E,[],[])))^"\n"],#4(ss(G,E,[],[])) )
;

fun evaluate(E) = print(stlst(eval([],E,[],[]))^"\n")   ;
end;