never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Representations.Sequence.ExplicitBounded ( sequenceExplicitBounded ) where
4
5 -- conjure
6 import Conjure.Prelude
7 import Conjure.Language
8 import Conjure.Language.ZeroVal ( zeroVal, EnumerateDomain )
9 import Conjure.Representations.Internal
10 import Conjure.Representations.Common
11
12
13 sequenceExplicitBounded :: forall m .
14 MonadFailDoc m=>
15 NameGen m =>
16 EnumerateDomain m =>
17 (?typeCheckerMode :: TypeCheckerMode) =>
18 Representation m
19 sequenceExplicitBounded = Representation chck downD structuralCons downC up symmetryOrdering
20
21 where
22
23 chck :: TypeOf_ReprCheck m
24 chck f (DomainSequence _ attrs@(SequenceAttr sizeAttr _) innerDomain) | hasMaxSize sizeAttr =
25 map (DomainSequence Sequence_ExplicitBounded attrs) <$> f innerDomain
26 chck _ _ = return []
27
28 nameMarker = mkOutName (Just "Length")
29 nameValues = mkOutName (Just "Values")
30
31 hasMaxSize SizeAttr_Size{} = True
32 hasMaxSize SizeAttr_MaxSize{} = True
33 hasMaxSize SizeAttr_MinMaxSize{} = True
34 hasMaxSize _ = False
35
36 getMaxSize (SizeAttr_MaxSize x) = return x
37 getMaxSize (SizeAttr_MinMaxSize _ x) = return x
38 getMaxSize _ = failDoc "Unknown maxSize"
39
40 downD :: TypeOf_DownD m
41 downD (name, domain@(DomainSequence
42 Sequence_ExplicitBounded
43 (SequenceAttr (SizeAttr_Size size) _)
44 innerDomain)) =
45 return $ Just
46 [ ( nameMarker domain name
47 , DomainInt TagInt [RangeBounded size size]
48 )
49 , ( nameValues domain name
50 , DomainMatrix
51 (DomainInt TagInt [RangeBounded 1 size])
52 innerDomain
53 ) ]
54 downD (name, domain@(DomainSequence
55 Sequence_ExplicitBounded
56 (SequenceAttr sizeAttr _)
57 innerDomain)) = do
58 maxSize <- getMaxSize sizeAttr
59 return $ Just
60 [ ( nameMarker domain name
61 , DomainInt TagInt [RangeBounded 0 maxSize]
62 )
63 , ( nameValues domain name
64 , DomainMatrix
65 (DomainInt TagInt [RangeBounded 1 maxSize])
66 innerDomain
67 ) ]
68 downD _ = na "{downD} ExplicitBounded"
69
70 structuralCons :: TypeOf_Structural m
71 structuralCons f downX1 (DomainSequence Sequence_ExplicitBounded
72 (SequenceAttr (SizeAttr_Size size) jectivityAttr) innerDomain) = do
73 let
74 injectiveCons :: Expression -> m [Expression]
75 injectiveCons values = do
76 innerType <- typeOfDomain innerDomain
77 case innerType of
78 TypeInt _ -> do
79 return $ return $ -- list
80 [essence| allDiff(&values) |]
81 _ -> do
82 (iPat, i) <- quantifiedVar
83 (jPat, j) <- quantifiedVar
84 return $ return $ -- list
85 [essence|
86 and([ &values[&i] != &values[&j]
87 | &iPat : int(1..&size)
88 , &jPat : int(1..&size)
89 , &i .< &j
90 ])
91 |]
92
93 surjectiveCons :: Expression -> m [Expression]
94 surjectiveCons values = do
95 (iPat, i) <- quantifiedVar
96 (jPat, j) <- quantifiedVar
97 return $ return $ -- list
98 [essence|
99 forAll &iPat : &innerDomain .
100 exists &jPat : int(1..&size) .
101 &values[&j] = &i
102 |]
103
104 jectivityCons :: Expression -> m [Expression]
105 jectivityCons values = case jectivityAttr of
106 JectivityAttr_None -> return []
107 JectivityAttr_Injective -> injectiveCons values
108 JectivityAttr_Surjective -> surjectiveCons values
109 JectivityAttr_Bijective -> (++) <$> injectiveCons values
110 <*> surjectiveCons values
111
112 let innerStructuralCons values = do
113 (iPat, i) <- quantifiedVarOverDomain [essenceDomain| int(1..&size) |]
114 let activeZone b = [essence| forAll &iPat : int(1..&size) . &b |]
115
116 -- preparing structural constraints for the inner guys
117 innerStructuralConsGen <- f innerDomain
118
119 let inLoop = [essence| &values[&i] |]
120 outs <- innerStructuralConsGen inLoop
121 return (map activeZone outs)
122
123 return $ \ sequ -> do
124 refs <- downX1 sequ
125 case refs of
126 [_marker,values] ->
127 concat <$> sequence
128 [ jectivityCons values
129 , innerStructuralCons values
130 ]
131 _ -> na "{structuralCons} ExplicitBounded"
132 structuralCons f downX1 (DomainSequence Sequence_ExplicitBounded (SequenceAttr sizeAttr jectivityAttr) innerDomain) = do
133 maxSize <- getMaxSize sizeAttr
134 let injectiveCons marker values = do
135 innerType <- typeOfDomain innerDomain
136 case innerType of
137 TypeInt _ -> do
138 (iPat, i) <- quantifiedVar
139 return $ return $ -- list
140 [essence| allDiff([ &values[&i]
141 | &iPat : int(1..&maxSize)
142 , &i <= &marker
143 ]) |]
144 _ -> do
145 (iPat, i) <- quantifiedVar
146 (jPat, j) <- quantifiedVar
147 return $ return $ -- list
148 [essence|
149 and([ &values[&i] != &values[&j]
150 | &iPat : int(1..&maxSize)
151 , &jPat : int(1..&maxSize)
152 , &i .< &j
153 , &i <= &marker
154 , &j <= &marker
155 ])
156 |]
157
158 let surjectiveCons marker values = do
159 (iPat, i) <- quantifiedVar
160 (jPat, j) <- quantifiedVar
161 return $ return $ -- list
162 [essence|
163 forAll &iPat : &innerDomain .
164 exists &jPat : int(1..&maxSize) .
165 (&j <= &marker) /\ &values[&j] = &i
166 |]
167
168 let jectivityCons marker values = case jectivityAttr of
169 JectivityAttr_None -> return []
170 JectivityAttr_Injective -> injectiveCons marker values
171 JectivityAttr_Surjective -> surjectiveCons marker values
172 JectivityAttr_Bijective -> (++) <$> injectiveCons marker values
173 <*> surjectiveCons marker values
174
175 let dontCareAfterMarker marker values = do
176 (iPat, i) <- quantifiedVar
177 return $ return $ -- list
178 [essence|
179 forAll &iPat : int(1..&maxSize) . &i > &marker ->
180 dontCare(&values[&i])
181 |]
182
183 let innerStructuralCons marker values = do
184 (iPat, i) <- quantifiedVarOverDomain [essenceDomain| int(1..&maxSize) |]
185 let activeZone b = [essence| forAll &iPat : int(1..&maxSize) . &i <= &marker -> &b |]
186
187 -- preparing structural constraints for the inner guys
188 innerStructuralConsGen <- f innerDomain
189
190 let inLoop = [essence| &values[&i] |]
191 outs <- innerStructuralConsGen inLoop
192 return (map activeZone outs)
193
194 return $ \ sequ -> do
195 refs <- downX1 sequ
196 case refs of
197 [marker,values] ->
198 concat <$> sequence
199 [ dontCareAfterMarker marker values
200 , return (mkSizeCons sizeAttr marker)
201 , jectivityCons marker values
202 , innerStructuralCons marker values
203 ]
204 _ -> na "{structuralCons} ExplicitBounded"
205
206 structuralCons _ _ _ = na "{structuralCons} ExplicitBounded"
207
208 downC :: TypeOf_DownC m
209 downC ( name
210 , domain@(DomainSequence _ (SequenceAttr (SizeAttr_Size size) _) innerDomain)
211 , viewConstantSequence -> Just constants
212 ) =
213 return $ Just
214 [ ( nameMarker domain name
215 , DomainInt TagInt [RangeBounded size size]
216 , ConstantInt TagInt (genericLength constants)
217 )
218 , ( nameValues domain name
219 , DomainMatrix (DomainInt TagInt [RangeBounded 1 size]) innerDomain
220 , ConstantAbstract $ AbsLitMatrix (DomainInt TagInt [RangeBounded 1 size]) constants
221 )
222 ]
223 downC ( name
224 , domain@(DomainSequence _ (SequenceAttr sizeAttr _) innerDomain)
225 , viewConstantSequence -> Just constants
226 ) = do
227 maxSize <- getMaxSize sizeAttr
228 let indexDomain i = mkDomainIntB (fromInt i) maxSize
229 maxSizeInt <-
230 case maxSize of
231 ConstantInt _ x -> return x
232 _ -> failDoc $ vcat
233 [ "Expecting an integer for the maxSize attribute."
234 , "But got:" <+> pretty maxSize
235 , "When working on:" <+> pretty name
236 , "With domain:" <+> pretty domain
237 ]
238 z <- zeroVal innerDomain
239 let zeroes = replicate (fromInteger (maxSizeInt - genericLength constants)) z
240 return $ Just
241 [ ( nameMarker domain name
242 , defRepr (indexDomain 0)
243 , ConstantInt TagInt (genericLength constants)
244 )
245 , ( nameValues domain name
246 , DomainMatrix (indexDomain 1) innerDomain
247 , ConstantAbstract $ AbsLitMatrix (indexDomain 1) (constants ++ zeroes)
248 )
249 ]
250 downC (name, domain, constant) = na $ vcat [ "{downC} ExplicitBounded"
251 , "name :" <+> pretty name
252 , "domain :" <+> pretty domain
253 , "constant:" <+> pretty constant
254 ]
255
256 up :: TypeOf_Up m
257 up ctxt (name, domain) =
258 case (lookup (nameMarker domain name) ctxt, lookup (nameValues domain name) ctxt) of
259 (Just marker, Just constantMatrix) ->
260 case marker of
261 ConstantInt _ card ->
262 case viewConstantMatrix constantMatrix of
263 Just (_, vals) ->
264 return (name, ConstantAbstract (AbsLitSequence (genericTake card vals)))
265 _ -> failDoc $ vcat
266 [ "Expecting a matrix literal for:" <+> pretty (nameValues domain name)
267 , "But got:" <+> pretty constantMatrix
268 , "When working on:" <+> pretty name
269 , "With domain:" <+> pretty domain
270 ]
271 _ -> failDoc $ vcat
272 [ "Expecting an integer literal for:" <+> pretty (nameMarker domain name)
273 , "But got:" <+> pretty marker
274 , "When working on:" <+> pretty name
275 , "With domain:" <+> pretty domain
276 ]
277 (Nothing, _) -> failDoc $ vcat $
278 [ "(in Sequence ExplicitBounded up 1)"
279 , "No value for:" <+> pretty (nameMarker domain name)
280 , "When working on:" <+> pretty name
281 , "With domain:" <+> pretty domain
282 ] ++
283 ("Bindings in context:" : prettyContext ctxt)
284 (_, Nothing) -> failDoc $ vcat $
285 [ "(in Sequence ExplicitBounded up 2)"
286 , "No value for:" <+> pretty (nameValues domain name)
287 , "When working on:" <+> pretty name
288 , "With domain:" <+> pretty domain
289 ] ++
290 ("Bindings in context:" : prettyContext ctxt)
291
292 symmetryOrdering :: TypeOf_SymmetryOrdering m
293 symmetryOrdering innerSO downX1 inp domain = do
294 [marker, values] <- downX1 inp
295 Just [_, (_, DomainMatrix index inner)] <- downD ("SO", domain)
296 (iPat, i) <- quantifiedVar
297 soValues <- innerSO downX1 [essence| &values[&i] |] inner
298 return
299 [essence|
300 ( &marker
301 , [ &soValues
302 | &iPat : &index
303 ]
304 )
305 |]