| 1 | | % (c) 2009-2025 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(bmachine_construction,[reset_bmachine_construction/0, |
| 6 | | check_machine/4, |
| 7 | | type_in_machine_l/7, |
| 8 | | type_open_predicate_with_quantifier/6, |
| 9 | | get_constructed_machine_name/2, get_constructed_machine_name_and_filenumber/3, |
| 10 | | type_open_formula/8, |
| 11 | | create_scope/6, % create type-checking scope |
| 12 | | filter_linking_invariant/3, |
| 13 | | machine_promotes_operations/2, |
| 14 | | machine_hides_unpromoted_operation/4, |
| 15 | | external_procedure_used/1, |
| 16 | | abstract_variable_removed_in/3, |
| 17 | | dummy_machine_name/2, |
| 18 | | extract_only_definitions/4]). |
| 19 | | |
| 20 | | :- use_module(module_information,[module_info/2]). |
| 21 | | :- module_info(group,typechecker). |
| 22 | | :- module_info(description,'This module contains the rules for loading, including, seeing, etc. B machines, scope of constants, variables, parameters, etc.'). |
| 23 | | |
| 24 | | :- use_module(library(lists)). |
| 25 | | :- use_module(library(avl)). |
| 26 | | |
| 27 | | :- use_module(self_check). |
| 28 | | :- use_module(tools). |
| 29 | | :- use_module(error_manager). |
| 30 | | :- use_module(debug). |
| 31 | | :- use_module(preferences). |
| 32 | | |
| 33 | | :- use_module(btypechecker). |
| 34 | | :- use_module(b_ast_cleanup). |
| 35 | | :- use_module(bsyntaxtree). |
| 36 | | :- use_module(bmachine_structure). |
| 37 | | :- use_module(pragmas). |
| 38 | | :- use_module(b_global_sets,[register_enumerated_sets/2]). |
| 39 | | |
| 40 | | :- use_module(bmachine_static_checks). |
| 41 | | :- use_module(tools_lists,[ord_member_nonvar_chk/2, remove_dups_keep_order/2]). |
| 42 | | |
| 43 | | :- use_module(translate,[print_machine/1]). |
| 44 | | |
| 45 | | |
| 46 | | :- set_prolog_flag(double_quotes, codes). |
| 47 | | |
| 48 | | %maximum_type_errors(100). |
| 49 | | |
| 50 | | :- dynamic debug_machine/0. |
| 51 | | :- dynamic abstract_variable_removed_in/3. |
| 52 | | |
| 53 | | :- use_module(pref_definitions,[b_get_important_preferences_from_raw_machine/2]). |
| 54 | | set_important_prefs_from_machine(Main,Machines) :- |
| 55 | | find_machine(Main,Machines,_MType,_Header,RawMachine), |
| 56 | ? | get_raw_model_type(Main,Machines,RawModelType),!, |
| 57 | | b_get_important_preferences_from_raw_machine(RawMachine,RawModelType), |
| 58 | | check_important_annotions_from_machine(RawMachine). |
| 59 | | |
| 60 | | check_important_annotions_from_machine(RawMachine) :- |
| 61 | ? | member(definitions(_Pos,Defs),RawMachine), |
| 62 | | member(expression_definition(DPOS,'PROB_REQUIRED_VERSION',[],RawValue),Defs),!, |
| 63 | | (RawValue = string(VPos,Version) |
| 64 | | -> add_message(bmachine_construction,'Checking PROB_REQUIRED_VERSION: ',Version,VPos), |
| 65 | | (check_version(Version,VPos) -> true ; true) |
| 66 | | ; add_warning(bmachine_construction,'PROB_REQUIRED_VERSION must provide a version number string.','',DPOS) |
| 67 | | ). |
| 68 | | check_important_annotions_from_machine(_). |
| 69 | | |
| 70 | | :- use_module(version,[compare_against_current_version/2,full_version_str/1]). |
| 71 | | check_version(VersAtom,DPOS) :- atom_codes(VersAtom,Codes), |
| 72 | | split_chars(Codes,".",VCNrs), |
| 73 | | maplist(codes_to_number(DPOS),VCNrs,VNrs), |
| 74 | | compare_against_current_version(VNrs,Result), |
| 75 | | (Result = current_older |
| 76 | | -> full_version_str(Cur), |
| 77 | | ajoin(['This model requires at newer version of ProB than ',Cur,'. Download at least version: '],Msg), |
| 78 | | add_warning(prob_too_old,Msg,VersAtom,DPOS) |
| 79 | | ; true). |
| 80 | | |
| 81 | | codes_to_number(DPOS,C,A) :- |
| 82 | | catch(number_codes(A,C), error(syntax_error(_N),_), |
| 83 | | (atom_codes(AA,C), |
| 84 | | add_warning(bmachine_construction,'Illegal part of version number (use only numbers separated by dots): ',AA,DPOS),fail)). |
| 85 | | |
| 86 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 87 | | |
| 88 | | :- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]). |
| 89 | | |
| 90 | | % typecheck complete machines (incl. includes) |
| 91 | | check_machine(MainName,MachinesMayContainGenerated,Result,FinalErrors) :- |
| 92 | | clear_warnings, |
| 93 | | debug_println(9,checking_machine(MainName)), |
| 94 | | temporary_set_preference(perform_stricter_static_checks,true,CHNG), |
| 95 | | strip_global_pragmas(MachinesMayContainGenerated,Machines,_WasGenerated), % TODO: is generated still used? |
| 96 | | set_important_prefs_from_machine(MainName,Machines), % set important prefs before type-checking,... |
| 97 | | check_main_machine_file_origin(MainName,Machines), |
| 98 | | % we need to find all SEES/USES declarations, because all references |
| 99 | | % refer to the same machine and that has to be included exactly once. |
| 100 | | find_uses(Machines,GlobalUses,NotIncluded,Errors,E1), |
| 101 | | % if a seen/used machine was not included, we include it by constructing |
| 102 | | % a dummy machine that extends the seen/used machine and the origional main machine |
| 103 | | extend_not_included_uses(NotIncluded,MainName,NewMainName,Machines,IMachines), |
| 104 | | % figure out the right order of machines, so that each machine is |
| 105 | | % type-checked before a dependend machine is loaded |
| 106 | | machine_order(IMachines,Order), |
| 107 | | assert_machine_order(Order), |
| 108 | | % expand (= type-check + includes) machines in the given order |
| 109 | | expand_machines(Order,IMachines,GlobalUses,[],Results1,E1,E2), |
| 110 | | % until now, the initialisation section consists of a list of init_stmt(MachineName,Desc,Substitution) |
| 111 | | % fold_initialisation merges those to one substitution, respecting the dependencies |
| 112 | | % between the machines |
| 113 | | maplist(fold_initialisation(Order),Results1,Results), |
| 114 | | % find main machine |
| 115 | | memberchk(machine(NewMainName,MainMachine),Results), %nl,print('MAIN:'),nl,print_machine(MainMachine), |
| 116 | | % if the main machine has parameters, we convert them to global sets resp. constants |
| 117 | | convert_parameters_to_global_sets(E2,[],MainMachine,Result1), |
| 118 | | % add some additional informations about the machine |
| 119 | | add_machine_infos(MainName,Machines,Results,Result1,Result), |
| 120 | | ( debug_machine -> print_machine(Result); true), |
| 121 | | %% comment in to pretty print all machines: |
| 122 | | %( member(machine(Name,Mchx),Results), format('~n*** Machine ~w~n',[Name]), print_machine(Mchx),nl,fail ; true), |
| 123 | | % finalize the list of errors, remove duplicates |
| 124 | | sort(Errors,FinalErrors), |
| 125 | | % output warnings |
| 126 | | show_warnings, |
| 127 | | % run static checks on the resulting machine |
| 128 | | static_check_main_machine(Result), |
| 129 | | reset_temporary_preference(perform_stricter_static_checks,CHNG). |
| 130 | | check_machine(Main,_,Result,FinalErrors) :- |
| 131 | | add_internal_error('Internal error: Checking the machine failed: ', |
| 132 | | check_machine(Main,_,Result,FinalErrors)), |
| 133 | | fail. |
| 134 | | |
| 135 | | % remove global pragrams at top-level and assert them |
| 136 | | strip_global_pragmas([],[],false). |
| 137 | | strip_global_pragmas([generated(POS,M)|Ms],MachinesOut,true) :- !, % @generated pragma used at top of file |
| 138 | | assertz(pragmas:global_pragma(generated,POS)), |
| 139 | | strip_global_pragmas([M|Ms],MachinesOut,_). |
| 140 | | strip_global_pragmas([unit_alias(_,Alias,Content,M)|Ms],MachinesOut,true) :- !, |
| 141 | | assertz(pragmas:global_pragma(unit_alias,[Alias|Content])), |
| 142 | | strip_global_pragmas([M|Ms],MachinesOut,_). |
| 143 | | strip_global_pragmas([M|Ms],[M|SMs],WasGenerated) :- |
| 144 | | strip_global_pragmas(Ms,SMs,WasGenerated). |
| 145 | | |
| 146 | | |
| 147 | | fold_initialisation(Order,machine(Name,Sections),machine(Name,NewSections)) :- |
| 148 | | select_section(initialisation,List,Subst,Sections,NewSections), |
| 149 | | maplist(extract_init_substitutions(List),Order,LSubstitutions), |
| 150 | | append(LSubstitutions,Substitutions), |
| 151 | | create_init_sequence(Substitutions,Subst). |
| 152 | | extract_init_substitutions(Unsorted,Name,Substitutions) :- |
| 153 | | convlist(unzip_init(Name),Unsorted,Substitutions). % keep inits for Name |
| 154 | | unzip_init(Name,init_stmt(Name,Subst),Subst). |
| 155 | | create_init_sequence([],Subst) :- !, create_texpr(skip,subst,[generated],Subst). |
| 156 | | create_init_sequence([I],I) :- !. |
| 157 | | create_init_sequence(L,Sequence) :- |
| 158 | | (L = [First|_], get_texpr_info(First,AllInfos), extract_pos_infos(AllInfos,Pos) -> true ; Pos=[]), |
| 159 | | % TODO: try and merge first and last position info |
| 160 | | (get_preference(allow_overriding_initialisation,true), |
| 161 | | override_initialisation_sequence(L,NL) |
| 162 | | -> NewList=NL ; NewList=L), |
| 163 | | create_texpr(sequence(NewList),subst,[initial_sequence|Pos],Sequence). |
| 164 | | |
| 165 | | :- use_module(b_read_write_info,[get_accessed_vars/4]). |
| 166 | | % override initialisation sequence, remove unnecessary earlier assignments (which may time-out, ...) |
| 167 | | % in future we may inline equalities into becomes_such that, e.g., x :: S ; x := 1 --> x :: X /\ {1} |
| 168 | | % currently x :: S ; x := 1 gets simplified to skip ; x := 1 |
| 169 | | override_initialisation_sequence(List,NewList) :- |
| 170 | | append(Prefix,[Last],List), |
| 171 | | Prefix = [_|_], % there are some earlier initialisation statements to simplify |
| 172 | | get_accessed_vars(Last,[],LIds,Read), |
| 173 | | ord_intersection(LIds,Read,RWIds), |
| 174 | | (RWIds = [] |
| 175 | | -> true |
| 176 | | ; add_warning(b_machine_construction,'Initialisation (override) statement reads written variables:',RWIds,Last) |
| 177 | | ), |
| 178 | | process_override(Last,Prefix, NewLast, SPrefix), |
| 179 | | append(SPrefix,[NewLast],NewList). |
| 180 | | |
| 181 | | |
| 182 | | process_override(b(parallel(List),subst,Info), Prefix, |
| 183 | | b(parallel(NewList),subst,Info), NewPrefix) :- !, |
| 184 | | l_process_override(List,Prefix,NewList,NewPrefix). |
| 185 | | process_override(Subst, Prefix, NewSubst, NewPrefix) :- |
| 186 | | create_after_pred(Subst,AfterPred), |
| 187 | | get_accessed_vars(Subst,[],Ids,Read), |
| 188 | | % write(after_pred(Ids, read(Read))),nl, translate:print_bexpr(AfterPred),nl, |
| 189 | | ord_intersection(Read,Ids,RWIds), |
| 190 | | (RWIds=[] |
| 191 | | -> maplist(try_simplify_init_stmt(Ids,AfterPred,Keep),Prefix,NewPrefix), |
| 192 | | !, |
| 193 | | (Keep==merged_override_stmt |
| 194 | | -> NewSubst = b(skip,subst,[was(Subst)]) |
| 195 | | ; NewSubst = Subst |
| 196 | | ) |
| 197 | | ; add_warning(b_machine_construction,'Initialisation statement reads written variables:',RWIds,Subst), |
| 198 | | fail % we actually have a before after predicate which may modify RWIds |
| 199 | | ). |
| 200 | | process_override(Subst, Prefix , Subst, Prefix) :- add_message(b_machine_construction,'Keeping: ',Subst,Subst). |
| 201 | | |
| 202 | | l_process_override([],Prefix,[],Prefix). |
| 203 | | l_process_override([H|List],Prefix,[H1|NewList],NewPrefix) :- |
| 204 | | process_override(H,Prefix,H1,Prefix1), |
| 205 | | l_process_override(List,Prefix1,NewList,NewPrefix). |
| 206 | | |
| 207 | | :- use_module(library(ordsets)). |
| 208 | | simplify_init_stmt(b(parallel(List),subst,I),OverrideIds,AfterPred,Keep,b(parallel(SList),subst,I)) :- !, |
| 209 | | maplist(try_simplify_init_stmt(OverrideIds,AfterPred,Keep),List,SList). |
| 210 | | simplify_init_stmt(Assign,OverrideIds,AfterPred,Keep,NewSubst) :- |
| 211 | | get_accessed_vars(Assign,[],AssignIds,_Read), |
| 212 | | (ord_subset(OverrideIds,AssignIds), |
| 213 | | merge_statement(Assign,AssignIds,AfterPred,NewSubst), |
| 214 | | Keep = merged_override_stmt |
| 215 | | -> % we need to remove the override assign, if it is non-det. |
| 216 | | add_message(b_machine_construction,'Adapting initialisation due to override: ',NewSubst,Assign) |
| 217 | | ; ord_subset(AssignIds,OverrideIds) |
| 218 | | % The assignment is useless, will be completely overriden |
| 219 | | -> NewSubst = b(skip,subst,[was(Assign)]), |
| 220 | | add_message(b_machine_construction,'Removing initialisation due to override: ',Assign,Assign), |
| 221 | | Keep = keep_override_stmt |
| 222 | | ). |
| 223 | | % TODO: we could simplify IF-THEN-ELSE, ... and other constructs |
| 224 | | |
| 225 | | % Note: the merging assumes the initialisation before the override assigns each overriden variable only once |
| 226 | | try_simplify_init_stmt(OverrideIds,AfterPred,Keep,Stmt,NewStmt) :- |
| 227 | | (simplify_init_stmt(Stmt,OverrideIds,AfterPred,Keep,N) |
| 228 | | -> NewStmt=N ; NewStmt=Stmt). |
| 229 | | |
| 230 | | merge_statement(b(Subst,subst,Info),AssignIds,AfterPred,b(NewSubst,subst,Info)) :- |
| 231 | | merge_stmt_aux(Subst,AssignIds,AfterPred,NewSubst). |
| 232 | | |
| 233 | | merge_stmt_aux(becomes_such(Ids,Pred),_AssignIds,AfterPred,becomes_such(Ids,NewPred)) :- |
| 234 | | conjunct_predicates([AfterPred,Pred],NewPred). |
| 235 | | merge_stmt_aux(becomes_element_of(Ids,Set),_,AfterPred2,becomes_such(Ids,NewPred)) :- |
| 236 | | create_couple(Ids,Couple), |
| 237 | | safe_create_texpr(member(Couple,Set),pred,AfterPred1), |
| 238 | | conjunct_predicates([AfterPred1,AfterPred2],NewPred). |
| 239 | | |
| 240 | | create_after_pred(b(Subst,subst,Info),Pred) :- create_after_pred_aux(Subst,Info,Pred). |
| 241 | | |
| 242 | | create_after_pred_aux(assign_single_id(Id,RHS),Info,b(equal(Id,RHS),pred,Info)). |
| 243 | | create_after_pred_aux(assign(LHS,RHS),_Info,Conj) :- % TODO: split assignments so that we can individually apply preds |
| 244 | | maplist(create_equality,LHS,RHS,Eqs), |
| 245 | | conjunct_predicates(Eqs,Conj). |
| 246 | | % the following two are non-deterministic; hence we need to remove the substitutions |
| 247 | | % in case we have managed to merge them into an earlier becomes_such,... (otherwise we may do a second non-det incompatible choice) |
| 248 | | create_after_pred_aux(becomes_element_of(Id,Set),Info,b(member(Couple,Set),pred,Info)) :- |
| 249 | | create_couple(Id,Couple). |
| 250 | | create_after_pred_aux(becomes_such(_,Pred),_Info,Pred). |
| 251 | | |
| 252 | | |
| 253 | | % ------------------------- |
| 254 | | |
| 255 | | add_machine_infos(MainName,Machines,CheckedMachines,Old,New) :- |
| 256 | ? | get_raw_model_type(MainName,Machines,RawModelType), functor(RawModelType,ModelType,_), % argument is position |
| 257 | | % model type could be machine or system (or model ?) |
| 258 | | !, |
| 259 | | append_to_section(meta,[model_type/ModelType,hierarchy/Hierarchy,header_pos/HeaderPosList],Old,NewT), |
| 260 | | get_refinement_hierarchy(MainName,Machines,Hierarchy), |
| 261 | | find_machine_header_positions(Machines,HeaderPosList), |
| 262 | | add_refined_machine(Hierarchy,CheckedMachines,NewT,New). |
| 263 | | get_refinement_hierarchy(Main,Machines,[Main|Abstractions]) :- |
| 264 | | ( find_refinement(Machines,Main,Abstract) -> |
| 265 | | get_refinement_hierarchy(Abstract,Machines,Abstractions) |
| 266 | | ; |
| 267 | | Abstractions = []). |
| 268 | | find_refinement([M|Rest],Name,Abstract) :- |
| 269 | | ( get_constructed_machine_name(M,Name) -> |
| 270 | | refines(M,Abstract) |
| 271 | | ; |
| 272 | | find_refinement(Rest,Name,Abstract)). |
| 273 | | |
| 274 | | find_machine_header_positions(Machines,SRes) :- |
| 275 | | Header = machine_header(Pos,_Nm,_Paras), |
| 276 | | findall(Name/Pos,find_machine(Name,Machines,_Type,Header,_Sections),Res), |
| 277 | | sort(Res,SRes). |
| 278 | | |
| 279 | | :- use_module(specfile,[animation_minor_mode/1]). |
| 280 | | % check whether the main machine has filenumber 1; if not something strange is going on. |
| 281 | | % an example can be found in prob_examples/public_examples/B/ErrorMachines/IllegalSeesIncludes/WrongNameM1.mch |
| 282 | | check_main_machine_file_origin(MainName,Machines) :- |
| 283 | ? | member(M,Machines), get_machine_parameters(M,MainName,_,Position), |
| 284 | | !, |
| 285 | | (Position = none -> true |
| 286 | | ; get_nr_name(Position,Number,Name) |
| 287 | | -> (Number=1 -> true |
| 288 | | ; ajoin(['Main machine name ',MainName,' overriden by machine in file ',Number,' :'],Msg), |
| 289 | | add_error(bmachine_construction,Msg,Name,Position)) |
| 290 | | ; add_error(bmachine_construction,'Could not extract file number and name:',Position) |
| 291 | | ). |
| 292 | | check_main_machine_file_origin(MainName,_) :- |
| 293 | | add_error(bmachine_construction,'Could not extract file number and name for main machine:',MainName). |
| 294 | | get_nr_name(none,Nr,Name) :- !, Nr=1,Name=none. |
| 295 | | get_nr_name(1,Nr,Name) :- !, Nr=1,Name=none. % TLA mode, animation_minor_mode(tla) not yet set and positions are numbers |
| 296 | | get_nr_name(Position,Number,Name) :- extract_file_number_and_name(Position,Number,Name). |
| 297 | | |
| 298 | | add_refined_machine([_Main,Refined|_],Machines,Old,New) :- |
| 299 | | member(machine(Refined,Body),Machines),!, |
| 300 | | append_to_section(meta,[refined_machine/Body],Old,New). |
| 301 | | add_refined_machine(_,_,M,M). % not refining |
| 302 | | |
| 303 | | convert_parameters_to_global_sets(Ein,Eout) --> |
| 304 | | % extract and remove parameters and constraints |
| 305 | | select_section(parameters,PP,[]), |
| 306 | | select_section(internal_parameters,IP,[]), |
| 307 | | {create_texpr(truth,pred,[],Truth)}, |
| 308 | | select_section(constraints,C,Truth), |
| 309 | | % split parameters into sets and scalars |
| 310 | | { split_list(is_set_parameter,PP,Sets,Scalars), |
| 311 | | foldl(type_set_parameter,Sets,Ein,Eout) }, |
| 312 | | % put the sets to the deferred sets |
| 313 | | append_to_section(deferred_sets,Sets), |
| 314 | | % and the scalars to the constants |
| 315 | | append_to_section(concrete_constants,Scalars), |
| 316 | | append_to_section(concrete_constants,IP), |
| 317 | | % the scalars should be typed by constraints, |
| 318 | | % so move the constraints to the properties |
| 319 | | select_section(properties,OldProps,NewProps), |
| 320 | | {conjunct_predicates([C,OldProps],NewProps)}. |
| 321 | | is_set_parameter(TExpr) :- |
| 322 | | % upper case identifiers denote set parameters, otherwise scalars |
| 323 | | get_texpr_id(TExpr,Name),is_upper_case(Name). |
| 324 | | type_set_parameter(TExpr,Ein,Eout) :- |
| 325 | | get_texpr_id(TExpr,Name), |
| 326 | | get_texpr_type(TExpr,Type), |
| 327 | | get_texpr_pos(TExpr,Pos), |
| 328 | | % we directly type the deferred set |
| 329 | | unify_types_werrors(set(global(Name)),Type,Pos,'PARAMETER',Ein,Eout). |
| 330 | | |
| 331 | | |
| 332 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 333 | | % included machines |
| 334 | | |
| 335 | | expand_machines([],_,_,M,M,Errors,Errors). |
| 336 | | expand_machines([M|Rest],Machines,GlobalUses,Typed,Result,Ein,Eout) :- |
| 337 | ? | ( expand_machine(M,Machines,GlobalUses,Typed,New,Ein,E1) -> true |
| 338 | | ; add_error(bmachine_construction,'Expansion of machine failed:',M),fail), |
| 339 | | expand_machines(Rest,Machines,GlobalUses,[machine(M,New)|Typed],Result,E1,Eout). |
| 340 | | |
| 341 | | % resolve all includes and typecheck the machine |
| 342 | | % expand_machine(Name,Machines,TypeChecked,Expanded) : |
| 343 | | % Name of the Machine to expand |
| 344 | | % Machines contains the list of all loaded machines |
| 345 | | % TypeChecked contains the list of all expanded machines so far |
| 346 | | % Expanded is the resulting machine |
| 347 | | expand_machine(Name,Machines,GlobalUses,TypeChecked,Expanded,Ein,Eout) :- |
| 348 | | debug_format(9,'~nExpanding machine ~w~n',[Name]), |
| 349 | | % find the machine in the list |
| 350 | | find_machine(Name,Machines,MType,Header,RawMachineWithPragmas), |
| 351 | | % remove pragmas for later reattachment |
| 352 | | strip_machine_section_pragmas(RawMachineWithPragmas,RawMachine,_Pragmas), |
| 353 | | % look for abstract machine |
| 354 | | get_abstractions(Name,Machines,TypeChecked,Abstractions), |
| 355 | | % merge all used and seen machines |
| 356 | | use_and_see_machines(RawMachine,TypeChecked,SeenRefs), |
| 357 | | % merge all included machines into one machine |
| 358 | | include_machines(RawMachine, TypeChecked, GlobalUses, Includes, Parameters, Included, Promotes), |
| 359 | | % Parameters contains now a list of parameters for each included machine |
| 360 | | % Included contains now a machine that represents all included machines |
| 361 | | % their parameters are renamed to internal_parameters |
| 362 | | append([Abstractions,Included,SeenRefs],RefMachines), |
| 363 | | % typecheck this machine |
| 364 | | debug_stats(type_machine(Name)), |
| 365 | ? | type_machine(Header,Name,MType,RawMachine,RefMachines,TypedLocal,RefMachines2,Ein,Err1), |
| 366 | | % merge included and including machine |
| 367 | | debug_stats(merge_included_machines(Name)), |
| 368 | | merge_included_machines(Name,TypedLocal,Included,Promotes,Expanded2,Err1,Err2), |
| 369 | | % add some predicates that state the equivalence between arguments |
| 370 | | % in the include statement and the parameters of the included machine |
| 371 | | add_link_constraints(Includes,MType,Parameters,RefMachines2,Expanded2,Expanded3,Err2,Err3), |
| 372 | | % put together refinement and abstraction. |
| 373 | | merge_refinement_and_abstraction(Name,Expanded3,[ref(local,TypedLocal)|RefMachines2],Expanded4,Err3,Eout), |
| 374 | | % merge used machines, will also prefix |
| 375 | | debug_stats(merge_used_machines(Name)), |
| 376 | | merge_used_machines(Included,Expanded4,Expanded5), |
| 377 | | % clean up the syntax tree |
| 378 | | debug_stats(clean_up_machine(Name)), |
| 379 | | clean_up_machine(Expanded5,RefMachines2,Expanded), |
| 380 | | debug_stats(finished_clean_up_and_expand_machine(Name)). |
| 381 | | |
| 382 | | strip_machine_section_pragmas(RawMachineWithPragmas,RawMachine,Pragmas) :- |
| 383 | | selectchk(units(_Pos,RealVariables,Pragmas),RawMachineWithPragmas,TRawMachine), !, |
| 384 | | RawMachine = [RealVariables|TRawMachine]. |
| 385 | | strip_machine_section_pragmas(Machine,Machine,[]). |
| 386 | | |
| 387 | | merge_included_machines(Name, TypedLocal, RefMachines, Promotes, Merged, Ein, Eout) :- |
| 388 | | (Promotes=[] -> true ; assertz(machine_promotes_operations(Name,Promotes))), |
| 389 | | include(is_included_ref,RefMachines,Included), |
| 390 | | create_machine(Name,Empty), |
| 391 | | % move the included operations into the promoted or unpromoted section |
| 392 | | move_operations(Included,Promotes,Included2,Ein,Eout), |
| 393 | | LocalAndIncluded = [ref(local,TypedLocal)|Included2], |
| 394 | | % TODO: make sure that the constants of two instances of the same machine do not repeat (check what should be done for distinct machines with same identifiers) |
| 395 | | concat_sections_of_refs([identifiers,initialisation,operation_bodies, |
| 396 | | assertions,used,values],LocalAndIncluded,Empty,Merged1), |
| 397 | | conjunct_sections_of_refs([constraints,properties,invariant],LocalAndIncluded,Merged1,Merged2), |
| 398 | | concat_section_of_simple_lists(freetypes,LocalAndIncluded,Merged2,Merged3), |
| 399 | | get_section(definitions,TypedLocal,Defs), |
| 400 | | write_section(definitions,Defs,Merged3,Merged). |
| 401 | | is_included_ref(ref(included,_)). |
| 402 | | |
| 403 | | concat_section_of_simple_lists(Sec,References,In,Out) :- |
| 404 | | maplist(extract_machine_from_ref,References,Machines), |
| 405 | | sort_machines_by_global_order(Machines,OMachines), |
| 406 | | foldl(concat_section_of_simple_lists2(Sec),OMachines,In,Out). |
| 407 | | concat_section_of_simple_lists2(Sec,Machine,In,Out) :- |
| 408 | | get_section(Sec,In,Orig), |
| 409 | | get_section(Sec,Machine,List), |
| 410 | | append(Orig,List,NewList), |
| 411 | | write_section(Sec,NewList,In,Out). |
| 412 | | |
| 413 | | merge_used_machines(RefMachines,Old,New) :- |
| 414 | | % get all included machines from the references |
| 415 | | convlist(ref_to_included_machine,RefMachines,Included), |
| 416 | | foldl(merge_used_machines2,Included,Old,New). |
| 417 | | merge_used_machines2(Included,Old,New) :- |
| 418 | | get_section(used,Included,IncludedUse), |
| 419 | | map_split_list(useful_renaming,IncludedUse,RenamingList,_), |
| 420 | | (RenamingList = [] -> New = Old ; rename_used(RenamingList,Old,New)). |
| 421 | | ref_to_included_machine(ref(included,Inc),Inc). |
| 422 | | |
| 423 | | % the renaming does not add a prefix; happens for constants in used/seen machines |
| 424 | | %useless_renaming(includeduse(_Mach,ID,TID)) :- get_texpr_id(TID,ID). |
| 425 | | useful_renaming(includeduse(_Mach,ID,TID),rename(ID,NewID)) :- get_texpr_id(TID,NewID), NewID \= ID. |
| 426 | | |
| 427 | | |
| 428 | | % will add prefixes to identifiers |
| 429 | | % TODO: unclear to me why this cannot be done by rename_bt? Is it for treating SEEN machines not included? |
| 430 | | rename_used(RenamingList,Old,New) :- |
| 431 | | expand_shortcuts([properties,invariant, assertions, |
| 432 | | initialisation,operation_bodies],Sections), % TO DO: also traverse GOAL ? should we later apply this at the REPL level as well ? should we apply it to other DEFINITIONS ? |
| 433 | | foldl(rename_used_sec(RenamingList),Sections,Old,New). |
| 434 | | rename_used_sec(RenamingList,Sec,Old,New) :- |
| 435 | | select_section_texprs(Sec,TExprs,NewTExprs,Old,New), |
| 436 | | rename_used2_l(TExprs,RenamingList,NewTExprs). |
| 437 | | |
| 438 | | rename_used2(TExpr,RenamingList,NewTExpr) :- |
| 439 | | get_texpr_expr(TExpr,operation(Id,Params,Results,Subst)),!, |
| 440 | | get_texpr_exprs(Params,Ps), |
| 441 | | remove_renamings(Ps,RenamingList,NRenamings0), |
| 442 | | get_texpr_exprs(Results,Rs), |
| 443 | | remove_renamings(Rs,NRenamings0,NRenamings), |
| 444 | | rename_used2_l(Params,NRenamings,NParams), % should normally do nothing; unless variable capture occurs |
| 445 | | rename_used2_l(Results,NRenamings,NResults), % ditto |
| 446 | | rename_used2(Subst,NRenamings,NSubst), |
| 447 | | get_texpr_type(TExpr,Type), |
| 448 | | get_texpr_info(TExpr,Info), |
| 449 | | l_rename_info(Info,NRenamings,NewInfo), |
| 450 | | create_texpr(operation(Id,NParams,NResults,NSubst),Type,NewInfo,NewTExpr). |
| 451 | | rename_used2(TExpr,RenamingList,NewTExpr) :- |
| 452 | | % rename identifier by adding machine prefix M.id |
| 453 | | get_texpr_id(TExpr,_), % result is also Id (always ??) |
| 454 | | TExpr = b(_,Type,Info), |
| 455 | | member(usesee(_MachName,Id,_UseOrSeeMode),Info), % TODO: do we need to check MachName matches includeduse/3 above? |
| 456 | | member(rename(Id,NewId),RenamingList), |
| 457 | | % we now rename Id to Name.Id |
| 458 | | !, NewTExpr = b(identifier(NewId),Type,Info). |
| 459 | | %add_message(rename,'Rename ID: ',TExpr,Info),add_message(rename,'Rename ID: ',NewTExpr,NewTExpr). |
| 460 | | rename_used2(TExpr,RenamingList,NTExpr1) :- |
| 461 | | remove_bt(TExpr,Expr,NExpr,NTExpr), |
| 462 | | syntaxtransformation_for_renaming(Expr,Subs,TNames,NSubs,NExpr),!, |
| 463 | | get_texpr_exprs(TNames,Names), |
| 464 | | remove_renamings(Names,RenamingList,NRenamings), |
| 465 | | rename_used2_l(Subs,NRenamings,NSubs), |
| 466 | | rename_infos(NTExpr,NRenamings,NTExpr1). |
| 467 | | rename_used2(TExpr,RenamingList,NTExpr) :- |
| 468 | | add_internal_error('Rename failed: ',rename_used2(TExpr,RenamingList,NTExpr)), |
| 469 | | NTExpr = TExpr. |
| 470 | | |
| 471 | | % update infos, e.g., read/modifies for while loops |
| 472 | | rename_infos(b(E,T,I),RenamingList,b(E,T,NI)) :- |
| 473 | | l_rename_info(I,RenamingList,NI). |
| 474 | | |
| 475 | | l_rename_info([],_,[]). |
| 476 | | l_rename_info([Info|T],RenamingList,[NewInfo|NT]) :- |
| 477 | | rename_info(RenamingList,Info,NewInfo), |
| 478 | | l_rename_info(T,RenamingList,NT). |
| 479 | | |
| 480 | | rename_info(RenamingList,Info,NewInfo) :- info_field_contains_ids(Info,I,NewInfo,SNI),!, |
| 481 | | maplist(rename_usage_info(RenamingList),I,NI), sort(NI,SNI). |
| 482 | | rename_info(_,I,I). |
| 483 | | |
| 484 | | info_field_contains_ids(reads(I),I,reads(SNI),SNI). |
| 485 | | info_field_contains_ids(modifies(I),I,modifies(SNI),SNI). |
| 486 | | info_field_contains_ids(non_det_modifies(I),I,non_det_modifies(SNI),SNI). |
| 487 | | info_field_contains_ids(modifies_locals(I),I,modifies_locals(SNI),SNI). |
| 488 | | info_field_contains_ids(reads_locals(I),I,reads_locals(SNI),SNI). |
| 489 | | info_field_contains_ids(used_ids(I),I,used_ids(SNI),SNI). |
| 490 | | |
| 491 | | rename_usage_info(RenamingList,ID,NewID) :- |
| 492 | | (member(rename(ID,NewID),RenamingList) -> true ; NewID = ID). |
| 493 | | |
| 494 | | |
| 495 | | rename_used2_l([],_,R) :- !, R=[]. |
| 496 | | rename_used2_l([T|Rest],RenamingList,[NT|NRest]) :- |
| 497 | | rename_used2(T,RenamingList,NT), !, |
| 498 | | rename_used2_l(Rest,RenamingList,NRest). |
| 499 | | rename_used2_l(X,Y,Z) :- add_internal_error('Rename failed: ', rename_used2_l(X,Y,Z)),Z=X. |
| 500 | | |
| 501 | | %rename_used_ids(InIds,RenamingList,OutIds) :- |
| 502 | | % maplist(rename_used_ids2(RenamingList),InIds,OutIds). |
| 503 | | %rename_used_ids2(RenamingList,InId,OutId) :- |
| 504 | | % memberchk(rename(InId,I2),RenamingList),!, OutId=I2. |
| 505 | | %rename_used_ids2(_RenamingList,Id,Id). |
| 506 | | |
| 507 | | get_abstractions(CName,Machines,TypedMachines,[ref(abstraction,Abstraction)]) :- |
| 508 | ? | refines(M,AName), |
| 509 | | get_constructed_machine_name(M,CName), |
| 510 | | memberchk(M,Machines),!, |
| 511 | | memberchk(machine(AName,Abstraction),TypedMachines). |
| 512 | | get_abstractions(_,_,_,[]). |
| 513 | | |
| 514 | | get_includes_and_promotes(Sections,M,Includes,Promotes) :- |
| 515 | | optional_rawmachine_section(includes,Sections,[],Includes1), |
| 516 | | optional_rawmachine_section(imports,Sections,[],Imports), |
| 517 | | optional_rawmachine_section(extends,Sections,[],Extends), |
| 518 | | optional_rawmachine_section(promotes,Sections,[],Promotes1), |
| 519 | | append([Includes1,Extends,Imports],Includes), |
| 520 | | maplist(expand_extends(M),Extends,Promotes2), |
| 521 | | append([Promotes1|Promotes2],Promotes). |
| 522 | | expand_extends(Machines,machine_reference(_,Ref,_),Promotes) :- |
| 523 | | split_prefix(Ref,Prefix,Name), |
| 524 | | memberchk(machine(Name,Body),Machines), |
| 525 | | get_section(promoted,Body,Promoted), |
| 526 | | prefix_identifiers(Promoted,Prefix,Renamings), |
| 527 | | rename_bt_l(Promoted,Renamings,TPromotes), |
| 528 | | maplist(add_nonpos,TPromotes,Promotes). |
| 529 | | add_nonpos(TId,identifier(none,Id)) :- |
| 530 | | get_texpr_id(TId,op(Id)). |
| 531 | | |
| 532 | | move_operations([],Promotes,[],Ein,Eout) :- |
| 533 | | foldl(add_promotes_not_found_error,Promotes,Ein,Eout). |
| 534 | | move_operations([ref(_,IncMachine)|IncRest],Promotes,[ref(included,NewIncMachine)|RefRest],Ein,Eout) :- |
| 535 | | move_operations2(IncMachine,Promotes,NewIncMachine,RestPromotes), |
| 536 | | move_operations(IncRest,RestPromotes,RefRest,Ein,Eout). |
| 537 | | move_operations2(Included,Promotes,Result,RestPromotes) :- |
| 538 | | select_section(promoted,IncOperations,Promoted,Included,Included1), |
| 539 | | select_section(unpromoted,OldUnpromoted,Unpromoted,Included1,Result), |
| 540 | | filter_promoted(IncOperations,Promotes,Promoted,NewUnpromoted,RestPromotes), |
| 541 | | append(OldUnpromoted,NewUnpromoted,Unpromoted). |
| 542 | | filter_promoted([],Promotes,[],[],Promotes). |
| 543 | | filter_promoted([TExpr|OpsRest],Promotes,Promoted,Unpromoted,RestPromotes) :- |
| 544 | | get_texpr_id(TExpr,op(P)), |
| 545 | | ( select(identifier(_,P),Promotes,RestPromotes1) -> |
| 546 | | !,Promoted = [TExpr|RestPromoted], |
| 547 | | Unpromoted = RestUnpromoted |
| 548 | | ; |
| 549 | | RestPromotes1 = Promotes, |
| 550 | | Promoted = RestPromoted, |
| 551 | | Unpromoted = [TExpr|RestUnpromoted]), |
| 552 | | filter_promoted(OpsRest,RestPromotes1,RestPromoted,RestUnpromoted,RestPromotes). |
| 553 | | add_promotes_not_found_error(identifier(Pos,Id),[error(Msg,Pos)|E],E) :- |
| 554 | | ajoin(['Promoted operation ',Id,' not found'],Msg). |
| 555 | | |
| 556 | | find_machine(Name,Machines,Type,Header,Sections) :- |
| 557 | | Header = machine_header(_,Name,_), |
| 558 | ? | ( (member(abstract_machine(_,_ModelType,Header,Sections),Machines), |
| 559 | | Type=machine) |
| 560 | | ; (member(refinement_machine(_,Header,_Abstract,Sections),Machines), |
| 561 | | Type=refinement) |
| 562 | | ; (member(implementation_machine(_,Header,_Abstract,Sections),Machines), |
| 563 | | Type=implementation)), |
| 564 | | !. |
| 565 | | |
| 566 | | include_machines(RawMachine, TypeChecked, GlobalUses, Includes, Parameters, Included, Promotes) :- |
| 567 | | get_includes_and_promotes(RawMachine,TypeChecked,Includes,Promotes), |
| 568 | | maplist(include_machine(TypeChecked, GlobalUses), Includes, Parameters, Singles), |
| 569 | | remove_duplicate_set_inclusions(Singles,Singles1), |
| 570 | | % duplicate constants inclusion is handled currently in concat_section_contents via section_can_have_duplicates |
| 571 | | % create refs |
| 572 | | maplist(create_ref,Singles1,Included). |
| 573 | | create_ref(IncMachine,ref(included,IncMachine)). |
| 574 | | |
| 575 | | % it is possible that a deferred or enumerated set is declared in an included machine |
| 576 | | % that is included more than once. We remove all but one occurrences. |
| 577 | | remove_duplicate_set_inclusions([],[]). |
| 578 | | remove_duplicate_set_inclusions([M],[M]) :- !. |
| 579 | | remove_duplicate_set_inclusions([M|Rest],[M|CleanedRest]) :- |
| 580 | | get_section(deferred_sets,M,DSets), |
| 581 | | get_section(enumerated_sets,M,ESets), |
| 582 | | get_section(enumerated_elements,M,EElements), |
| 583 | | append([DSets,ESets,EElements],Identifiers), |
| 584 | | sort(Identifiers,SortedIds), |
| 585 | | maplist(remove_duplicate_sets2(SortedIds),Rest,Rest2), |
| 586 | | remove_duplicate_set_inclusions(Rest2,CleanedRest). |
| 587 | | remove_duplicate_sets2(Identifiers,M,Cleaned) :- |
| 588 | | remove_duplicate_sets_section(deferred_sets,Identifiers,M,M1), |
| 589 | | remove_duplicate_sets_section(enumerated_sets,Identifiers,M1,M2), |
| 590 | | remove_duplicate_sets_section(enumerated_elements,Identifiers,M2,Cleaned). |
| 591 | | remove_duplicate_sets_section(Section,Identifiers,In,Out) :- |
| 592 | | select_section(Section,Old,New,In,Out), |
| 593 | | %get_texpr_ids(Identifiers,II),format('Removing duplicates ~w = ~w~n',[Section,II]), |
| 594 | | exclude(element_is_duplicate(Identifiers),Old,New). |
| 595 | | |
| 596 | | element_is_duplicate(Identifiers,TId) :- |
| 597 | | get_texpr_id(TId,Name), |
| 598 | | get_texpr_type(TId,Type), |
| 599 | | get_texpr_id(ToRemove,Name), |
| 600 | | get_texpr_type(ToRemove,Type), |
| 601 | | ord_member_nonvar_chk(ToRemove,Identifiers), |
| 602 | | get_texpr_info(TId,InfosA), |
| 603 | | get_texpr_info(ToRemove,InfosB), |
| 604 | | member(def(Sec,File),InfosA), |
| 605 | | member(def(Sec,File),InfosB), |
| 606 | | debug_format(5,'Removed duplicate included identifier: ~w~n',[Name]), |
| 607 | | !. |
| 608 | | |
| 609 | | include_machine(TypeChecked,GlobalUses,machine_reference(_Pos,FullRef,_Args), |
| 610 | | parameters(FullRef,Parameters), TM) :- |
| 611 | | split_prefix(FullRef,Prefix,Name), |
| 612 | | % TM1 is the already typechecked included machine: |
| 613 | ? | member(machine(Name,TM1),TypeChecked),!, |
| 614 | | debug_println(9,including_machine(Name)), |
| 615 | | % TM2 is a fresh copy, so we prevent unification of the parameter types: |
| 616 | | (get_section(parameters,TM1,[]) -> TM2=TM1 |
| 617 | | ; copy_term(TM1,TM2) % this can be expensive; only copy if there are parameters |
| 618 | | ), |
| 619 | | % If the included machine is used somewhere, we store the identifiers |
| 620 | | % to enable joining the different references later: |
| 621 | | include_usings(Name,GlobalUses,TM2,TM3), |
| 622 | | % TM3 is typechecked and all internal variables are renamed with a prefix |
| 623 | | hide_private_information(Name,FullRef,TM3,TM4), |
| 624 | | % TM4 is typechecked, and if it was referenced with a prefix (e.g. INCLUDES p.M2) |
| 625 | | % all variables are prefixed |
| 626 | | %print(prefixing(Prefix)),nl, |
| 627 | | prefix_machine(Prefix,TM4,TM5), |
| 628 | | % We need the parameters later to state their equivalence to the arguments |
| 629 | | get_section(parameters,TM5,Parameters), |
| 630 | | % We move the parameters to the internal parameters, because the resulting |
| 631 | | % machine has only the parameters of the including machine. |
| 632 | | parameters_to_internal(TM5,TM). |
| 633 | | |
| 634 | | include_usings(Name,GlobalUses,Old,New) :- |
| 635 | ? | ( member(usemch(Name,Prefix,_Kind,_FromMch,_Pos),GlobalUses) -> |
| 636 | | add_machine_prefix(Name,Prefix,FullName), |
| 637 | | store_usage_info(Old,FullName,UsedInfo), |
| 638 | | append_to_section(used,UsedInfo,Old,New) |
| 639 | | ; |
| 640 | | Old = New). |
| 641 | | % returns a list of which identifiers are used in the machine |
| 642 | | % for each identifier, we have a trible includeuse(Name,Id,TExpr) |
| 643 | | % where Name is the name of the used machine, Id is the |
| 644 | | % original ID and TExpr is the currently used reference to this |
| 645 | | % identifier |
| 646 | | store_usage_info(Machine,Name,UsedInfo) :- |
| 647 | | expand_shortcuts([identifiers],IdSections), |
| 648 | | foldl(store_usage_info2(Machine,Name),IdSections,UsedInfo,[]). |
| 649 | | store_usage_info2(Machine,Name,Sec,I,O) :- |
| 650 | | get_section(Sec,Machine,Content), |
| 651 | | foldl(store_usage_info3(Name),Content,I,O). |
| 652 | | store_usage_info3(Name,TId,[includeduse(Name,Id,TId)|L],L) :- |
| 653 | | get_texpr_id(TId,Id). |
| 654 | | |
| 655 | | % conjunct sections that contain predicates (CONSTRAINTS, PROPERTIES, INVARIANT) |
| 656 | | conjunct_sections_of_refs(Sections1,References,Old,New) :- |
| 657 | | expand_shortcuts(Sections1,Sections), |
| 658 | | maplist(extract_machine_from_ref,References,Machines), |
| 659 | | sort_machines_by_global_order(Machines,OMachines), |
| 660 | | foldl(conjunct_sections2(OMachines),Sections,Old,New). |
| 661 | | conjunct_sections2(Machines,Section,Old,New) :- |
| 662 | | % Section is constraints,properties,invariant, ... |
| 663 | | write_section(Section,NewContent,Old,New), % prepare new section |
| 664 | | get_section_of_machines(Machines,Section,Preds), |
| 665 | | %maplist(get_machine_name,Machines,Ns),print(got_sections(Section,Ns)),nl, |
| 666 | | %translate:l_print_bexpr_or_subst(Preds),nl, |
| 667 | | conjunct_predicates(Preds,NewContent). |
| 668 | | |
| 669 | | |
| 670 | | % merge sections that contain a list of expressions/formulas like identifiers, assertions, ... |
| 671 | | concat_sections_of_refs(Sections1,References,Old,New) :- |
| 672 | | maplist(extract_machine_from_ref,References,Machines), |
| 673 | | maplist(create_tag_by_reference,References,Tags), |
| 674 | | sort_machines_by_global_order(Machines,Tags,OMachines,STags), |
| 675 | | % should we only sort for some sections, e.g., assertions |
| 676 | | % for each machine, create a tag where the expression comes from |
| 677 | | concat_sections(Sections1,OMachines,STags,Old,New). |
| 678 | | |
| 679 | | extract_machine_from_ref(ref(_,M),M). |
| 680 | | |
| 681 | | create_tag_by_reference(ref(local,_Machine),[]) :- !. |
| 682 | | create_tag_by_reference(ref(RefType,Machine),[RefType/Name]) :- |
| 683 | | get_machine_name(Machine,Name). |
| 684 | | |
| 685 | | concat_sections(Sections1,Machines,Tags,Old,New) :- |
| 686 | | expand_shortcuts(Sections1,Sections), |
| 687 | | foldl(concat_section2(Machines,Tags),Sections,Old,New). |
| 688 | | concat_section2(Machines,Tags,Section,Old,New) :- |
| 689 | | write_section(Section,NewContent,Old,New), |
| 690 | | maplist(get_tagged_lsection_of_machine(Section),Machines,Tags,Contents), |
| 691 | | concat_section_contents(Section,Contents,NewContent). |
| 692 | | |
| 693 | | concat_section_contents(_,[SingleContent],Res) :- !, Res=SingleContent. % no need to remove_dups |
| 694 | | concat_section_contents(Section,Contents,NewContent) :- |
| 695 | | append(Contents,ConcContents), |
| 696 | | (section_can_have_duplicates(Section) |
| 697 | | -> remove_dup_tids_keep_order(ConcContents,NewContent) |
| 698 | | ; NewContent=ConcContents). |
| 699 | | |
| 700 | | % remove_dups version which keeps order of original elements |
| 701 | | % and works with typed identifiers |
| 702 | | % used if a machine is seen multiple times with different prefixes for e.g. constants |
| 703 | | % see Section 7.26 of Atelier-B handbook: |
| 704 | | % nom des éléments énumérés et des constantes de MSees, sans le préfixe de |
| 705 | | % renommage, si plusieurs instances de machines sont vues, les noms des |
| 706 | | % données ne doivent pas être répétés, |
| 707 | | remove_dup_tids_keep_order([],[]). |
| 708 | | remove_dup_tids_keep_order([H|T],[H|Res]) :- empty_avl(E), |
| 709 | | get_texpr_id(H,ID),avl_store(ID,E,true,A1), |
| 710 | | rem_dups3(T,A1,Res). |
| 711 | | |
| 712 | | rem_dups3([],_,[]). |
| 713 | | rem_dups3([H|T],AVL,Res) :- |
| 714 | | get_texpr_id(H,ID), |
| 715 | | (avl_fetch(ID,AVL) -> rem_dups3(T,AVL,Res) |
| 716 | | ; Res=[H|TRes], |
| 717 | | avl_store(ID,AVL,true,AVL1), |
| 718 | | rem_dups3(T,AVL1,TRes)). |
| 719 | | |
| 720 | | % see issue PROB-403 |
| 721 | | section_can_have_duplicates(X) :- section_can_be_included_multiple_times_nonprefixed(X). |
| 722 | | % should we also remove duplicates in PROPERTIES section ? cf. machines used in test 1857 |
| 723 | | |
| 724 | | |
| 725 | | get_tagged_lsection_of_machine(Section,Machine,Tags,TaggedContent) :- |
| 726 | | get_section(Section,Machine,Content), |
| 727 | | (Tags=[] -> TaggedContent=Content ; maplist(tag_with_origin(Tags),Content,TaggedContent)). |
| 728 | | |
| 729 | | tag_with_origin(Origins,TExpr,TaggedExpr) :- |
| 730 | | change_info_of_expression_or_init(TExpr,Info,TaggedInfo,TaggedExpr), |
| 731 | | % add a new origin to the old tag or if not existent, add a new info field |
| 732 | | ( Origins = [] -> TaggedInfo = Info |
| 733 | | ; selectchk(origin(Orest),Info,origin(Onew),TaggedInfo) -> append(Origins,Orest,Onew) |
| 734 | | ; TaggedInfo = [origin(Origins)|Info]). |
| 735 | | % the substitutions in the initialisation are additionally wrapped by an init_stmt/2 term |
| 736 | | % a small hack to work with those too. |
| 737 | | % TODO: this became a very ugly hack -- redo! |
| 738 | | change_info_of_expression_or_init(init_stmt(A,OExpr),Old,New,init_stmt(A,NExpr)) :- % ... |
| 739 | | !,change_info_of_expression_or_init(OExpr,Old,New,NExpr). |
| 740 | | % ignore the info for includeduse/3 completely |
| 741 | | change_info_of_expression_or_init(includeduse(A,B,C),[],_,includeduse(A,B,C)) :- !. |
| 742 | | change_info_of_expression_or_init(freetype(FTypeId,Cases),[],_,freetype(FTypeId,Cases)) :- !. |
| 743 | | change_info_of_expression_or_init(OExpr,Old,New,NExpr) :- |
| 744 | | create_texpr(Expr,Type,Old,OExpr),!, |
| 745 | | create_texpr(Expr,Type,New,NExpr). |
| 746 | | change_info_of_expression_or_init(OExpr,Old,New,NExpr) :- |
| 747 | | add_internal_error('Illegal typed expression:',change_info_of_expression_or_init(OExpr,Old,New,NExpr)), |
| 748 | | Old=[], NExpr=OExpr. |
| 749 | | |
| 750 | | % adds a prefix to all variables and promoted operations |
| 751 | | prefix_machine('',TM,TM) :- !. |
| 752 | | prefix_machine(Prefix,Old,New) :- |
| 753 | | debug_println(5,prefixing_machine(Prefix)), |
| 754 | | expand_shortcuts([variables,promoted], RenamedIdentiferSections), |
| 755 | | get_all_identifiers(RenamedIdentiferSections,Old,Identifiers), |
| 756 | | prefix_identifiers(Identifiers,Prefix,Renamings), |
| 757 | | find_relevant_sections(RenamedIdentiferSections,[machine],Sections1), |
| 758 | | append(RenamedIdentiferSections,Sections1,Sections), |
| 759 | | rename_in_sections(Sections,Renamings,Old,M), |
| 760 | | rename_includeduse(M,Renamings,New). |
| 761 | | rename_includeduse(Old,Renamings,New) :- |
| 762 | | select_section(used,OldContent,NewContent,Old,New), |
| 763 | | maplist(rename_includeduse2(Renamings),OldContent,NewContent). |
| 764 | | rename_includeduse2(Renamings,includeduse(M,N,TExpr),includeduse(M,N,NExpr)) :- |
| 765 | | rename_bt(TExpr,Renamings,NExpr). |
| 766 | | |
| 767 | | get_all_identifiers(Sections1,M,Identifiers) :- |
| 768 | | expand_shortcuts(Sections1,Sections), |
| 769 | | maplist(get_all_identifiers2(M),Sections,LIdentifiers), |
| 770 | | append(LIdentifiers,Identifiers). |
| 771 | | get_all_identifiers2(M,Sec,Identifiers) :- |
| 772 | | get_section(Sec,M,Identifiers). |
| 773 | | |
| 774 | | % hide all parameters and unpromoted operations |
| 775 | | hide_private_information(MachName,Prefix,Machine,NewMachine) :- |
| 776 | | get_section(parameters,Machine,Params), |
| 777 | | get_section(unpromoted,Machine,UnPromoted), |
| 778 | | append(Params,UnPromoted,ToHide), |
| 779 | | %debug_println(9,hide_private(Prefix,ToHide)), |
| 780 | | ( ToHide = [] -> NewMachine=Machine |
| 781 | | ; |
| 782 | | debug_format(9,'Hiding private parameters ~w and unpromoted operations ~w of machine ~w~n', |
| 783 | | [Params,UnPromoted,MachName]), |
| 784 | | maplist(store_hides_operation_info(MachName,Prefix),UnPromoted), |
| 785 | | prefix_identifiers(ToHide,Prefix,Renamings), |
| 786 | | % we have to do the renaming in promoted operations, too, because |
| 787 | | % those operations might use the renamed parameters and their reads/modifies |
| 788 | | % info must be updated |
| 789 | | rename_in_sections([parameters,promoted,unpromoted],Renamings,Machine,Machine1), |
| 790 | | rename_includeduse(Machine1,Renamings,Machine2), |
| 791 | | % now find sections that can see parameters,operations: |
| 792 | | rename_relevant_sections([parameters,operations],Renamings,Machine2,NewMachine) |
| 793 | | ). |
| 794 | | |
| 795 | | % store information about which operations got renamed: |
| 796 | | store_hides_operation_info(MachName,Prefix,TExpr) :- Prefix \= '', |
| 797 | | prefix_identifier(Prefix,TExpr,rename(op(Old),op(New))), |
| 798 | | get_texpr_pos(TExpr,Pos), |
| 799 | | !, |
| 800 | | debug_format(19,'Hiding unpromoted operation ~w in machine ~w, new name: ~w~n',[Old,MachName,New]), |
| 801 | | assertz(machine_hides_unpromoted_operation(Old,MachName,New,Pos)). |
| 802 | | store_hides_operation_info(_,_,_). |
| 803 | | |
| 804 | | prefix_identifiers(Identifiers,'',Identifiers) :- !. |
| 805 | | prefix_identifiers(Old,Prefix,New) :- |
| 806 | | maplist(prefix_identifier(Prefix),Old,New). |
| 807 | | prefix_identifier(Prefix,TExpr,rename(Old,New)) :- |
| 808 | | get_texpr_expr(TExpr,identifier(Old)), |
| 809 | | (Old=op(OI) -> New=op(NI) ; OI=Old,NI=New), |
| 810 | | ajoin([Prefix,'.',OI],NI). % , print(rename(Old,New)),nl. |
| 811 | | |
| 812 | | parameters_to_internal(M1,M2) :- |
| 813 | | select_section(internal_parameters,OldParams,Params,M1,M3), |
| 814 | | select_section(parameters,NewParams,[],M3,M2), |
| 815 | | append(OldParams,NewParams,Params). |
| 816 | | |
| 817 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 818 | | % uses and sees relations |
| 819 | | find_uses(Machines,GlobalUses,NotIncludedWoDups,Ein,Eout) :- |
| 820 | | findall(usemch(UsedMch,UPrefix,Kind,FromMchName,Pos), |
| 821 | | use_usage(Machines,Pos,Kind,UsedMch,UPrefix,FromMchName), UnsortedUses), |
| 822 | | sort(UnsortedUses,Uses), |
| 823 | | check_include_use(Uses,Machines,NotIncluded,Ein,Eout), |
| 824 | | remove_duplicate_uses(NotIncluded,NotIncludedWoDups), |
| 825 | | GlobalUses = Uses. %maplist(remove_prefix,Uses,GlobalUses). |
| 826 | | |
| 827 | | %remove_prefix(usemch(U,_,_,_,_),U). |
| 828 | | same_usemch(usemch(U,Prefix,_,_,_),usemch(U,Prefix,_,_,_)). % use same machine with same prefix |
| 829 | | same_usemch(usemch_not_inc(U,Prefix,_,_,_,_),usemch_not_inc(U,Prefix,_,_,_,_)). |
| 830 | | |
| 831 | | % remove duplicate uses: a non-included/imported machine can be seen in many places; |
| 832 | | % we only need to add it later once to the dummy machine |
| 833 | | remove_duplicate_uses([],R) :- !, R=[]. |
| 834 | | remove_duplicate_uses([USE|T],Res) :- remove_dup_aux(T,USE,Res). |
| 835 | | remove_dup_aux([],USE,[USE]). |
| 836 | | remove_dup_aux([USE|T],PREVUSE,Res) :- |
| 837 | | (same_usemch(USE,PREVUSE) -> remove_dup_aux(T,PREVUSE,Res) |
| 838 | | ; Res = [PREVUSE|TR], remove_dup_aux(T,USE,TR)). |
| 839 | | |
| 840 | | |
| 841 | | % check_include_use/5 checks if the used machines are included in any machine |
| 842 | | % check_include_use(+Uses,+Machines,-NotIncluded,Ein,Eout) |
| 843 | | % Uses: The list of machine names that are used |
| 844 | | % Machines: The list of machines |
| 845 | | % NotIncluded: The list of used machines (their names) that are not included |
| 846 | | % Ein/Eout: The errors (as difference-list) |
| 847 | | check_include_use([],_,[],Errors,Errors). |
| 848 | | check_include_use([USEMCH|Rest],Machines,NotIncluded,Ein,Eout) :- |
| 849 | | USEMCH = usemch(UsedMach,UsePrefix,Kind,FromMchName,Pos), |
| 850 | | findall(i(MachName,UsePrefix,IPos),include_usage(Machines,UsedMach,UsePrefix,MachName,IPos),Inc), |
| 851 | | ( Inc=[] -> Ein=E1, |
| 852 | | % find all places where the machine is included with another prefix |
| 853 | | findall(OtherPrefix,include_usage(Machines,UsedMach,OtherPrefix,_,_IPos),OtherInclusions), |
| 854 | | NotIncluded = [usemch_not_inc(UsedMach,UsePrefix,Kind,FromMchName,Pos,OtherInclusions)|RestNotIncluded], |
| 855 | | (debug_mode(off),OtherInclusions=[],UsePrefix='' -> true |
| 856 | | ; add_machine_prefix(UsedMach,UsePrefix,FullName), |
| 857 | | (OtherInclusions=[] |
| 858 | | -> ajoin(['machine ',Kind, ' in ', FromMchName, |
| 859 | | ' not included/imported anywhere else (will create dummy top-level machine to include it): '],Msg) |
| 860 | | ; ajoin_with_sep(OtherInclusions,',',I2), |
| 861 | | (UsePrefix='' |
| 862 | | -> ajoin(['machine ',Kind, ' in ', FromMchName, |
| 863 | | ' without prefix only included/imported with prefixes [',I2, |
| 864 | | '] (will create dummy top-level machine to include it): '],Msg) |
| 865 | | ; I2='' |
| 866 | | -> ajoin(['machine ',Kind, ' in ', FromMchName, |
| 867 | | ' only included/imported without prefix (will create dummy top-level machine to include it): '],Msg) |
| 868 | | ; ajoin(['machine ',Kind, ' in ', FromMchName, ' only included/imported with other prefixes [',I2, |
| 869 | | '] (will create dummy top-level machine to include it): '],Msg) |
| 870 | | ) |
| 871 | | ), |
| 872 | | add_message(bmachine_construction,Msg,FullName,Pos) |
| 873 | | ) |
| 874 | | ; Inc=[_] -> NotIncluded = RestNotIncluded, Ein=E1 |
| 875 | | ; Inc=[i(_M1,_,Pos1),i(_M2,_,Pos2)|_], |
| 876 | | NotIncluded = RestNotIncluded, |
| 877 | | translate_span(Pos1,PS1), |
| 878 | | translate_span(Pos2,PS2), |
| 879 | | (UsePrefix = '' |
| 880 | | -> ajoin([Kind,' machine ',UsedMach,' is included more than once: ',PS1,' and ',PS2],Msg) |
| 881 | | ; ajoin([Kind,' machine ',UsedMach,' is included more than once with prefix ',UsePrefix, |
| 882 | | ': ',PS1,' and ',PS2],Msg) |
| 883 | | ), |
| 884 | | Ein = [error(Msg,Pos)|E1] |
| 885 | | ), |
| 886 | | check_include_use(Rest,Machines,RestNotIncluded,E1,Eout). |
| 887 | | % extend_not_included_uses(+Uses,+Main,-Name,+Machines,-AllMachines): |
| 888 | | % Create a dummy machine that extends the main machine and extends or includes |
| 889 | | % all seen/used machines that are not included if such machines exist. |
| 890 | | % In case of refinement this is done for the whole refinement chain. |
| 891 | | % Uses: List of machine names and prefix usemch/2 of the machines that are used/seen but not included |
| 892 | | % Main: The name of the main machine |
| 893 | | % Name: The name of the generated dummy machine (or Main if no dummy machine is generated) |
| 894 | | % Machines: List of all specified Machines |
| 895 | | % AllMachines: List of all Machines + the new dummy machine(s) |
| 896 | | extend_not_included_uses([],Main,Main,Machines,Machines) :- !. |
| 897 | | extend_not_included_uses(Uses,Main,NewMainName,Machines,AllMachines) :- |
| 898 | | get_refinement_hierarchy(Main,Machines,RefChain), |
| 899 | | maplist(extend_not_included_uses2(Uses,Machines),RefChain,NewMachines), |
| 900 | | append(NewMachines,Machines,AllMachines), |
| 901 | | dummy_machine_name(Main,NewMainName), |
| 902 | | debug_format(19,'Creating dummy machine called ~w for main machine~n',[NewMainName]). |
| 903 | | extend_not_included_uses2(Uses,Machines,Name,DummyMachine) :- |
| 904 | | debug_format(19,'Creating dummy subsidiary machine for refined machine ~w~n',[Name]), |
| 905 | | create_dummy_machine(Name,Machines,Parameters,DummyParameters,Sections,DummyMachine), |
| 906 | | IncludeMain = machine_reference(none,Name,Parameters), |
| 907 | | ( get_preference(seen_machines_included,true) -> |
| 908 | | % extend just the main machine, include the used/seen machines |
| 909 | | References = [extends(none,[IncludeMain]),includes(none,UReferences)] |
| 910 | | ; |
| 911 | | % extends the main machine and all used/seen machines |
| 912 | | References = [extends(none,[IncludeMain|UReferences])]), |
| 913 | | maplist(find_using(Machines),Uses,UReferences,LUParameters), |
| 914 | | append([Parameters|LUParameters],DummyParameters), |
| 915 | | copy_raw_definitions(Name,Machines,OptDefs), |
| 916 | | % we store a flag "is_dummy" in the machine because we have a special case |
| 917 | | % later, see type_constraints/7. |
| 918 | | append([References,[is_dummy],OptDefs],Sections). |
| 919 | | create_dummy_machine(Name,Machines,Parameters,DummyParameters,Sections,DummyMachine) :- |
| 920 | | dummy_machine_name(Name,DummyName), |
| 921 | ? | get_raw_model_type(Name,Machines,ModelType), |
| 922 | | !, |
| 923 | | Header = machine_header(_,Name,Parameters), |
| 924 | | DummyHeader = machine_header(none,DummyName,DummyParameters), |
| 925 | ? | member(Machine,Machines), |
| 926 | ? | generate_raw_machine(Header,DummyHeader,ModelType,Sections,Machine,DummyMachine),!. |
| 927 | | |
| 928 | | generate_raw_machine(OldHeader,NewHeader,_,NewSections, |
| 929 | | abstract_machine(_, ModelType,OldHeader,_), |
| 930 | | abstract_machine(none,ModelType,NewHeader,NewSections)). |
| 931 | | generate_raw_machine(OldHeader,NewHeader,ModelType,NewSections, |
| 932 | | refinement_machine(_, OldHeader,_Abstract, _), |
| 933 | | abstract_machine(none,ModelType,NewHeader,NewSections)). |
| 934 | | generate_raw_machine(OldHeader,NewHeader,ModelType,NewSections, |
| 935 | | implementation_machine(_, OldHeader,_Abstract, _), |
| 936 | | abstract_machine(none,ModelType,NewHeader,NewSections)). |
| 937 | | |
| 938 | | dummy_machine_name(Name,DummyName) :- |
| 939 | | atom_concat('MAIN_MACHINE_FOR_',Name,DummyName). |
| 940 | | |
| 941 | | add_machine_prefix(UsedMch,'',Name) :- !, UsedMch=Name. |
| 942 | | add_machine_prefix(UsedMch,UsePrefix,Name) :- ajoin([UsePrefix,'.',UsedMch],Name). |
| 943 | | |
| 944 | | find_using(Machines,usemch_not_inc(UsedMch,UsePrefix,_,_,_,OtherPrefixes), |
| 945 | | machine_reference(none,Name,Arguments),Arguments) :- |
| 946 | | % invent a dummy prefix for the SEEN/USED machine which is not included |
| 947 | | % to avoid name-clashes with main machine |
| 948 | | % was using(U).U, but awkward to type in REPL |
| 949 | | % try machine name itself; unless somewhere else it is included this way |
| 950 | | (member(UsedMch,OtherPrefixes) % somewhere we already have an INCLUDES UsedMach.UsedMach |
| 951 | | -> DummyPrefix = using(UsedMch) |
| 952 | | ; DummyPrefix = UsedMch), |
| 953 | | ajoin([DummyPrefix,'.',UsedMch],Name0), |
| 954 | | add_machine_prefix(Name0,UsePrefix,Name), |
| 955 | ? | member(M,Machines), get_machine_parameters(M,UsedMch,Params,_),!, |
| 956 | | maplist(add_use_param,Params,Arguments). |
| 957 | | add_use_param(identifier(_,Param),identifier(none,Name)) :- |
| 958 | | ( is_upper_case(Param) -> |
| 959 | | ajoin(['Useparam(',Param,')'],Name) |
| 960 | | ; |
| 961 | | ajoin(['useparam(',Param,')'],Name)). |
| 962 | | |
| 963 | | % copy_raw_definitions(+Name,+Machines,-OptDefs): |
| 964 | | % Get the definitions section from a raw (untyped) machine |
| 965 | | % Name: Name of the machine |
| 966 | | % Machines: List of Machines |
| 967 | | % OptDefs: [] if no definitions are present or [Def] if a definition section Def is present |
| 968 | | copy_raw_definitions(Name,Machines,OptDefs) :- |
| 969 | ? | get_constructed_machine_name_and_body(M,Name,_,Sections), |
| 970 | | memberchk(M,Machines),!, |
| 971 | | Def = definitions(_,_), |
| 972 | | ( memberchk(Def,Sections) -> |
| 973 | | OptDefs = [Def] |
| 974 | | ; |
| 975 | | OptDefs = []). |
| 976 | | |
| 977 | | add_def_dependency_information(DefsIn,DefsOut,Ein,Eout) :- |
| 978 | | extract_def_name_set(DefsIn,DefNames,DN), |
| 979 | | maplist(add_def_dep(DN),DefsIn,Defs1), |
| 980 | | check_for_cyclic_def_dependency(Defs1,DefNames,DefsOut,Ein,Eout). |
| 981 | | |
| 982 | | extract_def_name_set(Defs,DefNames,DN) :- |
| 983 | | maplist(get_def_name,Defs,DefNames), |
| 984 | | maplist(to_mapset_entry,DefNames,DN1), |
| 985 | | list_to_avl(DN1,DN). |
| 986 | | |
| 987 | | get_def_name(Def,Name) :- arg(1,Def,Name). |
| 988 | | get_def_pos(Def,Pos) :- arg(3,Def,Pos). |
| 989 | | get_def_dependencies(Def,Dependencies) :- arg(6,Def,Dependencies). |
| 990 | | to_mapset_entry(Name,Name-true). |
| 991 | | |
| 992 | | add_def_dep(DN,In,Out) :- |
| 993 | | analyse_definition_dependencies(In,DN,Deps), |
| 994 | | In = definition_decl(Name,DefType,Pos,Args,RawExpr), |
| 995 | | Out = definition_decl(Name,DefType,Pos,Args,RawExpr,Deps). |
| 996 | | |
| 997 | | check_for_cyclic_def_dependency(Defs,DefNames,DefsOut,Ein,Eout) :- |
| 998 | | % check if we have a cyclic definition: |
| 999 | | create_definitions_avl(Defs,DefsAvl), |
| 1000 | | search_for_cyclic_definition(DefNames,DefsAvl,[],Pos,RCycle),!, |
| 1001 | | % if we have found a cyclic definition, generate an error message, ... |
| 1002 | | reverse(RCycle,Cycle),add_arrows(Cycle,Msg0), |
| 1003 | | ajoin(['Found cyclic definitions: '|Msg0],Msg), |
| 1004 | | Ein = [error(Msg,Pos)|E1], |
| 1005 | | % ... remove the definitions in the cycle (to prevent later infinite loops) ... |
| 1006 | | exclude(definition_in_list(Cycle),Defs,Defs1), |
| 1007 | | % ... and check the remaining definitions. |
| 1008 | | check_for_cyclic_def_dependency(Defs1,DefNames,DefsOut,E1,Eout). |
| 1009 | | check_for_cyclic_def_dependency(Defs,_DefNames,Defs,E,E). |
| 1010 | | add_arrows([E],[E]) :- !. |
| 1011 | | add_arrows([E|Erest],[E,'->'|Arest]) :- add_arrows(Erest,Arest). |
| 1012 | | definition_in_list(List,Def) :- |
| 1013 | | get_def_name(Def,Name),memberchk(Name,List). |
| 1014 | | |
| 1015 | | create_definitions_avl(Defs,DefsAvl) :- |
| 1016 | | maplist(split_def_name,Defs,Entries), |
| 1017 | | list_to_avl(Entries,DefsAvl). |
| 1018 | | split_def_name(Def,Name-Def) :- get_def_name(Def,Name). |
| 1019 | | |
| 1020 | | |
| 1021 | | % just a depth-first search to find a cycle |
| 1022 | | search_for_cyclic_definition(DefNames,Definitions,Visited,Pos,Cycle) :- |
| 1023 | ? | member(Name,DefNames),avl_fetch(Name,Definitions,Definition), |
| 1024 | | get_def_pos(Definition,Pos), |
| 1025 | | ( memberchk(Name,Visited) -> |
| 1026 | | Cycle = [Name|Visited] |
| 1027 | | ; |
| 1028 | | get_def_dependencies(Definition,Dependencies), |
| 1029 | | search_for_cyclic_definition(Dependencies,Definitions,[Name|Visited],_,Cycle) |
| 1030 | | ). |
| 1031 | | |
| 1032 | | :- assert_must_succeed(( |
| 1033 | | list_to_avl([def1-true,def2-true,def3-true,def4-true],DefNames), |
| 1034 | | analyse_definition_dependencies( |
| 1035 | | conjunct(none, |
| 1036 | | equals(none, |
| 1037 | | identifier(none,x), |
| 1038 | | identifier(none,def1)), |
| 1039 | | equals(none, |
| 1040 | | definition(none,def4, |
| 1041 | | [function(none, |
| 1042 | | identifier(none,def3), |
| 1043 | | integer(none,5))]), |
| 1044 | | identifier(y))),DefNames,Defs), |
| 1045 | | Defs==[def1,def3,def4] |
| 1046 | | )). |
| 1047 | | % analyse_definition_dependencies(+Expr,+DefinitionNames,Deps): |
| 1048 | | % Expr: raw (i.e. untyped) expression to analyse |
| 1049 | | % DN: AVL set (i.e. mapping from elements to 'true') of the names of the definitions |
| 1050 | | % This is needed to decide if an identifier is a reference to a definition |
| 1051 | | % Deps: A list of used definitions (a list of their names) |
| 1052 | | analyse_definition_dependencies(Expr,DN,Deps) :- |
| 1053 | | analyse_definition_dependencies2(Expr,DN,Unsorted,[]), |
| 1054 | | sort(Unsorted,Deps). |
| 1055 | | analyse_definition_dependencies2(VAR,_DN) --> {var(VAR)},!, |
| 1056 | | {add_internal_error('Variable DEFINITION expression in',analyse_definition_dependencies)}. |
| 1057 | | analyse_definition_dependencies2([Expr|Rest],DN) --> |
| 1058 | | !, analyse_definition_dependencies2(Expr,DN), |
| 1059 | | analyse_definition_dependencies2(Rest,DN). |
| 1060 | | analyse_definition_dependencies2(definition(_Pos,Name,Args),DN) --> |
| 1061 | | !,[Name],analyse_definition_dependencies2(Args,DN). |
| 1062 | | analyse_definition_dependencies2(identifier(_Pos,Name),DN) --> |
| 1063 | | {avl_fetch(Name,DN),!},[Name]. |
| 1064 | | analyse_definition_dependencies2(Expr,DN) --> |
| 1065 | | { compound(Expr),functor(Expr,_Functor,Arity),!}, |
| 1066 | | analyse_definition_dependencies_arg(2,Arity,Expr,DN). |
| 1067 | | analyse_definition_dependencies2(_Expr,_DN) --> []. |
| 1068 | | |
| 1069 | | analyse_definition_dependencies_arg(I,Arity,Expr,DN) --> |
| 1070 | | { I =< Arity,!,arg(I,Expr,Arg),I2 is I+1 }, |
| 1071 | | analyse_definition_dependencies2(Arg,DN), |
| 1072 | | analyse_definition_dependencies_arg(I2,Arity,Expr,DN). |
| 1073 | | analyse_definition_dependencies_arg(_I,_Arity,_Expr,_DN) --> []. |
| 1074 | | |
| 1075 | | |
| 1076 | | :- use_module(tools_positions, [get_position_filenumber/2]). |
| 1077 | | |
| 1078 | | get_constructed_machine_name(MachineTerm,Name) :- get_constructed_machine_name_and_body(MachineTerm,Name,_Pos,_). |
| 1079 | | % name and pos; pos can be used for filenumber |
| 1080 | | get_constructed_machine_name_and_filenumber(MachineTerm,Name,Filenumber) :- |
| 1081 | | get_constructed_machine_name_and_body(MachineTerm,Name,Pos,_), |
| 1082 | | (get_position_filenumber(Pos,FN) -> Filenumber=FN ; Filenumber=unknown). |
| 1083 | | get_constructed_machine_name_and_body(abstract_machine(_,_ModelType,machine_header(Pos,Name,_),Body),Name,Pos,Body). |
| 1084 | | get_constructed_machine_name_and_body(refinement_machine(_,machine_header(Pos,Name,_),_Abstract,Body),Name,Pos,Body). |
| 1085 | | get_constructed_machine_name_and_body(implementation_machine(_,machine_header(Pos,Name,_),_Abstract,Body),Name,Pos,Body). |
| 1086 | | |
| 1087 | | refines(refinement_machine(_,machine_header(_,_Name,_),Abstract,_Body),Abstract). |
| 1088 | | refines(implementation_machine(_,machine_header(_,_Name,_),Abstract,_Body),Abstract). |
| 1089 | | |
| 1090 | | get_machine_parameters(abstract_machine(Pos,_ModelType,machine_header(_,Name,Parameters),_),Name,Parameters,Pos). |
| 1091 | | get_machine_parameters(refinement_machine(Pos,machine_header(_,Name,Parameters),_,_),Name,Parameters,Pos). |
| 1092 | | get_machine_parameters(implementation_machine(Pos,machine_header(_,Name,Parameters),_,_),Name,Parameters,Pos). |
| 1093 | | |
| 1094 | | get_raw_model_type(Main,Machines,ModelType) :- |
| 1095 | ? | get_constructed_machine_name_and_body(M,Main,_,_), |
| 1096 | | memberchk(M,Machines), |
| 1097 | | ( refines(M,RefName) -> |
| 1098 | | get_raw_model_type(RefName,Machines,ModelType) |
| 1099 | | ; |
| 1100 | | M = abstract_machine(_,ModelType,_,_)). |
| 1101 | | |
| 1102 | | some_machine_name_body(Machines,M,Name,Body) :- |
| 1103 | ? | member(M,Machines), |
| 1104 | | get_constructed_machine_name_and_body(M,Name,_,Body). |
| 1105 | | |
| 1106 | | use_usage(Machines,Pos,Kind,UsedMch,UsePrefix,FromMchName) :- |
| 1107 | ? | some_machine_name_body(Machines,_,FromMchName,Body), |
| 1108 | ? | ( member(sees(Pos,R),Body),Kind=seen |
| 1109 | | ; member(uses(Pos,R),Body),Kind=used), |
| 1110 | ? | member(identifier(_,PrefixUse),R), |
| 1111 | | split_prefix(PrefixUse,UsePrefix,UsedMch). |
| 1112 | | % include_usage/4 checks if there is any machine in Machines that |
| 1113 | | % includes/extends/imports the used machine |
| 1114 | | % include_usage(+Machines,+Use,-Name): |
| 1115 | | % Machines: The list of machines |
| 1116 | | % UsedMch: The name of the used machine |
| 1117 | | % UsePrefix: the prefix with which the machine is used |
| 1118 | | % Name: The name of the machine that imports the used machine |
| 1119 | | % include_usage/4 fails if there is not such an import |
| 1120 | | include_usage(Machines,UsedMch,UsePrefix,MachName,Pos) :- |
| 1121 | ? | some_machine_name_body(Machines,_,MachName,Body), |
| 1122 | | ( member(includes(_,R),Body) |
| 1123 | | ; member(extends(_,R), Body) |
| 1124 | | ; member(imports(_,R), Body)), |
| 1125 | | member(machine_reference(Pos,PrefixRef,_),R), |
| 1126 | | % The name could be prefixed, we need it without prefix: |
| 1127 | | split_prefix(PrefixRef,UsePrefix,UsedMch). |
| 1128 | | |
| 1129 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1130 | | % uses and sees clauses |
| 1131 | | |
| 1132 | | % returns a list of references to used and seen machines |
| 1133 | | % the machines contain only identifier sections and |
| 1134 | | % the identifier are prefixed accordingly |
| 1135 | | % all identifier are marked as coming from a seen/used machine |
| 1136 | | use_and_see_machines(Sections,Machines,References) :- |
| 1137 | | get_uses_and_sees(Sections,Uses,Sees), |
| 1138 | | maplist(use_or_see_machine(used,Machines),Uses,Used), |
| 1139 | | maplist(use_or_see_machine(seen,Machines),Sees,Seen), |
| 1140 | | append(Used,Seen,References). |
| 1141 | | |
| 1142 | | % get uses and sees sections from the untyped machines |
| 1143 | | get_uses_and_sees(Sections,Uses,Sees) :- |
| 1144 | | get_uses_or_sees2(sees,Sections,Sees), |
| 1145 | | get_uses_or_sees2(uses,Sections,Uses). |
| 1146 | | get_uses_or_sees2(Mode,Sections,US) :- |
| 1147 | | optional_rawmachine_section(Mode,Sections,[],US1), |
| 1148 | | findall(I,member(identifier(_,I),US1),US). |
| 1149 | | |
| 1150 | | % Mode is used or seen |
| 1151 | | use_or_see_machine(Mode,TypedMachines,Ref,ref(Mode,Result)) :- |
| 1152 | | split_prefix(Ref,Prefix,MachName), |
| 1153 | | memberchk(machine(MachName,Typed),TypedMachines), |
| 1154 | | create_machine(MachName,Empty), |
| 1155 | | use_sections([sets],Mode,'',MachName,Typed,Empty,M1), |
| 1156 | | use_sections([constants,variables,promoted],Mode,Prefix,MachName,Typed,M1,Result). |
| 1157 | | use_sections(Sections,Mode,Prefix,MachName,Typed,Old,New) :- |
| 1158 | | expand_shortcuts(Sections,AllSections), |
| 1159 | | foldl(use_section(Mode,Prefix,MachName,Typed),AllSections,Old,New). |
| 1160 | | use_section(Mode,Prefix,MachName,Machine,Section,OldM,NewM) :- |
| 1161 | | get_section_texprs(Section,Machine,Identifiers), |
| 1162 | | write_section(Section,NewIds,OldM,NewM), |
| 1163 | | ( Prefix='' -> |
| 1164 | | Ids1=Identifiers |
| 1165 | | ; |
| 1166 | | prefix_identifiers(Identifiers,Prefix,Renamings), |
| 1167 | | rename_bt_l(Identifiers,Renamings,Ids1)), |
| 1168 | | maplist(add_use_info_to_identifier(Mode,MachName),Ids1,NewIds). |
| 1169 | | add_use_info_to_identifier(Mode,MachName,TExpr,New) :- |
| 1170 | | get_texpr_id(TExpr,PId), get_texpr_type(TExpr,Type), |
| 1171 | | get_texpr_id(New,PId), get_texpr_type(New,Type), |
| 1172 | | split_prefix(PId,_Prefix,Id), |
| 1173 | | get_texpr_info(TExpr,Info), |
| 1174 | | get_texpr_info(New,[usesee(MachName,Id,Mode)|Info]). |
| 1175 | | |
| 1176 | | |
| 1177 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1178 | | % add a section to the machine that describes the linking of |
| 1179 | | % parameters and arguments |
| 1180 | | add_link_constraints(Includes,MType,Parameters,RefMachines,Old,New,Ein,Eout) :- |
| 1181 | | AllRefMachines = [ref(local,Old)|RefMachines], |
| 1182 | | extract_parameter_types(RefMachines,NonGroundExceptions), |
| 1183 | | foldl(add_link_section(MType,Parameters,AllRefMachines,NonGroundExceptions), |
| 1184 | | Includes,Links/Ein,[]/Eout), % TO DO: Daniel check if [] is correct here |
| 1185 | | %print(conjunct_predicates(Links,Link)),nl, |
| 1186 | | conjunct_predicates(Links,Link), |
| 1187 | | select_section(constraints,OConstraints,NConstraints,Old,New), |
| 1188 | | conjunct_predicates([Link,OConstraints],NConstraints). |
| 1189 | | add_link_section(MType,Parameters,RefMachines,NonGroundExceptions, |
| 1190 | | machine_reference(Pos,Ref,Args),Links/Ein,RLinks/Eout) :- |
| 1191 | | visible_env(MType,includes,RefMachines,Env,Ein,E1), |
| 1192 | | memberchk(parameters(Ref,TParameters),Parameters), |
| 1193 | | ( same_length(TParameters, Args) -> |
| 1194 | | get_texpr_types(TParameters,Types), |
| 1195 | | btype_ground_dl(Args,Env,NonGroundExceptions,Types,TArgs,E1,Eout), |
| 1196 | | maplist(create_plink_equality,TParameters,TArgs,LLinks) |
| 1197 | | ; |
| 1198 | | E1 = [error('wrong number of machine arguments',Pos)|Eout], |
| 1199 | | LLinks = []), |
| 1200 | | append(LLinks,RLinks,Links). |
| 1201 | | create_plink_equality(P,A,E) :- |
| 1202 | | create_texpr(equal(P,A),pred,[parameterlink],E). |
| 1203 | | |
| 1204 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1205 | | % type machines |
| 1206 | | |
| 1207 | | type_machine(Header,Name,MType,RawMachine,RefMachines,TypedMachine,NewRefMachines,Ein,Eout) :- |
| 1208 | | Header = machine_header(_,Name,_), |
| 1209 | | create_machine(Name,Empty), |
| 1210 | | % (optional) definitions |
| 1211 | | extract_definitions(RawMachine,Empty,DefsOnly,Ein,E0), |
| 1212 | | debug_stats(extracted_definitions(Name)), |
| 1213 | | % create the identifiers that will be typed, |
| 1214 | | % Local will contain the identifier sections |
| 1215 | | create_id_sections(Header,RawMachine,Name,DefsOnly,Local), |
| 1216 | | debug_stats(created_identifier_sections(Name)), |
| 1217 | ? | create_freetypes(RawMachine,MType,RefMachines,Local,Local1,E0,E1), |
| 1218 | | % in case of a refinement, check if all newly defined operations are refinements |
| 1219 | | link_to_refinement(MType,Name,RawMachine,RefMachines,Local1,Local2,E1,E2), |
| 1220 | | % extract types that can be variables |
| 1221 | | debug_stats(created_link_to_refinement(Name)), |
| 1222 | | extract_parameter_types([ref(local,Local2)|RefMachines],NonGroundExceptions), |
| 1223 | | % check for a VALUES clause. They are a little bit tricky because they can replace |
| 1224 | | % already defined deferred sets by integers or other deferred sets |
| 1225 | | process_values_section(MType,RawMachine,NonGroundExceptions, |
| 1226 | | Local2/E2/RefMachines,Local3/E3/NewRefMachines), |
| 1227 | | % type-check the other sections (properties, invariant, operation_bodies, etc) |
| 1228 | | type_sections(RawMachine,MType,[ref(local,Local3)|NewRefMachines],NonGroundExceptions, |
| 1229 | | Name,E3,Eout,Local3,TypedMachine). |
| 1230 | | |
| 1231 | | % extract definitions from a definition file |
| 1232 | | extract_only_definitions(MainName,RawMachine,DefsOnlyMachine,FinalErrors) :- |
| 1233 | | create_machine(MainName,Empty), |
| 1234 | | extract_definitions(RawMachine,Empty,DefsOnlyMachine,Errors,[]), |
| 1235 | | sort(Errors,FinalErrors), |
| 1236 | | add_all_perrors(FinalErrors). |
| 1237 | | |
| 1238 | | extract_definitions(RawMachine,In,Out,Ein,Eout) :- |
| 1239 | | optional_rawmachine_section(definitions,RawMachine,[],AllDefinitions), |
| 1240 | | write_section(definitions,Definitions,In,Out), |
| 1241 | | % remove all references to definition files from definitions |
| 1242 | | exclude(is_file_definition,AllDefinitions,Definitions1), |
| 1243 | | % replace expression_definition(...) by defintion(expression,...), etc. |
| 1244 | | change_definition_style(Definitions1,Definitions2), |
| 1245 | | % analyse dependencies |
| 1246 | | add_def_dependency_information(Definitions2,Definitions3,Ein,Eout), |
| 1247 | | % replace external function definitions by calls to the external function |
| 1248 | | replace_external_declarations(Definitions3,Definitions). |
| 1249 | | |
| 1250 | | is_file_definition(file_definition(_Pos,_Filename)). |
| 1251 | | |
| 1252 | | change_definition_style(DefsIn,DefsOut) :- |
| 1253 | | maplist(change_definition_style2,DefsIn,DefsOut). |
| 1254 | | change_definition_style2(conversion(Pos,InnerDef),definition_decl(Name,DefType,InnerPos,Args,conversion(Pos,RawExpr))) :- |
| 1255 | | change_definition_style2(InnerDef,definition_decl(Name,DefType,InnerPos,Args,RawExpr)). |
| 1256 | | change_definition_style2(Def,definition_decl(Name,DefType,Pos,Args,RawExpr)) :- |
| 1257 | | Def =.. [Functor,Pos,Name,Args,RawExpr], |
| 1258 | | maplist(check_def_argument(Name,Pos),Args), |
| 1259 | | map_def_functor(Functor,DefType). |
| 1260 | | map_def_functor(expression_definition,expression). |
| 1261 | | map_def_functor(substitution_definition,substitution). |
| 1262 | | map_def_functor(predicate_definition,predicate). |
| 1263 | | |
| 1264 | | % check formal arguments of definitions , e.g., here xx in square2 is not an identifier: xx == 20; square2(xx) == xx*xx |
| 1265 | | check_def_argument(_,_,identifier(_,_)) :- !. |
| 1266 | | check_def_argument(DefName,DefPos,definition(_,ID,_)) :- !, |
| 1267 | | tools:ajoin(['Formal parameter ', ID, ' is a definition call in Definition: '],Msg), |
| 1268 | | add_error(bmachine_construction,Msg,DefName,DefPos). |
| 1269 | | check_def_argument(DefName,DefPos,FP) :- !, |
| 1270 | | tools:ajoin(['Formal parameter ', FP, ' is not an identifier in Definition: '],Msg), |
| 1271 | | add_error(bmachine_construction,Msg,DefName,DefPos). |
| 1272 | | |
| 1273 | | replace_external_declarations(Definitions,NewDefs) :- |
| 1274 | | split_list(is_external_declaration,Definitions,ExtFunctionDecls,RestDefs), |
| 1275 | | foldl(replace_external_declaration,ExtFunctionDecls,RestDefs,NewDefs). |
| 1276 | | is_external_declaration(definition_decl(DefName,expression,_Pos,_Params,_Def,_Dependencies)) :- |
| 1277 | ? | external_name(DefName,ExtType,_ExpectedDefType,_ExtCall,FunName), |
| 1278 | | debug_format(4,'external ~w declared: ~w~n', [ExtType,FunName]). |
| 1279 | | external_name(DefName,_,_,_,_) :- |
| 1280 | | \+ atom(DefName),!, |
| 1281 | | add_internal_error('Non-atomic DEFINITION id:',DefName),fail. |
| 1282 | | external_name(DefName,function,expression,external_function_call,FunName) :- |
| 1283 | | atom_concat('EXTERNAL_FUNCTION_',FunName,DefName). |
| 1284 | | external_name(DefName,predicate,predicate,external_pred_call,FunName) :- |
| 1285 | | atom_concat('EXTERNAL_PREDICATE_',FunName,DefName). |
| 1286 | | external_name(DefName,substitution,substitution,external_subst_call,FunName) :- |
| 1287 | | atom_concat('EXTERNAL_SUBSTITUTION_',FunName,DefName). |
| 1288 | | |
| 1289 | | replace_external_declaration(definition_decl(DefName,expression,DefPos,TypeParams,Decl,_Deps),In,Out) :- |
| 1290 | | OldDefinition = definition_decl(FunName,ExpectedDefType,Pos,FunParams,FunDef,Deps), |
| 1291 | | NewDefinition = definition_decl(FunName,ExpectedDefType,Pos,FunParams,ExtCall,Deps), |
| 1292 | ? | ( external_name(DefName,_ExtType,ExpectedDefType,ExtCallFunctor,FunName), |
| 1293 | | ExtCall =.. [ExtCallFunctor,Pos,FunName,FunParams,FunDef, |
| 1294 | | rewrite_protected(TypeParams),rewrite_protected(Decl)], |
| 1295 | | selectchk(OldDefinition,In,NewDefinition,Out) -> |
| 1296 | | assert_external_procedure_used(FunName) |
| 1297 | | ; external_name(DefName,ExpectedKind,_,_,FunName), |
| 1298 | | selectchk(definition_decl(FunName,OtherDefType,_OtherPos,_,_,_),In,_,_),!, |
| 1299 | | % definition found for different type of external function |
| 1300 | | ajoin(['No DEFINITION associated with external ',ExpectedKind, |
| 1301 | | ' (but definition as ',OtherDefType,' exists):'],Msg), |
| 1302 | | add_error(replace_external_declaration,Msg,DefName,DefPos), Out=In |
| 1303 | | ; external_name(DefName,ExpectedKind,_,_,FunName) -> |
| 1304 | | % no definition found for external function |
| 1305 | | ajoin(['No DEFINITION associated with external ',ExpectedKind,':'],Msg), |
| 1306 | | add_error(replace_external_declaration,Msg,DefName,DefPos), Out=In |
| 1307 | | ; % no definition found for external function |
| 1308 | | ajoin(['No DEFINITION associated with:'],Msg), |
| 1309 | | add_error(replace_external_declaration,Msg,DefName,DefPos), Out=In |
| 1310 | | ). |
| 1311 | | |
| 1312 | | :- use_module(external_function_declarations, |
| 1313 | | [external_function_library/2, safe_external_function_library/2, |
| 1314 | | get_external_function_definition/3]). |
| 1315 | | % store external definitions of a given library in the type environment, e.g. for debugging in Repl or VisB |
| 1316 | | % Library could be "LibraryStrings.def" |
| 1317 | | |
| 1318 | | store_ext_defs(Library,In,Out) :- |
| 1319 | | (Library = all_available_libraries |
| 1320 | | -> findall(extfun(Id,Lib),external_function_library(Id,Lib),Ids) |
| 1321 | | ; Library = safe_available_libraries |
| 1322 | | -> findall(extfun(Id,Lib),safe_external_function_library(Id,Lib),Ids) |
| 1323 | | ; findall(extfun(Id,Library),external_function_library(Id,Library),Ids) |
| 1324 | | ), |
| 1325 | | (Ids=[] -> add_warning(store_ext_defs,'No external functions found for library: ',Library) ; true), |
| 1326 | | foldl(store_ext_def,Ids,In,Out). |
| 1327 | | |
| 1328 | | store_ext_def(extfun(Id,Library),In,Out) :- env_lookup_type(Id,In,_),!, |
| 1329 | | debug_println(4,not_storing_ext_def(Id,Library)), % already imported from stdlib or user has other definition |
| 1330 | | Out=In. |
| 1331 | | store_ext_def(extfun(FunName,Library),In,Out) :- |
| 1332 | ? | get_external_function_definition(FunName,Library,DEFINITION),!, |
| 1333 | | debug_println(4,storing_ext_def(FunName,Library)), |
| 1334 | | env_store(FunName,DEFINITION,[loc('automatically included',Library,definitions)],In,Out). |
| 1335 | | store_ext_def(extfun(Id,_),In,Out) :- |
| 1336 | | add_internal_error('Cannot add external definition: ',Id), |
| 1337 | | Out=In. |
| 1338 | | |
| 1339 | | |
| 1340 | | % store which machine promotes which operations |
| 1341 | | :- dynamic machine_promotes_operations/2, machine_hides_unpromoted_operation/4, machine_global_order/1. |
| 1342 | | |
| 1343 | | reset_bmachine_construction :- |
| 1344 | | retractall(machine_promotes_operations(_,_)), |
| 1345 | | retractall(machine_hides_unpromoted_operation(_,_,_,_)), |
| 1346 | | retractall(abstract_variable_removed_in(_,_,_)), |
| 1347 | | retractall(machine_global_order(_)), |
| 1348 | | reset_external_procedure_used. |
| 1349 | | |
| 1350 | | |
| 1351 | | % maybe this information should be stored somewhere else ?? |
| 1352 | | :- dynamic external_procedure_used/1. |
| 1353 | | reset_external_procedure_used :- retractall(external_procedure_used(_)). |
| 1354 | | assert_external_procedure_used(FunName) :- |
| 1355 | | (external_procedure_used(FunName) -> true ; assertz(external_procedure_used(FunName))). |
| 1356 | | |
| 1357 | | link_to_refinement(machine,_,_RawMachine,_RefMachines,Local,Local,Errors,Errors). |
| 1358 | | link_to_refinement(refinement,Name,RawMachine,RefMachines,Local,NewLocal,Ein,Eout) :- |
| 1359 | | link_to_refinement(implementation,Name,RawMachine,RefMachines,Local,NewLocal,Ein,Eout). |
| 1360 | | link_to_refinement(implementation,Name,RawMachine,RefMachines,Local,NewLocal,Ein,Eout) :- |
| 1361 | | link_to_refinement2(implementation,Name,RawMachine,RefMachines,Local,NewLocal,Ein,Eout). |
| 1362 | | link_to_refinement2(_MType,Name,RawMachine,RefMachines,Local,NewLocal,Ein,Eout) :- |
| 1363 | | memberchk(ref(abstraction,AbstractMachine),RefMachines), |
| 1364 | | copy_constraints(Local,AbstractMachine,NewLocal,Ein,E1), |
| 1365 | | type_vars_in_refinement(AbstractMachine,NewLocal), |
| 1366 | | type_refinement_operations(Name,RawMachine,AbstractMachine,NewLocal,E1,Eout). |
| 1367 | | |
| 1368 | | copy_constraints(Local,AbstractMachine,NewLocal,Ein,Eout) :- |
| 1369 | | get_section(parameters,Local,LocalParameters), |
| 1370 | | get_section(parameters,AbstractMachine,AbstractParameters), |
| 1371 | | check_if_equal_identifiers(LocalParameters,AbstractParameters,Ein,Eout,Local), |
| 1372 | | get_section(constraints,AbstractMachine,Constraints), |
| 1373 | | write_section(constraints,Constraints,Local,NewLocal). |
| 1374 | | check_if_equal_identifiers(Local,Abstract,Ein,Eout,LocalMachine) :- |
| 1375 | | ( same_length(Local,Abstract) -> |
| 1376 | | foldl(check_if_equal_identifiers2,Local,Abstract,Ein,Eout) |
| 1377 | | ; |
| 1378 | | get_texpr_ids(Abstract,AIDs), |
| 1379 | | get_machine_name(LocalMachine,MachName), |
| 1380 | | ajoin(['Refinement ',MachName,' must have same Parameters ', AIDs,' as abstract Machine'],Msg), |
| 1381 | | Ein = [error(Msg,none)|Eout] |
| 1382 | | ). |
| 1383 | | check_if_equal_identifiers2(LParam,AParam,Ein,Eout) :- |
| 1384 | | get_texpr_id(LParam,LName), |
| 1385 | | get_texpr_id(AParam,AName), |
| 1386 | | ( LName = AName -> |
| 1387 | | % type in refinement is the same as in the abstraction |
| 1388 | | get_texpr_type(LParam,Type), |
| 1389 | | get_texpr_type(AParam,Type), |
| 1390 | | Ein=Eout |
| 1391 | | ; |
| 1392 | | get_texpr_pos(LParam,Pos), |
| 1393 | | ajoin(['Parameter ',LName,' of refinement machine must be ', |
| 1394 | | AName,' like in the abstract machine'],Msg), |
| 1395 | | Ein = [error(Msg,Pos)|Eout] |
| 1396 | | ). |
| 1397 | | |
| 1398 | | % in case of a refinement, give variables the same type as in the abstract machine |
| 1399 | | % the same for constants |
| 1400 | | type_vars_in_refinement(AbstractMachine,ConcreteMachine) :- |
| 1401 | | pass_type(AbstractMachine,[abstract_variables,concrete_variables], |
| 1402 | | ConcreteMachine,[abstract_variables,concrete_variables]), |
| 1403 | | pass_type(AbstractMachine,[abstract_constants,concrete_constants], |
| 1404 | | ConcreteMachine,[abstract_constants,concrete_constants]). |
| 1405 | | |
| 1406 | | % pass the type from variables in Sections1 of Machine1 to |
| 1407 | | % the variables of the same name in Sections2 of Machine2 |
| 1408 | | % Machine1,Machine2: a machine |
| 1409 | | % Sections1, Sections2: a list of section names |
| 1410 | | pass_type(Machine1,Sections1,Machine2,Sections2) :- |
| 1411 | | get_sections_and_append(Sections1,Machine1,Vars1), |
| 1412 | | get_sections_and_append(Sections2,Machine2,Vars2), |
| 1413 | | maplist(pass_type2(Vars2),Vars1). |
| 1414 | | get_sections_and_append([],_M,[]). |
| 1415 | | get_sections_and_append([Sec|RestSections],M,R) :- |
| 1416 | | get_section(Sec,M,L), append(L,Rest,R), |
| 1417 | | get_sections_and_append(RestSections,M,Rest). |
| 1418 | | pass_type2(DstVariables,SrcVariable) :- |
| 1419 | | get_texpr_id(SrcVariable,Id), |
| 1420 | | get_texpr_id(DstVariable,Id), |
| 1421 | | ( memberchk(DstVariable,DstVariables) -> |
| 1422 | | get_texpr_type(DstVariable,Type), |
| 1423 | | get_texpr_type(SrcVariable,Type) |
| 1424 | | ; |
| 1425 | | true). |
| 1426 | | |
| 1427 | | |
| 1428 | | % in case of a refinement, check if the defined operations are already defined |
| 1429 | | % in the abstract machine and copy that type. |
| 1430 | | type_refinement_operations(MName,RawMachine,AbstractMachine,Local,Ein,Eout) :- |
| 1431 | | get_operation_identifiers(RawMachine,Operations), |
| 1432 | | type_refinement_operations2(Operations,MName,Local,AbstractMachine,Ein,Eout). |
| 1433 | | type_refinement_operations2([],_,_,_AbstractMachine,Errors,Errors). |
| 1434 | | type_refinement_operations2([Op|Rest],MName,M,AbstractMachine,Ein,Eout) :- |
| 1435 | | get_abstract_operation_name_wo_infos(Op,AOp), |
| 1436 | | %print(treating_refines_operation(Op,AOp)),nl, |
| 1437 | | get_texpr_pos(Op,Pos), |
| 1438 | | % look up the abstract definition |
| 1439 | | get_abstract_op(AOp,MName,AbstractMachine,Pos,Ein,E1), |
| 1440 | | % store the type in the identifier section |
| 1441 | | copy_texpr_wo_info(Op,SOp), |
| 1442 | | ( get_section(promoted,M,Operations), |
| 1443 | | memberchk(SOp, Operations) -> true |
| 1444 | | ; get_section(unpromoted,M,Operations), % this is probably a LOCAL_OPERATION |
| 1445 | | memberchk(SOp, Operations) -> true |
| 1446 | | ; add_error(btypechecker,'Could not find operation for type checking:',Op),fail |
| 1447 | | ), |
| 1448 | | % do the rest |
| 1449 | | type_refinement_operations2(Rest,MName,M,AbstractMachine,E1,Eout). |
| 1450 | | % looks up the type of the operator in an abstract machine |
| 1451 | | get_abstract_op(Op,_,Abstraction,_,Errors,Errors) :- |
| 1452 | | % look for the operation in promoted and unpromoted |
| 1453 | | ( get_section(promoted,Abstraction,AbstractOps), member(Op,AbstractOps) |
| 1454 | | ; get_section(unpromoted,Abstraction,AbstractOps), member(Op,AbstractOps) ), |
| 1455 | | % forget alternatives |
| 1456 | | !. |
| 1457 | | get_abstract_op(Op,_,_Abstraction,_Pos,Errors,Errors) :- |
| 1458 | | % we might allow new operations |
| 1459 | | get_preference(allow_new_ops_in_refinement,true),!, % ALLOW_NEW_OPERATIONS_IN_REFINEMENT |
| 1460 | | get_texpr_type(Op,op(_,_)). |
| 1461 | | get_abstract_op(Op,MName,AbstractMachine,Pos,[warning(Msg,Pos)|Eout],Eout) :- |
| 1462 | | % in case we do not find the operation, store an error |
| 1463 | | get_texpr_id(Op,op(Id)), |
| 1464 | | get_machine_name(AbstractMachine,Name), |
| 1465 | | ajoin(['operation ', Id, ' from ', MName, ' is not defined in the abstract machine ',Name, |
| 1466 | | ' (set ALLOW_NEW_OPERATIONS_IN_REFINEMENT to TRUE to allow this)'], Msg). |
| 1467 | | % copy a typed expression without the additional information (just expression and type) |
| 1468 | | copy_texpr_wo_info(A,B) :- |
| 1469 | | % copy the expression and type, the additional information may be different |
| 1470 | | get_texpr_expr(A,Expr),get_texpr_expr(B,Expr), |
| 1471 | | get_texpr_type(A,Type),get_texpr_type(B,Type). |
| 1472 | | |
| 1473 | | get_abstract_operation_name_wo_infos(b(_,Type,Infos),Res) :- |
| 1474 | | memberchk(refines_operation(RefID),Infos),!, % renaming occurs: |
| 1475 | | Res = b(identifier(op(RefID)),Type,_). |
| 1476 | | get_abstract_operation_name_wo_infos(ID,Copy) :- copy_texpr_wo_info(ID,Copy). |
| 1477 | | |
| 1478 | | create_id_sections(Header,RawMachine,Name) --> |
| 1479 | | create_id_sections_header(Header), |
| 1480 | | %{print(created_header(Name)),nl}, |
| 1481 | | create_set_sections(RawMachine,Name), |
| 1482 | | %{print(created_set(Name)),nl}, |
| 1483 | | create_constants_sections(RawMachine), |
| 1484 | | %{print(created_constants(Name)),nl}, |
| 1485 | | create_variables_sections(RawMachine), |
| 1486 | | %{print(created_variables(Name)),nl}, |
| 1487 | | create_operations_sections(RawMachine,Name). |
| 1488 | | |
| 1489 | | extract_parameter_types(MachineRefs,ParameterTypes) :- |
| 1490 | | maplist(extract_parameter_types2,MachineRefs,ParameterTypesL), |
| 1491 | | append(ParameterTypesL,ParameterTypes). |
| 1492 | | extract_parameter_types2(ref(_,Machine),ParameterTypes) :- |
| 1493 | | get_section(parameters,Machine,VisibleParams), |
| 1494 | | get_section(internal_parameters,Machine,InternalParams), |
| 1495 | | append(VisibleParams,InternalParams,Params), |
| 1496 | | include(is_a_parameter_set,Params,ParameterSets), |
| 1497 | | maplist(get_texpr_set_type,ParameterSets,ParameterTypes). |
| 1498 | | is_a_parameter_set(TExpr) :- |
| 1499 | | get_texpr_info(TExpr,Info), |
| 1500 | | memberchk(parameter_set,Info). |
| 1501 | | |
| 1502 | | type_sections(RawMachine,MachineType,RefMachines,NonGroundExceptions,Name,Ein,Eout) --> |
| 1503 | | {debug_stats('TYPING CONSTRAINTS'(Name))}, |
| 1504 | | type_constraints(MachineType,Name,RawMachine,RefMachines,NonGroundExceptions,Ein,E1), |
| 1505 | | % Maybe the VALUES section must be moved up later because it may be used to |
| 1506 | | % substitute types (e.g. deferred sets to integers) for later use |
| 1507 | | {debug_stats('TYPING PROPERTIES'(Name))}, |
| 1508 | | type_section_with_single_predicate(properties,Name,[constants],MachineType,RawMachine,RefMachines,NonGroundExceptions,E1,E2), |
| 1509 | | {debug_stats('TYPING INVARIANT'(Name))}, |
| 1510 | | type_section_with_single_predicate(invariant,Name,[variables],MachineType,RawMachine,RefMachines,NonGroundExceptions,E2,E3), |
| 1511 | | {debug_stats('TYPING ASSERTIONS'(Name))}, |
| 1512 | | type_section_with_predicate_list(assertions,[],MachineType,RawMachine,RefMachines,NonGroundExceptions,E3,E4), |
| 1513 | | {debug_stats('TYPING INITIALISATION'(Name))}, |
| 1514 | | type_initialisation_section(RawMachine,Name,MachineType,RefMachines,NonGroundExceptions,E4,E5), |
| 1515 | | {debug_stats('TYPING OPERATIONS'(Name))}, |
| 1516 | | type_operations_section(RawMachine,MachineType,RefMachines,NonGroundExceptions,E5,Eout), |
| 1517 | | {debug_stats('FINISHED TYPING SECTIONS'(Name))}. |
| 1518 | | |
| 1519 | | % skip this section, it is copied from the abstract machine and |
| 1520 | | % does not need to be typed again |
| 1521 | | type_constraints(refinement,_,_RawMachine,_RefMachines,_NonGroundExceptions,Errors,Errors) --> !. |
| 1522 | | type_constraints(implementation,_,_RawMachine,_RefMachines,_NonGroundExceptions,Errors,Errors) --> !. |
| 1523 | | type_constraints(machine,Name,RawMachine,RefMachines,NonGroundExceptions,Ein,Eout) --> |
| 1524 | | % if the machine is a dummy machine (in presence of a not included seen or used |
| 1525 | | % machine), we must omit the check that the (lower case) parameters are all typed. |
| 1526 | | % We can assume that they are properly typed by the included machine. |
| 1527 | | {(is_dummy_machine(RawMachine) -> IdsToType = [] ; IdsToType = [parameters])}, |
| 1528 | | type_section_with_single_predicate(constraints,Name,IdsToType,machine, |
| 1529 | | RawMachine,RefMachines,NonGroundExceptions,Ein,Eout). |
| 1530 | | |
| 1531 | ? | is_dummy_machine(RawMachine) :- member(is_dummy,RawMachine),!. |
| 1532 | | |
| 1533 | | % Header: Parameters |
| 1534 | | create_id_sections_header(machine_header(_,_,Parameters),Old,New) :- |
| 1535 | | write_section(parameters,TParams,Old,New), |
| 1536 | | maplist(create_id_section_parameter,Parameters,TParams). |
| 1537 | | create_id_section_parameter(Param,TParam) :- |
| 1538 | | Expr=identifier(Name), |
| 1539 | | ext2int_with_pragma(Param,Expr,_,Type,Expr,[ParameterType],TParam), |
| 1540 | | ( is_upper_case(Name) -> |
| 1541 | | ParameterType = parameter_set, |
| 1542 | | Type = set(_) |
| 1543 | | ; |
| 1544 | | ParameterType = parameter_scalar). |
| 1545 | | is_upper_case(Name) :- \+ atom(Name),!, add_internal_error('Illegal call:', is_upper_case(Name)),fail. |
| 1546 | | is_upper_case(Name) :- atom_codes(Name,[C|_]), |
| 1547 | | memberchk(C,"ABCDEFGHIJKLMNOPQRSTUVWXYZ"). |
| 1548 | | |
| 1549 | | % Body: Sets |
| 1550 | | create_set_sections(Sections,MachineName) --> |
| 1551 | | write_section(deferred_sets,DeferredSets), |
| 1552 | | write_section(enumerated_sets,EnumeratedSets), |
| 1553 | | write_section(enumerated_elements,EnumeratedElements), |
| 1554 | | {optional_rawmachine_section(sets,Sections,[],Sets), |
| 1555 | | split_list(is_deferred_set_element,Sets,RawDeferredSets,RawEnumeratedSets), |
| 1556 | | maplist(create_deferred_set_section(MachineName),RawDeferredSets,DeferredSets), |
| 1557 | | maplist(create_enumerated_set_section(Sections,MachineName), |
| 1558 | | RawEnumeratedSets,EnumeratedSets,LEnumeratedElements), |
| 1559 | | append(LEnumeratedElements,EnumeratedElements)}. |
| 1560 | | is_deferred_set_element(AstElem) :- has_functor(AstElem,deferred_set,_). |
| 1561 | | create_deferred_set_section(MachineName,DS,TExpr) :- |
| 1562 | | unwrap_opt_description(DS,deferred_set(Pos,I),TInfos), |
| 1563 | | Infos = [given_set,def(deferred_set,MachineName)|TInfos], |
| 1564 | | create_global_id(I,Pos,Infos,TExpr). |
| 1565 | | create_enumerated_set_section(Sections,MachineName,ES,TExpr,Elements) :- |
| 1566 | | unwrap_opt_description(ES,EnumSetList,TInfos), |
| 1567 | | create_enum_set_aux(EnumSetList,Sections,MachineName,TInfos,TExpr,Elements). |
| 1568 | | |
| 1569 | | create_global_id(identifier(_,Id),Pos,Infos,TExpr) :- !, |
| 1570 | | add_warning(bmachine_construction,'Identifier unexpectedly not atomic: ',Id,Pos), % happened e.g. in ANTLR parser |
| 1571 | | create_identifier(Id,Pos,set(global(Id)),Infos,TExpr). |
| 1572 | | create_global_id(Id,Pos,Infos,TExpr) :- !, |
| 1573 | | create_identifier(Id,Pos,set(global(Id)),Infos,TExpr). |
| 1574 | | |
| 1575 | | create_enum_set_aux(enumerated_set(Pos,I,Elems),_,MachineName,TInfos,TExpr,Elements) :- !, |
| 1576 | | % regular case I = {Elems1, ...} |
| 1577 | | Infos = [given_set,def(enumerated_set,MachineName)|TInfos], |
| 1578 | | create_global_id(I,Pos,Infos,TExpr), |
| 1579 | | maplist(create_enum_set_element(I,MachineName),Elems,Elements). |
| 1580 | | create_enum_set_aux(enumerated_set_via_def(Pos,I,ElemsDEF),Sections,MachineName,TInfos,TExpr,Elements) :- !, |
| 1581 | | % we have the case I = ElemsDEF and DEFINITIONS ElemsDEF == {Elems1, ...} |
| 1582 | | Infos = [given_set,def(enumerated_set,MachineName)|TInfos], |
| 1583 | | create_global_id(I,Pos,Infos,TExpr), |
| 1584 | | (optional_rawmachine_section(definitions,Sections,[],Defs), |
| 1585 | | member(expression_definition(DPos,ElemsDEF,Paras,DefBody),Defs) |
| 1586 | | -> (Paras \= [] |
| 1587 | | -> add_error(bmachine_construction, |
| 1588 | | 'DEFINITION for enumerated set elements must not have parameters:',ElemsDEF,DPos), |
| 1589 | | Elements=[] |
| 1590 | | ; DefBody = set_extension(_,Elems), |
| 1591 | | maplist(create_enum_set_element(I,MachineName),Elems,Elements) |
| 1592 | | -> true |
| 1593 | | ; add_error(bmachine_construction, |
| 1594 | | 'DEFINITION for enumerated set elements must be of the form {El1,El2,...}:',ElemsDEF,DPos), |
| 1595 | | Elements=[] |
| 1596 | | ) |
| 1597 | | ; add_error(bmachine_construction,'No DEFINITION for enumerated set elements found:',ElemsDEF,Pos), |
| 1598 | | Elements=[] |
| 1599 | | ). |
| 1600 | | create_enum_set_aux(E,_,_,_,_,_) :- add_internal_error('Illegal enumerated set:',E),fail. |
| 1601 | | |
| 1602 | | |
| 1603 | | % deal with optional description(Pos,Desc,A) wrapper |
| 1604 | | has_functor(description(_,_Desc,A),Functor,Arity) :- !, functor(A,Functor,Arity). |
| 1605 | | has_functor(A,Functor,Arity) :- functor(A,Functor,Arity). |
| 1606 | | |
| 1607 | | % remove description wrapper and generate info field |
| 1608 | | unwrap_opt_description(Pragma,Res,Infos) :- |
| 1609 | | unwrap_pragma(Pragma,Expr,I),!, Res=Expr,Infos=I. |
| 1610 | | unwrap_opt_description(A,A,[]). |
| 1611 | | |
| 1612 | | |
| 1613 | | create_enum_set_element(Id,MachineName,Ext,Elem) :- |
| 1614 | | (Id=identifier(none,RID) |
| 1615 | | -> Type=global(RID), add_warning(bmachine_construction,'Unexpected non-atomic global set id: ',RID) |
| 1616 | | ; Type=global(Id)), |
| 1617 | | ext2int_with_pragma(Ext,Expr,_Pos,Type,Expr,[enumerated_set_element,def(enumerated_element,MachineName)],Elem). |
| 1618 | | |
| 1619 | | create_identifier(Id,Pos,Type,Infos,TExpr) :- |
| 1620 | | create_texpr(identifier(Id),Type,[nodeid(Pos)|Infos],TExpr). |
| 1621 | | |
| 1622 | | % Constants |
| 1623 | | create_constants_sections(RawMachine) --> |
| 1624 | | create_section_identifiers(constants,concrete_constants,RawMachine), |
| 1625 | | create_section_identifiers(abstract_constants,abstract_constants,RawMachine). |
| 1626 | | % Variables |
| 1627 | | create_variables_sections(RawMachine) --> |
| 1628 | | create_section_identifiers(concrete_variables,concrete_variables,RawMachine), |
| 1629 | | create_section_identifiers(variables,abstract_variables,RawMachine). |
| 1630 | | |
| 1631 | | % Freetypes: Treat them as additional constants, plus add entries in the "freetypes" |
| 1632 | | % section of the resulting machine |
| 1633 | | create_freetypes(RawMachine,MType,RefMachines,Old,New,Ein,Eout) :- |
| 1634 | | optional_rawmachine_section(freetypes,RawMachine,[],RawFreetypes), |
| 1635 | ? | create_freetypes2(RawFreetypes,MType,[ref(local,Old)|RefMachines],Old,New,Ein,Eout). |
| 1636 | | create_freetypes2([],_MType,_RefMachines,M,M,E,E) :- !. |
| 1637 | | create_freetypes2(RawFreetypes,MType,RefMachines,Old,New,Ein,Eout) :- |
| 1638 | | % we need the NonGroundExceptions for type checking |
| 1639 | | extract_parameter_types(RefMachines,NonGroundExceptions), |
| 1640 | | % create identifiers in the constants section |
| 1641 | ? | maplist(create_ids_for_freetype,RawFreetypes,IdsFreetypes), |
| 1642 | | % we just combined the results to keep the numbers of arguments low (too much for maplist) |
| 1643 | | maplist(split_ft,IdsFreetypes,IdentifiersL,Freetypes), |
| 1644 | | append(IdentifiersL,Identifiers), |
| 1645 | | % create properties for each freetype |
| 1646 | | foldl(create_properties_for_freetype(MType,RefMachines,NonGroundExceptions,Identifiers), |
| 1647 | | RawFreetypes,IdsFreetypes,PropertiesL,Ein,Eout), |
| 1648 | | conjunct_predicates(PropertiesL,Properties), |
| 1649 | | (debug_mode(off) -> true |
| 1650 | | ; format('Created PROPERTIES for FREETYPES:~n',[]), translate:nested_print_bexpr(Properties),nl), |
| 1651 | | append_to_section(abstract_constants,Identifiers,Old,Inter), |
| 1652 | | conjunct_to_section(properties,Properties,Inter,Inter2), |
| 1653 | | write_section(freetypes,Freetypes,Inter2,New). |
| 1654 | | |
| 1655 | | split_ft(ft(Ids,Freetype),Ids,Freetype). |
| 1656 | | |
| 1657 | | |
| 1658 | | create_ids_for_freetype(FT,ft([TId|TCons],freetype(Id,Cases))) :- |
| 1659 | | is_freetype_declaration(FT,_Pos,Id,_TypeParams,Constructors), |
| 1660 | | !, |
| 1661 | | create_typed_id_with_given_set_info(Id,set(freetype(Id)),TId), |
| 1662 | ? | maplist(create_ids_for_constructor(Id),Constructors,TCons,Cases). |
| 1663 | | create_ids_for_freetype(FT,_) :- |
| 1664 | | add_internal_error('Illegal freetype term:',create_ids_for_freetype(FT,_)),fail. |
| 1665 | | |
| 1666 | | % add given_set info so that is_just_type3 can detect this as a type |
| 1667 | | create_typed_id_with_given_set_info(IDName,Type,b(identifier(IDName),Type,[given_set])). |
| 1668 | | |
| 1669 | | % deconstruct a .prob Prolog encoding of a freetype declaration |
| 1670 | | % new versions of parser generate freetype parameters |
| 1671 | | is_freetype_declaration(freetype(Pos,Id,Constructors),Pos,Id,[],Constructors). |
| 1672 | | is_freetype_declaration(freetype(Pos,Id,TypeParams,Constructors),Pos,Id,TypeParams,Constructors) :- |
| 1673 | | (TypeParams=[] -> true ; add_warning(bmachine_construction,'Not yet supporting freetype parameters:',Id,Pos)). |
| 1674 | | |
| 1675 | | create_ids_for_constructor(Id,constructor(_Pos,Name,_Arg),TCons,case(Name,Type)) :- |
| 1676 | | create_typed_id(Name,set(couple(Type,freetype(Id))),TCons). |
| 1677 | | create_ids_for_constructor(Id,element(_Pos,Name),TCons,case(Name,constant([Name]))) :- |
| 1678 | | create_typed_id(Name,freetype(Id),TCons). |
| 1679 | | |
| 1680 | | create_properties_for_freetype(MType,RefMachines,NonGroundExceptions, AllFTIdentifiers, |
| 1681 | | FREETYPE,ft(Ids,_Freetypes),Properties,Ein,Eout) :- |
| 1682 | | is_freetype_declaration(FREETYPE,_Pos,Id,_TypeParams,Constructors), |
| 1683 | | debug_format(9,'Processing freetype ~w (one of ~w)~n',[Id,AllFTIdentifiers]), |
| 1684 | | % The freetype type |
| 1685 | | FType = freetype(Id), |
| 1686 | | % We use the standard type environment of properties... |
| 1687 | | visible_env(MType,properties,RefMachines,CEnv,Ein,E1), |
| 1688 | | % ...plus the identifiers of the free type (type name and constructor names) |
| 1689 | | add_identifiers_to_environment(Ids,CEnv,FEnv0), |
| 1690 | | % ...plus the identifiers of all free type names (will overwrite Id, but not a problem) |
| 1691 | | % Note: instead of adding all freetype ids, we could just add the ones preceding Id |
| 1692 | | add_identifiers_to_environment(AllFTIdentifiers,FEnv0,FEnv), |
| 1693 | | % We generate a comprehension set for all elements |
| 1694 | | create_typed_id(Id,set(FType),TId), |
| 1695 | | create_texpr(equal(TId,TComp),pred,[],FDef), |
| 1696 | | unique_typed_id("_freetype_arg",FType,Element), |
| 1697 | | create_recursive_compset([Element],ECond,set(FType),[],RecId,TComp), |
| 1698 | | create_typed_id(RecId,set(FType),TRecId), |
| 1699 | | % For each constructor, we generate a definition and a condition for the |
| 1700 | | % comprehension set above |
| 1701 | | foldl(create_properties_for_constructor(Id,FEnv,Element,TRecId,NonGroundExceptions), |
| 1702 | | Constructors,Defs,Conds,E1,Eout), |
| 1703 | | conjunct_predicates(Conds,ECond), |
| 1704 | | conjunct_predicates([FDef|Defs],Properties). |
| 1705 | | |
| 1706 | | /* create_properties_for_constructor(+Env,+Element,+RecId,+NGE,+Constructor,-Def,-Cond,Ein,Eout) |
| 1707 | | Env: Type environment |
| 1708 | | Element: A typed identifier "e" that is used in the definition of the freetype set: |
| 1709 | | ft = {e | e has_freetype_constructor x => e:...} |
| 1710 | | RecId: The typed identifier that can be used to refer to the freetype set (ft in the |
| 1711 | | example above |
| 1712 | | NGE: "Non ground exceptions", needed for type checking when having a parametrized machine |
| 1713 | | Constructor: The constructor expression as it comes from the parser |
| 1714 | | (constructor(Pos,Name,ArgSet) or element(Pos,Name)) |
| 1715 | | Def: The predicate that defines the constant for the constructor, |
| 1716 | | e.g. "cons = {i,o | i:NAT & o = freetype(cons,i)}" |
| 1717 | | Cond: The predicate that checks the argument of a freetype in the freetype set |
| 1718 | | (That would be the part "e:..." in the example above. |
| 1719 | | Ein,Eout: Used for type checker errors |
| 1720 | | */ |
| 1721 | | create_properties_for_constructor(FID,Env,Element,RecId,NonGroundExceptions, |
| 1722 | | Constructor,Def,Cond,Ein,Eout) :- |
| 1723 | | constructor_name(Constructor,Name), |
| 1724 | | env_lookup_type(Name,Env,CType), |
| 1725 | | create_properties_for_constructor2(Constructor,Env,NonGroundExceptions,FID, |
| 1726 | | Element,RecId,CDef,Cond,Ein,Eout), |
| 1727 | | get_texpr_type(CDef,CType), |
| 1728 | | create_typed_id(Name,CType,CId), |
| 1729 | | create_texpr(equal(CId,CDef),pred,[],Def). |
| 1730 | | constructor_name(element(_Pos,Name),Name). |
| 1731 | | constructor_name(constructor(_Pos,Name,_Domain),Name). |
| 1732 | | create_properties_for_constructor2(element(_Pos,Name),_Env,_NonGroundExceptions,FID, |
| 1733 | | _Element,_RecId,CDef,Cond,Ein,Ein) :- |
| 1734 | | create_texpr(value(freeval(FID,Name,term(Name))),freetype(FID),[],CDef), |
| 1735 | | create_texpr(truth,pred,[],Cond). |
| 1736 | | create_properties_for_constructor2(constructor(_Pos,Name,RArg),Env,NonGroundExceptions, |
| 1737 | | FID,Element,RecId,CDef,Cond,Ein,Eout) :- |
| 1738 | | % First, type check the given set of the domain: |
| 1739 | | btype_ground_dl([RArg],Env,NonGroundExceptions,[set(DType)],[TDomain],Ein,Eout), |
| 1740 | | % then create the RHS of "c = {i,o | i:Domain & o=freetype_constructor(Name,i)}" |
| 1741 | | create_definition_for_constructor(Name,TDomain,FID,CDef), |
| 1742 | | % The check in the freetype comprehension set is of the form |
| 1743 | | % e "of_freetype_case" Name => "content_of"(e) : Domain |
| 1744 | | create_texpr(implication(IsCase,DomainTest),pred,[],Cond), |
| 1745 | | create_texpr(freetype_case(FID,Name,Element),pred,[],IsCase), |
| 1746 | | create_texpr(freetype_destructor(FID,Name,Element),DType,[],Content), |
| 1747 | | % all references to the freetype itself are replaced by the recursive reference |
| 1748 | | replace_id_by_expr(TDomain,FID,RecId,TDomain2), |
| 1749 | | create_texpr(member(Content,TDomain2),pred,[],DomainTest). |
| 1750 | | |
| 1751 | | :- use_module(bsyntaxtree,[get_texpr_set_type/2]). |
| 1752 | | |
| 1753 | | /* The constructor is a function to the freetype, defined with a comprehension set: |
| 1754 | | The general form is "c = {i,o | i:Domain & o=freetype_constructor(Name,i)}" |
| 1755 | | create_definition_for_constructor(+Name,+DType,+FID,-CType,-CDef) :- |
| 1756 | | Name: Name of the constructor |
| 1757 | | TDomain: The user-specified domain |
| 1758 | | FID: The name of the free type |
| 1759 | | CDef: The RHS of the definition "Name = CDef" |
| 1760 | | */ |
| 1761 | | create_definition_for_constructor(Name,TDomain,FID,CDef) :- |
| 1762 | | % get the type of the domain: |
| 1763 | | get_texpr_set_type(TDomain,DType), |
| 1764 | | % create argument and result identifiers: |
| 1765 | | unique_typed_id("_constr_arg",DType,TArgId), % was constructor_arg and constructor_res |
| 1766 | | unique_typed_id("_constr_res",freetype(FID),TResId), |
| 1767 | | % The comprehension set as a whole |
| 1768 | | CType = set(couple(DType,freetype(FID))), |
| 1769 | | create_texpr(comprehension_set([TArgId,TResId],Pred),CType, |
| 1770 | | [prob_annotation('SYMBOLIC')],CDef), |
| 1771 | | create_texpr(conjunct(DomainCheck,Construction),pred,[],Pred), |
| 1772 | | % "i:Domain" |
| 1773 | | create_texpr(member(TArgId,TDomain),pred,[],DomainCheck), |
| 1774 | | % "o=freetype_constructor(i) |
| 1775 | | create_texpr(freetype_constructor(FID,Name,TArgId),freetype(FID),[],FreetypeCons), |
| 1776 | | create_texpr(equal(TResId,FreetypeCons),pred,[],Construction). |
| 1777 | | |
| 1778 | | % Operations |
| 1779 | | create_operations_sections(RawMachine,Name,Old,New) :- |
| 1780 | | write_section(promoted,PromotedOperationIds,Old,New0), |
| 1781 | | get_operation_identifiers(RawMachine,operations,OperationIdentifiers), |
| 1782 | | (get_operation_identifiers(RawMachine,local_operations,LocOpIDs), |
| 1783 | | LocOpIDs \= [] % if there is a LOCAL_OPERATIONS section we assume user wants to call them |
| 1784 | | -> maplist(add_infos_to_identifier([is_local_operation]),LocOpIDs,LocOpIds2), |
| 1785 | | append_to_section(unpromoted,LocOpIds2,New0,New), |
| 1786 | | % Now remove all LOCAL_OPERATIONS from the promoted ones |
| 1787 | | % see for example prob_examples/examples/B/ClearSy/RoboSim/SRanger_case_Jul25/logic_i.imp |
| 1788 | | exclude(duplicate_local_operation_id(Name,LocOpIDs),OperationIdentifiers,PromotedOperationIds) |
| 1789 | | ; New = New0, PromotedOperationIds = OperationIdentifiers |
| 1790 | | ). |
| 1791 | | |
| 1792 | | |
| 1793 | | |
| 1794 | | % check if a LOCAL_OPERATION is already declared in the OPERATIONS section: |
| 1795 | | % in this case: we use the operation body defined in the OPERATIONS section, but remove it from the promoted list |
| 1796 | | duplicate_local_operation_id(Name,OpIds,TID) :- |
| 1797 | | get_texpr_id(TID,op(OpID)), |
| 1798 | | member(TID2,OpIds), |
| 1799 | | get_texpr_id(TID2,op(OpID)),!, |
| 1800 | | debug_println(9,duplicate_local_operation_id(OpID,Name)). |
| 1801 | | |
| 1802 | | get_operation_identifiers(RawMachine,OperationIdentifiers) :- |
| 1803 | | get_operation_identifiers(RawMachine,operations,OperationIdentifiers). |
| 1804 | | get_operation_identifiers(RawMachine,SECTION,OperationIdentifiers) :- |
| 1805 | | optional_rawmachine_section(SECTION,RawMachine,[],Ops), |
| 1806 | | maplist(extract_operation_identifier,Ops,OperationIdentifiers). |
| 1807 | | extract_operation_identifier(Ext,TId) :- |
| 1808 | | remove_pos(Ext, operation(ExtId,_,_,_)),!, |
| 1809 | | ext2int_with_pragma(ExtId,identifier(I),_,op(_,_),identifier(op(I)),Infos,TId), |
| 1810 | | operation_infos(Infos). |
| 1811 | | extract_operation_identifier(Ext,TId) :- |
| 1812 | | remove_pos(Ext, refined_operation(ExtId,_,_,RefinesOp,_)),!, |
| 1813 | | ext2int_with_pragma(ExtId,identifier(I),_,op(_,_),identifier(op(I)),[refines_operation(RefinesOp)|Infos],TId), |
| 1814 | | operation_infos(Infos). |
| 1815 | | extract_operation_identifier(Ext,TId) :- |
| 1816 | | remove_pos(Ext, description_operation(_Desc,RealOp)),!, |
| 1817 | | extract_operation_identifier(RealOp,TId). |
| 1818 | | extract_operation_identifier(Ext,_) :- add_internal_error('Unknown operation node:',Ext),fail. |
| 1819 | | |
| 1820 | | % VALUES section: |
| 1821 | | % process_values_section(MachineType,RawMachine,NonGroundExceptions,Min/Ein/RefMIn,Mout/Eout/RefMOut): |
| 1822 | | % Type-check the VALUES section and change the type of valuated deferred sets, if necessary |
| 1823 | | % MachineType, RawMachine, NonGroundExceptions: as usual, see other comments |
| 1824 | | % Min/Mout: The currently constructed machine |
| 1825 | | % Ein/Eout: The difference list of errors |
| 1826 | | % RefMin/RefMout: The list of already typechecked machines. These typechecked machines can be |
| 1827 | | % altered by this predicate because if a deferred set is valuated by an integer set or |
| 1828 | | % other deferred set, all occurrences of the original type are replaced by the new type, |
| 1829 | | % even for the already typed machines. |
| 1830 | | process_values_section(MachineType,RawMachine,NonGroundExceptions,Min/Ein/RefMIn,Mout/Eout/RefMOut) :- |
| 1831 | | optional_rawmachine_section(values,RawMachine,[],RawValues), |
| 1832 | | process_values_section_aux(RawValues,MachineType,NonGroundExceptions, |
| 1833 | | Min/Ein/RefMIn,Mout/Eout/RefMOut). |
| 1834 | | process_values_section_aux([],_MachineType,_NonGroundExceptions,In,Out) :- !,In=Out. |
| 1835 | | process_values_section_aux(RawValues,MachineType,NonGroundExceptions, |
| 1836 | | Min/Ein/RefMin,Mout/Eout/RefMout) :- |
| 1837 | | debug_stats('TYPING VALUES'), |
| 1838 | | type_values_section(MachineType,RawValues,RefMin,NonGroundExceptions,Min/Ein,Mout/Eout), |
| 1839 | | % will be added as additional_property in bmachine |
| 1840 | | RefMin=RefMout. |
| 1841 | | |
| 1842 | | type_values_section(MachineType,RawValues,RefMachines,NonGroundExceptions,Min/Ein,Mout/Eout) :- |
| 1843 | | write_section(values,Values,Min,Mout), |
| 1844 | | visible_env(MachineType,values_expression,RefMachines,Env,Ein,E1), |
| 1845 | | % We have to pass an environment that can be modified because in each |
| 1846 | | % valuation the previously valuated constants can be used. |
| 1847 | | foldl(extract_values_entry(NonGroundExceptions),RawValues,Values,Env/E1,_ResultingEnv/Eout). |
| 1848 | | |
| 1849 | | extract_values_entry(NonGroundExceptions, values_entry(POS,ValueID,ValueExpr), Entry, |
| 1850 | | EnvIn/Ein,EnvOut/Eout) :- |
| 1851 | | % TODO: There seem to be a lot of additional constraints for valuations in VALUES that are not |
| 1852 | | % yet handled here |
| 1853 | | btype_ground_dl([ValueExpr],EnvIn,NonGroundExceptions,[Type],[TExpr],Ein,Eout), |
| 1854 | | clean_up(TExpr,[],CTExpr), % ensure we remove things like mult_or_cart/2 |
| 1855 | | create_identifier(ValueID,POS,Type,[valuated_constant],TypedID), |
| 1856 | | create_texpr(values_entry(TypedID,CTExpr),values_entry,[nodeid(POS)],Entry), |
| 1857 | | debug_println(9,valued_constant(ValueID)), |
| 1858 | | EnvOut=EnvIn. |
| 1859 | | %add_identifiers_to_environment([TypedID],EnvIn,EnvOut). % ideally we should register the new type of TypedID |
| 1860 | | % However: ProB can currently only process VALUES clauses where the type does not change |
| 1861 | | |
| 1862 | | % type_section_with_single_predicate(+Sec,+Name,+SectionsToType,+MachineType,+Sections, |
| 1863 | | % +RefMachines,+NonGroundExceptions,+Ein,-Eout,+Old,-New): |
| 1864 | | % Type a section such as INVARIANT, PROPERTIES, CONSTRAINTS with a single predicate |
| 1865 | | % Sec: section name in the raw (untyped) machine (e.g. invariant) |
| 1866 | | % Name: name of machine from which this section comes |
| 1867 | | % SectionsToType: list of section names that contain identifiers that must be typed |
| 1868 | | % by this predicate (e.g. all variables must be typed by the invariant) |
| 1869 | | % MachineType: machine type (machine, refinement, ...) |
| 1870 | | % Sections: list of sections representing the raw (untyped) machine |
| 1871 | | % RefMachines: list of already typed machines |
| 1872 | | % NonGroundExceptions: list of types that may be not ground because the concrete type |
| 1873 | | % is determinded by machine parameter |
| 1874 | | % Ein/Eout: difference list of errors |
| 1875 | | % Old/New: the new typed section is added (by conjunction) to the machine |
| 1876 | | type_section_with_single_predicate(Sec,Name,SectionsToType,MachineType,Sections, |
| 1877 | | RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :- |
| 1878 | | optional_rawmachine_section(Sec,Sections,truth(none),Predicate), |
| 1879 | | ( Predicate = truth(_) -> |
| 1880 | | % even if there is no content, we must check if all identifiers are typed |
| 1881 | | check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,Ein,Eout), |
| 1882 | | Old=New |
| 1883 | | ; |
| 1884 | | get_machine_infos(Sections,Infos), |
| 1885 | | toplevel_raw_predicate_sanity_check(Sec,Name,Predicate,Infos), |
| 1886 | | type_predicates(Sec,SectionsToType,MachineType,[Predicate],RefMachines,NonGroundExceptions, |
| 1887 | | [Typed],Ein,Eout), |
| 1888 | | conjunct_to_section(Sec,Typed,Old,New) |
| 1889 | | ), |
| 1890 | | !. |
| 1891 | | type_section_with_single_predicate(Sec,Name,SectsToType,MchType,_,_,_,_,_,_,_) :- |
| 1892 | | add_internal_error('type_section_with_single_predicate failed', |
| 1893 | | type_section_with_single_predicate(Sec,Name,SectsToType,MchType,_,_,_,_,_,_,_)), |
| 1894 | | fail. |
| 1895 | | |
| 1896 | | % get some infos relevant for sanity check: |
| 1897 | | get_machine_infos(Sections,Infos) :- |
| 1898 | | ((rawmachine_section_exists(concrete_variables,Sections) ; rawmachine_section_exists(abstract_variables,Sections)) |
| 1899 | | -> Infos = [has_variables|I1] ; Infos = I1), |
| 1900 | | ((rawmachine_section_exists(concrete_constants,Sections) ; rawmachine_section_exists(abstract_constants,Sections)) |
| 1901 | | -> I1 = [has_constants] ; I1 = []). |
| 1902 | | |
| 1903 | | % Type a section with multiple predicates, such as ASSERTIONS |
| 1904 | | type_section_with_predicate_list(Sec,SectionsToType,MachineType,Sections, |
| 1905 | | RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :- |
| 1906 | | write_section(Sec,Typed,Old,New), |
| 1907 | | optional_rawmachine_section(Sec,Sections,[],Predicates), |
| 1908 | | type_predicates(Sec,SectionsToType,MachineType,Predicates,RefMachines,NonGroundExceptions,Typed,Ein,Eout), |
| 1909 | | !. |
| 1910 | | type_section_with_predicate_list(Sec,SectsToType,MchType,Sects,RefMchs,NonGrndExc,Ein,Eout,Old,New) :- |
| 1911 | | add_internal_error('type_section_with_predicate_list failed', |
| 1912 | | type_section_with_predicate_list(Sec,SectsToType,MchType,Sects,RefMchs,NonGrndExc,Ein,Eout,Old,New)), |
| 1913 | | fail. |
| 1914 | | |
| 1915 | | |
| 1916 | | type_predicates(_Sec,SectionsToType,_MachineType,[],RefMachines,NonGroundExceptions,Typed,Ein,Eout) :- |
| 1917 | | !,Typed=[], |
| 1918 | | check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,Ein,Eout). |
| 1919 | | type_predicates(Sec,SectionsToType,MachineType,Predicates,RefMachines,NonGroundExceptions,Typed,Ein,Eout) :- |
| 1920 | | visible_env(MachineType, Sec, RefMachines, Env, Ein, E1), |
| 1921 | | same_length(Predicates,Types),maplist(is_pred_type,Types), |
| 1922 | | btype_ground_dl_in_section(Sec,Predicates,Env,NonGroundExceptions,Types,Typed1,E1,E2), |
| 1923 | | mark_with_section(Sec,Typed1,Typed), |
| 1924 | | check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,E2,Eout), |
| 1925 | | (no_perrors_occured(Ein,Eout) |
| 1926 | | -> perform_post_static_check(Typed) % only run if no type errors, it makes use of find_typed_identifier_uses |
| 1927 | | ; true |
| 1928 | | ). |
| 1929 | | |
| 1930 | | no_perrors_occured(Ein,Eout) :- Ein==Eout,!. |
| 1931 | | no_perrors_occured([H|T],Eout) :- nonvar(H),not_a_perror(H),no_perrors_occured(T,Eout). |
| 1932 | | |
| 1933 | | not_a_perror(warning(_,_)). |
| 1934 | | % other possible values: error(Msg,Pos), internal_error(Msg,Pos); see get_perror/2 |
| 1935 | | |
| 1936 | | % check if the identifiers that should be typed by this section are completly typed |
| 1937 | | check_if_all_ids_are_typed([],_RefMachines,_NonGroundExceptions,Ein,Eout) :- !,Ein=Eout. |
| 1938 | | check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,Ein,Eout) :- |
| 1939 | | memberchk(ref(local,Local),RefMachines), |
| 1940 | | get_all_identifiers(SectionsToType,Local,IdentifiersToType), |
| 1941 | | check_ground_types_dl(IdentifiersToType, NonGroundExceptions, Ein, Eout). |
| 1942 | | |
| 1943 | | |
| 1944 | | mark_with_section(Sec,In,Out) :- |
| 1945 | | maplist(mark_with_section2(Sec),In,Out). |
| 1946 | | mark_with_section2(Sec,In,Out) :- |
| 1947 | | remove_bt(In,conjunct(A,B),conjunct(NA,NB),Out),!, |
| 1948 | | mark_with_section2(Sec,A,NA), mark_with_section2(Sec,B,NB). |
| 1949 | | mark_with_section2(Sec,In,Out) :- |
| 1950 | | add_texpr_infos(In,[section(Sec)],Out). |
| 1951 | | |
| 1952 | | type_initialisation_section(Sections,Name,MType,RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :- |
| 1953 | | write_section(initialisation,Initialisation,Old,New), |
| 1954 | | ( rawmachine_section_with_opt_desc(initialisation,Sections,Init,Desc,DescPos) -> |
| 1955 | | visible_env(MType, initialisation, RefMachines, InitEnv, Ein, E1), |
| 1956 | | btype_ground_dl([Init],InitEnv,NonGroundExceptions,[subst],[TypedInit],E1,Eout), |
| 1957 | | (Desc='' -> TypedInit2 = TypedInit |
| 1958 | | ; add_texpr_infos(TypedInit,[description(Desc),description_position(DescPos)],TypedInit2) |
| 1959 | | ), |
| 1960 | | Initialisation=[init_stmt(Name,TypedInit2)] |
| 1961 | | ; |
| 1962 | | Ein=Eout, |
| 1963 | | Initialisation=[]). |
| 1964 | | |
| 1965 | | :- use_module(library(ugraphs)). |
| 1966 | | |
| 1967 | | type_operations_section(Sections,MType,RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :- |
| 1968 | | write_section(operation_bodies,Operations,Old,New), |
| 1969 | | visible_env(MType, operation_bodies, RefMachines, Env, Ein, E1), |
| 1970 | | optional_rawmachine_section(operations,Sections,[],Ops1), |
| 1971 | | optional_rawmachine_section(local_operations,Sections,[], LocalOps2), |
| 1972 | | exclude(duplicate_local_operation(Ops1),LocalOps2,FOps2), |
| 1973 | | append(FOps2,Ops1,Ops), |
| 1974 | | topological_sort_operations(Ops,LocalOps2,Env,SOps), |
| 1975 | | (debug_mode(off) -> true ; length(SOps,NrOps),debug_stats(finished_topological_sorting(NrOps))), |
| 1976 | | same_length(SOps,Types), maplist(is_op_type,Types), |
| 1977 | ? | btype_ground_dl(SOps,Env,NonGroundExceptions,Types,Operations,E1,Eout),!. |
| 1978 | | |
| 1979 | | % check if a LOCAL_OPERATION also exists as a regular operation; if so we can ignore it and |
| 1980 | | % just use the full operation; see also duplicate_local_operation_id above |
| 1981 | | duplicate_local_operation(NonLocalOps,LocalOperation) :- |
| 1982 | | raw_op_id(LocalOperation,OpName), |
| 1983 | | member(NonLocalOp,NonLocalOps), |
| 1984 | | raw_op_id(NonLocalOp,OpName), % we found a non-local operation with the same name |
| 1985 | | !, |
| 1986 | | raw_op_pos(LocalOperation,LPos), |
| 1987 | | raw_op_pos(NonLocalOp,NPos), |
| 1988 | | translate_span(NPos,PS2), |
| 1989 | | ajoin(['Ignoring LOCAL_OPERATION already defined in OPERATIONS section ',PS2,': '],Msg), |
| 1990 | | add_message(bmachine_construction,Msg,OpName,LPos). |
| 1991 | | |
| 1992 | | |
| 1993 | | allow_local_or_expr_op_calls :- |
| 1994 | | (get_preference(allow_local_operation_calls,true) -> true |
| 1995 | | ; get_preference(allow_operation_calls_in_expr,true)). |
| 1996 | | % at the moment ProB allows local calls inside expressions, independently of the allow_local_operation_calls preference |
| 1997 | | |
| 1998 | | % perform a topological sort of the operations: treat called operation before calling operation |
| 1999 | | % only relevant when allow_local_operation_calls is set to true |
| 2000 | | topological_sort_operations(Ops,LocalOps,Env,SortedOps) :- |
| 2001 | | (LocalOps = [] % there are no LOCAL_OPERATIONS |
| 2002 | | -> allow_local_or_expr_op_calls % unless call operations in machine itself, no need to perform a topological sort |
| 2003 | | ; true % we have local_operations, we need topological sort to ensure they are processed before other operations |
| 2004 | | ), |
| 2005 | | findall(OtherID-ID, (member(Op,Ops),op_calls_op(Op,Env,ID,OtherID)),Edges), |
| 2006 | | % print(edges(Edges)),nl, |
| 2007 | | % TO DO: maybe only store edges where OtherID also appears in Ops (i.e., call within same machine) |
| 2008 | | Edges \= [], |
| 2009 | | !, |
| 2010 | | findall(ID,(member(operation(_,RawID,_,_,_),Ops),raw_id(RawID,ID)),Vertices), %print(vertices(Vertices)),nl, |
| 2011 | | vertices_edges_to_ugraph(Vertices,Edges,Graph), |
| 2012 | | (top_sort(Graph,Sorted) |
| 2013 | | -> sort_ops(Sorted,Ops,SortedOps) |
| 2014 | | ; get_preference(allow_operation_calls_in_expr,true) -> |
| 2015 | | add_warning(topological_sort,'Mutual recursion or cycle in the (local) operation call graph, this may cause problems computing reads information: ',Edges), |
| 2016 | | SortedOps=Ops |
| 2017 | | % not necessarily a problem, because operations called in expressions are not allowed to modify the state |
| 2018 | | % TODO: however, we may have an issue with computing reads information correctly for mutual recursion !? |
| 2019 | | % direct recursion should be ok |
| 2020 | | ; add_error(topological_sort,'Cycle in the (local) operation call graph: ',Edges), |
| 2021 | | SortedOps=Ops). |
| 2022 | | topological_sort_operations(Ops,_,_,Ops). |
| 2023 | | |
| 2024 | | sort_ops([],Ops,Ops). % Ops should be [] |
| 2025 | | sort_ops([OpID|T],Ops,Res) :- |
| 2026 | | raw_op_id(Op1,OpID), |
| 2027 | | (select(Op1,Ops,TOps) |
| 2028 | | -> Res = [Op1|TSOps], sort_ops(T,TOps,TSOps) |
| 2029 | | ; % operation from another machine |
| 2030 | | % print(could_not_find(OpID,Ops)),nl, |
| 2031 | | sort_ops(T,Ops,Res) |
| 2032 | | ). |
| 2033 | | |
| 2034 | | is_op_type(op(_,_)). |
| 2035 | | is_pred_type(pred). |
| 2036 | | |
| 2037 | | % compute which other operations are directly called |
| 2038 | | op_calls_op(operation(_,RawID,_,_,RawBody),Env,ID,OtherID) :- raw_id(RawID,ID), |
| 2039 | | raw_body_calls_operation(RawBody,ID,Env,OtherID). |
| 2040 | | |
| 2041 | | raw_body_calls_operation(RawBody,ID,Env,OtherID) :- |
| 2042 | | raw_member(OpCall,RawBody), |
| 2043 | | raw_op_call(OpCall,ID,Env,RawOtherID), raw_id(RawOtherID,OtherID). |
| 2044 | | |
| 2045 | | raw_op_call(operation_call(_,RawOtherID,_,_),_,_, RawOtherID). |
| 2046 | | raw_op_call(operation_call_in_expr(_,RawOtherID,_),ID,_, RawOtherID) :- |
| 2047 | | \+ raw_id(RawOtherID,ID). % we do not look at direct recursion: it poses no problem for computing reads/writes info |
| 2048 | | raw_op_call(function(_,RawOtherID,_), ID, Env, RawOtherID) :- % function calls possibly not yet translated to operation_call_in_expr |
| 2049 | | get_preference(allow_operation_calls_in_expr,true), |
| 2050 | | \+ raw_id(RawOtherID,ID), % direct recursion ok |
| 2051 | | btypechecker:is_operation_call(RawOtherID,Env). |
| 2052 | | raw_op_call(identifier(Pos,OtherID), ID, Env, RawOtherID) :- % possible operation call in expr without arguments |
| 2053 | | OtherID \= ID, % direct recursion ok |
| 2054 | | get_preference(allow_operation_calls_in_expr,true), |
| 2055 | | RawOtherID = identifier(Pos,OtherID), |
| 2056 | | btypechecker:is_operation_call(RawOtherID,Env). |
| 2057 | | |
| 2058 | | |
| 2059 | | raw_op_id(operation(_,RawID,_,_,_RawBody),ID) :- raw_id(RawID,ID). |
| 2060 | | raw_id(identifier(_,ID),ID). |
| 2061 | | raw_op_pos(operation(Pos,_RawID,_,_,_RawBody),Pos). |
| 2062 | | |
| 2063 | | % a utility function to work on the raw AST Functor(POS,Arg1,...,Argn) |
| 2064 | | % this will not be able to look inside DEFINITIONS ! |
| 2065 | | % TO DO: deal with more raw substitutions which have list arguments |
| 2066 | | raw_member(X,X). |
| 2067 | | raw_member(X,parallel(_,List)) :- !, member(Term,List), raw_member(X,Term). |
| 2068 | | raw_member(X,sequence(_,List)) :- !, member(Term,List), raw_member(X,Term). |
| 2069 | | raw_member(X,[H|T]) :- !, (raw_member(X,H) ; raw_member(X,T)). |
| 2070 | | raw_member(X,Term) :- compound(Term), Term =.. [_Functor,_Pos|Args], |
| 2071 | | member(A,Args), raw_member(X,A). |
| 2072 | | |
| 2073 | | |
| 2074 | | create_section_identifiers(Section,DestSection,RawMachine,Old,New) :- |
| 2075 | | write_section(DestSection,Vars,Old,New), |
| 2076 | | optional_rawmachine_section(Section,RawMachine,[],Identifiers), |
| 2077 | | create_section_ids2(Identifiers,[],Vars,DestSection,New). |
| 2078 | | |
| 2079 | | create_section_ids2([],_,[],_,_). |
| 2080 | | create_section_ids2([Ext|Rest],Infos,Res,DestSection,MachSections) :- |
| 2081 | | expand_definition_to_variable_list(Ext,MachSections,List),!, |
| 2082 | | append(List,Rest,NewList), |
| 2083 | | create_section_ids2(NewList,Infos,Res,DestSection,MachSections). |
| 2084 | | create_section_ids2([Ext|Rest],Infos,Res,DestSection,MachSections) :- |
| 2085 | | create_section_id(Ext,Infos,DestSection,TId), |
| 2086 | | ( TId = error(Msg,Term,Pos) -> |
| 2087 | | Res = TRest, add_error(bmachine_construction,Msg,Term,Pos) |
| 2088 | | ; |
| 2089 | | Res = [TId|TRest]), |
| 2090 | | create_section_ids2(Rest,Infos,TRest,DestSection,MachSections). |
| 2091 | | create_section_id(Ext,Infos,DestSection,TId) :- |
| 2092 | | (unwrap_pragma(Ext,Ext2,PragmaInfos) -> append(PragmaInfos,Infos,FullInfos) |
| 2093 | | ; Ext2=Ext, FullInfos=Infos), |
| 2094 | | I=identifier(_), |
| 2095 | | ( ext2int(Ext2,I,_Pos,_Type,I,FullInfos,TId) -> |
| 2096 | | true |
| 2097 | | ; Ext2 = definition(POSINFO,ID,_) -> |
| 2098 | | TId = error('Trying to use DEFINITION name as identifier: ', |
| 2099 | | (ID,within(DestSection)), POSINFO) |
| 2100 | | ; |
| 2101 | | TId = error('Illegal identifier: ', |
| 2102 | | (Ext2,within(DestSection)), Ext2) |
| 2103 | | ). |
| 2104 | | |
| 2105 | | % support using DEFINITIONS which are variable lists; |
| 2106 | | % currently for ProB parser you need to write VARS == (x,y,..) for Atelier-B: VARS == x,y,.. |
| 2107 | | expand_definition_to_variable_list(definition(_POSINFO,ID,_),MachSections,List) :- |
| 2108 | | get_section(definitions,MachSections,Defs), |
| 2109 | | member(definition_decl(ID,expression,_InnerPos,[],RawExpr,_Deps),Defs), |
| 2110 | | extract_identifier_list(RawExpr,List,[]). |
| 2111 | | |
| 2112 | | % convert a raw tuple into a raw identifier list: |
| 2113 | | extract_identifier_list(identifier(Pos,ID)) --> [identifier(Pos,ID)]. |
| 2114 | | extract_identifier_list(couple(_,List)) --> |
| 2115 | | extract_identifier_list(List). |
| 2116 | | extract_identifier_list([]) --> []. |
| 2117 | | extract_identifier_list([H|T]) --> extract_identifier_list(H), extract_identifier_list(T). |
| 2118 | | |
| 2119 | | |
| 2120 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 2121 | | % sort the machines topologically |
| 2122 | | |
| 2123 | | % can be used to store the result: |
| 2124 | | assert_machine_order(Order) :- |
| 2125 | | retractall(machine_global_order(_)), |
| 2126 | | debug_print(9,machine_global_order(Order)), |
| 2127 | | assertz(machine_global_order(Order)). |
| 2128 | | |
| 2129 | | get_mach_position(Order,M,Ref,Pos-mch(M,Ref)) :- |
| 2130 | | get_machine_name(M,Name), |
| 2131 | ? | (nth1(Pos,Order,Name) -> true |
| 2132 | | ; add_internal_error('Unknown machine:',Name:Order), |
| 2133 | | Pos=0). |
| 2134 | | get_machine(_-mch(M,_),M). % re-extract info after sorting |
| 2135 | | get_reference(_-mch(_,R),R). |
| 2136 | | |
| 2137 | | :- use_module(library(samsort),[samkeysort/2]). |
| 2138 | | sort_machines_by_global_order(Machines,SortedMachines) :- |
| 2139 | | sort_machines_by_global_order(Machines,_,SortedMachines,_). |
| 2140 | | sort_machines_by_global_order(Machines,Refs,SortedMachines,SortedRefs) :- |
| 2141 | | machine_global_order(Order), |
| 2142 | | maplist(get_mach_position(Order),Machines,Refs,KM), % add position so that sorting works |
| 2143 | | samkeysort(KM,SKM), % for test 925 it is important to keep duplicates and not use sort/2 |
| 2144 | | maplist(get_machine,SKM,SortedMachines), |
| 2145 | | maplist(get_reference,SKM,SortedRefs),!. |
| 2146 | | %maplist(get_machine_name,Sorted,SNs),print(sorted(SNs)),nl. |
| 2147 | | sort_machines_by_global_order(M,R,M,R) :- |
| 2148 | | add_internal_error('Sorting machines failed:',M). |
| 2149 | | |
| 2150 | | % perform the actual computation: |
| 2151 | | machine_order(Machines,Order) :- |
| 2152 | | machine_dependencies(Machines,Dependencies), |
| 2153 | | topsort(Dependencies,Order). |
| 2154 | | |
| 2155 | | % sort the machines topologically |
| 2156 | | topsort(Deps,Sorted) :- |
| 2157 | | topsort2(Deps,[],Sorted). |
| 2158 | | topsort2([],_,[]) :- !. |
| 2159 | | topsort2(Deps,Known,Sorted) :- |
| 2160 | | split_list(all_deps_known(Known),Deps,DAvailable,DNotAvailable), |
| 2161 | | DAvailable = [_|_], % we have new machines available whose dependencies are all known |
| 2162 | | !, |
| 2163 | | maplist(dep_name,DAvailable,Available), |
| 2164 | | append(Available,Known,NewKnown), |
| 2165 | | append(Available,Rest,Sorted), |
| 2166 | | topsort2(DNotAvailable,NewKnown,Rest). |
| 2167 | | topsort2(Deps,_Known,_) :- |
| 2168 | | member(dep(Name,NameDeps),Deps), |
| 2169 | | add_error(bmachine_construction,'Could not resolve machine dependencies for: ',Name:depends_on(NameDeps)), |
| 2170 | | fail. |
| 2171 | | |
| 2172 | ? | all_deps_known(K,dep(_Name,Deps)) :- sort(Deps,DS),sort(K,KS),subseq0(KS,DS),!. |
| 2173 | | dep_name(dep(Name,_Deps),Name). |
| 2174 | | |
| 2175 | | % find dependencies between machines |
| 2176 | | machine_dependencies(Machines,Dependencies) :- |
| 2177 | | maplist(machine_dependencies2,Machines,Deps), |
| 2178 | | sort(Deps,Dependencies). |
| 2179 | | machine_dependencies2(M,dep(Name,Deps)) :- |
| 2180 | | get_constructed_machine_name_and_body(M,Name,_,Body), |
| 2181 | | findall(Ref, |
| 2182 | | (refines(M,Ref);machine_reference(Body,Ref)), |
| 2183 | | Deps). |
| 2184 | | |
| 2185 | | machine_reference(MachineBody,Ref) :- |
| 2186 | ? | ( member(sees(_,R),MachineBody) |
| 2187 | | ; member(uses(_,R),MachineBody) ), |
| 2188 | ? | member(identifier(_,PrefixRef),R), |
| 2189 | | split_prefix(PrefixRef,_,Ref). |
| 2190 | | machine_reference(MachineBody,Ref) :- |
| 2191 | | ( member(includes(_,R),MachineBody) |
| 2192 | ? | ; member(extends(_,R),MachineBody) |
| 2193 | | ; member(imports(_,R),MachineBody) ), |
| 2194 | ? | member(machine_reference(_,PrefixRef,_),R), |
| 2195 | | split_prefix(PrefixRef,_,Ref). |
| 2196 | | |
| 2197 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 2198 | | % refinements |
| 2199 | | merge_refinement_and_abstraction(Name,Concrete,RefMachines,Result,Ein,Eout) :- |
| 2200 | | memberchk(ref(abstraction,Abstraction),RefMachines), |
| 2201 | | append_sections([sets,concrete_constants,concrete_variables],Abstraction,Concrete,M1), |
| 2202 | | append_if_new(abstract_constants,Abstraction,M1,M2), |
| 2203 | | get_section(properties,Abstraction,AbstractProperties), |
| 2204 | | conjunct_to_section(properties,AbstractProperties,M2,M3), |
| 2205 | | % now get current invariant Invariant and filter out gluing/linking invariant |
| 2206 | | % (the linking invariant talks about variables which no longer exist; hence we cannot check it anymore) |
| 2207 | | select_section(invariant,Invariant,FullConcreteInvariant,M3,M4), |
| 2208 | | write_section(linking_invariant,LinkingInvariant,M4,Merged), |
| 2209 | | % we now also copy from the abstraction those invariants which are still valid |
| 2210 | | get_machine_sorted_variables(Abstraction,SortedAbsVars), |
| 2211 | | get_machine_sorted_variables(Concrete,SortedConcrVars), |
| 2212 | | assert_removed_abs_vars(SortedAbsVars,SortedConcrVars,Name), |
| 2213 | | get_section(invariant,Abstraction,AbstractInvariant), |
| 2214 | | filter_abstract_invariant(AbstractInvariant,SortedConcrVars,AbsInvariantStillValid), |
| 2215 | | filter_linking_invariant(Invariant,LinkingInvariant,ConcreteInvariant), |
| 2216 | | conjunct_predicates([AbsInvariantStillValid,ConcreteInvariant],FullConcreteInvariant), |
| 2217 | | propagate_abstract_operations(Abstraction,Merged,RefMachines,Result,Ein,Eout). |
| 2218 | | merge_refinement_and_abstraction(_,Machine,_,Machine,Errors,Errors). |
| 2219 | | |
| 2220 | | :- use_module(probsrc(bsyntaxtree), [same_id/3]). |
| 2221 | | assert_removed_abs_vars([],_,_). |
| 2222 | | assert_removed_abs_vars([TID1|H],[],Name) :- !, |
| 2223 | | assert_abstract_variable_removed_in(Name,TID1), |
| 2224 | | assert_removed_abs_vars(H,[],Name). |
| 2225 | | assert_removed_abs_vars([TID1|T1],[TID2|T2],Name) :- same_id(TID1,TID2,_),!, |
| 2226 | | assert_removed_abs_vars(T1,T2,Name). |
| 2227 | | assert_removed_abs_vars([TID1|T1],[TID2|T2],Name) :- TID1 @< TID2,!, |
| 2228 | | assert_abstract_variable_removed_in(Name,TID1), |
| 2229 | | assert_removed_abs_vars(T1,[TID2|T2],Name). |
| 2230 | | assert_removed_abs_vars([TID1|T1],[_|T2],Name) :- % TID2 added in Name |
| 2231 | | assert_removed_abs_vars([TID1|T1],T2,Name). |
| 2232 | | |
| 2233 | | |
| 2234 | | assert_abstract_variable_removed_in(Name,TID) :- |
| 2235 | | get_texpr_id(TID,ID), |
| 2236 | | ajoin(['Variable ',ID,' removed in refinement machine: '],Msg), |
| 2237 | | add_debug_message(bmachine_construction,Msg,Name,TID), |
| 2238 | | assertz(abstract_variable_removed_in(ID,Name,TID)). |
| 2239 | | |
| 2240 | | |
| 2241 | | % append sections from abstract machine to concrete machine: |
| 2242 | | append_sections(Sections,AbsMachine,Old,New) :- |
| 2243 | | expand_shortcuts(Sections,AllSections), |
| 2244 | | append_sections2(AllSections,AbsMachine,Old,New). |
| 2245 | | append_sections2([],_,M,M). |
| 2246 | | append_sections2([Section|Rest],AbsMachine,Old,New) :- |
| 2247 | | get_section(Section,AbsMachine,Content), |
| 2248 | | append_to_section3(Section,Content,Old,Inter), |
| 2249 | | append_sections2(Rest,AbsMachine,Inter,New). |
| 2250 | | |
| 2251 | | append_to_section3(Section,Content,Old,Inter) :- section_can_have_duplicates(Section),!, |
| 2252 | | append_to_section_and_remove_dups(Section,Content,Old,Inter). |
| 2253 | | append_to_section3(Section,Content,Old,Inter) :- append_to_section(Section,Content,Old,Inter). |
| 2254 | | |
| 2255 | | :- assert_must_succeed((create_machine(abs,EA), create_machine(conc,EB), |
| 2256 | | write_section(abstract_constants,[b(identifier(x),integer,[some_info])],EA,A), |
| 2257 | | write_section(abstract_constants,[b(identifier(x),integer,[other_info]), |
| 2258 | | b(identifier(y),integer,[info])],EB,B), |
| 2259 | | append_if_new(abstract_constants,A,B,ResultM), |
| 2260 | | get_section(abstract_constants,ResultM,ResultConst), |
| 2261 | | ResultConst==[b(identifier(x),integer,[other_info]), |
| 2262 | | b(identifier(y),integer,[info])] |
| 2263 | | )). |
| 2264 | | |
| 2265 | | append_if_new(Section,Machine,In,Out) :- |
| 2266 | | get_section(Section,Machine,Content), |
| 2267 | | select_section(Section,Old,New,In,Out), |
| 2268 | | get_texpr_ids(Old,ExistingIds), |
| 2269 | | exclude(is_in_existing_ids(ExistingIds),Content,NewElements), |
| 2270 | | append(Old,NewElements,New). |
| 2271 | | is_in_existing_ids(ExistingIds,TId) :- |
| 2272 | | get_texpr_id(TId,Id), |
| 2273 | | memberchk(Id,ExistingIds). |
| 2274 | | |
| 2275 | | % filter linking and concrete invariant |
| 2276 | | filter_linking_invariant(Invariant,Linking,Concrete) :- |
| 2277 | | split_conjuncts(Invariant,Predicates), |
| 2278 | | split_list(contains_abstraction_refs,Predicates,Linkings,Concretes), |
| 2279 | | conjunct_predicates(Linkings,Linking), |
| 2280 | | conjunct_predicates(Concretes,Concrete). |
| 2281 | | |
| 2282 | | |
| 2283 | | % contains_abstraction_refs can be used on predicates of the current machine: the abstraction info field has been computed for this machine |
| 2284 | | contains_abstraction_refs(TExpr) :- |
| 2285 | | syntaxtraversion(TExpr,_,_,Infos,Subs,_), |
| 2286 | | ( memberchk(abstraction,Infos) % This info field comes from the last argument of visibility/6 |
| 2287 | | -> true |
| 2288 | | ; member(Sub,Subs), |
| 2289 | | contains_abstraction_refs(Sub)). |
| 2290 | | |
| 2291 | | % Determine which part of the abstract invariant can be imported into the refinement machine |
| 2292 | | % TODO: should this be applied to WHILE loop INVARIANTS? |
| 2293 | | filter_abstract_invariant(AbsInvariant,SortedConcrVars,ConcreteInv) :- |
| 2294 | | split_conjuncts(AbsInvariant,Predicates), |
| 2295 | | filter_abs_invs(Predicates,SortedConcrVars,Concretes), |
| 2296 | | conjunct_predicates(Concretes,ConcreteInv). %, print('COPY: '), translate:print_bexpr(Concrete),nl. |
| 2297 | | :- use_module(translate,[translate_bexpression/2]). |
| 2298 | | |
| 2299 | | filter_abs_invs([],_,[]). |
| 2300 | | filter_abs_invs([TExpr|TInv],SortedConcrVars,Res) :- |
| 2301 | | contains_abstract_variables2(SortedConcrVars,TExpr,Cause),!, |
| 2302 | | (silent_mode(on) -> true |
| 2303 | | ; translate_bexpression(Cause,ID), |
| 2304 | | ajoin(['Discarding abstract INVARIANT (requires variable `',ID,'`): '],Msg), |
| 2305 | | add_message(bmachine_construction,Msg,TExpr,Cause) |
| 2306 | | ), |
| 2307 | | (adapt_invariant(SortedConcrVars,TExpr,NewTExpr) |
| 2308 | | -> Res = [NewTExpr|TRes], |
| 2309 | | add_message(bmachine_construction,'Replaced abstract INVARIANT by: ',NewTExpr,Cause) |
| 2310 | | ; Res=TRes |
| 2311 | | ), |
| 2312 | | filter_abs_invs(TInv,SortedConcrVars,TRes). |
| 2313 | | filter_abs_invs([TExpr|TInv],SortedConcrVars,[TExpr|TRes]) :- |
| 2314 | | filter_abs_invs(TInv,SortedConcrVars,TRes). |
| 2315 | | |
| 2316 | | contains_abstract_variables2(SortedConcrVars,TExpr,Cause) :- |
| 2317 | | syntaxtraversion(TExpr,Expr,Type,Infos,Subs,_), |
| 2318 | | ( memberchk(loc(_,_Mch,abstract_variables),Infos) % are there other things that pose problems: abstract_constants ? |
| 2319 | | -> %print('Abs: '),translate:print_bexpr(TExpr),nl, print(SortedConcrVars),nl, |
| 2320 | | Cause=TExpr, |
| 2321 | | \+ ord_member_nonvar_chk(b(Expr,Type,_),SortedConcrVars) % otherwise variable is re-introduced with same type |
| 2322 | | % in some Event-B models: VARIABLES keyword is used and in refinement VARIABLES are re-listed |
| 2323 | | % TO DO: check what happens when variable not immediately re-introduced |
| 2324 | | ; member(Sub,Subs), |
| 2325 | | contains_abstract_variables2(SortedConcrVars,Sub,Cause) |
| 2326 | | ). |
| 2327 | | |
| 2328 | | % try and keep part of invariant, e.g., if f:ABS-->Ran translate to f: TYPE +-> Ran |
| 2329 | | adapt_invariant(SortedConcrVars,b(member(LHS,RHS),pred,I),b(member(LHS,NewRHS),pred,I)) :- |
| 2330 | | \+ contains_abstract_variables2(SortedConcrVars,LHS,_), |
| 2331 | | adapt_to_concrete_superset(RHS,SortedConcrVars,NewRHS), |
| 2332 | | \+ get_texpr_expr(NewRHS,typeset). % not really useful |
| 2333 | | |
| 2334 | | adapt_to_concrete_superset(b(E,Type,Info),SortedConcrVars,b(NewE,Type,Info)) :- |
| 2335 | | adapt_super2(E,SortedConcrVars,NewE). % TODO: adapt info fields? |
| 2336 | | adapt_to_concrete_superset(b(_E,Type,_Info),_SortedConcrVars,b(typeset,Type,[])). |
| 2337 | | % Range of function remains concrete, Domain is abstract and no longer available: |
| 2338 | | adapt_super2(PFUN,SortedConcrVars,partial_function(NewDom,RAN)) :- |
| 2339 | | is_fun(PFUN,partial,DOM,RAN), |
| 2340 | | \+ contains_abstract_variables2(SortedConcrVars,RAN,_), |
| 2341 | | adapt_to_concrete_superset(DOM,SortedConcrVars,NewDom). |
| 2342 | | adapt_super2(TFUN,SortedConcrVars,partial_function(NewDom,RAN)) :- |
| 2343 | | is_fun(TFUN,total,DOM,RAN), |
| 2344 | | \+ contains_abstract_variables2(SortedConcrVars,RAN,_), |
| 2345 | | adapt_to_concrete_superset(DOM,SortedConcrVars,NewDom). |
| 2346 | | % Domain of function remains concrete, Range is abstract and no longer available: |
| 2347 | | adapt_super2(PFUN,SortedConcrVars,partial_function(DOM,NewRan)) :- |
| 2348 | | is_fun(PFUN,partial,DOM,RAN), |
| 2349 | | \+ contains_abstract_variables2(SortedConcrVars,DOM,_), |
| 2350 | | adapt_to_concrete_superset(RAN,SortedConcrVars,NewRan). |
| 2351 | | adapt_super2(TFUN,SortedConcrVars,total_function(DOM,NewRan)) :- |
| 2352 | | is_fun(TFUN,total,DOM,RAN), |
| 2353 | | \+ contains_abstract_variables2(SortedConcrVars,DOM,_), |
| 2354 | | adapt_to_concrete_superset(RAN,SortedConcrVars,NewRan). |
| 2355 | | adapt_super2(FUN,SortedConcrVars,partial_function(NewDom,NewRan)) :- |
| 2356 | | is_fun(FUN,_,DOM,RAN), |
| 2357 | | adapt_to_concrete_superset(DOM,SortedConcrVars,NewDom), |
| 2358 | | adapt_to_concrete_superset(RAN,SortedConcrVars,NewRan). |
| 2359 | | % TODO: more cases, intersection(ABS,CONCR) -> CONCR, cartesian_product |
| 2360 | | |
| 2361 | | is_fun(partial_function(DOM,RAN),partial,DOM,RAN). |
| 2362 | | is_fun(partial_injection(DOM,RAN),partial,DOM,RAN). |
| 2363 | | is_fun(partial_surjection(DOM,RAN),partial,DOM,RAN). |
| 2364 | | is_fun(partial_bijection(DOM,RAN),partial,DOM,RAN). |
| 2365 | | is_fun(total_function(DOM,RAN),total,DOM,RAN). |
| 2366 | | is_fun(total_injection(DOM,RAN),total,DOM,RAN). |
| 2367 | | is_fun(total_surjection(DOM,RAN),total,DOM,RAN). |
| 2368 | | is_fun(total_bijection(DOM,RAN),total,DOM,RAN). |
| 2369 | | |
| 2370 | | % --------------------- |
| 2371 | | |
| 2372 | | get_machine_sorted_variables(Machine,SortedAllVars) :- |
| 2373 | | get_section(abstract_variables,Machine,AbsVars), |
| 2374 | | get_section(concrete_variables,Machine,ConcVars), |
| 2375 | | append(ConcVars,AbsVars,AllVars), |
| 2376 | | sort(AllVars,SortedAllVars). |
| 2377 | | |
| 2378 | | split_conjuncts(Expr,List) :- |
| 2379 | | split_conjuncts2(Expr,List,[]). |
| 2380 | | split_conjuncts2(Expr) --> |
| 2381 | | {get_texpr_expr(Expr,conjunct(A,B)),!}, |
| 2382 | | split_conjuncts2(A), |
| 2383 | | split_conjuncts2(B). |
| 2384 | | split_conjuncts2(Expr) --> [Expr]. |
| 2385 | | |
| 2386 | | % copy the abstract operations or re-use their preconditions |
| 2387 | | % TODO: think about copying Initialisation? |
| 2388 | | propagate_abstract_operations(Abstract,Concrete,RefMachines,Result,Ein,Eout) :- |
| 2389 | | get_section(promoted,Abstract,APromoted), |
| 2390 | | get_section(operation_bodies,Abstract,ABodies), |
| 2391 | | % signature: select_section(SecName,OldContent,NewContent,OldMachine,NewMachine) |
| 2392 | | select_section(promoted,CPromotedIn,CPromotedOut,Concrete,Concrete2), |
| 2393 | | select_section(operation_bodies,CBodiesIn,CBodiesOut,Concrete2,Result), |
| 2394 | | propagate_aops(APromoted,ABodies,RefMachines,CPromotedIn,CBodiesIn,CPromotedOut,CBodiesOut,Ein,Eout). |
| 2395 | | propagate_aops([],_ABodies,_RefMachines,CPromoted,CBodies,CPromoted,CBodies,Errors,Errors). |
| 2396 | | propagate_aops([APromoted|ApRest],ABodies,RefMachines,CPromotedIn,CBodiesIn,CPromotedOut,CBodiesOut,Ein,Eout) :- |
| 2397 | | get_operation(APromoted,ABodies,AbstractOp), |
| 2398 | | def_get_texpr_id(APromoted,op(APromotedOpName)), |
| 2399 | | copy_texpr_wo_info(APromoted,CProm), |
| 2400 | | ( member(CProm,CPromotedIn) -> |
| 2401 | | debug_format(19,'Refining promoted abstract operation ~w to refinement machine.~n',[APromotedOpName]), |
| 2402 | | extract_concrete_preconditions(AbstractOp,RefMachines,Pre), |
| 2403 | | change_operation(APromoted,ConcreteOpOld,ConcreteOpNew,CBodiesIn,CBodiesRest), |
| 2404 | | add_precondition(Pre,ConcreteOpOld,ConcreteOpNew), % propagate PRE down to concrete operation |
| 2405 | | CPromotedIn = CPromotedRest, |
| 2406 | | Ein = E1 |
| 2407 | | % TO DO: do not copy if event is refined at least once with renaming ! |
| 2408 | | ; is_refined_by_some_event(APromotedOpName,CPromotedIn,ConcreteOpName) -> |
| 2409 | | debug_format(19,'Not copying abstract operation ~w to refinement machine, as it is refined by ~w.~n',[APromotedOpName,ConcreteOpName]), |
| 2410 | | CPromotedRest=CPromotedIn, CBodiesRest=CBodiesIn, |
| 2411 | | E1=Ein |
| 2412 | | ; |
| 2413 | | debug_format(19,'Copying abstract operation ~w to refinement machine, as it is not refined.~n',[APromotedOpName]), |
| 2414 | | % TO DO: check that this is also the right thing to do for Atelier-B Event-B |
| 2415 | | % TO DO: check that the variables are also still there |
| 2416 | | check_copied_operation(APromoted,AbstractOp,RefMachines,Ein,E1), |
| 2417 | | append(CPromotedIn,[APromoted],CPromotedRest), |
| 2418 | | append(CBodiesIn,[AbstractOp],CBodiesRest) |
| 2419 | | ), |
| 2420 | | propagate_aops(ApRest,ABodies,RefMachines,CPromotedRest,CBodiesRest,CPromotedOut,CBodiesOut,E1,Eout). |
| 2421 | | |
| 2422 | | is_refined_by_some_event(AbstractName,CPromotedList,ConcreteName) :- |
| 2423 | | member(TID,CPromotedList), |
| 2424 | | get_texpr_info(TID,Infos), |
| 2425 | | memberchk(refines_operation(AbstractName),Infos), |
| 2426 | | def_get_texpr_id(TID,ConcreteName). |
| 2427 | | |
| 2428 | | get_operation(TId,Bodies,Operation) :- |
| 2429 | | select_operation(TId,Bodies,Operation,_BodiesRest). |
| 2430 | | change_operation(TId,OldOp,NewOp,OldBodies,[NewOp|NewBodies]) :- |
| 2431 | | select_operation(TId,OldBodies,OldOp,NewBodies). |
| 2432 | | select_operation(TId,Bodies,Operation,BodiesRest) :- |
| 2433 | | copy_texpr_wo_info(TId,OpId), |
| 2434 | | get_texpr_expr(Operation,operation(OpId,_,_,_)), |
| 2435 | | select(Operation,Bodies,BodiesRest),!. |
| 2436 | | |
| 2437 | | extract_concrete_preconditions(Op,RefMachines,FPre) :- |
| 2438 | | extract_preconditions_op(Op,Pre), |
| 2439 | | extract_op_arguments(Op,Args), |
| 2440 | | conjunction_to_list(Pre,Pres), |
| 2441 | | % todo: check the "machine" parameter |
| 2442 | | visible_env(machine,operation_bodies,RefMachines,Env1,_Errors,[]), |
| 2443 | | store_variables(Args,Env1,Env), |
| 2444 | | filter_predicates_with_unknown_identifiers(Pres,Env,FPres), |
| 2445 | | conjunct_predicates(FPres,FPre). |
| 2446 | | |
| 2447 | | extract_op_arguments(Op,Params) :- |
| 2448 | | get_texpr_expr(Op,operation(_,_,Params,_)). |
| 2449 | | |
| 2450 | | extract_preconditions_op(OpExpr,Pre) :- |
| 2451 | | get_texpr_expr(OpExpr,operation(_,_,_,Subst)), |
| 2452 | | extract_preconditions(Subst,Pres,_), |
| 2453 | | conjunct_predicates(Pres,Pre). |
| 2454 | | extract_preconditions(TExpr,Pres,Inner) :- |
| 2455 | | get_texpr_expr(TExpr,Expr), |
| 2456 | | extract_preconditions2(Expr,TExpr,Pres,Inner). |
| 2457 | | extract_preconditions2(precondition(Pre,Subst),_,[Pre|Pres],Inner) :- !, |
| 2458 | | extract_preconditions(Subst,Pres,Inner). |
| 2459 | | extract_preconditions2(block(Subst),_,Pres,Inner) :- !, |
| 2460 | | extract_preconditions(Subst,Pres,Inner). |
| 2461 | | extract_preconditions2(_,Inner,[],Inner). |
| 2462 | | |
| 2463 | | :- use_module(btypechecker,[prime_atom0/2]). |
| 2464 | | filter_predicates_with_unknown_identifiers([],_Env,[]). |
| 2465 | | filter_predicates_with_unknown_identifiers([Pred|Prest],Env,Result) :- |
| 2466 | | ( find_unknown_identifier(Pred,Env,_Id) -> |
| 2467 | | !,Result = Rrest |
| 2468 | | ; |
| 2469 | | Result = [Pred|Rrest]), |
| 2470 | | filter_predicates_with_unknown_identifiers(Prest,Env,Rrest). |
| 2471 | | find_unknown_identifier(Pred,Env,Id) :- |
| 2472 | | get_texpr_id(Pred,Id),!, |
| 2473 | | \+ env_lookup_type(Id,Env,_), |
| 2474 | | (atom(Id),prime_atom0(UnprimedId,Id) |
| 2475 | | -> % we have an identifier with $0 at end |
| 2476 | | \+ env_lookup_type(UnprimedId,Env,_) % check unprimed identifier also unknown |
| 2477 | | ; true). |
| 2478 | | find_unknown_identifier(Pred,Env,Id) :- |
| 2479 | | syntaxtraversion(Pred,_,_,_,Subs,Names), |
| 2480 | | store_variables(Names,Env,Subenv), |
| 2481 | | find_unknown_identifier_l(Subs,Subenv,Id). |
| 2482 | | find_unknown_identifier_l([S|_],Env,Id) :- |
| 2483 | | find_unknown_identifier(S,Env,Id),!. |
| 2484 | | find_unknown_identifier_l([_|Rest],Env,Id) :- |
| 2485 | | find_unknown_identifier_l(Rest,Env,Id). |
| 2486 | | |
| 2487 | | :- use_module(library(ordsets),[ord_union/3]). |
| 2488 | | % we add a precondition to an existing operation |
| 2489 | | % Note: we need to update the reads info computed by the type checker (compute_accessed_vars_infos_for_operation) |
| 2490 | | add_precondition(b(truth,_,_),Old,New) :- !, Old=New. |
| 2491 | | add_precondition(Pre,b(Old,T,I),b(New,T,I2)) :- |
| 2492 | | Old=operation(Id,Res,Params,Subst), |
| 2493 | | New=operation(Id,Res,Params,NewSubst), |
| 2494 | | extract_preconditions(Subst,OldPres,Inner), |
| 2495 | | conjunct_predicates([Pre|OldPres],NewPre), |
| 2496 | | create_texpr(precondition(NewPre,Inner),subst,[],NewSubst), |
| 2497 | | (select(reads(OldReads),I,I1) % we do not have to update modifies(.), non_det_modifies(.), reads_locals(.),... |
| 2498 | | -> I2=[reads(NewReads)|I1], |
| 2499 | | get_texpr_ids(Params,Ignore), |
| 2500 | | find_identifier_uses(Pre,Ignore,PreUsedIds), |
| 2501 | | ord_union(PreUsedIds,OldReads,NewReads) |
| 2502 | | ; add_internal_error('No reads info for operation: ',add_precondition(Pre,b(Old,T,I),b(New,T,I2))), |
| 2503 | | I2=I). |
| 2504 | | |
| 2505 | | |
| 2506 | | |
| 2507 | | check_copied_operation(OpRef,Op,RefMachines,Ein,Eout) :- |
| 2508 | | % todo: check the "refinement" parameter |
| 2509 | | visible_env(refinement,operation_bodies,RefMachines,Env1,_Errors,[]), |
| 2510 | | get_texpr_id(OpRef,OpId),get_texpr_type(OpRef,OpType), |
| 2511 | | env_store(OpId,OpType,[],Env1,Env), |
| 2512 | | findall(U, find_unknown_identifier(Op,Env,U), Unknown1), |
| 2513 | | ( Unknown1=[] -> Ein=Eout |
| 2514 | | ; |
| 2515 | | sort(Unknown1,Unknown), |
| 2516 | | op(OpName) = OpId, |
| 2517 | | join_ids(Unknown,IdList), |
| 2518 | | (Unknown = [_] -> Plural=[]; Plural=['s']), |
| 2519 | | append([['Operation ',OpName, |
| 2520 | | ' was copied from abstract machine but the identifier'], |
| 2521 | | Plural, |
| 2522 | | [' '], |
| 2523 | | IdList, |
| 2524 | | [' cannot be seen anymore']],Msgs), |
| 2525 | | ajoin(Msgs,Msg), Ein = [error(Msg,none)|Eout] |
| 2526 | | ). |
| 2527 | | join_ids([I],[Msg]) :- !,opname(I,Msg). |
| 2528 | | join_ids([A|Rest],[Msg,','|Mrest]) :- opname(A,Msg),join_ids(Rest,Mrest). |
| 2529 | | opname(op(Id),Id) :- !. |
| 2530 | | opname(Id,Id). |
| 2531 | | |
| 2532 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 2533 | | % split an identifier into a (possible empty) prefix and the name itself |
| 2534 | | % e.g. split_prefix('path.to.machine', 'path.to', 'machine'). |
| 2535 | | split_prefix(Term,Prefix,Main) :- |
| 2536 | | one_arg_term(Functor,Arg,Term),!, |
| 2537 | | one_arg_term(Functor,MArg,Main), |
| 2538 | | split_prefix(Arg,Prefix,MArg). |
| 2539 | | split_prefix(PR,Prefix,Main) :- |
| 2540 | | safe_atom_chars(PR,Chars,split_prefix1), |
| 2541 | | split_prefix2(Chars,Chars,[],CPrefix,CMain), |
| 2542 | | safe_atom_chars(Main,CMain,split_prefix2), |
| 2543 | | safe_atom_chars(Prefix,CPrefix,split_prefix3). |
| 2544 | | split_prefix2([],Main,_,[],Main). |
| 2545 | | split_prefix2([C|Rest],Previous,PrefBefore,Prefix,Main) :- |
| 2546 | | ( C='.' -> |
| 2547 | | append(PrefBefore,RestPrefix,Prefix), |
| 2548 | | split_prefix2(Rest,Rest,[C],RestPrefix,Main) |
| 2549 | | ; |
| 2550 | | append(PrefBefore,[C],NextPref), |
| 2551 | | split_prefix2(Rest,Previous,NextPref,Prefix,Main)). |
| 2552 | | |
| 2553 | | rawmachine_section(Elem,List,Result) :- |
| 2554 | | rawmachine_section_with_opt_desc(Elem,List,Result,_,_). |
| 2555 | | |
| 2556 | | |
| 2557 | | rawmachine_section_with_opt_desc(Elem,List,Result,Desc,Pos) :- section_can_have_description_pragma(Elem), |
| 2558 | | functor(Pattern,Elem,2), |
| 2559 | | arg(2,Pattern,Result), |
| 2560 | | select(description_machine_clause(Pos,DescText,Pattern),List,_),!, |
| 2561 | | (DescText = description_text(_Pos,Desc) -> true ; Desc='?illegal_desc?'). |
| 2562 | | rawmachine_section_with_opt_desc(Elem,List,Result,'',unknown) :- |
| 2563 | | functor(Pattern,Elem,2), |
| 2564 | | arg(2,Pattern,Result), |
| 2565 | ? | select(Pattern,List,Rest),!, |
| 2566 | | (functor(Pattern2,Elem,2),member(Pattern2,Rest) |
| 2567 | | -> arg(1,Pattern2,Pos), |
| 2568 | | add_error(bmachine_construction,'Multiple sections for: ',Elem,Pos) |
| 2569 | | ; true). |
| 2570 | | |
| 2571 | | |
| 2572 | | section_can_have_description_pragma(initialisation). |
| 2573 | | |
| 2574 | | optional_rawmachine_section(Elem,List,Default,Result) :- |
| 2575 | | ( rawmachine_section(Elem,List,Result1) -> Result=Result1 |
| 2576 | | ; Result=Default). |
| 2577 | | |
| 2578 | | |
| 2579 | | one_arg_term(Functor,Arg,Term) :- %print(one_arg_term(Functor,Arg,Term)),nl, |
| 2580 | | functor(Term,Functor,1),arg(1,Term,Arg). |
| 2581 | | |
| 2582 | | % check if a rawmachine section list has a given section |
| 2583 | | rawmachine_section_exists(Elem,List) :- % |
| 2584 | | functor(Pattern,Elem,2), |
| 2585 | ? | (member(Pattern,List) -> true). |
| 2586 | | |
| 2587 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 2588 | | % visibility rules |
| 2589 | | |
| 2590 | | % the visibility/5 predicate declares what a part of a machine can see |
| 2591 | | % visibility(MType, Scope, Section, Access, Info) means: |
| 2592 | | % In a machine of type MType (machine, refinement, implementation), |
| 2593 | | % an expression in a Section (like invariant) can see |
| 2594 | | % the identifiers in the Access sections. Access is a list of |
| 2595 | | % sections, where shortcuts are allowed (see shortcut/2, e.g., shortcut(operations,[unpromoted,promoted]).). |
| 2596 | | % Scope defines where (in relation to the Section) |
| 2597 | | % the section in Access are (local: same machine, included: in an |
| 2598 | | % included machine, etc.) |
| 2599 | | % Info is a list of additional information that is added to each |
| 2600 | | % identifier in the environment to build up. E.g. in an operation |
| 2601 | | % definition, constants are marked readonly. |
| 2602 | | visibility(machine, local, constraints, [parameters],[]). |
| 2603 | | visibility(machine, local, includes, [parameters,sets,constants],[]). |
| 2604 | | visibility(machine, local, properties, [sets,constants],[]). |
| 2605 | | visibility(machine, local, invariant, [parameters,sets,constants,variables],[]). |
| 2606 | | visibility(machine, local, operation_bodies, [parameters,sets,constants],[readonly]). |
| 2607 | | visibility(machine, local, operation_bodies, [operations],Info) :- Info =[readonly,dontcall]. |
| 2608 | | % an operation to be readonly: means we cannot assign to it; but the operation itself can change variables |
| 2609 | | % for allow_operation_calls_in_expr=true we check that operation is inquiry in type checker |
| 2610 | | % (get_preference(allow_operation_calls_in_expr,true) -> Info = [inquiry] |
| 2611 | | % ; Info =[readonly,dontcall] ). % we check in btype(operation_call_in_expr) |
| 2612 | | visibility(machine, local, operation_bodies, [variables],[]). |
| 2613 | ? | visibility(machine, local, initialisation, Access,[not_initialised|Info]) :- visibility(machine,local,operation_bodies,Access,Info). |
| 2614 | | |
| 2615 | | visibility(machine, Scope, assertions, [Allow],[inquiry|DC]) :- |
| 2616 | | (Scope = local -> Allow=operations, DC=[dontcall] ; Allow=promoted, DC=[]), |
| 2617 | | get_preference(allow_operation_calls_in_expr,true). % if we allow calling operations in expressions |
| 2618 | | visibility(machine, Scope, invariant, [promoted],[inquiry]) :- |
| 2619 | | Scope \= local, % do not allow calling local operations in invariant; their correctness relies on the invariant |
| 2620 | | get_preference(allow_operation_calls_in_expr,true). |
| 2621 | | |
| 2622 | | visibility(machine, included, properties, [sets,constants],[]). |
| 2623 | | visibility(machine, included, invariant, [sets,constants,variables],[]). |
| 2624 | | visibility(machine, included, operation_bodies, [sets,constants,variables],[readonly]). |
| 2625 | | visibility(machine, included, operation_bodies, [promoted],Info) :- Info = [readonly]. |
| 2626 | | % for allow_operation_calls_in_expr=true we check that operation is inquiry in type checker |
| 2627 | | % (get_preference(allow_operation_calls_in_expr,true) -> Info = [inquiry] ; Info=[readonly]). |
| 2628 | | %visibility(machine, included, initialisation, [sets,constants,variables,promoted],[readonly]). |
| 2629 | | visibility(machine, included, initialisation, [sets,constants,promoted],[readonly]). |
| 2630 | | visibility(machine, included, initialisation, [variables],Info) :- |
| 2631 | | (get_preference(allow_overriding_initialisation,true) |
| 2632 | | -> Info = [] % allow overriding INITIALISATION / making it more concrete |
| 2633 | | ; Info = [readonly]). % default Atelier-B semantics |
| 2634 | | |
| 2635 | | visibility(machine, used, properties, [sets,constants],[]). |
| 2636 | | visibility(machine, used, invariant, [parameters,sets,constants,variables],[]). |
| 2637 | | visibility(machine, used, operation_bodies, [parameters,sets,constants,variables],[readonly]). |
| 2638 | | visibility(machine, used, initialisation, [parameters,sets,constants,variables],[readonly]). |
| 2639 | | visibility(machine, used, operation_bodies, [operations],[inquiry]) :- |
| 2640 | | get_preference(allow_operation_calls_for_uses,true). %% added by leuschel, allowed in Schneider Book |
| 2641 | | % but not allowed by Atelier-B; see test 2135 |
| 2642 | | |
| 2643 | | visibility(machine, seen, includes, [sets,constants],[]). |
| 2644 | | visibility(machine, seen, properties, [sets,constants],[]). |
| 2645 | | visibility(machine, seen, invariant, [sets,constants],[]). |
| 2646 | | visibility(machine, seen, operation_bodies, [sets,constants,variables],[readonly]). |
| 2647 | | visibility(machine, seen, initialisation, [sets,constants,variables],[readonly]). |
| 2648 | | visibility(machine, seen, operation_bodies, [operations],[inquiry]). %% added by leuschel, allow query operation |
| 2649 | | |
| 2650 | | visibility(refinement, local, Section, Access, Info) :- |
| 2651 | | Section \= assertions, % assertions are handled below |
| 2652 | | visibility(machine, local, Section, Access, Info). |
| 2653 | | |
| 2654 | | visibility(refinement, abstraction, includes, [sets,concrete_constants],[]). |
| 2655 | | visibility(refinement, abstraction, properties, [sets,constants],[]). |
| 2656 | | visibility(refinement, abstraction, invariant, [sets,constants,concrete_variables],[]). |
| 2657 | | visibility(refinement, abstraction, invariant, [abstract_variables],[abstraction]). |
| 2658 | | visibility(refinement, abstraction, operation_bodies, [sets,concrete_constants],[readonly]). |
| 2659 | | visibility(refinement, abstraction, operation_bodies, [concrete_variables],[]). |
| 2660 | | |
| 2661 | | visibility(refinement, included, properties, [sets,constants],[]). |
| 2662 | | visibility(refinement, included, invariant, [sets,constants,variables],[]). |
| 2663 | | visibility(refinement, included, operation_bodies, [sets,constants,variables,promoted],[re]). % What is re ??? TO DO: investigate |
| 2664 | | |
| 2665 | | visibility(refinement, seen, includes, [sets,constants],[]). |
| 2666 | | visibility(refinement, seen, properties, [sets,constants],[]). |
| 2667 | | visibility(refinement, seen, invariant, [sets,constants],[]). |
| 2668 | | visibility(refinement, seen, operation_bodies, [sets,constants,variables],[readonly]). |
| 2669 | | visibility(refinement, seen, operation_bodies, [operations],[inquiry]). |
| 2670 | | |
| 2671 | | visibility(refinement, Ref, initialisation, Access, [not_initialised|Info]) :- |
| 2672 | | visibility(refinement,Ref,operation_bodies,Access,Info). |
| 2673 | | |
| 2674 | | % assertions have same visibility as invariant |
| 2675 | | visibility(MType, Ref, assertions, Part, Access) :- |
| 2676 | ? | visibility(MType,Ref,invariant,Part,Access). |
| 2677 | | |
| 2678 | | visibility(implementation, Ref, Section, Part, Access) :- |
| 2679 | | visibility(refinement, Ref, Section, Part, Access). |
| 2680 | | visibility(implementation, local, values_expression, [concrete_constants,sets],[]). % seems to have no effect (yet); see ArrayValuationAImp |
| 2681 | | visibility(implementation, included, values_expression, [concrete_constants,sets],[]). |
| 2682 | | visibility(implementation, seen, values_expression, [concrete_constants,sets],[]). |
| 2683 | | visibility(implementation, abstraction,values_expression, [concrete_constants,sets],[]). |
| 2684 | | |
| 2685 | | % For predicates over pre- and post-states |
| 2686 | | visibility(MType, Rev, prepost, Access, Info) :- |
| 2687 | ? | visibility(MType, Rev, invariant, Access, Info). |
| 2688 | | visibility(MType, Rev, prepost, Access, [primed,poststate|Info]) :- |
| 2689 | ? | visibility(MType, Rev, invariant, Access, Info). |
| 2690 | | |
| 2691 | | % add error messages for some common mistakes (access to parameters in the properties) |
| 2692 | | visibility(machine, local, properties, [parameters], [error('a parameter cannot be accessed in the PROPERTIES section')]). |
| 2693 | | % the following rule should be helpful for the user, but additionally it also |
| 2694 | | % provides a mechanism to re-introduce abstract variables in the INVARIANT |
| 2695 | | % section of a while loop (to enable this, an identifier is also marked with "abstraction") |
| 2696 | | % in the predicate allow_access_to_abstract_var |
| 2697 | | visibility(refinement, abstraction, operation_bodies, [abstract_variables], |
| 2698 | | [error('illegal access to an abstract variable in an operation'),abstraction]). |
| 2699 | | visibility(refinement, abstraction, operation_bodies, [abstract_constants], |
| 2700 | | [error('illegal access to an abstract constant in an operation (only allowed in WHILE INVARIANT or ASSERT)'),abstraction]). |
| 2701 | | |
| 2702 | | |
| 2703 | | % lookups up all identifier sections that are accessible from |
| 2704 | | % the given section, removes all shortcuts and removes |
| 2705 | | % duplicate entries |
| 2706 | | % |
| 2707 | | % Returns a list of vis(Section,Info) where Section is the |
| 2708 | | % identifier section that can be seen with Info as a list |
| 2709 | | % of additional information |
| 2710 | | expanded_visibility(MType, Ref, Part, Access) :- |
| 2711 | | findall(vis(Section,Infos), |
| 2712 | | ( visibility(MType,Ref,Part,Sections1,Infos), |
| 2713 | | expand_shortcuts(Sections1,Sections), |
| 2714 | | member(Section,Sections)), |
| 2715 | | Access1), |
| 2716 | | sort(Access1,Access). |
| 2717 | | %format('MType=~w, Ref=~w, Part=~w~n Vis=~w~n',[MType,Ref,Part,Access]). |
| 2718 | | |
| 2719 | | % visible_env/6 creates a type environment for a certain |
| 2720 | | % part of a machine by looking up which identifier should |
| 2721 | | % be visible from there and what additional information should |
| 2722 | | % be added (e.g. to restrict access to read-only) |
| 2723 | | % |
| 2724 | | % The visibility/6 facts are used to define which identifier are visible |
| 2725 | | % |
| 2726 | | % MType: machine type (machine, refinement, ...) |
| 2727 | | % Part: part of the machine for which the environment should be created |
| 2728 | | % RefMachines: referred machines that are already typed |
| 2729 | | % Env: The created environment |
| 2730 | | % Errors: errors might be added if multiple variables with the same identifier |
| 2731 | | % are declared |
| 2732 | | visible_env(MType, Part, RefMachines, Env, Err_in, Err_out) :- |
| 2733 | | env_empty(Init), |
| 2734 | | visible_env(MType, Part, RefMachines, Init, Env, Err_in, Err_out). |
| 2735 | | % visible_env/7 is like visible_env/6, but an initial environment |
| 2736 | | % can be given in "In" |
| 2737 | | visible_env(MType, Part, RefMachines, In, Out, Err_in, Err_out) :- |
| 2738 | | foldl(visible_env2(MType,Part),RefMachines,In/Err_in,Out/Err_out). |
| 2739 | | visible_env2(MType,Part,extended_local_ref(Machine),InEnvErr,OutEnvErr) :- !, |
| 2740 | | Scope=local, |
| 2741 | | get_machine_name(Machine,MName), |
| 2742 | | %format('adding identifiers from machine ~w for scope ~w~n',[MName,Scope]), |
| 2743 | | get_section(definitions,Machine,Defs), |
| 2744 | | foldl(env_add_def(MName),Defs,InEnvErr,InEnvErr2), |
| 2745 | | (bmachine:additional_configuration_machine(_MchName,AddMachine), |
| 2746 | | get_section(definitions,AddMachine,AdditionalDefs) |
| 2747 | | -> foldl(env_add_def(MName),AdditionalDefs,InEnvErr2,InterEnvErr) |
| 2748 | | ; InterEnvErr = InEnvErr2 |
| 2749 | | ), |
| 2750 | | expanded_visibility(MType, Scope, Part, Access), |
| 2751 | | foldl(create_vis_env(Scope,MName,Machine),Access,InterEnvErr,OutEnvErr). |
| 2752 | | visible_env2(MType,Part,ref(Scope,Machine),InEnvErr,OutEnvErr) :- |
| 2753 | | get_machine_name(Machine,MName), |
| 2754 | | %format('adding identifiers from machine ~w for scope ~w~n',[MName,Scope]), |
| 2755 | | ( Scope == local -> |
| 2756 | | get_section(definitions,Machine,Defs), |
| 2757 | | %nl,print(adding_defs(Defs)),nl,nl, |
| 2758 | | foldl(env_add_def(MName),Defs,InEnvErr,InterEnvErr) |
| 2759 | | ; |
| 2760 | | InEnvErr=InterEnvErr), |
| 2761 | | expanded_visibility(MType, Scope, Part, Access), |
| 2762 | | foldl(create_vis_env(Scope,MName,Machine),Access,InterEnvErr,OutEnvErr). |
| 2763 | | env_add_def(MName,definition_decl(Name,PType,Pos,Params,Body,_Deps),InEnvErr,OutEnvErr) :- |
| 2764 | | Type = definition(PType,Params,Body), |
| 2765 | | Info = [nodeid(Pos),loc(local,MName,definitions)], |
| 2766 | | create_texpr(identifier(Name),Type,Info,TExpr), |
| 2767 | | add_unique_variable(TExpr,InEnvErr,OutEnvErr),!. |
| 2768 | | env_add_def(MName,Def,EnvErr,EnvErr) :- |
| 2769 | | add_internal_error('Cannot deal with DEFINITION: ',env_add_def(MName,Def)). |
| 2770 | | |
| 2771 | | create_vis_env(Scope,MName,IDS,vis(Section,Infos),InEnvErr,OutEnvErr) :- |
| 2772 | | get_section(Section,IDS,Identifiers1), |
| 2773 | | % get_texpr_ids(Identifiers1,II),format('Got identifiers for ~w:~w = ~w~n',[MName,Section,II]), |
| 2774 | | (Section=freetypes |
| 2775 | | -> generate_free_type_ids(Identifiers1,Identifiers2) |
| 2776 | | ; Identifiers2=Identifiers1), |
| 2777 | | maplist(add_infos_to_identifier([loc(Scope,MName,Section)|Infos]),Identifiers2,Identifiers), |
| 2778 | | l_add_unique_variables(Identifiers,InEnvErr,OutEnvErr). |
| 2779 | | |
| 2780 | | % optimized version of foldl(add_unique_variable,Identifiers,InEnvErr,OutEnvErr). |
| 2781 | | l_add_unique_variables([],Env,Env). |
| 2782 | | l_add_unique_variables([ID|T],InEnvErr,OutEnvErr) :- |
| 2783 | | add_unique_variable(ID,InEnvErr,IntEnv), |
| 2784 | | l_add_unique_variables(T,IntEnv,OutEnvErr). |
| 2785 | | |
| 2786 | | % freetypes: generate IDs for Z freetype section |
| 2787 | | % The classical B FREETYPE section is dealt with in another place (TODO: unify this) |
| 2788 | | generate_free_type_ids([freetype(FTypeId,Cases)|T],[b(identifier(FTypeId),set(freetype(FTypeId)),[])|FT]) :- !, |
| 2789 | | findall(b(identifier(CaseID),CaseType,[]), |
| 2790 | | (member(case(CaseID,ArgType),Cases), gen_freecase_type(ArgType,FTypeId,CaseType)), |
| 2791 | | FT, FT2), |
| 2792 | | %write(generated_freetype_cases(FT)),nl, |
| 2793 | | generate_free_type_ids(T,FT2). |
| 2794 | | generate_free_type_ids(T,T). |
| 2795 | | |
| 2796 | | gen_freecase_type(ArgType,FTypeId,Type) :- nonvar(ArgType), ArgType=constant(_),!, Type = freetype(FTypeId). |
| 2797 | | gen_freecase_type(ArgType,FTypeId,set(couple(ArgType,freetype(FTypeId)))). |
| 2798 | | |
| 2799 | | add_unique_variable(Var1,Old/Err_in,New/Err_out) :- |
| 2800 | | optionally_rewrite_id(Var1,Var), |
| 2801 | | get_texpr_id(Var,Id), |
| 2802 | | get_texpr_type(Var,Type), |
| 2803 | | get_texpr_info(Var,InfosOfNew),!, |
| 2804 | | ( env_lookup_type(Id,Old,_) -> |
| 2805 | | % we have a collision of two identifiers |
| 2806 | | handle_collision(Var,Id,Type,Old,InfosOfNew,New,Err_in,Err_out) |
| 2807 | | ; |
| 2808 | | % no collision, just introduce the new identifier |
| 2809 | | env_store(Id,Type,InfosOfNew,Old,New), |
| 2810 | | %btypechecker:portray_env(New),nl, |
| 2811 | | Err_in=Err_out |
| 2812 | | ). |
| 2813 | | add_unique_variable(Var,Env/Err,Env/Err) :- print(Var),nl, |
| 2814 | | ( Var = b(definition(DEFNAME,_),_,INFO) -> |
| 2815 | | add_error(add_unique_variable,'DEFINITION used in place of Identifier: ',DEFNAME,INFO) |
| 2816 | | ; Var = b(description(Txt,_),_,INFO) -> |
| 2817 | | add_error(add_unique_variable,'Unsupported @desc pragma: ',Txt,INFO) |
| 2818 | | ; |
| 2819 | | add_error(add_unique_variable,'Expected Identifier, but got: ',Var,Var) |
| 2820 | | ). |
| 2821 | | |
| 2822 | | add_infos_to_identifier(NewInfos,In,Out) :- |
| 2823 | | add_texpr_infos(In,NewInfos,Out). |
| 2824 | | |
| 2825 | | % get the ID of the variable, prime it if the infos contain "primed" |
| 2826 | | optionally_rewrite_id(Var,NewVar) :- |
| 2827 | | get_texpr_info(Var,InfosIn), |
| 2828 | | ( selectchk(primed,InfosIn,InfosOut) -> |
| 2829 | | get_texpr_id(Var,Id1), |
| 2830 | | get_texpr_type(Var,Type), |
| 2831 | | atom_concat(Id1,'\'',Id), |
| 2832 | | create_texpr(identifier(Id),Type,InfosOut,NewVar) |
| 2833 | | ; |
| 2834 | | Var = NewVar). |
| 2835 | | |
| 2836 | | :- use_module(translate,[translate_span/2]). |
| 2837 | | % in case of a collision, we have three options: |
| 2838 | | % - overwrite the old identifier, |
| 2839 | | % - ignore the new identifier or |
| 2840 | | % - generate an error message |
| 2841 | | handle_collision(Var,Name,Type,OldEnv,InfosOfNew,NewEnv,Ein,Eout) :- |
| 2842 | | env_lookup_infos(Name,OldEnv,InfosOfExisting), |
| 2843 | | %btypechecker:portray_env(OldEnv),nl, |
| 2844 | | ( collision_precedence(Name,InfosOfExisting,InfosOfNew) -> |
| 2845 | | % this identifier should be ignored |
| 2846 | | OldEnv = NewEnv, |
| 2847 | | Ein = Eout |
| 2848 | | ; collision_precedence(Name,InfosOfNew,InfosOfExisting) -> |
| 2849 | | % the existing should be overwritten |
| 2850 | | env_store(Name,Type,InfosOfNew,OldEnv,NewEnv), |
| 2851 | | Ein = Eout |
| 2852 | | ; |
| 2853 | | % generate error and let the environment unchanged |
| 2854 | | (Name = op(IName) -> Kind='Operation identifier'; Name=IName, Kind='Identifier'), |
| 2855 | | get_texpr_pos(Var,Pos1), |
| 2856 | | safe_get_info_pos(InfosOfExisting,Pos2), |
| 2857 | | ( double_inclusion_allowed(Name,Pos1,Pos2,InfosOfExisting) |
| 2858 | | -> %print(double_inclusion_of_id_allowed(Name,Type,Pos1,OldEnv,InfosOfExisting)),nl, |
| 2859 | | OldEnv=NewEnv, |
| 2860 | | Ein=Eout |
| 2861 | | ; (better_pos(Pos2,Pos1), \+ better_pos(Pos1,Pos2) |
| 2862 | | -> Pos = Pos2, translate_span(Pos1,PS1) |
| 2863 | | ; Pos = Pos1, |
| 2864 | | PS1='' % Pos1 is already part of error span |
| 2865 | | ), |
| 2866 | | translate_inclusion_path(InfosOfExisting,Path2), |
| 2867 | | get_texpr_info(Var,Info1), translate_inclusion_path(Info1,Path1), |
| 2868 | | (Pos1=Pos2, Path1=Path2 |
| 2869 | | -> ajoin([Kind,' \'', IName, '\'', PS1, Path1, ' included twice '],Msg) |
| 2870 | | % This should probably not happen; internal error in machine construction? |
| 2871 | | ; translate_span(Pos2,PS2), |
| 2872 | | %ajoin(['Identifier \'', IName, '\' declared twice at (Line:Col[:File]) ', PS1, Path1, ' and ', PS2, Path2],Msg), |
| 2873 | | ajoin([Kind,' \'', IName, '\'', PS1, Path1, ' already declared at ', PS2, Path2],Msg) |
| 2874 | | ), |
| 2875 | | %format(user_error,'*** ~w~n',[Msg]),trace, |
| 2876 | | Ein = [error(Msg,Pos)|Eout], |
| 2877 | | OldEnv = NewEnv |
| 2878 | | ) |
| 2879 | | ). |
| 2880 | | |
| 2881 | | |
| 2882 | | % example identifier: %b(identifier(aa),integer,[loc(seen,M2,concrete_constants),readonly,usesee(M2,aa,seen),origin([included/M1]),nodeid(pos(18,2,2,11,2,13))]) |
| 2883 | | |
| 2884 | | % try and infer inclusion path of identifier from Infos |
| 2885 | | translate_inclusion_path(Infos,Str) :- member(loc(How,Machine,Section),Infos),!, |
| 2886 | | (member(origin(Path),Infos) -> get_origin_path(Path,T) ; T=[')']), |
| 2887 | | ajoin([' (', How,' from ', Section, ' section of ', Machine |T],Str). |
| 2888 | | translate_inclusion_path(_,''). |
| 2889 | | |
| 2890 | | get_origin_path([How/Machine|T],[', ', How,' from ',Machine|TRes]) :- !, |
| 2891 | | get_origin_path(T,TRes). |
| 2892 | | get_origin_path(_,[')']). |
| 2893 | | |
| 2894 | | |
| 2895 | | % SEE ISSUE PROB-403, test 1857 |
| 2896 | | % Correct behaviour related to multiple instantiation is specified in |
| 2897 | | % B Reference Manual (AtelierB 4.2.1), 8.3 B Project/Instantiating and renaming. |
| 2898 | | % => Constants and Sets defined in machines instantiated multiple times CAN be used in the including machine with their original (non-prefixed names). |
| 2899 | | % Note: this code did lead to the constants being added multiple times; this has been fixed in concat_section_contents |
| 2900 | | double_inclusion_allowed(Name,Pos1,Pos2,InfosOfExisting) :- |
| 2901 | | %print(check_double_inclusion(Name,Pos1,Pos2,InfosOfExisting)),nl, |
| 2902 | | Pos1==Pos2, |
| 2903 | | %print(chk(InfosOfExisting)),nl, |
| 2904 | | member(loc(LOC,_,Section),InfosOfExisting), |
| 2905 | | %print(try(LOC,Section)),nl, |
| 2906 | | section_can_be_included_multiple_times_nonprefixed(Section), |
| 2907 | | % check that we are in a context of an included machine identifier: |
| 2908 | | (inclusion_directive(LOC,Name,Pos2) |
| 2909 | | -> true |
| 2910 | | ; %LOC is probably local |
| 2911 | | member(origin([INCL/_MACHINE|_]),InfosOfExisting), |
| 2912 | | inclusion_directive(INCL,Name,Pos2) |
| 2913 | | ). |
| 2914 | | |
| 2915 | | inclusion_directive(included,_,_). |
| 2916 | | inclusion_directive(used,_,_). |
| 2917 | | inclusion_directive(seen,_,_). % imports ?? |
| 2918 | | inclusion_directive(abstraction,Name,Pos) :- % probably not allowed by Atelier-B |
| 2919 | | (debug_mode(off) -> true |
| 2920 | | ; add_message(bmachine_construction,'Allowing double inclusion from abstraction of: ',Name,Pos)). |
| 2921 | | |
| 2922 | | section_can_be_included_multiple_times_nonprefixed(abstract_constants). |
| 2923 | | section_can_be_included_multiple_times_nonprefixed(concrete_constants). |
| 2924 | | section_can_be_included_multiple_times_nonprefixed(sets). |
| 2925 | | section_can_be_included_multiple_times_nonprefixed(enumerated_sets). |
| 2926 | | section_can_be_included_multiple_times_nonprefixed(enumerated_elements). |
| 2927 | | section_can_be_included_multiple_times_nonprefixed(deferred_sets). % added 2.12.2022 |
| 2928 | | section_can_be_included_multiple_times_nonprefixed(constants). % shortcut |
| 2929 | | |
| 2930 | | |
| 2931 | | % decide which position info is better: prefer info in main file (highlighting) |
| 2932 | | :- use_module(bmachine,[b_get_main_filenumber/1]). |
| 2933 | | better_pos(Pos,_) :- get_position_filenumber(Pos,Filenumber), |
| 2934 | | b_get_main_filenumber(Filenumber). |
| 2935 | | better_pos(_,none). |
| 2936 | | |
| 2937 | | safe_get_info_pos(Info,Pos) :- (get_info_pos(Info,Pos) -> true ; Pos=none). |
| 2938 | | |
| 2939 | | % collision_precedence/3 decides if the first variable takes |
| 2940 | | % precedence over the second in case of a collision |
| 2941 | | % the decision is made by the additional information of both |
| 2942 | | % variables |
| 2943 | | collision_precedence(_Name,PreferredVarInfos,DroppedVarInfos) :- |
| 2944 | | % in case of a re-introduced variable from the abstraction, |
| 2945 | | % we prefer the concrete variable to the abstract one. |
| 2946 | | is_abstraction(DroppedVarInfos,PreferredVarInfos),!. |
| 2947 | | collision_precedence(_Name,PreferredVarInfos,DroppedVarInfos) :- |
| 2948 | | % We are checking an Event-B model with multi-level support |
| 2949 | | % and have the same variable in two different refinement levels. |
| 2950 | | % Then the one in the more refined module takes precedence |
| 2951 | | member(level(L1),PreferredVarInfos), |
| 2952 | | member(level(L2),DroppedVarInfos), |
| 2953 | | % Level 0 is the abstract level, level 1 the first refinement, etc. |
| 2954 | | L1 > L2,!. |
| 2955 | | collision_precedence(Name,PreferredVarInfos,DroppedVarInfos) :- |
| 2956 | | % A local definition takes precedence over a non-local identifier |
| 2957 | | % TODO: |
| 2958 | | member(loc(local,_DefMachine,definitions),PreferredVarInfos), |
| 2959 | | member(loc(_,_VarMachine,Section),DroppedVarInfos), |
| 2960 | | Section \= definitions,!, |
| 2961 | | (preferences:get_preference(warn_if_definition_hides_variable,true) |
| 2962 | | % default is true; we could also check clash_strict_checks |
| 2963 | | -> get_id_kind(Section,HiddenIdKind), |
| 2964 | | (get_info_pos(PreferredVarInfos,Pos1), Pos1 \= none, |
| 2965 | | get_info_pos(DroppedVarInfos,Pos2), Pos2 \= none |
| 2966 | | -> translate:translate_span(Pos1,Pos1Str), translate:translate_span(Pos2,Pos2Str), |
| 2967 | | ajoin(['Warning: DEFINITION of ', Name, ' at ', Pos1Str, |
| 2968 | | ' hides ',HiddenIdKind,' with same name at ', Pos2Str, '.'], Msg) |
| 2969 | | ; ajoin(['Warning: DEFINITION of ', Name, ' hides ',HiddenIdKind,' with same name.'], Msg), |
| 2970 | | Pos1 = unknown |
| 2971 | | ), |
| 2972 | | store_warning(Msg,Pos1) % TO DO: add position info |
| 2973 | | ; true |
| 2974 | | ). |
| 2975 | | % TO DO: allow identical DEFINITIONS ? |
| 2976 | | |
| 2977 | | % translate section name into a name for the identifier |
| 2978 | | get_id_kind(abstract_constants,'constant'). |
| 2979 | | get_id_kind(concrete_constants,'constant'). |
| 2980 | | get_id_kind(parameters,'parameter'). |
| 2981 | | get_id_kind(deferred_sets,'deferred set'). |
| 2982 | | get_id_kind(enumerated_sets,'enumerated set'). |
| 2983 | | get_id_kind(enumerated_elements,'enumerated set element'). |
| 2984 | | get_id_kind(freetypes,'freetype'). |
| 2985 | | get_id_kind(promoted,'operation'). |
| 2986 | | % TODO: complete and use in other places |
| 2987 | | get_id_kind(_SectionName,'variable'). |
| 2988 | | |
| 2989 | | |
| 2990 | | % is_abstraction/2 tries to find out if (in case of a name clash of |
| 2991 | | % two variables) the second variable is just the re-introduced abstract |
| 2992 | | % variable in a refinement. |
| 2993 | | % InfosAbs is the list of information about the abstract variable |
| 2994 | | % InfosConc is the list of information about the concrete variable |
| 2995 | | is_abstraction(InfosAbs,InfosConc) :- |
| 2996 | | % one variable is an abstract variable, introduced in the abstraction |
| 2997 | | member(loc(abstraction,_,abstract_variables),InfosAbs), |
| 2998 | | % the other is either an abstract or concrete variable, |
| 2999 | | member(VarType,[abstract_variables,concrete_variables]), |
| 3000 | | % introduced either locally or in an included machine |
| 3001 | | member(Scope,[local,included]), |
| 3002 | | member(loc(Scope,_,VarType),InfosConc). |
| 3003 | | % and the same for constants: |
| 3004 | | is_abstraction(InfosAbs,InfosConc) :- |
| 3005 | | % one variable is an abstract variable, introduced in the abstraction |
| 3006 | | member(loc(abstraction,_,abstract_constants),InfosAbs), |
| 3007 | | % the other is either an abstract or concrete variable, |
| 3008 | | member(VarType,[abstract_constants,concrete_constants]), |
| 3009 | | % introduced either locally or in an included machine |
| 3010 | | member(Scope,[local,included]), |
| 3011 | | member(loc(Scope,_,VarType),InfosConc). |
| 3012 | | |
| 3013 | | % shortcuts for sections, to ease the use of typical combinations of |
| 3014 | | % sections |
| 3015 | | shortcut(all_parameters,[parameters,internal_parameters]). |
| 3016 | | shortcut(sets,[deferred_sets,enumerated_sets,enumerated_elements|T]) :- |
| 3017 | | (animation_minor_mode(M), (M=z ; M=eventb) |
| 3018 | | -> T = [freetypes] |
| 3019 | | ; T = []). % The FREETYPES section in classical B is unfortunately dealt with differently and |
| 3020 | | % we currently have errors if add the freetypes section here |
| 3021 | | shortcut(constants,[abstract_constants,concrete_constants]). |
| 3022 | | shortcut(variables,[abstract_variables,concrete_variables]). |
| 3023 | | shortcut(operations,[unpromoted,promoted]). |
| 3024 | | shortcut(identifiers,[all_parameters,sets,constants,variables,operations]). |
| 3025 | | |
| 3026 | | expand_shortcuts(Sections,Expanded) :- |
| 3027 | | foldl(expand_shortcut,Sections,Expanded,[]). |
| 3028 | | expand_shortcut(Section,Sections,RSections) :- |
| 3029 | | ( shortcut(Section,Expanded) -> |
| 3030 | | foldl(expand_shortcut,Expanded,Sections,RSections) |
| 3031 | | ; valid_section(Section) -> |
| 3032 | | Sections = [Section|RSections] |
| 3033 | | ; |
| 3034 | | add_internal_error('invalid section',expand_shortcut(Section,Sections,RSections)),fail). |
| 3035 | | |
| 3036 | | % find sections that can see given sections |
| 3037 | | find_relevant_sections(RSecs,MTypes,Result) :- |
| 3038 | | expand_shortcuts(RSecs,Sections), |
| 3039 | | findall(R, |
| 3040 | | ( member(MType,MTypes), |
| 3041 | | visibility(MType,local,R,SAccess,_), |
| 3042 | | expand_shortcuts(SAccess,Access), |
| 3043 | | member(S,Sections), |
| 3044 | | member(S,Access), |
| 3045 | | valid_section(R)), |
| 3046 | | Result1), |
| 3047 | | sort(Result1,Result). |
| 3048 | | |
| 3049 | | |
| 3050 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 3051 | | % renaming |
| 3052 | | |
| 3053 | | rename_relevant_sections(DefSecs,Renamings,Machine,New) :- |
| 3054 | | find_relevant_sections(DefSecs,[machine],Relevant), |
| 3055 | | rename_in_sections(Relevant,Renamings,Machine,New). |
| 3056 | | rename_in_sections([],_,M,M). |
| 3057 | | rename_in_sections([Section|Rest],Renamings,Old,New) :- |
| 3058 | | select_section_texprs(Section,OTExprs,NTExprs,Old,Inter), |
| 3059 | | rename_bt_l(OTExprs,Renamings,NTExprs), |
| 3060 | | rename_in_sections(Rest,Renamings,Inter,New). |
| 3061 | | |
| 3062 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 3063 | | :- use_module(kernel_freetypes,[register_freetypes/1]). |
| 3064 | | % cleaning up machine |
| 3065 | | clean_up_machine(In,RefMachines,Out) :- |
| 3066 | | extract_parameter_types([ref(local,In)|RefMachines],NonGroundExceptions), |
| 3067 | | clean_up_machine2(NonGroundExceptions,In,Out). |
| 3068 | | clean_up_machine2(NonGroundExceptions) --> |
| 3069 | | get_section_content(enumerated_sets,Enum), |
| 3070 | | get_section_content(enumerated_elements,Elems), |
| 3071 | | {register_enumerated_sets(Enum,Elems)}, % register name of enumerated sets, e.g., to detect finite in ast_cleanup |
| 3072 | | get_section_content(freetypes,Freetypes), |
| 3073 | | {register_freetypes(Freetypes)}, % so that info is available in ast_cleanup for eval_set_extension |
| 3074 | | clean_up_section(constraints,NonGroundExceptions), |
| 3075 | | clean_up_section(properties,NonGroundExceptions), |
| 3076 | | clean_up_section(invariant,NonGroundExceptions), |
| 3077 | | clean_up_section(initialisation,NonGroundExceptions), |
| 3078 | | clean_up_section(assertions,NonGroundExceptions), |
| 3079 | | clean_up_section(operation_bodies,NonGroundExceptions). |
| 3080 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 3081 | | :- if(environ(prob_safe_mode,true)). |
| 3082 | | clean_up_section(Section,NonGroundExceptions,In,Out) :- |
| 3083 | | select_section_texprs(Section,Old,New,In,Out), |
| 3084 | | %format('Cleaning up and optimizing section ~w~n',[Section]), %maplist(check_ast,Old), % this will raise errors |
| 3085 | | clean_up_l_with_optimizations(Old,NonGroundExceptions,New,Section), |
| 3086 | | %format('Checking result of clean_up section ~w~n',[Section]), |
| 3087 | | maplist(check_ast(true),New), |
| 3088 | | formatsilent('Finished checking section ~w~n',[Section]). |
| 3089 | | :- else. |
| 3090 | | clean_up_section(Section,NonGroundExceptions,In,Out) :- |
| 3091 | | % debug_stats(cleaning_up(Section)), |
| 3092 | | select_section_texprs(Section,Old,New,In,Out), |
| 3093 | | clean_up_l_with_optimizations(Old,NonGroundExceptions,New,Section). |
| 3094 | | :- endif. |
| 3095 | | |
| 3096 | | get_section_content(SecName,SectionContent,Mch,Mch) :- get_section(SecName,Mch,SectionContent). |
| 3097 | | |
| 3098 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 3099 | | % type expressions in context of an already type-checked machine |
| 3100 | | % TO DO: maybe do some performance optimisations for identifiers, values, ... to avoid creating scope, see formula_typecheck2_for_eval optimisation |
| 3101 | | % b_type_literal does it in bmachine before calling type_in_machine_l |
| 3102 | | type_in_machine_l(Exprs,Scope,NonGroundExceptions,Machine,Types,TExprs,Errors) :- |
| 3103 | | MType = machine, |
| 3104 | | create_scope_if_necessary(Exprs,Scope,MType,Machine,Env,Errors,E1), % this can be expensive for big B machines |
| 3105 | | %runtime_profiler:profile_single_call(create_scope,unknown, |
| 3106 | | % bmachine_construction:create_scope(Scope,MType,Machine,Env,Errors,E1)), |
| 3107 | | btype_ground_dl(Exprs,Env,NonGroundExceptions,Types,TExprUncleans,E1,[]), |
| 3108 | | perform_post_static_check(TExprUncleans), |
| 3109 | ? | maplist(clean_up_pred_or_expr(NonGroundExceptions),TExprUncleans,TExprs). |
| 3110 | | |
| 3111 | | % detect a few common expressions which do not require creating a scope of all the identifiers |
| 3112 | | create_scope_if_necessary([E],_Scope,MType,Machine,Env,Ein,Eout) :- raw_expr_wo_ids(E),!, |
| 3113 | | create_scope([],MType,Machine,Env,Ein,Eout). |
| 3114 | | create_scope_if_necessary(_Exprs,Scope,MType,Machine,Env,Ein,Eout) :- |
| 3115 | | create_scope(Scope,MType,Machine,Env,Ein,Eout). |
| 3116 | | |
| 3117 | | % a few common raw ASTs which do not refer to identifiers |
| 3118 | | raw_expr_wo_ids(falsity(_)). |
| 3119 | | raw_expr_wo_ids(truth(_)). |
| 3120 | | raw_expr_wo_ids(empty_set(_)). |
| 3121 | | raw_expr_wo_ids(equal(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B). |
| 3122 | | raw_expr_wo_ids(not_equal(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B). |
| 3123 | | raw_expr_wo_ids(interval(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B). |
| 3124 | | raw_expr_wo_ids(add(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B). |
| 3125 | | raw_expr_wo_ids(minus_or_set_subtract(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B). |
| 3126 | | raw_expr_wo_ids(mult_or_cart(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B). |
| 3127 | | raw_expr_wo_ids(unary_minus(_,A)) :- raw_expr_wo_ids(A). |
| 3128 | | raw_expr_wo_ids(boolean_true(_)). |
| 3129 | | raw_expr_wo_ids(boolean_false(_)). |
| 3130 | | raw_expr_wo_ids(bool_set(_)). |
| 3131 | | raw_expr_wo_ids(integer(_,_)). |
| 3132 | | raw_expr_wo_ids(real(_,_)). |
| 3133 | | raw_expr_wo_ids(string(_,_)). |
| 3134 | | |
| 3135 | | |
| 3136 | | % note prob_ids(visible), external_library(all_available_libraries) scope is expanded somewhere else |
| 3137 | | create_scope(pre_expanded_scope(PEnv,Errors),_MType,_Machine,Env,Ein,Eout) :- |
| 3138 | | !, % already pre-expanded |
| 3139 | | Env=PEnv, append(Errors,Eout, Ein). |
| 3140 | | create_scope(Scope,MType,Machine,Env,Ein,Eout) :- |
| 3141 | | env_empty(Init), |
| 3142 | | add_theory_operators(Machine,Init,WithOperators), |
| 3143 | | foldl(create_scope2(MType,Machine),Scope,WithOperators/Ein,Env/Eout). |
| 3144 | | add_theory_operators(Machine,Ein,Eout) :- |
| 3145 | | get_section(operators,Machine,Operators), |
| 3146 | | keys_and_values(Operators,Ids,Ops), |
| 3147 | | foldl(env_store_operator,Ids,Ops,Ein,Eout). |
| 3148 | | create_scope2(MType,Machine,Scope,In/Ein,Out/Eout) :- |
| 3149 | | ( Scope = constants -> |
| 3150 | | visible_env(MType,properties,[ref(local,Machine)],In,Out,Ein,Eout) |
| 3151 | | ; Scope = variables -> |
| 3152 | | visible_env(MType,invariant,[ref(local,Machine)],In,Out,Ein,Eout) |
| 3153 | | ; Scope = variables_and_additional_defs -> |
| 3154 | | visible_env(MType,invariant,[extended_local_ref(Machine)],In,Out,Ein,Eout) |
| 3155 | | ; Scope = assertions_scope_and_additional_defs -> |
| 3156 | | visible_env(MType,assertions,[extended_local_ref(Machine)],In,Out,Ein,Eout) |
| 3157 | | ; Scope = prepost -> |
| 3158 | | visible_env(MType,prepost,[ref(local,Machine)],In,Out,Ein,Eout) |
| 3159 | | ; Scope = operation_bodies -> |
| 3160 | | visible_env(MType,operation_bodies,[ref(local,Machine)],In,Out,Ein,Eout) |
| 3161 | | ; Scope = operation(Op) -> |
| 3162 | | create_operation_scope(Op,Machine,In,Out), Ein=Eout |
| 3163 | | ; Scope = env(ExplicitEnv) -> |
| 3164 | | ExplicitEnv = Out, Ein=Eout |
| 3165 | | ; Scope = identifier(Ids) -> |
| 3166 | | store_variables(Ids,In,Out), Ein=Eout |
| 3167 | | ; Scope = external_library(LibName) % be sure to make these last to avoid duplication errors |
| 3168 | | -> store_ext_defs(LibName,In,Out), Ein=Eout |
| 3169 | | ; |
| 3170 | | add_error(bmachine_construction, 'invalid scope', Scope),fail). |
| 3171 | | create_operation_scope(Op,Machine,In,Out) :- |
| 3172 | | get_section(operation_bodies,Machine,OpBodies), |
| 3173 | | get_texpr_id(OpId,op(Op)), |
| 3174 | | get_texpr_expr(TOp,operation(OpId,Results,Params,_)), |
| 3175 | | ( member(TOp,OpBodies) -> |
| 3176 | | append(Results,Params,LocalVariables), |
| 3177 | | store_variables(LocalVariables,In,Out) |
| 3178 | | ; |
| 3179 | | ajoin(['operation \'',Op,'\' not found for building scope'], Msg), |
| 3180 | | add_error(bmachine_construction,Msg),fail). |
| 3181 | | store_variables(Ids,In,Out) :- foldl(store_variable,Ids,In,Out). |
| 3182 | | store_variable(Id,In,Out) :- |
| 3183 | | get_texpr_id(Id,Name),get_texpr_type(Id,Type), |
| 3184 | | env_store(Name,Type,[],In,Out). |
| 3185 | | |
| 3186 | | type_open_predicate_with_quantifier(OptionalOuterQuantifier,Predicate,Scope,Machine,TResult,Errors) :- |
| 3187 | | type_open_formula(Predicate,Scope,false,Machine,pred,Identifiers,TPred,Errors), |
| 3188 | | ( Identifiers = [] -> |
| 3189 | | TResult = TPred |
| 3190 | | ; OptionalOuterQuantifier=forall -> |
| 3191 | | create_forall(Identifiers,TPred,TResult) |
| 3192 | | ; OptionalOuterQuantifier=no_quantifier -> |
| 3193 | | TResult = TPred |
| 3194 | | ; % OptionalOuterQuantifier=exists |
| 3195 | | %perform_do_not_enumerate_analysis(Identifiers,TPred,'EXISTS',Span,TPred2), % now done by apply_kodkod_or_other_optimisations |
| 3196 | | create_exists(Identifiers,TPred,TResult) |
| 3197 | | ). |
| 3198 | | |
| 3199 | | type_open_formula(Raw,Scope,AllowOpenIdsinExpressions,Machine,Type,Identifiers,Result,Errors) :- |
| 3200 | | create_scope_if_necessary([Raw],Scope,machine,Machine,Env1,Errors,E1), |
| 3201 | | ( Identifiers==[] -> Mode=closed, Env1=Env |
| 3202 | | ; Mode=open, openenv(Env1,Env)), |
| 3203 | | btype_ground_dl([Raw],Env,[],[Type],[TExprUnclean],E1,E2), |
| 3204 | | ( Mode=closed -> true |
| 3205 | | ; |
| 3206 | | openenv_identifiers(Env,Identifiers), % TODO: treat theory operators ? |
| 3207 | | check_ground_types_dl(Identifiers,[],E2,E3) |
| 3208 | | ), |
| 3209 | | %print(type_open_formula(Identifiers,TExprUnclean)),nl, |
| 3210 | | mark_outer_quantifier_ids(TExprUnclean,TExprUnclean2), |
| 3211 | | perform_post_static_check([TExprUnclean2]), |
| 3212 | | clean_up_pred_or_expr([],TExprUnclean2,TResult), % TODO: only run if requested |
| 3213 | | ( Identifiers = [] -> % no newly introduced identifiers, no problem |
| 3214 | | E3 = [] |
| 3215 | | ; Type = pred -> % newly introduced identifiers in a predicate - ok |
| 3216 | | E3 = [] |
| 3217 | | ; AllowOpenIdsinExpressions=true -> % we explicitly allow open ids in expressions |
| 3218 | | E3 = [] |
| 3219 | | ; % newly introduced identifiers in expression make no sense |
| 3220 | | % (is that so?) |
| 3221 | | foldl(add_unknown_identifier_error,Identifiers,E3,[]) |
| 3222 | | ), |
| 3223 | | Result = TResult. |
| 3224 | | add_unknown_identifier_error(TId,[error(Msg,Pos)|E],E) :- |
| 3225 | | get_texpr_id(TId,Id), |
| 3226 | | ajoin(['Unknown identifier ',Id,'.'],Msg), |
| 3227 | | % TO DO: generate fuzzy match and possible completions message |
| 3228 | | get_texpr_pos(TId,Pos). |
| 3229 | | |
| 3230 | | % mark outermost identfiers so that they don't get optimized away |
| 3231 | | % e.g., ensure that we print the solution for something like #(y2,x2).(x2 : 0..10 & y2 : 0..10 & x2 = 10 & y2 = 10) |
| 3232 | | mark_outer_quantifier_ids(b(exists(IDS,Pred),pred,Info),Res) :- |
| 3233 | | maplist(mark_id,IDS,MIDS),!, |
| 3234 | | Res = b(exists(MIDS,Pred),pred,Info). |
| 3235 | | mark_outer_quantifier_ids(b(let_predicate(IDS,Exprs,Pred),pred,Info),Res) :- |
| 3236 | | maplist(mark_id,IDS,MIDS),!, |
| 3237 | | Res = b(let_predicate(MIDS,Exprs,Pred),pred,Info). |
| 3238 | | mark_outer_quantifier_ids(b(forall(IDS,LHS,RHS),pred,Info),Res) :- |
| 3239 | | maplist(mark_id,IDS,MIDS),!, |
| 3240 | | Res = b(forall(MIDS,LHS,RHS),pred,Info). |
| 3241 | | mark_outer_quantifier_ids(X,X). |
| 3242 | | |
| 3243 | | mark_id(b(identifier(ID),TYPE,INFO),b(identifier(ID),TYPE,[do_not_optimize_away|INFO])). |
| 3244 | | |
| 3245 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 3246 | | |
| 3247 | | % some additional static checks; they should be run only once before ast_cleanup runs |
| 3248 | | % TO DO: move maybe some of the exists/forall checks here; would be simpler and not require removed_typing inspection |
| 3249 | | |
| 3250 | | :- use_module(bsyntaxtree,[map_over_typed_bexpr/2]). |
| 3251 | | perform_post_static_check([Typed|_]) :- %print(t(Typed)),nl, |
| 3252 | | preferences:get_preference(disprover_mode,false), |
| 3253 | | map_over_typed_bexpr(post_static_check,Typed), |
| 3254 | | fail. |
| 3255 | | perform_post_static_check([_|T]) :- !, perform_post_static_check(T). |
| 3256 | | perform_post_static_check(_). |
| 3257 | | |
| 3258 | | post_static_check(b(E,T,I)) :- |
| 3259 | | %bsyntaxtree:check_infos(I,post_static_check), |
| 3260 | | post_static_check_aux(E,T,I). |
| 3261 | | |
| 3262 | | :- use_module(bsyntaxtree,[find_identifier_uses/3, is_a_disjunct_or_implication/4]). |
| 3263 | | :- use_module(library(ordsets),[ord_subtract/3]). |
| 3264 | | % should detect patterns like { zz | # r__1, q__1, zz . ( ...)} |
| 3265 | | % {x,z|z=1}[{TRUE}] = {1} |
| 3266 | | % %x.(1=1|1)(TRUE) = 1 |
| 3267 | | post_static_check_aux(lambda(Ids,Body,Expr),_T,Info) :- |
| 3268 | | get_texpr_ids(Ids,AtomicIds), sort(AtomicIds,SortedIds), |
| 3269 | | find_identifier_uses(Body,[],UsedIds1), |
| 3270 | | find_identifier_uses(Expr,[],UsedIds2), % relevant for tests 1106, 1264, 1372, 1622 to also look at Expr |
| 3271 | | ord_subtract(SortedIds,UsedIds1,S2), |
| 3272 | | ord_subtract(S2,UsedIds2,UnusedIds), UnusedIds \= [], |
| 3273 | | add_warning_with_info('Condition of lambda does not use these identifiers: ',UnusedIds,Body,Info). |
| 3274 | | post_static_check_aux(comprehension_set(Ids,Body),_T,Info) :- |
| 3275 | | get_texpr_ids(Ids,AtomicIds), sort(AtomicIds,SortedIds), |
| 3276 | | find_identifier_uses(Body,[],UsedIds), |
| 3277 | | ord_subtract(SortedIds,UsedIds,UnusedIds), UnusedIds \= [], |
| 3278 | | add_warning_with_info('Body of comprehension set does not use these identifiers: ',UnusedIds,Body,Info). |
| 3279 | | post_static_check_aux(exists(Ids,P),_T,Info) :- |
| 3280 | | is_a_disjunct_or_implication(P,Type,_Q,_R), |
| 3281 | | exists_body_warning(Ids,P,Info,Type). |
| 3282 | | |
| 3283 | | % see also check_implication_inside_exists ast cleanup rule |
| 3284 | | exists_body_warning(_,_,_,_) :- animation_minor_mode(X),(X=eventb ; X=tla),!. |
| 3285 | | exists_body_warning(Ids,P,I,Type) :- |
| 3286 | | ajoin(['Body of existential quantifier is a(n) ',Type, |
| 3287 | | ' (not allowed by Atelier-B): '],Msg), |
| 3288 | | add_warning_with_info(Msg,b(exists(Ids,P),pred,I),P,I). |
| 3289 | | |
| 3290 | | |
| 3291 | | |
| 3292 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 3293 | | % Warnings |
| 3294 | | |
| 3295 | | :- use_module(bsyntaxtree,[contains_info_pos/1]). |
| 3296 | | add_warning_with_info(Msg1,Msg2,P,Info) :- |
| 3297 | | (contains_info_pos(Info) -> Pos=Info ; Pos=P), |
| 3298 | | add_warning(bmachine_construction,Msg1,Msg2,Pos). |
| 3299 | | |
| 3300 | | :- dynamic warnings/2. |
| 3301 | | clear_warnings :- |
| 3302 | | retractall( warnings(_,_) ). |
| 3303 | | show_warnings :- |
| 3304 | | warnings(Warning,Span), |
| 3305 | | add_warning(bmachine_construction, Warning,'',Span), |
| 3306 | | fail. |
| 3307 | | show_warnings. |
| 3308 | | |
| 3309 | | |
| 3310 | | store_warning(Warning,Span) :- |
| 3311 | | (warnings(Warning,Span) -> true ; assertz(warnings(Warning,Span))). |