never executed always true always false
1 {-
2 - Module : Conjure.Process.Boost
3 - Description : Strengthen a model using type- and domain-inference.
4 - Copyright : Billy Brown 2017
5 - License : BSD3
6
7 Processing step that attempts to strengthen an Essence model, using methods described in the "Reformulating Essence Specifications for Robustness" paper.
8 -}
9
10 {-# LANGUAGE QuasiQuotes #-}
11
12 module Conjure.Process.Boost ( boost ) where
13
14 import Data.List ( find, union )
15 import Data.Map.Strict ( Map )
16 import qualified Data.Map.Strict as M ( (!?), empty, union )
17
18 import Conjure.Prelude
19 import Conjure.Language
20 import Conjure.Language.Domain.AddAttributes
21 import Conjure.Language.NameResolution ( resolveNames )
22 -- These two are needed together
23 import Conjure.Language.Expression.DomainSizeOf ()
24 import Conjure.Language.DomainSizeOf ( domainSizeOf )
25 import Conjure.Compute.DomainOf ( domainOf )
26 import Conjure.UI.Model ( evaluateModel )
27 import Conjure.UI.VarSymBreaking ( outputVarSymBreaking )
28 import Conjure.Process.Enumerate ( EnumerateDomain )
29
30
31 -- aeson
32 import qualified Data.Aeson as JSON ( decodeStrict )
33 -- shelly
34 import Shelly ( run )
35 -- directory
36 import System.Directory ( removeFile )
37 -- text
38 import qualified Data.Text.Encoding as T ( encodeUtf8 )
39 -- uniplate zipper
40 import Data.Generics.Uniplate.Zipper ( Zipper, zipper, down, fromZipper, hole, replaceHole, right, up )
41
42
43 type ExpressionZ = Zipper Expression Expression
44 type FindVar = (Name, Domain () Expression)
45 type AttrPair = (AttrName, Maybe Expression)
46 type ToAddToRem = ([ExpressionZ], [ExpressionZ])
47
48 -- | Strengthen a model using type- and domain-inference.
49 boost ::
50 MonadFailDoc m =>
51 MonadIO m =>
52 MonadLog m =>
53 MonadUserError m =>
54 NameGen m =>
55 EnumerateDomain m =>
56 (?typeCheckerMode :: TypeCheckerMode) =>
57 LogLevel -> -- ^ Log level to use.
58 Bool -> -- ^ Generate logs for rule applications.
59 Model -> -- ^ Model to strengthen.
60 m Model -- ^ Strengthened model.
61 boost logLevel logRuleSuccesses = resolveNames >=> return . fixRelationProj >=> core
62 where
63 -- core :: ... => Model -> m Model
64 core model1 = do
65 -- Apply attribute rules to each decision (find) variable
66 (model2, toAddToRem) <- foldM (\modelAndToKeep findAndCstrs@((n, d), _) ->
67 foldM (\(m1, tatr1) (rule, name) -> do
68 (attrs, tatr2) <- nested rule m1 findAndCstrs
69 let m2 = foldr (uncurry3 addAttrsToModel) m1 attrs
70 when (((not (null attrs) && m1 /= m2) ||
71 (tatr2 /= mempty && toAddRem tatr2 tatr1 /= tatr1)) &&
72 logRuleSuccesses)
73 (log logLevel $ name <+> if null attrs
74 then vcat $ map (pretty . hole) (fst tatr2)
75 else pretty n <+> ":" <+> pretty d)
76 return (m2, toAddRem tatr2 tatr1))
77 modelAndToKeep [ (surjectiveIsTotalBijective, "function marked total and bijective")
78 , (totalInjectiveIsBijective, "function marked bijective")
79 , (definedForAllIsTotal, "function marked total")
80 , (diffArgResultIsInjective, "function marked injective")
81 , (varSize, "added or refined domain size attribute")
82 , (setSize, "added or refined set domain size attribute")
83 , (mSetSizeOccur, "added or refined multiset occurrence attribute")
84 , (mSetOccur, "added or refined multiset occurrence attribute")
85 , (partRegular, "marked partition regular")
86 , (numPartsToAttr, "added or refined partition domain numParts attribute")
87 , (partSizeToAttr, "added or refined partition domain partSize attribute")
88 , (funcRangeEqSet, "equated function range and set")
89 , (forAllIneqToIneqSum, "lifted arithmetic relation from two forAlls to a sum")
90 , (fasterIteration, "refined distinctness condition on forAll")
91 ])
92 (model1, ([], []))
93 (zip (collectFindVariables model1)
94 (repeat $ map zipper $ collectConstraints model1))
95
96 -- Apply constraint additions and removals
97 model3' <- resolveNames $
98 addConstraints (fst toAddToRem) $
99 remConstraints (snd toAddToRem) model2
100 model3 <- evaluateModel model3'
101
102 -- Apply type change rules to each decision (find) variable
103 (model4, toAddToRem') <- foldM (\modelAndToKeep findAndCstrs@((n, d), _) ->
104 foldM (\(m1, tatr1) (rule, name) -> do
105 let dCur = fromMaybe d (lookup n (collectFindVariables m1))
106 (dom, tatr2) <- rule m1 ((n, dCur), snd findAndCstrs)
107 when ((dom /= dCur || toAddRem tatr2 tatr1 /= tatr1) &&
108 logRuleSuccesses)
109 (log logLevel $ name <+> pretty n <+> ":" <+> pretty dCur)
110 return (updateDecl (n, dom) m1, toAddRem tatr2 tatr1))
111 modelAndToKeep [ (mSetToSet, "multiset changed to set")
112 , (partialBijectiveToInverse, "partial bijective function inverted")
113 , (relationToSizedSetFunction, "relation changed to function with fixed-size set codomain")
114 ])
115 (model3, ([], []))
116 (zip (collectFindVariables model3)
117 (repeat $ map zipper $ collectConstraints model3))
118
119 -- Apply constraint additions and removals
120 model5' <- resolveNames $
121 addConstraints (fst toAddToRem') $
122 remConstraints (snd toAddToRem') model4
123 model5 <- evaluateModel model5'
124
125 -- Make another pass if the model was updated, but stop if it contains machine names
126 if model1 == model5 || any containsMachineName (collectConstraints model5)
127 then return model5
128 else core model5
129 -- Does an expression contain a reference with a machine name?
130 containsMachineName = any isMachineName . universe
131 isMachineName (Reference MachineName{} _) = True
132 isMachineName _ = False
133
134 -- | 'uncurry' for functions of three arguments and triples.
135 uncurry3 :: (a -> b -> c -> d) -> ((a, b, c) -> d)
136 uncurry3 f (x, y, z) = f x y z
137
138 -- | Collect decision (find) variables from a model, returning their name and domain.
139 collectFindVariables :: Model -> [FindVar]
140 collectFindVariables = mapMaybe collectFind . mStatements
141 where
142 collectFind (Declaration (FindOrGiven Find n d)) = Just (n, d)
143 collectFind _ = Nothing
144
145 -- | Collect the constraints in a model.
146 collectConstraints :: Model -> [Expression]
147 collectConstraints = concatMap getSuchThat . mStatements
148 where
149 getSuchThat (SuchThat cs) = cs
150 getSuchThat _ = []
151
152 -- | Add constraints to a model.
153 addConstraints :: [ExpressionZ] -> Model -> Model
154 addConstraints [] m = m
155 addConstraints cs m@Model { mStatements = stmts }
156 = m { mStatements = addConstraints' stmts }
157 where
158 addConstraints' (SuchThat cs':ss) = SuchThat (cs' `union` map fromZipper cs) : ss
159 addConstraints' (s:ss) = s : addConstraints' ss
160 addConstraints' [] = [SuchThat (map fromZipper cs)]
161
162 -- | Remove a list of constraints from a model.
163 remConstraints :: [ExpressionZ] -> Model -> Model
164 remConstraints cs m@Model { mStatements = stmts }
165 = m { mStatements = filter (not . emptySuchThat) $ map remConstraints' stmts }
166 where
167 remConstraints' (SuchThat cs') = SuchThat $ filter (`notElem` map fromZipper cs) cs'
168 remConstraints' s = s
169 emptySuchThat (SuchThat []) = True
170 emptySuchThat _ = False
171
172 -- | Update the domain of a declaration in a model.
173 updateDecl :: FindVar -> Model -> Model
174 updateDecl (n, d) m@Model { mStatements = stmts } = m { mStatements = map updateDecl' stmts }
175 where
176 updateDecl' (Declaration (FindOrGiven Find n' _))
177 | n == n' = Declaration (FindOrGiven Find n d)
178 updateDecl' decl = decl
179
180 -- | Try adding an attribute at a given depth of a variable's domain, in a model.
181 addAttrsToModel :: FindVar -> Int -> [AttrPair] -> Model -> Model
182 addAttrsToModel (n, _) depth attrs m
183 = let d = snd <$> find (\(n', _) -> n == n') (collectFindVariables m)
184 in case d >>= flip (addAttrsToDomain depth) attrs of
185 Just d' -> updateDecl (n, d') m
186 Nothing -> m
187 where
188 addAttrsToDomain :: (MonadFailDoc m) => Int -> Domain () Expression -> [AttrPair] -> m (Domain () Expression)
189 addAttrsToDomain 0 dom = addAttributesToDomain dom . map mkAttr
190 addAttrsToDomain level (DomainSet r as inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainSet r as)
191 addAttrsToDomain level (DomainMSet r as inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainMSet r as)
192 addAttrsToDomain level (DomainMatrix index inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainMatrix index)
193 addAttrsToDomain level (DomainFunction r as from inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainFunction r as from)
194 addAttrsToDomain level (DomainSequence r as inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainSequence r as)
195 addAttrsToDomain level (DomainPartition r as inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainPartition r as)
196 addAttrsToDomain _ _ = const (failDoc "[addAttrsToDomain] not a supported nested domain")
197 -- Special treatment for functions
198 mkAttr (attr, Just [essence| image(&f, &_) |]) = (attr, Just [essence| max(range(&f)) |])
199 mkAttr (attr, Just [essence| image(&f, &_) - 1 |]) = (attr, Just [essence| max(range(&f)) - 1 |])
200 mkAttr (attr, Just [essence| image(&f, &_) + 1 |]) = (attr, Just [essence| max(range(&f)) + 1 |])
201 mkAttr (attr, e') = (attr, e')
202
203 -- | Does an expression directly reference a given name variable?
204 nameExpEq :: Name -> Expression -> Bool
205 nameExpEq n (Reference n' _) = n == n'
206 nameExpEq n [essence| image(&f, &x) |] = nameExpEq n f || nameExpEq n x
207 nameExpEq n [essence| &f(&x) |] = nameExpEq n f || nameExpEq n x
208 nameExpEq n [essence| defined(&f) |] = nameExpEq n f
209 nameExpEq n [essence| range(&f) |] = nameExpEq n f
210 nameExpEq n [essence| |&x| |] = nameExpEq n x
211 nameExpEq _ _ = False
212
213 -- | Does a reference refer to an abstract pattern?
214 refersTo :: Expression -> AbstractPattern -> Bool
215 refersTo (Reference n _) a = n `elem` namesFromAbstractPattern a
216 refersTo _ _ = False
217
218 -- | Get a single name from an abstract pattern.
219 nameFromAbstractPattern :: (MonadFailDoc m) => AbstractPattern -> m Name
220 nameFromAbstractPattern a = case namesFromAbstractPattern a of
221 [n] -> pure n
222 [] -> failDoc "[nameFromAbstractPattern] no names in abstract pattern"
223 _ -> failDoc "[nameFromAbstractPattern] more than one name in abstract pattern"
224
225 -- | Get the list of names from an abstract pattern.
226 namesFromAbstractPattern :: AbstractPattern -> [Name]
227 namesFromAbstractPattern (Single n) = [n]
228 namesFromAbstractPattern (AbsPatTuple ns) = concatMap namesFromAbstractPattern ns
229 namesFromAbstractPattern (AbsPatMatrix ns) = concatMap namesFromAbstractPattern ns
230 namesFromAbstractPattern (AbsPatSet ns) = concatMap namesFromAbstractPattern ns
231 namesFromAbstractPattern _ = []
232
233 -- | Get the list of names from a generator.
234 namesFromGenerator :: Generator -> [Name]
235 namesFromGenerator (GenDomainNoRepr a _) = namesFromAbstractPattern a
236 namesFromGenerator (GenDomainHasRepr n _) = [n]
237 namesFromGenerator (GenInExpr a _) = namesFromAbstractPattern a
238
239 -- | Find an expression at any depth of unconditional forAll expressions.
240 findInUncondForAll :: (Expression -> Bool) -> [ExpressionZ] -> [Expression]
241 findInUncondForAll p = map hole . findInUncondForAllZ p
242
243 -- | Find an expression at any depth of unconditional forAll expressions,
244 -- returning a Zipper containing the expression's context.
245 findInUncondForAllZ :: (Expression -> Bool) -> [ExpressionZ] -> [ExpressionZ]
246 findInUncondForAllZ p = concatMap findInForAll
247 where
248 findInForAll z | p (hole z) = [z]
249 findInForAll z
250 = case hole z of
251 [essence| forAll &_ in defined(&_) . &_ |]
252 -> []
253 [essence| forAll &x, &y : &_, &x' != &y' . &_ |]
254 | x' `refersTo` x && y' `refersTo` y
255 -> maybe [] findInForAll (down z >>= down)
256 [essence| forAll &x, &y in &_, &x' != &y' . &_ |]
257 | x' `refersTo` x && y' `refersTo` y
258 -> maybe [] findInForAll (down z >>= down)
259 Op (MkOpAnd (OpAnd (Comprehension _ gorcs)))
260 | all (not . isCondition) gorcs
261 -> maybe [] findInForAll (down z >>= down)
262 [essence| &_ /\ &_ |]
263 -> maybe [] findInForAll (down z)
264 `union`
265 maybe [] findInForAll (right z >>= down)
266 -- Only accept OR cases if both sides contain a match
267 [essence| &_ \/ &_ |]
268 -> let leftResult = maybe [] findInForAll (down z)
269 rightResult = maybe [] findInForAll (right z >>= down)
270 in if not (null leftResult) && not (null rightResult)
271 then leftResult `union` rightResult
272 else []
273 _ -> []
274 isCondition Condition{} = True
275 isCondition _ = False
276
277 -- | Lens function over a binary expression.
278 type BinExprLens m = Proxy m -> (Expression -> Expression -> Expression,
279 Expression -> m (Expression, Expression))
280
281 -- | Get the lens for an expression and the values it matches.
282 matching :: Expression
283 -> [(BinExprLens Maybe, a)]
284 -> Maybe (a, (Expression, Expression))
285 matching e ops = case mapMaybe (\(f1, f2) -> (,) f2 <$> match f1 e) ops of
286 [x] -> pure x
287 _ -> failDoc $ "no matching operator for expression:" <+> pretty e
288
289 -- | (In)equality operator lens pairs.
290 ineqOps :: [(BinExprLens Maybe, BinExprLens Identity)]
291 ineqOps = [ (opEq, opEq)
292 , (opLt, opLt)
293 , (opLeq, opLeq)
294 , (opGt, opGt)
295 , (opGeq, opGeq)
296 ]
297
298 -- | Opposites of (in)equality operator lens pairs.
299 oppIneqOps :: [(BinExprLens Maybe, BinExprLens Identity)]
300 oppIneqOps = [ (opEq, opEq)
301 , (opLt, opGt)
302 , (opLeq, opGeq)
303 , (opGt, opLt)
304 , (opGeq, opLeq)
305 ]
306
307 -- | (In)equality operator to size attribute modifier pairs.
308 ineqSizeAttrs :: [(BinExprLens Maybe, (AttrName, Expression -> Maybe Expression))]
309 ineqSizeAttrs = [ (opEq, ("size", Just))
310 , (opLt, ("maxSize", Just . \x -> x - 1))
311 , (opLeq, ("maxSize", Just))
312 , (opGt, ("minSize", Just . (+ 1)))
313 , (opGeq, ("minSize", Just))
314 ]
315
316 -- | (In)equality operator to size attribute modifier pairs.
317 ineqOccurAttrs :: [(BinExprLens Maybe, [(AttrName, Expression -> Maybe Expression)])]
318 ineqOccurAttrs = [ (opEq, [ ("minOccur", Just), ("maxOccur", Just) ])
319 , (opLt, [ ("maxOccur", Just . \x -> x - 1) ])
320 , (opLeq, [ ("maxOccur", Just) ])
321 , (opGt, [ ("minOccur", Just . (+ 1)) ])
322 , (opGeq, [ ("minOccur", Just) ])
323 ]
324
325 -- | Unzip where the key is a 'Maybe' but the values should all be combined.
326 unzipMaybeK :: Monoid m => [(Maybe a, m)] -> ([a], m)
327 unzipMaybeK = foldr (\(mx, y) (xs, z) ->
328 case mx of
329 Just x -> (x:xs, y `mappend` z)
330 Nothing -> ( xs, y `mappend` z))
331 ([], mempty)
332
333 -- | Does an expression contain a find variable?
334 isFind :: Expression -> Bool
335 isFind (Reference _ (Just (DeclNoRepr Find _ _ _))) = True
336 isFind (Reference _ (Just (DeclHasRepr Find _ _))) = True
337 isFind Reference{} = False
338 isFind Constant{} = False
339 isFind [essence| &f(&_) |] = isFind f
340 isFind [essence| image(&f, &_) |] = isFind f
341 isFind e = any isFind $ children e
342
343 -- | Add expressions to the ToAdd list.
344 toAdd :: [ExpressionZ] -> ToAddToRem -> ToAddToRem
345 toAdd e = first (`union` e)
346
347 -- | Add expressions to the ToRemove list.
348 toRem :: [ExpressionZ] -> ToAddToRem -> ToAddToRem
349 toRem e = second (`union` e)
350
351 -- | Combine two 'ToAddToRem' values.
352 toAddRem :: ToAddToRem -> ToAddToRem -> ToAddToRem
353 toAddRem (ta, tr) = toAdd ta . toRem tr
354
355 -- | Apply a rule to arbitrary levels of nested domains.
356 nested :: (MonadFailDoc m, MonadLog m, NameGen m, ?typeCheckerMode :: TypeCheckerMode)
357 => (Model -> (FindVar, [ExpressionZ])
358 -> m ([AttrPair], ToAddToRem))
359 -> Model
360 -> (FindVar, [ExpressionZ])
361 -> m ([(FindVar, Int, [AttrPair])], ToAddToRem)
362 nested rule m fc@(fv, cs) = do
363 -- Apply the rule at the top level
364 (attrs, toAddToRem) <- rule m fc
365 -- Look deeper into the domain if possible, for forAll constraints involving it
366 nestedResults <- fmap mconcat $ forM cs $ \c ->
367 case hole c of
368 [essence| forAll &x in &gen . &_ |] | nameExpEq (fst fv) gen ->
369 -- Create the new decision variable at this level
370 case (,) <$> nameFromAbstractPattern x
371 <*> (domainOf gen >>= innerDomainOf) of
372 Left _ -> return mempty
373 Right fv' -> do
374 -- Apply the rule from here
375 out <- nested rule m (fv', mapMaybe (down >=> down) [c])
376 case out of
377 ([], _) -> return mempty
378 -- The rule was applied, so unwrap the variable and increase the depth
379 (vs, tatr') -> return ( [ (fv, d + 1, as) | (_, d, as) <- vs ]
380 , tatr')
381 _ -> return mempty
382 -- Do not add a modification if there are no attributes
383 let attrs' = if null attrs then [] else [(fv, 0, attrs)]
384 return $ mappend nestedResults (attrs', toAddToRem)
385
386 -- | If a function is surjective or bijective, and its domain and codomain
387 -- are of equal size, then it is total and bijective.
388 surjectiveIsTotalBijective :: (MonadFailDoc m, MonadLog m)
389 => Model
390 -> (FindVar, [ExpressionZ])
391 -> m ([AttrPair], ToAddToRem)
392 surjectiveIsTotalBijective _ ((_, dom), _)
393 = case dom of
394 DomainFunction _ (FunctionAttr _ p j) from to
395 | (p == PartialityAttr_Partial && j == JectivityAttr_Bijective) ||
396 j == JectivityAttr_Surjective -> do
397 (fromSize, toSize) <- functionDomainSizes from to
398 if fromSize == toSize
399 then return ([("total", Nothing), ("bijective", Nothing)], mempty)
400 else return mempty
401 DomainSequence _ (SequenceAttr (SizeAttr_Size s ) j) to
402 | j `elem` [JectivityAttr_Bijective, JectivityAttr_Surjective] -> do
403 toSize <- domainSizeOf to
404 if s == toSize
405 then return ([("bijective", Nothing)], mempty)
406 else return mempty
407 _ -> return mempty
408
409 -- | Calculate the sizes of the domain and codomain of a function.
410 functionDomainSizes :: (MonadFailDoc m)
411 => Domain () Expression -- ^ The function's domain.
412 -> Domain () Expression -- ^ The function's codomain.
413 -> m (Expression, Expression) -- ^ The sizes of the two.
414 functionDomainSizes from to = (,) <$> domainSizeOf from <*> domainSizeOf to
415
416 -- | If a function is total and injective, and its domain and codomain
417 -- are of equal size, then it is bijective.
418 totalInjectiveIsBijective :: (MonadFailDoc m, MonadLog m)
419 => Model
420 -> (FindVar, [ExpressionZ])
421 -> m ([AttrPair], ToAddToRem)
422 totalInjectiveIsBijective _ ((_, dom), _)
423 = case dom of
424 DomainFunction _ (FunctionAttr _ PartialityAttr_Total JectivityAttr_Injective) from to -> do
425 (fromSize, toSize) <- functionDomainSizes from to
426 if fromSize == toSize
427 then return ([("bijective", Nothing)], mempty)
428 else return mempty
429 _ -> return mempty
430
431 -- | If a function is defined for all values in its domain, then it is total.
432 definedForAllIsTotal :: (MonadFailDoc m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
433 => Model
434 -> (FindVar, [ExpressionZ])
435 -> m ([AttrPair], ToAddToRem)
436 definedForAllIsTotal _ ((n, dom), cs)
437 -- Is the function called with parameters generated from its domain in an expression?
438 = let definedIn from e = any (funcCalledWithGenParams from) (children e)
439 in case dom of
440 DomainFunction _ (FunctionAttr _ PartialityAttr_Partial _) from _
441 | any (definedIn from) $ findInUncondForAll isOp cs
442 -> return ([("total", Nothing)], mempty)
443 _ -> return mempty
444 where
445 -- Look for operator expressions but leave comprehensions, ANDs and ORs up to findInUncondForAll
446 isOp (Op (MkOpAnd (OpAnd Comprehension{}))) = False
447 isOp [essence| &_ /\ &_ |] = False
448 isOp [essence| &_ \/ &_ |] = False
449 -- Disallow implications which may remove some cases
450 isOp [essence| &_ -> &_ |] = False
451 isOp Op{} = True
452 isOp _ = False
453 -- Determine whether a function is called with values generated from its domain
454 funcCalledWithGenParams d [essence| image(&f, ¶m) |]
455 = nameExpEq n f && case domainOf param of
456 Right d' -> d' == d
457 Left _ -> False
458 funcCalledWithGenParams _ _ = False
459
460 -- | If all distinct inputs to a function have distinct results, then it is injective.
461 -- It will also be total if there are no conditions other than the disequality between
462 -- the two inputs.
463 diffArgResultIsInjective :: (MonadFailDoc m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
464 => Model
465 -> (FindVar, [ExpressionZ])
466 -> m ([AttrPair], ToAddToRem)
467 diffArgResultIsInjective _ ((n, DomainFunction _ (FunctionAttr _ _ ject) from _), cs)
468 | (ject == JectivityAttr_None || ject == JectivityAttr_Surjective) &&
469 not (null $ findInUncondForAll isDistinctDisequality cs)
470 -- It is known that no inputs are ignored
471 = return ([("injective", Nothing), ("total", Nothing)], mempty)
472 where
473 -- Match a very specific pattern, which will also add the total attribute
474 isDistinctDisequality [essence| &i != &j -> image(&f, &i') != image(&f', &j') |]
475 = f == f' && i == i' && j == j' &&
476 nameExpEq n f && -- the function is the one under consideration
477 domIsGen i && domIsGen j -- the values are generated from the function's domain
478 isDistinctDisequality _ = False
479 domIsGen x = case domainOf x of
480 Right dom -> dom == from
481 Left _ -> False
482 diffArgResultIsInjective _ _ = return mempty
483
484 -- | Set a size attribute on a variable.
485 varSize :: (MonadFailDoc m, MonadLog m)
486 => Model
487 -> (FindVar, [ExpressionZ])
488 -> m ([AttrPair], ToAddToRem)
489 varSize _ ((n, _), cs) = do
490 results <- forM cs $ \c ->
491 case matching (hole c) ineqSizeAttrs of
492 -- Do not allow find variables to be put in attributes
493 Just ((attr, f), (cardinalityOf -> Just x, e)) | nameExpEq n x && not (isFind e)
494 -> pure (Just (attr, f e), ([], [c]))
495 _ -> pure (Nothing, mempty)
496 return $ unzipMaybeK results
497
498
499 cardinalityOf :: Expression -> Maybe Expression
500 cardinalityOf [essence| |&x| |] = Just x
501 cardinalityOf [essence| sum([1 | &_ <- &x]) |] = Just x
502 cardinalityOf _ = Nothing
503
504
505 -- | Set the minimum size of a set based on it being a superset of another.
506 setSize :: (MonadFailDoc m, MonadLog m, NameGen m, ?typeCheckerMode :: TypeCheckerMode)
507 => Model
508 -> (FindVar, [ExpressionZ])
509 -> m ([AttrPair], ToAddToRem)
510 setSize _ ((n, DomainSet{}), cs)
511 = fmap mconcat $ forM (findInUncondForAllZ isSubSupSet cs) $ \c ->
512 case hole c of
513 -- subset(Eq)
514 [essence| &l subset &r |] | nameExpEq n r -> return (minSize l (+ 1), mempty)
515 [essence| &l subset &r |] | nameExpEq n l -> return (maxSize r (\x -> x - 1), mempty)
516 [essence| &l subsetEq &r |] | nameExpEq n r -> return (minSize l id, mempty)
517 [essence| &l subsetEq &r |] | nameExpEq n l -> return (maxSize r id, mempty)
518 -- supset(Eq)
519 [essence| &l supset &r |] | nameExpEq n l -> return (minSize r (+ 1), mempty)
520 [essence| &l supset &r |] | nameExpEq n r -> return (maxSize l (\x -> x - 1), mempty)
521 [essence| &l supsetEq &r |] | nameExpEq n l -> return (minSize r id, mempty)
522 [essence| &l supsetEq &r |] | nameExpEq n r -> return (maxSize l id, mempty)
523 _ -> return mempty
524 where
525 isSubSupSet [essence| &_ subset &_ |] = True
526 isSubSupSet [essence| &_ subsetEq &_ |] = True
527 isSubSupSet [essence| &_ supset &_ |] = True
528 isSubSupSet [essence| &_ supsetEq &_ |] = True
529 isSubSupSet _ = False
530 minSize [essence| defined(&g) |] f
531 = case domainOf g of
532 Right (DomainFunction _ (FunctionAttr _ PartialityAttr_Total _) from _) ->
533 case domainSizeOf from of
534 Just s -> [("minSize", Just (f s))]
535 Nothing -> mempty
536 _ -> mempty
537 minSize [essence| range(&g) |] f
538 = case domainOf g of
539 Right (DomainFunction _ (FunctionAttr _ PartialityAttr_Total j) from to)
540 | j == JectivityAttr_Bijective || j == JectivityAttr_Surjective ->
541 case domainSizeOf to of
542 Just s -> [("minSize", Just (f s))]
543 Nothing -> mempty
544 | j == JectivityAttr_Injective ->
545 case domainSizeOf from of
546 Just s -> [("minSize", Just (f s))]
547 Nothing -> mempty
548 | otherwise -> [("minSize", Just (f 1))]
549 _ -> mempty
550 minSize e f = case domainOf e of
551 Right (DomainSet _ (SetAttr (SizeAttr_Size mn)) _) ->
552 [("minSize", Just (f mn))]
553 Right (DomainSet _ (SetAttr (SizeAttr_MinSize mn)) _) ->
554 [("minSize", Just (f mn))]
555 Right (DomainSet _ (SetAttr (SizeAttr_MinMaxSize mn _)) _) ->
556 [("minSize", Just (f mn))]
557 _ -> mempty
558 -- TODO: extend for Matrix, MSet, Partition and Sequence
559 maxSize [essence| defined(&g) |] f
560 = case domainOf g >>= innerDomainOf of
561 Right (DomainTuple [d, _]) ->
562 case domainSizeOf d of
563 Just s -> [("maxSize", Just (f s))]
564 Nothing -> mempty
565 _ -> mempty
566 maxSize [essence| range(&g) |] f
567 = case domainOf g >>= innerDomainOf of
568 Right (DomainTuple [_, d]) ->
569 case domainSizeOf d of
570 Just s -> [("maxSize", Just (f s))]
571 Nothing -> mempty
572 _ -> mempty
573 maxSize e f = case domainOf e of
574 Right (DomainSet _ (SetAttr (SizeAttr_Size mx)) _) ->
575 [("maxSize", Just (f mx))]
576 Right (DomainSet _ (SetAttr (SizeAttr_MaxSize mx)) _) ->
577 [("maxSize", Just (f mx))]
578 Right (DomainSet _ (SetAttr (SizeAttr_MinMaxSize _ mx)) _) ->
579 [("maxSize", Just (f mx))]
580 Right d@(DomainSet _ (SetAttr SizeAttr_None) _) ->
581 case domainSizeOf d of
582 Just mx -> [("maxSize", Just (f mx))]
583 Nothing -> mempty
584 _ -> mempty
585 -- TODO: extend for Matrix, MSet, Partition and Sequence
586 setSize _ _ = return mempty
587
588 -- | The maxSize, and minOccur attributes of an mset affect its maxOccur and minSize attributes.
589 mSetSizeOccur :: (MonadFailDoc m, MonadLog m)
590 => Model
591 -> (FindVar, [ExpressionZ])
592 -> m ([AttrPair], ToAddToRem)
593 mSetSizeOccur _ ((_, d), _)
594 = case d of
595 -- Ordering is important here, as there is a rule that applies
596 -- to maxSize and minOccur, but none that applies to minSize
597 -- and maxOccur. size uses the maxSize rule, but can ignore a
598 -- minOccur because it cannot have its minSize changed.
599 -- size -> maxOccur
600 DomainMSet _ (MSetAttr (SizeAttr_Size mx) _) _
601 -> return ([("maxOccur", Just mx)], mempty)
602 -- minOccur -> minSize
603 DomainMSet _ (MSetAttr _ (OccurAttr_MinOccur mn)) _
604 -> return ([("minSize", Just mn)], mempty)
605 DomainMSet _ (MSetAttr _ (OccurAttr_MinMaxOccur mn _)) _
606 -> return ([("minSize", Just mn)], mempty)
607 -- maxSize -> maxOccur
608 DomainMSet _ (MSetAttr (SizeAttr_MaxSize mx) _) _
609 -> return ([("maxOccur", Just mx)], mempty)
610 DomainMSet _ (MSetAttr (SizeAttr_MinMaxSize _ mx) _) _
611 -> return ([("maxOccur", Just mx)], mempty)
612 _ -> return mempty
613
614 -- | Infer multiset occurrence attributes from constraints.
615 mSetOccur :: (MonadFailDoc m, MonadLog m)
616 => Model
617 -> (FindVar, [ExpressionZ])
618 -> m ([AttrPair], ToAddToRem)
619 mSetOccur _ ((n, DomainMSet _ _ d), cs)
620 = return $ mconcat $ flip mapMaybe (findInUncondForAllZ (not . null . isFreq) cs) $ \e ->
621 case isFreq (hole e) of
622 [] -> Nothing
623 -- Only remove constraints if they are all used up.
624 -- Because freq(a, b) = c adds two attributes, removing constraints
625 -- in an AND expression cannot work, in the case of freq(a, b) = c /\ e
626 -- because there are two attributes and two terms, but term e may not
627 -- be removed.
628 as -> let tattr = case hole e of
629 AbstractLiteral AbsLitMatrix{} -> mempty
630 _ -> ([], [e])
631 in Just (as, tattr)
632 where
633 isFreq :: Expression -> [AttrPair]
634 isFreq (AbstractLiteral (AbsLitMatrix _ es)) = concatMap isFreq es
635 isFreq e = case matching e oppIneqOps of
636 Just (_, ([essence| freq(&x, &v) |], e'))
637 | valid x v e' -> case matching e ineqOccurAttrs of
638 Just (as, _) -> map (second ($ e')) as
639 Nothing -> []
640 -- Flip the terms
641 Just (oper, (l, r@[essence| freq(&x, &v) |]))
642 | valid x v l -> isFreq $ make oper r l
643 _ -> []
644 -- Make sure that the expression's components are valid
645 valid :: Expression -> Expression -> Expression -> Bool
646 valid x v e = nameExpEq n x && isGen v && isConst e
647 -- Make sure that the value is generated from the mset's domain
648 isGen (Reference _ (Just (InComprehension (GenDomainNoRepr _ d')))) = d == d'
649 isGen (Reference _ (Just (DeclNoRepr Quantified _ d' _))) = d == d'
650 isGen (Reference _ (Just (InComprehension (GenInExpr _ e )))) = nameExpEq n e
651 isGen _ = False
652 -- Make sure that the mset is being equated to a constant
653 isConst (Reference _ (Just (DeclNoRepr Given _ _ _))) = True
654 isConst (Constant ConstantInt{}) = True
655 isConst _ = False
656 mSetOccur _ _ = return mempty
657
658 -- | Mark a partition regular if there is a constraint on its parts constraining them to be of equal size.
659 partRegular :: (MonadFailDoc m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
660 => Model
661 -> (FindVar, [ExpressionZ])
662 -> m ([AttrPair], ToAddToRem)
663 partRegular _ ((_, DomainPartition{}), cs) = do
664 attrs <- forM cs $ \c ->
665 case hole c of
666 -- [essence| forAll &x in parts(&p) . forAll &y in parts(&p') . &xCard = &yCard |]
667 [essence| and([ &xCard = &yCard | &x <- parts(&p), &y <- parts(&p') ]) |]
668 | Just (Reference x' _) <- cardinalityOf xCard
669 , Just (Reference y' _) <- cardinalityOf yCard
670 , or [ and [x == Single x', y == Single y']
671 , and [x == Single y', y == Single x']
672 ]
673 , p == p'
674 -> pure (Just ("regular", Nothing), ([], [c]))
675 _ -> pure (Nothing, mempty)
676 return $ unzipMaybeK attrs
677 partRegular _ _ = return mempty
678
679
680 -- | Convert constraints acting on the number of parts in a partition to an attribute.
681 numPartsToAttr :: (MonadFailDoc m, MonadLog m)
682 => Model
683 -> (FindVar, [ExpressionZ])
684 -> m ([AttrPair], ToAddToRem)
685 numPartsToAttr _ ((n, DomainPartition{}), cs) = do
686 attrs <- forM cs $ \c ->
687 case matching (hole c) ineqSizeAttrs of
688 -- Do not allow find variables to be put in attributes
689 Just ((attr, f), ([essence| |parts(&x)| |], e)) | nameExpEq n x && not (isFind e)
690 -> pure (Just (changeAttr attr, f e), ([], [c]))
691 _ -> pure (Nothing, mempty)
692 return $ unzipMaybeK attrs
693 where
694 -- Change a size attribute name to a numParts attribute name
695 changeAttr "size" = "numParts"
696 changeAttr "minSize" = "minNumParts"
697 changeAttr "maxSize" = "maxNumParts"
698 changeAttr a = a
699 numPartsToAttr _ _ = return mempty
700
701 -- | Convert constraints acting on the sizes of parts in a partition to an attribute.
702 partSizeToAttr :: (MonadFailDoc m, MonadLog m)
703 => Model
704 -> (FindVar, [ExpressionZ])
705 -> m ([AttrPair], ToAddToRem)
706 partSizeToAttr _ ((n, DomainPartition{}), cs) = do
707 attrs <- forM cs $ \c ->
708 case hole c of
709 [essence| forAll &x in parts(&p) . &xCard = &e |]
710 | Just x' <- cardinalityOf xCard
711 , valid p x x' e
712 -> pure (Just ("partSize", Just e), ([], [c]))
713 [essence| forAll &x in parts(&p) . &xCard < &e |]
714 | Just x' <- cardinalityOf xCard
715 , valid p x x' e
716 -> pure (Just ("maxPartSize", Just (e - 1)), ([], [c]))
717 [essence| forAll &x in parts(&p) . &xCard <= &e |]
718 | Just x' <- cardinalityOf xCard
719 , valid p x x' e
720 -> pure (Just ("maxPartSize", Just e), ([], [c]))
721 [essence| forAll &x in parts(&p) . &xCard > &e |]
722 | Just x' <- cardinalityOf xCard
723 , valid p x x' e
724 -> pure (Just ("minPartSize", Just (e + 1)), ([], [c]))
725 [essence| forAll &x in parts(&p) . &xCard >= &e |]
726 | Just x' <- cardinalityOf xCard
727 , valid p x x' e
728 -> pure (Just ("minPartSize", Just e), ([], [c]))
729 _ -> pure (Nothing, mempty)
730 return $ unzipMaybeK attrs
731 where
732 -- Make sure that the expression's components are valid
733 valid :: Expression -> AbstractPattern -> Expression -> Expression -> Bool
734 valid p x v e = nameExpEq n p && v `refersTo` x && not (isFind e)
735 partSizeToAttr _ _ = return mempty
736
737 -- | Equate the range of a function to a set of the former is a subset of the latter
738 -- and all values in the set are results of the function.
739 funcRangeEqSet :: (MonadFailDoc m, MonadLog m)
740 => Model
741 -> (FindVar, [ExpressionZ])
742 -> m ([AttrPair], ToAddToRem)
743 funcRangeEqSet _ ((n, DomainSet{}), cs)
744 -- Get references to the set and the function whose range it is a superset of
745 = let funcSubsets = mapMaybe funcSubsetEqOf $
746 findInUncondForAllZ (isJust . funcSubsetEqOf . zipper) cs
747 -- Reduce the functions to those whose values are equated to the values in the set
748 fsToUse = flip filter funcSubsets $ \(_, f) ->
749 not $ null $ findInUncondForAll (funcValEqSetVal (hole f)) cs
750 -- Transform the functions into new constraints, preserving structure
751 csToAdd = flip mapMaybe fsToUse $ \(s, f) ->
752 let f' = hole f
753 in replaceHole [essence| range(&f') = &s |] <$>
754 (up f >>= up)
755 in return ([], (csToAdd, []))
756 where
757 -- Get the function whose range is a subsetEq of the set
758 funcSubsetEqOf z = case hole z of
759 [essence| range(&_) subsetEq &s |] | nameExpEq n s
760 -> (,) s <$> (down z >>= down)
761 [essence| &s supsetEq range(&_) |] | nameExpEq n s
762 -> (,) s <$> (down z >>= right >>= down)
763 _ -> Nothing
764 -- Are the values of the function equal to the values of the set?
765 funcValEqSetVal f [essence| forAll &x in &s . image(&f', &_) = &x' |]
766 = nameExpEq n s && f == f' && x' `refersTo` x
767 funcValEqSetVal f [essence| forAll &x in &s . &x' = image(&f', &_) |]
768 = nameExpEq n s && f == f' && x' `refersTo` x
769 funcValEqSetVal _ _ = False
770 funcRangeEqSet _ _ = return mempty
771
772
773 -- | An (in)equality in a forAll implies that the (in)equality also applies to
774 -- the sums of both terms.
775 forAllIneqToIneqSum :: (MonadFailDoc m, MonadLog m, NameGen m, ?typeCheckerMode :: TypeCheckerMode)
776 => Model
777 -> (FindVar, [ExpressionZ])
778 -> m ([AttrPair], ToAddToRem)
779 forAllIneqToIneqSum _ (_, cs) = do
780 let matches = mapMaybe matchParts $ findInUncondForAllZ (isJust . matchParts . zipper) cs
781 csToAdd <- mapMaybe mkConstraint <$> filterM partsAreNumeric matches
782 return ([], (csToAdd, []))
783 where
784 -- Match and extract the desired parts of the expression
785 matchParts :: ExpressionZ -> Maybe (Generator, Maybe ExpressionZ, Expression, Expression)
786 matchParts z = case hole z of
787 Op (MkOpAnd (OpAnd (Comprehension e [Generator g])))
788 -> matching e ineqOps >>=
789 uncurry (matchComponents g z) . snd
790 _ -> Nothing
791 -- Match the components of the expression of interest
792 matchComponents :: Generator -> ExpressionZ -> Expression -> Expression
793 -> Maybe (Generator, Maybe ExpressionZ, Expression, Expression)
794 matchComponents g z e1 e2
795 | refInExpr (namesFromGenerator g) e1 && refInExpr (namesFromGenerator g) e2
796 = Just (g, down z >>= down, e1, e2)
797 matchComponents _ _ _ _ = Nothing
798 -- Is a name referred to in an expression?
799 refInExpr names = any (\e -> any (`nameExpEq` e) names) . universe
800 -- Are the parts of the matched expression numeric?
801 partsAreNumeric (_, _, e1, e2) = (&&) <$> domainIsNumeric e1 <*> domainIsNumeric e2
802 domainIsNumeric e = case domainOf e of
803 Right DomainInt{} -> return True
804 Right (DomainAny _ (TypeInt _)) -> return True
805 _ -> return False
806 -- Replace the forAll with the (in)equality between sums
807 mkConstraint :: (Generator, Maybe ExpressionZ, Expression, Expression) -> Maybe ExpressionZ
808 mkConstraint (gen, Just z, _, _)
809 -- Use matching with ineqOps to get the operation that is used on the two expressions
810 = case matching (hole z) ineqOps of
811 Just (f, (e1, e2))
812 -> let mkSumOf = Op . MkOpSum . OpSum . flip Comprehension [Generator gen]
813 -- Two steps to get out of the forAll, and replace it with the constraint
814 in replaceHole (make f (mkSumOf e1) (mkSumOf e2)) <$> (up z >>= up)
815 _ -> Nothing
816 mkConstraint _ = Nothing
817
818 -- | Iterate slightly faster over a domain if generating two distinct variables.
819 fasterIteration :: (MonadFailDoc m, MonadFailDoc m,MonadIO m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
820 => Model
821 -> (FindVar, [ExpressionZ])
822 -> m ([AttrPair], ToAddToRem)
823 fasterIteration m (_, cs) = do
824 let iters = findInUncondForAllZ (isJust . doubleDistinctIter . zipper) cs
825 fmap ((,) [] . mconcat) $ forM iters $ \z -> do
826 -- Find the equivalent variables
827 [equivs] <- sequence [ findEquivVars (hole z) ]
828 -- Only apply to equivalent variables and make the new constraint
829 case doubleDistinctIter z >>= onlyEquivalent equivs >>= changeIterator of
830 Nothing -> return mempty
831 -- Remove the old constraint
832 Just z' -> return ([z'], [z])
833 where
834 -- Match the elemenents of interest in the constraint
835 doubleDistinctIter z
836 = case hole z of
837 Op (MkOpAnd (OpAnd (Comprehension _ [ Generator (GenInExpr x v)
838 , Generator (GenInExpr y v')
839 , Condition [essence| &x' != &y' |]
840 ])))
841 | v == v' && x' `refersTo` x && y' `refersTo` y
842 -> Just ((x, x'), (y, y'), v, down z >>= down)
843 Op (MkOpAnd (OpAnd (Comprehension _ [ Generator (GenDomainNoRepr x d)
844 , Generator (GenDomainNoRepr y d')
845 , Condition [essence| &x' != &y' |]
846 ])))
847 | d == d' && x' `refersTo` x && y' `refersTo` y
848 -> Just ((x, x'), (y, y'), Domain d, down z >>= down)
849 _ -> Nothing
850 -- Find which variables are equivalent in an expression
851 findEquivVars :: (MonadIO m) => Expression -> m (Map Text Text)
852 findEquivVars e = case e of
853 [essence| forAll &_, &_ : &_, &_ . &e' |] -> liftIO $ findSyms e'
854 [essence| forAll &_, &_ in &_, &_ . &e' |] -> liftIO $ findSyms e'
855 _ -> return M.empty
856 -- Find the symmetries in an expression
857 findSyms :: Expression -> IO (Map Text Text)
858 findSyms e = do
859 let m' = addConstraints [zipper e] $ remConstraints cs m
860 let filename = ".tmp-variable-strengthening.json"
861 outputVarSymBreaking filename m'
862 symmetries <- ferret $ stringToText filename
863 removeFile filename
864 case (JSON.decodeStrict $ T.encodeUtf8 symmetries) :: Maybe [Map Text Text] of
865 Nothing -> return M.empty
866 Just ss -> return $ foldr M.union M.empty ss
867 -- Only perform the modification if the variables are equivalent in the expression
868 onlyEquivalent es v@((x, _), (y, _), _, _)
869 = case namesFromAbstractPattern x of
870 [Name nx] -> case namesFromAbstractPattern y of
871 [Name ny] -> case es M.!? nx of
872 Just ny' | ny == ny' -> Just v
873 _ -> Nothing
874 _ -> Nothing
875 _ -> Nothing
876 -- Change the iterator to use the new, faster notation
877 changeIterator ((x, x'), (y, y'), v, Just z)
878 = let e = hole z
879 in case v of
880 r@Reference{}
881 -> case domainOf r of
882 Left _ -> Nothing
883 Right DomainSet{}
884 -> replaceHole [essence| forAll {&x, &y} subsetEq &v . &e |] <$>
885 (up z >>= up)
886 Right _
887 -> replaceHole [essence| forAll &x, &y in &v, &y' > &x' . &e |] <$>
888 (up z >>= up)
889 Op MkOpDefined{}
890 -> replaceHole [essence| forAll &x, &y in &v, &y' > &x' . &e |] <$>
891 (up z >>= up)
892 Domain d
893 -> replaceHole [essence| forAll &x, &y : &d, &y' > &x' . &e |] <$>
894 (up z >>= up)
895 _ -> Nothing
896 changeIterator _ = Nothing
897
898 -- | Call ferret's symmetry detection on a JSON file
899 ferret :: Text -> IO Text
900 ferret path = sh (run "symmetry_detect" [ "--json", path ]) `catch`
901 (\(_ :: SomeException) -> return "{}")
902
903 -- | Change the type of a multiset with `maxOccur 1` to set.
904 mSetToSet :: (MonadFailDoc m, MonadLog m)
905 => Model
906 -> (FindVar, [ExpressionZ])
907 -> m (Domain () Expression, ToAddToRem)
908 mSetToSet _ ((n, DomainMSet r (MSetAttr sa oa) d), cs) | maxOccur1 oa = do
909 let dom' = DomainSet r (SetAttr sa) d
910 let torem = filter (any (nameExpEq n) . universe . hole) cs
911 let toadd = map (zipper . transform (\e -> if nameExpEq n e
912 then [essence| toMSet(&e) |]
913 else e)
914 . hole)
915 cs
916 return (dom', (toadd, torem))
917 where
918 maxOccur1 (OccurAttr_MaxOccur 1) = True
919 maxOccur1 (OccurAttr_MinMaxOccur _ 1) = True
920 maxOccur1 _ = False
921 mSetToSet _ ((_, dom), _) = return (dom, mempty)
922
923 -- | Invert a partial bijective function into a total injective function.
924 -- Constraints are translated to preserve meaning where possible.
925 partialBijectiveToInverse :: (MonadFailDoc m, MonadLog m)
926 => Model
927 -> (FindVar, [ExpressionZ])
928 -> m (Domain () Expression, ToAddToRem)
929 partialBijectiveToInverse _ (((n, dom@(DomainFunction r (FunctionAttr _ PartialityAttr_Partial JectivityAttr_Bijective) from to)), cs)) = do
930 let relatedConstraints = filter (any (nameExpEq n) . universe . hole) cs
931 case mapM (rewriteInvertedFunctionConstraint n . hole) relatedConstraints of
932 Just rewritten
933 | all (not . hasUnsupportedInverseUse n) rewritten ->
934 let dom' = DomainFunction r
935 (FunctionAttr SizeAttr_None PartialityAttr_Total JectivityAttr_Injective)
936 to
937 from
938 in return (dom', (map zipper rewritten, relatedConstraints))
939 _ -> return (dom, mempty)
940 partialBijectiveToInverse _ ((_, dom), _) = return (dom, mempty)
941
942 -- | Rewrite a constraint to use the inverse function.
943 rewriteInvertedFunctionConstraint :: Name -> Expression -> Maybe Expression
944 rewriteInvertedFunctionConstraint n c = Just $ transform rewrite c
945 where
946 rewrite [essence| preImage(&f, &y) = &s |]
947 | nameExpEq n f
948 , Just x <- singletonSetElement s
949 = [essence| image(&f, &y) = &x |]
950 rewrite [essence| &s = preImage(&f, &y) |]
951 | nameExpEq n f
952 , Just x <- singletonSetElement s
953 = [essence| image(&f, &y) = &x |]
954 rewrite [essence| &x in preImage(&f, &y) |]
955 | nameExpEq n f
956 = [essence| image(&f, &y) = &x |]
957 rewrite [essence| image(&f, &x) = &y |]
958 | nameExpEq n f
959 = [essence| image(&f, &y) = &x |]
960 rewrite [essence| &y = image(&f, &x) |]
961 | nameExpEq n f
962 = [essence| image(&f, &y) = &x |]
963 rewrite [essence| &f(&x) = &y |]
964 | nameExpEq n f
965 = [essence| &f(&y) = &x |]
966 rewrite [essence| &y = &f(&x) |]
967 | nameExpEq n f
968 = [essence| &f(&y) = &x |]
969 rewrite e = e
970
971 -- | A singleton set expression: {x} or toSet([x]).
972 singletonSetElement :: Expression -> Maybe Expression
973 singletonSetElement [essence| {&x} |] = Just x
974 singletonSetElement [essence| toSet([&x]) |] = Just x
975 singletonSetElement _ = Nothing
976
977 -- | Check if an expression still contains unsupported occurrences of a function
978 -- that has been inverted.
979 hasUnsupportedInverseUse :: Name -> Expression -> Bool
980 hasUnsupportedInverseUse n [essence| image(&f, &x) = &y |] | nameExpEq n f
981 = hasUnsupportedInverseUse n x || hasUnsupportedInverseUse n y
982 hasUnsupportedInverseUse n [essence| &y = image(&f, &x) |] | nameExpEq n f
983 = hasUnsupportedInverseUse n x || hasUnsupportedInverseUse n y
984 hasUnsupportedInverseUse n [essence| &f(&x) = &y |] | nameExpEq n f
985 = hasUnsupportedInverseUse n x || hasUnsupportedInverseUse n y
986 hasUnsupportedInverseUse n [essence| &y = &f(&x) |] | nameExpEq n f
987 = hasUnsupportedInverseUse n x || hasUnsupportedInverseUse n y
988 hasUnsupportedInverseUse n [essence| preImage(&f, &_) |] | nameExpEq n f = True
989 hasUnsupportedInverseUse n [essence| image(&f, &_) |] | nameExpEq n f = True
990 hasUnsupportedInverseUse n [essence| &f(&_) |] | nameExpEq n f = True
991 hasUnsupportedInverseUse n (Reference n' _) = n == n'
992 hasUnsupportedInverseUse n e = any (hasUnsupportedInverseUse n) (children e)
993
994 -- | Change a binary relation into a total function to a fixed-size set,
995 -- when each value in the first component is constrained to have the same
996 -- number of related second-component values.
997 relationToSizedSetFunction :: (MonadFailDoc m, MonadLog m, NameGen m)
998 => Model
999 -> (FindVar, [ExpressionZ])
1000 -> m (Domain () Expression, ToAddToRem)
1001 relationToSizedSetFunction _ ((n, dom@(DomainRelation r relAttrs [from, to])), cs) = do
1002 let RelationAttr relSizeAttr _ = relAttrs
1003 let relatedConstraints = filter (any (nameExpEq n) . universe . hole) cs
1004 let cardinalityCs = mapMaybe (matchCardinalityConstraint n) relatedConstraints
1005 case nub [k | (k, _) <- cardinalityCs] of
1006 [k] | not (null cardinalityCs) ->
1007 do compatible <- relationAttrsCompatible relAttrs from k
1008 let edgeCs = mapMaybe (matchEdgeDisjointnessConstraint n) relatedConstraints
1009 let matchedCs = map snd cardinalityCs `union` map snd edgeCs
1010 let unmatched = filter (`notElem` matchedCs) relatedConstraints
1011 let dom' = DomainFunction r
1012 (FunctionAttr SizeAttr_None PartialityAttr_Total JectivityAttr_None)
1013 from
1014 (DomainSet def (SetAttr (SizeAttr_Size k)) to)
1015 case mapM (rewriteRelationConstraint n . hole) unmatched of
1016 Nothing -> return (dom, mempty)
1017 Just rewrittenUnmatched
1018 | compatible -> do
1019 edgeAdds <- mapM (fmap zipper . mkEdgeDisjointConstraint n . fst) edgeCs
1020 sizeAdds <- map zipper <$> relationSizeConstraints n from relSizeAttr
1021 let toadd = edgeAdds `union` sizeAdds `union` map zipper rewrittenUnmatched
1022 return (dom', (toadd, relatedConstraints))
1023 | otherwise -> return (dom, mempty)
1024 _ -> return (dom, mempty)
1025 relationToSizedSetFunction _ ((_, dom), _) = return (dom, mempty)
1026
1027 -- | The relation attributes must be representable by the target function form.
1028 relationAttrsCompatible :: MonadFailDoc m
1029 => RelationAttr Expression
1030 -> Domain () Expression
1031 -> Expression
1032 -> m Bool
1033 relationAttrsCompatible (RelationAttr _ binRelAttrs) _from _k
1034 | binRelAttrs /= def = return False
1035 | otherwise = return True
1036
1037 -- | Preserve relation size attributes as explicit constraints after type change.
1038 relationSizeConstraints :: NameGen m
1039 => Name
1040 -> Domain () Expression
1041 -> SizeAttr Expression
1042 -> m [Expression]
1043 relationSizeConstraints _ _ SizeAttr_None = return []
1044 relationSizeConstraints n from sa = do
1045 (uP, u) <- quantifiedVar
1046 let f = fromName n
1047 let totalSize = [essence| sum([ |&f(&u)| | &uP : &from ]) |]
1048 return $
1049 case sa of
1050 SizeAttr_Size s -> [[essence| &totalSize = &s |]]
1051 SizeAttr_MinSize s -> [[essence| &totalSize >= &s |]]
1052 SizeAttr_MaxSize s -> [[essence| &totalSize <= &s |]]
1053 SizeAttr_MinMaxSize lo hi -> [ [essence| &totalSize >= &lo |]
1054 , [essence| &totalSize <= &hi |]
1055 ]
1056
1057 -- | Match a fixed-cardinality-per-first-component constraint for a binary relation.
1058 matchCardinalityConstraint :: Name -> ExpressionZ -> Maybe (Expression, ExpressionZ)
1059 matchCardinalityConstraint n z = matchSumCard <|> matchSumMembership <|> matchProjCard
1060 where
1061 matchSumCard =
1062 case hole z of
1063 [essence| and([ &k = sum([toInt(&lhs = &u') | &ca <- &rel]) | &u : &_ ]) |]
1064 | nameExpEq n rel
1065 , tupleFirstOf lhs ca
1066 , u' `refersTo` u
1067 , validCardinalityExpr k
1068 -> Just (k, z)
1069 [essence| and([ sum([toInt(&lhs = &u') | &ca <- &rel]) = &k | &u : &_ ]) |]
1070 | nameExpEq n rel
1071 , tupleFirstOf lhs ca
1072 , u' `refersTo` u
1073 , validCardinalityExpr k
1074 -> Just (k, z)
1075 _ -> Nothing
1076 matchSumMembership =
1077 case hole z of
1078 [essence| and([ sum([toInt((&u', &v') in &rel) | &v : &_ ]) = &k | &u : &_ ]) |]
1079 | nameExpEq n rel
1080 , u' `refersTo` u
1081 , v' `refersTo` v
1082 , validCardinalityExpr k
1083 -> Just (k, z)
1084 [essence| and([ &k = sum([toInt((&u', &v') in &rel) | &v : &_ ]) | &u : &_ ]) |]
1085 | nameExpEq n rel
1086 , u' `refersTo` u
1087 , v' `refersTo` v
1088 , validCardinalityExpr k
1089 -> Just (k, z)
1090 [essence| and([ sum([toInt(tuple(&u', &v') in &rel) | &v : &_ ]) = &k | &u : &_ ]) |]
1091 | nameExpEq n rel
1092 , u' `refersTo` u
1093 , v' `refersTo` v
1094 , validCardinalityExpr k
1095 -> Just (k, z)
1096 [essence| and([ &k = sum([toInt(tuple(&u', &v') in &rel) | &v : &_ ]) | &u : &_ ]) |]
1097 | nameExpEq n rel
1098 , u' `refersTo` u
1099 , v' `refersTo` v
1100 , validCardinalityExpr k
1101 -> Just (k, z)
1102 _ -> Nothing
1103 matchProjCard =
1104 case hole z of
1105 [essence| and([ |&rel(&u', _)| = &k | &u : &_ ]) |]
1106 | nameExpEq n rel
1107 , u' `refersTo` u
1108 , validCardinalityExpr k
1109 -> Just (k, z)
1110 [essence| and([ &k = |&rel(&u', _)| | &u : &_ ]) |]
1111 | nameExpEq n rel
1112 , u' `refersTo` u
1113 , validCardinalityExpr k
1114 -> Just (k, z)
1115 _ -> Nothing
1116
1117 -- | Rewrite a constraint from binary relation usage to function-to-set usage.
1118 rewriteRelationConstraint :: Name -> Expression -> Maybe Expression
1119 rewriteRelationConstraint n c =
1120 let c' = transform rewrite c
1121 in if hasUnsupportedBinaryRelationUse n c'
1122 then Nothing
1123 else Just c'
1124 where
1125 rewrite [essence| (&x, &y) in &rel |] | nameExpEq n rel = [essence| &y in &rel(&x) |]
1126 rewrite [essence| tuple(&x, &y) in &rel |] | nameExpEq n rel = [essence| &y in &rel(&x) |]
1127 rewrite [essence| &rel(&x, _) |] | nameExpEq n rel = [essence| &rel(&x) |]
1128 rewrite e = e
1129
1130 -- | Check whether an expression still relies on binary-relation-only operators.
1131 hasUnsupportedBinaryRelationUse :: Name -> Expression -> Bool
1132 hasUnsupportedBinaryRelationUse n [essence| &f(&x) |] | nameExpEq n f
1133 = hasUnsupportedBinaryRelationUse n x
1134 hasUnsupportedBinaryRelationUse n [essence| image(&f, &x) |] | nameExpEq n f
1135 = hasUnsupportedBinaryRelationUse n x
1136 hasUnsupportedBinaryRelationUse n [essence| defined(&f) |] | nameExpEq n f = False
1137 hasUnsupportedBinaryRelationUse n [essence| range(&f) |] | nameExpEq n f = False
1138 hasUnsupportedBinaryRelationUse n [essence| (&_, &_) in &rel |] | nameExpEq n rel = True
1139 hasUnsupportedBinaryRelationUse n [essence| tuple(&_, &_) in &rel |] | nameExpEq n rel = True
1140 hasUnsupportedBinaryRelationUse n [essence| &rel(&_, _) |] | nameExpEq n rel = True
1141 hasUnsupportedBinaryRelationUse n (Reference n' _) = n == n'
1142 hasUnsupportedBinaryRelationUse n e = any (hasUnsupportedBinaryRelationUse n) (children e)
1143
1144 -- | Match edge constraints of the form:
1145 -- forAll (u,v) in edges . forAll ca in rel . ca[1] = u -> !((v, ca[2]) in rel)
1146 matchEdgeDisjointnessConstraint :: Name -> ExpressionZ -> Maybe (Expression, ExpressionZ)
1147 matchEdgeDisjointnessConstraint n z =
1148 case hole z of
1149 [essence| and([and([ &lhs = &u' -> !((&v', &rhs) in &rel2) | &ca <- &rel1 ])
1150 | (&u, &v) <- &edges ]) |]
1151 | nameExpEq n rel1
1152 , nameExpEq n rel2
1153 , tupleFirstOf lhs ca
1154 , tupleSecondOf rhs ca
1155 , u' `refersTo` u
1156 , v' `refersTo` v
1157 -> Just (edges, z)
1158 _ -> Nothing
1159
1160 -- | Rewrite the matched edge constraint for the transformed function.
1161 mkEdgeDisjointConstraint :: NameGen m => Name -> Expression -> m Expression
1162 mkEdgeDisjointConstraint n edges = do
1163 (uvP, uv) <- quantifiedVar
1164 let f = fromName n
1165 return [essence| and([ &f(&uv[2]) intersect &f(&uv[1]) = {} | &uvP <- &edges ]) |]
1166
1167 tupleFirstOf :: Expression -> AbstractPattern -> Bool
1168 tupleFirstOf [essence| &ca'[1] |] ca = ca' `refersTo` ca
1169 tupleFirstOf _ _ = False
1170
1171 tupleSecondOf :: Expression -> AbstractPattern -> Bool
1172 tupleSecondOf [essence| &ca'[2] |] ca = ca' `refersTo` ca
1173 tupleSecondOf _ _ = False
1174
1175 validCardinalityExpr :: Expression -> Bool
1176 validCardinalityExpr e = not (isFind e)