never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Horizontal.Relation where
4
5 import Conjure.Rules.Import
6
7
8 rule_Comprehension_Literal :: Rule
9 rule_Comprehension_Literal = "relation-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, matchDefs [opToSet,opToMSet,opToRelation] expr)
13 _ -> na "rule_Comprehension_Literal"
14 (TypeRelation taus, elems) <- match relationLiteral expr
15 let outLiteral = make matrixLiteral
16 (TypeMatrix (TypeInt TagInt) (TypeTuple taus))
17 (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength elems))])
18 [ AbstractLiteral (AbsLitTuple row)
19 | row <- elems
20 ]
21 let upd val old = lambdaToFunction pat old val
22 return
23 ( "Comprehension on relation 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_Literal"
32
33
34 -- [ body | i <- rel(...) ]
35 -- [ body | jPat <- rel(...), j = ]
36 rule_Comprehension_Projection :: Rule
37 rule_Comprehension_Projection = "relation-comprehension-projection" `namedRule` theRule where
38 theRule (Comprehension body gensOrConds) = do
39 (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
40 Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDef opToSet expr)
41 _ -> na "rule_Comprehension_Projection"
42 (rel, args) <- match opRelationProj expr
43 TypeRelation{} <- typeOf rel
44 let upd val old = lambdaToFunction pat old val
45 return
46 ( "Comprehension on relation literals"
47 , do
48 (jPat, j) <- quantifiedVar
49 -- those indices to keep
50 let val = AbstractLiteral $ AbsLitTuple
51 [ [essence| &j[&iExpr] |]
52 | (i, Nothing) <- zip allNats args
53 , let iExpr = fromInt i
54 ]
55 let conditions =
56 [ Condition [essence| &j[&iExpr] = &arg |]
57 | (i, Just arg) <- zip allNats args
58 , let iExpr = fromInt i
59 ]
60 return $ Comprehension
61 (upd val body)
62 $ gocBefore
63 ++ [Generator (GenInExpr jPat rel)]
64 ++ conditions
65 ++ transformBi (upd val) gocAfter
66 )
67 theRule _ = na "rule_Comprehension_Projection"
68
69
70 rule_PowerSet_Comprehension :: Rule
71 rule_PowerSet_Comprehension = "relation-powerSet-comprehension" `namedRule` theRule where
72 theRule (Comprehension body gensOrConds) = do
73 (gocBefore, (setPat, setPatNum, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
74 Generator (GenInExpr setPat@(AbsPatSet pats) expr) -> return (setPat, length pats, expr)
75 _ -> na "rule_PowerSet_Comprehension"
76 let upd val old = lambdaToFunction setPat old val
77 rel <- match opPowerSet expr
78 TypeRelation{} <- typeOf rel
79 return
80 ( "Horizontal rule for powerSet relation-comprehension"
81 , do
82 outPats <- replicateM setPatNum quantifiedVar
83 let val = AbstractLiteral $ AbsLitSet [ j | (_,j) <- outPats ]
84 return $
85 Comprehension (upd val body) $ concat
86 [ gocBefore
87 , concat
88 [ [ Generator (GenInExpr pat rel) ]
89 | (pat,_) <- take 1 outPats
90 ]
91 , concat
92 [ [ Generator (GenInExpr pat rel)
93 , Condition [essence| &beforeX < &patX |]
94 ]
95 | ((_, beforeX), (pat, patX)) <- zip outPats (tail outPats)
96 ]
97 , transformBi (upd val) gocAfter
98 ]
99 )
100 theRule _ = na "rule_PowerSet_Comprehension"
101
102
103 rule_Eq :: Rule
104 rule_Eq = "relation-eq" `namedRule` theRule where
105 theRule p = do
106 (x,y) <- match opEq p
107 TypeRelation{} <- typeOf x
108 TypeRelation{} <- typeOf y
109 return
110 ( "Horizontal rule for relation equality"
111 , do
112 (iPat, i) <- quantifiedVar
113 return
114 [essence|
115 (forAll &iPat in &x . &i in &y)
116 /\
117 (forAll &iPat in &y . &i in &x)
118 /\
119 (|&x| = |&y|)
120 |]
121 )
122
123
124 rule_Neq :: Rule
125 rule_Neq = "relation-neq" `namedRule` theRule where
126 theRule [essence| &x != &y |] = do
127 TypeRelation{} <- typeOf x
128 TypeRelation{} <- typeOf y
129 return
130 ( "Horizontal rule for relation dis-equality"
131 , do
132 (iPat, i) <- quantifiedVar
133 return
134 [essence|
135 (exists &iPat in &x . !(&i in &y))
136 \/
137 (exists &iPat in &y . !(&i in &x))
138 |]
139 )
140 theRule _ = na "rule_Neq"
141
142
143 rule_SubsetEq :: Rule
144 rule_SubsetEq = "relation-subsetEq" `namedRule` theRule where
145 theRule [essence| &x subsetEq &y |] = do
146 TypeRelation{} <- typeOf x
147 TypeRelation{} <- typeOf y
148 return
149 ( "Horizontal rule for relation subsetEq"
150 , do
151 (iPat, i) <- quantifiedVar
152 return [essence| forAll &iPat in (&x) . &i in &y |]
153 )
154 theRule _ = na "rule_SubsetEq"
155
156
157 rule_Subset :: Rule
158 rule_Subset = "relation-subset" `namedRule` theRule where
159 theRule [essence| &a subset &b |] = do
160 TypeRelation{} <- typeOf a
161 TypeRelation{} <- typeOf b
162 return
163 ( "Horizontal rule for relation subset"
164 , return [essence| &a subsetEq &b /\ &a != &b |]
165 )
166 theRule _ = na "rule_Subset"
167
168
169 rule_Supset :: Rule
170 rule_Supset = "relation-supset" `namedRule` theRule where
171 theRule [essence| &a supset &b |] = do
172 TypeRelation{} <- typeOf a
173 TypeRelation{} <- typeOf b
174 return
175 ( "Horizontal rule for relation supset"
176 , return [essence| &b subset &a |]
177 )
178 theRule _ = na "rule_Supset"
179
180
181 rule_SupsetEq :: Rule
182 rule_SupsetEq = "relation-subsetEq" `namedRule` theRule where
183 theRule [essence| &a supsetEq &b |] = do
184 TypeRelation{} <- typeOf a
185 TypeRelation{} <- typeOf b
186 return
187 ( "Horizontal rule for relation supsetEq"
188 , return [essence| &b subsetEq &a |]
189 )
190 theRule _ = na "rule_SupsetEq"
191
192
193 rule_Image :: Rule
194 rule_Image = "relation-image" `namedRule` theRule where
195 theRule p = do
196 (rel, args) <- match opRelationImage p
197 TypeRelation{} <- typeOf rel
198 let arg = AbstractLiteral (AbsLitTuple args)
199 return
200 ( "relation image to relation membership"
201 , return [essence| &arg in &rel |]
202 )
203
204
205 rule_In :: Rule
206 rule_In = "relation-in" `namedRule` theRule where
207 theRule [essence| &x in &rel |] = do
208 TypeRelation{} <- typeOf rel
209 return
210 ( "relation membership to existential quantification"
211 , do
212 (iPat, i) <- quantifiedVar
213 return [essence| exists &iPat in toSet(&rel) . &i = &x |]
214 )
215 theRule _ = na "rule_In"
216
217
218 rule_Card :: Rule
219 rule_Card = "relation-cardinality" `namedRule` theRule where
220 theRule [essence| |&x| |] = do
221 TypeRelation{} <- typeOf x
222 return
223 ( "Relation cardinality"
224 , return [essence| |toSet(&x)| |]
225 )
226 theRule _ = na "rule_Card"
227
228
229 rule_Param_Card :: Rule
230 rule_Param_Card = "param-card-of-relation" `namedRule` theRule where
231 theRule [essence| |&x| |] = do
232 TypeRelation _ <- typeOf x
233 unless (categoryOf x == CatParameter) $ na "rule_Param_Card"
234 DomainRelation _ (RelationAttr (SizeAttr_Size n) _) _ <- domainOf x
235 return
236 ( "cardinality of a parameter relation"
237 , return n
238 )
239 theRule _ = na "rule_Param_Card"