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