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]). |