never executed always true always false
1 {-# LANGUAGE Rank2Types #-}
2 {-# LANGUAGE RecordWildCards #-}
3 {-# LANGUAGE QuasiQuotes #-}
4
5 module Conjure.Representations.Partition.PartitionAsSet ( partitionAsSet ) where
6
7 -- conjure
8 import Conjure.Prelude
9 import Conjure.Language.Definition
10 import Conjure.Language.Constant
11 import Conjure.Language.Domain
12 import Conjure.Language.TH
13 import Conjure.Language.Pretty
14 import Conjure.Language.Type
15 import Conjure.Language.Expression.DomainSizeOf ( domainSizeOf )
16 import Conjure.Representations.Internal
17
18
19 partitionAsSet
20 :: forall m . (MonadFailDoc m, NameGen m, ?typeCheckerMode :: TypeCheckerMode)
21 => (forall x . DispatchFunction m x)
22 -> (forall r x . ReprOptionsFunction m r x)
23 -> Bool
24 -> Representation m
25 partitionAsSet dispatch reprOptions useLevels = Representation chck downD structuralCons downC up symmetryOrdering
26
27 where
28
29 chck :: TypeOf_ReprCheck m
30 chck _ dom1@(DomainPartition _ attrs _) = do
31 -- this is a "lookahead"
32 -- do the horizontal representation move: go from "partition of T" to "set of set of T"
33 -- do representation selection on the set
34 -- lookup the chosen representations and store them inside Partition_AsSet
35 dom2 <- outDomain_ dom1
36 dom3 <- reprOptions dom2
37 return [ DomainPartition (Partition_AsSet r1 r2) attrs innerDomain
38 | DomainSet r1 _ (DomainSet r2 _ innerDomain) <- dom3
39 -- special hack: do not use Set_ExplicitVarSizeWithFlags when --representation-levels=yes
40 , if useLevels
41 then r1 /= Set_ExplicitVarSizeWithFlags && r2 /= Set_ExplicitVarSizeWithFlags
42 else True
43 ]
44 chck _ _ = return []
45
46 outName :: Domain HasRepresentation x -> Name -> Name
47 outName = mkOutName Nothing
48
49 outDomain_ :: Pretty x => Domain () x -> m (Domain () x)
50 outDomain_ (DomainPartition () PartitionAttr{..} innerDomain) =
51 return (DomainSet () (SetAttr partsNum) (DomainSet () (SetAttr partsSize) innerDomain))
52 outDomain_ domain = na $ vcat [ "{outDomain_} PartitionAsSet"
53 , "domain:" <+> pretty domain
54 ]
55
56 outDomain :: Pretty x => Domain HasRepresentation x -> m (Domain HasRepresentation x)
57 outDomain (DomainPartition (Partition_AsSet repr1 repr2) PartitionAttr{..} innerDomain) =
58 return (DomainSet repr1 (SetAttr partsNum) (DomainSet repr2 (SetAttr partsSize) innerDomain))
59 outDomain domain = na $ vcat [ "{outDomain} PartitionAsSet"
60 , "domain:" <+> pretty domain
61 ]
62
63 downD :: TypeOf_DownD m
64 downD (name, inDom) = do
65 outDom <- outDomain inDom
66 return $ Just [ ( outName inDom name , outDom ) ]
67
68 structuralCons :: TypeOf_Structural m
69 structuralCons f downX1 inDom@(DomainPartition r attrs innerDomain) = return $ \ inpRel -> do
70 refs <- downX1 inpRel
71 let
72
73 fixedPartSize =
74 case attrs of
75 PartitionAttr _ SizeAttr_Size{} _ -> True
76 _ -> False
77
78 exactlyOnce :: Expression -> m [Expression]
79 exactlyOnce rel = do
80 innerType <- typeOfDomain innerDomain
81 let useAllDiff =
82 case r of
83 -- we use a sum when the inner set is occurrence
84 Partition_AsSet _ Set_Occurrence -> False
85 _ ->
86 case innerType of
87 TypeInt{} -> True
88 _ -> False -- or if the inner type is not int
89
90 (iPat, i) <- quantifiedVar
91 (jPat, j) <- quantifiedVar
92 if useAllDiff
93 then return $ return $ -- for list
94 [essence|
95 allDiff([ &j
96 | &iPat <- &rel
97 , &jPat <- &i
98 ])
99 |]
100 else return $ return $ -- for list
101 [essence|
102 forAll &iPat : &innerDomain .
103 1 = sum([ 1
104 | &jPat <- &rel
105 , &i in &j
106 ])
107 |]
108
109 regular :: Expression -> m [Expression]
110 regular rel | isRegular attrs && not fixedPartSize = do
111 (iPat, i) <- quantifiedVar
112 (jPat, j) <- quantifiedVar
113 return $ return -- for list
114 [essence|
115 and([ |&i| = |&j|
116 | &iPat <- &rel
117 , &jPat <- &rel
118 ])
119 |]
120 regular _ = return []
121
122 partsAren'tEmpty :: Expression -> m [Expression]
123 partsAren'tEmpty rel = do
124 (iPat, i) <- quantifiedVar
125 return $ return [essence| and([ |&i| >= 1 | &iPat <- &rel ]) |]
126
127 sumOfParts :: Expression -> m [Expression]
128 sumOfParts rel = do
129 case domainSizeOf innerDomain of
130 Left _err -> return []
131 Right n -> do
132 (iPat, i) <- quantifiedVar
133 return $ return [essence| &n = sum([ |&i| | &iPat <- &rel ]) |]
134
135 case refs of
136 [rel] -> do
137 outDom <- outDomain inDom
138 innerStructuralConsGen <- f outDom
139 concat <$> sequence
140 [ exactlyOnce rel
141 , regular rel
142 , partsAren'tEmpty rel
143 , innerStructuralConsGen rel
144 , sumOfParts rel
145 ]
146 _ -> na $ vcat [ "{structuralCons} PartitionAsSet"
147 , pretty inDom
148 ]
149 structuralCons _ _ domain = na $ vcat [ "{structuralCons} PartitionAsSet"
150 , "domain:" <+> pretty domain
151 ]
152
153 downC :: TypeOf_DownC m
154 downC ( name
155 , inDom
156 , viewConstantPartition -> Just vals
157 ) = do
158 outDom <- outDomain inDom
159 rDownC
160 (dispatch outDom)
161 ( outName inDom name
162 , outDom
163 , ConstantAbstract $ AbsLitSet $ map (ConstantAbstract . AbsLitSet) vals
164 )
165 downC (name, domain, constant) = na $ vcat [ "{downC} PartitionAsSet"
166 , "name:" <+> pretty name
167 , "domain:" <+> pretty domain
168 , "constant:" <+> pretty constant
169 ]
170
171 up :: TypeOf_Up m
172 up ctxt (name, domain@(DomainPartition Partition_AsSet{} _ _)) =
173 case lookup (outName domain name) ctxt of
174 Nothing -> failDoc $ vcat $
175 [ "(in PartitionAsSet up)"
176 , "No value for:" <+> pretty (outName domain name)
177 , "When working on:" <+> pretty name
178 , "With domain:" <+> pretty domain
179 ] ++
180 ("Bindings in context:" : prettyContext ctxt)
181 Just (viewConstantSet -> Just sets) -> do
182 let setOut (viewConstantSet -> Just xs) = return xs
183 setOut c = failDoc $ "Expecting a set, but got:" <++> pretty c
184 vals <- mapM setOut sets
185 return (name, ConstantAbstract (AbsLitPartition vals))
186 Just (ConstantUndefined msg ty) -> -- undefined propagates
187 return (name, ConstantUndefined ("PartitionAsSet " `mappend` msg) ty)
188 Just constant -> failDoc $ vcat $
189 [ "Incompatible value for:" <+> pretty (outName domain name)
190 , "When working on:" <+> pretty name
191 , "With domain:" <+> pretty domain
192 , "Expected a set value, but got:" <++> pretty constant
193 ] ++
194 ("Bindings in context:" : prettyContext ctxt)
195 up _ (name, domain) = na $ vcat [ "{up} PartitionAsSet"
196 , "name:" <+> pretty name
197 , "domain:" <+> pretty domain
198 ]
199
200 symmetryOrdering :: TypeOf_SymmetryOrdering m
201 symmetryOrdering innerSO downX1 inp domain = do
202 [inner] <- downX1 inp
203 Just [(_, innerDomain)] <- downD ("SO", domain)
204 innerSO downX1 inner innerDomain