1 % (c) 2009-2017 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_tools, [contains_top/1,
6 check_state_add_error/2,
7 insert_spacer_and_join/2,
8 is_unit_list/1,
9 append_to_tcltk_replay_sequence/1,
10 reset_tcltk_replay_sequence/0,
11 replay_tcltk_sequence/0,
12 state_was_updated/2,
13 extract_value_list/2
14 ]).
15
16 :- use_module(library(lists)).
17
18 %:- use_module(library(tcltk)). % will be included automatically by prob_tcltk.pl; we do not want probcli to depend on Tcl/Tk
19
20 :- use_module(probsrc(tools)).
21 :- use_module(probsrc(self_check)).
22 :- use_module(probsrc(state_space)).
23 %:- use_module(probsrc(coverage_tools_annotations),['$NOT_COVERED'/1]).
24
25 :- use_module(probsrc(module_information)).
26 :- module_info(group,plugin_units).
27 :- module_info(description,'Units Plugin: Analysis tools used in several places.').
28
29
30 :- use_module(units).
31
32 :- dynamic tcltk_replay_sequence/1.
33
34 % TO DO: remove this callback to Tcl/Tk
35 %:- use_module(library(tcltk),[tcl_eval/3]).
36 to_tcltk(Command) :-
37 on_exception(_E, (user:cur_tcl_process(Tcl), tcltk:tcl_eval(Tcl, Command, _)), true).
38
39 append_to_tcltk_replay_sequence(X) :-
40 retract(tcltk_replay_sequence(S1)),
41 assert(tcltk_replay_sequence([X|S1])).
42
43 reset_tcltk_replay_sequence :-
44 retractall(tcltk_replay_sequence(_)),
45 assert(tcltk_replay_sequence([])).
46
47 replay_tcltk_sequence :-
48 ? to_tcltk('procInsertHistoryOptionsState'),
49 ? retract(tcltk_replay_sequence(Seq)),
50 ? reverse(Seq,Seq2),
51 ? replay_tcltk_sequence(Seq2).
52 replay_tcltk_sequence([]).
53 % in tcltk mode
54 %replay_tcltk_sequence([Op|T]) :-
55 % state_space:current_options(Options),
56 % nth0(N,Options,(_,_,Op,_)),
57 % ajoin(['procPerformOptionByIOption', ' ', N],Command),
58 % to_tcltk(Command), !,
59 % replay_tcltk_sequence(T),
60 % '$NOT_COVERED'('GUI code not used in automatic tests').
61 % in cli mode
62 replay_tcltk_sequence([Op|T]) :-
63 ? current_state_id(CurID),
64 ? visited_expression(CurID,CurState),
65 ? user:compute_all_transitions(CurID,CurState),
66 ? user:tcltk_perform_action(Op,_NewID),
67 ? replay_tcltk_sequence(T).
68 insert_spacer_and_join(List,Output) :-
69 atomic(List) -> Output=List ; ajoin_with_sep(List,' ',Output).
70
71 :- assert_must_succeed(contains_top(type(top([])))).
72 :- assert_must_succeed(contains_top(type(top([_])))).
73 :- assert_must_succeed(contains_top(type(type2(top([]),_)))).
74 :- assert_must_succeed(contains_top(type(type2(top([_]),_)))).
75 :- assert_must_fail(contains_top(type(_))).
76 contains_top(X) :- var(X), !, fail.
77 contains_top(X) :- X=top(_).
78 contains_top([H|T]) :-
79 ? !, (contains_top(H) ; contains_top(T)).
80 contains_top(Pred) :-
81 ? !, Pred =.. [Head|Tail],
82 ? Tail = [_|_],
83 ? (contains_top(Head) ; contains_top(Tail)).
84
85 check_state_add_error(ID, concrete_constants(State)) :-
86 !, check_state_add_error(ID,State).
87 check_state_add_error(_ID,[]).
88 check_state_add_error(ID,[bind(Var,Type)|T]) :-
89 ? contains_top(Type), !,
90 ajoin(['Multiple Units inferred for variable ', Var, '. This is a type error.'], ErrTerm),
91 units:units_error_context(Context),
92 store_state_error(ID,abort_error('Multiple Units inferred',
93 'State contains Error',ErrTerm,Context),_),
94 check_state_add_error(ID,T).
95 check_state_add_error(ID,[bind(Var,Type)|T]) :-
96 \+(ground(Type)), units:static_result(_,ListOfVars),
97 member(Var,ListOfVars), !,
98 ajoin(['Variable ', Var, ' is involved in constraint but still unset'], ErrTerm),
99 units:units_error_context(Context),
100 store_state_error(ID,abort_error('Constraint variable unset',
101 'Unsolved Constraint',ErrTerm,Context),_),
102 check_state_add_error(ID,T).
103 check_state_add_error(ID, [_H|T]) :-
104 check_state_add_error(ID,T).
105
106 is_unit_list(X) :- var(X), !, fail.
107 is_unit_list([X]) :- var(X), !, fail.
108 is_unit_list([]).
109 is_unit_list([[_,_,_]|T]) :-
110 is_unit_list(T).
111
112 :- assert_must_succeed(state_was_updated([bind(a,_A)],[bind(a,a)])).
113 :- assert_must_fail(state_was_updated([bind(a,_A)],[bind(a,_B)])).
114 :- assert_must_fail(state_was_updated([bind(a,top([]))],[bind(a,top([]))])).
115 :- assert_must_fail(state_was_updated([bind(a,top([]))],[bind(a,top([[[0,s,1]]]))])).
116 :- assert_must_fail(state_was_updated([bind(a,top([]))],[bind(a,top([[[0,s,1]],[[0,m,1]]]))])).
117 :- assert_must_succeed(state_was_updated([bind(a,top([])),bind(b,1)],[bind(a,top([[[0,s,1]]])),bind(b,2)])).
118 :- assert_must_succeed(state_was_updated([bind(a,A),bind(b,_B)],[bind(a,A),bind(b,b)])).
119 :- assert_must_succeed(state_was_updated([bind(a,A),bind(b,integer(_B))],[bind(a,A),bind(b,integer([[0,m,1],[0,s,-1]]))])).
120 :- assert_must_succeed(state_was_updated([bind(a,5),bind(b,integer(_B))],[bind(a,5),bind(b,integer([[0,m,1],[0,s,-1]]))])).
121 :- assert_must_succeed(state_was_updated([bind(a,integer(_A))],[bind(a,integer([[0,m,1],[0,s,-1]]))])).
122 :- assert_must_succeed(state_was_updated([bind(v,integer([[0,s,1]])),bind(w,integer(_)),bind(x,integer([[0,m,1]])),bind(y,integer([[0,m,-1]]))],
123 [bind(v,integer(top([]))),bind(w,integer(_)),bind(x,integer([[0,m,1]])),bind(y,integer([[0,m,-1]]))])).
124 state_was_updated([bind(ID,Val)|T1],[bind(ID,Val2)|T2]) :-
125 ? (\+ground(Val)), (\+ground(Val2)),
126 ? !, state_was_updated(T1,T2).
127 state_was_updated([bind(ID,Val)|_T1],[bind(ID,Val2)|_T2]) :-
128 (\+ground(Val)), ground(Val2).
129 state_was_updated([bind(ID,Val)|T1],[bind(ID,Val2)|T2]) :-
130 ? Val == Val2,
131 ? !, state_was_updated(T1,T2).
132 state_was_updated([bind(ID,Val)|T1],[bind(ID,Val2)|T2]) :-
133 ? contains_top(Val), contains_top(Val2), !,
134 state_was_updated(T1,T2).
135 state_was_updated([bind(ID,Val)|_T1],[bind(ID,Val2)|_T2]) :-
136 Val \== Val2.
137
138 extract_value_list([],[]).
139 extract_value_list([bind(_,X)|T],[X|ET]) :- extract_value_list(T,ET).