Theory J1WellType

(*  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⇩₁::T⇩₁;  P,E ⊢1 e⇩₂::T⇩₂ ⟧
  ⟹  P,E ⊢1 e⇩₁;;e⇩₂ :: T⇩₂"

| WT1Cond:
  "⟦ P,E ⊢1 e :: Boolean;  P,E ⊢1 e⇩₁::T⇩₁;  P,E ⊢1 e⇩₂::T⇩₂; P ⊢ lub(T⇩₁,T⇩₂) = T ⟧
  ⟹ P,E ⊢1 if (e) e⇩₁ else e⇩₂ :: 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⇩₁ :: T;  P,E@[Class C] ⊢1 e⇩₂ :: T; is_class P C ⟧
  ⟹ P,E ⊢1 try e⇩₁ catch(C V) e⇩₂ :: 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