never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Horizontal.Permutation where
4
5 import Conjure.Rules.Import
6 import Conjure.Util.Permutation (fromCycles, size, toCycles, toFunction)
7
8 rule_Cardinality_Literal :: Rule
9 rule_Cardinality_Literal = "permutation-cardinality-literal" `namedRule` theRule
10 where
11 theRule p' = do
12 p <- match opTwoBars p'
13 (TypePermutation _, elems) <- match permutationLiteral p
14 let i' = Constant . ConstantInt TagInt . fromIntegral . size <$> fromCycles elems
15 case i' of
16 Left er -> failDoc $ "Permutation literal invalid." <++> stringToDoc (show er)
17 Right i ->
18 return
19 ( "Horizontal rule for permutation cardinality, AsFunction representation.",
20 do
21 return [essence| &i |]
22 )
23
24 rule_Defined_Literal :: Rule
25 rule_Defined_Literal = "permutation-defined-literal" `namedRule` theRule
26 where
27 theRule p' = do
28 p <- match opDefined p'
29 (TypePermutation _, elems) <- match permutationLiteral p
30 let i' = AbstractLiteral . AbsLitSet . nub . join . toCycles <$> fromCycles elems
31 case i' of
32 Left er -> failDoc $ "Permutation literal invalid." <++> stringToDoc (show er)
33 Right i ->
34 return
35 ( "Horizontal rule for permutation defined, AsFunction representation.",
36 do
37 return [essence| &i |]
38 )
39
40 rule_Equality :: Rule
41 rule_Equality = "permutation-equality" `namedRule` theRule
42 where
43 theRule e = do
44 (p, q) <- match opEq e
45 TypePermutation {} <- typeOf p
46 TypePermutation {} <- typeOf q
47 return
48 ( "Horizontal rule for permutation equality",
49 return [essence| toSet(&p) = toSet(&q) |]
50 )
51
52 rule_Disequality :: Rule
53 rule_Disequality = "permutation-disequality" `namedRule` theRule
54 where
55 theRule e = do
56 (p, q) <- match opNeq e
57 TypePermutation {} <- typeOf p
58 TypePermutation {} <- typeOf q
59 return
60 ( "Horizontal rule for permutation disequality",
61 return [essence| toSet(&p) != toSet(&q) |]
62 )
63
64 rule_Comprehension :: Rule
65 rule_Comprehension = "permutation-comprehension" `namedRule` theRule
66 where
67 theRule (Comprehension body gensOrConds) = do
68 (gocBefore, (pat, perm), gocAfter) <- matchFirst gensOrConds $ \case
69 Generator (GenInExpr pat expr) -> return (pat, matchDefs [opToSet] expr)
70 _ -> na "rule_Comprehension"
71 (TypePermutation inner, elems) <- match permutationLiteral perm
72 DomainPermutation _ _ innerD <- domainOf perm
73 let f' = toFunction <$> fromCycles elems
74 case f' of
75 Left er -> failDoc $ "Permutation literal invalid." <++> stringToDoc (show er)
76 Right f -> do
77 let outLiteral =
78 make
79 matrixLiteral
80 (TypeMatrix (TypeInt TagInt) (TypeTuple [inner, inner]))
81 innerD
82 [ AbstractLiteral
83 ( AbsLitTuple
84 [ de,
85 f de
86 ]
87 )
88 | de <- join elems
89 ]
90 return
91 ( "Horizontal rule for permutation-comprehension",
92 do
93 return
94 $ Comprehension body
95 $ gocBefore
96 ++ [ Generator (GenInExpr pat [essence| &outLiteral|])
97 ]
98 ++ gocAfter
99 )
100 theRule _ = na "rule_Comprehension"
101
102 rule_In :: Rule
103 rule_In = "permutation-in" `namedRule` theRule
104 where
105 theRule p = do
106 (x, s) <- match opIn p
107 TypePermutation {} <- typeOf s
108 -- do not apply this rule to quantified variables
109 -- or else we might miss the opportunity to apply a more specific vertical rule
110 when (referenceToComprehensionVar s) $ na "rule_In"
111 return
112 ( "Horizontal rule for permutation-in.",
113 do
114 (iPat, i) <- quantifiedVar
115 return [essence| exists &iPat in &s . &i = &x |]
116 )
117
118 rule_Permutation_Inverse :: Rule
119 rule_Permutation_Inverse = "permutation-inverse" `namedRule` theRule
120 where
121 theRule [essence| inverse(&p1, &p2)|] = do
122 TypePermutation {} <- typeOf p1
123 TypePermutation {} <- typeOf p2
124 return
125 ( "Horizontal rule for permutation-inverse",
126 do
127 (iPat, i) <- quantifiedVar
128 return
129 [essence|
130 (forAll &iPat in &p1 . image(&p2,&i[2]) = &i[1])
131 /\
132 (forAll &iPat in &p2 . image(&p1,&i[2]) = &i[1])
133 |]
134 )
135 theRule _ = na "rule_Permutation_Inverse"
136
137 rule_Compose_Image :: Rule
138 rule_Compose_Image = "permutation-compose-image" `namedRule` theRule
139 where
140 theRule [essence| image(compose(&g, &h),&i) |] = do
141 TypePermutation innerG <- typeOf g
142 TypePermutation innerH <- typeOf g
143 typeI <- typeOf i
144 if let ?typeCheckerMode = StronglyTyped in typesUnify [innerG, innerH, typeI]
145 then
146 return
147 ( "Horizontal rule for image of permutation composition",
148 do
149 return [essence| image(&g, image(&h,&i)) |]
150 )
151 else na "rule_Compose_Image"
152 theRule _ = na "rule_Compose_Image"
153
154 rule_Image_Literal :: Rule
155 rule_Image_Literal = "permutation-image-literal" `namedRule` theRule
156 where
157 theRule [essence| image(&p, &i) |] = do
158 (TypePermutation inner, elems) <- match permutationLiteral p
159 typeI <- typeOf i
160 let f' = toFunction <$> fromCycles elems
161 case f' of
162 Left er -> failDoc $ "Permutation literal invalid." <++> stringToDoc (show er)
163 Right f -> do
164 if let ?typeCheckerMode = StronglyTyped in typesUnify [inner, typeI]
165 then do
166 let srtdel = sort (join elems)
167 indexr =
168 (\x -> [essence| sum(&x) |])
169 ( fromList
170 ( (\(n, q) -> [essence| toInt(&q = &i) * &n |])
171 <$> zip [1 ..] srtdel
172 )
173 )
174 matIdx =
175 mkDomainIntB
176 (fromInt 0)
177 (fromInt (fromIntegral (length srtdel)))
178 matLit =
179 make
180 matrixLiteral
181 (TypeMatrix (TypeInt TagInt) inner)
182 matIdx
183 ([essence| &i |] : (f <$> srtdel))
184 iDomain <- domainOf i
185 minval <- minOfDomain iDomain
186 return
187 ( "Horizontal rule for permutation literal application to a single value (image), AsFunction representation",
188 do
189 return [essence| catchUndef(&matLit[&indexr], &minval) |]
190 )
191 else failDoc "Permutation applied to a type its inner does not unify with"
192 theRule _ = na "rule_Image_Literal"