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(partition_detection, [detect_partitions/2, detect_all_partitions_in_predicate/2]).
6
7		:- use_module(module_information,[module_info/2]).
8		:- module_info(group,typechecker).
9		:- module_info(description,'This module detects set partition predicates.').
10
11		:- use_module(library(lists)).
12		:- use_module(bsyntaxtree).
13		:- use_module(bmachine_structure,[select_section/5]).
14
15		detect_partitions(In,Out) :-
16		select_section(properties,Old,New,In,Out),
17		detect_all_partitions_in_predicate(Old,New).
18
19		% detect all set partition predicates at "top-level", not inside inner predicates (bool(.), comprehension_set,...)
20		% this is assumed to be checked by b_ast_cleanup during bottom-up construction
21		detect_all_partitions_in_predicate(Predicate,NewPredicate) :-
22		( detect_partitions_in_predicate(Predicate,P1) ->
23		detect_all_partitions_in_predicate(P1,NewPredicate)
24		; otherwise ->
25		Predicate=NewPredicate %, print('detected: '),translate:print_bexpr(NewPredicate),nl
26		%detect_partitions_inside_predicate(Predicate,NewPredicate) % now done in b_ast_cleanup
27		).
28
29		% detect partitions of set of the type:
30		% x /\ y = {} & x \/ y = z
31		detect_partitions_in_predicate(Predicate,NewPredicate) :-
32		conjunction_to_list(Predicate,PList),
33		detect_partitions_in_predicates(PList,PNew),
34		conjunct_predicates(PNew,NewPredicate).
35		detect_partitions_in_predicates(Predicates,NewPredicates) :- Predicates \= [],
36	?	find_union(Superset,Partitions,Predicates,P1),
37		create_pairs(Partitions,Pairs),
38		get_texpr_type(Superset,Type),
39		find_all_intersections(Pairs,Type,RestPairs,P1,P2),
40		RestPairs=[],
41		!,
42		safe_create_texpr(partition(Superset,Partitions),pred,Part),
43		NewPredicates=[Part|P2].
44
45		:- use_module(bsyntaxtree,[get_texpr_set_type/2]).
46		% should we also find A = {c1,c2,...cn} with all_different(c1,...,cn) ??
47		find_union(Superset,Partitions,In,Out) :-
48	?	create_texpr(equal(A,B),pred,_,Equal),
49	?	get_texpr_set_type(A,Type),
50	?	get_texpr_set_type(B,Type),
51	?	select(Equal,In,Out),
52		( is_union(A,Partitions) -> Superset=B
53		; is_union(B,Partitions) -> Superset=A).
54		is_union(Expr,Partitions) :-
55		get_texpr_expr(Expr,union(_,_)),
56		collect_union(Expr,Partitions,[]).
57		collect_union(Expr) -->
58		{get_texpr_expr(Expr,union(A,B)),!},
59		collect_union(A),
60		collect_union(B).
61		collect_union(Expr) --> [Expr].
62
63		create_pairs(Parts,Pairs) :-
64		create_pairs2(Parts,Pairs,[]).
65		create_pairs2([]) --> [].
66		create_pairs2([A|Rest]) -->
67		create_pairs3(Rest,A),
68		create_pairs2(Rest).
69		create_pairs3([],_) --> [].
70		create_pairs3([B|Rest],A) -->
71		[distinct(A,B)],
72		create_pairs3(Rest,A).
73
74		find_all_intersections(Pairs,Type,RestPairs,In,Out) :-
75		find_all_intersections2(In,Pairs,Type,RestPairs,Out).
76		find_all_intersections2([],Pairs,_,Pairs,[]).
77		find_all_intersections2([Expr|Erest],Pairs,Type,RestPairs,Out) :-
78		is_disjoint_pred(Expr,Type,A,B),
79		remove_pair(A,B,Pairs,InterPairs),!,
80		find_all_intersections2(Erest,InterPairs,Type,RestPairs,Out).
81		find_all_intersections2([Expr|Erest],Pairs,Type,RestPairs,[Expr|Out]) :-
82		find_all_intersections2(Erest,Pairs,Type,RestPairs,Out).
83
84		is_disjoint_pred(b(Expr,_,_),Type,A,B) :-
85		is_disjoint_pred2(Expr,Type,A,B).
86		is_disjoint_pred2(equal(X,Y),_,A,B) :- % detect A /\ B = {} or {} = A /\ B
87		( get_texpr_expr(X,empty_set) -> Inter=Y
88		; get_texpr_expr(Y,empty_set) -> Inter=X),
89		get_texpr_expr(Inter,intersection(A,B)).
90		is_disjoint_pred2(not_equal(X,Y),set(Type),A,B) :- get_texpr_type(X,Type),
91		A = b(set_extension([X]),set(Type),_),
92		B = b(set_extension([Y]),set(Type),_).
93		is_disjoint_pred2(negation(NE),Type,A,B) :-
94		is_disjoint_neg_pred(NE,Type,A,B).
95
96		is_disjoint_neg_pred(b(Expr,_,_),Type,A,B) :-
97		is_disjoint_neg_pred2(Expr,Type,A,B).
98		is_disjoint_neg_pred2(not_equal(X,Y),_,A,B) :- % detect A /\ B /= {} or {} /= A /\ B
99		( get_texpr_expr(X,empty_set) -> Inter=Y
100		; get_texpr_expr(Y,empty_set) -> Inter=X),
101		get_texpr_expr(Inter,intersection(A,B)).
102		is_disjoint_neg_pred2(equal(X,Y),set(Type),A,B) :- get_texpr_type(X,Type),
103		A = b(set_extension([X]),set(Type),_),
104		B = b(set_extension([Y]),set(Type),_).
105		is_disjoint_neg_pred2(negation(NE),Type,A,B) :-
106		is_disjoint_pred(NE,Type,A,B).
107
108		remove_pair(A,B,In,Out) :-
109		remove_all_infos(A,FA),
110		remove_all_infos(B,FB),
111	?	( select(distinct(FA,FB),In,Out)
112		; select(distinct(FB,FA),In,Out)),!.