The full Exp interpreter

Considering all this, here is the complete interpreter for Exp: 

 
program eval_exp is
    use Exp;
    use PSP;
    use messargs;

    import add(integer, integer, integer), 
           sub(integer, integer, integer), 
           mult(integer, integer, integer), 
           neg(integer, integer), 
           diff(string, string) from expfunc ;
 
    import message(string,string,string,string,path,string,_) 
           from message ;

    export 
      env[pair(variable "RESULT", integer 0)] |- exp : I, env  &
      UPDATE(env |- variable "RESULT", I : env')
     as init_eval_exp(exp) = env';

    export  
      env |- exp : I, env' &
      UPDATE(env' |- variable "RESULT", I : env'')
     as full_eval_exp(exp, env) = env'';

    judgement ENV |- Exp : INTEGER, ENV ;

    env |- integer N : integer N, env ;

    env |- EXP1 : integer x1, env'  &  
    env'|- EXP2 : integer x2, env''  &  
    add(x1, x2, x)
    ---------------- 
    env |- plus(EXP1, EXP2) : integer x, env'' ;

    env |- EXP1 : integer x1, env'  &  
    env'|- EXP2 : integer x2, env''  &  
    sub(x1, x2, x)
    ---------------- 
    env |- minus(EXP1, EXP2) : integer x, env'' ;


    env |- EXP1 : integer x1, env'  &  
    env'|- EXP2 : integer x2, env''  &  
    mult(x1, x2, x)
    ---------------- 
    env |- prod(EXP1, EXP2) : integer x, env'' ;

    env |- EXP : integer x1, env'  &  
    neg(x1, x)
    ---------------- 
    env |- uminus(EXP) : integer x, env' ;

    env |- EXP1 : v, env'
    ----------------
    env |- exp_s[EXP1] : v, env' ;


    env |- EXP1 : v1, env'  &  
    env'|- EXPS : v, env'' 
    ----------------
    env |- exp_s[EXP1.EXPS] : v, env'' ;

    env |- EXP : v, env' & 
    UPDATE(env' |- variable V, v : env'')
    ----------------    
    env |- assign(variable V, EXP) : v, env'' ;

    GETVALUE(env |- variable V : v, env')
    ----------------    
    env |- variable V : v, env' ;

  set UPDATE is

    judgement ENV |- Exp::VAR, INTEGER : ENV ;
 

    env[] |- variable V, I : env[pair(variable V, I)] ;
          do message("Exp", "interpreter", "variable-added", 
                     "Warning", nil(), "",
                     messarg(tree(variable V), ref(subject), 
                                  info "private")) ;

    env[pair(variable V, _) . env]
         |- variable V, I : env[pair(variable V, I) . env] ;

    env  |- variable V, n : env'
    -------------
    env[pair(variable V', I) . env] 
         |- variable V, n : env[pair(variable V', I) . env'] ;
       provided diff(V, V') ;

  end UPDATE ; 

  set GETVALUE is

    judgement ENV |- Exp::VAR : INTEGER, ENV ;
 

    message("Exp", "interpreter", "variable-added", 
            "Warning", nil(), "",
            messarg(tree(variable V), ref(subject), 
                    info "private"))
    ---------------- 
    env[] |- variable V : integer 0, 
                          env[pair(variable V, integer 0)] ;

    env[pair(variable V, I) . env] 
       |- variable V : I, env[pair(variable V, I) . env] ;

    env  |- variable V : n, env'
    -------------
    env[pair(variable V', I) . env] 
         |- variable V : n, env[pair(variable V', I) . env'] ;
      provided diff(V, V') ;

  end GETVALUE ;
end eval_exp ;

Tutorial