signature SMALL =
sig
type var=string ;
datatype IExpr= 
                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  
               |VAR of var| INT of int ;

type Env= (var * int) list ;

exception  UNDECLAREDVARIABLE ;
val reduce: (IExpr*Env) -> IExpr 
val proof: ( IExpr * Env * ((Env*IExpr*IExpr*string) list)) ->  (Env*IExpr*IExpr*string) list  ; 
  
end ;

structure SSTEP: SMALL =

struct

type var=string ;
datatype IExpr=
                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
               |VAR of var| INT of int ;

type Env= (var * int) list ;

exception  UNDECLAREDVARIABLE ;


(* independent *)

fun equal(x:var,y:var)=
  let
    
    fun eq([],[])=true 
        |eq(a::x,[])=false 
        |eq([],b::y)=false 
        |eq(a::x,b::y)= if (a=b) then eq(x,y) else false ;
   in
     eq(explode(x),explode(y)) 
  end 

   
(* independent *)

fun find(x:var,[])= raise UNDECLAREDVARIABLE    
| find(x,y::E)=
        let 
          

val (a,b)=y ;
        
in
    if equal(x,a) then INT(b) else find(x,E) 
 end
 

(* independent *)

fun upd(E,x,n)=
let 

fun up_iter(left,[],(x,n))=left@(x,n)::[]
    |up_iter(left,y::right,(x,n))=
      let
        val (a,b)=y ;
      in
    if equal(x,a) then left@(x,n)::right 
    else up_iter(left@y::[],right,(x,n))
end

in

up_iter([],E,(x,n)) 
end


(* independent *)

fun reduce(INT(n),E)=INT(n)
|reduce(ERR(e),E)=ERR(e) 
|reduce(PLUS(INT(n1),INT(n2)),E)=INT(n1+n2) 
|reduce(VAR(x),E)= find(x,E)
|reduce(PLUS(ERR(e1),e2),E)=ERR(e1)
|reduce(PLUS(INT(n),ERR(e)),E)=ERR(e)
|reduce(PLUS(INT(n),e),E)=PLUS(INT(n),reduce(e,E)) 
|reduce(PLUS(e1,e2),E)=PLUS(reduce(e1,E),e2) 

|reduce(MINUS(INT(n1),INT(n2)),E)=INT(n1-n2)
|reduce(MINUS(ERR(e1),e2),E)=ERR(e1) 
|reduce(MINUS(INT(n),ERR(e)),E)=ERR(e)
|reduce(MINUS(INT(n),e),E)=MINUS(INT(n),reduce(e,E))
|reduce(MINUS(e1,e2),E)=MINUS(reduce(e1,E),e2)

|reduce(MULT(INT(n1),INT(n2)),E)=INT(n1*n2)
|reduce(MULT(ERR(e1),e2),E)=ERR(e1) 
|reduce(MULT(INT(n),ERR(e)),E)=ERR(e)
|reduce(MULT(INT(n),e),E)=MULT(INT(n),reduce(e,E))
|reduce(MULT(e1,e2),E)=MULT(reduce(e1,E),e2)

|reduce(DIV(INT(n1),INT(n2)),E)=if (n2=0) then ERR(DIV(INT(n1),INT(n2)))
                            else INT(n1 div n2)
|reduce(DIV(ERR(e1),e2),E)=ERR(e1) 
|reduce(DIV(INT(n),ERR(e)),E)=ERR(e)
|reduce(DIV(INT(n),e),E)=DIV(INT(n),reduce(e,E))
|reduce(DIV(e1,e2),E)=DIV(reduce(e1,E),e2)

|reduce(MOD(INT(n1),INT(n2)),E)=INT(n1 mod n2)
|reduce(MOD(ERR(e1),e2),E)=ERR(e1) 
|reduce(MOD(INT(n),ERR(e)),E)=ERR(e)
|reduce(MOD(INT(n),e),E)=MOD(INT(n),reduce(e,E))
|reduce(MOD(e1,e2),E)=MOD(reduce(e1,E),e2)  

|reduce(LET(VAR(x), INT(n1), INT(n2)),E)= INT(n2) 
|reduce(LET(VAR(x), INT(n1), e2),E)=
       LET(VAR(x),INT(n1),reduce(e2,upd(E,x,n1))) 

|reduce(LET(VAR(x),e1,e2),E)=LET(VAR(x),reduce(e1,E),e2) ;



fun  proof(INT(n:int),E:Env,[]:(Env*IExpr*IExpr*string) list )=(E,INT(n),INT(n),"zero")::[]  
|proof(INT(n:int),E:Env,L:(Env*IExpr*IExpr*string) list )= rev(L)
|proof(ERR(e:IExpr),E,[])=(E,ERR(e),ERR(e),"zero")::[]
|proof(ERR(e:IExpr),E,L)=rev(L)
|proof(PLUS(INT(n1),INT(n2)),E,L)=proof(reduce(PLUS(INT(n1),INT(n2)),E),E,(E,PLUS(INT(n1),INT(n2)),reduce(PLUS(INT(n1),INT(n2)),E),"add0")::L)

 
|proof(VAR(x),E,L)= proof(reduce(VAR(x),E),E,(E,VAR(x),reduce(VAR(x),E),"vbl")::L)
|proof(PLUS(ERR(e1),e2),E,L)=proof(reduce(PLUS(ERR(e1),e2),E),E,(E,PLUS(ERR(e1),e2),reduce(PLUS(ERR(e1),e2),E),"err0")::L)

|proof(PLUS(INT(n),ERR(e)),E,L)=proof(reduce(PLUS(INT(n),ERR(e)),E),E,(E,PLUS(INT(n),ERR(e)),reduce(PLUS(INT(n),ERR(e)),E),"err0")::L)

|proof(PLUS(INT(n),e),E,L)=proof(PLUS(INT(n),reduce(e,E)),E,(E,PLUS(INT(n),e),reduce(PLUS(INT(n),e),E),"addr")::L) 
|proof(PLUS(e1,e2),E,L)=proof(reduce(e1,E),E,(E,PLUS(e1,e2),reduce(PLUS(e1,e2),E),"addl")::L)

|proof(MINUS(INT(n1),INT(n2)),E,L)=proof(reduce(MINUS(INT(n1),INT(n2)),E),E,(E,MINUS(INT(n1),INT(n2)),reduce(MINUS(INT(n1),INT(n2)),E),"sub0")::L)
|proof(MINUS(ERR(e1),e2),E,L)=proof(reduce(MINUS(ERR(e1),e2),E),E,(E,MINUS(ERR(e1),e2),reduce(MINUS(ERR(e1),e2),E),"err0")::L)
|proof(MINUS(INT(n),ERR(e)),E,L)=proof(reduce(MINUS(INT(n),ERR(e)),E),E,(E,MINUS(INT(n),ERR(e)),reduce(MINUS(INT(n),ERR(e)),E),"err0")::L)
|proof(MINUS(INT(n),e),E,L)=proof(reduce(e,E),E,(E,MINUS(INT(n),e),reduce(MINUS(INT(n),e),E),"subr")::L)
|proof(MINUS(e1,e2),E,L)=proof(reduce(e1,E),E,(E,MINUS(e1,e2),reduce(MINUS(e1,e2),E),"subl")::L)

|proof(MULT(INT(n1),INT(n2)),E,L)=proof(reduce(MULT(INT(n1),INT(n2)),E),E,(E,MULT(INT(n1),INT(n2)),reduce(MULT(INT(n1),INT(n2)),E),"mult0")::L)
|proof(MULT(ERR(e1),e2),E,L)=proof(reduce(MULT(ERR(e1),e2),E),E,(E,MULT(ERR(e1),e2),reduce(MULT(ERR(e1),e2),E),"err0")::L)
|proof(MULT(INT(n),ERR(e)),E,L)=proof(reduce(MULT(INT(n),ERR(e)),E),E,(E,MULT(INT(n),ERR(e)),reduce(MULT(INT(n),ERR(e)),E),"err0")::L)
|proof(MULT(INT(n),e),E,L)=proof(reduce(e,E),E,(E,MULT(INT(n),e),reduce(MULT(INT(n),e),E),"multr")::L)
|proof(MULT(e1,e2),E,L)=proof(reduce(e1,E),E,(E,MULT(e1,e2),reduce(MULT(e1,e2),E),"multl")::L)

|proof(DIV(INT(n1),INT(n2)),E,L)=proof(reduce(DIV(INT(n1),INT(n2)),E),E,(E,DIV(INT(n1),INT(n2)),reduce(DIV(INT(n1),INT(n2)),E),"div0")::L)
|proof(DIV(ERR(e1),e2),E,L)=proof(reduce(DIV(ERR(e1),e2),E),E,(E,DIV(ERR(e1),e2),reduce(DIV(ERR(e1),e2),E),"err0")::L) 
|proof(DIV(INT(n),ERR(e)),E,L)=proof(reduce(DIV(INT(n),ERR(e)),E),E,(E,DIV(INT(n),ERR(e)),reduce(DIV(INT(n),ERR(e)),E),"err0")::L)
|proof(DIV(INT(n),e),E,L)=proof(reduce(e,E),E,(E,DIV(INT(n),e),reduce(DIV(INT(n),e),E),"divr")::L)
|proof(DIV(e1,e2),E,L)=proof(reduce(e1,E),E,(E,DIV(e1,e2),reduce(DIV(e1,e2),E),"divl")::L)

|proof(MOD(INT(n1),INT(n2)),E,L)=proof(reduce(MOD(INT(n1),INT(n2)),E),E,(E,MOD(INT(n1),INT(n2)),reduce(MOD(INT(n1),INT(n2)),E),"mod0")::L)
|proof(MOD(ERR(e1),e2),E,L)=proof(reduce(MOD(ERR(e1),e2),E),E,(E,MOD(ERR(e1),e2),reduce(MOD(ERR(e1),e2),E),"err0")::L)
|proof(MOD(INT(n),ERR(e)),E,L)=proof(reduce(MOD(INT(n),ERR(e)),E),E,(E,MOD(INT(n),ERR(e)),reduce(MOD(INT(n),ERR(e)),E),"err0")::L)
|proof(MOD(INT(n),e),E,L)=proof(reduce(e,E),E,(E,MOD(INT(n),e),reduce(MOD(INT(n),e),E),"modr")::L)
|proof(MOD(e1,e2),E,L)=proof(reduce(e1,E),E,(E,MOD(e1,e2),reduce(MOD(e1,e2),E),"modl")::L)

|proof(LET(VAR(x), INT(n1), INT(n2)),E,L)=proof(reduce(LET (VAR(x), INT(n1), INT(n2)),E),E,(E,LET(VAR(x), INT(n1), INT(n2)),reduce(LET(VAR(x), INT(n1), INT(n2)),E),"let0")::L) 

|proof(LET(VAR(x), INT(n1), e2),E,L)= proof(reduce(e2,upd(E,x,n1)),upd(E,x,n1),(E,LET(VAR(x), INT(n1), e2),reduce(LET(VAR(x), INT(n1), e2),E),"letR")::L)

|proof(LET(VAR(x),e1,e2),E,L)=proof(reduce(e1,E),E,(E,LET(VAR(x),e1,e2),reduce(LET(VAR(x),e1,e2),E),"letL")::L) ;








 






end ;
open SSTEP ;