]> matita.cs.unibo.it Git - helm.git/blob - weblib/While/syntax.ma
lablgladecc => lablgladecc3
[helm.git] / 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" 'minus 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}.