never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Horizontal.MSet where
4
5 import Conjure.Rules.Import
6
7
8 rule_Comprehension_Literal :: Rule
9 rule_Comprehension_Literal = "mset-comprehension-literal" `namedRule` theRule where
10 theRule (Comprehension body gensOrConds) = do
11 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
12 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
13 _ -> na "rule_Comprehension_Literal"
14 (TypeMSet tau, elems) <- match msetLiteral expr
15 let outLiteral = make matrixLiteral
16 (TypeMatrix (TypeInt TagInt) tau)
17 (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength elems))])
18 elems
19 let upd val old = lambdaToFunction pat old val
20 return
21 ( "Comprehension on mset literals"
22 , do
23 (iPat, i) <- quantifiedVar
24 return $ Comprehension (upd i body)
25 $ gocBefore
26 ++ [Generator (GenInExpr iPat outLiteral)]
27 ++ transformBi (upd i) gocAfter
28 )
29 theRule _ = na "rule_Comprehension_Literal"
30
31
32
33 -- freq(toMSet(flatten(m)), arg) ~~> sum([ toInt(arg = i) | i in mset ])
34 rule_Freq_toMSet_Flatten :: Rule
35 rule_Freq_toMSet_Flatten = "mset-freq-toMSet_Flatten" `namedRule` theRule where
36 theRule p = do
37 (mset, arg) <- match opFreq p
38 m <- match opToMSet mset >>= match opFlatten
39 indexDoms <- indexDomainsOf m
40 forM_ indexDoms $ \case
41 DomainAny{} -> na "rule_Comprehension_Flatten"
42 _ -> return ()
43 when (null indexDoms) $ na "rule_Comprehension_Flatten"
44 return
45 ( "Comprehension on a matrix flatten"
46 , do
47 (gens, is) <- unzip <$> sequence
48 [ do
49 (iPat, i) <- quantifiedVar
50 return (Generator (GenDomainNoRepr iPat d), i)
51 | d <- indexDoms
52 ]
53 let mis = make opMatrixIndexing m is
54 return $ make opSum $ Comprehension [essence| toInt(&arg = &mis) |] gens
55 )
56
57
58 rule_Comprehension_ToSet_Literal :: Rule
59 rule_Comprehension_ToSet_Literal = "mset-comprehension-toSet-literal" `namedRule` theRule where
60 theRule (Comprehension body gensOrConds) = do
61 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
62 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
63 _ -> na "rule_Comprehension_ToSet_Literal"
64 mset <- match opToSet expr
65 (TypeMSet tau, elems) <- match msetLiteral mset
66 let outLiteralDomain = mkDomainIntB 1 (fromInt $ genericLength elems)
67 let outLiteral = make matrixLiteral (TypeMatrix (TypeInt TagInt) tau) outLiteralDomain elems
68 let upd val old = lambdaToFunction pat old val
69 return
70 ( "Comprehension on toSet of mset literals"
71 , do
72 (iPat, i) <- quantifiedVar
73 (jPat, j) <- quantifiedVar
74 let iIndexed = [essence| &outLiteral[&i] |]
75 let jIndexed = [essence| &outLiteral[&j] |]
76 return $ Comprehension (upd iIndexed body)
77 $ gocBefore
78 ++ [ Generator (GenDomainNoRepr iPat outLiteralDomain)
79 , Condition [essence|
80 !(exists &jPat : &outLiteralDomain .
81 (&j < &i) /\ (&iIndexed = &jIndexed))
82 |]
83 ]
84 ++ transformBi (upd iIndexed) gocAfter
85 )
86 theRule _ = na "rule_Comprehension_ToSet_Literal"
87
88
89 rule_Eq :: Rule
90 rule_Eq = "mset-eq" `namedRule` theRule where
91 theRule p = do
92 (x,y) <- match opEq p
93 TypeMSet{} <- typeOf x
94 TypeMSet{} <- typeOf y
95 return
96 ( "Horizontal rule for mset equality"
97 , do
98 (iPat, i) <- quantifiedVar
99 return
100 [essence|
101 (forAll &iPat in &x . freq(&x,&i) = freq(&y,&i)) /\
102 (forAll &iPat in &y . freq(&x,&i) = freq(&y,&i))
103 |]
104 )
105
106
107 rule_Neq :: Rule
108 rule_Neq = "mset-neq" `namedRule` theRule where
109 theRule [essence| &x != &y |] = do
110 TypeMSet{} <- typeOf x
111 TypeMSet{} <- typeOf y
112 return
113 ( "Horizontal rule for mset dis-equality"
114 , do
115 (iPat, i) <- quantifiedVar
116 return
117 [essence|
118 (exists &iPat in &x . freq(&x,&i) != freq(&y,&i)) \/
119 (exists &iPat in &y . freq(&x,&i) != freq(&y,&i))
120 |]
121 )
122 theRule _ = na "rule_Neq"
123
124
125 rule_SubsetEq :: Rule
126 rule_SubsetEq = "mset-subsetEq" `namedRule` theRule where
127 theRule p = do
128 (x,y) <- match opSubsetEq p
129 TypeMSet{} <- typeOf x
130 TypeMSet{} <- typeOf y
131 return
132 ( "Horizontal rule for mset subsetEq"
133 , do
134 (iPat, i) <- quantifiedVar
135 return [essence| forAll &iPat in &x . freq(&x,&i) <= freq(&y,&i) |]
136 )
137
138
139 rule_Subset :: Rule
140 rule_Subset = "mset-subset" `namedRule` theRule where
141 theRule [essence| &x subset &y |] = do
142 TypeMSet{} <- typeOf x
143 TypeMSet{} <- typeOf y
144 return
145 ( "Horizontal rule for mset subset"
146 , do
147 (iPat, i) <- quantifiedVar
148 return
149 [essence|
150 (forAll &iPat in &x . freq(&x,&i) <= freq(&y,&i)) /\
151 (exists &iPat in &x . freq(&x,&i) < freq(&y,&i))
152 |]
153 )
154 theRule _ = na "rule_Subset"
155
156
157 rule_Supset :: Rule
158 rule_Supset = "mset-supset" `namedRule` theRule where
159 theRule [essence| &a supset &b |] = do
160 TypeMSet{} <- typeOf a
161 TypeMSet{} <- typeOf b
162 return
163 ( "Horizontal rule for mset supset"
164 , return [essence| &b subset &a |]
165 )
166 theRule _ = na "rule_Supset"
167
168
169 rule_SupsetEq :: Rule
170 rule_SupsetEq = "mset-subsetEq" `namedRule` theRule where
171 theRule [essence| &a supsetEq &b |] = do
172 TypeMSet{} <- typeOf a
173 TypeMSet{} <- typeOf b
174 return
175 ( "Horizontal rule for mset supsetEq"
176 , return [essence| &b subsetEq &a |]
177 )
178 theRule _ = na "rule_SupsetEq"
179
180
181 rule_MaxMin :: Rule
182 rule_MaxMin = "mset-max-min" `namedRule` theRule where
183 theRule [essence| max(&s) |] = do
184 TypeMSet (TypeInt _) <- typeOf s
185 return
186 ( "Horizontal rule for mset max"
187 , case () of
188 _ | Just (_, xs) <- match msetLiteral s, length xs > 0 -> return $ make opMax $ fromList xs
189 _ -> do
190 (iPat, i) <- quantifiedVar
191 return [essence| max([&i | &iPat <- &s]) |]
192 )
193 theRule [essence| min(&s) |] = do
194 TypeMSet (TypeInt _) <- typeOf s
195 return
196 ( "Horizontal rule for mset min"
197 , case () of
198 _ | Just (_, xs) <- match msetLiteral s, length xs > 0 -> return $ make opMin $ fromList xs
199 _ -> do
200 (iPat, i) <- quantifiedVar
201 return [essence| min([&i | &iPat <- &s]) |]
202 )
203 theRule _ = na "rule_MaxMin"
204
205
206 -- freq(mset,arg) ~~> sum([ toInt(arg = i) | i in mset ])
207 rule_Freq :: Rule
208 rule_Freq = "mset-freq" `namedRule` theRule where
209 theRule p = do
210 (mset, arg) <- match opFreq p
211 case match opToMSet mset >>= match opFlatten of
212 Nothing -> return ()
213 Just{} -> na "There is a better rule for this: rule_Freq_toMSet_Flatten"
214 TypeMSet{} <- typeOf mset
215 -- avoid applying this rule when "mset" is of the form "toMSet of set"
216 case mset of
217 [essence| toMSet(&s) |] -> do
218 tyS <- typeOf s
219 case tyS of
220 TypeSet{} -> na "rule_Freq"
221 _ -> return ()
222 _ -> return ()
223 return
224 ( "Horizontal rule for mset-freq."
225 , do
226 (iPat, i) <- quantifiedVar
227 return [essence| sum &iPat in &mset . toInt(&i = &arg) |]
228 )
229
230
231 -- x in s ~~> or([ x = i | i in s ])
232 rule_In :: Rule
233 rule_In = "mset-in" `namedRule` theRule where
234 theRule p = do
235 (x,s) <- match opIn p
236 TypeMSet{} <- typeOf s
237 return
238 ( "Horizontal rule for mset-in."
239 , do
240 (iPat, i) <- quantifiedVar
241 return [essence| exists &iPat in &s . &i = &x |]
242 )
243
244
245 rule_Card :: Rule
246 rule_Card = "mset-card" `namedRule` theRule where
247 theRule p = do
248 s <- match opTwoBars p
249 TypeMSet{} <- typeOf s
250 return
251 ( "Horizontal rule for mset cardinality."
252 , do
253 (iPat, _) <- quantifiedVar
254 return [essence| sum &iPat in &s . 1 |]
255 )