never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Representations.Set.ExplicitVarSizeWithFlags ( setExplicitVarSizeWithFlags ) 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 setExplicitVarSizeWithFlags :: forall m . (MonadFailDoc m, NameGen m, EnumerateDomain m) => Representation m
16 setExplicitVarSizeWithFlags = Representation chck downD structuralCons downC up symmetryOrdering
17
18 where
19
20 chck :: TypeOf_ReprCheck m
21 chck _ (DomainSet _ (SetAttr SizeAttr_Size{}) _) = return []
22 chck f (DomainSet _ attrs innerDomain) =
23 map (DomainSet Set_ExplicitVarSizeWithFlags attrs) <$> f innerDomain
24 chck _ _ = return []
25
26 nameFlag = mkOutName (Just "Flags")
27 nameValues = mkOutName (Just "Values")
28
29 getMaxSize attrs innerDomain = case attrs of
30 SizeAttr_MaxSize x -> return x
31 SizeAttr_MinMaxSize _ x -> return x
32 _ -> reTag TagInt <$> domainSizeOf innerDomain
33
34
35 downD :: TypeOf_DownD m
36 downD (name, domain@(DomainSet _ (SetAttr attrs) innerDomain)) = do
37 maxSize <- getMaxSize attrs innerDomain
38 let indexDomain = mkDomainIntB 1 maxSize
39 return $ Just
40 [ ( nameFlag domain name
41 , DomainMatrix (forgetRepr indexDomain) DomainBool
42 )
43 , ( nameValues domain name
44 , DomainMatrix (forgetRepr indexDomain) innerDomain
45 )
46 ]
47 downD _ = na "{downD} ExplicitVarSizeWithFlags"
48
49 structuralCons :: TypeOf_Structural m
50 structuralCons f downX1 (DomainSet Set_ExplicitVarSizeWithFlags (SetAttr attrs) innerDomain) = do
51 maxSize <- getMaxSize attrs innerDomain
52 let
53 orderingWhenFlagged flags values = do
54 (iPat, i) <- quantifiedVar
55 return $ return $ -- list
56 [essence|
57 forAll &iPat : int(1..&maxSize-1) . &flags[&i+1] -> &values[&i] .< &values[&i+1]
58 |]
59
60 dontCareWhenNotFlagged flags values = do
61 (iPat, i) <- quantifiedVar
62 return $ return $ -- list
63 [essence|
64 forAll &iPat : int(1..&maxSize) . &flags[&i] = false -> dontCare(&values[&i])
65 |]
66
67 flagsToTheLeft flags = do
68 (iPat, i) <- quantifiedVar
69 return $ return $ -- list
70 [essence|
71 forAll &iPat : int(1..&maxSize-1) . &flags[&i+1] -> &flags[&i]
72 |]
73
74 cardinality flags = do
75 (iPat, i) <- quantifiedVar
76 return [essence| sum &iPat : int(1..&maxSize) . toInt(&flags[&i]) |]
77
78 innerStructuralCons flags values = do
79 (iPat, i) <- quantifiedVarOverDomain [essenceDomain| int(1..&maxSize) |]
80 let activeZone b = [essence| forAll &iPat : int(1..&maxSize) . &flags[&i] -> &b |]
81
82 -- preparing structural constraints for the inner guys
83 innerStructuralConsGen <- f innerDomain
84
85 let inLoop = [essence| &values[&i] |]
86 outs <- innerStructuralConsGen inLoop
87 return (map activeZone outs)
88
89 return $ \ set -> do
90 refs <- downX1 set
91 case refs of
92 [flags, values] ->
93 concat <$> sequence
94 [ orderingWhenFlagged flags values
95 , dontCareWhenNotFlagged flags values
96 , flagsToTheLeft flags
97 , mkSizeCons attrs <$> cardinality flags
98 , innerStructuralCons flags values
99 ]
100 _ -> na "{structuralCons} ExplicitVarSizeWithFlags"
101
102 structuralCons _ _ _ = na "{structuralCons} ExplicitVarSizeWithFlags"
103
104 downC :: TypeOf_DownC m
105 downC ( name
106 , domain@(DomainSet _ (SetAttr attrs) innerDomain)
107 , viewConstantSet -> Just constants
108 ) = do
109 maxSize <- getMaxSize attrs innerDomain
110 let indexDomain = mkDomainIntB 1 maxSize
111
112 maxSizeInt <-
113 case maxSize of
114 ConstantInt _ x -> return x
115 _ -> failDoc $ vcat
116 [ "Expecting an integer for the maxSize attribute."
117 , "But got:" <+> pretty maxSize
118 , "When working on:" <+> pretty name
119 , "With domain:" <+> pretty domain
120 ]
121 z <- zeroVal innerDomain
122 let zeroes = replicate (fromInteger (maxSizeInt - genericLength constants)) z
123
124 let trues = replicate (length constants) (ConstantBool True)
125 let falses = replicate (fromInteger (maxSizeInt - genericLength constants)) (ConstantBool False)
126
127 return $ Just
128 [ ( nameFlag domain name
129 , DomainMatrix
130 (forgetRepr indexDomain)
131 DomainBool
132 , ConstantAbstract $ AbsLitMatrix
133 (forgetRepr indexDomain)
134 (trues ++ falses)
135 )
136 , ( nameValues domain name
137 , DomainMatrix
138 (forgetRepr indexDomain)
139 innerDomain
140 , ConstantAbstract $ AbsLitMatrix
141 (forgetRepr indexDomain)
142 (constants ++ zeroes)
143 )
144 ]
145 downC _ = na "{downC} ExplicitVarSizeWithFlags"
146
147 up :: TypeOf_Up m
148 up ctxt (name, domain) =
149 case (lookup (nameFlag domain name) ctxt, lookup (nameValues domain name) ctxt) of
150 (Just flagMatrix, Just constantMatrix) ->
151 case viewConstantMatrix flagMatrix of
152 -- TODO: check if indices match
153 Just (_, flags) ->
154 case viewConstantMatrix constantMatrix of
155 Just (_, vals) ->
156 return (name, ConstantAbstract $ AbsLitSet
157 [ v
158 | (i,v) <- zip flags vals
159 , viewConstantBool i == Just True
160 ] )
161 _ -> failDoc $ vcat
162 [ "Expecting a matrix literal for:" <+> pretty (nameValues domain name)
163 , "But got:" <+> pretty constantMatrix
164 , "When working on:" <+> pretty name
165 , "With domain:" <+> pretty domain
166 ]
167 _ -> failDoc $ vcat
168 [ "Expecting a matrix literal for:" <+> pretty (nameFlag domain name)
169 , "But got:" <+> pretty flagMatrix
170 , "When working on:" <+> pretty name
171 , "With domain:" <+> pretty domain
172 ]
173 (Nothing, _) -> failDoc $ vcat $
174 [ "(in Set ExplicitVarSizeWithFlags up 1)"
175 , "No value for:" <+> pretty (nameFlag domain name)
176 , "When working on:" <+> pretty name
177 , "With domain:" <+> pretty domain
178 ] ++
179 ("Bindings in context:" : prettyContext ctxt)
180 (_, Nothing) -> failDoc $ vcat $
181 [ "(in Set ExplicitVarSizeWithFlags up 2)"
182 , "No value for:" <+> pretty (nameValues domain name)
183 , "When working on:" <+> pretty name
184 , "With domain:" <+> pretty domain
185 ] ++
186 ("Bindings in context:" : prettyContext ctxt)
187
188 symmetryOrdering :: TypeOf_SymmetryOrdering m
189 symmetryOrdering innerSO downX1 inp domain = do
190 [flags, values] <- downX1 inp
191 Just [_, (_, DomainMatrix index inner)] <- downD ("SO", domain)
192 (iPat, i) <- quantifiedVar
193 soValues <- innerSO downX1 [essence| &values[&i] |] inner
194 return
195 [essence|
196 [ (&flags[&i], &soValues) | &iPat : &index]
197 |]
198