weblib/While/syntax.ma

   1 (* While Syntax *)
   2
   3 include "basics/logic.ma".
   4 include "basics/types.ma".
   5 include "basics/bool.ma".
   6 include "arithmetics/nat.ma".
   7
   8 (* Variables *)
   9
  10 inductive Var : Type[0] ≝
  11   Id : nat → Var.
  12
  13 (* Arithmetic expressions *)
  14
  15 inductive Aexp : Type[0] ≝
  16   | Const : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Aexp
  17   | Aid : \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6Var → Aexp
  18   | Add : Aexp → Aexp → Aexp
  19   | Sub : Aexp → Aexp → Aexp
  20   | Mul : Aexp → Aexp → Aexp
  21   | Div : Aexp → Aexp → Aexp
  22   | Mod : Aexp → Aexp → Aexp
  23  .
  24
  25 interpretation "Aexp plus" 'plus x y = (Add x y).
  26 interpretation "Aexp minus" 'plus x y = (Sub x y).
  27 interpretation "Aexp times" 'times x y = (Mul x y).
  28
  29 (* Boolean expressions *)
  30 inductive Bexp : Type[0] ≝
  31   | BFalse : Bexp
  32   | BTtrue : Bexp
  33   | BNot : Bexp → Bexp
  34   | BAnd : Bexp → Bexp → Bexp
  35   | BOr : Bexp → Bexp → Bexp
  36   | Eq : \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → Bexp
  37   | LE : \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → Bexp
  38 .
  39
  40 interpretation "Bexp not" 'not x = (BNot x).
  41 interpretation "Bexp and" 'and x y = (BAnd x y).
  42 interpretation "Bexp or" 'or x y = (BOr x y).
  43 interpretation "Bexp 'less or equal to'" 'leq x y = (LE x y).
  44
  45 (* Commands *)
  46 inductive Cmd : Type[0] ≝
  47   | Skip : Cmd
  48   | Assign : Var → \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → Cmd
  49   | Seq : Cmd → Cmd → Cmd
  50   | If : \ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"\ 6Bexp\ 5/a\ 6 → Cmd → Cmd → Cmd
  51   | While : \ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"\ 6Bexp\ 5/a\ 6 → Cmd → Cmd
  52 .
  53
  54 notation "hvbox(c1 break ; c2)"
  55   left associative with precedence 47 for @{Seq $c1 $c2}.
  56
  57 notation "hvbox(var break <- val)"
  58   left associative with precedence 48 for @{Assign $var $val}.