Code specialization (unavoidable to correctly handle anchors)

tybor · Mar 18, 2010 · e44dced · e44dced
1 parent 0df08fd
commit e44dced
Show file tree

Hide file tree

Showing 109 changed files with 1,882 additions and 229 deletions.
diff --git a/src/tools/interpreter/liberty_interpreter_object.e b/src/tools/interpreter/liberty_interpreter_object.e
@@ -84,6 +84,12 @@ feature {ANY}
 			Result.type = target_type
 		end
 
+	specialized_in (a_type: LIBERTY_ACTUAL_TYPE): like Current is
+		do
+			check False end
+			crash
+		end
+
 feature {LIBERTY_INTERPRETER_EXTERNAL_TYPE_ANY_BUILTINS} -- Standard builtings
 	builtin_is_equal (other: LIBERTY_INTERPRETER_OBJECT): BOOLEAN is
 		require

diff --git a/src/tools/main/libertyi.ace b/src/tools/main/libertyi.ace
@@ -26,7 +26,7 @@ cluster
 			assertion(ensure)
 		option
 			debug(all): LIBERTY_ACTUAL_TYPE, LIBERTY_INTERPRETER, LIBERTY_INTERPRETER_FEATURE_CALL
-			assertion(all): LIBERTY_INTERPRETER, LIBERTY_INTERPRETER_FEATURE_CALL
+			assertion(all): LIBERTY_INTERPRETER, LIBERTY_INTERPRETER_FEATURE_CALL, LIBERTY_FEATURE_ENTITY
 		end
 
 generate

diff --git a/src/tools/semantics/code/assertions/liberty_assertions.e b/src/tools/semantics/code/assertions/liberty_assertions.e
@@ -37,6 +37,15 @@ feature {LIBERTY_TYPE_BUILDER_TOOLS}
 			Result /= Void
 		end
 
+feature {LIBERTY_FEATURE, LIBERTY_ASSERTIONS}
+	specialized_in (a_type: LIBERTY_ACTUAL_TYPE): like Current is
+		require
+			a_type /= Void
+		deferred
+		ensure
+			Result /= Void
+		end
+
 feature {}
 	assertions_marker: LIBERTY_REACHABLE_COLLECTION_MARKER[LIBERTY_ASSERTION]
 

diff --git a/src/tools/semantics/code/assertions/liberty_check.e b/src/tools/semantics/code/assertions/liberty_check.e
@@ -16,18 +16,26 @@ class LIBERTY_CHECK
 
 inherit
 	LIBERTY_WRITTEN_ASSERTIONS
+		export {LIBERTY_FEATURE, LIBERTY_ASSERTIONS, LIBERTY_CHECK_INSTRUCTION}
+			specialized_in
+		end
 
-create {LIBERTY_TYPE_BUILDER_TOOLS}
+create {LIBERTY_TYPE_BUILDER_TOOLS, LIBERTY_CHECK}
 	make
 
 feature {}
-	make (a_assertions: like assertions) is
+	make (a_assertions: like assertions_list) is
 		require
 			a_assertions /= Void
 		do
-			assertions := a_assertions
+			assertions_list := a_assertions
 		ensure
-			assertions = a_assertions
+			assertions_list = a_assertions
+		end
+
+	specialized (a_assertions: like assertions_list): like Current is
+		do
+			create Result.make(a_assertions)
 		end
 
 feature {ANY}

diff --git a/src/tools/semantics/code/assertions/liberty_composed_assertions.e b/src/tools/semantics/code/assertions/liberty_composed_assertions.e
@@ -27,6 +27,28 @@ feature {LIBERTY_REACHABLE, LIBERTY_REACHABLE_COLLECTION_MARKER}
 			right.mark_reachable_code(mark)
 		end
 
+feature {LIBERTY_FEATURE, LIBERTY_ASSERTIONS}
+	specialized_in (a_type: LIBERTY_ACTUAL_TYPE): like Current is
+		local
+			l, r: LIBERTY_ASSERTIONS
+		do
+			l := left.specialized_in(a_type)
+			r := right.specialized_in(a_type)
+			if l = left and then r = Void then
+				Result := Current
+			else
+				Result := twin
+				Result.set_specialized_in(l, r)
+			end
+		end
+
+feature {LIBERTY_COMPOSED_ASSERTIONS}
+	set_specialized_in (l: like left; r: like right) is
+		do
+			left := l
+			right := r
+		end
+
 feature {}
 	make (a_left: like left; a_right: like right) is
 		require

diff --git a/src/tools/semantics/code/assertions/liberty_ensure.e b/src/tools/semantics/code/assertions/liberty_ensure.e
@@ -17,17 +17,22 @@ class LIBERTY_ENSURE
 inherit
 	LIBERTY_WRITTEN_ASSERTIONS
 
-create {LIBERTY_TYPE_BUILDER_TOOLS}
+create {LIBERTY_TYPE_BUILDER_TOOLS, LIBERTY_ENSURE}
 	make
 
 feature {}
-	make (a_assertions: like assertions) is
+	make (a_assertions: like assertions_list) is
 		require
 			a_assertions /= Void
 		do
-			assertions := a_assertions
+			assertions_list := a_assertions
 		ensure
-			assertions = a_assertions
+			assertions_list = a_assertions
+		end
+
+	specialized (a_assertions: like assertions_list): like Current is
+		do
+			create Result.make(a_assertions)
 		end
 
 feature {ANY}

diff --git a/src/tools/semantics/code/assertions/liberty_ensure_then.e b/src/tools/semantics/code/assertions/liberty_ensure_then.e
@@ -17,10 +17,10 @@ class LIBERTY_ENSURE_THEN
 inherit
 	LIBERTY_ENSURE
 		redefine
-			accept
+			accept, specialized
 		end
 
-create {LIBERTY_TYPE_BUILDER_TOOLS}
+create {LIBERTY_TYPE_BUILDER_TOOLS, LIBERTY_ENSURE_THEN}
 	make
 
 feature {ANY}
@@ -32,4 +32,10 @@ feature {ANY}
 			v0.visit_liberty_ensure_then(Current)
 		end
 
+feature {}
+	specialized (a_assertions: like assertions_list): like Current is
+		do
+			create Result.make(a_assertions)
+		end
+
 end
diff --git a/src/tools/semantics/code/assertions/liberty_invariant.e b/src/tools/semantics/code/assertions/liberty_invariant.e
@@ -16,18 +16,26 @@ class LIBERTY_INVARIANT
 
 inherit
 	LIBERTY_WRITTEN_ASSERTIONS
+		export {LIBERTY_FEATURE, LIBERTY_ASSERTIONS, LIBERTY_LOOP}
+			specialized_in
+		end
 
-create {LIBERTY_TYPE_BUILDER_TOOLS}
+create {LIBERTY_TYPE_BUILDER_TOOLS, LIBERTY_INVARIANT}
 	make
 
 feature {}
-	make (a_assertions: like assertions) is
+	make (a_assertions: like assertions_list) is
 		require
 			a_assertions /= Void
 		do
-			assertions := a_assertions
+			assertions_list := a_assertions
 		ensure
-			assertions = a_assertions
+			assertions_list = a_assertions
+		end
+
+	specialized (a_assertions: like assertions_list): like Current is
+		do
+			create Result.make(a_assertions)
 		end
 
 feature {ANY}

diff --git a/src/tools/semantics/code/assertions/liberty_require.e b/src/tools/semantics/code/assertions/liberty_require.e
@@ -17,17 +17,22 @@ class LIBERTY_REQUIRE
 inherit
 	LIBERTY_WRITTEN_ASSERTIONS
 
-create {LIBERTY_TYPE_BUILDER_TOOLS}
+create {LIBERTY_TYPE_BUILDER_TOOLS, LIBERTY_REQUIRE}
 	make
 
 feature {}
-	make (a_assertions: like assertions) is
+	make (a_assertions: like assertions_list) is
 		require
 			a_assertions /= Void
 		do
-			assertions := a_assertions
+			assertions_list := a_assertions
 		ensure
-			assertions = a_assertions
+			assertions_list = a_assertions
+		end
+
+	specialized (a_assertions: like assertions_list): like Current is
+		do
+			create Result.make(a_assertions)
 		end
 
 feature {ANY}

diff --git a/src/tools/semantics/code/assertions/liberty_require_else.e b/src/tools/semantics/code/assertions/liberty_require_else.e
@@ -17,10 +17,10 @@ class LIBERTY_REQUIRE_ELSE
 inherit
 	LIBERTY_REQUIRE
 		redefine
-			accept
+			accept, specialized
 		end
 
-create {LIBERTY_TYPE_BUILDER_TOOLS}
+create {LIBERTY_TYPE_BUILDER_TOOLS, LIBERTY_REQUIRE_ELSE}
 	make
 
 feature {ANY}
@@ -32,4 +32,10 @@ feature {ANY}
 			v0.visit_liberty_require_else(Current)
 		end
 
+feature {}
+	specialized (a_assertions: like assertions_list): like Current is
+		do
+			create Result.make(a_assertions)
+		end
+
 end
diff --git a/src/tools/semantics/code/assertions/liberty_require_then.e b/src/tools/semantics/code/assertions/liberty_require_then.e
@@ -17,10 +17,10 @@ class LIBERTY_REQUIRE_THEN
 inherit
 	LIBERTY_REQUIRE
 		redefine
-			accept
+			accept, specialized
 		end
 
-create {LIBERTY_TYPE_BUILDER_TOOLS}
+create {LIBERTY_TYPE_BUILDER_TOOLS, LIBERTY_REQUIRE_THEN}
 	make
 
 feature {ANY}
@@ -32,4 +32,10 @@ feature {ANY}
 			v0.visit_liberty_require_then(Current)
 		end
 
+feature {}
+	specialized (a_assertions: like assertions_list): like Current is
+		do
+			create Result.make(a_assertions)
+		end
+
 end
diff --git a/src/tools/semantics/code/assertions/liberty_written_assertions.e b/src/tools/semantics/code/assertions/liberty_written_assertions.e
@@ -18,14 +18,57 @@ inherit
 	LIBERTY_ASSERTIONS
 
 feature {ANY}
-	assertions: TRAVERSABLE[LIBERTY_ASSERTION]
+	assertions: TRAVERSABLE[LIBERTY_ASSERTION] is
+		do
+			Result := assertions_list
+		end
+
+feature {LIBERTY_FEATURE, LIBERTY_ASSERTIONS}
+	specialized_in (a_type: LIBERTY_ACTUAL_TYPE): like Current is
+		local
+			al: like assertions_list
+			a: LIBERTY_ASSERTION
+			i: INTEGER
+		do
+			from
+				al := assertions_list
+				i := al.lower
+			until
+				i > al.upper
+			loop
+				a := al.item(i).specialized_in(a_type)
+				if a /= al.item(i) then
+					if al = assertions_list then
+						al := assertions_list.twin
+					end
+					al.put(a, i)
+				end
+				i := i + 1
+			end
+			if al = assertions_list then
+				Result := Current
+			else
+				Result := specialized(al)
+			end
+		end
+
+feature {}
+	specialized (a_assertions: like assertions_list): like Current is
+		deferred
+		ensure
+			Result /= Current
+			Result.assertions_list = a_assertions
+		end
 
 feature {LIBERTY_REACHABLE, LIBERTY_REACHABLE_COLLECTION_MARKER}
 	mark_reachable_code (mark: INTEGER) is
 		do
 			assertions_marker.mark_reachable_code(mark, assertions)
 		end
 
+feature {LIBERTY_WRITTEN_ASSERTIONS}
+	assertions_list: COLLECTION[LIBERTY_ASSERTION]
+
 invariant
 	assertions /= Void
 

diff --git a/src/tools/semantics/code/entities/liberty_current.e b/src/tools/semantics/code/entities/liberty_current.e
@@ -19,7 +19,7 @@ inherit
 		redefine out_in_tagged_out_memory
 		end
 
-create {LIBERTY_TYPE_BUILDER_TOOLS}
+create {LIBERTY_ACTUAL_TYPE}
 	make
 
 feature {ANY}
@@ -35,6 +35,11 @@ feature {ANY}
 
 	result_type: LIBERTY_ACTUAL_TYPE
 
+	specialized_in (a_type: LIBERTY_ACTUAL_TYPE): like Current is
+		do
+			Result := a_type.current_entity
+		end
+
 feature {LIBERTY_REACHABLE, LIBERTY_REACHABLE_COLLECTION_MARKER}
 	mark_reachable_code (mark: INTEGER) is
 		do