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