Modules FTreeAnalysisSig, FTreeAnalysisSpec
authorJoachim Breitner <mail@joachim-breitner.de>
Wed, 14 Jan 2015 16:00:10 +0000 (16:00 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Wed, 14 Jan 2015 16:00:10 +0000 (16:00 +0000)
Launchbury/CoCallCardinality.thy
Launchbury/FTreeAnalysis.thy [deleted file]
Launchbury/FTreeAnalysisSig.thy [new file with mode: 0644]
Launchbury/FTreeAnalysisSpec.thy [new file with mode: 0644]
Launchbury/FTreeCardinality.thy

index b73963c..e83b5a4 100644 (file)
@@ -2,6 +2,8 @@ theory CoCallCardinality
 imports FTreeCardinality CoCallAnalysisSig "CoCallGraph-FTree"
 begin
 
+hide_const Multiset.single
+
 lemma valid_lists_many_calls:
   assumes "\<not> one_call_in_path x p"
   assumes "p \<in> valid_lists S G"
@@ -61,17 +63,17 @@ lemma carrier_Fexp': "carrier (Fexp e\<cdot>a) \<subseteq> fv e"
   unfolding Fexp_simp carrier_ccFTree
   by (rule Aexp_edom)
 
-sublocale FutureAnalysis Fexp.
+sublocale FTreeAnalysis Fexp.
 
 lemma carrier_AnalBinds_below:
   "carrier ((Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<subseteq> edom ((ABinds \<Delta>)\<cdot>(Aheap \<Delta> e\<cdot>a))"
 by (auto simp add: Fexp.AnalBinds_lookup Fexp_def split: option.splits 
          elim!: set_mp[OF edom_mono[OF monofun_cfun_fun[OF ABind_below_ABinds]]])
 
-sublocale FutureAnalysisCarrier Fexp
+sublocale FTreeAnalysisCarrier Fexp
   apply default unfolding Fexp_simp carrier_ccFTree..
 
-sublocale FutureAnalysisCorrect Fexp
+sublocale FTreeAnalysisCorrect Fexp
 proof default
   fix x e a
 
@@ -173,7 +175,7 @@ lemma Fheap_simp: "Fheap \<Gamma> e\<cdot>a = (if nonrec \<Gamma> then ccFTree (
 lemma carrier_Fheap':"carrier (Fheap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
     unfolding Fheap_simp carrier_ccFTree by simp
 
-sublocale FutureAnalysisCardinalityHeap Fexp Aexp Aheap Fheap
+sublocale FTreeAnalysisCardinalityHeap Fexp Aexp Aheap Fheap
 proof default
   fix \<Gamma> e a
   show "carrier (Fheap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
diff --git a/Launchbury/FTreeAnalysis.thy b/Launchbury/FTreeAnalysis.thy
deleted file mode 100644 (file)
index 44db857..0000000
+++ /dev/null
@@ -1,30 +0,0 @@
-theory FTreeAnalysis
-imports ArityAnalysisSpec  "FTree-HOLCF"  AnalBinds CallFutureCardinality
-begin
-
-locale FutureAnalysis =
- fixes Fexp :: "exp \<Rightarrow> Arity \<rightarrow> var ftree"
-begin
-  sublocale Fexp!: ExpAnalysis Fexp.
-  abbreviation "FBinds == Fexp.AnalBinds"
-end
-
-locale FutureAnalysisCarrier = FutureAnalysis + EdomArityAnalysis +
-  assumes carrier_Fexp: "carrier (Fexp e\<cdot>a) = edom (Aexp e\<cdot>a)"
-
-locale FutureAnalysisCorrect = FutureAnalysisCarrier +
-  assumes Fexp_App: "many_calls x \<otimes>\<otimes> (Fexp e)\<cdot>(inc\<cdot>a) \<sqsubseteq> Fexp (App e x)\<cdot>a"
-  assumes Fexp_Lam: "without y (Fexp e\<cdot>(pred\<cdot>n)) \<sqsubseteq> Fexp (Lam [y]. e) \<cdot> n"
-  assumes Fexp_subst: "Fexp (e[y::=x])\<cdot>a \<sqsubseteq> many_calls x \<otimes>\<otimes> without y ((Fexp e)\<cdot>a)"
-  assumes Fexp_Var: "single v \<sqsubseteq> Fexp (Var v)\<cdot>a"
-  assumes Fun_repeatable: "isLam e \<Longrightarrow> repeatable (Fexp e\<cdot>0)"
-
-locale FutureAnalysisCardinalityHeap = 
-  FutureAnalysisCorrect + CorrectArityAnalysisLet + 
-  fixes Fheap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> var ftree"
-  assumes carrier_Fheap: "carrier (Fheap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
-  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"
-  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"
-  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"
-
-end
diff --git a/Launchbury/FTreeAnalysisSig.thy b/Launchbury/FTreeAnalysisSig.thy
new file mode 100644 (file)
index 0000000..670c7c7
--- /dev/null
@@ -0,0 +1,12 @@
+theory FTreeAnalysisSig
+imports Arity  "FTree-HOLCF"  AnalBinds
+begin
+
+locale FTreeAnalysis =
+ fixes Fexp :: "exp \<Rightarrow> Arity \<rightarrow> var ftree"
+begin
+  sublocale Fexp!: ExpAnalysis Fexp.
+  abbreviation "FBinds == Fexp.AnalBinds"
+end
+
+end
diff --git a/Launchbury/FTreeAnalysisSpec.thy b/Launchbury/FTreeAnalysisSpec.thy
new file mode 100644 (file)
index 0000000..58e5783
--- /dev/null
@@ -0,0 +1,26 @@
+theory FTreeAnalysisSpec
+imports FTreeAnalysisSig ArityAnalysisSpec CallFutureCardinality 
+begin
+
+hide_const Multiset.single
+
+locale FTreeAnalysisCarrier = FTreeAnalysis + EdomArityAnalysis +
+  assumes carrier_Fexp: "carrier (Fexp e\<cdot>a) = edom (Aexp e\<cdot>a)"
+
+locale FTreeAnalysisCorrect = FTreeAnalysisCarrier +
+  assumes Fexp_App: "many_calls x \<otimes>\<otimes> (Fexp e)\<cdot>(inc\<cdot>a) \<sqsubseteq> Fexp (App e x)\<cdot>a"
+  assumes Fexp_Lam: "without y (Fexp e\<cdot>(pred\<cdot>n)) \<sqsubseteq> Fexp (Lam [y]. e) \<cdot> n"
+  assumes Fexp_subst: "Fexp (e[y::=x])\<cdot>a \<sqsubseteq> many_calls x \<otimes>\<otimes> without y ((Fexp e)\<cdot>a)"
+  assumes Fexp_Var: "single v \<sqsubseteq> Fexp (Var v)\<cdot>a"
+  assumes Fun_repeatable: "isLam e \<Longrightarrow> repeatable (Fexp e\<cdot>0)"
+
+locale FTreeAnalysisCardinalityHeap = 
+  FTreeAnalysisCorrect + CorrectArityAnalysisLet + 
+  fixes Fheap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> var ftree"
+  assumes carrier_Fheap: "carrier (Fheap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
+  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"
+  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"
+  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"
+
+
+end
index e5f3966..1b73701 100644 (file)
@@ -1,8 +1,10 @@
 theory FTreeCardinality
-imports FTreeAnalysis CardinalityAnalysis CallFutureCardinality
+imports FTreeAnalysisSpec CardinalityAnalysis CallFutureCardinality
 begin
 
-context FutureAnalysis
+hide_const Multiset.single
+
+context FTreeAnalysis
 begin
 
 fun unstack :: "stack \<Rightarrow> exp \<Rightarrow> exp" where
@@ -39,7 +41,7 @@ lemma pathsCards_none: "pathsCard (paths t) x = none \<Longrightarrow> x \<notin
 lemma const_on_edom_disj: "const_on f S empty \<longleftrightarrow> edom f \<inter> S = {}"
   by (auto simp add: empty_is_bottom edom_def)
 
-context FutureAnalysisCarrier
+context FTreeAnalysisCarrier
 begin
   lemma carrier_FBinds: "carrier ((FBinds \<Gamma>\<cdot>ae) x) \<subseteq> fv \<Gamma>"
   apply (simp add: Fexp.AnalBinds_lookup)
@@ -52,7 +54,7 @@ end
 
 
 
-context FutureAnalysisCorrect
+context FTreeAnalysisCorrect
 begin
 
   sublocale CardinalityPrognosisCorrect prognosis
@@ -226,7 +228,7 @@ begin
   qed
 end
 
-context FutureAnalysisCardinalityHeap
+context FTreeAnalysisCardinalityHeap
 begin
 
   definition cHeap where