1		% (c) 2009 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		; otherwise ->
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		unify_kodkod_types(int_expression,int_expression,Expr,Expr) :- !.
83		unify_kodkod_types(formula,formula,Expr,Expr) :- !.
84		unify_kodkod_types(rel([R]),int_expression,Expr,int2intset(Expr)) :-
85		intset_relation_kodkod_name(R),!.
86		unify_kodkod_types(rel([R]),int_expression,Expr,int2pow2(Expr)) :-
87		pow2integer_relation_kodkod_name(R),!.
88		unify_kodkod_types(int_expression,rel([_]),Expr,expr2int(Expr)).
89		% intset_relation_kodkod_name(R).
90
91		type_kodkod2(relref(Id), Env, rel(Types), relref(Id)) :- !,
92		lookup_reltypes(Id,Env,Types).
93		type_kodkod2(varref(Id), Env, VType, K) :- !,
94		lookup_vartypes(Id,Env,Types),
95		( Types = [p2i] ->
96		VType = int_expression, K=expr2int(varref(Id))
97		; otherwise ->
98		VType = rel(Types), K=varref(Id)).
99		type_kodkod2(int(I), _Env, int_expression, int(I)) :- !.
100		type_kodkod2(prj(Pos,Arg), Env, rel(P), prj(Pos,NArg)) :-
101		!,type_kodkod(Arg,Env,rel(S),NArg),
102		nth0s(Pos,S,P).
103		type_kodkod2(forall(Decls,Formula), Env, formula, forall(NDecls,NFormula)) :-
104		!,type_quantifier(Decls,Formula,Env,_,NDecls,NFormula).
105		type_kodkod2(exists(Decls,Formula), Env, formula, exists(NDecls,NFormula)) :-
106		!,type_quantifier(Decls,Formula,Env,_,NDecls,NFormula).
107		type_kodkod2(comp(Decls,Expr), Env, rel(Types), comp(NDecls,NExpr)) :-
108		!,type_quantifier(Decls,Expr,Env,rel(Types),NDecls,NExpr).
109		type_kodkod2(Expr, Env, Type, NExpr) :-
110		functor(Expr,F,Arity),
111		functor(Lookup,F,Arity),
112		ktype(Lookup,Type),!,
113		Expr =.. [_|Args], Lookup =.. [_|Types],
114		maplist(type_kodkod3(Env),Args,Types,NArgs),
115		NExpr =.. [F|NArgs].
116		type_kodkod2(Expr, _Env, _Type, _NExpr) :-
117		throw( unsupported_kodkod_expression(Expr) ).
118
119		% just to swap arguments
120		type_kodkod3(Env,Expr,Type,NExpr) :-
121		type_kodkod(Expr,Env,Type,NExpr).
122
123		type_quantifier(Decls,Subexpr,Env,rel(Types),NDecls,NSubexpr) :-
124		type_kodkod_declarations(Decls,Env,Env,NDecls,Subenv,Types),
125		type_kodkod(Subexpr,Subenv,formula,NSubexpr).
126
127		type_kodkod_declarations([],_,Env,[],Env,[]).
128		type_kodkod_declarations([Decl|Drest],Env,EnvIn,[NDecl|Nrest],EnvOut,Types) :-
129		type_kodkod_declaration(Decl,Env,EnvIn,NDecl,EnvInter,Types1),
130		safe_append(Types1,Types2,Types),
131		type_kodkod_declarations(Drest,Env,EnvInter,Nrest,EnvOut,Types2).
132		type_kodkod_declaration(decl(Id,Arity,Mult,Expr),Env,EnvIn,
133		decl(Id,Arity,Mult,NExpr),EnvOut,Types) :-
134		add_var_to_type_env(Id,Types,Env,Subenv),
135		type_kodkod(Expr,Subenv,rel(Types),NExpr),
136		add_var_to_type_env(Id,Types,EnvIn,EnvOut).
137
138
139		ktype(true,formula).
140		ktype(false,formula).
141		ktype(not(formula),formula).
142		ktype(and(formula,formula),formula).
143		ktype(or(formula,formula),formula).
144		ktype(implies(formula,formula),formula).
145		ktype(iff(formula,formula),formula).
146
147		ktype(one(rel(_)), formula).
148		ktype(some(rel(_)), formula).
149		ktype(no(rel(_)), formula).
150		ktype(lone(rel(_)), formula).
151		ktype(set(rel(_)), formula).
152
153		ktype(in(rel(T),rel(T)), formula).
154		ktype(equals(T,T),formula).
155		ktype(pfunc(rel(_),rel(_),rel(_)), formula).
156		ktype(func(rel(_),rel(_),rel(_)), formula).
157
158		ktype(empty,rel(_)).
159		ktype(iden,rel(_)).
160		ktype(univ,rel(_)).
161		ktype(intersection(rel(A),rel(A)), rel(A)).
162		ktype(union(rel(A),rel(A)), rel(A)).
163		ktype(difference(rel(A),rel(A)), rel(A)).
164		ktype(overwrite(rel(A),rel(A)), rel(A)).
165		ktype(closure(rel(A)), rel(A)).
166		ktype(reflexive_closure(rel(A)), rel(A)).
167		ktype(product(rel(A),rel(B)), rel(C)) :- safe_append(A,B,C).
168		ktype(transpose(rel(R)), rel(T)) :- safe_reverse(R,T).
169		ktype(join(rel(A),rel([Bhead|Btail])), rel(C)) :-
170		safe_append(Astart,[Bhead],A),
171		safe_append(Astart,Btail,C).
172		ktype(if(formula,rel(R),rel(R)), rel(R)).
173
174		ktype(gt(int_expression,int_expression), formula).
175		ktype(gte(int_expression,int_expression), formula).
176		ktype(lt(int_expression,int_expression), formula).
177		ktype(lte(int_expression,int_expression), formula).
178
179		ktype(card(rel(_)), int_expression).
180		ktype(add(int_expression,int_expression), int_expression).
181		ktype(sub(int_expression,int_expression), int_expression).
182		ktype(mul(int_expression,int_expression), int_expression).
183		ktype(div(int_expression,int_expression), int_expression).
184		ktype(floored_div(int_expression,int_expression), int_expression).
185		ktype(mod(int_expression,int_expression), int_expression).
186		ktype(sum(rel([_])), int_expression).
187
188		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
189
190		nth0s(Positions,List,Elements) :- maplist(nth0s2(List),Positions,Elements).
191		nth0s2(List,Position,Element) :- nth0(Position,List,Element).
192
193		safe_append(A,B,C) :-
194		complete_list(A,AComplete),
195		complete_list(B,BComplete),
196		complete_list(C,CComplete),
197		safe_append2(A,B,C,AComplete,BComplete,CComplete).
198		:- block safe_append2(?,?,?,-,-,?), safe_append2(?,?,?,-,?,-).
199		safe_append2(A,B,C,1,1,1) :- append(A,B,C),!.
200		:- block complete_list(-,?).
201		complete_list([],1).
202		complete_list([_|T],Trigger) :- complete_list(T,Trigger).
203
204		safe_reverse(A,B) :-
205		safe_reverse2(A,[],B),
206		safe_reverse2(B,[],A).
207		:- block safe_reverse2(-,?,?).
208		safe_reverse2([],Acc,Acc).
209		safe_reverse2([H|T],Acc,Rev) :-
210		safe_reverse2(T,[H|Acc],Rev).