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 rule_Comprehension_ToSet_Literal :: Rule
33 rule_Comprehension_ToSet_Literal = "mset-comprehension-toSet-literal" `namedRule` theRule where
34 theRule (Comprehension body gensOrConds) = do
35 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
36 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
37 _ -> na "rule_Comprehension_ToSet_Literal"
38 mset <- match opToSet expr
39 (TypeMSet tau, elems) <- match msetLiteral mset
40 let outLiteralDomain = mkDomainIntB 1 (fromInt $ genericLength elems)
41 let outLiteral = make matrixLiteral (TypeMatrix (TypeInt TagInt) tau) outLiteralDomain elems
42 let upd val old = lambdaToFunction pat old val
43 return
44 ( "Comprehension on toSet of mset literals"
45 , do
46 (iPat, i) <- quantifiedVar
47 (jPat, j) <- quantifiedVar
48 let iIndexed = [essence| &outLiteral[&i] |]
49 let jIndexed = [essence| &outLiteral[&j] |]
50 return $ Comprehension (upd iIndexed body)
51 $ gocBefore
52 ++ [ Generator (GenDomainNoRepr iPat outLiteralDomain)
53 , Condition [essence|
54 !(exists &jPat : &outLiteralDomain .
55 (&j < &i) /\ (&iIndexed = &jIndexed))
56 |]
57 ]
58 ++ transformBi (upd iIndexed) gocAfter
59 )
60 theRule _ = na "rule_Comprehension_ToSet_Literal"
61
62
63 rule_Eq :: Rule
64 rule_Eq = "mset-eq" `namedRule` theRule where
65 theRule p = do
66 (x,y) <- match opEq p
67 TypeMSet{} <- typeOf x
68 TypeMSet{} <- typeOf y
69 return
70 ( "Horizontal rule for mset equality"
71 , do
72 (iPat, i) <- quantifiedVar
73 return
74 [essence|
75 (forAll &iPat in &x . freq(&x,&i) = freq(&y,&i)) /\
76 (forAll &iPat in &y . freq(&x,&i) = freq(&y,&i))
77 |]
78 )
79
80
81 rule_Neq :: Rule
82 rule_Neq = "mset-neq" `namedRule` theRule where
83 theRule [essence| &x != &y |] = do
84 TypeMSet{} <- typeOf x
85 TypeMSet{} <- typeOf y
86 return
87 ( "Horizontal rule for mset dis-equality"
88 , do
89 (iPat, i) <- quantifiedVar
90 return
91 [essence|
92 (exists &iPat in &x . freq(&x,&i) != freq(&y,&i)) \/
93 (exists &iPat in &y . freq(&x,&i) != freq(&y,&i))
94 |]
95 )
96 theRule _ = na "rule_Neq"
97
98
99 rule_SubsetEq :: Rule
100 rule_SubsetEq = "mset-subsetEq" `namedRule` theRule where
101 theRule p = do
102 (x,y) <- match opSubsetEq p
103 TypeMSet{} <- typeOf x
104 TypeMSet{} <- typeOf y
105 return
106 ( "Horizontal rule for mset subsetEq"
107 , do
108 (iPat, i) <- quantifiedVar
109 return [essence| forAll &iPat in &x . freq(&x,&i) <= freq(&y,&i) |]
110 )
111
112
113 rule_Subset :: Rule
114 rule_Subset = "mset-subset" `namedRule` theRule where
115 theRule [essence| &x subset &y |] = do
116 TypeMSet{} <- typeOf x
117 TypeMSet{} <- typeOf y
118 return
119 ( "Horizontal rule for mset subset"
120 , do
121 (iPat, i) <- quantifiedVar
122 return
123 [essence|
124 (forAll &iPat in &x . freq(&x,&i) <= freq(&y,&i)) /\
125 (exists &iPat in &x . freq(&x,&i) < freq(&y,&i))
126 |]
127 )
128 theRule _ = na "rule_Subset"
129
130
131 rule_Supset :: Rule
132 rule_Supset = "mset-supset" `namedRule` theRule where
133 theRule [essence| &a supset &b |] = do
134 TypeMSet{} <- typeOf a
135 TypeMSet{} <- typeOf b
136 return
137 ( "Horizontal rule for mset supset"
138 , return [essence| &b subset &a |]
139 )
140 theRule _ = na "rule_Supset"
141
142
143 rule_SupsetEq :: Rule
144 rule_SupsetEq = "mset-subsetEq" `namedRule` theRule where
145 theRule [essence| &a supsetEq &b |] = do
146 TypeMSet{} <- typeOf a
147 TypeMSet{} <- typeOf b
148 return
149 ( "Horizontal rule for mset supsetEq"
150 , return [essence| &b subsetEq &a |]
151 )
152 theRule _ = na "rule_SupsetEq"
153
154
155 rule_MaxMin :: Rule
156 rule_MaxMin = "mset-max-min" `namedRule` theRule where
157 theRule [essence| max(&s) |] = do
158 TypeMSet (TypeInt _) <- typeOf s
159 return
160 ( "Horizontal rule for mset max"
161 , case () of
162 _ | Just (_, xs) <- match msetLiteral s, length xs > 0 -> return $ make opMax $ fromList xs
163 _ -> do
164 (iPat, i) <- quantifiedVar
165 return [essence| max([&i | &iPat <- &s]) |]
166 )
167 theRule [essence| min(&s) |] = do
168 TypeMSet (TypeInt _) <- typeOf s
169 return
170 ( "Horizontal rule for mset min"
171 , case () of
172 _ | Just (_, xs) <- match msetLiteral s, length xs > 0 -> return $ make opMin $ fromList xs
173 _ -> do
174 (iPat, i) <- quantifiedVar
175 return [essence| min([&i | &iPat <- &s]) |]
176 )
177 theRule _ = na "rule_MaxMin"
178
179
180 -- freq(mset,arg) ~~> sum([ toInt(arg = i) | i in mset ])
181 rule_Freq :: Rule
182 rule_Freq = "mset-freq" `namedRule` theRule where
183 theRule p = do
184 (mset, arg) <- match opFreq p
185 TypeMSet{} <- typeOf mset
186 -- avoid applying this rule when "mset" is of the form "toMSet of set"
187 case mset of
188 [essence| toMSet(&s) |] -> do
189 tyS <- typeOf s
190 case tyS of
191 TypeSet{} -> na "rule_Freq"
192 _ -> return ()
193 _ -> return ()
194 return
195 ( "Horizontal rule for mset-freq."
196 , do
197 (iPat, i) <- quantifiedVar
198 return [essence| sum &iPat in &mset . toInt(&i = &arg) |]
199 )
200
201
202 -- x in s ~~> or([ x = i | i in s ])
203 rule_In :: Rule
204 rule_In = "mset-in" `namedRule` theRule where
205 theRule p = do
206 (x,s) <- match opIn p
207 TypeMSet{} <- typeOf s
208 return
209 ( "Horizontal rule for mset-in."
210 , do
211 (iPat, i) <- quantifiedVar
212 return [essence| exists &iPat in &s . &i = &x |]
213 )
214
215
216 rule_Card :: Rule
217 rule_Card = "mset-card" `namedRule` theRule where
218 theRule p = do
219 s <- match opTwoBars p
220 TypeMSet{} <- typeOf s
221 return
222 ( "Horizontal rule for mset cardinality."
223 , do
224 (iPat, _) <- quantifiedVar
225 return [essence| sum &iPat in &s . 1 |]
226 )