1		% (c) 2009-2019 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		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6		% Pragma handling
7
8		:- module(pragmas, [ global_pragma/2
9		, apply_pragmas_to_event_b_machine/3
10		, extract_pragmas_from_event_b_extensions/2
11		]).
12
13		:- use_module(module_information,[module_info/2]).
14		:- module_info(group,typechecker).
15		:- module_info(description,'This module handles pragmas loaded with a b machine').
16
17		:- use_module(library(lists)).
18
19		:- use_module(bmachine_structure).
20
21		:- dynamic global_pragma/2.
22
23		:- use_module(probsrc(eventhandling),[register_event_listener/3]).
24
25		% TO DO: remove or ensure it is called
26		init :-
27		register_event_listener(start_initialising_specification,retractall(global_pragma(_,_)),'clean stored pragmas').
28		init.
29
30		% pragma rules: pragma(Pragma, Expr, Type, Info)
31		%pragma_rule(X,E,T,I) :- print(pragma_rule(X,E,T,I)),nl,fail.
32		pragma_rule(label,IdList, _, _, label(IdList)) :- IdList = [_|_].
33		pragma_rule(unit,Unit, _, _, unit(Unit)).
34		pragma_rule(inferred_unit,Unit, _, _, inferred_unit(Unit)).
35		pragma_rule(inferredunit,Unit, _, _, inferred_unit(Unit)).
36		pragma_rule(conversion,[], _, _, conversion).
37		pragma_rule(symbolic,[],_,_,prob_annotation('SYMBOLIC')).
38
39		% pragma which apply to the entire file; they do not need a location
40		%global_pragma(generated).
41		%global_pragma(unit_alias).
42
43		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
44		% Event-B
45		extract_pragmas_from_event_b_extensions(Ext,Pragmas) :-
46		findall(P,
47		(member(P,Ext), P=pragma(_T,_S,_A,_C)),
48		Pragmas).
49
50		% currently possible pragmas:
51		% - attach a unit to a variable
52		% - attach a unit to a constant
53		% - mark a concrete constant as abstract/symbolic -> this moves the constant!
54		apply_pragmas_to_event_b_machine(Pragmas,Machine,ResultingMachine) :-
55		get_section(abstract_constants,Machine,AbsConstants),
56		maplist(apply_event_b_pragmas(Pragmas),AbsConstants,NewAbsConstants),
57		get_section(concrete_constants,Machine,ConcConstants),
58		maplist(apply_event_b_pragmas(Pragmas),ConcConstants,NewConcConstants),
59		get_section(abstract_variables,Machine,AbsVars),
60		maplist(apply_event_b_pragmas(Pragmas),AbsVars,NewAbsVars),
61		get_section(concrete_variables,Machine,ConcVars),
62		maplist(apply_event_b_pragmas(Pragmas),ConcVars,NewConcVars),
63		write_section(abstract_constants,NewAbsConstants,Machine,TmpMachine1),
64		write_section(concrete_constants,NewConcConstants,TmpMachine1,TmpMachine2),
65		write_section(abstract_variables,NewAbsVars,TmpMachine2,TmpMachine3),
66		write_section(concrete_variables,NewConcVars,TmpMachine3,ResultingMachine).
67
68		apply_event_b_pragmas(Pragmas,b(identifier(Name),Type,Infos),b(identifier(Name),Type,Infos2)) :-
69		member(pragma(PragmaType,_Machine,Name,Content),Pragmas)
70		-> pragma_rule(PragmaType,Content,b(identifier(Name),Type,Infos),Type,AdditionalArgument),
71		Infos2 = [AdditionalArgument|Infos]
72		; Infos2 = Infos.