section ‹Abstract Syntax of IMP2›
theory Syntax
imports Main
begin

  text ‹We define the abstract syntax of the IMP2 language,
 and a minimal concrete syntax for direct use in terms.›


  subsection ‹Primitives›  
  text ‹Variable and procedure names are strings.›
  type_synonym vname = string
  type_synonym pname = string

  text ‹The variable names are partitioned into local and global variables.›
  fun is_global :: "vname → bool" where
    "is_global [] ⟷ True"
  | "is_global (CHR ''G''#_) ⟷ True"
  | "is_global _ ⟷ False"

  abbreviation "is_local a ≡ ¬is_global a"
  
  
    
  text ‹
 Primitive values are integers,
 and values are arrays modeled as functions from integers to primitive values.
 
 Note that values and primitive values are usually part of the semantics, however,
 as they occur as literals in the abstract syntax, we already define them here.
 ›
  
  type_synonym pval = "int"
  type_synonym val = "int → pval"

  (*
    TODO: Cf. SortedAlgebra, used in CeTa. Akihisa Yamada
      Should give aexp, bexp with type-checking, term ops, etc.
  
  *)

  subsection ‹Arithmetic Expressions›
  text ‹Arithmetic expressions consist of constants, indexed array variables,
 and unary and binary operations. The operations are modeled by reflecting
 arbitrary functions into the abstract syntax.›
  
  datatype aexp = 
      N int 
    | Vidx vname aexp
    | Unop "int → int" aexp 
    | Binop "int → int → int" aexp aexp
    
  subsection ‹Boolean Expressions›
  text ‹Boolean expressions consist of constants, the not operation, binary connectives,
 and comparison operations. Binary connectives and comparison operations are modeled by
 reflecting arbitrary functions into the abstract syntax. The not operation is the only
 meaningful unary Boolean operation, so we chose to model it explicitly instead of
 reflecting and unary Boolean function.›
    
  datatype bexp = 
      Bc bool 
    | Not bexp 
    | BBinop "bool → bool → bool" bexp bexp 
    | Cmpop "int → int → bool" aexp aexp

    
  subsection ‹Commands›
  text ‹
 The commands can roughly be put into five categories:
 🚫[Skip] The no-op command
 🚫[Assignment commands] Commands to assign the value of an arithmetic expression, copy or clear arrays,
 and a command to simultaneously assign all local variables, which is only used internally
 to simplify the definition of a small-step semantics.
 🚫[Block commands] The standard sequential composition, if-then-else, and while commands,
 and a scope command which executes a command with a fresh set of local variables.
 🚫[Procedure commands] Procedure call, and a procedure scope command, which executes
 a command in a specified procedure environment. Similar to the scope command,
 which introduces new local variables, and thus limits the effect of variable manipulations
 to the content of the command, the procedure scope command introduces new procedures,
 and limits the validity of their names to the content of the command. This greatly
 simplifies modular definition of programs, as procedure names can be used locally.
 
 ›
  
  
  datatype
    com = 
        SKIP                              ― ‹No-op›
        
        ― ‹Assignment›
        | AssignIdx vname aexp aexp       ― ‹Assign to index in array›
        | ArrayCpy vname vname            ― ‹Copy whole array›
        | ArrayClear vname                ― ‹Clear array›
        | Assign_Locals "vname → val"    ― ‹Internal: Assign all local variables simultaneously›
        
        ― ‹Block›
        | Seq    com  com                 ― ‹Sequential composition›
        | If     bexp com com             ― ‹Conditional›
        | While  bexp com                 ― ‹While-loop›
        | Scope com                       ― ‹Local variable scope›
        
        ― ‹Procedure›
        | PCall pname                     ― ‹Procedure call›
        | PScope "pname ⇀ com" com       ― ‹Procedure scope›

  subsubsection ‹Minimal Concrete Syntax›
  text ‹The commands come with a minimal concrete syntax, which is compatible
 to the syntax of ‹IMP›.›
  
  notation AssignIdx      (‹_[_] ::= _› [1000, 0, 61] 61)
  notation ArrayCpy       (‹_[] ::= _› [1000, 1000] 61)
  notation ArrayClear     (‹CLEAR _[]› [1000] 61)
  
  notation Seq            (‹_;;/ _›  [61, 60] 60)
  notation If             (‹(IF _/ THEN _/ ELSE _)›  [0, 0, 61] 61)
  notation While          (‹(WHILE _/ DO _)›  [0, 61] 61)
  notation Scope          (‹SCOPE _› [61] 61)
        
        
  subsection ‹Program›                
  type_synonym program = "pname ⇀ com"
        

  subsection ‹Default Array Index›
  text ‹We define abbreviations to make arrays look like plain integer variables:
 Without explicitly specifying an array index, the index ‹0› will be used automatically.
 ›
  
  abbreviation "V x ≡ Vidx x (N 0)"  
  abbreviation Assign (‹_ ::= _› [1000, 61] 61) 
    where "x ::= a ≡ (x[N 0] ::= a)"
        
   
end