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                   (dom, tatr2) <- rule m1 findAndCstrs
  106                   when ((dom /= d || toAddRem tatr2 tatr1 /= tatr1) &&
  107                         logRuleSuccesses)
  108                        (log logLevel $ name <+> pretty n <+> ":" <+> pretty d)
  109                   return (updateDecl (n, dom) m1, toAddRem tatr2 tatr1))
  110               modelAndToKeep [ (mSetToSet, "multiset changed to set")
  111                              -- , (relationToFunction, "relation to function")
  112                              ])
  113           (model3, ([], []))
  114           (zip (collectFindVariables model3)
  115                (repeat $ map zipper $ collectConstraints model3))
  116 
  117       -- Apply constraint additions and removals
  118       model5' <- resolveNames $
  119                  addConstraints (fst toAddToRem') $
  120                  remConstraints (snd toAddToRem') model4
  121       model5  <- evaluateModel model5'
  122 
  123       -- Make another pass if the model was updated, but stop if it contains machine names
  124       if model1 == model5 || any containsMachineName (collectConstraints model5)
  125          then return model5
  126          else core model5
  127     -- Does an expression contain a reference with a machine name?
  128     containsMachineName = any isMachineName . universe
  129     isMachineName (Reference MachineName{} _) = True
  130     isMachineName _                           = False
  131 
  132 -- | 'uncurry' for functions of three arguments and triples.
  133 uncurry3 :: (a -> b -> c -> d) -> ((a, b, c) -> d)
  134 uncurry3 f (x, y, z) = f x y z
  135 
  136 -- | Collect decision (find) variables from a model, returning their name and domain.
  137 collectFindVariables :: Model -> [FindVar]
  138 collectFindVariables = mapMaybe collectFind . mStatements
  139   where
  140     collectFind (Declaration (FindOrGiven Find n d)) = Just (n, d)
  141     collectFind _                                    = Nothing
  142 
  143 -- | Collect the constraints in a model.
  144 collectConstraints :: Model -> [Expression]
  145 collectConstraints = concatMap getSuchThat . mStatements
  146   where
  147     getSuchThat (SuchThat cs) = cs
  148     getSuchThat _             = []
  149 
  150 -- | Add constraints to a model.
  151 addConstraints :: [ExpressionZ] -> Model -> Model
  152 addConstraints [] m = m
  153 addConstraints cs m@Model { mStatements = stmts }
  154   = m { mStatements = addConstraints' stmts }
  155   where
  156     addConstraints' (SuchThat cs':ss) = SuchThat (cs' `union` map fromZipper cs) : ss
  157     addConstraints' (s:ss)            = s : addConstraints' ss
  158     addConstraints' []                = [SuchThat (map fromZipper cs)]
  159 
  160 -- | Remove a list of constraints from a model.
  161 remConstraints :: [ExpressionZ] -> Model -> Model
  162 remConstraints cs m@Model { mStatements = stmts }
  163   = m { mStatements = filter (not . emptySuchThat) $ map remConstraints' stmts }
  164   where
  165     remConstraints' (SuchThat cs') = SuchThat $ filter (`notElem` map fromZipper cs) cs'
  166     remConstraints' s              = s
  167     emptySuchThat (SuchThat []) = True
  168     emptySuchThat _             = False
  169 
  170 -- | Update the domain of a declaration in a model.
  171 updateDecl :: FindVar -> Model -> Model
  172 updateDecl (n, d) m@Model { mStatements = stmts } = m { mStatements = map updateDecl' stmts }
  173   where
  174     updateDecl' (Declaration (FindOrGiven Find n' _))
  175       | n == n' = Declaration (FindOrGiven Find n d)
  176     updateDecl' decl = decl
  177 
  178 -- | Try adding an attribute at a given depth of a variable's domain, in a model.
  179 addAttrsToModel :: FindVar -> Int -> [AttrPair] -> Model -> Model
  180 addAttrsToModel (n, _) depth attrs m
  181   = let d = snd <$> find (\(n', _) -> n == n') (collectFindVariables m)
  182         in case d >>= flip (addAttrsToDomain depth) attrs of
  183                 Just d' -> updateDecl (n, d') m
  184                 Nothing -> m
  185   where
  186     addAttrsToDomain :: (MonadFailDoc m) => Int -> Domain () Expression -> [AttrPair] -> m (Domain () Expression)
  187     addAttrsToDomain 0 dom = addAttributesToDomain dom . map mkAttr
  188     addAttrsToDomain level (DomainSet r as inner)           = addAttrsToDomain (level - 1) inner >=> (pure . DomainSet r as)
  189     addAttrsToDomain level (DomainMSet r as inner)          = addAttrsToDomain (level - 1) inner >=> (pure . DomainMSet r as)
  190     addAttrsToDomain level (DomainMatrix index inner)       = addAttrsToDomain (level - 1) inner >=> (pure . DomainMatrix index)
  191     addAttrsToDomain level (DomainFunction r as from inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainFunction r as from)
  192     addAttrsToDomain level (DomainSequence r as inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainSequence r as)
  193     addAttrsToDomain level (DomainPartition r as inner)     = addAttrsToDomain (level - 1) inner >=> (pure . DomainPartition r as)
  194     addAttrsToDomain _ _ = const (failDoc "[addAttrsToDomain] not a supported nested domain")
  195     -- Special treatment for functions
  196     mkAttr (attr, Just [essence| image(&f, &_) |])     = (attr, Just [essence| max(range(&f)) |])
  197     mkAttr (attr, Just [essence| image(&f, &_) - 1 |]) = (attr, Just [essence| max(range(&f)) - 1 |])
  198     mkAttr (attr, Just [essence| image(&f, &_) + 1 |]) = (attr, Just [essence| max(range(&f)) + 1 |])
  199     mkAttr (attr, e')                                  = (attr, e')
  200 
  201 -- | Does an expression directly reference a given name variable?
  202 nameExpEq :: Name -> Expression -> Bool
  203 nameExpEq n (Reference n' _)           = n == n'
  204 nameExpEq n [essence| image(&f, &x) |] = nameExpEq n f || nameExpEq n x
  205 nameExpEq n [essence| &f(&x) |]        = nameExpEq n f || nameExpEq n x
  206 nameExpEq n [essence| defined(&f) |]   = nameExpEq n f
  207 nameExpEq n [essence| range(&f) |]     = nameExpEq n f
  208 nameExpEq n [essence| |&x| |]          = nameExpEq n x
  209 nameExpEq _ _                          = False
  210 
  211 -- | Does a reference refer to an abstract pattern?
  212 refersTo :: Expression -> AbstractPattern -> Bool
  213 refersTo (Reference n _) a = n `elem` namesFromAbstractPattern a
  214 refersTo _ _               = False
  215 
  216 -- | Get a single name from an abstract pattern.
  217 nameFromAbstractPattern :: (MonadFailDoc m) => AbstractPattern -> m Name
  218 nameFromAbstractPattern a = case namesFromAbstractPattern a of
  219                                  [n] -> pure n
  220                                  []  -> failDoc "[nameFromAbstractPattern] no names in abstract pattern"
  221                                  _   -> failDoc "[nameFromAbstractPattern] more than one name in abstract pattern"
  222 
  223 -- | Get the list of names from an abstract pattern.
  224 namesFromAbstractPattern :: AbstractPattern -> [Name]
  225 namesFromAbstractPattern (Single n)        = [n]
  226 namesFromAbstractPattern (AbsPatTuple ns)  = concatMap namesFromAbstractPattern ns
  227 namesFromAbstractPattern (AbsPatMatrix ns) = concatMap namesFromAbstractPattern ns
  228 namesFromAbstractPattern (AbsPatSet ns)    = concatMap namesFromAbstractPattern ns
  229 namesFromAbstractPattern _                 = []
  230 
  231 -- | Get the list of names from a generator.
  232 namesFromGenerator :: Generator -> [Name]
  233 namesFromGenerator (GenDomainNoRepr a _)  = namesFromAbstractPattern a
  234 namesFromGenerator (GenDomainHasRepr n _) = [n]
  235 namesFromGenerator (GenInExpr a _)        = namesFromAbstractPattern a
  236 
  237 -- | Find an expression at any depth of unconditional forAll expressions.
  238 findInUncondForAll :: (Expression -> Bool) -> [ExpressionZ] -> [Expression]
  239 findInUncondForAll p = map hole . findInUncondForAllZ p
  240 
  241 -- | Find an expression at any depth of unconditional forAll expressions,
  242 --   returning a Zipper containing the expression's context.
  243 findInUncondForAllZ :: (Expression -> Bool) -> [ExpressionZ] -> [ExpressionZ]
  244 findInUncondForAllZ p = concatMap findInForAll
  245   where
  246     findInForAll z | p (hole z) = [z]
  247     findInForAll z
  248       = case hole z of
  249              [essence| forAll &_ in defined(&_) . &_ |]
  250                  -> []
  251              [essence| forAll &x, &y : &_, &x' != &y' . &_ |]
  252                | x' `refersTo` x && y' `refersTo` y
  253                  -> maybe [] findInForAll (down z >>= down)
  254              [essence| forAll &x, &y in &_, &x' != &y' . &_ |]
  255                | x' `refersTo` x && y' `refersTo` y
  256                  -> maybe [] findInForAll (down z >>= down)
  257              Op (MkOpAnd (OpAnd (Comprehension _ gorcs)))
  258                | all (not . isCondition) gorcs
  259                  -> maybe [] findInForAll (down z >>= down)
  260              [essence| &_ /\ &_ |]
  261                  -> maybe [] findInForAll (down z)
  262                     `union`
  263                     maybe [] findInForAll (right z >>= down)
  264              -- Only accept OR cases if both sides contain a match
  265              [essence| &_ \/ &_ |]
  266                  -> let leftResult  = maybe [] findInForAll (down z)
  267                         rightResult = maybe [] findInForAll (right z >>= down)
  268                         in if not (null leftResult) && not (null rightResult)
  269                               then leftResult `union` rightResult
  270                               else []
  271              _   -> []
  272     isCondition Condition{} = True
  273     isCondition _           = False
  274 
  275 -- | Lens function over a binary expression.
  276 type BinExprLens m = Proxy m -> (Expression -> Expression -> Expression,
  277                                  Expression -> m (Expression, Expression))
  278 
  279 -- | Get the lens for an expression and the values it matches.
  280 matching :: Expression
  281          -> [(BinExprLens Maybe, a)]
  282          -> Maybe (a, (Expression, Expression))
  283 matching e ops = case mapMaybe (\(f1, f2) -> (,) f2 <$> match f1 e) ops of
  284                       [x] -> pure x
  285                       _   -> failDoc $ "no matching operator for expression:" <+> pretty e
  286 
  287 -- | (In)equality operator lens pairs.
  288 ineqOps :: [(BinExprLens Maybe, BinExprLens Identity)]
  289 ineqOps = [ (opEq,  opEq)
  290           , (opLt,  opLt)
  291           , (opLeq, opLeq)
  292           , (opGt,  opGt)
  293           , (opGeq, opGeq)
  294           ]
  295 
  296 -- | Opposites of (in)equality operator lens pairs.
  297 oppIneqOps :: [(BinExprLens Maybe, BinExprLens Identity)]
  298 oppIneqOps = [ (opEq, opEq)
  299              , (opLt, opGt)
  300              , (opLeq, opGeq)
  301              , (opGt, opLt)
  302              , (opGeq, opLeq)
  303              ]
  304 
  305 -- | (In)equality operator to size attribute modifier pairs.
  306 ineqSizeAttrs :: [(BinExprLens Maybe, (AttrName, Expression -> Maybe Expression))]
  307 ineqSizeAttrs = [ (opEq,  ("size",    Just))
  308                 , (opLt,  ("maxSize", Just . \x -> x - 1))
  309                 , (opLeq, ("maxSize", Just))
  310                 , (opGt,  ("minSize", Just . (+ 1)))
  311                 , (opGeq, ("minSize", Just))
  312                 ]
  313 
  314 -- | (In)equality operator to size attribute modifier pairs.
  315 ineqOccurAttrs :: [(BinExprLens Maybe, [(AttrName, Expression -> Maybe Expression)])]
  316 ineqOccurAttrs = [ (opEq,  [ ("minOccur", Just), ("maxOccur", Just) ])
  317                  , (opLt,  [ ("maxOccur", Just . \x -> x - 1) ])
  318                  , (opLeq, [ ("maxOccur", Just) ])
  319                  , (opGt,  [ ("minOccur", Just . (+ 1)) ])
  320                  , (opGeq, [ ("minOccur", Just) ])
  321                  ]
  322 
  323 -- | Unzip where the key is a 'Maybe' but the values should all be combined.
  324 unzipMaybeK :: Monoid m => [(Maybe a, m)] -> ([a], m)
  325 unzipMaybeK = foldr (\(mx, y) (xs, z) ->
  326                      case mx of
  327                           Just x  -> (x:xs, y `mappend` z)
  328                           Nothing -> (  xs, y `mappend` z))
  329               ([], mempty)
  330 
  331 -- | Does an expression contain a find variable?
  332 isFind :: Expression -> Bool
  333 isFind (Reference _ (Just (DeclNoRepr  Find _ _ _))) = True
  334 isFind (Reference _ (Just (DeclHasRepr Find _ _)))   = True
  335 isFind Reference{}                                   = False
  336 isFind Constant{}                                    = False
  337 isFind [essence| &f(&_) |]                           = isFind f
  338 isFind [essence| image(&f, &_) |]                    = isFind f
  339 isFind e                                             = any isFind $ children e
  340 
  341 -- | Add expressions to the ToAdd list.
  342 toAdd :: [ExpressionZ] -> ToAddToRem -> ToAddToRem
  343 toAdd e = first (`union` e)
  344 
  345 -- | Add expressions to the ToRemove list.
  346 toRem :: [ExpressionZ] -> ToAddToRem -> ToAddToRem
  347 toRem e = second (`union` e)
  348 
  349 -- | Combine two 'ToAddToRem' values.
  350 toAddRem :: ToAddToRem -> ToAddToRem -> ToAddToRem
  351 toAddRem (ta, tr) = toAdd ta . toRem tr
  352 
  353 -- | Apply a rule to arbitrary levels of nested domains.
  354 nested :: (MonadFailDoc m, MonadLog m, NameGen m, ?typeCheckerMode :: TypeCheckerMode)
  355        => (Model -> (FindVar, [ExpressionZ])
  356                  -> m ([AttrPair], ToAddToRem))
  357        -> Model
  358        -> (FindVar, [ExpressionZ])
  359        -> m ([(FindVar, Int, [AttrPair])], ToAddToRem)
  360 nested rule m fc@(fv, cs) = do
  361   -- Apply the rule at the top level
  362   (attrs, toAddToRem) <- rule m fc
  363   -- Look deeper into the domain if possible, for forAll constraints involving it
  364   nestedResults <- fmap mconcat $ forM cs $ \c ->
  365     case hole c of
  366          [essence| forAll &x in &gen . &_ |] | nameExpEq (fst fv) gen ->
  367            -- Create the new decision variable at this level
  368            case (,) <$> nameFromAbstractPattern x
  369                     <*> (domainOf gen >>= innerDomainOf) of
  370                 Left  _   -> return mempty
  371                 Right fv' -> do
  372                             -- Apply the rule from here
  373                             out <- nested rule m (fv', mapMaybe (down >=> down) [c])
  374                             case out of
  375                                  ([], _)     -> return mempty
  376                                  -- The rule was applied, so unwrap the variable and increase the depth
  377                                  (vs, tatr') -> return ( [ (fv, d + 1, as) | (_, d, as) <- vs ]
  378                                                        , tatr')
  379          _ -> return mempty
  380   -- Do not add a modification if there are no attributes
  381   let attrs' = if null attrs then [] else [(fv, 0, attrs)]
  382   return $ mappend nestedResults (attrs', toAddToRem)
  383 
  384 -- | If a function is surjective or bijective, and its domain and codomain
  385 --   are of equal size, then it is total and bijective.
  386 surjectiveIsTotalBijective :: (MonadFailDoc m, MonadLog m)
  387                            => Model
  388                            -> (FindVar, [ExpressionZ])
  389                            -> m ([AttrPair], ToAddToRem)
  390 surjectiveIsTotalBijective _ ((_, dom), _)
  391   = case dom of
  392          DomainFunction _ (FunctionAttr _ p j) from to
  393            | (p == PartialityAttr_Partial && j == JectivityAttr_Bijective) ||
  394              j == JectivityAttr_Surjective -> do
  395                (fromSize, toSize) <- functionDomainSizes from to
  396                if fromSize == toSize
  397                   then return ([("total", Nothing), ("bijective", Nothing)], mempty)
  398                   else return mempty
  399          DomainSequence _ (SequenceAttr (SizeAttr_Size s ) j) to
  400            | j `elem` [JectivityAttr_Bijective, JectivityAttr_Surjective] -> do
  401                toSize <- domainSizeOf to
  402                if s == toSize
  403                   then return ([("bijective", Nothing)], mempty)
  404                   else return mempty
  405          _ -> return mempty
  406 
  407 -- | Calculate the sizes of the domain and codomain of a function.
  408 functionDomainSizes :: (MonadFailDoc m)
  409                     => Domain () Expression       -- ^ The function's domain.
  410                     -> Domain () Expression       -- ^ The function's codomain.
  411                     -> m (Expression, Expression) -- ^ The sizes of the two.
  412 functionDomainSizes from to = (,) <$> domainSizeOf from <*> domainSizeOf to
  413 
  414 -- | If a function is total and injective, and its domain and codomain
  415 --   are of equal size, then it is bijective.
  416 totalInjectiveIsBijective :: (MonadFailDoc m, MonadLog m)
  417                           => Model
  418                           -> (FindVar, [ExpressionZ])
  419                           -> m ([AttrPair], ToAddToRem)
  420 totalInjectiveIsBijective _ ((_, dom), _)
  421   = case dom of
  422          DomainFunction _ (FunctionAttr _ PartialityAttr_Total JectivityAttr_Injective) from to -> do
  423            (fromSize, toSize) <- functionDomainSizes from to
  424            if fromSize == toSize
  425               then return ([("bijective", Nothing)], mempty)
  426               else return mempty
  427          _ -> return mempty
  428 
  429 -- | If a function is defined for all values in its domain, then it is total.
  430 definedForAllIsTotal :: (MonadFailDoc m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
  431                      => Model
  432                      -> (FindVar, [ExpressionZ])
  433                      -> m ([AttrPair], ToAddToRem)
  434 definedForAllIsTotal _ ((n, dom), cs)
  435   -- Is the function called with parameters generated from its domain in an expression?
  436   = let definedIn from e = any (funcCalledWithGenParams from) (children e)
  437         in case dom of
  438                 DomainFunction _ (FunctionAttr _ PartialityAttr_Partial _) from _
  439                   | any (definedIn from) $ findInUncondForAll isOp cs
  440                     -> return ([("total", Nothing)], mempty)
  441                 _ -> return mempty
  442   where
  443     -- Look for operator expressions but leave comprehensions, ANDs and ORs up to findInUncondForAll
  444     isOp (Op (MkOpAnd (OpAnd Comprehension{}))) = False
  445     isOp [essence| &_ /\ &_ |]                  = False
  446     isOp [essence| &_ \/ &_ |]                  = False
  447     -- Disallow implications which may remove some cases
  448     isOp [essence| &_ -> &_ |]                  = False
  449     isOp Op{}                                   = True
  450     isOp _                                      = False
  451     -- Determine whether a function is called with values generated from its domain
  452     funcCalledWithGenParams d [essence| image(&f, &param) |]
  453       = nameExpEq n f && case domainOf param of
  454                               Right d' -> d' == d
  455                               Left _   -> False
  456     funcCalledWithGenParams _ _ = False
  457 
  458 -- | If all distinct inputs to a function have distinct results, then it is injective.
  459 --   It will also be total if there are no conditions other than the disequality between
  460 --   the two inputs.
  461 diffArgResultIsInjective :: (MonadFailDoc m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
  462                          => Model
  463                          -> (FindVar, [ExpressionZ])
  464                          -> m ([AttrPair], ToAddToRem)
  465 diffArgResultIsInjective _ ((n, DomainFunction _ (FunctionAttr _ _ ject) from _), cs)
  466   | (ject == JectivityAttr_None || ject == JectivityAttr_Surjective) &&
  467     not (null $ findInUncondForAll isDistinctDisequality cs)
  468     -- It is known that no inputs are ignored
  469     = return ([("injective", Nothing), ("total", Nothing)], mempty)
  470   where
  471     -- Match a very specific pattern, which will also add the total attribute
  472     isDistinctDisequality [essence| &i != &j -> image(&f, &i') != image(&f', &j') |]
  473       = f == f' && i == i' && j == j' &&
  474         nameExpEq n f &&          -- the function is the one under consideration
  475         domIsGen i && domIsGen j  -- the values are generated from the function's domain
  476     isDistinctDisequality _ = False
  477     domIsGen x = case domainOf x of
  478                       Right dom -> dom == from
  479                       Left _    -> False
  480 diffArgResultIsInjective _ _ = return mempty
  481 
  482 -- | Set a size attribute on a variable.
  483 varSize :: (MonadFailDoc m, MonadLog m)
  484         => Model
  485         -> (FindVar, [ExpressionZ])
  486         -> m ([AttrPair], ToAddToRem)
  487 varSize _ ((n, _), cs) = do
  488   results <- forM cs $ \c ->
  489     case matching (hole c) ineqSizeAttrs of
  490          -- Do not allow find variables to be put in attributes
  491          Just ((attr, f), (cardinalityOf -> Just x, e)) | nameExpEq n x && not (isFind e)
  492            -> pure (Just (attr, f e), ([], [c]))
  493          _ -> pure (Nothing, mempty)
  494   return $ unzipMaybeK results
  495 
  496 
  497 cardinalityOf :: Expression -> Maybe Expression
  498 cardinalityOf [essence| |&x| |] = Just x
  499 cardinalityOf [essence| sum([1 | &_ <- &x]) |] = Just x
  500 cardinalityOf _ = Nothing
  501 
  502 
  503 -- | Set the minimum size of a set based on it being a superset of another.
  504 setSize :: (MonadFailDoc m, MonadLog m, NameGen m, ?typeCheckerMode :: TypeCheckerMode)
  505         => Model
  506         -> (FindVar, [ExpressionZ])
  507         -> m ([AttrPair], ToAddToRem)
  508 setSize _ ((n, DomainSet{}), cs)
  509   = fmap mconcat $ forM (findInUncondForAllZ isSubSupSet cs) $ \c ->
  510     case hole c of
  511          -- subset(Eq)
  512          [essence| &l subset   &r |] | nameExpEq n r -> return (minSize l (+ 1), mempty)
  513          [essence| &l subset   &r |] | nameExpEq n l -> return (maxSize r (\x -> x - 1), mempty)
  514          [essence| &l subsetEq &r |] | nameExpEq n r -> return (minSize l id, mempty)
  515          [essence| &l subsetEq &r |] | nameExpEq n l -> return (maxSize r id, mempty)
  516          -- supset(Eq)
  517          [essence| &l supset   &r |] | nameExpEq n l -> return (minSize r (+ 1), mempty)
  518          [essence| &l supset   &r |] | nameExpEq n r -> return (maxSize l (\x -> x - 1), mempty)
  519          [essence| &l supsetEq &r |] | nameExpEq n l -> return (minSize r id, mempty)
  520          [essence| &l supsetEq &r |] | nameExpEq n r -> return (maxSize l id, mempty)
  521          _                                           -> return mempty
  522   where
  523     isSubSupSet [essence| &_ subset   &_ |] = True
  524     isSubSupSet [essence| &_ subsetEq &_ |] = True
  525     isSubSupSet [essence| &_ supset   &_ |] = True
  526     isSubSupSet [essence| &_ supsetEq &_ |] = True
  527     isSubSupSet _                           = False
  528     minSize [essence| defined(&g) |] f
  529       = case domainOf g of
  530              Right (DomainFunction _ (FunctionAttr _ PartialityAttr_Total _) from _) ->
  531                case domainSizeOf from of
  532                     Just s  -> [("minSize", Just (f s))]
  533                     Nothing -> mempty
  534              _ -> mempty
  535     minSize [essence| range(&g) |] f
  536       = case domainOf g of
  537              Right (DomainFunction _ (FunctionAttr _ PartialityAttr_Total j) from to)
  538                | j == JectivityAttr_Bijective || j == JectivityAttr_Surjective ->
  539                  case domainSizeOf to of
  540                       Just s  -> [("minSize", Just (f s))]
  541                       Nothing -> mempty
  542                | j == JectivityAttr_Injective ->
  543                  case domainSizeOf from of
  544                       Just s  -> [("minSize", Just (f s))]
  545                       Nothing -> mempty
  546                | otherwise    -> [("minSize", Just (f 1))]
  547              _ -> mempty
  548     minSize e f = case domainOf e of
  549                        Right (DomainSet _ (SetAttr (SizeAttr_Size mn)) _) ->
  550                          [("minSize", Just (f mn))]
  551                        Right (DomainSet _ (SetAttr (SizeAttr_MinSize mn)) _) ->
  552                          [("minSize", Just (f mn))]
  553                        Right (DomainSet _ (SetAttr (SizeAttr_MinMaxSize mn _)) _) ->
  554                          [("minSize", Just (f mn))]
  555                        _ -> mempty
  556                        -- TODO: extend for Matrix, MSet, Partition and Sequence
  557     maxSize [essence| defined(&g) |] f
  558       = case domainOf g >>= innerDomainOf of
  559              Right (DomainTuple [d, _]) ->
  560                case domainSizeOf d of
  561                     Just s  -> [("maxSize", Just (f s))]
  562                     Nothing -> mempty
  563              _ -> mempty
  564     maxSize [essence| range(&g) |] f
  565       = case domainOf g >>= innerDomainOf of
  566              Right (DomainTuple [_, d]) ->
  567                case domainSizeOf d of
  568                     Just s  -> [("maxSize", Just (f s))]
  569                     Nothing -> mempty
  570              _ -> mempty
  571     maxSize e f = case domainOf e of
  572                        Right (DomainSet _ (SetAttr (SizeAttr_Size mx)) _) ->
  573                          [("maxSize", Just (f mx))]
  574                        Right (DomainSet _ (SetAttr (SizeAttr_MaxSize mx)) _) ->
  575                          [("maxSize", Just (f mx))]
  576                        Right (DomainSet _ (SetAttr (SizeAttr_MinMaxSize _ mx)) _) ->
  577                          [("maxSize", Just (f mx))]
  578                        Right d@(DomainSet _ (SetAttr SizeAttr_None) _) ->
  579                          case domainSizeOf d of
  580                               Just mx -> [("maxSize", Just (f mx))]
  581                               Nothing -> mempty
  582                        _ -> mempty
  583                        -- TODO: extend for Matrix, MSet, Partition and Sequence
  584 setSize _ _ = return mempty
  585 
  586 -- | The maxSize, and minOccur attributes of an mset affect its maxOccur and minSize attributes.
  587 mSetSizeOccur :: (MonadFailDoc m, MonadLog m)
  588               => Model
  589               -> (FindVar, [ExpressionZ])
  590               -> m ([AttrPair], ToAddToRem)
  591 mSetSizeOccur _ ((_, d), _)
  592   = case d of
  593          -- Ordering is important here, as there is a rule that applies
  594          -- to maxSize and minOccur, but none that applies to minSize
  595          -- and maxOccur. size uses the maxSize rule, but can ignore a
  596          -- minOccur because it cannot have its minSize changed.
  597          -- size -> maxOccur
  598          DomainMSet _ (MSetAttr (SizeAttr_Size mx) _) _
  599            -> return ([("maxOccur", Just mx)], mempty)
  600          -- minOccur -> minSize
  601          DomainMSet _ (MSetAttr _ (OccurAttr_MinOccur mn)) _
  602            -> return ([("minSize", Just mn)], mempty)
  603          DomainMSet _ (MSetAttr _ (OccurAttr_MinMaxOccur mn _)) _
  604            -> return ([("minSize", Just mn)], mempty)
  605          -- maxSize -> maxOccur
  606          DomainMSet _ (MSetAttr (SizeAttr_MaxSize mx) _) _
  607            -> return ([("maxOccur", Just mx)], mempty)
  608          DomainMSet _ (MSetAttr (SizeAttr_MinMaxSize _ mx) _) _
  609            -> return ([("maxOccur", Just mx)], mempty)
  610          _ -> return mempty
  611 
  612 -- | Infer multiset occurrence attributes from constraints.
  613 mSetOccur :: (MonadFailDoc m, MonadLog m)
  614           => Model
  615           -> (FindVar, [ExpressionZ])
  616           -> m ([AttrPair], ToAddToRem)
  617 mSetOccur _ ((n, DomainMSet _ _ d), cs)
  618   = return $ mconcat $ flip mapMaybe (findInUncondForAllZ (not . null . isFreq) cs) $ \e ->
  619       case isFreq (hole e) of
  620            [] -> Nothing
  621            -- Only remove constraints if they are all used up.
  622            -- Because freq(a, b) = c adds two attributes, removing constraints
  623            -- in an AND expression cannot work, in the case of freq(a, b) = c /\ e
  624            -- because there are two attributes and two terms, but term e may not
  625            -- be removed.
  626            as -> let tattr = case hole e of
  627                                   AbstractLiteral AbsLitMatrix{} -> mempty
  628                                   _                              -> ([], [e])
  629                      in Just (as, tattr)
  630   where
  631     isFreq :: Expression -> [AttrPair]
  632     isFreq (AbstractLiteral (AbsLitMatrix _ es)) = concatMap isFreq es
  633     isFreq e = case matching e oppIneqOps of
  634                     Just (_, ([essence| freq(&x, &v) |], e'))
  635                       | valid x v e' -> case matching e ineqOccurAttrs of
  636                                              Just (as, _) -> map (second ($ e')) as
  637                                              Nothing      -> []
  638                     -- Flip the terms
  639                     Just (oper, (l, r@[essence| freq(&x, &v) |]))
  640                       | valid x v l -> isFreq $ make oper r l
  641                     _               -> []
  642     -- Make sure that the expression's components are valid
  643     valid :: Expression -> Expression -> Expression -> Bool
  644     valid x v e = nameExpEq n x && isGen v && isConst e
  645     -- Make sure that the value is generated from the mset's domain
  646     isGen (Reference _ (Just (InComprehension (GenDomainNoRepr _ d')))) = d == d'
  647     isGen (Reference _ (Just (DeclNoRepr Quantified _ d' _)))           = d == d'
  648     isGen (Reference _ (Just (InComprehension (GenInExpr _ e ))))       = nameExpEq n e
  649     isGen _                                                             = False
  650     -- Make sure that the mset is being equated to a constant
  651     isConst (Reference _ (Just (DeclNoRepr Given _ _ _))) = True
  652     isConst (Constant ConstantInt{})                      = True
  653     isConst _                                             = False
  654 mSetOccur _ _ = return mempty
  655 
  656 -- | Mark a partition regular if there is a constraint on its parts constraining them to be of equal size.
  657 partRegular :: (MonadFailDoc m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
  658             => Model
  659             -> (FindVar, [ExpressionZ])
  660             -> m ([AttrPair], ToAddToRem)
  661 partRegular _ ((_, DomainPartition{}), cs) = do
  662     attrs <- forM cs $ \c ->
  663       case hole c of
  664            -- [essence| forAll &x in parts(&p) . forAll &y in parts(&p') . &xCard = &yCard |]
  665            [essence| and([ &xCard = &yCard | &x <- parts(&p), &y <- parts(&p') ]) |]
  666              | Just (Reference x' _) <- cardinalityOf xCard
  667              , Just (Reference y' _) <- cardinalityOf yCard
  668              , or [ and [x == Single x', y == Single y']
  669                   , and [x == Single y', y == Single x']
  670                   ]
  671              , p == p'
  672              -> pure (Just ("regular", Nothing), ([], [c]))
  673            _ -> pure (Nothing, mempty)
  674     return $ unzipMaybeK attrs
  675 partRegular _ _ = return mempty
  676 
  677 
  678 -- | Convert constraints acting on the number of parts in a partition to an attribute.
  679 numPartsToAttr :: (MonadFailDoc m, MonadLog m)
  680                => Model
  681                -> (FindVar, [ExpressionZ])
  682                -> m ([AttrPair], ToAddToRem)
  683 numPartsToAttr _ ((n, DomainPartition{}), cs) = do
  684   attrs <- forM cs $ \c ->
  685     case matching (hole c) ineqSizeAttrs of
  686          -- Do not allow find variables to be put in attributes
  687          Just ((attr, f), ([essence| |parts(&x)| |], e)) | nameExpEq n x && not (isFind e)
  688            -> pure (Just (changeAttr attr, f e), ([], [c]))
  689          _ -> pure (Nothing, mempty)
  690   return $ unzipMaybeK attrs
  691   where
  692     -- Change a size attribute name to a numParts attribute name
  693     changeAttr "size"    = "numParts"
  694     changeAttr "minSize" = "minNumParts"
  695     changeAttr "maxSize" = "maxNumParts"
  696     changeAttr a         = a
  697 numPartsToAttr _ _ = return mempty
  698 
  699 -- | Convert constraints acting on the sizes of parts in a partition to an attribute.
  700 partSizeToAttr :: (MonadFailDoc m, MonadLog m)
  701                => Model
  702                -> (FindVar, [ExpressionZ])
  703                -> m ([AttrPair], ToAddToRem)
  704 partSizeToAttr _ ((n, DomainPartition{}), cs) = do
  705   attrs <- forM cs $ \c ->
  706     case hole c of
  707          [essence| forAll &x in parts(&p) . &xCard =  &e |]
  708              | Just x' <- cardinalityOf xCard
  709              , valid p x x' e
  710              -> pure (Just ("partSize", Just e), ([], [c]))
  711          [essence| forAll &x in parts(&p) . &xCard <  &e |]
  712              | Just x' <- cardinalityOf xCard
  713              , valid p x x' e
  714              -> pure (Just ("maxPartSize", Just (e - 1)), ([], [c]))
  715          [essence| forAll &x in parts(&p) . &xCard <= &e |]
  716              | Just x' <- cardinalityOf xCard
  717              , valid p x x' e
  718              -> pure (Just ("maxPartSize", Just e), ([], [c]))
  719          [essence| forAll &x in parts(&p) . &xCard >  &e |]
  720              | Just x' <- cardinalityOf xCard
  721              , valid p x x' e
  722              -> pure (Just ("minPartSize", Just (e + 1)), ([], [c]))
  723          [essence| forAll &x in parts(&p) . &xCard >= &e |]
  724              | Just x' <- cardinalityOf xCard
  725              , valid p x x' e
  726              -> pure (Just ("minPartSize", Just e), ([], [c]))
  727          _ -> pure (Nothing, mempty)
  728   return $ unzipMaybeK attrs
  729   where
  730     -- Make sure that the expression's components are valid
  731     valid :: Expression -> AbstractPattern -> Expression -> Expression -> Bool
  732     valid p x v e = nameExpEq n p && v `refersTo` x && not (isFind e)
  733 partSizeToAttr _ _ = return mempty
  734 
  735 -- | Equate the range of a function to a set of the former is a subset of the latter
  736 --   and all values in the set are results of the function.
  737 funcRangeEqSet :: (MonadFailDoc m, MonadLog m)
  738                => Model
  739                -> (FindVar, [ExpressionZ])
  740                -> m ([AttrPair], ToAddToRem)
  741 funcRangeEqSet _ ((n, DomainSet{}), cs)
  742   -- Get references to the set and the function whose range it is a superset of
  743   = let funcSubsets = mapMaybe funcSubsetEqOf $
  744                       findInUncondForAllZ (isJust . funcSubsetEqOf . zipper) cs
  745         -- Reduce the functions to those whose values are equated to the values in the set
  746         fsToUse = flip filter funcSubsets $ \(_, f) ->
  747                   not $ null $ findInUncondForAll (funcValEqSetVal (hole f)) cs
  748         -- Transform the functions into new constraints, preserving structure
  749         csToAdd = flip mapMaybe fsToUse $ \(s, f) ->
  750                   let f' = hole f
  751                       in replaceHole [essence| range(&f') = &s |] <$>
  752                          (up f >>= up)
  753         in return ([], (csToAdd, []))
  754   where
  755     -- Get the function whose range is a subsetEq of the set
  756     funcSubsetEqOf z = case hole z of
  757                             [essence| range(&_) subsetEq &s |] | nameExpEq n s
  758                               -> (,) s <$> (down z >>= down)
  759                             [essence| &s supsetEq range(&_) |] | nameExpEq n s
  760                               -> (,) s <$> (down z >>= right >>= down)
  761                             _ -> Nothing
  762     -- Are the values of the function equal to the values of the set?
  763     funcValEqSetVal f [essence| forAll &x in &s . image(&f', &_) = &x' |]
  764       = nameExpEq n s && f == f' && x' `refersTo` x
  765     funcValEqSetVal f [essence| forAll &x in &s . &x' = image(&f', &_) |]
  766       = nameExpEq n s && f == f' && x' `refersTo` x
  767     funcValEqSetVal _ _ = False
  768 funcRangeEqSet _ _ = return mempty
  769 
  770 
  771 -- | An (in)equality in a forAll implies that the (in)equality also applies to
  772 --   the sums of both terms.
  773 forAllIneqToIneqSum :: (MonadFailDoc m, MonadLog m, NameGen m, ?typeCheckerMode :: TypeCheckerMode)
  774                     => Model
  775                     -> (FindVar, [ExpressionZ])
  776                     -> m ([AttrPair], ToAddToRem)
  777 forAllIneqToIneqSum _ (_, cs) = do
  778   let matches = mapMaybe matchParts $ findInUncondForAllZ (isJust . matchParts . zipper) cs
  779   csToAdd <- mapMaybe mkConstraint <$> filterM partsAreNumeric matches
  780   return ([], (csToAdd, []))
  781   where
  782     -- Match and extract the desired parts of the expression
  783     matchParts :: ExpressionZ -> Maybe (Generator, Maybe ExpressionZ, Expression, Expression)
  784     matchParts z = case hole z of
  785                         Op (MkOpAnd (OpAnd (Comprehension e [Generator g])))
  786                           -> matching e ineqOps >>=
  787                              uncurry (matchComponents g z) . snd
  788                         _ -> Nothing
  789     -- Match the components of the expression of interest
  790     matchComponents :: Generator -> ExpressionZ -> Expression -> Expression
  791                     -> Maybe (Generator, Maybe ExpressionZ, Expression, Expression)
  792     matchComponents g z e1 e2
  793       | refInExpr (namesFromGenerator g) e1 && refInExpr (namesFromGenerator g) e2
  794         = Just (g, down z >>= down, e1, e2)
  795     matchComponents _ _ _ _ = Nothing
  796     -- Is a name referred to in an expression?
  797     refInExpr names = any (\e -> any (`nameExpEq` e) names) . universe
  798     -- Are the parts of the matched expression numeric?
  799     partsAreNumeric (_, _, e1, e2) = (&&) <$> domainIsNumeric e1 <*> domainIsNumeric e2
  800     domainIsNumeric e = case domainOf e of
  801                              Right DomainInt{}           -> return True
  802                              Right (DomainAny _ (TypeInt _)) -> return True
  803                              _                               -> return False
  804     -- Replace the forAll with the (in)equality between sums
  805     mkConstraint :: (Generator, Maybe ExpressionZ, Expression, Expression) -> Maybe ExpressionZ
  806     mkConstraint (gen, Just z, _, _)
  807       -- Use matching with ineqOps to get the operation that is used on the two expressions
  808       = case matching (hole z) ineqOps of
  809              Just (f, (e1, e2))
  810                -> let mkSumOf = Op . MkOpSum . OpSum . flip Comprehension [Generator gen]
  811                       -- Two steps to get out of the forAll, and replace it with the constraint
  812                       in replaceHole (make f (mkSumOf e1) (mkSumOf e2)) <$> (up z >>= up)
  813              _ -> Nothing
  814     mkConstraint _ = Nothing
  815 
  816 -- | Iterate slightly faster over a domain if generating two distinct variables.
  817 fasterIteration :: (MonadFailDoc m, MonadFailDoc m,MonadIO m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
  818                 => Model
  819                 -> (FindVar, [ExpressionZ])
  820                 -> m ([AttrPair], ToAddToRem)
  821 fasterIteration m (_, cs) = do
  822   let iters = findInUncondForAllZ (isJust . doubleDistinctIter . zipper) cs
  823   fmap ((,) [] . mconcat) $ forM iters $ \z -> do
  824     -- Find the equivalent variables
  825     [equivs] <- sequence [ findEquivVars (hole z) ]
  826     -- Only apply to equivalent variables and make the new constraint
  827     case doubleDistinctIter z >>= onlyEquivalent equivs >>= changeIterator of
  828          Nothing -> return mempty
  829          -- Remove the old constraint
  830          Just z' -> return ([z'], [z])
  831   where
  832     -- Match the elemenents of interest in the constraint
  833     doubleDistinctIter z
  834       = case hole z of
  835              Op (MkOpAnd (OpAnd (Comprehension _ [ Generator (GenInExpr x v)
  836                                                  , Generator (GenInExpr y v')
  837                                                  , Condition [essence| &x' != &y' |]
  838                                                  ])))
  839                | v == v' && x' `refersTo` x && y' `refersTo` y
  840                  -> Just ((x, x'), (y, y'), v, down z >>= down)
  841              Op (MkOpAnd (OpAnd (Comprehension _ [ Generator (GenDomainNoRepr x d)
  842                                                  , Generator (GenDomainNoRepr y d')
  843                                                  , Condition [essence| &x' != &y' |]
  844                                                  ])))
  845                | d == d' && x' `refersTo` x && y' `refersTo` y
  846                  -> Just ((x, x'), (y, y'), Domain d, down z >>= down)
  847              _ -> Nothing
  848     -- Find which variables are equivalent in an expression
  849     findEquivVars :: (MonadIO m) => Expression -> m (Map Text Text)
  850     findEquivVars e = case e of
  851                            [essence| forAll &_, &_ : &_, &_ . &e' |]  -> liftIO $ findSyms e'
  852                            [essence| forAll &_, &_ in &_, &_ . &e' |] -> liftIO $ findSyms e'
  853                            _ -> return M.empty
  854     -- Find the symmetries in an expression
  855     findSyms :: Expression -> IO (Map Text Text)
  856     findSyms e = do
  857       let m' = addConstraints [zipper e] $ remConstraints cs m
  858       let filename = ".tmp-variable-strengthening.json"
  859       outputVarSymBreaking filename m'
  860       symmetries <- ferret $ stringToText filename
  861       removeFile filename
  862       case (JSON.decodeStrict $ T.encodeUtf8 symmetries) :: Maybe [Map Text Text] of
  863            Nothing -> return M.empty
  864            Just ss -> return $ foldr M.union M.empty ss
  865     -- Only perform the modification if the variables are equivalent in the expression
  866     onlyEquivalent es v@((x, _), (y, _), _, _)
  867       = case namesFromAbstractPattern x of
  868              [Name nx] -> case namesFromAbstractPattern y of
  869                                [Name ny] -> case es M.!? nx of
  870                                                  Just ny' | ny == ny' -> Just v
  871                                                  _ -> Nothing
  872                                _         -> Nothing
  873              _         -> Nothing
  874     -- Change the iterator to use the new, faster notation
  875     changeIterator ((x, x'), (y, y'), v, Just z)
  876       = let e = hole z
  877             in case v of
  878                     r@Reference{}
  879                       -> case domainOf r of
  880                               Left _ -> Nothing
  881                               Right DomainSet{}
  882                                 -> replaceHole [essence| forAll {&x, &y} subsetEq &v . &e |] <$>
  883                                    (up z >>= up)
  884                               Right _
  885                                 -> replaceHole [essence| forAll &x, &y in &v, &y' > &x' . &e |] <$>
  886                                    (up z >>= up)
  887                     Op MkOpDefined{}
  888                       -> replaceHole [essence| forAll &x, &y in &v, &y' > &x' . &e |] <$>
  889                          (up z >>= up)
  890                     Domain d
  891                       -> replaceHole [essence| forAll &x, &y : &d, &y' > &x' . &e |] <$>
  892                          (up z >>= up)
  893                     _ -> Nothing
  894     changeIterator _ = Nothing
  895 
  896 -- | Call ferret's symmetry detection on a JSON file
  897 ferret :: Text -> IO Text
  898 ferret path = sh (run "symmetry_detect" [ "--json", path ]) `catch`
  899               (\(_ :: SomeException) -> return "{}")
  900 
  901 -- | Change the type of a multiset with `maxOccur 1` to set.
  902 mSetToSet :: (MonadFailDoc m, MonadLog m)
  903           => Model
  904           -> (FindVar, [ExpressionZ])
  905           -> m (Domain () Expression, ToAddToRem)
  906 mSetToSet _ ((n, DomainMSet r (MSetAttr sa oa) d), cs) | maxOccur1 oa = do
  907   let dom'  = DomainSet r (SetAttr sa) d
  908   let torem = filter (any (nameExpEq n) . universe . hole) cs
  909   let toadd = map (zipper . transform (\e -> if nameExpEq n e
  910                                                 then [essence| toMSet(&e) |]
  911                                                 else e)
  912                           . hole)
  913                   cs
  914   return (dom', (toadd, torem))
  915   where
  916     maxOccur1 (OccurAttr_MaxOccur 1)      = True
  917     maxOccur1 (OccurAttr_MinMaxOccur _ 1) = True
  918     maxOccur1 _                           = False
  919 mSetToSet _ ((_, dom), _) = return (dom, mempty)
  920 
  921 -- relationToFunction ::
  922 --     MonadFailDoc m =>
  923 --     MonadLog m =>
  924 --     Model ->
  925 --     (FindVar, [ExpressionZ]) ->
  926 --     m (Domain () Expression, ToAddToRem)
  927 -- -- relationToFunction _ ((n, DomainRelation r (MSetAttr sa oa) d), cs) | maxOccur1 oa = do
  928 -- --   let dom'  = DomainSet r (SetAttr sa) d
  929 -- --   let torem = filter (any (nameExpEq n) . universe . hole) cs
  930 -- --   let toadd = map (zipper . transform (\e -> if nameExpEq n e
  931 -- --                                                 then [essence| toMSet(&e) |]
  932 -- --                                                 else e)
  933 -- --                           . hole)
  934 -- --                   cs
  935 -- --   return (dom', (toadd, torem))
  936 -- --   where
  937 -- --     maxOccur1 (OccurAttr_MaxOccur 1)      = True
  938 -- --     maxOccur1 (OccurAttr_MinMaxOccur _ 1) = True
  939 -- --     maxOccur1 _                           = False
  940 -- relationToFunction _ ((_, dom), _) = return (dom, mempty)