--
-- A Virtual Machine for Minila program
--

--
-- A command (instruction) set
--
mod! COMMAND {
  pr(NAT)
  pr(VAR)
  [Command ErrCommand < Command&Err]
  op errCommand : -> ErrCommand {constr}
  op push : Nat -> Command {constr}
  op load : Var -> Command {constr}
  op store : Var -> Command {constr}
  op multiply : -> Command {constr}
  op divide : -> Command {constr}
  op mod : -> Command {constr}
  op add : -> Command {constr}
  op minus : -> Command {constr}
  op lessThan : -> Command {constr}
  op greaterThan : -> Command {constr}
  op equal : -> Command {constr}
  op notEqual : -> Command {constr}
  op and : -> Command {constr}
  op or : -> Command {constr}
  op jump : Nat -> Command {constr}
  op bjump : Nat -> Command {constr}
  op jumpOnCond : Nat -> Command {constr}
  op quit : -> Command {constr}
}

view TRIV-ERR2COMMAND from TRIV-ERR to COMMAND {
  sort Elt -> Command,
  sort Err -> ErrCommand,
  sort Elt&Err -> Command&Err,
  op err -> errCommand
}

--
-- A command sequence is represented as a list of commands.
--
mod! CLIST {
  pr(LIST(M <= TRIV-ERR2COMMAND)
     * {sort List -> CList, op nil -> clnil} )
}

--
-- - Function vm takes a command sequence and returns the
--   environment made by executing the command sequence.
-- - Function exec takes a command sequence, a program pointe
--   pointing to a command in the sequence, a stack, and an
--   environment, and execute the command under the environment
--   with the stack.
-- - Function exec2 is an auxiliary function of exec.
--
mod! VM {
  pr(CLIST)
  pr(ENV)
  pr(STACK)
  op vm : CList -> Env&Err
  op exec : CList Nat Stack&Err Env&Err -> Env&Err
  op exec2 : Command&Err CList Nat Stack&Err Env&Err -> Env&Err
  var CL : CList
  var PC : Nat
  var Stk : Stack
  var Env : Env
  vars N N1 N2 : Nat
  var V : Var
  var C : Command
  -- vm
  eq vm(CL) = exec(CL,0,empstk,empEnv) .
  -- exec
  eq exec(CL,PC,errStack,E&E:Env&Err) = errEnv .
  eq exec(CL,PC,S&E:Stack&Err,errEnv) = errEnv .
  eq exec(CL,PC,Stk,Env) = exec2(nth(CL,PC),CL,PC,Stk,Env) .
  -- exec2
  eq exec2(errCommand,CL,PC,S&E:Stack&Err,E&E:Env&Err) = errEnv .
  eq exec2(C&E:Command&Err,CL,PC,errStack,E&E:Env&Err) = errEnv .
  eq exec2(C&E:Command&Err,CL,PC,S&E:Stack&Err,errEnv) = errEnv .
  --
  eq exec2(push(N),CL,PC,Stk,Env) = exec(CL,PC + 1,N | Stk,Env) .
  --
  eq exec2(load(V),CL,PC,Stk,Env)
     = exec(CL,PC + 1,lookup(V,Env) | Stk,Env) .
  --
  eq exec2(store(V),CL,PC,empstk,Env) = errEnv .
  eq exec2(store(V),CL,PC,N | Stk,Env)
     = exec(CL,PC + 1,Stk,update(V,N,Env)) .
  --
  eq exec2(multiply,CL,PC,empstk,Env) = errEnv .
  eq exec2(multiply,CL,PC,N1 | empstk,Env) = errEnv .
  eq exec2(multiply,CL,PC,N2 | N1 | Stk,Env)
     = exec(CL,PC + 1,N1 * N2 | Stk,Env) .
  --
  eq exec2(divide,CL,PC,empstk,Env) = errEnv .
  eq exec2(divide,CL,PC,N1 | empstk,Env) = errEnv .
  eq exec2(divide,CL,PC,N2 | N1 | Stk,Env)
     = exec(CL,PC + 1,N1 quo N2 | Stk,Env) .
  --
  eq exec2(mod,CL,PC,empstk,Env) = errEnv .
  eq exec2(mod,CL,PC,N1 | empstk,Env) = errEnv .
  eq exec2(mod,CL,PC,N2 | N1 | Stk,Env)
     = exec(CL,PC + 1,N1 rem N2 | Stk,Env) .
  --
  eq exec2(add,CL,PC,empstk,Env) = errEnv .
  eq exec2(add,CL,PC,N1 | empstk,Env) = errEnv .
  eq exec2(add,CL,PC,N2 | N1 | Stk,Env)
     = exec(CL,PC + 1,N1 + N2 | Stk,Env) .
  --
  eq exec2(minus,CL,PC,empstk,Env) = errEnv .
  eq exec2(minus,CL,PC,N1 | empstk,Env) = errEnv .
  eq exec2(minus,CL,PC,N2 | N1 | Stk,Env)
     = exec(CL,PC + 1,sd(N1,N2) | Stk,Env) .
  --
  eq exec2(lessThan,CL,PC,empstk,Env) = errEnv .
  eq exec2(lessThan,CL,PC,N1 | empstk,Env) = errEnv .
  eq exec2(lessThan,CL,PC,N2 | N1 | Stk,Env)
     = if N1 < N2 then exec(CL,PC + 1,1 | Stk,Env)
                  else exec(CL,PC + 1,0 | Stk,Env) fi .
  --
  eq exec2(greaterThan,CL,PC,empstk,Env) = errEnv .
  eq exec2(greaterThan,CL,PC,N1 | empstk,Env) = errEnv .
  eq exec2(greaterThan,CL,PC,N2 | N1 | Stk,Env)
     = if N1 > N2 then exec(CL,PC + 1,1 | Stk,Env)
                    else exec(CL,PC + 1,0 | Stk,Env) fi .
  --
  eq exec2(equal,CL,PC,empstk,Env) = errEnv .
  eq exec2(equal,CL,PC,N1 | empstk,Env) = errEnv .
  eq exec2(equal,CL,PC,N2 | N1 | Stk,Env)
     = if N1 == N2 then exec(CL,PC + 1,1 | Stk,Env)
                   else exec(CL,PC + 1,0 | Stk,Env) fi .
  --
  eq exec2(notEqual,CL,PC,empstk,Env) = errEnv .
  eq exec2(notEqual,CL,PC,N1 | empstk,Env) = errEnv .
  eq exec2(notEqual,CL,PC,N2 | N1 | Stk,Env)
     = if N1 == N2 then exec(CL,PC + 1,0 | Stk,Env)
                   else exec(CL,PC + 1,1 | Stk,Env) fi .
  --
  eq exec2(and,CL,PC,empstk,Env) = errEnv .
  eq exec2(and,CL,PC,N1 | empstk,Env) = errEnv .
  eq exec2(and,CL,PC,N2 | N1 | Stk,Env)
     = if N1 == 0 or N2 == 0
       then exec(CL,PC + 1,0 | Stk,Env)
       else exec(CL,PC + 1,1 | Stk,Env) fi .
  --
  eq exec2(or,CL,PC,empstk,Env) = errEnv .
  eq exec2(or,CL,PC,N1 | empstk,Env) = errEnv .
  eq exec2(or,CL,PC,N2 | N1 | Stk,Env)
     = if N1 == 0 and N2 == 0
       then exec(CL,PC + 1,0 | Stk,Env)
       else exec(CL,PC + 1,1 | Stk,Env) fi .
  --
  eq exec2(jump(N),CL,PC,Stk,Env) = exec(CL,PC + N,Stk,Env) .
  --
  eq exec2(bjump(N),CL,PC,Stk,Env) = exec(CL,sd(PC,N),Stk,Env) .
  --
  eq exec2(jumpOnCond(N),CL,PC,empstk,Env) = errEnv .
  eq exec2(jumpOnCond(N),CL,PC,N1 | Stk,Env)
     = if N1 == 0 then exec(CL,PC + 1,Stk,Env)
                  else exec(CL,PC + N,Stk,Env) fi .
  --
  eq exec2(quit,CL,PC,Stk,Env) = Env .
}


open VM
ops cl1 cl2 cl3 cl4 : -> CList .
eq cl1 = push(2) | store(v(0)) | quit | clnil .
red vm(cl1) .
eq cl2 = push(4) | push(3) | add | store(v(0)) | quit | clnil .
red vm(cl2) .
eq cl3 = push(4) | add | quit | clnil .
red vm(cl3) .
eq cl4 = push(4) | push(0) | divide | store(v(0)) | quit | clnil .
red vm(cl4) .
close