diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,7 +1,8 @@ # RSolve -A general solver for type checkers of programming languages and real world puzzles with complex constraints. +[![](https://img.shields.io/hackage/v/RSolve.svg)](hackage.haskell.org/package/RSolve) +A general solver for type checkers of programming languages and real world puzzles with complex constraints. ## Preview @@ -9,7 +10,7 @@ ### The Most Graceful Hindley-Milner Unification -Check `RSolve.HM.Core` and `RSolve.HM.Example`. +Check `RSolve.HM.Core` and `RSolve.HM.Example`. Uncomment the code in `Main.hs` could reproduce following program: @@ -23,8 +24,8 @@ u2 <- new u3 <- new u4 <- new - -- u1 -> u2 where u1, u2 is not generic - let arrow_var = Op Arrow (Var u1) (Var u2) + -- 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 @@ -41,7 +42,6 @@ _ <- solveNeg mapM require [Var u1, Var u2, arrow_inst1, arrow_inst2, arrow_generic, arrow_match] - ``` output: @@ -57,7 +57,7 @@ ### N-Option Puzzles -This implememtation is presented at `RSolve.Options`, which provides the abstractions to solve all kinds of puzzles described with options. +This implementation 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: @@ -75,8 +75,8 @@ _ <- solve $ b `neq` c _ <- solveNeg -- `Not` condition requires this _ <- solvePred -- unnecessary - mapM require [a, b, c] - + mapM require [a, b, c] + main = do format ["a", "b", "c"] . nub . L.map fst $ runBr test2 emptyLState diff --git a/RSolve.cabal b/RSolve.cabal --- a/RSolve.cabal +++ b/RSolve.cabal @@ -1,5 +1,5 @@ name: RSolve -version: 0.1.0.0 +version: 0.1.0.1 synopsis: A general solver for equations description: A general solver for type checkers of programming languages and real world puzzles with complex constraints. @@ -29,13 +29,13 @@ , 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 +-- 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 diff --git a/src/Main.hs b/src/Main.hs deleted file mode 100644 --- a/src/Main.hs +++ /dev/null @@ -1,26 +0,0 @@ -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 diff --git a/src/RSolve/BrMonad.hs b/src/RSolve/BrMonad.hs --- a/src/RSolve/BrMonad.hs +++ b/src/RSolve/BrMonad.hs @@ -1,5 +1,6 @@ module RSolve.BrMonad where import Control.Monad +import Control.Monad.Fail import Control.Applicative newtype Br s a = Br {runBr :: s -> [(a, s)]} @@ -10,6 +11,9 @@ instance Applicative (Br s) where pure = return (<*>) = ap + +instance MonadFail (Br s) where + fail _ = empty instance Monad (Br s) where m >>= k = diff --git a/src/RSolve/HM/Core.hs b/src/RSolve/HM/Core.hs --- a/src/RSolve/HM/Core.hs +++ b/src/RSolve/HM/Core.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE GADTs #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE TupleSections #-} diff --git a/src/RSolve/HM/Example.hs b/src/RSolve/HM/Example.hs deleted file mode 100644 --- a/src/RSolve/HM/Example.hs +++ /dev/null @@ -1,54 +0,0 @@ -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 diff --git a/src/RSolve/Options/Example.hs b/src/RSolve/Options/Example.hs deleted file mode 100644 --- a/src/RSolve/Options/Example.hs +++ /dev/null @@ -1,186 +0,0 @@ -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