never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Process.AttributeAsConstraints
4 ( attributeAsConstraints
5 , mkAttributeToConstraint
6 ) where
7
8 import Conjure.Prelude
9 import Conjure.Language.Definition
10 import Conjure.Language.Domain
11 import Conjure.Language.Domain.AddAttributes ( addAttributesToDomain )
12 import Conjure.Language.Expression.Op
13 import Conjure.Language.Pretty
14 import Conjure.Language.TH
15
16
17 -- | From the top level constraints, find the AACs and lift them to the domains of the declarations.
18 -- Complain for any remaining AACs.
19 attributeAsConstraints :: MonadFailDoc m => Model -> m Model
20 attributeAsConstraints m = do
21 let statements0 = mStatements m
22 statements1 <- transformBiM attributeAsConstraints_OnLocals statements0
23 statements2 <- attributeAsConstraints_OnStmts statements1
24 return m { mStatements = statements2 }
25
26
27 attributeAsConstraints_OnLocals :: MonadFailDoc m => Expression -> m Expression
28 attributeAsConstraints_OnLocals (WithLocals h (AuxiliaryVars locals)) =
29 WithLocals h . AuxiliaryVars <$> attributeAsConstraints_OnStmts locals
30 attributeAsConstraints_OnLocals x = return x
31
32
33 attributeAsConstraints_OnStmts :: MonadFailDoc m => [Statement] -> m [Statement]
34 attributeAsConstraints_OnStmts statements0 = do
35
36 -- collecting top level attribute-as-constraints
37 (statements1, topLevelAACs) <- runWriterT $ forM statements0 $ \ st -> case st of
38 Where xs -> do
39 xs1 <- fmap concat $ forM xs $ \ x -> case x of
40 Op (MkOpAttributeAsConstraint (OpAttributeAsConstraint (Reference nm _) attr val)) -> do
41 tell [(nm, attr, val)]
42 return []
43 _ -> return [x]
44 return [ Where xs1 | not (null xs1) ]
45 SuchThat xs -> do
46 xs1 <- fmap concat $ forM xs $ \ x -> case x of
47 Op (MkOpAttributeAsConstraint (OpAttributeAsConstraint (Reference nm _) attr val)) -> do
48 tell [(nm, attr, val)]
49 return []
50 _ -> return [x]
51 return [ SuchThat xs1 | not (null xs1) ]
52 _ -> return [st]
53
54 -- adding the top level attribute-as-constraints as attributes to the relevant domains
55 statements2 <- forM (concat statements1) $ \ st -> case st of
56 Declaration (FindOrGiven forg name domain) -> do
57 let newAttrs = [ (attr, val) | (nm, attr, val) <- topLevelAACs, name == nm ]
58 domain' <- addAttributesToDomain domain newAttrs
59 return (Declaration (FindOrGiven forg name domain'))
60 _ -> return st
61
62 return statements2
63
64
65 mkAttributeToConstraint
66 :: (NameGen m, MonadFailDoc m, Pretty r, Eq r)
67 => Domain r Expression -- the input domain
68 -> AttrName -- the name of the attribute
69 -> Maybe Expression -- the value for the attribute
70 -> Expression -- the input thing
71 -> m Expression -- the constraint
72
73 mkAttributeToConstraint domain attr mval x = do
74 gen <- attributeToConstraint domain attr mval
75 cons <- gen x
76 return cons
77
78 attributeToConstraint
79 :: (NameGen m, MonadFailDoc m, Pretty r, Eq r)
80 => Domain r Expression -- the input domain
81 -> AttrName -- the name of the attribute
82 -> Maybe Expression -- the value for the attribute
83 -> m (Expression -> m Expression) -- the constraint generator
84
85 attributeToConstraint domain@DomainSet{} = generator where
86 generator "size" (Just val) = return $ \ x -> return [essence| |&x| = &val |]
87 generator "minSize" (Just val) = return $ \ x -> return [essence| |&x| >= &val |]
88 generator "maxSize" (Just val) = return $ \ x -> return [essence| |&x| <= &val |]
89 generator attr _ =
90 failDoc $ vcat [ "Unsupported attribute:" <+> pretty attr
91 , "For the domain:" <+> pretty domain
92 ]
93
94 attributeToConstraint domain@DomainMSet{} = generator where
95 generator "size" (Just val) = return $ \ x -> return [essence| |&x| = &val |]
96 generator "minSize" (Just val) = return $ \ x -> return [essence| |&x| >= &val |]
97 generator "maxSize" (Just val) = return $ \ x -> return [essence| |&x| <= &val |]
98 generator "minOccur" (Just val) = return $ \ x -> do
99 (iPat, i) <- quantifiedVar
100 return [essence| forAll &iPat in &x . freq(&x,&i) >= &val |]
101 generator "maxOccur" (Just val) = return $ \ x -> do
102 (iPat, i) <- quantifiedVar
103 return [essence| forAll &iPat in &x . freq(&x,&i) <= &val |]
104 generator attr _ =
105 failDoc $ vcat [ "Unsupported attribute:" <+> pretty attr
106 , "For the domain:" <+> pretty domain
107 ]
108
109 attributeToConstraint domain@(DomainFunction _ _ inF inT) = generator where
110 generator "size" (Just val) = return $ \ x -> return [essence| |&x| = &val |]
111 generator "minSize" (Just val) = return $ \ x -> return [essence| |&x| >= &val |]
112 generator "maxSize" (Just val) = return $ \ x -> return [essence| |&x| <= &val |]
113 generator "total" Nothing = return $ \ x -> do
114 (iPat, i) <- quantifiedVar
115 return [essence| forAll &iPat : &inF . &i in defined(&x) |]
116 generator "injective" Nothing = return $ \ x -> do
117 (iPat, i) <- quantifiedVar
118 return [essence| allDiff([ &x(&i) | &iPat : &inF ]) |]
119 generator "surjective" Nothing = return $ \ x -> do
120 (iPat, i) <- quantifiedVar
121 return [essence| forAll &iPat : &inT . &i in range(&x) |]
122 generator "bijective" Nothing = return $ \ x -> do
123 a <- generator "injective" Nothing >>= \ gen -> gen x
124 b <- generator "injective" Nothing >>= \ gen -> gen x
125 return [essence| &a /\ &b |]
126 generator attr _ =
127 failDoc $ vcat [ "Unsupported attribute:" <+> pretty attr
128 , "For the domain:" <+> pretty domain
129 ]
130
131 attributeToConstraint domain@(DomainRelation _ _ [dom,dom2]) | dom == dom2 = generator where
132 generator "size" (Just val) = return $ \ x -> return [essence| |&x| = &val |]
133 generator "minSize" (Just val) = return $ \ x -> return [essence| |&x| >= &val |]
134 generator "maxSize" (Just val) = return $ \ x -> return [essence| |&x| <= &val |]
135
136 generator "reflexive" Nothing = return $ \ rel -> do
137 (xP, x) <- quantifiedVar
138 return [essence| forAll &xP : &dom . &rel(&x,&x) |]
139 generator "irreflexive" Nothing = return $ \ rel -> do
140 (xP, x) <- quantifiedVar
141 return [essence| forAll &xP : &dom . !(&rel(&x,&x)) |]
142 generator "coreflexive" Nothing = return $ \ rel -> do
143 (xP, x) <- quantifiedVar
144 (yP, y) <- quantifiedVar
145 return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) -> &x=&y |]
146 generator "symmetric" Nothing = return $ \ rel -> do
147 (xP, x) <- quantifiedVar
148 (yP, y) <- quantifiedVar
149 return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) -> &rel(&y,&x) |]
150 generator "antiSymmetric" Nothing = return $ \ rel -> do
151 (xP, x) <- quantifiedVar
152 (yP, y) <- quantifiedVar
153 return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) /\ &rel(&y,&x) -> &x=&y |]
154 generator "aSymmetric" Nothing = return $ \ rel -> do
155 (xP, x) <- quantifiedVar
156 (yP, y) <- quantifiedVar
157 return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) -> !(&rel(&y,&x)) |]
158 generator "transitive" Nothing = return $ \ rel -> do
159 (xP, x) <- quantifiedVar
160 (yP, y) <- quantifiedVar
161 (zP, z) <- quantifiedVar
162 return [essence| forAll &xP, &yP, &zP : &dom . &rel(&x,&y) /\ &rel(&y,&z) -> &rel(&x,&z) |]
163 generator "total" Nothing = return $ \ rel -> do
164 (xP, x) <- quantifiedVar
165 (yP, y) <- quantifiedVar
166 return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) \/ &rel(&y,&x) |]
167 generator "connex" Nothing = return $ \ rel -> do
168 (xP, x) <- quantifiedVar
169 (yP, y) <- quantifiedVar
170 return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) \/ &rel(&y,&x) \/ &x = &y |]
171 generator "Euclidean" Nothing = return $ \ rel -> do
172 (xP, x) <- quantifiedVar
173 (yP, y) <- quantifiedVar
174 (zP, z) <- quantifiedVar
175 return [essence| forAll &xP, &yP, &zP : &dom . &rel(&x,&y) /\ &rel(&x,&z) -> &rel(&y,&z) |]
176 generator "serial" Nothing = return $ \ rel -> do
177 (xP, x) <- quantifiedVar
178 (yP, y) <- quantifiedVar
179 return [essence| forAll &xP : &dom . exists &yP : &dom . &rel(&x,&y) |]
180 generator "equivalence" Nothing = return $ \ rel -> do
181 a <- generator "reflexive" Nothing >>= \ gen -> gen rel
182 b <- generator "symmetric" Nothing >>= \ gen -> gen rel
183 c <- generator "transitive" Nothing >>= \ gen -> gen rel
184 return [essence| &a /\ &b /\ &c |]
185 generator "partialOrder" Nothing = return $ \ rel -> do
186 a <- generator "reflexive" Nothing >>= \ gen -> gen rel
187 b <- generator "antiSymmetric" Nothing >>= \ gen -> gen rel
188 c <- generator "transitive" Nothing >>= \ gen -> gen rel
189 return [essence| &a /\ &b /\ &c |]
190 generator attr _ =
191 failDoc $ vcat [ "Unsupported attribute:" <+> pretty attr
192 , "For the domain:" <+> pretty domain
193 ]
194
195 attributeToConstraint domain@DomainRelation{} = generator where
196 generator "size" (Just val) = return $ \ x -> return [essence| |&x| = &val |]
197 generator "minSize" (Just val) = return $ \ x -> return [essence| |&x| >= &val |]
198 generator "maxSize" (Just val) = return $ \ x -> return [essence| |&x| <= &val |]
199 generator attr _ =
200 failDoc $ vcat [ "Unsupported attribute:" <+> pretty attr
201 , "For the domain:" <+> pretty domain
202 ]
203
204 attributeToConstraint domain@DomainPartition{} = generator where
205 generator "size" (Just val) = return $ \ x -> return [essence| |&x| = &val |]
206 generator "minSize" (Just val) = return $ \ x -> return [essence| |&x| >= &val |]
207 generator "maxSize" (Just val) = return $ \ x -> return [essence| |&x| <= &val |]
208 generator "numParts" (Just val) = return $ \ x -> return [essence| |parts(&x)| = &val |]
209 generator "minNumParts" (Just val) = return $ \ x -> return [essence| |parts(&x)| >= &val |]
210 generator "maxNumParts" (Just val) = return $ \ x -> return [essence| |parts(&x)| <= &val |]
211 generator "partSize" (Just val) = return $ \ x -> do
212 (iPat, i) <- quantifiedVar
213 return [essence| forAll &iPat in parts(&x) . |&i| = &val |]
214 generator "minPartSize" (Just val) = return $ \ x -> do
215 (iPat, i) <- quantifiedVar
216 return [essence| forAll &iPat in parts(&x) . |&i| >= &val |]
217 generator "maxPartSize" (Just val) = return $ \ x -> do
218 (iPat, i) <- quantifiedVar
219 return [essence| forAll &iPat in parts(&x) . |&i| <= &val |]
220 generator "regular" Nothing = return $ \ x -> do
221 (iPat, i) <- quantifiedVar
222 (jPat, j) <- quantifiedVar
223 return [essence| forAll &iPat, &jPat in parts(&x) . |&i| = |&j| |]
224 generator attr _ =
225 failDoc $ vcat [ "Unsupported attribute:" <+> pretty attr
226 , "For the domain:" <+> pretty domain
227 ]
228
229 attributeToConstraint domain = generator where
230 generator attr _ =
231 failDoc $ vcat [ "Unsupported attribute:" <+> pretty attr
232 , "For the domain:" <+> pretty domain
233 ]