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(typing_tools,[ | |
6 | is_infinite_type/1, % check if a type is infinite | |
7 | valid_ground_type/1, % check if a type is a valid ground type | |
8 | contains_infinite_type/1, | |
9 | any_value_for_type/2, | |
10 | normalize_type/2 | |
11 | ]). | |
12 | ||
13 | %:- use_module(bsyntaxtree, [get_texpr_types/2, syntaxtraversion/6, find_typed_identifier_uses/3]). | |
14 | :- use_module(library(lists), [maplist/3]). | |
15 | ||
16 | % check if a type is infinite for ProB animation; deferred sets are not counted as infinite here! | |
17 | is_infinite_type(integer). | |
18 | is_infinite_type(string). | |
19 | is_infinite_type(freetype(_)). | |
20 | is_infinite_type(set(X)) :- is_infinite_type(X). | |
21 | is_infinite_type(seq(_)). | |
22 | is_infinite_type(couple(X,Y)) :- (is_infinite_type(X) -> true ; is_infinite_type(Y)). | |
23 | is_infinite_type(record(Fields)) :- | |
24 | ((member(field(_,Type),Fields), is_infinite_type(Type)) -> true). | |
25 | ||
26 | contains_infinite_type([H|T]) :- | |
27 | (is_infinite_type(H) -> true ; contains_infinite_type(T)). | |
28 | ||
29 | :- use_module(error_manager). | |
30 | ||
31 | valid_ground_type(X) :- var(X),!, add_error(valid_ground_type,'Variable as type: ',X),fail. | |
32 | valid_ground_type(X) :- valid_ground_type_aux(X),!. | |
33 | valid_ground_type(X) :- add_error(valid_ground_type,'Illegal type term: ',X),fail. | |
34 | ||
35 | %:- use_module(b_global_sets,[b_global_set/1]). | |
36 | ||
37 | valid_ground_type_aux(any) :- format(user_error,'! Type contains *any*~n',[]). % can happen, e.g., for test 949 due to assertion prj1({{}},BOOL)({}|->TRUE) = {} | |
38 | valid_ground_type_aux(integer). | |
39 | valid_ground_type_aux(string). | |
40 | valid_ground_type_aux(boolean). | |
41 | valid_ground_type_aux(global(G)) :- atom(G). | |
42 | %bmachine:b_get_machine_set(G). | |
43 | %b_global_sets:b_global_set(G). | |
44 | valid_ground_type_aux(freetype(FT)) :- ground(FT). | |
45 | valid_ground_type_aux(set(X)) :- valid_ground_type(X). | |
46 | valid_ground_type_aux(seq(X)) :- valid_ground_type(X). | |
47 | valid_ground_type_aux(couple(X,Y)) :- valid_ground_type(X), valid_ground_type(Y). | |
48 | valid_ground_type_aux(record(Fields)) :- valid_fields(Fields). | |
49 | ||
50 | valid_fields([]). | |
51 | valid_fields([field(Name,_)|_]) :- \+ atom(Name),!, | |
52 | add_error(valid_ground_type,'Illegal record field name: ',Name),fail. | |
53 | valid_fields([field(_Name,Type)|T]) :- | |
54 | valid_ground_type(Type), | |
55 | valid_fields(T). | |
56 | ||
57 | ||
58 | % -------------- | |
59 | ||
60 | :- use_module(kernel_freetypes,[get_freeval_type/3]). | |
61 | :- use_module(b_global_sets,[b_get_fd_type_bounds/3,get_global_type_value/3]). | |
62 | any_value_for_type(T,V) :- if(inst2(T,V),true, (nl,print('*** instantiate_to_any_value failed: '), print(T:V),nl,nl %,trace,inst2(T,V) | |
63 | )). | |
64 | %inst2(_,V) :- ground(V),!. | |
65 | %inst2(Type,V) :- print(inst2(Type,V)),nl,trace,fail. | |
66 | inst2(boolean,V) :- !, inst3(V,pred_true). | |
67 | inst2(pred,V) :- !, inst3(V,pred_true). | |
68 | inst2(integer,V) :- !, V=int(X),inst_fd(X,0). | |
69 | inst2(set(_),V) :- !, inst3(V,[]). % TO DO: what if V already partially instantiated | |
70 | inst2(seq(_),V) :- !, inst3(V,[]). % TO DO: what if V already partially instantiated | |
71 | inst2(couple(TA,TB),V) :- !, V=(A,B), inst2(TA,A), inst2(TB,B). | |
72 | inst2(string,V) :- !, V=string(X), inst3(X,''). | |
73 | inst2(global(T),V) :- !, get_global_type_value(V,T,X), | |
74 | b_get_fd_type_bounds(T,LowBnd,_UpBnd), | |
75 | inst_fd(X,LowBnd). | |
76 | inst2(record(Fields),rec(Vals)) :- !, instantiate_fields(Fields,Vals). | |
77 | inst2(constant([A]),V) :- !, V=term(A). | |
78 | inst2(freetype(FT),V) :- !, V=freeval(FT,CASE,Val), | |
79 | (nonvar(CASE) -> (get_freeval_type(FT,CASE,Type) -> any_value_for_type(Type,Val)) % ensure no backtracking | |
80 | ; nonvar(Val) -> print((nonvar_value(V))),nl, get_freeval_type(FT,CASE,Type), any_value_for_type(Type,Val) | |
81 | ; (get_freeval_type(FT,C,Type) -> CASE=C, any_value_for_type(Type,Val)) | |
82 | ). | |
83 | inst2(X,V) :- print(cannot_inst2(X,V)),nl. | |
84 | ||
85 | inst3(X,V) :- (var(X) -> X=V ; true). | |
86 | ||
87 | :- use_module(probsrc(clpfd_interface), [clpfd_some_element_in_domain/2]). | |
88 | inst_fd(X,_) :- nonvar(X),!. | |
89 | inst_fd(X,_Default) :- clpfd_some_element_in_domain(X,El),!, X=El. | |
90 | inst_fd(X,X). | |
91 | ||
92 | instantiate_fields([],[]). | |
93 | instantiate_fields([field(Name,Type)|T],[field(Name,Val)|TV]) :- | |
94 | any_value_for_type(Type,Val), | |
95 | instantiate_fields(T,TV). | |
96 | ||
97 | % ---------------------- | |
98 | ||
99 | % replace seq(X) by set(couple(integer,X)) | |
100 | ||
101 | normalize_type(X,Y) :- | |
102 | (normalize_type_aux(X,Y) -> true ; add_internal_error('Illegal type: ',normalize_type(X,Y)),Y=X). | |
103 | ||
104 | normalize_type_aux(V,R) :- var(V),!,R=V. | |
105 | normalize_type_aux(any,any). | |
106 | normalize_type_aux(pred,pred). | |
107 | normalize_type_aux(subst,subst). | |
108 | normalize_type_aux(boolean,boolean). | |
109 | normalize_type_aux(integer,integer). | |
110 | normalize_type_aux(string,string). | |
111 | normalize_type_aux(global(F),global(F)). | |
112 | normalize_type_aux(freetype(F),freetype(F)). | |
113 | normalize_type_aux(set(X),set(N)) :- normalize_type_aux(X,N). | |
114 | normalize_type_aux(seq(X),set(couple(integer,N))) :- normalize_type_aux(X,N). | |
115 | normalize_type_aux(couple(X,Y),couple(NX,NY)) :- normalize_type_aux(X,NX),normalize_type_aux(Y,NY). | |
116 | normalize_type_aux(record(F),record(NF)) :- normalize_type_fields(F,NF). | |
117 | normalize_type_aux(op(A,B),op(NA,NB)) :- maplist(normalize_type_aux,A,NA), maplist(normalize_type_aux,B,NB). | |
118 | ||
119 | normalize_type_fields([],[]). | |
120 | normalize_type_fields([field(N,T)|R],[field(N,NT)|RN]) :- normalize_type_aux(T,NT),normalize_type_fields(R,RN). |