never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Vertical.Function.Function1DPartial where
4
5 import Conjure.Rules.Import
6
7
8 rule_Comprehension :: Rule
9 rule_Comprehension = "function-comprehension{Function1DPartial}" `namedRule` theRule where
10 theRule (Comprehension body gensOrConds) = do
11 (gocBefore, (pat, func), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
12 Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDefs [opToSet,opToMSet,opToRelation] expr)
13 _ -> na "rule_Comprehension"
14 Function_1DPartial <- representationOf func
15 TypeFunction{ } <- typeOf func
16 DomainFunction _ _ index _ <- domainOf func
17 [flags,values] <- downX1 func
18 let upd val old = lambdaToFunction pat old val
19 return
20 ( "Mapping over a function, Function1DPartial representation"
21 , do
22 (jPat, j) <- quantifiedVar
23 let valuesIndexed = [essence| (&j, &values[&j]) |]
24 let flagsIndexed = [essence| &flags [&j] |]
25 return $ Comprehension (upd valuesIndexed body)
26 $ gocBefore
27 ++ [ Generator (GenDomainNoRepr jPat (forgetRepr index))
28 , Condition [essence| &flagsIndexed |]
29 ]
30 ++ transformBi (upd valuesIndexed) gocAfter
31 )
32 theRule _ = na "rule_Comprehension"
33
34
35 rule_PowerSet_Comprehension :: Rule
36 rule_PowerSet_Comprehension = "function-powerSet-comprehension{Function1DPartial}" `namedRule` theRule where
37 theRule (Comprehension body gensOrConds) = do
38 (gocBefore, (setPat, setPatNum, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
39 Generator (GenInExpr setPat@(AbsPatSet pats) expr) -> return (setPat, length pats, expr)
40 _ -> na "rule_PowerSet_Comprehension"
41 func <- match opPowerSet expr
42 TypeFunction{} <- typeOf func
43 Function_1DPartial <- representationOf func
44 DomainFunction _ _ index _ <- domainOf func
45 [flags,values] <- downX1 func
46 let upd val old = lambdaToFunction setPat old val
47 return
48 ( "Vertical rule for set-comprehension, Explicit representation"
49 , do
50 outPats <- replicateM setPatNum quantifiedVar
51 let val = AbstractLiteral $ AbsLitSet [ [essence| (&flags[&j], &values[&j]) |] | (_,j) <- outPats ]
52 return $ Comprehension (upd val body) $ concat
53 [ gocBefore
54 , concat
55 [ [ Generator (GenDomainNoRepr pat index) ]
56 | (pat,_) <- take 1 outPats
57 ]
58 , concat
59 [ [ Generator (GenDomainNoRepr pat index)
60 , Condition [essence| &patX > &beforeX |]
61 ]
62 | ((_, beforeX), (pat, patX)) <- zip outPats (tail outPats)
63 ]
64 , transformBi (upd val) gocAfter
65 ]
66 )
67 theRule _ = na "rule_PowerSet_Comprehension"
68
69
70 rule_Image_NotABool :: Rule
71 rule_Image_NotABool = "function-image{Function1DPartial}-not-a-bool" `namedRule` theRule where
72 theRule [essence| image(&f,&x) |] = do
73 Function_1DPartial <- representationOf f
74 TypeFunction _ tyTo <- typeOf f
75 case tyTo of
76 TypeBool -> na "function ? --> bool"
77 _ -> return ()
78 [flags,values] <- downX1 f
79 return
80 ( "Function image, Function1DPartial representation, not-a-bool"
81 , return [essence| { &values[&x]
82 @ such that &flags[&x]
83 }
84 |]
85 )
86 theRule _ = na "rule_Image_NotABool"
87
88
89 rule_Image_Bool :: Rule
90 rule_Image_Bool = "function-image{Function1DPartial}-bool" `namedRule` theRule where
91 theRule p = do
92 let
93 imageChild ch@[essence| image(&f,&x) |] = do
94 Function_1DPartial <- representationOf f
95 TypeFunction _ tyTo <- typeOf f
96 case tyTo of
97 TypeBool -> do
98 [flags,values] <- downX1 f
99 tell $ return [essence| &flags[&x] |]
100 return [essence| { &values[&x] @ such that &flags[&x] } |]
101 _ -> return ch
102 imageChild ch = return ch
103 topMost <- asks isTopMostZ
104 (p', flags) <-
105 if topMost
106 then -- this term sits at the topmost level, requires special treatment
107 runWriterT (imageChild p)
108 else
109 runWriterT (descendM imageChild p)
110 case flags of
111 [] -> na "rule_Image_Bool"
112 _ -> do
113 -- let flagsCombined = make opAnd $ fromList flags
114 return
115 ( "Function image, Function1DPartial representation, bool"
116 , return p'
117 )
118
119
120 rule_InDefined :: Rule
121 rule_InDefined = "function-in-defined{Function1DPartial}" `namedRule` theRule where
122 theRule [essence| &x in defined(&f) |] = do
123 TypeFunction{} <- typeOf f
124 Function_1DPartial <- representationOf f
125 [flags,_values] <- downX1 f
126 return
127 ( "Function in defined, Function1DPartial representation"
128 , return [essence| &flags[&x] |]
129 )
130 theRule _ = na "rule_InDefined"
131
132
133 rule_DefinedEqDefined :: Rule
134 rule_DefinedEqDefined = "set-subsetEq" `namedRule` theRule where
135 theRule [essence| defined(&x) = defined(&y) |] = do
136 TypeFunction{} <- typeOf x
137 Function_1DPartial <- representationOf x
138 [xFlags,_] <- downX1 x
139 TypeFunction{} <- typeOf y
140 Function_1DPartial <- representationOf y
141 [yFlags,_] <- downX1 y
142 DomainFunction _ _ xIndex _ <- domainOf x
143 DomainFunction _ _ yIndex _ <- domainOf y
144 unless (xIndex == yIndex) (na "rule_DefinedEqDefined")
145 return
146 ( "Horizontal rule for set subsetEq"
147 , do
148 (iPat, i) <- quantifiedVar
149 return [essence| forAll &iPat : &xIndex . &xFlags[&i] = &yFlags[&i] |]
150 )
151 theRule _ = na "rule_DefinedEqDefined"
152