| 1 | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(bmachine_structure,[ create_machine/2 % create a new, empty machine | |
| 6 | , get_machine_name/2 % get the name of the machine | |
| 7 | , valid_section/1 % checks if the given section exists | |
| 8 | , get_section/3 % get the content of a section | |
| 9 | , write_section/4 % overwrite the content of a section | |
| 10 | , select_section/5 % modify the content of a section | |
| 11 | , get_section_of_machines/3 % get one section for multiple machines | |
| 12 | , get_section_texprs/3 % get all typed expressions of a section | |
| 13 | , select_section_texprs/5 % modify the typed expressions of a section | |
| 14 | , append_to_section/4 % append a list to a section | |
| 15 | , append_to_section_and_remove_dups/4 % append a list and remove duplicates | |
| 16 | , conjunct_to_section/4 % write the conjunction of the new and old value | |
| 17 | ]). | |
| 18 | ||
| 19 | :- use_module(tools_lists,[is_list_simple/1]). | |
| 20 | :- use_module(bsyntaxtree). | |
| 21 | ||
| 22 | :- use_module(module_information,[module_info/2]). | |
| 23 | :- module_info(group,typechecker). | |
| 24 | :- module_info(description,'Here is the data structure defined that holds a complete B machine.'). | |
| 25 | ||
| 26 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 27 | % access to machines | |
| 28 | ||
| 29 | % creates an empty machine | |
| 30 | create_machine(Name,M) :- | |
| 31 | create_texpr(truth,pred,[initial],Truth), | |
| 32 | M = machine(Name, | |
| 33 | [deferred_sets/[], enumerated_sets/[], enumerated_elements/[], | |
| 34 | parameters/[], internal_parameters/[], | |
| 35 | abstract_constants/[], concrete_constants/[], | |
| 36 | abstract_variables/[], concrete_variables/[], | |
| 37 | promoted/[], unpromoted/[], | |
| 38 | ||
| 39 | constraints/Truth, | |
| 40 | properties/Truth, | |
| 41 | invariant/Truth, | |
| 42 | linking_invariant/Truth, | |
| 43 | assertions/[], | |
| 44 | ||
| 45 | initialisation/[], | |
| 46 | operation_bodies/[], | |
| 47 | definitions/[], | |
| 48 | used/[], | |
| 49 | freetypes/[], | |
| 50 | operators/[], | |
| 51 | values/[], | |
| 52 | ||
| 53 | meta/[] | |
| 54 | ]). | |
| 55 | ||
| 56 | get_machine_name(machine(Name,_),Name). | |
| 57 | ||
| 58 | % checks if the given secion exists | |
| 59 | valid_section(Sec) :- | |
| 60 | ? | create_machine(_,machine(_,List)), member(Sec/_,List),!. |
| 61 | ||
| 62 | % get the content of a section | |
| 63 | get_section(Sec,machine(_,List),Content) :- !, | |
| 64 | memberchk(Sec/C,List),C=Content. | |
| 65 | get_section(Sec,M,C) :- | |
| 66 | add_internal_error('Illegal machine:',get_section(Sec,M,C)),fail. | |
| 67 | ||
| 68 | % overwrite the content of a section | |
| 69 | write_section(Sec,Content,Old,New) :- select_section(Sec,_,Content,Old,New). | |
| 70 | ||
| 71 | :- use_module(error_manager,[add_internal_error/2]). | |
| 72 | ||
| 73 | % modify the content of a section | |
| 74 | select_section(Sec,OldContent,NewContent,machine(Name,OldM),machine(Name,NewM)) :- | |
| 75 | select_section2(OldM,NewM,Sec,O,N),!, | |
| 76 | O=OldContent,N=NewContent. | |
| 77 | select_section(Sec,Old,_,M,NewM) :- | |
| 78 | add_internal_error('Section does not exist:',select_section(Sec,Old,_,M,NewM)), | |
| 79 | Old=[],NewM=M. | |
| 80 | select_section2([Sec/C1|R1],[Sec/C2|R2],Select,O,N) :- | |
| 81 | ( Sec==Select -> O=C1, N=C2, R1=R2 | |
| 82 | ; C1=C2, select_section2(R1,R2,Select,O,N)). | |
| 83 | ||
| 84 | % append the content to a section (section content must be a list) | |
| 85 | append_to_section(_Sec,Content,Old,New) :- Content==[],!,Old=New. | |
| 86 | append_to_section(Sec,Content,Old,New) :- | |
| 87 | select_section(Sec,Before,App,Old,New), | |
| 88 | append(Before,Content,App). | |
| 89 | ||
| 90 | % just append new elements to a section; removes duplicates | |
| 91 | append_to_section_and_remove_dups(Sec,Content,Old,New) :- | |
| 92 | select_section(Sec,Before,App2,Old,New), | |
| 93 | append(Before,Content,App), | |
| 94 | remove_dups_merge_origin(App,App2). % ideally we should just remove dups from Content, not Before | |
| 95 | ||
| 96 | :- use_module(library(avl)). | |
| 97 | :- use_module(library(lists),[select/3, subseq0/2]). | |
| 98 | % remove duplicates, apart from the origin field, which can be merged if compatible | |
| 99 | remove_dups_merge_origin([],[]). | |
| 100 | remove_dups_merge_origin([H|T],[H|Res]) :- | |
| 101 | empty_avl(E), decompose_texpr_origin(H,HT,HO), | |
| 102 | avl_store(HT,E,HO,A1), | |
| 103 | rem_dups_o(T,A1,Res). | |
| 104 | ||
| 105 | decompose_texpr_origin(b(E,T,I),b(E,T,I2),Origin) :- select(origin(Origin),I,I2),!. | |
| 106 | decompose_texpr_origin(TE,TE,[]). | |
| 107 | origin_compatible(StoredOrigin,NewOrigin) :- | |
| 108 | (subseq0(StoredOrigin,NewOrigin) -> true % the origin is included in the stored origin | |
| 109 | ; print(incompatible_origin),nl,fail). % TODO: merge | |
| 110 | ||
| 111 | rem_dups_o([],_,[]). | |
| 112 | rem_dups_o([H|T],AVL,Res) :- | |
| 113 | decompose_texpr_origin(H,HTExpr,NewOrigin), | |
| 114 | (avl_fetch(HTExpr,AVL,StoredOrigin), | |
| 115 | origin_compatible(StoredOrigin,NewOrigin) | |
| 116 | -> rem_dups_o(T,AVL,Res) | |
| 117 | ; Res=[H|TRes], | |
| 118 | avl_store(HTExpr,AVL,NewOrigin,AVL1), | |
| 119 | rem_dups_o(T,AVL1,TRes)). | |
| 120 | ||
| 121 | % --------------- | |
| 122 | ||
| 123 | % append the content to a section (section content must be a list) | |
| 124 | conjunct_to_section(Sec,Content,Old,New) :- | |
| 125 | select_section(Sec,Before,App,Old,New), | |
| 126 | conjunct_predicates([Before,Content],App). | |
| 127 | ||
| 128 | % get the content of a section | |
| 129 | % get_section_of_machines(List of Machine,Name of Section,List of Content) | |
| 130 | get_section_of_machines([],_,[]). | |
| 131 | get_section_of_machines([Machine|MRest],Section,[Content|CRest]) :- | |
| 132 | get_section(Section,Machine,Content), | |
| 133 | get_section_of_machines(MRest,Section,CRest). | |
| 134 | %get_sections([],_,[]). | |
| 135 | %get_sections([Sec|Rest],M,[Content|CRest]) :- | |
| 136 | % get_section(Sec,M,Content),get_sections(Rest,M,CRest). | |
| 137 | ||
| 138 | % get all typed expressions of a section | |
| 139 | get_section_texprs(Sec,Machine,TExprs) :- | |
| 140 | get_section(Sec,Machine,Content), | |
| 141 | ? | extract_sec_texprs(Sec,Content,TExprs). |
| 142 | extract_sec_texprs(Sec,C,C) :- has_texpr_l(Sec). | |
| 143 | extract_sec_texprs(Sec,C,[C]) :- has_texpr(Sec). | |
| 144 | extract_sec_texprs(initialisation,C,I) :- | |
| 145 | ( is_texpr(C) -> I=[C] | |
| 146 | ; is_list_simple(C) -> findall(Subst,member(init(_,Subst),C),I)). | |
| 147 | ||
| 148 | % modify the typed expressions of a section | |
| 149 | select_section_texprs(Sec,OldTExprs,NewTExprs,OldMachine,NewMachine) :- | |
| 150 | select_section(Sec,OldContent,NewContent,OldMachine,NewMachine), | |
| 151 | change_sec_texprs(Sec,OldContent,OldTExprs,NewTExprs,NewContent). | |
| 152 | change_sec_texprs(Sec,O,O,N,N) :- has_texpr_l(Sec),!. | |
| 153 | change_sec_texprs(Sec,O,[O],[N],N) :- has_texpr(Sec),!. | |
| 154 | change_sec_texprs(initialisation,O,OI,NI,N) :- | |
| 155 | ( is_list_simple(O) | |
| 156 | -> change_init(O,OI,NI,N) | |
| 157 | ; OI=[O], NI=[N]). | |
| 158 | ||
| 159 | change_init([],[],[],[]). | |
| 160 | change_init([init(Name,O)|IOrest],[O|Orest],[N|Nrest],[init(Name,N)|INrest]) :- | |
| 161 | change_init(IOrest,Orest,Nrest,INrest). | |
| 162 | ||
| 163 | ||
| 164 | has_texpr_l(Sec) :- | |
| 165 | memberchk(Sec,[deferred_sets, enumerated_sets, enumerated_elements, | |
| 166 | parameters, internal_parameters, abstract_constants, concrete_constants, | |
| 167 | abstract_variables, concrete_variables, | |
| 168 | promoted, unpromoted, assertions, | |
| 169 | operation_bodies,values]). | |
| 170 | has_texpr(Sec) :- memberchk(Sec,[constraints, properties, invariant]). |