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