namespace http://cds.omdoc.org/examples/programs❚

import rules scala://mmt.kwarc.info❚

theory Machine : http://cds.omdoc.org/urtheories?LF =
  obj: type❙
  loc: type❙
  
  command: type❙

  add: obj ⟶ loc ⟶ command❙
  get: loc ⟶ obj ⟶ command❙
  update: loc ⟶ obj ⟶ command❙
  delete: loc ⟶ obj ⟶ command❙

  chan: type❙
  stdio: chan❙
  in : chan ⟶ obj ⟶ command❙
  out: chan ⟶ obj ⟶ command❙
  
  execute: command ⟶ type❙
❚