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