RSolve (empty) → 0.1.0.0
raw patch · 12 files changed
+854/−0 lines, 12 filesdep +RSolvedep +basedep +containerssetup-changed
Dependencies added: RSolve, base, containers
Files
- LICENSE +21/−0
- README.md +93/−0
- RSolve.cabal +41/−0
- Setup.hs +2/−0
- src/Main.hs +26/−0
- src/RSolve/BrMonad.hs +26/−0
- src/RSolve/HM/Core.hs +115/−0
- src/RSolve/HM/Example.hs +54/−0
- src/RSolve/Infr.hs +99/−0
- src/RSolve/Logic.hs +89/−0
- src/RSolve/Options/Core.hs +102/−0
- src/RSolve/Options/Example.hs +186/−0
+ LICENSE view
@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2018 ++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ README.md view
@@ -0,0 +1,93 @@+# RSolve++A general solver for type checkers of programming languages and real world puzzles with complex constraints. +++## Preview++Here are 2 special cases presented in the following sections to show how powerful `RSolve` is.++### The Most Graceful Hindley-Milner Unification++Check `RSolve.HM.Core` and `RSolve.HM.Example`. ++Uncomment the code in `Main.hs` could reproduce following program:++```haskell+check = do+ let i = Prim Int+ let f = Prim Float+ let arrow = Op Arrow i f+ -- u means undecided+ u1 <- new+ u2 <- new+ u3 <- new+ u4 <- new+ -- u1 -> u2 where u1, u2 is not generic + let arrow_var = Op Arrow (Var u1) (Var u2) + -- int -> int+ let arrow_inst1 = Op Arrow i i+ -- float -> float+ let arrow_inst2 = Op Arrow f f+ -- a generic function+ let arrow_generic = Forall [u3] $ Op Arrow (Var u3) (Var u3)++ let arrow_match = Op Arrow (Var u4) (Var u4)++ _ <- solve $ Unify arrow arrow_var+ _ <- solve $ Unify arrow_inst1 arrow_match+ _ <- solve $ Unify arrow_generic arrow_inst1+ _ <- solve $ Unify arrow_generic arrow_inst2+ _ <- solveNeg++ mapM require [Var u1, Var u2, arrow_inst1, arrow_inst2, arrow_generic, arrow_match]+ +```++output:++```+u1 : Int+u2 : Float+arrow_inst1 : (Int -> Int)+arrow_inst2 : (Float -> Float)+arrow_generic : forall a2.(a2 -> a2)+arrow_match : (Int -> Int)+```++### N-Option Puzzles++This implememtation is presented at `RSolve.Options`, which provides the abstractions to solve all kinds of puzzles described with options.++A Hello World program could be found at `src/Main.hs` which solves a complex problem described with following link:++https://www.zhihu.com/question/68411978/answer/558913247.+++However, the much easier cases taking the same background as above problem (logic constraints described with four options `A, B, C, D`) could be enjoyale:++```haskell+test2 = do+ a <- store $ sol [A, B, C]+ b <- store $ sol [B, C, D]+ c <- store $ sol [C]+ _ <- solve $ a `eq` b+ _ <- solve $ b `neq` c+ _ <- solveNeg -- `Not` condition requires this+ _ <- solvePred -- unnecessary+ mapM require [a, b, c] + +main = do+ format ["a", "b", "c"] . nub . L.map fst+ $ runBr test2 emptyLState+```++output:++```+λ stack exec RSolve+====+"a" : Sol (fromList [B])+"b" : Sol (fromList [B])+"c" : Sol (fromList [C])+```
+ RSolve.cabal view
@@ -0,0 +1,41 @@+name: RSolve+version: 0.1.0.0+synopsis: A general solver for equations+description: A general solver for type checkers of programming languages+ and real world puzzles with complex constraints.+homepage: https://github.com/thautwarm/Rsolver#readme+license: MIT+license-file: LICENSE+author: thautwarm+maintainer: twshere@outlook.com+copyright: 2018 thautwarm+category: Language+build-type: Simple+cabal-version: >=1.10+extra-source-files: README.md++source-repository head+ type: git+ location: https://github.com/thautwarm/Rsolver.git++library+ hs-source-dirs: src+ default-language: Haskell2010+ build-depends: base >= 4 && < 5+ , containers+ exposed-modules: RSolve.BrMonad+ , RSolve.Infr+ , RSolve.Logic+ , RSolve.HM.Core+ , RSolve.Options.Core++executable RSolveExample+ hs-source-dirs: src+ main-is: Main.hs+ build-depends: base >= 4 && < 5+ , RSolve+ , containers+ default-language: Haskell2010+ other-modules: RSolve.HM.Example+ , RSolve.Options.Example+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Main.hs view
@@ -0,0 +1,26 @@+module Main where+import RSolve.Options.Example+import RSolve.HM.Example+++main =+ putStrLn "HM unification" >>+ hmUnificationExample >>+ putStrLn "4-option puzzles" >>+ optionExample++++-- test2 = do+-- a <- store $ sol [A, B, C]+-- b <- store $ sol [B, C, D]+-- c <- store $ sol [C]+-- _ <- solve $ a `eq` b+-- _ <- solve $ b `neq` c+-- _ <- solveNeg -- `Not` condition requires this+-- _ <- solvePred -- unnecessary+-- mapM require [a, b, c]++-- main = do+-- format ["a", "b", "c"] . nub . L.map fst+-- $ runBr test2 emptyLState
+ src/RSolve/BrMonad.hs view
@@ -0,0 +1,26 @@+module RSolve.BrMonad where+import Control.Monad+import Control.Applicative++newtype Br s a = Br {runBr :: s -> [(a, s)]}++instance Functor (Br s) where+ fmap = liftM++instance Applicative (Br s) where+ pure = return+ (<*>) = ap++instance Monad (Br s) where+ m >>= k =+ Br $ \s ->+ let xs = runBr m s+ in join [ runBr (k a) s | (a, s) <- xs]+ return a = Br $ \s -> [(a, s)]++instance Alternative (Br s) where+ empty = Br $ const []+ ma <|> mb = Br $ \s -> runBr ma s ++ runBr mb s++getBy f = Br $ \s -> [(f s, s)]+putBy f = Br $ \s -> [((), f s)]
+ src/RSolve/HM/Core.hs view
@@ -0,0 +1,115 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TupleSections #-}+-- https://github.com/thautwarm/reFining/blob/master/DotNet/reFining/reFining++module RSolve.HM.Core where+import RSolve.BrMonad+import RSolve.Infr+import RSolve.Logic+import Control.Applicative+import qualified Data.Map as M++type Id = Int++data TypeOp = Arrow | Join | Stmt+ deriving (Show, Eq, Ord)++data Prim = Int | Float | Char+ deriving (Show, Eq, Ord)+++data Core where+ Prim :: Prim -> Core++ Op :: TypeOp -> Core -> Core -> Core++ Forall :: [Id] -> Core -> Core++ Var :: Id -> Core+ deriving (Eq)++instance Show Core where+ show (Prim a) = show a+ show (Op Arrow a b) =+ "(" ++ show a ++ " -> " ++ show b ++ ")"+ show (Op Join a b) = show a ++ ", " ++ show b+ show (Op Stmt a b) = show a ++ ";\n" ++ show b+ show (Forall xs b) =+ let f a b = a ++ " a" ++ show b+ in foldl f "forall " xs ++ "." ++ show b+ show (Var a) = "a" ++ show a++free :: M.Map Id Core -> Core -> Core+free m = mkFree+ where+ mkFree a@(Prim _) = a+ mkFree (Op op a b) = Op op (mkFree a) (mkFree b)+ mkFree (Forall a b) = Forall a (mkFree b)+ mkFree a@(Var id) =+ M.findWithDefault a id m++occurIn :: Addr -> Addr -> Br (LState Core) Bool+occurIn l = contains . Var+ where+ contains (Prim _) = return False++ contains (Var a) =+ if a == l then return True+ else tryLoad a >>= \case+ Just a -> contains a+ _ -> return False++ contains (Op _ a b) = (||) <$> contains a <*> contains b+ contains (Forall _ a) = contains a++instance Reference Core where+ mkRef = Var+ isRef (Var a) = Just a+ isRef _ = Nothing+++instance Unify Core where+ prune v@(Var a) = tryLoad a >>= \case+ Just var -> prune var+ _ -> return v++ prune a@(Prim _) = return a++ prune (Forall a b) = Forall a <$> prune b+ prune (Op op a b) = Op op <$> prune a <*> prune b++ unify (Prim a) (Prim b) =+ if a == b then return ()+ else empty++ unify l@(Var a) r@(Var b)+ | a == b = return ()+ | otherwise = do+ recursive <- occurIn a b+ if recursive+ then error "ill formed definition like a = a -> b"+ else update a r++ unify l r@(Var _) = unify r l++ unify (Var id) r = update id r++ -- type operators are not frist class+ unify (Op opl l1 l2) (Op opr r1 r2) =+ if opl /= opr then empty+ else+ unify l1 r1 >> unify l2 r2++ unify (Forall freevars poly) r = do+ pairs <- mapM freepair freevars+ let freemap = M.fromList pairs+ let l = free freemap poly+ unify l r+ where+ freepair freevar = (freevar,) <$> mkRef <$> new++ unify l r@(Forall _ _) = unify r l++
+ src/RSolve/HM/Example.hs view
@@ -0,0 +1,54 @@+module RSolve.HM.Example where+import RSolve.HM.Core+import RSolve.BrMonad+import RSolve.Infr+import RSolve.Logic+import Control.Monad++test = do+ let i = Prim Int+ let f = Prim Float+ let arrow = Op Arrow i f++ -- u means undecided+ u1 <- new+ u2 <- new+ u3 <- new+ u4 <- new++ -- u1 -> u2 where u1, u2 is not generic+ let arrow_var = Op Arrow (Var u1) (Var u2)++ -- int -> int+ let arrow_inst1 = Op Arrow i i++ -- float -> float+ let arrow_inst2 = Op Arrow f f+++ let arrow_match = Op Arrow (Var u4) (Var u4)++ -- a generic function+ let arrow_generic = Forall [u3] $ Op Arrow (Var u3) (Var u3)++ _ <- solve $ Unify arrow arrow_var+ _ <- solve $ Unify arrow_inst1 arrow_match+ _ <- solve $ Unify arrow_generic arrow_inst1+ _ <- solve $ Unify arrow_generic arrow_inst2+ _ <- solveNeg++ mapM require [Var u1, Var u2, arrow_inst1, arrow_inst2, arrow_generic, arrow_match]++format :: [(String, Core)] -> IO ()+format [] = do+ putStrLn "================="+format ((a, b):xs) = do+ _ <- putStrLn $ a ++ " : " ++ show b+ format xs+formayMany fields lst =+ forM_ [zip fields items | items <- lst] format+++hmUnificationExample = do+ let fields = ["u1", "u2", "arrow_inst1", "arrow_inst2", "arrow_generic", "arrow_match"]+ formayMany fields . map fst $ runBr test emptyLState
+ src/RSolve/Infr.hs view
@@ -0,0 +1,99 @@+module RSolve.Infr where+import RSolve.BrMonad+import Control.Applicative+import qualified Data.Set as S+import qualified Data.Map as M+import qualified Data.List as L++type Addr = Int+class Eq a => Reference a where+ -- reference can be stored in Map+ isRef :: a -> Maybe Addr+ mkRef :: Addr -> a++class Reference a => Unify a where+ prune :: a -> Br (LState a) a+ unify :: a -> a -> Br (LState a) ()+ complement :: a -> a -> Br (LState a) ()+ complement a b =+ if a == b then return ()+ else empty++class EnumSet a where+ toEnumerable :: Br (LState a) ()+++data Allocator a =+ Allocator { storage :: M.Map Addr a+ , addr :: Addr }+ deriving (Show)+++data LState a =+ LState { allocator :: Allocator a+ , negPairs :: [(a, a)]+ , constrains :: [Br (LState a) Bool] }++allocator' st (LState _ negs cs) = LState st negs cs+negPairs' negs (LState st _ cs) = LState st negs cs+constrains' cs (LState st negs _) = LState st negs cs+++inc :: Reference a => Allocator a -> (Addr, Allocator a)+inc (Allocator s c) = (c, Allocator s $ c + 1)++alloc :: Reference a => a -> Allocator a -> (Addr, Allocator a)+alloc a (Allocator s c) = (c, Allocator (M.insert c a s) (c + 1))++renew :: Reference a => Addr -> a -> Allocator a -> Allocator a+renew addr obj r@(Allocator s c) =+ case isRef obj of+ Just addr' | addr' == addr -> r -- avoid recursive definition+ _ -> Allocator (M.insert addr obj s) c++store :: (Reference a, Eq a) => a -> Br (LState a) a+store a = do+ st <- getBy allocator+ let (n, st') = alloc a st+ _ <- putBy $ allocator' st'+ return $ mkRef n+++-- update state+update :: Reference a => Addr -> a -> Br (LState a) ()+update addr obj = getBy allocator >>= putBy . allocator' . renew addr obj+++load :: Addr -> Br (LState a) a+load addr =+ ((M.! addr) . storage) <$> getBy allocator+++tryLoad :: Addr -> Br (LState a) (Maybe a)+tryLoad addr =+ (M.lookup addr . storage) <$> getBy allocator+++-- for the system which take leverage of generics+new :: Reference a => Br (LState a) Addr+new = do+ st <- getBy allocator+ let (addr', st') = inc st+ _ <- putBy $ allocator' st'+ return addr'++negUnify :: Reference a => a -> a -> Br (LState a) ()+negUnify a b = do+ negs <- getBy negPairs+ if check negs then+ putBy $ negPairs' ((a, b) : negs)+ else return ()+ where+ check [] = True+ check ((a', b'):xs)+ | (a', b') == (a, b) || (a', b') == (b, a) = False+ | otherwise = check xs+++emptyAllocator = Allocator M.empty 0+emptyLState = LState emptyAllocator [] []
+ src/RSolve/Logic.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE GADTs #-}+module RSolve.Logic where+import RSolve.BrMonad+import RSolve.Infr+import Data.List (nub)+import Control.Applicative++data Cond a where+ Unify :: Unify a => a -> a -> Cond a+ Not :: Cond a -> Cond a+ Pred :: Br (LState a) Bool -> Cond a++ Or :: Cond a -> Cond a -> Cond a+ And :: Cond a -> Cond a -> Cond a+ Imply :: Cond a -> Cond a -> Cond a++solve :: Cond a -> Br (LState a) ()+solve (Unify l r) = do+ l <- prune l+ r <- prune r+ unify l r++solve (Or l r) =+ solve l <|> solve (And (Not l) r)++solve (And l r) =+ solve l >> solve r++solve (Imply l r) =+ solve (Not l) <|> solve r++solve (Pred c) = do+ cs <- getBy constrains+ putBy $ constrains' (c:cs)++solve (Not emmm) =+ case emmm of+ Pred c -> solve $ Pred (not <$> c)+ Not emmm -> solve emmm+ Or l r -> solve $ And (Not l)(Not r)+ And l r -> solve $ Or (Not l)(Not r)+ Imply l r -> solve $ And l (Not r)+ Unify l r -> do+ l <- prune l+ r <- prune r+ negUnify l r++solveNeg :: Unify a => Br (LState a) ()+solveNeg = do+ negs <- getBy negPairs+ negs <- pruneTuples negs+ solveNeg' $ nub (negs)+ where+ pruneTuples [] = return []+ pruneTuples ((a, b):xs) = do+ a <- prune a+ b <- prune b+ xs' <- pruneTuples xs+ let+ process (Just a) (Just b) = x:xs+ where+ mkRef2 a b = (mkRef a, mkRef b)+ x = if a > b then mkRef2 a b else mkRef2 b a+ process _ _ = (a, b):xs'+ return $ process (isRef a) (isRef b)+ solveNeg' [] = return ()+ solveNeg' ((a,b):xs) =+ (a `complement` b) >> solveNeg' xs++solvePred :: EnumSet a => Br (LState a) ()+solvePred = do+ _ <- toEnumerable+ cs <- getBy constrains+ checkPredicate cs+ where+ checkPredicate [] = return ()+ checkPredicate (x:xs) = do+ x <- x+ if x then checkPredicate xs+ else empty++require :: Unify a => a -> Br (LState a) a+require a = do+ a <- prune a+ case isRef a of+ Just a -> load a+ _ -> return a++
+ src/RSolve/Options/Core.hs view
@@ -0,0 +1,102 @@+module RSolve.Options.Core where+import RSolve.BrMonad+import RSolve.Infr+import RSolve.Logic+import Control.Monad+import Control.Applicative+import Prelude hiding (not, or, and)+import qualified Data.Set as S+import qualified Data.Map as M+import qualified Data.List as L++data Option = A | B | C | D+ deriving (Eq, Show, Ord, Enum)++data Term = Var Int | Sol (S.Set Option)+ deriving (Eq, Show)++pruneSol :: Term -> Br (LState Term) (Int, Maybe (S.Set Option))+pruneSol (Var addr) = do+ t <- load addr+ case t of+ Var addr' -> do+ r @ (addrLast, _) <- pruneSol t+ update addr (Var addrLast) >> return r+ Sol lxs ->+ return (addr, Just lxs)+ -- if S.null lxs then error "emmm"+ -- else return (addr, Just lxs)++pruneSol r @ (Sol xs) =+ store r >>= \(Var addr) ->+ return (addr, Just xs)++instance Reference Term where+ isRef (Var addr) = Just addr+ isRef _ = Nothing+ mkRef a = Var a++++instance Unify Term where+ prune a = pruneSol a >>= return . Var . fst+ unify l r =+ pruneSol l >>= \(lFrom, lxsm) ->+ pruneSol r >>= \(rFrom, rxsm) ->+ case (lxsm, rxsm) of+ (Nothing, _) -> update lFrom (Var rFrom)+ (Just lxs, _) | S.null lxs -> empty+ (_, Just rxs) | S.null rxs -> empty+ (Just _, Nothing ) -> unify r l+ (Just lxs, Just rxs) ->+ let xs = S.intersection lxs rxs in+ if S.null xs+ then empty+ else do+ new <- store $ Sol xs+ update lFrom new >> update rFrom new++ complement l r = do+ (l, Just lxs) <- pruneSol l+ (r, Just rxs) <- pruneSol r+ case (S.size lxs, S.size rxs) of+ (1, 1) | lxs == rxs -> empty+ (1, 1) | lxs /= rxs -> return ()+ (nl, nr) | nl < nr -> complement (Var r) (Var l)+ (nl, nr) | nl >= nr -> do+ let+ x:xs = L.map f . S.toList $ rxs+ f :: Option -> Br (LState Term) ()+ f re =+ let lnew_set = S.delete re lxs+ in+ if S.null lnew_set+ then empty+ else do+ lnew <- store . Sol $ lnew_set+ rnew <- store . Sol . S.singleton $ re+ update l lnew >> update r rnew+ L.foldl (<|>) x xs++instance EnumSet Term where+ toEnumerable = do+ st <- getBy $ storage . allocator+ M.foldlWithKey f (return ()) st+ where+ f :: Br (LState Term) () -> Addr -> Term -> Br (LState Term) ()+ f a k b =+ case b of+ Var _ -> a+ Sol set ->+ let+ lst = S.toList set+ g :: [Option] -> Br (LState Term) ()+ g [] = error "unexpected"+ g (x:xs) = do+ x <- store . Sol . S.singleton $ x+ let s = update k x+ case xs of+ [] -> s+ _ -> s <|> g xs+ in a >> g lst+
+ src/RSolve/Options/Example.hs view
@@ -0,0 +1,186 @@+module RSolve.Options.Example where+import RSolve.Options.Core+import RSolve.BrMonad+import RSolve.Infr+import RSolve.Logic+import Control.Monad+import Prelude hiding (not, or, and)+import qualified Data.Set as S+import qualified Data.Map as M+import qualified Data.List as L++nub = L.nub+sol = Sol . S.fromList+total = [A, B, C, D]+toSol a = do+ (_, Just b) <- pruneSol a+ if S.size b /= 1 then error $ show b+ else return $ S.elemAt 0 b+eq a b = Unify a b+neq a b = Not $ a `eq` b+not = Not+and = And+or = Or+(|-) a b = Imply a b++(==>) :: Option -> (Cond Term) -> Term -> (Cond Term)+(==>) a b c = c `eq` sol [a] `and` b++(|||) :: (Term -> (Cond Term)) -> (Term -> Cond Term) -> (Term -> Cond Term)+a ||| b = \t -> a t `or` b t++for :: Term -> (Term -> Cond Term) -> Br (LState Term) ()+for a f = solve $ f a++infixr 7 `eq`, `neq`+infixr 5 `or`+infixr 6 `and`, |-+infixr 4 ==>+infixr 3 |||++test = do+ _1 <- store $ sol total+ _2 <- store $ sol total+ _3 <- store $ sol total+ _4 <- store $ sol total+ _5 <- store $ sol total+ _6 <- store $ sol total+ _7 <- store $ sol total+ _8 <- store $ sol total+ _9 <- store $ sol total+ _10 <- store $ sol total+ _ <- for _2 $+ A ==> _5 `eq` sol [C] |||+ B ==> _5 `eq` sol [D] |||+ C ==> _5 `eq` sol [A] |||+ D ==> _5 `eq` sol [B]+ _ <- for _3 $+ let+ diff3 :: [Term] -> Term -> Cond Term+ diff3 lst a =+ let conds = [a `neq` e | e <- L.delete a lst]+ in case conds of+ [] -> error "emmm"+ x:xs -> L.foldl and x xs+ f = diff3 [_3, _6, _2, _4]+ in A ==> f _3 |||+ B ==> f _6 |||+ C ==> f _2 |||+ D ==> f _4+ _ <- for _4 $+ A ==> _1 `eq` _5 |||+ B ==> _2 `eq` _7 |||+ C ==> _1 `eq` _9 |||+ D ==> _6 `eq` _10+ _ <- for _5 $+ A ==> _5 `eq` _8 |||+ B ==> _5 `eq` _4 |||+ C ==> _5 `eq` _9 |||+ D ==> _5 `eq` _7+ _ <- for _6 $+ A ==> _2 `eq` _8 `and` _4 `eq` _8 |||+ B ==> _1 `eq` _8 `and` _6 `eq` _8 |||+ C ==> _3 `eq` _8 `and` _10 `eq` _8 |||+ D ==> _5 `eq` _8 `and` _9 `eq` _8+ let+ solution = do+ mapM toSol [_1, _2, _3, _4, _5, _6, _7, _8, _9, _10]+ count :: Br (LState Term) (M.Map Option Int)+ count = do+ solution <- solution+ return . countImpl $ solution+ where+ countImpl :: [Option] -> M.Map Option Int+ countImpl [] = M.empty+ countImpl (x:xs) = M.alter f x $ countImpl xs+ f Nothing = Just 1+ f (Just a) = Just $ a + 1+ msearch cond = do+ count <- count+ return $ M.foldlWithKey f [] count+ where+ f [] k v = [(k, v)]+ f r@((k', v'):_) k v =+ case compare v v' of+ a | a == cond -> [(k, v)]+ EQ -> (k, v) : r+ _ -> r+ msearchNSuite :: (Int -> Int -> Bool) -> Option -> Br (LState Term) (Maybe Int)+ msearchNSuite cond opt = do+ count <- count+ case M.lookup opt count of+ Nothing -> do++ return (Just 0)+ Just n ->+ let+ f Nothing k v = Nothing+ f r@(Just a) k v =+ if cond v n then Nothing+ else r+ in return $ M.foldlWithKey f (Just n) count+ _ <- for _7 $+ let minIs a =+ let m = do+ lst <- msearch LT+ return $ L.all (\(k, v) -> k == a) lst+ in Pred m+ in A ==> minIs C |||+ B ==> minIs B |||+ C ==> minIs A |||+ D ==> minIs D+ _ <- for _8 $+ let+ notAdjacent a b = do+ a <- toSol a+ b <- toSol b+ let sep = (fromEnum a - fromEnum b)+ return $ abs(sep) > 1+ in A ==> Pred (notAdjacent _1 _7) |||+ B ==> Pred (notAdjacent _1 _5) |||+ C ==> Pred (notAdjacent _1 _2) |||+ D ==> Pred (notAdjacent _1 _10)+ _ <- for _9 $+ let+ f x =+ let a = _1 `eq` _6 in+ let b = x `eq` _5 in+ not a `and` b `or` not b `and` a+ in A ==> f _6 |||+ B ==> f _10 |||+ C ==> f _2 |||+ D ==> f _9+ _ <- for _10 $+ let+ by a =+ Pred m+ where m = do+ (_, minCount):_ <- msearch LT+ (_, maxCount):_ <- msearch GT+ return $ maxCount - minCount == a+ in A ==> by 3 |||+ B ==> by 2 |||+ C ==> by 4 |||+ D ==> by 1+ _ <- solveNeg+ _ <- solvePred+ mapM require [_1, _2, _3, _4, _5, _6, _7, _8, _9, _10]++format :: [String] -> [[Term]] -> IO ()+format names xs =+ let+ formatCell :: (String, Term) -> IO()+ formatCell (a, b) = putStrLn $ show a ++ " : " ++ show b+ formatLine :: [(String, Term)] -> IO()+ formatLine xs = do+ _ <- putStrLn "===="+ forM_ xs formatCell+ formatLines xs =+ forM_ xs $ \line -> formatLine $ L.zip names line+ in formatLines xs++++optionExample = do+ format [show i | i <- [1..10]] . nub . L.map fst+ $ runBr test emptyLState