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