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 |