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