never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Representations.MSet.ExplicitWithFlags ( msetExplicitWithFlags ) where
4
5 -- conjure
6 import Conjure.Prelude
7 import Conjure.Language
8 import Conjure.Language.DomainSizeOf
9 import Conjure.Language.Expression.DomainSizeOf ()
10 import Conjure.Language.ZeroVal ( zeroVal, EnumerateDomain )
11 import Conjure.Representations.Internal
12 import Conjure.Representations.Common
13
14
15 msetExplicitWithFlags :: forall m . (MonadFailDoc m, NameGen m, EnumerateDomain m) => Representation m
16 msetExplicitWithFlags = Representation chck downD structuralCons downC up symmetryOrdering
17
18 where
19
20 chck :: TypeOf_ReprCheck m
21 chck f (DomainMSet _ attrs innerDomain) =
22 map (DomainMSet MSet_ExplicitWithFlags attrs) <$> f innerDomain
23 chck _ _ = return []
24
25 nameFlag = mkOutName (Just "Flags")
26 nameValues = mkOutName (Just "Values")
27
28 getMaxSize attrs innerDomain = case attrs of
29 MSetAttr (SizeAttr_Size x) _ -> return x
30 MSetAttr (SizeAttr_MaxSize x) _ -> return x
31 MSetAttr (SizeAttr_MinMaxSize _ x) _ -> return x
32 MSetAttr _ (OccurAttr_MaxOccur x) -> do y <- domainSizeOf innerDomain ; return (x * y)
33 MSetAttr _ (OccurAttr_MinMaxOccur _ x) -> do y <- domainSizeOf innerDomain ; return (x * y)
34 _ -> failDoc ("getMaxSize, mset not supported. attributes:" <+> pretty attrs)
35
36 getMinOccur attrs = case attrs of
37 MSetAttr _ (OccurAttr_MinOccur x) -> Just x
38 MSetAttr _ (OccurAttr_MinMaxOccur x _) -> Just x
39 _ -> Nothing
40
41 getMaxOccur attrs = case attrs of
42 MSetAttr _ (OccurAttr_MaxOccur x) -> return x
43 MSetAttr _ (OccurAttr_MinMaxOccur _ x) -> return x
44 MSetAttr (SizeAttr_Size x) _ -> return x
45 MSetAttr (SizeAttr_MaxSize x) _ -> return x
46 MSetAttr (SizeAttr_MinMaxSize _ x) _ -> return x
47 _ -> failDoc ("getMaxOccur, mset not supported. attributes:" <+> pretty attrs)
48
49 downD :: TypeOf_DownD m
50 downD (name, domain@(DomainMSet _ attrs innerDomain)) = do
51 maxSize <- getMaxSize attrs innerDomain
52 maxOccur <- getMaxOccur attrs
53 let indexDomain = mkDomainIntB 1 maxSize
54 let flagDomain = defRepr $ mkDomainIntB 0 maxOccur
55 return $ Just
56 [ ( nameFlag domain name
57 , DomainMatrix indexDomain flagDomain
58 )
59 , ( nameValues domain name
60 , DomainMatrix indexDomain innerDomain
61 )
62 ]
63 downD _ = na "{downD} ExplicitVarSizeWithFlags"
64
65 structuralCons :: TypeOf_Structural m
66 structuralCons f downX1 (DomainMSet MSet_ExplicitWithFlags attrs@(MSetAttr sizeAttrs _) innerDomain) = do
67 maxSize <- getMaxSize attrs innerDomain
68 let
69 orderingWhenFlagged flags values = do
70 (iPat, i) <- quantifiedVar
71 return $ return $ -- list
72 [essence|
73 forAll &iPat : int(1..&maxSize-1) . &flags[&i+1] > 0 -> &values[&i] .< &values[&i+1]
74 |]
75
76 dontCareWhenNotFlagged flags values = do
77 (iPat, i) <- quantifiedVar
78 return $ return $ -- list
79 [essence|
80 forAll &iPat : int(1..&maxSize) . &flags[&i] = 0 -> dontCare(&values[&i])
81 |]
82
83 flagsToTheLeft flags = do
84 (iPat, i) <- quantifiedVar
85 return $ return $ -- list
86 [essence|
87 forAll &iPat : int(1..&maxSize-1) . &flags[&i+1] > 0 -> &flags[&i] > 0
88 |]
89
90 cardinality flags = do
91 (iPat, i) <- quantifiedVar
92 return [essence| sum &iPat : int(1..&maxSize) . &flags[&i] |]
93
94 -- maxOccur is enforced by the domain of the flag
95 minOccurrenceCons flags = do
96 (jPat, j) <- quantifiedVar
97 return
98 [ [essence| forAll &jPat : int(1..&maxSize) . &flags[&j] = 0 \/ &flags[&j] >= &minOccur |]
99 | Just minOccur <- [getMinOccur attrs]
100 ]
101
102 innerStructuralCons flags values = do
103 (iPat, i) <- quantifiedVarOverDomain [essenceDomain| int(1..&maxSize) |]
104 let activeZone b = [essence| forAll &iPat : int(1..&maxSize) . &flags[&i] > 0 -> &b |]
105
106 -- preparing structural constraints for the inner guys
107 innerStructuralConsGen <- f innerDomain
108
109 let inLoop = [essence| &values[&i] |]
110 outs <- innerStructuralConsGen inLoop
111 return (map activeZone outs)
112
113 return $ \ mset -> do
114 refs <- downX1 mset
115 case refs of
116 [flags, values] ->
117 concat <$> sequence
118 [ orderingWhenFlagged flags values
119 , dontCareWhenNotFlagged flags values
120 , flagsToTheLeft flags
121 , minOccurrenceCons flags
122 , mkSizeCons sizeAttrs <$> cardinality flags
123 , innerStructuralCons flags values
124 ]
125 _ -> na "{structuralCons} ExplicitVarSizeWithFlags"
126
127 structuralCons _ _ _ = na "{structuralCons} ExplicitVarSizeWithFlags"
128
129 downC :: TypeOf_DownC m
130 downC ( name
131 , domain@(DomainMSet _ attrs innerDomain)
132 , viewConstantMSet -> Just constants'
133 ) = do
134 maxSize <- getMaxSize attrs innerDomain
135 let indexDomain = mkDomainIntB 1 maxSize
136
137 let constants = histogram constants'
138
139 maxSizeInt <-
140 case maxSize of
141 ConstantInt _ x -> return x
142 _ -> failDoc $ vcat
143 [ "Expecting an integer for the maxSize attribute."
144 , "But got:" <+> pretty maxSize
145 , "When working on:" <+> pretty name
146 , "With domain:" <+> pretty domain
147 ]
148 z <- zeroVal innerDomain
149 let zeroes = replicate (fromInteger (maxSizeInt - genericLength constants)) z
150
151 let counts = map (ConstantInt TagInt . snd) constants
152 let falses = replicate (fromInteger (maxSizeInt - genericLength constants)) (ConstantInt TagInt 0)
153
154 return $ Just
155 [ ( nameFlag domain name
156 , DomainMatrix indexDomain DomainBool
157 , ConstantAbstract $ AbsLitMatrix indexDomain (counts ++ falses)
158 )
159 , ( nameValues domain name
160 , DomainMatrix indexDomain innerDomain
161 , ConstantAbstract $ AbsLitMatrix indexDomain (map fst constants ++ zeroes)
162 )
163 ]
164 downC _ = na "{downC} ExplicitVarSizeWithFlags"
165
166 up :: TypeOf_Up m
167 up ctxt (name, domain) =
168 case (lookup (nameFlag domain name) ctxt, lookup (nameValues domain name) ctxt) of
169 (Just flagMatrix, Just constantMatrix) ->
170 case viewConstantMatrix flagMatrix of
171 -- TODO: check if indices match
172 Just (_, flags) ->
173 case viewConstantMatrix constantMatrix of
174 Just (_, vals) ->
175 return (name, ConstantAbstract $ AbsLitMSet $ concat
176 [ replicate (fromInteger i) v
177 | (ConstantInt TagInt i,v) <- zip flags vals
178 ] )
179 _ -> failDoc $ vcat
180 [ "Expecting a matrix literal for:" <+> pretty (nameValues domain name)
181 , "But got:" <+> pretty constantMatrix
182 , "When working on:" <+> pretty name
183 , "With domain:" <+> pretty domain
184 ]
185 _ -> failDoc $ vcat
186 [ "Expecting a matrix literal for:" <+> pretty (nameFlag domain name)
187 , "But got:" <+> pretty flagMatrix
188 , "When working on:" <+> pretty name
189 , "With domain:" <+> pretty domain
190 ]
191 (Nothing, _) -> failDoc $ vcat $
192 [ "(in MSet ExplicitVarSizeWithFlags up 1)"
193 , "No value for:" <+> pretty (nameFlag domain name)
194 , "When working on:" <+> pretty name
195 , "With domain:" <+> pretty domain
196 ] ++
197 ("Bindings in context:" : prettyContext ctxt)
198 (_, Nothing) -> failDoc $ vcat $
199 [ "(in MSet ExplicitVarSizeWithFlags up 2)"
200 , "No value for:" <+> pretty (nameValues domain name)
201 , "When working on:" <+> pretty name
202 , "With domain:" <+> pretty domain
203 ] ++
204 ("Bindings in context:" : prettyContext ctxt)
205
206 symmetryOrdering :: TypeOf_SymmetryOrdering m
207 symmetryOrdering innerSO downX1 inp domain = do
208 [flags, values] <- downX1 inp
209 Just [_, (_, DomainMatrix index inner)] <- downD ("SO", domain)
210 (iPat, i) <- quantifiedVar
211 soValues <- innerSO downX1 [essence| &values[&i] |] inner
212 return
213 [essence|
214 [ ( -&flags[&i]
215 , &soValues
216 )
217 | &iPat : &index
218 ]
219 |]