never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Representations.Function.FunctionNDPartial ( functionNDPartial ) where
4
5 -- conjure
6 import Conjure.Prelude
7 import Conjure.Bug
8 import Conjure.Language
9 import Conjure.Language.ZeroVal ( zeroVal, EnumerateDomain )
10 import Conjure.Representations.Internal
11 import Conjure.Representations.Common
12 import Conjure.Representations.Function.Function1D ( domainValues )
13 import Conjure.Representations.Function.FunctionND ( viewAsDomainTuple, mkLensAsDomainTuple )
14
15
16 functionNDPartial :: forall m .
17 MonadFailDoc m =>
18 NameGen m =>
19 EnumerateDomain m =>
20 (?typeCheckerMode :: TypeCheckerMode) =>
21 Representation m
22 functionNDPartial = Representation chck downD structuralCons downC up symmetryOrdering
23
24 where
25
26 chck :: TypeOf_ReprCheck m
27 chck f (DomainFunction _
28 attrs@(FunctionAttr _ PartialityAttr_Partial _)
29 innerDomainFr@(viewAsDomainTuple -> Just innerDomainFrs)
30 innerDomainTo) | all domainCanIndexMatrix innerDomainFrs = do
31 innerDomainFr' <- f innerDomainFr
32 innerDomainTo' <- f innerDomainTo
33 return [ DomainFunction Function_NDPartial attrs fr to
34 | fr <- innerDomainFr'
35 , to <- innerDomainTo'
36 ]
37 chck _ _ = return []
38
39 nameFlags = mkOutName (Just "Flags")
40 nameValues = mkOutName (Just "Values")
41
42 downD :: TypeOf_DownD m
43 downD (name, domain@(DomainFunction Function_NDPartial
44 (FunctionAttr _ PartialityAttr_Partial _)
45 (viewAsDomainTuple -> Just innerDomainFrs)
46 innerDomainTo)) | all domainCanIndexMatrix innerDomainFrs = do
47 let unroll is j = foldr DomainMatrix j is
48 return $ Just
49 [ ( nameFlags domain name
50 , unroll (map forgetRepr innerDomainFrs) DomainBool
51 )
52 , ( nameValues domain name
53 , unroll (map forgetRepr innerDomainFrs) innerDomainTo
54 )
55 ]
56 downD _ = na "{downD} FunctionNDPartial"
57
58 structuralCons :: TypeOf_Structural m
59 structuralCons f downX1
60 (DomainFunction Function_NDPartial
61 (FunctionAttr sizeAttr PartialityAttr_Partial jectivityAttr)
62 innerDomainFr@(viewAsDomainTuple -> Just innerDomainFrs)
63 innerDomainTo) | all domainCanIndexMatrix innerDomainFrs = do
64 let
65 kRange = case innerDomainFr of
66 DomainTuple ts -> map fromInt [1 .. genericLength ts]
67 DomainRecord rs -> map (fromName . fst) rs
68 _ -> bug $ vcat [ "FunctionNDPartial.structuralCons"
69 , "innerDomainFr:" <+> pretty innerDomainFr
70 ]
71 toIndex x = [ [essence| &x[&k] |] | k <- kRange ]
72 index x m = make opMatrixIndexing m (toIndex x)
73
74 let
75 injectiveCons :: Expression -> Expression -> m [Expression]
76 injectiveCons flags values = do
77 (iPat, i) <- quantifiedVar
78 (jPat, j) <- quantifiedVar
79 let flagsIndexedI = index i flags
80 let valuesIndexedI = index i values
81 let flagsIndexedJ = index j flags
82 let valuesIndexedJ = index j values
83 return $ return $ -- list
84 [essence|
85 and([ &valuesIndexedI != &valuesIndexedJ
86 | &iPat : &innerDomainFr
87 , &jPat : &innerDomainFr
88 , &i .< &j
89 , &flagsIndexedI
90 , &flagsIndexedJ
91 ])
92 |]
93
94 surjectiveCons :: Expression -> Expression -> m [Expression]
95 surjectiveCons flags values = do
96 (iPat, i) <- quantifiedVar
97 (jPat, j) <- quantifiedVar
98
99 let flagsIndexed = index j flags
100 let valuesIndexed = index j values
101 return $ return $ -- list
102 [essence|
103 forAll &iPat : &innerDomainTo .
104 exists &jPat : &innerDomainFr .
105 &flagsIndexed /\ &valuesIndexed = &i
106 |]
107
108 jectivityCons :: Expression -> Expression -> m [Expression]
109 jectivityCons flags values = case jectivityAttr of
110 JectivityAttr_None -> return []
111 JectivityAttr_Injective -> injectiveCons flags values
112 JectivityAttr_Surjective -> surjectiveCons flags values
113 JectivityAttr_Bijective -> (++) <$> injectiveCons flags values
114 <*> surjectiveCons flags values
115
116 cardinality :: Expression -> m Expression
117 cardinality flags = do
118 (iPat, i) <- quantifiedVar
119 let flagsIndexed = index i flags
120 return [essence| sum &iPat : &innerDomainFr . toInt(&flagsIndexed) |]
121
122 dontCareInactives :: Expression -> Expression -> m [Expression]
123 dontCareInactives flags values = do
124 (iPat, i) <- quantifiedVar
125 let flagsIndexed = index i flags
126 let valuesIndexed = index i values
127 return $ return $ -- list
128 [essence|
129 forAll &iPat : &innerDomainFr . &flagsIndexed = false ->
130 dontCare(&valuesIndexed)
131 |]
132
133 let innerStructuralCons flags values = do
134 (iPat, i) <- quantifiedVarOverDomain (forgetRepr innerDomainFr)
135 let flagsIndexed = index i flags
136 let valuesIndexed = index i values
137 let activeZone b = [essence| forAll &iPat : &innerDomainFr . &flagsIndexed -> &b |]
138
139 -- preparing structural constraints for the inner guys
140 innerStructuralConsGen <- f innerDomainTo
141
142 let inLoop = valuesIndexed
143 outs <- innerStructuralConsGen inLoop
144 return (map activeZone outs)
145
146 return $ \ rel -> do
147 refs <- downX1 rel
148 case refs of
149 [flags,values] ->
150 concat <$> sequence
151 [ jectivityCons flags values
152 , dontCareInactives flags values
153 , mkSizeCons sizeAttr <$> cardinality flags
154 , innerStructuralCons flags values
155 ]
156 _ -> na "{structuralCons} FunctionNDPartial"
157
158 structuralCons _ _ _ = na "{structuralCons} FunctionNDPartial"
159
160 downC :: TypeOf_DownC m
161 downC ( name
162 , domain@(DomainFunction Function_NDPartial
163 (FunctionAttr _ PartialityAttr_Partial _)
164 innerDomainFr@(viewAsDomainTuple -> Just innerDomainFrs)
165 innerDomainTo)
166 , viewConstantFunction -> Just vals
167 ) | all domainCanIndexMatrix innerDomainFrs
168 , Just (_mk, inspect) <- mkLensAsDomainTuple innerDomainFr = do
169 z <- zeroVal innerDomainTo
170 let
171 check :: [Constant] -> Maybe Constant
172 check indices = listToMaybe [ v
173 | (inspect -> Just k, v) <- vals
174 , k == indices
175 ]
176
177 let
178 unrollD :: [Domain () Constant] -> Domain r Constant -> Domain r Constant
179 unrollD is j = foldr DomainMatrix j is
180
181 let
182 unrollC :: MonadFailDoc m
183 => [Domain () Constant]
184 -> [Constant] -- indices
185 -> m (Constant, Constant)
186 unrollC [i] prevIndices = do
187 domVals <- domainValues i
188 let active val = check $ prevIndices ++ [val]
189 return ( ConstantAbstract $ AbsLitMatrix i
190 [ case active val of
191 Nothing -> ConstantBool False
192 Just{} -> ConstantBool True
193 | val <- domVals ]
194 , ConstantAbstract $ AbsLitMatrix i
195 [ fromMaybe z (active val)
196 | val <- domVals ]
197 )
198 unrollC (i:is) prevIndices = do
199 domVals <- domainValues i
200 (matrixFlags, matrixVals) <- fmap unzip $ forM domVals $ \ val ->
201 unrollC is (prevIndices ++ [val])
202 return ( ConstantAbstract $ AbsLitMatrix i matrixFlags
203 , ConstantAbstract $ AbsLitMatrix i matrixVals
204 )
205 unrollC is prevIndices = failDoc $ vcat [ "FunctionNDPartial.up.unrollC"
206 , " is :" <+> vcat (map pretty is)
207 , " prevIndices:" <+> pretty (show prevIndices)
208 ]
209
210 (outFlags, outValues) <- unrollC (map forgetRepr innerDomainFrs) []
211 return $ Just
212 [ ( nameFlags domain name
213 , unrollD (map forgetRepr innerDomainFrs) DomainBool
214 , outFlags
215 )
216 , ( nameValues domain name
217 , unrollD (map forgetRepr innerDomainFrs) innerDomainTo
218 , outValues
219 )
220 ]
221
222 downC _ = na "{downC} FunctionNDPartial"
223
224 up :: TypeOf_Up m
225 up ctxt (name, domain@(DomainFunction Function_NDPartial
226 (FunctionAttr _ PartialityAttr_Partial _)
227 innerDomainFr@(viewAsDomainTuple -> Just innerDomainFrs) _))
228
229 | Just (mk, _inspect) <- mkLensAsDomainTuple innerDomainFr =
230
231 case (lookup (nameFlags domain name) ctxt, lookup (nameValues domain name) ctxt) of
232 (Just flagMatrix, Just valuesMatrix) -> do
233 let
234 allIndices :: (MonadFailDoc m, Pretty r) => [Domain r Constant] -> m [[Constant]]
235 allIndices = fmap sequence . mapM domainValues
236
237 index :: MonadFailDoc m => Constant -> [Constant] -> m Constant
238 index m [] = return m
239 index (ConstantAbstract (AbsLitMatrix indexDomain vals)) (i:is) = do
240 froms <- domainValues indexDomain
241 case lookup i (zip froms vals) of
242 Nothing -> failDoc "Value not found. FunctionNDPartial.up.index"
243 Just v -> index v is
244 index m is = bug ("FunctionNDPartial.up.index" <+> pretty m <+> pretty (show is))
245
246 indices <- allIndices innerDomainFrs
247 vals <- forM indices $ \ these -> do
248 flag <- index flagMatrix these
249 value <- index valuesMatrix these
250 case viewConstantBool flag of
251 Just False -> return Nothing
252 Just True -> return (Just (mk these, value))
253 _ -> failDoc $ vcat
254 [ "Expecting a boolean literal, but got:" <++> pretty flag
255 , " , and :" <+> pretty value
256 , "When working on:" <+> pretty name
257 , "With domain:" <+> pretty domain
258 ]
259 return ( name
260 , ConstantAbstract $ AbsLitFunction $ catMaybes vals
261 )
262
263 (Nothing, _) -> failDoc $ vcat $
264 [ "(in FunctionNDPartial up 1)"
265 , "No value for:" <+> pretty (nameFlags domain name)
266 , "When working on:" <+> pretty name
267 , "With domain:" <+> pretty domain
268 ] ++
269 ("Bindings in context:" : prettyContext ctxt)
270 (_, Nothing) -> failDoc $ vcat $
271 [ "(in FunctionNDPartial up 2)"
272 , "No value for:" <+> pretty (nameValues domain name)
273 , "When working on:" <+> pretty name
274 , "With domain:" <+> pretty domain
275 ] ++
276 ("Bindings in context:" : prettyContext ctxt)
277 up _ _ = na "{up} FunctionNDPartial"
278
279 symmetryOrdering :: TypeOf_SymmetryOrdering m
280 symmetryOrdering innerSO downX1 inp domain = do
281 [flags, values] <- downX1 inp
282 Just [_, (_, DomainMatrix innerDomainFr innerDomainTo)] <- downD ("SO", domain)
283 (iPat, i) <- quantifiedVar
284
285 -- setting up the quantification
286 let kRange = case innerDomainFr of
287 DomainTuple ts -> map fromInt [1 .. genericLength ts]
288 DomainRecord rs -> map (fromName . fst) rs
289 _ -> bug $ vcat [ "FunctionND.rule_Comprehension"
290 , "indexDomain:" <+> pretty innerDomainFr
291 ]
292 toIndex = [ [essence| &i[&k] |] | k <- kRange ]
293 flagsIndexed = make opMatrixIndexing flags toIndex
294 valuesIndexed = make opMatrixIndexing values toIndex
295
296 soValues <- innerSO downX1 valuesIndexed innerDomainTo
297
298 return $
299 Comprehension
300 [essence| ( -&flagsIndexed
301 , &soValues
302 )
303 |]
304 [Generator (GenDomainNoRepr iPat (forgetRepr innerDomainFr))]