never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Horizontal.Sequence where
4
5 import Conjure.Rules.Import
6
7
8 rule_Comprehension_Literal :: Rule
9 rule_Comprehension_Literal = "sequence-comprehension-literal" `namedRule` theRule where
10 theRule (Comprehension body gensOrConds) = do
11 (gofBefore, (pat, expr), gofAfter) <- matchFirst gensOrConds $ \ gof -> case gof of
12 Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDefs [opToSet,opToMSet,opToRelation] expr)
13 _ -> na "rule_Comprehension_Literal"
14 (TypeSequence t, elems) <- match sequenceLiteral expr
15 let outLiteral = make matrixLiteral
16 (TypeMatrix (TypeInt TagInt) t)
17 (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength elems))])
18 elems
19 let upd val old = lambdaToFunction pat old val
20 return
21 ( "Comprehension on sequence literals"
22 , do
23 (iPat, i) <- quantifiedVar
24 let val = [essence| (&i, &outLiteral[&i]) |]
25 return $ Comprehension (upd val body)
26 $ gofBefore
27 ++ [Generator (GenDomainNoRepr iPat $ mkDomainIntB 1 (fromInt $ genericLength elems))]
28 ++ transformBi (upd val) gofAfter
29 )
30 theRule _ = na "rule_Comprehension_Literal"
31
32
33 rule_Image_Literal_Bool :: Rule
34 rule_Image_Literal_Bool = "sequence-image-literal-bool" `namedRule` theRule where
35 theRule p = do
36 (func, arg) <- match opImage p
37 (TypeSequence TypeBool, elems) <- match sequenceLiteral func
38 -- let argIsUndef = make opNot $ make opOr $ fromList
39 -- [ [essence| &a = &arg |]
40 -- | (a,_) <- elems
41 -- ]
42 return $
43 if null elems
44 then
45 ( "Image of empty sequence literal"
46 , return [essence| false |] -- undefined is false.
47 )
48 else
49 ( "Image of sequence literal"
50 , return $ make opOr $ fromList
51 [ [essence| (&a = &arg) /\ &b |] -- if this is ever true, the output is true.
52 -- undefined is still false.
53 | (a',b) <- zip allNats elems
54 , let a = fromInt a'
55 ]
56 )
57
58
59 rule_Image_Literal_Int :: Rule
60 rule_Image_Literal_Int = "sequence-image-literal-int" `namedRule` theRule where
61 theRule p = do
62 (func, arg) <- match opImage p
63 (TypeSequence (TypeInt _), elems) <- match sequenceLiteral func
64 return
65 ( "Image of sequence literal"
66 , return $
67 let
68 val = make opSum $ fromList
69 -- if this is ever true, the output is the value of b.
70 [ [essence| toInt(&a = &arg) * &b |]
71 | (a',b) <- zip allNats elems
72 , let a = fromInt a'
73 ]
74 len = fromInt $ genericLength elems
75 argIsDef = [essence| &arg <= &len |]
76 in
77 WithLocals val (DefinednessConstraints [argIsDef])
78 )
79
80
81 rule_Eq_Literal :: Rule
82 rule_Eq_Literal = "sequence-eq-literal" `namedRule` theRule where
83 theRule p = do
84 (x,y) <- match opEq p
85 xTy <- typeOf x
86 yTy <- typeOf y
87 case (xTy, yTy) of
88 (TypeSequence{}, _) -> return ()
89 (_, TypeSequence{}) -> return ()
90 _ -> na "rule_Eq_Literal"
91 (other, vals) <- case ( match sequenceLiteral x, match matrixLiteral x
92 , match sequenceLiteral y, match matrixLiteral y) of
93 (Just (_, vals), _ , _ , _ ) -> return (y, vals)
94 (_ , Just (_, _, vals), _ , _ ) -> return (y, vals)
95 (_ , _ , Just (_, vals), _ ) -> return (x, vals)
96 (_ , _ , _ , Just (_, _, vals)) -> return (x, vals)
97 _ -> na "sequence not empty"
98 return
99 ( "Horizontal rule for sequence equality, one side empty"
100 , do
101 let len = fromInt (genericLength vals)
102 return $ make opAnd $ fromList
103 $ [essence| |&other| = &len |]
104 : [ [essence| &other(&i) = &val |]
105 | (i_, val) <- zip allNats vals
106 , let i = fromInt i_
107 ]
108 )
109
110
111 rule_Eq :: Rule
112 rule_Eq = "sequence-eq" `namedRule` theRule where
113 theRule p = do
114 (x,y) <- match opEq p
115 TypeSequence{} <- typeOf x
116 TypeSequence{} <- typeOf y
117 case (match sequenceLiteral x, match sequenceLiteral y) of
118 (Just (_, []), _) -> na "Sequence{rule_Eq}: one side empty"
119 (_, Just (_, [])) -> na "Sequence{rule_Eq}: one side empty"
120 _ -> return ()
121 return
122 ( "Horizontal rule for sequence equality"
123 , do
124 (iPat, i) <- quantifiedVar
125 return
126 [essence|
127 (forAll &iPat in &x . &y(&i[1]) = &i[2])
128 /\
129 (forAll &iPat in &y . &x(&i[1]) = &i[2])
130 /\
131 defined(&x) = defined(&y)
132 |]
133 )
134
135
136 rule_Eq_Comprehension :: Rule
137 rule_Eq_Comprehension = "sequence-eq-comprehension" `namedRule` theRule where
138 theRule p = do
139 (x, y@(Comprehension _ goc)) <- do
140 (x,y) <- match opEq p
141 case x of
142 Comprehension{} -> return (y, x) -- swap if x is a Comprehension
143 _ -> return (x, y)
144 TypeSequence{} <- typeOf x
145 return
146 ( "Horizontal rule for sequence equality, with a comprehension on the rhs"
147 , do
148 (iPat, i) <- quantifiedVar
149 let cardinality = Comprehension 1 goc
150 return
151 [essence|
152 |&x| = sum(&cardinality) /\
153 and([ &y[&i[1]] = &i[2]
154 | &iPat <- &x
155 ])
156 |]
157 )
158
159
160 rule_Neq :: Rule
161 rule_Neq = "sequence-neq" `namedRule` theRule where
162 theRule [essence| &x != &y |] = do
163 TypeSequence{} <- typeOf x
164 TypeSequence{} <- typeOf y
165 return
166 ( "Horizontal rule for sequence dis-equality"
167 , do
168 (iPat, i) <- quantifiedVar
169 return
170 [essence|
171 (exists &iPat in &x . !(&i in &y))
172 \/
173 (exists &iPat in &y . !(&i in &x))
174 |]
175 )
176 theRule _ = na "rule_Neq"
177
178
179 rule_SubsetEq :: Rule
180 rule_SubsetEq = "sequence-subsetEq" `namedRule` theRule where
181 theRule p = do
182 (x,y) <- match opSubsetEq p
183 TypeSequence{} <- typeOf x
184 TypeSequence{} <- typeOf y
185 return
186 ( "Horizontal rule for sequence subsetEq"
187 , do
188 (iPat, i) <- quantifiedVar
189 return
190 [essence|
191 (forAll &iPat in &x . &y(&i[1]) = &i[2])
192 /\
193 defined(&x) subsetEq defined(&y)
194 |]
195 )
196
197
198 rule_Subset :: Rule
199 rule_Subset = "sequence-subset" `namedRule` theRule where
200 theRule [essence| &a subset &b |] = do
201 TypeSequence{} <- typeOf a
202 TypeSequence{} <- typeOf b
203 return
204 ( "Horizontal rule for sequence subset"
205 , return [essence| &a subsetEq &b /\ &a != &b |]
206 )
207 theRule _ = na "rule_Subset"
208
209
210 rule_Supset :: Rule
211 rule_Supset = "sequence-supset" `namedRule` theRule where
212 theRule [essence| &a supset &b |] = do
213 TypeSequence{} <- typeOf a
214 TypeSequence{} <- typeOf b
215 return
216 ( "Horizontal rule for sequence supset"
217 , return [essence| &b subset &a |]
218 )
219 theRule _ = na "rule_Supset"
220
221
222 rule_SupsetEq :: Rule
223 rule_SupsetEq = "sequence-subsetEq" `namedRule` theRule where
224 theRule [essence| &a supsetEq &b |] = do
225 TypeSequence{} <- typeOf a
226 TypeSequence{} <- typeOf b
227 return
228 ( "Horizontal rule for sequence supsetEq"
229 , return [essence| &b subsetEq &a |]
230 )
231 theRule _ = na "rule_SupsetEq"
232
233
234 rule_Comprehension_PreImage :: Rule
235 rule_Comprehension_PreImage = "sequence-preImage" `namedRule` theRule where
236 theRule (Comprehension body gensOrConds) = do
237 (gofBefore, (pat, expr), gofAfter) <- matchFirst gensOrConds $ \ gof -> case gof of
238 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
239 _ -> na "rule_Comprehension_PreImage"
240 (func, img) <- match opPreImage expr
241 TypeSequence{} <- typeOf func
242 let upd val old = lambdaToFunction pat old val
243 return
244 ( "Mapping over the preImage of a sequence"
245 , do
246 (jPat, j) <- quantifiedVar
247 let val = [essence| &j[1] |]
248 return $ Comprehension
249 (upd val body)
250 $ gofBefore
251 ++ [ Generator (GenInExpr jPat func)
252 , Condition [essence| &j[2] = &img |]
253 ]
254 ++ transformBi (upd val) gofAfter
255 )
256 theRule _ = na "rule_Comprehension_PreImage"
257
258
259 rule_Card :: Rule
260 rule_Card = "sequence-cardinality" `namedRule` theRule where
261 theRule [essence| |&s| |] = do
262 TypeSequence{} <- typeOf s
263 dom <- domainOf s
264 return
265 ( "Horizontal rule for sequence cardinality."
266 , case dom of
267 DomainSequence _ (SequenceAttr (SizeAttr_Size n) _) _
268 -> return n
269 DomainSequence _ (SequenceAttr _ jectivity) inner
270 | jectivity `elem` [JectivityAttr_Surjective, JectivityAttr_Bijective]
271 -> domainSizeOf inner
272 _ -> do
273 (iPat, _) <- quantifiedVar
274 return [essence| sum &iPat in &s . 1 |]
275 )
276 theRule _ = na "rule_Card"
277
278
279 rule_Comprehension_Defined :: Rule
280 rule_Comprehension_Defined = "sequence-defined" `namedRule` theRule where
281 theRule (Comprehension body gensOrConds) = do
282 (gofBefore, (pat, expr), gofAfter) <- matchFirst gensOrConds $ \ gof -> case gof of
283 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
284 _ -> na "rule_Comprehension_Defined"
285 s <- match opDefined expr
286 DomainSequence _ (SequenceAttr sizeAttr _) _ <- domainOf s
287 maxSize <- case sizeAttr of
288 SizeAttr_Size x -> return x
289 SizeAttr_MaxSize x -> return x
290 SizeAttr_MinMaxSize _ x -> return x
291 _ -> failDoc "rule_Comprehension_Defined maxSize"
292 let upd val old = lambdaToFunction pat old val
293 return
294 ( "Mapping over defined(f)"
295 , do
296 (jPat, j) <- quantifiedVar
297 let val = j
298 return $ Comprehension
299 (upd val body)
300 $ gofBefore
301 ++ [ Generator (GenDomainNoRepr jPat $ mkDomainIntB 1 maxSize)
302 , Condition [essence| &j <= |&s| |]
303 ]
304 ++ transformBi (upd val) gofAfter
305 )
306 theRule _ = na "rule_Comprehension_Defined"
307
308
309 -- | TODO: This may allow repetitions.
310 rule_Comprehension_Range :: Rule
311 rule_Comprehension_Range = "sequence-range" `namedRule` theRule where
312 theRule (Comprehension body gensOrConds) = do
313 (gofBefore, (pat, expr), gofAfter) <- matchFirst gensOrConds $ \ gof -> case gof of
314 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
315 _ -> na "rule_Comprehension_PreImage"
316 func <- match opRange expr
317 TypeSequence{} <- typeOf func
318 let upd val old = lambdaToFunction pat old val
319 return
320 ( "Mapping over range(f)"
321 , do
322 (jPat, j) <- quantifiedVar
323 let val = [essence| &j[2] |]
324 return $ Comprehension
325 (upd val body)
326 $ gofBefore
327 ++ [ Generator (GenInExpr jPat func) ]
328 ++ transformBi (upd val) gofAfter
329 )
330 theRule _ = na "rule_Comprehension_Range"
331
332
333 rule_In :: Rule
334 rule_In = "sequence-in" `namedRule` theRule where
335 theRule [essence| &x in &f |] = do
336 TypeSequence{} <- typeOf f
337 return
338 ( "Sequence membership to sequence image."
339 , return [essence| &f(&x[1]) = &x[2] |]
340 )
341 theRule _ = na "rule_In"
342
343
344 rule_Restrict_Image :: Rule
345 rule_Restrict_Image = "sequence-restrict-image" `namedRule` theRule where
346 theRule p = do
347 (func', arg) <- match opImage p
348 (func , dom) <- match opRestrict func'
349 TypeSequence{} <- typeOf func
350 return
351 ( "Sequence image on a restricted sequence."
352 , do
353 (iPat, i) <- quantifiedVar
354 let bob = [essence| exists &iPat : &dom . &i = &arg |]
355 return $ WithLocals (make opImage func arg) (DefinednessConstraints [bob])
356 )
357
358
359 rule_Restrict_Comprehension :: Rule
360 rule_Restrict_Comprehension = "sequence-restrict-comprehension" `namedRule` theRule where
361 theRule (Comprehension body gensOrConds) = do
362 (gofBefore, (iPat, iPatName, expr), gofAfter) <- matchFirst gensOrConds $ \ gof -> case gof of
363 Generator (GenInExpr iPat@(Single iPatName) expr) -> return (iPat, iPatName, expr)
364 _ -> na "rule_Comprehension_PreImage"
365 (func, dom) <- match opRestrict expr
366 TypeSequence{} <- typeOf func
367 return
368 ( "Mapping over restrict(func, dom)"
369 , do
370 (jPat, j) <- quantifiedVar
371 let i = Reference iPatName Nothing
372 return $ Comprehension body
373 $ gofBefore
374 ++ [ Generator (GenInExpr iPat func)
375 , Condition [essence| exists &jPat : &dom . &j = &i[1] |]
376 ]
377 ++ gofAfter
378 )
379 theRule _ = na "rule_Restrict_Comprehension"
380
381
382
383 rule_Image_Bool :: Rule
384 rule_Image_Bool = "sequence-image-bool" `namedRule` theRule where
385 theRule Reference{} = na "rule_Image_Bool"
386 theRule p = do
387 let
388 onChildren
389 :: MonadState (Maybe (Expression, Expression)) m
390 => Expression
391 -> m (Expression -> Expression)
392 onChildren ch = do
393 let
394 try = do
395 (func, arg) <- match opImage ch
396 case match opRestrict func of
397 Nothing -> return ()
398 Just{} -> na "rule_Image_Bool" -- do not use this rule for restricted sequences
399 case match opTransform func of
400 Nothing -> na "rule_Image_Bool" -- only use this rule for transformed sequences
401 Just{} -> return ()
402 TypeSequence TypeBool <- typeOf func
403 return (func, arg)
404 case try of
405 Nothing -> return (const ch) -- do not failDoc if a child is not of proper form
406 Just (func, arg) -> do -- just return it back unchanged
407 seenBefore <- gets id
408 case seenBefore of
409 Nothing -> do
410 modify $ const $ Just (func, arg)
411 return id
412 Just{} ->
413 return (const ch)
414
415 let (children_, gen) = uniplate p
416 (genChildren, mFunc) <- runStateT (mapM onChildren children_) Nothing
417 let
418 mkP :: Expression -> Expression
419 mkP new = gen $ fmap ($ new) genChildren
420 (func, arg) <- maybe (na "rule_Image_Bool") return mFunc -- Nothing signifies no relevant children
421 return
422 ( "Sequence image, bool."
423 , do
424 (iPat, i) <- quantifiedVar
425 return $ mkP $ make opOr $ Comprehension [essence| &i[2] |]
426 [ Generator (GenInExpr iPat func)
427 , Condition [essence| &i[1] = &arg |]
428 ]
429 )
430
431
432 rule_Image_Int :: Rule
433 rule_Image_Int = "sequence-image-int" `namedRule` theRule where
434 theRule Reference{} = na "rule_Image_Int"
435 theRule p = do
436 let
437 onChildren
438 :: MonadState (Maybe (Expression, Expression)) m
439 => Expression
440 -> m (Expression -> Expression)
441 onChildren ch = do
442 let
443 try = do
444 (func, arg) <- match opImage ch
445 case match opRestrict func of
446 Nothing -> return ()
447 Just{} -> na "rule_Image_Int" -- do not use this rule for restricted sequences
448 case match opTransform func of
449 Nothing -> na "rule_Image_Int" -- only use this rule for transformed sequences
450 Just{} -> return ()
451 TypeSequence (TypeInt _) <- typeOf func
452 return (func, arg)
453 case try of
454 Nothing -> return (const ch) -- do not failDoc if a child is not of proper form
455 Just (func, arg) -> do -- just return it back unchanged
456 seenBefore <- gets id
457 case seenBefore of
458 Nothing -> do
459 modify $ const $ Just (func, arg)
460 return id
461 Just{} ->
462 return (const ch)
463
464 let (children_, gen) = uniplate p
465 (genChildren, mFunc) <- runStateT (mapM onChildren children_) Nothing
466 let
467 mkP :: Expression -> Expression
468 mkP new = gen $ fmap ($ new) genChildren
469 (func, arg) <- maybe (na "rule_Image_Int") return mFunc -- Nothing signifies no relevant children
470 return
471 ( "Sequence image, int."
472 , do
473 (iPat, i) <- quantifiedVar
474 let val = make opSum $ Comprehension [essence| &i[2] |]
475 [ Generator (GenInExpr iPat func)
476 , Condition [essence| &i[1] = &arg |]
477 ]
478 isDefined = [essence| &arg in defined(&func) |]
479 return $ mkP $ WithLocals val (DefinednessConstraints [isDefined])
480 )
481
482
483 rule_Comprehension_Image :: Rule
484 rule_Comprehension_Image = "sequence-image-comprehension" `namedRule` theRule where
485 theRule (Comprehension body gensOrConds) = do
486 (gofBefore, (pat, expr), gofAfter) <- matchFirst gensOrConds $ \ gof -> case gof of
487 Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
488 _ -> na "rule_Comprehension_Image"
489 (mkModifier, expr2) <- match opModifier expr
490 (func, arg) <- match opImage expr2
491 TypeSequence{} <- typeOf func
492 case match opRestrict func of
493 Nothing -> return ()
494 Just{} -> na "rule_Image_Bool" -- do not use this rule for restricted sequences
495 let upd val old = lambdaToFunction pat old val
496 return
497 ( "Mapping over the image of a sequence"
498 , do
499 (iPat, i) <- quantifiedVar
500 (jPat, j) <- quantifiedVar
501 return $ Comprehension
502 (upd j body)
503 $ gofBefore
504 ++ [ Generator (GenInExpr iPat (mkModifier func))
505 , Condition [essence| &i[1] = &arg |]
506 , Generator (GenInExpr jPat [essence| &i[2] |])
507 ]
508 ++ transformBi (upd j) gofAfter
509 )
510 theRule _ = na "rule_Comprehension_Image"
511
512
513 rule_Substring :: Rule
514 rule_Substring = "substring" `namedRule` theRule where
515 theRule [essence| &a substring &b |] = do
516 TypeSequence{} <- typeOf a
517 TypeSequence{} <- typeOf b
518
519 DomainSequence _ (SequenceAttr aSizeAttr _) _ <- domainOf a
520 aMaxSize <- case aSizeAttr of
521 SizeAttr_Size x -> return x
522 SizeAttr_MaxSize x -> return x
523 SizeAttr_MinMaxSize _ x -> return x
524 _ -> failDoc "rule_Substring maxSize"
525
526 DomainSequence _ (SequenceAttr bSizeAttr _) _ <- domainOf b
527 bMaxSize <- case bSizeAttr of
528 SizeAttr_Size x -> return x
529 SizeAttr_MaxSize x -> return x
530 SizeAttr_MinMaxSize _ x -> return x
531 _ -> failDoc "rule_Substring maxSize"
532
533 let maxSize = [essence| max([&aMaxSize, &bMaxSize]) |]
534
535 return
536 ( "Horizontal rule for substring on 2 sequences"
537 , do
538 (iPat, i) <- quantifiedVar
539 (jPat, j) <- quantifiedVar
540 return $ make opOr $ Comprehension
541 (make opAnd $ Comprehension
542 [essence| &j[2] = image(&b, &i + &j[1]) |]
543 [ Generator (GenInExpr jPat a)
544 ]
545 )
546 [ Generator (GenDomainNoRepr iPat $ mkDomainIntB 0 [essence| &maxSize - 1 |])]
547 )
548 theRule _ = na "rule_Substring"
549
550
551 rule_Subsequence :: Rule
552 rule_Subsequence = "subsequence" `namedRule` theRule where
553 theRule [essence| &a subsequence &b |] = do
554 TypeSequence{} <- typeOf a
555 TypeSequence{} <- typeOf b
556
557 DomainSequence _ (SequenceAttr aSizeAttr _) _ <- domainOf a
558 aMaxSize <- case aSizeAttr of
559 SizeAttr_Size x -> return x
560 SizeAttr_MaxSize x -> return x
561 SizeAttr_MinMaxSize _ x -> return x
562 _ -> failDoc "rule_Subsequence maxSize"
563
564 DomainSequence _ (SequenceAttr bSizeAttr _) _ <- domainOf b
565 bMaxSize <- case bSizeAttr of
566 SizeAttr_Size x -> return x
567 SizeAttr_MaxSize x -> return x
568 SizeAttr_MinMaxSize _ x -> return x
569 _ -> failDoc "rule_Subsequence maxSize"
570
571 -- for each value in a, find an index into b such that these indices are in increasing order
572 -- when there are multiple mappings that produce the same "a" (i.e. when there are duplicates in b)
573 -- this is does not functionally define the aux variable
574 return
575 ( "Horizontal rule for subsequence on 2 sequences"
576 , do
577 (auxName, aux) <- auxiliaryVar
578 (iPat, i) <- quantifiedVar
579 return $ WithLocals
580 [essence|
581 and([ &i[2] = image(&b, image(&aux, &i[1]))
582 | &iPat <- &a
583 ])
584 |]
585 (AuxiliaryVars
586 [ Declaration (FindOrGiven LocalFind auxName
587 (DomainSequence def (SequenceAttr aSizeAttr def) (mkDomainIntB 1 bMaxSize)))
588 , SuchThat
589 [ [essence| and([ image(&aux, &i-1) < image(&aux, &i)
590 | &iPat : int(2..&aMaxSize)
591 , &i <= |&aux|
592 ])
593 |]
594 , [essence| |&a| = |&aux|
595 |]
596 ]
597 ])
598 )
599 theRule _ = na "rule_Subsequence"