never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Horizontal.Partition where
4
5 import Conjure.Rules.Import
6
7
8 rule_Comprehension_Literal :: Rule
9 rule_Comprehension_Literal = "partition-comprehension-literal" `namedRule` theRule where
10 theRule (Comprehension body gensOrConds) = do
11 (gocBefore, (pat, p), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
12 Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDef opParts expr)
13 _ -> na "rule_Comprehension_Literal"
14 (TypePartition tau, elems) <- match partitionLiteral p
15 let outLiteral = make matrixLiteral
16 (TypeMatrix (TypeInt TagInt) (TypeSet tau))
17 (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength elems))])
18 [ AbstractLiteral (AbsLitSet e)
19 | e <- elems
20 ]
21 let upd val old = lambdaToFunction pat old val
22 return
23 ( "Comprehension on partition literals"
24 , do
25 (iPat, i) <- quantifiedVar
26 return $ Comprehension (upd i body)
27 $ gocBefore
28 ++ [Generator (GenInExpr iPat outLiteral)]
29 ++ transformBi (upd i) gocAfter
30 )
31 theRule _ = na "rule_Comprehension_PartitionLiteral"
32
33
34 rule_Eq :: Rule
35 rule_Eq = "partition-eq" `namedRule` theRule where
36 theRule p = do
37 (x,y) <- match opEq p
38 TypePartition{} <- typeOf x
39 TypePartition{} <- typeOf y
40 return
41 ( "Horizontal rule for partition equality"
42 , return $ make opEq (make opParts x) (make opParts y)
43 )
44
45
46 rule_Neq :: Rule
47 rule_Neq = "partition-neq" `namedRule` theRule where
48 theRule [essence| &x != &y |] = do
49 TypePartition{} <- typeOf x
50 TypePartition{} <- typeOf y
51 return
52 ( "Horizontal rule for partition dis-equality"
53 , do
54 (iPat, i) <- quantifiedVar
55 return [essence|
56 (exists &iPat in &x . !(&i in &y))
57 \/
58 (exists &iPat in &y . !(&i in &x))
59 |]
60 )
61 theRule _ = na "rule_Neq"
62
63
64 rule_Together :: Rule
65 rule_Together = "partition-together" `namedRule` theRule where
66 theRule [essence| together(&x,&p) |] = do
67 TypePartition{} <- typeOf p
68 DomainPartition _ _ inner <- domainOf p
69 return
70 ( "Horizontal rule for partition-together"
71 , do
72 (iPat, i) <- quantifiedVar
73 (jPat, j) <- quantifiedVar
74 (kPat, k) <- quantifiedVar
75 return [essence|
76 (exists &iPat in parts(&p) . &x subsetEq &i)
77 /\
78 $ the items in x appear somewhere in the partition
79 (forAll &jPat in &x . exists &kPat : &inner . &j = &k)
80 |]
81 )
82 theRule _ = na "rule_Together"
83
84
85 rule_Apart :: Rule
86 rule_Apart = "partition-apart" `namedRule` theRule where
87 theRule [essence| apart(&x,&p) |] = do
88 case p of
89 -- this is because this rule would change the parity of the DefinednessConstraints
90 -- they should be bubbled up first.
91 WithLocals{} -> na "rule_Apart"
92 _ -> return ()
93 TypePartition{} <- typeOf p
94 DomainPartition _ _ inner <- domainOf p
95 return
96 ( "Horizontal rule for partition-apart"
97 , do
98 (iPat, i) <- quantifiedVar
99 (jPat, j) <- quantifiedVar
100 (kPat, k) <- quantifiedVar
101 return [essence|
102 (forAll &iPat in parts(&p) . !(&x subsetEq &i))
103 /\
104 $ the items in x appear somewhere in the partition
105 (forAll &jPat in &x . exists &kPat : &inner . &j = &k)
106 |]
107 )
108 theRule _ = na "rule_Apart"
109
110
111 rule_Party :: Rule
112 rule_Party = "partition-party" `namedRule` theRule where
113 theRule (Comprehension body gensOrConds) = do
114 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
115 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
116 _ -> na "rule_Comprehension_Literal"
117 (mkModifier, expr2) <- match opModifier expr
118 (wanted, p) <- match opParty expr2
119 TypePartition{} <- typeOf p
120 let upd val old = lambdaToFunction pat old val
121 return
122 ( "Comprehension on a particular part of a partition"
123 , do
124 (iPat, i) <- quantifiedVar
125 (jPat, j) <- quantifiedVar
126 return $
127 Comprehension (upd j body)
128 $ gocBefore
129 ++ [ Generator (GenInExpr iPat (make opParts p))
130 , Condition [essence| &wanted in &i |]
131 , Generator (GenInExpr jPat (mkModifier i))
132 ]
133 ++ transformBi (upd j) gocAfter
134 )
135 theRule _ = na "rule_Party"
136
137
138 rule_Participants :: Rule
139 rule_Participants = "partition-participants" `namedRule` theRule where
140 theRule (Comprehension body gensOrConds) = do
141 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
142 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
143 _ -> na "rule_Comprehension_Literal"
144 p <- match opParticipants expr
145 TypePartition{} <- typeOf p
146 let upd val old = lambdaToFunction pat old val
147 return
148 ( "Comprehension on participants of a partition"
149 , do
150 (iPat, i) <- quantifiedVar
151 (jPat, j) <- quantifiedVar
152 return $ Comprehension (upd j body)
153 $ gocBefore
154 ++ [ Generator (GenInExpr iPat (make opParts p))
155 , Generator (GenInExpr jPat i)
156 ]
157 ++ transformBi (upd j) gocAfter
158 )
159 theRule _ = na "rule_Participants"
160
161
162 rule_Card :: Rule
163 rule_Card = "partition-card" `namedRule` theRule where
164 theRule p = do
165 partition_ <- match opTwoBars p
166 TypePartition{} <- typeOf partition_
167 return
168 ( "Cardinality of a partition"
169 , return $ make opTwoBars $ make opParticipants partition_
170 )
171
172
173 rule_In :: Rule
174 rule_In = "partition-in" `namedRule` theRule where
175 theRule [essence| &x in &p |] = do
176 TypePartition{} <- typeOf p
177 return
178 ( "Horizontal rule for partition-in."
179 , return [essence| &x in parts(&p) |]
180 )
181 theRule _ = na "rule_In"