Theory CoCallAnalysisSpec

theory CoCallAnalysisSpec
imports CoCallAritySig ArityAnalysisSpec
begin

hide_const Multiset.single

locale CoCallArityEdom = CoCallArity + EdomArityAnalysis

locale CoCallAritySafe = CoCallArity + CoCallAnalyisHeap + ArityAnalysisLetSafe +
  assumes ccExp_App: "ccExp e⋅(inc⋅a) ⊔ ccProd {x} (insert x (fv e)) ⊑ ccExp (App e x)⋅a"
  assumes ccExp_Lam: "cc_restr (fv (Lam [y]. e)) (ccExp e⋅(pred⋅n)) ⊑ ccExp (Lam [y]. e)⋅n"
  assumes ccExp_subst: "x ∉  S ⟹ y ∉ S ⟹ cc_restr S (ccExp e[y::=x]⋅a) ⊑ cc_restr S (ccExp e⋅a)"
  assumes ccExp_pap: "isVal e ⟹ ccExp e⋅0 = ccSquare (fv e)"
  assumes ccExp_Let: "cc_restr (-domA Γ) (ccHeap Γ e⋅a) ⊑ ccExp (Let Γ e)⋅a"
  assumes ccExp_IfThenElse: "ccExp scrut⋅0 ⊔ (ccExp e1⋅a ⊔ ccExp e2⋅a) ⊔ ccProd (edom (Aexp scrut⋅0)) (edom (Aexp e1⋅a) ∪ edom (Aexp e2⋅a)) ⊑ ccExp (scrut ? e1 : e2)⋅a"

  assumes ccHeap_Exp: "ccExp e⋅a ⊑ ccHeap Δ e⋅a"
  assumes ccHeap_Heap: "map_of Δ x = Some e' ⟹ (Aheap Δ e⋅a) x= up⋅a' ⟹ ccExp e'⋅a' ⊑ ccHeap Δ e⋅a"
  assumes ccHeap_Extra_Edges:
    "map_of Δ x = Some e' ⟹ (Aheap Δ e⋅a) x = up⋅a' ⟹ ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ) ⊑ ccHeap Δ e⋅a"

  assumes aHeap_thunks_rec: " ¬ nonrec Γ ⟹ x ∈ thunks Γ ⟹ x ∈ edom (Aheap Γ e⋅a) ⟹ (Aheap Γ e⋅a) x = up⋅0"
  assumes aHeap_thunks_nonrec: "nonrec Γ ⟹ x ∈ thunks Γ ⟹ x--x ∈ ccExp e⋅a ⟹ (Aheap Γ e⋅a) x = up⋅0"


end