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

--
-- An instruction set
--
mod! INSTRUCT principal-sort Instruct {
  pr(NAT)
  pr(VAR)
  [Instruct ErrInstruct < Instruct&Err]
  op errInstruct : -> ErrInstruct {constr} .
  op push : Nat -> Instruct {constr} .
  op load : Var -> Instruct {constr} .
  op store : Var -> Instruct {constr} .
  op multiply : -> Instruct {constr} .
  op divide : -> Instruct {constr} .
  op mod : -> Instruct {constr} .
  op add : -> Instruct {constr} .
  op minus : -> Instruct {constr} .
  op lessThan : -> Instruct {constr} .
  op greaterThan : -> Instruct {constr} .
  op equal : -> Instruct {constr} .
  op notEqual : -> Instruct {constr} .
  op and : -> Instruct {constr} .
  op or : -> Instruct {constr} .
  op jump : Nat -> Instruct {constr} .
  op bjump : Nat -> Instruct {constr} .
  op jumpOnCond : Nat -> Instruct {constr} .
  op quit : -> Instruct {constr} .
}

view TRIV-ERR2INSTRUCT from TRIV-ERR to INSTRUCT {
  sort Elt -> Instruct,
  sort Err -> ErrInstruct,
  sort Elt&Err -> Instruct&Err,
  op err -> errInstruct
}

--
-- An instruction sequence is represented as a list of instructions.
--
mod! ILIST {
  pr(LIST(M <= TRIV-ERR2INSTRUCT)
     * {sort List -> IList, op nil -> iln} )
}

--
-- - Function vm takes an instruction sequence and returns the
--   environment made by executing the instruction sequence.
-- - Function exec takes an instruction sequence, a program pointe
--   pointing to an instruction in the sequence, a stack, and an
--   environment, and execute the instruction under the environment
--   with the stack.
-- - Function exec2 is an auxiliary function of exec.
--
mod! VM {
  pr(ILIST)
  pr(ENV)
  pr(STACK)
  op run : IList -> Env&Err .
  op exec : IList Nat Stack&Err Env&Err -> Env&Err .
  op exec2 : Instruct&Err IList Nat Stack&Err Env&Err -> Env&Err .
  var IL : IList .
  var PC : Nat .
  var Stk : Stack .
  var Env : Env .
  vars N N1 N2 : Nat .
  var V : Var .
  var E&E : Env&Err .
  var S&E : Stack&Err .
  var I&E : Instruct&Err .
  -- run
  -- exec
  -- exec2
}

eof

open VM .
  ops x y z : -> Var .
  ops il1 il2 : -> IList .
  eq il1 = push(1) | store(x) | push(2) | store (y) | load(y) | load(y) | multiply |
           store(y) | load(x) | push(2) | multiply | store(x) | push(16) | load(x) |
           equal | jumpOnCond(2) | bjump(12) | quit | iln .
  red run(il1) .
  eq il2 = push(1) | store(x) | push(2) | store (y) | load(y) | load(y) | multiply |
           store(y) | load(x) | push(2) | multiply | store(x) | push(64) | load(x) |
           equal | jumpOnCond(2) | bjump(12) | quit | iln .
  red run(il2) .
close