(*  Title:      Jinja/J/Expr.thy
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Expressions›

theory Expr
imports "../Common/Exceptions"
begin

datatype bop = Eq | Add     ― ‹names of binary operations›

datatype 'a exp
  = new cname      ― ‹class instance creation›
  | Cast cname "('a exp)"      ― ‹type cast›
  | Val val      ― ‹value›
  | BinOp "('a exp)" bop "('a exp)"     (‹_ «_¬ _› [80,0,81] 80)      ― ‹binary operation›
  | Var 'a                                               ― ‹local variable (incl. parameter)›
  | LAss 'a "('a exp)"     (‹_:=_› [90,90]90)                    ― ‹local assignment›
  | FAcc "('a exp)" vname cname     (‹_∙_{_}› [10,90,99]90)      ― ‹field access›
  | FAss "('a exp)" vname cname "('a exp)"     (‹_∙_{_} := _› [10,90,99,90]90)      ― ‹field assignment›
  | Call "('a exp)" mname "('a exp list)"     (‹_∙_'(_')› [90,99,0] 90)            ― ‹method call›
  | Block 'a ty "('a exp)"     (‹'{_:_; _}›)
  | Seq "('a exp)" "('a exp)"     (‹_;;/ _›             [61,60]60)
  | Cond "('a exp)" "('a exp)" "('a exp)"     (‹if '(_') _/ else _› [80,79,79]70)
  | While "('a exp)" "('a exp)"     (‹while '(_') _›     [80,79]70)
  | throw "('a exp)"
  | TryCatch "('a exp)" cname 'a "('a exp)"     (‹try _/ catch'(_ _') _›  [0,99,80,79] 70)

type_synonym
  expr = "vname exp"            ― ‹Jinja expression›
type_synonym
  J_mb = "vname list × expr"    ― ‹Jinja method body: parameter names and expression›
type_synonym
  J_prog = "J_mb prog"          ― ‹Jinja program›

text‹The semantics of binary operators:›

fun binop :: "bop × val × val → val option" where
  "binop(Eq,v₁,v₂) = Some(Bool (v₁ = v₂))"
| "binop(Add,Intg i₁,Intg i₂) = Some(Intg(i₁+i₂))"
| "binop(bop,v₁,v₂) = None"

lemma [simp]:
  "(binop(Add,v₁,v₂) = Some v) = (∃i₁ i₂. v₁ = Intg i₁ ∧ v₂ = Intg i₂ ∧ v = Intg(i₁+i₂))"
(*<*)by(cases v\<^sub>1; cases v\<^sub>2) auto(*>*)


subsection "Syntactic sugar"

abbreviation (input)
  InitBlock:: "'a → ty → 'a exp → 'a exp → 'a exp"   (‹(1'{_:_ := _;/ _})›) where
  "InitBlock V T e1 e2 == {V:T; V := e1;; e2}"

abbreviation unit where "unit == Val Unit"
abbreviation null where "null == Val Null"
abbreviation "addr a == Val(Addr a)"
abbreviation "true == Val(Bool True)"
abbreviation "false == Val(Bool False)"

abbreviation
  Throw :: "addr → 'a exp" where
  "Throw a == throw(Val(Addr a))"

abbreviation
  THROW :: "cname → 'a exp" where
  "THROW xc == Throw(addr_of_sys_xcpt xc)"


subsection‹Free Variables›

primrec fv :: "expr → vname set" and fvs :: "expr list → vname set" where
  "fv(new C) = {}"
| "fv(Cast C e) = fv e"
| "fv(Val v) = {}"
| "fv(e₁ «bop¬ e₂) = fv e₁ ∪ fv e₂"
| "fv(Var V) = {V}"
| "fv(LAss V e) = {V} ∪ fv e"
| "fv(e∙F{D}) = fv e"
| "fv(e₁∙F{D}:=e₂) = fv e₁ ∪ fv e₂"
| "fv(e∙M(es)) = fv e ∪ fvs es"
| "fv({V:T; e}) = fv e - {V}"
| "fv(e₁;;e₂) = fv e₁ ∪ fv e₂"
| "fv(if (b) e₁ else e₂) = fv b ∪ fv e₁ ∪ fv e₂"
| "fv(while (b) e) = fv b ∪ fv e"
| "fv(throw e) = fv e"
| "fv(try e₁ catch(C V) e₂) = fv e₁ ∪ (fv e₂ - {V})"
| "fvs([]) = {}"
| "fvs(e#es) = fv e ∪ fvs es"

lemma [simp]: "fvs(es₁ @ es₂) = fvs es₁ ∪ fvs es₂"
(*<*)by (induct es\<^sub>1 type:list) auto(*>*)

lemma [simp]: "fvs(map Val vs) = {}"
(*<*)by (induct vs) auto(*>*)

end