# Theory J1

(*  Title:      Jinja/Compiler/J1.thy
Author:     Tobias Nipkow
*)

chapter ‹Compilation \label{cha:comp}›

section ‹An Intermediate Language›

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

type_synonym expr⇩1 = "nat exp"
type_synonym J⇩1_prog = "expr⇩1 prog"
type_synonym state⇩1 = "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⇩1 «bop» e⇩2) = max (max_vars e⇩1) (max_vars e⇩2)"
| "max_vars(Var V) = 0"
| "max_vars(V:=e) = max_vars e"
| "max_vars(e∙F{D}) = max_vars e"
| "max_vars(FAss e⇩1 F D e⇩2) = max (max_vars e⇩1) (max_vars e⇩2)"
| "max_vars(e∙M(es)) = max (max_vars e) (max_varss es)"
| "max_vars({V:T; e}) = max_vars e + 1"
| "max_vars(e⇩1;;e⇩2) = max (max_vars e⇩1) (max_vars e⇩2)"
| "max_vars(if (e) e⇩1 else e⇩2) =
max (max_vars e) (max (max_vars e⇩1) (max_vars e⇩2))"
| "max_vars(while (b) e) = max (max_vars b) (max_vars e)"
| "max_vars(throw e) = max_vars e"
| "max_vars(try e⇩1 catch(C V) e⇩2) = max (max_vars e⇩1) (max_vars e⇩2 + 1)"

inductive
eval⇩1 :: "J⇩1_prog ⇒ expr⇩1 ⇒ state⇩1 ⇒ expr⇩1 ⇒ state⇩1 ⇒ bool"
("_ ⊢⇩1 ((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
and evals⇩1 :: "J⇩1_prog ⇒ expr⇩1 list ⇒ state⇩1 ⇒ expr⇩1 list ⇒ state⇩1 ⇒ bool"
("_ ⊢⇩1 ((1⟨_,/_⟩) [⇒]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
for P :: J⇩1_prog
where

New⇩1:
"⟦ 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)⟩"
| NewFail⇩1:
P ⊢⇩1 ⟨new C, (h,l)⟩ ⇒ ⟨THROW OutOfMemory,(h,l)⟩"

| Cast⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨addr a,(h,l)⟩; h a = Some(D,fs); P ⊢ D ≼⇧* C ⟧
⟹ P ⊢⇩1 ⟨Cast C e,s⇩0⟩ ⇒ ⟨addr a,(h,l)⟩"
| CastNull⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
P ⊢⇩1 ⟨Cast C e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩"
| CastFail⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨addr a,(h,l)⟩; h a = Some(D,fs); ¬ P ⊢ D ≼⇧* C ⟧
⟹ P ⊢⇩1 ⟨Cast C e,s⇩0⟩ ⇒ ⟨THROW ClassCast,(h,l)⟩"
| CastThrow⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨Cast C e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

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

| BinOp⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩; P ⊢⇩1 ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v⇩2,s⇩2⟩; binop(bop,v⇩1,v⇩2) = Some v ⟧
⟹ P ⊢⇩1 ⟨e⇩1 «bop» e⇩2,s⇩0⟩ ⇒ ⟨Val v,s⇩2⟩"
| BinOpThrow⇩1⇩1:
"P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e,s⇩1⟩ ⟹
P ⊢⇩1 ⟨e⇩1 «bop» e⇩2, s⇩0⟩ ⇒ ⟨throw e,s⇩1⟩"
| BinOpThrow⇩2⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩; P ⊢⇩1 ⟨e⇩2,s⇩1⟩ ⇒ ⟨throw e,s⇩2⟩ ⟧
⟹ P ⊢⇩1 ⟨e⇩1 «bop» e⇩2,s⇩0⟩ ⇒ ⟨throw e,s⇩2⟩"

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

| LAss⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨Val v,(h,ls)⟩; i < size ls; ls' = ls[i := v] ⟧
⟹ P ⊢⇩1 ⟨i:= e,s⇩0⟩ ⇒ ⟨unit,(h,ls')⟩"
| LAssThrow⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨i:= e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| FAcc⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨addr a,(h,ls)⟩; h a = Some(C,fs); fs(F,D) = Some v ⟧
⟹ P ⊢⇩1 ⟨e∙F{D},s⇩0⟩ ⇒ ⟨Val v,(h,ls)⟩"
| FAccNull⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
P ⊢⇩1 ⟨e∙F{D},s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩1⟩"
| FAccThrow⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨e∙F{D},s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| FAss⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩; P ⊢⇩1 ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v,(h⇩2,l⇩2)⟩;
h⇩2 a = Some(C,fs); fs' = fs((F,D)↦v); h⇩2' = h⇩2(a↦(C,fs')) ⟧
⟹ P ⊢⇩1 ⟨e⇩1∙F{D}:= e⇩2,s⇩0⟩ ⇒ ⟨unit,(h⇩2',l⇩2)⟩"
| FAssNull⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨null,s⇩1⟩;  P ⊢⇩1 ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v,s⇩2⟩ ⟧
⟹ P ⊢⇩1 ⟨e⇩1∙F{D}:= e⇩2,s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩2⟩"
| FAssThrow⇩1⇩1:
"P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨e⇩1∙F{D}:= e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"
| FAssThrow⇩2⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P ⊢⇩1 ⟨e⇩2,s⇩1⟩ ⇒ ⟨throw e',s⇩2⟩ ⟧
⟹ P ⊢⇩1 ⟨e⇩1∙F{D}:= e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"

| CallObjThrow⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨e∙M(es),s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"
| CallNull⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩; P ⊢⇩1 ⟨es,s⇩1⟩ [⇒] ⟨map Val vs,s⇩2⟩ ⟧
⟹ P ⊢⇩1 ⟨e∙M(es),s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩2⟩"
| Call⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩; P ⊢⇩1 ⟨es,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,ls⇩2)⟩;
h⇩2 a = Some(C,fs); P ⊢ C sees M:Ts→T = body in D;
size vs = size Ts; ls⇩2' = (Addr a) # vs @ replicate (max_vars body) undefined;
P ⊢⇩1 ⟨body,(h⇩2,ls⇩2')⟩ ⇒ ⟨e',(h⇩3,ls⇩3)⟩ ⟧
⟹ P ⊢⇩1 ⟨e∙M(es),s⇩0⟩ ⇒ ⟨e',(h⇩3,ls⇩2)⟩"
| CallParamsThrow⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P ⊢⇩1 ⟨es,s⇩1⟩ [⇒] ⟨es',s⇩2⟩;
es' = map Val vs @ throw ex # es⇩2 ⟧
⟹ P ⊢⇩1 ⟨e∙M(es),s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩"

| Block⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨e',s⇩1⟩ ⟹ P ⊢⇩1 ⟨Block i T e,s⇩0⟩ ⇒ ⟨e',s⇩1⟩"

| Seq⇩1:
"⟦ P ⊢⇩1 ⟨e⇩0,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P ⊢⇩1 ⟨e⇩1,s⇩1⟩ ⇒ ⟨e⇩2,s⇩2⟩ ⟧
⟹ P ⊢⇩1 ⟨e⇩0;;e⇩1,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
| SeqThrow⇩1:
"P ⊢⇩1 ⟨e⇩0,s⇩0⟩ ⇒ ⟨throw e,s⇩1⟩ ⟹
P ⊢⇩1 ⟨e⇩0;;e⇩1,s⇩0⟩ ⇒ ⟨throw e,s⇩1⟩"

| CondT⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨true,s⇩1⟩; P ⊢⇩1 ⟨e⇩1,s⇩1⟩ ⇒ ⟨e',s⇩2⟩ ⟧
⟹ P ⊢⇩1 ⟨if (e) e⇩1 else e⇩2,s⇩0⟩ ⇒ ⟨e',s⇩2⟩"
| CondF⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨false,s⇩1⟩; P ⊢⇩1 ⟨e⇩2,s⇩1⟩ ⇒ ⟨e',s⇩2⟩ ⟧
⟹ P ⊢⇩1 ⟨if (e) e⇩1 else e⇩2,s⇩0⟩ ⇒ ⟨e',s⇩2⟩"
| CondThrow⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨if (e) e⇩1 else e⇩2, s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| WhileF⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨false,s⇩1⟩ ⟹
P ⊢⇩1 ⟨while (e) c,s⇩0⟩ ⇒ ⟨unit,s⇩1⟩"
| WhileT⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨true,s⇩1⟩; P ⊢⇩1 ⟨c,s⇩1⟩ ⇒ ⟨Val v⇩1,s⇩2⟩;
P ⊢⇩1 ⟨while (e) c,s⇩2⟩ ⇒ ⟨e⇩3,s⇩3⟩ ⟧
⟹ P ⊢⇩1 ⟨while (e) c,s⇩0⟩ ⇒ ⟨e⇩3,s⇩3⟩"
| WhileCondThrow⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨while (e) c,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"
| WhileBodyThrow⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨true,s⇩1⟩; P ⊢⇩1 ⟨c,s⇩1⟩ ⇒ ⟨throw e',s⇩2⟩⟧
⟹ P ⊢⇩1 ⟨while (e) c,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"

| Throw⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩ ⟹
P ⊢⇩1 ⟨throw e,s⇩0⟩ ⇒ ⟨Throw a,s⇩1⟩"
| ThrowNull⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
P ⊢⇩1 ⟨throw e,s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩1⟩"
| ThrowThrow⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨throw e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| Try⇩1:
"P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩ ⟹
P ⊢⇩1 ⟨try e⇩1 catch(C i) e⇩2,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩"
| TryCatch⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨Throw a,(h⇩1,ls⇩1)⟩;
h⇩1 a = Some(D,fs); P ⊢ D ≼⇧* C; i < length ls⇩1;
P ⊢⇩1 ⟨e⇩2,(h⇩1,ls⇩1[i:=Addr a])⟩ ⇒ ⟨e⇩2',(h⇩2,ls⇩2)⟩ ⟧
⟹ P ⊢⇩1 ⟨try e⇩1 catch(C i) e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',(h⇩2,ls⇩2)⟩"
| TryThrow⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨Throw a,(h⇩1,ls⇩1)⟩; h⇩1 a = Some(D,fs); ¬ P ⊢ D ≼⇧* C ⟧
⟹ P ⊢⇩1 ⟨try e⇩1 catch(C i) e⇩2,s⇩0⟩ ⇒ ⟨Throw a,(h⇩1,ls⇩1)⟩"

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

| Cons⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P ⊢⇩1 ⟨es,s⇩1⟩ [⇒] ⟨es',s⇩2⟩ ⟧
⟹ P ⊢⇩1 ⟨e#es,s⇩0⟩ [⇒] ⟨Val v # es',s⇩2⟩"
| ConsThrow⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨e#es,s⇩0⟩ [⇒] ⟨throw e' # es, s⇩1⟩"

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

lemma eval⇩1_preserves_len:
"P ⊢⇩1 ⟨e⇩0,(h⇩0,ls⇩0)⟩ ⇒ ⟨e⇩1,(h⇩1,ls⇩1)⟩ ⟹ length ls⇩0 = length ls⇩1"
and evals⇩1_preserves_len:
"P ⊢⇩1 ⟨es⇩0,(h⇩0,ls⇩0)⟩ [⇒] ⟨es⇩1,(h⇩1,ls⇩1)⟩ ⟹ length ls⇩0 = length ls⇩1"
(*<*)by (induct rule:eval⇩1_evals⇩1_inducts, simp_all)(*>*)

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

lemma eval⇩1_final: "P ⊢⇩1 ⟨e,s⟩ ⇒ ⟨e',s'⟩ ⟹ final e'"
and evals⇩1_final: "P ⊢⇩1 ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ finals es'"
(*<*)by(induct rule:eval⇩1_evals⇩1.inducts, simp_all)(*>*)

end