Module name: CoCallAnalysisSig
authorJoachim Breitner <mail@joachim-breitner.de>
Wed, 14 Jan 2015 15:50:09 +0000 (15:50 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Wed, 14 Jan 2015 15:50:09 +0000 (15:50 +0000)
Launchbury/CoCallAnalysis.thy [deleted file]
Launchbury/CoCallAnalysisBinds.thy
Launchbury/CoCallAnalysisSig.thy [new file with mode: 0644]
Launchbury/CoCallCardinality.thy
Launchbury/CoCallFix.thy

diff --git a/Launchbury/CoCallAnalysis.thy b/Launchbury/CoCallAnalysis.thy
deleted file mode 100644 (file)
index 303d779..0000000
+++ /dev/null
@@ -1,11 +0,0 @@
-theory CoCallAnalysis
-imports Terms Arity CoCallGraph
-begin
-
-locale CoCallAnalysis =
-  fixes ccExp :: "exp \<Rightarrow> Arity \<rightarrow> CoCalls"
-
-locale CoCallAnalyisHeap = 
-  fixes ccHeap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> CoCalls"
-
-end
index d0574cc..5a5fcc2 100644 (file)
@@ -1,5 +1,5 @@
 theory CoCallAnalysisBinds
-imports CoCallAnalysis AEnv  "AList-Utils-HOLCF" "Arity-Nominal""CoCallGraph-Nominal"
+imports CoCallAnalysisSig AEnv  "AList-Utils-HOLCF" "Arity-Nominal""CoCallGraph-Nominal"
 begin
 
 context CoCallAnalysis
diff --git a/Launchbury/CoCallAnalysisSig.thy b/Launchbury/CoCallAnalysisSig.thy
new file mode 100644 (file)
index 0000000..37e89d8
--- /dev/null
@@ -0,0 +1,11 @@
+theory CoCallAnalysisSig
+imports Terms Arity CoCallGraph
+begin
+
+locale CoCallAnalysis =
+  fixes ccExp :: "exp \<Rightarrow> Arity \<rightarrow> CoCalls"
+
+locale CoCallAnalyisHeap = 
+  fixes ccHeap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> CoCalls"
+
+end
index 1240c93..b73963c 100644 (file)
@@ -1,5 +1,5 @@
 theory CoCallCardinality
-imports FTreeCardinality CoCallAnalysis "CoCallGraph-FTree" "/home/jojo/uni/info/isa-where-to-move/Where_To_Move"
+imports FTreeCardinality CoCallAnalysisSig "CoCallGraph-FTree"
 begin
 
 lemma valid_lists_many_calls:
index 3da5be4..c821f66 100644 (file)
@@ -1,5 +1,5 @@
 theory CoCallFix
-imports CoCallAnalysis CoCallAnalysisBinds ArityAnalysisSpec "Env-Nominal"  ArityAnalysisFix
+imports CoCallAnalysisSig CoCallAnalysisBinds ArityAnalysisSig "Env-Nominal"  ArityAnalysisFix
 begin