Theory Term

(*  Title:      HOL/NanoJava/Term.thy
    Author:     David von Oheimb, Technische Universitaet Muenchen
*)

section "Statements and expression emulations"

theory Term imports Main begin

typedecl cname  ― ‹class    name›
typedecl mname  ― ‹method   name›
typedecl fname  ― ‹field    name›
typedecl vname  ― ‹variable name›

axiomatization
  This ― ‹This pointer›
  Par  ― ‹method parameter›
  Res  :: vname ― ‹method result›
 ― ‹Inequality axioms are not required for the meta theory.›
(*
where
  This_neq_Par [simp]: "This ≠ Par"
  Par_neq_Res  [simp]: "Par ≠ Res"
  Res_neq_This [simp]: "Res ≠ This"
*)

datatype stmt
  = Skip                   ― ‹empty statement›
  | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
  | Cond expr  stmt stmt   ("If '(_') _ Else _" [ 3,91,91] 91)
  | Loop vname stmt        ("While '(_') _"     [ 3,91   ] 91)
  | LAss vname expr        ("_ :== _"           [99,   95] 94) ― ‹local assignment›
  | FAss expr  fname expr  ("_.._:==_"          [95,99,95] 94) ― ‹field assignment›
  | Meth "cname × mname"   ― ‹virtual method›
  | Impl "cname × mname"   ― ‹method implementation›
and expr
  = NewC cname       ("new _"        [   99] 95) ― ‹object creation›
  | Cast cname expr                              ― ‹type cast›
  | LAcc vname                                   ― ‹local access›
  | FAcc expr  fname ("_.._"         [95,99] 95) ― ‹field access›
  | Call cname expr mname expr                   
                     ("{_}_.._'(_')" [99,95,99,95] 95) ― ‹method call›

end