Theory CoCallAnalysisSpec

theory CoCallAnalysisSpec
imports CoCallAritySig ArityAnalysisSpec
begin


locale CoCallArityEdom = CoCallArity + EdomArityAnalysis

locale CoCallAritySafe = CoCallArity + CoCallAnalyisHeap + ArityAnalysisLetSafe +
  assumes ccExp_App: "ccExp e(inca)  ccProd {x} (insert x (fv e))  ccExp (App e x)a"
  assumes ccExp_Lam: "cc_restr (fv (Lam [y]. e)) (ccExp e(predn))  ccExp (Lam [y]. e)n"
  assumes ccExp_subst: "x   S  y  S  cc_restr S (ccExp e[y::=x]a)  cc_restr S (ccExp ea)"
  assumes ccExp_pap: "isVal e  ccExp e0 = ccSquare (fv e)"
  assumes ccExp_Let: "cc_restr (-domA Γ) (ccHeap Γ ea)  ccExp (Let Γ e)a"
  assumes ccExp_IfThenElse: "ccExp scrut0  (ccExp e1a  ccExp e2a)  ccProd (edom (Aexp scrut0)) (edom (Aexp e1a)  edom (Aexp e2a))  ccExp (scrut ? e1 : e2)a"

  assumes ccHeap_Exp: "ccExp ea  ccHeap Δ ea"
  assumes ccHeap_Heap: "map_of Δ x = Some e'  (Aheap Δ ea) x= upa'  ccExp e'a'  ccHeap Δ ea"
  assumes ccHeap_Extra_Edges:
    "map_of Δ x = Some e'  (Aheap Δ ea) x = upa'  ccProd (fv e') (ccNeighbors x (ccHeap Δ ea) - {x}  thunks Δ)  ccHeap Δ ea"

  assumes aHeap_thunks_rec: " ¬ nonrec Γ  x  thunks Γ  x  edom (Aheap Γ ea)  (Aheap Γ ea) x = up0"
  assumes aHeap_thunks_nonrec: "nonrec Γ  x  thunks Γ  x--x  ccExp ea  (Aheap Γ ea) x = up0"


end