never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Rules.Vertical.Function.FunctionAsRelation where
4
5 import Conjure.Rules.Import
6
7
8 -- TODO: this is incomplete
9 rule_Image_Eq :: Rule
10 rule_Image_Eq = "function-image-eq{FunctionAsRelation}" `namedRule` theRule where
11
12 -- =
13 theRule [essence| image(&func, &x) = &y |] = do
14 Function_AsRelation{} <- representationOf func
15 [rel] <- downX1 func
16 return
17 ( "Function image-equals, FunctionAsRelation representation"
18 , do
19 (iPat, i) <- quantifiedVar
20 return [essence| or([ &i[1] = &x /\ &i[2] = &y | &iPat <- &rel ]) |]
21 )
22 theRule [essence| &y = image(&func, &x) |] = do
23 Function_AsRelation{} <- representationOf func
24 [rel] <- downX1 func
25 return
26 ( "Function image-equals, FunctionAsRelation representation"
27 , do
28 (iPat, i) <- quantifiedVar
29 return [essence| or([ &i[1] = &x /\ &i[2] = &y | &iPat <- &rel ]) |]
30 )
31
32 -- <=
33 theRule [essence| image(&func, &x) <= &y |] = do
34 Function_AsRelation{} <- representationOf func
35 [rel] <- downX1 func
36 return
37 ( "Function image-equals, FunctionAsRelation representation"
38 , do
39 (iPat, i) <- quantifiedVar
40 return [essence| or([ &i[1] = &x /\ &i[2] <= &y | &iPat <- &rel ]) |]
41 )
42 theRule [essence| &y >= image(&func, &x) |] = do
43 Function_AsRelation{} <- representationOf func
44 [rel] <- downX1 func
45 return
46 ( "Function image-equals, FunctionAsRelation representation"
47 , do
48 (iPat, i) <- quantifiedVar
49 return [essence| or([ &i[1] = &x /\ &i[2] <= &y | &iPat <- &rel ]) |]
50 )
51
52 -- >=
53 theRule [essence| image(&func, &x) >= &y |] = do
54 Function_AsRelation{} <- representationOf func
55 [rel] <- downX1 func
56 return
57 ( "Function image-equals, FunctionAsRelation representation"
58 , do
59 (iPat, i) <- quantifiedVar
60 return [essence| or([ &i[1] = &x /\ &i[2] >= &y | &iPat <- &rel ]) |]
61 )
62 theRule [essence| &y <= image(&func, &x) |] = do
63 Function_AsRelation{} <- representationOf func
64 [rel] <- downX1 func
65 return
66 ( "Function image-equals, FunctionAsRelation representation"
67 , do
68 (iPat, i) <- quantifiedVar
69 return [essence| or([ &i[1] = &x /\ &i[2] >= &y | &iPat <- &rel ]) |]
70 )
71
72 theRule _ = na "rule_Image"
73
74
75 rule_Comprehension :: Rule
76 rule_Comprehension = "function-comprehension{FunctionAsRelation}" `namedRule` theRule where
77 theRule (Comprehension body gensOrConds) = do
78 (gocBefore, (pat, func), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
79 Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDefs [opToSet,opToMSet,opToRelation] expr)
80 _ -> na "rule_Comprehension"
81 Function_AsRelation{} <- representationOf func
82 [rel] <- downX1 func
83 return
84 ( "Mapping over a function, FunctionAsRelation representation"
85 , return $
86 Comprehension body
87 $ gocBefore
88 ++ [ Generator (GenInExpr pat rel) ]
89 ++ gocAfter
90 )
91 theRule _ = na "rule_Comprehension"
92
93
94 -- TODO
95 -- rule_PowerSet_Comprehension :: Rule
96 -- rule_PowerSet_Comprehension = "function-powerSet-comprehension{FunctionAsRelation}" `namedRule` theRule where
97 -- theRule (Comprehension body gensOrConds) = do
98 -- traceM $ show $ "rule_PowerSet_Comprehension [1]" <+> pretty (Comprehension body gensOrConds)
99 -- (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
100 -- Generator (GenInExpr pat expr) -> return (pat, expr)
101 -- _ -> na "rule_Comprehension"
102 -- traceM $ show $ "rule_PowerSet_Comprehension [2]" <+> pretty expr
103 -- func <- matchDefs [opToSet,opToMSet,opToRelation] <$> match opPowerSet expr
104 -- traceM $ show $ "rule_PowerSet_Comprehension [3]" <+> pretty func
105 -- repr <- representationOf func
106 -- traceM $ show $ "rule_PowerSet_Comprehension [4]" <+> pretty repr
107 -- Function_AsRelation{} <- representationOf func
108 -- traceM $ "rule_PowerSet_Comprehension [4]"
109 -- [rel] <- downX1 func
110 -- traceM $ show $ "rule_PowerSet_Comprehension [4]" <+> pretty rel
111 -- return
112 -- ( "Mapping over a function, FunctionAsRelation representation"
113 -- , return $
114 -- Comprehension body
115 -- $ gocBefore
116 -- ++ [ Generator (GenInExpr pat (make opPowerSet rel)) ]
117 -- ++ gocAfter
118 -- )
119 -- theRule _ = na "rule_PowerSet_Comprehension"
120
121
122 rule_InDefined :: Rule
123 rule_InDefined = "function-inDefined{FunctionAsRelation}" `namedRule` theRule where
124 theRule [essence| &x in defined(&func) |] = do
125 TypeFunction{} <- typeOf func
126 Function_AsRelation (Relation_AsSet Set_Explicit) <- representationOf func
127 tableCheck x func
128 xParts <- downX1 x
129 let vars = fromList xParts
130 [rel] <- downX1 func
131 [set] <- downX1 rel
132 [matrix] <- downX1 set
133 [from, _to] <- downX1 matrix
134 parts <- downX1 from
135 (index:_) <- indexDomainsOf from
136 (iPat, i) <- quantifiedVar
137 let oneRow = fromList [ [essence| &p[&i] |] | p <- parts ]
138 let table = [essence| [ &oneRow | &iPat : &index ] |]
139 return
140 ( "relation membership to table"
141 , return [essence| table(&vars, &table) |]
142 )
143 theRule _ = na "rule_InDefined"
144
145 tableCheck ::
146 MonadFailDoc m =>
147 (?typeCheckerMode :: TypeCheckerMode) =>
148 Expression -> Expression -> m ()
149 tableCheck x func | categoryOf func < CatDecision = do
150 tyX <- typeOf x
151 case tyX of
152 TypeTuple ts | and [ case t of TypeInt{} -> True ; _ -> False | t <- ts ] -> return ()
153 _ -> na "tableCheck"
154 tableCheck _ _ = na "tableCheck"
155
156
157 rule_InToSet :: Rule
158 rule_InToSet = "function-inToSet{FunctionAsRelation}" `namedRule` theRule where
159 theRule [essence| &x in toSet(&func) |] = do
160 TypeFunction{} <- typeOf func
161 Function_AsRelation (Relation_AsSet Set_Explicit) <- representationOf func
162 tableCheck x func
163 [keyFrom, keyTo] <- downX1 x
164 keyFromParts <- downX1 keyFrom
165 let vars = fromList (keyFromParts ++ [keyTo])
166 [rel] <- downX1 func
167 [set] <- downX1 rel
168 [matrix] <- downX1 set
169 [from, to] <- downX1 matrix
170 parts <- downX1 from
171 (index:_) <- indexDomainsOf from
172 (iPat, i) <- quantifiedVar
173 let oneRow = fromList $ [ [essence| &p[&i] |] | p <- parts ]
174 ++ [ [essence| &to[&i] |] ]
175 let table = [essence| [ &oneRow | &iPat : &index ] |]
176 return
177 ( "relation membership to table"
178 , return [essence| table(&vars, &table) |]
179 )
180 theRule _ = na "rule_InToSet"
181
182 tableCheck ::
183 MonadFailDoc m =>
184 (?typeCheckerMode :: TypeCheckerMode) =>
185 Expression -> Expression -> m ()
186 tableCheck x func | categoryOf func < CatDecision = do
187 tyX <- typeOf x
188 case tyX of
189 TypeTuple [TypeTuple ts, to] | and [ case t of TypeInt{} -> True ; _ -> False | t <- (to:ts) ] -> return ()
190 _ -> na "tableCheck"
191 tableCheck _ _ = na "tableCheck"