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

chapter ‹Compilation \label{cha:comp}›

section ‹An Intermediate Language›

theory J1 imports "../J/BigStep" begin

type_synonym expr₁ = "nat exp"
type_synonym J₁_prog = "expr₁ prog"
type_synonym state₁ = "heap × (val list)"

primrec
  max_vars :: "'a exp → nat"
  and max_varss :: "'a exp list → nat"
where
  "max_vars(new C) = 0"
| "max_vars(Cast C e) = max_vars e"
| "max_vars(Val v) = 0"
| "max_vars(e₁ «bop¬ e₂) = max (max_vars e₁) (max_vars e₂)"
| "max_vars(Var V) = 0"
| "max_vars(V:=e) = max_vars e"
| "max_vars(e∙F{D}) = max_vars e"
| "max_vars(FAss e₁ F D e₂) = max (max_vars e₁) (max_vars e₂)"
| "max_vars(e∙M(es)) = max (max_vars e) (max_varss es)"
| "max_vars({V:T; e}) = max_vars e + 1"
| "max_vars(e₁;;e₂) = max (max_vars e₁) (max_vars e₂)"
| "max_vars(if (e) e₁ else e₂) =
   max (max_vars e) (max (max_vars e₁) (max_vars e₂))"
| "max_vars(while (b) e) = max (max_vars b) (max_vars e)"
| "max_vars(throw e) = max_vars e"
| "max_vars(try e₁ catch(C V) e₂) = max (max_vars e₁) (max_vars e₂ + 1)"

| "max_varss [] = 0"
| "max_varss (e#es) = max (max_vars e) (max_varss es)"

inductive
  eval₁ :: "J₁_prog → expr₁ → state₁ → expr₁ → state₁ → bool"
          (‹_ ⊨₁ ((1⟨_,/_⟩) →/ (1⟨_,/_⟩))› [51,0,0,0,0] 81)
  and evals₁ :: "J₁_prog → expr₁ list → state₁ → expr₁ list → state₁ → bool"
           (‹_ ⊨₁ ((1⟨_,/_⟩) [→]/ (1⟨_,/_⟩))› [51,0,0,0,0] 81)
  for P :: J₁_prog
where

  New₁:
  "[ new_Addr h = Some a; P ⊨ C has_fields FDTs; h' = h(a↦(C,init_fields FDTs)) ]
  ==> P ⊨₁ ⟨new C,(h,l)⟩ → ⟨addr a,(h',l)⟩"
| NewFail₁:
  "new_Addr h = None ==>
  P ⊨₁ ⟨new C, (h,l)⟩ → ⟨THROW OutOfMemory,(h,l)⟩"

| Cast₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨addr a,(h,l)⟩; h a = Some(D,fs); P ⊨ D ⪯^* C ]
  ==> P ⊨₁ ⟨Cast C e,s₀⟩ → ⟨addr a,(h,l)⟩"
| CastNull₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨null,s₁⟩ ==>
  P ⊨₁ ⟨Cast C e,s₀⟩ → ⟨null,s₁⟩"
| CastFail₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨addr a,(h,l)⟩; h a = Some(D,fs); ¬ P ⊨ D ⪯^* C ]
  ==> P ⊨₁ ⟨Cast C e,s₀⟩ → ⟨THROW ClassCast,(h,l)⟩"
| CastThrow₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨₁ ⟨Cast C e,s₀⟩ → ⟨throw e',s₁⟩"

| Val₁:
  "P ⊨₁ ⟨Val v,s⟩ → ⟨Val v,s⟩"

| BinOp₁:
  "[ P ⊨₁ ⟨e₁,s₀⟩ → ⟨Val v₁,s₁⟩; P ⊨₁ ⟨e₂,s₁⟩ → ⟨Val v₂,s₂⟩; binop(bop,v₁,v₂) = Some v ]
  ==> P ⊨₁ ⟨e₁ «bop¬ e₂,s₀⟩ → ⟨Val v,s₂⟩"
| BinOpThrow₁₁:
  "P ⊨₁ ⟨e₁,s₀⟩ → ⟨throw e,s₁⟩ ==>
  P ⊨₁ ⟨e₁ «bop¬ e₂, s₀⟩ → ⟨throw e,s₁⟩"
| BinOpThrow₂₁:
  "[ P ⊨₁ ⟨e₁,s₀⟩ → ⟨Val v₁,s₁⟩; P ⊨₁ ⟨e₂,s₁⟩ → ⟨throw e,s₂⟩ ]
  ==> P ⊨₁ ⟨e₁ «bop¬ e₂,s₀⟩ → ⟨throw e,s₂⟩"

| Var₁:
  "[ ls!i = v; i < size ls ] ==>
  P ⊨₁ ⟨Var i,(h,ls)⟩ → ⟨Val v,(h,ls)⟩"

| LAss₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨Val v,(h,ls)⟩; i < size ls; ls' = ls[i := v] ]
  ==> P ⊨₁ ⟨i:= e,s₀⟩ → ⟨unit,(h,ls')⟩"
| LAssThrow₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨₁ ⟨i:= e,s₀⟩ → ⟨throw e',s₁⟩"

| FAcc₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨addr a,(h,ls)⟩; h a = Some(C,fs); fs(F,D) = Some v ]
  ==> P ⊨₁ ⟨e∙F{D},s₀⟩ → ⟨Val v,(h,ls)⟩"
| FAccNull₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨null,s₁⟩ ==>
  P ⊨₁ ⟨e∙F{D},s₀⟩ → ⟨THROW NullPointer,s₁⟩"
| FAccThrow₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨₁ ⟨e∙F{D},s₀⟩ → ⟨throw e',s₁⟩"

| FAss₁:
  "[ P ⊨₁ ⟨e₁,s₀⟩ → ⟨addr a,s₁⟩; P ⊨₁ ⟨e₂,s₁⟩ → ⟨Val v,(h₂,l₂)⟩;
    h₂ a = Some(C,fs); fs' = fs((F,D)↦v); h₂' = h₂(a↦(C,fs')) ]
  ==> P ⊨₁ ⟨e₁∙F{D}:= e₂,s₀⟩ → ⟨unit,(h₂',l₂)⟩"
| FAssNull₁:
  "[ P ⊨₁ ⟨e₁,s₀⟩ → ⟨null,s₁⟩; P ⊨₁ ⟨e₂,s₁⟩ → ⟨Val v,s₂⟩ ]
  ==> P ⊨₁ ⟨e₁∙F{D}:= e₂,s₀⟩ → ⟨THROW NullPointer,s₂⟩"
| FAssThrow₁₁:
  "P ⊨₁ ⟨e₁,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨₁ ⟨e₁∙F{D}:= e₂,s₀⟩ → ⟨throw e',s₁⟩"
| FAssThrow₂₁:
  "[ P ⊨₁ ⟨e₁,s₀⟩ → ⟨Val v,s₁⟩; P ⊨₁ ⟨e₂,s₁⟩ → ⟨throw e',s₂⟩ ]
  ==> P ⊨₁ ⟨e₁∙F{D}:= e₂,s₀⟩ → ⟨throw e',s₂⟩"

| CallObjThrow₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨₁ ⟨e∙M(es),s₀⟩ → ⟨throw e',s₁⟩"
| CallNull₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨null,s₁⟩; P ⊨₁ ⟨es,s₁⟩ [→] ⟨map Val vs,s₂⟩ ]
  ==> P ⊨₁ ⟨e∙M(es),s₀⟩ → ⟨THROW NullPointer,s₂⟩"
| Call₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨addr a,s₁⟩; P ⊨₁ ⟨es,s₁⟩ [→] ⟨map Val vs,(h₂,ls₂)⟩;
    h₂ a = Some(C,fs); P ⊨ C sees M:Ts→T = body in D;
    size vs = size Ts; ls₂' = (Addr a) # vs @ replicate (max_vars body) undefined;
    P ⊨₁ ⟨body,(h₂,ls₂')⟩ → ⟨e',(h₃,ls₃)⟩ ]
  ==> P ⊨₁ ⟨e∙M(es),s₀⟩ → ⟨e',(h₃,ls₂)⟩"
| CallParamsThrow₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨Val v,s₁⟩; P ⊨₁ ⟨es,s₁⟩ [→] ⟨es',s₂⟩;
     es' = map Val vs @ throw ex # es₂ ]
   ==> P ⊨₁ ⟨e∙M(es),s₀⟩ → ⟨throw ex,s₂⟩"

| Block₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨e',s₁⟩ ==> P ⊨₁ ⟨Block i T e,s₀⟩ → ⟨e',s₁⟩"

| Seq₁:
  "[ P ⊨₁ ⟨e₀,s₀⟩ → ⟨Val v,s₁⟩; P ⊨₁ ⟨e₁,s₁⟩ → ⟨e₂,s₂⟩ ]
  ==> P ⊨₁ ⟨e₀;;e₁,s₀⟩ → ⟨e₂,s₂⟩"
| SeqThrow₁:
  "P ⊨₁ ⟨e₀,s₀⟩ → ⟨throw e,s₁⟩ ==>
  P ⊨₁ ⟨e₀;;e₁,s₀⟩ → ⟨throw e,s₁⟩"

| CondT₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨true,s₁⟩; P ⊨₁ ⟨e₁,s₁⟩ → ⟨e',s₂⟩ ]
  ==> P ⊨₁ ⟨if (e) e₁ else e₂,s₀⟩ → ⟨e',s₂⟩"
| CondF₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨false,s₁⟩; P ⊨₁ ⟨e₂,s₁⟩ → ⟨e',s₂⟩ ]
  ==> P ⊨₁ ⟨if (e) e₁ else e₂,s₀⟩ → ⟨e',s₂⟩"
| CondThrow₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨₁ ⟨if (e) e₁ else e₂, s₀⟩ → ⟨throw e',s₁⟩"

| WhileF₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨false,s₁⟩ ==>
  P ⊨₁ ⟨while (e) c,s₀⟩ → ⟨unit,s₁⟩"
| WhileT₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨true,s₁⟩; P ⊨₁ ⟨c,s₁⟩ → ⟨Val v₁,s₂⟩;
    P ⊨₁ ⟨while (e) c,s₂⟩ → ⟨e₃,s₃⟩ ]
  ==> P ⊨₁ ⟨while (e) c,s₀⟩ → ⟨e₃,s₃⟩"
| WhileCondThrow₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨₁ ⟨while (e) c,s₀⟩ → ⟨throw e',s₁⟩"
| WhileBodyThrow₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨true,s₁⟩; P ⊨₁ ⟨c,s₁⟩ → ⟨throw e',s₂⟩]
  ==> P ⊨₁ ⟨while (e) c,s₀⟩ → ⟨throw e',s₂⟩"

| Throw₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨addr a,s₁⟩ ==>
  P ⊨₁ ⟨throw e,s₀⟩ → ⟨Throw a,s₁⟩"
| ThrowNull₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨null,s₁⟩ ==>
  P ⊨₁ ⟨throw e,s₀⟩ → ⟨THROW NullPointer,s₁⟩"
| ThrowThrow₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨₁ ⟨throw e,s₀⟩ → ⟨throw e',s₁⟩"

| Try₁:
  "P ⊨₁ ⟨e₁,s₀⟩ → ⟨Val v₁,s₁⟩ ==>
  P ⊨₁ ⟨try e₁ catch(C i) e₂,s₀⟩ → ⟨Val v₁,s₁⟩"
| TryCatch₁:
  "[ P ⊨₁ ⟨e₁,s₀⟩ → ⟨Throw a,(h₁,ls₁)⟩;
    h₁ a = Some(D,fs); P ⊨ D ⪯^* C; i < length ls₁;
    P ⊨₁ ⟨e₂,(h₁,ls₁[i:=Addr a])⟩ → ⟨e₂',(h₂,ls₂)⟩ ]
  ==> P ⊨₁ ⟨try e₁ catch(C i) e₂,s₀⟩ → ⟨e₂',(h₂,ls₂)⟩"
| TryThrow₁:
  "[ P ⊨₁ ⟨e₁,s₀⟩ → ⟨Throw a,(h₁,ls₁)⟩; h₁ a = Some(D,fs); ¬ P ⊨ D ⪯^* C ]
  ==> P ⊨₁ ⟨try e₁ catch(C i) e₂,s₀⟩ → ⟨Throw a,(h₁,ls₁)⟩"

| Nil₁:
  "P ⊨₁ ⟨[],s⟩ [→] ⟨[],s⟩"

| Cons₁:
  "[ P ⊨₁ ⟨e,s₀⟩ → ⟨Val v,s₁⟩; P ⊨₁ ⟨es,s₁⟩ [→] ⟨es',s₂⟩ ]
  ==> P ⊨₁ ⟨e#es,s₀⟩ [→] ⟨Val v # es',s₂⟩"
| ConsThrow₁:
  "P ⊨₁ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨₁ ⟨e#es,s₀⟩ [→] ⟨throw e' # es, s₁⟩"

(*<*)
lemmas eval₁_evals₁_induct = eval₁_evals₁.induct [split_format (complete)]
  and eval₁_evals₁_inducts = eval₁_evals₁.inducts [split_format (complete)]
(*>*)

lemma eval₁_preserves_len:
  "P ⊨₁ ⟨e₀,(h₀,ls₀)⟩ → ⟨e₁,(h₁,ls₁)⟩ ==> length ls₀ = length ls₁"
and evals₁_preserves_len:
  "P ⊨₁ ⟨es₀,(h₀,ls₀)⟩ [→] ⟨es₁,(h₁,ls₁)⟩ ==> length ls₀ = length ls₁"
(*<*)by (induct rule:eval\<^sub>1_evals\<^sub>1_inducts, simp_all)(*>*)


lemma evals₁_preserves_elen:
  "∧es' s s'. P ⊨₁ ⟨es,s⟩ [→] ⟨es',s'⟩ ==> length es = length es'"
(*<*)by(induct es type:list) (auto elim:evals\<^sub>1.cases)(*>*)


lemma eval₁_final: "P ⊨₁ ⟨e,s⟩ → ⟨e',s'⟩ ==> final e'"
 and evals₁_final: "P ⊨₁ ⟨es,s⟩ [→] ⟨es',s'⟩ ==> finals es'"
(*<*)by(induct rule:eval\<^sub>1_evals\<^sub>1.inducts, simp_all)(*>*)


end