Theory CallExpr

(*  Title:      JinjaThreads/Common/CallExpr.thy
    Author:     Andreas Lochbihler
*)

chapter ‹Compilation \label{cha:comp}›

section ‹Method calls in expressions›

theory CallExpr imports 
  "../J/Expr"
begin

fun inline_call :: "('a,'b,'addr) exp ⇒ ('a,'b,'addr) exp ⇒ ('a,'b,'addr) exp"
  and inline_calls :: "('a,'b,'addr) exp ⇒ ('a,'b,'addr) exp list ⇒ ('a,'b,'addr) exp list"
where
  "inline_call f (new C) = new C"
| "inline_call f (newA T⌊e⌉) = newA T⌊inline_call f e⌉"
| "inline_call f (Cast C e) = Cast C (inline_call f e)"
| "inline_call f (e instanceof T) = (inline_call f e) instanceof T"
| "inline_call f (Val v) = Val v"
| "inline_call f (Var V) = Var V"
| "inline_call f (V:=e) = V := inline_call f e"
| "inline_call f (e «bop» e') = (if is_val e then (e «bop» inline_call f e') else (inline_call f e «bop» e'))"
| "inline_call f (a⌊i⌉) = (if is_val a then a⌊inline_call f i⌉ else (inline_call f a)⌊i⌉)"
| "inline_call f (AAss a i e) =
   (if is_val a then if is_val i then AAss a i (inline_call f e) else AAss a (inline_call f i) e
    else AAss (inline_call f a) i e)"
| "inline_call f (a∙length) = inline_call f a∙length"
| "inline_call f (e∙F{D}) = inline_call f e∙F{D}"
| "inline_call f (FAss e F D e') = (if is_val e then FAss e F D (inline_call f e') else FAss (inline_call f e) F D e')"
| "inline_call f (CompareAndSwap e D F e' e'') = 
   (if is_val e then if is_val e' then CompareAndSwap e D F e' (inline_call f e'') 
     else CompareAndSwap e D F (inline_call f e') e''
    else CompareAndSwap (inline_call f e) D F e' e'')"
| "inline_call f (e∙M(es)) = 
   (if is_val e then if is_vals es ∧ is_addr e then f else e∙M(inline_calls f es) else inline_call f e∙M(es))"
| "inline_call f ({V:T=vo; e}) = {V:T=vo; inline_call f e}"
| "inline_call f (sync⇘V⇙ (o') e) = sync⇘V⇙ (inline_call f o') e"
| "inline_call f (insync⇘V⇙ (a) e) = insync⇘V⇙ (a) (inline_call f e)"
| "inline_call f (e;;e') = inline_call f e;;e'"
| "inline_call f (if (b) e else e') = (if (inline_call f b) e else e')"
| "inline_call f (while (b) e) = while (b) e"
| "inline_call f (throw e) = throw (inline_call f e)"
| "inline_call f (try e1 catch(C V) e2) = try inline_call f e1 catch(C V) e2"

| "inline_calls f [] = []"
| "inline_calls f (e#es) = (if is_val e then e # inline_calls f es else inline_call f e # es)"

fun collapse :: "'addr expr × 'addr expr list ⇒ 'addr expr" where
  "collapse (e, []) = e"
| "collapse (e, (e' # es)) = collapse (inline_call e e', es)"

definition is_call :: "('a, 'b, 'addr) exp ⇒ bool"
where "is_call e = (call e ≠ None)"

definition is_calls :: "('a, 'b, 'addr) exp list ⇒ bool"
where "is_calls es = (calls es ≠ None)"



lemma inline_calls_map_Val_append [simp]:
  "inline_calls f (map Val vs @ es) = map Val vs @ inline_calls f es"
by(induct vs, auto)

lemma inline_call_eq_Val_aux:
  "inline_call e E = Val v ⟹ call E = ⌊aMvs⌋ ⟹ e = Val v"
by(induct E)(auto split: if_split_asm)

lemmas inline_call_eq_Val [dest] = inline_call_eq_Val_aux inline_call_eq_Val_aux[OF sym, THEN sym]

lemma inline_calls_eq_empty [simp]: "inline_calls e es = [] ⟷ es = []"
by(cases es, auto)

lemma inline_calls_map_Val [simp]: "inline_calls e (map Val vs) = map Val vs"
by(induct vs) auto

lemma  fixes E :: "('a,'b, 'addr) exp" and Es :: "('a,'b, 'addr) exp list"
  shows inline_call_eq_Throw [dest]: "inline_call e E = Throw a ⟹ call E = ⌊aMvs⌋ ⟹ e = Throw a ∨ e = addr a"
by(induct E rule: exp.induct)(fastforce split:if_split_asm)+

lemma Throw_eq_inline_call_eq [dest]:
  "inline_call e E = Throw a ⟹ call E = ⌊aMvs⌋ ⟹ Throw a = e ∨ addr a = e"
by(auto dest: inline_call_eq_Throw[OF sym])

lemma is_vals_inline_calls [dest]:
  "⟦ is_vals (inline_calls e es); calls es = ⌊aMvs⌋ ⟧ ⟹ is_val e"
by(induct es, auto split: if_split_asm)

lemma [dest]: "⟦ inline_calls e es = map Val vs; calls es = ⌊aMvs⌋ ⟧ ⟹ is_val e"
              "⟦ map Val vs = inline_calls e es; calls es = ⌊aMvs⌋ ⟧ ⟹ is_val e"
by(fastforce intro!: is_vals_inline_calls del: is_val.intros simp add: is_vals_conv elim: sym)+

lemma inline_calls_eq_Val_Throw [dest]:
  "⟦ inline_calls e es = map Val vs @ Throw a # es'; calls es = ⌊aMvs⌋ ⟧ ⟹ e = Throw a ∨ is_val e"
apply(induct es arbitrary: vs a es')
apply(auto simp add: Cons_eq_append_conv split: if_split_asm)
done

lemma Val_Throw_eq_inline_calls [dest]:
  "⟦ map Val vs @ Throw a # es' = inline_calls e es; calls es = ⌊aMvs⌋ ⟧ ⟹ Throw a = e ∨ is_val e"
by(auto dest: inline_calls_eq_Val_Throw[OF sym])

declare option.split [split del] if_split_asm [split]  if_split [split del]

lemma call_inline_call [simp]:
  "call e = ⌊aMvs⌋ ⟹ call (inline_call {v:T=vo; e'} e) = call e'"
  "calls es = ⌊aMvs⌋ ⟹ calls (inline_calls {v:T=vo;e'} es) = call e'"
apply(induct e and es rule: call.induct calls.induct)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce split: if_split)
apply(fastforce)
apply(fastforce)
apply(fastforce split: if_split)
apply(clarsimp)
 apply(fastforce split: if_split)
apply(fastforce split: if_split)
apply(fastforce)
apply(fastforce)
apply(fastforce split: if_split)
apply(fastforce split: if_split)
apply(fastforce split: if_split)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce split: if_split)
done

declare option.split [split] if_split [split] if_split_asm [split del]

lemma fv_inline_call: "fv (inline_call e' e) ⊆ fv e ∪ fv e'"
  and fvs_inline_calls: "fvs (inline_calls e' es) ⊆ fvs es ∪ fv e'"
by(induct e and es rule: call.induct calls.induct)(fastforce split: if_split_asm)+

lemma contains_insync_inline_call_conv:
  "contains_insync (inline_call e e') ⟷ contains_insync e ∧ call e' ≠ None ∨ contains_insync e'"
  and contains_insyncs_inline_calls_conv:
  "contains_insyncs (inline_calls e es') ⟷ contains_insync e ∧ calls es' ≠ None ∨ contains_insyncs es'"
by(induct e' and es' rule: call.induct calls.induct)(auto split: if_split_asm simp add: is_vals_conv)

lemma contains_insync_inline_call [simp]:
  "call e' = ⌊aMvs⌋ ⟹ contains_insync (inline_call e e') ⟷ contains_insync e ∨ contains_insync e'"
  and contains_insyncs_inline_calls [simp]:
  "calls es' = ⌊aMvs⌋ ⟹ contains_insyncs (inline_calls e es') ⟷ contains_insync e ∨ contains_insyncs es'"
by(simp_all add: contains_insync_inline_call_conv contains_insyncs_inline_calls_conv)

lemma collapse_append [simp]:
  "collapse (e, es @ es') = collapse (collapse (e, es), es')"
by(induct es arbitrary: e, auto)

lemma collapse_conv_foldl:
  "collapse (e, es) = foldl inline_call e es"
by(induct es arbitrary: e) simp_all

lemma fv_collapse: "∀e ∈ set es. is_call e ⟹ fv (collapse (e, es)) ⊆ fvs (e # es)"
apply(induct es arbitrary: e)
apply(insert fv_inline_call)
apply(fastforce dest: subsetD)+
done

lemma final_inline_callD: "⟦ final (inline_call E e); is_call e ⟧ ⟹ final E"
by(induct e)(auto simp add: is_call_def split: if_split_asm)

lemma collapse_finalD: "⟦ final (collapse (e, es)); ∀e∈set es. is_call e ⟧ ⟹ final e"
by(induct es arbitrary: e)(auto dest: final_inline_callD)

context heap_base begin

definition synthesized_call :: "'m prog ⇒ 'heap ⇒ ('addr × mname × 'addr val list) ⇒ bool"
where
  "synthesized_call P h = 
   (λ(a, M, vs). ∃T Ts Tr D. typeof_addr h a = ⌊T⌋ ∧ P ⊢ class_type_of T sees M:Ts→Tr = Native in D)"

lemma synthesized_call_conv:
  "synthesized_call P h (a, M, vs) = 
   (∃T Ts Tr D. typeof_addr h a = ⌊T⌋ ∧ P ⊢ class_type_of T sees M:Ts→Tr = Native in D)"
by(simp add: synthesized_call_def)

end

end