1 | % (c) 2009-2013 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 | , conjunct_to_section/4 % write the conjunction of the new and old value | |
16 | ]). | |
17 | ||
18 | :- use_module(tools,[is_list_simple/1]). | |
19 | :- use_module(bsyntaxtree). | |
20 | ||
21 | :- use_module(module_information,[module_info/2]). | |
22 | :- module_info(group,typechecker). | |
23 | :- module_info(description,'Here is the data structure defined that holds a complete B machine.'). | |
24 | ||
25 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
26 | % access to machines | |
27 | ||
28 | % creates an empty machine | |
29 | create_machine(Name,M) :- | |
30 | create_texpr(truth,pred,[initial],Truth), | |
31 | M = machine(Name, | |
32 | [deferred_sets/[], enumerated_sets/[], enumerated_elements/[], | |
33 | parameters/[], internal_parameters/[], | |
34 | abstract_constants/[], concrete_constants/[], | |
35 | abstract_variables/[], concrete_variables/[], | |
36 | promoted/[], unpromoted/[], | |
37 | ||
38 | constraints/Truth, | |
39 | properties/Truth, | |
40 | invariant/Truth, | |
41 | linking_invariant/Truth, | |
42 | assertions/[], | |
43 | ||
44 | initialisation/[], | |
45 | operation_bodies/[], | |
46 | definitions/[], | |
47 | used/[], | |
48 | freetypes/[], | |
49 | operators/[], | |
50 | values/[], | |
51 | ||
52 | meta/[] | |
53 | ]). | |
54 | ||
55 | get_machine_name(machine(Name,_),Name). | |
56 | ||
57 | % checks if the given secion exists | |
58 | valid_section(Sec) :- | |
59 | ? | create_machine(_,machine(_,List)), member(Sec/_,List),!. |
60 | ||
61 | % get the content of a section | |
62 | get_section(Sec,machine(_,List),Content) :- | |
63 | memberchk(Sec/C,List),C=Content. | |
64 | ||
65 | % overwrite the content of a section | |
66 | write_section(Sec,Content,Old,New) :- select_section(Sec,_,Content,Old,New). | |
67 | ||
68 | % modify the content of a section | |
69 | select_section(Sec,OldContent,NewContent,machine(Name,OldM),machine(Name,NewM)) :- | |
70 | select_section2(OldM,NewM,Sec,O,N),!, | |
71 | O=OldContent,N=NewContent. | |
72 | select_section2([Sec/C1|R1],[Sec/C2|R2],Select,O,N) :- | |
73 | ( Sec==Select -> O=C1, N=C2, R1=R2 | |
74 | ; otherwise -> C1=C2, select_section2(R1,R2,Select,O,N)). | |
75 | ||
76 | % append the content to a section (section content must be a list) | |
77 | append_to_section(Sec,Content,Old,New) :- | |
78 | select_section(Sec,Before,App,Old,New), | |
79 | append(Before,Content,App). | |
80 | ||
81 | % append the content to a section (section content must be a list) | |
82 | conjunct_to_section(Sec,Content,Old,New) :- | |
83 | select_section(Sec,Before,App,Old,New), | |
84 | conjunct_predicates([Before,Content],App). | |
85 | ||
86 | % get the content of a section | |
87 | % get_section_of_machines(List of Machine,Name of Section,List of Content) | |
88 | get_section_of_machines([],_,[]). | |
89 | get_section_of_machines([Machine|MRest],Section,[Content|CRest]) :- | |
90 | get_section(Section,Machine,Content), | |
91 | get_section_of_machines(MRest,Section,CRest). | |
92 | %get_sections([],_,[]). | |
93 | %get_sections([Sec|Rest],M,[Content|CRest]) :- | |
94 | % get_section(Sec,M,Content),get_sections(Rest,M,CRest). | |
95 | ||
96 | % get all typed expressions of a section | |
97 | get_section_texprs(Sec,Machine,TExprs) :- | |
98 | ? | get_section(Sec,Machine,Content), |
99 | ? | extract_sec_texprs(Sec,Content,TExprs). |
100 | extract_sec_texprs(Sec,C,C) :- has_texpr_l(Sec). | |
101 | extract_sec_texprs(Sec,C,[C]) :- has_texpr(Sec). | |
102 | extract_sec_texprs(initialisation,C,I) :- | |
103 | ( is_texpr(C) -> I=[C] | |
104 | ; is_list_simple(C) -> findall(Subst,member(init(_,Subst),C),I)). | |
105 | ||
106 | % modify the typed expressions of a section | |
107 | select_section_texprs(Sec,OldTExprs,NewTExprs,OldMachine,NewMachine) :- | |
108 | select_section(Sec,OldContent,NewContent,OldMachine,NewMachine), | |
109 | change_sec_texprs(Sec,OldContent,OldTExprs,NewTExprs,NewContent). | |
110 | change_sec_texprs(Sec,O,O,N,N) :- has_texpr_l(Sec),!. | |
111 | change_sec_texprs(Sec,O,[O],[N],N) :- has_texpr(Sec),!. | |
112 | change_sec_texprs(initialisation,O,OI,NI,N) :- | |
113 | ( is_list_simple(O) -> change_init(O,OI,NI,N) | |
114 | ; otherwise -> OI=[O], NI=[N]). | |
115 | change_init([],[],[],[]). | |
116 | change_init([init(Name,O)|IOrest],[O|Orest],[N|Nrest],[init(Name,N)|INrest]) :- | |
117 | change_init(IOrest,Orest,Nrest,INrest). | |
118 | ||
119 | ||
120 | has_texpr_l(Sec) :- | |
121 | memberchk(Sec,[deferred_sets, enumerated_sets, enumerated_elements, | |
122 | parameters, internal_parameters, abstract_constants, concrete_constants, | |
123 | abstract_variables, concrete_variables, | |
124 | promoted, unpromoted, assertions, | |
125 | operation_bodies,values]). | |
126 | has_texpr(Sec) :- memberchk(Sec,[constraints, properties, invariant]). |