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

theory OperationalSemantics : http://cds.omdoc.org/urtheories?LF =
  include ?Syntax❙
  include ?Machine❙
 
  objectify : {a} prog a ⟶ obj  ❘ # objectify 2❙
  varloc: {a} Var a ⟶ loc ⟶ type❘ # 2 @ 3❙
  
  eval : {a} prog a ⟶ prog a ⟶ type❘ # 2 ⟿ 3 prec 3❙

  eval_seq: {a,b, p:prog a, q: prog b, x,y} p⟿x ⟶ q⟿y ⟶ p;q ⟿ y❙
  
  eval_if_true : {a, c, t,e: prog a, x} c⟿true ⟶ t⟿x ⟶ if c then t else e ⟿ x❙
  eval_if_false: {a, c, t,e: prog a, x} c⟿false ⟶ e⟿x ⟶ if c then t else e ⟿ x❙
  
  eval_while_true : {c, b, x, y} c⟿true ⟶ b⟿x ⟶ while c b ⟿ y ⟶ while c b ⟿ y❙
  eval_while_false: {c, b} c⟿false ⟶ while c b ⟿ unit❙
  
  eval_var    : {a,b, p: prog a, cont: Var a ⟶ prog b, l, x, y}
                p⟿x ⟶ execute (add (objectify x) l) ⟶ ({v} v@l ⟶ cont v ⟿ y)
              ⟶ (var p cont)⟿y❙
             
  eval_varref : {a,v:Var a,l,x}
                v@l ⟶ execute (get l (objectify x))
              ⟶ v' ⟿ x❙
              
  eval_assign : {a, v: Var a,p,l,x}
                p⟿x ⟶ v@l ⟶ execute (update l (objectify x))
              ⟶ v←p ⟿ unit❙
  
  eval_print  : {a, p: prog a, x}
                p⟿x ⟶ execute (out stdio (objectify x))
              ⟶ (print p) ⟿ unit❙
  
  eval_read   : {a, x: prog a}
                execute (in stdio (objectify x))
              ⟶ (read a) ⟿ x❙
❚