1 | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(btypechecker, | |
6 | [btype/7, % typecheck B syntax node | |
7 | btype_l/6, % typecheck list of B syntax nodes | |
8 | btype_ground/6, % typecheck and check if all new identifier have ground types | |
9 | btype_ground_dl/7, % typecheck and check if all new identifier have ground types; difference-list version | |
10 | btype_ground_dl_in_section/8, % version of above with additional context name parameter | |
11 | check_ground_types_dl/4, % check if a list of identifiers has only ground types | |
12 | unify_types_werrors/6, % unify two types, return list of errors in case of type mismatch | |
13 | unify_types_werrors/4, | |
14 | %unify_types_werrors_l/6, % unify two list of types | |
15 | unify_types_strict/2, % unify two types, just fail in case of type mismatch | |
16 | l_unify_types_strict/2, % ditto for two lists of types | |
17 | ||
18 | ext2int/7, % convert a (raw) syntax element into a typed element | |
19 | remove_pos/2, % remove position info from a (raw) syntax element | |
20 | % TODO[DP, 15.03.2013]: In case of a re-structuring of modules, | |
21 | % maybe it is a good idea to move the type environment predicates to a module of its own | |
22 | env_empty/1, % create an empty type environment | |
23 | env_lookup_type/3, % lookup a type of an identifier in the environment | |
24 | env_lookup_infos/3, % lookup additional infos of an identifier in the environment | |
25 | env_store/5, % store the type of an identifier in the environment | |
26 | env_store_operator/4, % store a theory operator into the environment | |
27 | env_store_definition/3, % store an untyped definition_decl/6 ast in the environment | |
28 | env_identifiers/2, | |
29 | add_identifiers_to_environment/3, | |
30 | operation_infos/1, % give a list of (uninstantiated) infos that operations need for type-checking | |
31 | compute_accessed_vars_infos_for_operation/8, % (re)-compute reads/write infos for operation | |
32 | ||
33 | couplise_list/2, % [a,b,c] -> couple(couple(a,b),c) | |
34 | prime_identifiers/2, prime_identifier/2, prime_id/2, is_primed_id/1, | |
35 | prime_identifiers0/2, prime_identifier0/2, prime_atom0/2, | |
36 | ||
37 | fasttype/2, % manually create a syntax tree with type infos | |
38 | lookup_type_for_expr/2, % interface predicate to <:> | |
39 | ||
40 | openenv/2, % create an "open" type environment, where unknown identifiers will be added on demand | |
41 | openenv_identifiers/2, % get the introduced identifiers of an open type environment | |
42 | opentype/5, % type-check an expression without having every identifier declared in advance | |
43 | ||
44 | reset_typechecker/0, | |
45 | machine_string/1, % succeeds for every explicit string seen so far by the type checker | |
46 | store_typecheck_error/4, | |
47 | ||
48 | coerce_type/4 | |
49 | ]). | |
50 | ||
51 | :- use_module(tools). | |
52 | ||
53 | :- use_module(module_information,[module_info/2]). | |
54 | :- module_info(group,typechecker). | |
55 | :- module_info(description,'ProBs type checker and type inference module.'). | |
56 | ||
57 | :- use_module(library(lists)). | |
58 | :- use_module(library(terms)). | |
59 | :- use_module(library(avl)). | |
60 | :- use_module(library(ordsets)). | |
61 | ||
62 | :- use_module(error_manager). | |
63 | :- use_module(self_check). | |
64 | :- use_module(kernel_records,[normalise_record_type/2, record_has_multiple_field_names/2]). | |
65 | ||
66 | :- use_module(translate). | |
67 | ||
68 | :- use_module(bsyntaxtree). | |
69 | :- use_module(b_ast_cleanup). | |
70 | :- use_module(debug). | |
71 | :- use_module(input_syntax_tree,[raw_replace/3, try_get_raw_position_info/2]). | |
72 | :- use_module(preferences,[get_preference/2, preference/2]). | |
73 | :- use_module(b_read_write_info,[get_accessed_vars/5]). | |
74 | :- use_module(external_functions, [get_external_function_type/3]). | |
75 | :- use_module(parsercall, [transform_string_template/3]). | |
76 | ||
77 | % operator for type inference rules | |
78 | :- op(600, xfy, (<:>)). % used to be ::, but changed to <:> for Logtalk | |
79 | ||
80 | %:- dynamic op_modifies_reads_cache/3. % store modifies and reads information for operations | |
81 | :- dynamic machine_string/1. /* keep a list of all explicit strings seen in the machine so far */ | |
82 | /* Probably better: do it in a separeate traversal; talk to Daniel about this */ | |
83 | reset_typechecker :- reset_machine_strings. %, retractall(op_modifies_reads_cache(_,_,_)). | |
84 | reset_machine_strings :- retractall(machine_string(_)). | |
85 | assert_machine_string(S) :- machine_string(S) -> true ; assertz(machine_string(S)). | |
86 | ||
87 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
88 | % miniature B type checker | |
89 | ||
90 | btype_ground(Exprs,Env,NonGroundExceptions,Types,TExprs,Errors) :- | |
91 | btype_ground_dl(Exprs,Env,NonGroundExceptions,Types,TExprs,Errors,[]). | |
92 | ||
93 | :- dynamic current_type_checking_context/1. | |
94 | get_current_context(C) :- | |
95 | (current_type_checking_context(SecName) -> ajoin([' in ',SecName],C) ; C=''). | |
96 | ||
97 | % a version of btype_ground_dl which stores current context | |
98 | btype_ground_dl_in_section(SectionName,Exprs,Env,NonGroundExceptions,Types,TExprs,EIn,EOut) :- | |
99 | retractall(current_type_checking_context(_)), | |
100 | assertz(current_type_checking_context(SectionName)), | |
101 | call_cleanup(btype_ground_dl(Exprs,Env,NonGroundExceptions,Types,TExprs,EIn,EOut), | |
102 | retractall(current_type_checking_context(_))). | |
103 | % dl: difference list version | |
104 | btype_ground_dl(Exprs,Env,NonGroundExceptions,Types,TExprs,EIn,EOut) :- | |
105 | same_length(Exprs,Types), same_length(Exprs,TExprs), | |
106 | get_texpr_types(TExprs,Types),!, | |
107 | ? | do_typecheck_dl(Exprs,Env,[ground(NonGroundExceptions)],TExprs,EIn,EOut). |
108 | btype_ground_dl(Exprs,Env,NG,Types,TExprs,EIn,EOut) :- | |
109 | add_internal_error('Illegal call to:',btype_ground_dl(Exprs,Env,NG,Types,TExprs,EIn,EOut)), | |
110 | fail. | |
111 | ||
112 | % do_typecheck type-checks the expression and checks if the types | |
113 | % of introduced variables (like in quantifiers) are ground | |
114 | do_typecheck(Exprs,Env,Options,TExprs,Errors) :- | |
115 | do_typecheck_dl(Exprs,Env,Options,TExprs,Errors,[]). | |
116 | ||
117 | do_typecheck_dl(Exprs,Env,Options,TExprs,ErrorsIn,ErrorsOut) :- | |
118 | typecheck_result_init(ErrorsIn,Delayed,Identifiers,TRStart), | |
119 | % type-check the expressions | |
120 | ? | btype_l(Exprs,Env,_Type,TExprs,TRStart,TR), |
121 | typecheck_result_get_errors(TR,E1), | |
122 | typecheck_result_get_delayed_rules(TR,[]), | |
123 | typecheck_result_get_identifiers(TR,[]), | |
124 | foldl(trigger_delayed_rule,Delayed,E1,E2), | |
125 | % get the newly introduced identifiers and check if their types are | |
126 | % ground | |
127 | ( memberchk(ground(NonGroundExceptions),Options) -> | |
128 | check_ground_types_dl(Identifiers,NonGroundExceptions,E2,ErrorsOut) | |
129 | ; | |
130 | E2=ErrorsOut). | |
131 | ||
132 | trigger_delayed_rule(dr(Trigger,Errors),Ein,Eout) :- | |
133 | % ground trigger, enforce blocked rule | |
134 | Trigger = 0, | |
135 | % by now Errors should have given a ground value by the co-routine | |
136 | add_all(Errors,Ein,Eout). | |
137 | add_all([]) --> !. | |
138 | add_all([E|Rest]) --> [E], add_all(Rest). | |
139 | ||
140 | ||
141 | % Utilities for tr(.) DCG argument for type-checking | |
142 | type_error_or_warning_occurred(TRin,TRout) :- | |
143 | % TO DO ? : also check for warnings | |
144 | TRout=tr(Errors1,_,_,_), | |
145 | TRin =tr(Errors2,_,_,_), Errors1 \== Errors2. | |
146 | ||
147 | typecheck_result_init(Errors,DR,Ids,tr(Errors,DR,Ids,[error_count(0,50,unknown)])). % 50: maximum number of errors reported; note: the error manager has itself an upper-bound on the number of errors reported | |
148 | ||
149 | % typecheck_result_add_error(Error,TRin,TRout) usually this will be called with TRout a variable | |
150 | typecheck_result_add_error(Error,tr(Errors,DR,Ids,Flags),tr(RestErrors,DR,Ids,NewFlags)) :- | |
151 | ? | (select(error_count(N,Max,PrevPos),Flags,NF) |
152 | -> N1 is N+1, NewFlags = [error_count(N1,Max,NewLastPos)|NF], | |
153 | (Error = error(_,Pos) -> NewLastPos = Pos ; NewLastPos = PrevPos), | |
154 | (N<Max -> Errors = [Error|RestErrors] | |
155 | ; Errors = RestErrors % we have reached the maximum: do not store error; we could throw an exception to stop typechecking altogether, ,throw(tr_exceeded(Errors,DR,Ids,Flags)) | |
156 | ) | |
157 | ; NewFlags = Flags, Errors = [Error|RestErrors] | |
158 | ). | |
159 | ||
160 | typecheck_result_add_delayed_rule(Trigger,RuleErrors, | |
161 | tr(Errors,[dr(Trigger,RuleErrors)|Rules],Ids,Flags),tr(Errors,Rules,Ids,Flags)) :- !. | |
162 | typecheck_result_add_delayed_rule(Trigger,RuleErrors,In,Out) :- | |
163 | add_internal_error('Could not add delayed rule: ',typecheck_result_add_delayed_rule(Trigger,RuleErrors,In,Out)), | |
164 | Out=In. | |
165 | ||
166 | typecheck_result_add_identifier(Id,tr(Errors,Rules,[Id|Ids],Flags),tr(Errors,Rules,Ids,Flags)). | |
167 | ||
168 | %typecheck_max_errors_exceeded(tr(_,_,_,Flags)) :- | |
169 | % member(error_count(N,Max,_),Flags),number(N),number(Max),N>Max. | |
170 | ||
171 | typecheck_result_get_errors(tr(FullErrors,_DR,_Ids,Flags),RestErrors) :- | |
172 | ((member(error_count(N,Max,LastPos),Flags),number(N),number(Max),N>Max) | |
173 | -> tools:ajoin(['Maximum number (',Max,') of type errors exceeded: ',N],Msg), | |
174 | ExcErr=error(Msg,LastPos), | |
175 | %append(Errors,[ExcErr],FullErrors) | |
176 | FullErrors = [ExcErr|RestErrors] | |
177 | ; FullErrors = RestErrors). | |
178 | ||
179 | typecheck_result_get_delayed_rules(tr(_Errors,Rules,_Ids,_Flags),Rules). | |
180 | ||
181 | typecheck_result_get_identifiers(tr(_Errors,_Rules,Ids,_Flags),Ids). | |
182 | ||
183 | %typecheck_result_finalize(tr([],[],[])). % not used at the moment | |
184 | ||
185 | typecheck_result_get_flags(tr(_,_,_,Flags),Flags). | |
186 | ||
187 | typecheck_add_flag(Flag,tr(Errors,Rules,Ids,Flags),tr(Errors,Rules,Ids,NewFlags)) :- | |
188 | (member(Flag,Flags) -> NewFlags=Flags ; NewFlags=[Flag|Flags]). | |
189 | ||
190 | % btype/7 is the central predicate of the type-checker | |
191 | % type-checking is done in three "stages": | |
192 | % btype/5: extracts the obligatory position information from the input syntax element | |
193 | % decouples the type in the argument and the type of the expression by | |
194 | % an explicit unify_types/5 call | |
195 | % calls btype1 | |
196 | % btype1/7: calls btype_rewrite for optional rewriting rules | |
197 | % if no more rewriting rules can be applied, btype2 is called | |
198 | % btype2/7: does the actual type-checking | |
199 | ||
200 | % btype(+Src,+Ext,+Env,Type,-Result,TRin,TRout): | |
201 | % Src: Where the call comes from | |
202 | % Ext: The AST of the expression to type check as it comes from the parser | |
203 | % Env: The type environment (see the env_... predicates) | |
204 | % Type: The type of the expression (could be as input or output) | |
205 | % Result: The type checked AST | |
206 | % TRin/TRout: typecheck_result data structure, see typecheck_result_... predicates | |
207 | btype(Src,Ext,Env,Type,Result,TRin,TRout) :- | |
208 | (var(Ext) | |
209 | -> add_internal_error('btype Ext is variable: ',Src:Ext) | |
210 | ; true), | |
211 | ? | if(btype_aux(Ext,Env,Type,Result,TRin,TRout),true, |
212 | add_error_and_fail(btype,'btype failed: ',Src:Ext) | |
213 | %(add_error(btype,'btype failed: ',Src:Ext),trace, btype_aux(Ext,Env,Type,Result,TRin,TRout)) | |
214 | ), | |
215 | (var(TRout) -> add_error(btype,'TRout is variable: ',Src:Ext) ; true). | |
216 | ||
217 | btype_aux(Ext,Env,Type,Result,TRin,TRout) :- | |
218 | % convert the external raw representation Ext (first argument is the position) | |
219 | % into the typed representation | |
220 | ext2int(btype,Ext,Expr,Pos,Type,TExpr,Infos,Result0), | |
221 | % type-check the expression | |
222 | ? | btype1(Expr,Pos,Env,TExpr,LType,Infos,NewPos,TRin,TR1), |
223 | % an explicit unify decouples the expected and inferred type | |
224 | (Pos\=NewPos | |
225 | -> %debug_println(19,updating_position_info(Pos,NewPos)), | |
226 | update_pos(Result0,NewPos,Result) | |
227 | ; Result = Result0), | |
228 | unify_types(Type,LType,Pos,TExpr,TR1,TRout). | |
229 | ||
230 | update_pos(b(R0,T,Infos),NewPos,b(R0,T,[nodeid(NewPos)|Infos0])) :- | |
231 | delete(Infos,nodeid(_),Infos0). | |
232 | ||
233 | % btype1/7 tries to apply rewriting rules until no more rules | |
234 | % are applyable, then btype2/7 is called | |
235 | % btype1(+Expr,+Pos,+Env,-TExpr,-Type,-Infos,-NewPos,+TRin,-TRout): | |
236 | % NewPos: potentially updated position information when definitions are expanded | |
237 | btype1(Expr,Pos,Env,TExpr,Type,Infos,NewPos,TRin,TRout) :- | |
238 | ? | catch( btype_try_rewrite(Expr,Pos,Env,TExpr,Type,Infos,NewPos,TRin,TRout), |
239 | rewrite_exception(Msg,Name), | |
240 | handle_rewrite_exception(Msg,Name,Pos,TExpr,Infos,TRin,TRout) | |
241 | ). | |
242 | btype_try_rewrite(Expr,Pos,Env,TExpr,Type,Infos,NewPos2,TRin,TRout) :- | |
243 | ? | btype_rewrite(Expr,Env,Pos,NewExpr,NewPos),!, |
244 | ? | btype1(NewExpr,NewPos,Env,TExpr,Type,Infos,NewPos2,TRin,TRout). |
245 | btype_try_rewrite(Expr,Pos,Env,TExpr,Type,Infos,Pos,TRin,TRout2) :- | |
246 | ? | btype2(Expr,Pos,Env,TExpr,Type,Infos,TRin,TRout1), |
247 | ? | btype_static_check(TExpr,Pos,Env,TRout1,TRout2). |
248 | ||
249 | % a few static checking rules | |
250 | btype_static_check(let(IDList,Equalities,_Body),Pos,Env) --> | |
251 | btype_static_check_let(IDList,Equalities,Pos,no_reuse,Env). % here Atelier-B prohibits reuse | |
252 | btype_static_check(let_expression(IDList,Equalities,_Body),Pos,Env) --> | |
253 | btype_static_check_let(IDList,Equalities,Pos,allow_reuse,Env). % here we allow reuse | |
254 | btype_static_check(let_predicate(IDList,Equalities,_Body),Pos,Env) --> | |
255 | btype_static_check_let(IDList,Equalities,Pos,allow_reuse,Env). | |
256 | btype_static_check(_,_,_) --> []. | |
257 | ||
258 | btype_static_check_let(IDList,Equalities,Pos,AllowReuse,Env,TRin,TRout) :- | |
259 | def_get_texpr_ids(IDList,Ids), sort(Ids,SIds), | |
260 | check_let_equalities(Equalities,Pos,AllowReuse,SIds,[],NotDefined,_Defined,Env,TRin,TRout1), | |
261 | (NotDefined==[] -> TRout = TRout1 | |
262 | ; type_error_or_warning_occurred(TRin,TRout1) -> | |
263 | format(user_error,'*** Let does not define variables: ~w~n',[NotDefined]), | |
264 | TRout1 = TRout % we have already raised errors | |
265 | ; %print(tr(TRin)),nl,print(tr(TRout1)),nl, | |
266 | ajoin_with_sep(['Let does not define variables:'|NotDefined],' ',Msg), | |
267 | store_typecheck_error(Msg,Pos,TRout1,TRout)). | |
268 | ||
269 | % TO DO: we should maybe run these after the type checker has run | |
270 | % AllowReuse: allow let identifiers to be re-used in later RHS sides; normally not allowed by Atelier-B | |
271 | check_let_equalities(b(P,T,I),Pos,AllowReuse,ToDefine,AlreadyDefined,T2,A2,Env) --> | |
272 | check_let_equalities_aux(P,T,I,Pos,AllowReuse,ToDefine,AlreadyDefined,T2,A2,Env). | |
273 | check_let_equalities_aux(P,Type,Info,Pos,AR,_,_,_,_,_) --> | |
274 | {var(P)},!, | |
275 | {add_internal_error('Illegal variable:',check_let_equalities_aux(P,Type,Info,Pos,AR,_,_,_,_,_))}. | |
276 | check_let_equalities_aux(conjunct(L,R),_,_,Pos,AllowReuse,ToDefine,AlreadyDefined,T2,A2,Env) --> !, | |
277 | check_let_equalities(L,Pos,AllowReuse,ToDefine,AlreadyDefined,T1,Already1,Env), | |
278 | check_let_equalities(R,Pos,AllowReuse,T1,Already1,T2,A2,Env). | |
279 | check_let_equalities_aux(equal(LHS,RHS),_,_,_Pos,AllowReuse,ToDefine,AlreadyDefined,T2,A2,Env) --> | |
280 | {get_texpr_id(LHS,LID)}, | |
281 | %{print(equal(LID,ToDefine,AlreadyDefined,T2,A2)),nl}, | |
282 | ? | {select(LID,ToDefine,T2)}, % OK: we define an introduced ID |
283 | !, | |
284 | {ord_add_element(AlreadyDefined,LID,A2)}, | |
285 | {find_identifier_uses(RHS,[],Used)}, % can we already call this here ?? TO DO Check non-ground typing does not cause problem | |
286 | check_let_rhs(RHS,Used,ToDefine,AlreadyDefined,AllowReuse,Env). | |
287 | check_let_equalities_aux(equal(LHS,RHS),Type,Info,Pos,_AllowReuse,T,A,T,A,_Env,TrIn,TrOut) :- | |
288 | translate_bexpression(b(equal(LHS,RHS),Type,Info),IStr), % are the types guaranteed to be instantiated ? | |
289 | (get_texpr_id(LHS,LID) | |
290 | -> (member(LID,A) -> Msg1 = 'LET redefines identifier: ' | |
291 | ; Msg1 = 'LET defines undeclared identifier: ' | |
292 | ) | |
293 | ; Msg1 = 'LET contains an equality whose left-hand-side is not an identifier: '), | |
294 | ajoin([Msg1,IStr],Msg), | |
295 | (get_texpr_pos(LHS,PosM) -> true ; PosM=Pos), | |
296 | store_typecheck_error(Msg,PosM,TrIn,TrOut). | |
297 | check_let_equalities_aux(IllegalPred,Type,Info,_Pos,_AllowReuse,T,A,T,A,_Env) --> | |
298 | {translate_bexpression(b(IllegalPred,Type,Info),IStr), | |
299 | ajoin(['LET contains a predicate which is not an equality: ',IStr],Msg)}, | |
300 | store_typecheck_error(Msg,Info). | |
301 | ||
302 | :- use_module(specfile,[z_mode/0]). | |
303 | check_let_rhs(_RHS,Used,ToDefine,AlreadyDefined,_AllowReuse,Env) --> {z_mode}, !, | |
304 | % We do not seem to call this code in Z Mode ! | |
305 | ({ord_union(ToDefine,AlreadyDefined,All), | |
306 | possible_ambiguity(Used,All,Env,ClashIds)} | |
307 | -> {format('*** Warning: possible clash in LET: ~w~n',[ClashIds])} | |
308 | ; [] | |
309 | ). | |
310 | check_let_rhs(RHS,Used,ToDefine,AlreadyDefined,no_reuse,_Env) --> | |
311 | {get_preference(allow_let_to_reuse_introduced_ids,false)}, | |
312 | {ord_union(ToDefine,AlreadyDefined,All), ord_intersection(Used,All,Inter)}, | |
313 | {Inter\=[]}, | |
314 | !, | |
315 | % potentially cyclic let | |
316 | {ajoin_with_sep(['LET right-hand-side uses left-hand introduced ids (set ALLOW_COMPLEX_LETS to TRUE to allow this):'|Inter],' ',Msg), | |
317 | get_texpr_info(RHS,Info)}, | |
318 | store_typecheck_error(Msg,Info). | |
319 | check_let_rhs(RHS,Used,ToDefine,_AlreadyDefined,allow_reuse,_Env) --> | |
320 | {ord_intersection(Used,ToDefine,Inter), Inter \= []}, % we use left-hand side ID not yet introduced | |
321 | !, | |
322 | % potentially cyclic let | |
323 | {ajoin_with_sep(['LET right-hand-side uses not-yet-defined identifiers:'|Inter],' ',Msg), | |
324 | get_texpr_info(RHS,Info)}, | |
325 | store_typecheck_error(Msg,Info). | |
326 | check_let_rhs(RHS,Used,_ToDefine,AlreadyDefined,allow_reuse,Env) --> | |
327 | {possible_ambiguity(Used,AlreadyDefined,Env,ClashIds)}, | |
328 | % we use variables which are visible and introduced: could be very confusing | |
329 | !, | |
330 | {ajoin_with_sep(['Possible ambiguity: LET right-hand-side re-uses visible identifiers:'|ClashIds],' ',Msg), | |
331 | get_texpr_info(RHS,Info)}, | |
332 | store_typecheck_error(Msg,Info). | |
333 | check_let_rhs(_,_,_,_,_,_) --> []. | |
334 | ||
335 | possible_ambiguity(Used,AlreadyDefined,Env,ClashIds) :- | |
336 | env_get_visible_ids(Env,Visible), | |
337 | ord_intersection(Used,AlreadyDefined,Inter1), | |
338 | ord_intersection(Inter1,Visible,ClashIds), | |
339 | ClashIds \= []. | |
340 | ||
341 | handle_rewrite_exception(Msg,Name,Pos,TExpr,Infos,TRin,TRout) :- !, | |
342 | store_typecheck_error(Msg,Pos,TRin,TRout), | |
343 | % Type remains unbound, Infos are empty | |
344 | Infos = [], | |
345 | TExpr = identifier(Name). | |
346 | ||
347 | % btype2/8 encodes the type checking rules | |
348 | btype2(identifier(I1), Pos, Env, identifier(I), Type, Infos, TRin, TRout) :- | |
349 | !, % In case the identifier is a list, join it with '.' (e.g. ['M',x] -> 'M.x') | |
350 | (is_list(I1) -> ajoin_with_sep(I1,'.',I) ; I1=I), | |
351 | % get the identifier's type from the type environment | |
352 | lookup_type(I,Env,Pos,Type,TRin,TR1), | |
353 | % copy also additional information from the environment, | |
354 | lookup_infos(I,Env,AllInfos), | |
355 | % but not all (e.g. no position information) | |
356 | extract_id_information(AllInfos,Infos), | |
357 | % an access to this identifier might be illegal, check this | |
358 | ? | (member(error(Error),AllInfos) -> store_typecheck_error(Error, Pos, TR1, TRout) ; TR1=TRout). |
359 | btype2(primed_identifier(Id,N), Pos, Env, identifier(FullId), Type, Infos, TRin, TRout) :- | |
360 | !, % a primed identifier is of the form x$0, we just convert it to | |
361 | % a normal identifier called "x$0" and type-check it. | |
362 | number_suffix(Id,N,FullId), | |
363 | btype(primed_identifier(Id,N),identifier(Pos,FullId),Env,Type,TId,TRin,TRout), | |
364 | get_texpr_info(TId,IdInfos), | |
365 | extract_id_information(IdInfos,Infos). | |
366 | btype2(forall(Ids,EImplication), _, Env, forall(TIdentifiers,TDomain,TPred), pred, [], TRin, TRout) :- | |
367 | !,add_ext_variables_with_info(Ids,Env,[introduced_by(forall)],TIdentifiers,Subenv,TRin,TR1), | |
368 | ext2int(btype2,EImplication,Implication,IPos,_,_,_,_), | |
369 | (btype_rewrite(Implication,Env,IPos,Implication2,IPos2) -> true % in case we have a definition we need to expand it now to transform it into an implication | |
370 | ; Implication2=Implication, IPos2=IPos), | |
371 | % we expect an implication as predicate, if not, generate an error | |
372 | ( Implication2=implication(Domain,Pred) -> | |
373 | btype(forall_domain(Ids),Domain,Subenv,pred,TDomain,TR1,TR2), | |
374 | btype(forall_pred(Ids),Pred,Subenv,pred,TPred,TR2,TRout) | |
375 | ; | |
376 | store_typecheck_error('expected implication in universal quantification ',IPos2,TR1,TR2), | |
377 | create_texpr(truth,pred,[],TDomain), | |
378 | btype(foralle_impl(Ids),EImplication,Subenv,pred,TPred,TR2,TRout) | |
379 | ). | |
380 | btype2(external_function_call_auto(FunName,FunParams), _Pos, Env, | |
381 | external_function_call(FunName,TFunParams), OutputType , [], TRin, TRout) :- !, | |
382 | % artificial raw node external_function_call_auto which infers type information from ProB's database | |
383 | ? | get_external_function_type(FunName,ExpectedArgTypes,OutputType), |
384 | ? | btype_l(FunParams,Env,ArgTypes,TFunParams,TRin,TRin2), |
385 | maplist(get_texpr_pos,TFunParams,ArgPos), | |
386 | unify_types_l(ArgTypes,ExpectedArgTypes,ArgPos,FunName,TRin2,TRout). | |
387 | btype2(external_pred_call_auto(FunName,FunParams), Pos, Env, | |
388 | external_pred_call(FunName,TFunParams), pred , [], TRin, TRout) :- !, | |
389 | % artificial raw node external_pred_call_auto which infers type information from ProB's database | |
390 | ? | get_external_function_type(FunName,ExpectedArgTypes,OutputType), |
391 | unify_types(OutputType,boolean,Pos,no_expression,TRin,TRin1), | |
392 | btype_l(FunParams,Env,ArgTypes,TFunParams,TRin1,TRin2), | |
393 | maplist(get_texpr_pos,TFunParams,ArgPos), | |
394 | unify_types_l(ArgTypes,ExpectedArgTypes,ArgPos,FunName,TRin2,TRout). | |
395 | btype2(external_function_call(FunName,FunParams,_FunDef,TypeParams,Decl), Pos, Env, | |
396 | external_function_call(FunName,TFunParams), OutputType , [], TRin, TRout) :- | |
397 | /* note: position info is automatically added to info field; hence [] ok */ | |
398 | (FunParams = [] -> InputType = empty_type, FullType = set(OutputType) | |
399 | ; FullType = set(set(couple(InputType,OutputType)))), | |
400 | !, btype_external_call(FunName,TypeParams,FunParams,Decl,FullType, | |
401 | InputType,Pos,Env,TFunParams,TRin,TRout). | |
402 | btype2(external_pred_call(FunName,FunParams,_FunDef,TypeParams,Decl), Pos, Env, | |
403 | external_pred_call(FunName,TFunParams), pred, [], TRin, TRout) :- | |
404 | !, btype_external_call(FunName,TypeParams,FunParams,Decl,set(InputType),InputType, | |
405 | Pos,Env,TFunParams,TRin,TRout). | |
406 | btype2(external_subst_call(FunName,FunParams,_FunDef,TypeParams,Decl), Pos, Env, | |
407 | external_subst_call(FunName,TFunParams), subst, [], TRin, TRout) :- | |
408 | !, btype_external_call(FunName,TypeParams,FunParams,Decl,set(InputType),InputType, | |
409 | Pos,Env,TFunParams,TRin,TRout). | |
410 | btype2(integer(I), _, _, integer(I), integer, [], TR, TR) :- !. | |
411 | btype2(integer_set(S), _, _, integer_set(S), set(integer), [], TR, TR) :- !. | |
412 | btype2(real(I), _, _, real(I), real, [], TR, TR) :- !. | |
413 | %btype2(real_set, _, _, real_set, set(real), [], TR, TR) :- !. | |
414 | btype2(string(I), _, _, string(I), string, [], TR, TR) :- !, assert_machine_string(I). | |
415 | btype2(multiline_template(I), _, _, string(I), string, [], TR, TR) :- !, | |
416 | format('xTemplate: `~w`~n',[I]), | |
417 | assert_machine_string(I). | |
418 | btype2(assign(IdFuns,Exprs), Pos, Env, assign(TIdFuns,TExprs), subst, [], TRin, TRout) :- | |
419 | !, | |
420 | common_prefix(IdFuns,Exprs,IdFuns1,Exprs1,OK), | |
421 | btype_l(IdFuns1,Env,Types,TIdFuns,TRin,TR1), | |
422 | ? | btype_l(Exprs1, Env,Types,TExprs, TR1, TR2), |
423 | foldl(check_assign_lhs(Env),TIdFuns,TR2,TR3), | |
424 | ( OK=same_length -> TRout=TR3 | |
425 | ; | |
426 | store_typecheck_error('different number of variables on left and right side of a substitution ',Pos,TR3,TRout) | |
427 | ). | |
428 | btype2(becomes_element_of(Ids,Expr), _, Env, becomes_element_of(TIds,TExpr), subst, [], TRin, TRout) :- | |
429 | !,btype_l(Ids,Env,Types,TIds,TRin,TR1), | |
430 | foldl(check_assign_lhs(Env),TIds,TR1,TR2), | |
431 | couplise_list(Types,Type), | |
432 | btype(becomes_element_of(Ids),Expr,Env,set(Type),TExpr,TR2, TRout). | |
433 | btype2(becomes_such(Ids,Pred), _, Env, becomes_such(TIds,TPred), subst, [], TRin, TRout) :- | |
434 | !,btype_l(Ids,Env,_,TIds,TRin,TR1), | |
435 | foldl(check_assign_lhs(Env),TIds,TR1,TR2), | |
436 | % for each LHS identifier x (in Ids), we add an identifier of the form | |
437 | % x$0 with the same type to the environment | |
438 | foldl(add_primed_id,TIds,Env,Subenv), | |
439 | btype(becomes_such,Pred,Subenv,pred,TPred,TR2,TRout). | |
440 | btype2(evb2_becomes_such(Ids,Pred), _, Env, evb2_becomes_such(TIds,TPred), subst, [], TRin, TRout) :- | |
441 | !,check_evb_becomes_such(evb2_becomes_such,Ids,Pred,Env,TIds,TPred,TRin,TRout). | |
442 | btype2(operation_call(Op,Res,Args), Pos, Env, TOp, subst, Infos, TRin, TRout) :- | |
443 | %print(opcall(Op)),nl, portray_env(Env),nl, | |
444 | !,type_operation_call(Op,Res,Args,Pos,Env,TOp,Infos,TRin,TRout). | |
445 | btype2(operation_call_in_expr(Op,Args), Pos, Env, operation_call_in_expr(TOp,TArgs), Type, Infos, TRin, TRout) :- | |
446 | !, ext2int(btype2_opcall,Op,identifier(Opid),IPos,_,_,_,_), | |
447 | btype2(identifier(op(Opid)),IPos,Env,Identifier,op(ArgTypes,ResTypes),OpInfos,TRin,TR1), | |
448 | Identifier = identifier(_), % Identifier = identifier(op(Opid)) | |
449 | create_texpr(Identifier,subst,OpInfos,TOp), | |
450 | (same_length(Args,ArgTypes) | |
451 | -> btype_l(Args,Env,ArgTypes,TArgs,TR1,TR2) | |
452 | ; add_operation_call_error(ArgTypes,Args,Pos,Opid,'arguments(s)',_,TR1,TR2), | |
453 | TArgs=[] | |
454 | ), | |
455 | when(ground(ResTypes), | |
456 | % sometimes, e.g., in ASSERTIONS, operations have not yet been type checked and ResType is a variable | |
457 | (couplise_list(ResTypes,Type) -> true | |
458 | ; add_error(btype2,'Unexpected return type calling operation in expression:',Opid,Pos))), | |
459 | get_operation_infos(OpInfos,Infos), | |
460 | % print(op_call_in_expr(Opid,ResTypes,Infos,Type)),nl, | |
461 | ( memberchk(modifies(Modifies),Infos) -> | |
462 | (Modifies==[] -> TR2=TR3 | |
463 | ; var(Modifies) -> TR2=TR3, | |
464 | % the info has not yet been computed; add a co-routine (which must however raise error immediately) | |
465 | when(nonvar(Modifies),(Modifies==[] -> true | |
466 | ; add_error(btype2,'Read-only operation expected when calling operation in expressions ',Opid,Pos))) | |
467 | ; get_op_name_modifies_message(Opid,' when calling inside expression',Modifies,Msg), | |
468 | store_typecheck_error(Msg,Pos,TR2,TR3) % used to be called query operation | |
469 | ) | |
470 | ; add_internal_error(btypechecker,'Missing modifies info field:',operation_call_in_expr(Op,Args),Pos),TR2=TR3 | |
471 | ), | |
472 | ( memberchk(reads(_),Infos) -> TR3=TRout | |
473 | ; add_internal_error(btypechecker,'Missing reads info field:',operation_call_in_expr(Op,Args),Pos),TR3=TRout). | |
474 | btype2(case(Expr,Eithers,Else), _, Env, case(TExpr,TEithers,TElse), subst, [], TRin, TRout) :- | |
475 | !,btype(case,Expr,Env,Type,TExpr,TRin,TR1), | |
476 | foldl(btype_caseor(Env,Type),Eithers,TEithers,LExprs,TR1,TR2), | |
477 | append(LExprs,Exprs), | |
478 | btype(case_else,Else,Env,subst,TElse,TR2,TR3), | |
479 | % The next check could be made dependend on a preference (non-literal values allowed in | |
480 | % CASE statements), in that case add TR3=TRout as an alternative | |
481 | check_case_expressions(Exprs,TR3,TRout). | |
482 | btype2(struct(Fields), Pos, Env, struct(TRecord), set(RType), [], TRin, TRout) :- | |
483 | !, btype(struct,rec(Pos,Fields),Env,_,TRecord,TRin,TR1), | |
484 | get_texpr_expr(TRecord,rec(TFields)), | |
485 | foldl(extract_field_type,TFields,FieldTypes,TR1,TR2), | |
486 | normalise_record_type(record(FieldTypes),RType), | |
487 | TR2=TRout. | |
488 | % (record_has_multiple_field_names(FieldTypes,FieldName) %% error already raised by rec(.) clause below | |
489 | btype2(rec(Fields), Pos, Env, rec(TFields), RType, [], TRin, TRout) :- | |
490 | !, foldl(btype_field_rec(Env),Fields,FTypes,TFields1,TRin,TR2), | |
491 | normalise_record_type(record(FTypes),RType), | |
492 | % we sort the field arguments here, so we do not have to normalise them every | |
493 | % time in the interpreter | |
494 | RType = record(NormedFieldTypes), | |
495 | sort_record_fields(NormedFieldTypes,TFields1,TFields,_), | |
496 | (record_has_multiple_field_names(NormedFieldTypes,FieldName) | |
497 | -> ajoin(['Field ',FieldName,' used multiple times in record '],Msg), | |
498 | store_typecheck_error(Msg,Pos,TR2,TRout) | |
499 | ; TR2=TRout | |
500 | ). | |
501 | btype2(record_field(Record,I), Pos, Env, record_field(TRecord,Id), Type, [], TRin, TRout) :- | |
502 | !, | |
503 | btype(record_field,Record, Env, RType, TRecord, TRin, TR1), | |
504 | remove_pos(I,identifier(Id)), | |
505 | unify_types(record(Fields),RType,Pos,TRecord,TR1,TR2), | |
506 | check_field_type(Fields,Id,Type,Pos,TR2,TRout). | |
507 | btype2(refined_operation(Id,Results,Args,_RefinesID,Body), Pos, Env, TExpr, Type, Infos, TRin, TRout) :- | |
508 | !, % TO DO: do we need to treat RefinesID ? | |
509 | btype2(operation(Id,Results,Args,Body), Pos, Env, TExpr, Type, Infos, TRin, TRout). | |
510 | btype2(description_operation(Desc,Operation), _Pos, Env, TExpr, Type, [description(Desc)|Infos], TRin, TRout) :- | |
511 | !, | |
512 | btype(description, Operation, Env, Type, Result, TRin, TRout), | |
513 | get_texpr_expr(Result,TExpr), | |
514 | get_btype_infos_from_sub(Result,Infos). | |
515 | btype2(operation(Id,Results,Args,Body), Pos, Env, operation(TId,TResults,TArgs,TBody), Type, | |
516 | Infos, TRin, TRout) :- | |
517 | %print(checking_op(Id)),nl, | |
518 | !, %debug_stats(checking_operation(Id,Args)), | |
519 | % type-check the identifier to look up the operation's type | |
520 | % in the environment. | |
521 | % we call ext2int and btype2/7 directly instead of going over | |
522 | % btype/5, because we use op(Name) instead of Name to look up | |
523 | % the type. This is done to seperate operation and variable name | |
524 | % spaces (Note: that was a stupid and ugly hack) | |
525 | ext2int(btype2_operation,Id,identifier(Opid),IPos,Type,Topid,IdInfos,TId), | |
526 | btype2(identifier(op(Opid)),IPos,Env,Topid,Type,IdInfos,TRin,TR0), | |
527 | % introduce a sub-environment Subenv by adding the argument and | |
528 | % result variables | |
529 | check_for_duplicate_raw_ids(Results,[],'results for operation ',Opid,FilteredResults,TR0,TR1), | |
530 | add_ext_variables_with_info(FilteredResults,Env,[introduced_by(operation)],TResults,Subenv1,TR1,TR2), | |
531 | check_for_duplicate_raw_ids(Args,[],'arguments for operation ',Opid,FilteredArgs,TR2,TR2b), | |
532 | add_ext_variables_with_info(FilteredArgs,Subenv1,[readonly,introduced_by(operation)],TArgs,Subenv,TR2b,TR3), | |
533 | % get their types and determine the resulting operation's type | |
534 | get_texpr_types(TResults,LResultTypes), | |
535 | get_texpr_types(TArgs,LArgTypes), | |
536 | unify_types(op(LArgTypes,LResultTypes),Type,Pos,TId,TR3,TR4), | |
537 | % type the operation's body in the sub-environment | |
538 | ? | btype(operation(Id),Body, Subenv, subst, TBody, TR4, TRout), |
539 | % the list of modified machine variables is the list of changed | |
540 | % variables by the substitutions in the body minus the result variables | |
541 | compute_accessed_vars_infos_for_operation(Id,TResults,TArgs,TBody,Modifies,Reads,NonDetModified,Infos), | |
542 | %assertz(op_modifies_reads_cache(Opid,Modifies,Reads)), % cache information for operation_calls; possibly temporary solution until we understand the code for operation_call [Note: we can have multiple versions ! at different refinement levels !!] | |
543 | % make sure that the List of modified variables of this operation | |
544 | % is also up-to-date in the type environment | |
545 | (memberchk(modifies(EnvModifies),IdInfos), | |
546 | memberchk(reads(EnvReads),IdInfos), | |
547 | memberchk(non_det_modifies(EnvNonDetModifies),IdInfos) -> | |
548 | % Check if the environment variables and the local variables are unifiable. | |
549 | % If not, an operation with the same name must have been defined before | |
550 | % We can ignore this, later an error message will be raised; triggered in test 1307 | |
551 | ( EnvModifies=Modifies | |
552 | -> ( EnvReads=Reads | |
553 | -> ( EnvNonDetModifies=NonDetModified -> true | |
554 | ; add_message(btypechecker,'Duplicate operation, conflict in non_det_modifies info for ',Opid,IPos) | |
555 | ) | |
556 | ; add_message(btypechecker,'Duplicate operation, conflict in reads info for ',Opid,IPos) | |
557 | ) | |
558 | ; add_message(btypechecker,'Duplicate operation, conflict in modifies info for ',Opid,IPos) | |
559 | ) | |
560 | ; add_error(btypechecker,'Cannot store modifies/reads info for: ',Opid,IPos) | |
561 | ), | |
562 | debug_format(9,'Finished checking operation ~w, reads:~w, writes=~w~n',[Id,Reads,Modifies]). | |
563 | btype2(while(Pred,Body,Inv,Var), _, Env, while(TPred,TBody,TInv,TVar), subst, FullInfo, TRin, TRout) :- !, | |
564 | btype(while,Pred,Env,pred,TPred,TRin,TR1), | |
565 | btype(while_body,Body,Env,subst,TBody,TR1,TR2), | |
566 | % In contrast to the other substitutions, in the invariant and variant | |
567 | % part of a while loop it is possible to reference abstract variables | |
568 | % and also imported variables (cf. 6.17 AtelierB handbook), | |
569 | % as they are not used to influence the behaviour of the substitution. | |
570 | % We create a new environment InvEnv where those access restrictions are | |
571 | % removed. | |
572 | allow_access_to_abstract_vars(Env,InvEnv), % TODO: also make available in ASSERT, cf Atelier-B handbook | |
573 | add_primed_old_value_variables(InvEnv,PInvEnv), | |
574 | btype(while_inv,Inv,PInvEnv,pred,TInv,TR2,TR3), | |
575 | btype(while_variant,Var,InvEnv,integer,TVar,TR3,TRout), | |
576 | % tag this statement with an appropiate info if a reference to the original value | |
577 | % of a variable is made in the invariant. | |
578 | % This info is used in the clean_up (see b_ast_cleanup) to insert a LET statement. | |
579 | check_for_old_state_references(TInv,Info), | |
580 | FullInfo = [modifies(Modifies),reads(AllReads)|Info], | |
581 | % TO DO: ideally we should compute those in one go for all substitutions: | |
582 | % here we compute information again which we have already computed for operations | |
583 | get_accessed_vars(b(while(TPred,TBody,TInv,TVar),subst,Info),[],Modifies,_NonDetModifies,Reads), | |
584 | (debug:debug_mode(off) -> true | |
585 | ; format('WHILE Reads : ~w~n Modifies : ~w~n',[Reads,Modifies]), | |
586 | print('VARIANT: '),translate:print_bexpr(TVar),nl | |
587 | ), | |
588 | (member(refers_to_old_state(SortedRefs),Info) | |
589 | -> findall(Primed,member(oref(Primed,_,_),SortedRefs),PrimedDollarVars), sort(PrimedDollarVars,SPDV), | |
590 | ord_union(SPDV,Reads,AllReads) %, print(add(SPDV,Reads)),nl | |
591 | ; AllReads = Reads). | |
592 | ||
593 | btype2(parallel(Substs),Pos,Env,parallel(TSubsts), subst, [], TRin, TRout) :- | |
594 | ? | !, btype_l(Substs,Env,_,TSubsts,TRin,TR1), |
595 | check_no_double_assignment(TSubsts,Pos,TR1,TRout). | |
596 | btype2(minus_or_set_subtract(A,B), Pos, Env, minus_or_set_subtract(TA,TB), Type, [], TRin, TRout) :- | |
597 | !,btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1), | |
598 | delayed_type_minus(TypeA,TypeB,Type,Pos,A,B,TR1,TRout). | |
599 | btype2(add(A,B), Pos, Env, add(TA,TB), Type, [], TRin, TRout) :- | |
600 | allow_to_use_real_types, | |
601 | !,TypeA=TypeB, TypeA=Type, | |
602 | btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1), | |
603 | delayed_type_arith('+',Type,Pos,TR1,TRout). | |
604 | btype2(div(A,B), Pos, Env, div(TA,TB), Type, [], TRin, TRout) :- | |
605 | allow_to_use_real_types, | |
606 | !,TypeA=TypeB, TypeA=Type, | |
607 | btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1), | |
608 | delayed_type_arith('/',Type,Pos,TR1,TRout). | |
609 | btype2(unary_minus(A), Pos, Env, unary_minus(TA), Type, [], TRin, TRout) :- | |
610 | allow_to_use_real_types, | |
611 | !,btype_l([A],Env,[TypeA],[TA],TRin,TR1), | |
612 | delayed_type_arith_unary('-',TypeA,Type,Pos,A,TR1,TRout). | |
613 | btype2(power_of(A,B), Pos, Env, power_of(TA,TB), Type, [], TRin, TRout) :- | |
614 | allow_to_use_real_types, | |
615 | !,btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1), % second arg must be integer, unlike RPOW | |
616 | (TypeB=integer -> TR2=TR1 | |
617 | ; pretty_type(TypeB,TBS), | |
618 | ajoin(['Exponentiation (**) requires exponent of type INTEGER not ',TBS, | |
619 | ' (use RPOW if you need a REAL exponent)'],Msg), | |
620 | store_typecheck_error(Msg,Pos,TR1,TR2) | |
621 | ), | |
622 | delayed_type_arith_unary('**',TypeA,Type,Pos,A,TR2,TRout). | |
623 | btype2(general_sum(A,B,C), Pos, Env, Res, Type, [], TRin, TRout) :- !, % SIGMA | |
624 | (allow_to_use_real_types -> true ; Type=integer), | |
625 | btype3(general_sum(A,B,C), Pos, Env, Res, Type, [], TRin, TR1), | |
626 | delayed_type_arith(general_sum,Type,Pos,TR1,TRout). | |
627 | btype2(general_product(A,B,C), Pos, Env, Res, Type, [], TRin, TRout) :- !, % PI | |
628 | (allow_to_use_real_types -> true ; Type=integer), | |
629 | btype3(general_product(A,B,C), Pos, Env, Res, Type, [], TRin, TR1), | |
630 | delayed_type_arith(general_product,Type,Pos,TR1,TRout). | |
631 | btype2(max(A), Pos, Env, Res, Type, [], TRin, TRout) :- !, % max | |
632 | (allow_to_use_real_types -> true ; Type=integer), | |
633 | btype3(max(A), Pos, Env, Res, Type, [], TRin, TR1), | |
634 | delayed_type_arith(max,Type,Pos,TR1,TRout). | |
635 | btype2(min(A), Pos, Env, Res, Type, [], TRin, TRout) :- !, % min | |
636 | (allow_to_use_real_types -> true ; Type=integer), | |
637 | btype3(min(A), Pos, Env, Res, Type, [], TRin, TR1), | |
638 | delayed_type_arith(min,Type,Pos,TR1,TRout). | |
639 | btype2(less_equal(A,B), Pos, Env, less_equal(TA,TB), pred, [], TRin, TRout) :- | |
640 | allow_to_use_real_types, | |
641 | !, TypeA=TypeB, btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1), | |
642 | delayed_type_arith_comparison('<=',TypeA,Pos,TR1,TRout). | |
643 | btype2(greater_equal(A,B), Pos, Env, greater_equal(TA,TB), pred, [], TRin, TRout) :- | |
644 | allow_to_use_real_types, | |
645 | !, TypeA=TypeB, btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1), | |
646 | delayed_type_arith_comparison('>=',TypeA,Pos,TR1,TRout). | |
647 | btype2(less(A,B), Pos, Env, less(TA,TB), pred, [], TRin, TRout) :- | |
648 | allow_to_use_real_types, | |
649 | !, TypeA=TypeB, btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1), | |
650 | delayed_type_arith_comparison('<',TypeA,Pos,TR1,TRout). | |
651 | btype2(greater(A,B), Pos, Env, greater(TA,TB), pred, [], TRin, TRout) :- | |
652 | allow_to_use_real_types, | |
653 | !, TypeA=TypeB, btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1), | |
654 | delayed_type_arith_comparison('>',TypeA,Pos,TR1,TRout). | |
655 | btype2(concat(A,B), Pos, Env, concat(TA,TB), Type, [], TRin, TRout) :- | |
656 | get_preference(allow_sequence_operators_on_strings,true), % a^b --> STRING_APPEND(a,b) | |
657 | btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1), | |
658 | TypeA \== integer, % otherwise trigger error_rewrite below for exponentiation | |
659 | !, | |
660 | delayed_type_string_or_seq(TypeA,TypeB,Type,Pos,concat,A,B,TR1,TRout). | |
661 | btype2(rev(A), Pos, Env, rev(TA), Type, [], TRin, TRout) :- | |
662 | get_preference(allow_sequence_operators_on_strings,true), % rev(Str) --> STRING_REV(Str) | |
663 | Type = TypeA, | |
664 | btype_l([A],Env,[TypeA],[TA],TRin,TR1), | |
665 | !, | |
666 | delayed_type_string_or_seq_unary(TypeA,TypeA,Pos,rev,A,TR1,TRout). | |
667 | % TODO: first(Str) --> STRING_CHARS(Str)(1), last(Str) --> STRING_CHARS(Str)(size(Str)), Str(i) --> STRING_CHARS(Str)(i) | |
668 | btype2(size(A), Pos, Env, size(TA), Type, [], TRin, TRout) :- | |
669 | get_preference(allow_sequence_operators_on_strings,true), % size(Str) --> STRING_LENGTH(Str) | |
670 | Type = integer, | |
671 | btype_l([A],Env,[TypeA],[TA],TRin,TR1), | |
672 | !, | |
673 | delayed_type_string_or_seq_unary(TypeA,TypeA,Pos,size,A,TR1,TRout). | |
674 | btype2(general_concat(A), Pos, Env, general_concat(TA), Type, [], TRin, TRout) :- | |
675 | get_preference(allow_sequence_operators_on_strings,true), % conc(Strs) --> STRING_CONC(Str) | |
676 | ? | btype_l([A],Env,[TypeA],[TA],TRin,TR1), |
677 | !, | |
678 | delayed_type_seq_string_or_seq_seq(TypeA,Type,Pos,'conc',A,TR1,TRout). | |
679 | btype2(mult_or_cart(A,B), Pos, Env, mult_or_cart(TA,TB), Type, [], TRin, TRout) :- | |
680 | !,btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1), | |
681 | delayed_type_times(TypeA,TypeB,Type,Pos,A,B,TR1,TRout). | |
682 | btype2(substitution(Subst,Pred), _Pos, Env, TSubst, pred, [], TRin, TRout) :- | |
683 | !, type_substitution_expression(Subst,Pred,Env,TSubst,TRin,TRout). | |
684 | btype2(extended_expr(Id,Args,Args2), Pos, Env, Result, Type, [was(operator(Id))|Info], TRin, TRout) :- | |
685 | ? | !, lookup_eventb_operator(Id,Args,Args2,Pos,Env,expr,Result,Type,Info,TRin,TRout). |
686 | btype2(extended_pred(Id,Args,Args2), Pos, Env, Result, Type, [was(operator(Id))|Info], TRin, TRout) :- | |
687 | ? | !, lookup_eventb_operator(Id,Args,Args2,Pos,Env,pred,Result,Type,Info,TRin,TRout). |
688 | btype2(extended_formula(Id,Args,Args2), Pos, Env, Result, Type, [was(operator(Id))|Info], TRin, TRout) :- | |
689 | % not known whether expr or pred, we leave _PrdOrExpr as variable so that create_z_let can infer it | |
690 | ? | !, lookup_eventb_operator(Id,Args,Args2,Pos,Env,_PredOrExpr,Result,Type,Info,TRin,TRout). |
691 | btype2(recursive_let(Id,Set),_Pos,Env,recursive(TId,TSet),set(Type),[],TRin,TRout) :- !, | |
692 | add_ext_variables([Id], Env, [TId], SubEnv, TRin, TR1), | |
693 | get_texpr_type(TId,set(Type)), | |
694 | btype(recursive,Set,SubEnv,set(Type),TSet,TR1,TRout). | |
695 | btype2(set_extension(RawList),Pos,_Env,value(Val),set(Type),[],TR,TR) :- | |
696 | % optimisation: -> skip type checking the content and just generate an AVL set directly | |
697 | % can have a large performance impact for data validation projects | |
698 | simple_set_extension_type(RawList,Type), | |
699 | (preference(optimize_ast,true), | |
700 | read_raw_simple_values(set(Type),set_extension(Pos,RawList),Val) | |
701 | -> true %,add_message(btypechecker,'Converted set_extension:',Type,Pos) | |
702 | ; %add_message(btypechecker,'Failed to convert set_extension:',Type,Pos), | |
703 | fail), !. | |
704 | btype2(sequence_extension(RawList),Pos,_Env,value(Val),seq(Type),[],TR,TR) :- | |
705 | % ditto for sequence extensions | |
706 | simple_set_extension_type(RawList,Type), | |
707 | (preference(optimize_ast,true), | |
708 | read_raw_simple_values(set(couple(integer,Type)),sequence_extension(Pos,RawList),Val) | |
709 | -> true %,add_message(btypechecker,'Converted sequence_extension:',Type,Pos) | |
710 | ; %add_message(btypechecker,'Failed to convert sequence_extension:',Type,Pos), | |
711 | fail), !. | |
712 | btype2(typeset,_Pos,_Env,typeset,set(_),[],TR,TR) :- !. | |
713 | btype2(typeof(InnerExpr,TypeExpr),_Pos,Env,Expr,Type,Info,TRin,TRout) :- | |
714 | !, btype(typeof,TypeExpr,Env,set(Type),_TTypeExpr,TRin,TR1), | |
715 | ? | btype(typeof,InnerExpr,Env,Type,TExpr,TR1,TRout), |
716 | get_texpr_expr(TExpr,Expr),get_btype_infos_from_sub(TExpr,Info). | |
717 | % merge the pragma ast nodes into the info fields | |
718 | btype2(label(Label,Node), _Pos, Env, TExpr, Type, InfosOut, TRin, TRout) :- !, | |
719 | btype(label, Node, Env, Type, Result, TRin, TRout), | |
720 | get_texpr_expr(Result,TExpr), | |
721 | get_btype_infos_from_sub(Result,Infos), | |
722 | add_label_to_infos(Infos,Label,InfosOut). | |
723 | btype2(description(Desc,Node), _Pos, Env, TExpr, Type, [description(Desc)|Infos], TRin, TRout) :- !, | |
724 | btype(description, Node, Env, Type, Result, TRin, TRout), | |
725 | get_texpr_expr(Result,TExpr), | |
726 | get_btype_infos_from_sub(Result,Infos). | |
727 | btype2(symbolic_comprehension_set(A,B), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !, | |
728 | ? | btype2(comprehension_set(A,B), Pos, Env, TExpr, Type, Infos, TRin, TRout). |
729 | btype2(symbolic_event_b_comprehension_set(A,B,C), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !, | |
730 | btype2(event_b_comprehension_set(A,B,C), Pos, Env, TExpr, Type, Infos, TRin, TRout). | |
731 | btype2(symbolic_quantified_union(A,B,C), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !, | |
732 | btype2(quantified_union(A,B,C), Pos, Env, TExpr, Type, Infos, TRin, TRout). | |
733 | btype2(symbolic_lambda(A,B,C), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !, | |
734 | btype2(lambda(A,B,C), Pos, Env, TExpr, Type, Infos, TRin, TRout). | |
735 | btype2(symbolic_composition(A,B), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !, | |
736 | btype2(composition(A,B), Pos, Env, TExpr, Type, Infos, TRin, TRout). | |
737 | btype2(conversion(Node), _Pos, Env, TExpr, Type, [conversion|Infos], TRin, TRout) :- !, | |
738 | btype(conversion, Node, Env, Type, Result, TRin, TRout), | |
739 | get_texpr_expr(Result,TExpr), | |
740 | get_btype_infos_from_sub(Result,Infos). | |
741 | btype2(let_predicate(Ids,Equalities,Pred), Pos, Env, let_predicate(TIdsOut,TExprsOut,TPred), pred, [], TRin, TRout) :- | |
742 | !, % TODO: extract position info from Pos? | |
743 | check_for_duplicate_raw_ids(Ids,[],'LET arguments','',FIds,TRin,TR0), | |
744 | add_ext_variables_with_info(FIds,Env,[introduced_by(let_predicate)],TIds,Subenv,TR0,TR1), | |
745 | btype(let_predicate, Equalities, Subenv, pred, TEqualities, TR1, TR2), % should we introduced variables only one by one ? | |
746 | btype(let_predicate, Pred, Subenv, pred, TPred, TR2, TR3), | |
747 | btype_static_check_let(TIds,TEqualities,Pos,allow_reuse,Env,TR3,TR4), | |
748 | split_let_equalities_into_ids_and_expressions(Ids,TEqualities,TIdsOut,TExprsOut,Pos,TR4,TRout). | |
749 | btype2(let_expression(Ids,Equalities,Expr), Pos, Env, let_expression(TIdsOut,TExprsOut,TExpr), Type, [], TRin, TRout) :- !, | |
750 | check_for_duplicate_raw_ids(Ids,[],'LET arguments','',FIds,TRin,TR0), | |
751 | add_ext_variables_with_info(FIds,Env,[introduced_by(let_expression)],TIds,Subenv,TR0,TR1), | |
752 | btype(let_expression, Equalities, Subenv, pred, TEqualities, TR1, TR2), | |
753 | btype(let_expression, Expr, Subenv, Type, TExpr, TR2, TR3), | |
754 | btype_static_check_let(TIds,TEqualities,Pos,allow_reuse,Env,TR3,TR4), | |
755 | split_let_equalities_into_ids_and_expressions(Ids,TEqualities,TIdsOut,TExprsOut,Pos,TR4,TRout). | |
756 | btype2(value(Val),_Pos,_Env,value(Val),Type,[],TR,TR) :- % support value/1 terms in raw ast | |
757 | infer_value_type(Val,Type), | |
758 | !. | |
759 | btype2(witness_then(Pred,Subst), Pos, Env, TExpr, subst, Infos, TRin, TRout) :- !, | |
760 | make_open(Env,OEnv), | |
761 | % Witness predicates access abstract ANY parameters; we do not support this yet and hence remove Pred | |
762 | % From Atelier B Event-B reference: | |
763 | % In Atelier B, the witness is only used for each disappearing | |
764 | % parameter of a refined ANY substitution. Moreover, only deterministic witnesses are allowed | |
765 | % in the Atelier B through equality predicates. | |
766 | btype(witness_predicate,Pred, OEnv, pred, TPred, TRin, TR0), | |
767 | add_message(btypecker,'Ignoring WITNESS predicate: ',TPred,Pos), | |
768 | btype(witness_body,Subst, Env, subst, TSubst, TR0, TRout), | |
769 | TSubst = b(TExpr,subst,Infos). | |
770 | btype2(Expr, Pos, Env, TExpr, Type, V, TRin, TRout) :- | |
771 | ? | btype3(Expr, Pos, Env, TExpr, Type, V, TRin, TRout). |
772 | ||
773 | ||
774 | ||
775 | btype3(Expr, Pos, Env, TExpr, Type, [], TRin, TRout) :- | |
776 | % this is the most simple case of a type-check | |
777 | safe_functor(btype2_expr,Expr,Functor,Arity), | |
778 | safe_functor(btype2_lookup,Lookup,Functor,Arity), | |
779 | Lookup <:> Type, | |
780 | !, | |
781 | safe_functor(btype2_texpr,TExpr,Functor,Arity), | |
782 | ? | type_and_unify_args(1,Arity,Pos,Env,Expr,Lookup,TExpr,TRin,TRMid), |
783 | (\+ type_error_or_warning_occurred(TRin,TRMid) | |
784 | -> TRMid = TRout | |
785 | ; typecheck_result_get_flags(TRMid,Flags), | |
786 | nonmember(try_rewrite,Flags), | |
787 | typecheck_add_flag(try_rewrite,TRMid,TRMid0), % avoid an exponential blow-up in rewrites; we only do one rewrite at a time | |
788 | %print(try_rewrite(Expr)),nl, | |
789 | error_rewrite(Expr,RewrittenExpr,RewriteMsg), % a common user error may be present | |
790 | % print(rewrite(RewrittenExpr)),nl, | |
791 | % Copy the code from above; we assume | |
792 | copy_term(TRMid0,TRMid1), % copy error variable; avoid instantiating TRMid with error msgs from RewrittenExpr | |
793 | btype2(RewrittenExpr,Pos,Env,_,_,[],TRMid1,TRMid2), | |
794 | %safe_functor(btype2_expr,RewrittenExpr,Functor2,Arity2), | |
795 | %safe_functor(btype2_lookup,Lookup2,Functor2,Arity2), | |
796 | %Lookup <:> Type, print(rewritten_t(Lookup,Type)),nl, | |
797 | % safe_functor(btype2_texpr,TExpr2,Functor2,Arity2), | |
798 | %type_and_unify_args(1,Arity2,Pos,Env,RewrittenExpr,Lookup2,TExpr2,TRMid1,TRMid1), | |
799 | % print(rewrite_ok(TRMid1)),nl, | |
800 | \+ type_error_or_warning_occurred(TRMid1,TRMid2) % the rewrite removed the type error | |
801 | -> ajoin(['Did you ',RewriteMsg,' ?'],Msg), | |
802 | store_typecheck_error(Msg,Pos,TRMid,TRout) | |
803 | ; %print(no_rule_applicable),nl, | |
804 | TRMid=TRout). | |
805 | % Unflatten compact chains of associative operators, e. g. conjunction and disjunction. | |
806 | % The term has a single list argument containing all operands, | |
807 | % e. g. conjunct(pos(...), [A, B, C, ...]). | |
808 | % This format is used since BParser 2.9.31 and in the ANTLR parser. | |
809 | % Old versions of the ANTLR parser (before 2023-10) didn't use a list | |
810 | % and instead added all operands as extra term arguments. | |
811 | % This was limited by Prolog max_arity (255 for SICStus) and is no longer supported. | |
812 | btype3(Expr, Pos, Env, ResExpr, Type, Info, TRin, TRout) :- | |
813 | functor(Expr,Functor,1), | |
814 | associative_functor(Functor), | |
815 | arg(1,Expr,Args), | |
816 | unflatten_assoc(Args,Functor,Pos,NewExpr),!, | |
817 | % TO DO: comment in conjunct/1 typing rules below and support conjunct/1 in bsyntaxtree, ... | |
818 | ? | btype(associative_functor,NewExpr, Env, Type, b(ResExpr,Type,Info0), TRin, TRout), |
819 | delete(Info0,nodeid(_),Info). % the position info will be added by ext2int in btype_aux. | |
820 | % error case. should not be reached | |
821 | btype3(Expr, _Pos, _, _, _, _, TR, TR) :- | |
822 | safe_functor(btype2_uncovered,Expr,F,Arity), | |
823 | add_internal_error('Uncovered construct in type checker: ',F/Arity), | |
824 | fail. | |
825 | ||
826 | associative_functor(conjunct). | |
827 | associative_functor(disjunct). | |
828 | unflatten_assoc([P|Rest],Func,Pos,Result) :- !, unflat2(Rest,P,Func,Pos,Result). | |
829 | unflatten_assoc(V,F,P,R) :- add_internal_error('Illegal call: ',unflatten_assoc(V,F,P,R)),fail. | |
830 | unflat2([],P,_Func,_Pos,P). | |
831 | unflat2([Q|Rest],P,Func,Pos,Result) :- | |
832 | R =.. [Func,Pos,P,Q], | |
833 | unflat2(Rest,R,Func,Pos,Result). | |
834 | ||
835 | ||
836 | ||
837 | :- use_module(kernel_objects,[infer_value_type/2]). | |
838 | ||
839 | compute_accessed_vars_infos_for_operation(_Id,TResults,TArgs,TBody,Modifies,Reads,NonDetModified,Infos) :- | |
840 | append(TResults,TArgs,TLocals), | |
841 | get_texpr_ids(TLocals,Locals), list_to_ord_set(Locals,SLocals),% locals of an operation are either arguments or return variables | |
842 | get_accessed_vars(TBody,[],AllModifies,AllNonDetModified,AllReads), | |
843 | % we now no longer pass Locals, we filter out later to compute reads_locals; otherwise we do not see reading of output variables,... | |
844 | %print(modified_reads(_Id,AllModifies,AllReads)),nl, | |
845 | ord_subtract(AllModifies,SLocals,Modifies), | |
846 | ord_subtract(AllReads,SLocals,Reads), | |
847 | ord_subtract(AllNonDetModified,SLocals,NonDetModified), | |
848 | ord_intersection(AllModifies,SLocals,LocalModifies), | |
849 | ord_intersection(AllReads,SLocals,LocalReads), | |
850 | Infos = [modifies(Modifies),reads(Reads),non_det_modifies(NonDetModified), | |
851 | modifies_locals(LocalModifies),reads_locals(LocalReads)]. | |
852 | ||
853 | split_let_equalities_into_ids_and_expressions(RawIds,EqualitiesPred,IDs,Expressions,_,TR,TR) :- | |
854 | conjunction_to_list(EqualitiesPred,ListOfEqualities), | |
855 | split_let_equality_into_id_and_expression2(ListOfEqualities,IDs,Expressions,RawIds), | |
856 | !. | |
857 | split_let_equalities_into_ids_and_expressions(_,EQs,[],[],Pos,TRIn,TROut) :- | |
858 | translate_bexpression(EQs,PPEqs), | |
859 | ajoin_with_sep(['Let equalities could not be split into ids and expressions:',PPEqs],' ',Msg), | |
860 | store_typecheck_error(Msg,Pos,TRIn,TROut). | |
861 | ||
862 | split_let_equality_into_id_and_expression2([],[],[],_). | |
863 | split_let_equality_into_id_and_expression2([Equality|TE],[TID|TI],[Expression|TEs],RawIds) :- | |
864 | get_texpr_expr(Equality,equal(TID,Expression)), | |
865 | ? | get_texpr_id(TID,ID), select(identifier(_,ID),RawIds,RawIds2), |
866 | !, | |
867 | split_let_equality_into_id_and_expression2(TE,TI,TEs,RawIds2). | |
868 | split_let_equality_into_id_and_expression2([_|TE],TI,TEs,RawIds) :- | |
869 | split_let_equality_into_id_and_expression2(TE,TI,TEs,RawIds). | |
870 | ||
871 | add_label_to_infos([],Label,[label([Label])]). | |
872 | add_label_to_infos([label(LA)|T],Label,[label([Label|LA])|T]) :- !. | |
873 | add_label_to_infos([F|T],Label,[F|TN]) :- | |
874 | add_label_to_infos(T,Label,TN). | |
875 | ||
876 | % check if a set extension is of type integer or couple(integer,...) by inspecting | |
877 | % the first element | |
878 | simple_set_extension_type([First,_|_],Type) :- !, % At least two elements; | |
879 | %maybe we should only apply it for even longer ones? unless elements are themselves complex set extensions | |
880 | simple_set_extension_type2(First,Type). % of type integer, string, boolean or couple / set_extension / seq_ext | |
881 | simple_set_extension_type(L,Type) :- L \= [_|_], | |
882 | add_internal_error('set_extension not a list: ',simple_set_extension_type(L,Type)),fail. | |
883 | simple_set_extension_type2(boolean_false(_),boolean). | |
884 | simple_set_extension_type2(boolean_true(_),boolean). | |
885 | simple_set_extension_type2(integer(_,_),integer). | |
886 | simple_set_extension_type2(unary_minus(_,integer(_,_)),integer). | |
887 | simple_set_extension_type2(string(_,_),string). | |
888 | simple_set_extension_type2(couple(Pos,List),Type) :- % n-ary couple | |
889 | couplise_list_pos(List,Pos,Couple), | |
890 | simple_set_extension_type2(Couple,Type). | |
891 | simple_set_extension_type2(couple(_Pos,A,B),couple(TA,TB)) :- % binary couple | |
892 | simple_set_extension_type2(A,TA), | |
893 | simple_set_extension_type2(B,TB). | |
894 | simple_set_extension_type2(set_extension(_Pos,List),set(Type)) :- % nested set | |
895 | List = [H|_], | |
896 | simple_set_extension_type2(H,Type). | |
897 | simple_set_extension_type2(sequence_extension(_Pos,List),set(couple(integer,Type))) :- | |
898 | % nested sequence | |
899 | % (we do not generate seq(Type) because we only examine first element and the others could be different) | |
900 | List = [H|_], | |
901 | simple_set_extension_type2(H,Type). | |
902 | ||
903 | % convert a raw integer, string, boolean, or pairs of integers into a value | |
904 | read_raw_simple_values(boolean,RI,Val) :- get_raw_boolean(RI,Val). | |
905 | read_raw_simple_values(integer,RI,int(I)) :- get_raw_integer(RI,I). | |
906 | read_raw_simple_values(string,string(_Pos,S),string(S)). | |
907 | %TODO: real(Atom), rec(Fields), intervals, sequence_extension (see eval_set_extension) | |
908 | read_raw_simple_values(couple(TA,TB),couple(_Pos,List),(VA,VB)) :- | |
909 | flatten_couples(List,FlattenedList), % flatten leftmost couple elements into a list | |
910 | read_raw_simple_couple(TA,VA,FlattenedList,Rest), % couple(couple(Ta,Tb),Tc) --> [a,b,c] | |
911 | read_raw_right_of_couple(TB,VB,Rest,[]). | |
912 | read_raw_simple_values(set(Type),AST,Val) :- | |
913 | read_raw_simple_set(AST,Type,Val). | |
914 | ||
915 | read_raw_simple_set(empty_set(_Pos),_,Val) :- Val=[]. % empty_set ok as we already have the type | |
916 | read_raw_simple_set(set_extension(_Pos,RawList),Type,Val) :- | |
917 | l_read_raw_simple_values(RawList,Type,Vals), | |
918 | custom_explicit_sets:convert_to_avl(Vals,Val). | |
919 | read_raw_simple_set(sequence_extension(_Pos,RawList),couple(integer,Type),Val) :- | |
920 | l_read_raw_simple_values(RawList,Type,Vals), | |
921 | add_indexes(Vals,1,SeqVals), | |
922 | custom_explicit_sets:convert_to_avl(SeqVals,Val). | |
923 | ||
924 | % read list of simple values | |
925 | l_read_raw_simple_values([],_Type,[]). | |
926 | l_read_raw_simple_values([H|T],Type,[V|VT]) :- | |
927 | read_raw_simple_values(Type,H,V), | |
928 | l_read_raw_simple_values(T,Type,VT). | |
929 | ||
930 | add_indexes([],_,[]). | |
931 | add_indexes([H|T],Idx,[(int(Idx),H)|IT]) :- I1 is Idx+1, add_indexes(T,I1,IT). | |
932 | ||
933 | read_raw_simple_couple(boolean,Val) --> [RI], {get_raw_boolean(RI,Val)}. | |
934 | read_raw_simple_couple(integer,int(I)) --> [RI], {get_raw_integer(RI,I)}. | |
935 | read_raw_simple_couple(string,string(I)) --> [string(_Pos,I)]. | |
936 | read_raw_simple_couple(set(Type),Val) --> [SetExtension], | |
937 | {read_raw_simple_values(set(Type),SetExtension,Val)}. | |
938 | read_raw_simple_couple(couple(TA,TB),(VA,VB)) --> % couple values for TA are in the same list | |
939 | read_raw_simple_couple(TA,VA), | |
940 | read_raw_right_of_couple(TB,VB). % if TB is a couple type then the value in the list must be a couple | |
941 | ||
942 | % special rule for right of couple: here a couple type must be treated differently | |
943 | read_raw_right_of_couple(couple(TA,TB),Val) --> !, [RawCouple], | |
944 | {read_raw_simple_values(couple(TA,TB),RawCouple,Val)}. | |
945 | read_raw_right_of_couple(Type,Val) --> read_raw_simple_couple(Type,Val). | |
946 | ||
947 | flatten_couples(C,Res) :- flatten_dcg(C,Res,[]). | |
948 | flatten_dcg(couple(_Pos,List)) --> !, flatten_dcg(List). | |
949 | flatten_dcg([H|T]) --> !, flatten_dcg(H), copy_list(T). | |
950 | flatten_dcg(OtherVal) --> [OtherVal]. | |
951 | ||
952 | copy_list([]) --> []. | |
953 | copy_list([H|T]) --> [H], copy_list(T). | |
954 | ||
955 | get_raw_boolean(boolean_true(_),pred_true). | |
956 | get_raw_boolean(boolean_false(_),pred_false). | |
957 | ||
958 | get_raw_integer(integer(_Pos,I),I). | |
959 | get_raw_integer(unary_minus(_Pos,RI),MI) :- get_raw_integer(RI,I), integer(I), MI is -I. | |
960 | ||
961 | % find common prefix of two lists (assigned variables, assigned expressions) | |
962 | common_prefix([],[],[],[],Res) :- !, Res=same_length. | |
963 | common_prefix([H1|T1],[H2|T2],[H1|TT1],[H2|TT2],OK) :- !, | |
964 | common_prefix(T1,T2,TT1,TT2,OK). | |
965 | common_prefix(_,_,[],[],not_same_length). | |
966 | ||
967 | check_no_double_assignment(TSubsts,Pos,TRin,TRout) :- | |
968 | maplist(modified_var,TSubsts,Mods), | |
969 | ( (preference(allow_simultaneous_assignments,false), | |
970 | find_common_variables(Mods,Var)) -> | |
971 | ajoin(['Simultaneous assignment to variable ',Var],Msg), | |
972 | store_typecheck_error(Msg,Pos,TRin,TRout) | |
973 | ; | |
974 | TRin = TRout). | |
975 | modified_var(TSubst,Modified) :- | |
976 | get_accessed_vars(TSubst,[],Modified,_NDModified,_Read). | |
977 | find_common_variables([Vars|Rest],Var) :- | |
978 | find_common_variables2(Rest,Vars,Var). | |
979 | find_common_variables2([Vars|Vrest],Prior,Var) :- | |
980 | ord_intersection(Vars,Prior,FoundVars), | |
981 | ( memberchk(Var,FoundVars) -> true | |
982 | ; | |
983 | ord_union(Vars,Prior,NewVars), | |
984 | find_common_variables2(Vrest,NewVars,Var)). | |
985 | ||
986 | type_substitution_expression(Subst,Pred,Env, | |
987 | let_predicate(TypedLhs,TypedRhs,TPred),TRin,TRout) :- | |
988 | ( remove_pos(Subst,assign(Lhs,Rhs)) -> | |
989 | ( same_length(Lhs,Rhs) -> | |
990 | /* Typecheck the right side of the substitution */ | |
991 | btype_l(Rhs,Env,Types,TypedRhs,TRin,TR1), | |
992 | /* The left site of the substitution introduces new variables which have the | |
993 | same type as the corrresponding element of the RHS */ | |
994 | add_ext_variables_with_info(Lhs,Env,[introduced_by(let)],TypedLhs,SubEnv,TR1,TR2), | |
995 | get_texpr_types(TypedLhs,Types), | |
996 | /* Type the predicates in the sub-environment */ | |
997 | btype(substitution_expression,Pred,SubEnv,pred,TPred,TR2,TRout) | |
998 | ; /* LHS hat not the same number of elements as RHS */ | |
999 | ext2int(Subst,_,Pos,_,_,_,_), | |
1000 | TypedLhs=[], TypedRhs=[], create_texpr(truth,pred,[],TPred), | |
1001 | store_typecheck_error('Expected same number of elements on both sides of an assignment', | |
1002 | Pos,TRin,TRout)) | |
1003 | ; /* Substitution is no assignment (the parser should not allow this) */ | |
1004 | add_internal_error('Expected assignment in substitution expression, but was: ',Subst), | |
1005 | fail). | |
1006 | ||
1007 | delayed_type_minus(TypeA,TypeB,ResType,Pos,ExprA,ExprB,TRin,TRout) :- | |
1008 | arg(1,ExprA,PosA), arg(1,ExprB,PosB), | |
1009 | % In case of A-B=C we know that A, B and C have the same type | |
1010 | unify_types_l([ResType,ResType],[TypeA,TypeB],[PosA,PosB],'-',TRin,TR1), | |
1011 | % but not if it is integer or set(_) | |
1012 | typecheck_result_add_delayed_rule(Trigger,Errors,TR1,TRout), | |
1013 | delayed_type_minus2(ResType,Trigger,Pos,Errors). | |
1014 | :- block delayed_type_minus2(-,-,?,?). | |
1015 | delayed_type_minus2(Type,_Trigger,Pos,Errors) :- | |
1016 | ( var(Type) -> | |
1017 | Errors = [error('Ambiguous expression (arithmetic minus or set minus?)',Pos)] | |
1018 | ; (Type = integer ; Type = real) -> | |
1019 | Errors = [] | |
1020 | ; | |
1021 | unify_types_werrors_l([set(_)],[Type],[Pos],'-',Errors,[]) | |
1022 | ). | |
1023 | ||
1024 | % for arithmetic operators which can be of type integer or real | |
1025 | delayed_type_arith_unary(OP,TypeA,ResType,Pos,ExprA,TRin,TRout) :- | |
1026 | arg(1,ExprA,PosA), | |
1027 | unify_types_l([ResType],[TypeA],[PosA],OP,TRin,TR1), | |
1028 | % check integer or real | |
1029 | typecheck_result_add_delayed_rule(Trigger,Errors,TR1,TRout), | |
1030 | delayed_type_arith2(ResType,Trigger,OP,Pos,Errors). | |
1031 | delayed_type_arith_comparison(OP,TypeAB,Pos,TRin,TRout) :- | |
1032 | typecheck_result_add_delayed_rule(Trigger,Errors,TRin,TRout), | |
1033 | delayed_type_arith2(TypeAB,Trigger,OP,Pos,Errors). | |
1034 | delayed_type_arith(OP,ResType,Pos,TRin,TRout) :- | |
1035 | % In case of A OP B=C we know that A, B and C have the same type | |
1036 | %%used to call: unify_types_l([ResType,ResType],[TypeA,TypeB],[PosA,PosB],TRin,TR1), | |
1037 | % check integer or real | |
1038 | typecheck_result_add_delayed_rule(Trigger,Errors,TRin,TRout), | |
1039 | delayed_type_arith2(ResType,Trigger,OP,Pos,Errors). | |
1040 | :- block delayed_type_arith2(-,-,?,?,?). | |
1041 | delayed_type_arith2(Type,_Trigger,OP,Pos,Errors) :- | |
1042 | ( var(Type) -> | |
1043 | ajoin(['Ambiguous expression using ',OP, ' (can be of type REAL or INTEGER)'], Msg), | |
1044 | % for compatibility we could force integer type | |
1045 | Errors = [error(Msg,Pos)] | |
1046 | ; (Type = integer ; Type = real) -> | |
1047 | Errors = [] | |
1048 | ; | |
1049 | unify_types_werrors_l([integer],[Type],[Pos],OP,Errors,[]) % TO DO: integer or real | |
1050 | ). | |
1051 | ||
1052 | % for concat: allow a types to be either string or seq(A) | |
1053 | delayed_type_string_or_seq(TypeA,TypeB,ResType,Pos,Context,ExprA,ExprB,TRin,TRout) :- | |
1054 | arg(1,ExprA,PosA), arg(1,ExprB,PosB), | |
1055 | % In case of A^B=C we know that A, B and C have the same type | |
1056 | unify_types_l([ResType,ResType],[TypeA,TypeB],[PosA,PosB],Context,TRin,TR1), | |
1057 | % but not if it is integer or set(_) | |
1058 | typecheck_result_add_delayed_rule(Trigger,Errors,TR1,TRout), | |
1059 | delayed_type_string_or_seq2(ResType,Trigger,Pos,Context,Errors). | |
1060 | :- block delayed_type_string_or_seq2(-,-,?,?,?). | |
1061 | delayed_type_string_or_seq2(Type,_Trigger,Pos,Context,Errors) :- | |
1062 | ( %var(Type) -> Errors = [error('Ambiguous expression (seq(_) or string operator?)',Pos)] ; | |
1063 | Type == string -> | |
1064 | Errors = [] | |
1065 | ; | |
1066 | unify_types_werrors_l([seq(_)],[Type],[Pos],Context,Errors,[]) | |
1067 | ). | |
1068 | ||
1069 | % version of above with one argument, e.g., for rev or size: | |
1070 | delayed_type_string_or_seq_unary(TypeA,ResType,Pos,Context,ExprA,TRin,TRout) :- | |
1071 | arg(1,ExprA,PosA), | |
1072 | % In case of A^B=C we know that A, B and C have the same type | |
1073 | unify_types(ResType,TypeA,PosA,Context,TRin,TR1), | |
1074 | % but not if it is integer or set(_) | |
1075 | typecheck_result_add_delayed_rule(Trigger,Errors,TR1,TRout), | |
1076 | delayed_type_string_or_seq2(ResType,Trigger,Pos,Context,Errors). | |
1077 | ||
1078 | ||
1079 | % for general_concat(seq(Type)) -> Type, where Type = string or seq(T) | |
1080 | delayed_type_seq_string_or_seq_seq(TypeA,ResType,Pos,Context,ExprA,TRin,TRout) :- | |
1081 | arg(1,ExprA,PosA), | |
1082 | unify_types_l([seq(ResType)],[TypeA],[PosA],Context,TRin,TR1), | |
1083 | % but not if it is integer or set(_) | |
1084 | typecheck_result_add_delayed_rule(Trigger,Errors,TR1,TRout), | |
1085 | delayed_type_string_or_seq2(ResType,Trigger,Pos,Context,Errors). | |
1086 | ||
1087 | % delayed_type_times(TypeA,TypeB,ResType,Pos,ExprA,ExprB,TRin,TRout): | |
1088 | % "A*B=R" | |
1089 | % TypeA: type of A, TypeB: type of B, ResType: type of R | |
1090 | % Pos: position info for error messages | |
1091 | % ExprA/B: expressions to generate pretty error messages | |
1092 | delayed_type_times(TypeA,TypeB,ResType,Pos,ExprA,ExprB,TRin,TRout) :- | |
1093 | arg(1,ExprA,PosA), arg(1,ExprB,PosB), | |
1094 | ( maplist(var,[TypeA,TypeB,ResType]) -> | |
1095 | typecheck_result_add_delayed_rule(Trigger,Errors,TRin,TRout), | |
1096 | delayed_type_times2(TypeA,TypeB,ResType,Trigger,Pos,PosA,PosB,Errors) | |
1097 | ; contains_exact_type([TypeA,TypeB,ResType],integer) -> | |
1098 | % One type is an integer | |
1099 | unify_types_l([integer,integer,integer],[TypeA,TypeB,ResType],[PosA,PosB,Pos],'*',TRin,TRout) | |
1100 | ; contains_exact_type([TypeA,TypeB,ResType],real) -> | |
1101 | % One type is a real | |
1102 | (allow_to_use_real_types -> ExpectedType=real ; ExpectedType=integer), | |
1103 | unify_types_l([ExpectedType,ExpectedType,ExpectedType],[TypeA,TypeB,ResType],[PosA,PosB,Pos],'*',TRin,TRout) | |
1104 | ; | |
1105 | % A type is known, no need for a delay | |
1106 | unify_types_l([set(couple(X,Y)),set(X),set(Y)],[ResType,TypeA,TypeB],[Pos,PosA,PosB],'*',TRin,TRout) | |
1107 | ). | |
1108 | :- block delayed_type_times2(-,-,-,-,?,?,?,?). | |
1109 | delayed_type_times2(A,B,Res,_Trigger,Pos,PosA,PosB,Errors) :- | |
1110 | ( maplist(var,[A,B,Res]) -> | |
1111 | Errors = [error('Ambiguous expression (multiplication or cartesian product?)',Pos)] | |
1112 | ; contains_exact_type([A,B,Res],integer) -> | |
1113 | unify_types_werrors_l([integer,integer,integer],[A,B,Res],[PosA,PosB,Pos],'*',Errors,[]) | |
1114 | ; contains_exact_type([A,B,Res],real) -> | |
1115 | (allow_to_use_real_types -> ExpectedType=real ; ExpectedType=integer), | |
1116 | unify_types_werrors_l([ExpectedType,ExpectedType,ExpectedType],[A,B,Res],[PosA,PosB,Pos],'*',Errors,[]) | |
1117 | ; | |
1118 | unify_types_werrors_l([set(X),set(Y),set(couple(X,Y))],[A,B,Res],[PosA,PosB,Pos],'*',Errors,[]) | |
1119 | ). | |
1120 | ||
1121 | :- use_module(probsrc(bmachine_eventb),[some_operator_uses_reals/0]). | |
1122 | :- use_module(probsrc(specfile), [animation_minor_mode/1]). | |
1123 | allow_to_use_real_types :- | |
1124 | get_preference(allow_arith_operators_on_reals,ALLOW), | |
1125 | (ALLOW = true -> true | |
1126 | ; ALLOW = default, | |
1127 | (animation_minor_mode(eventb) | |
1128 | -> some_operator_uses_reals % for the moment disable REAL usage for Event-B models unless we detect an operator | |
1129 | ; \+ animation_minor_mode(alloy) % for test 1929 | |
1130 | ) | |
1131 | % e.g., for EventBPrologPackages/Tests/TestInvalidInit_mch.eventb we get a type error | |
1132 | ). | |
1133 | ||
1134 | contains_exact_type([T|Rest],Type) :- (T==Type -> true ; contains_exact_type(Rest,Type)). | |
1135 | ||
1136 | type_operation_call(Op,Res,Args,Pos,Env,operation_call(TOp,TRes,TArgs),Infos,TRin,TRout) :- | |
1137 | ext2int(btype2_opcall,Op,identifier(Opid),IPos,_,_,_,_), % succeeds if operation name is a proper identifier | |
1138 | !, | |
1139 | btype2(identifier(op(Opid)),IPos,Env,Identifier,op(ArgTypes1,ResTypes1),OpInfos,TRin,TR1), | |
1140 | Identifier = identifier(OpIdW), % OpIdW = op(_) | |
1141 | create_texpr(Identifier,subst,OpInfos,TOp), | |
1142 | btype_l(Args,Env,_ArgTypes,TArgs,TR1,TR2), | |
1143 | btype_l(Res,Env,_ResTypes,TRes,TR2,TR3), | |
1144 | foldl(check_assign_lhs(Env),TRes,TR3,TR4), | |
1145 | ( same_length(Args,ArgTypes1) -> | |
1146 | ( same_length(Res,ResTypes1) -> | |
1147 | % number of arguments resp. results ok | |
1148 | type_operation_call2(OpIdW,Env,Pos,TRes,TArgs,ArgTypes1,ResTypes1,Infos,TR4,TRout) | |
1149 | ; | |
1150 | % wrong number of result identifiers given | |
1151 | add_operation_call_error(ResTypes1,Res,Pos,Opid,'result identifiers(s)',Infos,TR4,TRout)) | |
1152 | ; | |
1153 | % wrong number of arguments given | |
1154 | add_operation_call_error(ArgTypes1,Args,Pos,Opid,'arguments(s)',Infos,TR4,TRout)). | |
1155 | type_operation_call(Op,_Res,_Args,Pos,_Env,skip,[],TRin,TRout) :- | |
1156 | % operation name is not an id but e.g. a function call | |
1157 | functor(Op,Func,_), | |
1158 | ajoin(['Expected an identifier for operation call but got "',Func,'" operator'],Msg), | |
1159 | store_typecheck_error(Msg,Pos,TRin,TRout). | |
1160 | type_operation_call2(OpId,Env,Pos,TRes,TArgs,ArgTypes,ResTypes,Infos,TRin,TRout) :- | |
1161 | check_arguments(TArgs,ArgTypes,OpId,TRin,TR1), % check the arguments | |
1162 | check_arguments(TRes,ResTypes,OpId,TR1,TR2), % check the result | |
1163 | ||
1164 | % if the called operation is not found in the environment, | |
1165 | % an error was stored above, and we skip the following section | |
1166 | ( env_lookup_infos(OpId,Env,EnvInfos) -> | |
1167 | % we currently return the modifies/1 information of the called operation | |
1168 | % the only information about this node. This information is needed by | |
1169 | % get_modified_vars/3. | |
1170 | get_operation_infos(EnvInfos,Infos), | |
1171 | % check if we are in a section where we can only call operations | |
1172 | % that make no changes to the state ("inquiry") | |
1173 | ( memberchk(dontcall,EnvInfos), | |
1174 | get_preference(allow_local_operation_calls,false) -> % or allow_operation_calls_in_expr ? | |
1175 | % it is not allowed do call the operation: this is the case if a local | |
1176 | % operation is used (only operations of included/used/seen machines are allowed to call) | |
1177 | % TO DO: we are allowed to call LOCAL_OPERATIONS from other OPERATIONS | |
1178 | def_get_op_name(OpId,OpName), | |
1179 | ajoin(['A local operation "',OpName,'" must not be called'],Msg), | |
1180 | store_typecheck_error(Msg,Pos,TR2,TRout) | |
1181 | ; memberchk(inquiry,EnvInfos) -> | |
1182 | % check whether we call a read-only query-operation, if the target it marked "inquiry only" | |
1183 | ( memberchk(modifies([]),Infos) -> TR2=TRout | |
1184 | ; memberchk(modifies(Modifies),Infos), Modifies = [_|_], def_get_op_name(OpId,OpName) -> | |
1185 | get_op_name_modifies_message(OpName,'',Modifies,Msg), | |
1186 | store_typecheck_error(Msg,Pos,TR2,TRout) | |
1187 | ; store_typecheck_error('Read-Only operation expected ',Pos,TR2,TRout) % was named query-operation | |
1188 | ) | |
1189 | ; | |
1190 | % ok, we may call even state-changing operations | |
1191 | TR2=TRout | |
1192 | ) | |
1193 | ; | |
1194 | % operation not found, skip additional checks above and | |
1195 | % state (maybe incorrectly, but errors are reported anyway), | |
1196 | % that the operation call does not modify any variables | |
1197 | Infos = [modifies([]),reads([]),non_det_modifies([])], | |
1198 | TR2=TRout). | |
1199 | check_arguments(TArgs,ArgTypes1,ContextExpr,TRin,TRout) :- | |
1200 | get_texpr_types(TArgs,ArgTypes), maplist(get_texpr_pos,TArgs,ArgPos), | |
1201 | unify_types_l(ArgTypes1,ArgTypes,ArgPos,ContextExpr,TRin,TRout). | |
1202 | ||
1203 | def_get_op_name(op(OpName),Res) :- !, Res=OpName. | |
1204 | def_get_op_name(A,Res) :- add_warning(btypechecker,'Expected op(.) identifier:',A), | |
1205 | atom(A),!, Res=A. | |
1206 | def_get_op_name(_,'?'). | |
1207 | ||
1208 | get_op_name_modifies_message(OpName,Context,[MVar|OtherMod],Msg) :- !, | |
1209 | (OtherMod = [] -> EG = '' ; EG = ', e.g.,'), | |
1210 | ajoin(['Read-Only operation expected',Context,' (operation ',OpName, ' writes', EG,' variable ',MVar,')'],Msg). | |
1211 | get_op_name_modifies_message(_,_,_,'Read-Only operation expected'). % should not happen | |
1212 | ||
1213 | % Generate an error for the wrong numbers of arguments resp. result identifiers | |
1214 | add_operation_call_error(ExpTypes,GivenExpr,Pos,Opid,Title,Infos,TRin,TRout) :- | |
1215 | (Infos = [modifies([]),reads([])] -> true % Info field must be set, even in case of an error | |
1216 | ; add_internal_error('Could not set operation infos: ',Opid:Infos)), | |
1217 | length(ExpTypes,Expected),length(GivenExpr,Given), | |
1218 | ajoin(['Expected ',Expected,' ',Title,' for operation ',Opid, | |
1219 | ', but ',Given,' ',Title,' given'],Msg), | |
1220 | store_typecheck_error(Msg,Pos,TRin,TRout). | |
1221 | ||
1222 | ||
1223 | % common typing patterns: | |
1224 | % type a list of expressions, return the list of types and typed expressions | |
1225 | btype_l([],_Env,Types,TExprs,TR,TR) :- | |
1226 | (Types=[] -> TExprs = [] | |
1227 | ; add_error(btype_l,'Too few expressions/arguments provided, types expected:',Types), | |
1228 | % normally these errors should be caught earlier | |
1229 | TExprs=[]). | |
1230 | btype_l([Expr|Rest],Env,Types,[TExpr|TERest],TRin,TRout) :- | |
1231 | (Types = [Type|TRest] | |
1232 | -> % (translate:print_raw_bexpr(Expr),nl -> true ; true), | |
1233 | (try_get_raw_position_info(Expr,RodinPos), | |
1234 | RodinPos = rodinpos(_,_,_) | |
1235 | -> set_typecheck_position_context(RodinPos), | |
1236 | ? | btype(btype_l,Expr,Env,Type,TExpr,TRin,TR1), |
1237 | reset_typecheck_position_context | |
1238 | ? | ; btype(btype_l,Expr,Env,Type,TExpr,TRin,TR1) |
1239 | ), | |
1240 | ? | btype_l(Rest,Env,TRest,TERest,TR1,TRout) |
1241 | ; add_error(btype_l,'Too many expressions/arguments provided, additional expr:',Expr), | |
1242 | fail). | |
1243 | ||
1244 | % type a list of expressions whose type is the same | |
1245 | btype_same([],_Env,_Type,[],TR,TR). | |
1246 | btype_same([Expr|ERest],Env,Type,[TExpr|TERest],TRin,TRout) :- | |
1247 | ? | btype(btype_same,Expr, Env, ElemType, TExpr, TRin, TR1), |
1248 | get_texpr_pos(TExpr,Pos), | |
1249 | unify_types(Type,ElemType,Pos,TExpr,TR1,TR2), | |
1250 | ? | btype_same(ERest,Env,Type,TERest,TR2,TRout). |
1251 | ||
1252 | % for a list of identifiers, create a subenvironment with | |
1253 | % their primed versions. I.e., for each identifier "x", introduce | |
1254 | % a variable "x$0" into the environment. | |
1255 | % The type and additional information is copied from the original | |
1256 | % identifier, aditionally information about what the original | |
1257 | % identifier was ist stored. | |
1258 | add_primed_id(TId,InEnv,SubEnv) :- | |
1259 | def_get_texpr_id(TId,Id), | |
1260 | get_texpr_type(TId,Type), | |
1261 | get_texpr_info(TId,Infos), | |
1262 | number_suffix(Id,0,FullId), | |
1263 | % the additional information is used in the interpreter to store the | |
1264 | % values before the substitution under the alternative names | |
1265 | %env_store(FullId,Type,[before_substitution(Id,FullId)|Infos],InEnv,SubEnv). | |
1266 | env_store(FullId,Type,Infos,InEnv,SubEnv). | |
1267 | ||
1268 | ||
1269 | ||
1270 | % special cases | |
1271 | ||
1272 | check_evb_becomes_such(Label,Ids,Pred,Env,TIds,TPred,TRin,TRout) :- | |
1273 | btype_l(Ids,Env,_,TIds,TRin,TR1), | |
1274 | foldl(check_assign_lhs(Env),TIds,TR1,TR2), | |
1275 | prime_identifiers(TIds,TPrimed), | |
1276 | add_identifiers_to_environment(TPrimed,Env,Subenv), | |
1277 | btype(Label,Pred,Subenv,pred,TPred,TR2,TRout). | |
1278 | ||
1279 | % CASE ... EITHER .. OR ... END | |
1280 | btype_caseor(Env,Type,CaseOr,TCaseOr,TExprs,TRin,TRout) :- | |
1281 | ext2int(btype_caseor,CaseOr,case_or(Exprs,Subst),_,pred,case_or(TExprs,TSubst),[],TCaseOr), | |
1282 | % a case expresiion can have multiple expressions that may match, all of the same type "Type" | |
1283 | btype_same(Exprs,Env,Type,TExprs,TRin,TR1), | |
1284 | btype(btype_caseor,Subst,Env,subst,TSubst,TR1,TRout). | |
1285 | % TO DO: check that Field1 of case_or(Field1,_) is a literal value | |
1286 | check_case_expressions(Exprs,TRin,TRout) :- | |
1287 | maplist(is_literal,Exprs),!, % only literals allowed | |
1288 | ( contains_duplicate_literal(Exprs,Duplicate) -> | |
1289 | translate_bexpression(Duplicate,DStr), | |
1290 | get_texpr_pos(Duplicate,Pos), | |
1291 | ajoin(['Duplicate case in CASE statement: ',DStr],Msg), | |
1292 | store_typecheck_error(Msg,Pos,TRin,TRout) | |
1293 | ; % ok, all literals, no duplicates | |
1294 | TRin=TRout | |
1295 | ). | |
1296 | check_case_expressions(Exprs,TRin,TRout) :- | |
1297 | % there are elements that are not literals | |
1298 | exclude(is_literal,Exprs,NonLiterals), | |
1299 | foldl(non_literal_error,NonLiterals,TRin,TRout). | |
1300 | is_literal(TExpr) :- | |
1301 | get_texpr_expr(TExpr,Expr), | |
1302 | get_texpr_info(TExpr,Info), | |
1303 | is_literal2(Expr,Info). | |
1304 | is_literal2(identifier(_),Info) :- | |
1305 | memberchk(enumerated_set_element,Info). | |
1306 | is_literal2(integer(_),_Info). | |
1307 | is_literal2(real(_),_Info). | |
1308 | is_literal2(boolean_true,_Info). | |
1309 | is_literal2(boolean_false,_Info). | |
1310 | is_literal2(string(_),_Info). | |
1311 | non_literal_error(TExpr,TRin,TRout) :- | |
1312 | translate_bexpression(TExpr,Str), | |
1313 | get_texpr_pos(TExpr,Pos), | |
1314 | ajoin(['CASE argument \'',Str,'\' is not a literal value.'],Msg), | |
1315 | store_typecheck_error(Msg,Pos,TRin,TRout). | |
1316 | contains_duplicate_literal(TExprs,Duplicate) :- | |
1317 | % This can be done, because we know that TExprs are literals, so there are no | |
1318 | % sub-expressions with positions information or similar problems | |
1319 | append(_Prefix,[Dup|Rest],TExprs), | |
1320 | get_texpr_expr(Dup,Expr), | |
1321 | get_texpr_expr(Duplicate,Expr), | |
1322 | memberchk(Duplicate,Rest),!. | |
1323 | ||
1324 | btype_field_rec(Env,Ext,field(Id,Type),field(Id,TExpr),TRin,TRout) :- | |
1325 | remove_pos(Ext,rec_entry(Identifier,Expr)), | |
1326 | (remove_pos(Identifier,identifier(Id)) -> true | |
1327 | ; add_error_and_fail(btype_field_rec,'Invalid record field Identifier',Identifier)), | |
1328 | btype(field,Expr,Env,Type,TExpr,TRin,TRout). | |
1329 | ||
1330 | extract_field_type(field(Id,TExpr),field(Id,Type),TRin,TRout) :- | |
1331 | get_texpr_type(TExpr,SetType), | |
1332 | get_texpr_pos(TExpr,Pos), | |
1333 | unify_types(set(Type),SetType,Pos,TExpr,TRin,TRout). | |
1334 | ||
1335 | sort_record_fields(Var,F,R,R2) :- var(Var),!, | |
1336 | add_internal_error('Illegal variable argument:',sort_record_fields(Var,F,R,R2)), | |
1337 | fail. | |
1338 | sort_record_fields([],Rest,[],Rest). | |
1339 | sort_record_fields([field(Id,_Type)|Trest],Fields,[Field|Frest],RestFields) :- | |
1340 | Field = field(Id,_Value), | |
1341 | ? | select(Field,Fields,Fields1),!, |
1342 | sort_record_fields(Trest,Fields1,Frest,RestFields). | |
1343 | ||
1344 | lookup_eventb_operator(Id,Args1,Args2,Pos,Env,ExPr,Result,Type,Info,TRin,TRout) :- | |
1345 | ( env_lookup_infos(operator(Id),Env,[Module:Callback]) -> | |
1346 | append(Args1,Args2,Args), % do not distinguish between expressions and predicates | |
1347 | ? | btype_l(Args,Env,_Types,TArgs,TRin,TR1), |
1348 | % calls registered operator code like direct_definition | |
1349 | ? | call(Module:Callback,Id,TArgs,Pos,Env,ExPr,TExpr,TR1,TRout), |
1350 | create_texpr(Result,Type,Info,TExpr) | |
1351 | ; Args1=[], Args2=[], % it could by a datatype that is registered as such in the environment | |
1352 | env_lookup_type(Id,Env,Type) % cf T_TemperatureMachine_mch.eventb; no longer required ? | |
1353 | -> format('~nLooked up datatype ~w of type ~w~n',[Id,Type]), | |
1354 | lookup_type(Id,Env,Pos,Type,TRin,TRout), | |
1355 | lookup_infos(Id,Env,Info), | |
1356 | Result = identifier(Id) | |
1357 | ; | |
1358 | length(Args1,L1), length(Args2,L2), Arity is L1+L2, | |
1359 | ajoin(['Unknown operator "',Id,'" of arity ',Arity],Msg), | |
1360 | store_typecheck_error(Msg,Pos,TRin,TRout), | |
1361 | failure_syntax_element(ExPr,Id,Result,Type)). | |
1362 | % TODO[DP,2013-01-31]: copied from bmachine_eventb -> refactor! | |
1363 | failure_syntax_element(expr,Id,identifier(Id),_). | |
1364 | failure_syntax_element(pred,_Id,falsity,pred). | |
1365 | ||
1366 | get_operation_infos(Info,OpInfos) :- | |
1367 | operation_infos(OpInfos), | |
1368 | get_operation_infos2(OpInfos,Info). | |
1369 | get_operation_infos2([],_). | |
1370 | get_operation_infos2([Info|Rest],AllInfos) :- | |
1371 | memberchk(Info,AllInfos), | |
1372 | get_operation_infos2(Rest,AllInfos). | |
1373 | ||
1374 | % the following information is required for each operation identifier | |
1375 | % it is "filled" by the type-checker (the operation/4 case of btype2) via compute_accessed_vars_infos_for_operation | |
1376 | operation_infos(Infos) :- findall(I,operation_info(I),Infos). | |
1377 | operation_info(modifies(_)). | |
1378 | operation_info(reads(_)). | |
1379 | operation_info(non_det_modifies(_)). | |
1380 | ||
1381 | ||
1382 | % unify type arguments of two terms | |
1383 | % N is the number of the argument which should be processed | |
1384 | % Arity is the arity of the term, so 1 <= N <= Arity | |
1385 | % Env is the type environment | |
1386 | % TypeTerm is a term that corresponds to the syntax element | |
1387 | % e.g. "1<5" ~ less(1,5) has a type term less(integer,integer) | |
1388 | % in the arguments of the TypeTerm, special constructs may be used: | |
1389 | % "[Type]" declares that there is a list of expressions with the same Type | |
1390 | % "ids" declares that there is a list of identifiers wich build a | |
1391 | % sub-environment which will be used in the following arguments | |
1392 | % (strict left-to-right) | |
1393 | % "ids(T)" is like "ids" but the types of the identifiers are merged | |
1394 | % | |
1395 | % TExpr is the typed expression of the complete expression | |
1396 | % GI as usual: Introduced identifier and errors | |
1397 | type_and_unify_args(N,Arity,Pos,Env,Expr,TypeTerm,TExpr,TRin,TRout) :- | |
1398 | %print(chck(N,Arity,Expr,TypeTerm,TExpr)),nl, | |
1399 | ( N =< Arity -> | |
1400 | arg(N,Expr,Arg), % Expr is the raw expression of the Nth argument | |
1401 | arg(N,TypeTerm,ArgType), % ArgType is the corresponding type | |
1402 | arg(N,TExpr,ArgTExpr), % TExpr is the corresponding typed expression | |
1403 | ? | type_and_unify_args_aux(ArgType,Arg,Pos,Expr,Env,ArgTExpr,NextEnv,TRin,TR2), |
1404 | N2 is N+1, | |
1405 | ? | type_and_unify_args(N2,Arity,Pos,NextEnv,Expr,TypeTerm,TExpr,TR2,TRout) |
1406 | ; | |
1407 | TRin=TRout | |
1408 | ). | |
1409 | type_and_unify_args_aux(ArgType,Arg,Pos,Expr,Env,ArgTExpr,NextEnv,TRin,TRout) :- | |
1410 | % new identifiers are introduced, they are | |
1411 | % available in the environment of the following arguments | |
1412 | nonvar(ArgType), | |
1413 | id_introduced(ArgType,CoupledType,Duplicates,Infos), | |
1414 | !, | |
1415 | functor(Expr,ExprFunctor,_), % Stored inside the information of newly created variables | |
1416 | flatten_illegal_couples(Arg,FixedArg), | |
1417 | ( Duplicates = unique -> check_for_duplicates(FixedArg,Env,all,TRin,TR0) | |
1418 | ; Duplicates = allowed -> check_for_duplicates(FixedArg,Env,[definition],TRin,TR0) | |
1419 | ), % just check that there are no clashes with definitions | |
1420 | check_for_duplicates_within_list(FixedArg,[],TR0,TR1), % check that within the list there are no duplicates | |
1421 | add_introduced_by_info(ExprFunctor,Infos,NewInfos), | |
1422 | add_ext_variables_with_info(FixedArg,Env,NewInfos,ArgTExpr,NextEnv,TR1,TR2), | |
1423 | % convert the list of types to a "couplised" type, | |
1424 | % (e.g. [a] -> a, or [a,b] -> couple(a,b) ) | |
1425 | % in many cases (if ArgType==ids), the "couplised" type is just ignored | |
1426 | idlist_to_type(ArgTExpr,CoupledType1), | |
1427 | unify_types(CoupledType,CoupledType1,Pos,ArgTExpr,TR2,TRout). | |
1428 | type_and_unify_args_aux(ArgType,Arg,_Pos,_Expr,Env,ArgTExpr,NextEnv,TRin,TRout) :- | |
1429 | % if the argument is of the form [...] we expect a list of | |
1430 | % expressions with the same type | |
1431 | nonvar(ArgType),ArgType = [CommonType],!, | |
1432 | ? | btype_same(Arg,Env,CommonType,ArgTExpr,TRin,TRout), |
1433 | NextEnv = Env. | |
1434 | type_and_unify_args_aux(ArgType,Arg,Pos,Expr,Env,ArgTExpr,NextEnv,TRin,TRout) :- | |
1435 | % standard case: just type-check the argument | |
1436 | ? | btype(type_and_unify_args(Pos,Expr,Arg,ArgType),Arg,Env,ArgType,ArgTExpr,TRin,TRout), |
1437 | NextEnv = Env. | |
1438 | ||
1439 | % Note: Nothing seems to use introduced_by(_); except for exists in b_intepreter | |
1440 | add_introduced_by_info(exists,Infos,Res) :- !, Res=[introduced_by(exists)|Infos]. | |
1441 | add_introduced_by_info(_,Infos,Infos). | |
1442 | ||
1443 | % id_introduced(+Pattern,-CoupledType,-DuplicateIdentifiers,-Infos): | |
1444 | % Pattern is a pattern in the type checking database (<:>/2). | |
1445 | % id_introduced/4 extracts the CoupledType (may be a free variable), | |
1446 | % (see the declaration of "comprehension_set" for an example use) | |
1447 | % and returns a flag if an introduction of an already existing variable | |
1448 | % is allowed. (E.g. LET does not allow to declare an existing identifier). | |
1449 | % Additional infos that are added to the type environment are supported. | |
1450 | id_introduced(ids,_,allowed,[]). | |
1451 | id_introduced(ids(CoupledType),CoupledType,allowed,[]). | |
1452 | id_introduced(new_ids,_,unique,[]). | |
1453 | id_introduced(new_readonly_ids,_,unique,[readonly]). | |
1454 | id_introduced(new_readonly_ids(CoupledType),CoupledType,unique,[readonly]). | |
1455 | % Atelier-B actually does allow ANY/LET/VAR to override existing ids ! | |
1456 | ||
1457 | ||
1458 | % check_for_duplicates(IdList,Env,TRin,TRout): | |
1459 | % IdList is a list of (not typechecked) identifiers | |
1460 | % If an identifier already exists in the environment Env, an error | |
1461 | % is added (if the type matches the InvalidTypes argument) | |
1462 | %check_for_duplicates(IdList,Env,TRin,TRout) :- check_for_duplicates(IdList,Env,all,TRin,TRout). | |
1463 | check_for_duplicates(IdList,Env,InvalidTypes,TRin,TRout) :- | |
1464 | foldl(check_for_duplicates_aux(Env,InvalidTypes),IdList,TRin,TRout). | |
1465 | check_for_duplicates_aux(Env,InvalidTypes,identifier(Pos,Id),TRin,TRout) :- !, | |
1466 | (env_lookup_type(Id,Env,IdType), % Id exists already in the environment with type IdType | |
1467 | check_invalid_type(InvalidTypes,IdType) | |
1468 | -> | |
1469 | (env_lookup_position_string(Id,Env,PosStr) -> PosInfo = [' at (line:column) =',PosStr] ; PosInfo = []), | |
1470 | (get_idtype_desc(IdType,Desc) | |
1471 | -> ajoin(['Identifier ',Id,' has already been declared as ', Desc|PosInfo],Msg) | |
1472 | ; ajoin(['Identifier ',Id,' has already been declared'|PosInfo],Msg)), | |
1473 | store_typecheck_warning(Msg,Pos,TRin,TRout) % we now use store_typecheck_warning instead of store_typecheck_error | |
1474 | ; | |
1475 | TRin=TRout | |
1476 | ). | |
1477 | check_for_duplicates_aux(_Env,_InvalidTypes,Other,TRin,TRout) :- !, | |
1478 | % Illegal other term at place where ids are expected: Other; possibly via DEFINITION rewrite | |
1479 | expected_identifier_error(Other,TRin,TRout). | |
1480 | ||
1481 | expected_identifier_error(Other,TRin,TRout) :- | |
1482 | safe_functor(check_for_duplicates,Other,Functor,Arity), | |
1483 | (try_get_raw_position_info(Other,Pos) -> true ; Pos=unknown), | |
1484 | ajoin(['Term is not an identifier (possibly due to DEFINITION rewrite): ', Functor,'/',Arity],Msg), | |
1485 | store_typecheck_error(Msg,Pos,TRin,TRout). | |
1486 | ||
1487 | % check within a list of raw ids whether there are duplicates | |
1488 | % e.g. {xx,xx|xx:BOOL} is not allowed | |
1489 | check_for_duplicates_within_list([],_,Tr,Tr). | |
1490 | check_for_duplicates_within_list([identifier(Pos,ID)|_],Prev,TRin,TRout) :- member(ID,Prev),!, | |
1491 | ajoin(['Identifier ',ID,' is introduced twice in the same construct'],Msg), | |
1492 | store_typecheck_error(Msg,Pos,TRin,TRout). | |
1493 | check_for_duplicates_within_list([identifier(_,ID)|T],Prev,TRin,TRout) :- !, | |
1494 | check_for_duplicates_within_list(T,[ID|Prev],TRin,TRout). | |
1495 | check_for_duplicates_within_list([Other|T],Prev,TRin,TRout) :- | |
1496 | expected_identifier_error(Other,TRin,TR2), | |
1497 | check_for_duplicates_within_list(T,Prev,TR2,TRout). | |
1498 | ||
1499 | get_idtype_desc(IdType,_) :- var(IdType),!,fail. | |
1500 | get_idtype_desc(global(S),Desc) :- !, ajoin(['element of SET ',S],Desc). | |
1501 | % TO DO: add more descriptionsid_introduced | |
1502 | get_idtype_desc(IdType,Desc) :- nonvar(IdType), functor(IdType,Desc,_). | |
1503 | ||
1504 | % check if the type is one we do not allow in this context | |
1505 | check_invalid_type(all,_). | |
1506 | check_invalid_type([H|T],IdType) :- nonvar(IdType), functor(IdType,F,_), member(F,[H|T]). | |
1507 | ||
1508 | % remove illegal couple terms introduced by Prolog BParser: TO DO: adapt Prolog BParser for UNION/INTER/... | |
1509 | flatten_illegal_couples([],Res) :- !, Res=[]. | |
1510 | flatten_illegal_couples([couple(_Pos,Ids)],Res) :- !, Res = Ids. | |
1511 | flatten_illegal_couples([H|T],Res) :- !, Res = [H|T]. | |
1512 | flatten_illegal_couples(identifier(Pos,ID),Res) :- | |
1513 | add_warning(btypechecker,'Fixing error in AST, missing list around:',ID,Pos), | |
1514 | Res = [identifier(Pos,ID)]. | |
1515 | ||
1516 | % environment access | |
1517 | lookup_type(Id,Env,Pos,Type,TRin,TRout) :- | |
1518 | ( env_lookup_type(Id,Env,Type) -> | |
1519 | TRin=TRout | |
1520 | ; | |
1521 | %print(Id), nl,portray_env(Env),nl, | |
1522 | get_current_context(Ctxt), | |
1523 | (Id = op(Op) | |
1524 | -> UMsg = 'Unknown operation "', Id0 = Op | |
1525 | ; UMsg = 'Unknown identifier "', Id0 = Id | |
1526 | ), | |
1527 | ( Id \= op(_), env_lookup_type(op(Id),Env,_OpType) -> | |
1528 | ajoin(['Illegal use of operation identifier "',Id,'"',Ctxt],Msg) | |
1529 | ; Id \= op(_), is_primed_of(Id,UnprimedId), env_lookup_type(UnprimedId,Env,_UpType) -> | |
1530 | ajoin(['Primed version "', Id, '" of identifier ', UnprimedId, ' not available',Ctxt],Msg) | |
1531 | % id$0: available in becomes_such or in invariant of while loops for abstract/imported variables | |
1532 | ; Id \= operator(_), env_lookup_type(operator(Id),Env,_OpType) -> | |
1533 | % did happen in REPL when EventB Theories loaded; should no longer happen | |
1534 | % we now rewrite function applications to extended_expr/_pred in btype_rewrite | |
1535 | ajoin(['Use of this Event-B theory operator not supported yet: "',Id,'"',Ctxt],Msg) | |
1536 | ; fuzzy_find_possible_ids(Id0,Env,AlternativeIds,_Len) -> | |
1537 | (AlternativeIds=[AlternativeId] -> | |
1538 | ajoin([UMsg,Id0,'"',Ctxt,', did you mean "',AlternativeId,'"?'],Msg) | |
1539 | ; wrap_ids_in_quotes(AlternativeIds,WIds), | |
1540 | ajoin([UMsg,Id0,'"',Ctxt,', did you mean one of: '|WIds],Msg) | |
1541 | ) | |
1542 | ; find_possible_completion_ids(Id0,Env,AlternativeIds,Len) -> | |
1543 | (AlternativeIds=[AlternativeId] -> | |
1544 | ajoin([UMsg,Id0,'"',Ctxt,', the possible completion is "',AlternativeId,'"'],Msg) | |
1545 | ; Len=<3 -> | |
1546 | wrap_ids_in_quotes(AlternativeIds,WIds), | |
1547 | ajoin([UMsg,Id0,'"',Ctxt,', the ', Len, ' possible completions are '|WIds],Msg) | |
1548 | ; prefix_length(AlternativeIds,AIds3,3), wrap_ids_in_quotes(AIds3,WIds), | |
1549 | ajoin([UMsg,Id0,'"',Ctxt,', 3 possible completions (out of ',Len,') are '|WIds],Msg) | |
1550 | ) | |
1551 | ? | ; find_possible_suffix_id(Id,Env,AlternativeId) -> |
1552 | ajoin([UMsg,Id0,'"',Ctxt,', a possible alternative is "',AlternativeId,'"'],Msg) | |
1553 | ; | |
1554 | ajoin([UMsg,Id0,'"',Ctxt],Msg) % (lookup type) | |
1555 | % TO DO: maybe look if the identifier exists in the machine project (b_get_machine_constants,b_get_machine_variables,...), but is not visible; we need bmachine to register the ids | |
1556 | %, env_get_visible_ids(Env,Ids), format(user_error,'Known identifiers are: ~w~n',[Ids]) | |
1557 | ), | |
1558 | store_typecheck_error(Msg,Pos,TRin,TRout)). | |
1559 | lookup_infos(Id,Env,Infos) :- | |
1560 | (env_lookup_infos(Id,Env,Infos) -> ! ; Infos=[]). | |
1561 | ||
1562 | is_primed_of(Id0,Id) :- atom(Id0), atom_concat(Id,'$0',Id0). | |
1563 | ||
1564 | :- use_module(tools_matching,[fuzzy_match_codes/2, codes_to_lower_case/2,get_current_expr_keywords/1]). | |
1565 | ||
1566 | fuzzy_find_possible_ids(Id,Env,SortedAlternativeIds,Len) :- | |
1567 | findall(AId,fuzzy_find_possible_id(Id,Env,AId),AlternativeIds), | |
1568 | sort(AlternativeIds,SortedAlternativeIds), | |
1569 | length(SortedAlternativeIds,Len), | |
1570 | Len>0. | |
1571 | ||
1572 | fuzzy_find_possible_id(Id,Env,AlternativeId) :- atom_codes(Id,Codes1), | |
1573 | codes_to_lower_case(Codes1,LCodes1), | |
1574 | env_get_visible_ids_and_keywords(Env,Ids), | |
1575 | ? | member(AIdOrOp,Ids), id_or_op_codes(AIdOrOp,AlternativeId,Codes2), |
1576 | codes_to_lower_case(Codes2,LCodes2), | |
1577 | ? | fuzzy_match_codes(LCodes1,LCodes2), |
1578 | AlternativeId \= Id. | |
1579 | ||
1580 | env_get_visible_ids_and_keywords(ids(Ids),AllIds) :- !, % special env to provide local available ids | |
1581 | AllIds=Ids. | |
1582 | env_get_visible_ids_and_keywords(Env,AllIds) :- | |
1583 | env_get_visible_ids(Env,Ids), | |
1584 | get_current_expr_keywords(Keywords), | |
1585 | ord_union(Ids,Keywords,AllIds). | |
1586 | ||
1587 | wrap_ids_in_quotes([],[]). | |
1588 | wrap_ids_in_quotes([ID],['"',ID,'"']) :- !. | |
1589 | wrap_ids_in_quotes([ID|T],['"',ID,'", '|WT]) :- wrap_ids_in_quotes(T,WT). | |
1590 | ||
1591 | ||
1592 | find_possible_completion_ids(Id,Env,SortedAlternativeIds,Len) :- | |
1593 | findall(AId,find_possible_completion_id(Id,Env,AId),AlternativeIds), | |
1594 | sort(AlternativeIds,SortedAlternativeIds), | |
1595 | length(SortedAlternativeIds,Len), | |
1596 | Len>0. | |
1597 | ||
1598 | % find possible completion of an (unknown) identifier | |
1599 | find_possible_completion_id(Id,Env,AlternativeId) :- atom_codes(Id,Codes1), | |
1600 | codes_to_lower_case(Codes1,LCodes1), | |
1601 | env_get_visible_ids_and_keywords(Env,Ids), % TODO: we could sort the Ids | |
1602 | ? | member(AIdOrOp,Ids), id_or_op_codes(AIdOrOp,AlternativeId,Codes2), |
1603 | codes_to_lower_case(Codes2,LCodes2), | |
1604 | prefix(LCodes2,LCodes1), | |
1605 | AlternativeId \= Id. | |
1606 | ||
1607 | id_or_op_codes(op(ID),RealID,Codes) :- !, RealID=ID, atom_codes(ID,Codes). | |
1608 | id_or_op_codes(operator(ID),RealID,Codes) :- !, RealID=ID, atom_codes(ID,Codes). | |
1609 | id_or_op_codes(ID,ID,Codes) :- atom(ID),!, atom_codes(ID,Codes). | |
1610 | ||
1611 | % find if an (unknown) identifier is a suffix of some known id; | |
1612 | % or a known id is a prefix (supposing the id is not too short or the delta in length not too large) | |
1613 | find_possible_suffix_id(Id,Env,AlternativeId) :- id_or_op_codes(Id,_,Codes1), | |
1614 | codes_to_lower_case(Codes1,LCodes1), | |
1615 | length(Codes1,Len1), Len1 > 1, | |
1616 | env_get_visible_ids_and_keywords(Env,Ids), | |
1617 | ? | member(AIdOrOp,Ids), id_or_op_codes(AIdOrOp,AlternativeId,Codes2), |
1618 | codes_to_lower_case(Codes2,LCodes2), | |
1619 | (suffix(LCodes2,LCodes1) -> true % known identifier is an extension of id | |
1620 | ; prefix(LCodes1,LCodes2), | |
1621 | length(LCodes2,Len2), | |
1622 | (Len2 > 2 ; Diff is Len1-Len2, Diff <3) % Diff of 1 is already handled in fuzzy_match_codes | |
1623 | ), | |
1624 | AlternativeId \= Id. | |
1625 | ||
1626 | ||
1627 | % check if the left hand side of an assignment is writeable | |
1628 | check_assign_lhs(Env,TExpr,TRin,TRout) :- | |
1629 | ( id_or_function_or_rec(TExpr,Id) -> | |
1630 | get_texpr_type(TExpr,Type), | |
1631 | lookup_infos(Id,Env,Infos), | |
1632 | ? | ( member(readonly,Infos) -> |
1633 | get_texpr_pos(TExpr,Pos), | |
1634 | store_typecheck_error('read-only expression on left hand side of assignment ',Pos,TRin,TRout) | |
1635 | ; nonvar(Type), Type = op(_,_) -> | |
1636 | get_texpr_pos(TExpr,Pos), | |
1637 | store_typecheck_error('operation on left hand side of assignment ',Pos,TRin,TRout) | |
1638 | ; | |
1639 | TRin=TRout | |
1640 | ) | |
1641 | ; | |
1642 | get_texpr_pos(TExpr,Pos), | |
1643 | store_typecheck_error('unsupported expression on left hand side of assignment ',Pos,TRin,TRout)). | |
1644 | ||
1645 | id_or_function_or_rec(TIdFunc,Id) :- | |
1646 | id_or_function_or_rec(TIdFunc,_,Id). | |
1647 | ||
1648 | id_or_function_or_rec(TIdFunc,AccessType,Id) :- % AccessType: ensure we do not mix functions and record_fields | |
1649 | get_texpr_expr(TIdFunc,IdFunc), | |
1650 | id_or_function2(IdFunc,AccessType,Id). | |
1651 | id_or_function2(identifier(Id),_,Id). | |
1652 | id_or_function2(function(Func,_Arg),function,Id) :- % allow things like ff(a)(b) := RHS | |
1653 | id_or_function_or_rec(Func,function,Id). | |
1654 | id_or_function2(record_field(Record,_Arg),record_field,Id) :- | |
1655 | % we do not allow things like ff(a)'field:= RHS but we allo ff'field1'field2:= RHS and xx'field := RHS | |
1656 | id_or_function_or_rec(Record,record_field,Id). | |
1657 | ||
1658 | % extract information for identifiers from the environment | |
1659 | % currently, use all information but the position | |
1660 | extract_id_information(InfosIn,InfosOut) :- | |
1661 | exclude(is_information_to_remove,InfosIn,InfosOut). | |
1662 | is_information_to_remove(nodeid(_)). % the nodeid of the usage of the id is already stored | |
1663 | is_information_to_remove(remove(_)). | |
1664 | ||
1665 | % get infos to pass from subterm to higher term in btype2: position info is already set up via ext2int | |
1666 | get_btype_infos_from_sub(b(_,_,Infos0),Infos) :- | |
1667 | delete(Infos0,nodeid(_),Infos). % nodeid position info already added higher | |
1668 | ||
1669 | % some helper predicates | |
1670 | :- assert_must_succeed(btypechecker:couplise_list([a],a)). | |
1671 | :- assert_must_succeed(btypechecker:couplise_list([a,b],couple(a,b))). | |
1672 | :- assert_must_succeed(btypechecker:couplise_list([a,b,c],couple(couple(a,b),c))). | |
1673 | :- assert_must_succeed(btypechecker:couplise_list([a,b,c,d],couple(couple(couple(a,b),c),d))). | |
1674 | couplise_list([A],R) :- !,R=A. | |
1675 | couplise_list([A,B],R) :- !,R=couple(A,B). | |
1676 | couplise_list([A,B|Rest],Result) :- | |
1677 | couplise_list([couple(A,B)|Rest],Result). | |
1678 | ||
1679 | couplise_list_pos([A],_,A) :- !. | |
1680 | couplise_list_pos([A,B],Pos,couple(Pos,A,B)) :- !. | |
1681 | couplise_list_pos([A,B|Rest],Pos,Result) :- | |
1682 | couplise_list_pos([couple(Pos,A,B)|Rest],Pos,Result). | |
1683 | ||
1684 | idlist_to_type(Exprs,Type) :- | |
1685 | get_texpr_types(Exprs,Types), | |
1686 | couplise_list(Types,Type). | |
1687 | ||
1688 | % remove choice_or constructs in a list | |
1689 | % there has to be at least one occurrence of choice_or | |
1690 | remove_choice_ors(Options,Substs) :- | |
1691 | memberchk(choice_or(_,_),Options), % TODO: Is it ok that this could fail? | |
1692 | maplist(remove_choice_or2,Options,Substs). | |
1693 | remove_choice_or2(choice_or(_,Subst),Subst) :- !. | |
1694 | remove_choice_or2(Subst,Subst). | |
1695 | ||
1696 | add_identifiers_to_environment(Ids,In,Out) :- | |
1697 | foldl(add_identifier_to_environment,Ids,In,Out). | |
1698 | add_identifier_to_environment(TExpr,In,Out) :- | |
1699 | def_get_texpr_id(TExpr,Id), | |
1700 | get_texpr_type(TExpr,Type), | |
1701 | get_texpr_info(TExpr,Info), | |
1702 | env_store(Id,Type,Info,In,Out). | |
1703 | ||
1704 | % can nows also be used to unprime ids: | |
1705 | % Event-B style priming: x' is state of x after | |
1706 | prime_identifiers(TExprs,Primed) :- | |
1707 | maplist(prime_identifier,TExprs,Primed). | |
1708 | prime_identifier(b(identifier(Id),Type,Info),b(identifier(Primed),Type,Info)) :- | |
1709 | atom_concat(Id,'\'',Primed). | |
1710 | % add (or remove) a prime (') to a plain identifier (without syntax structure) | |
1711 | prime_id(UnPrimed,Primed) :- | |
1712 | atom_concat(UnPrimed,'\'',Primed). | |
1713 | is_primed_id(Id) :- atom_codes(Id,Codes),last(Codes,0'\'). | |
1714 | ||
1715 | % Note: we could use '\x2032\' for priming; this Unicode prime is accepted by the BParser | |
1716 | % Or we could do this in the pretty_printer | |
1717 | ||
1718 | % Clasccial B semantics: x$0 is state of x before | |
1719 | prime_identifiers0(TExprs,Primed) :- | |
1720 | maplist(prime_identifier0,TExprs,Primed). | |
1721 | prime_identifier0(b(identifier(Id),Type,Info),b(identifier(Primed),Type,Info)) :- | |
1722 | atom_concat(Id,'$0',Primed). | |
1723 | prime_atom0(Id,Primed) :- atom_concat(Id,'$0',Primed). | |
1724 | ||
1725 | ||
1726 | % allow access to abstract variables by removing all "error/1" | |
1727 | % information from identifiers in the environment which also | |
1728 | % carry the "abstraction" information | |
1729 | allow_access_to_abstract_vars(OldEnv,NewEnv) :- | |
1730 | env_transform_infos(OldEnv,_,OldInfos,NewInfos,NewEnv), | |
1731 | maplist(allow_access_to_abstract_var,OldInfos,NewInfos). | |
1732 | % Iterate over the information list | |
1733 | allow_access_to_abstract_var(OldInfo,NewInfo) :- | |
1734 | % abstract variable where no access is permitted | |
1735 | ? | member(abstraction,OldInfo), |
1736 | % remove the error flag | |
1737 | ? | select(error(_),OldInfo,NewInfo),!. % requires that visibility/5 in bmachine_construction adds error field |
1738 | allow_access_to_abstract_var(Info,Info). | |
1739 | ||
1740 | % for each local concrete_variable, add a variable x$0 of the same | |
1741 | % type to the scope. (Needed in while loop invariants) | |
1742 | % TODO: This is not completely correct. The variable should only be added | |
1743 | % if there is an abstract variable of the same name. | |
1744 | add_primed_old_value_variables(InvEnv,PInvEnv) :- | |
1745 | env_transform_infos(InvEnv,Ids,Infos,_,_), | |
1746 | foldl(add_primed_old_value_variable,Ids,Infos,InvEnv,PInvEnv). | |
1747 | add_primed_old_value_variable(Id,Info,In,Out) :- | |
1748 | % We add a primed version if it is a concrete variable declared in this machine | |
1749 | Id \= op(_), | |
1750 | memberchk(loc(Loc,_,Sec),Info), | |
1751 | (Loc=local ; Loc=included), % included seems to be used for IMPORTS | |
1752 | memberchk(Sec,[concrete_variables,abstract_variables]),!, | |
1753 | atom_concat(Id,'$0',Primed), | |
1754 | env_lookup_type(Id,In,Type), | |
1755 | env_store(Primed,Type,[refers_to_old_state(Id)],In,Out). | |
1756 | add_primed_old_value_variable(_Id,_Info,Env,Env). | |
1757 | ||
1758 | % check if a reference to the original value of a variable is made. | |
1759 | % This is only possible in the loop invariant of a while statement | |
1760 | % The reference to an original value is an identifier marked with an refers_to_old_state(Id) tag, | |
1761 | % see add_primed_old_value_variables/2 above. | |
1762 | check_for_old_state_references(TExpr,Info) :- | |
1763 | check_for_old_state_references2(TExpr,Refs,[]), | |
1764 | sort(Refs,SortedRefs), | |
1765 | ( SortedRefs = [] -> Info = [] | |
1766 | ; SortedRefs = [_|_] -> Info = [refers_to_old_state(SortedRefs)]). | |
1767 | check_for_old_state_references2(TExpr) --> | |
1768 | { syntaxtraversion(TExpr,Expr,Type,Infos,Subs,_) }, | |
1769 | check_for_old_state_references3(Expr,Type,Infos), | |
1770 | foldl(check_for_old_state_references2,Subs). | |
1771 | check_for_old_state_references3(identifier(Id),Type,Infos) --> | |
1772 | {memberchk(refers_to_old_state(OrigId),Infos),!}, [oref(Id,OrigId,Type)]. | |
1773 | check_for_old_state_references3(_Expr,_Type,_Infos) --> !. | |
1774 | ||
1775 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
1776 | % error handling | |
1777 | store_typecheck_error(Msg,Pos,TRin,TRout) :- | |
1778 | update_position(Pos,NewPos), | |
1779 | (typecheck_result_add_error(error(Msg,NewPos),TRin,TRout) -> true | |
1780 | ; add_internal_error('Could not store typecheck error: ', Msg), | |
1781 | TRin=TRout). | |
1782 | store_typecheck_warning(Msg,Pos,TRin,TRout) :- | |
1783 | update_position(Pos,NewPos), | |
1784 | (typecheck_result_add_error(warning(Msg,NewPos),TRin,TRout) -> true | |
1785 | ; add_internal_error('Could not store typecheck warning: ', Msg), | |
1786 | TRin=TRout). | |
1787 | ||
1788 | % update position for Rodin, as only top-level predicates/expressions have position infos | |
1789 | update_position(none,NewPos) :- bb_get(typecheck_rodin_error_context,RPos),!, NewPos=RPos. | |
1790 | update_position(P,P). | |
1791 | ||
1792 | %set_rodin_typecheck_position_context(rodinpos(M,Label,I)) :- | |
1793 | % bb_put(typecheck_rodin_error_context,rodinpos(M,Label,I)). | |
1794 | ||
1795 | set_typecheck_position_context(Pos) :- bb_put(typecheck_rodin_error_context,Pos). | |
1796 | reset_typecheck_position_context :- (bb_delete(typecheck_rodin_error_context,_) -> true ; true). | |
1797 | ||
1798 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
1799 | % type unification | |
1800 | ||
1801 | unify_types_werrors_l(A,B,Pos,Context,Ein,Eout) :- | |
1802 | typecheck_result_init(Ein,[],[],TRStart), | |
1803 | unify_types_l(A,B,Pos,Context,TRStart,TR), | |
1804 | typecheck_result_get_errors(TR,Eout), | |
1805 | typecheck_result_get_delayed_rules(TR,[]), | |
1806 | typecheck_result_get_identifiers(TR,[]). | |
1807 | ||
1808 | unify_types_werrors(A,B,Pos,Context) :- | |
1809 | unify_types_werrors(A,B,Pos,Context,Errors,[]), | |
1810 | (Errors = [] -> true ; add_all_perrors(Errors),fail). | |
1811 | unify_types_werrors(A,B,Pos,Context,Ein,Eout) :- | |
1812 | unify_types_werrors_l([A],[B],[Pos],Context,Ein,Eout). | |
1813 | ||
1814 | %unify_types_l(A,B,Pos) --> | |
1815 | % unify_types_l_aux(A,B,Pos,no_expression,1). | |
1816 | unify_types_l(A,B,Pos,ContextExpr) --> | |
1817 | unify_types_l_aux(A,B,Pos,ContextExpr,1). | |
1818 | ||
1819 | unify_types_l_aux([],[],[],_,_,TR,TR). | |
1820 | unify_types_l_aux([A|Arest],[B|Brest],[Pos|Prest],ContextExpr,Nr,TRin,TRout) :- | |
1821 | unify_types(A,B,Pos,argument_of(Nr,ContextExpr),TRin,TR1), | |
1822 | N1 is Nr+1, | |
1823 | unify_types_l_aux(Arest,Brest,Prest,ContextExpr,N1,TR1,TRout). | |
1824 | ||
1825 | ||
1826 | ||
1827 | unify_types(A,B,_,_,TR,TR) :- | |
1828 | unify_types_strict(A,B),!. | |
1829 | unify_types(A,B,Pos,Expr,TRin,TRout) :- | |
1830 | unify_failed(A,B,Pos,Expr,TRin,TRout). | |
1831 | ||
1832 | unify_failed(A,B,Pos,ContextExpr,TRin,TRout) :- | |
1833 | ( nonvar(ContextExpr), | |
1834 | ContextExpr\=no_expression, | |
1835 | my_translate(ContextExpr,ExprString) % calling predicate with unwrapped AST | |
1836 | -> | |
1837 | TailMsg = [' in \'', ExprString, '\''] | |
1838 | ; TailMsg = []), | |
1839 | unify_failed_msg(A,B,MsgList,TailMsg), | |
1840 | ajoin(MsgList,Msg), | |
1841 | store_typecheck_error(Msg,Pos,TRin,TRout). | |
1842 | ||
1843 | % translate some special context expressions for better error reporting; in particular for Rodin models | |
1844 | my_translate(argument_of(3,BinOp),Res) :- BinOp='*', !, | |
1845 | Res = 'result of *'. | |
1846 | my_translate(argument_of(Nr,Expr),Res) :- !, my_translate(Expr,TE), | |
1847 | ajoin(['argument ',Nr,' of ',TE],Res). | |
1848 | my_translate(no_expression,Res) :- !,Res='?'. | |
1849 | my_translate(Atom,Res) :- atom(Atom), \+ is_syntax_constant(Atom), | |
1850 | !, % avoid **** Unknown functor message | |
1851 | Res=Atom. | |
1852 | my_translate(Expr,ExprString) :- translate_bexpression(Expr,ExprString). | |
1853 | ||
1854 | unify_failed_msg(A,B,MsgList,Rest) :- | |
1855 | match_instance(A,record([field(Field,_)|_])), | |
1856 | match_instance(B,record(Fields)), | |
1857 | get_field_names(Fields,Names), | |
1858 | nonmember(Field,Names), | |
1859 | !, | |
1860 | ajoin_with_sep(Names,',',NL), | |
1861 | MsgList = ['Type mismatch: Expected record with field ', Field, ', but had only fields {',NL,'}'|Rest]. | |
1862 | unify_failed_msg(A,B,['Type mismatch: Expected ', PA, ', but was ', PB|Rest0],Rest) :- | |
1863 | % TO DO: provide better user-feedback | |
1864 | pretty_type(A,PA), pretty_type(B,PB), | |
1865 | (A=integer, B = real, % TODO: cover more cases where REAL occurs deeper in type | |
1866 | \+ allow_to_use_real_types | |
1867 | -> Rest0 = [' (set ALLOW_REALS preference to TRUE to enable using reals)' |Rest] | |
1868 | ; Rest=Rest0). | |
1869 | ||
1870 | get_field_names(V,_) :- var(V),!,fail. | |
1871 | get_field_names([],[]). | |
1872 | get_field_names([H|T],[FH|FT]) :- get_field_name(H,FH), get_field_names(T,FT). | |
1873 | get_field_name(F,Field) :- nonvar(F),F=field(Field,_). | |
1874 | match_instance(V,Pat) :- var(Pat),!,Pat=V. | |
1875 | match_instance(V,_Pat) :- var(V),!,fail. | |
1876 | match_instance(F,Pat) :- nonvar(F), functor(F,N,A), functor(Pat,N,A), | |
1877 | (A>0 -> F=..FL, Pat =.. PL, maplist(match_instance,FL,PL) ; true). | |
1878 | ||
1879 | %unify_failed(record([field(b,_54661)|_54843]),record([field(a,integer)]),pos(11,-1,1,18,1,20),b(identifier(r),record([field(a,integer)]),[nodeid(pos(12,-1,1,18,1,18))]),tr(_51997,_53271,_53273,[]),_54857) | |
1880 | ||
1881 | :- assert_must_succeed(( btypechecker:unify_types_strict(set(couple(boolean,string)), set(couple(boolean,string))) )). | |
1882 | :- assert_must_succeed(( btypechecker:unify_types_strict(seq(integer), set(couple(integer,integer))) )). | |
1883 | :- assert_must_succeed(( btypechecker:unify_types_strict(seq(set(couple(integer,integer))), | |
1884 | set(couple(integer,seq(integer)))) )). | |
1885 | :- assert_must_succeed(( btypechecker:unify_types_strict(seq(integer), any) )). | |
1886 | :- assert_must_succeed(( btypechecker:unify_types_strict(any, set(couple(integer,integer))) )). | |
1887 | :- assert_must_succeed(( btypechecker:unify_types_strict(_X, set(couple(integer,integer))) )). | |
1888 | :- assert_must_succeed(( btypechecker:unify_types_strict(seq(any), set(couple(integer,boolean))) )). | |
1889 | ||
1890 | unify_types_strict(A,B) :- | |
1891 | ( var(A) -> | |
1892 | (var(B) -> A=B ; unify_types1(B,A)) | |
1893 | ; | |
1894 | unify_types1(A,B) | |
1895 | ),!. | |
1896 | ||
1897 | unify_types1(A,B) :- var(B),contains_var(B,A),!,fail. | |
1898 | unify_types1(A,B) :- unify_types2(A,B). | |
1899 | ||
1900 | unify_types2(any,B) :- !, | |
1901 | (var(B) -> B=any | |
1902 | ; true). % TO DO: set inner variables to any ? | |
1903 | unify_types2(_,B) :- B==any, !. % Maybe these two cases should be removed and type errors generated | |
1904 | % where the type cannot be inferred | |
1905 | unify_types2(set(A),set(B)) :- !, unify_types_strict(A,B). | |
1906 | unify_types2(seq(A),seq(B)) :- !, unify_types_strict(A,B). | |
1907 | unify_types2(set(A),seq(B)) :- !, unify_types_strict(seq(B),set(A)). | |
1908 | unify_types2(seq(A),set(B)) :- !, unify_types_strict(couple(integer,A),B). | |
1909 | unify_types2(couple(A,B),couple(X,Y)) :- !,unify_types_strict(A,X),unify_types_strict(B,Y). | |
1910 | unify_types2(string,string). | |
1911 | unify_types2(integer,integer). | |
1912 | unify_types2(real,real). | |
1913 | unify_types2(boolean,boolean). | |
1914 | unify_types2(global(G),global(G)). | |
1915 | unify_types2(pred,pred). | |
1916 | unify_types2(subst,subst). | |
1917 | unify_types2(record(A),record(B)) :- !, unify_fields(B,A). | |
1918 | unify_types2(rec(A),_) :- !, add_internal_error('Use record(.) as type:',unify_types2(rec(A),_)),fail. | |
1919 | unify_types2(op(ParamsA,ResultsA),op(ParamsB,ResultsB)) :- | |
1920 | l_unify_types_strict(ParamsA,ParamsB), | |
1921 | l_unify_types_strict(ResultsA,ResultsB). | |
1922 | unify_types2(freetype(Name),freetype(Name)). | |
1923 | unify_types2(freetype(Name,TypeParams1),freetype(Name,TypeParams2)) :- | |
1924 | l_unify_types_strict(TypeParams1,TypeParams2). | |
1925 | unify_types2(witness,witness). | |
1926 | unify_types2(status,status). | |
1927 | ||
1928 | % unify_types_strict for a list of types | |
1929 | l_unify_types_strict(A,B) :- var(A),!,A=B. | |
1930 | l_unify_types_strict([],B) :- !, B=[]. | |
1931 | l_unify_types_strict([T1|Rest1],[T2|Rest2]) :- | |
1932 | unify_types_strict(T1,T2), | |
1933 | l_unify_types_strict(Rest1,Rest2). | |
1934 | ||
1935 | unify_fields(Sub,Super) :- | |
1936 | nonvar(Sub),nonvar(Super),!, | |
1937 | ( Sub = [field(Name,Type)|SubRest] -> | |
1938 | extract_field(Super,Name,Type,SuperRest), | |
1939 | unify_fields(SubRest,SuperRest) | |
1940 | ; Sub = [] -> | |
1941 | Super = [] | |
1942 | ; add_internal_error('Illegal type: ',unify_fields(Sub,Super)),fail | |
1943 | ). | |
1944 | unify_fields(Fields,Fields). | |
1945 | ||
1946 | extract_field(L,Name,Type,Rest) :- | |
1947 | extract_field2(L,Name,Type,Rest). | |
1948 | extract_field2(L,Name,Type,Rest) :- nonvar(L),!, | |
1949 | L = [field(FName,FType)|LRest], | |
1950 | ( Name = FName -> | |
1951 | unify_types_strict(Type,FType), | |
1952 | Rest=LRest | |
1953 | ; | |
1954 | Rest=[field(FName,FType)|NRest], | |
1955 | extract_field2(LRest,Name,Type,NRest)). | |
1956 | extract_field2(L,Name,Type,LRest) :- | |
1957 | L = [field(Name,Type)|LRest]. | |
1958 | ||
1959 | % a special rule that checks whether a given record with name Id matches an expected type in a Field List | |
1960 | % used for record_field accesses | |
1961 | check_field_type(Fields,Id,Type,Pos,Trin,TRout) :- | |
1962 | %when(nonvar(Fields), (Fields==[] -> print(empty_rec(Id,Pos)),nl,trace ; true)), | |
1963 | typecheck_result_add_delayed_rule(Trigger,Errors,Trin,TRout), | |
1964 | delayed_check_field_type(Fields,Fields,Id,Type,Pos,Trigger,Errors). | |
1965 | ||
1966 | :- block delayed_check_field_type(-,?,?,?,?,-,?). | |
1967 | delayed_check_field_type(Fields,_,Id,FType,Pos,Trigger,Errors) :- var(Fields),!, | |
1968 | ajoin(['Could not determine type for record field access ',Id],Msg), | |
1969 | % This could be disabled for typechecking definitions | |
1970 | (get_preference(allow_untyped_identifiers,true_with_string_type) % we are type-checking definitions | |
1971 | -> (debug_mode(on) -> add_message(btypechecker,Msg,'',Pos) ; true), | |
1972 | Fields = [field(Id,FType)|_], Errors=[] | |
1973 | ; delay_add_errors(Trigger,Errors,[error(Msg,Pos)]) | |
1974 | ). | |
1975 | delayed_check_field_type([],AllFields,Id,_Type,Pos,Trigger,Errors) :- | |
1976 | maplist(get_field_id,AllFields,AllIds), sort(AllIds,SAI), | |
1977 | (fuzzy_find_possible_ids(Id,ids(SAI),AlternativeIds,_Len) | |
1978 | -> wrap_ids_in_quotes(AlternativeIds,WIds), | |
1979 | ajoin(['Unknown field "',Id,'" for record field access, did you mean one of: '|WIds],Msg) | |
1980 | ; wrap_ids_in_quotes(SAI,WIds), | |
1981 | ajoin(['Unknown field "',Id,'" for record field access, must be one of: '|WIds],Msg) | |
1982 | ), | |
1983 | delay_add_errors(Trigger,Errors,[error(Msg,Pos)]). | |
1984 | delayed_check_field_type([field(Id,FType)|_],_AllFields,Id,Type,Pos,Trigger,Errors) :- !, | |
1985 | (unify_types_strict(FType,Type) -> Errors=[] | |
1986 | ; unify_failed_msg(Type,FType,MsgList,[' for record field access ',Id]), | |
1987 | ajoin(MsgList,Msg), | |
1988 | delay_add_errors(Trigger,Errors,[error(Msg,Pos)])). | |
1989 | delayed_check_field_type([_|TF],AllFields,Id,Type,Pos,Trigger,Errors) :- | |
1990 | delayed_check_field_type(TF,AllFields,Id,Type,Pos,Trigger,Errors). | |
1991 | ||
1992 | % add errors when the delayed rule trigger is activated | |
1993 | :- block delay_add_errors(-,?,?). | |
1994 | delay_add_errors(_,Errors,Errors). | |
1995 | ||
1996 | get_field_id(field(Id,_),Id). | |
1997 | ||
1998 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
1999 | % check if all types of the variables are ground | |
2000 | check_ground_types_dl(TExprs,Exceptions,Ein,Eout) :- %print(check_ground(TExprs)),nl, | |
2001 | foldl(check_ground_type_dl(Exceptions),TExprs,Ein,Eout). | |
2002 | check_ground_type_dl(Exceptions,TExpr,Ein,Eout) :- | |
2003 | get_texpr_type(TExpr,Type), | |
2004 | ( is_ground_type(Exceptions,Type) -> | |
2005 | Ein=Eout | |
2006 | % TO DO allow polymorphic typing, without any instantiation | |
2007 | ; | |
2008 | % (ground(Type) -> true ; format('Not ground, exceptions = ~w~n~w~n~n',[Exceptions,Type])), | |
2009 | get_texpr_expr(TExpr,identifier(Id)), | |
2010 | ( \+ get_preference(allow_untyped_identifiers,false), | |
2011 | instantiate_non_ground_type(Exceptions,Type) | |
2012 | -> translate:pretty_type(Type,TS), | |
2013 | debug_format(20,'% Instantiated type of ~w to ~w~n',[Id,TS]), | |
2014 | Ein=Eout | |
2015 | ; get_texpr_pos(TExpr,Pos), | |
2016 | ajoin(['Could not infer type of ',Id], Msg), | |
2017 | Ein=[error(Msg,Pos)|Eout] | |
2018 | ) | |
2019 | ). | |
2020 | is_ground_type(_Exceptions,Type) :- ground(Type),!. | |
2021 | is_ground_type(Exceptions,Type) :- var(Type),!,exact_member(Type,Exceptions). | |
2022 | is_ground_type(Exceptions,Type) :- | |
2023 | Type =.. [_|TArgs], | |
2024 | maplist(is_ground_type(Exceptions),TArgs). | |
2025 | ||
2026 | :- use_module(b_global_sets,[generate_fresh_supplementary_global_set/1]). | |
2027 | instantiate_non_ground_type(_Exceptions,Type) :- ground(Type),!. | |
2028 | instantiate_non_ground_type(Exceptions,Type) :- var(Type),!, | |
2029 | (exact_member(Type,Exceptions) -> true | |
2030 | ; get_preference(allow_untyped_identifiers,true_with_string_type) -> | |
2031 | Type = string | |
2032 | ; % if preference set to true we allow those untyped vars and use new deferred sets for them | |
2033 | generate_fresh_supplementary_global_set(GS), | |
2034 | Type = global(GS) | |
2035 | ). | |
2036 | instantiate_non_ground_type(Exceptions,record(Fields)) :- !, | |
2037 | inst_non_ground_type_fields(Exceptions,Fields). | |
2038 | instantiate_non_ground_type(Exceptions,Type) :- | |
2039 | Type =.. [_|TArgs], | |
2040 | maplist(instantiate_non_ground_type(Exceptions),TArgs). | |
2041 | ||
2042 | inst_non_ground_type_fields(_,Type) :- var(Type),!, Type=[]. % empty record | |
2043 | inst_non_ground_type_fields(Exceptions,[field(_,Type)|TF]) :- | |
2044 | instantiate_non_ground_type(Exceptions,Type), | |
2045 | inst_non_ground_type_fields(Exceptions,TF). | |
2046 | ||
2047 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
2048 | % rewrite rules to clean up the syntax tree | |
2049 | ||
2050 | % substitute definitions | |
2051 | btype_rewrite(RawExpr,Env,Pos,Result,NewPos) :- | |
2052 | is_definition_call(RawExpr,Env),!, | |
2053 | rewrite_definition(RawExpr,Pos,Env,Result,NewPos). | |
2054 | % transform operation calls inside expressions | |
2055 | btype_rewrite(function(Fun,Args),Env,Pos,Result,Pos) :- % function is also rewritten in btype_rewrite2 | |
2056 | %print(fun(Fun)),nl, portray_env(Env), | |
2057 | (preference(allow_operation_calls_in_expr,true), % detect operation calls with arguments | |
2058 | is_operation_call(Fun,Env) | |
2059 | -> Result = operation_call_in_expr(Fun,Args) | |
2060 | ; Fun = identifier(_,Id), | |
2061 | ? | is_eventb_operator(Id,Env), |
2062 | \+ try_get_operator_arity(Id,0) % operator is a constant (e.g. a lambda function); we need to rewrite Id below | |
2063 | -> debug_format(19,'Rewrite function application of ~w to operator call~n',[Id]), | |
2064 | Result = extended_formula(Id,Args,[]) % we don't know if it is expr or pred | |
2065 | ),!. | |
2066 | % other (not definition-related) rules | |
2067 | btype_rewrite(identifier(Op),Env,Pos,Result,Pos) :- !, % identifiers are not rewritten in btype_rewrite2 | |
2068 | (preference(allow_operation_calls_in_expr,true), % detect operation calls without arguments | |
2069 | lookup_operation_name(Op,Env,_ArgTypes,_ResTypes) | |
2070 | %ArgTypes=[], % if ArgTypes \= [] we get add_operation_call_error later in typechecker | |
2071 | % we could check if ResTypes are \= [] | |
2072 | -> Result = operation_call_in_expr(identifier(Pos,Op),[]) | |
2073 | ? | ; is_eventb_operator(Op,Env) |
2074 | -> Result = extended_formula(Op,[],[])). % we don't know if it is expr or pred | |
2075 | btype_rewrite(multiline_template(TS),_Env,Pos,Result,Pos) :- | |
2076 | debug_format(19,'Parsing template: `~w`~n',[TS]), | |
2077 | atom_codes(TS,Codes), | |
2078 | ? | (transform_string_template(Codes,Pos,RawExpr) |
2079 | -> remove_pos(RawExpr,Result) | |
2080 | ; Result = string(TS)). | |
2081 | btype_rewrite(Expr,_Env,Pos,New,Pos) :- btype_rewrite2(Expr,Pos,New). | |
2082 | ||
2083 | ||
2084 | :- use_module(bmachine_eventb,[stored_operator_direct_definition/8]). | |
2085 | try_get_operator_arity(Id,Arity) :- | |
2086 | stored_operator_direct_definition(Id,_Proj,_Thy,Parameters,_Def,_WD,_TP,_Kind), | |
2087 | length(Parameters,Arity). | |
2088 | % if nothing stored: todo use get_operator_arity_from_callback | |
2089 | ||
2090 | % this check below is only necessary when we use the SableCC parser, wich does not know | |
2091 | % about operators and does not generate extended_expr or extended_pred nodes but | |
2092 | % identifier/1 and function/2 nodes | |
2093 | is_eventb_operator(Id,Env) :- | |
2094 | ? | eventb_mode, % we could check if we are in REPL or VisB |
2095 | env_lookup_operator(Id,Env), % this is an operator, OpType always boolean !! | |
2096 | \+ env_check_identifier_defined(Id,Env). % there is no local definition overriding it; not sure we need this check | |
2097 | ||
2098 | env_lookup_operator(Id,openenv(_,Env)) :- !, % operators cannot be introduced by exists and hence cannot be in openenv | |
2099 | env_lookup_operator(Id,Env). | |
2100 | env_lookup_operator(Id,Env) :- env_lookup_type(operator(Id),Env,_OpType). | |
2101 | ||
2102 | is_operation_call(identifier(_,Name),Env) :- lookup_operation_name(Name,Env,_,_). | |
2103 | % lookup OPERATION with Name in Environment Env | |
2104 | lookup_operation_name(Name,Env,ArgTypes1,ResTypes1) :- | |
2105 | env_lookup_type(op(Name),Env,Type), nonvar(Type), | |
2106 | Type = op(ArgTypes1,ResTypes1), | |
2107 | % Now check if we do not have a regular id in scope; relevant for e.g. test 1873, 1953 | |
2108 | \+ env_id_exists(Name,Env). % relevant for test 1953; env_lookup_type always succeeds with open_env, e.g., in REPL | |
2109 | ||
2110 | env_id_exists(Id,Env) :- env_identifiers(Env,Ids), | |
2111 | ord_member(Id,Ids). | |
2112 | ||
2113 | % a shorter version of the | |
2114 | is_definition_call(identifier(Name),Env) :- | |
2115 | lookup_definition(Name,Env,_,_Params,_Body). | |
2116 | is_definition_call(function(DefIdP,_Args),Env) :- | |
2117 | remove_pos(DefIdP,identifier(Name)), | |
2118 | % the definition should have parameters, if not, it could be | |
2119 | % that a function is defined and normal function application is | |
2120 | % needed | |
2121 | % Note: There is a rewrite rule for functions that converts a list | |
2122 | % of arguments into couples. That rewrite rule must not be called | |
2123 | % before this rule. | |
2124 | Params = [_|_], % only applicable if the Definition also takes parameters | |
2125 | lookup_definition(Name,Env,_,Params,_Body). | |
2126 | is_definition_call(definition(_Name,_Args),_Env). | |
2127 | ||
2128 | rewrite_definition(identifier(Name),Pos,Env,Result,NewPos) :- | |
2129 | rewrite_definition2(Name,[],Pos,Env,Result,NewPos). | |
2130 | rewrite_definition(function(DefIdP,Args),Pos,Env,Result,NewPos) :- | |
2131 | % A function application where the function is an identifier | |
2132 | % may be a definition with arguments | |
2133 | remove_pos(DefIdP,identifier(Name)), | |
2134 | rewrite_definition2(Name,Args,Pos,Env,Result,NewPos). | |
2135 | rewrite_definition(definition(Name,Args),Pos,Env,Result,NewPos) :- | |
2136 | % the standard way of using a definition | |
2137 | rewrite_definition2(Name,Args,Pos,Env,Result,NewPos). | |
2138 | ||
2139 | rewrite_definition2(Name,Args,CallPos,Env,Result,NewPos) :- | |
2140 | ( lookup_definition(Name,Env,DefType,FormalParams,Body) -> | |
2141 | (btype_rewrite_definition(DefType,FormalParams,Name,CallPos,Env,Args,Body,NewBody) | |
2142 | -> % add context_pos infos | |
2143 | add_raw_ast_pos_info_context(definition_call(Name),CallPos,NewBody,NewBody1), | |
2144 | % TODO: keep track of actual arguments Args for call_stack | |
2145 | remove_pos(NewBody1,Result,NewPos) % remove position info | |
2146 | %,print(def_rewrote(Name,CallPos,Args)),nl,print(Result),nl | |
2147 | ; add_internal_error('Rewriting definition failed: ',Name),fail | |
2148 | ) | |
2149 | ; env_lookup_type(Name,Env,Type) -> | |
2150 | ajoin(['Definition ',Name,' has been overriden by identifier of type ',Type],ErrMsg), | |
2151 | % we could try and rewrite the definition call into the local no-longer accessible DEFINITION | |
2152 | % but maybe it is safer to always give an error; | |
2153 | % this case here can happen in VisB when VisB defs override B DEFINITIONS | |
2154 | throw(rewrite_exception(ErrMsg,Name)) | |
2155 | ; | |
2156 | ajoin(['Definition ',Name,' not found'],ErrMsg), | |
2157 | throw(rewrite_exception(ErrMsg,Name)) | |
2158 | ). | |
2159 | ||
2160 | btype_rewrite_definition(_DefType,Params,Name,CallPos,Env,Args,Body,NewBody) :- | |
2161 | ( same_length(Params,Args) -> | |
2162 | b_rewrite_def_aux(Params,Name,CallPos,Env,Args,Body,NewBody) | |
2163 | ; | |
2164 | length(Params,ExpectedPNr),length(Args,AN), | |
2165 | (AN=0 | |
2166 | -> ajoin(['Expected ',ExpectedPNr,' arguments for definition ',Name],ErrMsg), | |
2167 | % this happens when we provide more than ExpectedPNr arguments; | |
2168 | % the parser seems to translate this into a definition call with 0 args and then a function call | |
2169 | throw(rewrite_exception(ErrMsg,Name)) | |
2170 | ; AN=1, Args=[Arg1], | |
2171 | eventb_mode, % allow maplet notation to call definitions | |
2172 | % (probably automatically promoted definitions from external_function_declarations) | |
2173 | decompose_couples(Arg1,ExpectedPNr,CArgs,[]) | |
2174 | -> b_rewrite_def_aux(Params,Name,CallPos,Env,CArgs,Body,NewBody) | |
2175 | ; ajoin(['Expected ',ExpectedPNr,' instead of ',AN,' arguments for definition ',Name],ErrMsg), | |
2176 | throw(rewrite_exception(ErrMsg,Name)) | |
2177 | ) | |
2178 | ). | |
2179 | ||
2180 | % in context of Event-B function calls must be written using maplets/couple notation | |
2181 | decompose_couples(couple(_,[Arg1,Arg2]),NrParas) --> | |
2182 | {NrParas>1, P1 is NrParas-1},!,decompose_couples(Arg1,P1), [Arg2]. | |
2183 | decompose_couples(X,1) --> [X]. | |
2184 | ||
2185 | b_rewrite_def_aux(Params,Name,CallPos,Env,Args,Body,NewBody) :- | |
2186 | check_def_body_capture(Name,CallPos,Body,Env), | |
2187 | maplist(definition_expansion_on_raw_def_paras_with_pos(Env),Args,NewArgs), | |
2188 | maplist(create_def_replace(Name),Params,NewArgs,Replaces), | |
2189 | %% replacing DEFINITION parameters by actual arguments | |
2190 | %% THIS CAN LEAD TO DUPLICATION of computation ! | |
2191 | %% TO DO: try and introduce let_expression,... (or use CSE later); problem: we are not yet in a typed context here; we may not always know whether this is a predicate, expression or substitution !? | |
2192 | %% print(old_body(Name,Body,replaces(Replaces))),nl, | |
2193 | raw_replace(Body,Replaces,NewBody). %% ,print(replaced_def(Name,NewBody)),nl %% | |
2194 | %%TODO: keep track of original position as well | |
2195 | ||
2196 | create_def_replace(_,identifier(_,Old),New,Res) :- !, Res=replace(Old,New). | |
2197 | create_def_replace(Name,Term,_,_) :- (Term=definition(_Pos,Old,_) -> true ; Old=''), | |
2198 | ajoin(['Cannot apply definition ',Name,', formal parameter ',Old, ' is not an identifier'],ErrMsg), | |
2199 | throw(rewrite_exception(ErrMsg,Name)). | |
2200 | % lookup DEFINITION with Name in Environment Env | |
2201 | lookup_definition(Name,Env,DefType,Params,Body) :- | |
2202 | env_lookup_type(Name,Env,Type), nonvar(Type), | |
2203 | Type = definition(DefType,Params,Body). | |
2204 | ||
2205 | :- use_module(input_syntax_tree,[extract_raw_identifiers/2]). | |
2206 | :- use_module(translate,[translate_span_with_filename/2]). | |
2207 | % check for potential variable captures | |
2208 | check_def_body_capture(Name,CallPos,Body,Env) :- | |
2209 | extract_raw_identifiers(Body,Ids), | |
2210 | ? | member(Id,Ids), %format('Checking for capture in call of ~w of ids ~w~n',[Name,Ids]), portray_env(Env),nl, |
2211 | env_lookup_infos(Id,Env,Infos), memberchk(duplicate_id_hides(HiddenInfos),Infos), | |
2212 | translate_span_with_filename(HiddenInfos,OuterPosStr), | |
2213 | translate_span_with_filename(Infos,PosStr), | |
2214 | ajoin(['Possible variable capture, identifier ',Id,' ',OuterPosStr,' is hidden by ',Id,' ',PosStr,' in DEFINITION call of: '],Msg), | |
2215 | add_warning(definition_variable_capture,Msg,Name,CallPos), | |
2216 | fail. | |
2217 | check_def_body_capture(_,_,_,_). | |
2218 | ||
2219 | ||
2220 | % expressions | |
2221 | btype_rewrite2(couple([A,B]),_,couple(A,B)) :- !. | |
2222 | btype_rewrite2(couple(Elements),Pos,couple(X,Y)) :- couplise_list_pos(Elements,Pos,couple(_,X,Y)). | |
2223 | btype_rewrite2(function(Fun,Args),Pos,function(Fun,Arg)) :- | |
2224 | couplise_list_pos(Args,Pos,Arg). | |
2225 | ||
2226 | % substitutions and operations | |
2227 | btype_rewrite2(if(Pred,Subst,Elsifs,Else),Pos,if(IfList)) :- | |
2228 | (Else=skip(_) -> IfList = [if_elsif(Pos,Pred,Subst)|Elsifs] | |
2229 | ; append([if_elsif(Pos,Pred,Subst)|Elsifs],[if_elsif(none,truth(none),Else)],IfList)). | |
2230 | btype_rewrite2(case(Expr,Either,EitherSubst,Ors,Else),Pos, | |
2231 | case(Expr,[case_or(Pos,Either,EitherSubst)|Ors],Else)). | |
2232 | btype_rewrite2(select(Pred,Then,Whens,Else),Pos,select([select_when(Pos,Pred,Then)|Whens],Else)). | |
2233 | btype_rewrite2(select(Pred,Then,Whens),Pos,select([select_when(Pos,Pred,Then)|Whens])). | |
2234 | btype_rewrite2(choice([]),_,choice([])). | |
2235 | btype_rewrite2(choice(Options),_,choice(Substs)) :- | |
2236 | remove_choice_ors(Options,Substs). | |
2237 | ||
2238 | % integer sets | |
2239 | btype_rewrite2(integer_set,_,integer_set('INTEGER')). | |
2240 | btype_rewrite2(natural_set,_,integer_set('NATURAL')). | |
2241 | btype_rewrite2(natural1_set,_,integer_set('NATURAL1')). | |
2242 | btype_rewrite2(nat_set,_,integer_set('NAT')). | |
2243 | btype_rewrite2(nat1_set,_,integer_set('NAT1')). | |
2244 | btype_rewrite2(int_set,_,integer_set('INT')). | |
2245 | ||
2246 | % applying rewriting of definitions on the raw (un-typed input) syntax tree | |
2247 | % this is used for parameters of definitions (which do not have their own position info) | |
2248 | definition_expansion_on_raw_def_paras_with_pos(Env,RawExprPos,OutAst) :- | |
2249 | compound(RawExprPos),ext2int(RawExprPos,RawExpr,Pos,_,_,_,_),!, | |
2250 | definition_expansion_on_compound_para(Pos,Env,RawExpr,NewPos,OutAst1), | |
2251 | OutAst1 =.. [Functor|Args], OutAst =.. [Functor,NewPos|Args]. | |
2252 | definition_expansion_on_raw_def_paras_with_pos(_Env,Ast,Ast). | |
2253 | definition_expansion_on_compound_para(Pos,Env,RawExpr,NewPos2,OutAst) :- | |
2254 | is_definition_call(RawExpr,Env),!, % definition all within parameters of a definition | |
2255 | rewrite_definition(RawExpr,Pos,Env,InterAst,NewPos), | |
2256 | definition_expansion_on_compound_para(NewPos,Env,InterAst,NewPos2,OutAst). | |
2257 | definition_expansion_on_compound_para(Pos,Env,InAst,Pos,OutAst) :- | |
2258 | compound(InAst), | |
2259 | InAst =.. [Functor|Args],!, | |
2260 | same_functor(InAst,OutAst), | |
2261 | OutAst =.. [Functor|NewArgs], | |
2262 | maplist(definition_expansion_on_raw_def_paras_with_pos(Env),Args,NewArgs). | |
2263 | definition_expansion_on_compound_para(Pos,_Env,Ast,Pos,Ast). | |
2264 | ||
2265 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
2266 | % extract syntax tree positions | |
2267 | ||
2268 | remove_pos(Ext,Expr,Pos) :- | |
2269 | ext2int(removepos,Ext,Expr,Pos,_,_,_,_). | |
2270 | remove_pos(Ext,Expr) :- | |
2271 | ext2int(removepos,Ext,Expr,_,_,_,_,_). | |
2272 | ||
2273 | % create a enhanced syntax element from a raw input | |
2274 | % ext2int(+Ext,-Expr,-Pos,+Type,+TExpr,+RestInfos,-Result): | |
2275 | % Ext: raw information with position info (from parser) | |
2276 | % Expr: the underlying expression without position info (e.g. identifier(x)) | |
2277 | % Pos: the position extracted from the raw expression | |
2278 | % Type: the type used for the typed expression | |
2279 | % TExpr: the new expression in the enhanced syntax tree format | |
2280 | % (but without the information for the root element) | |
2281 | % RestInfos: Additional list of informations that will be stored inside | |
2282 | % the element aside from the position information | |
2283 | % Result: the new completed element (with type and additional information) | |
2284 | % Example: "1+x" | |
2285 | % Ext: add(pos1,integer(pos2,1),identifier(pos3,x) | |
2286 | % Expr: add(integer(pos2,1),identifier(pos3,x)) | |
2287 | % Result: b(TExpr,Type,[nodeid(pos1)|RestInfos]) | |
2288 | ext2int(Ext,Expr,Pos,Type,TExpr,RestInfos,Res) :- | |
2289 | ext2int(unknown_src,Ext,Expr,Pos,Type,TExpr,RestInfos,Res). | |
2290 | ext2int(Src,Ext,Expr,_Pos,_Type,_TExpr,_RestInfos,_) :- | |
2291 | var(Ext),!,add_error(ext2int,'Variable Ext: ',Src:Expr,Expr),fail. | |
2292 | ext2int(_Src,Ext,Expr,Pos,Type,TExpr,RestInfos,b(TExpr,Type,ResInfos)) :- | |
2293 | % the first argument contains the position information | |
2294 | safe_functor(ext2int_ext,Ext,Functor,Arity), | |
2295 | (Arity=0 -> add_internal_error('Not raw AST:',Ext),fail ; true), | |
2296 | arg(1,Ext,ExtPos), | |
2297 | extract_optional_external_info(ExtPos,Pos0,Infos,RestInfos), | |
2298 | (number(Pos0), % happens for definitions generated by TLA2B | |
2299 | try_extract_position_backup(Ext,Pos) | |
2300 | -> true | |
2301 | ; Pos=Pos0 | |
2302 | ), | |
2303 | % now construct a copy without the first argument | |
2304 | NArity is Arity-1, | |
2305 | safe_functor(ext2int_expr,Expr,Functor,NArity), | |
2306 | (Pos==none -> ResInfos = Infos ; ResInfos = [nodeid(Pos)|Infos]), | |
2307 | copy_ext_term(Arity,Ext,Expr). | |
2308 | % It is possible to inject information into the AST from outside | |
2309 | % by using info(Pos,Info) or info(Pos,[Info1,...,InfoN]) as position | |
2310 | % Those terms are copied directly into the AST. | |
2311 | % The result is returned in form of a difference list I1-I2. | |
2312 | extract_optional_external_info(info(Pos,ExtInfo),Pos,I1,I2) :- !, | |
2313 | ( ExtInfo = [] -> I1=I2 | |
2314 | ; ExtInfo = [_|_] -> append(ExtInfo,I2,I1) | |
2315 | ; I1=[ExtInfo|I2]). | |
2316 | extract_optional_external_info(Pos,Pos,Infos,Infos). | |
2317 | ||
2318 | % try extract position from deeper in the term; TODO: fix TLA2B | |
2319 | try_extract_position_backup(definition(_,_Name,[identifier(POS,_)|_]),POS). | |
2320 | ||
2321 | copy_ext_term(1,_,_) :- !. | |
2322 | copy_ext_term(N1,Ext,Int) :- | |
2323 | N2 is N1-1, arg(N1,Ext,Arg), arg(N2,Int,Arg), | |
2324 | copy_ext_term(N2,Ext,Int). | |
2325 | ||
2326 | ||
2327 | check_for_duplicate_raw_ids([],_,_,_,[],TR,TR). | |
2328 | check_for_duplicate_raw_ids([identifier(Pos,IdName)|T],List,Construct,Name,Res,TRin,TRout) :- !, | |
2329 | %print(check(IdName,Name,Construct,List)),nl, | |
2330 | (member(IdName,List) | |
2331 | -> ajoin(['Duplicate identifier ',IdName,' for ',Construct,Name],Msg), | |
2332 | store_typecheck_error(Msg,Pos,TRin,TR2), | |
2333 | check_for_duplicate_raw_ids(T,List,Construct,Name,Res,TR2,TRout) | |
2334 | ; Res = [identifier(Pos,IdName)|ResT], | |
2335 | check_for_duplicate_raw_ids(T,[IdName|List],Construct,Name,ResT,TRin,TRout)). | |
2336 | check_for_duplicate_raw_ids([H|T],List,Construct,Name,[H|RT],TRin,TRout) :- | |
2337 | check_for_duplicate_raw_ids(T,List,Construct,Name,RT,TRin,TRout). | |
2338 | ||
2339 | % add variables to the environment | |
2340 | % - the variables are given as raw parser terms | |
2341 | % and returned in typed format | |
2342 | % - additionally the identifier is stored in the list of newly introduced | |
2343 | % identifiers | |
2344 | add_ext_variables(Identifiers, Env, TExprs, NewEnv, TRin, TRout) :- | |
2345 | add_ext_variables_with_info(Identifiers, Env, [], TExprs, NewEnv, TRin, TRout). | |
2346 | ||
2347 | add_ext_variables_with_info(Identifiers, Env, AddInfo, TExprs, NewEnv, TRin, TRout) :- | |
2348 | foldl(add_ext_variable_with_info(AddInfo), Identifiers, TExprs, TRin/Env, TRout/NewEnv). | |
2349 | add_ext_variable_with_info(AddInfo, Identifier, TExpr, TRin/Env, TRout/NewEnv) :- | |
2350 | % convert the raw format to the typed format | |
2351 | Expr = identifier(Name), | |
2352 | % Krings: in the following line, AddInfo was set to [] | |
2353 | % thus, additional information was only added to the type environment, | |
2354 | % not to the identifier itself. introduced_by was only store inside of | |
2355 | % expressions, not at the identifier declarations. this might break something? | |
2356 | ext2int(add_ext_variables_with_info,Identifier,Expr,_,Type,Expr,AddInfo1,TExpr),!, | |
2357 | (env_lookup_existing_infos(Name,Env,HiddenInfos) | |
2358 | -> AddInfo1 = [duplicate_id_hides(HiddenInfos)|AddInfo] % we hide an existing identifier; store this information | |
2359 | ; AddInfo1 = AddInfo | |
2360 | ), | |
2361 | % add the identifier's type and info to the type environment | |
2362 | get_texpr_info(TExpr,Infos), | |
2363 | env_store(Name,Type,Infos,Env,NewEnv), | |
2364 | % store the identifier in the list of newly introduced identifiers | |
2365 | typecheck_result_add_identifier(TExpr,TRin,TRout). | |
2366 | add_ext_variable_with_info(_AddInfo, Expr, TExpr, TRin/Env, TRout/Env) :- | |
2367 | % We expected an identifier but there was something different | |
2368 | ext2int(add_ext_variables_with_info,Expr,_,Pos,_,_,_,_), | |
2369 | ( translate_raw_expr_functor(Expr,TS) | |
2370 | -> ajoin(['Expected identifier, but got operator: ',TS],Msg), | |
2371 | ajoin(['not an identifier:',TS],ID) | |
2372 | ; functor(Expr,F,_), ajoin(['not an identifier:',F],ID), | |
2373 | Msg='Expected identifier' | |
2374 | ), | |
2375 | store_typecheck_error(Msg,Pos,TRin,TRout), | |
2376 | % just to make sure that there is no variable as AST element: | |
2377 | create_texpr(identifier(ID),_,[found(Expr)],TExpr). | |
2378 | ||
2379 | translate_raw_expr_functor(Expr,Translation) :- | |
2380 | % note: we cannot call translate_bexpression yet; not yet wrapped and typed ! | |
2381 | nonvar(Expr), functor(Expr,F,_), | |
2382 | translate_prolog_constructor(F,Translation). | |
2383 | ||
2384 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
2385 | % type rules | |
2386 | ||
2387 | % just a convenience interface predicate to extract typing infos for expression and sub-expressions | |
2388 | % in conjunction with syntaxtransformation to fill in types for subarguments | |
2389 | lookup_type_for_expr(Var,Type) :- var(Var), !, add_internal_error('Variable expr:', lookup_type_for_expr(Var,Type)). | |
2390 | lookup_type_for_expr(integer(_),Type) :- !, Type=integer. | |
2391 | lookup_type_for_expr(string(_),Type) :- !, Type=string. | |
2392 | lookup_type_for_expr(real(_),Type) :- !, Type=real. | |
2393 | lookup_type_for_expr(exists(_,pred),Type) :- !, Type=pred. | |
2394 | lookup_type_for_expr(forall(_,pred,pred),Type) :- !, Type=pred. | |
2395 | lookup_type_for_expr(let_predicate(_,_,pred),Type) :- !, Type=pred. % TODO: equalities | |
2396 | lookup_type_for_expr(let_expression(_,_,T),Type) :- !, Type=T. | |
2397 | lookup_type_for_expr(let_expression_global(_,_,T),Type) :- !, Type=T. | |
2398 | %lookup_type_for_expr(operation_call_in_expr(Operation,OpCallParaValues),Type) :- !, TODO: get operation return type | |
2399 | lookup_type_for_expr(comprehension_set(_,pred),Type) :- !, Type=set(_). | |
2400 | lookup_type_for_expr(value(V),Type) :- !, | |
2401 | (nonvar(V),V=avl_set(_) -> Type=set(_) ; true). % TO DO: infer type from value | |
2402 | lookup_type_for_expr(set_extension(List),Type) :- !, | |
2403 | (List=[ST|_] -> SetType=ST | |
2404 | ; List=[] -> add_warning(check_ast,'Empty set_extension:',List) % can be generated by fuzzer | |
2405 | ; add_internal_error('Illegal subtype:', lookup_type_for_expr(set_extension(List),Type))), | |
2406 | Type = set(SetType). | |
2407 | lookup_type_for_expr(sequence_extension(List),Type) :- !, | |
2408 | (List=[ST|_] -> SeqType=ST | |
2409 | ; List=[] -> add_warning(check_ast,'Empty sequence_extension:',List) % can be generated by fuzzer | |
2410 | ; add_internal_error('Illegal subtype:', lookup_type_for_expr(sequence_extension(List),Type))), | |
2411 | Type = set(couple(integer,SeqType)). | |
2412 | lookup_type_for_expr(general_sum(_,pred,Type),Type) :- !, | |
2413 | integer_or_real_type(Type). % Note: this clause may return a variable with a pending co-routine | |
2414 | lookup_type_for_expr(general_product(_,pred,Type),Type) :- !, integer_or_real_type(Type). % ditto | |
2415 | lookup_type_for_expr(partition(set(_),_),Type) :- !, Type = pred. % TODO: check list | |
2416 | lookup_type_for_expr(rec(Fields),Type) :- !, Type = record(FieldTypes), | |
2417 | (var(Fields) -> add_internal_error('Variable fields list: ',lookup_type_for_expr(rec(Fields),Type)) | |
2418 | ; sort(Fields,SFields), | |
2419 | maplist(lookup_field_type,SFields,FieldTypes)). | |
2420 | lookup_type_for_expr(record_field(_Record,_Name),_Type) :- !. %TODO: infer type | |
2421 | lookup_type_for_expr(struct(_RecordFieldTypes),set(_Type)) :- !. %TODO: infer type | |
2422 | lookup_type_for_expr(external_pred_call(_Name,_Args),Type) :- !,Type=pred. | |
2423 | lookup_type_for_expr(external_subst_call(_Name,_Args),Type) :- !,Type=subst. | |
2424 | lookup_type_for_expr(external_function_call(_Name,_Args),_Type) :- !. % TODO infer type | |
2425 | lookup_type_for_expr(recursive_let(_,_),Type) :- !, Type=set(_). | |
2426 | lookup_type_for_expr(operation(_,_,_,_),Type) :- !,Type=op(_Params,_Results). % TODO: infer params and results | |
2427 | lookup_type_for_expr(Subst,Type) :- is_subst_syntaxelement(Subst),!,Type=subst. | |
2428 | lookup_type_for_expr(Expr,Type) :- % print(lookup(Expr)),nl, | |
2429 | Expr <:> Type. | |
2430 | % TODO: cover all constructs with ids or [Type] annotations | |
2431 | % TODO: provide a better convenience predicate for a local type consistency check | |
2432 | ||
2433 | ||
2434 | lookup_field_type(field(Name,Val),field(Name,ValType)) :- | |
2435 | (var(Val) -> true % here it is ok to have a variable, e.g., if we use lookup_type_for_expr after syntaxtransformation | |
2436 | ; lookup_type_for_expr(Val,ValType)). | |
2437 | ||
2438 | :- block integer_or_real_type(-). | |
2439 | integer_or_real_type(integer). | |
2440 | integer_or_real_type(real). | |
2441 | ||
2442 | ||
2443 | % predicates | |
2444 | truth <:> pred. | |
2445 | falsity <:> pred. | |
2446 | conjunct(pred,pred) <:> pred. | |
2447 | %conjunct([pred]) <:> pred. | |
2448 | negation(pred) <:> pred. | |
2449 | disjunct(pred,pred) <:> pred. | |
2450 | %disjunct([pred]) <:> pred. | |
2451 | implication(pred,pred) <:> pred. | |
2452 | equivalence(pred,pred) <:> pred. | |
2453 | equal(A,A) <:> pred. | |
2454 | not_equal(A,A) <:> pred. | |
2455 | member(A,set(A)) <:> pred. | |
2456 | not_member(A,set(A)) <:> pred. | |
2457 | subset(set(A),set(A)) <:> pred. | |
2458 | subset_strict(set(A),set(A)) <:> pred. | |
2459 | not_subset(set(A),set(A)) <:> pred. | |
2460 | not_subset_strict(set(A),set(A)) <:> pred. | |
2461 | less_equal(integer,integer) <:> pred. | |
2462 | less(integer,integer) <:> pred. | |
2463 | less_equal_real(real,real) <:> pred. | |
2464 | less_real(real,real) <:> pred. | |
2465 | greater_equal(integer,integer) <:> pred. | |
2466 | greater(integer,integer) <:> pred. | |
2467 | finite(set(_)) <:> pred. | |
2468 | exists(ids,pred) <:> pred. | |
2469 | partition(set(T),[set(T)]) <:> pred. | |
2470 | % external_subst_call(_,[_]) <:> pred. | |
2471 | ||
2472 | % expressions | |
2473 | boolean_true <:> boolean. | |
2474 | boolean_false <:> boolean. | |
2475 | max_int <:> integer. | |
2476 | min_int <:> integer. | |
2477 | empty_set <:> set(_). | |
2478 | integer_set(_) <:> set(integer). % new | |
2479 | bool_set <:> set(boolean). | |
2480 | float_set <:> set(real). | |
2481 | real_set <:> set(real). | |
2482 | string_set <:> set(string). | |
2483 | convert_bool(pred) <:> boolean. | |
2484 | convert_real(integer) <:> real. | |
2485 | convert_int_floor(real) <:> integer. | |
2486 | convert_int_ceiling(real) <:> integer. | |
2487 | add(integer,integer) <:> integer. | |
2488 | add_real(real,real) <:> real. | |
2489 | %general_sum(ids,pred,integer) <:> integer. % can also be applied to real | |
2490 | %general_product(ids,pred,integer) <:> integer. % can also be applied to reals | |
2491 | minus(integer,integer) <:> integer. | |
2492 | minus_real(real,real) <:> real. | |
2493 | unary_minus(integer) <:> integer. | |
2494 | unary_minus_real(real) <:> real. | |
2495 | multiplication(integer,integer) <:> integer. | |
2496 | multiplication_real(real,real) <:> real. | |
2497 | cartesian_product(set(A),set(B)) <:> set(couple(A,B)). | |
2498 | div(integer,integer) <:> integer. | |
2499 | div_real(real,real) <:> real. | |
2500 | floored_div(integer,integer) <:> integer. | |
2501 | modulo(integer,integer) <:> integer. | |
2502 | power_of(integer,integer) <:> integer. | |
2503 | power_of_real(real,real) <:> real. % operator in Atelier-B requires integer as second arg; we add conversion | |
2504 | successor <:> set(couple(integer,integer)). | |
2505 | predecessor <:> set(couple(integer,integer)). | |
2506 | %max(set(integer)) <:> integer. | |
2507 | max(set(T)) <:> T. | |
2508 | max_real(set(real)) <:> real. | |
2509 | %min(set(integer)) <:> integer. | |
2510 | min(set(T)) <:> T. | |
2511 | min_real(set(real)) <:> real. | |
2512 | card(set(_)) <:> integer. | |
2513 | couple(A,B) <:> couple(A,B). | |
2514 | pow_subset(set(A)) <:> set(set(A)). | |
2515 | pow1_subset(set(A)) <:> set(set(A)). | |
2516 | fin_subset(set(A)) <:> set(set(A)). | |
2517 | fin1_subset(set(A)) <:> set(set(A)). | |
2518 | interval(integer,integer) <:> set(integer). | |
2519 | union(set(A),set(A)) <:> set(A). | |
2520 | intersection(set(A),set(A)) <:> set(A). | |
2521 | set_subtraction(set(A),set(A)) <:> set(A). /* ?? */ | |
2522 | general_union(set(set(A))) <:> set(A). | |
2523 | general_intersection(set(set(A))) <:> set(A). | |
2524 | relations(set(A),set(B)) <:> set(set(couple(A,B))). | |
2525 | identity(set(A)) <:> set(couple(A,A)). | |
2526 | event_b_identity <:> set(couple(A,A)). % for Rodin 1.0 | |
2527 | reverse(set(couple(A,B))) <:> set(couple(B,A)). % function inverse ~ | |
2528 | first_projection(set(A),set(B)) <:> set(couple(couple(A,B),A)). | |
2529 | event_b_first_projection(set(couple(A,B))) <:> set(couple(couple(A,B),A)). % should no longer appear after Rodin 1.0 | |
2530 | event_b_first_projection_v2 <:> set(couple(couple(A,_B),A)). % for Rodin 1.0 | |
2531 | second_projection(set(A),set(B)) <:> set(couple(couple(A,B),B)). | |
2532 | event_b_second_projection(set(couple(A,B))) <:> set(couple(couple(A,B),B)). % should no longer appear after Rodin 1.0 | |
2533 | event_b_second_projection_v2 <:> set(couple(couple(_A,B),B)). % for Rodin 1.0 | |
2534 | first_of_pair(couple(A,_)) <:> A. % new | |
2535 | second_of_pair(couple(_,B)) <:> B. % new | |
2536 | composition(set(couple(A,B)),set(couple(B,C))) <:> set(couple(A,C)). | |
2537 | ring(set(couple(B,C)),set(couple(A,B))) <:> set(couple(A,C)). | |
2538 | direct_product(set(couple(E,F)),set(couple(E,G))) <:> set(couple(E,couple(F,G))). | |
2539 | parallel_product(set(couple(E,F)),set(couple(G,H))) <:> set(couple(couple(E,G),couple(F,H))). | |
2540 | trans_function(set(couple(A,B))) <:> set(couple(A,set(B))). | |
2541 | trans_relation(set(couple(A,set(B)))) <:> set(couple(A,B)). | |
2542 | iteration(set(couple(A,A)),integer) <:> set(couple(A,A)). | |
2543 | reflexive_closure(set(couple(A,A))) <:> set(couple(A,A)). | |
2544 | closure(set(couple(A,A))) <:> set(couple(A,A)). | |
2545 | domain(set(couple(A,_))) <:> set(A). | |
2546 | range(set(couple(_,B))) <:> set(B). | |
2547 | image(set(couple(A,B)),set(A)) <:> set(B). | |
2548 | domain_restriction(set(A),set(couple(A,B))) <:> set(couple(A,B)). | |
2549 | domain_subtraction(set(A),set(couple(A,B))) <:> set(couple(A,B)). | |
2550 | range_restriction(set(couple(A,B)),set(B)) <:> set(couple(A,B)). | |
2551 | range_subtraction(set(couple(A,B)),set(B)) <:> set(couple(A,B)). | |
2552 | overwrite(set(couple(A,B)),set(couple(A,B))) <:> set(couple(A,B)). | |
2553 | partial_function(A,B)<:>T :- relations(A,B)<:>T. | |
2554 | total_function(A,B)<:>T :- relations(A,B)<:>T. | |
2555 | partial_injection(A,B)<:>T :- relations(A,B)<:>T. | |
2556 | total_injection(A,B)<:>T :- relations(A,B)<:>T. | |
2557 | partial_surjection(A,B)<:>T :- relations(A,B)<:>T. | |
2558 | total_surjection(A,B)<:>T :- relations(A,B)<:>T. | |
2559 | total_bijection(A,B)<:>T :- relations(A,B)<:>T. | |
2560 | partial_bijection(A,B)<:>T :- relations(A,B)<:>T. | |
2561 | total_relation(A,B)<:>T :- relations(A,B)<:>T. | |
2562 | surjection_relation(A,B)<:>T :- relations(A,B)<:>T. | |
2563 | total_surjection_relation(A,B)<:>T :- relations(A,B)<:>T. | |
2564 | seq(set(A)) <:> set(seq(A)). | |
2565 | seq1(X)<:>T :- seq(X)<:>T. | |
2566 | iseq(X)<:>T :- seq(X)<:>T. | |
2567 | iseq1(X)<:>T :- seq(X)<:>T. | |
2568 | perm(set(A)) <:> set(seq(A)). | |
2569 | empty_sequence <:> seq(_). | |
2570 | size(seq(_)) <:> integer. | |
2571 | first(seq(A)) <:> A. | |
2572 | last(seq(A)) <:> A. | |
2573 | front(seq(A)) <:> seq(A). | |
2574 | tail(seq(A)) <:> seq(A). | |
2575 | rev(seq(A)) <:> seq(A). | |
2576 | concat(seq(A),seq(A)) <:> seq(A). | |
2577 | insert_front(A,seq(A)) <:> seq(A). | |
2578 | insert_tail(seq(A),A) <:> seq(A). | |
2579 | restrict_front(seq(A),integer) <:> seq(A). | |
2580 | restrict_tail(seq(A),integer) <:> seq(A). | |
2581 | general_concat(seq(seq(A))) <:> seq(A). | |
2582 | function(set(couple(A,B)),A) <:> B. | |
2583 | set_extension([T]) <:> set(T). | |
2584 | sequence_extension([T]) <:> seq(T). | |
2585 | comprehension_set(ids(T),pred) <:> set(T). | |
2586 | event_b_comprehension_set(ids,T,pred) <:> set(T). | |
2587 | lambda(ids(A),pred,R) <:> set(couple(A,R)). | |
2588 | general_sum(ids,pred,T) <:> T. % was integer, now can also be real | |
2589 | general_product(ids,pred,T) <:> T. % was integer, now can also be real | |
2590 | quantified_union(ids,pred,set(T)) <:> set(T). | |
2591 | quantified_intersection(ids,pred,set(T)) <:> set(T). | |
2592 | mu(set(T)) <:> T. | |
2593 | if_then_else(pred,T,T) <:> T. | |
2594 | tree(set(A)) <:> set(set(couple(seq(integer),A))). % Section 5.20 of Atelier-B manrefb.pdf | |
2595 | btree(A) <:> T :- tree(A) <:> T. | |
2596 | tree_over(A) <:> set(couple(seq(integer),A)). % dummy function to ease writing of rules below | |
2597 | const(A,seq(TreeA)) <:> TreeA :- tree_over(A) <:> TreeA. | |
2598 | top(TreeA) <:> A :- tree_over(A) <:> TreeA. | |
2599 | prefix(TreeA) <:> seq(A) :- tree_over(A) <:> TreeA. | |
2600 | postfix(TreeA) <:> seq(A) :- tree_over(A) <:> TreeA. | |
2601 | sizet(TreeA) <:> integer :- tree_over(_) <:> TreeA. | |
2602 | mirror(TreeA) <:> TreeA :- tree_over(_) <:> TreeA. | |
2603 | rank(TreeA,seq(integer)) <:> integer :- tree_over(_) <:> TreeA. % seq(integer) is the type of paths | |
2604 | father(TreeA,seq(integer)) <:> seq(integer) :- tree_over(_) <:> TreeA. | |
2605 | son(TreeA,seq(integer),integer) <:> seq(integer) :- tree_over(_) <:> TreeA. | |
2606 | subtree(TreeA,seq(integer)) <:> TreeA :- tree_over(_) <:> TreeA. | |
2607 | arity(TreeA,seq(integer)) <:> integer :- tree_over(_) <:> TreeA. | |
2608 | sons(TreeA) <:> seq(TreeA) :- tree_over(_) <:> TreeA. | |
2609 | bin(A) <:> TreeA :- tree_over(A) <:> TreeA. | |
2610 | bin(TreeA,A,TreeA) <:> TreeA :- tree_over(A) <:> TreeA. | |
2611 | infix(TreeA) <:> seq(A) :- tree_over(A) <:> TreeA. | |
2612 | left(TreeA) <:> TreeA :- tree_over(_) <:> TreeA. | |
2613 | right(TreeA) <:> TreeA :- tree_over(_) <:> TreeA. | |
2614 | ||
2615 | % records are handled in btype2; TODO: provide support here | |
2616 | % rec(Fields) <:> record(FieldTypes) :- | |
2617 | % record_field(RecordType) <:> FieldType :- member() | |
2618 | assertion_expression(pred,_Msg,Type) <:> Type. % generated by ast_cleanup, should we check _Msg is atom? | |
2619 | typeset <:> _AnyType. | |
2620 | ||
2621 | % substitutions | |
2622 | skip <:> subst. | |
2623 | block(subst) <:> subst. | |
2624 | precondition(pred,subst) <:> subst. | |
2625 | sequence([subst]) <:> subst. | |
2626 | any(new_readonly_ids,pred,subst) <:> subst. | |
2627 | if([subst]) <:> subst. | |
2628 | if_elsif(pred,subst) <:> subst. | |
2629 | assertion(pred,subst) <:> subst. | |
2630 | witness_then(pred,subst) <:> subst. | |
2631 | let(new_readonly_ids,pred,subst) <:> subst. | |
2632 | var(new_ids,subst) <:> subst. % was ids instead of new_ids; see test 1658 | |
2633 | select([subst],subst) <:> subst. | |
2634 | select([subst]) <:> subst. | |
2635 | select_when(pred,subst) <:> subst. | |
2636 | choice([subst]) <:> subst. | |
2637 | ||
2638 | % not used for type check | |
2639 | %parallel([subst]) <:> subst. | |
2640 | %any(ids,pred,subst) <:> subst. | |
2641 | %assign(ids(T),[T]) <:> subst. | |
2642 | % ... | |
2643 | ||
2644 | % other stuff | |
2645 | witness(_,pred) <:> witness. | |
2646 | ordinary <:> status. | |
2647 | anticipated(_) <:> status. | |
2648 | convergent(_) <:> status. | |
2649 | ||
2650 | ||
2651 | % error_rewrites: common mistakes users make | |
2652 | % the message will be wrapped in 'Did you ' and ' ?' | |
2653 | :- use_module(specfile,[eventb_mode/0]). | |
2654 | error_rewrite(insert_front(A,B),insert_tail(A,B),'use -> instead of <- (sequence append)'). | |
2655 | error_rewrite(insert_front(A,B),couple(A,B),'use -> instead of |-> (maplet) or total function (-->)'). | |
2656 | error_rewrite(insert_front(A,B),total_function(A,B),'use -> instead of --> (total function)'). | |
2657 | error_rewrite(insert_tail(A,B),insert_front(A,B),'use <- instead of -> (sequence prepend)'). | |
2658 | % error_rewrite(insert_tail(A,B),less(A,B),'use <- instead of < - (less)'). for predicate x <- 3 | |
2659 | error_rewrite(image(A,B),image(A,set_extension(unknown_src,[B])),'forget the curly braces {.} inside the relational image [.]'). % :- get_texpr_type(B,TB). % f[1] instead of f[{1}] | |
2660 | %error_rewrite(image(A,B),function(A,B),'use relational image .[.] instead of function application .(.)'). % does not seem to trigger | |
2661 | error_rewrite(concat(A,B),power_of(A,B),'use ^ (concat) instead of ** (exponentation)'). | |
2662 | error_rewrite(power_of(A,B),cartesian_product(A,B),'use ** (exponentation) instead of * (cartesian product)') :- \+ eventb_mode. | |
2663 | ||
2664 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
2665 | ||
2666 | ||
2667 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ | |
2668 | % type environment | |
2669 | env_empty(env(Avl)) :- empty_avl(Avl). | |
2670 | ||
2671 | env_lookup_type(Id,Env,Type) :- | |
2672 | env_lookup2(Env,Id,Type,_Infos). | |
2673 | env_lookup_infos(Id,Env,Infos) :- | |
2674 | env_lookup2(Env,Id,_Type,Infos). | |
2675 | env_lookup_position_string(Id,Env,PosStr) :- | |
2676 | env_lookup2(Env,Id,_Type,Infos), | |
2677 | get_info_pos(Infos,Pos), Pos \= none, | |
2678 | translate:translate_span(Pos,PosStr). | |
2679 | env_lookup2(env(Avl),Id,Type,Infos) :- | |
2680 | avl_fetch(Id,Avl,entry(Type,Infos)). | |
2681 | env_lookup2(openenv(Open,Env),Id,Type,Infos) :- | |
2682 | (env_lookup2(Env,Id,Type,Infos) -> true ; openenv_lookup(Open,Id,Type,Infos)). | |
2683 | ||
2684 | % check if an identifier is already defined either in static environment, or already in open env (but not adding new ids) | |
2685 | env_check_identifier_defined(Id,openenv(Open,Env)) :- !, | |
2686 | (env_lookup_type(Id,Env,_) -> true ; openenv_check_id_defined(Id,Open)). | |
2687 | env_check_identifier_defined(Id,Env) :- env_lookup_type(Id,Env,_). | |
2688 | ||
2689 | env_lookup_existing_infos(Id,openenv(_,Env),Infos) :- !, | |
2690 | env_lookup_infos(Id,Env,Infos). | |
2691 | env_lookup_existing_infos(Id,Env,Infos) :- env_lookup2(Env,Id,_,Infos). | |
2692 | ||
2693 | env_get_visible_ids(env(Avl),Ids) :- avl_domain(Avl,Ids). | |
2694 | ||
2695 | env_store(Id,Type,Infos,In,Out) :- | |
2696 | env_store2(In,Id,Type,Infos,Out). | |
2697 | env_store2(env(In),Id,Type,Infos,env(Out)) :- | |
2698 | avl_store(Id,In,entry(Type,Infos),Out). | |
2699 | env_store2(openenv(Open,In),Id,Type,Infos,openenv(Open,Out)) :- | |
2700 | env_store2(In,Id,Type,Infos,Out). | |
2701 | ||
2702 | env_store_definition(definition_decl(Name,DefType,_Pos,Params,Body,_Deps), In, Out) :- | |
2703 | env_store(Name, definition(DefType,Params,Body), [], In, Out). | |
2704 | ||
2705 | % store a callback predicate in the environment | |
2706 | env_store_operator(Id,Module:Callback,In,Out) :- | |
2707 | % the type is ignored, we just use the info field | |
2708 | debug_format(4,'Storing operator "~w" (callback ~w:~w)~n',[Id,Module,Callback]), | |
2709 | env_store(operator(Id),boolean,[Module:Callback],In,Out). | |
2710 | ||
2711 | % the open environment acts like the normal type environment with the | |
2712 | % exception that a lookup of an identifier always works, in case the | |
2713 | % identifier was not in the environment, it will be added to it. | |
2714 | openenv(Env,openenv(_,Env)). | |
2715 | make_open(Env,Res) :- nonvar(Env), Env = openenv(_,_),!, Res=Env. | |
2716 | make_open(Env,OpenEnv) :- openenv(Env,OpenEnv). | |
2717 | openenv_lookup([Head|Tail],Id,Type,Infos) :- | |
2718 | Infos=[], | |
2719 | ( Head = entry(Id,_,_) -> % may store new identifier if Head was a variable | |
2720 | Head = entry(Id,Type,Infos) | |
2721 | ; | |
2722 | openenv_lookup(Tail,Id,Type,Infos)). | |
2723 | ||
2724 | openenv_check_id_defined(Var,_Id) :- var(Var),!,fail. | |
2725 | openenv_check_id_defined([Head|Tail],Id) :- | |
2726 | ( Head = entry(Id,_,_) -> true | |
2727 | ; openenv_check_id_defined(Tail,Id)). | |
2728 | ||
2729 | openenv_identifiers(openenv(List,_),Ids) :- | |
2730 | openenv_identifiers2(List,Ids). | |
2731 | openenv_identifiers2(List,[]) :- var(List),!. | |
2732 | openenv_identifiers2([],[]). | |
2733 | openenv_identifiers2([entry(Id,Type,Infos)|Rest],[TId|IdRest]) :- | |
2734 | create_texpr(identifier(Id),Type,Infos,TId), | |
2735 | openenv_identifiers2(Rest,IdRest). | |
2736 | ||
2737 | env_identifiers(env(Avl),Ids) :- | |
2738 | avl_domain(Avl,Ids). | |
2739 | env_identifiers(openenv(Open,Env),Ids) :- | |
2740 | env_identifiers(Env,Ids1), | |
2741 | open_env_identifiers(Open,Ids2), | |
2742 | append(Ids2,Ids1,UIds),sort(UIds,Ids). | |
2743 | open_env_identifiers(L,Ids) :- var(L),!,Ids=[]. | |
2744 | open_env_identifiers([],[]). | |
2745 | open_env_identifiers([entry(Id,_,_)|Orest],[Id|Irest]) :- | |
2746 | open_env_identifiers(Orest,Irest). | |
2747 | ||
2748 | ||
2749 | % gives a list of all known identifiers and their information in a type | |
2750 | % environment. A second list of the same size is used to build up a new | |
2751 | % environment whith the same identifiers and types but with new information | |
2752 | env_transform_infos(env(Avl),Ids,OldInfos,NewInfos,env(NewAvl)) :- | |
2753 | % transform a standard environment by converting it to a list, | |
2754 | % iterate over the list and convert the result back | |
2755 | avl_to_list(Avl,OldEntries), | |
2756 | maplist(env_transinfo2,OldEntries,Id_OldInfo_NewInfo,NewEntries), | |
2757 | maplist(split_slash,Id_OldInfo_NewInfo,Ids,Old_New_Info), | |
2758 | maplist(split_slash,Old_New_Info,OldInfos,NewInfos), | |
2759 | ord_list_to_avl(NewEntries,NewAvl). | |
2760 | env_transform_infos(openenv(Open,Env),Ids,OldInfos,NewInfos,openenv(NewOpen,NewEnv)) :- | |
2761 | % an open environment iterates first over the (open) list, | |
2762 | % calls then the code for the standard environment and concatenates | |
2763 | % the generated lists. | |
2764 | env_transinfo_open(Open,Ids1,OldInfos1,NewInfos1,NewOpen), | |
2765 | env_transform_infos(Env,Ids2,OldInfos2,NewInfos2,NewEnv), | |
2766 | append(Ids1,Ids2,Ids), | |
2767 | append(OldInfos1,OldInfos2,OldInfos), | |
2768 | append(NewInfos1,NewInfos2,NewInfos). | |
2769 | % iterate over standard environments | |
2770 | env_transinfo2(Id-entry(Type,OldInfo),Id/(OldInfo/NewInfo),Id-entry(Type,NewInfo)). | |
2771 | % iterate over the open list (last element is not [] but a variable) | |
2772 | env_transinfo_open(OpenEnv,[],[],NewInfo,NewEnv) :- var(OpenEnv),!,OpenEnv=NewEnv,NewInfo=[]. | |
2773 | env_transinfo_open([],[],[],[],[]). | |
2774 | env_transinfo_open([entry(Id,Type,OldInfo)|ORest],[Id|IdRest],[OldInfo|OIRest],[NewInfo|NIRest],[entry(Id,Type,NewInfo)|NRest]) :- | |
2775 | env_transinfo_open(ORest,IdRest,OIRest,NIRest,NRest). | |
2776 | split_slash(A/B,A,B). | |
2777 | ||
2778 | ||
2779 | % utility to portray environment | |
2780 | :- public portray_env/1. | |
2781 | portray_env(env(In)) :- !, format('ENV:~n',[]),portray_avl_env(In). | |
2782 | portray_env(openenv(Open,In)) :- !, format('OPENENV (~w): ',[Open]), portray_env(In). | |
2783 | portray_env(E) :- !, format('*** UNKNOWN ENV: ~w~n',[E]). | |
2784 | portray_avl_env(A) :- avl_member(Id,A,entry(Type,_Infos)), format(' ~w : ~w~n',[Id,Type]),fail. | |
2785 | %portray_avl_env(A) :- avl_member(Id,A,entry(Type,Infos)), format(' ~w : ~w ~w~n',[Id,Type,Infos]),fail. | |
2786 | portray_avl_env(_) :- nl. | |
2787 | ||
2788 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
2789 | % fast manual generation of syntax trees | |
2790 | % this code is only for testing, not for use in the regular type checking | |
2791 | % of user-given expressions | |
2792 | ||
2793 | fasttype(Expr,TExpr) :- | |
2794 | term_variables(Expr,OldVars), | |
2795 | (Expr= +_ -> fasttype2(Expr,TExpr,unknown) ; fasttype2(Expr,TExpr,_Type)), | |
2796 | term_variables(TExpr,NewVars), | |
2797 | ( fasttype_check_new_vars(NewVars,OldVars) -> true | |
2798 | ; add_error(btypechecker, 'fasttype/2 introduced new variables'),fail). | |
2799 | fasttype2(Type<<Expr,b(TExpr,Type,[]),Type) :- !, | |
2800 | safe_functor(fasttype2,Expr,F,Arity), | |
2801 | safe_functor(fasttype2,TExpr,F,Arity), | |
2802 | safe_functor(fasttype2,Pattern,F,Arity), | |
2803 | ( Pattern <:> Type -> | |
2804 | fasttype_args(Arity,Expr,TExpr,Pattern) | |
2805 | ; | |
2806 | fasttype_all_unknown(Arity,Pattern)), | |
2807 | fasttype_args(Arity,Expr,TExpr,Pattern). | |
2808 | fasttype2(+Expr,TExpr,Type) :- !, | |
2809 | ( Type==unknown -> | |
2810 | safe_functor(fasttype2,Expr,F,Arity), | |
2811 | safe_functor(fasttype2,Pattern,F,Arity), | |
2812 | ( fasttype_lookup(Pattern,NType) -> | |
2813 | fasttype2(NType<<Expr,TExpr,NType) | |
2814 | ; | |
2815 | add_error(btypechecker,'Not able to simply infer type:',Expr),fail) | |
2816 | ; | |
2817 | fasttype2(Type<<Expr,TExpr,Type)). | |
2818 | fasttype2([H|T],[TH|TT],_) :- !,fasttype2(H,TH,unknown),fasttype2(T,TT,unknown). | |
2819 | fasttype2(Expr,Expr,_). | |
2820 | ||
2821 | fasttype_all_unknown(0,_) :- !. | |
2822 | fasttype_all_unknown(N,Pattern) :- | |
2823 | arg(N,Pattern,unknown), | |
2824 | N1 is N-1, fasttype_all_unknown(N1,Pattern). | |
2825 | ||
2826 | fasttype_args(0,_,_,_) :- !. | |
2827 | fasttype_args(N,Expr,NExpr,Pattern) :- | |
2828 | arg(N,Expr,Arg), arg(N,NExpr,NArg), | |
2829 | arg(N,Pattern,ArgType), | |
2830 | fasttype2(Arg,NArg,ArgType), | |
2831 | N1 is N-1, | |
2832 | fasttype_args(N1,Expr,NExpr,Pattern). | |
2833 | ||
2834 | fasttype_lookup(integer(_),integer). | |
2835 | fasttype_lookup(Pattern,Type) :- Pattern <:> Type. | |
2836 | ||
2837 | fasttype_check_new_vars(Old,New) :- | |
2838 | sort(Old,SOld), sort(New, SNew), | |
2839 | fasttype_check_new_vars2(SOld,SNew). | |
2840 | fasttype_check_new_vars2([],_). | |
2841 | fasttype_check_new_vars2([N|NRest],[O|ORest]) :- | |
2842 | (N==O -> fasttype_check_new_vars(NRest,ORest) ; fasttype_check_new_vars([N|NRest],ORest)). | |
2843 | ||
2844 | ||
2845 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
2846 | % type expressions without declaring the identifiers | |
2847 | ||
2848 | % opentype type-checks an expression without having to declare every used | |
2849 | % identifier in advance. | |
2850 | % Exprs - a list of raw expressions to be type-checked | |
2851 | % InitEnv - an initial environment | |
2852 | % Identifiers - used identifiers that weren't in the initial environment | |
2853 | % DeferredSets - new introduced deferred sets for variables whose type couldn't be infered | |
2854 | % CleanExprs - the type-checked (and cleaned-up) list of expressions | |
2855 | opentype(Exprs,InitEnv,Identifiers,DeferredSets,CleanExprs) :- | |
2856 | openenv(InitEnv,OpenEnv), | |
2857 | do_typecheck(Exprs,OpenEnv,[],TypedExprs,Errors), | |
2858 | ( Errors = [] -> | |
2859 | true | |
2860 | ; Errors = [_|_] -> | |
2861 | throw(type_errors(Errors))), | |
2862 | % all identifier I whose type have the form set(_), | |
2863 | % introduce implicitly a new type global(I) | |
2864 | foldl(declare_deferred_sets,TypedExprs,DS1,[]), | |
2865 | % ensure that all bounded identifiers have ground types | |
2866 | ground_name_types_by_defsets(TypedExprs,DS2), | |
2867 | % ensure that all free identifiers have ground types | |
2868 | openenv_identifiers(OpenEnv,AllIdentifiers), | |
2869 | ground_free_types_by_defsets(AllIdentifiers,DS3), | |
2870 | % join all deferred sets | |
2871 | append([DS1,DS2,DS3],DeferredSets), | |
2872 | % the returned identifiers should not contain the global sets | |
2873 | exclude(tid_in_idlist(DeferredSets),AllIdentifiers,Identifiers), | |
2874 | % clean the expression up | |
2875 | clean_up_l_wo_optimizations(TypedExprs,[],CleanExprs,opentype). | |
2876 | ||
2877 | % used by opentype/4 | |
2878 | tid_in_idlist(IdList,TId) :- | |
2879 | def_get_texpr_id(TId,Id), | |
2880 | memberchk(Id,IdList). | |
2881 | ||
2882 | % used by opentype/4 | |
2883 | declare_deferred_sets(TExpr) --> | |
2884 | {syntaxtraversion(TExpr,Expr,Type,_,Subs,_)}, | |
2885 | declare_deferred_sets2(Expr,Type), | |
2886 | foldl(declare_deferred_sets,Subs). | |
2887 | declare_deferred_sets2(identifier(Id),Type) --> | |
2888 | {nonvar(Type),Type=set(SType),var(SType),!,SType=global(Id)},[Id]. | |
2889 | declare_deferred_sets2(_,_) --> []. | |
2890 | ||
2891 | % used by opentype/4, get all types of introduced identifiers | |
2892 | % (e.g. in quantifiers) and ground them by introducing deferred sets | |
2893 | ground_name_types_by_defsets(TExprs,DefSets) :- | |
2894 | get_all_name_types_l(TExprs,Types), | |
2895 | ground_by_defsets(Types,'_NSet',DefSets). | |
2896 | % used by opentype/4, get all types of the given identifiers | |
2897 | % and ground them by introducing deferred sets | |
2898 | ground_free_types_by_defsets(Ids,DefSets) :- | |
2899 | get_texpr_types(Ids,Types), | |
2900 | ground_by_defsets(Types,'_FSet',DefSets). | |
2901 | % takes a list of types and ground them by introducing | |
2902 | % deferred sets, each set's name starting with Prefix | |
2903 | ground_by_defsets(Types,Prefix,DefSets) :- | |
2904 | term_variables(Types,VarTypes), | |
2905 | foldl(ground_by_defsets2(Prefix),VarTypes,DefSets,1,_). | |
2906 | ground_by_defsets2(Prefix,global(DS),DS,N,N2) :- | |
2907 | number_chars(N,CN), | |
2908 | safe_atom_chars(Prefix,CS,ground_by_defsets2_1), | |
2909 | append(CS,CN,Chars), | |
2910 | safe_atom_chars(DS,Chars,ground_by_defsets2_2), | |
2911 | N2 is N+1. | |
2912 | ||
2913 | % get the types of all introduced identifiers | |
2914 | % (e.g. in quantifiers) | |
2915 | get_all_name_types(TExpr,Types) :- | |
2916 | syntaxtraversion(TExpr,_,_,_,Subs,Names), | |
2917 | get_texpr_types(Names,NTypes), | |
2918 | append(NTypes,RTypes,Types), | |
2919 | get_all_name_types_l(Subs,RTypes). | |
2920 | get_all_name_types_l(Exprs,Types) :- | |
2921 | maplist(get_all_name_types,Exprs,LTypes), | |
2922 | append(LTypes,Types). | |
2923 | ||
2924 | %check_nonvar(Src,V) :- var(V) -> add_error(check_nonvar,'Is a variable: ',Src:V) ; true. | |
2925 | ||
2926 | % type-checking of external functions/predicates/substitutions | |
2927 | btype_external_call(FunName,rewrite_protected(TypeParams),FunParams,rewrite_protected(Decl), | |
2928 | DeclType,InputType,Pos,Env,TFunParams,TRin,TRout) :- | |
2929 | add_ext_variables(TypeParams,Env,_TTypeParams,DeclSubenv,TRin,TR1), | |
2930 | btype(extcall_decl,Decl,DeclSubenv,DeclType,_TypedDecl,TR1,TR2), | |
2931 | % TODO: check against originally (for Atelier-B) defined function | |
2932 | % first identify the types of the parameters | |
2933 | btype_l(FunParams,Env,ParamTypes,TFunParams,TR2,TR3), | |
2934 | % now check if the function parameters match the input type | |
2935 | (ParamTypes = [] | |
2936 | -> /* the external call has no parameters */ | |
2937 | (InputType = empty_type -> TR3=TRout | |
2938 | ; add_error(btype_external_call,'Illegal call to external DEFINITION; it takes no arguments:',FunName), | |
2939 | fail) | |
2940 | ; couplise_list(ParamTypes,JoinedParamType), | |
2941 | unify_types(InputType,JoinedParamType,Pos,no_expression,TR3,TRout)). | |
2942 | ||
2943 | % ---------------------------- | |
2944 | ||
2945 | ||
2946 | % add CallPos (if /= unknown) as additional position information for sub-expressions | |
2947 | ||
2948 | add_raw_ast_pos_info_context(Ctxt,CPos,Raw,NewRaw) :- | |
2949 | simplify_call_pos(CPos,SimpleCPos), | |
2950 | add_raw_ast_pos_info_context2(Ctxt,SimpleCPos,Raw,NewRaw). | |
2951 | ||
2952 | %simplify_call_pos(pos_context(P1,_,_),Res) :- | |
2953 | % get_preference(provide_trace_information,false), %sometimes the full nesting is very useful | |
2954 | % % for definition calls we only used to store the actual position of the call, | |
2955 | % % not in which scope this call itself has occurred (to avoid overly complex messages) | |
2956 | % BUT now with call_stack display this information is presented more clearly and is very useful | |
2957 | % !, | |
2958 | % simplify_call_pos(P1,Res). | |
2959 | simplify_call_pos(P,P). | |
2960 | ||
2961 | add_raw_ast_pos_info_context2(_,_,Raw,NewRaw) :- | |
2962 | simple_raw(Raw),!, | |
2963 | NewRaw=Raw. | |
2964 | add_raw_ast_pos_info_context2(Ctxt,CPos,Raw,NewRaw) :- | |
2965 | list_operator(Raw,Pos,L,NewRaw,NewPos,NewL),!, | |
2966 | combine_pos(Pos,Ctxt,CPos,NewPos), | |
2967 | maplist(add_raw_ast_pos_info_context2(Ctxt,CPos),L,NewL). | |
2968 | add_raw_ast_pos_info_context2(Ctxt,CPos,Raw,NewRaw) :- % print(Raw),nl, | |
2969 | Raw =.. [Op,Pos1|T], raw_operator(Op), | |
2970 | !, | |
2971 | maplist(add_raw_ast_pos_info_context2(Ctxt,CPos),T,T2), | |
2972 | combine_pos(Pos1,Ctxt,CPos,NewPos), | |
2973 | NewRaw =.. [Op,NewPos|T2]. | |
2974 | add_raw_ast_pos_info_context2(_,_,R,R). % :- print(uncovered_raw(R)),nl,nl. | |
2975 | ||
2976 | %combine_pos(none,P,R) :- !, R=P. | |
2977 | combine_pos(P1,Ctxt,P2,pos_context(P1,Ctxt,P2)). | |
2978 | ||
2979 | simple_raw(F) :- functor(F,_,1). | |
2980 | simple_raw(identifier(_,_)). | |
2981 | simple_raw(integer(_,_)). | |
2982 | simple_raw(string(_,_)). | |
2983 | ||
2984 | % operators which have lists as arguments | |
2985 | list_operator(comprehension_set(P,Args,L),P,[L],comprehension_set(P2,Args,L2),P2,[L2]). | |
2986 | list_operator(couple(P,L),P,L,couple(P2,L2),P2,L2). | |
2987 | list_operator(definition(P,F,L),P,L,definition(P2,F,L2),P2,L2). | |
2988 | list_operator(external_function_call(P,N,L,F,T1,T2),P,L, | |
2989 | external_function_call(P2,N,L2,F,T1,T2),P2,L2). | |
2990 | list_operator(external_pred_call(P,N,L,F,T1,T2),P,L, | |
2991 | external_pred_call(P2,N,L2,F,T1,T2),P2,L2). | |
2992 | list_operator(external_subst_call(P,N,L,F,T1,T2),P,L, | |
2993 | external_subst_call(P2,N,L2,F,T1,T2),P2,L2). | |
2994 | list_operator(function(P,F,L),P,[F|L],function(P2,F2,L2),P2,[F2|L2]). | |
2995 | list_operator(general_sum(P,Args,B,E),P,[B,E|Args], | |
2996 | general_sum(P2,Args2,B2,E2),P2,[B2,E2|Args2]). | |
2997 | list_operator(lambda(P,Args,B,E),P,[B,E],lambda(P2,Args,B2,E2),P2,[B2,E2]). | |
2998 | list_operator(sequence_extension(P,L),P,L,sequence_extension(P2,L2),P2,L2). | |
2999 | list_operator(set_extension(P,L),P,L,set_extension(P2,L2),P2,L2). | |
3000 | ||
3001 | % simple raw operators whose first argument is a position and all other are raw formulas | |
3002 | raw_operator(add). | |
3003 | raw_operator(add_real). | |
3004 | raw_operator(card). | |
3005 | raw_operator(cartesian_product). | |
3006 | raw_operator(conjunct). | |
3007 | raw_operator(convert_bool). | |
3008 | raw_operator(convert_real). | |
3009 | raw_operator(convert_int_floor). | |
3010 | raw_operator(convert_int_ceiling). | |
3011 | %raw_operator(couple). | |
3012 | %raw_operator(definition). | |
3013 | raw_operator(disjunct). | |
3014 | raw_operator(div). | |
3015 | raw_operator(div_real). | |
3016 | raw_operator(domain). | |
3017 | raw_operator(equal). | |
3018 | raw_operator(equivalence). | |
3019 | raw_operator(first). | |
3020 | raw_operator(first_projection). | |
3021 | raw_operator(front). | |
3022 | raw_operator(greater). | |
3023 | raw_operator(greater_equal). | |
3024 | raw_operator(identifier). | |
3025 | raw_operator(image). | |
3026 | raw_operator(implication). | |
3027 | raw_operator(interval). | |
3028 | raw_operator(intersection). | |
3029 | raw_operator(last). | |
3030 | raw_operator(less). | |
3031 | raw_operator(less_equal). | |
3032 | raw_operator(less_real). | |
3033 | raw_operator(less_equal_real). | |
3034 | raw_operator(max). | |
3035 | raw_operator(member). | |
3036 | raw_operator(minus_or_set_subtract). | |
3037 | raw_operator(minus). | |
3038 | raw_operator(minus_real). | |
3039 | raw_operator(min). | |
3040 | raw_operator(multiplication). | |
3041 | raw_operator(multiplication_real). | |
3042 | raw_operator(mult_or_cart). | |
3043 | raw_operator(negation). | |
3044 | raw_operator(not_equal). | |
3045 | raw_operator(not_member). | |
3046 | raw_operator(not_subset_strict). | |
3047 | raw_operator(not_subset). | |
3048 | raw_operator(overwrite). | |
3049 | raw_operator(power_of). | |
3050 | raw_operator(power_of_real). | |
3051 | raw_operator(range). | |
3052 | raw_operator(reverse). | |
3053 | raw_operator(seq). | |
3054 | raw_operator(size). | |
3055 | raw_operator(subset_strict). | |
3056 | raw_operator(subset). | |
3057 | raw_operator(tail). | |
3058 | raw_operator(unary_minus). | |
3059 | raw_operator(unary_minus_real). | |
3060 | raw_operator(union). | |
3061 | % external_function_call, ... : treated in list_operator | |
3062 | %raw_operator(Op) :- print(uncovered_op(Op)),nl,fail. | |
3063 | % TO DO: add more operators | |
3064 | ||
3065 | %------------------- | |
3066 | ||
3067 | % try to coerce one type (without loss of precision) to an expected type if possible | |
3068 | % e.g., coercion of an integer to a real value | |
3069 | %coerce_type(Type,ExpectedType,OldExpr,NewExpr) | |
3070 | coerce_type(integer,real,OldExpr,NewCoercedExpr) :- | |
3071 | safe_create_texpr(convert_real(OldExpr),real,NewCoercedExpr). | |
3072 | coerce_type(pred,boolean,OldExpr,NewCoercedExpr) :- | |
3073 | safe_create_texpr(convert_bool(OldExpr),real,NewCoercedExpr). | |
3074 | %coerce_type(couple(A,B),couple(A2,B2),) | |
3075 | % insert TO_STRING, coerece inside couples, sets, records |