theory FTreeImplCardinality
imports FTreeAnalysisSig CardinalityAnalysisSig CallFutureCardinality
begin
hide_const Multiset.single
context FTreeAnalysis
begin
fun unstack :: "stack \ exp \ exp" where
"unstack [] e = e"
| "unstack (Alts e1 e2 # S) e = unstack S e"
| "unstack (Upd x # S) e = unstack S e"
| "unstack (Arg x # S) e = unstack S (App e x)"
| "unstack (Dummy x # S) e = unstack S e"
fun Fstack :: "Arity list \ stack \ var ftree"
where "Fstack _ [] = \"
| "Fstack (a#as) (Alts e1 e2 # S) = (Fexp e1\a \\ Fexp e2\a) \\ Fstack as S"
| "Fstack as (Arg x # S) = many_calls x \\ Fstack as S"
| "Fstack as (_ # S) = Fstack as S"
(*
lemma carrier_Fstack[simp]: "carrier (Fstack S) = ap S"
by (induction S rule: Fstack.induct) (auto simp add: empty_is_bottom[symmetric])
*)
fun prognosis :: "AEnv \ Arity list \ Arity \ conf \ var \ two"
where "prognosis ae as a (\, e, S) = pathsCard (paths (substitute (FBinds \\ae) (thunks \) (Fexp e\a \\ Fstack as S)))"
end
end