Theory Term

theory Term
imports Main
(*  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