44db857153c9f18b49877151dcebb5504b9f9f71
[darcs-mirror-isa-launchbury.git] / Launchbury / FTreeAnalysis.thy
1 theory FTreeAnalysis
2 imports ArityAnalysisSpec  "FTree-HOLCF"  AnalBinds CallFutureCardinality
3 begin
4
5 locale FutureAnalysis =
6  fixes Fexp :: "exp \<Rightarrow> Arity \<rightarrow> var ftree"
7 begin
8   sublocale Fexp!: ExpAnalysis Fexp.
9   abbreviation "FBinds == Fexp.AnalBinds"
10 end
11
12 locale FutureAnalysisCarrier = FutureAnalysis + EdomArityAnalysis +
13   assumes carrier_Fexp: "carrier (Fexp e\<cdot>a) = edom (Aexp e\<cdot>a)"
14
15 locale FutureAnalysisCorrect = FutureAnalysisCarrier +
16   assumes Fexp_App: "many_calls x \<otimes>\<otimes> (Fexp e)\<cdot>(inc\<cdot>a) \<sqsubseteq> Fexp (App e x)\<cdot>a"
17   assumes Fexp_Lam: "without y (Fexp e\<cdot>(pred\<cdot>n)) \<sqsubseteq> Fexp (Lam [y]. e) \<cdot> n"
18   assumes Fexp_subst: "Fexp (e[y::=x])\<cdot>a \<sqsubseteq> many_calls x \<otimes>\<otimes> without y ((Fexp e)\<cdot>a)"
19   assumes Fexp_Var: "single v \<sqsubseteq> Fexp (Var v)\<cdot>a"
20   assumes Fun_repeatable: "isLam e \<Longrightarrow> repeatable (Fexp e\<cdot>0)"
21
22 locale FutureAnalysisCardinalityHeap = 
23   FutureAnalysisCorrect + CorrectArityAnalysisLet + 
24   fixes Fheap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> var ftree"
25   assumes carrier_Fheap: "carrier (Fheap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
26   assumes Fheap_thunk: "x \<in> thunks \<Gamma> \<Longrightarrow> p \<in> paths (Fheap \<Gamma> e\<cdot>a) \<Longrightarrow> \<not> one_call_in_path x p \<Longrightarrow> (Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
27   assumes Fheap_substitute: "ftree_restr (domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<sqsubseteq> Fheap \<Delta> e\<cdot>a"
28   assumes Fexp_Let: "ftree_restr (- domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))  (thunks \<Delta>) (Fexp e\<cdot>a)) \<sqsubseteq> Fexp (Terms.Let \<Delta> e)\<cdot>a"
29
30 end