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

theory Syntax : http://cds.omdoc.org/urtheories?LF =
  tp: type❙
  Bool: tp❙
  Nat : tp❙
  Unit: tp❙

  prog: tp ⟶ type❙

  true : prog Bool❙
  false: prog Bool❙
  unit : prog Unit❙
  zero : prog Nat❙
  succ : prog Nat ⟶ prog Nat❘# succ 1❙
  one  : prog Nat❘
       = succ zero❙ 
  equal : {a} prog a ⟶ prog a ⟶ prog Bool ❘ # 2 = 3 prec 10❙
  not   : prog Bool ⟶ prog Bool           ❘ # ¬ 1   prec 8 ❙
  plus  : prog Nat ⟶ prog Nat ⟶ prog Nat  ❘ # 1 + 2 prec 20❙
  minus : prog Nat ⟶ prog Nat ⟶ prog Nat  ❘ # 1 - 2 prec 20❙
  
  seq   : {a,b} prog a ⟶ prog b ⟶ prog b          ❘ # 3 ; 4 prec 5❙
  ifte  : {a} prog Bool ⟶ prog a ⟶ prog a ⟶ prog a❘ # if 2 then 3 else 4 prec 3❙
  ifte2 : prog Bool ⟶ prog Unit ⟶ prog Unit❘
        = [b,c] if b then c else unit❙
  while : prog Bool ⟶ prog Unit ⟶ prog Unit❙

  print : {a} prog a ⟶ prog Unit❘ # print 2❙
  read  : {a} prog a❙
  
  val : {a,b} prog a ⟶ (prog a ⟶ prog b) ⟶ prog b❘ # val 3 4❙

  Var : tp ⟶ type❙
  var : {a,b} prog a ⟶ (Var a ⟶ prog b) ⟶ prog b❘ # var 3 4❙
  varref : {a} Var a ⟶ prog a❘ # 2 ' prec 30❙
  assign : {a} Var a ⟶ prog a ⟶ prog Unit❘ # 2 ← 3 prec 10❙
❚
  
theory Test : ?Syntax =
  main = val (read Nat) [x]
         var zero [y]
         while (¬ x = y') (
           print x;
           y ← succ y'
         )❙
❚


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❙
❚

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❙
❚