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