RSolve 0.1.0.0 → 0.1.0.1
raw patch · 7 files changed
+23/−285 lines, 7 filesdep −RSolve
Dependencies removed: RSolve
Files
- README.md +8/−8
- RSolve.cabal +10/−10
- src/Main.hs +0/−26
- src/RSolve/BrMonad.hs +4/−0
- src/RSolve/HM/Core.hs +1/−1
- src/RSolve/HM/Example.hs +0/−54
- src/RSolve/Options/Example.hs +0/−186
README.md view
@@ -1,7 +1,8 @@ # RSolve -A general solver for type checkers of programming languages and real world puzzles with complex constraints. +[](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
RSolve.cabal view
@@ -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
− src/Main.hs
@@ -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
src/RSolve/BrMonad.hs view
@@ -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 =
src/RSolve/HM/Core.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE GADTs #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE TupleSections #-}
− src/RSolve/HM/Example.hs
@@ -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
− src/RSolve/Options/Example.hs
@@ -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