1 % (c) 2009-2019 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/5, % unify two types, return list of errors in case of type mismatch
13 unify_types_werrors_l/5, % unify two list of types
14 unify_types_strict/2, % unify two types, just fail in case of type mismatch
15
16 ext2int/7, % convert a (raw) syntax element into a typed element
17 remove_pos/2, % remove position info from a (raw) syntax element
18 % TODO[DP, 15.03.2013]: In case of a re-structuring of modules,
19 % maybe it is a good idea to move the type environment predicates to a module of its own
20 env_empty/1, % create an empty type environment
21 env_lookup_type/3, % lookup a type of an identifier in the environment
22 env_lookup_infos/3, % lookup additional infos of an identifier in the environment
23 env_store/5, % store the type of an identifier in the environment
24 env_store_operator/4, % store a theory operator into the environment
25 env_store_definition/3, % store an untyped definition_decl/6 ast in the environment
26 env_identifiers/2,
27 add_identifiers_to_environment/3,
28 operation_infos/1, % give a list of (uninstantiated) infos that operations need for type-checking
29 compute_accessed_vars_infos_for_operation/8, % (re)-compute reads/write infos for operation
30
31 couplise_list/2, % [a,b,c] -> couple(couple(a,b),c)
32 prime_identifiers/2, prime_identifier/2,
33 prime_identifiers0/2, prime_identifier0/2, prime_atom0/2,
34
35 fasttype/2, % manually create a syntax tree with type infos
36
37 openenv/2, % create an "open" type environment, where unknown identifiers will be added on demand
38 openenv_identifiers/2, % get the introduced identifiers of an open type environment
39 opentype/5, % type-check an expression without having every identifier declared in advance
40
41 reset_typechecker/0,
42 machine_string/1, % succeeds for every explicit string seen so far by the type checker
43 store_typecheck_error/4
44 ]).
45
46 :- use_module(tools).
47
48 :- use_module(module_information,[module_info/2]).
49 :- module_info(group,typechecker).
50 :- module_info(description,'ProBs type checker and type inference module.').
51
52 :- use_module(library(lists)).
53 :- use_module(library(terms)).
54 :- use_module(library(avl)).
55 :- use_module(library(ordsets)).
56
57 :- use_module(error_manager).
58 :- use_module(self_check).
59 :- use_module(kernel_records,[normalise_record_type/2, record_has_multiple_field_names/2]).
60
61 :- use_module(translate).
62
63 :- use_module(bsyntaxtree).
64 :- use_module(b_ast_cleanup).
65 :- use_module(debug).
66 :- use_module(input_syntax_tree,[raw_replace/3]).
67 :- use_module(preferences,[get_preference/2, preference/2]).
68 :- use_module(b_read_write_info,[get_accessed_vars/5]).
69
70 % operator for type inference rules
71 :- op(800,xfx,::).
72
73 %:- dynamic op_modifies_reads_cache/3. % store modifies and reads information for operations
74 :- dynamic machine_string/1. /* keep a list of all explicit strings seen in the machine so far */
75 /* Probably better: do it in a separeate traversal; talk to Daniel about this */
76 reset_typechecker :- reset_machine_strings. %, retractall(op_modifies_reads_cache(_,_,_)).
77 reset_machine_strings :- retractall(machine_string(_)).
78 assert_machine_string(S) :- machine_string(S) -> true ; assert(machine_string(S)).
79
80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81 % miniature B type checker
82
83 btype_ground(Exprs,Env,NonGroundExceptions,Types,TExprs,Errors) :-
84 btype_ground_dl(Exprs,Env,NonGroundExceptions,Types,TExprs,Errors,[]).
85
86 :- dynamic current_type_checking_context/1.
87 get_current_context(C) :-
88 (current_type_checking_context(SecName) -> ajoin([' in ',SecName],C) ; C='').
89
90 % a version of btype_ground_dl which stores current context
91 btype_ground_dl_in_section(SectionName,Exprs,Env,NonGroundExceptions,Types,TExprs,EIn,EOut) :-
92 retractall(current_type_checking_context(_)),
93 assert(current_type_checking_context(SectionName)),
94 call_cleanup(btype_ground_dl(Exprs,Env,NonGroundExceptions,Types,TExprs,EIn,EOut),
95 retractall(current_type_checking_context(_))).
96 % dl: difference list version
97 btype_ground_dl(Exprs,Env,NonGroundExceptions,Types,TExprs,EIn,EOut) :-
98 ~~mnf(same_length(Exprs,Types)), ~~mnf(same_length(Exprs,TExprs)),
99 ~~mnf(get_texpr_types(TExprs,Types)),
100 ~~mnf(do_typecheck_dl(Exprs,Env,[ground(NonGroundExceptions)],TExprs,EIn,EOut)).
101
102 % do_typecheck type-checks the expression and checks if the types
103 % of introduced variables (like in quantifiers) are ground
104 do_typecheck(Exprs,Env,Options,TExprs,Errors) :-
105 do_typecheck_dl(Exprs,Env,Options,TExprs,Errors,[]).
106
107 do_typecheck_dl(Exprs,Env,Options,TExprs,ErrorsIn,ErrorsOut) :-
108 typecheck_result_init(ErrorsIn,Delayed,Identifiers,TRStart),
109 % type-check the expressions
110 btype_l(Exprs,Env,_Type,TExprs,TRStart,TR),
111 typecheck_result_get_errors(TR,E1),
112 typecheck_result_get_delayed_rules(TR,[]),
113 typecheck_result_get_identifiers(TR,[]),
114 foldl(trigger_delayed_rule,Delayed,E1,E2),
115 % get the newly introduced identifiers and check if their types are
116 % ground
117 ( memberchk(ground(NonGroundExceptions),Options) ->
118 check_ground_types_dl(Identifiers,NonGroundExceptions,E2,ErrorsOut)
119 ; otherwise ->
120 E2=ErrorsOut).
121
122 trigger_delayed_rule(dr(Trigger,Errors),Ein,Eout) :-
123 % ground trigger, enforce blocked rule
124 Trigger = 0,
125 % by now Errors should have given a ground value by the co-routine
126 add_all(Errors,Ein,Eout).
127 add_all([]) --> !.
128 add_all([E|Rest]) --> [E], add_all(Rest).
129
130
131 % Utilities for tr(.) DCG argument for type-checking
132 type_error_or_warning_occurred(TRin,TRout) :-
133 % TO DO ? : also check for warnings
134 TRout=tr(Errors1,_,_,_),
135 TRin =tr(Errors2,_,_,_), Errors1 \== Errors2.
136
137 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
138
139 % typecheck_result_add_error(Error,TRin,TRout) usually this will be called with TRout a variable
140 typecheck_result_add_error(Error,tr(Errors,DR,Ids,Flags),tr(RestErrors,DR,Ids,NewFlags)) :-
141 ? (select(error_count(N,Max,PrevPos),Flags,NF)
142 -> N1 is N+1, NewFlags = [error_count(N1,Max,NewLastPos)|NF],
143 (Error = error(_,Pos) -> NewLastPos = Pos ; NewLastPos = PrevPos),
144 (N<Max -> Errors = [Error|RestErrors]
145 ; 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))
146 )
147 ; NewFlags = Flags, Errors = [Error|RestErrors]
148 ).
149
150 typecheck_result_add_delayed_rule(Trigger,RuleErrors,
151 tr(Errors,[dr(Trigger,RuleErrors)|Rules],Ids,Flags),tr(Errors,Rules,Ids,Flags)) :- !.
152 typecheck_result_add_delayed_rule(Trigger,RuleErrors,In,Out) :-
153 add_internal_error('Could not add delayed rule: ',typecheck_result_add_delayed_rule(Trigger,RuleErrors,In,Out)),
154 Out=In.
155
156 typecheck_result_add_identifier(Id,tr(Errors,Rules,[Id|Ids],Flags),tr(Errors,Rules,Ids,Flags)).
157
158 %typecheck_max_errors_exceeded(tr(_,_,_,Flags)) :-
159 % member(error_count(N,Max,_),Flags),number(N),number(Max),N>Max.
160
161 typecheck_result_get_errors(tr(FullErrors,_DR,_Ids,Flags),RestErrors) :-
162 ((member(error_count(N,Max,LastPos),Flags),number(N),number(Max),N>Max)
163 -> tools:ajoin(['Maximum number (',Max,') of type errors exceeded: ',N],Msg),
164 ExcErr=error(Msg,LastPos),
165 %append(Errors,[ExcErr],FullErrors)
166 FullErrors = [ExcErr|RestErrors]
167 ; FullErrors = RestErrors).
168
169 typecheck_result_get_delayed_rules(tr(_Errors,Rules,_Ids,_Flags),Rules).
170
171 typecheck_result_get_identifiers(tr(_Errors,_Rules,Ids,_Flags),Ids).
172
173 %typecheck_result_finalize(tr([],[],[])). % not used at the moment
174
175 typecheck_result_get_flags(tr(_,_,_,Flags),Flags).
176
177 typecheck_add_flag(Flag,tr(Errors,Rules,Ids,Flags),tr(Errors,Rules,Ids,NewFlags)) :-
178 (member(Flag,Flags) -> NewFlags=Flags ; NewFlags=[Flag|Flags]).
179
180 % btype/7 is the central predicate of the type-checker
181 % type-checking is done in three "stages":
182 % btype/5: extracts the obligatory position information from the input syntax element
183 % decouples the type in the argument and the type of the expression by
184 % an explicit unify_types/5 call
185 % calls btype1
186 % btype1/7: calls btype_rewrite for optional rewriting rules
187 % if no more rewriting rules can be applied, btype2 is called
188 % btype2/7: does the actual type-checking
189
190 % btype(+Src,+Ext,+Env,Type,-Result,TRin,TRout):
191 % Src: Where the call comes from
192 % Ext: The AST of the expression to type check as it comes from the parser
193 % Env: The type environment (see the env_... predicates)
194 % Type: The type of the expression (could be as input or output)
195 % Result: The type checked AST
196 % TRin/TRout: typecheck_result data structure, see typecheck_result_... predicates
197 btype(Src,Ext,Env,Type,Result,TRin,TRout) :-
198 (var(Ext)
199 -> add_internal_error('btype Ext is variable: ',Src:Ext)
200 ; true),
201 if(btype_aux(Ext,Env,Type,Result,TRin,TRout),true,
202 add_error_and_fail(btype,'btype failed: ',Src:Ext)
203 %(add_error(btype,'btype failed: ',Src:Ext),trace, btype_aux(Ext,Env,Type,Result,TRin,TRout))
204 ),
205 (var(TRout) -> add_error(btype,'TRout is variable: ',Src:Ext) ; true).
206
207 btype_aux(Ext,Env,Type,Result,TRin,TRout) :-
208 % convert the external representation Ext (first argument is the position)
209 % into the typed representation
210 ext2int(btype,Ext,Expr,Pos,Type,TExpr,Infos,Result0),
211 % type-check the expression
212 btype1(Expr,Pos,Env,TExpr,LType,Infos,NewPos,TRin,TR1),
213 % an explicit unify decouples the expected and inferred type
214 (Pos\=NewPos
215 -> %debug_println(19,updating_position_info(Pos,NewPos)),
216 update_pos(Result0,NewPos,Result)
217 ; Result = Result0),
218 unify_types(Type,LType,Pos,TExpr,TR1,TRout).
219
220 update_pos(b(R0,T,Infos),NewPos,b(R0,T,[nodeid(NewPos)|Infos0])) :-
221 delete(Infos,node_id(_),Infos0).
222
223 % btype1/7 tries to apply rewriting rules until no more rules
224 % are applyable, then btype2/7 is called
225 % btype1(+Expr,+Pos,+Env,-TExpr,-Type,-Infos,-NewPos,+TRin,-TRout):
226 % NewPos: potentially updated position information when definitions are expanded
227 btype1(Expr,Pos,Env,TExpr,Type,Infos,NewPos,TRin,TRout) :-
228 catch( btype_try_rewrite(Expr,Pos,Env,TExpr,Type,Infos,NewPos,TRin,TRout),
229 E,
230 handle_rewrite_exception(E,Pos,TExpr,Infos,TRin,TRout)
231 ).
232 btype_try_rewrite(Expr,Pos,Env,TExpr,Type,Infos,NewPos2,TRin,TRout) :-
233 btype_rewrite(Expr,Env,Pos,NewExpr,NewPos),!,
234 btype1(NewExpr,NewPos,Env,TExpr,Type,Infos,NewPos2,TRin,TRout).
235 btype_try_rewrite(Expr,Pos,Env,TExpr,Type,Infos,Pos,TRin,TRout2) :-
236 btype2(Expr,Pos,Env,TExpr,Type,Infos,TRin,TRout1),
237 btype_static_check(TExpr,Pos,Env,TRout1,TRout2).
238
239 % a few static checking rules
240 btype_static_check(let(IDList,Equalities,_Body),Pos,Env) -->
241 btype_static_check_let(IDList,Equalities,Pos,no_reuse,Env). % here Atelier-B prohibits reuse
242 btype_static_check(let_expression(IDList,Equalities,_Body),Pos,Env) -->
243 btype_static_check_let(IDList,Equalities,Pos,allow_reuse,Env). % here we allow reuse
244 btype_static_check(let_predicate(IDList,Equalities,_Body),Pos,Env) -->
245 btype_static_check_let(IDList,Equalities,Pos,allow_reuse,Env).
246 btype_static_check(_,_,_) --> [].
247
248 btype_static_check_let(IDList,Equalities,Pos,AllowReuse,Env,TRin,TRout) :-
249 def_get_texpr_ids(IDList,Ids), sort(Ids,SIds),
250 check_let_equalities(Equalities,Pos,AllowReuse,SIds,[],NotDefined,_Defined,Env,TRin,TRout1),
251 (NotDefined==[] -> TRout = TRout1
252 ; type_error_or_warning_occurred(TRin,TRout1) ->
253 format(user_error,'*** Let does not define variables: ~w~n',[NotDefined]),
254 TRout1 = TRout % we have already raised errors
255 ; %print(tr(TRin)),nl,print(tr(TRout1)),nl,
256 ajoin_with_sep(['Let does not define variables:'|NotDefined],' ',Msg),
257 store_typecheck_error(Msg,Pos,TRout1,TRout)).
258
259
260 % AllowReuse: allow let identifiers to be re-used in later RHS sides; normally not allowed by Atelier-B
261 check_let_equalities(b(P,T,I),Pos,AllowReuse,ToDefine,AlreadyDefined,T2,A2,Env) -->
262 check_let_equalities_aux(P,T,I,Pos,AllowReuse,ToDefine,AlreadyDefined,T2,A2,Env).
263 check_let_equalities_aux(P,Type,Info,Pos,AR,_,_,_,_,_) -->
264 {var(P)},!,
265 {add_internal_error('Illegal variable:',check_let_equalities_aux(P,Type,Info,Pos,AR,_,_,_,_,_))}.
266 check_let_equalities_aux(conjunct(L,R),_,_,Pos,AllowReuse,ToDefine,AlreadyDefined,T2,A2,Env) --> !,
267 check_let_equalities(L,Pos,AllowReuse,ToDefine,AlreadyDefined,T1,Already1,Env),
268 check_let_equalities(R,Pos,AllowReuse,T1,Already1,T2,A2,Env).
269 check_let_equalities_aux(equal(LHS,RHS),_,_,_Pos,AllowReuse,ToDefine,AlreadyDefined,T2,A2,Env) -->
270 {get_texpr_id(LHS,LID)},
271 %{print(equal(LID,ToDefine,AlreadyDefined,T2,A2)),nl},
272 {select(LID,ToDefine,T2)}, % OK: we define an introduced ID
273 !,
274 {ord_add_element(AlreadyDefined,LID,A2)},
275 {find_identifier_uses(RHS,[],Used)}, % can we already call this here ?? TO DO Check non-ground typing does not cause problem
276 check_let_rhs(RHS,Used,ToDefine,AlreadyDefined,AllowReuse,Env).
277 check_let_equalities_aux(equal(LHS,RHS),Type,Info,Pos,_AllowReuse,T,A,T,A,_Env,TrIn,TrOut) :-
278 translate_bexpression(b(equal(LHS,RHS),Type,Info),IStr), % are the types guaranteed to be instantiated ?
279 (get_texpr_id(LHS,LID)
280 -> (member(LID,A) -> Msg1 = 'LET redefines identifier: '
281 ; Msg1 = 'LET defines undeclared identifier: '
282 )
283 ; Msg1 = 'LET contains an equality whose left-hand-side is not an identifier: '),
284 ajoin([Msg1,IStr],Msg),
285 (get_texpr_pos(LHS,PosM) -> true ; PosM=Pos),
286 store_typecheck_error(Msg,PosM,TrIn,TrOut).
287 check_let_equalities_aux(IllegalPred,Type,Info,_Pos,_AllowReuse,T,A,T,A,_Env) -->
288 {translate_bexpression(b(IllegalPred,Type,Info),IStr),
289 ajoin(['LET contains a predicate which is not an equality: ',IStr],Msg)},
290 store_typecheck_error(Msg,Info).
291
292 :- use_module(specfile,[z_mode/0]).
293 check_let_rhs(_RHS,Used,ToDefine,AlreadyDefined,_AllowReuse,Env) --> {z_mode}, !,
294 % We do not seem to call this code in Z Mode !
295 ({ord_union(ToDefine,AlreadyDefined,All),
296 possible_ambiguity(Used,All,Env,ClashIds)}
297 -> {format('*** Warning: possible clash in LET: ~w~n',[ClashIds])}
298 ; []
299 ).
300 check_let_rhs(RHS,Used,ToDefine,AlreadyDefined,no_reuse,_Env) -->
301 {get_preference(allow_let_to_reuse_introduced_ids,false)},
302 {ord_union(ToDefine,AlreadyDefined,All), ord_intersection(Used,All,Inter)},
303 {Inter\=[]},
304 !,
305 % potentially cyclic let
306 {ajoin_with_sep(['LET right-hand-side uses left-hand introduced ids (set ALLOW_COMPLEX_LETS to TRUE to allow this):'|Inter],' ',Msg),
307 get_texpr_info(RHS,Info)},
308 store_typecheck_error(Msg,Info).
309 check_let_rhs(RHS,Used,ToDefine,_AlreadyDefined,allow_reuse,_Env) -->
310 {ord_intersection(Used,ToDefine,Inter), Inter \= []}, % we use left-hand side ID not yet introduced
311 !,
312 % potentially cyclic let
313 {ajoin_with_sep(['LET right-hand-side uses not-yet-defined identifiers:'|Inter],' ',Msg),
314 get_texpr_info(RHS,Info)},
315 store_typecheck_error(Msg,Info).
316 check_let_rhs(RHS,Used,_ToDefine,AlreadyDefined,allow_reuse,Env) -->
317 {possible_ambiguity(Used,AlreadyDefined,Env,ClashIds)},
318 % we use variables which are visible and introduced: could be very confusing
319 !,
320 {ajoin_with_sep(['Possible ambiguity: LET right-hand-side re-uses visible identifiers:'|ClashIds],' ',Msg),
321 get_texpr_info(RHS,Info)},
322 store_typecheck_error(Msg,Info).
323 check_let_rhs(_,_,_,_,_,_) --> [].
324
325 possible_ambiguity(Used,AlreadyDefined,Env,ClashIds) :-
326 env_get_visible_ids(Env,Visible),
327 ord_intersection(Used,AlreadyDefined,Inter1),
328 ord_intersection(Inter1,Visible,ClashIds),
329 ClashIds \= [].
330
331 handle_rewrite_exception(rewrite_exception(Msg,Name),Pos,TExpr,Infos,TRin,TRout) :- !,
332 store_typecheck_error(Msg,Pos,TRin,TRout),
333 % Type remains unbound, Infos are empty
334 Infos = [],
335 TExpr = identifier(Name).
336 handle_rewrite_exception(E,_Pos,_TExpr,_Infos,_TRin,_TRout) :- throw(E).
337
338 % btype2/8 encodes the type checking rules
339 btype2(identifier(I1), Pos, Env, identifier(I), Type, Infos, TRin, TRout) :-
340 !, % In case the identifier is a list, join it with '.' (e.g. ['M',x] -> 'M.x')
341 ( is_list(I1) -> ajoin_with_sep(I1,'.',I)
342 ; otherwise -> I1=I),
343 % get the identifier's type from the type environment
344 lookup_type(I,Env,Pos,Type,TRin,TR1),
345 % copy also additional information from the environment,
346 lookup_infos(I,Env,AllInfos),
347 % but not all (e.g. no position information)
348 extract_id_information(AllInfos,Infos),
349 % an access to this identifier might be illegal, check this
350 ( member(error(Error),AllInfos) -> store_typecheck_error(Error, Pos, TR1, TRout)
351 ; otherwise -> TR1=TRout).
352 btype2(primed_identifier(Id,N), Pos, Env, identifier(FullId), Type, Infos, TRin, TRout) :-
353 !, % a primed identifier is of the form x$0, we just convert it to
354 % a normal identifier called "x$0" and type-check it.
355 number_suffix(Id,N,FullId),
356 btype(primed_identifier(Id,N),identifier(Pos,FullId),Env,Type,TId,TRin,TRout),
357 get_texpr_info(TId,Infos).
358 btype2(forall(Ids,EImplication), _, Env, forall(TIdentifiers,TDomain,TPred), pred, [], TRin, TRout) :-
359 !,add_ext_variables_with_info(Ids,Env,[introduced_by(forall)],TIdentifiers,Subenv,TRin,TR1),
360 ext2int(btype2,EImplication,Implication,IPos,_,_,_,_),
361 (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
362 ; Implication2=Implication, IPos2=IPos),
363 % we expect an implication as predicate, if not, generate an error
364 ( Implication2=implication(Domain,Pred) ->
365 btype(forall_domain(Ids),Domain,Subenv,pred,TDomain,TR1,TR2),
366 btype(forall_pred(Ids),Pred,Subenv,pred,TPred,TR2,TRout)
367 ; otherwise ->
368 store_typecheck_error('expected implication in universal quantification ',IPos2,TR1,TR2),
369 create_texpr(truth,pred,[],TDomain),
370 btype(foralle_impl(Ids),EImplication,Subenv,pred,TPred,TR2,TRout)
371 ).
372 btype2(external_function_call(FunName,FunParams,_FunDef,TypeParams,Decl), Pos, Env,
373 external_function_call(FunName,TFunParams), OutputType , [], TRin, TRout) :-
374 /* note: position info is automatically added to info field; hence [] ok */
375 (FunParams = [] -> InputType = empty_type, FullType = set(OutputType)
376 ; FullType = set(set(couple(InputType,OutputType)))),
377 !, btype_external_call(FunName,TypeParams,FunParams,Decl,FullType,
378 InputType,Pos,Env,TFunParams,TRin,TRout).
379 btype2(external_pred_call(FunName,FunParams,_FunDef,TypeParams,Decl), Pos, Env,
380 external_pred_call(FunName,TFunParams), pred, [], TRin, TRout) :-
381 !, btype_external_call(FunName,TypeParams,FunParams,Decl,set(InputType),InputType,
382 Pos,Env,TFunParams,TRin,TRout).
383 btype2(external_subst_call(FunName,FunParams,_FunDef,TypeParams,Decl), Pos, Env,
384 external_subst_call(FunName,TFunParams), subst, [], TRin, TRout) :-
385 !, btype_external_call(FunName,TypeParams,FunParams,Decl,set(InputType),InputType,
386 Pos,Env,TFunParams,TRin,TRout).
387 btype2(integer(I), _, _, integer(I), integer, [], TR, TR) :- !.
388 btype2(integer_set(S), _, _, integer_set(S), set(integer), [], TR, TR) :- !.
389 btype2(string(I), _, _, string(I), string, [], TR, TR) :- !, assert_machine_string(I).
390 btype2(assign(IdFuns,Exprs), Pos, Env, assign(TIdFuns,TExprs), subst, [], TRin, TRout) :-
391 !,
392 common_prefix(IdFuns,Exprs,IdFuns1,Exprs1,OK),
393 btype_l(IdFuns1,Env,Types,TIdFuns,TRin,TR1),
394 btype_l(Exprs1, Env,Types,TExprs, TR1, TR2),
395 foldl(check_assign_lhs(Env),TIdFuns,TR2,TR3),
396 ( OK=same_length -> TRout=TR3
397 ; otherwise ->
398 store_typecheck_error('different number of variables on left and right side of a substitution ',Pos,TR3,TRout)
399 ).
400 btype2(becomes_element_of(Ids,Expr), _, Env, becomes_element_of(TIds,TExpr), subst, [], TRin, TRout) :-
401 !,btype_l(Ids,Env,Types,TIds,TRin,TR1),
402 foldl(check_assign_lhs(Env),TIds,TR1,TR2),
403 couplise_list(Types,Type),
404 btype(becomes_element_of(Ids),Expr,Env,set(Type),TExpr,TR2, TRout).
405 btype2(becomes_such(Ids,Pred), _, Env, becomes_such(TIds,TPred), subst, [], TRin, TRout) :-
406 !,btype_l(Ids,Env,_,TIds,TRin,TR1),
407 foldl(check_assign_lhs(Env),TIds,TR1,TR2),
408 % for each LHS identifier x (in Ids), we add an identifier of the form
409 % x$0 with the same type to the environment
410 foldl(add_primed_id,TIds,Env,Subenv),
411 btype(becomes_such,Pred,Subenv,pred,TPred,TR2,TRout).
412 btype2(evb2_becomes_such(Ids,Pred), _, Env, evb2_becomes_such(TIds,TPred), subst, [], TRin, TRout) :-
413 !,check_evb_becomes_such(evb2_becomes_such,Ids,Pred,Env,TIds,TPred,TRin,TRout).
414 btype2(operation_call(Op,Res,Args), Pos, Env, TOp, subst, Infos, TRin, TRout) :-
415 %print(opcall(Op)),nl, portray_env(Env),nl,
416 !,type_operation_call(Op,Res,Args,Pos,Env,TOp,Infos,TRin,TRout).
417 btype2(operation_call_in_expr(Op,Args), Pos, Env, operation_call_in_expr(TOp,TArgs), Type, Infos, TRin, TRout) :-
418 !, ext2int(btype2_opcall,Op,identifier(Opid),IPos,_,_,_,_),
419 btype2(identifier(op(Opid)),IPos,Env,identifier(OpId),op(ArgTypes,ResTypes),OpInfos,TRin,TR1),
420 create_texpr(identifier(OpId),subst,OpInfos,TOp),
421 btype_l(Args,Env,ArgTypes,TArgs,TR1,TR2),
422 couplise_list(ResTypes,Type),
423 get_operation_infos(OpInfos,Infos),
424 %print(op_call_in_expr(Opid,Infos)),
425 ( memberchk(modifies(Modifies),Infos) ->
426 (Modifies==[] -> TR2=TRout
427 ; var(Modifies) -> TR2=TRout,
428 % the info has not yet been computed; add a co-routine (which must however raise error immediately)
429 when(nonvar(Modifies),(Modifies==[] -> true
430 ; add_error(btype2,'query-operation expected when calling operation in expressions ',Opid,Pos)))
431 ; otherwise -> print(error(Infos)),nl, store_typecheck_error('query-operation expected when calling operation in expressions ',Pos,TR2,TRout)
432 )
433 ; add_internal_error(btypechecker,'Missing modifies info field:',operation_call_in_expr(Op,Args),Pos),TR2=TRout
434 ).
435 btype2(case(Expr,Eithers,Else), _, Env, case(TExpr,TEithers,TElse), subst, [], TRin, TRout) :-
436 !,btype(case,Expr,Env,Type,TExpr,TRin,TR1),
437 foldl(btype_caseor(Env,Type),Eithers,TEithers,LExprs,TR1,TR2),
438 append(LExprs,Exprs),
439 btype(case_else,Else,Env,subst,TElse,TR2,TR3),
440 % The next check could be made dependend on a preference (non-literal values allowed in
441 % CASE statements), in that case add TR3=TRout as an alternative
442 check_case_expressions(Exprs,TR3,TRout).
443 btype2(struct(Fields), Pos, Env, struct(TRecord), set(RType), [], TRin, TRout) :-
444 !, btype(struct,rec(Pos,Fields),Env,_,TRecord,TRin,TR1),
445 get_texpr_expr(TRecord,rec(TFields)),
446 foldl(extract_field_type,TFields,FieldTypes,TR1,TR2),
447 normalise_record_type(record(FieldTypes),RType),
448 TR2=TRout.
449 % (record_has_multiple_field_names(FieldTypes,FieldName) %% error already raised by rec(.) clause below
450 btype2(rec(Fields), Pos, Env, rec(TFields), RType, [], TRin, TRout) :-
451 !, foldl(btype_field_rec(Env),Fields,FTypes,TFields1,TRin,TR2),
452 normalise_record_type(record(FTypes),RType),
453 % we sort the field arguments here, so we do not have to normalise them every
454 % time in the interpreter
455 RType = record(NormedFieldTypes),
456 sort_record_fields(NormedFieldTypes,TFields1,TFields),
457 (record_has_multiple_field_names(NormedFieldTypes,FieldName)
458 -> ajoin(['Field ',FieldName,' used multiple times in record '],Msg),
459 store_typecheck_error(Msg,Pos,TR2,TRout)
460 ; TR2=TRout
461 ).
462 btype2(record_field(Record,I), Pos, Env, record_field(TRecord,Id), Type, [], TRin, TRout) :-
463 !,btype(record_field,Record, Env, RType, TRecord, TRin, TR1),
464 remove_pos(I,identifier(Id)),
465 unify_types(record([field(Id,Type)|_]),RType,Pos,TRecord,TR1,TRout).
466 btype2(refined_operation(Id,Results,Args,_RefinesID,Body), Pos, Env, TExpr, Type, Infos, TRin, TRout) :-
467 !, % TO DO: do we need to treat RefinesID ?
468 btype2(operation(Id,Results,Args,Body), Pos, Env, TExpr, Type, Infos, TRin, TRout).
469 btype2(operation(Id,Results,Args,Body), Pos, Env, operation(TId,TResults,TArgs,TBody), Type,
470 Infos, TRin, TRout) :-
471 %print(checking_op(Id)),nl,
472 !, %debug_stats(checking_operation(Id,Args)),
473 % type-check the identifier to look up the operation's type
474 % in the environment.
475 % we call ext2int and btype2/7 directly instead of going over
476 % btype/5, because we use op(Name) instead of Name to look up
477 % the type. This is done to seperate operation and variable name
478 % spaces (Note: that was a stupid and ugly hack)
479 ext2int(btype2_operation,Id,identifier(Opid),IPos,Type,Topid,IdInfos,TId),
480 btype2(identifier(op(Opid)),IPos,Env,Topid,Type,IdInfos,TRin,TR0),
481 % introduce a sub-environment Subenv by adding the argument and
482 % result variables
483 check_for_duplicate_raw_ids(Results,[],'results for operation ',Opid,FilteredResults,TR0,TR1),
484 add_ext_variables_with_info(FilteredResults,Env,[introduced_by(operation)],TResults,Subenv1,TR1,TR2),
485 check_for_duplicate_raw_ids(Args,[],'arguments for operation ',Opid,FilteredArgs,TR2,TR2b),
486 add_ext_variables_with_info(FilteredArgs,Subenv1,[readonly,introduced_by(operation)],TArgs,Subenv,TR2b,TR3),
487 % get their types and determine the resulting operation's type
488 get_texpr_types(TResults,LResultTypes),
489 get_texpr_types(TArgs,LArgTypes),
490 unify_types(op(LArgTypes,LResultTypes),Type,Pos,TId,TR3,TR4),
491 % type the operation's body in the sub-environment
492 btype(operation(Id),Body, Subenv, subst, TBody, TR4, TRout),
493 % the list of modified machine variables is the list of changed
494 % variables by the substitutions in the body minus the result variables
495 compute_accessed_vars_infos_for_operation(Id,TResults,TArgs,TBody,Modifies,Reads,NonDetModified,Infos),
496 %assert(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 !!]
497 % make sure that the List of modified variables of this operation
498 % is also up-to-date in the type environment
499 (memberchk(modifies(EnvModifies),IdInfos),
500 memberchk(reads(EnvReads),IdInfos),
501 memberchk(non_det_modifies(EnvNonDetModifies),IdInfos) ->
502 % Check if the environment variables and the local variables are unifiable.
503 % If not, an operation with the same name must have been defined before
504 % We can ignore this, later an error message will be raised.
505 ( EnvModifies=Modifies -> true; add_message(btypechecker,'Conflict in modifies info for ',Id,IPos)),
506 ( EnvReads=Reads -> true; add_message(btypechecker,'Conflict in reads info for ',Id,IPos)),
507 ( EnvNonDetModifies=NonDetModified -> true; add_message(btypechecker,'Conflict in non_det_modifies info for ',Id,IPos))
508 ; add_error(btypechecker,'Cannot store modifies/reads info for: ',Opid,IPos)
509 ),
510 debug_format(9,'Finished checking operation ~w, reads:~w, writes=~w~n',[Id,Reads,Modifies]).
511 btype2(while(Pred,Body,Inv,Var), _, Env, while(TPred,TBody,TInv,TVar), subst, FullInfo, TRin, TRout) :- !,
512 btype(while,Pred,Env,pred,TPred,TRin,TR1),
513 btype(while_body,Body,Env,subst,TBody,TR1,TR2),
514 % In contrast to the other substitutions, in the invariant and variant
515 % part of a while loop it is possible to reference abstract variables,
516 % as they are not used to influence the behaviour of the substitution.
517 % We create a new environment InvEnv where those access restrictions are
518 % removed.
519 allow_access_to_abstract_vars(Env,InvEnv),
520 add_primed_old_value_variables(InvEnv,PInvEnv),
521 btype(while_inv,Inv,PInvEnv,pred,TInv,TR2,TR3),
522 btype(while_variant,Var,InvEnv,integer,TVar,TR3,TRout),
523 % tag this statement with an appropiate info if a reference to the original value
524 % of a variable is made in the invariant.
525 % This info is used in the clean_up (see b_ast_cleanup) to insert a LET statement.
526 check_for_old_state_references(TInv,Info),
527 FullInfo = [modifies(Modifies),reads(AllReads)|Info],
528 % TO DO: ideally we should compute those in one go for all substitutions:
529 % here we compute information again which we have already computed for operations
530 get_accessed_vars(b(while(TPred,TBody,TInv,TVar),subst,Info),[],Modifies,_NonDetModifies,Reads),
531 (debug:debug_mode(off) -> true
532 ; format('WHILE Reads : ~w~n Modifies : ~w~n',[Reads,Modifies]),
533 print('VARIANT: '),translate:print_bexpr(TVar),nl
534 ),
535 (member(refers_to_old_state(SortedRefs),Info)
536 -> findall(Primed,member(oref(Primed,_,_),SortedRefs),PrimedDollarVars), sort(PrimedDollarVars,SPDV),
537 ord_union(SPDV,Reads,AllReads) %, print(add(SPDV,Reads)),nl
538 ; AllReads = Reads).
539
540 btype2(parallel(Substs),Pos,Env,parallel(TSubsts), subst, [], TRin, TRout) :-
541 !, btype_l(Substs,Env,_,TSubsts,TRin,TR1),
542 check_no_double_assignment(TSubsts,Pos,TR1,TRout).
543 btype2(minus_or_set_subtract(A,B), Pos, Env, minus_or_set_subtract(TA,TB), Type, [], TRin, TRout) :-
544 !,btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
545 delayed_type_minus(TypeA,TypeB,Type,Pos,A,B,TR1,TRout).
546 btype2(concat(A,B), Pos, Env, concat(TA,TB), Type, [], TRin, TRout) :-
547 get_preference(allow_sequence_operators_on_strings,true),
548 btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
549 TypeA \== integer, % otherwise trigger error_rewrite below for exponentiation
550 !,
551 delayed_type_string_or_seq(TypeA,TypeB,Type,Pos,A,B,TR1,TRout).
552 % TO DO: also treat size(.) in a similar way
553 btype2(mult_or_cart(A,B), Pos, Env, mult_or_cart(TA,TB), Type, [], TRin, TRout) :-
554 !,btype_l([A,B],Env,[TypeA,TypeB],[TA,TB],TRin,TR1),
555 delayed_type_times(TypeA,TypeB,Type,Pos,A,B,TR1,TRout).
556 btype2(substitution(Subst,Pred), _Pos, Env, TSubst, pred, [], TRin, TRout) :-
557 !, type_substitution_expression(Subst,Pred,Env,TSubst,TRin,TRout).
558 btype2(extended_expr(Id,Args,Args2), Pos, Env, Result, Type, [was_operator(Id)|Info], TRin, TRout) :-
559 !, lookup_eventb_operator(Id,Args,Args2,Pos,Env,expr,Result,Type,Info,TRin,TRout).
560 btype2(extended_pred(Id,Args,Args2), Pos, Env, Result, Type, [was_operator(Id)|Info], TRin, TRout) :-
561 !, lookup_eventb_operator(Id,Args,Args2,Pos,Env,pred,Result,Type,Info,TRin,TRout).
562 btype2(recursive_let(Id,Set),_Pos,Env,recursive(TId,TSet),set(Type),[],TRin,TRout) :- !,
563 add_ext_variables([Id], Env, [TId], SubEnv, TRin, TR1),
564 get_texpr_type(TId,set(Type)),
565 btype(recursive,Set,SubEnv,set(Type),TSet,TR1,TRout).
566 btype2(set_extension(RawIntegers),_Pos,_Env,value(V),set(Type),[],TR,TR) :-
567 % optimisation: is this a set of integers or pair of integers?
568 % -> skip type checking the content and just generate an AVL set directly
569 simple_set_extension_type(RawIntegers,Type),
570 maplist(read_raw_integers(Type),RawIntegers,Integers),!,
571 custom_explicit_sets:convert_to_avl(Integers,V).
572 btype2(typeset,_Pos,_Env,typeset,set(_),[],TR,TR) :- !.
573 btype2(typeof(InnerExpr,TypeExpr),_Pos,Env,Expr,Type,Info,TRin,TRout) :-
574 !, btype(typeof,TypeExpr,Env,set(Type),_TTypeExpr,TRin,TR1),
575 btype(typeof,InnerExpr,Env,Type,TExpr,TR1,TRout),
576 get_texpr_expr(TExpr,Expr),get_texpr_info(TExpr,Info).
577 btype2(Expr, Pos, Env, TExpr, Type, [], TRin, TRout) :-
578 % this is the most simple case of a type-check
579 safe_functor(btype2_expr,Expr,Functor,Arity),
580 safe_functor(btype2_lookup,Lookup,Functor,Arity),
581 Lookup :: Type,
582 !,
583 safe_functor(btype2_texpr,TExpr,Functor,Arity),
584 type_and_unify_args(1,Arity,Pos,Env,Expr,Lookup,TExpr,TRin,TRMid),
585 (\+ type_error_or_warning_occurred(TRin,TRMid)
586 -> TRMid = TRout
587 ; typecheck_result_get_flags(TRMid,Flags),
588 nonmember(try_rewrite,Flags),
589 typecheck_add_flag(try_rewrite,TRMid,TRMid0), % avoid an exponential blow-up in rewrites; we only do one rewrite at a time
590 %print(try_rewrite(Expr)),nl,
591 error_rewrite(Expr,RewrittenExpr,RewriteMsg), % a common user error may be present
592 % print(rewrite(RewrittenExpr)),nl,
593 % Copy the code from above; we assume
594 copy_term(TRMid0,TRMid1), % copy error variable; avoid instantiating TRMid with error msgs from RewrittenExpr
595 btype2(RewrittenExpr,Pos,Env,_,_,[],TRMid1,TRMid2),
596 %safe_functor(btype2_expr,RewrittenExpr,Functor2,Arity2),
597 %safe_functor(btype2_lookup,Lookup2,Functor2,Arity2),
598 %Lookup :: Type, print(rewritten_t(Lookup,Type)),nl,
599 % safe_functor(btype2_texpr,TExpr2,Functor2,Arity2),
600 %type_and_unify_args(1,Arity2,Pos,Env,RewrittenExpr,Lookup2,TExpr2,TRMid1,TRMid1),
601 % print(rewrite_ok(TRMid1)),nl,
602 \+ type_error_or_warning_occurred(TRMid1,TRMid2) % the rewrite removed the type error
603 -> ajoin(['Did you ',RewriteMsg,' ?'],Msg),
604 store_typecheck_error(Msg,Pos,TRMid,TRout)
605 ; %print(no_rule_applicable),nl,
606 TRMid=TRout).
607
608 % merge the pragma ast nodes into the info fields
609 btype2(label(Label,Node), _Pos, Env, TExpr, Type, InfosOut, TRin, TRout) :- !,
610 btype(label, Node, Env, Type, Result, TRin, TRout),
611 get_texpr_expr(Result,TExpr),
612 get_texpr_info(Result,Infos),
613 add_label_to_infos(Infos,Label,InfosOut).
614 btype2(description(Desc,Node), _Pos, Env, TExpr, Type, [description(Desc)|Infos], TRin, TRout) :- !,
615 btype(description, Node, Env, Type, Result, TRin, TRout),
616 get_texpr_expr(Result,TExpr),
617 get_texpr_info(Result,Infos).
618 btype2(symbolic_comprehension_set(A,B), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !,
619 btype2(comprehension_set(A,B), Pos, Env, TExpr, Type, Infos, TRin, TRout).
620 btype2(symbolic_quantified_union(A,B,C), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !,
621 btype2(quantified_union(A,B,C), Pos, Env, TExpr, Type, Infos, TRin, TRout).
622 btype2(symbolic_lambda(A,B,C), Pos, Env, TExpr, Type, [prob_annotation('SYMBOLIC')|Infos], TRin, TRout) :- !,
623 btype2(lambda(A,B,C), Pos, Env, TExpr, Type, Infos, TRin, TRout).
624 btype2(conversion(Node), _Pos, Env, TExpr, Type, [conversion|Infos], TRin, TRout) :- !,
625 btype(conversion, Node, Env, Type, Result, TRin, TRout),
626 get_texpr_expr(Result,TExpr),
627 get_texpr_info(Result,Infos).
628 btype2(let_predicate(Ids,Equalities,Pred), Pos, Env, let_predicate(TIdsOut,TExprsOut,TPred), pred, [], TRin, TRout) :- !,
629 check_for_duplicate_raw_ids(Ids,[],'LET arguments','',FIds,TRin,TR0),
630 add_ext_variables_with_info(FIds,Env,[introduced_by(let_predicate)],TIds,Subenv,TR0,TR1),
631 btype(let_predicate, Equalities, Subenv, pred, TEqualities, TR1, TR2), % should we introduced variables only one by one ?
632 btype(let_predicate, Pred, Subenv, pred, TPred, TR2, TR3),
633 btype_static_check_let(TIds,TEqualities,Pos,allow_reuse,Env,TR3,TR4),
634 split_let_equalities_into_ids_and_expressions(Ids,TEqualities,TIdsOut,TExprsOut,Pos,TR4,TRout).
635 btype2(let_expression(Ids,Equalities,Expr), Pos, Env, let_expression(TIdsOut,TExprsOut,TExpr), Type, [], TRin, TRout) :- !,
636 check_for_duplicate_raw_ids(Ids,[],'LET arguments','',FIds,TRin,TR0),
637 add_ext_variables_with_info(FIds,Env,[introduced_by(let_expression)],TIds,Subenv,TR0,TR1),
638 btype(let_expression, Equalities, Subenv, pred, TEqualities, TR1, TR2),
639 btype(let_expression, Expr, Subenv, Type, TExpr, TR2, TR3),
640 btype_static_check_let(TIds,TEqualities,Pos,allow_reuse,Env,TR3,TR4),
641 split_let_equalities_into_ids_and_expressions(Ids,TEqualities,TIdsOut,TExprsOut,Pos,TR4,TRout).
642 % error case. should not be reached
643 btype2(Expr, _Pos, _, _, _, _, TR, TR) :-
644 safe_functor(btype2_uncovered,Expr,F,Arity),
645 add_internal_error('Uncovered construct in type checker: ',F/Arity),
646 fail.
647
648
649 compute_accessed_vars_infos_for_operation(_Id,TResults,TArgs,TBody,Modifies,Reads,NonDetModified,Infos) :-
650 append(TResults,TArgs,TLocals),
651 get_texpr_ids(TLocals,Locals), list_to_ord_set(Locals,SLocals),
652 get_accessed_vars(TBody,[],AllModifies,AllNonDetModified,AllReads), % we now no longer pass Locals, we filter out later
653 %print(modified_reads(Opid,AllModifies,AllReads)),nl,
654 %print(nondet(Id,AllNonDetModified,SLocals,IdInfos)),nl,
655 ord_subtract(AllModifies,SLocals,Modifies),
656 ord_subtract(AllReads,SLocals,Reads),
657 ord_subtract(AllNonDetModified,SLocals,NonDetModified),
658 ord_intersection(AllModifies,SLocals,LocalModifies),
659 ord_intersection(AllReads,SLocals,LocalReads),
660 Infos = [modifies(Modifies),reads(Reads),non_det_modifies(NonDetModified),
661 modifies_locals(LocalModifies),reads_locals(LocalReads)].
662
663 split_let_equalities_into_ids_and_expressions(RawIds,EqualitiesPred,IDs,Expressions,_,TR,TR) :-
664 conjunction_to_list(EqualitiesPred,ListOfEqualities),
665 split_let_equality_into_id_and_expression2(ListOfEqualities,IDs,Expressions,RawIds),
666 !.
667 split_let_equalities_into_ids_and_expressions(_,EQs,[],[],Pos,TRIn,TROut) :-
668 translate_bexpression(EQs,PPEqs),
669 ajoin_with_sep(['Let equalities could not be split into ids and expressions:',PPEqs],' ',Msg),
670 store_typecheck_error(Msg,Pos,TRIn,TROut).
671
672 split_let_equality_into_id_and_expression2([],[],[],_).
673 split_let_equality_into_id_and_expression2([Equality|TE],[TID|TI],[Expression|TEs],RawIds) :-
674 get_texpr_expr(Equality,equal(TID,Expression)),
675 get_texpr_id(TID,ID), select(identifier(_,ID),RawIds,RawIds2),
676 !,
677 split_let_equality_into_id_and_expression2(TE,TI,TEs,RawIds2).
678 split_let_equality_into_id_and_expression2([_|TE],TI,TEs,RawIds) :-
679 split_let_equality_into_id_and_expression2(TE,TI,TEs,RawIds).
680
681 add_label_to_infos([],Label,[label([Label])]).
682 add_label_to_infos([label(LA)|T],Label,[label([Label|LA])|T]) :- !.
683 add_label_to_infos([F|T],Label,[F|TN]) :-
684 add_label_to_infos(T,Label,TN).
685
686 % check if a set extension is of type integer or couple(integer,...) by inspecting
687 % the first element
688 simple_set_extension_type([First,_|_],Type) :- % At least two elements
689 simple_set_extension_type2(First,Type). % of type integer or couple of integers
690 simple_set_extension_type2(integer(_,_),integer).
691 simple_set_extension_type2(couple(Pos,List),Type) :-
692 couplise_list_pos(List,Pos,Couple),
693 simple_set_extension_type2(Couple,Type).
694 simple_set_extension_type2(couple(_Pos,A,B),couple(TA,TB)) :-
695 simple_set_extension_type2(A,TA),
696 simple_set_extension_type2(B,TB).
697 % convert a raw integer or pairs of integers into a value
698 read_raw_integers(integer,integer(_Pos,I),int(I)).
699 read_raw_integers(couple(TA,TB),couple(_Pos,List),(VA,VB)) :-
700 read_raw_integer_couple(TA,VA,List,Rest),
701 read_raw_integer_couple(TB,VB,Rest,[]).
702 read_raw_integer_couple(integer,int(I)) --> [integer(_Pos,I)].
703 read_raw_integer_couple(couple(TA,TB),(VA,VB)) -->
704 read_raw_integer_couple(TA,VA),
705 read_raw_integer_couple(TB,VB).
706
707 % find common prefix of two lists (assigned variables, assigned expressions)
708 common_prefix([],[],[],[],Res) :- !, Res=same_length.
709 common_prefix([H1|T1],[H2|T2],[H1|TT1],[H2|TT2],OK) :- !,
710 common_prefix(T1,T2,TT1,TT2,OK).
711 common_prefix(_,_,[],[],not_same_length).
712
713 check_no_double_assignment(TSubsts,Pos,TRin,TRout) :-
714 maplist(modified_var,TSubsts,Mods),
715 ( (preferences:preference(allow_simultaneous_assignments,false),
716 find_common_variables(Mods,Var)) ->
717 ajoin(['Simultaneous assignment to variable ',Var],Msg),
718 store_typecheck_error(Msg,Pos,TRin,TRout)
719 ; otherwise ->
720 TRin = TRout).
721 modified_var(TSubst,Modified) :-
722 get_accessed_vars(TSubst,[],Modified,_NDModified,_Read).
723 find_common_variables([Vars|Rest],Var) :-
724 find_common_variables2(Rest,Vars,Var).
725 find_common_variables2([Vars|Vrest],Prior,Var) :-
726 ord_intersection(Vars,Prior,FoundVars),
727 ( memberchk(Var,FoundVars) -> true
728 ; otherwise ->
729 ord_union(Vars,Prior,NewVars),
730 find_common_variables2(Vrest,NewVars,Var)).
731
732 type_substitution_expression(Subst,Pred,Env,
733 let_predicate(TypedLhs,TypedRhs,TPred),TRin,TRout) :-
734 ( remove_pos(Subst,assign(Lhs,Rhs)) ->
735 ( same_length(Lhs,Rhs) ->
736 /* Typecheck the right side of the substitution */
737 btype_l(Rhs,Env,Types,TypedRhs,TRin,TR1),
738 /* The left site of the substitution introduces new variables which have the
739 same type as the corrresponding element of the RHS */
740 add_ext_variables_with_info(Lhs,Env,[introduced_by(let)],TypedLhs,SubEnv,TR1,TR2),
741 get_texpr_types(TypedLhs,Types),
742 /* Type the predicates in the sub-environment */
743 btype(substitution_expression,Pred,SubEnv,pred,TPred,TR2,TRout)
744 ; otherwise /* LHS hat not the same number of elements as RHS */ ->
745 ext2int(Subst,_,Pos,_,_,_,_),
746 TypedLhs=[], TypedRhs=[], create_texpr(truth,pred,[],TPred),
747 store_typecheck_error('Expected same number of elements on both sides of an assignment',
748 Pos,TRin,TRout))
749 ; otherwise /* Substitution is no assignment (the parser should not allow this) */ ->
750 add_internal_error('Expected assignment in substitution expression, but was: ',Subst),
751 fail).
752
753 delayed_type_minus(TypeA,TypeB,ResType,Pos,ExprA,ExprB,TRin,TRout) :-
754 arg(1,ExprA,PosA), arg(1,ExprB,PosB),
755 % In case of A-B=C we know that A, B and C have the same type
756 unify_types_l([ResType,ResType],[TypeA,TypeB],[PosA,PosB],TRin,TR1),
757 % but not if it is integer or set(_)
758 typecheck_result_add_delayed_rule(Trigger,Errors,TR1,TRout),
759 delayed_type_minus2(ResType,Trigger,Pos,Errors).
760 :- block delayed_type_minus2(-,-,?,?).
761 delayed_type_minus2(Type,_Trigger,Pos,Errors) :-
762 ( var(Type) ->
763 Errors = [error('Ambiguous expression (arithmetic minus or set minus?)',Pos)]
764 ; Type = integer ->
765 Errors = []
766 ; otherwise ->
767 unify_types_werrors_l([set(_)],[Type],[Pos],Errors,[])
768 ).
769
770 % allow a types to be either string or seq(A)
771 delayed_type_string_or_seq(TypeA,TypeB,ResType,Pos,ExprA,ExprB,TRin,TRout) :-
772 arg(1,ExprA,PosA), arg(1,ExprB,PosB),
773 % In case of A^B=C we know that A, B and C have the same type
774 unify_types_l([ResType,ResType],[TypeA,TypeB],[PosA,PosB],TRin,TR1),
775 % but not if it is integer or set(_)
776 typecheck_result_add_delayed_rule(Trigger,Errors,TR1,TRout),
777 delayed_type_string_or_seq2(ResType,Trigger,Pos,Errors).
778 :- block delayed_type_string_or_seq2(-,-,?,?).
779 delayed_type_string_or_seq2(Type,_Trigger,Pos,Errors) :-
780 ( %var(Type) -> Errors = [error('Ambiguous expression (seq(_) or string operator?)',Pos)] ;
781 Type == string ->
782 Errors = []
783 ; otherwise ->
784 unify_types_werrors_l([seq(_)],[Type],[Pos],Errors,[])
785 ).
786
787 % delayed_type_times(TypeA,TypeB,ResType,Pos,ExprA,ExprB,TRin,TRout):
788 % "A*B=R"
789 % TypeA: type of A, TypeB: type of B, ResType: type of R
790 % Pos: position info for error messages
791 % ExprA/B: expressions to generate pretty error messages
792 delayed_type_times(TypeA,TypeB,ResType,Pos,ExprA,ExprB,TRin,TRout) :-
793 arg(1,ExprA,PosA), arg(1,ExprB,PosB),
794 ( maplist(var,[TypeA,TypeB,ResType]) ->
795 typecheck_result_add_delayed_rule(Trigger,Errors,TRin,TRout),
796 delayed_type_times2(TypeA,TypeB,ResType,Trigger,Pos,PosA,PosB,Errors)
797 ; contains_integer_type([TypeA,TypeB,ResType]) ->
798 % One type is an integer
799 unify_types_l([integer,integer,integer],[ResType,TypeA,TypeB],[Pos,PosA,PosB],TRin,TRout)
800 ; otherwise ->
801 % A type is known, no need for a delay
802 unify_types_l([set(couple(X,Y)),set(X),set(Y)],[ResType,TypeA,TypeB],[Pos,PosA,PosB],TRin,TRout)
803 ).
804 :- block delayed_type_times2(-,-,-,-,?,?,?,?).
805 delayed_type_times2(A,B,Res,_Trigger,Pos,PosA,PosB,Errors) :-
806 ( maplist(var,[A,B,Res]) ->
807 Errors = [error('Ambiguous expression (multiplication or cartesian product?)',Pos)]
808 ; contains_integer_type([A,B,Res]) ->
809 unify_types_werrors_l([integer,integer,integer],[Res,A,B],[Pos,PosA,PosB],Errors,[])
810 ; otherwise ->
811 unify_types_werrors_l([set(couple(X,Y)),set(X),set(Y)],[Res,A,B],[Pos,PosA,PosB],Errors,[])
812 ).
813
814 contains_integer_type([T|_Rest]) :- T==integer,!.
815 contains_integer_type([_T|Rest]) :- contains_integer_type(Rest).
816
817 type_operation_call(Op,Res,Args,Pos,Env,operation_call(TOp,TRes,TArgs),Infos,TRin,TRout) :-
818 ext2int(btype2_opcall,Op,identifier(Opid),IPos,_,_,_,_), % succeeds if operation name is a proper identifier
819 !,
820 btype2(identifier(op(Opid)),IPos,Env,identifier(OpId),op(ArgTypes1,ResTypes1),OpInfos,TRin,TR1),
821 create_texpr(identifier(OpId),subst,OpInfos,TOp),
822 btype_l(Args,Env,_ArgTypes,TArgs,TR1,TR2),
823 btype_l(Res,Env,_ResTypes,TRes,TR2,TR3),
824 foldl(check_assign_lhs(Env),TRes,TR3,TR4),
825 ( same_length(Args,ArgTypes1) ->
826 ( same_length(Res,ResTypes1) ->
827 % number of arguments resp. results ok
828 type_operation_call2(OpId,Env,Pos,TRes,TArgs,ArgTypes1,ResTypes1,Infos,TR4,TRout)
829 ; otherwise ->
830 % wrong number of result identifiers given
831 add_operation_call_error(ResTypes1,Res,Pos,Opid,'result identifiers(s)',Infos,TR4,TRout))
832 ; otherwise ->
833 % wrong number of arguments given
834 add_operation_call_error(ArgTypes1,Args,Pos,Opid,'arguments(s)',Infos,TR4,TRout)).
835 type_operation_call(Op,_Res,_Args,Pos,_Env,skip,[],TRin,TRout) :-
836 % operation name is not an id but e.g. a function call
837 functor(Op,Func,_),
838 ajoin(['Expected an identifier for operation call but got "',Func,'" operator'],Msg),
839 store_typecheck_error(Msg,Pos,TRin,TRout).
840 type_operation_call2(OpId,Env,Pos,TRes,TArgs,ArgTypes,ResTypes,Infos,TRin,TRout) :-
841 check_arguments(TArgs,ArgTypes,TRin,TR1), % check the arguments
842 check_arguments(TRes,ResTypes,TR1,TR2), % check the result
843
844 % if the called operation is not found in the environment,
845 % an error was stored above, and we skip the following section
846 ( env_lookup_infos(OpId,Env,EnvInfos) ->
847 % we currently return the modifies/1 information of the called operation
848 % the only information about this node. This information is needed by
849 % get_modified_vars/3.
850 get_operation_infos(EnvInfos,Infos),
851 % check if we are in a section where we can only call operations
852 % that make no changes to the state ("inquiry")
853 ( (memberchk(dontcall,EnvInfos), get_preference(allow_local_operation_calls,false)) ->
854 % it is not allowed do call the operation: this is the case if a local
855 % operation is used (only operations of included/used/seen machines are allowed to call)
856 % TO DO: we are allowed to call LOCAL_OPERATIONS from other OPERATIONS
857 store_typecheck_error('a local operation must not be called',Pos,TR2,TRout)
858 ; memberchk(inquiry,EnvInfos) ->
859 % check whether we call a query-operation, if the target it marked "inquiry only"
860 ( memberchk(modifies([]),Infos) -> TR2=TRout
861 ; otherwise -> store_typecheck_error('query-operation expected ',Pos,TR2,TRout))
862 ; otherwise ->
863 % ok, we may call even state-changing operations
864 TR2=TRout
865 )
866 ; otherwise ->
867 % operation not found, skip additional checks above and
868 % state (maybe incorrectly, but errors are reported anyway),
869 % that the operation call does not modify any variables
870 Infos = [modifies([]),reads([]),non_det_modifies([])],
871 TR2=TRout).
872 check_arguments(TArgs,ArgTypes1,TRin,TRout) :-
873 get_texpr_types(TArgs,ArgTypes), maplist(get_texpr_pos,TArgs,ArgPos),
874 unify_types_l(ArgTypes1,ArgTypes,ArgPos,TRin,TRout).
875
876 % Generator an error for the wrong numbers of arguments resp. result identifiers
877 add_operation_call_error(ExpTypes,GivenExpr,Pos,Opid,Title,Infos,TRin,TRout) :-
878 Infos = [modifies([]),reads([])], % Info field must be set, even in case of an error
879 length(ExpTypes,Expected),length(GivenExpr,Given),
880 ajoin(['Expected ',Expected,' ',Title,' for operation ',Opid,
881 ', but ',Given,' ',Title,' given'],Msg),
882 store_typecheck_error(Msg,Pos,TRin,TRout).
883
884
885 % common typing patterns:
886 % type a list of expressions, return the list of types and typed expressions
887 btype_l([],_Env,[],[],TR,TR).
888 btype_l([Expr|Rest],Env,[Type|TRest],[TExpr|TERest],TRin,TRout) :-
889 btype(btype_l,Expr,Env,Type,TExpr,TRin,TR1),
890 btype_l(Rest,Env,TRest,TERest,TR1,TRout).
891
892 % type a list of expressions whose type is the same
893 btype_same([],_Env,_Type,[],TR,TR).
894 btype_same([Expr|ERest],Env,Type,[TExpr|TERest],TRin,TRout) :-
895 btype(btype_same,Expr, Env, ElemType, TExpr, TRin, TR1),
896 get_texpr_pos(TExpr,Pos),
897 unify_types(Type,ElemType,Pos,TExpr,TR1,TR2),
898 btype_same(ERest,Env,Type,TERest,TR2,TRout).
899
900 % for a list of identifiers, create a subenvironment with
901 % their primed versions. I.e., for each identifier "x", introduce
902 % a variable "x$0" into the environment.
903 % The type and additional information is copied from the original
904 % identifier, aditionally information about what the original
905 % identifier was ist stored.
906 add_primed_id(TId,InEnv,SubEnv) :-
907 def_get_texpr_id(TId,Id),
908 get_texpr_type(TId,Type),
909 get_texpr_info(TId,Infos),
910 number_suffix(Id,0,FullId),
911 % the additional information is used in the interpreter to store the
912 % values before the substitution under the alternative names
913 %env_store(FullId,Type,[before_substitution(Id,FullId)|Infos],InEnv,SubEnv).
914 env_store(FullId,Type,Infos,InEnv,SubEnv).
915
916
917
918 % special cases
919
920 check_evb_becomes_such(Label,Ids,Pred,Env,TIds,TPred,TRin,TRout) :-
921 btype_l(Ids,Env,_,TIds,TRin,TR1),
922 foldl(check_assign_lhs(Env),TIds,TR1,TR2),
923 prime_identifiers(TIds,TPrimed),
924 add_identifiers_to_environment(TPrimed,Env,Subenv),
925 btype(Label,Pred,Subenv,pred,TPred,TR2,TRout).
926
927 % CASE ... EITHER .. OR ... END
928 btype_caseor(Env,Type,CaseOr,TCaseOr,TExprs,TRin,TRout) :-
929 ext2int(btype_caseor,CaseOr,case_or(Exprs,Subst),_,pred,case_or(TExprs,TSubst),[],TCaseOr),
930 % a case expresiion can have multiple expressions that may match, all of the same type "Type"
931 btype_same(Exprs,Env,Type,TExprs,TRin,TR1),
932 btype(btype_caseor,Subst,Env,subst,TSubst,TR1,TRout).
933 % TO DO: check that Field1 of case_or(Field1,_) is a literal value
934 check_case_expressions(Exprs,TRin,TRout) :-
935 maplist(is_literal,Exprs),!, % only literals allowed
936 ( contains_duplicate_literal(Exprs,Duplicate) ->
937 translate_bexpression(Duplicate,DStr),
938 get_texpr_pos(Duplicate,Pos),
939 ajoin(['Duplicate case in CASE statement: ',DStr],Msg),
940 store_typecheck_error(Msg,Pos,TRin,TRout)
941 ; otherwise -> % ok, all literals, no duplicates
942 TRin=TRout
943 ).
944 check_case_expressions(Exprs,TRin,TRout) :-
945 % there are elements that are not literals
946 exclude(is_literal,Exprs,NonLiterals),
947 foldl(non_literal_error,NonLiterals,TRin,TRout).
948 is_literal(TExpr) :-
949 get_texpr_expr(TExpr,Expr),
950 get_texpr_info(TExpr,Info),
951 is_literal2(Expr,Info).
952 is_literal2(identifier(_),Info) :-
953 memberchk(enumerated_set_element,Info).
954 is_literal2(integer(_),_Info).
955 is_literal2(boolean_true,_Info).
956 is_literal2(boolean_false,_Info).
957 is_literal2(string(_),_Info).
958 non_literal_error(TExpr,TRin,TRout) :-
959 translate_bexpression(TExpr,Str),
960 get_texpr_pos(TExpr,Pos),
961 ajoin(['CASE argument \'',Str,'\' is not a literal value.'],Msg),
962 store_typecheck_error(Msg,Pos,TRin,TRout).
963 contains_duplicate_literal(TExprs,Duplicate) :-
964 % This can be done, because we know that TExprs are literals, so there are no
965 % sub-expressions with positions information or similar problems
966 append(_Prefix,[Dup|Rest],TExprs),
967 get_texpr_expr(Dup,Expr),
968 get_texpr_expr(Duplicate,Expr),
969 memberchk(Duplicate,Rest),!.
970
971 btype_field_rec(Env,Ext,field(Id,Type),field(Id,TExpr),TRin,TRout) :-
972 remove_pos(Ext,rec_entry(Identifier,Expr)),
973 (remove_pos(Identifier,identifier(Id)) -> true
974 ; add_error_and_fail(btype_field_rec,'Invalid record field Identifier',Identifier)),
975 btype(field,Expr,Env,Type,TExpr,TRin,TRout).
976
977 extract_field_type(field(Id,TExpr),field(Id,Type),TRin,TRout) :-
978 get_texpr_type(TExpr,SetType),
979 get_texpr_pos(TExpr,Pos),
980 unify_types(set(Type),SetType,Pos,TExpr,TRin,TRout).
981
982 sort_record_fields([],_,[]).
983 sort_record_fields([field(Id,_Type)|Trest],Fields,[Field|Frest]) :-
984 Field = field(Id,_Value),
985 member(Field,Fields),!,
986 sort_record_fields(Trest,Fields,Frest).
987
988 lookup_eventb_operator(Id,Args1,Args2,Pos,Env,ExPr,Result,Type,Info,TRin,TRout) :-
989 ( env_lookup_infos(operator(Id),Env,[Module:Callback]) ->
990 append(Args1,Args2,Args), % do not distinguish between expressions and predicates
991 btype_l(Args,Env,_Types,TArgs,TRin,TR1),
992 call(Module:Callback,Id,TArgs,Pos,Env,ExPr,TExpr,TR1,TRout),
993 create_texpr(Result,Type,Info,TExpr)
994 ; otherwise ->
995 ajoin(['Unknown operator identifier ',Id],Msg),
996 store_typecheck_error(Msg,Pos,TRin,TRout),
997 failure_syntax_element(ExPr,Id,Result,Type)).
998 % TODO[DP,2013-01-31]: copied from bmachine_eventb -> refactor!
999 failure_syntax_element(expr,Id,identifier(Id),_).
1000 failure_syntax_element(pred,_Id,falsity,pred).
1001
1002 get_operation_infos(Info,OpInfos) :-
1003 operation_infos(OpInfos),
1004 get_operation_infos2(OpInfos,Info).
1005 get_operation_infos2([],_).
1006 get_operation_infos2([Info|Rest],AllInfos) :-
1007 memberchk(Info,AllInfos),
1008 get_operation_infos2(Rest,AllInfos).
1009
1010 % the following information is required for each operation identifier
1011 % it is "filled" by the type-checker (the operation/4 case of btype2)
1012 operation_infos(Infos) :- findall(I,operation_info(I),Infos).
1013 operation_info(modifies(_)).
1014 operation_info(reads(_)).
1015 operation_info(non_det_modifies(_)).
1016
1017
1018 % unify type arguments of two terms
1019 % N is the number of the argument which should be processed
1020 % Arity is the arity of the term, so 1 <= N <= Arity
1021 % Env is the type environment
1022 % TypeTerm is a term that corresponds to the syntax element
1023 % e.g. "1<5" ~ less(1,5) has a type term less(integer,integer)
1024 % in the arguments of the TypeTerm, special constructs may be used:
1025 % "[Type]" declares that there is a list of expressions with the same Type
1026 % "ids" declares that there is a list of identifiers wich build a
1027 % sub-environment which will be used in the following arguments
1028 % (strict left-to-right)
1029 % "ids(T)" is like "ids" but the types of the identifiers are merged
1030 %
1031 % TExpr is the typed expression of the complete expression
1032 % GI as usual: Introduced identifier and errors
1033 type_and_unify_args(N,Arity,Pos,Env,Expr,TypeTerm,TExpr,TRin,TRout) :-
1034 %print(chck(N,Arity,Expr,TypeTerm,TExpr)),nl,
1035 ( N =< Arity ->
1036 arg(N,Expr,Arg), % Expr is the raw expression of the Nth argument
1037 arg(N,TypeTerm,ArgType), % ArgType is the corresponding type
1038 arg(N,TExpr,ArgTExpr), % TExpr is the corresponding typed expression
1039 type_and_unify_args_aux(ArgType,Arg,Pos,Expr,Env,ArgTExpr,NextEnv,TRin,TR2),
1040 N2 is N+1,
1041 type_and_unify_args(N2,Arity,Pos,NextEnv,Expr,TypeTerm,TExpr,TR2,TRout)
1042 ; otherwise ->
1043 TRin=TRout
1044 ).
1045 type_and_unify_args_aux(ArgType,Arg,Pos,Expr,Env,ArgTExpr,NextEnv,TRin,TRout) :-
1046 % new identifiers are introduced, they are
1047 % available in the environment of the following arguments
1048 nonvar(ArgType),id_introduced(ArgType,CoupledType,Duplicates,Infos),!,
1049 functor(Expr,ExprFunctor,_), % Stored inside the information of newly created variables
1050 flatten_illegal_couples(Arg,FixedArg),
1051 ( Duplicates = unique -> check_for_duplicates(FixedArg,Env,all,TRin,TR1)
1052 ; Duplicates = allowed -> check_for_duplicates(FixedArg,Env,[definition],TRin,TR1)), % just check that there are no clashes with definitions
1053 add_introduced_by_info(ExprFunctor,Infos,NewInfos),
1054 add_ext_variables_with_info(FixedArg,Env,NewInfos,ArgTExpr,NextEnv,TR1,TR2),
1055 % convert the list of types to a "couplised" type,
1056 % (e.g. [a] -> a, or [a,b] -> couple(a,b) )
1057 % in many cases (if ArgType==ids), the "couplised" type is just ignored
1058 idlist_to_type(ArgTExpr,CoupledType1),
1059 unify_types(CoupledType,CoupledType1,Pos,ArgTExpr,TR2,TRout).
1060 type_and_unify_args_aux(ArgType,Arg,_Pos,_Expr,Env,ArgTExpr,NextEnv,TRin,TRout) :-
1061 % if the argument is of the form [...] we expect a list of
1062 % expressions with the same type
1063 nonvar(ArgType),ArgType = [CommonType],!,
1064 btype_same(Arg,Env,CommonType,ArgTExpr,TRin,TRout),
1065 NextEnv = Env.
1066 type_and_unify_args_aux(ArgType,Arg,Pos,Expr,Env,ArgTExpr,NextEnv,TRin,TRout) :-
1067 % standard case: just type-check the argument
1068 btype(type_and_unify_args(Pos,Expr,Arg,ArgType),Arg,Env,ArgType,ArgTExpr,TRin,TRout),
1069 NextEnv = Env.
1070
1071 % Note: Nothing seems to use introduced_by(_); except for exists in b_intepreter
1072 add_introduced_by_info(exists,Infos,Res) :- !, Res=[introduced_by(exists)|Infos].
1073 add_introduced_by_info(_,Infos,Infos).
1074
1075 % id_introduced(+Pattern,-CoupledType,-DuplicateIdentifiers,-Infos):
1076 % Pattern is a pattern in the type checking database (::/2).
1077 % id_introduced/4 extracts the CoupledType (may be a free variable),
1078 % (see the declaration of "comprehension_set" for an example use)
1079 % and returns a flag if an introduction of an already existing variable
1080 % is allowed. (E.g. LET does not allow to declare an existing identifier).
1081 % Additional infos that are added to the type environment are supported.
1082 id_introduced(ids,_,allowed,[]).
1083 id_introduced(ids(CoupledType),CoupledType,allowed,[]).
1084 id_introduced(new_ids,_,unique,[]).
1085 id_introduced(new_readonly_ids,_,unique,[readonly]).
1086 id_introduced(new_readonly_ids(CoupledType),CoupledType,unique,[readonly]).
1087 % Atelier-B actually does allow ANY/LET/VAR to override existing ids !
1088 % TO DO: maybe only generate a warning in check_for_duplicates!
1089
1090 % check_for_duplicates(IdList,Env,TRin,TRout):
1091 % IdList is a list of (not typechecked) identifiers
1092 % If an identifier already exists in the environment Env, an error
1093 % is added (if the type matches the InvalidTypes argument)
1094 %check_for_duplicates(IdList,Env,TRin,TRout) :- check_for_duplicates(IdList,Env,all,TRin,TRout).
1095 check_for_duplicates(IdList,Env,InvalidTypes,TRin,TRout) :-
1096 foldl(check_for_duplicates_aux(Env,InvalidTypes),IdList,TRin,TRout).
1097 check_for_duplicates_aux(Env,InvalidTypes,identifier(Pos,Id),TRin,TRout) :-
1098 ( (env_lookup_type(Id,Env,IdType), check_invalid_type(InvalidTypes,IdType)) ->
1099 ? (env_lookup_position_string(Id,Env,PosStr) -> PosInfo = [' at (line:column) =',PosStr] ; PosInfo = []),
1100 (get_idtype_desc(IdType,Desc)
1101 -> ajoin(['Identifier ',Id,' has already been declared as ', Desc|PosInfo],Msg)
1102 ; ajoin(['Identifier ',Id,' has already been declared'|PosInfo],Msg)),
1103 store_typecheck_warning(Msg,Pos,TRin,TRout) % we now use store_typecheck_warning instead of store_typecheck_error
1104 ; otherwise ->
1105 TRin=TRout
1106 ).
1107
1108 get_idtype_desc(IdType,_) :- var(IdType),!,fail.
1109 get_idtype_desc(global(S),Desc) :- !, ajoin(['element of SET ',S],Desc).
1110 % TO DO: add more descriptions
1111 get_idtype_desc(IdType,Desc) :- nonvar(IdType), functor(IdType,Desc,_).
1112
1113 % check if the type is one we do not allow in this context
1114 check_invalid_type(all,_).
1115 check_invalid_type([H|T],IdType) :- nonvar(IdType), functor(IdType,F,_), member(F,[H|T]).
1116
1117 % remove illegal couple terms introduced by Prolog BParser: TO DO: adapt Prolog BParser for UNION/INTER/...
1118 flatten_illegal_couples([],Res) :- !, Res=[].
1119 flatten_illegal_couples([couple(_Pos,Ids)],Res) :- !, Res = Ids.
1120 flatten_illegal_couples([H|T],Res) :- !, Res = [H|T].
1121 flatten_illegal_couples(identifier(Pos,ID),Res) :-
1122 add_warning(btypechecker,'Fixing error in AST, missing list:',ID,Pos),
1123 Res = [identifier(Pos,ID)].
1124
1125 % environment access
1126 lookup_type(Id,Env,Pos,Type,TRin,TRout) :-
1127 ( env_lookup_type(Id,Env,Type) ->
1128 TRin=TRout
1129 ; otherwise ->
1130 get_current_context(Ctxt),
1131 (Id = op(Op)
1132 -> UMsg = 'Unknown operation "', Id0 = Op
1133 ; UMsg = 'Unknown identifier "', Id0 = Id
1134 ),
1135 ( Id \= op(_), env_lookup_type(op(Id),Env,_OpType) ->
1136 ajoin(['Illegal use of operation identifier "',Id,'"',Ctxt],Msg)
1137 ; Id \= op(_), is_primed_of(Id,UnprimedId), env_lookup_type(UnprimedId,Env,_UpType) ->
1138 ajoin(['Primed version "', Id, '" of identifier ', UnprimedId, ' not available',Ctxt],Msg)
1139 ; fuzzy_find_possible_ids(Id0,Env,AlternativeIds,_Len) ->
1140 (AlternativeIds=[AlternativeId] ->
1141 ajoin([UMsg,Id0,'"',Ctxt,', did you mean "',AlternativeId,'"?'],Msg)
1142 ; wrap_ids_in_quotes(AlternativeIds,WIds),
1143 ajoin([UMsg,Id0,'"',Ctxt,', did you mean one of: '|WIds],Msg)
1144 )
1145 ; find_possible_completion_ids(Id0,Env,AlternativeIds,Len) ->
1146 (AlternativeIds=[AlternativeId] ->
1147 ajoin([UMsg,Id0,'"',Ctxt,', the possible completion is "',AlternativeId,'"'],Msg)
1148 ; Len=<3 ->
1149 wrap_ids_in_quotes(AlternativeIds,WIds),
1150 ajoin([UMsg,Id0,'"',Ctxt,', the ', Len, ' possible completions are '|WIds],Msg)
1151 ; prefix_length(AlternativeIds,AIds3,3), wrap_ids_in_quotes(AIds3,WIds),
1152 ajoin([UMsg,Id0,'"',Ctxt,', 3 possible completions (out of ',Len,') are '|WIds],Msg)
1153 )
1154 ; otherwise ->
1155 ajoin([UMsg,Id0,'"',Ctxt],Msg) % (lookup type)
1156 % 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
1157 %, env_get_visible_ids(Env,Ids), format(user_error,'Known identifiers are: ~w~n',[Ids])
1158 ),
1159 % print(err(Id)),nl,print(Env),nl,trace,
1160 store_typecheck_error(Msg,Pos,TRin,TRout)).
1161 lookup_infos(Id,Env,Infos) :-
1162 ( env_lookup_infos(Id,Env,Infos) -> !
1163 ; otherwise -> Infos=[]).
1164
1165 is_primed_of(Id0,Id) :- atom(Id0), atom_concat(Id,'$0',Id0).
1166
1167 :- use_module(tools_matching,[fuzzy_match_codes/2, codes_to_lower_case/2,get_current_keywords/1]).
1168
1169 fuzzy_find_possible_ids(Id,Env,AlternativeIds,Len) :-
1170 findall(AId,fuzzy_find_possible_id(Id,Env,AId),AlternativeIds),
1171 length(AlternativeIds,Len),
1172 Len>0.
1173
1174 fuzzy_find_possible_id(Id,Env,AlternativeId) :- atom_codes(Id,Codes1),
1175 codes_to_lower_case(Codes1,LCodes1),
1176 env_get_visible_ids_and_keywords(Env,Ids),
1177 member(AIdOrOp,Ids), id_or_op_codes(AIdOrOp,AlternativeId,Codes2),
1178 codes_to_lower_case(Codes2,LCodes2),
1179 fuzzy_match_codes(LCodes1,LCodes2).
1180
1181 env_get_visible_ids_and_keywords(Env,AllIds) :-
1182 env_get_visible_ids(Env,Ids),
1183 get_current_keywords(Keywords),
1184 ord_union(Ids,Keywords,AllIds).
1185
1186 wrap_ids_in_quotes([],[]).
1187 wrap_ids_in_quotes([ID],['"',ID,'"']) :- !.
1188 wrap_ids_in_quotes([ID|T],['"',ID,'", '|WT]) :- wrap_ids_in_quotes(T,WT).
1189
1190
1191 find_possible_completion_ids(Id,Env,AlternativeIds,Len) :-
1192 findall(AId,find_possible_completion_id(Id,Env,AId),AlternativeIds),
1193 length(AlternativeIds,Len),
1194 Len>0.
1195
1196 % find possible completion of an (unknown) identifier
1197 find_possible_completion_id(Id,Env,AlternativeId) :- atom_codes(Id,Codes1),
1198 env_get_visible_ids_and_keywords(Env,Ids),
1199 member(AIdOrOp,Ids), id_or_op_codes(AIdOrOp,AlternativeId,Codes2),
1200 prefix(Codes2,Codes1).
1201
1202 id_or_op_codes(op(ID),RealID,Codes) :- !, RealID=ID, atom_codes(ID,Codes).
1203 id_or_op_codes(ID,ID,Codes) :- !, atom_codes(ID,Codes).
1204
1205
1206 % check if the left hand side of an assignment is writeable
1207 check_assign_lhs(Env,TExpr,TRin,TRout) :-
1208 ( id_or_function(TExpr,Id) ->
1209 get_texpr_type(TExpr,Type),
1210 lookup_infos(Id,Env,Infos),
1211 ( member(readonly,Infos) ->
1212 get_texpr_pos(TExpr,Pos),
1213 store_typecheck_error('read-only expression on left hand side of assignment ',Pos,TRin,TRout)
1214 ; nonvar(Type), Type = op(_,_) ->
1215 get_texpr_pos(TExpr,Pos),
1216 store_typecheck_error('operation on left hand side of assignment ',Pos,TRin,TRout)
1217 ; otherwise ->
1218 TRin=TRout
1219 )
1220 ; otherwise ->
1221 get_texpr_pos(TExpr,Pos),
1222 store_typecheck_error('unsupported expression on left hand side of assignment ',Pos,TRin,TRout)).
1223
1224
1225 id_or_function(TIdFunc,Id) :-
1226 get_texpr_expr(TIdFunc,IdFunc),
1227 id_or_function2(IdFunc,Id).
1228 id_or_function2(identifier(Id),Id).
1229 id_or_function2(function(Func,_Arg),Id) :-
1230 id_or_function(Func,Id).
1231
1232 % extract information for identifiers from the environment
1233 % currently, use all information but the position
1234 extract_id_information(InfosIn,InfosOut) :-
1235 exclude(is_information_to_remove,InfosIn,InfosOut).
1236 is_information_to_remove(nodeid(_)).
1237 is_information_to_remove(remove(_)).
1238
1239
1240 % some helper predicates
1241 :- assert_must_succeed(btypechecker:couplise_list([a],a)).
1242 :- assert_must_succeed(btypechecker:couplise_list([a,b],couple(a,b))).
1243 :- assert_must_succeed(btypechecker:couplise_list([a,b,c],couple(couple(a,b),c))).
1244 :- assert_must_succeed(btypechecker:couplise_list([a,b,c,d],couple(couple(couple(a,b),c),d))).
1245 couplise_list([A],R) :- !,R=A.
1246 couplise_list([A,B],R) :- !,R=couple(A,B).
1247 couplise_list([A,B|Rest],Result) :-
1248 couplise_list([couple(A,B)|Rest],Result).
1249
1250 couplise_list_pos([A],_,A) :- !.
1251 couplise_list_pos([A,B],Pos,couple(Pos,A,B)) :- !.
1252 couplise_list_pos([A,B|Rest],Pos,Result) :-
1253 couplise_list_pos([couple(Pos,A,B)|Rest],Pos,Result).
1254
1255 idlist_to_type(Exprs,Type) :-
1256 get_texpr_types(Exprs,Types),
1257 couplise_list(Types,Type).
1258
1259 % remove choice_or constructs in a list
1260 % there has to be at least one occurrence of choice_or
1261 remove_choice_ors(Options,Substs) :-
1262 memberchk(choice_or(_,_),Options), % TODO: Is it ok that this could fail?
1263 maplist(remove_choice_or2,Options,Substs).
1264 remove_choice_or2(choice_or(_,Subst),Subst) :- !.
1265 remove_choice_or2(Subst,Subst).
1266
1267 add_identifiers_to_environment(Ids,In,Out) :-
1268 foldl(add_identifier_to_environment,Ids,In,Out).
1269 add_identifier_to_environment(TExpr,In,Out) :-
1270 def_get_texpr_id(TExpr,Id),
1271 get_texpr_type(TExpr,Type),
1272 get_texpr_info(TExpr,Info),
1273 env_store(Id,Type,Info,In,Out).
1274
1275 % can nows also be used to unprime ids:
1276 % Event-B style priming: x' is state of x after
1277 prime_identifiers(TExprs,Primed) :-
1278 maplist(prime_identifier,TExprs,Primed).
1279 prime_identifier(b(identifier(Id),Type,Info),b(identifier(Primed),Type,Info)) :-
1280 atom_concat(Id,'\'',Primed).
1281 % Clasccial B semantics: x$0 is state of x before
1282 prime_identifiers0(TExprs,Primed) :-
1283 maplist(prime_identifier0,TExprs,Primed).
1284 prime_identifier0(b(identifier(Id),Type,Info),b(identifier(Primed),Type,Info)) :-
1285 atom_concat(Id,'$0',Primed).
1286 prime_atom0(Id,Primed) :- atom_concat(Id,'$0',Primed).
1287
1288
1289 % allow access to abstract variables by removing all "error/1"
1290 % information from identifiers in the environment which also
1291 % carry the "abstraction" information
1292 allow_access_to_abstract_vars(OldEnv,NewEnv) :-
1293 env_transform_infos(OldEnv,_,OldInfos,NewInfos,NewEnv),
1294 maplist(allow_access_to_abstract_var,OldInfos,NewInfos).
1295 % Iterate over the information list
1296 allow_access_to_abstract_var(OldInfo,NewInfo) :-
1297 % abstract variable where no access is permitted
1298 member(abstraction,OldInfo),
1299 % remove the error flag
1300 select(error(_),OldInfo,NewInfo),!.
1301 allow_access_to_abstract_var(Info,Info).
1302
1303 % for each local concrete_variable, add a variable x$0 of the same
1304 % type to the scope. (Needed in while loop invariants)
1305 % TODO: This is not completely correct. The variable should only be added
1306 % if there is an abstract variable of the same name.
1307 add_primed_old_value_variables(InvEnv,PInvEnv) :-
1308 env_transform_infos(InvEnv,Ids,Infos,_,_),
1309 foldl(add_primed_old_value_variable,Ids,Infos,InvEnv,PInvEnv).
1310 add_primed_old_value_variable(Id,Info,In,Out) :-
1311 % We add a primed version if it is a concrete variable declared in this machine
1312 memberchk(loc(local,_,Sec),Info),memberchk(Sec,[concrete_variables,abstract_variables]),!,
1313 atom_concat(Id,'$0',Primed),
1314 env_lookup_type(Id,In,Type),
1315 env_store(Primed,Type,[refers_to_old_state(Id)],In,Out).
1316 add_primed_old_value_variable(_Id,_Info,Env,Env).
1317
1318 % check if a reference to the original value of a variable is made.
1319 % This is only possible in the loop invariant of a while statement
1320 % The reference to an original value is an identifier marked with an refers_to_old_state(Id) tag,
1321 % see add_primed_old_value_variables/2 above.
1322 check_for_old_state_references(TExpr,Info) :-
1323 check_for_old_state_references2(TExpr,Refs,[]),
1324 sort(Refs,SortedRefs),
1325 ( SortedRefs = [] -> Info = []
1326 ; SortedRefs = [_|_] -> Info = [refers_to_old_state(SortedRefs)]).
1327 check_for_old_state_references2(TExpr) -->
1328 { syntaxtraversion(TExpr,Expr,Type,Infos,Subs,_) },
1329 check_for_old_state_references3(Expr,Type,Infos),
1330 foldl(check_for_old_state_references2,Subs).
1331 check_for_old_state_references3(identifier(Id),Type,Infos) -->
1332 {memberchk(refers_to_old_state(OrigId),Infos),!}, [oref(Id,OrigId,Type)].
1333 check_for_old_state_references3(_Expr,_Type,_Infos) --> !.
1334
1335 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1336 % error handling
1337 store_typecheck_error(Msg,Pos,TRin,TRout) :-
1338 (typecheck_result_add_error(error(Msg,Pos),TRin,TRout) -> true
1339 ; add_internal_error('Could not store typecheck error: ', Msg),
1340 TRin=TRout).
1341 store_typecheck_warning(Msg,Pos,TRin,TRout) :-
1342 (typecheck_result_add_error(warning(Msg,Pos),TRin,TRout) -> true
1343 ; add_internal_error('Could not store typecheck warning: ', Msg),
1344 TRin=TRout).
1345
1346 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1347 % type unification
1348
1349 unify_types_werrors_l(A,B,Pos,Ein,Eout) :-
1350 typecheck_result_init(Ein,[],[],TRStart),
1351 unify_types_l(A,B,Pos,TRStart,TR),
1352 typecheck_result_get_errors(TR,Eout),
1353 typecheck_result_get_delayed_rules(TR,[]),
1354 typecheck_result_get_identifiers(TR,[]).
1355 unify_types_werrors(A,B,Pos,Ein,Eout) :-
1356 unify_types_werrors_l([A],[B],[Pos],Ein,Eout).
1357
1358 unify_types_l([],[],[],TR,TR).
1359 unify_types_l([A|Arest],[B|Brest],[Pos|Prest],TRin,TRout) :-
1360 unify_types(A,B,Pos,no_expression,TRin,TR1),
1361 unify_types_l(Arest,Brest,Prest,TR1,TRout).
1362
1363
1364
1365 unify_types(A,B,_,_,TR,TR) :-
1366 unify_types_strict(A,B),!.
1367 unify_types(A,B,Pos,Expr,TRin,TRout) :-
1368 unify_failed(A,B,Pos,Expr,TRin,TRout).
1369 unify_failed(A,B,Pos,Expr,TRin,TRout) :-
1370 %print(unify_failed(A,B,Pos,Expr,TRin,TRout)),nl,trace,
1371 ( nonvar(Expr),Expr\=no_expression,translate_bexpression(Expr,ExprString) ->
1372 TailMsg = [' in \'', ExprString, '\'']
1373 ; otherwise -> TailMsg = []),
1374 unify_failed_msg(A,B,MsgList,TailMsg),
1375 ajoin(MsgList,Msg),
1376 store_typecheck_error(Msg,Pos,TRin,TRout).
1377
1378 unify_failed_msg(A,B,MsgList,Rest) :-
1379 match_instance(A,record([field(Field,_)|_])),
1380 match_instance(B,record(Fields)),
1381 get_field_names(Fields,Names),
1382 nonmember(Field,Names),
1383 !,
1384 ajoin_with_sep(Names,',',NL),
1385 MsgList = ['Type mismatch: Expected record with field ', Field, ', but had only fields {',NL,'}'|Rest].
1386 unify_failed_msg(A,B,['Type mismatch: Expected ', PA, ', but was ', PB|Rest],Rest) :- % TO DO: provide better user-feedback
1387 pretty_type(A,PA), pretty_type(B,PB).
1388
1389 get_field_names(V,_) :- var(V),!,fail.
1390 get_field_names([],[]).
1391 get_field_names([H|T],[FH|FT]) :- get_field_name(H,FH), get_field_names(T,FT).
1392 get_field_name(F,Field) :- nonvar(F),F=field(Field,_).
1393 match_instance(V,Pat) :- var(Pat),!,Pat=V.
1394 match_instance(V,_Pat) :- var(V),!,fail.
1395 match_instance(F,Pat) :- nonvar(F), functor(F,N,A), functor(Pat,N,A),
1396 (A>0 -> F=..FL, Pat =.. PL, maplist(match_instance,FL,PL) ; true).
1397
1398 %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)
1399
1400 :- assert_must_succeed(( btypechecker:unify_types_strict(set(couple(boolean,string)), set(couple(boolean,string))) )).
1401 :- assert_must_succeed(( btypechecker:unify_types_strict(seq(integer), set(couple(integer,integer))) )).
1402 :- assert_must_succeed(( btypechecker:unify_types_strict(seq(set(couple(integer,integer))),
1403 set(couple(integer,seq(integer)))) )).
1404 :- assert_must_succeed(( btypechecker:unify_types_strict(seq(integer), any) )).
1405 :- assert_must_succeed(( btypechecker:unify_types_strict(any, set(couple(integer,integer))) )).
1406 :- assert_must_succeed(( btypechecker:unify_types_strict(_X, set(couple(integer,integer))) )).
1407 :- assert_must_succeed(( btypechecker:unify_types_strict(seq(any), set(couple(integer,boolean))) )).
1408
1409 unify_types_strict(A,B) :-
1410 ( var(A) ->
1411 ( var(B) -> A=B
1412 ; otherwise -> unify_types1(B,A))
1413 ; otherwise ->
1414 unify_types1(A,B)
1415 ),!.
1416
1417 unify_types1(A,B) :- var(B),contains_var(B,A),!,fail.
1418 unify_types1(A,B) :- unify_types2(A,B).
1419
1420 unify_types2(any,B) :- !,
1421 (var(B) -> B=any
1422 ; true). % TO DO: set inner variables to any ?
1423 unify_types2(_,B) :- B==any, !. % Maybe these two cases should be removed and type errors generated
1424 % where the type cannot be inferred
1425 unify_types2(set(A),set(B)) :- !, unify_types_strict(A,B).
1426 unify_types2(seq(A),seq(B)) :- !, unify_types_strict(A,B).
1427 unify_types2(set(A),seq(B)) :- !, unify_types_strict(seq(B),set(A)).
1428 unify_types2(seq(A),set(B)) :- !, unify_types_strict(couple(integer,A),B).
1429 unify_types2(couple(A,B),couple(X,Y)) :- !,unify_types_strict(A,X),unify_types_strict(B,Y).
1430 unify_types2(string,string).
1431 unify_types2(integer,integer).
1432 unify_types2(boolean,boolean).
1433 unify_types2(global(G),global(G)).
1434 unify_types2(pred,pred).
1435 unify_types2(subst,subst).
1436 unify_types2(record(A),record(B)) :- !, unify_fields(B,A).
1437 unify_types2(op(ParamsA,ResultsA),op(ParamsB,ResultsB)) :-
1438 unify_types_l(ParamsA,ParamsB),
1439 unify_types_l(ResultsA,ResultsB).
1440 unify_types2(freetype(Name),freetype(Name)).
1441 unify_types2(freetype(Name,TypeParams1),freetype(Name,TypeParams2)) :-
1442 unify_types_l(TypeParams1,TypeParams2).
1443 unify_types2(witness,witness).
1444 unify_types2(status,status).
1445
1446
1447 unify_types_l(A,B) :- var(A),!,A=B.
1448 unify_types_l([],[]) :- !.
1449 unify_types_l([T1|Rest1],[T2|Rest2]) :-
1450 unify_types_strict(T1,T2),unify_types_l(Rest1,Rest2).
1451
1452 unify_fields(Sub,Super) :-
1453 nonvar(Sub),nonvar(Super),!,
1454 ( Sub = [field(Name,Type)|SubRest] ->
1455 extract_field(Super,Name,Type,SuperRest),
1456 unify_fields(SubRest,SuperRest)
1457 ; Sub = [] ->
1458 Super = []
1459 ; add_internal_error('Illegal type: ',unify_fields(Sub,Super)),fail
1460 ).
1461 unify_fields(Fields,Fields).
1462
1463 extract_field(L,Name,Type,Rest) :-
1464 extract_field2(L,Name,Type,Rest).
1465 extract_field2(L,Name,Type,Rest) :- nonvar(L),!,
1466 L = [field(FName,FType)|LRest],
1467 ( Name = FName ->
1468 unify_types_strict(Type,FType),
1469 Rest=LRest
1470 ; otherwise ->
1471 Rest=[field(FName,FType)|NRest],
1472 extract_field2(LRest,Name,Type,NRest)).
1473 extract_field2(L,Name,Type,LRest) :-
1474 L = [field(Name,Type)|LRest].
1475
1476 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1477 % check if all types of the variables are ground
1478 check_ground_types_dl(TExprs,Exceptions,Ein,Eout) :- %print(check_ground(TExprs)),nl,
1479 foldl(check_ground_type_dl(Exceptions),TExprs,Ein,Eout).
1480 check_ground_type_dl(Exceptions,TExpr,Ein,Eout) :-
1481 get_texpr_type(TExpr,Type),
1482 ( is_ground_type(Exceptions,Type) ->
1483 Ein=Eout
1484 % TO DO allow polymorphic typing, without any instantiation
1485 ; otherwise ->
1486 % (ground(Type) -> true ; format('Not ground, exceptions = ~w~n~w~n~n',[Exceptions,Type])),
1487 get_texpr_expr(TExpr,identifier(Id)),
1488 ( \+ preferences:get_preference(allow_untyped_identifiers,false),
1489 instantiate_non_ground_type(Exceptions,Type)
1490 -> translate:pretty_type(Type,TS),
1491 debug_format(20,'% Instantiated type of ~w to ~w~n',[Id,TS]),
1492 Ein=Eout
1493 ; get_texpr_pos(TExpr,Pos),
1494 ajoin(['Could not infer type of ',Id], Msg),
1495 Ein=[error(Msg,Pos)|Eout]
1496 )
1497 ).
1498 is_ground_type(_Exceptions,Type) :- ground(Type),!.
1499 is_ground_type(Exceptions,Type) :- var(Type),!,exact_member(Type,Exceptions).
1500 is_ground_type(Exceptions,Type) :-
1501 Type =.. [_|TArgs],
1502 maplist(is_ground_type(Exceptions),TArgs).
1503
1504 :- use_module(b_global_sets,[generate_fresh_supplementary_global_set/1]).
1505 instantiate_non_ground_type(_Exceptions,Type) :- ground(Type),!.
1506 instantiate_non_ground_type(Exceptions,Type) :- var(Type),!,
1507 (exact_member(Type,Exceptions) -> true
1508 ; preferences:get_preference(allow_untyped_identifiers,true_with_string_type) ->
1509 Type = string
1510 ; % if preference set to true we allow those untyped vars and use new deferred sets for them
1511 generate_fresh_supplementary_global_set(GS),
1512 Type = global(GS)
1513 ).
1514 instantiate_non_ground_type(Exceptions,Type) :-
1515 Type =.. [_|TArgs],
1516 maplist(instantiate_non_ground_type(Exceptions),TArgs).
1517
1518
1519
1520 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1521 % rewrite rules to clean up the syntax tree
1522
1523 % substitute definitions
1524 btype_rewrite(RawExpr,Env,Pos,Result,NewPos) :-
1525 is_definition_call(RawExpr,Env),!,
1526 rewrite_definition(RawExpr,Pos,Env,Result,NewPos).
1527 % transform operation calls inside expressions
1528 btype_rewrite(function(Fun,Args),Env,Pos,Result,Pos) :- %print(fun(Fun)),nl, portray_env(Env),
1529 is_operation_call(Fun,Env),!,
1530 debug_println(19,allowing_op_call_in_expression(Fun)),
1531 Result = operation_call_in_expr(Fun,Args).
1532 % other (not definition-related) rules
1533 btype_rewrite(Expr,_Env,Pos,New,Pos) :- btype_rewrite2(Expr,Pos,New).
1534
1535 is_operation_call(identifier(_,Name),Env) :- lookup_operation_name(Name,Env,_,_).
1536 % lookup OPERATION with Name in Environment Env
1537 lookup_operation_name(Name,Env,ArgTypes1,ResTypes1) :-
1538 env_lookup_type(op(Name),Env,Type), nonvar(Type), %print(Type),nl,
1539 Type = op(ArgTypes1,ResTypes1).
1540
1541 % a shorter version of the
1542 is_definition_call(identifier(Name),Env) :-
1543 lookup_definition(Name,Env,_,_Params,_Body).
1544 is_definition_call(function(DefIdP,_Args),Env) :-
1545 remove_pos(DefIdP,identifier(Name)),
1546 % the definition should have parameters, if not, it could be
1547 % that a function is defined and normal function application is
1548 % needed
1549 % Note: There is a rewrite rule for functions that converts a list
1550 % of arguments into couples. That rewrite rule must not be called
1551 % before this rule.
1552 lookup_definition(Name,Env,_,[_|_],_Body).
1553 is_definition_call(definition(_Name,_Args),_Env).
1554
1555 rewrite_definition(identifier(Name),Pos,Env,Result,NewPos) :-
1556 rewrite_definition2(Name,[],Pos,Env,Result,NewPos).
1557 rewrite_definition(function(DefIdP,Args),Pos,Env,Result,NewPos) :-
1558 % A function application where the function is an identifier
1559 % may be a definition with arguments
1560 remove_pos(DefIdP,identifier(Name)),
1561 rewrite_definition2(Name,Args,Pos,Env,Result,NewPos).
1562 rewrite_definition(definition(Name,Args),Pos,Env,Result,NewPos) :-
1563 % the standard way of using a definition
1564 rewrite_definition2(Name,Args,Pos,Env,Result,NewPos).
1565
1566 rewrite_definition2(Name,Args,CallPos,Env,Result,NewPos) :-
1567 ( lookup_definition(Name,Env,DefType,Params,Body) ->
1568 (btype_rewrite_definition(DefType,Params,Name,Env,Args,Body,NewBody)
1569 -> % add context_pos infos
1570 add_raw_ast_pos_info_context(definition_call(Name),CallPos,NewBody,NewBody1),
1571 remove_pos(NewBody1,Result,NewPos) % remove position info
1572 %,print(def_rewrote(Name,CallPos,Args)),nl,print(Result),nl
1573 ; add_internal_error('Rewriting definition failed: ',Name),fail
1574 )
1575 ; otherwise ->
1576 ajoin(['Definition ',Name,' not found'],ErrMsg),
1577 throw(rewrite_exception(ErrMsg,Name))).
1578
1579 btype_rewrite_definition(_DefType,Params,Name,Env,Args,Body,NewBody) :-
1580 ( same_length(Params,Args) ->
1581 maplist(definition_expansion_on_raw_def_paras_with_pos(Env),Args,NewArgs),
1582 maplist(create_def_replace(Name),Params,NewArgs,Replaces),
1583 %% replacing DEFINITION parameters by actual arguments
1584 %% THIS CAN LEAD TO DUPLICATION of computation !
1585 %% 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 !?
1586 %% print(old_body(Name,Body,replaces(Replaces))),nl,
1587 raw_replace(Body,Replaces,NewBody) %% ,print(replaced_def(Name,NewBody)),nl %%
1588 %%TODO: keep track of original position as well !
1589 ; otherwise ->
1590 length(Params,PN),length(Args,AN),
1591 (AN=0
1592 -> ajoin(['Expected ',PN,' arguments for definition ',Name],ErrMsg) % this happens when we provide more than PN arguments; the parser seems to translate this into a definition call with 0 args and then a function call
1593 ; ajoin(['Expected ',PN,' instead of ',AN,' arguments for definition ',Name],ErrMsg)
1594 ),
1595 throw(rewrite_exception(ErrMsg,Name))).
1596 create_def_replace(_,identifier(_,Old),New,Res) :- !, Res=replace(Old,New).
1597 create_def_replace(Name,Term,_,_) :- (Term=definition(_Pos,Old,_) -> true ; Old=''),
1598 ajoin(['Cannot apply definition ',Name,', formal parameter ',Old, ' is not an identifier'],ErrMsg),
1599 throw(rewrite_exception(ErrMsg,Name)).
1600 % lookup DEFINITION with Name in Environment Env
1601 lookup_definition(Name,Env,DefType,Params,Body) :-
1602 env_lookup_type(Name,Env,Type), nonvar(Type),
1603 Type = definition(DefType,Params,Body).
1604
1605 % expressions
1606 btype_rewrite2(couple([A,B]),_,couple(A,B)) :- !.
1607 btype_rewrite2(couple(Elements),Pos,couple(X,Y)) :- couplise_list_pos(Elements,Pos,couple(_,X,Y)).
1608 btype_rewrite2(function(Fun,Args),Pos,function(Fun,Arg)) :-
1609 couplise_list_pos(Args,Pos,Arg).
1610
1611 % substitutions and operations
1612 btype_rewrite2(if(Pred,Subst,Elsifs,Else),Pos,if(IfList)) :-
1613 (Else=skip(_) -> IfList = [if_elsif(Pos,Pred,Subst)|Elsifs]
1614 ; append([if_elsif(Pos,Pred,Subst)|Elsifs],[if_elsif(none,truth(none),Else)],IfList)).
1615 btype_rewrite2(case(Expr,Either,EitherSubst,Ors,Else),Pos,
1616 case(Expr,[case_or(Pos,Either,EitherSubst)|Ors],Else)).
1617 btype_rewrite2(select(Pred,Then,Whens,Else),Pos,select([select_when(Pos,Pred,Then)|Whens],Else)).
1618 btype_rewrite2(select(Pred,Then,Whens),Pos,select([select_when(Pos,Pred,Then)|Whens])).
1619 btype_rewrite2(choice([]),_,choice([])).
1620 btype_rewrite2(choice(Options),_,choice(Substs)) :-
1621 remove_choice_ors(Options,Substs).
1622
1623 % integer sets
1624 btype_rewrite2(integer_set,_,integer_set('INTEGER')).
1625 btype_rewrite2(natural_set,_,integer_set('NATURAL')).
1626 btype_rewrite2(natural1_set,_,integer_set('NATURAL1')).
1627 btype_rewrite2(nat_set,_,integer_set('NAT')).
1628 btype_rewrite2(nat1_set,_,integer_set('NAT1')).
1629 btype_rewrite2(int_set,_,integer_set('INT')).
1630
1631 % applying rewriting of definitions on the raw (un-typed input) syntax tree
1632 % this is used for parameters of definitions (which do not have their own position info)
1633 definition_expansion_on_raw_def_paras_with_pos(Env,RawExprPos,OutAst) :-
1634 compound(RawExprPos),ext2int(RawExprPos,RawExpr,Pos,_,_,_,_),!,
1635 definition_expansion_on_compound_para(Pos,Env,RawExpr,NewPos,OutAst1),
1636 OutAst1 =.. [Functor|Args], OutAst =.. [Functor,NewPos|Args].
1637 definition_expansion_on_raw_def_paras_with_pos(_Env,Ast,Ast).
1638 definition_expansion_on_compound_para(Pos,Env,RawExpr,NewPos2,OutAst) :-
1639 is_definition_call(RawExpr,Env),!, % definition all within parameters of a definition
1640 rewrite_definition(RawExpr,Pos,Env,InterAst,NewPos),
1641 definition_expansion_on_compound_para(NewPos,Env,InterAst,NewPos2,OutAst).
1642 definition_expansion_on_compound_para(Pos,Env,InAst,Pos,OutAst) :-
1643 compound(InAst),
1644 InAst =.. [Functor|Args],!,
1645 same_functor(InAst,OutAst),
1646 OutAst =.. [Functor|NewArgs],
1647 maplist(definition_expansion_on_raw_def_paras_with_pos(Env),Args,NewArgs).
1648 definition_expansion_on_compound_para(Pos,_Env,Ast,Pos,Ast).
1649
1650 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1651 % extract syntax tree positions
1652
1653 remove_pos(Ext,Expr,Pos) :-
1654 ext2int(removepos,Ext,Expr,Pos,_,_,_,_).
1655 remove_pos(Ext,Expr) :-
1656 ext2int(removepos,Ext,Expr,_,_,_,_,_).
1657
1658 % create a enhanced syntax element from a raw input
1659 % ext2int(+Ext,-Expr,-Pos,+Type,+TExpr,+RestInfos,-Result):
1660 % Ext: raw information with position info (from parser)
1661 % Expr: the underlying expression without position info (e.g. identifier(x))
1662 % Pos: the position extracted from the raw expression
1663 % Type: the type used for the typed expression
1664 % TExpr: the new expression in the enhanced syntax tree format
1665 % (but without the information for the root element)
1666 % RestInfos: Additional list of informations that will be stored inside
1667 % the element aside from the position information
1668 % Result: the new completed element (with type and additional information)
1669 % Example: "1+x"
1670 % Ext: add(pos1,integer(pos2,1),identifier(pos3,x)
1671 % Expr: add(integer(pos2,1),identifier(pos3,x))
1672 % Result: b(TExpr,Type,[nodeid(pos1)|RestInfos])
1673 ext2int(Ext,Expr,Pos,Type,TExpr,RestInfos,Res) :-
1674 ext2int(unknown_src,Ext,Expr,Pos,Type,TExpr,RestInfos,Res).
1675 ext2int(Src,Ext,Expr,_Pos,_Type,_TExpr,_RestInfos,_) :-
1676 var(Ext),!,add_error(ext2int,'Variable Ext: ',Src:Expr,Expr),fail.
1677 ext2int(_Src,Ext,Expr,Pos,Type,TExpr,RestInfos,b(TExpr,Type,[nodeid(Pos)|Infos])) :-
1678 % the first argument contains the position information
1679 safe_functor(ext2int_ext,Ext,Functor,Arity),
1680 (Arity=0 -> add_internal_error('Not raw AST:',Ext),fail ; true),
1681 arg(1,Ext,ExtPos),
1682 extract_optional_external_info(ExtPos,Pos,Infos,RestInfos),
1683 % now construct a copy without the first argument
1684 NArity is Arity-1,
1685 safe_functor(ext2int_expr,Expr,Functor,NArity),
1686 copy_ext_term(Arity,Ext,Expr).
1687 % It is possible to inject information into the AST from outside
1688 % by using info(Pos,Info) or info(Pos,[Info1,...,InfoN]) as position
1689 % Those terms are copied directly into the AST.
1690 % The result is returned in form of a difference list I1-I2.
1691 extract_optional_external_info(info(Pos,ExtInfo),Pos,I1,I2) :- !,
1692 ( ExtInfo = [] -> I1=I2
1693 ; ExtInfo = [_|_] -> append(ExtInfo,I2,I1)
1694 ; otherwise -> I1=[ExtInfo|I2]).
1695 extract_optional_external_info(Pos,Pos,Infos,Infos).
1696
1697 copy_ext_term(1,_,_) :- !.
1698 copy_ext_term(N1,Ext,Int) :-
1699 N2 is N1-1, arg(N1,Ext,Arg), arg(N2,Int,Arg),
1700 copy_ext_term(N2,Ext,Int).
1701
1702
1703 check_for_duplicate_raw_ids([],_,_,_,[],TR,TR).
1704 check_for_duplicate_raw_ids([identifier(Pos,IdName)|T],List,Construct,Name,Res,TRin,TRout) :- !,
1705 %print(check(IdName,Name,Construct,List)),nl,
1706 (member(IdName,List)
1707 -> ajoin(['Duplicate identifier ',IdName,' for ',Construct,Name],Msg),
1708 store_typecheck_error(Msg,Pos,TRin,TR2),
1709 check_for_duplicate_raw_ids(T,List,Construct,Name,Res,TR2,TRout)
1710 ; Res = [identifier(Pos,IdName)|ResT],
1711 check_for_duplicate_raw_ids(T,[IdName|List],Construct,Name,ResT,TRin,TRout)).
1712 check_for_duplicate_raw_ids([H|T],List,Construct,Name,[H|RT],TRin,TRout) :-
1713 check_for_duplicate_raw_ids(T,List,Construct,Name,RT,TRin,TRout).
1714
1715 % add variables to the environment
1716 % - the variables are given as raw parser terms
1717 % and returned in typed format
1718 % - additionally the identifier is stored in the list of newly introduced
1719 % identifiers
1720 add_ext_variables(Identifiers, Env, TExprs, NewEnv, TRin, TRout) :-
1721 add_ext_variables_with_info(Identifiers, Env, [], TExprs, NewEnv, TRin, TRout).
1722
1723 add_ext_variables_with_info(Identifiers, Env, AddInfo, TExprs, NewEnv, TRin, TRout) :-
1724 foldl(add_ext_variable_with_info(AddInfo), Identifiers, TExprs, TRin/Env, TRout/NewEnv).
1725 add_ext_variable_with_info(AddInfo, Identifier, TExpr, TRin/Env, TRout/NewEnv) :-
1726 % convert the raw format to the typed format
1727 Expr = identifier(Name),
1728 % Krings: in the following line, AddInfo was set to []
1729 % thus, additional information was only added to the type environment,
1730 % not to the identifier itself. introduced_by was only store inside of
1731 % expressions, not at the identifier declarations. this might break something?
1732 ext2int(add_ext_variables_with_info,Identifier,Expr,_,Type,Expr,AddInfo,TExpr),!,
1733 % add the identifier's type and info to the type environment
1734 get_texpr_info(TExpr,Infos),
1735 % append not needed anymore, as additional information is stored in
1736 % the identifier. see comment above.
1737 %append(AddInfo,Infos,AllInfos),
1738 env_store(Name,Type,Infos,Env,NewEnv),
1739 % store the identifier in the list of newly introduced identifiers
1740 typecheck_result_add_identifier(TExpr,TRin,TRout).
1741 add_ext_variable_with_info(_AddInfo, Expr, TExpr, TRin/Env, TRout/Env) :-
1742 % We expected an identifier but there was something different
1743 ext2int(add_ext_variables_with_info,Expr,_,Pos,_,_,_,_),
1744 ( translate_raw_expr_functor(Expr,TS)
1745 -> ajoin(['Expected identifier, but got operator: ',TS],Msg),
1746 ajoin(['not an identifier:',TS],ID)
1747 ; functor(Expr,F,_), ajoin(['not an identifier:',F],ID),
1748 Msg='Expected identifier'
1749 ),
1750 store_typecheck_error(Msg,Pos,TRin,TRout),
1751 % just to make sure that there is no variable as AST element:
1752 create_texpr(identifier(ID),_,[found(Expr)],TExpr).
1753
1754 translate_raw_expr_functor(Expr,Translation) :-
1755 % note: we cannot call translate_bexpression yet; not yet wrapped and typed !
1756 nonvar(Expr), functor(Expr,F,_),
1757 translate_prolog_constructor(F,Translation).
1758
1759 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1760 % type rules
1761
1762 % predicates
1763 truth :: pred.
1764 falsity :: pred.
1765 conjunct(pred,pred) :: pred.
1766 negation(pred) :: pred.
1767 disjunct(pred,pred) :: pred.
1768 implication(pred,pred) :: pred.
1769 equivalence(pred,pred) :: pred.
1770 equal(A,A) :: pred.
1771 not_equal(A,A) :: pred.
1772 member(A,set(A)) :: pred.
1773 not_member(A,set(A)) :: pred.
1774 subset(set(A),set(A)) :: pred.
1775 subset_strict(set(A),set(A)) :: pred.
1776 not_subset(set(A),set(A)) :: pred.
1777 not_subset_strict(set(A),set(A)) :: pred.
1778 less_equal(integer,integer) :: pred.
1779 less(integer,integer) :: pred.
1780 greater_equal(integer,integer) :: pred.
1781 greater(integer,integer) :: pred.
1782 finite(set(_)) :: pred.
1783 exists(ids,pred) :: pred.
1784 partition(set(T),[set(T)]) :: pred.
1785
1786 % expressions
1787 boolean_true :: boolean.
1788 boolean_false :: boolean.
1789 max_int :: integer.
1790 min_int :: integer.
1791 empty_set :: set(_).
1792 bool_set :: set(boolean).
1793 string_set :: set(string).
1794 convert_bool(pred) :: boolean.
1795 add(integer,integer) :: integer.
1796 minus(integer,integer) :: integer.
1797 unary_minus(integer) :: integer.
1798 multiplication(integer,integer) :: integer.
1799 cartesian_product(set(A),set(B)) :: set(couple(A,B)).
1800 div(integer,integer) :: integer.
1801 floored_div(integer,integer) :: integer.
1802 modulo(integer,integer) :: integer.
1803 power_of(integer,integer) :: integer.
1804 successor :: set(couple(integer,integer)).
1805 predecessor :: set(couple(integer,integer)).
1806 max(set(integer)) :: integer.
1807 min(set(integer)) :: integer.
1808 card(set(_)) :: integer.
1809 couple(A,B) :: couple(A,B).
1810 pow_subset(set(A)) :: set(set(A)).
1811 pow1_subset(set(A)) :: set(set(A)).
1812 fin_subset(set(A)) :: set(set(A)).
1813 fin1_subset(set(A)) :: set(set(A)).
1814 interval(integer,integer) :: set(integer).
1815 union(set(A),set(A)) :: set(A).
1816 intersection(set(A),set(A)) :: set(A).
1817 set_subtraction(set(A),set(A)) :: set(A). /* ?? */
1818 general_union(set(set(A))) :: set(A).
1819 general_intersection(set(set(A))) :: set(A).
1820 relations(set(A),set(B)) :: set(set(couple(A,B))).
1821 identity(set(A)) :: set(couple(A,A)).
1822 event_b_identity :: set(couple(A,A)). % for Rodin 1.0
1823 reverse(set(couple(A,B))) :: set(couple(B,A)). % function inverse ~
1824 first_projection(set(A),set(B)) :: set(couple(couple(A,B),A)).
1825 event_b_first_projection(set(couple(A,B))) :: set(couple(couple(A,B),A)). % should no longer appear after Rodin 1.0
1826 event_b_first_projection_v2 :: set(couple(couple(A,_B),A)). % for Rodin 1.0
1827 second_projection(set(A),set(B)) :: set(couple(couple(A,B),B)).
1828 event_b_second_projection(set(couple(A,B))) :: set(couple(couple(A,B),B)). % should no longer appear after Rodin 1.0
1829 event_b_second_projection_v2 :: set(couple(couple(_A,B),B)). % for Rodin 1.0
1830 composition(set(couple(A,B)),set(couple(B,C))) :: set(couple(A,C)).
1831 ring(set(couple(B,C)),set(couple(A,B))) :: set(couple(A,C)).
1832 direct_product(set(couple(E,F)),set(couple(E,G))) :: set(couple(E,couple(F,G))).
1833 parallel_product(set(couple(E,F)),set(couple(G,H))) :: set(couple(couple(E,G),couple(F,H))).
1834 trans_function(set(couple(A,B))) :: set(couple(A,set(B))).
1835 trans_relation(set(couple(A,set(B)))) :: set(couple(A,B)).
1836 iteration(set(couple(A,A)),integer) :: set(couple(A,A)).
1837 reflexive_closure(set(couple(A,A))) :: set(couple(A,A)).
1838 closure(set(couple(A,A))) :: set(couple(A,A)).
1839 domain(set(couple(A,_))) :: set(A).
1840 range(set(couple(_,B))) :: set(B).
1841 image(set(couple(A,B)),set(A)) :: set(B).
1842 domain_restriction(set(A),set(couple(A,B))) :: set(couple(A,B)).
1843 domain_subtraction(set(A),set(couple(A,B))) :: set(couple(A,B)).
1844 range_restriction(set(couple(A,B)),set(B)) :: set(couple(A,B)).
1845 range_subtraction(set(couple(A,B)),set(B)) :: set(couple(A,B)).
1846 overwrite(set(couple(A,B)),set(couple(A,B))) :: set(couple(A,B)).
1847 partial_function(A,B)::T :- relations(A,B)::T.
1848 total_function(A,B)::T :- relations(A,B)::T.
1849 partial_injection(A,B)::T :- relations(A,B)::T.
1850 total_injection(A,B)::T :- relations(A,B)::T.
1851 partial_surjection(A,B)::T :- relations(A,B)::T.
1852 total_surjection(A,B)::T :- relations(A,B)::T.
1853 total_bijection(A,B)::T :- relations(A,B)::T.
1854 partial_bijection(A,B)::T :- relations(A,B)::T.
1855 total_relation(A,B)::T :- relations(A,B)::T.
1856 surjection_relation(A,B)::T :- relations(A,B)::T.
1857 total_surjection_relation(A,B)::T :- relations(A,B)::T.
1858 seq(set(A)) :: set(seq(A)).
1859 seq1(X)::T :- seq(X)::T.
1860 iseq(X)::T :- seq(X)::T.
1861 iseq1(X)::T :- seq(X)::T.
1862 perm(set(A)) :: set(seq(A)).
1863 empty_sequence :: seq(_).
1864 size(seq(_)) :: integer.
1865 first(seq(A)) :: A.
1866 last(seq(A)) :: A.
1867 front(seq(A)) :: seq(A).
1868 tail(seq(A)) :: seq(A).
1869 rev(seq(A)) :: seq(A).
1870 concat(seq(A),seq(A)) :: seq(A).
1871 insert_front(A,seq(A)) :: seq(A).
1872 insert_tail(seq(A),A) :: seq(A).
1873 restrict_front(seq(A),integer) :: seq(A).
1874 restrict_tail(seq(A),integer) :: seq(A).
1875 general_concat(seq(seq(A))) :: seq(A).
1876 function(set(couple(A,B)),A) :: B.
1877 set_extension([T]) :: set(T).
1878 sequence_extension([T]) :: seq(T).
1879 comprehension_set(ids(T),pred) :: set(T).
1880 event_b_comprehension_set(ids,T,pred) :: set(T).
1881 lambda(ids(A),pred,R) :: set(couple(A,R)).
1882 general_sum(ids,pred,integer) :: integer.
1883 general_product(ids,pred,integer) :: integer.
1884 quantified_union(ids,pred,set(T)) :: set(T).
1885 quantified_intersection(ids,pred,set(T)) :: set(T).
1886 mu(set(T)) :: T.
1887 if_then_else(pred,T,T) :: T.
1888 tree(set(A)) :: set(set(couple(seq(integer),A))). % Section 5.20 of Atelier-B manrefb.pdf
1889 btree(A) :: T :- tree(A) :: T.
1890 tree_over(A) :: set(couple(seq(integer),A)). % dummy function to ease writing of rules below
1891 const(A,seq(TreeA)) :: TreeA :- tree_over(A) :: TreeA.
1892 top(TreeA) :: A :- tree_over(A) :: TreeA.
1893 prefix(TreeA) :: seq(A) :- tree_over(A) :: TreeA.
1894 postfix(TreeA) :: seq(A) :- tree_over(A) :: TreeA.
1895 sizet(TreeA) :: integer :- tree_over(_) :: TreeA.
1896 mirror(TreeA) :: TreeA :- tree_over(_) :: TreeA.
1897 rank(TreeA,seq(integer)) :: integer :- tree_over(_) :: TreeA. % seq(integer) is the type of paths
1898 father(TreeA,seq(integer)) :: seq(integer) :- tree_over(_) :: TreeA.
1899 son(TreeA,seq(integer),integer) :: seq(integer) :- tree_over(_) :: TreeA.
1900 subtree(TreeA,seq(integer)) :: TreeA :- tree_over(_) :: TreeA.
1901 arity(TreeA,seq(integer)) :: integer :- tree_over(_) :: TreeA.
1902 sons(TreeA) :: seq(TreeA) :- tree_over(_) :: TreeA.
1903 bin(A) :: TreeA :- tree_over(A) :: TreeA.
1904 bin(TreeA,A,TreeA) :: TreeA :- tree_over(A) :: TreeA.
1905 infix(TreeA) :: seq(A) :- tree_over(A) :: TreeA.
1906 left(TreeA) :: TreeA :- tree_over(_) :: TreeA.
1907 right(TreeA) :: TreeA :- tree_over(_) :: TreeA.
1908
1909 % substitutions
1910 skip :: subst.
1911 block(subst) :: subst.
1912 precondition(pred,subst) :: subst.
1913 sequence([subst]) :: subst.
1914 any(new_readonly_ids,pred,subst) :: subst.
1915 if([subst]) :: subst.
1916 if_elsif(pred,subst) :: subst.
1917 assertion(pred,subst) :: subst.
1918 let(new_readonly_ids,pred,subst) :: subst.
1919 var(new_ids,subst) :: subst. % was ids instead of new_ids; see test 1658
1920 select([subst],subst) :: subst.
1921 select([subst]) :: subst.
1922 select_when(pred,subst) :: subst.
1923 choice([subst]) :: subst.
1924
1925 % other stuff
1926 witness(_,pred) :: witness.
1927 ordinary :: status.
1928 anticipated(_) :: status.
1929 convergent(_) :: status.
1930
1931
1932 % error_rewrites: common mistakes users make
1933 % the message will be wrapped in 'Did you ' and ' ?'
1934 :- use_module(specfile,[eventb_mode/0]).
1935 error_rewrite(insert_front(A,B),insert_tail(A,B),'use -> instead of <- (sequence append)').
1936 error_rewrite(insert_front(A,B),couple(A,B),'use -> instead of |-> (maplet) or total function (-->)').
1937 error_rewrite(insert_front(A,B),total_function(A,B),'use -> instead of --> (total function)').
1938 error_rewrite(insert_tail(A,B),insert_front(A,B),'use <- instead of -> (sequence prepend)').
1939 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}]
1940 %error_rewrite(image(A,B),function(A,B),'use relational image .[.] instead of function application .(.)'). % does not seem to trigger
1941 error_rewrite(concat(A,B),power_of(A,B),'use ^ (concat) instead of ** (exponentation)').
1942 error_rewrite(power_of(A,B),cartesian_product(A,B),'use ** (exponentation) instead of * (cartesian product)') :- \+ eventb_mode.
1943
1944 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1945
1946
1947 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
1948 % type environment
1949 env_empty(env(Avl)) :- empty_avl(Avl).
1950
1951 env_lookup_type(Id,Env,Type) :-
1952 env_lookup2(Env,Id,Type,_Infos).
1953 env_lookup_infos(Id,Env,Infos) :-
1954 env_lookup2(Env,Id,_Type,Infos).
1955 env_lookup_position_string(Id,Env,PosStr) :-
1956 ? env_lookup2(Env,Id,_Type,Infos),
1957 ? get_info_pos(Infos,Pos), Pos \= none,
1958 ? translate:translate_span(Pos,PosStr).
1959 env_lookup2(env(Avl),Id,Type,Infos) :-
1960 avl_fetch(Id,Avl,entry(Type,Infos)).
1961 env_lookup2(openenv(Open,Env),Id,Type,Infos) :-
1962 ( env_lookup2(Env,Id,Type,Infos) ->
1963 true
1964 ; otherwise ->
1965 openenv_lookup(Open,Id,Type,Infos)).
1966
1967 env_get_visible_ids(env(Avl),Ids) :- avl_domain(Avl,Ids).
1968
1969 env_store(Id,Type,Infos,In,Out) :-
1970 env_store2(In,Id,Type,Infos,Out).
1971 env_store2(env(In),Id,Type,Infos,env(Out)) :-
1972 avl_store(Id,In,entry(Type,Infos),Out).
1973 env_store2(openenv(Open,In),Id,Type,Infos,openenv(Open,Out)) :-
1974 env_store2(In,Id,Type,Infos,Out).
1975
1976 env_store_definition(definition_decl(Name,DefType,_Pos,Params,Body,_Deps), In, Out) :-
1977 env_store(Name, definition(DefType,Params,Body), [], In, Out).
1978
1979 % store a callback predicate in the environment
1980 env_store_operator(Id,Module:Callback,In,Out) :-
1981 % the type is ignored, we just use the info field
1982 env_store(operator(Id),boolean,[Module:Callback],In,Out).
1983
1984 % the open environment acts like the normal type environment with the
1985 % exception that a lookup of an identifier always works, in case the
1986 % identifier was not in the environment, it will be added to it.
1987 openenv(Env,openenv(_,Env)).
1988 openenv_lookup([Head|Tail],Id,Type,Infos) :-
1989 Infos=[],
1990 ( Head = entry(Id,_,_) ->
1991 Head = entry(Id,Type,Infos)
1992 ; otherwise ->
1993 openenv_lookup(Tail,Id,Type,Infos)).
1994 openenv_identifiers(openenv(List,_),Ids) :-
1995 openenv_identifiers2(List,Ids).
1996 openenv_identifiers2(List,[]) :- var(List),!.
1997 openenv_identifiers2([],[]).
1998 openenv_identifiers2([entry(Id,Type,Infos)|Rest],[TId|IdRest]) :-
1999 create_texpr(identifier(Id),Type,Infos,TId),
2000 openenv_identifiers2(Rest,IdRest).
2001
2002 env_identifiers(env(Avl),Ids) :-
2003 avl_domain(Avl,Ids).
2004 env_identifiers(openenv(Open,Env),Ids) :-
2005 env_identifiers(Env,Ids1),
2006 open_env_identifiers(Open,Ids2),
2007 append(Ids2,Ids1,UIds),sort(UIds,Ids).
2008 open_env_identifiers(L,Ids) :- var(L),!,Ids=[].
2009 open_env_identifiers([],[]).
2010 open_env_identifiers([entry(Id,_,_)|Orest],[Id|Irest]) :-
2011 open_env_identifiers(Orest,Irest).
2012
2013
2014 % gives a list of all known identifiers and their information in a type
2015 % environment. A second list of the same size is used to build up a new
2016 % environment whith the same identifiers and types but with new information
2017 env_transform_infos(env(Avl),Ids,OldInfos,NewInfos,env(NewAvl)) :-
2018 % transform a standard environment by converting it to a list,
2019 % iterate over the list and convert the result back
2020 avl_to_list(Avl,OldEntries),
2021 maplist(env_transinfo2,OldEntries,Id_OldInfo_NewInfo,NewEntries),
2022 maplist(split_slash,Id_OldInfo_NewInfo,Ids,Old_New_Info),
2023 maplist(split_slash,Old_New_Info,OldInfos,NewInfos),
2024 ord_list_to_avl(NewEntries,NewAvl).
2025 env_transform_infos(openenv(Open,Env),Ids,OldInfos,NewInfos,openenv(NewOpen,NewEnv)) :-
2026 % an open environment iterates first over the (open) list,
2027 % calls then the code for the standard environment and concatenates
2028 % the generated lists.
2029 env_transinfo_open(Open,Ids1,OldInfos1,NewInfos1,NewOpen),
2030 env_transform_infos(Env,Ids2,OldInfos2,NewInfos2,NewEnv),
2031 append(Ids1,Ids2,Ids),
2032 append(OldInfos1,OldInfos2,OldInfos),
2033 append(NewInfos1,NewInfos2,NewInfos).
2034 % iterate over standard environments
2035 env_transinfo2(Id-entry(Type,OldInfo),Id/(OldInfo/NewInfo),Id-entry(Type,NewInfo)).
2036 % iterate over the open list (last element is not [] but a variable)
2037 env_transinfo_open(OpenEnv,[],[],NewInfo,NewEnv) :- var(OpenEnv),!,OpenEnv=NewEnv,NewInfo=[].
2038 env_transinfo_open([],[],[],[],[]).
2039 env_transinfo_open([entry(Id,Type,OldInfo)|ORest],[Id|IdRest],[OldInfo|OIRest],[NewInfo|NIRest],[entry(Id,Type,NewInfo)|NRest]) :-
2040 env_transinfo_open(ORest,IdRest,OIRest,NIRest,NRest).
2041 split_slash(A/B,A,B).
2042
2043
2044 % utility to portray environment
2045 portray_env(env(In)) :- !, format('ENV:~n',[]),portray_avl_env(In).
2046 portray_env(openenv(Open,In)) :- !, format('OPENENV (~w): ',[Open]),portray_avl_env(In).
2047 portray_env(E) :- !, format('*** UNKNOWN ENV: ~w~n',[E]).
2048 portray_avl_env(A) :- avl_member(Id,A,entry(Type,_Infos)), format(' ~w : ~w~n',[Id,Type]),fail.
2049 portray_avl_env(_) :- nl.
2050
2051 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2052 % fast manual generation of syntax trees
2053 % this code is only for testing, not for use in the regular type checking
2054 % of user-given expressions
2055
2056 :- if(current_prolog_flag(dialect,sicstus)).
2057 :- if((current_prolog_flag(version_data,sicstus(4,X,_,_,_)),X<3)).
2058 :- use_module(library(terms),[term_variables/2]). % is built-in in SICSTUS 4.3
2059 :- endif.
2060 :- endif.
2061
2062 fasttype(Expr,TExpr) :-
2063 term_variables(Expr,OldVars),
2064 ( Expr= +_ -> fasttype2(Expr,TExpr,unknown)
2065 ; otherwise -> fasttype2(Expr,TExpr,_Type)),
2066 term_variables(TExpr,NewVars),
2067 ( fasttype_check_new_vars(NewVars,OldVars) -> true
2068 ; add_error(btypechecker, 'fasttype/2 introduced new variables'),fail).
2069 fasttype2(Type<<Expr,b(TExpr,Type,[]),Type) :- !,
2070 safe_functor(fasttype2,Expr,F,Arity),
2071 safe_functor(fasttype2,TExpr,F,Arity),
2072 safe_functor(fasttype2,Pattern,F,Arity),
2073 ( Pattern :: Type ->
2074 fasttype_args(Arity,Expr,TExpr,Pattern)
2075 ; otherwise ->
2076 fasttype_all_unknown(Arity,Pattern)),
2077 fasttype_args(Arity,Expr,TExpr,Pattern).
2078 fasttype2(+Expr,TExpr,Type) :- !,
2079 ( Type==unknown ->
2080 safe_functor(fasttype2,Expr,F,Arity),
2081 safe_functor(fasttype2,Pattern,F,Arity),
2082 ( fasttype_lookup(Pattern,NType) ->
2083 fasttype2(NType<<Expr,TExpr,NType)
2084 ; otherwise ->
2085 add_error(btypechecker,'Not able to simply infer type:',Expr),fail)
2086 ; otherwise ->
2087 fasttype2(Type<<Expr,TExpr,Type)).
2088 fasttype2([H|T],[TH|TT],_) :- !,fasttype2(H,TH,unknown),fasttype2(T,TT,unknown).
2089 fasttype2(Expr,Expr,_).
2090
2091 fasttype_all_unknown(0,_) :- !.
2092 fasttype_all_unknown(N,Pattern) :-
2093 arg(N,Pattern,unknown),
2094 N1 is N-1, fasttype_all_unknown(N1,Pattern).
2095
2096 fasttype_args(0,_,_,_) :- !.
2097 fasttype_args(N,Expr,NExpr,Pattern) :-
2098 arg(N,Expr,Arg), arg(N,NExpr,NArg),
2099 arg(N,Pattern,ArgType),
2100 fasttype2(Arg,NArg,ArgType),
2101 N1 is N-1,
2102 fasttype_args(N1,Expr,NExpr,Pattern).
2103
2104 fasttype_lookup(integer(_),integer).
2105 fasttype_lookup(Pattern,Type) :- Pattern :: Type.
2106
2107 fasttype_check_new_vars(Old,New) :-
2108 sort(Old,SOld), sort(New, SNew),
2109 fasttype_check_new_vars2(SOld,SNew).
2110 fasttype_check_new_vars2([],_).
2111 fasttype_check_new_vars2([N|NRest],[O|ORest]) :-
2112 ( N==O -> fasttype_check_new_vars(NRest,ORest)
2113 ; otherwise -> fasttype_check_new_vars([N|NRest],ORest)).
2114
2115
2116 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2117 % type expressions without declaring the identifiers
2118
2119 % opentype type-checks an expression without having to declare every used
2120 % identifier in advance.
2121 % Exprs - a list of raw expressions to be type-checked
2122 % InitEnv - an initial environment
2123 % Identifiers - used identifiers that weren't in the initial environment
2124 % DeferredSets - new introduced deferred sets for variables whose type couldn't be infered
2125 % CleanExprs - the type-checked (and cleaned-up) list of expressions
2126 opentype(Exprs,InitEnv,Identifiers,DeferredSets,CleanExprs) :-
2127 openenv(InitEnv,OpenEnv),
2128 do_typecheck(Exprs,OpenEnv,[],TypedExprs,Errors),
2129 ( Errors = [] ->
2130 true
2131 ; Errors = [_|_] ->
2132 throw(type_errors(Errors))),
2133 % all identifier I whose type have the form set(_),
2134 % introduce implicitly a new type global(I)
2135 foldl(declare_deferred_sets,TypedExprs,DS1,[]),
2136 % ensure that all bounded identifiers have ground types
2137 ground_name_types_by_defsets(TypedExprs,DS2),
2138 % ensure that all free identifiers have ground types
2139 openenv_identifiers(OpenEnv,AllIdentifiers),
2140 ground_free_types_by_defsets(AllIdentifiers,DS3),
2141 % join all deferred sets
2142 append([DS1,DS2,DS3],DeferredSets),
2143 % the returned identifiers should not contain the global sets
2144 exclude(tid_in_idlist(DeferredSets),AllIdentifiers,Identifiers),
2145 % clean the expression up
2146 clean_up_l_wo_optimizations(TypedExprs,[],CleanExprs,opentype).
2147
2148 % used by opentype/4
2149 tid_in_idlist(IdList,TId) :-
2150 def_get_texpr_id(TId,Id),
2151 memberchk(Id,IdList).
2152
2153 % used by opentype/4
2154 declare_deferred_sets(TExpr) -->
2155 {syntaxtraversion(TExpr,Expr,Type,_,Subs,_)},
2156 declare_deferred_sets2(Expr,Type),
2157 foldl(declare_deferred_sets,Subs).
2158 declare_deferred_sets2(identifier(Id),Type) -->
2159 {nonvar(Type),Type=set(SType),var(SType),!,SType=global(Id)},[Id].
2160 declare_deferred_sets2(_,_) --> [].
2161
2162 % used by opentype/4, get all types of introduced identifiers
2163 % (e.g. in quantifiers) and ground them by introducing deferred sets
2164 ground_name_types_by_defsets(TExprs,DefSets) :-
2165 get_all_name_types_l(TExprs,Types),
2166 ground_by_defsets(Types,'_NSet',DefSets).
2167 % used by opentype/4, get all types of the given identifiers
2168 % and ground them by introducing deferred sets
2169 ground_free_types_by_defsets(Ids,DefSets) :-
2170 get_texpr_types(Ids,Types),
2171 ground_by_defsets(Types,'_FSet',DefSets).
2172 % takes a list of types and ground them by introducing
2173 % deferred sets, each set's name starting with Prefix
2174 ground_by_defsets(Types,Prefix,DefSets) :-
2175 term_variables(Types,VarTypes),
2176 foldl(ground_by_defsets2(Prefix),VarTypes,DefSets,1,_).
2177 ground_by_defsets2(Prefix,global(DS),DS,N,N2) :-
2178 number_chars(N,CN),
2179 safe_atom_chars(Prefix,CS,ground_by_defsets2_1),
2180 append(CS,CN,Chars),
2181 safe_atom_chars(DS,Chars,ground_by_defsets2_2),
2182 N2 is N+1.
2183
2184 % get the types of all introduced identifiers
2185 % (e.g. in quantifiers)
2186 get_all_name_types(TExpr,Types) :-
2187 syntaxtraversion(TExpr,_,_,_,Subs,Names),
2188 get_texpr_types(Names,NTypes),
2189 append(NTypes,RTypes,Types),
2190 get_all_name_types_l(Subs,RTypes).
2191 get_all_name_types_l(Exprs,Types) :-
2192 maplist(get_all_name_types,Exprs,LTypes),
2193 append(LTypes,Types).
2194
2195 %check_nonvar(Src,V) :- var(V) -> add_error(check_nonvar,'Is a variable: ',Src:V) ; true.
2196
2197 % type-checking of external functions/predicates/substitutions
2198 btype_external_call(FunName,rewrite_protected(TypeParams),FunParams,rewrite_protected(Decl),
2199 DeclType,InputType,Pos,Env,TFunParams,TRin,TRout) :-
2200 add_ext_variables(TypeParams,Env,_TTypeParams,DeclSubenv,TRin,TR1),
2201 btype(extcall_decl,Decl,DeclSubenv,DeclType,_TypedDecl,TR1,TR2),
2202 % TODO: check against originally (for Atelier-B) defined function
2203 % first identify the types of the parameters
2204 btype_l(FunParams,Env,ParamTypes,TFunParams,TR2,TR3),
2205 % now check if the function parameters match the input type
2206 (ParamTypes = []
2207 -> /* the external call has no parameters */
2208 (InputType = empty_type -> TR3=TRout
2209 ; add_error(btype_external_call,'External Definition has no arguments:',FunName),
2210 fail)
2211 ; couplise_list(ParamTypes,JoinedParamType),
2212 unify_types(InputType,JoinedParamType,Pos,no_expression,TR3,TRout)).
2213
2214 % ----------------------------
2215
2216
2217 % add CallPos (if /= unknown) as additional position information for sub-expressions
2218
2219 add_raw_ast_pos_info_context(Ctxt,CPos,Raw,NewRaw) :-
2220 % for definition calls we only store the actual position of the call,
2221 % not in which scope this call itself has occurred (to avoid overly complex messages)
2222 simplify_call_pos(CPos,SimpleCPos),
2223 add_raw_ast_pos_info_context2(Ctxt,SimpleCPos,Raw,NewRaw).
2224
2225 simplify_call_pos(pos_context(P1,_,_),Res) :- !,
2226 simplify_call_pos(P1,Res).
2227 simplify_call_pos(P,P).
2228
2229 add_raw_ast_pos_info_context2(_,_,Raw,NewRaw) :-
2230 simple_raw(Raw),!,
2231 NewRaw=Raw.
2232 add_raw_ast_pos_info_context2(Ctxt,CPos,Raw,NewRaw) :-
2233 list_operator(Raw,Pos,L,NewRaw,NewPos,NewL),!,
2234 combine_pos(Pos,Ctxt,CPos,NewPos),
2235 maplist(add_raw_ast_pos_info_context2(Ctxt,CPos),L,NewL).
2236 add_raw_ast_pos_info_context2(Ctxt,CPos,Raw,NewRaw) :- % print(Raw),nl,
2237 Raw =.. [Op,Pos1|T], raw_operator(Op),
2238 !,
2239 maplist(add_raw_ast_pos_info_context2(Ctxt,CPos),T,T2),
2240 combine_pos(Pos1,Ctxt,CPos,NewPos),
2241 NewRaw =.. [Op,NewPos|T2].
2242 add_raw_ast_pos_info_context2(_,_,R,R). % :- print(uncovered_raw(R)),nl,nl.
2243
2244 %combine_pos(none,P,R) :- !, R=P.
2245 combine_pos(P1,Ctxt,P2,pos_context(P1,Ctxt,P2)).
2246
2247 simple_raw(F) :- functor(F,_,1).
2248 simple_raw(identifier(_,_)).
2249 simple_raw(integer(_,_)).
2250 simple_raw(string(_,_)).
2251
2252 list_operator(comprehension_set(P,Args,L),P,[L],comprehension_set(P2,Args,L2),P2,[L2]).
2253 list_operator(couple(P,L),P,L,couple(P2,L2),P2,L2).
2254 list_operator(definition(P,F,L),P,L,definition(P2,F,L2),P2,L2).
2255 list_operator(external_function_call(P,N,L,F,T1,T2),P,L,
2256 external_function_call(P2,N,L2,F,T1,T2),P2,L2).
2257 list_operator(function(P,F,L),P,[F|L],function(P2,F2,L2),P2,[F2|L2]).
2258 list_operator(general_sum(P,Args,B,E),P,[B,E|Args],
2259 general_sum(P2,Args2,B2,E2),P2,[B2,E2|Args2]).
2260 list_operator(lambda(P,Args,B,E),P,[B,E],lambda(P2,Args,B2,E2),P2,[B2,E2]).
2261 list_operator(sequence_extension(P,L),P,L,sequence_extension(P2,L2),P2,L2).
2262 list_operator(set_extension(P,L),P,L,set_extension(P2,L2),P2,L2).
2263
2264 raw_operator(add).
2265 raw_operator(card).
2266 raw_operator(cartesian_product).
2267 raw_operator(conjunct).
2268 raw_operator(convert_bool).
2269 %raw_operator(couple).
2270 %raw_operator(definition).
2271 raw_operator(disjunct).
2272 raw_operator(div).
2273 raw_operator(domain).
2274 raw_operator(equal).
2275 raw_operator(equivalence).
2276 raw_operator(first).
2277 raw_operator(first_projection).
2278 raw_operator(front).
2279 raw_operator(greater).
2280 raw_operator(greater_equal).
2281 raw_operator(identifier).
2282 raw_operator(image).
2283 raw_operator(implication).
2284 raw_operator(interval).
2285 raw_operator(intersection).
2286 raw_operator(last).
2287 raw_operator(less).
2288 raw_operator(less_equal).
2289 raw_operator(max).
2290 raw_operator(member).
2291 raw_operator(minus_or_set_subtract).
2292 raw_operator(minus).
2293 raw_operator(min).
2294 raw_operator(multiplication).
2295 raw_operator(mult_or_cart).
2296 raw_operator(negation).
2297 raw_operator(not_equal).
2298 raw_operator(not_member).
2299 raw_operator(overwrite).
2300 raw_operator(power_of).
2301 raw_operator(range).
2302 raw_operator(reverse).
2303 raw_operator(seq).
2304 raw_operator(size).
2305 raw_operator(subset).
2306 raw_operator(tail).
2307 raw_operator(unary_minus).
2308 raw_operator(union).
2309 %raw_operator(Op) :- print(uncovered_op(Op)),nl,fail.
2310 % TO DO: add more operators