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 |