1 % (c) 2014 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_rewrite,[ apply_rewriting_rules/2 ]).
6
7 :- use_module(probsrc(module_information),[module_info/2]).
8 :- module_info(group,kodkod).
9 :- module_info(description,'This module contains rewriting rules that are applied during tge translation to Kodkod.').
10
11 :- use_module(library(lists)).
12 :- use_module(probsrc(bsyntaxtree)).
13 :- use_module(kodkod_tools).
14
15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16 % applying re-writing rules to make some statements translatable to Kodkod
17
18 apply_rewriting_rules(TExpr,NTExpr) :-
19 remove_bt(TExpr,Expr,NExpr,NTExpr),
20 get_texpr_info(TExpr,Info),
21 apply_rewriting_rules_pre(Expr,Info,IExpr),
22 syntaxtransformation(IExpr,Subs,_,NSubs,Expr1),
23 maplist(apply_rewriting_rules,Subs,NSubs),
24 apply_rewriting_rules_post(Expr1,Info,NExpr).
25 apply_rewriting_rules_pre(Expr,Info,NExpr) :-
26 kodkod_rewrite_pre(Expr,Info,Expr1),!,
27 apply_rewriting_rules_pre(Expr1,Info,NExpr).
28 apply_rewriting_rules_pre(Expr,_,Expr).
29 apply_rewriting_rules_post(Expr,Info,NExpr) :-
30 kodkod_rewrite_post(Expr,Info,Expr1),!,
31 apply_rewriting_rules_post(Expr1,Info,NExpr).
32 apply_rewriting_rules_post(Expr,_,Expr).
33
34 :- use_module(probsrc(bsyntaxtree),[get_texpr_set_type/2]).
35 kodkod_rewrite_pre(not_equal(A,B),_,negation(Equal)) :- !,
36 create_kk_tpred(equal(A,B),Equal).
37 kodkod_rewrite_pre(member(Elem,Powset),_,Result) :-
38 get_texpr_expr(Powset,PExpr),
39 get_texpr_info(Elem,ElemInfo),
40 kodkod_rewrite_membership(PExpr,Elem,ElemInfo,Result),
41 !.
42 kodkod_rewrite_pre(subset(Subset,Powset),_,forall([Elem],TPre,TCond)) :-
43 get_texpr_info(Subset,Info),
44 get_texpr_set_type(Subset,ElemType),
45 unique_identifier(TId),
46 element_analysis(Info,ElemInfo),
47 create_texpr(identifier(TId),ElemType,ElemInfo,Elem),
48 get_texpr_expr(Powset,PExpr),
49 kodkod_rewrite_membership(PExpr,Elem,ElemInfo,Cond),!,
50 create_texpr(member(Elem,Subset),pred,[],TPre),
51 create_texpr(Cond,pred,[],TCond).
52 kodkod_rewrite_pre(size(Seq),_,card(Seq)) :- !.
53 kodkod_rewrite_post(interval(A,B),Info,comprehension_set([TmpId],Predicate)) :- !,
54 element_analysis(Info,ElemInfo),
55 unique_identifier(TId),
56 create_texpr(identifier(TId),integer,ElemInfo,TmpId),
57 create_texpr(less_equal(A,TmpId),pred,[],Left),
58 create_texpr(less_equal(TmpId,B),pred,[],Right),
59 conjunct_predicates([Left,Right],Predicate).
60 kodkod_rewrite_post(sequence_extension(Elems),_Info,set_extension(Pairs)) :- !,
61 convert_elements_to_pairs(Elems,1,Pairs).
62 kodkod_rewrite_post(general_sum([TId],Pred,Expr),_Info,general_sum([TId],NPred,Expr)) :-
63 get_texpr_id(TId,Id), get_texpr_id(TElem,Id),
64 extract_finite_integer_range(TId,[],IRange),
65 \+ get_texpr_expr(Pred,member(TElem,_TSet)),!,
66 write('rewritten\n'),
67 create_texpr(comprehension_set([TId],Pred),set(integer),[analysis([elem(interval):IRange])],
68 TCompSet),
69 create_texpr(member(TId,TCompSet),pred,[],NPred).
70 convert_elements_to_pairs([],_,[]).
71 convert_elements_to_pairs([Elem|Erest],Index,[Pair|Prest]) :-
72 convert_element_to_pair(Elem,Index,Pair),
73 I2 is Index + 1,
74 convert_elements_to_pairs(Erest,I2,Prest).
75 convert_element_to_pair(Elem,Index,Pair) :-
76 Range = irange(Index,Index),
77 create_texpr(integer(Index),integer,[analysis([interval:Range])],TIndex),
78 get_texpr_type(Elem,Type),
79 get_texpr_info(Elem,EInfo),
80 findall(right(Scope):Info,
81 ( memberchk(analysis(AInfos),EInfo),member(Scope:Info,AInfos)),
82 RInfos),
83 create_texpr(couple(TIndex,Elem),couple(integer,Type),[analysis([left(interval):Range|RInfos])],Pair).
84
85 kodkod_rewrite_membership(pow_subset(Set),Elem,_,subset(Elem,Set)).
86 kodkod_rewrite_membership(fin_subset(Set),Elem,_,subset(Elem,Set)).
87 kodkod_rewrite_membership(relations(A,B),Elem,_,subset(Elem,Cartesian)) :-
88 create_kk_tpred(cartesian_product(A,B),Cartesian).
89 kodkod_rewrite_membership(pow1_subset(Set),Elem,ElemInfo,conjunct(Subset,Exists)) :-
90 get_texpr_set_type(Set,Type),
91 create_texpr(identifier('___elem'),Type,[kodkod|ElemInfo],Id),
92 create_kk_tpred(subset(Elem,Set),Subset),
93 create_kk_tpred(exists([Id],Member),Exists),
94 create_kk_tpred(member(Id,Set),Member).
95 kodkod_rewrite_membership(fin1_subset(Set),Elem,Info,Pred) :-
96 kodkod_rewrite_membership(pow1_subset(Set),Elem,Info,Pred).
97 kodkod_rewrite_membership(interval(A,B),Elem,_,conjunct(Lower,Upper)) :-
98 create_kk_tpred(less_equal(A,Elem),Lower),
99 create_kk_tpred(less_equal(Elem,B),Upper).
100 kodkod_rewrite_membership(integer_set('NATURAL'),Elem,_,less_equal(Zero,Elem)) :-
101 create_integer_with_analysis(0,Zero).
102 kodkod_rewrite_membership(integer_set('NATURAL1'),Elem,_,less_equal(One,Elem)) :-
103 create_integer_with_analysis(1,One).
104 create_kk_tpred(Pred,TPred) :-
105 create_texpr(Pred,pred,[kodkod],TPred).
106 create_integer_with_analysis(I,Expr) :-
107 create_texpr(integer(I),integer,[analysis([interval:irange(I,I)])],Expr).
108
109 element_analysis(SetInfo,[analysis(MemberInfo)]) :-
110 findall( S:R,
111 ( member(analysis(Analysis), SetInfo),
112 member(elem(S):R,Analysis)),
113 MemberInfo).