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