| 1 | | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
| 2 | | % Heinrich Heine Universitaet Duesseldorf |
| 3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
| 4 | | |
| 5 | | :- module(bmachine_construction,[reset_bmachine_construction/0, |
| 6 | | check_machine/4, |
| 7 | | type_in_machine_l/6, |
| 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 | | filter_linking_invariant/3, |
| 12 | | external_procedure_used/1]). |
| 13 | | |
| 14 | | :- use_module(library(lists)). |
| 15 | | :- use_module(library(avl)). |
| 16 | | |
| 17 | | :- use_module(self_check). |
| 18 | | :- use_module(tools). |
| 19 | | :- use_module(error_manager). |
| 20 | | :- use_module(debug). |
| 21 | | :- use_module(preferences). |
| 22 | | |
| 23 | | :- use_module(btypechecker). |
| 24 | | :- use_module(b_ast_cleanup). |
| 25 | | :- use_module(bsyntaxtree). |
| 26 | | :- use_module(bmachine_structure). |
| 27 | | :- use_module(pragmas). |
| 28 | | |
| 29 | | :- use_module(bmachine_static_checks). |
| 30 | | |
| 31 | | :- use_module(translate,[print_machine/1]). |
| 32 | | |
| 33 | | :- use_module(module_information,[module_info/2]). |
| 34 | | :- module_info(group,typechecker). |
| 35 | | :- module_info(description,'This module contains the rules for loading, including, seeing, etc. B machines, scope of constants, variables, parameters, etc.'). |
| 36 | | |
| 37 | | %maximum_type_errors(100). |
| 38 | | |
| 39 | | :- dynamic debug_machine/0. |
| 40 | | |
| 41 | | :- use_module(pref_definitions,[b_get_important_preferences_from_raw_machine/2]). |
| 42 | | set_important_prefs_from_machine(Main,Machines) :- |
| 43 | ? | find_machine(Main,Machines,_MType,_Header,RawMachine), |
| 44 | ? | get_raw_model_type(Main,Machines,RawModelType), |
| 45 | | b_get_important_preferences_from_raw_machine(RawMachine,RawModelType). |
| 46 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 47 | | |
| 48 | | :- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]). |
| 49 | | |
| 50 | | % typecheck complete machines (incl. includes) |
| 51 | | check_machine(MainName,MachinesMayContainGenerated,Result,FinalErrors) :- |
| 52 | ? | clear_warnings, |
| 53 | ? | debug_println(9,checking_machine(MainName)), |
| 54 | ? | temporary_set_preference(perform_stricter_static_checks,true,CHNG), |
| 55 | ? | strip_global_pragmas(MachinesMayContainGenerated,Machines,_WasGenerated), % TODO: is generated still used? |
| 56 | ? | set_important_prefs_from_machine(MainName,Machines), % set important prefs before type-checking,... |
| 57 | | % we need to find all SEES/USES declarations, because all references |
| 58 | | % refer to the same machine and that has to be included exactly once. |
| 59 | ? | ~~mnf( find_uses(Machines,Uses,NotIncluded,Errors,E1) ), |
| 60 | | % if a seen/used machine was not included, we include it by constructing |
| 61 | | % a dummy machine that extends the seen/used machine and the origional |
| 62 | | % main machine |
| 63 | ? | ~~mnf( extend_not_included_uses(NotIncluded,MainName,NewMainName,Machines,IMachines) ), |
| 64 | | % figure out the right order of machines, so that each machine is |
| 65 | | % type-checked before a dependend machine is loaded |
| 66 | ? | ~~mnf( machine_order(IMachines,Order) ), |
| 67 | | % expand (= type-check + includes) machines in the given order |
| 68 | ? | ~~mnf( expand_machines(Order,IMachines,Uses,[],Results1,E1,E2) ), |
| 69 | | % until now, the initialisation section consists of a list of init(MachineName,Substitution) |
| 70 | | % fold_initialisation merges those to one substitution, respecting the dependencies |
| 71 | | % between the machines |
| 72 | ? | maplist(fold_initialisation(Order),Results1,Results), |
| 73 | | % find main machine |
| 74 | ? | memberchk(machine(NewMainName,MainMachine),Results), %nl,print('MAIN:'),nl,print_machine(MainMachine), |
| 75 | | % if the main machine has parameters, we convert them to global sets resp. constants |
| 76 | ? | ~~mnf( convert_parameters_to_global_sets(E2,[],MainMachine,Result1) ), |
| 77 | | % add some additional informations about the machine |
| 78 | ? | add_machine_infos(MainName,Machines,Results,Result1,Result), |
| 79 | | ( debug_machine -> print_machine(Result); true), |
| 80 | | % finalize the list of errors, remove duplicates |
| 81 | | sort(Errors,FinalErrors), |
| 82 | | % output warnings |
| 83 | | show_warnings, |
| 84 | | % run static checks on the resulting machine |
| 85 | | static_check_main_machine(Result), |
| 86 | | reset_temporary_preference(perform_stricter_static_checks,CHNG). |
| 87 | | check_machine(Main,_,Result,FinalErrors) :- |
| 88 | | add_internal_error('Internal error: Checking the machine failed: ', |
| 89 | | check_machine(Main,_,Result,FinalErrors)), |
| 90 | | % trace,check_machine(Main,Machines,Result,FinalErrors), |
| 91 | | fail. |
| 92 | | |
| 93 | | strip_global_pragmas([],[],false). |
| 94 | | strip_global_pragmas([generated(_,M)|Ms],MachinesOut,true) :- !, |
| 95 | | strip_global_pragmas([M|Ms],MachinesOut,_). |
| 96 | | strip_global_pragmas([unit_alias(_,Alias,Content,M)|Ms],MachinesOut,true) :- !, |
| 97 | | assert(pragmas:global_pragma(unit_alias,[Alias|Content])), |
| 98 | | strip_global_pragmas([M|Ms],MachinesOut,_). |
| 99 | | strip_global_pragmas([M|Ms],[M|SMs],WasGenerated) :- |
| 100 | | strip_global_pragmas(Ms,SMs,WasGenerated). |
| 101 | | |
| 102 | | fold_initialisation(Order,machine(Name,Sections),machine(Name,NewSections)) :- |
| 103 | ? | select_section(initialisation,List,Subst,Sections,NewSections), |
| 104 | ? | maplist(extract_init_substitutions(List),Order,LSubstitutions), |
| 105 | ? | append(LSubstitutions,Substitutions), |
| 106 | ? | create_sequence(Substitutions,Subst). |
| 107 | | extract_init_substitutions(Unsorted,Name,Substitutions) :- |
| 108 | | convlist(unzip_init(Name),Unsorted,Substitutions). |
| 109 | | unzip_init(Name,init(Name,Subst),Subst). |
| 110 | | create_sequence([],Subst) :- create_texpr(skip,subst,[generated],Subst). |
| 111 | | create_sequence([I],I) :- !. |
| 112 | | create_sequence(L,Sequence) :- create_texpr(sequence(L),subst,[initial_sequence],Sequence). |
| 113 | | |
| 114 | | add_machine_infos(Main,Machines,CheckedMachines,Old,New) :- |
| 115 | ? | get_raw_model_type(Main,Machines,RawModelType), functor(RawModelType,ModelType,_), % argument is position |
| 116 | | % model type could be machine or system (or model ?) |
| 117 | | append_to_section(meta,[model_type/ModelType,hierarchy/Hierarchy],Old,NewT), |
| 118 | | get_refinement_hierarchy(Main,Machines,Hierarchy), |
| 119 | | add_refined_machine(Hierarchy,CheckedMachines,NewT,New). |
| 120 | | get_refinement_hierarchy(Main,Machines,[Main|Abstractions]) :- |
| 121 | | ( find_refinement(Machines,Main,Abstract) -> |
| 122 | | get_refinement_hierarchy(Abstract,Machines,Abstractions) |
| 123 | | ; otherwise -> |
| 124 | | Abstractions = []). |
| 125 | | find_refinement([M|Rest],Name,Abstract) :- |
| 126 | | ( get_constructed_machine_name(M,Name) -> |
| 127 | | refines(M,Abstract) |
| 128 | | ; otherwise -> |
| 129 | | find_refinement(Rest,Name,Abstract)). |
| 130 | | |
| 131 | | add_refined_machine([_Main,Refined|_],Machines,Old,New) :- |
| 132 | | member(machine(Refined,Body),Machines), |
| 133 | | append_to_section(meta,[refined_machine/Body],Old,New). |
| 134 | | add_refined_machine(_,_,M,M). % not refining |
| 135 | | |
| 136 | | convert_parameters_to_global_sets(Ein,Eout) --> |
| 137 | | % extract and remove parameters and constraints |
| 138 | | select_section(parameters,PP,[]), |
| 139 | | select_section(internal_parameters,IP,[]), |
| 140 | | {create_texpr(truth,pred,[],Truth)}, |
| 141 | | select_section(constraints,C,Truth), |
| 142 | | % split parameters into sets and scalars |
| 143 | | { split_list(is_set_parameter,PP,Sets,Scalars), |
| 144 | | foldl(type_set_parameter,Sets,Ein,Eout) }, |
| 145 | | % put the sets to the deferred sets |
| 146 | | append_to_section(deferred_sets,Sets), |
| 147 | | % and the scalars to the constants |
| 148 | | append_to_section(concrete_constants,Scalars), |
| 149 | | append_to_section(concrete_constants,IP), |
| 150 | | % the scalars should be typed by constraints, |
| 151 | | % so move the constraints to the properties |
| 152 | | select_section(properties,OldProps,NewProps), |
| 153 | | {conjunct_predicates([C,OldProps],NewProps)}. |
| 154 | | is_set_parameter(TExpr) :- |
| 155 | | % upper case identifiers denote set parameters, otherwise scalars |
| 156 | | get_texpr_id(TExpr,Name),is_upper_case(Name). |
| 157 | | type_set_parameter(TExpr,Ein,Eout) :- |
| 158 | | get_texpr_id(TExpr,Name), |
| 159 | | get_texpr_type(TExpr,Type), |
| 160 | | get_texpr_pos(TExpr,Pos), |
| 161 | | % we directly type the deferred set |
| 162 | | unify_types_werrors(set(global(Name)),Type,Pos,Ein,Eout). |
| 163 | | |
| 164 | | |
| 165 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 166 | | % included machines |
| 167 | | |
| 168 | | expand_machines([],_,_,M,M,Errors,Errors). |
| 169 | | expand_machines([M|Rest],Machines,Uses,Typed,Result,Ein,Eout) :- |
| 170 | ? | ~~mnf( expand_machine(M,Machines,Uses,Typed,New,Ein,E1) ), |
| 171 | ? | expand_machines(Rest,Machines,Uses,[machine(M,New)|Typed],Result,E1,Eout). |
| 172 | | |
| 173 | | % resolve all includes and typecheck the machine |
| 174 | | % expand_machine(Name,Machines,TypeChecked,Expanded) : |
| 175 | | % Name of the Machine to expand |
| 176 | | % Machines contains the list of all loaded machines |
| 177 | | % TypeChecked contains the list of all expanded machines so far |
| 178 | | % Expanded is the resulting machine |
| 179 | | expand_machine(Name,Machines,GlobalUses,TypeChecked,Expanded,Ein,Eout) :- |
| 180 | | % find the machine in the list |
| 181 | ? | ~~mnf( find_machine(Name,Machines,MType,Header,RawMachineWithPragmas) ), |
| 182 | | % remove pragmas for later reattachment |
| 183 | ? | ~~mnf( strip_machine_section_pragmas(RawMachineWithPragmas,RawMachine,_Pragmas) ), |
| 184 | | % look for abstract machine |
| 185 | ? | ~~mnf( get_abstractions(Name,Machines,TypeChecked,Abstractions) ), |
| 186 | | % merge all used and seen machines |
| 187 | ? | ~~mnf( use_and_see_machines(RawMachine,TypeChecked,SeenRefs) ), |
| 188 | | % merge all included machines into one machine |
| 189 | | ~~mnf( include_machines(RawMachine, TypeChecked, GlobalUses, Includes, Parameters, Included, Promotes) ), |
| 190 | | % Parameters contains now a list of parameters for each included machine |
| 191 | | % Included contains now a machine that represents all included machines |
| 192 | | % their parameters are renamed to internal_parameters |
| 193 | | append([Abstractions,Included,SeenRefs],RefMachines), |
| 194 | | % typecheck this machine |
| 195 | | debug_stats(type_machine(Name)), |
| 196 | | ~~mnf( type_machine(Header,Name,MType,RawMachine,RefMachines,TypedLocal,RefMachines2,Ein,Err1) ), |
| 197 | | % merge included and including machine |
| 198 | | debug_stats(merge_included_machines(Name)), |
| 199 | | ~~mnf( merge_included_machines(Name,TypedLocal,Included,Promotes,Expanded2,Err1,Err2) ), |
| 200 | | % add some predicates that state the equivalence between arguments |
| 201 | | % in the include statement and the parameters of the included machine |
| 202 | | ~~mnf( add_link_constraints(Includes,MType,Parameters,RefMachines2,Expanded2,Expanded3,Err2,Err3) ), |
| 203 | | % put together refinement and abstraction. |
| 204 | | ~~mnf( merge_refinement_and_abstraction(Expanded3,[ref(local,TypedLocal)|RefMachines2],Expanded4,Err3,Eout)), |
| 205 | | % merge used machines, will also prefix |
| 206 | | debug_stats(merge_used_machines(Name)), |
| 207 | | ~~mnf( merge_used_machines(Included,Expanded4,Expanded5) ), |
| 208 | | % clean up the syntax tree |
| 209 | | debug_stats(clean_up_machine(Name)), |
| 210 | | ~~mnf( clean_up_machine(Expanded5,RefMachines2,Expanded) ), |
| 211 | | debug_stats(finished_clean_up_and_expand_machine(Name)). |
| 212 | | |
| 213 | | strip_machine_section_pragmas(RawMachineWithPragmas,RawMachine,Pragmas) :- |
| 214 | | selectchk(units(_Pos,RealVariables,Pragmas),RawMachineWithPragmas,TRawMachine), !, |
| 215 | | RawMachine = [RealVariables|TRawMachine]. |
| 216 | | strip_machine_section_pragmas(Machine,Machine,[]). |
| 217 | | |
| 218 | | merge_included_machines(Name, TypedLocal, RefMachines, Promotes, Merged, Ein, Eout) :- |
| 219 | | include(is_included_ref,RefMachines,Included), |
| 220 | | create_machine(Name,Empty), |
| 221 | | % move the included operations into the promoted or unpromoted section |
| 222 | | ~~mnf( move_operations(Included,Promotes,Included2,Ein,Eout) ), |
| 223 | | LocalAndIncluded = [ref(local,TypedLocal)|Included2], |
| 224 | | % 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) |
| 225 | | ~~mnf( concat_sections_of_refs([identifiers,initialisation,operation_bodies, |
| 226 | | assertions,used,values],LocalAndIncluded,Empty,Merged1) ), |
| 227 | | ~~mnf( conjunct_sections_of_refs([constraints,properties,invariant],LocalAndIncluded,Merged1,Merged2) ), |
| 228 | | ~~mnf( concat_section_of_simple_lists(freetypes,LocalAndIncluded,Merged2,Merged3) ), |
| 229 | | ~~mnf( get_section(definitions,TypedLocal,Defs) ), |
| 230 | | ~~mnf( write_section(definitions,Defs,Merged3,Merged) ). |
| 231 | | is_included_ref(ref(included,_)). |
| 232 | | |
| 233 | | concat_section_of_simple_lists(Sec,References,In,Out) :- |
| 234 | | maplist(extract_machine_from_ref,References,Machines), |
| 235 | | foldl(concat_section_of_simple_lists2(Sec),Machines,In,Out). |
| 236 | | concat_section_of_simple_lists2(Sec,Machine,In,Out) :- |
| 237 | | get_section(Sec,In,Orig), |
| 238 | | get_section(Sec,Machine,List), |
| 239 | | append(Orig,List,NewList), |
| 240 | | write_section(Sec,NewList,In,Out). |
| 241 | | |
| 242 | | merge_used_machines(RefMachines,Old,New) :- |
| 243 | | % get all included machines from the references |
| 244 | | convlist(ref_to_included_machine,RefMachines,Included), |
| 245 | | foldl(merge_used_machines2,Included,Old,New). |
| 246 | | merge_used_machines2(Included,Old,New) :- |
| 247 | | get_section(used,Included,IncludedUse), |
| 248 | | ( IncludedUse = [] -> New = Old |
| 249 | | ; otherwise -> |
| 250 | | rename_used(IncludedUse,Old,New)). |
| 251 | | ref_to_included_machine(ref(included,Inc),Inc). |
| 252 | | |
| 253 | | % will add prefixes to identifiers |
| 254 | | rename_used(IncludedUse,Old,New) :- |
| 255 | | %print(renaming(IncludedUse)),nl, |
| 256 | | expand_shortcuts([properties,invariant, assertions, |
| 257 | | 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 ? |
| 258 | | foldl(rename_used_sec(IncludedUse),Sections,Old,New). |
| 259 | | rename_used_sec(IncludedUse,Sec,Old,New) :- |
| 260 | | select_section_texprs(Sec,TExprs,NewTExprs,Old,New), |
| 261 | | rename_used2_l(TExprs,IncludedUse,NewTExprs). |
| 262 | | |
| 263 | | rename_used2(TExpr,IncludedUse,NewTExpr) :- |
| 264 | | get_texpr_expr(TExpr,operation(Id,Params,Results,Subst)),!, |
| 265 | | rename_used2_l(Params,IncludedUse,NParams), |
| 266 | | rename_used2_l(Results,IncludedUse,NResults), |
| 267 | | rename_used2(Subst,IncludedUse,NSubst), |
| 268 | | get_texpr_type(TExpr,Type), |
| 269 | | get_texpr_info(TExpr,Info), |
| 270 | | selectchk(modifies(MIn),Info,Info1),selectchk(reads(RIn),Info1,RestInfo), |
| 271 | | rename_used_ids(MIn,IncludedUse,MOut), |
| 272 | | rename_used_ids(RIn,IncludedUse,ROut), |
| 273 | | create_texpr(operation(Id,NParams,NResults,NSubst),Type,[modifies(MOut),reads(ROut)|RestInfo], |
| 274 | | NewTExpr). |
| 275 | | rename_used2(TExpr,IncludedUse,NewTExpr) :- |
| 276 | | % rename identifier by adding machine prefix M.id |
| 277 | | get_texpr_id(TExpr,_), % result is also Id (always ??) |
| 278 | | get_texpr_info(TExpr,Info), |
| 279 | ? | member(usesee(Name,Id,_Mode),Info), |
| 280 | ? | member(includeduse(Name,Id,NewTExpr),IncludedUse), % This seems to reuse position information from includeduse list for all identifiers !! TO DO: check this |
| 281 | | % we now rename Id to Name.Id |
| 282 | | !. %, print(ren_id(Name,Id)),nl. |
| 283 | | rename_used2(TExpr,IncludedUse,NTExpr1) :- |
| 284 | | remove_bt(TExpr,Expr,NExpr,NTExpr), |
| 285 | | syntaxtransformation(Expr,Subs,_,NSubs,NExpr),!, |
| 286 | | rename_used2_l(Subs,IncludedUse,NSubs), |
| 287 | | rename_infos(NTExpr,IncludedUse,NTExpr1). |
| 288 | | rename_used2(TExpr,IncludedUse,NTExpr) :- |
| 289 | | add_internal_error('Rename failed: ',rename_used2(TExpr,IncludedUse,NTExpr)), |
| 290 | | NTExpr = TExpr. |
| 291 | | |
| 292 | | % update infos, e.g., read/modifies for while loops |
| 293 | | rename_infos(b(E,T,I),List,b(E,T,NI)) :- maplist(rename_info(List),I,NI). |
| 294 | | |
| 295 | | rename_info(IncludeUseList,Info,NewInfo) :- info_field_contains_ids(Info,I,NewInfo,SNI),!, |
| 296 | | maplist(rename_usage_info(IncludeUseList),I,NI), sort(NI,SNI). |
| 297 | | rename_info(_,I,I). |
| 298 | | |
| 299 | | info_field_contains_ids(reads(I),I,reads(SNI),SNI). |
| 300 | | info_field_contains_ids(modifies(I),I,modifies(SNI),SNI). |
| 301 | | info_field_contains_ids(non_det_modifies(I),I,non_det_modifies(SNI),SNI). |
| 302 | | info_field_contains_ids(modifies_locals(I),I,modifies_locals(SNI),SNI). |
| 303 | | info_field_contains_ids(reads_locals(I),I,reads_locals(SNI),SNI). |
| 304 | | info_field_contains_ids(used_ids(I),I,used_ids(SNI),SNI). |
| 305 | | |
| 306 | | rename_usage_info(IncludeUseList,ID,NewID) :- |
| 307 | ? | (member(includeduse(_,ID,NewTExpr),IncludeUseList) -> get_texpr_id(NewTExpr,NewID) ; NewID = ID). |
| 308 | | |
| 309 | | |
| 310 | | rename_used2_l([],_,R) :- !, R=[]. |
| 311 | | rename_used2_l([T|Rest],IncludedUse,[NT|NRest]) :- |
| 312 | | rename_used2(T,IncludedUse,NT), !, |
| 313 | | rename_used2_l(Rest,IncludedUse,NRest). |
| 314 | | rename_used2_l(X,Y,Z) :- add_internal_error('Rename failed: ', rename_used2_l(X,Y,Z)),Z=X. |
| 315 | | |
| 316 | | rename_used_ids(InIds,IncludedUse,OutIds) :- |
| 317 | | maplist(rename_used_ids2(IncludedUse),InIds,OutIds). |
| 318 | | rename_used_ids2(IncludedUse,InId,OutId) :- |
| 319 | | memberchk(includeduse(_,InId,TOutId),IncludedUse),!, |
| 320 | | get_texpr_id(TOutId,OutId). |
| 321 | | rename_used_ids2(_IncludedUse,Id,Id). |
| 322 | | |
| 323 | | get_abstractions(CName,Machines,TypedMachines,[ref(abstraction,Abstraction)]) :- |
| 324 | ? | refines(M,AName), |
| 325 | | get_constructed_machine_name(M,CName), |
| 326 | | memberchk(M,Machines),!, |
| 327 | | memberchk(machine(AName,Abstraction),TypedMachines). |
| 328 | | get_abstractions(_,_,_,[]). |
| 329 | | |
| 330 | | get_includes_and_promotes(Sections,M,Includes,Promotes) :- |
| 331 | | optional_rawmachine_section(includes,Sections,[],Includes1), |
| 332 | | optional_rawmachine_section(imports,Sections,[],Imports), |
| 333 | | optional_rawmachine_section(extends,Sections,[],Extends), |
| 334 | | optional_rawmachine_section(promotes,Sections,[],Promotes1), |
| 335 | | append([Includes1,Extends,Imports],Includes), |
| 336 | | maplist(expand_extends(M),Extends,Promotes2), |
| 337 | | append([Promotes1|Promotes2],Promotes). |
| 338 | | expand_extends(Machines,machine_reference(_,Ref,_),Promotes) :- |
| 339 | | split_prefix(Ref,Prefix,Name), |
| 340 | | memberchk(machine(Name,Body),Machines), |
| 341 | | get_section(promoted,Body,Promoted), |
| 342 | | prefix_identifiers(Promoted,Prefix,Renamings), |
| 343 | | rename_bt_l(Promoted,Renamings,TPromotes), |
| 344 | | maplist(add_nonpos,TPromotes,Promotes). |
| 345 | | add_nonpos(TId,identifier(none,Id)) :- |
| 346 | | get_texpr_id(TId,op(Id)). |
| 347 | | |
| 348 | | move_operations([],Promotes,[],Ein,Eout) :- |
| 349 | | foldl(add_promotes_not_found_error,Promotes,Ein,Eout). |
| 350 | | move_operations([ref(_,IncMachine)|IncRest],Promotes,[ref(included,NewIncMachine)|RefRest],Ein,Eout) :- |
| 351 | | move_operations2(IncMachine,Promotes,NewIncMachine,RestPromotes), |
| 352 | | move_operations(IncRest,RestPromotes,RefRest,Ein,Eout). |
| 353 | | move_operations2(Included,Promotes,Result,RestPromotes) :- |
| 354 | | select_section(promoted,IncOperations,Promoted,Included,Included1), |
| 355 | | select_section(unpromoted,OldUnpromoted,Unpromoted,Included1,Result), |
| 356 | | filter_promoted(IncOperations,Promotes,Promoted,NewUnpromoted,RestPromotes), |
| 357 | | append(OldUnpromoted,NewUnpromoted,Unpromoted). |
| 358 | | filter_promoted([],Promotes,[],[],Promotes). |
| 359 | | filter_promoted([TExpr|OpsRest],Promotes,Promoted,Unpromoted,RestPromotes) :- |
| 360 | | get_texpr_id(TExpr,op(P)), |
| 361 | ? | ( select(identifier(_,P),Promotes,RestPromotes1) -> |
| 362 | | !,Promoted = [TExpr|RestPromoted], |
| 363 | | Unpromoted = RestUnpromoted |
| 364 | | ; otherwise -> |
| 365 | | RestPromotes1 = Promotes, |
| 366 | | Promoted = RestPromoted, |
| 367 | | Unpromoted = [TExpr|RestUnpromoted]), |
| 368 | | filter_promoted(OpsRest,RestPromotes1,RestPromoted,RestUnpromoted,RestPromotes). |
| 369 | | add_promotes_not_found_error(identifier(Pos,Id),[error(Msg,Pos)|E],E) :- |
| 370 | | ajoin(['Promoted operation ',Id,' not found'],Msg). |
| 371 | | |
| 372 | | find_machine(Name,Machines,Type,Header,Sections) :- |
| 373 | | Header = machine_header(_,Name,_), |
| 374 | ? | ( (member(abstract_machine(_,_ModelType,Header,Sections),Machines), |
| 375 | | Type=machine) |
| 376 | | ; (member(refinement_machine(_,Header,_Abstract,Sections),Machines), |
| 377 | | Type=refinement) |
| 378 | | ; (member(implementation_machine(_,Header,_Abstract,Sections),Machines), |
| 379 | | Type=implementation)), |
| 380 | | !. |
| 381 | | |
| 382 | | include_machines(RawMachine, TypeChecked, GlobalUses, Includes, Parameters, Included, Promotes) :- |
| 383 | | get_includes_and_promotes(RawMachine,TypeChecked,Includes,Promotes), |
| 384 | | maplist(include_machine(TypeChecked, GlobalUses), Includes, Parameters, Singles), |
| 385 | | remove_duplicate_set_inclusions(Singles,Singles1), |
| 386 | | % create refs |
| 387 | | maplist(create_ref,Singles1,Included). |
| 388 | | create_ref(IncMachine,ref(included,IncMachine)). |
| 389 | | |
| 390 | | % it is possible that a deferred or enumerated set is declared in an included machine |
| 391 | | % that is included more than once. We remove all but one occurrences. |
| 392 | | remove_duplicate_set_inclusions([],[]). |
| 393 | | remove_duplicate_set_inclusions([M],[M]) :- !. |
| 394 | | remove_duplicate_set_inclusions([M|Rest],[M|CleanedRest]) :- |
| 395 | | get_section(deferred_sets,M,DSets), |
| 396 | | get_section(enumerated_sets,M,ESets), |
| 397 | | get_section(enumerated_elements,M,EElements), |
| 398 | | append([DSets,ESets,EElements],Identifiers), |
| 399 | | maplist(remove_duplicate_sets2(Identifiers),Rest,CleanedRest). |
| 400 | | remove_duplicate_sets2(Identifiers,M,Cleaned) :- |
| 401 | | remove_duplicate_sets_section(deferred_sets,Identifiers,M,M1), |
| 402 | | remove_duplicate_sets_section(enumerated_sets,Identifiers,M1,M2), |
| 403 | | remove_duplicate_sets_section(enumerated_elements,Identifiers,M2,Cleaned). |
| 404 | | remove_duplicate_sets_section(Section,Identifiers,In,Out) :- |
| 405 | | select_section(Section,Old,New,In,Out), |
| 406 | | exclude(element_is_duplicate(Identifiers),Old,New). |
| 407 | | element_is_duplicate(Identifiers,TId) :- |
| 408 | | get_texpr_id(TId,Name), |
| 409 | | get_texpr_type(TId,Type), |
| 410 | | get_texpr_id(ToRemove,Name), |
| 411 | | get_texpr_type(ToRemove,Type), |
| 412 | | member(ToRemove,Identifiers), |
| 413 | | get_texpr_info(TId,InfosA), |
| 414 | | get_texpr_info(ToRemove,InfosB), |
| 415 | | member(def(Sec,File),InfosA), |
| 416 | | member(def(Sec,File),InfosB), |
| 417 | | !. |
| 418 | | |
| 419 | | include_machine(TypeChecked,Used,machine_reference(_Pos,FullRef,_Args), |
| 420 | | parameters(FullRef,Parameters), TM) :- |
| 421 | | split_prefix(FullRef,Prefix,Name), |
| 422 | | % TM1 is the already typechecked included machine: |
| 423 | ? | member(machine(Name,TM1),TypeChecked),!, |
| 424 | | debug_println(9,including_machine(Name)), |
| 425 | | % TM2 is a fresh copy, so we prevent unification of the parameter types: |
| 426 | | copy_term(TM1,TM2), |
| 427 | | % If the included machine is used somewhere, we store the identifiers |
| 428 | | % to enable joining the different references later: |
| 429 | | include_usings(Name,Used,TM2,TM3), |
| 430 | | % TM3 is typechecked and all internal variables are renamed with a prefix |
| 431 | | hide_private_information(FullRef,TM3,TM4), |
| 432 | | % TM4 is typechecked, and if it was referenced with a prefix (e.g. INCLUDES p.M2) |
| 433 | | % all variables are prefixed |
| 434 | | %print(prefixing(Prefix)),nl, |
| 435 | | prefix_machine(Prefix,TM4,TM5), |
| 436 | | % We need the parameters later to state their equivilance to the arguments |
| 437 | | get_section(parameters,TM5,Parameters), |
| 438 | | % We move the parameters to the internal parameters, because the resulting |
| 439 | | % machine has only the parameters of the including machine. |
| 440 | | parameters_to_internal(TM5,TM). |
| 441 | | |
| 442 | | include_usings(Name,Uses,Old,New) :- |
| 443 | ? | ( member(Name,Uses) -> |
| 444 | | store_usage_info(Old,Name,UsedInfo), |
| 445 | | append_to_section(used,UsedInfo,Old,New) |
| 446 | | ; otherwise -> |
| 447 | | Old = New). |
| 448 | | % returns a list of which identifiers are used in the machine |
| 449 | | % for each identifier, we have a trible includeuse(Name,Id,TExpr) |
| 450 | | % where Name is the name of the used machine, Id is the |
| 451 | | % original ID and TExpr is the currently used reference to this |
| 452 | | % identifier |
| 453 | | store_usage_info(Machine,Name,UsedInfo) :- |
| 454 | | expand_shortcuts([identifiers],IdSections), |
| 455 | | foldl(store_usage_info2(Machine,Name),IdSections,UsedInfo,[]). |
| 456 | | store_usage_info2(Machine,Name,Sec,I,O) :- |
| 457 | | get_section(Sec,Machine,Content), |
| 458 | | foldl(store_usage_info3(Name),Content,I,O). |
| 459 | | store_usage_info3(Name,TId,[includeduse(Name,Id,TId)|L],L) :- |
| 460 | | get_texpr_id(TId,Id). |
| 461 | | |
| 462 | | % conjunct sections that contain predicates |
| 463 | | conjunct_sections_of_refs(Sections1,References,Old,New) :- |
| 464 | | expand_shortcuts(Sections1,Sections), |
| 465 | | maplist(extract_machine_from_ref,References,Machines), |
| 466 | | foldl(conjunct_sections2(Machines),Sections,Old,New). |
| 467 | | conjunct_sections2(Machines,Section,Old,New) :- |
| 468 | | write_section(Section,NewContent,Old,New), |
| 469 | | get_section_of_machines(Machines,Section,Preds), |
| 470 | | conjunct_predicates(Preds,NewContent). |
| 471 | | |
| 472 | | % merge sections that contain a list of expressions |
| 473 | | concat_sections_of_refs(Sections1,References,Old,New) :- |
| 474 | | maplist(extract_machine_from_ref,References,Machines), |
| 475 | | % for each machine, create a tag where the expression comes from |
| 476 | | maplist(create_tag_by_reference,References,Tags), |
| 477 | | concat_sections(Sections1,Machines,Tags,Old,New). |
| 478 | | extract_machine_from_ref(ref(_,M),M). |
| 479 | | create_tag_by_reference(ref(local,_Machine),[]) :- !. |
| 480 | | create_tag_by_reference(ref(RefType,Machine),[RefType/Name]) :- |
| 481 | | get_machine_name(Machine,Name). |
| 482 | | concat_sections(Sections1,Machines,Tags,Old,New) :- |
| 483 | | expand_shortcuts(Sections1,Sections), |
| 484 | | foldl(concat_section2(Machines,Tags),Sections,Old,New). |
| 485 | | concat_section2(Machines,Tags,Section,Old,New) :- |
| 486 | | write_section(Section,NewContent,Old,New), |
| 487 | | maplist(get_tagged_lsection_of_machine(Section),Machines,Tags,Contents), |
| 488 | | append(Contents,NewContent). |
| 489 | | get_tagged_lsection_of_machine(Section,Machine,Tags,TaggedContent) :- |
| 490 | | get_section(Section,Machine,Content), |
| 491 | | maplist(tag_with_origin(Tags),Content,TaggedContent). |
| 492 | | tag_with_origin(Origins,TExpr,TaggedExpr) :- |
| 493 | | change_info_of_expression_or_init(TExpr,Info,TaggedInfo,TaggedExpr), |
| 494 | | % add a new origin to the old tag or if not existent, add a new info field |
| 495 | | ( Origins = [] -> TaggedInfo = Info |
| 496 | | ; selectchk(origin(Orest),Info,origin(Onew),TaggedInfo) -> append(Origins,Orest,Onew) |
| 497 | | ; otherwise -> TaggedInfo = [origin(Origins)|Info]). |
| 498 | | % the substitutions in the initialisation are additionally wrapped by an init/2 term |
| 499 | | % a small hack to work with those to. |
| 500 | | % TODO: this became a very ugly hack -- redo! |
| 501 | | change_info_of_expression_or_init(init(A,OExpr),Old,New,init(A,NExpr)) :- |
| 502 | | !,change_info_of_expression_or_init(OExpr,Old,New,NExpr). |
| 503 | | % ignore the info for includeduse/3 completely |
| 504 | | change_info_of_expression_or_init(includeduse(A,B,C),[],_,includeduse(A,B,C)) :- !. |
| 505 | | change_info_of_expression_or_init(OExpr,Old,New,NExpr) :- |
| 506 | | create_texpr(Expr,Type,Old,OExpr), create_texpr(Expr,Type,New,NExpr). |
| 507 | | |
| 508 | | |
| 509 | | % adds a prefix to all variables and promoted operations |
| 510 | | prefix_machine('',TM,TM) :- !. |
| 511 | | prefix_machine(Prefix,Old,New) :- |
| 512 | | debug_println(5,prefixing_machine(Prefix)), |
| 513 | | expand_shortcuts([variables,promoted], RenamedIdentiferSections), |
| 514 | | get_all_identifiers(RenamedIdentiferSections,Old,Identifiers), |
| 515 | | prefix_identifiers(Identifiers,Prefix,Renamings), |
| 516 | | find_relevant_sections(RenamedIdentiferSections,[machine],Sections1), |
| 517 | | append(RenamedIdentiferSections,Sections1,Sections), |
| 518 | | rename_in_sections(Sections,Renamings,Old,M), |
| 519 | | rename_includeduse(M,Renamings,New). |
| 520 | | rename_includeduse(Old,Renamings,New) :- |
| 521 | | select_section(used,OldContent,NewContent,Old,New), |
| 522 | | maplist(rename_includeduse2(Renamings),OldContent,NewContent). |
| 523 | | rename_includeduse2(Renamings,includeduse(M,N,TExpr),includeduse(M,N,NExpr)) :- |
| 524 | | rename_bt(TExpr,Renamings,NExpr). |
| 525 | | |
| 526 | | get_all_identifiers(Sections1,M,Identifiers) :- |
| 527 | | expand_shortcuts(Sections1,Sections), |
| 528 | | maplist(get_all_identifiers2(M),Sections,LIdentifiers), |
| 529 | | append(LIdentifiers,Identifiers). |
| 530 | | get_all_identifiers2(M,Sec,Identifiers) :- |
| 531 | | get_section(Sec,M,Identifiers). |
| 532 | | |
| 533 | | % hide all parameters and unpromoted operations |
| 534 | | hide_private_information(Prefix,Machine,NewMachine) :- |
| 535 | | get_section(parameters,Machine,Params), |
| 536 | | get_section(unpromoted,Machine,UnPromoted), |
| 537 | | append(Params,UnPromoted,ToHide), |
| 538 | | %debug_println(9,hide_private(Prefix,ToHide)), |
| 539 | | ( ToHide = [] -> NewMachine=Machine |
| 540 | | ; otherwise -> |
| 541 | | prefix_identifiers(ToHide,Prefix,Renamings), |
| 542 | | % we have to do the renaming in promoted operations, too, because |
| 543 | | % those operations might use the renamed parameters and their reads/modifies |
| 544 | | % info must be updated |
| 545 | | rename_in_sections([parameters,promoted,unpromoted],Renamings,Machine,Machine1), |
| 546 | | rename_includeduse(Machine1,Renamings,Machine2), |
| 547 | | rename_relevant_sections([parameters,operations],Renamings,Machine2,NewMachine)). |
| 548 | | |
| 549 | | prefix_identifiers(Identifiers,'',Identifiers) :- !. |
| 550 | | prefix_identifiers(Old,Prefix,New) :- |
| 551 | | maplist(prefix_identifier(Prefix),Old,New). |
| 552 | | prefix_identifier(Prefix,TExpr,rename(Old,New)) :- |
| 553 | | get_texpr_expr(TExpr,identifier(Old)), |
| 554 | | ( Old=op(OI) -> New=op(NI) |
| 555 | | ; otherwise -> OI=Old,NI=New), |
| 556 | | ajoin([Prefix,'.',OI],NI). % , print(rename(Old,New)),nl. |
| 557 | | |
| 558 | | parameters_to_internal(M1,M2) :- |
| 559 | | select_section(internal_parameters,OldParams,Params,M1,M3), |
| 560 | | select_section(parameters,NewParams,[],M3,M2), |
| 561 | | append(OldParams,NewParams,Params). |
| 562 | | |
| 563 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 564 | | % uses and sees relations |
| 565 | | find_uses(Machines,Uses,NotIncluded,Ein,Eout) :- |
| 566 | | findall(U, use_usage(Machines,_,U), UnsortedUses), |
| 567 | | sort(UnsortedUses,Uses), |
| 568 | | check_include_use(Uses,Machines,NotIncluded,Ein,Eout). |
| 569 | | |
| 570 | | % check_include_use/5 checks if the used machines are included in any machine |
| 571 | | % check_include_use(+Uses,+Machines,-NotIncluded,Ein,Eout) |
| 572 | | % Uses: The list of machine names that are used |
| 573 | | % Machines: The list of machines |
| 574 | | % NotIncluded: The list of used machines (their names) that are not included |
| 575 | | % Ein/Eout: The errors (as difference-list) |
| 576 | | check_include_use([],_,[],Errors,Errors). |
| 577 | | check_include_use([U|Rest],Machines,NotIncluded,Ein,Eout) :- |
| 578 | | findall(I,include_usage(Machines,U,I),Inc), |
| 579 | | ( Inc=[] -> NotIncluded = [U|RestNotIncluded], Ein=E1 |
| 580 | | ; Inc=[_] -> NotIncluded = RestNotIncluded, Ein=E1 |
| 581 | | ; otherwise -> |
| 582 | | NotIncluded = RestNotIncluded, |
| 583 | | use_usage(Machines,Pos,U), |
| 584 | | Ein = [error('used machine is included more than once',Pos)|E1] |
| 585 | | ), |
| 586 | | check_include_use(Rest,Machines,RestNotIncluded,E1,Eout). |
| 587 | | % extend_not_included_uses(+Uses,+Main,-Name,+Machines,-AllMachines): |
| 588 | | % Create a dummy machine that extends the main machine and extends or includes |
| 589 | | % all seen/used machines that are not included if such machines exist. |
| 590 | | % In case of refinement this is done for the whole refinement chain. |
| 591 | | % Uses: List of machine names of the machines that are used/seen but not included |
| 592 | | % Main: The name of the main machine |
| 593 | | % Name: The name of the generated dummy machine (or Main if no dummy machine is generated) |
| 594 | | % Machines: List of all specified Machines |
| 595 | | % AllMachines: List of all Machines + the new dummy machine(s) |
| 596 | | extend_not_included_uses([],Main,Main,Machines,Machines) :- !. |
| 597 | | extend_not_included_uses(Uses,Main,Name,Machines,AllMachines) :- |
| 598 | | get_refinement_hierarchy(Main,Machines,RefChain), |
| 599 | | maplist(extend_not_included_uses2(Uses,Machines),RefChain,NewMachines), |
| 600 | | append(NewMachines,Machines,AllMachines), |
| 601 | | dummy_machine_name(Main,Name). |
| 602 | | extend_not_included_uses2(Uses,Machines,Name,DummyMachine) :- |
| 603 | | create_dummy_machine(Name,Machines,Parameters,DummyParameters,Sections,DummyMachine), |
| 604 | | IncludeMain = machine_reference(none,Name,Parameters), |
| 605 | | ( get_preference(seen_machines_included,true) -> |
| 606 | | % extend just the main machine, include the used/seen machines |
| 607 | | References = [extends(none,[IncludeMain]),includes(none,UReferences)] |
| 608 | | ; otherwise -> |
| 609 | | % extends the main machine and all used/seen machines |
| 610 | | References = [extends(none,[IncludeMain|UReferences])]), |
| 611 | | maplist(find_using(Machines),Uses,UReferences,LUParameters), |
| 612 | | append([Parameters|LUParameters],DummyParameters), |
| 613 | | copy_raw_definitions(Name,Machines,OptDefs), |
| 614 | | % we store a flag "is_dummy" in the machine because we have a special case |
| 615 | | % later, see type_constraints/7. |
| 616 | | append([References,[is_dummy],OptDefs],Sections). |
| 617 | | create_dummy_machine(Name,Machines,Parameters,DummyParameters,Sections,DummyMachine) :- |
| 618 | | dummy_machine_name(Name,DummyName), |
| 619 | ? | get_raw_model_type(Name,Machines,ModelType), |
| 620 | | Header = machine_header(_,Name,Parameters), |
| 621 | | DummyHeader = machine_header(none,DummyName,DummyParameters), |
| 622 | ? | member(Machine,Machines), |
| 623 | | generate_raw_machine(Header,DummyHeader,ModelType,Sections,Machine,DummyMachine),!. |
| 624 | | |
| 625 | | generate_raw_machine(OldHeader,NewHeader,_,NewSections, |
| 626 | | abstract_machine(_, ModelType,OldHeader,_), |
| 627 | | abstract_machine(none,ModelType,NewHeader,NewSections)). |
| 628 | | generate_raw_machine(OldHeader,NewHeader,ModelType,NewSections, |
| 629 | | refinement_machine(_, OldHeader,_Abstract, _), |
| 630 | | abstract_machine(none,ModelType,NewHeader,NewSections)). |
| 631 | | generate_raw_machine(OldHeader,NewHeader,ModelType,NewSections, |
| 632 | | implementation_machine(_, OldHeader,_Abstract, _), |
| 633 | | abstract_machine(none,ModelType,NewHeader,NewSections)). |
| 634 | | dummy_machine_name(Name,DummyName) :- |
| 635 | | atom_concat('MAIN_MACHINE_FOR_',Name,DummyName). |
| 636 | | |
| 637 | | find_using(Machines,U,machine_reference(none,Name,Arguments),Arguments) :- |
| 638 | | % was using(U).U |
| 639 | | ajoin([U,'.',U],Name), |
| 640 | ? | member(M,Machines), get_machine_parameters(M,U,Params),!, |
| 641 | | maplist(add_use_param,Params,Arguments). |
| 642 | | add_use_param(identifier(_,Param),identifier(none,Name)) :- |
| 643 | | ( is_upper_case(Param) -> |
| 644 | | ajoin(['Useparam(',Param,')'],Name) |
| 645 | | ; otherwise -> |
| 646 | | ajoin(['useparam(',Param,')'],Name)). |
| 647 | | |
| 648 | | % copy_raw_definitions(+Name,+Machines,-OptDefs): |
| 649 | | % Get the definitions section from a raw (untyped) machine |
| 650 | | % Name: Name of the machine |
| 651 | | % Machines: List of Machines |
| 652 | | % OptDefs: [] if no definitions are present or [Def] if a definition section Def is present |
| 653 | | copy_raw_definitions(Name,Machines,OptDefs) :- |
| 654 | ? | get_constructed_machine_name_and_body(M,Name,_,Sections), |
| 655 | | memberchk(M,Machines),!, |
| 656 | | Def = definitions(_,_), |
| 657 | | ( memberchk(Def,Sections) -> |
| 658 | | OptDefs = [Def] |
| 659 | | ; otherwise -> |
| 660 | | OptDefs = []). |
| 661 | | |
| 662 | | add_def_dependency_information(DefsIn,DefsOut,Ein,Eout) :- |
| 663 | | extract_def_name_set(DefsIn,DefNames,DN), |
| 664 | | maplist(add_def_dep(DN),DefsIn,Defs1), |
| 665 | | check_for_cyclic_def_dependency(Defs1,DefNames,DefsOut,Ein,Eout). |
| 666 | | |
| 667 | | extract_def_name_set(Defs,DefNames,DN) :- |
| 668 | | maplist(get_def_name,Defs,DefNames), |
| 669 | | maplist(to_mapset_entry,DefNames,DN1), |
| 670 | | list_to_avl(DN1,DN). |
| 671 | | |
| 672 | | get_def_name(Def,Name) :- arg(1,Def,Name). |
| 673 | | get_def_pos(Def,Pos) :- arg(3,Def,Pos). |
| 674 | | get_def_dependencies(Def,Dependencies) :- arg(6,Def,Dependencies). |
| 675 | | to_mapset_entry(Name,Name-true). |
| 676 | | |
| 677 | | add_def_dep(DN,In,Out) :- |
| 678 | | analyse_definition_dependencies(In,DN,Deps), |
| 679 | | In = definition_decl(Name,DefType,Pos,Args,RawExpr), |
| 680 | | Out = definition_decl(Name,DefType,Pos,Args,RawExpr,Deps). |
| 681 | | |
| 682 | | check_for_cyclic_def_dependency(Defs,DefNames,DefsOut,Ein,Eout) :- |
| 683 | | % check if we have a cyclic definition: |
| 684 | | create_definitions_avl(Defs,DefsAvl), |
| 685 | | search_for_cyclic_definition(DefNames,DefsAvl,[],Pos,RCycle),!, |
| 686 | | % if we have found a cyclic definition, generate an error message, ... |
| 687 | | reverse(RCycle,Cycle),add_arrows(Cycle,Msg0), |
| 688 | | ajoin(['Found cyclic definitions: '|Msg0],Msg), |
| 689 | | Ein = [error(Msg,Pos)|E1], |
| 690 | | % ... remove the definitions in the cycle (to prevent later infinite loops) ... |
| 691 | | exclude(definition_in_list(Cycle),Defs,Defs1), |
| 692 | | % ... and check the remaining definitions. |
| 693 | | check_for_cyclic_def_dependency(Defs1,DefNames,DefsOut,E1,Eout). |
| 694 | | check_for_cyclic_def_dependency(Defs,_DefNames,Defs,E,E). |
| 695 | | add_arrows([E],[E]) :- !. |
| 696 | | add_arrows([E|Erest],[E,'->'|Arest]) :- add_arrows(Erest,Arest). |
| 697 | | definition_in_list(List,Def) :- |
| 698 | | get_def_name(Def,Name),memberchk(Name,List). |
| 699 | | |
| 700 | | create_definitions_avl(Defs,DefsAvl) :- |
| 701 | | maplist(split_def_name,Defs,Entries), |
| 702 | | list_to_avl(Entries,DefsAvl). |
| 703 | | split_def_name(Def,Name-Def) :- get_def_name(Def,Name). |
| 704 | | |
| 705 | | |
| 706 | | % just a depth-first search to find a cycle |
| 707 | | search_for_cyclic_definition(DefNames,Definitions,Visited,Pos,Cycle) :- |
| 708 | ? | member(Name,DefNames),avl_fetch(Name,Definitions,Definition), |
| 709 | | get_def_pos(Definition,Pos), |
| 710 | | ( memberchk(Name,Visited) -> |
| 711 | | Cycle = [Name|Visited] |
| 712 | | ; otherwise -> |
| 713 | | get_def_dependencies(Definition,Dependencies), |
| 714 | | search_for_cyclic_definition(Dependencies,Definitions,[Name|Visited],_,Cycle) |
| 715 | | ). |
| 716 | | |
| 717 | | :- assert_must_succeed(( |
| 718 | | list_to_avl([def1-true,def2-true,def3-true,def4-true],DefNames), |
| 719 | | analyse_definition_dependencies( |
| 720 | | conjunct(none, |
| 721 | | equals(none, |
| 722 | | identifier(none,x), |
| 723 | | identifier(none,def1)), |
| 724 | | equals(none, |
| 725 | | definition(none,def4, |
| 726 | | [function(none, |
| 727 | | identifier(none,def3), |
| 728 | | integer(none,5))]), |
| 729 | | identifier(y))),DefNames,Defs), |
| 730 | | Defs==[def1,def3,def4] |
| 731 | | )). |
| 732 | | % analyse_definition_dependencies(+Expr,+DefinitionNames,Deps): |
| 733 | | % Expr: raw (i.e. untyped) expression to analyse |
| 734 | | % DN: AVL set (i.e. mapping from elements to 'true') of the names of the definitions |
| 735 | | % This is needed to decide if an identifier is a reference to a definition |
| 736 | | % Deps: A list of used definitions (a list of their names) |
| 737 | | analyse_definition_dependencies(Expr,DN,Deps) :- |
| 738 | | analyse_definition_dependencies2(Expr,DN,Unsorted,[]), |
| 739 | | sort(Unsorted,Deps). |
| 740 | | analyse_definition_dependencies2(VAR,_DN) --> {var(VAR)},!, |
| 741 | | {add_internal_error('Variable DEFINITION expression in',analyse_definition_dependencies)}. |
| 742 | | analyse_definition_dependencies2([Expr|Rest],DN) --> |
| 743 | | !, analyse_definition_dependencies2(Expr,DN), |
| 744 | | analyse_definition_dependencies2(Rest,DN). |
| 745 | | analyse_definition_dependencies2(definition(_Pos,Name,Args),DN) --> |
| 746 | | !,[Name],analyse_definition_dependencies2(Args,DN). |
| 747 | | analyse_definition_dependencies2(identifier(_Pos,Name),DN) --> |
| 748 | | {avl_fetch(Name,DN),!},[Name]. |
| 749 | | analyse_definition_dependencies2(Expr,DN) --> |
| 750 | | { compound(Expr),functor(Expr,_Functor,Arity),!}, |
| 751 | | analyse_definition_dependencies_arg(2,Arity,Expr,DN). |
| 752 | | analyse_definition_dependencies2(_Expr,_DN) --> []. |
| 753 | | |
| 754 | | analyse_definition_dependencies_arg(I,Arity,Expr,DN) --> |
| 755 | | { I =< Arity,!,arg(I,Expr,Arg),I2 is I+1 }, |
| 756 | | analyse_definition_dependencies2(Arg,DN), |
| 757 | | analyse_definition_dependencies_arg(I2,Arity,Expr,DN). |
| 758 | | analyse_definition_dependencies_arg(_I,_Arity,_Expr,_DN) --> []. |
| 759 | | |
| 760 | | |
| 761 | | |
| 762 | | get_constructed_machine_name(MachineTerm,Name) :- get_constructed_machine_name_and_body(MachineTerm,Name,_Pos,_). |
| 763 | | % name and pos; pos can be used for filenumber |
| 764 | | get_constructed_machine_name_and_filenumber(MachineTerm,Name,Filenumber) :- |
| 765 | | get_constructed_machine_name_and_body(MachineTerm,Name,Pos,_), |
| 766 | | (Pos = pos(_,FN,_Srow,_Scol,_Erow,_Ecol) -> Filenumber=FN ; Filenumber=unknown). |
| 767 | | get_constructed_machine_name_and_body(abstract_machine(_,_ModelType,machine_header(Pos,Name,_),Body),Name,Pos,Body). |
| 768 | | get_constructed_machine_name_and_body(refinement_machine(_,machine_header(Pos,Name,_),_Abstract,Body),Name,Pos,Body). |
| 769 | | get_constructed_machine_name_and_body(implementation_machine(_,machine_header(Pos,Name,_),_Abstract,Body),Name,Pos,Body). |
| 770 | | |
| 771 | | refines(refinement_machine(_,machine_header(_,_Name,_),Abstract,_Body),Abstract). |
| 772 | | refines(implementation_machine(_,machine_header(_,_Name,_),Abstract,_Body),Abstract). |
| 773 | | |
| 774 | | get_machine_parameters(abstract_machine(_,_ModelType,machine_header(_,Name,Parameters),_),Name,Parameters). |
| 775 | | get_machine_parameters(refinement_machine(_,machine_header(_,Name,Parameters),_,_),Name,Parameters). |
| 776 | | get_machine_parameters(implementation_machine(_,machine_header(_,Name,Parameters),_,_),Name,Parameters). |
| 777 | | |
| 778 | | get_raw_model_type(Main,Machines,ModelType) :- |
| 779 | ? | get_constructed_machine_name_and_body(M,Main,_,_), |
| 780 | | memberchk(M,Machines), |
| 781 | | ( refines(M,RefName) -> |
| 782 | | get_raw_model_type(RefName,Machines,ModelType) |
| 783 | | ; otherwise -> |
| 784 | | M = abstract_machine(_,ModelType,_,_)). |
| 785 | | |
| 786 | | some_machine_name_body(Machines,M,Name,Body) :- |
| 787 | ? | member(M,Machines), |
| 788 | | get_constructed_machine_name_and_body(M,Name,_,Body). |
| 789 | | |
| 790 | | use_usage(Machines,Pos,Use) :- |
| 791 | ? | some_machine_name_body(Machines,_,_,Body), |
| 792 | ? | ( member(sees(Pos,R),Body) |
| 793 | | ; member(uses(Pos,R),Body)), |
| 794 | ? | member(identifier(_,PrefixUse),R), |
| 795 | | split_prefix(PrefixUse,_,Use). |
| 796 | | % include_usage/3 checks if there is any machine in Machines that |
| 797 | | % includes/extends/imports the used machine |
| 798 | | % include_usage(+Machines,+Use,-Name): |
| 799 | | % Machines: The list of machines |
| 800 | | % Use: The name of the used machine |
| 801 | | % Name: The name of the machine that imports the used machine |
| 802 | | % include_usage/3 fails if there is not such an import |
| 803 | | include_usage(Machines,Use,Name) :- |
| 804 | ? | some_machine_name_body(Machines,_,Name,Body), |
| 805 | | ( member(includes(_,R),Body) |
| 806 | | ; member(extends(_,R), Body) |
| 807 | | ; member(imports(_,R), Body)), |
| 808 | | member(machine_reference(_Pos,PrefixRef,_),R), |
| 809 | | % The name could be prefixed, we need it without prefix: |
| 810 | | split_prefix(PrefixRef,_,Use). |
| 811 | | |
| 812 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 813 | | % uses and sees clauses |
| 814 | | |
| 815 | | % returns a list of references to used and seen machines |
| 816 | | % the machines contain only identifier sections and |
| 817 | | % the identifier are prefixed accordingly |
| 818 | | % all identifier are marked as coming from a seen/used machine |
| 819 | | use_and_see_machines(Sections,Machines,References) :- |
| 820 | ? | get_uses_and_sees(Sections,Uses,Sees), |
| 821 | ? | maplist(use_or_see_machine(used,Machines),Uses,Used), |
| 822 | ? | maplist(use_or_see_machine(seen,Machines),Sees,Seen), |
| 823 | | append(Used,Seen,References). |
| 824 | | |
| 825 | | % get uses and sees sections from the untyped machines |
| 826 | | get_uses_and_sees(Sections,Uses,Sees) :- |
| 827 | | get_uses_or_sees2(sees,Sections,Sees), |
| 828 | | get_uses_or_sees2(uses,Sections,Uses). |
| 829 | | get_uses_or_sees2(Mode,Sections,US) :- |
| 830 | | optional_rawmachine_section(Mode,Sections,[],US1), |
| 831 | | findall(I,member(identifier(_,I),US1),US). |
| 832 | | |
| 833 | | use_or_see_machine(Mode,TypedMachines,Ref,ref(Mode,Result)) :- |
| 834 | ? | split_prefix(Ref,Prefix,Name), |
| 835 | ? | memberchk(machine(Name,Typed),TypedMachines), |
| 836 | ? | create_machine(Name,Empty), |
| 837 | ? | use_sections([sets],Mode,'',Name,Typed,Empty,M1), |
| 838 | ? | use_sections([constants,variables,promoted],Mode,Prefix,Name,Typed,M1,Result). |
| 839 | | use_sections(Sections,Mode,Prefix,MName,Typed,Old,New) :- |
| 840 | ? | expand_shortcuts(Sections,AllSections), |
| 841 | ? | foldl(use_section(Mode,Prefix,MName,Typed),AllSections,Old,New). |
| 842 | | use_section(Mode,Prefix,MName,Machine,Section,OldM,NewM) :- |
| 843 | ? | get_section_texprs(Section,Machine,Identifiers), |
| 844 | | write_section(Section,NewIds,OldM,NewM), |
| 845 | | ( Prefix='' -> |
| 846 | | Ids1=Identifiers |
| 847 | | ; otherwise -> |
| 848 | | prefix_identifiers(Identifiers,Prefix,Renamings), |
| 849 | | rename_bt_l(Identifiers,Renamings,Ids1)), |
| 850 | | maplist(add_use_info_to_identifier(Mode,MName),Ids1,NewIds). |
| 851 | | add_use_info_to_identifier(Mode,Name,TExpr,New) :- |
| 852 | | get_texpr_id(TExpr,PId), get_texpr_type(TExpr,Type), |
| 853 | | get_texpr_id(New,PId), get_texpr_type(New,Type), |
| 854 | | split_prefix(PId,_Prefix,Id), |
| 855 | | get_texpr_info(TExpr,Info), |
| 856 | | get_texpr_info(New,[usesee(Name,Id,Mode)|Info]). |
| 857 | | |
| 858 | | |
| 859 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 860 | | % add a section to the machine that describes the linking of |
| 861 | | % parameters and arguments |
| 862 | | add_link_constraints(Includes,MType,Parameters,RefMachines,Old,New,Ein,Eout) :- |
| 863 | | AllRefMachines = [ref(local,Old)|RefMachines], |
| 864 | | extract_parameter_types(RefMachines,NonGroundExceptions), |
| 865 | | foldl(add_link_section(MType,Parameters,AllRefMachines,NonGroundExceptions), |
| 866 | | Includes,Links/Ein,[]/Eout), % TO DO: Daniel check if [] is correct here |
| 867 | | %print(conjunct_predicates(Links,Link)),nl, |
| 868 | | conjunct_predicates(Links,Link), |
| 869 | | select_section(constraints,OConstraints,NConstraints,Old,New), |
| 870 | | conjunct_predicates([Link,OConstraints],NConstraints). |
| 871 | | add_link_section(MType,Parameters,RefMachines,NonGroundExceptions, |
| 872 | | machine_reference(Pos,Ref,Args),Links/Ein,RLinks/Eout) :- |
| 873 | | visible_env(MType,includes,RefMachines,Env,Ein,E1), |
| 874 | | memberchk(parameters(Ref,TParameters),Parameters), |
| 875 | | ( same_length(TParameters, Args) -> |
| 876 | | get_texpr_types(TParameters,Types), |
| 877 | | btype_ground_dl(Args,Env,NonGroundExceptions,Types,TArgs,E1,Eout), |
| 878 | | maplist(create_equality,TParameters,TArgs,LLinks) |
| 879 | | ; otherwise -> |
| 880 | | E1 = [error('wrong number of machine arguments',Pos)|Eout], |
| 881 | | LLinks = []), |
| 882 | | append(LLinks,RLinks,Links). |
| 883 | | create_equality(P,A,E) :- |
| 884 | | create_texpr(equal(P,A),pred,[parameterlink],E). |
| 885 | | |
| 886 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 887 | | % type machines |
| 888 | | |
| 889 | | type_machine(Header,Name,MType,RawMachine,RefMachines,TypedMachine,NewRefMachines,Ein,Eout) :- |
| 890 | | Header = machine_header(_,Name,_), |
| 891 | | create_machine(Name,Empty), |
| 892 | | % (optional) definitions |
| 893 | | extract_definitions(RawMachine,Empty,DefsOnly,Ein,E0), |
| 894 | | debug_stats(extracted_definitions(Name)), |
| 895 | | % create the identifiers that will be typed, |
| 896 | | % Local will contain the identifier sections |
| 897 | | ~~mnf( create_id_sections(Header,RawMachine,Name,DefsOnly,Local)), |
| 898 | | debug_stats(created_identifier_sections(Name)), |
| 899 | | ~~mnf( create_freetypes(RawMachine,MType,RefMachines,Local,Local1,E0,E1)), |
| 900 | | % in case of a refinement, check if all newly defined operations are refinements |
| 901 | | ~~mnf( link_to_refinement(MType,RawMachine,RefMachines,Local1,Local2,E1,E2)), |
| 902 | | % extract types that can be variables |
| 903 | | debug_stats(created_link_to_refinement(Name)), |
| 904 | | ~~mnf(extract_parameter_types([ref(local,Local2)|RefMachines],NonGroundExceptions)), |
| 905 | | % check for a VALUES clause. They are a little bit tricky because they can replace |
| 906 | | % already defined deferred sets by integers or other deferred sets |
| 907 | | process_values_section(MType,RawMachine,NonGroundExceptions, |
| 908 | | Local2/E2/RefMachines,Local3/E3/NewRefMachines), |
| 909 | | % type-check the other sections (properties, invariant, operation_bodies, etc) |
| 910 | | ~~mnf( type_sections(RawMachine,MType,[ref(local,Local3)|NewRefMachines],NonGroundExceptions, |
| 911 | | Name,E3,Eout,Local3,TypedMachine)). |
| 912 | | |
| 913 | | extract_definitions(RawMachine,In,Out,Ein,Eout) :- |
| 914 | | optional_rawmachine_section(definitions,RawMachine,[],AllDefinitions), |
| 915 | | write_section(definitions,Definitions,In,Out), |
| 916 | | % remove all references to definition files from definitions |
| 917 | | exclude(is_file_definition,AllDefinitions,Definitions1), |
| 918 | | % replace expression_definition(...) by defintion(expression,...), etc. |
| 919 | | change_definition_style(Definitions1,Definitions2), |
| 920 | | % analyse dependencies |
| 921 | | add_def_dependency_information(Definitions2,Definitions3,Ein,Eout), |
| 922 | | % replace external function definitions by calls to the external function |
| 923 | | replace_external_declarations(Definitions3,Definitions). |
| 924 | | |
| 925 | | is_file_definition(file_definition(_Pos,_Filename)). |
| 926 | | |
| 927 | | change_definition_style(DefsIn,DefsOut) :- |
| 928 | | maplist(change_definition_style2,DefsIn,DefsOut). |
| 929 | | change_definition_style2(conversion(Pos,InnerDef),definition_decl(Name,DefType,InnerPos,Args,conversion(Pos,RawExpr))) :- |
| 930 | | change_definition_style2(InnerDef,definition_decl(Name,DefType,InnerPos,Args,RawExpr)). |
| 931 | | change_definition_style2(Def,definition_decl(Name,DefType,Pos,Args,RawExpr)) :- |
| 932 | | Def =.. [Functor,Pos,Name,Args,RawExpr], |
| 933 | | maplist(check_def_argument(Name,Pos),Args), |
| 934 | | map_def_functor(Functor,DefType). |
| 935 | | map_def_functor(expression_definition,expression). |
| 936 | | map_def_functor(substitution_definition,substitution). |
| 937 | | map_def_functor(predicate_definition,predicate). |
| 938 | | |
| 939 | | % check formal arguments of definitions , e.g., here xx in square2 is not an identifier: xx == 20; square2(xx) == xx*xx |
| 940 | | check_def_argument(_,_,identifier(_,_)) :- !. |
| 941 | | check_def_argument(DefName,DefPos,definition(_,ID,_)) :- !, |
| 942 | | tools:ajoin(['Formal parameter ', ID, ' is a definition call in Definition: '],Msg), |
| 943 | | add_error(bmachine_construction,Msg,DefName,DefPos). |
| 944 | | check_def_argument(DefName,DefPos,FP) :- !, |
| 945 | | tools:ajoin(['Formal parameter ', FP, ' is not an identifier in Definition: '],Msg), |
| 946 | | add_error(bmachine_construction,Msg,DefName,DefPos). |
| 947 | | |
| 948 | | replace_external_declarations(Definitions,NewDefs) :- |
| 949 | | split_list(is_external_declaration,Definitions,ExtFunctionDecls,RestDefs), |
| 950 | | foldl(replace_external_declaration,ExtFunctionDecls,RestDefs,NewDefs). |
| 951 | | is_external_declaration(definition_decl(DefName,expression,_Pos,_Params,_Def,_Dependencies)) :- |
| 952 | ? | external_name(DefName,ExtType,_ExpectedDefType,_ExtCall,FunName), |
| 953 | | (debug_mode(on) -> format('external ~w declared: ~w~n', [ExtType,FunName]) ; true). |
| 954 | | external_name(DefName,function,expression,external_function_call,FunName) :- |
| 955 | | atom_concat('EXTERNAL_FUNCTION_',FunName,DefName). |
| 956 | | external_name(DefName,predicate,predicate,external_pred_call,FunName) :- |
| 957 | | atom_concat('EXTERNAL_PREDICATE_',FunName,DefName). |
| 958 | | external_name(DefName,substitution,substitution,external_subst_call,FunName) :- |
| 959 | | atom_concat('EXTERNAL_SUBSTITUTION_',FunName,DefName). |
| 960 | | replace_external_declaration(definition_decl(DefName,expression,DefPos,TypeParams,Decl,_Deps),In,Out) :- |
| 961 | | OldDefinition = definition_decl(FunName,ExpectedDefType,Pos,FunParams,FunDef,Deps), |
| 962 | | NewDefinition = definition_decl(FunName,ExpectedDefType,Pos,FunParams,ExtCall,Deps), |
| 963 | ? | ( external_name(DefName,_ExtType,ExpectedDefType,ExtCallFunctor,FunName), |
| 964 | | ExtCall =.. [ExtCallFunctor,Pos,FunName,FunParams,FunDef, |
| 965 | | rewrite_protected(TypeParams),rewrite_protected(Decl)], |
| 966 | | selectchk(OldDefinition,In,NewDefinition,Out) -> |
| 967 | | assert_external_procedure_used(FunName) |
| 968 | | ; otherwise -> |
| 969 | | % no definition found for external function |
| 970 | | add_error(replace_external_declaration,'No DEFINITION associated with: ',DefName,DefPos), |
| 971 | | Out=In). |
| 972 | | |
| 973 | | reset_bmachine_construction :- reset_external_procedure_used. |
| 974 | | |
| 975 | | % maybe this information should be stored somewhere else ?? |
| 976 | | :- dynamic external_procedure_used/1. |
| 977 | | reset_external_procedure_used :- retractall(external_procedure_used(_)). |
| 978 | | assert_external_procedure_used(FunName) :- |
| 979 | | (external_procedure_used(FunName) -> true ; assert(external_procedure_used(FunName))). |
| 980 | | |
| 981 | | link_to_refinement(machine,_RawMachine,_RefMachines,Local,Local,Errors,Errors). |
| 982 | | link_to_refinement(refinement,RawMachine,RefMachines,Local,NewLocal,Ein,Eout) :- |
| 983 | | link_to_refinement(implementation,RawMachine,RefMachines,Local,NewLocal,Ein,Eout). |
| 984 | | link_to_refinement(implementation,RawMachine,RefMachines,Local,NewLocal,Ein,Eout) :- |
| 985 | | link_to_refinement2(implementation,RawMachine,RefMachines,Local,NewLocal,Ein,Eout). |
| 986 | | link_to_refinement2(_MType,RawMachine,RefMachines,Local,NewLocal,Ein,Eout) :- |
| 987 | | memberchk(ref(abstraction,AbstractMachine),RefMachines), |
| 988 | | copy_constraints(Local,AbstractMachine,NewLocal,Ein,E1), |
| 989 | | type_vars_in_refinement(AbstractMachine,NewLocal), |
| 990 | | type_refinement_operations(RawMachine,AbstractMachine,NewLocal,E1,Eout). |
| 991 | | |
| 992 | | copy_constraints(Local,AbstractMachine,NewLocal,Ein,Eout) :- |
| 993 | | get_section(parameters,Local,LocalParameters), |
| 994 | | get_section(parameters,AbstractMachine,AbstractParameters), |
| 995 | | check_if_equal_identifiers(LocalParameters,AbstractParameters,Ein,Eout,Local), |
| 996 | | get_section(constraints,AbstractMachine,Constraints), |
| 997 | | write_section(constraints,Constraints,Local,NewLocal). |
| 998 | | check_if_equal_identifiers(Local,Abstract,Ein,Eout,LocalMachine) :- |
| 999 | | ( same_length(Local,Abstract) -> |
| 1000 | | foldl(check_if_equal_identifiers2,Local,Abstract,Ein,Eout) |
| 1001 | | ; otherwise -> |
| 1002 | | get_texpr_ids(Abstract,AIDs), |
| 1003 | | get_machine_name(LocalMachine,MachName), |
| 1004 | | ajoin(['Refinement ',MachName,' must have same Parameters ', AIDs,' as abstract Machine'],Msg), |
| 1005 | | Ein = [error(Msg,none)|Eout] |
| 1006 | | ). |
| 1007 | | check_if_equal_identifiers2(LParam,AParam,Ein,Eout) :- |
| 1008 | | get_texpr_id(LParam,LName), |
| 1009 | | get_texpr_id(AParam,AName), |
| 1010 | | ( LName = AName -> |
| 1011 | | % type in refinement is the same as in the abstraction |
| 1012 | | get_texpr_type(LParam,Type), |
| 1013 | | get_texpr_type(AParam,Type), |
| 1014 | | Ein=Eout |
| 1015 | | ; otherwise -> |
| 1016 | | get_texpr_pos(LParam,Pos), |
| 1017 | | ajoin(['Parameter ',LName,' of refinement machine must be ', |
| 1018 | | AName,' like in the abstract machine'],Msg), |
| 1019 | | Ein = [error(Msg,Pos)|Eout] |
| 1020 | | ). |
| 1021 | | |
| 1022 | | % in case of a refinement, give variables the same type as in the abstract machine |
| 1023 | | % the same for constants |
| 1024 | | type_vars_in_refinement(AbstractMachine,ConcreteMachine) :- |
| 1025 | | pass_type(AbstractMachine,[abstract_variables,concrete_variables], |
| 1026 | | ConcreteMachine,[abstract_variables,concrete_variables]), |
| 1027 | | pass_type(AbstractMachine,[abstract_constants,concrete_constants], |
| 1028 | | ConcreteMachine,[abstract_constants,concrete_constants]). |
| 1029 | | |
| 1030 | | % pass the type from variables in Sections1 of Machine1 to |
| 1031 | | % the variables of the same name in Sections2 of Machine2 |
| 1032 | | % Machine1,Machine2: a machine |
| 1033 | | % Sections1, Sections2: a list of section names |
| 1034 | | pass_type(Machine1,Sections1,Machine2,Sections2) :- |
| 1035 | | get_sections_and_append(Sections1,Machine1,Vars1), |
| 1036 | | get_sections_and_append(Sections2,Machine2,Vars2), |
| 1037 | | maplist(pass_type2(Vars2),Vars1). |
| 1038 | | get_sections_and_append([],_M,[]). |
| 1039 | | get_sections_and_append([Sec|RestSections],M,R) :- |
| 1040 | | get_section(Sec,M,L), append(L,Rest,R), |
| 1041 | | get_sections_and_append(RestSections,M,Rest). |
| 1042 | | pass_type2(DstVariables,SrcVariable) :- |
| 1043 | | get_texpr_id(SrcVariable,Id), |
| 1044 | | get_texpr_id(DstVariable,Id), |
| 1045 | | ( memberchk(DstVariable,DstVariables) -> |
| 1046 | | get_texpr_type(DstVariable,Type), |
| 1047 | | get_texpr_type(SrcVariable,Type) |
| 1048 | | ; otherwise -> |
| 1049 | | true). |
| 1050 | | |
| 1051 | | |
| 1052 | | % in case of a refinement, check if the defined operations are already defined |
| 1053 | | % in the abstract machine and copy that type. |
| 1054 | | type_refinement_operations(RawMachine,AbstractMachine,Local,Ein,Eout) :- |
| 1055 | | get_operation_identifiers(RawMachine,Operations), |
| 1056 | | ~~mnf(type_refinement_operations2(Operations,Local,AbstractMachine,Ein,Eout)). |
| 1057 | | type_refinement_operations2([],_,_AbstractMachine,Errors,Errors). |
| 1058 | | type_refinement_operations2([Op|Rest],M,AbstractMachine,Ein,Eout) :- |
| 1059 | | get_abstract_operation_name_wo_infos(Op,AOp), |
| 1060 | | %print(treating_refines_operation(Op,AOp)),nl, |
| 1061 | | get_texpr_pos(Op,Pos), |
| 1062 | | % look up the abstract definition |
| 1063 | | get_abstract_op(AOp,AbstractMachine,Pos,Ein,E1), |
| 1064 | | % store the type in the identifier section |
| 1065 | | copy_texpr_wo_info(Op,SOp), |
| 1066 | | get_section(promoted,M,Operations), |
| 1067 | | memberchk(SOp, Operations), |
| 1068 | | % do the rest |
| 1069 | | type_refinement_operations2(Rest,M,AbstractMachine,E1,Eout). |
| 1070 | | % looks up the type of the operator in an abstract machine |
| 1071 | | get_abstract_op(Op,Abstraction,_,Errors,Errors) :- |
| 1072 | | % look for the operation in promoted and unpromoted |
| 1073 | | ( get_section(promoted,Abstraction,AbstractOps), member(Op,AbstractOps) |
| 1074 | | ; get_section(unpromoted,Abstraction,AbstractOps), member(Op,AbstractOps) ), |
| 1075 | | % forget alternatives |
| 1076 | | !. |
| 1077 | | get_abstract_op(Op,_Abstraction,_Pos,Errors,Errors) :- |
| 1078 | | % we might allow new operations |
| 1079 | | get_preference(allow_new_ops_in_refinement,true),!, |
| 1080 | | get_texpr_type(Op,op(_,_)). |
| 1081 | | get_abstract_op(Op,_,Pos,[error(Msg,Pos)|Eout],Eout) :- |
| 1082 | | % in case we do not find the operation, store an error |
| 1083 | | get_texpr_id(Op,op(Id)), |
| 1084 | | ajoin(['operation ', Id, ' is not defined in the abstract machine'], Msg). |
| 1085 | | % copy a typed expression without the additional information (just expression and type) |
| 1086 | | copy_texpr_wo_info(A,B) :- |
| 1087 | | % copy the expression and type, the additional information may be different |
| 1088 | | get_texpr_expr(A,Expr),get_texpr_expr(B,Expr), |
| 1089 | | get_texpr_type(A,Type),get_texpr_type(B,Type). |
| 1090 | | |
| 1091 | | get_abstract_operation_name_wo_infos(b(_,Type,Infos),Res) :- |
| 1092 | | memberchk(refines_operation(RefID),Infos),!, % renaming occurs: |
| 1093 | | Res = b(identifier(op(RefID)),Type,_). |
| 1094 | | get_abstract_operation_name_wo_infos(ID,Copy) :- copy_texpr_wo_info(ID,Copy). |
| 1095 | | |
| 1096 | | create_id_sections(Header,RawMachine,Name) --> |
| 1097 | | create_id_sections_header(Header), |
| 1098 | | %{print(created_header(Name)),nl}, |
| 1099 | | create_set_sections(RawMachine,Name), |
| 1100 | | %{print(created_set(Name)),nl}, |
| 1101 | | create_constants_sections(RawMachine), |
| 1102 | | %{print(created_constants(Name)),nl}, |
| 1103 | | create_variables_sections(RawMachine), |
| 1104 | | %{print(created_variables(Name)),nl}, |
| 1105 | | create_operations_sections(RawMachine). |
| 1106 | | |
| 1107 | | extract_parameter_types(MachineRefs,ParameterTypes) :- |
| 1108 | | maplist(extract_parameter_types2,MachineRefs,ParameterTypesL), |
| 1109 | | append(ParameterTypesL,ParameterTypes). |
| 1110 | | extract_parameter_types2(ref(_,Machine),ParameterTypes) :- |
| 1111 | | get_section(parameters,Machine,VisibleParams), |
| 1112 | | get_section(internal_parameters,Machine,InternalParams), |
| 1113 | | append(VisibleParams,InternalParams,Params), |
| 1114 | | include(is_a_parameter_set,Params,ParameterSets), |
| 1115 | | maplist(get_texpr_set_type,ParameterSets,ParameterTypes). |
| 1116 | | is_a_parameter_set(TExpr) :- |
| 1117 | | get_texpr_info(TExpr,Info), |
| 1118 | | memberchk(parameter_set,Info). |
| 1119 | | |
| 1120 | | type_sections(RawMachine,MachineType,RefMachines,NonGroundExceptions,Name,Ein,Eout) --> |
| 1121 | | {debug_stats('TYPING CONSTRAINTS'(Name))}, |
| 1122 | | type_constraints(MachineType,Name,RawMachine,RefMachines,NonGroundExceptions,Ein,E1), |
| 1123 | | % Maybe the VALUES section must be moved up later because it may be used to |
| 1124 | | % substitute types (e.g. deferred sets to integers) for later use |
| 1125 | | {debug_stats('TYPING PROPERTIES'(Name))}, |
| 1126 | | type_section_with_single_predicate(properties,Name,[constants],MachineType,RawMachine,RefMachines,NonGroundExceptions,E1,E2), |
| 1127 | | {debug_stats('TYPING INVARIANT'(Name))}, |
| 1128 | | type_section_with_single_predicate(invariant,Name,[variables],MachineType,RawMachine,RefMachines,NonGroundExceptions,E2,E3), |
| 1129 | | {debug_stats('TYPING ASSERTIONS'(Name))}, |
| 1130 | | type_section_with_predicate_list(assertions,[],MachineType,RawMachine,RefMachines,NonGroundExceptions,E3,E4), |
| 1131 | | {debug_stats('TYPING INITIALISATION'(Name))}, |
| 1132 | | type_initialisation_section(RawMachine,Name,MachineType,RefMachines,NonGroundExceptions,E4,E5), |
| 1133 | | {debug_stats('TYPING OPERATIONS'(Name))}, |
| 1134 | | type_operations_section(RawMachine,MachineType,RefMachines,NonGroundExceptions,E5,Eout), |
| 1135 | | {debug_stats('FINISHED TYPING SECTIONS'(Name))}. |
| 1136 | | |
| 1137 | | % skip this section, it is copied from the abstract machine and |
| 1138 | | % does not need to be typed again |
| 1139 | | type_constraints(refinement,_,_RawMachine,_RefMachines,_NonGroundExceptions,Errors,Errors) --> !. |
| 1140 | | type_constraints(implementation,_,_RawMachine,_RefMachines,_NonGroundExceptions,Errors,Errors) --> !. |
| 1141 | | type_constraints(machine,Name,RawMachine,RefMachines,NonGroundExceptions,Ein,Eout) --> |
| 1142 | | % if the machine is a dummy machine (in presence of a not included seen or used |
| 1143 | | % machine), we must omit the check that the (lower case) parameters are all typed. |
| 1144 | | % We can assume that they are properly typed by the included machine. |
| 1145 | | {( is_dummy_machine(RawMachine) -> IdsToType = [] |
| 1146 | | ; otherwise -> IdsToType = [parameters])}, |
| 1147 | | type_section_with_single_predicate(constraints,Name,IdsToType,machine, |
| 1148 | | RawMachine,RefMachines,NonGroundExceptions,Ein,Eout). |
| 1149 | | |
| 1150 | ? | is_dummy_machine(RawMachine) :- member(is_dummy,RawMachine),!. |
| 1151 | | |
| 1152 | | % Header: Parameters |
| 1153 | | create_id_sections_header(machine_header(_,_,Parameters),Old,New) :- |
| 1154 | | write_section(parameters,TParams,Old,New), |
| 1155 | | maplist(create_id_section_parameter,Parameters,TParams). |
| 1156 | | create_id_section_parameter(Param,TParam) :- |
| 1157 | | Expr=identifier(Name), |
| 1158 | | ext2int(Param,Expr,_,Type,Expr,[ParameterType],TParam), |
| 1159 | | ( is_upper_case(Name) -> |
| 1160 | | ParameterType = parameter_set, |
| 1161 | | Type = set(_) |
| 1162 | | ; otherwise -> |
| 1163 | | ParameterType = parameter_scalar). |
| 1164 | | is_upper_case(Name) :- \+ atom(Name),!, add_internal_error('Illegal call:', is_upper_case(Name)),fail. |
| 1165 | | is_upper_case(Name) :- atom_codes(Name,[C|_]), |
| 1166 | | memberchk(C,"ABCDEFGHIJKLMNOPQRSTUVWXYZ"). |
| 1167 | | |
| 1168 | | % Body: Sets |
| 1169 | | create_set_sections(Sections,MachineName) --> |
| 1170 | | write_section(deferred_sets,DeferredSets), |
| 1171 | | write_section(enumerated_sets,EnumeratedSets), |
| 1172 | | write_section(enumerated_elements,EnumeratedElements), |
| 1173 | | {optional_rawmachine_section(sets,Sections,[],Sets), |
| 1174 | | split_list(is_deferred_set_element,Sets,RawDeferredSets,RawEnumeratedSets), |
| 1175 | | maplist(create_deferred_set_section(MachineName),RawDeferredSets,DeferredSets), |
| 1176 | | maplist(create_enumerated_set_section(MachineName), |
| 1177 | | RawEnumeratedSets,EnumeratedSets,LEnumeratedElements), |
| 1178 | | append(LEnumeratedElements,EnumeratedElements)}. |
| 1179 | | is_deferred_set_element(AstElem) :- has_functor(AstElem,deferred_set,_). |
| 1180 | | create_deferred_set_section(MachineName,DS,TExpr) :- |
| 1181 | | unwrap_opt_description(DS,deferred_set(Pos,I),TInfos), |
| 1182 | | Infos = [given_set,def(deferred_set,MachineName)|TInfos], |
| 1183 | | create_identifier(I,Pos,set(global(I)),Infos,TExpr). |
| 1184 | | create_enumerated_set_section(MachineName,ES,TExpr,Elements) :- |
| 1185 | | unwrap_opt_description(ES,enumerated_set(Pos,I,Elems),TInfos), |
| 1186 | | Infos = [given_set,def(enumerated_set,MachineName)|TInfos], |
| 1187 | | create_identifier(I,Pos,set(global(I)),Infos,TExpr), |
| 1188 | | maplist(create_element(global(I),MachineName),Elems,Elements). |
| 1189 | | |
| 1190 | | % deal with optional description(Pos,Desc,A) wrapper |
| 1191 | | has_functor(description(_,_Desc,A),Functor,Arity) :- !, functor(A,Functor,Arity). |
| 1192 | | has_functor(A,Functor,Arity) :- functor(A,Functor,Arity). |
| 1193 | | |
| 1194 | | % remove description wrapper and generate info field |
| 1195 | | unwrap_opt_description(description(_,Desc,A),Res,Infos) :- !, Res=A, Infos=[description(Desc)]. |
| 1196 | | unwrap_opt_description(A,A,[]). |
| 1197 | | |
| 1198 | | create_element(Type,MachineName,Ext,Elem) :- |
| 1199 | | ext2int(Ext,Expr,_,Type,Expr,[enumerated_set_element,def(enumerated_element,MachineName)],Elem). |
| 1200 | | create_identifier(Id,Pos,Type,Infos,TExpr) :- |
| 1201 | | create_texpr(identifier(Id),Type,[nodeid(Pos)|Infos],TExpr). |
| 1202 | | |
| 1203 | | % Constants |
| 1204 | | create_constants_sections(RawMachine) --> |
| 1205 | | create_section_identifiers(constants,concrete_constants,RawMachine), |
| 1206 | | create_section_identifiers(abstract_constants,abstract_constants,RawMachine). |
| 1207 | | % Variables |
| 1208 | | create_variables_sections(RawMachine) --> |
| 1209 | | create_section_identifiers(concrete_variables,concrete_variables,RawMachine), |
| 1210 | | create_section_identifiers(variables,abstract_variables,RawMachine). |
| 1211 | | |
| 1212 | | % Freetypes: Treat them as additional constants, plus add entries in the "freetypes" |
| 1213 | | % section of the resulting machine |
| 1214 | | create_freetypes(RawMachine,MType,RefMachines,Old,New,Ein,Eout) :- |
| 1215 | | optional_rawmachine_section(freetypes,RawMachine,[],RawFreetypes), |
| 1216 | | create_freetypes2(RawFreetypes,MType,[ref(local,Old)|RefMachines],Old,New,Ein,Eout). |
| 1217 | | create_freetypes2([],_MType,_RefMachines,M,M,E,E) :- !. |
| 1218 | | create_freetypes2(RawFreetypes,MType,RefMachines,Old,New,Ein,Eout) :- |
| 1219 | | % we need the NonGroundExceptions for type checking |
| 1220 | | extract_parameter_types(RefMachines,NonGroundExceptions), |
| 1221 | | % create identifiers in the constants section |
| 1222 | | maplist(create_ids_for_freetype,RawFreetypes,IdsFreetypes), |
| 1223 | | % we just combined the results to keep the numbers of arguments low (too much for maplist) |
| 1224 | | maplist(split_ft,IdsFreetypes,IdentifiersL,Freetypes), |
| 1225 | | append(IdentifiersL,Identifiers), |
| 1226 | | % create properties for each freetype |
| 1227 | | foldl(create_properties_for_freetype(MType,RefMachines,NonGroundExceptions), |
| 1228 | | RawFreetypes,IdsFreetypes,PropertiesL,Ein,Eout), |
| 1229 | | conjunct_predicates(PropertiesL,Properties), |
| 1230 | | append_to_section(abstract_constants,Identifiers,Old,Inter), |
| 1231 | | conjunct_to_section(properties,Properties,Inter,Inter2), |
| 1232 | | write_section(freetypes,Freetypes,Inter2,New). |
| 1233 | | split_ft(ft(Ids,Freetype),Ids,Freetype). |
| 1234 | | create_ids_for_freetype(freetype(_Pos,Id,Constructors),ft([TId|TCons],freetype(Id,Cases))) :- |
| 1235 | | create_typed_id(Id,set(freetype(Id)),TId), |
| 1236 | | maplist(create_ids_for_constructor(Id),Constructors,TCons,Cases). |
| 1237 | | create_ids_for_constructor(Id,constructor(_Pos,Name,_Arg),TCons,case(Name,Type)) :- |
| 1238 | | create_typed_id(Name,set(couple(Type,freetype(Id))),TCons). |
| 1239 | | create_ids_for_constructor(Id,element(_Pos,Name),TCons,case(Name,constant([Name]))) :- |
| 1240 | | create_typed_id(Name,freetype(Id),TCons). |
| 1241 | | create_properties_for_freetype(MType,RefMachines,NonGroundExceptions, |
| 1242 | | freetype(_Pos,Id,Constructors),ft(Ids,_Freetypes),Properties,Ein,Eout) :- |
| 1243 | | % The freetype type |
| 1244 | | FType = freetype(Id), |
| 1245 | | % We use the standard type environment of properties... |
| 1246 | | visible_env(MType,properties,RefMachines,CEnv,Ein,E1), |
| 1247 | | % ...plus the identifiers of the free type (type name and constructor names) |
| 1248 | | add_identifiers_to_environment(Ids,CEnv,FEnv), |
| 1249 | | % We generate a comprehension set for all elements |
| 1250 | | create_typed_id(Id,set(FType),TId), |
| 1251 | | create_texpr(equal(TId,TComp),pred,[],FDef), |
| 1252 | | unique_typed_id("_freetype_arg",FType,Element), |
| 1253 | | create_recursive_compset([Element],ECond,set(FType),[],RecId,TComp), |
| 1254 | | create_typed_id(RecId,set(FType),TRecId), |
| 1255 | | % For each constructor, we generate a definition and a condition for the |
| 1256 | | % comprehension set above |
| 1257 | | foldl(create_properties_for_constructor(Id,FEnv,Element,TRecId,NonGroundExceptions), |
| 1258 | | Constructors,Defs,Conds,E1,Eout), |
| 1259 | | conjunct_predicates(Conds,ECond), |
| 1260 | | conjunct_predicates([FDef|Defs],Properties). |
| 1261 | | |
| 1262 | | /* create_properties_for_constructor(+Env,+Element,+RecId,+NGE,+Constructor,-Def,-Cond,Ein,Eout) |
| 1263 | | Env: Type environment |
| 1264 | | Element: A typed identifier "e" that is used in the definition of the freetype set: |
| 1265 | | ft = {e | e has_freetype_constructor x => e:...} |
| 1266 | | RecId: The typed identifier that can be used to refer to the freetype set (ft in the |
| 1267 | | example above |
| 1268 | | NGE: "Non ground exceptions", needed for type checking when having a parametrized machine |
| 1269 | | Constructor: The constructor expression as it comes from the parser |
| 1270 | | (constructor(Pos,Name,ArgSet) or element(Pos,Name)) |
| 1271 | | Def: The predicate that defines the constant for the constructor, |
| 1272 | | e.g. "cons = {i,o | i:NAT & o = freetype(cons,i)}" |
| 1273 | | Cond: The predicate that checks the argument of a freetype in the freetype set |
| 1274 | | (That would be the part "e:..." in the example above. |
| 1275 | | Ein,Eout: Used for type checker errors |
| 1276 | | */ |
| 1277 | | create_properties_for_constructor(FID,Env,Element,RecId,NonGroundExceptions, |
| 1278 | | Constructor,Def,Cond,Ein,Eout) :- |
| 1279 | | constructor_name(Constructor,Name), |
| 1280 | | env_lookup_type(Name,Env,CType), |
| 1281 | | create_properties_for_constructor2(Constructor,Env,NonGroundExceptions,FID, |
| 1282 | | Element,RecId,CDef,Cond,Ein,Eout), |
| 1283 | | get_texpr_type(CDef,CType), |
| 1284 | | create_typed_id(Name,CType,CId), |
| 1285 | | create_texpr(equal(CId,CDef),pred,[],Def). |
| 1286 | | constructor_name(element(_Pos,Name),Name). |
| 1287 | | constructor_name(constructor(_Pos,Name,_Domain),Name). |
| 1288 | | create_properties_for_constructor2(element(_Pos,Name),_Env,_NonGroundExceptions,FID, |
| 1289 | | _Element,_RecId,CDef,Cond,Ein,Ein) :- |
| 1290 | | create_texpr(value(freeval(FID,Name,term(Name))),freetype(FID),[],CDef), |
| 1291 | | create_texpr(truth,pred,[],Cond). |
| 1292 | | create_properties_for_constructor2(constructor(_Pos,Name,RArg),Env,NonGroundExceptions, |
| 1293 | | FID,Element,RecId,CDef,Cond,Ein,Eout) :- |
| 1294 | | % First, type check the given set of the domain: |
| 1295 | | btype_ground_dl([RArg],Env,NonGroundExceptions,[set(DType)],[TDomain],Ein,Eout), |
| 1296 | | % then create the RHS of "c = {i,o | i:Domain & o=freetype_constructor(Name,i)}" |
| 1297 | | create_definition_for_constructor(Name,TDomain,FID,CDef), |
| 1298 | | % The check in the freetype comprehension set is of the form |
| 1299 | | % e "of_freetype_case" Name => "content_of"(e) : Domain |
| 1300 | | create_texpr(implication(IsCase,DomainTest),pred,[],Cond), |
| 1301 | | create_texpr(freetype_case(FID,Name,Element),pred,[],IsCase), |
| 1302 | | create_texpr(freetype_destructor(FID,Name,Element),DType,[],Content), |
| 1303 | | % all references to the freetype itself are replaced by the recursive reference |
| 1304 | | replace_id_by_expr(TDomain,FID,RecId,TDomain2), |
| 1305 | | create_texpr(member(Content,TDomain2),pred,[],DomainTest). |
| 1306 | | |
| 1307 | | :- use_module(bsyntaxtree,[get_texpr_set_type/2]). |
| 1308 | | |
| 1309 | | /* The constructor is a function to the freetype, defined with a comprehension set: |
| 1310 | | The general form is "c = {i,o | i:Domain & o=freetype_constructor(Name,i)}" |
| 1311 | | create_definition_for_constructor(+Name,+DType,+FID,-CType,-CDef) :- |
| 1312 | | Name: Name of the constructor |
| 1313 | | TDomain: The user-specified domain |
| 1314 | | FID: The name of the free type |
| 1315 | | CDef: The RHS of the definition "Name = CDef" |
| 1316 | | */ |
| 1317 | | create_definition_for_constructor(Name,TDomain,FID,CDef) :- |
| 1318 | | % get the type of the domain: |
| 1319 | | get_texpr_set_type(TDomain,DType), |
| 1320 | | % create argument and result identifiers: |
| 1321 | | unique_typed_id("_constr_arg",DType,TArgId), % was constructor_arg and constructor_res |
| 1322 | | unique_typed_id("_constr_res",freetype(FID),TResId), |
| 1323 | | % The comprehension set as a whole |
| 1324 | | CType = set(couple(DType,freetype(FID))), |
| 1325 | | create_texpr(comprehension_set([TArgId,TResId],Pred),CType, |
| 1326 | | [prob_annotation('SYMBOLIC')],CDef), |
| 1327 | | create_texpr(conjunct(DomainCheck,Construction),pred,[],Pred), |
| 1328 | | % "i:Domain" |
| 1329 | | create_texpr(member(TArgId,TDomain),pred,[],DomainCheck), |
| 1330 | | % "o=freetype_constructor(i) |
| 1331 | | create_texpr(freetype_constructor(FID,Name,TArgId),freetype(FID),[],FreetypeCons), |
| 1332 | | create_texpr(equal(TResId,FreetypeCons),pred,[],Construction). |
| 1333 | | |
| 1334 | | % Operations |
| 1335 | | create_operations_sections(RawMachine,Old,New) :- |
| 1336 | | write_section(promoted,OperationIdentifiers,Old,New0), |
| 1337 | | get_operation_identifiers(RawMachine,operations,OperationIdentifiers), |
| 1338 | | (allow_local_op_calls, |
| 1339 | | get_operation_identifiers(RawMachine,local_operations,LocOpIDs), |
| 1340 | | LocOpIDs \= [] |
| 1341 | | -> append_to_section(unpromoted,LocOpIDs,New0,New) % TODO: check that it does not yet exist |
| 1342 | | ; New = New0 |
| 1343 | | ). |
| 1344 | | |
| 1345 | | get_operation_identifiers(RawMachine,OperationIdentifiers) :- |
| 1346 | | get_operation_identifiers(RawMachine,operations,OperationIdentifiers). |
| 1347 | | get_operation_identifiers(RawMachine,SECTION,OperationIdentifiers) :- |
| 1348 | | optional_rawmachine_section(SECTION,RawMachine,[],Ops), |
| 1349 | | maplist(extract_operation_identifier,Ops,OperationIdentifiers). |
| 1350 | | extract_operation_identifier(Ext,TId) :- |
| 1351 | | remove_pos(Ext, operation(ExtId,_,_,_)),!, |
| 1352 | | ext2int(ExtId,identifier(I),_,op(_,_),identifier(op(I)),Infos,TId), |
| 1353 | | operation_infos(Infos). |
| 1354 | | extract_operation_identifier(Ext,TId) :- |
| 1355 | | remove_pos(Ext, refined_operation(ExtId,_,_,RefinesOp,_)),!, |
| 1356 | | ext2int(ExtId,identifier(I),_,op(_,_),identifier(op(I)),[refines_operation(RefinesOp)|Infos],TId), |
| 1357 | | operation_infos(Infos). |
| 1358 | | extract_operation_identifier(Ext,_) :- add_internal_error('Unknown operation node:',Ext),fail. |
| 1359 | | |
| 1360 | | % VALUES section: |
| 1361 | | % process_values_section(MachineType,RawMachine,NonGroundExceptions,Min/Ein/RefMIn,Mout/Eout/RefMOut): |
| 1362 | | % Type-check the VALUES section and change the type of valuated deferred sets, if necessary |
| 1363 | | % MachineType, RawMachine, NonGroundExceptions: as usual, see other comments |
| 1364 | | % Min/Mout: The currently constructed machine |
| 1365 | | % Ein/Eout: The difference list of errors |
| 1366 | | % RefMin/RefMout: The list of already typechecked machines. These typechecked machines can be |
| 1367 | | % altered by this predicate because if a deferred set is valuated by an integer set or |
| 1368 | | % other deferred set, all occurrences of the original type are replaced by the new type, |
| 1369 | | % even for the already typed machines. |
| 1370 | | process_values_section(MachineType,RawMachine,NonGroundExceptions,Min/Ein/RefMIn,Mout/Eout/RefMOut) :- |
| 1371 | | optional_rawmachine_section(values,RawMachine,[],RawValues), |
| 1372 | | process_values_section_aux(RawValues,MachineType,NonGroundExceptions, |
| 1373 | | Min/Ein/RefMIn,Mout/Eout/RefMOut). |
| 1374 | | process_values_section_aux([],_MachineType,_NonGroundExceptions,In,Out) :- !,In=Out. |
| 1375 | | process_values_section_aux(RawValues,MachineType,NonGroundExceptions, |
| 1376 | | Min/Ein/RefMin,Mout/Eout/RefMout) :- |
| 1377 | | debug_stats('TYPING VALUES'), |
| 1378 | | type_values_section(MachineType,RawValues,RefMin,NonGroundExceptions,Min/Ein,Mout/Eout), |
| 1379 | | % will be added as additional_property in bmachine |
| 1380 | | RefMin=RefMout. |
| 1381 | | |
| 1382 | | type_values_section(MachineType,RawValues,RefMachines,NonGroundExceptions,Min/Ein,Mout/Eout) :- |
| 1383 | | write_section(values,Values,Min,Mout), |
| 1384 | | visible_env(MachineType,values_expression,RefMachines,Env,Ein,E1), |
| 1385 | | % We have to pass an environment that can be modified because in each |
| 1386 | | % valuation the previously valuated constants can be used. |
| 1387 | | foldl(extract_values_entry(NonGroundExceptions),RawValues,Values,Env/E1,_ResultingEnv/Eout). |
| 1388 | | |
| 1389 | | extract_values_entry(NonGroundExceptions, values_entry(POS,ValueID,ValueExpr), Entry, |
| 1390 | | EnvIn/Ein,EnvOut/Eout) :- |
| 1391 | | % TODO: There seem to be a lot of additional constraints for valuations that are not |
| 1392 | | % yet handled here |
| 1393 | | btype_ground_dl([ValueExpr],EnvIn,NonGroundExceptions,[Type],[TExpr],Ein,Eout), |
| 1394 | | create_identifier(ValueID,POS,Type,[valuated_constant],TypedID), |
| 1395 | | create_texpr(values_entry(TypedID,TExpr),values_entry,[nodeid(POS)],Entry), |
| 1396 | | debug_println(9,valued_constant(ValueID)), |
| 1397 | | add_identifiers_to_environment([TypedID],EnvIn,EnvOut). |
| 1398 | | |
| 1399 | | % type_section_with_single_predicate(+Sec,+Name,+SectionsToType,+MachineType,+Sections, |
| 1400 | | % +RefMachines,+NonGroundExceptions,+Ein,-Eout,+Old,-New): |
| 1401 | | % Type a section such as INVARIANT, PROPERTIES, CONSTRAINTS with a single predicate |
| 1402 | | % Sec: section name in the raw (untyped) machine (e.g. invariant) |
| 1403 | | % Name: name of machine from which this section comes |
| 1404 | | % SectionsToType: list of section names that contain identifiers that must be typed |
| 1405 | | % by this predicate (e.g. all variables must be typed by the invariant) |
| 1406 | | % MachineType: machine type (machine, refinement, ...) |
| 1407 | | % Sections: list of sections representing the raw (untyped) machine |
| 1408 | | % RefMachines: list of already typed machines |
| 1409 | | % NonGroundExceptions: list of types that may be not ground because the concrete type |
| 1410 | | % is determinded by machine parameter |
| 1411 | | % Ein/Eout: difference list of errors |
| 1412 | | % Old/New: the new typed section is added (by conjunction) to the machine |
| 1413 | | type_section_with_single_predicate(Sec,Name,SectionsToType,MachineType,Sections, |
| 1414 | | RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :- |
| 1415 | | ~~mnf(optional_rawmachine_section(Sec,Sections,truth(none),Predicate)), |
| 1416 | | ( Predicate = truth(_) -> |
| 1417 | | % even if there is no content, we must check if all identifiers are typed |
| 1418 | | check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,Ein,Eout), |
| 1419 | | Old=New |
| 1420 | | ; otherwise -> |
| 1421 | | get_machine_infos(Sections,Infos), |
| 1422 | | toplevel_raw_predicate_sanity_check(Sec,Name,Predicate,Infos), |
| 1423 | | type_predicates(Sec,SectionsToType,MachineType,[Predicate],RefMachines,NonGroundExceptions, |
| 1424 | | [Typed],Ein,Eout), |
| 1425 | | conjunct_to_section(Sec,Typed,Old,New) |
| 1426 | | ), |
| 1427 | | !. |
| 1428 | | type_section_with_single_predicate(Sec,Name,SectsToType,MchType,_,_,_,_,_,_,_) :- |
| 1429 | | add_internal_error('type_section_with_single_predicate failed', |
| 1430 | | type_section_with_single_predicate(Sec,Name,SectsToType,MchType,_,_,_,_,_,_,_)), |
| 1431 | | fail. |
| 1432 | | |
| 1433 | | % get some infos relevant for sanity check: |
| 1434 | | get_machine_infos(Sections,Infos) :- |
| 1435 | ? | ((rawmachine_section_exists(concrete_variables,Sections) ; rawmachine_section_exists(abstract_variables,Sections)) |
| 1436 | | -> Infos = [has_variables|I1] ; Infos = I1), |
| 1437 | | ((rawmachine_section_exists(concrete_constants,Sections) ; rawmachine_section_exists(abstract_constants,Sections)) |
| 1438 | | -> I1 = [has_constants] ; I1 = []). |
| 1439 | | |
| 1440 | | % Type a section with multiple predicates, such as ASSERTIONS |
| 1441 | | type_section_with_predicate_list(Sec,SectionsToType,MachineType,Sections, |
| 1442 | | RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :- |
| 1443 | | write_section(Sec,Typed,Old,New), |
| 1444 | | ~~mnf(optional_rawmachine_section(Sec,Sections,[],Predicates)), |
| 1445 | | type_predicates(Sec,SectionsToType,MachineType,Predicates,RefMachines,NonGroundExceptions,Typed,Ein,Eout), |
| 1446 | | !. |
| 1447 | | type_section_with_predicate_list(Sec,SectsToType,MchType,Sects,RefMchs,NonGrndExc,Ein,Eout,Old,New) :- |
| 1448 | | add_internal_error('type_section_with_predicate_list failed', |
| 1449 | | type_section_with_predicate_list(Sec,SectsToType,MchType,Sects,RefMchs,NonGrndExc,Ein,Eout,Old,New)), |
| 1450 | | fail. |
| 1451 | | |
| 1452 | | |
| 1453 | | type_predicates(_Sec,SectionsToType,_MachineType,[],RefMachines,NonGroundExceptions,Typed,Ein,Eout) :- |
| 1454 | | !,Typed=[], |
| 1455 | | check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,Ein,Eout). |
| 1456 | | type_predicates(Sec,SectionsToType,MachineType,Predicates,RefMachines,NonGroundExceptions,Typed,Ein,Eout) :- |
| 1457 | | debug:debug_println(9,typing(Sec,MachineType)), |
| 1458 | | visible_env(MachineType, Sec, RefMachines, Env, Ein, E1), |
| 1459 | | same_length(Predicates,Types),maplist(is_pred_type,Types), |
| 1460 | | debug:debug_println(9,btype(Sec,MachineType)), |
| 1461 | | btype_ground_dl_in_section(Sec,Predicates,Env,NonGroundExceptions,Types,Typed1,E1,E2), |
| 1462 | | mark_with_section(Sec,Typed1,Typed), |
| 1463 | | debug:debug_println(9,check_all_ids_typed), |
| 1464 | | check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,E2,Eout), |
| 1465 | | debug:debug_println(9,finished_check_all_ids_typed). |
| 1466 | | |
| 1467 | | % check if the identifiers that should be typed by this section are completly typed |
| 1468 | | check_if_all_ids_are_typed([],_RefMachines,_NonGroundExceptions,Ein,Eout) :- !,Ein=Eout. |
| 1469 | | check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,Ein,Eout) :- |
| 1470 | | memberchk(ref(local,Local),RefMachines), |
| 1471 | | get_all_identifiers(SectionsToType,Local,IdentifiersToType), |
| 1472 | | check_ground_types_dl(IdentifiersToType, NonGroundExceptions, Ein, Eout). |
| 1473 | | |
| 1474 | | |
| 1475 | | mark_with_section(Sec,In,Out) :- |
| 1476 | | maplist(mark_with_section2(Sec),In,Out). |
| 1477 | | mark_with_section2(Sec,In,Out) :- |
| 1478 | | remove_bt(In,conjunct(A,B),conjunct(NA,NB),Out),!, |
| 1479 | | mark_with_section2(Sec,A,NA), mark_with_section2(Sec,B,NB). |
| 1480 | | mark_with_section2(Sec,In,Out) :- |
| 1481 | | add_texpr_infos(In,[section(Sec)],Out). |
| 1482 | | |
| 1483 | | type_initialisation_section(Sections,Name,MType,RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :- |
| 1484 | | write_section(initialisation,Initialisation,Old,New), |
| 1485 | | ( rawmachine_section(initialisation,Sections,Init) -> |
| 1486 | | visible_env(MType, initialisation, RefMachines, InitEnv, Ein, E1), |
| 1487 | | btype_ground_dl([Init],InitEnv,NonGroundExceptions,[subst],[TypedInit],E1,Eout), |
| 1488 | | Initialisation=[init(Name,TypedInit)] |
| 1489 | | ; otherwise -> |
| 1490 | | Ein=Eout, |
| 1491 | | Initialisation=[]). |
| 1492 | | |
| 1493 | | :- use_module(library(ugraphs)). |
| 1494 | | |
| 1495 | | type_operations_section(Sections,MType,RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :- |
| 1496 | | ~~mnf( write_section(operation_bodies,Operations,Old,New) ), |
| 1497 | | ~~mnf( visible_env(MType, operation_bodies, RefMachines, Env, Ein, E1) ), |
| 1498 | | ~~mnf( optional_rawmachine_section(operations,Sections,[],Ops1) ), |
| 1499 | | optional_rawmachine_section(local_operations,Sections,[], Ops2), |
| 1500 | | append(Ops2,Ops1,Ops), |
| 1501 | | topological_sort(Ops,Env,SOps), |
| 1502 | | (debug_mode(off) -> true ; length(SOps,NrOps),debug_stats(finished_topological_sorting(NrOps))), |
| 1503 | | same_length(SOps,Types), maplist(is_op_type,Types), |
| 1504 | | ~~mnf( btype_ground_dl(SOps,Env,NonGroundExceptions,Types,Operations,E1,Eout) ),!. |
| 1505 | | |
| 1506 | | allow_local_op_calls :- |
| 1507 | | (get_preference(allow_local_operation_calls,true) -> true ; get_preference(allow_operation_calls_in_expr,true)). |
| 1508 | | % perform a topological sort of the operations: treat called operation before calling operation |
| 1509 | | % only relevant when allow_local_operation_calls is set to true |
| 1510 | | topological_sort(Ops,Env,SortedOps) :- |
| 1511 | | allow_local_op_calls, |
| 1512 | | findall(OtherID-ID, (member(Op,Ops),op_calls_op(Op,Env,ID,OtherID)),Edges), |
| 1513 | | % print(edges(Edges)),nl, |
| 1514 | | % TO DO: maybe only store edges where OtherID also appears in Ops (i.e., call within same machine) |
| 1515 | | Edges \= [], |
| 1516 | | !, |
| 1517 | | findall(ID,(member(operation(_,RawID,_,_,_),Ops),raw_id(RawID,ID)),Vertices), %print(vertices(Vertices)),nl, |
| 1518 | | vertices_edges_to_ugraph(Vertices,Edges,Graph), |
| 1519 | | (top_sort(Graph,Sorted) |
| 1520 | | -> sort_ops(Sorted,Ops,SortedOps) |
| 1521 | | ; get_preference(allow_operation_calls_in_expr,true) -> |
| 1522 | | add_warning(topological_sort,'Mutual recursion or cycle in the (local) operation call graph, this may cause problems computing reads information: ',Edges), |
| 1523 | | SortedOps=Ops |
| 1524 | | % not a problem, because operations called in expressions are not allowed to modify the state |
| 1525 | | % TODO: however, we may have an issue with computing reads information correctly for mutual recursion !? |
| 1526 | | % direct recursion should be ok |
| 1527 | | ; add_error(topological_sort,'Cycle in the (local) operation call graph: ',Edges), |
| 1528 | | SortedOps=Ops). |
| 1529 | | topological_sort(Ops,_,Ops). |
| 1530 | | |
| 1531 | | sort_ops([],Ops,Ops). % Ops should be [] |
| 1532 | | sort_ops([OpID|T],Ops,Res) :- |
| 1533 | | raw_op_id(Op1,OpID), |
| 1534 | | (select(Op1,Ops,TOps) |
| 1535 | | -> Res = [Op1|TSOps], sort_ops(T,TOps,TSOps) |
| 1536 | | ; % operation from another machine |
| 1537 | | % print(could_not_find(OpID,Ops)),nl, |
| 1538 | | sort_ops(T,Ops,Res) |
| 1539 | | ). |
| 1540 | | |
| 1541 | | is_op_type(op(_,_)). |
| 1542 | | is_pred_type(pred). |
| 1543 | | |
| 1544 | | % compute which other operations are directly called |
| 1545 | | op_calls_op(operation(_,RawID,_,_,RawBody),Env,ID,OtherID) :- raw_id(RawID,ID), |
| 1546 | | raw_body_calls_operation(RawBody,ID,Env,OtherID). |
| 1547 | | |
| 1548 | | raw_body_calls_operation(RawBody,ID,Env,OtherID) :- |
| 1549 | | raw_member(OpCall,RawBody), |
| 1550 | | raw_op_call(OpCall,ID,Env,RawOtherID), raw_id(RawOtherID,OtherID). |
| 1551 | | |
| 1552 | | raw_op_call(operation_call(_,RawOtherID,_,_),_,_, RawOtherID). |
| 1553 | | raw_op_call(operation_call_in_expr(_,RawOtherID,_),ID,_, RawOtherID) :- |
| 1554 | | \+ raw_id(RawOtherID,ID). % we do not look direct recursion: it poses no problem for computing reads/writes info |
| 1555 | | raw_op_call(function(_,RawOtherID,_), ID, Env, RawOtherID) :- % function calls possibly not yet translated to operation_call_in_expr |
| 1556 | | get_preference(allow_operation_calls_in_expr,true), |
| 1557 | | \+ raw_id(RawOtherID,ID), % direct recursion ok |
| 1558 | | btypechecker:is_operation_call(RawOtherID,Env). |
| 1559 | | |
| 1560 | | raw_op_id(operation(_,RawID,_,_,_RawBody),ID) :- raw_id(RawID,ID). |
| 1561 | | raw_id(identifier(_,ID),ID). |
| 1562 | | |
| 1563 | | % a utility function to work on the raw AST Functor(POS,Arg1,...,Argn) |
| 1564 | | % this will not be able to look inside DEFINITIONS ! |
| 1565 | | % TO DO: deal with more raw substitutions which have list arguments |
| 1566 | | raw_member(X,X). |
| 1567 | | raw_member(X,parallel(_,List)) :- !, member(Term,List), raw_member(X,Term). |
| 1568 | | raw_member(X,sequence(_,List)) :- !, member(Term,List), raw_member(X,Term). |
| 1569 | | raw_member(X,[H|T]) :- !, (raw_member(X,H) ; raw_member(X,T)). |
| 1570 | | raw_member(X,Term) :- compound(Term), Term =.. [_Functor,_Pos|Args], |
| 1571 | | member(A,Args), raw_member(X,A). |
| 1572 | | |
| 1573 | | |
| 1574 | | create_section_identifiers(Section,DestSection,RawMachine,Old,New) :- |
| 1575 | | ~~mnf(write_section(DestSection,Vars,Old,New)), |
| 1576 | | ~~mnf(optional_rawmachine_section(Section,RawMachine,[],Identifiers)), |
| 1577 | | ~~mnf(create_section_ids2(Identifiers,[],Vars,DestSection,New)). |
| 1578 | | |
| 1579 | | create_section_ids2([],_,[],_,_). |
| 1580 | | create_section_ids2([Ext|Rest],Infos,Res,DestSection,MachSections) :- |
| 1581 | | expand_definition_to_variable_list(Ext,MachSections,List),!, |
| 1582 | | append(List,Rest,NewList), |
| 1583 | | create_section_ids2(NewList,Infos,Res,DestSection,MachSections). |
| 1584 | | create_section_ids2([Ext|Rest],Infos,Res,DestSection,MachSections) :- |
| 1585 | | create_section_id(Ext,Infos,DestSection,TId), |
| 1586 | | ( TId = error(Msg,Term,Pos) -> |
| 1587 | | Res = TRest, add_error(bmachine_construction,Msg,Term,Pos) |
| 1588 | | ; otherwise -> |
| 1589 | | Res = [TId|TRest]), |
| 1590 | | create_section_ids2(Rest,Infos,TRest,DestSection,MachSections). |
| 1591 | | create_section_id(Ext,Infos,DestSection,TId) :- |
| 1592 | | I=identifier(_), |
| 1593 | | ( ext2int(Ext,I,_Pos,_Type,I,Infos,TId) -> |
| 1594 | | true |
| 1595 | | ; unwrap_pragma(Ext,ID,PragmaInfos) -> append(PragmaInfos,Infos,FullInfos), |
| 1596 | | ext2int(ID,I,_,_,I,FullInfos,TId) |
| 1597 | | ; Ext = definition(POSINFO,ID,_) -> |
| 1598 | | TId = error('Trying to use DEFINITION name as identifier: ', |
| 1599 | | (ID,within(DestSection)), POSINFO) |
| 1600 | | ; otherwise -> |
| 1601 | | TId = error('Illegal identifier: ', |
| 1602 | | (Ext,within(DestSection)), Ext) |
| 1603 | | ). |
| 1604 | | |
| 1605 | | % support using DEFINITIONS which are variable lists; |
| 1606 | | % currently for ProB parser you need to write VARS == (x,y,..) for Atelier-B: VARS == x,y,.. |
| 1607 | | expand_definition_to_variable_list(definition(_POSINFO,ID,_),MachSections,List) :- |
| 1608 | | get_section(definitions,MachSections,Defs), |
| 1609 | | member(definition_decl(ID,expression,_InnerPos,[],RawExpr,_Deps),Defs), |
| 1610 | | extract_identifier_list(RawExpr,List,[]). |
| 1611 | | |
| 1612 | | % convert a raw tuple into a raw identifier list: |
| 1613 | | extract_identifier_list(identifier(Pos,ID)) --> [identifier(Pos,ID)]. |
| 1614 | | extract_identifier_list(couple(_,List)) --> |
| 1615 | | extract_identifier_list(List). |
| 1616 | | extract_identifier_list([]) --> []. |
| 1617 | | extract_identifier_list([H|T]) --> extract_identifier_list(H), extract_identifier_list(T). |
| 1618 | | |
| 1619 | | |
| 1620 | | unwrap_pragma(description(_,D,ID),ID,[description(D)]). |
| 1621 | | unwrap_pragma(unit(_,U,ID),ID,[unit(U)]). |
| 1622 | | unwrap_pragma(new_unit(_,U,ID),ID,[new_unit(U)]). |
| 1623 | | unwrap_pragma(inferred_unit(_,_,ID),ID,[]). % currently ignored |
| 1624 | | unwrap_pragma(inferredunit(_,_,ID),ID,[]). % currently ignored |
| 1625 | | |
| 1626 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1627 | | % sort the machines topologically |
| 1628 | | |
| 1629 | | machine_order(Machines,Order) :- |
| 1630 | | machine_dependencies(Machines,Dependencies), |
| 1631 | | topsort(Dependencies,Order). |
| 1632 | | |
| 1633 | | % sort the machines topologically |
| 1634 | | topsort(Deps,Sorted) :- |
| 1635 | | topsort2(Deps,[],Sorted). |
| 1636 | | topsort2([],_,[]) :- !. |
| 1637 | | topsort2(Deps,Known,Sorted) :- |
| 1638 | | split_list(all_deps_known(Known),Deps,DAvailable,DNotAvailable), |
| 1639 | | DAvailable = [_|_], % we have new machines available whose dependencies are all known |
| 1640 | | !, |
| 1641 | | maplist(dep_name,DAvailable,Available), |
| 1642 | | append(Available,Known,NewKnown), |
| 1643 | | append(Available,Rest,Sorted), |
| 1644 | | topsort2(DNotAvailable,NewKnown,Rest). |
| 1645 | | topsort2(Deps,_Known,_) :- |
| 1646 | | member(dep(Name,NameDeps),Deps), |
| 1647 | | add_error(bmachine_construction,'Could not resolve machine dependencies for: ',Name:depends_on(NameDeps)), |
| 1648 | | fail. |
| 1649 | | |
| 1650 | ? | all_deps_known(K,dep(_Name,Deps)) :- sort(Deps,DS),sort(K,KS),subseq0(KS,DS),!. |
| 1651 | | dep_name(dep(Name,_Deps),Name). |
| 1652 | | |
| 1653 | | % find dependencies between machines |
| 1654 | | machine_dependencies(Machines,Dependencies) :- |
| 1655 | | maplist(machine_dependencies2,Machines,Deps), |
| 1656 | | sort(Deps,Dependencies). |
| 1657 | | machine_dependencies2(M,dep(Name,Deps)) :- |
| 1658 | | get_constructed_machine_name_and_body(M,Name,_,Body), |
| 1659 | | findall(Ref, |
| 1660 | | (refines(M,Ref);machine_reference(Body,Ref)), |
| 1661 | | Deps). |
| 1662 | | |
| 1663 | | machine_reference(MachineBody,Ref) :- |
| 1664 | ? | ( member(sees(_,R),MachineBody) |
| 1665 | | ; member(uses(_,R),MachineBody) ), |
| 1666 | ? | member(identifier(_,PrefixRef),R), |
| 1667 | | split_prefix(PrefixRef,_,Ref). |
| 1668 | | machine_reference(MachineBody,Ref) :- |
| 1669 | ? | ( member(includes(_,R),MachineBody) |
| 1670 | ? | ; member(extends(_,R),MachineBody) |
| 1671 | | ; member(imports(_,R),MachineBody) ), |
| 1672 | ? | member(machine_reference(_,PrefixRef,_),R), |
| 1673 | | split_prefix(PrefixRef,_,Ref). |
| 1674 | | |
| 1675 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1676 | | % refinements |
| 1677 | | merge_refinement_and_abstraction(Concrete,RefMachines,Result,Ein,Eout) :- |
| 1678 | | memberchk(ref(abstraction,Abstraction),RefMachines), |
| 1679 | | append_sections([sets,concrete_constants,concrete_variables],Abstraction,Concrete,M1), |
| 1680 | | append_if_new(abstract_constants,Abstraction,M1,M2), |
| 1681 | | get_section(properties,Abstraction,AbstractProperties), |
| 1682 | | conjunct_to_section(properties,AbstractProperties,M2,M3), |
| 1683 | | % now get current invariant Invariant and filter out gluing/linking invariant |
| 1684 | | % (the linking invariant talks about variables which no longer exist; hence we cannot check it anymore) |
| 1685 | | select_section(invariant,Invariant,FullConcreteInvariant,M3,M4), |
| 1686 | | write_section(linking_invariant,LinkingInvariant,M4,Merged), |
| 1687 | | % we now also copy from the abstraction those invariants which are still valid |
| 1688 | | get_section(invariant,Abstraction,AbstractInvariant), |
| 1689 | | filter_abstract_invariant(AbstractInvariant,Concrete,AbsInvariantStillValid), |
| 1690 | | filter_linking_invariant(Invariant,LinkingInvariant,ConcreteInvariant), |
| 1691 | | conjunct_predicates([AbsInvariantStillValid,ConcreteInvariant],FullConcreteInvariant), |
| 1692 | | propagate_abstract_operations(Abstraction,Merged,RefMachines,Result,Ein,Eout). |
| 1693 | | merge_refinement_and_abstraction(Machine,_,Machine,Errors,Errors). |
| 1694 | | |
| 1695 | | % append sections from abstract machine to concrete machine: |
| 1696 | | append_sections(Sections,AbsMachine,Old,New) :- |
| 1697 | | expand_shortcuts(Sections,AllSections), |
| 1698 | | append_sections2(AllSections,AbsMachine,Old,New). |
| 1699 | | append_sections2([],_,M,M). |
| 1700 | | append_sections2([Section|Rest],AbsMachine,Old,New) :- |
| 1701 | | get_section(Section,AbsMachine,Content), |
| 1702 | | append_to_section(Section,Content,Old,Inter), |
| 1703 | | append_sections2(Rest,AbsMachine,Inter,New). |
| 1704 | | |
| 1705 | | :- assert_must_succeed((create_machine(abs,EA), create_machine(conc,EB), |
| 1706 | | write_section(abstract_constants,[b(identifier(x),integer,[some_info])],EA,A), |
| 1707 | | write_section(abstract_constants,[b(identifier(x),integer,[other_info]), |
| 1708 | | b(identifier(y),integer,[info])],EB,B), |
| 1709 | | append_if_new(abstract_constants,A,B,ResultM), |
| 1710 | | get_section(abstract_constants,ResultM,ResultConst), |
| 1711 | | ResultConst==[b(identifier(x),integer,[other_info]), |
| 1712 | | b(identifier(y),integer,[info])] |
| 1713 | | )). |
| 1714 | | |
| 1715 | | append_if_new(Section,Machine,In,Out) :- |
| 1716 | | get_section(Section,Machine,Content), |
| 1717 | | select_section(Section,Old,New,In,Out), |
| 1718 | | get_texpr_ids(Old,ExistingIds), |
| 1719 | | exclude(is_in_existing_ids(ExistingIds),Content,NewElements), |
| 1720 | | append(Old,NewElements,New). |
| 1721 | | is_in_existing_ids(ExistingIds,TId) :- |
| 1722 | | get_texpr_id(TId,Id), |
| 1723 | | memberchk(Id,ExistingIds). |
| 1724 | | |
| 1725 | | % filter linking and concrete invaraint |
| 1726 | | filter_linking_invariant(Invariant,Linking,Concrete) :- |
| 1727 | | split_conjuncts(Invariant,Predicates), |
| 1728 | | split_list(contains_abstraction_refs,Predicates,Linkings,Concretes), |
| 1729 | | conjunct_predicates(Linkings,Linking), |
| 1730 | | conjunct_predicates(Concretes,Concrete). |
| 1731 | | |
| 1732 | | |
| 1733 | | % contains_abstraction_refs can be used on predicates of the current machine: the abstraction info field has been computed for this machine |
| 1734 | | contains_abstraction_refs(TExpr) :- |
| 1735 | | syntaxtraversion(TExpr,_,_,Infos,Subs,_), |
| 1736 | | ( memberchk(abstraction,Infos) % This info field comes from the last argument of visibility/6 |
| 1737 | | -> true |
| 1738 | | ; member(Sub,Subs), |
| 1739 | | contains_abstraction_refs(Sub)). |
| 1740 | | |
| 1741 | | :- use_module(tools_lists,[ord_member_nonvar_chk/2]). |
| 1742 | | % Determine which part of the abstract invariant can be imported into the refinement machine |
| 1743 | | filter_abstract_invariant(AbsInvariant,ConcreteMachine,ConcreteInv) :- |
| 1744 | | split_conjuncts(AbsInvariant,Predicates), |
| 1745 | | get_machine_sorted_variables(ConcreteMachine,SortedConcrVars), |
| 1746 | | split_list(contains_abstract_variables(SortedConcrVars),Predicates,_Discard,Concretes), |
| 1747 | | %print(discarded(_Discard)),nl, |
| 1748 | | conjunct_predicates(Concretes,ConcreteInv). %, print('COPY: '), translate:print_bexpr(Concrete),nl. |
| 1749 | | contains_abstract_variables(SortedConcrVars,TExpr) :- |
| 1750 | | syntaxtraversion(TExpr,Expr,Type,Infos,Subs,_), |
| 1751 | | ( memberchk(loc(_,_,abstract_variables),Infos) % are there other things that pose problems: abstract_constants ? |
| 1752 | | -> %print('Abs: '),translate:print_bexpr(TExpr),nl, print(SortedConcrVars),nl, |
| 1753 | | \+ ord_member_nonvar_chk(b(Expr,Type,_),SortedConcrVars) % otherwise variable is re-introduced with same type |
| 1754 | | % in some Event-B models: VARIABLES keyword is used and in refinement VARIABLES are re-listed |
| 1755 | | % TO DO: check what happens when variable not immediately re-introduced |
| 1756 | | ; member(Sub,Subs), |
| 1757 | | contains_abstract_variables(SortedConcrVars,Sub)), print('Filtering INV: '),translate:print_bexpr(TExpr),nl. |
| 1758 | | |
| 1759 | | get_machine_sorted_variables(Machine,SortedAllVars) :- |
| 1760 | | get_section(abstract_variables,Machine,AbsVars), |
| 1761 | | get_section(concrete_variables,Machine,ConcVars), |
| 1762 | | append(ConcVars,AbsVars,AllVars), |
| 1763 | | sort(AllVars,SortedAllVars). |
| 1764 | | |
| 1765 | | split_conjuncts(Expr,List) :- |
| 1766 | | split_conjuncts2(Expr,List,[]). |
| 1767 | | split_conjuncts2(Expr) --> |
| 1768 | | {get_texpr_expr(Expr,conjunct(A,B)),!}, |
| 1769 | | split_conjuncts2(A), |
| 1770 | | split_conjuncts2(B). |
| 1771 | | split_conjuncts2(Expr) --> [Expr]. |
| 1772 | | |
| 1773 | | % copy the abstract operations or re-use their preconditions |
| 1774 | | propagate_abstract_operations(Abstract,Concrete,RefMachines,Result,Ein,Eout) :- |
| 1775 | | get_section(promoted,Abstract,APromoted), |
| 1776 | | get_section(operation_bodies,Abstract,ABodies), |
| 1777 | | % signature: select_section(SecName,OldContent,NewContent,OldMachine,NewMachine) |
| 1778 | | select_section(promoted,CPromotedIn,CPromotedOut,Concrete,Concrete2), |
| 1779 | | select_section(operation_bodies,CBodiesIn,CBodiesOut,Concrete2,Result), |
| 1780 | | propagate_aops(APromoted,ABodies,RefMachines,CPromotedIn,CBodiesIn,CPromotedOut,CBodiesOut,Ein,Eout). |
| 1781 | | propagate_aops([],_ABodies,_RefMachines,CPromoted,CBodies,CPromoted,CBodies,Errors,Errors). |
| 1782 | | propagate_aops([APromoted|ApRest],ABodies,RefMachines,CPromotedIn,CBodiesIn,CPromotedOut,CBodiesOut,Ein,Eout) :- |
| 1783 | | get_operation(APromoted,ABodies,AbstractOp), |
| 1784 | | def_get_texpr_id(APromoted,op(APromotedOpName)), |
| 1785 | | copy_texpr_wo_info(APromoted,CProm), |
| 1786 | | ( member(CProm,CPromotedIn) -> |
| 1787 | | debug_format(19,'Refining promoted abstract operation ~w to refinement machine.~n',[APromotedOpName]), |
| 1788 | | extract_concrete_preconditions(AbstractOp,RefMachines,Pre), |
| 1789 | | change_operation(APromoted,ConcreteOpOld,ConcreteOpNew,CBodiesIn,CBodiesRest), |
| 1790 | | add_precondition(Pre,ConcreteOpOld,ConcreteOpNew), |
| 1791 | | CPromotedIn = CPromotedRest, |
| 1792 | | Ein = E1 |
| 1793 | | % TO DO: do not copy if event is refined at least once with renaming ! |
| 1794 | | ; is_refined_by_some_event(APromotedOpName,CPromotedIn,ConcreteOpName) -> |
| 1795 | | debug_format(19,'Not copying abstract operation ~w to refinement machine, as it is refined by ~w.~n',[APromotedOpName,ConcreteOpName]), |
| 1796 | | CPromotedRest=CPromotedIn, CBodiesRest=CBodiesIn, |
| 1797 | | E1=Ein |
| 1798 | | ; otherwise -> |
| 1799 | | debug_format(19,'Copying abstract operation ~w to refinement machine, as it is not refined.~n',[APromotedOpName]), |
| 1800 | | % TO DO: check that this is also the right thing to do for Atelier-B Event-B |
| 1801 | | check_copied_operation(APromoted,AbstractOp,RefMachines,Ein,E1), |
| 1802 | | append(CPromotedIn,[APromoted],CPromotedRest), |
| 1803 | | append(CBodiesIn,[AbstractOp],CBodiesRest) |
| 1804 | | ), |
| 1805 | | propagate_aops(ApRest,ABodies,RefMachines,CPromotedRest,CBodiesRest,CPromotedOut,CBodiesOut,E1,Eout). |
| 1806 | | |
| 1807 | | is_refined_by_some_event(AbstractName,CPromotedList,ConcreteName) :- |
| 1808 | | member(TID,CPromotedList), |
| 1809 | | get_texpr_info(TID,Infos), |
| 1810 | | memberchk(refines_operation(AbstractName),Infos), |
| 1811 | | def_get_texpr_id(TID,ConcreteName). |
| 1812 | | |
| 1813 | | get_operation(TId,Bodies,Operation) :- |
| 1814 | | select_operation(TId,Bodies,Operation,_BodiesRest). |
| 1815 | | change_operation(TId,OldOp,NewOp,OldBodies,[NewOp|NewBodies]) :- |
| 1816 | | select_operation(TId,OldBodies,OldOp,NewBodies). |
| 1817 | | select_operation(TId,Bodies,Operation,BodiesRest) :- |
| 1818 | | copy_texpr_wo_info(TId,OpId), |
| 1819 | | get_texpr_expr(Operation,operation(OpId,_,_,_)), |
| 1820 | | select(Operation,Bodies,BodiesRest),!. |
| 1821 | | |
| 1822 | | extract_concrete_preconditions(Op,RefMachines,FPre) :- |
| 1823 | | extract_preconditions_op(Op,Pre), |
| 1824 | | extract_op_arguments(Op,Args), |
| 1825 | | conjunction_to_list(Pre,Pres), |
| 1826 | | % todo: check the "machine" parameter |
| 1827 | | visible_env(machine,operation_bodies,RefMachines,Env1,_Errors,[]), |
| 1828 | | store_variables(Args,Env1,Env), |
| 1829 | | filter_predicates_with_unknown_identifiers(Pres,Env,FPres), |
| 1830 | | conjunct_predicates(FPres,FPre). |
| 1831 | | |
| 1832 | | extract_op_arguments(Op,Params) :- |
| 1833 | | get_texpr_expr(Op,operation(_,_,Params,_)). |
| 1834 | | |
| 1835 | | extract_preconditions_op(OpExpr,Pre) :- |
| 1836 | | get_texpr_expr(OpExpr,operation(_,_,_,Subst)), |
| 1837 | | extract_preconditions(Subst,Pres,_), |
| 1838 | | conjunct_predicates(Pres,Pre). |
| 1839 | | extract_preconditions(TExpr,Pres,Inner) :- |
| 1840 | | get_texpr_expr(TExpr,Expr), |
| 1841 | | extract_preconditions2(Expr,TExpr,Pres,Inner). |
| 1842 | | extract_preconditions2(precondition(Pre,Subst),_,[Pre|Pres],Inner) :- !, |
| 1843 | | extract_preconditions(Subst,Pres,Inner). |
| 1844 | | extract_preconditions2(block(Subst),_,Pres,Inner) :- !, |
| 1845 | | extract_preconditions(Subst,Pres,Inner). |
| 1846 | | extract_preconditions2(_,Inner,[],Inner). |
| 1847 | | |
| 1848 | | filter_predicates_with_unknown_identifiers([],_Env,[]). |
| 1849 | | filter_predicates_with_unknown_identifiers([Pred|Prest],Env,Result) :- |
| 1850 | | ( find_unknown_identifier(Pred,Env,_Id) -> |
| 1851 | | !,Result = Rrest |
| 1852 | | ; otherwise -> |
| 1853 | | Result = [Pred|Rrest]), |
| 1854 | | filter_predicates_with_unknown_identifiers(Prest,Env,Rrest). |
| 1855 | | find_unknown_identifier(Pred,Env,Id) :- |
| 1856 | | get_texpr_id(Pred,Id),!, |
| 1857 | | \+ env_lookup_type(Id,Env,_). |
| 1858 | | find_unknown_identifier(Pred,Env,Id) :- |
| 1859 | | syntaxtraversion(Pred,_,_,_,Subs,Names), |
| 1860 | | store_variables(Names,Env,Subenv), |
| 1861 | | find_unknown_identifier_l(Subs,Subenv,Id). |
| 1862 | | find_unknown_identifier_l([S|_],Env,Id) :- |
| 1863 | | find_unknown_identifier(S,Env,Id),!. |
| 1864 | | find_unknown_identifier_l([_|Rest],Env,Id) :- |
| 1865 | | find_unknown_identifier_l(Rest,Env,Id). |
| 1866 | | |
| 1867 | | add_precondition(Pre,Old,New) :- |
| 1868 | | remove_bt(Old,operation(Id,Res,Params,Subst),operation(Id,Res,Params,NewSubst),New), |
| 1869 | | extract_preconditions(Subst,OldPres,Inner), |
| 1870 | | conjunct_predicates([Pre|OldPres],NewPre), |
| 1871 | | create_texpr(precondition(NewPre,Inner),subst,[],NewSubst). |
| 1872 | | |
| 1873 | | |
| 1874 | | check_copied_operation(OpRef,Op,RefMachines,Ein,Eout) :- |
| 1875 | | % todo: check the "refinement" parameter |
| 1876 | | visible_env(refinement,operation_bodies,RefMachines,Env1,_Errors,[]), |
| 1877 | | get_texpr_id(OpRef,OpId),get_texpr_type(OpRef,OpType), |
| 1878 | | env_store(OpId,OpType,[],Env1,Env), |
| 1879 | | findall(U, find_unknown_identifier(Op,Env,U), Unknown1), |
| 1880 | | sort(Unknown1,Unknown), |
| 1881 | | ( Unknown=[] -> Ein=Eout |
| 1882 | | ; otherwise -> |
| 1883 | | op(OpName) = OpId, |
| 1884 | | join_ids(Unknown,IdList), |
| 1885 | | (Unknown = [_] -> Plural=[]; Plural=['s']), |
| 1886 | | append([['Operation ',OpName, |
| 1887 | | ' was copied from abstract machine but the identifier'], |
| 1888 | | Plural, |
| 1889 | | [' '], |
| 1890 | | IdList, |
| 1891 | | [' cannot be seen anymore']],Msgs), |
| 1892 | | ajoin(Msgs,Msg), Ein = [error(Msg,none)|Eout] |
| 1893 | | ). |
| 1894 | | join_ids([I],[Msg]) :- !,opname(I,Msg). |
| 1895 | | join_ids([A|Rest],[Msg,','|Mrest]) :- opname(A,Msg),join_ids(Rest,Mrest). |
| 1896 | | opname(op(Id),Id) :- !. |
| 1897 | | opname(Id,Id). |
| 1898 | | |
| 1899 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1900 | | % split an identifier into a (possible empty) prefix and the name itself |
| 1901 | | % e.g. split_prefix('path.to.machine', 'path.to', 'machine'). |
| 1902 | | split_prefix(Term,Prefix,Main) :- |
| 1903 | | one_arg_term(Functor,Arg,Term),!, |
| 1904 | | one_arg_term(Functor,MArg,Main), |
| 1905 | | split_prefix(Arg,Prefix,MArg). |
| 1906 | | split_prefix(PR,Prefix,Main) :- %print(split_prefix(PR,Prefix,Main)),nl,trace, |
| 1907 | | safe_atom_chars(PR,Chars,split_prefix1), |
| 1908 | | split_prefix2(Chars,Chars,[],CPrefix,CMain), |
| 1909 | | safe_atom_chars(Main,CMain,split_prefix2), |
| 1910 | | safe_atom_chars(Prefix,CPrefix,split_prefix3). |
| 1911 | | split_prefix2([],Main,_,[],Main). |
| 1912 | | split_prefix2([C|Rest],Previous,PrefBefore,Prefix,Main) :- |
| 1913 | | ( C='.' -> |
| 1914 | | append(PrefBefore,RestPrefix,Prefix), |
| 1915 | | split_prefix2(Rest,Rest,[C],RestPrefix,Main) |
| 1916 | | ; otherwise -> |
| 1917 | | append(PrefBefore,[C],NextPref), |
| 1918 | | split_prefix2(Rest,Previous,NextPref,Prefix,Main)). |
| 1919 | | |
| 1920 | | rawmachine_section(Elem,List,Result) :- % |
| 1921 | | functor(Pattern,Elem,2), |
| 1922 | | arg(2,Pattern,Result), |
| 1923 | ? | select(Pattern,List,Rest),!, |
| 1924 | | (functor(Pattern2,Elem,2),member(Pattern2,Rest) |
| 1925 | | -> arg(1,Pattern2,Pos), |
| 1926 | | add_error(bmachine_construction,'Multiple sections for: ',Elem,Pos) |
| 1927 | | ; true). |
| 1928 | | |
| 1929 | | optional_rawmachine_section(Elem,List,Default,Result) :- |
| 1930 | | ( rawmachine_section(Elem,List,Result1) -> true |
| 1931 | | ; Result1=Default), |
| 1932 | | Result1=Result. |
| 1933 | | |
| 1934 | | one_arg_term(Functor,Arg,Term) :- %print(one_arg_term(Functor,Arg,Term)),nl, |
| 1935 | | functor(Term,Functor,1),arg(1,Term,Arg). |
| 1936 | | |
| 1937 | | % check if a rawmachine section list has a given section |
| 1938 | | rawmachine_section_exists(Elem,List) :- % |
| 1939 | | functor(Pattern,Elem,2), |
| 1940 | ? | (member(Pattern,List) -> true). |
| 1941 | | |
| 1942 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1943 | | % visibility rules |
| 1944 | | |
| 1945 | | % the visibility/5 predicate declares what a part of a machine can see |
| 1946 | | % visibility(MType, Scope, Section, Access, Info) means: |
| 1947 | | % In a machine of type MType (machine, refinement, implementation), |
| 1948 | | % an expression in a Section (like invariant) can see |
| 1949 | | % the identifiers in the Access sections. Access is a list of |
| 1950 | | % sections, where shortcuts are allowed (see shortcut/2, e.g., shortcut(operations,[unpromoted,promoted]).). |
| 1951 | | % Scope defines where (in relation to the Section) |
| 1952 | | % the section in Access are (local: same machine, included: in an |
| 1953 | | % included machine, etc.) |
| 1954 | | % Info is a list of additional information that is added to each |
| 1955 | | % identifier in the environment to build up. E.g. in an operation |
| 1956 | | % definition, constants are marked readonly. |
| 1957 | | visibility(machine, local, constraints, [parameters],[]). |
| 1958 | | visibility(machine, local, includes, [parameters,sets,constants],[]). |
| 1959 | | visibility(machine, local, properties, [sets,constants],[]). |
| 1960 | | visibility(machine, local, invariant, [parameters,sets,constants,variables],[]). |
| 1961 | | visibility(machine, local, operation_bodies, [parameters,sets,constants],[readonly]). |
| 1962 | | visibility(machine, local, operation_bodies, [operations],Info) :- |
| 1963 | | (get_preference(allow_operation_calls_in_expr,true) -> Info = [inquiry] |
| 1964 | | ; Info =[readonly,dontcall] ). |
| 1965 | | visibility(machine, local, operation_bodies, [variables],[]). |
| 1966 | ? | visibility(machine, local, initialisation, Access,[not_initialised|Info]) :- visibility(machine,local,operation_bodies,Access,Info). |
| 1967 | | |
| 1968 | | visibility(machine, Scope, assertions, [Allow],[inquiry]) :- |
| 1969 | | (Scope = local -> Allow=operations ; Allow=promoted), |
| 1970 | | get_preference(allow_operation_calls_in_expr,true). % if we allow calling operations in expressions |
| 1971 | | visibility(machine, Scope, invariant, [promoted],[inquiry]) :- Scope \= local, |
| 1972 | | get_preference(allow_operation_calls_in_expr,true). |
| 1973 | | |
| 1974 | | visibility(machine, included, properties, [sets,constants],[]). |
| 1975 | | visibility(machine, included, invariant, [sets,constants,variables],[]). |
| 1976 | | visibility(machine, included, operation_bodies, [sets,constants,variables],[readonly]). |
| 1977 | | visibility(machine, included, operation_bodies, [promoted],Info) :- get_operation_call_info(Info). |
| 1978 | | visibility(machine, included, initialisation, [sets,constants,variables,promoted],[readonly]). |
| 1979 | | |
| 1980 | | visibility(machine, used, properties, [sets,constants],[]). |
| 1981 | | visibility(machine, used, invariant, [parameters,sets,constants,variables],[]). |
| 1982 | | visibility(machine, used, operation_bodies, [parameters,sets,constants,variables],[readonly]). |
| 1983 | | visibility(machine, used, initialisation, [parameters,sets,constants,variables],[readonly]). |
| 1984 | | visibility(machine, used, operation_bodies, [operations],[inquiry]). %% added by leuschel |
| 1985 | | |
| 1986 | | visibility(machine, seen, includes, [sets,constants],[]). |
| 1987 | | visibility(machine, seen, properties, [sets,constants],[]). |
| 1988 | | visibility(machine, seen, invariant, [sets,constants],[]). |
| 1989 | | visibility(machine, seen, operation_bodies, [sets,constants,variables],[readonly]). |
| 1990 | | visibility(machine, seen, initialisation, [sets,constants,variables],[readonly]). |
| 1991 | | visibility(machine, seen, operation_bodies, [operations],[inquiry]). %% added by leuschel |
| 1992 | | |
| 1993 | | visibility(refinement, local, Section, Access, Info) :- |
| 1994 | | Section \= assertions, % assertions are handled below |
| 1995 | | visibility(machine, local, Section, Access, Info). |
| 1996 | | |
| 1997 | | visibility(refinement, abstraction, includes, [sets,concrete_constants],[]). |
| 1998 | | visibility(refinement, abstraction, properties, [sets,constants],[]). |
| 1999 | | visibility(refinement, abstraction, invariant, [sets,constants,concrete_variables],[]). |
| 2000 | | visibility(refinement, abstraction, invariant, [abstract_variables],[abstraction]). |
| 2001 | | visibility(refinement, abstraction, operation_bodies, [sets,concrete_constants],[readonly]). |
| 2002 | | visibility(refinement, abstraction, operation_bodies, [concrete_variables],[]). |
| 2003 | | |
| 2004 | | visibility(refinement, included, properties, [sets,constants],[]). |
| 2005 | | visibility(refinement, included, invariant, [sets,constants,variables],[]). |
| 2006 | | visibility(refinement, included, operation_bodies, [sets,constants,variables,promoted],[re]). % What is re ??? TO DO: investigate |
| 2007 | | |
| 2008 | | visibility(refinement, seen, includes, [sets,constants],[]). |
| 2009 | | visibility(refinement, seen, properties, [sets,constants],[]). |
| 2010 | | visibility(refinement, seen, invariant, [sets,constants],[]). |
| 2011 | | visibility(refinement, seen, operation_bodies, [sets,constants,variables],[readonly]). |
| 2012 | | visibility(refinement, seen, operation_bodies, [operations],[inquiry]). |
| 2013 | | |
| 2014 | | visibility(refinement, Ref, initialisation, Access, [not_initialised|Info]) :- |
| 2015 | | visibility(refinement,Ref,operation_bodies,Access,Info). |
| 2016 | | |
| 2017 | | % assertions have same visibility as invariant |
| 2018 | | visibility(MType, Ref, assertions, Part, Access) :- |
| 2019 | ? | visibility(MType,Ref,invariant,Part,Access). |
| 2020 | | |
| 2021 | | visibility(implementation, Ref, Section, Part, Access) :- |
| 2022 | | visibility(refinement, Ref, Section, Part, Access). |
| 2023 | | visibility(implementation, included, values_expression, [concrete_constants,sets],[]). |
| 2024 | | visibility(implementation, seen, values_expression, [concrete_constants,sets],[]). |
| 2025 | | |
| 2026 | | % For predicates over pre- and poststates |
| 2027 | | visibility(MType, Rev, prepost, Access, Info) :- |
| 2028 | ? | visibility(MType, Rev, invariant, Access, Info). |
| 2029 | | visibility(MType, Rev, prepost, Access, [primed,poststate|Info]) :- |
| 2030 | ? | visibility(MType, Rev, invariant, Access, Info). |
| 2031 | | |
| 2032 | | % add error messages for some common mistakes (access to parameters in the properties) |
| 2033 | | visibility(machine, local, properties, [parameters], [error('a parameter cannot be accessed in the PROPERTIES section')]). |
| 2034 | | % the following rule should be helpful for the user, but additionally it also |
| 2035 | | % provides a mechanism to re-introduce abstract variables in the INVARIANT |
| 2036 | | % section of a while loop (to enable this, an identifier is also marked with "abstraction") |
| 2037 | | visibility(refinement, abstraction, operation_bodies, [abstract_variables], [error('illegal access to an abstract variable in an operation'),abstraction]). |
| 2038 | | |
| 2039 | | get_operation_call_info(Info) :- |
| 2040 | | (get_preference(allow_operation_calls_in_expr,true) -> Info = [inquiry] ; Info=[readonly]). |
| 2041 | | |
| 2042 | | % lookups up all identifier sections that are accessible from |
| 2043 | | % the given section, removes all shortcuts and removes |
| 2044 | | % duplicate entries |
| 2045 | | % |
| 2046 | | % Returns a list of vis(Section,Info) where Section is the |
| 2047 | | % identifier section that can be seen with Info as a list |
| 2048 | | % of additional information |
| 2049 | | expanded_visibility(MType, Ref, Part, Access) :- |
| 2050 | | findall(vis(Section,Infos), |
| 2051 | | ( visibility(MType,Ref,Part,Sections1,Infos), |
| 2052 | | expand_shortcuts(Sections1,Sections), |
| 2053 | | member(Section,Sections)), |
| 2054 | | Access1), |
| 2055 | | sort(Access1,Access). |
| 2056 | | |
| 2057 | | % visible_env/6 creates a type environment for a certain |
| 2058 | | % part of a machine by looking up which identifier should |
| 2059 | | % be visible from there and what additional information should |
| 2060 | | % be added (e.g. to restrict access to read-only) |
| 2061 | | % |
| 2062 | | % The visibility/6 facts are used to define which identifier are visible |
| 2063 | | % |
| 2064 | | % MType: machine type (machine, refinement, ...) |
| 2065 | | % Part: part of the machine for which the environment should be created |
| 2066 | | % RefMachines: referred machines that are already typed |
| 2067 | | % Env: The created environment |
| 2068 | | % Errors: errors might be added if multiple variables with the same identifier |
| 2069 | | % are declared |
| 2070 | | visible_env(MType, Part, RefMachines, Env, Err_in, Err_out) :- |
| 2071 | | env_empty(Init), |
| 2072 | | visible_env(MType, Part, RefMachines, Init, Env, Err_in, Err_out). |
| 2073 | | % visible_env/7 is like visible_env/6, but an initial environment |
| 2074 | | % can be given in "In" |
| 2075 | | visible_env(MType, Part, RefMachines, In, Out, Err_in, Err_out) :- |
| 2076 | | foldl(visible_env2(MType,Part),RefMachines,In/Err_in,Out/Err_out). |
| 2077 | | visible_env2(MType,Part,ref(Scope,Machine),InEnvErr,OutEnvErr) :- |
| 2078 | | get_machine_name(Machine,MName), |
| 2079 | | debug_println(9,visible_env2(MName,Scope)), |
| 2080 | | ( Scope == local -> |
| 2081 | | ~~mnf(get_section(definitions,Machine,Defs)), |
| 2082 | | %nl,print(adding_defs(Defs)),nl,nl, |
| 2083 | | foldl(env_add_def(MName),Defs,InEnvErr,InterEnvErr) |
| 2084 | | ; otherwise -> |
| 2085 | | InEnvErr=InterEnvErr), |
| 2086 | | ~~mnf(expanded_visibility(MType, Scope, Part, Access)), |
| 2087 | | foldl(create_vis_env(Scope,MName,Machine),Access,InterEnvErr,OutEnvErr). |
| 2088 | | env_add_def(MName,definition_decl(Name,PType,Pos,Params,Body,_Deps),InEnvErr,OutEnvErr) :- |
| 2089 | | Type = definition(PType,Params,Body), |
| 2090 | | Info = [nodeid(Pos),loc(local,MName,definitions)], |
| 2091 | | create_texpr(identifier(Name),Type,Info,TExpr), |
| 2092 | | add_unique_variable(TExpr,InEnvErr,OutEnvErr),!. |
| 2093 | | env_add_def(MName,Def,EnvErr,EnvErr) :- |
| 2094 | | add_internal_error('Cannot deal with DEFINITION: ',env_add_def(MName,Def,EnvErr,EnvErr)). |
| 2095 | | |
| 2096 | | create_vis_env(Scope,MName,IDS,vis(Section,Infos),InEnvErr,OutEnvErr) :- |
| 2097 | | ~~mnf(get_section(Section,IDS,Identifiers1)), |
| 2098 | | maplist(add_infos_to_identifier([loc(Scope,MName,Section)|Infos]),Identifiers1,Identifiers), |
| 2099 | | foldl(add_unique_variable,Identifiers,InEnvErr,OutEnvErr). |
| 2100 | | |
| 2101 | | add_unique_variable(Var1,Old/Err_in,New/Err_out) :- |
| 2102 | | optionally_rewrite_id(Var1,Var), |
| 2103 | | get_texpr_id(Var,Id), |
| 2104 | | get_texpr_type(Var,Type), |
| 2105 | | get_texpr_info(Var,InfosOfNew),!, |
| 2106 | | ( env_lookup_type(Id,Old,_) -> |
| 2107 | | % we have a collision of two identifiers |
| 2108 | | handle_collision(Var,Id,Type,Old,InfosOfNew,New,Err_in,Err_out) |
| 2109 | | ; otherwise -> |
| 2110 | | % no collision, just introduce the new identifier |
| 2111 | | env_store(Id,Type,InfosOfNew,Old,New), |
| 2112 | | Err_in=Err_out |
| 2113 | | ). |
| 2114 | | add_unique_variable(Var,Env/Err,Env/Err) :- |
| 2115 | | ( Var = b(definition(DEFNAME,_),_,INFO) -> |
| 2116 | | add_error(add_unique_variable,'DEFINITION used in place of Identifier: ',DEFNAME,INFO) |
| 2117 | | ; otherwise -> |
| 2118 | | add_error(add_unique_variable,'Expected Identifier, but got: ',Var,Var) |
| 2119 | | ). |
| 2120 | | |
| 2121 | | add_infos_to_identifier(NewInfos,In,Out) :- |
| 2122 | | add_texpr_infos(In,NewInfos,Out). |
| 2123 | | |
| 2124 | | % get the ID of the variable, prime it if the infos contain "primed" |
| 2125 | | optionally_rewrite_id(Var,NewVar) :- |
| 2126 | | get_texpr_info(Var,InfosIn), |
| 2127 | | ( selectchk(primed,InfosIn,InfosOut) -> |
| 2128 | | get_texpr_id(Var,Id1), |
| 2129 | | get_texpr_type(Var,Type), |
| 2130 | | atom_concat(Id1,'\'',Id), |
| 2131 | | create_texpr(identifier(Id),Type,InfosOut,NewVar) |
| 2132 | | ; otherwise -> |
| 2133 | | Var = NewVar). |
| 2134 | | |
| 2135 | | :- use_module(translate,[translate_span/2]). |
| 2136 | | % in case of a collision, we have three options: |
| 2137 | | % - overwrite the old identifier, |
| 2138 | | % - ignore the new identifier or |
| 2139 | | % - generate an error message |
| 2140 | | handle_collision(Var,Name,Type,OldEnv,InfosOfNew,NewEnv,Ein,Eout) :- |
| 2141 | | env_lookup_infos(Name,OldEnv,InfosOfExisting), |
| 2142 | | ( collision_precedence(Name,InfosOfExisting,InfosOfNew) -> |
| 2143 | | % this identifier should be ignored |
| 2144 | | OldEnv = NewEnv, |
| 2145 | | Ein = Eout |
| 2146 | | ; collision_precedence(Name,InfosOfNew,InfosOfExisting) -> |
| 2147 | | % the existing should be overwritten |
| 2148 | | env_store(Name,Type,InfosOfNew,OldEnv,NewEnv), |
| 2149 | | Ein = Eout |
| 2150 | | ; otherwise -> |
| 2151 | | % generate error and let the environment unchanged |
| 2152 | | (Name = op(IName) -> true; Name=IName), |
| 2153 | | get_texpr_pos(Var,Pos1), |
| 2154 | | safe_get_info_pos(InfosOfExisting,Pos2), |
| 2155 | | ( double_inclusion_allowed(Pos1,Pos2,InfosOfExisting) |
| 2156 | | -> print(double_inclusion_of_id_allowed(Name,Type,Pos1,OldEnv,InfosOfExisting)),nl, |
| 2157 | | OldEnv=NewEnv, Ein=Eout |
| 2158 | | ; (better_pos(Pos2,Pos1), \+ better_pos(Pos1,Pos2) |
| 2159 | | -> Pos = Pos2 |
| 2160 | | ; Pos = Pos1), |
| 2161 | | translate_span(Pos1,PS1), translate_span(Pos2,PS2), |
| 2162 | | ajoin(['Identifier \'', IName, '\' declared twice at (Line:Col[:File]) ', PS1, ' and ', PS2],Msg), |
| 2163 | | Ein = [error(Msg,Pos)|Eout], |
| 2164 | | OldEnv = NewEnv |
| 2165 | | ) |
| 2166 | | ). |
| 2167 | | |
| 2168 | | % SEE ISSUE PROB-403 |
| 2169 | | % Correct behaviour related to multiple instantiation is specified in |
| 2170 | | % B Reference Manual (AtelierB 4.2.1), 8.3 B Project/Instantiating and renaming. |
| 2171 | | % => Constants and Sets defined in machines instantiated multiple times CAN be used in the including machine with their original (non-prefixed names). |
| 2172 | | % we do not use this code yet: this leads to the constants being added multiple times |
| 2173 | | double_inclusion_allowed(Pos1,Pos2,InfosOfExisting) :- fail, % DISABLE AT THE MOMENT; TO DO: FIX |
| 2174 | | Pos1==Pos2, |
| 2175 | | print(chk(InfosOfExisting)),nl, |
| 2176 | | member(loc(LOC,_,Section),InfosOfExisting), |
| 2177 | | section_can_be_included_multiple_times_nonprefixed(Section), |
| 2178 | | % check that we are in a context of an included machine identifier: |
| 2179 | | (inclusion_directive(LOC) |
| 2180 | | -> true |
| 2181 | | ; %LOC is probably local |
| 2182 | | member(origin([INCL/_MACHINE|_]),InfosOfExisting), inclusion_directive(INCL) |
| 2183 | | ). |
| 2184 | | |
| 2185 | | inclusion_directive(included). |
| 2186 | | inclusion_directive(used). |
| 2187 | | inclusion_directive(seen). % imports ?? |
| 2188 | | |
| 2189 | | section_can_be_included_multiple_times_nonprefixed(abstract_constants). |
| 2190 | | section_can_be_included_multiple_times_nonprefixed(concrete_constants). |
| 2191 | | section_can_be_included_multiple_times_nonprefixed(sets). |
| 2192 | | section_can_be_included_multiple_times_nonprefixed(enumerated_sets). |
| 2193 | | section_can_be_included_multiple_times_nonprefixed(enumerated_elements). |
| 2194 | | |
| 2195 | | |
| 2196 | | % decide which position info is better: prefer info in main file (highlighting) |
| 2197 | | :- use_module(bmachine,[b_get_main_filenumber/1]). |
| 2198 | | better_pos(pos(_,Filenumber,_Srow,_Scol,_Erow,_Ecol),_) :- b_get_main_filenumber(Filenumber). |
| 2199 | | better_pos(_,none). |
| 2200 | | |
| 2201 | | safe_get_info_pos(Info,Pos) :- (get_info_pos(Info,Pos) -> true ; Pos=none). |
| 2202 | | |
| 2203 | | % collision_precedence/3 decides if the first variable takes |
| 2204 | | % precedence over the second in case of a collision |
| 2205 | | % the decision is made by the additional information of both |
| 2206 | | % variables |
| 2207 | | collision_precedence(_Name,PreferredVarInfos,DroppedVarInfos) :- |
| 2208 | | % in case of a re-introduced variable from the abstraction, |
| 2209 | | % we prefer the concrete variable to the abstract one. |
| 2210 | | is_abstraction(DroppedVarInfos,PreferredVarInfos),!. |
| 2211 | | collision_precedence(_Name,PreferredVarInfos,DroppedVarInfos) :- |
| 2212 | | % We are checking an Event-B model with multi-level support |
| 2213 | | % and have the same variable in two different refinement levels. |
| 2214 | | % Then the one in the more refined module takes precedence |
| 2215 | | member(level(L1),PreferredVarInfos), |
| 2216 | | member(level(L2),DroppedVarInfos), |
| 2217 | | % Level 0 is the abstract level, level 1 the first refinement, etc. |
| 2218 | | L1 > L2,!. |
| 2219 | | collision_precedence(Name,PreferredVarInfos,DroppedVarInfos) :- |
| 2220 | | % A local definition takes precedence over a non-local identifier |
| 2221 | | % TODO: |
| 2222 | | member(loc(local,_DefMachine,definitions),PreferredVarInfos), |
| 2223 | ? | member(loc(_,_VarMachine,Section),DroppedVarInfos), |
| 2224 | | Section \= definitions,!, |
| 2225 | | (preferences:get_preference(warn_if_definition_hides_variable,true) |
| 2226 | | -> ((get_info_pos(PreferredVarInfos,Pos1), Pos1 \= none, |
| 2227 | | get_info_pos(DroppedVarInfos,Pos2), Pos2 \= none) |
| 2228 | | -> translate:translate_span(Pos1,Pos1Str), translate:translate_span(Pos2,Pos2Str), |
| 2229 | | ajoin(['Warning: DEFINITION of ', Name, ' at ', Pos1Str, |
| 2230 | | ' hides variable with same name at', Pos2Str, '.'], Msg) |
| 2231 | | ; ajoin(['Warning: DEFINITION of ', Name, ' hides variable with same name.'], Msg) |
| 2232 | | ), |
| 2233 | | add_warning(Msg) |
| 2234 | | ; true |
| 2235 | | ). |
| 2236 | | |
| 2237 | | % is_abstraction/2 tries to find out if (in case of a name clash of |
| 2238 | | % two variables) the second variable is just the re-introduced abstract |
| 2239 | | % variable in a refinement. |
| 2240 | | % InfosAbs is the list of information about the abstract variable |
| 2241 | | % InfosConc is the list of information about the concrete variable |
| 2242 | | is_abstraction(InfosAbs,InfosConc) :- |
| 2243 | | % one variable is an abstract variable, introduced in the abstraction |
| 2244 | | member(loc(abstraction,_,abstract_variables),InfosAbs), |
| 2245 | | % the other is either an abstract or concrete variable, |
| 2246 | | member(VarType,[abstract_variables,concrete_variables]), |
| 2247 | | % introduced either locally or in an included machine |
| 2248 | | member(Scope,[local,included]), |
| 2249 | | member(loc(Scope,_,VarType),InfosConc). |
| 2250 | | % and the same for constants: |
| 2251 | | is_abstraction(InfosAbs,InfosConc) :- |
| 2252 | | % one variable is an abstract variable, introduced in the abstraction |
| 2253 | | member(loc(abstraction,_,abstract_constants),InfosAbs), |
| 2254 | | % the other is either an abstract or concrete variable, |
| 2255 | | member(VarType,[abstract_constants,concrete_constants]), |
| 2256 | | % introduced either locally or in an included machine |
| 2257 | | member(Scope,[local,included]), |
| 2258 | | member(loc(Scope,_,VarType),InfosConc). |
| 2259 | | |
| 2260 | | % shortcuts for sections, to ease the use of typical combinations of |
| 2261 | | % sections |
| 2262 | | shortcut(all_parameters,[parameters,internal_parameters]). |
| 2263 | | shortcut(sets,[deferred_sets,enumerated_sets,enumerated_elements]). |
| 2264 | | shortcut(constants,[abstract_constants,concrete_constants]). |
| 2265 | | shortcut(variables,[abstract_variables,concrete_variables]). |
| 2266 | | shortcut(operations,[unpromoted,promoted]). |
| 2267 | | shortcut(identifiers,[all_parameters,sets,constants,variables,operations]). |
| 2268 | | |
| 2269 | | expand_shortcuts(Sections,Expanded) :- |
| 2270 | | foldl(expand_shortcut,Sections,Expanded,[]). |
| 2271 | | expand_shortcut(Section,Sections,RSections) :- |
| 2272 | | ( shortcut(Section,Expanded) -> |
| 2273 | | foldl(expand_shortcut,Expanded,Sections,RSections) |
| 2274 | | ; valid_section(Section) -> |
| 2275 | | Sections = [Section|RSections] |
| 2276 | | ; otherwise -> |
| 2277 | | add_internal_error('invalid section',expand_shortcut(Section,Sections,RSections)),fail). |
| 2278 | | |
| 2279 | | % find sections that can see given sections |
| 2280 | | find_relevant_sections(RSecs,MTypes,Result) :- |
| 2281 | | expand_shortcuts(RSecs,Sections), |
| 2282 | | % print(find_rel_sections_for(Sections)),nl, |
| 2283 | | findall(R, |
| 2284 | | ( member(MType,MTypes), |
| 2285 | | visibility(MType,local,R,SAccess,_), |
| 2286 | | expand_shortcuts(SAccess,Access), |
| 2287 | | member(S,Sections), |
| 2288 | | member(S,Access), |
| 2289 | | valid_section(R)), |
| 2290 | | Result1), |
| 2291 | | sort(Result1,Result). |
| 2292 | | |
| 2293 | | |
| 2294 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 2295 | | % renaming |
| 2296 | | |
| 2297 | | rename_relevant_sections(DefSecs,Renamings,Machine,New) :- |
| 2298 | | find_relevant_sections(DefSecs,[machine],Relevant), |
| 2299 | | rename_in_sections(Relevant,Renamings,Machine,New). |
| 2300 | | rename_in_sections([],_,M,M). |
| 2301 | | rename_in_sections([Section|Rest],Renamings,Old,New) :- |
| 2302 | | select_section_texprs(Section,OTExprs,NTExprs,Old,Inter), |
| 2303 | | rename_bt_l(OTExprs,Renamings,NTExprs), |
| 2304 | | rename_in_sections(Rest,Renamings,Inter,New). |
| 2305 | | |
| 2306 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 2307 | | % cleaning up machine |
| 2308 | | clean_up_machine(In,RefMachines,Out) :- |
| 2309 | | extract_parameter_types([ref(local,In)|RefMachines],NonGroundExceptions), |
| 2310 | | clean_up_machine2(NonGroundExceptions,In,Out). |
| 2311 | | clean_up_machine2(NonGroundExceptions) --> |
| 2312 | | clean_up_section(constraints,NonGroundExceptions), |
| 2313 | | clean_up_section(properties,NonGroundExceptions), |
| 2314 | | clean_up_section(invariant,NonGroundExceptions), |
| 2315 | | clean_up_section(initialisation,NonGroundExceptions), |
| 2316 | | clean_up_section(assertions,NonGroundExceptions), |
| 2317 | | clean_up_section(operation_bodies,NonGroundExceptions). |
| 2318 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 2319 | | :- if(environ(prob_safe_mode,true)). |
| 2320 | | clean_up_section(Section,NonGroundExceptions,In,Out) :- |
| 2321 | | select_section_texprs(Section,Old,New,In,Out), |
| 2322 | | %format('Cleaning up and optimizing section ~w~n',[Section]), %maplist(check_ast,Old), % this will raise errors |
| 2323 | | clean_up_l_with_optimizations(Old,NonGroundExceptions,New,Section), |
| 2324 | | %format('Checking result of clean_up section ~w~n',[Section]), |
| 2325 | | maplist(check_ast(true),New), |
| 2326 | | formatsilent('Finished checking section ~w~n',[Section]). |
| 2327 | | :- else. |
| 2328 | | clean_up_section(Section,NonGroundExceptions,In,Out) :- |
| 2329 | | % debug_stats(cleaning_up(Section)), |
| 2330 | | select_section_texprs(Section,Old,New,In,Out), |
| 2331 | | clean_up_l_with_optimizations(Old,NonGroundExceptions,New,Section). |
| 2332 | | :- endif. |
| 2333 | | |
| 2334 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 2335 | | % type expressions in context of an already type-checked machine |
| 2336 | | % TO DO: maybe do some performance optimisations for identifiers, values, ... to avoid creating scope, see evaluate_formula_typecheck2 optimisation |
| 2337 | | type_in_machine_l(Exprs,Scope,Machine,Types,TExprs,Errors) :- |
| 2338 | | MType = machine, |
| 2339 | | create_scope(Scope,MType,Machine,Env,Errors,E1), % this can be expensive for big B machines |
| 2340 | | %runtime_profiler:profile_single_call(create_scope,unknown, |
| 2341 | | % bmachine_construction:create_scope(Scope,MType,Machine,Env,Errors,E1)), |
| 2342 | | btype_ground_dl(Exprs,Env,[],Types,TExprUncleans,E1,[]), |
| 2343 | | maplist(clean_up_pred_or_expr([]),TExprUncleans,TExprs). |
| 2344 | | |
| 2345 | | % note prob_ids(visible) scope is expanded somewhere else |
| 2346 | | create_scope(Scope,MType,Machine,Env,Ein,Eout) :- |
| 2347 | | env_empty(Init), |
| 2348 | | add_theory_operators(Machine,Init,WithOperators), |
| 2349 | | foldl(create_scope2(MType,Machine),Scope,WithOperators/Ein,Env/Eout). |
| 2350 | | add_theory_operators(Machine,Ein,Eout) :- |
| 2351 | | get_section(operators,Machine,Operators), |
| 2352 | | keys_and_values(Operators,Ids,Ops), |
| 2353 | | foldl(env_store_operator,Ids,Ops,Ein,Eout). |
| 2354 | | create_scope2(MType,Machine,Scope,In/Ein,Out/Eout) :- |
| 2355 | | ( Scope = constants -> |
| 2356 | | ~~mnf( visible_env(MType,properties,[ref(local,Machine)],In,Out,Ein,Eout) ) |
| 2357 | | ; Scope = variables -> |
| 2358 | | ~~mnf( visible_env(MType,invariant,[ref(local,Machine)],In,Out,Ein,Eout) ) |
| 2359 | | ; Scope = assertions_scope -> |
| 2360 | | ~~mnf( visible_env(MType,assertions,[ref(local,Machine)],In,Out,Ein,Eout) ) |
| 2361 | | ; Scope = prepost -> |
| 2362 | | ~~mnf( visible_env(MType,prepost,[ref(local,Machine)],In,Out,Ein,Eout) ) |
| 2363 | | ; Scope = operation_bodies -> |
| 2364 | | ~~mnf( visible_env(MType,operation_bodies,[ref(local,Machine)],In,Out,Ein,Eout) ) |
| 2365 | | ; Scope = operation(Op) -> |
| 2366 | | create_operation_scope(Op,Machine,In,Out), Ein=Eout |
| 2367 | | ; Scope = env(ExplicitEnv) -> |
| 2368 | | ExplicitEnv = Out, Ein=Eout |
| 2369 | | ; Scope = identifier(Ids) -> |
| 2370 | | ~~mnf( store_variables(Ids,In,Out) ), Ein=Eout |
| 2371 | | ; otherwise -> |
| 2372 | | add_error(bmachine_construction, 'invalid scope', Scope),fail). |
| 2373 | | create_operation_scope(Op,Machine,In,Out) :- |
| 2374 | | get_section(operation_bodies,Machine,OpBodies), |
| 2375 | | get_texpr_id(OpId,op(Op)), |
| 2376 | | get_texpr_expr(TOp,operation(OpId,Results,Params,_)), |
| 2377 | | ( member(TOp,OpBodies) -> |
| 2378 | | append(Results,Params,LocalVariables), |
| 2379 | | store_variables(LocalVariables,In,Out) |
| 2380 | | ; otherwise -> |
| 2381 | | ajoin(['operation \'',Op,'\' not found for building scope'], Msg), |
| 2382 | | add_error(bmachine_construction,Msg),fail). |
| 2383 | | store_variables(Ids,In,Out) :- foldl(store_variable,Ids,In,Out). |
| 2384 | | store_variable(Id,In,Out) :- |
| 2385 | | get_texpr_id(Id,Name),get_texpr_type(Id,Type), |
| 2386 | | env_store(Name,Type,[],In,Out). |
| 2387 | | |
| 2388 | | type_open_predicate_with_quantifier(OptionalOuterQuantifier,Predicate,Scope,Machine,Result,Errors) :- |
| 2389 | | type_open_formula(Predicate,Scope,false,Machine,pred,Identifiers,TPred,Errors), |
| 2390 | | ( Identifiers = [] -> |
| 2391 | | Result = TPred |
| 2392 | | ; OptionalOuterQuantifier=forall -> |
| 2393 | | create_forall(Identifiers,TPred,Result) |
| 2394 | | ; OptionalOuterQuantifier=no_quantifier -> |
| 2395 | | Result = TPred |
| 2396 | | ; otherwise -> create_exists(Identifiers,TPred,Result) |
| 2397 | | ). |
| 2398 | | |
| 2399 | | type_open_formula(Raw,Scope,AllowOpenIdsinExpressions,Machine,Type,Identifiers,Result,Errors) :- |
| 2400 | | create_scope(Scope,machine,Machine,Env1,Errors,E1), |
| 2401 | | ( Identifiers==[] -> Mode=closed, Env1=Env |
| 2402 | | ; otherwise -> Mode=open, openenv(Env1,Env)), |
| 2403 | | btype_ground_dl([Raw],Env,[],[Type],[TExprUnclean],E1,E2), |
| 2404 | | ( Mode=closed -> true |
| 2405 | | ; otherwise -> |
| 2406 | | openenv_identifiers(Env,Identifiers), |
| 2407 | | check_ground_types_dl(Identifiers,[],E2,E3) |
| 2408 | | ), |
| 2409 | | %print(type_open_formula(Identifiers,TExprUnclean)),nl, |
| 2410 | | mark_outer_quantifier_ids(TExprUnclean,TExprUnclean2), |
| 2411 | | clean_up_pred_or_expr([],TExprUnclean2,TResult), |
| 2412 | | ( Identifiers = [] -> % no newly introduced identifiers, no problem |
| 2413 | | E3 = [] |
| 2414 | | ; Type = pred -> % newly introduced identifiers in a predicate - ok |
| 2415 | | E3 = [] |
| 2416 | | ; AllowOpenIdsinExpressions=true -> % we explicitly allow open ids in expressions |
| 2417 | | E3 = [] |
| 2418 | | ; otherwise -> % newly introduced identifiers in expression make no sense |
| 2419 | | % (is that so?) |
| 2420 | | foldl(add_unknown_identifier_error,Identifiers,E3,[]) |
| 2421 | | ), |
| 2422 | | Result = TResult. |
| 2423 | | add_unknown_identifier_error(TId,[error(Msg,Pos)|E],E) :- |
| 2424 | | get_texpr_id(TId,Id), |
| 2425 | | ajoin(['Unknown identifier ',Id,'.'],Msg), |
| 2426 | | get_texpr_pos(TId,Pos). |
| 2427 | | |
| 2428 | | % mark outermost identfiers so that they don't get optimized away |
| 2429 | | % e.g., ensure that we print the solution for something like #(y2,x2).(x2 : 0..10 & y2 : 0..10 & x2 = 10 & y2 = 10) |
| 2430 | | mark_outer_quantifier_ids(b(exists(IDS,Pred),pred,Info),Res) :- |
| 2431 | | maplist(mark_id,IDS,MIDS),!, |
| 2432 | | Res = b(exists(MIDS,Pred),pred,Info). |
| 2433 | | mark_outer_quantifier_ids(b(let_predicate(IDS,Exprs,Pred),pred,Info),Res) :- |
| 2434 | | maplist(mark_id,IDS,MIDS),!, |
| 2435 | | Res = b(let_predicate(MIDS,Exprs,Pred),pred,Info). |
| 2436 | | mark_outer_quantifier_ids(b(forall(IDS,LHS,RHS),pred,Info),Res) :- |
| 2437 | | maplist(mark_id,IDS,MIDS),!, |
| 2438 | | Res = b(forall(MIDS,LHS,RHS),pred,Info). |
| 2439 | | mark_outer_quantifier_ids(X,X). |
| 2440 | | |
| 2441 | | mark_id(b(identifier(ID),TYPE,INFO),b(identifier(ID),TYPE,[do_not_optimize_away|INFO])). |
| 2442 | | |
| 2443 | | |
| 2444 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 2445 | | % Warnings |
| 2446 | | |
| 2447 | | :- dynamic warnings/1. |
| 2448 | | clear_warnings :- |
| 2449 | | retractall( warnings(_) ). |
| 2450 | | show_warnings :- |
| 2451 | | warnings(Warning), |
| 2452 | | add_warning(bmachine_construction, Warning), |
| 2453 | | fail. |
| 2454 | | show_warnings. |
| 2455 | | |
| 2456 | | |
| 2457 | | add_warning(Warning) :- |
| 2458 | | ( warnings(Warning) -> true |
| 2459 | | ; otherwise -> assert( warnings(Warning) ) ). |