commit by user andrea

[helm.git] / weblib / While / syntax.ma

diff --git a/weblib/While/syntax.ma b/weblib/While/syntax.ma
new file mode 100644 (file)
index 0000000..b55d89d
--- /dev/null
+++ b/weblib/While/syntax.ma
@@ -0,0 +1,58 @@
+(* While Syntax *)
+
+include "basics/logic.ma".
+include "basics/types.ma".
+include "basics/bool.ma".
+include "arithmetics/nat.ma".
+
+(* Variables *)
+
+inductive Var : Type[0] ≝
+  Id : nat → Var.
+ 
+(* Arithmetic expressions *)
+
+inductive Aexp : Type[0] ≝
+  | Const : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Aexp
+  | Aid : \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6Var → Aexp
+  | Add : Aexp → Aexp → Aexp
+  | Sub : Aexp → Aexp → Aexp
+  | Mul : Aexp → Aexp → Aexp
+  | Div : Aexp → Aexp → Aexp
+  | Mod : Aexp → Aexp → Aexp
+ .
+
+interpretation "Aexp plus" 'plus x y = (Add x y).
+interpretation "Aexp minus" 'plus x y = (Sub x y).
+interpretation "Aexp times" 'times x y = (Mul x y).
+
+(* Boolean expressions *)
+inductive Bexp : Type[0] ≝
+  | BFalse : Bexp
+  | BTtrue : Bexp
+  | BNot : Bexp → Bexp
+  | BAnd : Bexp → Bexp → Bexp
+  | BOr : Bexp → Bexp → Bexp
+  | 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
+  | 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
+.
+
+interpretation "Bexp not" 'not x = (BNot x).
+interpretation "Bexp and" 'and x y = (BAnd x y).
+interpretation "Bexp or" 'or x y = (BOr x y).
+interpretation "Bexp 'less or equal to'" 'leq x y = (LE x y).
+
+(* Commands *)
+inductive Cmd : Type[0] ≝
+  | Skip : Cmd
+  | Assign : Var → \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → Cmd
+  | Seq : Cmd → Cmd → Cmd
+  | If : \ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"\ 6Bexp\ 5/a\ 6 → Cmd → Cmd → Cmd
+  | While : \ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"\ 6Bexp\ 5/a\ 6 → Cmd → Cmd
+.
+
+notation "hvbox(c1 break ; c2)"
+  left associative with precedence 47 for @{Seq $c1 $c2}.
+
+notation "hvbox(var break <- val)"
+  left associative with precedence 48 for @{Assign $var $val}.
\ No newline at end of file