/[eiffelstudio]/branches/eth/eve/Src/framework/program_analysis/expression/expression/epa_quantified_expression.e
ViewVC logotype

Contents of /branches/eth/eve/Src/framework/program_analysis/expression/expression/epa_quantified_expression.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 98118 - (show annotations)
Thu Nov 19 13:59:02 2015 UTC (3 years, 10 months ago) by maxpei
File size: 6219 byte(s)
Fixed a fault in AutoFix. Due to the fault, violated contract expression may not be used as a fixing target.
1 ´╗┐note
2 description: "Objects that represent quantified expressions"
3 author: ""
4 date: "$Date$"
5 revision: "$Revision$"
6
7 deferred class
8 EPA_QUANTIFIED_EXPRESSION
9
10 inherit
11 EPA_EXPRESSION
12 undefine
13 text_in_context
14 redefine
15 is_quantified,
16 text,
17 ast
18 end
19
20 feature{NONE} -- Initialization
21
22 make (a_variable: STRING; a_variable_type: TYPE_A; a_predicate: like predicate; a_class: like class_; a_feature: like feature_; a_written_class: like written_class)
23 -- Initialize Current.
24 do
25 create variables.make (1)
26 variables.compare_objects
27 variables.put (a_variable_type, a_variable.twin)
28 set_class (a_class)
29 set_feature (a_feature)
30 set_written_class (a_written_class)
31 predicate := a_predicate
32 text := text_with_predicate (predicate.text)
33 type := boolean_type
34 if ast = Void then
35 build_ast (a_variable, a_variable_type, a_predicate.ast)
36 end
37 end
38
39 feature{NONE} -- Initialization
40
41 make_from_ast (a_quantification: QUANTIFIED_AS; a_class: like class_; a_feature: like feature_; a_written_class: like written_class)
42 -- Initialize Current from `a_quantification'.
43 -- For the moment, we only support single varaible in `a_for_all_as'.
44 local
45 l_predicate: EPA_AST_EXPRESSION
46 do
47 ast := a_quantification
48 create l_predicate.make_with_text_and_type (a_class, a_feature, text_from_ast (a_quantification.expression), a_written_class, boolean_type)
49 make (a_quantification.variables.first.item_name (1), type_a_from_string (text_from_ast (a_quantification.variables.first.type), a_class), l_predicate, a_class, a_feature, a_written_class)
50 end
51
52 feature -- Access
53
54 variables: HASH_TABLE [TYPE_A, STRING]
55 -- Bounded variables and their types
56 -- Key is the name of a bounded variable, value is the type of that variable
57 -- Note: For the moment, only single bounded variable is supported.
58
59 predicate: EPA_EXPRESSION
60 -- Predicate of current quantification
61
62 type: TYPE_A
63 -- Type of Current expression
64
65 ast: QUANTIFIED_AS
66 -- AST of current expression
67
68 text: STRING
69 -- Expression text of current item
70 -- Note: The output may not in correct Eiffel syntax, so it cannot be directly used
71 -- as an expression to evaluate (for example, in debugger).
72 -- Current Eiffel syntax does not support some of the well-formed quantified expressions,
73 -- for example, forall x. old has(x) implies has (x). 2.3.2010 Jasonw.
74
75 text_with_predicate (a_predicate: STRING): STRING
76 -- Text of current expression
77 local
78 l_cursor: CURSOR
79 l_variables: like variables
80 i, c: INTEGER
81 do
82 create Result.make (64)
83 Result.append (quantifier_name)
84 Result.append_character (' ')
85
86 l_variables := variables
87 l_cursor := l_variables.cursor
88 from
89 i := 1
90 c := l_variables.count
91 l_variables.start
92 until
93 l_variables.after
94 loop
95 Result.append (l_variables.key_for_iteration)
96 -- Result.append (once ": ")
97 -- Result.append (l_variables.item_for_iteration.name)
98 if i < c then
99 Result.append (once ", ")
100 end
101 i := i + 1
102 l_variables.forth
103 end
104 l_variables.go_to (l_cursor)
105 Result.append (once " : ")
106 Result.append (a_predicate)
107 end
108
109 feature -- Status report
110
111 is_quantified: BOOLEAN = True
112 -- Is Current expression quantified, either universal or existential?
113
114 is_variables_valid: BOOLEAN
115 -- Is variables valid?
116 local
117 l_feature: detachable like feature_
118 do
119 fixme ("Only single bounded variable is supported for the moment. 2.3.2010 Jasonw")
120 Result := variables.count = 1
121
122 if Result then
123 -- Check there is no feature with the same feature name as bounded variables.
124 l_feature := feature_
125 from
126 variables.start
127 until
128 variables.after or not Result
129 loop
130 Result := attached context_class.feature_named (variables.key_for_iteration)
131 if Result and then l_feature /= Void then
132 to_implement ("Check if there is no local variable with the same name as the variable. 2.3.2010 Jasonw")
133 end
134 variables.forth
135 end
136 end
137 end
138
139 feature -- Access
140
141 quantifier_name: STRING
142 -- Name of the quantifier
143 deferred
144 end
145
146 feature{NONE} -- Implementation
147
148 build_ast (a_variable_name: STRING; a_type: TYPE_A; a_expression: EXPR_AS)
149 -- Build `ast' from `a_variable_name' and `a_expression'
150 deferred
151 end
152
153 type_in_text_from_a_type (a_type: TYPE_A): STRING
154 -- Type in text from `a_type' object.
155 -- Adapted from {LIKE_FEATURE} and {FORMAL_A}.
156 local
157 do
158 if attached {LIKE_FEATURE} a_type as lt_like then
159 create Result.make (20)
160 -- Result.append_character ('[')
161 if lt_like.has_attached_mark then
162 Result.append_character ('!')
163 elseif lt_like.has_detachable_mark then
164 Result.append_character ('?')
165 end
166 if lt_like.has_separate_mark then
167 Result.append ({SHARED_TEXT_ITEMS}.ti_separate_keyword)
168 Result.append_character (' ')
169 end
170 Result.append ("like " + lt_like.feature_name)
171 elseif attached {FORMAL_A} a_type as lt_formal then
172 Result := class_.generics [lt_formal.position].name.name
173 else
174 Result := a_type.name
175 end
176 end
177
178 build_ast_internal (a_variable_name: STRING; a_type: TYPE_A; a_expression: EXPR_AS; a_universal: BOOLEAN)
179 -- Build `ast' from `a_variable_name' and `a_expression'
180 local
181 l_vars_def: EIFFEL_LIST [LIST_DEC_AS]
182 l_text: STRING
183 l_parser: like entity_declaration_parser
184 do
185 create l_text.make (32)
186 l_text.append (ti_local_keyword)
187 l_text.append_character ('%N')
188 l_text.append (a_variable_name)
189 l_text.append_character (':')
190
191 -- Resolve generic parameters if any.
192 -- l_text.append (type_in_text_from_a_type (a_type))
193 l_text.append (type_in_text_from_a_type (a_type.instantiated_in(class_.constraint_actual_type)))
194
195 l_parser := entity_declaration_parser
196 l_parser.set_syntax_version (l_parser.Provisional_syntax)
197 l_parser.parse_from_ascii_string (l_text, Void)
198 l_vars_def := l_parser.entity_declaration_node
199 if a_universal then
200 create {FOR_ALL_AS} ast.initialize (l_vars_def, a_expression)
201 else
202 create {THERE_EXISTS_AS} ast.initialize (l_vars_def, a_expression)
203 end
204 end
205
206 invariant
207 predicate_is_valid: predicate.is_predicate and not predicate.is_quantified
208
209 end

Properties

Name Value
svn:eol-style native
svn:keywords Author Date ID Revision

  ViewVC Help
Powered by ViewVC 1.1.23