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