1		% (c) 2009-2024 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(kodkod_typing,[kodkod_insert_casts/4]).
6
7		:- use_module(library(lists)).
8		:- use_module(library(avl)).
9
10		:- use_module(probsrc(module_information),[module_info/2]).
11		:- use_module(probsrc(tools),[foldl/4]).
12
13		:- use_module(kodkod_tools).
14
15		:- module_info(group,kodkod).
16		:- module_info(description,'This is a small internal type checker for Kodkod expressions. It\'s needed for inserting casts between different integer representations.').
17
18		kodkod_insert_casts(Kin,TypeMap,IdMap,Kout) :-
19		create_refmap(TypeMap,IdMap,Env),
20		type_kodkod(Kin,Env,formula,Kout).
21
22		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
23		% create Kodkod typechecking environment
24		create_refmap(TypeMap,IdMap,ktypenv(Env,StartEnv)) :-
25		empty_avl(StartEnv),
26		create_refmap_types(TypeMap,StartEnv,TypeEnv),
27		create_refmap_ids(IdMap,TypeEnv,Env).
28		lookup_reltypes(Id,ktypenv(Env,_Vars),Types) :-
29		avl_fetch(Id,Env,Types).
30		lookup_vartypes(Id,ktypenv(_Env,Vars),Types) :-
31		avl_fetch(Id,Vars,Types).
32		add_var_to_type_env(Id,Types,ktypenv(E,EnvIn),ktypenv(E,EnvOut)) :-
33		avl_store(Id,EnvIn,Types,EnvOut).
34
35		create_refmap_types(TypeMap,In,Out) :-
36		avl_range(TypeMap,Relations1),
37		maplist(remove_relation_wrapper,Relations1,Relations),
38		foldl(add_to_refmap,Relations,In,Out).
39		remove_relation_wrapper(relation(_,_,Rel),Rel).
40
41		create_refmap_ids(IdMap,In,Out) :-
42		avl_range(IdMap,Relations),
43		foldl(add_to_refmap,Relations,In,Out).
44		add_to_refmap(R,In,Inter) :-
45		get_rel_types(R,Id,Types),
46		avl_store(Id,In,Types,Inter).
47		get_rel_types(reldef(Id,Types,_,_,_),Id,Types).
48		get_rel_types(intsetrel(Id,_,_),Id,[R]) :-
49		intset_relation_kodkod_name(R).
50		get_rel_types(pow2rel(Id,_,_),Id,[R]) :-
51		pow2integer_relation_kodkod_name(R).
52
53		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54		% typechecking kodkod expressions with inserting type-casts
55
56		type_kodkod(KExpr1, Env, OuterType, OuterExpr) :-
57		( KExpr1 = KExpr:ExpectedType ->
58		% The expression has an explicit type associated,
59		% first make sure that this expected type matches the type seen
60		% by the caller (insert cast if necessary)
61		unify_kodkod_types(ExpectedType,OuterType,Expr,OuterExpr)
62		;
63		% If there is no explicit type given, the type seen by the
64		% outside is used as the expected type. No cast is needed
65		KExpr=KExpr1, ExpectedType=OuterType, OuterExpr=Expr
66		),
67		% Now type-check the expression itself
68		type_kodkod2(KExpr, Env, InnerType, InnerExpr),
69		% and try to match the types (insert cat if necessary)
70		unify_kodkod_types(ExpectedType,InnerType,InnerExpr,Expr).
71
72		:- block unify_kodkod_types(-,-,?,?).
73		unify_kodkod_types(rel(A),rel(B),Expr,NewExpr) :- !,
74		( A=B -> Expr=NewExpr
75		% both relations can be unified, good
76		; A=[IS],intset_relation_kodkod_name(IS),
77		B=[P2I],pow2integer_relation_kodkod_name(P2I) ->
78		% expected was a set of integers but given was a set representing
79		% one integer by its bits
80		% TODO: this conversion is not optimal, better try to avoid rel([p2i])
81		NewExpr = int2intset(expr2int(Expr))
82		; A = [P2I],pow2integer_relation_kodkod_name(P2I),
83		B = [IS],intset_relation_kodkod_name(IS)
84		-> % happens in test 709 when rewriting (x=E or x=F) into x:{E,F}
85		% ((x=y or x=z) => (y=x or z=x)) & ((x=y or x=z) <=> (y=x or z=x))
86		% Test 2197 tests it explicitly
87		NewExpr = int2pow2(expr2int(Expr))
88		).
89		unify_kodkod_types(int_expression,int_expression,Expr,Expr) :- !.
90		unify_kodkod_types(formula,formula,Expr,Expr) :- !.
91		unify_kodkod_types(rel([R]),int_expression,Expr,int2intset(Expr)) :-
92		intset_relation_kodkod_name(R),!.
93		unify_kodkod_types(rel([R]),int_expression,Expr,int2pow2(Expr)) :-
94		pow2integer_relation_kodkod_name(R),!.
95		unify_kodkod_types(int_expression,rel([_]),Expr,expr2int(Expr)).
96		% intset_relation_kodkod_name(R).
97
98
99
100		type_kodkod2(relref(Id), Env, rel(Types), relref(Id)) :- !,
101		lookup_reltypes(Id,Env,Types).
102		type_kodkod2(varref(Id), Env, VType, K) :- !,
103		lookup_vartypes(Id,Env,Types),
104		( Types = [p2i] ->
105		VType = int_expression, K=expr2int(varref(Id))
106		;
107		VType = rel(Types), K=varref(Id)).
108		type_kodkod2(int(I), _Env, int_expression, int(I)) :- !.
109		type_kodkod2(prj(Pos,Arg), Env, rel(P), prj(Pos,NArg)) :-
110		!,type_kodkod(Arg,Env,rel(S),NArg),
111		nth0s(Pos,S,P).
112		type_kodkod2(forall(Decls,Formula), Env, formula, forall(NDecls,NFormula)) :-
113		!,type_quantifier(Decls,Formula,Env,_,NDecls,NFormula).
114		type_kodkod2(exists(Decls,Formula), Env, formula, exists(NDecls,NFormula)) :-
115		!,type_quantifier(Decls,Formula,Env,_,NDecls,NFormula).
116		type_kodkod2(comp(Decls,Expr), Env, rel(Types), comp(NDecls,NExpr)) :-
117		!,type_quantifier(Decls,Expr,Env,rel(Types),NDecls,NExpr).
118		type_kodkod2(Expr, Env, Type, NExpr) :-
119		functor(Expr,F,Arity),
120		functor(Lookup,F,Arity),
121		ktype(Lookup,Type),!,
122		Expr =.. [_|Args], Lookup =.. [_|Types],
123		maplist(type_kodkod3(Env),Args,Types,NArgs),
124		NExpr =.. [F|NArgs].
125		type_kodkod2(Expr, _Env, _Type, _NExpr) :-
126		throw( unsupported_kodkod_expression(Expr) ).
127
128		% just to swap arguments
129		type_kodkod3(Env,Expr,Type,NExpr) :-
130		type_kodkod(Expr,Env,Type,NExpr).
131
132		type_quantifier(Decls,Subexpr,Env,rel(Types),NDecls,NSubexpr) :-
133		type_kodkod_declarations(Decls,Env,Env,NDecls,Subenv,Types),
134		type_kodkod(Subexpr,Subenv,formula,NSubexpr).
135
136		type_kodkod_declarations([],_,Env,[],Env,[]).
137		type_kodkod_declarations([Decl|Drest],Env,EnvIn,[NDecl|Nrest],EnvOut,Types) :-
138		type_kodkod_declaration(Decl,Env,EnvIn,NDecl,EnvInter,Types1),
139		safe_append(Types1,Types2,Types),
140		type_kodkod_declarations(Drest,Env,EnvInter,Nrest,EnvOut,Types2).
141		type_kodkod_declaration(decl(Id,Arity,Mult,Expr),Env,EnvIn,
142		decl(Id,Arity,Mult,NExpr),EnvOut,Types) :-
143		add_var_to_type_env(Id,Types,Env,Subenv),
144		type_kodkod(Expr,Subenv,rel(Types),NExpr),
145		add_var_to_type_env(Id,Types,EnvIn,EnvOut).
146
147
148		ktype(true,formula).
149		ktype(false,formula).
150		ktype(not(formula),formula).
151		ktype(and(formula,formula),formula).
152		ktype(or(formula,formula),formula).
153		ktype(implies(formula,formula),formula).
154		ktype(iff(formula,formula),formula).
155
156		ktype(one(rel(_)), formula).
157		ktype(some(rel(_)), formula).
158		ktype(no(rel(_)), formula).
159		ktype(lone(rel(_)), formula).
160		ktype(set(rel(_)), formula).
161
162		ktype(in(rel(T),rel(T)), formula).
163		ktype(equals(T,T),formula).
164		ktype(pfunc(rel(_),rel(_),rel(_)), formula).
165		ktype(func(rel(_),rel(_),rel(_)), formula).
166
167		ktype(empty,rel(_)).
168		ktype(iden,rel(_)).
169		ktype(univ,rel(_)).
170		ktype(intersection(rel(A),rel(A)), rel(A)).
171		ktype(union(rel(A),rel(A)), rel(A)).
172		ktype(difference(rel(A),rel(A)), rel(A)).
173		ktype(overwrite(rel(A),rel(A)), rel(A)).
174		ktype(closure(rel(A)), rel(A)).
175		ktype(reflexive_closure(rel(A)), rel(A)).
176		ktype(product(rel(A),rel(B)), rel(C)) :- safe_append(A,B,C).
177		ktype(transpose(rel(R)), rel(T)) :- safe_reverse(R,T).
178		ktype(join(rel(A),rel([Bhead|Btail])), rel(C)) :-
179		safe_append(Astart,[Bhead],A),
180		safe_append(Astart,Btail,C).
181		ktype(if(formula,rel(R),rel(R)), rel(R)).
182
183		ktype(gt(int_expression,int_expression), formula).
184		ktype(gte(int_expression,int_expression), formula).
185		ktype(lt(int_expression,int_expression), formula).
186		ktype(lte(int_expression,int_expression), formula).
187
188		ktype(card(rel(_)), int_expression).
189		ktype(add(int_expression,int_expression), int_expression).
190		ktype(sub(int_expression,int_expression), int_expression).
191		ktype(mul(int_expression,int_expression), int_expression).
192		ktype(div(int_expression,int_expression), int_expression).
193		ktype(floored_div(int_expression,int_expression), int_expression).
194		ktype(mod(int_expression,int_expression), int_expression).
195		ktype(sum(rel([_])), int_expression).
196
197		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
198
199		nth0s(Positions,List,Elements) :- maplist(nth0s2(List),Positions,Elements).
200		nth0s2(List,Position,Element) :- nth0(Position,List,Element).
201
202		safe_append(A,B,C) :-
203		complete_list(A,AComplete),
204		complete_list(B,BComplete),
205		complete_list(C,CComplete),
206		safe_append2(A,B,C,AComplete,BComplete,CComplete).
207		:- block safe_append2(?,?,?,-,-,?), safe_append2(?,?,?,-,?,-).
208		safe_append2(A,B,C,1,1,1) :- append(A,B,C),!.
209		:- block complete_list(-,?).
210		complete_list([],1).
211		complete_list([_|T],Trigger) :- complete_list(T,Trigger).
212
213		safe_reverse(A,B) :-
214		safe_reverse2(A,[],B),
215		safe_reverse2(B,[],A).
216		:- block safe_reverse2(-,?,?).
217		safe_reverse2([],Acc,Acc).
218		safe_reverse2([H|T],Acc,Rev) :-
219		safe_reverse2(T,[H|Acc],Rev).