Theory TTreeAnalysisSpec

theory TTreeAnalysisSpec
imports TTreeAnalysisSig ArityAnalysisSpec "Cardinality-Domain-Lists"
begin

hide_const Multiset.single

locale TTreeAnalysisCarrier = TTreeAnalysis + EdomArityAnalysis +
  assumes carrier_Fexp: "carrier (Texp e⋅a) = edom (Aexp e⋅a)"

locale TTreeAnalysisSafe = TTreeAnalysisCarrier +
  assumes Texp_App: "many_calls x ⊗⊗ (Texp e)⋅(inc⋅a) ⊑ Texp (App e x)⋅a"
  assumes Texp_Lam: "without y (Texp e⋅(pred⋅n)) ⊑ Texp (Lam [y]. e) ⋅ n"
  assumes Texp_subst: "Texp (e[y::=x])⋅a ⊑ many_calls x ⊗⊗ without y ((Texp e)⋅a)"
  assumes Texp_Var: "single v ⊑ Texp (Var v)⋅a"
  assumes Fun_repeatable: "isVal e ⟹ repeatable (Texp e⋅0)"
  assumes Texp_IfThenElse: "Texp scrut⋅0 ⊗⊗ (Texp e1⋅a ⊕⊕ Texp e2⋅a) ⊑ Texp (scrut ? e1 : e2)⋅a"

locale TTreeAnalysisCardinalityHeap = 
  TTreeAnalysisSafe + ArityAnalysisLetSafe + 
  fixes Theap :: "heap ⇒ exp ⇒ Arity → var ttree"
  assumes carrier_Fheap: "carrier (Theap Γ e⋅a) = edom (Aheap Γ e⋅a)"
  assumes Theap_thunk: "x ∈ thunks Γ ⟹ p ∈ paths (Theap Γ e⋅a) ⟹ ¬ one_call_in_path x p ⟹ (Aheap Γ e⋅a) x = up⋅0"
  assumes Theap_substitute: "ttree_restr (domA Δ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)) ⊑ Theap Δ e⋅a"
  assumes Texp_Let: "ttree_restr (- domA Δ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a))  (thunks Δ) (Texp e⋅a)) ⊑ Texp (Terms.Let Δ e)⋅a"


end