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