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(units_prettyprint, [units_pp_trans/2,
6 units_pp_prop/2,
7 units_pp_value/2,
8 pp/3,
9 pp_fixpoint_result/3
10 ]).
11
12 :- use_module(library(codesio)).
13 :- use_module(library(lists)).
14 :- use_module(library(avl)).
15
16 :- use_module(probsrc(tools)).
17 :- use_module(probsrc(error_manager)).
18
19 :- use_module(units_alias).
20 :- use_module(units_tools).
21 :- use_module(units).
22 :- use_module(units_interpreter).
23
24 :- use_module(probsrc(module_information)).
25 :- module_info(group,plugin_units).
26 :- module_info(description,'Units Plugin: Prettyprinter for properties and transitions').
27
28 units_pp_trans(Transition,Pretty) :-
29 %write(units_pp_trans(Transition,Pretty)),
30 pp(classic,Transition,PrettyTerm),
31 write_to_codes(PrettyTerm,Pretty).
32
33 units_pp_prop(Property,Pretty) :-
34 pp(classic,Property,PrettyTerm),
35 write_to_codes(PrettyTerm,Pretty).
36
37 units_pp_value(Value,Pretty) :-
38 pp(classic,Value,PrettyTerm),
39 write_to_codes(PrettyTerm,Pretty).
40
41
42 pp(_ClassicOrEventB,X,unknown) :- var(X), !.
43 pp(ClassicOrEventB,integer(X),Y) :- !, pp(ClassicOrEventB,X,Y).
44 pp(ClassicOrEventB,int(X),Y) :- !, pp(ClassicOrEventB,X,Y).
45 pp(ClassicOrEventB,boolean(X),Y) :- !, pp(ClassicOrEventB,X,Y).
46 pp(ClassicOrEventB,string(X),Y) :- !, pp(ClassicOrEventB,X,Y).
47 pp(ClassicOrEventB,global_set(X),Y) :- !, pp(ClassicOrEventB,X,Y).
48 pp(ClassicOrEventB,set(X),Y) :- !, pp(ClassicOrEventB,X,Y).
49 pp(ClassicOrEventB,couple(X,Y),Pretty) :- !,
50 pp(ClassicOrEventB,X,PPX), pp(ClassicOrEventB,Y,PPY),
51 ajoin([PPX, ' -> ', PPY],Pretty).
52 pp(ClassicOrEventB,global(X,_Y),Pretty) :- !,
53 pp(ClassicOrEventB,X,Pretty).
54 % in the tcltk interface, the error is shown in a different way
55 % thus, we do not need to include it in the prettyprint
56 pp(classic,X,error) :- X=top(_), !.
57 % in rodin, we show an error listing all infered units
58 pp(eventb,X,PPOut) :-
59 X=top(List), !,
60 maplist(pp_unit(eventb),List,PPList),
61 ajoin([multiple, '(', PPList, ')'], PPOut).
62 % avl_sets from inside a value term
63 pp(ClassicOrEventB,avl_set(A),PPOut) :- !,
64 avl_domain(A,Dom), maplist(pp(ClassicOrEventB),Dom,PPDom),
65 ajoin_with_sep(PPDom,',',JoinedDom),
66 ajoin(['{',JoinedDom,'}'],PPOut).
67 pp(_ClassicOrEventB,'$setup_constants','SETUP_CONSTANTS') :- !.
68 pp(_ClassicOrEventB,'$initialise_machine','INITIALISATION') :- !.
69 pp(_ClassicOrEventB,X,X) :- atom(X), !.
70 pp(_ClassicOrEventB,X,X) :- number(X), !.
71 pp(ClassicOrEventB,'-->'(Operation,ResultValues),PrettyTransition) :- !,
72 pp(ClassicOrEventB,Operation,PrettyOperation),
73 pp(ClassicOrEventB,ResultValues,PrettyResults),
74 ajoin([PrettyOperation, '-->', PrettyResults],PrettyTransition).
75 pp(ClassicOrEventB,L,Result) :-
76 is_unit_list(L),
77 pp_unit(ClassicOrEventB,L,Result),!.
78 pp(_ClassicOrEventB,[],[]) :- !.
79 pp(ClassicOrEventB,[H|T],[PH|PT]) :- !,
80 pp(ClassicOrEventB,H,PH),
81 pp(ClassicOrEventB,T,PT).
82 pp(ClassicOrEventB,Compound,Pretty) :-
83 Compound =.. [Head|Args], !,
84 pp(ClassicOrEventB,Head,PrettyHead),
85 pp(ClassicOrEventB,Args,PrettyArgs),
86 Pretty =.. [PrettyHead|PrettyArgs].
87 pp(_ClassicOrEventB,Term,_Pretty) :-
88 !, add_error_fail(units_prettyprint, 'Term not implemented: ', [Term]).
89
90 pp_unit(ClassicOrEventB,L,Result) :-
91 subseq(L,Com,Sub),
92 unit_alias(Aliased,Sub), !,
93 (Com = []
94 -> Result = Aliased
95 ; pp_unit(ClassicOrEventB,Com,ComPP),
96 ajoin_with_sep([Aliased,ComPP],' * ',Result)).
97 pp_unit(ClassicOrEventB,[[EtoT,Symbol,EtoS]|T],Result) :-
98 exponentiation_operator(ClassicOrEventB,Exponentiation),
99 (EtoT = 0
100 -> EtoTPP = ''
101 ; (EtoT = 1 -> EtoTPP = '10*' ; ajoin([10,Exponentiation,EtoT,'*'],EtoTPP))),
102 (EtoS = 1 -> EtoSPP = Symbol ; ajoin([Symbol,Exponentiation,EtoS],EtoSPP)),
103 ajoin([EtoTPP,EtoSPP],FirstUnitPP),
104 (T = []
105 -> Result = FirstUnitPP
106 ; pp_unit(ClassicOrEventB,T,TPP),
107 ajoin_with_sep([FirstUnitPP,TPP],' * ',Result)).
108
109 exponentiation_operator(classic,'**').
110 exponentiation_operator(eventb,'^').
111
112
113 % predicates below should only be called from tcltk
114 pp_fixpoint_result(FixPointState,UnboundInConstraint,PP) :-
115 pp_state(FixPointState,PPFixPointState),
116 evaluate_fixpoint(FixPointState,UnboundInConstraint,Part2),
117 units:iterations(Iterations),
118 evaluate_operation(OperationsResult),
119 ajoin(['Fixpoint reached after ', Iterations,' Iterations\n\nState:\n',PPFixPointState,'\n\n',Part2,'\n',OperationsResult],PP).
120
121 pp_state([],'').
122 pp_state([bind(Key,Val)|T],Res) :-
123 pp_state(T,PPT),
124 pp(classic,Val,PPVal),
125 ajoin([Key, ' = ', PPVal, '\n', PPT],Res).
126
127 evaluate_operation(OperationsResult) :-
128 findall(Name, units_interpreter:top_in_parameters(Name), ListOfNames1),
129 findall(Name, units_interpreter:top_in_results(Name), ListOfNames2),
130 (ListOfNames1 = []
131 -> OperationsResult1 = ''
132 ; ajoin(['Multiple units inferred for parameters of: ', ListOfNames1, '\n\n'], OperationsResult1)
133 ),
134 (ListOfNames2 = []
135 -> OperationsResult = OperationsResult1
136 ; ajoin([OperationsResult1,'Multiple units inferred for results of: ', ListOfNames2], OperationsResult)
137 ).
138
139 evaluate_fixpoint([],_Unbound,'').
140 evaluate_fixpoint([bind(Id,Val)|State],Unbound,AtomOut) :-
141 \+(ground(Val)), member(Id,Unbound), !,
142 ajoin(['No unit inferred for Variable / Constant, but used in constraint: ',Id,'\n'],Out1),
143 evaluate_fixpoint(State,Unbound,SubOut),
144 ajoin([Out1,SubOut],AtomOut).
145 evaluate_fixpoint([bind(Id,Val)|State],Unbound,AtomOut) :-
146 \+(ground(Val)), !,
147 ajoin(['No unit inferred for Variable / Constant: ',Id,'\n'],Out1),
148 evaluate_fixpoint(State,Unbound,SubOut),
149 ajoin([Out1,SubOut],AtomOut).
150 evaluate_fixpoint([bind(Id,Val)|State],Unbound,AtomOut) :-
151 contains_top(Val), !,
152 ajoin(['Multiple units inferred for Variable / Constant: ',Id,'\n'],Out1),
153 evaluate_fixpoint(State,Unbound,SubOut),
154 ajoin([Out1,SubOut],AtomOut).
155 evaluate_fixpoint([bind(_Id,_Val)|State],Unbound,SubOut) :-
156 evaluate_fixpoint(State,Unbound,SubOut).