Theory CoCallAnalysisSig

theory CoCallAnalysisSig
imports "Terms" Arity CoCallGraph
begin

locale CoCallAnalysis =
  fixes ccExp :: "exp ⇒ Arity → CoCalls"
begin
  abbreviation ccExp_syn ("𝒢⇘_⇙")
    where "𝒢⇘a⇙ ≡ (λe. ccExp e⋅a)"
  abbreviation ccExp_bot_syn ("𝒢⇧⊥⇘_⇙")
    where "𝒢⇧⊥⇘a⇙ ≡ (λe. fup⋅(ccExp e)⋅a)"
end

locale CoCallAnalyisHeap = 
  fixes ccHeap :: "heap ⇒ exp ⇒ Arity → CoCalls"

end