Theory CoCallAnalysisImpl

theory CoCallAnalysisImpl
imports "Arity-Nominal" "Nominal-HOLCF" "Env-Nominal"  "Env-Set-Cpo" "Env-HOLCF" CoCallFix
begin

fun combined_restrict :: "var set ⇒ (AEnv × CoCalls) ⇒ (AEnv × CoCalls)"
  where "combined_restrict S (env, G) = (env f|` S, cc_restr S G)"

lemma fst_combined_restrict[simp]:
  "fst (combined_restrict S p) = fst p f|` S"
  by (cases p, simp)

lemma snd_combined_restrict[simp]:
  "snd (combined_restrict S p) = cc_restr S (snd p)"
  by (cases p, simp)

lemma combined_restrict_eqvt[eqvt]:
  shows "π ∙ combined_restrict S p = combined_restrict (π ∙ S) (π ∙ p)"
  by (cases p) auto

lemma combined_restrict_cont:
  "cont (λx. combined_restrict S x)"
proof-
  have "cont (λ(env, G). combined_restrict S (env, G))" by simp
  then show ?thesis by (simp only: case_prod_eta) 
qed
lemmas cont_compose[OF combined_restrict_cont, cont2cont, simp]

lemma combined_restrict_perm:
  assumes "supp π ♯* S" and [simp]: "finite S"
  shows "combined_restrict S (π ∙ p) = combined_restrict S p"
proof(cases p)
  fix env :: AEnv and  G :: CoCalls
  assume "p = (env, G)"
  moreover 
  from assms
  have "env_restr S (π ∙ env) = env_restr S env" by (rule env_restr_perm)
  moreover
  from assms
  have "cc_restr S (π ∙ G) = cc_restr S G" by (rule cc_restr_perm)
  ultimately
  show ?thesis by simp
qed

definition predCC :: "var set ⇒ (Arity → CoCalls) ⇒ (Arity → CoCalls)"
  where "predCC S f = (Λ a. if a ≠ 0 then cc_restr S (f⋅(pred⋅a)) else ccSquare S)"

lemma predCC_eq:
  shows "predCC S f ⋅ a = (if a ≠ 0 then cc_restr S (f⋅(pred⋅a)) else ccSquare S)"
  unfolding predCC_def
  apply (rule beta_cfun)
  apply (rule cont_if_else_above)
  apply (auto dest: set_mp[OF ccField_cc_restr])
  done

lemma predCC_eqvt[eqvt, simp]: "π ∙ (predCC S f) = predCC (π ∙ S) (π ∙ f)"
  apply (rule cfun_eqvtI)
  unfolding predCC_eq
  by perm_simp rule

lemma cc_restr_predCC:
  "cc_restr S (predCC S' f⋅n) = (predCC (S' ∩ S) (Λ n. cc_restr S (f⋅n)))⋅n"
  unfolding predCC_eq
  by (auto simp add: inf_commute ccSquare_def)

lemma cc_restr_predCC'[simp]:
  "cc_restr S (predCC S f⋅n) = predCC S f⋅n"
  unfolding predCC_eq by simp

  
nominal_function
  cCCexp :: "exp ⇒ (Arity → AEnv × CoCalls)" 
where
  "cCCexp (Var x) =      (Λ n . (esing x ⋅ (up ⋅ n),                                   ⊥))"
| "cCCexp (Lam [x]. e) = (Λ n . combined_restrict (fv (Lam [x]. e)) (fst (cCCexp e⋅(pred⋅n)), predCC (fv (Lam [x]. e)) (Λ a. snd(cCCexp e⋅a))⋅n))"
| "cCCexp (App e x) =    (Λ n . (fst (cCCexp e⋅(inc⋅n)) ⊔ (esing x ⋅ (up⋅0)),          snd (cCCexp e⋅(inc⋅n)) ⊔ ccProd {x} (insert x (fv e))))"
| "cCCexp (Let Γ e) =    (Λ n . combined_restrict (fv (Let Γ e)) (CoCallArityAnalysis.cccFix_choose cCCexp Γ ⋅ (cCCexp e⋅n)))"
| "cCCexp (Bool b) =     ⊥"
| "cCCexp (scrut ? e1 : e2) = (Λ n. (fst (cCCexp scrut⋅0) ⊔ fst (cCCexp e1⋅n) ⊔ fst (cCCexp e2⋅n),
     snd (cCCexp scrut⋅0) ⊔ (snd (cCCexp e1⋅n) ⊔ snd (cCCexp e2⋅n)) ⊔ ccProd (edom (fst (cCCexp scrut⋅0))) (edom (fst (cCCexp e1⋅n)) ∪ edom (fst (cCCexp e2⋅n)))))"
proof goal_cases
  case 1
  show ?case
    unfolding eqvt_def cCCexp_graph_aux_def
    apply rule
    apply (perm_simp)
    apply (simp add: Abs_cfun_eqvt)
    done
next
  case 3
  thus ?case by (metis Terms.exp_strong_exhaust)
next
  case prems: (10 x e x' e')
  from prems(9)
  show ?case
  proof(rule eqvt_lam_case)
    fix π :: perm
    assume *: "supp (-π) ♯* (fv (Lam [x]. e) :: var set)" 
    {
    fix n
    have "combined_restrict (fv (Lam [x]. e)) (fst (cCCexp_sumC (π ∙ e)⋅(pred⋅n)), predCC (fv (Lam [x]. e)) (Λ a. snd(cCCexp_sumC (π ∙ e)⋅a))⋅n)
       = combined_restrict (fv (Lam [x]. e)) (- π ∙ (fst (cCCexp_sumC (π ∙ e)⋅(pred⋅n)), predCC (fv (Lam [x]. e)) (Λ a. snd(cCCexp_sumC (π ∙ e)⋅a))⋅n))"
      by (rule combined_restrict_perm[symmetric, OF *]) simp
    also have "… = combined_restrict (fv (Lam [x]. e)) (fst (cCCexp_sumC e⋅(pred⋅n)), predCC (- π ∙ fv (Lam [x]. e)) (Λ a. snd(cCCexp_sumC e⋅a))⋅n)"
      by (perm_simp, simp add: eqvt_at_apply[OF prems(1)] pemute_minus_self Abs_cfun_eqvt)
    also have "- π ∙ fv (Lam [x]. e) = (fv (Lam [x]. e) :: var set)" by (rule perm_supp_eq[OF *])
    also note calculation
    }
    thus "(Λ n. combined_restrict (fv (Lam [x]. e)) (fst (cCCexp_sumC (π ∙ e)⋅(pred⋅n)), predCC (fv (Lam [x]. e)) (Λ a. snd(cCCexp_sumC (π ∙ e)⋅a))⋅n))
        = (Λ n. combined_restrict (fv (Lam [x]. e)) (fst (cCCexp_sumC e⋅(pred⋅n)), predCC (fv (Lam [x]. e)) (Λ a. snd(cCCexp_sumC e⋅a))⋅n))" by simp
  qed
next
  case prems: (19 Γ body Γ' body')
  from prems(9)
  show ?case
  proof (rule eqvt_let_case)
    fix π :: perm
    assume *: "supp (-π) ♯* (fv (Terms.Let Γ body) :: var set)"
    
    { fix n
      have "combined_restrict (fv (Terms.Let Γ body)) (CoCallArityAnalysis.cccFix_choose cCCexp_sumC (π ∙ Γ)⋅(cCCexp_sumC (π ∙ body)⋅n))
      =  combined_restrict (fv (Terms.Let Γ body)) (- π ∙ (CoCallArityAnalysis.cccFix_choose cCCexp_sumC (π ∙ Γ)⋅(cCCexp_sumC (π ∙ body)⋅n)))"
        by (rule combined_restrict_perm[OF *, symmetric]) simp
      also have "- π ∙ (CoCallArityAnalysis.cccFix_choose cCCexp_sumC (π ∙ Γ)⋅(cCCexp_sumC (π ∙ body)⋅n)) = 
                       CoCallArityAnalysis.cccFix_choose (- π ∙ cCCexp_sumC) Γ⋅((- π ∙ cCCexp_sumC) body⋅n)"
        by (simp add: pemute_minus_self)
      also have "CoCallArityAnalysis.cccFix_choose (- π ∙ cCCexp_sumC) Γ = CoCallArityAnalysis.cccFix_choose cCCexp_sumC Γ"
        by (rule cccFix_choose_cong[OF eqvt_at_apply[OF prems(1)] refl])
      also have "(- π ∙ cCCexp_sumC) body = cCCexp_sumC body"
        by (rule eqvt_at_apply[OF prems(2)])
      also note calculation
    }
    thus "(Λ n. combined_restrict (fv (Terms.Let Γ body)) (CoCallArityAnalysis.cccFix_choose cCCexp_sumC (π ∙ Γ)⋅(cCCexp_sumC (π ∙ body)⋅n))) =
         (Λ n. combined_restrict (fv (Terms.Let Γ body)) (CoCallArityAnalysis.cccFix_choose cCCexp_sumC Γ⋅(cCCexp_sumC body⋅n)))" by (simp only:)
  qed
qed auto

nominal_termination (eqvt) by lexicographic_order

locale CoCallAnalysisImpl
begin
sublocale CoCallArityAnalysis cCCexp.
sublocale ArityAnalysis Aexp.

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

abbreviation ccExp_syn'' ("𝒢⇘_⇙") where "𝒢⇘a⇙ e ≡ CCexp e⋅a"
abbreviation ccExp_bot_syn'' ("𝒢⇧⊥⇘_⇙") where "𝒢⇧⊥⇘a⇙ e ≡ fup⋅(CCexp e)⋅a"


lemma cCCexp_eq[simp]:
  "cCCexp (Var x)⋅n =      (esing x ⋅ (up ⋅ n),                                   ⊥)"
  "cCCexp (Lam [x]. e)⋅n = combined_restrict (fv (Lam [x]. e)) (fst (cCCexp e⋅(pred⋅n)), predCC (fv (Lam [x]. e)) (Λ a. snd(cCCexp e⋅a))⋅n)"
  "cCCexp (App e x)⋅n =    (fst (cCCexp e⋅(inc⋅n)) ⊔ (esing x ⋅ (up⋅0)),          snd (cCCexp e⋅(inc⋅n)) ⊔ ccProd {x} (insert x (fv e)))"
  "cCCexp (Let Γ e)⋅n =    combined_restrict (fv (Let Γ e)) (CoCallArityAnalysis.cccFix_choose cCCexp Γ ⋅ (cCCexp e⋅n))"
  "cCCexp (Bool b)⋅n = ⊥"
  "cCCexp (scrut ? e1 : e2)⋅n = (fst (cCCexp scrut⋅0) ⊔ fst (cCCexp e1⋅n) ⊔ fst (cCCexp e2⋅n),
        snd (cCCexp scrut⋅0) ⊔ (snd (cCCexp e1⋅n) ⊔ snd (cCCexp e2⋅n)) ⊔ ccProd (edom (fst (cCCexp scrut⋅0))) (edom (fst (cCCexp e1⋅n)) ∪ edom (fst (cCCexp e2⋅n))))"
by (simp_all)
declare cCCexp.simps[simp del]


lemma Aexp_pre_simps:
  "𝒜⇘a⇙ (Var x) = esing x⋅(up⋅a)"
  "𝒜⇘a⇙ (Lam [x]. e) = Aexp e⋅(pred⋅a) f|` fv (Lam [x]. e)"
  "𝒜⇘a⇙ (App e x) = Aexp e⋅(inc⋅a) ⊔ esing x⋅(up⋅0)"
  "¬ nonrec Γ ⟹
     𝒜⇘a⇙ (Let Γ e) = (Afix Γ⋅(𝒜⇘a⇙ e ⊔ (λ_.up⋅0) f|` thunks Γ)) f|` (fv (Let Γ e))"
  "x ∉ fv e ⟹
     𝒜⇘a⇙ (let x be e in exp) =
        (fup⋅(Aexp e)⋅(ABind_nonrec x e⋅(𝒜⇘a⇙ exp, CCexp exp⋅a)) ⊔ 𝒜⇘a⇙ exp)
            f|` (fv (let x be e in exp))"
  "𝒜⇘a⇙ (Bool b) = ⊥"
  "𝒜⇘a⇙ (scrut ? e1 : e2) = 𝒜⇘0⇙ scrut ⊔ 𝒜⇘a⇙ e1 ⊔ 𝒜⇘a⇙ e2"
 by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq)+


lemma CCexp_pre_simps:
  "CCexp (Var x)⋅n = ⊥"
  "CCexp (Lam [x]. e)⋅n = predCC (fv (Lam [x]. e)) (CCexp e)⋅n"
  "CCexp (App e x)⋅n = CCexp e⋅(inc⋅n) ⊔ ccProd {x} (insert x (fv e))"
  "¬ nonrec Γ ⟹
      CCexp (Let Γ e)⋅n = cc_restr (fv (Let Γ e))
        (CCfix Γ⋅(Afix Γ⋅(Aexp e⋅n ⊔ (λ_.up⋅0) f|` thunks Γ), CCexp e⋅n))"
  "x ∉ fv e ⟹ CCexp (let x be e in exp)⋅n =
    cc_restr (fv (let x be e in exp))
       (ccBind x e ⋅(Aheap_nonrec x e⋅(Aexp exp⋅n, CCexp exp⋅n), CCexp exp⋅n)
       ⊔ ccProd (fv e) (ccNeighbors x (CCexp exp⋅n) - (if isVal e then {} else {x})) ⊔ CCexp exp⋅n)"
  "CCexp (Bool b)⋅n = ⊥"
  "CCexp (scrut ? e1 : e2)⋅n =
       CCexp scrut⋅0 ⊔
       (CCexp e1⋅n ⊔ CCexp e2⋅n) ⊔
       ccProd (edom (Aexp scrut⋅0)) (edom (Aexp e1⋅n) ∪ edom (Aexp e2⋅n))"
by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq predCC_eq)+

lemma 
  shows ccField_CCexp: "ccField (CCexp e⋅a) ⊆ fv e" and Aexp_edom': "edom (𝒜⇘a⇙ e) ⊆ fv e"
  apply (induction e arbitrary: a rule: exp_induct_rec)
  apply (auto simp add: CCexp_pre_simps predCC_eq Aexp_pre_simps dest!: set_mp[OF ccField_cc_restr] set_mp[OF ccField_ccProd_subset])
  apply fastforce+
  done

lemma cc_restr_CCexp[simp]:
  "cc_restr (fv e) (CCexp e⋅a) = CCexp e⋅a"
by (rule cc_restr_noop[OF ccField_CCexp])

lemma ccField_fup_CCexp:
  "ccField (fup⋅(CCexp e)⋅n) ⊆ fv e"
by (cases n) (auto dest: set_mp[OF ccField_CCexp])

lemma cc_restr_fup_ccExp_useless[simp]: "cc_restr (fv e) (fup⋅(CCexp e)⋅n) = fup⋅(CCexp e)⋅n"
  by (rule cc_restr_noop[OF ccField_fup_CCexp])

sublocale EdomArityAnalysis Aexp by standard (rule Aexp_edom')

lemma CCexp_simps[simp]:
  "𝒢⇘a⇙(Var x) = ⊥"
  "𝒢⇘0⇙(Lam [x]. e) = (fv (Lam [x]. e))²"
  "𝒢⇘inc⋅a⇙(Lam [x]. e) = cc_delete x (𝒢⇘a⇙ e)"
  "𝒢⇘a⇙ (App e x) = 𝒢⇘inc⋅a⇙ e ⊔ {x} G×insert x (fv e)"
  "¬ nonrec Γ ⟹ 𝒢⇘a⇙ (Let Γ e) =
    (CCfix Γ⋅(Afix Γ⋅(𝒜⇘a⇙ e ⊔ (λ_.up⋅0) f|` thunks Γ), 𝒢⇘a⇙ e)) G|` (- domA Γ)"
  "x ∉ fv e' ⟹ 𝒢⇘a⇙ (let x be e' in e) =
    cc_delete x
       (ccBind x e' ⋅(Aheap_nonrec x e'⋅(𝒜⇘a⇙ e, 𝒢⇘a⇙ e), 𝒢⇘a⇙ e)
       ⊔ fv e' G× (ccNeighbors x (𝒢⇘a⇙ e) - (if isVal e' then {} else {x})) ⊔ 𝒢⇘a⇙ e)"
  "𝒢⇘a⇙ (Bool b) = ⊥"
  "𝒢⇘a⇙ (scrut ? e1 : e2) =
       𝒢⇘0⇙ scrut ⊔ (𝒢⇘a⇙ e1 ⊔ 𝒢⇘a⇙ e2) ⊔
       edom (𝒜⇘0⇙ scrut) G× (edom (𝒜⇘a⇙ e1) ∪ edom (𝒜⇘a⇙ e2))"
by (auto simp add: CCexp_pre_simps Diff_eq cc_restr_cc_restr[symmetric] predCC_eq 
            simp del: cc_restr_cc_restr cc_restr_join
            intro!: cc_restr_noop
            dest!: set_mp[OF ccField_cc_delete] set_mp[OF ccField_cc_restr]  set_mp[OF ccField_CCexp]
                   set_mp[OF ccField_CCfix] set_mp[OF ccField_ccBind]  set_mp[OF ccField_ccProd_subset] elem_to_ccField
     )

definition Aheap where
  "Aheap Γ e = (Λ a. if nonrec Γ then (case_prod Aheap_nonrec (hd Γ))⋅(Aexp e⋅a, CCexp e⋅a) else  (Afix Γ ⋅ (Aexp e⋅a ⊔ (λ_.up⋅0) f|` thunks Γ)) f|` domA Γ)"

lemma Aheap_simp1[simp]:
  "¬ nonrec Γ ⟹ Aheap Γ e ⋅a = (Afix Γ ⋅ (Aexp e⋅a ⊔ (λ_.up⋅0) f|` thunks Γ)) f|` domA Γ"
  unfolding Aheap_def by simp

lemma Aheap_simp2[simp]:
  "x ∉ fv e' ⟹ Aheap [(x,e')] e ⋅a = Aheap_nonrec x e'⋅(Aexp e⋅a, CCexp e⋅a)"
  unfolding Aheap_def by (simp add: nonrec_def)

lemma Aheap_eqvt'[eqvt]:
  "π ∙ (Aheap Γ e) = Aheap (π ∙ Γ) (π ∙ e)"
  apply (rule cfun_eqvtI)
  apply (cases nonrec π rule: eqvt_cases[where x = Γ])
  apply simp
  apply (erule nonrecE)
  apply simp
  apply (erule nonrecE)
  apply simp
  apply (perm_simp, rule)
  apply simp
  apply (perm_simp, rule)
  done

sublocale ArityAnalysisHeap Aheap.

sublocale ArityAnalysisHeapEqvt Aheap
proof
  fix π show "π ∙ Aheap = Aheap"
    by perm_simp rule
qed

lemma Aexp_lam_simp: "Aexp (Lam [x]. e) ⋅ n = env_delete x (Aexp e ⋅ (pred ⋅ n))"
proof-
  have "Aexp (Lam [x]. e) ⋅ n = Aexp e⋅(pred⋅n) f|` (fv e - {x})" by (simp add: Aexp_pre_simps)
  also have "... = env_delete x (Aexp e⋅(pred⋅n)) f|` (fv e - {x})" by simp
  also have "… = env_delete x (Aexp e⋅(pred⋅n))"
     by (rule env_restr_useless) (auto dest: set_mp[OF Aexp_edom])
  finally show ?thesis.
qed

lemma Aexp_Let_simp1:
  "¬ nonrec Γ ⟹ 𝒜⇘a⇙ (Let Γ e) = (Afix Γ⋅(𝒜⇘a⇙ e ⊔ (λ_.up⋅0) f|` thunks Γ)) f|` (- domA Γ)"
  unfolding Aexp_pre_simps
  by (rule env_restr_cong) (auto simp add: dest!: set_mp[OF Afix_edom] set_mp[OF Aexp_edom] set_mp[OF thunks_domA])

lemma Aexp_Let_simp2:
  "x ∉ fv e ⟹ 𝒜⇘a⇙(let x be e in exp) = env_delete x (𝒜⇧⊥⇘ABind_nonrec x e ⋅ (𝒜⇘a⇙ exp, CCexp exp⋅a)⇙ e ⊔ 𝒜⇘a⇙ exp)"
  unfolding Aexp_pre_simps env_delete_restr
  by (rule env_restr_cong) (auto dest!: set_mp[OF fup_Aexp_edom]  set_mp[OF Aexp_edom])

lemma Aexp_simps[simp]:
  "𝒜⇘a⇙(Var x) = esing x⋅(up⋅a)"
  "𝒜⇘a⇙(Lam [x]. e) = env_delete x (𝒜⇘pred⋅a⇙ e)"
  "𝒜⇘a⇙(App e x) = Aexp e⋅(inc⋅a) ⊔ esing x⋅(up⋅0)"
  "¬ nonrec Γ ⟹ 𝒜⇘a⇙(Let Γ e) =
      (Afix Γ⋅(𝒜⇘a⇙ e ⊔ (λ_.up⋅0) f|` thunks Γ)) f|` (- domA Γ)"
  "x ∉ fv e' ⟹ 𝒜⇘a⇙(let x be e' in e) =
      env_delete x (𝒜⇧⊥⇘ABind_nonrec x e'⋅(𝒜⇘a⇙ e, 𝒢⇘a⇙ e)⇙ e' ⊔ 𝒜⇘a⇙ e)"
  "𝒜⇘a⇙(Bool b) = ⊥"
  "𝒜⇘a⇙(scrut ? e1 : e2) = 𝒜⇘0⇙ scrut ⊔ 𝒜⇘a⇙ e1 ⊔ 𝒜⇘a⇙ e2"
 by (simp_all add: Aexp_lam_simp Aexp_Let_simp1 Aexp_Let_simp2, simp_all add: Aexp_pre_simps)


end


end