never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Representations.Set.ExplicitVarSizeWithDummy ( setExplicitVarSizeWithDummy ) 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.Representations.Internal
12 import Conjure.Representations.Common
13
14
15 setExplicitVarSizeWithDummy :: forall m . (MonadFailDoc m, NameGen m) => Representation m
16 setExplicitVarSizeWithDummy = 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@DomainInt{}) =
23 map (DomainSet Set_ExplicitVarSizeWithDummy attrs) <$> f innerDomain
24 chck _ _ = return []
25
26 outName :: Domain HasRepresentation x -> Name -> Name
27 outName = mkOutName Nothing
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 calcDummyDomain :: Pretty r => Domain r Expression -> Domain r Expression
35 calcDummyDomain (DomainInt t [RangeBounded lb ub]) =
36 DomainInt t [RangeBounded lb [essence| &ub + 1 |]]
37 calcDummyDomain dom@(DomainInt t ranges) =
38 let dummyElem = calcDummyElem dom
39 in DomainInt t (ranges ++ [RangeSingle dummyElem])
40 calcDummyDomain dom = bug ("ExplicitVarSizeWithDummy.calcDummyDomain" <+> pretty dom)
41
42 calcDummyElem :: Pretty r => Domain r Expression -> Expression
43 calcDummyElem dom =
44 let theMax = bugFail "calcDummyElem: maxOfDomain" (maxOfDomain dom)
45 in [essence| &theMax + 1 |]
46
47 calcDummyElemC :: Pretty r => Domain r Constant -> Constant
48 calcDummyElemC (DomainInt _ []) = bug "ExplicitVarSizeWithDummy.calcDummyElemC []"
49 calcDummyElemC (DomainInt t rs) = ConstantInt t $
50 1 + maximum [ i
51 | r <- rs
52 , i <- case r of
53 RangeSingle (ConstantInt _ x) -> [x]
54 RangeBounded (ConstantInt _ x) (ConstantInt _ y) -> [x..y]
55 _ -> bug ("ExplicitVarSizeWithDummy.calcDummyElemC" <+> pretty r)
56 ]
57 calcDummyElemC d = bug ("ExplicitVarSizeWithDummy.calcDummyElemC" <+> pretty d)
58
59 downD :: TypeOf_DownD m
60 downD (name, domain@(DomainSet Set_ExplicitVarSizeWithDummy (SetAttr attrs) innerDomain@DomainInt{})) = do
61 let domainWithDummy = calcDummyDomain innerDomain
62 maxSize <- getMaxSize attrs innerDomain
63 return $ Just
64 [ ( outName domain name
65 , DomainMatrix
66 (DomainInt TagInt [RangeBounded 1 maxSize])
67 domainWithDummy
68 ) ]
69 downD _ = na "{downD} ExplicitVarSizeWithDummy"
70
71 structuralCons :: TypeOf_Structural m
72 structuralCons f downX1 (DomainSet Set_ExplicitVarSizeWithDummy (SetAttr attrs) innerDomain) = do
73 maxSize <- getMaxSize attrs innerDomain
74 let
75 dummyElem = calcDummyElem innerDomain
76
77 ordering m = do
78 (iPat, i) <- quantifiedVar
79 return $ return -- for list
80 [essence|
81 forAll &iPat : int(1..&maxSize-1) .
82 (&m[&i] .< &m[&i+1]) \/ (&m[&i] = &dummyElem)
83 |]
84
85 dummyToTheRight m = do
86 (iPat, i) <- quantifiedVar
87 return $ return -- for list
88 [essence|
89 forAll &iPat : int(1..&maxSize-1) .
90 (&m[&i] = &dummyElem) -> (&m[&i+1] = &dummyElem)
91 |]
92
93 cardinality m = do
94 (iPat, i) <- quantifiedVar
95 return [essence| sum &iPat : int(1..&maxSize) . toInt(&m[&i] != &dummyElem) |]
96
97 innerStructuralCons m = do
98 (iPat, i) <- quantifiedVarOverDomain [essenceDomain| int(1..&maxSize) |]
99 let activeZone b = [essence| forAll &iPat : int(1..&maxSize) . &m[&i] != &dummyElem -> &b |]
100
101 -- preparing structural constraints for the inner guys
102 innerStructuralConsGen <- f innerDomain
103
104 let inLoop = [essence| &m[&i] |]
105 outs <- innerStructuralConsGen inLoop
106 return (map activeZone outs)
107
108 return $ \ ref -> do
109 refs <- downX1 ref
110 case refs of
111 [m] ->
112 concat <$> sequence
113 [ ordering m
114 , dummyToTheRight m
115 , mkSizeCons attrs <$> cardinality m
116 , innerStructuralCons m
117 ]
118 _ -> na "{structuralCons} ExplicitVarSizeWithDummy"
119 structuralCons _ _ _ = na "{structuralCons} ExplicitVarSizeWithDummy"
120
121 downC :: TypeOf_DownC m
122 downC ( name
123 , domain@(DomainSet Set_ExplicitVarSizeWithDummy (SetAttr attrs) innerDomain)
124 , viewConstantSet -> Just constants
125 ) = do
126 maxSize <- getMaxSize attrs innerDomain
127 let indexDomain i = mkDomainIntB (fromInt i) maxSize
128 maxSizeInt <-
129 case maxSize of
130 ConstantInt _ x -> return x
131 _ -> failDoc $ vcat
132 [ "Expecting an integer for the maxSize attribute."
133 , "But got:" <+> pretty maxSize
134 , "When working on:" <+> pretty name
135 , "With domain:" <+> pretty domain
136 ]
137 let dummyElem = calcDummyElemC innerDomain
138 let dummies = replicate (fromInteger (maxSizeInt - genericLength constants)) dummyElem
139 return $ Just
140 [ ( outName domain name
141 , DomainMatrix (indexDomain 1) innerDomain
142 , ConstantAbstract $ AbsLitMatrix (indexDomain 1) (constants ++ dummies)
143 )
144 ]
145 downC _ = na "{downC} ExplicitVarSizeWithDummy"
146
147 up :: TypeOf_Up m
148 up ctxt (name, domain@(DomainSet Set_ExplicitVarSizeWithDummy _ innerDomain)) = do
149 let dummyElem = calcDummyElemC innerDomain
150 case lookup (outName domain name) ctxt of
151 Nothing -> failDoc $ vcat $
152 [ "(in Set ExplicitVarSizeWithDummy up)"
153 , "No value for:" <+> pretty (outName domain name)
154 , "When working on:" <+> pretty name
155 , "With domain:" <+> pretty domain
156 ] ++
157 ("Bindings in context:" : prettyContext ctxt)
158 Just constant ->
159 case viewConstantMatrix constant of
160 Just (_, vals) ->
161 return (name, ConstantAbstract (AbsLitSet [ v | v <- vals, v /= dummyElem ]))
162 _ -> failDoc $ vcat
163 [ "Expecting a matrix literal for:" <+> pretty (outName domain name)
164 , "But got:" <+> pretty constant
165 , "When working on:" <+> pretty name
166 , "With domain:" <+> pretty domain
167 ]
168 up _ _ = na "{up} ExplicitVarSizeWithDummy"
169
170 symmetryOrdering :: TypeOf_SymmetryOrdering m
171 symmetryOrdering innerSO downX1 inp domain = do
172 [inner] <- downX1 inp
173 Just [(_, innerDomain)] <- downD ("SO", domain)
174 innerSO downX1 inner innerDomain
175