(* Title: JinjaThreads/Compiler/J1WellType.thy Author: Gerwin Klein, Andreas Lochbihler *) section ‹Type rules for the intermediate language› theory J1WellType imports J1State "../Common/ExternalCallWF" "../Common/SemiType" begin declare Listn.lesub_list_impl_same_size[simp del] listE_length [simp del] subsection "Well-Typedness" type_synonym env1 = "ty list" ― ‹type environment indexed by variable number› inductive WT1 :: "'addr J1_prog ⇒ env1 ⇒ 'addr expr1 ⇒ ty ⇒ bool" ("_,_ ⊢1 _ :: _" [51,0,0,51] 50) and WTs1 :: "'addr J1_prog ⇒ env1 ⇒ 'addr expr1 list ⇒ ty list ⇒ bool" ("_,_ ⊢1 _ [::] _" [51,0,0,51]50) for P :: "'addr J1_prog" where WT1New: "is_class P C ⟹ P,E ⊢1 new C :: Class C" | WT1NewArray: "⟦ P,E ⊢1 e :: Integer; is_type P (T⌊⌉) ⟧ ⟹ P,E ⊢1 newA T⌊e⌉ :: T⌊⌉" | WT1Cast: "⟦ P,E ⊢1 e :: T; P ⊢ U ≤ T ∨ P ⊢ T ≤ U; is_type P U ⟧ ⟹ P,E ⊢1 Cast U e :: U" | WT1InstanceOf: "⟦ P,E ⊢1 e :: T; P ⊢ U ≤ T ∨ P ⊢ T ≤ U; is_type P U; is_refT U ⟧ ⟹ P,E ⊢1 e instanceof U :: Boolean" | WT1Val: "typeof v = Some T ⟹ P,E ⊢1 Val v :: T" | WT1Var: "⟦ E!V = T; V < size E ⟧ ⟹ P,E ⊢1 Var V :: T" | WT1BinOp: "⟦ P,E ⊢1 e1 :: T1; P,E ⊢1 e2 :: T2; P ⊢ T1«bop»T2 :: T ⟧ ⟹ P,E ⊢1 e1«bop»e2 :: T" | WT1LAss: "⟦ E!i = T; i < size E; P,E ⊢1 e :: T'; P ⊢ T' ≤ T ⟧ ⟹ P,E ⊢1 i:=e :: Void" | WT1AAcc: "⟦ P,E ⊢1 a :: T⌊⌉; P,E ⊢1 i :: Integer ⟧ ⟹ P,E ⊢1 a⌊i⌉ :: T" | WT1AAss: "⟦ P,E ⊢1 a :: T⌊⌉; P,E ⊢1 i :: Integer; P,E ⊢1 e :: T'; P ⊢ T' ≤ T ⟧ ⟹ P,E ⊢1 a⌊i⌉ := e :: Void" | WT1ALength: "P,E ⊢1 a :: T⌊⌉ ⟹ P,E ⊢1 a∙length :: Integer" | WTFAcc1: "⟦ P,E ⊢1 e :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees F:T (fm) in D ⟧ ⟹ P,E ⊢1 e∙F{D} :: T" | WTFAss1: "⟦ P,E ⊢1 e1 :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees F:T (fm) in D; P,E ⊢1 e2 :: T'; P ⊢ T' ≤ T ⟧ ⟹ P,E ⊢1 e1∙F{D} := e2 :: Void" | WTCAS1: "⟦ P,E ⊢1 e1 :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees F:T (fm) in D; volatile fm; P,E ⊢1 e2 :: T'; P ⊢ T' ≤ T; P,E ⊢1 e3 :: T''; P ⊢ T'' ≤ T ⟧ ⟹ P,E ⊢1 e1∙compareAndSwap(D∙F, e2, e3) :: Boolean" | WT1Call: "⟦ P,E ⊢1 e :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees M:Ts → T = m in D; P,E ⊢1 es [::] Ts'; P ⊢ Ts' [≤] Ts ⟧ ⟹ P,E ⊢1 e∙M(es) :: T" | WT1Block: "⟦ is_type P T; P,E@[T] ⊢1 e :: T'; case vo of None ⇒ True | ⌊v⌋ ⇒ ∃T'. typeof v = ⌊T'⌋ ∧ P ⊢ T' ≤ T ⟧ ⟹ P,E ⊢1 {V:T=vo; e} :: T'" | WT1Synchronized: "⟦ P,E ⊢1 o' :: T; is_refT T; T ≠ NT; P,E@[Class Object] ⊢1 e :: T' ⟧ ⟹ P,E ⊢1 sync⇘V⇙ (o') e :: T'" | WT1Seq: "⟦ P,E ⊢1 e⇩_{1}::T⇩_{1}; P,E ⊢1 e⇩_{2}::T⇩_{2}⟧ ⟹ P,E ⊢1 e⇩_{1};;e⇩_{2}:: T⇩_{2}" | WT1Cond: "⟦ P,E ⊢1 e :: Boolean; P,E ⊢1 e⇩_{1}::T⇩_{1}; P,E ⊢1 e⇩_{2}::T⇩_{2}; P ⊢ lub(T⇩_{1},T⇩_{2}) = T ⟧ ⟹ P,E ⊢1 if (e) e⇩_{1}else e⇩_{2}:: T" | WT1While: "⟦ P,E ⊢1 e :: Boolean; P,E ⊢1 c::T ⟧ ⟹ P,E ⊢1 while (e) c :: Void" | WT1Throw: "⟦ P,E ⊢1 e :: Class C; P ⊢ C ≼⇧^{*}Throwable ⟧ ⟹ P,E ⊢1 throw e :: Void" | WT1Try: "⟦ P,E ⊢1 e⇩_{1}:: T; P,E@[Class C] ⊢1 e⇩_{2}:: T; is_class P C ⟧ ⟹ P,E ⊢1 try e⇩_{1}catch(C V) e⇩_{2}:: T" | WT1Nil: "P,E ⊢1 [] [::] []" | WT1Cons: "⟦ P,E ⊢1 e :: T; P,E ⊢1 es [::] Ts ⟧ ⟹ P,E ⊢1 e#es [::] T#Ts" declare WT1_WTs1.intros[intro!] declare WT1Nil[iff] inductive_cases WT1_WTs1_cases[elim!]: "P,E ⊢1 Val v :: T" "P,E ⊢1 Var i :: T" "P,E ⊢1 Cast D e :: T" "P,E ⊢1 e instanceof U :: T" "P,E ⊢1 i:=e :: T" "P,E ⊢1 {i:U=vo; e} :: T" "P,E ⊢1 e1;;e2 :: T" "P,E ⊢1 if (e) e1 else e2 :: T" "P,E ⊢1 while (e) c :: T" "P,E ⊢1 throw e :: T" "P,E ⊢1 try e1 catch(C i) e2 :: T" "P,E ⊢1 e∙F{D} :: T" "P,E ⊢1 e1∙F{D}:=e2 :: T" "P,E ⊢1 e∙compareAndSwap(D∙F, e', e'') :: T" "P,E ⊢1 e1 «bop» e2 :: T" "P,E ⊢1 new C :: T" "P,E ⊢1 newA T'⌊e⌉ :: T" "P,E ⊢1 a⌊i⌉ := e :: T" "P,E ⊢1 a⌊i⌉ :: T" "P,E ⊢1 a∙length :: T" "P,E ⊢1 e∙M(es) :: T" "P,E ⊢1 sync⇘V⇙ (o') e :: T" "P,E ⊢1 insync⇘V⇙ (a) e :: T" "P,E ⊢1 [] [::] Ts" "P,E ⊢1 e#es [::] Ts" lemma WTs1_same_size: "P,E ⊢1 es [::] Ts ⟹ size es = size Ts" by (induct es arbitrary: Ts) auto lemma WTs1_snoc_cases: assumes wt: "P,E ⊢1 es @ [e] [::] Ts" obtains T Ts' where "P,E ⊢1 es [::] Ts'" "P,E ⊢1 e :: T" proof - from wt have "∃T Ts'. P,E ⊢1 es [::] Ts' ∧ P,E ⊢1 e :: T" by(induct es arbitrary: Ts) auto thus thesis by(auto intro: that) qed lemma WTs1_append: assumes wt: "P,Env ⊢1 es @ es' [::] Ts" obtains Ts' Ts'' where "P,Env ⊢1 es [::] Ts'" "P,Env ⊢1 es' [::] Ts''" proof - from wt have "∃Ts' Ts''. P,Env ⊢1 es [::] Ts' ∧ P,Env ⊢1 es' [::] Ts''" by(induct es arbitrary: Ts) auto thus ?thesis by(auto intro: that) qed lemma WT1_not_contains_insync: "P,E ⊢1 e :: T ⟹ ¬ contains_insync e" and WTs1_not_contains_insyncs: "P,E ⊢1 es [::] Ts ⟹ ¬ contains_insyncs es" by(induct rule: WT1_WTs1.inducts) auto lemma WT1_expr_locks: "P,E ⊢1 e :: T ⟹ expr_locks e = (λa. 0)" and WTs1_expr_lockss: "P,E ⊢1 es [::] Ts ⟹ expr_lockss es = (λa. 0)" by(induct rule: WT1_WTs1.inducts)(auto) lemma assumes wf: "wf_prog wfmd P" shows WT1_unique: "P,E ⊢1 e :: T1 ⟹ P,E ⊢1 e :: T2 ⟹ T1 = T2" and WTs1_unique: "P,E ⊢1 es [::] Ts1 ⟹ P,E ⊢1 es [::] Ts2 ⟹ Ts1 = Ts2" apply(induct arbitrary: T2 and Ts2 rule:WT1_WTs1.inducts) apply blast apply blast apply blast apply blast apply clarsimp apply blast apply(blast dest: WT_binop_fun) apply blast apply blast apply blast apply blast apply (blast dest:sees_field_idemp sees_field_fun) apply (blast dest: sees_field_fun) apply blast apply(erule WT1_WTs1_cases) apply(simp) apply (blast dest:sees_method_idemp sees_method_fun) apply blast apply blast apply blast apply(blast dest: is_lub_unique[OF wf]) apply blast apply blast apply blast apply blast apply blast done lemma assumes wf: "wf_prog p P" shows WT1_is_type: "P,E ⊢1 e :: T ⟹ set E ⊆ types P ⟹ is_type P T" and WTs1_is_type: "P,E ⊢1 es [::] Ts ⟹ set E ⊆ types P ⟹ set Ts ⊆ types P" apply(induct rule:WT1_WTs1.inducts) apply simp apply simp apply simp apply simp apply (simp add:typeof_lit_is_type) apply (fastforce intro:nth_mem) apply(simp add: WT_binop_is_type) apply(simp) apply(simp del: is_type_array add: is_type_ArrayD) apply(simp) apply(simp) apply (simp add:sees_field_is_type[OF _ wf]) apply simp apply simp apply(fastforce dest!: sees_wf_mdecl[OF wf] simp:wf_mdecl_def) apply(simp) apply(simp add: is_class_Object[OF wf]) apply simp apply(blast dest: is_lub_is_type[OF wf]) apply simp apply simp apply simp apply simp apply(simp) done lemma blocks1_WT: "⟦ P,Env @ Ts ⊢1 body :: T; set Ts ⊆ types P ⟧ ⟹ P,Env ⊢1 blocks1 (length Env) Ts body :: T" proof(induct n≡"length Env" Ts body arbitrary: Env rule: blocks1.induct) case 1 thus ?case by simp next case (2 T' Ts e) note IH = ‹⋀Env'. ⟦Suc (length Env) = length Env'; P,Env' @ Ts ⊢1 e :: T; set Ts ⊆ types P ⟧ ⟹ P,Env' ⊢1 blocks1 (length Env') Ts e :: T› from ‹set (T' # Ts) ⊆ types P› have "set Ts ⊆ types P" "is_type P T'" by(auto) moreover from ‹P,Env @ T' # Ts ⊢1 e :: T› have "P,(Env @ [T']) @ Ts ⊢1 e :: T" by simp note IH[OF _ this] ultimately show ?case by auto qed lemma WT1_fv: "⟦ P,E ⊢1 e :: T; ℬ e (length E); syncvars e ⟧ ⟹ fv e ⊆ {0..<length E}" and WTs1_fvs: "⟦ P,E ⊢1 es [::] Ts; ℬs es (length E); syncvarss es ⟧ ⟹ fvs es ⊆ {0..<length E}" proof(induct rule: WT1_WTs1.inducts) case (WT1Synchronized E e1 T e2 T' V) note IH1 = ‹⟦ℬ e1 (length E); syncvars e1⟧ ⟹ fv e1 ⊆ {0..<length E}› note IH2 = ‹⟦ℬ e2 (length (E @ [Class Object])); syncvars e2⟧ ⟹ fv e2 ⊆ {0..<length (E @ [Class Object])}› from ‹ℬ (sync⇘V⇙ (e1) e2) (length E)› have [simp]: "V = length E" and B1: "ℬ e1 (length E)" and B2: "ℬ e2 (Suc (length E))" by auto from ‹syncvars (sync⇘V⇙ (e1) e2)› have sync1: "syncvars e1" and sync2: "syncvars e2" and V: "V ∉ fv e2" by auto have "fv e2 ⊆ {0..<length E}" proof fix x assume x: "x ∈ fv e2" with V have "x ≠ length E" by auto moreover from IH2 B2 sync2 have "fv e2 ⊆ {0..<Suc (length E)}" by auto with x have "x < Suc (length E)" by auto ultimately show "x ∈ {0..<length E}" by auto qed with IH1[OF B1 sync1] show ?case by(auto) next case (WT1Cond E e e1 T1 e2 T2 T) thus ?case by(auto del: subsetI) qed fastforce+ end