# Theory SM_Syntax

```section ‹Syntax of SM›
theory SM_Syntax
imports Main
begin
text ‹
In this theory, we define the syntax of SM, the Simple Modeling language.
›

text ‹Literals›
type_synonym ident = String.literal     ― ‹ Identifier ›
type_synonym numeric = int              ― ‹ Numeric value ›

datatype bin_op =                               ― ‹ Binary operators ›
bo_plus | bo_minus | bo_mul | bo_div | bo_mod ― ‹Standard arith›
| bo_less | bo_less_eq | bo_eq                  ― ‹Comparison›
| bo_and | bo_or | bo_xor                       ― ‹Bit-Wise›

datatype un_op =                    ― ‹ Unary operators ›
uo_minus | uo_not

(* Expressions *)
datatype exp =
e_var ident                       ― ‹ Variable (local/global based on scope) ›
| e_localvar ident                  ― ‹ Local variable ›
| e_globalvar ident                 ― ‹ Global variable ›
| e_const numeric                   ― ‹ Numeric constant ›
| e_bin bin_op exp exp              ― ‹ Binary operators ›
| e_un un_op exp                    ― ‹ Unary operators ›

(* Commands *)
datatype cmd =
Assign exp ident exp | Assign_local exp ident exp | Assign_global exp ident exp
| Test exp
| Skip
| Seq cmd cmd | Or cmd cmd                  ― ‹Control flow›
| Break | Continue                          ― ‹More control flow›
| Iterate cmd cmd                           ― ‹Iterate command›
| Invalid                                   ― ‹Internal: Invalid command›

definition "Loop cmd ≡ Iterate cmd cmd"    ― ‹Syntactic sugar›

text ‹A variable declaration just contains a name›
type_synonym var_decl = ident

text ‹A process contains a body and local variable declarations›
record proc_decl =
name :: "ident"
body :: "cmd"
local_vars :: "var_decl list"

text ‹A program contains process declarations and global variable
declarations›
record program =
processes :: "proc_decl list"
global_vars :: "var_decl list"

end
```