Theory CoCallFix

theory CoCallFix
imports CoCallAnalysisSig CoCallAnalysisBinds ArityAnalysisSig "Env-Nominal"  ArityAnalysisFix
begin


locale CoCallArityAnalysis =
  fixes cccExp :: "exp ⇒ (Arity → AEnv × CoCalls)"
begin

definition Aexp :: "exp ⇒ (Arity → AEnv)"
  where "Aexp e = (Λ a. fst (cccExp e ⋅ a))"

sublocale ArityAnalysis Aexp.

abbreviation Aexp_syn' ("𝒜⇘_⇙") where "𝒜⇘a⇙ ≡ (λe. Aexp e⋅a)"
abbreviation Aexp_bot_syn' ("𝒜⇧⊥⇘_⇙") where "𝒜⇧⊥⇘a⇙ ≡ (λe. fup⋅(Aexp e)⋅a)"

lemma Aexp_eq:
  "𝒜⇘a⇙ e = fst (cccExp e ⋅ a)"
  unfolding Aexp_def by (rule beta_cfun) (intro cont2cont)

lemma fup_Aexp_eq:
  "fup⋅(Aexp e)⋅a = fst (fup⋅(cccExp e)⋅a)"
  by (cases a)(simp_all add: Aexp_eq)


definition CCexp :: "exp ⇒ (Arity → CoCalls)" where "CCexp Γ = (Λ a. snd (cccExp Γ⋅a))"
lemma CCexp_eq:
  "CCexp e⋅a = snd (cccExp e ⋅ a)"
  unfolding CCexp_def by (rule beta_cfun) (intro cont2cont)

lemma fup_CCexp_eq:
  "fup⋅(CCexp e)⋅a = snd (fup⋅(cccExp e)⋅a)"
  by (cases a)(simp_all add: CCexp_eq)

sublocale CoCallAnalysis CCexp.

definition CCfix :: "heap ⇒ (AEnv × CoCalls) → CoCalls"
  where "CCfix Γ = (Λ aeG. (μ G'. ccBindsExtra Γ⋅(fst aeG , G') ⊔ snd aeG))"

lemma CCfix_eq:
  "CCfix Γ⋅(ae,G) = (μ G'. ccBindsExtra Γ⋅(ae, G') ⊔ G)"
  unfolding CCfix_def
  by simp

lemma CCfix_unroll: "CCfix Γ⋅(ae,G) = ccBindsExtra Γ⋅(ae, CCfix Γ⋅(ae,G)) ⊔ G"
  unfolding  CCfix_eq
  apply (subst fix_eq)
  apply simp
  done

lemma fup_ccExp_restr_subst': 
  assumes "⋀ a. cc_restr S (CCexp e[x::=y]⋅a) = cc_restr S (CCexp e⋅a)"
  shows "cc_restr S (fup⋅(CCexp e[x::=y])⋅a) = cc_restr S (fup⋅(CCexp e)⋅a)"
  using assms
  by (cases a) (auto simp del: cc_restr_cc_restr simp add: cc_restr_cc_restr[symmetric])

lemma ccBindsExtra_restr_subst': 
  assumes "⋀ x' e a. (x',e) ∈ set Γ ⟹ cc_restr S (CCexp e[x::=y]⋅a) = cc_restr S (CCexp e⋅a)"
  assumes "x ∉ S"
  assumes "y ∉ S"
  assumes "domA Γ ⊆ S"
  shows  "cc_restr S (ccBindsExtra  Γ[x::h=y]⋅(ae, G)) 
       = cc_restr S (ccBindsExtra  Γ⋅(ae f|` S , cc_restr S G))"
  apply (simp add: ccBindsExtra_simp ccBinds_eq ccBind_eq Int_absorb2[OF assms(4)] fv_subst_int[OF assms(3,2)])
  apply (intro arg_cong2[where f = "op ⊔"] refl  arg_cong[OF mapCollect_cong])
  apply (subgoal_tac "k ∈ S")
  apply (auto intro: fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]] simp add: fv_subst_int[OF assms(3,2)]   fv_subst_int2[OF assms(3,2)] ccSquare_def)[1]
  apply (metis assms(4) contra_subsetD domI dom_map_of_conv_domA)
  apply (subgoal_tac "k ∈ S")
  apply (auto intro: fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]]
              simp add: fv_subst_int[OF assms(3,2)]   fv_subst_int2[OF assms(3,2)] ccSquare_def cc_restr_twist[where S = S] simp del: cc_restr_cc_restr)[1]
  apply (subst fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]], assumption)
  apply (simp add: fv_subst_int[OF assms(3,2)]   fv_subst_int2[OF assms(3,2)] )
  apply (subst fup_ccExp_restr_subst'[OF assms(1)[OF map_of_SomeD]], assumption)
  apply (simp add: fv_subst_int[OF assms(3,2)]   fv_subst_int2[OF assms(3,2)] )
  apply (metis assms(4) contra_subsetD domI dom_map_of_conv_domA)
  done

lemma ccBindsExtra_restr:
  assumes "domA Γ ⊆ S"
  shows "cc_restr S (ccBindsExtra Γ⋅(ae, G)) = cc_restr S (ccBindsExtra Γ⋅(ae f|` S, cc_restr S G))"
  using assms
  apply (simp add: ccBindsExtra_simp ccBinds_eq ccBind_eq Int_absorb2)
  apply (intro arg_cong2[where f = "op ⊔"] refl arg_cong[OF mapCollect_cong])
  apply (subgoal_tac "k ∈ S")
  apply simp
  apply (metis contra_subsetD domI dom_map_of_conv_domA)
  apply (subgoal_tac "k ∈ S")
  apply simp
  apply (metis contra_subsetD domI dom_map_of_conv_domA)
  done

lemma CCfix_restr:
  assumes "domA Γ ⊆ S"
  shows "cc_restr S (CCfix Γ⋅(ae, G)) = cc_restr S (CCfix Γ⋅(ae f|` S, cc_restr S G))"
  unfolding CCfix_def
  apply simp
  apply (rule parallel_fix_ind[where P = "λ x y . cc_restr S x = cc_restr S y"])
  apply simp
  apply rule
  apply simp
  apply (subst (1 2) ccBindsExtra_restr[OF assms])
  apply (auto)
  done

lemma ccField_CCfix:
  shows "ccField (CCfix Γ⋅(ae, G)) ⊆ fv Γ ∪ ccField G"
  unfolding CCfix_def
  apply simp
  apply (rule fix_ind[where P = "λ x . ccField x ⊆ fv Γ ∪ ccField G"])
  apply (auto dest!: set_mp[OF ccField_ccBindsExtra])
  done


lemma CCfix_restr_subst':
  assumes "⋀ x' e a. (x',e) ∈ set Γ ⟹ cc_restr S (CCexp e[x::=y]⋅a) = cc_restr S (CCexp e⋅a)"
  assumes "x ∉ S"
  assumes "y ∉ S"
  assumes "domA Γ ⊆ S"
  shows "cc_restr S (CCfix Γ[x::h=y]⋅(ae, G)) = cc_restr S (CCfix Γ⋅(ae f|` S, cc_restr S G))"
  unfolding CCfix_def
  apply simp
  apply (rule parallel_fix_ind[where P = "λ x y . cc_restr S x = cc_restr S y"])
  apply simp
  apply rule
  apply simp
  apply (subst  ccBindsExtra_restr_subst'[OF assms], assumption)
  apply (subst ccBindsExtra_restr[OF assms(4)]) back 
  apply (auto)
  done


end

lemma Aexp_eqvt[eqvt]:  "π ∙ (CoCallArityAnalysis.Aexp cccExp e) = CoCallArityAnalysis.Aexp (π ∙ cccExp) (π ∙ e)"
  apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.Aexp_eq by perm_simp rule

lemma CCexp_eqvt[eqvt]:  "π ∙ (CoCallArityAnalysis.CCexp cccExp e) = CoCallArityAnalysis.CCexp (π ∙ cccExp) (π ∙ e)"
  apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.CCexp_eq by perm_simp rule

lemma CCfix_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.CCfix cccExp Γ) = CoCallArityAnalysis.CCfix (π ∙ cccExp) (π ∙ Γ)"
  unfolding CoCallArityAnalysis.CCfix_def by perm_simp (simp_all add: Abs_cfun_eqvt)

lemma ccFix_cong[fundef_cong]:
  "⟦ (⋀ e. e ∈ snd ` set heap2 ⟹ cccexp1 e = cccexp2 e); heap1 = heap2 ⟧
      ⟹ CoCallArityAnalysis.CCfix cccexp1 heap1 = CoCallArityAnalysis.CCfix cccexp2 heap2"
   unfolding CoCallArityAnalysis.CCfix_def
   apply (rule arg_cong) back
   apply (rule ccBindsExtra_cong)
   apply (auto simp add: CoCallArityAnalysis.CCexp_def)
   done


context CoCallArityAnalysis
begin
definition cccFix ::  "heap ⇒ ((AEnv × CoCalls) → (AEnv × CoCalls))"
  where "cccFix Γ = (Λ i. (Afix Γ⋅(fst i ⊔ (λ_.up⋅0) f|` thunks Γ), CCfix Γ⋅(Afix Γ⋅(fst i  ⊔ (λ_.up⋅0) f|` (thunks Γ)), snd i)))"

lemma cccFix_eq:
  "cccFix Γ⋅i = (Afix Γ⋅(fst i ⊔ (λ_.up⋅0) f|` thunks Γ), CCfix Γ⋅(Afix Γ⋅(fst i  ⊔ (λ_.up⋅0) f|` (thunks Γ)), snd i))"
  unfolding cccFix_def
  by (rule beta_cfun)(intro cont2cont)
end

lemma cccFix_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.cccFix cccExp Γ) = CoCallArityAnalysis.cccFix  (π ∙ cccExp) (π ∙ Γ)"
  apply (rule cfun_eqvtI) unfolding CoCallArityAnalysis.cccFix_eq by perm_simp rule

lemma cccFix_cong[fundef_cong]:
  "⟦ (⋀ e. e ∈ snd ` set heap2 ⟹ cccexp1 e = cccexp2 e); heap1 = heap2 ⟧
      ⟹ CoCallArityAnalysis.cccFix cccexp1 heap1 = CoCallArityAnalysis.cccFix cccexp2 heap2"
   unfolding CoCallArityAnalysis.cccFix_def
   apply (rule cfun_eqI)
   apply auto
   apply (rule arg_cong[OF Afix_cong], auto simp add: CoCallArityAnalysis.Aexp_def)[1]
   apply (rule arg_cong2[OF ccFix_cong Afix_cong ])
   apply (auto simp add: CoCallArityAnalysis.Aexp_def)
   done


subsubsection {* The non-recursive case *}

definition ABind_nonrec :: "var ⇒ exp ⇒ AEnv × CoCalls → Arity⇩⊥"
where
  "ABind_nonrec x e = (Λ i. (if isVal e ∨ x--x∉(snd i) then fst i x else up⋅0))"

lemma ABind_nonrec_eq:
  "ABind_nonrec x e⋅(ae,G) = (if isVal e ∨ x--x∉G then ae x else up⋅0)"
  unfolding ABind_nonrec_def
  apply (subst beta_cfun)
  apply (rule cont_if_else_above)
  apply auto
  by (metis in_join join_self_below(4))

lemma ABind_nonrec_eqvt[eqvt]: "π ∙ (ABind_nonrec x e) = ABind_nonrec (π ∙ x) (π ∙ e)"
  apply (rule cfun_eqvtI)
  apply (case_tac xa, simp)
  unfolding ABind_nonrec_eq
  by perm_simp rule

lemma ABind_nonrec_above_arg:
  "ae x ⊑ ABind_nonrec x e ⋅ (ae, G)"
unfolding ABind_nonrec_eq by auto

definition Aheap_nonrec where
  "Aheap_nonrec x e = (Λ i. esing x⋅(ABind_nonrec x e⋅i))"

lemma Aheap_nonrec_simp:
  "Aheap_nonrec x e⋅i = esing x⋅(ABind_nonrec x e⋅i)"
  unfolding Aheap_nonrec_def by simp

lemma Aheap_nonrec_lookup[simp]:
  "(Aheap_nonrec x e⋅i) x = ABind_nonrec x e⋅i"
  unfolding Aheap_nonrec_simp by simp

lemma Aheap_nonrec_eqvt'[eqvt]:
  "π ∙ (Aheap_nonrec x e) = Aheap_nonrec (π ∙ x) (π ∙ e)"
  apply (rule cfun_eqvtI)
  unfolding Aheap_nonrec_simp
  by (perm_simp, rule)


context CoCallArityAnalysis
begin

  definition Afix_nonrec
   where "Afix_nonrec x e = (Λ i. fup⋅(Aexp e)⋅(ABind_nonrec x e ⋅ i) ⊔ fst i)"

  lemma Afix_nonrec_eq[simp]:
    "Afix_nonrec x e ⋅ i = fup⋅(Aexp e)⋅(ABind_nonrec x e ⋅ i) ⊔ fst i"
    unfolding Afix_nonrec_def
    by (rule beta_cfun) simp

  definition CCfix_nonrec
   where "CCfix_nonrec x e = (Λ i. ccBind x e ⋅ (Aheap_nonrec x e⋅i, snd i)  ⊔ ccProd (fv e) (ccNeighbors x (snd i) - (if isVal e then {} else {x})) ⊔ snd i)"

  lemma CCfix_nonrec_eq[simp]:
    "CCfix_nonrec x e ⋅ i = ccBind x e⋅(Aheap_nonrec x e⋅i, snd i)  ⊔ ccProd (fv e) (ccNeighbors x (snd i) - (if isVal e then {} else {x})) ⊔ snd i"
    unfolding CCfix_nonrec_def
    by (rule beta_cfun) (intro cont2cont)

  definition cccFix_nonrec ::  "var ⇒ exp ⇒ ((AEnv × CoCalls) → (AEnv × CoCalls))"
    where "cccFix_nonrec x e = (Λ i. (Afix_nonrec x e ⋅i , CCfix_nonrec x e ⋅i))"

  lemma cccFix_nonrec_eq[simp]:
    "cccFix_nonrec x e⋅i = (Afix_nonrec x e ⋅i , CCfix_nonrec x e ⋅i)"
    unfolding cccFix_nonrec_def
    by (rule beta_cfun) (intro cont2cont)

end


lemma AFix_nonrec_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.Afix_nonrec cccExp x e) = CoCallArityAnalysis.Afix_nonrec (π ∙ cccExp) (π ∙ x) (π ∙ e)"
  apply (rule cfun_eqvtI)
  unfolding CoCallArityAnalysis.Afix_nonrec_eq
  by perm_simp rule


lemma CCFix_nonrec_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.CCfix_nonrec cccExp x e) = CoCallArityAnalysis.CCfix_nonrec (π ∙ cccExp) (π ∙ x) (π ∙ e)"
  apply (rule cfun_eqvtI)
  unfolding CoCallArityAnalysis.CCfix_nonrec_eq
  by perm_simp rule

lemma cccFix_nonrec_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.cccFix_nonrec cccExp x e) = CoCallArityAnalysis.cccFix_nonrec (π ∙ cccExp) (π ∙ x) (π ∙ e)"
  apply (rule cfun_eqvtI)
  unfolding CoCallArityAnalysis.cccFix_nonrec_eq
  by perm_simp rule

subsubsection {* Combining the cases *}

context CoCallArityAnalysis
begin
  definition cccFix_choose ::  "heap ⇒ ((AEnv × CoCalls) → (AEnv × CoCalls))"
    where "cccFix_choose Γ = (if nonrec Γ then case_prod cccFix_nonrec (hd Γ) else cccFix Γ)"

  lemma cccFix_choose_simp1[simp]:
    "¬ nonrec Γ ⟹ cccFix_choose Γ = cccFix Γ"
  unfolding cccFix_choose_def by simp

  lemma cccFix_choose_simp2[simp]:
    "x ∉ fv e ⟹ cccFix_choose [(x,e)] = cccFix_nonrec x e"
  unfolding cccFix_choose_def nonrec_def by auto

end

lemma cccFix_choose_eqvt[eqvt]: "π ∙ (CoCallArityAnalysis.cccFix_choose cccExp Γ) = CoCallArityAnalysis.cccFix_choose (π ∙ cccExp) (π ∙ Γ)"
  unfolding CoCallArityAnalysis.cccFix_choose_def 
  apply (cases nonrec π  rule: eqvt_cases[where x = Γ])
  apply (perm_simp, rule)
  apply simp
  apply (erule nonrecE)
  apply (simp )

  apply simp
  done

lemma cccFix_nonrec_cong[fundef_cong]:
  "cccexp1 e = cccexp2 e  ⟹ CoCallArityAnalysis.cccFix_nonrec cccexp1 x e = CoCallArityAnalysis.cccFix_nonrec cccexp2 x e"
   apply (rule cfun_eqI)
   unfolding CoCallArityAnalysis.cccFix_nonrec_eq
   unfolding CoCallArityAnalysis.Afix_nonrec_eq
   unfolding CoCallArityAnalysis.CCfix_nonrec_eq
   unfolding CoCallArityAnalysis.fup_Aexp_eq
   apply (simp only: )
   apply (rule arg_cong[OF ccBind_cong])
   apply simp
   unfolding CoCallArityAnalysis.CCexp_def
   apply simp
   done

lemma cccFix_choose_cong[fundef_cong]:
  "⟦ (⋀ e. e ∈ snd ` set heap2 ⟹ cccexp1 e = cccexp2 e); heap1 = heap2 ⟧
      ⟹ CoCallArityAnalysis.cccFix_choose cccexp1 heap1 = CoCallArityAnalysis.cccFix_choose cccexp2 heap2"
   unfolding CoCallArityAnalysis.cccFix_choose_def
   apply (rule cfun_eqI)
   apply (auto elim!: nonrecE)
   apply (rule arg_cong[OF cccFix_nonrec_cong], auto)
   apply (rule arg_cong[OF cccFix_cong], auto)[1]
   done

end