Theory CardinalityAnalysisSpec

theory CardinalityAnalysisSpec
imports ArityAnalysisSpec CardinalityAnalysisSig ConstOn
begin

locale CardinalityPrognosisEdom = CardinalityPrognosis +
  assumes edom_prognosis:
    "edom (prognosis ae as a (Γ, e, S)) ⊆ fv Γ ∪ fv e ∪ fv S"

locale CardinalityPrognosisShape = CardinalityPrognosis +
  assumes prognosis_env_cong: "ae f|` domA Γ = ae' f|` domA Γ ⟹ prognosis ae as u (Γ, e, S) = prognosis ae' as u (Γ, e, S)"
  assumes prognosis_reorder: "map_of Γ = map_of Δ  ⟹  prognosis ae as u (Γ, e, S) = prognosis ae as u (Δ, e, S)"
  assumes prognosis_ap: "const_on (prognosis ae as a (Γ, e, S)) (ap S) many"
  assumes prognosis_upd: "prognosis ae as u (Γ, e, S) ⊑ prognosis ae as u (Γ, e, Upd x # S)"
  assumes prognosis_not_called: "ae x = ⊥ ⟹ prognosis ae as a (Γ, e, S) ⊑ prognosis ae as a (delete x Γ, e, S)"
  assumes prognosis_called: "once ⊑ prognosis ae as a (Γ, Var x, S) x"

locale CardinalityPrognosisApp = CardinalityPrognosis +
  assumes prognosis_App: "prognosis ae as (inc⋅a) (Γ, e, Arg x # S) ⊑ prognosis ae as a (Γ, App e x, S)"

locale CardinalityPrognosisLam = CardinalityPrognosis +
  assumes prognosis_subst_Lam: "prognosis ae as (pred⋅a) (Γ, e[y::=x], S) ⊑ prognosis ae as a (Γ, Lam [y]. e, Arg x # S)"

locale CardinalityPrognosisVar = CardinalityPrognosis +
  assumes prognosis_Var_lam: "map_of Γ x = Some e ⟹ ae x = up⋅u ⟹ isVal e ⟹ prognosis ae as u (Γ, e, S) ⊑ record_call x ⋅ (prognosis ae as a (Γ, Var x, S))"
  assumes prognosis_Var_thunk: "map_of Γ x = Some e ⟹ ae x = up⋅u ⟹ ¬ isVal e ⟹ prognosis ae as u (delete x Γ, e, Upd x # S) ⊑ record_call x ⋅ (prognosis ae as a (Γ, Var x, S))"
  assumes prognosis_Var2: "isVal e ⟹ x ∉ domA Γ ⟹ prognosis ae as 0 ((x, e) # Γ, e, S) ⊑ prognosis ae as 0 (Γ, e, Upd x # S)"

locale CardinalityPrognosisIfThenElse = CardinalityPrognosis +
  assumes prognosis_IfThenElse: "prognosis ae (a#as) 0 (Γ, scrut, Alts e1 e2 # S) ⊑ prognosis ae as a (Γ, scrut ? e1 : e2, S)"
  assumes prognosis_Alts: "prognosis ae as a (Γ, if b then e1 else e2, S) ⊑ prognosis ae (a#as) 0 (Γ, Bool b, Alts e1 e2 # S)"

locale CardinalityPrognosisLet = CardinalityPrognosis + CardinalityHeap + ArityAnalysisHeap +
  assumes prognosis_Let:
  "atom ` domA Δ ♯* Γ ⟹ atom ` domA Δ ♯* S ⟹ edom ae ⊆ domA Γ ∪ upds S ⟹ prognosis (Aheap Δ e⋅a ⊔ ae) as a (Δ @ Γ, e, S) ⊑ cHeap Δ e⋅a ⊔ prognosis ae as a (Γ, Terms.Let Δ e, S)"

locale CardinalityHeapSafe = CardinalityHeap + ArityAnalysisHeap +
  assumes Aheap_heap3: "x ∈ thunks Γ ⟹ many ⊑ (cHeap Γ e⋅a) x ⟹ (Aheap Γ e⋅a) x = up⋅0"
  assumes edom_cHeap: "edom (cHeap Δ e⋅a) = edom (Aheap Δ e⋅a)"

locale CardinalityPrognosisSafe =
  CardinalityPrognosisEdom +
  CardinalityPrognosisShape +
  CardinalityPrognosisApp +
  CardinalityPrognosisLam + 
  CardinalityPrognosisVar +
  CardinalityPrognosisLet +
  CardinalityPrognosisIfThenElse +
  CardinalityHeapSafe +
  ArityAnalysisLetSafe

end