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 values = do
96 (iPat, i) <- quantifiedVar
97 (jPat, j) <- quantifiedVar
98 return
99 [ [essence| forAll &iPat : &innerDomain . exists &jPat : int(1..&maxSize) . &flags[&j] >= &minOccur /\ &values[&j] = &i |]
100 | Just minOccur <- [getMinOccur attrs]
101 ]
102
103 innerStructuralCons flags values = do
104 (iPat, i) <- quantifiedVarOverDomain [essenceDomain| int(1..&maxSize) |]
105 let activeZone b = [essence| forAll &iPat : int(1..&maxSize) . &flags[&i] > 0 -> &b |]
106
107 -- preparing structural constraints for the inner guys
108 innerStructuralConsGen <- f innerDomain
109
110 let inLoop = [essence| &values[&i] |]
111 outs <- innerStructuralConsGen inLoop
112 return (map activeZone outs)
113
114 return $ \ mset -> do
115 refs <- downX1 mset
116 case refs of
117 [flags, values] ->
118 concat <$> sequence
119 [ orderingWhenFlagged flags values
120 , dontCareWhenNotFlagged flags values
121 , flagsToTheLeft flags
122 , minOccurrenceCons flags values
123 , mkSizeCons sizeAttrs <$> cardinality flags
124 , innerStructuralCons flags values
125 ]
126 _ -> na "{structuralCons} ExplicitVarSizeWithFlags"
127
128 structuralCons _ _ _ = na "{structuralCons} ExplicitVarSizeWithFlags"
129
130 downC :: TypeOf_DownC m
131 downC ( name
132 , domain@(DomainMSet _ attrs innerDomain)
133 , viewConstantMSet -> Just constants'
134 ) = do
135 maxSize <- getMaxSize attrs innerDomain
136 let indexDomain = mkDomainIntB 1 maxSize
137
138 let constants = histogram constants'
139
140 maxSizeInt <-
141 case maxSize of
142 ConstantInt _ x -> return x
143 _ -> failDoc $ vcat
144 [ "Expecting an integer for the maxSize attribute."
145 , "But got:" <+> pretty maxSize
146 , "When working on:" <+> pretty name
147 , "With domain:" <+> pretty domain
148 ]
149 z <- zeroVal innerDomain
150 let zeroes = replicate (fromInteger (maxSizeInt - genericLength constants)) z
151
152 let counts = map (ConstantInt TagInt . snd) constants
153 let falses = replicate (fromInteger (maxSizeInt - genericLength constants)) (ConstantInt TagInt 0)
154
155 return $ Just
156 [ ( nameFlag domain name
157 , DomainMatrix indexDomain DomainBool
158 , ConstantAbstract $ AbsLitMatrix indexDomain (counts ++ falses)
159 )
160 , ( nameValues domain name
161 , DomainMatrix indexDomain innerDomain
162 , ConstantAbstract $ AbsLitMatrix indexDomain (map fst constants ++ zeroes)
163 )
164 ]
165 downC _ = na "{downC} ExplicitVarSizeWithFlags"
166
167 up :: TypeOf_Up m
168 up ctxt (name, domain) =
169 case (lookup (nameFlag domain name) ctxt, lookup (nameValues domain name) ctxt) of
170 (Just flagMatrix, Just constantMatrix) ->
171 case viewConstantMatrix flagMatrix of
172 -- TODO: check if indices match
173 Just (_, flags) ->
174 case viewConstantMatrix constantMatrix of
175 Just (_, vals) ->
176 return (name, ConstantAbstract $ AbsLitMSet $ concat
177 [ replicate (fromInteger i) v
178 | (ConstantInt TagInt i,v) <- zip flags vals
179 ] )
180 _ -> failDoc $ vcat
181 [ "Expecting a matrix literal for:" <+> pretty (nameValues domain name)
182 , "But got:" <+> pretty constantMatrix
183 , "When working on:" <+> pretty name
184 , "With domain:" <+> pretty domain
185 ]
186 _ -> failDoc $ vcat
187 [ "Expecting a matrix literal for:" <+> pretty (nameFlag domain name)
188 , "But got:" <+> pretty flagMatrix
189 , "When working on:" <+> pretty name
190 , "With domain:" <+> pretty domain
191 ]
192 (Nothing, _) -> failDoc $ vcat $
193 [ "(in MSet ExplicitVarSizeWithFlags up 1)"
194 , "No value for:" <+> pretty (nameFlag domain name)
195 , "When working on:" <+> pretty name
196 , "With domain:" <+> pretty domain
197 ] ++
198 ("Bindings in context:" : prettyContext ctxt)
199 (_, Nothing) -> failDoc $ vcat $
200 [ "(in MSet ExplicitVarSizeWithFlags up 2)"
201 , "No value for:" <+> pretty (nameValues domain name)
202 , "When working on:" <+> pretty name
203 , "With domain:" <+> pretty domain
204 ] ++
205 ("Bindings in context:" : prettyContext ctxt)
206
207 symmetryOrdering :: TypeOf_SymmetryOrdering m
208 symmetryOrdering innerSO downX1 inp domain = do
209 [flags, values] <- downX1 inp
210 Just [_, (_, DomainMatrix index inner)] <- downD ("SO", domain)
211 (iPat, i) <- quantifiedVar
212 soValues <- innerSO downX1 [essence| &values[&i] |] inner
213 return
214 [essence|
215 [ ( -&flags[&i]
216 , &soValues
217 )
218 | &iPat : &index
219 ]
220 |]
221