Theory J1

(*  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 expr1 = "nat exp"
type_synonym J1_prog = "expr1 prog"
type_synonym state1 = "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(e1 «bop» e2) = max (max_vars e1) (max_vars e2)"
| "max_vars(Var V) = 0"
| "max_vars(V:=e) = max_vars e"
| "max_vars(e∙F{D}) = max_vars e"
| "max_vars(FAss e1 F D e2) = max (max_vars e1) (max_vars e2)"
| "max_vars(e∙M(es)) = max (max_vars e) (max_varss es)"
| "max_vars({V:T; e}) = max_vars e + 1"
| "max_vars(e1;;e2) = max (max_vars e1) (max_vars e2)"
| "max_vars(if (e) e1 else e2) =
   max (max_vars e) (max (max_vars e1) (max_vars e2))"
| "max_vars(while (b) e) = max (max_vars b) (max_vars e)"
| "max_vars(throw e) = max_vars e"
| "max_vars(try e1 catch(C V) e2) = max (max_vars e1) (max_vars e2 + 1)"

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

inductive
  eval1 :: "J1_prog ⇒ expr1 ⇒ state1 ⇒ expr1 ⇒ state1 ⇒ bool"
          ("_ ⊢1 ((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  and evals1 :: "J1_prog ⇒ expr1 list ⇒ state1 ⇒ expr1 list ⇒ state1 ⇒ bool"
           ("_ ⊢1 ((1⟨_,/_⟩) [⇒]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  for P :: J1_prog
where

  New1:
  "⟦ new_Addr h = Some a; P ⊢ C has_fields FDTs; h' = h(a↦(C,init_fields FDTs)) ⟧
  ⟹ P ⊢1 ⟨new C,(h,l)⟩ ⇒ ⟨addr a,(h',l)⟩"
| NewFail1:
  "new_Addr h = None ⟹
  P ⊢1 ⟨new C, (h,l)⟩ ⇒ ⟨THROW OutOfMemory,(h,l)⟩"

| Cast1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,(h,l)⟩; h a = Some(D,fs); P ⊢ D ≼* C ⟧
  ⟹ P ⊢1 ⟨Cast C e,s0⟩ ⇒ ⟨addr a,(h,l)⟩"
| CastNull1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢1 ⟨Cast C e,s0⟩ ⇒ ⟨null,s1⟩"
| CastFail1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,(h,l)⟩; h a = Some(D,fs); ¬ P ⊢ D ≼* C ⟧
  ⟹ P ⊢1 ⟨Cast C e,s0⟩ ⇒ ⟨THROW ClassCast,(h,l)⟩"
| CastThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨Cast C e,s0⟩ ⇒ ⟨throw e',s1⟩"

| Val1:
  "P ⊢1 ⟨Val v,s⟩ ⇒ ⟨Val v,s⟩"

| BinOp1:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨Val v1,s1⟩; P ⊢1 ⟨e2,s1⟩ ⇒ ⟨Val v2,s2⟩; binop(bop,v1,v2) = Some v ⟧
  ⟹ P ⊢1 ⟨e1 «bop» e2,s0⟩ ⇒ ⟨Val v,s2⟩"
| BinOpThrow11:
  "P ⊢1 ⟨e1,s0⟩ ⇒ ⟨throw e,s1⟩ ⟹
  P ⊢1 ⟨e1 «bop» e2, s0⟩ ⇒ ⟨throw e,s1⟩"
| BinOpThrow21:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨Val v1,s1⟩; P ⊢1 ⟨e2,s1⟩ ⇒ ⟨throw e,s2⟩ ⟧
  ⟹ P ⊢1 ⟨e1 «bop» e2,s0⟩ ⇒ ⟨throw e,s2⟩"

| Var1:
  "⟦ ls!i = v; i < size ls ⟧ ⟹
  P ⊢1 ⟨Var i,(h,ls)⟩ ⇒ ⟨Val v,(h,ls)⟩"

| LAss1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨Val v,(h,ls)⟩; i < size ls; ls' = ls[i := v] ⟧
  ⟹ P ⊢1 ⟨i:= e,s0⟩ ⇒ ⟨unit,(h,ls')⟩"
| LAssThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨i:= e,s0⟩ ⇒ ⟨throw e',s1⟩"

| FAcc1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,(h,ls)⟩; h a = Some(C,fs); fs(F,D) = Some v ⟧
  ⟹ P ⊢1 ⟨e∙F{D},s0⟩ ⇒ ⟨Val v,(h,ls)⟩"
| FAccNull1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢1 ⟨e∙F{D},s0⟩ ⇒ ⟨THROW NullPointer,s1⟩"
| FAccThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨e∙F{D},s0⟩ ⇒ ⟨throw e',s1⟩"

| FAss1:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨addr a,s1⟩; P ⊢1 ⟨e2,s1⟩ ⇒ ⟨Val v,(h2,l2)⟩;
    h2 a = Some(C,fs); fs' = fs((F,D)↦v); h2' = h2(a↦(C,fs')) ⟧
  ⟹ P ⊢1 ⟨e1∙F{D}:= e2,s0⟩ ⇒ ⟨unit,(h2',l2)⟩"
| FAssNull1:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨null,s1⟩;  P ⊢1 ⟨e2,s1⟩ ⇒ ⟨Val v,s2⟩ ⟧
  ⟹ P ⊢1 ⟨e1∙F{D}:= e2,s0⟩ ⇒ ⟨THROW NullPointer,s2⟩"
| FAssThrow11:
  "P ⊢1 ⟨e1,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨e1∙F{D}:= e2,s0⟩ ⇒ ⟨throw e',s1⟩"
| FAssThrow21:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢1 ⟨e2,s1⟩ ⇒ ⟨throw e',s2⟩ ⟧
  ⟹ P ⊢1 ⟨e1∙F{D}:= e2,s0⟩ ⇒ ⟨throw e',s2⟩"

| CallObjThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨e∙M(es),s0⟩ ⇒ ⟨throw e',s1⟩"
| CallNull1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨null,s1⟩; P ⊢1 ⟨es,s1⟩ [⇒] ⟨map Val vs,s2⟩ ⟧
  ⟹ P ⊢1 ⟨e∙M(es),s0⟩ ⇒ ⟨THROW NullPointer,s2⟩"
| Call1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩; P ⊢1 ⟨es,s1⟩ [⇒] ⟨map Val vs,(h2,ls2)⟩;
    h2 a = Some(C,fs); P ⊢ C sees M:Ts→T = body in D;
    size vs = size Ts; ls2' = (Addr a) # vs @ replicate (max_vars body) undefined;
    P ⊢1 ⟨body,(h2,ls2')⟩ ⇒ ⟨e',(h3,ls3)⟩ ⟧
  ⟹ P ⊢1 ⟨e∙M(es),s0⟩ ⇒ ⟨e',(h3,ls2)⟩"
| CallParamsThrow1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢1 ⟨es,s1⟩ [⇒] ⟨es',s2⟩;
     es' = map Val vs @ throw ex # es2 ⟧
   ⟹ P ⊢1 ⟨e∙M(es),s0⟩ ⇒ ⟨throw ex,s2⟩"

| Block1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨e',s1⟩ ⟹ P ⊢1 ⟨Block i T e,s0⟩ ⇒ ⟨e',s1⟩"

| Seq1:
  "⟦ P ⊢1 ⟨e0,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢1 ⟨e1,s1⟩ ⇒ ⟨e2,s2⟩ ⟧
  ⟹ P ⊢1 ⟨e0;;e1,s0⟩ ⇒ ⟨e2,s2⟩"
| SeqThrow1:
  "P ⊢1 ⟨e0,s0⟩ ⇒ ⟨throw e,s1⟩ ⟹
  P ⊢1 ⟨e0;;e1,s0⟩ ⇒ ⟨throw e,s1⟩"

| CondT1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢1 ⟨e1,s1⟩ ⇒ ⟨e',s2⟩ ⟧
  ⟹ P ⊢1 ⟨if (e) e1 else e2,s0⟩ ⇒ ⟨e',s2⟩"
| CondF1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨false,s1⟩; P ⊢1 ⟨e2,s1⟩ ⇒ ⟨e',s2⟩ ⟧
  ⟹ P ⊢1 ⟨if (e) e1 else e2,s0⟩ ⇒ ⟨e',s2⟩"
| CondThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨if (e) e1 else e2, s0⟩ ⇒ ⟨throw e',s1⟩"

| WhileF1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨false,s1⟩ ⟹
  P ⊢1 ⟨while (e) c,s0⟩ ⇒ ⟨unit,s1⟩"
| WhileT1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢1 ⟨c,s1⟩ ⇒ ⟨Val v1,s2⟩;
    P ⊢1 ⟨while (e) c,s2⟩ ⇒ ⟨e3,s3⟩ ⟧
  ⟹ P ⊢1 ⟨while (e) c,s0⟩ ⇒ ⟨e3,s3⟩"
| WhileCondThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨while (e) c,s0⟩ ⇒ ⟨throw e',s1⟩"
| WhileBodyThrow1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢1 ⟨c,s1⟩ ⇒ ⟨throw e',s2⟩⟧
  ⟹ P ⊢1 ⟨while (e) c,s0⟩ ⇒ ⟨throw e',s2⟩"

| Throw1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩ ⟹
  P ⊢1 ⟨throw e,s0⟩ ⇒ ⟨Throw a,s1⟩"
| ThrowNull1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢1 ⟨throw e,s0⟩ ⇒ ⟨THROW NullPointer,s1⟩"
| ThrowThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨throw e,s0⟩ ⇒ ⟨throw e',s1⟩"

| Try1:
  "P ⊢1 ⟨e1,s0⟩ ⇒ ⟨Val v1,s1⟩ ⟹
  P ⊢1 ⟨try e1 catch(C i) e2,s0⟩ ⇒ ⟨Val v1,s1⟩"
| TryCatch1:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨Throw a,(h1,ls1)⟩;
    h1 a = Some(D,fs); P ⊢ D ≼* C; i < length ls1;
    P ⊢1 ⟨e2,(h1,ls1[i:=Addr a])⟩ ⇒ ⟨e2',(h2,ls2)⟩ ⟧
  ⟹ P ⊢1 ⟨try e1 catch(C i) e2,s0⟩ ⇒ ⟨e2',(h2,ls2)⟩"
| TryThrow1:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨Throw a,(h1,ls1)⟩; h1 a = Some(D,fs); ¬ P ⊢ D ≼* C ⟧
  ⟹ P ⊢1 ⟨try e1 catch(C i) e2,s0⟩ ⇒ ⟨Throw a,(h1,ls1)⟩"

| Nil1:
  "P ⊢1 ⟨[],s⟩ [⇒] ⟨[],s⟩"

| Cons1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢1 ⟨es,s1⟩ [⇒] ⟨es',s2⟩ ⟧
  ⟹ P ⊢1 ⟨e#es,s0⟩ [⇒] ⟨Val v # es',s2⟩"
| ConsThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨e#es,s0⟩ [⇒] ⟨throw e' # es, s1⟩"

(*<*)
lemmas eval1_evals1_induct = eval1_evals1.induct [split_format (complete)]
  and eval1_evals1_inducts = eval1_evals1.inducts [split_format (complete)]
(*>*)

lemma eval1_preserves_len:
  "P ⊢1 ⟨e0,(h0,ls0)⟩ ⇒ ⟨e1,(h1,ls1)⟩ ⟹ length ls0 = length ls1"
and evals1_preserves_len:
  "P ⊢1 ⟨es0,(h0,ls0)⟩ [⇒] ⟨es1,(h1,ls1)⟩ ⟹ length ls0 = length ls1"
(*<*)by (induct rule:eval1_evals1_inducts, simp_all)(*>*)


lemma evals1_preserves_elen:
  "⋀es' s s'. P ⊢1 ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ length es = length es'"
(*<*)by(induct es type:list) (auto elim:evals1.cases)(*>*)


lemma eval1_final: "P ⊢1 ⟨e,s⟩ ⇒ ⟨e',s'⟩ ⟹ final e'"
 and evals1_final: "P ⊢1 ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ finals es'"
(*<*)by(induct rule:eval1_evals1.inducts, simp_all)(*>*)


end