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).