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 :- module(pref_definitions,[b_get_preferences_from_machine/0, b_get_preferences_from_machine/1,
6 b_get_important_preferences_from_raw_machine/2,
7 b_get_set_pref_definition/3,
8 b_get_definition_string_list_from_spec/2, b_get_definition_string_from_spec/2]).
9
10 :- use_module(module_information).
11 :- module_info(group,tools).
12 :- module_info(description,'Tools for extracting information from DEFINITIONS.').
13
14 :- use_module(error_manager).
15 :- use_module(self_check).
16 :- use_module(tools,[ajoin/2, ajoin_with_sep/3]).
17 :- use_module(bmachine,[b_definition_prefixed/4,b_get_typed_definition/3]).
18 :- use_module(preferences,[temporary_set_preference/2,eclipse_preference/2,preference_val_type/2]).
19 :- use_module(btypechecker,[unify_types_werrors/5]).
20 :- use_module(bsyntaxtree).
21 :- use_module(debug,[debug_println/2]).
22 % get and set important preferences from a raw, untyped machine (as they
23 % may influence type checking,...);
24 % example: IGNORE_PRJ_TYPES, WARN_IF_DEFINITION_HIDES_VARIABLE
25 b_get_important_preferences_from_raw_machine(RawMachine,RawModelType) :-
26 ? (b_get_important_pref_type(RawModelType,Pref,PVal) ;
27 ? b_get_important_pref_mach(RawMachine,Pref,PVal)),
28 %print(pref(Pref,PType,PVal)),nl,
29 (temporary_set_preference(Pref,PVal)
30 -> debug_println(9,set_important_pref(PREFString,Pref,PVal))
31 ; add_error(pref_definitions,'Could not set DEFINITION preference to specified value: ',(PREFString:PVal))
32 ),
33 fail.
34 b_get_important_preferences_from_raw_machine(_,_).
35
36 b_get_important_pref_mach(RawMachine,Pref,PVal) :-
37 ? member(definitions(_Pos,Defs),RawMachine),
38 ? member(expression_definition(_DPOS,DefName,[],RawVALUE),Defs),
39 ? atom_concat('SET_PREF_',PREFString,DefName),
40 ? eclipse_preference(PREFString,Pref),
41 ? preference_val_type(Pref,PType),
42 ? (PType=bool ; PType=xbool), % at the moment only boolean preferences supported
43 convert_raw_pref_val(PType,RawVALUE,PVal).
44
45 b_get_important_pref_type(system(Pos),Pref,PVal) :-
46 % SET_PREF_ALLOW_NEW_OPERATIONS_IN_REFINEMENT == TRUE; for Event-B Atelier-B style; alternatively we could set animation_minor_mode ?
47 add_message(pref_definitions,'Detected Event-B model; setting ALLOW_NEW_OPERATIONS_IN_REFINEMENT to ','TRUE',Pos),
48 Pref=allow_new_ops_in_refinement, PVal=true.
49
50
51 convert_raw_pref_val(bool,boolean_true(_),true).
52 convert_raw_pref_val(bool,boolean_false(_),false).
53 %convert_raw_pref_val(int,integer(_,V),V).
54 %convert_raw_pref_val(nat,integer(_,V),V). % range checking done in temporary_set_preference
55 %convert_raw_pref_val(nat1,integer(_,V),V).
56 %convert_raw_pref_val(neg,integer(_,V),V).
57 %convert_raw_pref_val(range(_,_),integer(_,V),V).
58 %convert_raw_pref_val(string(_),string(_,S),S).
59
60 :- use_module(translate,[translate_bexpression/2]).
61 b_get_preferences_from_machine(List) :-
62 findall(set_pref(String,ValS),(get_def_aux(String,TExpr),translate_bexpression(TExpr,ValS)),List).
63 % now a version that does not need to obtain a list with all preferences set:
64 b_get_preferences_from_machine :- get_def_aux(_,_),fail.
65 b_get_preferences_from_machine.
66
67 get_def_aux(String,TExpr) :-
68 ? b_definition_prefixed(_,'SET_PREF_',String,DefName),
69 ? b_get_set_pref_definition(DefName,String,TExpr),
70 set_pref_from_machine(String,TExpr).
71
72 b_get_set_pref_definition(DefName,String,TExpr) :-
73 ? b_definition_prefixed(_,'SET_PREF_',String,DefName),
74 ? b_get_typed_definition(DefName,[],TExpr).
75
76
77 set_pref_from_machine(String,TExpr) :-
78 ? (eclipse_preference(String,Pref) -> true
79 ; preference_val_type(String,_), Pref=String % user uses directly internal Prolog Name
80 ),
81 !,
82 preference_val_type(Pref,PType),
83 convert_pref_val(PType,TExpr,PVal),
84 (temporary_set_preference(Pref,PVal)
85 -> true
86 ; add_error(pref_definitions,'Could not set DEFINITION preference: ',(String:PVal))
87 ).
88 set_pref_from_machine(String,_TExpr) :-
89 add_error(pref_definitions,'Error in SET_PREF DEFINITION. Preference does not exist: ',String),fail.
90
91 convert_pref_val(int,TExpr,Val) :- !,
92 check_type(integer,TExpr),
93 compute_expr(TExpr,int(Val)).
94 convert_pref_val(nat,TExpr,Val) :- !,
95 convert_pref_val(int,TExpr,Val),
96 ( (ground(Val),Val >= 0) -> true
97 ; otherwise -> error(TExpr,'Value must be a natural (>= 0)')).
98 convert_pref_val(neg,TExpr,Val) :- !,
99 convert_pref_val(int,TExpr,Val),
100 ( (ground(Val),Val =< 0) -> true
101 ; otherwise -> error(TExpr,'Value must be non-positive (<= 0)')).
102 convert_pref_val(nat1,TExpr,Val) :- !,
103 convert_pref_val(int,TExpr,Val),
104 ( (ground(Val),Val >= 1) -> true
105 ; otherwise -> error(TExpr,'Value must be a natural >= 1')).
106 convert_pref_val(range(Low,Up),TExpr,Val) :-!,
107 convert_pref_val(int,TExpr,Val),
108 ( ground(Val),Val >= Low, Val =< Up -> true
109 ; otherwise -> ajoin(['Value must be in the interval [',Low,',',Up,']'],Msg),
110 error(TExpr,Msg)).
111 convert_pref_val(bool,TExpr,Val) :- !,
112 check_type(boolean, TExpr),
113 compute_expr(TExpr,BVal),
114 ( BVal = pred_true /* bool_true */ -> Val = true
115 ; BVal = pred_false /* bool_false */ -> Val = false
116 ; otherwise -> add_error(pref_definitions,'Unexpected result (neither true nor false)',BVal)).
117 convert_pref_val(xbool,TExpr,Val) :- !, % extended boolean
118 (get_texpr_type(TExpr,boolean) -> true ; check_type(string,TExpr)),
119 compute_expr(TExpr,BVal),
120 ( BVal = pred_true /* bool_true */ -> Val = true
121 ; BVal = pred_false /* bool_false */ -> Val = false
122 ; BVal=string(Val),member(Val,[false,true,full]) -> true
123 ; otherwise -> add_error(pref_definitions,'Unexpected result (neither true, false nor full)',BVal)).
124 convert_pref_val(string,TExpr,Val) :- !,
125 check_type(string, TExpr),
126 get_texpr_expr(TExpr,string(Val)).
127 convert_pref_val(path,TExpr,Val) :- !,
128 check_type(string, TExpr),
129 get_texpr_expr(TExpr,string(Val)).
130 convert_pref_val([H|T],TExpr,Val) :- !,
131 check_type(string, TExpr),
132 get_texpr_expr(TExpr,string(Val)),
133 (member(Val,[H|T]) -> true
134 ; ajoin_with_sep(['Value must be one of:',H|T],' ',Msg),
135 error(TExpr,Msg)).
136 convert_pref_val(PrefType,_,_) :-
137 add_error(pref_definitions,'Unsupported preference type in definitions:',PrefType),fail.
138
139 :- use_module(b_interpreter,[b_compute_expression_nowf/4]).
140 compute_expr(TExpr,Res) :-
141 if( b_compute_expression_nowf(TExpr,[],[],R) , Res=R ,
142 add_error_fail(pref_definitions,'Computing expression failed: ',TExpr)).
143 error(TExpr,Msg) :-
144 get_texpr_pos(TExpr,Pos),
145 add_all_perrors([error(Msg,Pos)]),
146 fail.
147
148 check_type(Type,TExpr) :-
149 get_texpr_type(TExpr,EType),
150 get_texpr_pos(TExpr,Pos),
151 unify_types_werrors(Type,EType,Pos,Errors,[]),
152 ( Errors = [] -> true
153 ; otherwise -> add_all_perrors(Errors),fail).
154
155 % -------------------
156
157
158 :- use_module(tools,[safe_atom_codes/2, string_concatenate/3]).
159 :- use_module(bmachine,[b_definition_prefixed/4,b_get_definition_string_from_machine/2]).
160 :- use_module(specfile,[animation_mode/1]).
161 :- use_module(xtl_interface,[xtl_get_definition_string/2]).
162
163 /* for tcltk: */
164 b_get_definition_string_list_from_spec(Def_Name_Prefix,Result) :-
165 atom_codes(Def_Name_Prefix,Codes), append(Codes,_,CodesPrefix),
166 findall(S, (b_get_definition_string_from_spec(Def_Name,DS),
167 safe_atom_codes(Def_Name,CodesPrefix), /* check that name begins with the same characters as Def_Name_Prefix */
168 string_concatenate(DS,';',S)), Result).
169
170 b_get_definition_string_from_spec(Def_Name,DS) :- animation_mode(xtl),!,
171 xtl_get_definition_string(Def_Name,DS).
172 b_get_definition_string_from_spec(Def_Name,DS) :-
173 b_get_definition_string_from_machine(Def_Name,DS).
174