RSolve 0.1.0.1 → 2.0.0.0

raw patch · 15 files changed

+682/−531 lines, 15 filesdep +RSolvedep +lensdep +mtldep ~basenew-component:exe:RSolve-exePVP ok

version bump matches the API change (PVP)

Dependencies added: RSolve, lens, mtl

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• ChangeLog.md +6/−0
• README.md +123/−63
• RSolve.cabal +71/−35
• app/Main.hs +2/−0
• src/RSolve/BrMonad.hs +0/−30
• src/RSolve/HM.hs +208/−0
• src/RSolve/HM/Core.hs +0/−115
• src/RSolve/Infr.hs +0/−99
• src/RSolve/Logic.hs +6/−87
• src/RSolve/MapLike.hs +51/−0
• src/RSolve/MultiState.hs +43/−0
• src/RSolve/Options/Core.hs +0/−102
• src/RSolve/PropLogic.hs +72/−0
• src/RSolve/Solver.hs +8/−0
• test/Spec.hs +92/−0

@@ -0,0 +1,6 @@+## 1.0.0.0+- 2019-08-04+    - Removed the general solver tentatively(for maintainability and good design).+    - Separated the logic formulas from the problem domains.+    - Removed the solver for `Options`.+    - Re-implemented the solver for `HM`.

@@ -1,93 +1,153 @@ # RSolve -[![](https://img.shields.io/hackage/v/RSolve.svg)](hackage.haskell.org/package/RSolve)+[![](https://img.shields.io/hackage/v/RSolve.svg)](https://hackage.haskell.org/package/RSolve) -A general solver for type checkers of programming languages and real world puzzles with complex constraints.+NOTE: NO LONGER for general logic programming, this package is now dedicated for the simple propositional logic. -## Preview+The README is going to get updated. -Here are 2 special cases presented in the following sections to show how powerful `RSolve` is.+## Propositional Logic -### The Most Graceful Hindley-Milner Unification+RSolve uses [disjunctive normal form](https://en.wikipedia.org/wiki/Disjunctive_normal_form) to solve logic problems. -Check `RSolve.HM.Core` and `RSolve.HM.Example`.+This disjunctive normal form works naturally with the logic problems where the atom formulas can be generalized to an arbitrary equation in the problem domain by introducing a problem domain specific solver. A vivid+example can be found at `RSolve.HM`, where+I implemented an extended algo-W for [HM unification](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system). -Uncomment the code in `Main.hs` could reproduce following program: +To take advantage of RSolve, we should implement 2 classes:++- `AtomF`, which stands for the atom formula.++- `CtxSolver`, which stands for the way to solve a bunch of atom formulas.++However we might not need to a solver sometimes:+ ```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)+data Value = A | B | C | D+    deriving (Show, Eq, Ord, Enum) -    let arrow_match = Op Arrow (Var u4) (Var u4)+data At = At {at_l :: String, at_r :: Value}+    deriving (Show, Eq, Ord) -    _ <- solve $ Unify arrow arrow_var-    _ <- solve $ Unify arrow_inst1 arrow_match-    _ <- solve $ Unify arrow_generic arrow_inst1-    _ <- solve $ Unify arrow_generic arrow_inst2-    _ <- solveNeg+instance AtomF At where+    notA At {at_l = lhs, at_r = rhs} =+        let wholeSet  = enumFrom (toEnum 0) :: [Value]+            contrasts = delete rhs wholeSet+        in [At {at_l = lhs, at_r = rhs'} | rhs' <- contrasts] -    mapM require [Var u1, Var u2, arrow_inst1, arrow_inst2, arrow_generic, arrow_match]-```+infix 6 <==>+s <==> v = Atom $ At s v -output:+equations = do+    assert $ "a" <==> A :||: "a" <==> B+    assert $ Not ("a" <==> A) +main =+  let equationGroups = unionEquations equations+  in forM equationGroups print ```-u1 : Int-u2 : Float-arrow_inst1 : (Int -> Int)-arrow_inst2 : (Float -> Float)-arrow_generic : forall  a2.(a2 -> a2)-arrow_match : (Int -> Int)+produces+```haskell+[At {at_l = "a", at_r = A},At {at_l = "a", at_r = B}]+[At {at_l = "a", at_r = A},At {at_l = "a", at_r = C}]+[At {at_l = "a", at_r = A},At {at_l = "a", at_r = D}]+[At {at_l = "a", at_r = B}]+[At {at_l = "a", at_r = B},At {at_l = "a", at_r = C}]+[At {at_l = "a", at_r = B},At {at_l = "a", at_r = C},At {at_l = "a", at_r = D}]+[At {at_l = "a", at_r = B},At {at_l = "a", at_r = D}] ``` -### N-Option Puzzles+According to the property of the problem domain, we can figure out that+only the 4-th(1-based indexing) equation group+`[At {at_l = "a", at_r = B}]`+will produce a feasible solution because symbol `a` can+only hold one value. -This implementation is presented at `RSolve.Options`,  which provides the abstractions to solve all kinds of puzzles described with options.+When do we need a solver? For instance, type checking&inference. -A Hello World program could be found at `src/Main.hs` which solves a complex problem described with following link:+In this case, we need type checking environments to represent the checking states: -https://www.zhihu.com/question/68411978/answer/558913247.+```haskell+data TCEnv = TCEnv {+          _noms  :: M.Map Int T  -- nominal type ids+        , _tvars :: M.Map Int T  -- type variables+        , _neqs  :: S.Set (T, T) -- negation constraints+    }+    deriving (Show) +emptyTCEnv = TCEnv M.empty M.empty S.empty+``` -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:+For sure we also need to represent the type:  ```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+data T+    = TVar Int+    | TFresh String+    | T :-> T+    | T :*  T -- tuple+    | TForall (S.Set String) T+    | TApp T T -- type application+    | TNom Int -- nominal type index+    deriving (Eq, Ord) ``` -output:+Then the atom formula of HM unification is: +```haskell+data Unif+    = Unif {+          lhs :: T+        , rhs :: T+        , neq :: Bool -- lhs /= rhs or  lhs == rhs?+      }+  deriving (Eq, Ord) ```-λ stack exec RSolve-====-"a" : Sol (fromList [B])-"b" : Sol (fromList [B])-"c" : Sol (fromList [C])++We then need to implement this:++```haskell+-- class AtomF a => CtxSolver s a where+--     solve :: a -> MS s ()+prune :: T -> MS TCEnv T -- MS: MultiState+instance CtxSolver TCEnv Unif where+  solver = ...+````++Finally we got this:++```haskell+infixl 6 <=>+a <=> b = Atom $ Unif {lhs=a, rhs=b, neq=False}+solu = do+    a <- newTVar+    b <- newTVar+    c <- newTVar+    d <- newTVar+    let [eqs] = unionEquations $+                do+                assert $ TVar a <=> TForall (S.fromList ["s"]) ((TFresh "s") :-> (TFresh "s" :* TFresh "s"))+                assert $ TVar a <=> (TVar b :-> (TVar c :* TVar d))+                assert $ TVar d <=> TNom 1+    -- return eqs+    forM_ eqs solve+    return eqs+    a <- prune $ TVar a+    b <- prune $ TVar b+    c <- prune $ TVar c+    return (a, b, c)++test :: Eq a => String -> a -> a -> IO ()+test msg a b+    | a == b = return ()+    | otherwise = print msg++main = do+    forM (unionEquations equations) print++    let (a, b, c):_ = map fst $ runMS solu emptyTCEnv+    test "1 failed" (show a) "@t1 -> @t1 * @t1"+    test "2 failed" (show b) "@t1"+    test "3 failed" (show c) "@t1" ```

@@ -1,41 +1,77 @@-name:                RSolve-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.-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+cabal-version: 1.12 +-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: e5b30745fe99238706cc93bcd6a0c1fe3d35090d5dc5cabf244120d6d382d56c++name:           RSolve+version:        2.0.0.0+description:    A general solver for equations+category:       Logic,Unification+homepage:       https://github.com/thautwarm/RSolve#readme+bug-reports:    https://github.com/thautwarm/RSolve/issues+author:         thautwarm+maintainer:     twshere@outlook.com+copyright:      2018, 2019 thautwarm+license:        MIT+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md+ source-repository head-  type:     git-  location: https://github.com/thautwarm/Rsolver.git+  type: git+  location: https://github.com/thautwarm/RSolve  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+  exposed-modules:+      RSolve.HM+      RSolve.Logic+      RSolve.MapLike+      RSolve.MultiState+      RSolve.PropLogic+      RSolve.Solver+  other-modules:+      Paths_RSolve+  hs-source-dirs:+      src+  build-depends:+      base >=4.7 && <5+    , containers+    , lens+    , mtl+  default-language: Haskell2010 --- 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 RSolve-exe+  main-is: Main.hs+  other-modules:+      Paths_RSolve+  hs-source-dirs:+      app+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      RSolve+    , base >=4.7 && <5+    , containers+    , lens+    , mtl+  default-language: Haskell2010 +test-suite RSolve-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      Paths_RSolve+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      RSolve+    , base >=4.7 && <5+    , containers+    , lens+    , mtl+  default-language: Haskell2010

@@ -0,0 +1,2 @@+module Main where+main = putStrLn "No CLI support yet"

@@ -1,30 +0,0 @@-module RSolve.BrMonad where-import Control.Monad-import Control.Monad.Fail-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 MonadFail (Br s) where-  fail _ = empty--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)]

@@ -0,0 +1,208 @@+-- | HM unification implementations based on propositional logics,+--   based on nominal type system.+-- Author: Taine Zhao(thautwarm)+-- Date: 2019-08-04+-- License: MIT+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE MultiParamTypeClasses #-}++module RSolve.HM+where+import RSolve.Logic+import RSolve.Solver+import RSolve.MultiState+import Control.Lens (Lens', view, over, makeLenses)+import Control.Applicative+import Control.Monad+import Debug.Trace++import qualified Data.List as L+import qualified Data.Map  as M+import qualified Data.Set  as S++type Fix a = a -> a++infixl 6 :->, :*++data T+    = TVar Int+    | TFresh String+    | T :-> T+    | T :*  T -- tuple+    | TForall (S.Set String) T+    | TApp T T -- type application+    | TNom Int -- nominal type index+    deriving (Eq, Ord)++deConsTOp :: T -> Maybe (T -> T -> T, T, T)+deConsTOp = \case+    a :-> b  -> Just ((:->), a, b)+    a :*  b  -> Just ((:*),  a, b)+    TApp a b -> Just (TApp,  a, b)+    _ -> Nothing++instance Show T where+    show = \case+        TVar idx    -> "@" ++ show idx+        TFresh s    -> s+        a :-> b     -> showNest a ++ " -> " ++ show b+        a :*  b     -> showNest a ++ " * " ++ show b+        TForall l t -> "forall " ++ (unwords $ S.toList l) ++ ". " ++ show t+        TApp t1 t2  -> show t1 ++ " " ++ showNest t2+        TNom i       -> "@t" ++ show i+        where+            showNest s+                | isNest s  = "(" ++ show s ++ ")"+                | otherwise = show s+            isNest s = case s of+                TApp _ _    -> True+                TForall _ s -> isNest s+                _ :-> _     -> True+                _ :* _      -> True+                _           -> False++data Unif+    = Unif {+          lhs :: T+        , rhs :: T+        , neq :: Bool+      }+    deriving (Eq, Ord)++instance Show Unif where+    show Unif {lhs, rhs, neq} =+        let op = if neq then " /= " else " == "+        in  show lhs ++ op ++ show rhs++instance AtomF Unif where+    notA a@Unif {neq} = [a {neq = not neq}]++data TCEnv = TCEnv {+          _noms  :: M.Map Int T  -- nominal type ids+        , _tvars :: M.Map Int T  -- type variables+        , _neqs  :: S.Set (T, T) -- negation constraints+    }+    deriving (Show)++emptyTCEnv = TCEnv M.empty M.empty S.empty++makeLenses ''TCEnv++newTVar :: MS TCEnv Int+newTVar = do+    i <- getsMS $ M.size . view tvars+    modifyMS $ over tvars $ M.insert i (TVar i)+    return i++newTNom :: MS TCEnv Int+newTNom = do+    i <- getsMS $ M.size . view noms+    modifyMS $ over noms $ M.insert i (TNom i)+    return i++loadTVar :: Int -> MS TCEnv T+loadTVar i = getsMS $ (M.! i) . view tvars++occurIn :: Int -> T -> MS TCEnv Bool+occurIn l = contains+    where+        contains (deConsTOp -> Just (_, a, b)) = (||) <$> contains a <*> contains b+        contains (TNom _)      = return False+        contains (TForall _ a) = contains a+        contains (TFresh _)    = return False+        contains (TVar a)+            | a == l           = return True+            | otherwise        = do+                tvar <- loadTVar a+                case tvar of+                    TVar a' | a' == a -> return False+                    _                 -> contains tvar++free :: M.Map String T -> T -> T+free m = mkFree+    where+        mkFree (deConsTOp -> Just (op, a, b)) = op (mkFree a) (mkFree b)+        mkFree a@(TNom i)       = a+        mkFree (TForall n t)    = TForall n $ flip free t $ M.withoutKeys m n+        mkFree a@(TVar _)       = a+        mkFree a@(TFresh id)    = M.findWithDefault a id m++prune :: T -> MS TCEnv T+prune = \case+        (deConsTOp   -> Just (op, a, b)) -> op <$> prune a <*> prune b+        a@(TNom i)   -> return a+        TVar i       ->+            loadTVar i >>= \case+                a@(TVar  i') | i' == i -> return a+                a                      -> do+                    t <- prune a+                    update i t+                    return t++        a@(TFresh _) -> return a+        TForall a b  -> TForall a <$> prune b++update :: Int -> T -> MS TCEnv ()+update i t = modifyMS $ over tvars $ M.insert i t++addNEq :: (T, T) -> MS TCEnv ()+addNEq t = modifyMS $ over neqs (S.insert t)++unify :: Fix (Unif -> MS TCEnv ())+unify self Unif {lhs, rhs, neq=True} = addNEq (lhs, rhs)++unify self Unif {lhs=TNom a, rhs=TNom b}+    | a == b      = return ()+    | otherwise   = empty++unify self Unif {lhs=TVar a, rhs = TVar b} = do+    recursive <- occurIn a (TVar b)+    if recursive+    then error "ill formed definition like a = a -> b"+    else update a (TVar b)++unify self Unif {lhs=TVar id, rhs, neq} = update id rhs++unify self a@Unif {lhs, rhs=rhs@(TVar _)} = self a {lhs=rhs, rhs=lhs}++-- type operators are not frist class+unify self Unif {lhs=l1 :-> l2, rhs= r1 :-> r2} =+    self Unif {lhs=l1, rhs=r1, neq=False} >>+    self Unif {lhs=l2, rhs=r2, neq=False}++unify self Unif {lhs=l1 :* l2, rhs= r1 :* r2} =+    self Unif {lhs=l1, rhs=r1, neq=False} >>+    self Unif {lhs=l2, rhs=r2, neq=False}++-- TODO: type aliases?+unify self Unif {lhs=TApp l1 l2, rhs= TApp r1 r2} =+    self Unif {lhs=l1, rhs=r1, neq=False} >>+    self Unif {lhs=l2, rhs=r2, neq=False}++unify self Unif {lhs=TForall freevars poly, rhs} = do+    pairs <- mapM freepair $ S.toList freevars+    let freemap = M.fromList pairs+    let l = free freemap poly+    self Unif {lhs=l, rhs=rhs, neq=False}+    where freepair freevar = (freevar,) . TVar <$> newTVar++unify self a@Unif {lhs, rhs=rhs@(TForall _ _)} =+    self a {lhs=rhs, rhs=lhs}++instance CtxSolver TCEnv Unif where+    solve =+        let frec = unify (pruneUnif >=> frec)+        in  pruneUnif >=> frec+        where+            pruneUnif a@Unif {neq=True} = return a+            pruneUnif a@Unif {lhs, rhs} = do+                lhs <- prune lhs+                rhs <- prune rhs+                return $ a {lhs=lhs , rhs=rhs}+++

@@ -1,115 +0,0 @@-{-# 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--

@@ -1,99 +0,0 @@-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 [] []

@@ -1,89 +1,8 @@-{-# 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--+-- atom formula+class (Show a, Ord a) => AtomF a where+    -- | Specifies how to handle the negations.+    --   For the finite and enumerable solutions,+    --   we can return its supplmentary set.+    notA :: a -> [a]

@@ -0,0 +1,51 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}++module RSolve.MapLike where+import Data.Maybe+import Data.Kind+import Prelude hiding (lookup, insert)+import qualified Data.Map  as M+import qualified Data.List as L+import qualified Data.Set  as S++class MapLike m k v | m -> k, m -> v where+    lookup :: k -> m -> Maybe v+    (!)    :: m -> k -> v+    m ! k  = fromJust (lookup k m)+    insert :: k -> v -> m -> m+    adjust :: (v -> v) -> k -> m -> m+    member :: k -> m -> Bool+    update :: (v -> Maybe v) -> k -> m -> m+++instance Ord k => MapLike (M.Map k v) k v where+    lookup = M.lookup+    (!) = (M.!)+    insert = M.insert+    adjust = M.adjust+    member = M.member+    update = M.update++instance Eq k => MapLike [(k, v)] k v where+    lookup = L.lookup+    insert k v = \case+        []   -> [(k, v)]+        (k', v'):xs | k' == k -> (k, v):xs+        x:xs -> x:insert k v xs+    adjust f k = \case+        []   -> []+        (k', v):xs | k' == k -> (k', f v):xs+        x:xs -> x:adjust f k xs+    k `member` m = case lookup k m of+            Just  _ -> True+            Nothing -> False+    update f k = \case+        [] -> []+        hd@(k', v):xs | k == k' ->+            case f v of+                Just v'  -> (k, v'):tl+                Nothing  -> hd:tl+            where tl = update f k xs

@@ -0,0 +1,43 @@+-- | state monads extended to have branches+-- Author: Taine Zhao(thautwarm)+-- Date: 2018-12+-- License: MIT+module RSolve.MultiState where+import Control.Monad+import Control.Monad.Fail+import Control.Applicative++newtype MS s a = MS {runMS :: s -> [(a, s)]}++instance Functor (MS s) where+  fmap = liftM++instance Applicative (MS s) where+  pure = return+  (<*>)  = ap++instance MonadFail (MS s) where+  fail _ = empty++instance Monad (MS s) where+  m >>= k =+    MS $ \s ->+       let xs = runMS m s+       in join [runMS (k a) s' | (a, s') <- xs]+  return a = MS $ \s -> [(a, s)]++instance Alternative (MS s) where+  empty = MS $ const []+  ma <|> mb = MS $ \s -> runMS ma s ++ runMS mb s++getMS  :: MS s s+getMS = MS $ \s -> [(s, s)]++putMS  :: s -> MS s ()+putMS s = MS $ const [((), s)]++getsMS :: (s -> a) -> MS s a+getsMS f = MS $ \s -> [(f s, s)]++modifyMS :: (s -> s) -> MS s ()+modifyMS f = MS $ \s -> [((), f s)]

@@ -1,102 +0,0 @@-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-

@@ -0,0 +1,72 @@+-- | Propositional logic infrastructures+-- Author: Taine Zhao(thautwarm)+-- Date: 2019-08-03+-- License: MIT+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE DeriveFunctor #-}++module RSolve.PropLogic+    (AtomF(..), WFF(..), NF(..), assertNF, normal, assert, unionEquations)+where++import RSolve.Logic+import RSolve.MultiState+import Control.Applicative ((<|>))+import qualified Data.Set as S++infixl 5 :&&, :&&:+infixl 3 :||, :||:, :=>:++data WFF a+    -- | Atom formula, should be specified by the problem+    = Atom a+    | Not  (WFF a)+    -- | And+    | WFF a :&&: WFF a+    -- | Or+    | WFF a :||: WFF a+    -- | Implication+    | WFF a :=>:  WFF a+    deriving (Functor, Eq, Ord)++-- | normalized WWF, where '[NF a]' the disjunctive normal form.+data NF a+    = AtomN a+    | NF a :&& NF a+    | NF a :|| NF a+    deriving (Functor, Eq, Ord)++normal :: AtomF a => WFF a -> NF a+normal = \case+    Atom a -> AtomN a+    p1 :&&: p2  -> normal p1 :&& normal p2+    p1 :||: p2  -> normal p1 :|| normal (Not p1 :&&: p2)+    Not (Atom a) ->+        case map AtomN $ notA a of+            hd:tl -> foldl (:||) hd tl+            []    -> error $ "Supplementary set of " ++ show a ++ " is empty!"+    Not (Not p)  -> normal p+    Not (p1 :&&: p2) -> normal (Not p1) :|| normal (Not p2)+    Not (p1 :||: p2) -> normal (Not p1) :&& normal (Not p2)+    Not (p1 :=>: p2) -> normal (Not p1 :||: p2)++assertNF :: AtomF a => NF a -> MS (S.Set a) ()+assertNF = \case+    AtomN a   -> modifyMS (S.insert a)+    p1 :&& p2 -> assertNF p1 >> assertNF p2+    p1 :|| p2 -> assertNF p1 <|> assertNF p2+++-- | Use a propositinal logic formula to build logic equations+--   incrementally.+assert :: AtomF a => WFF a -> MS (S.Set a) ()+assert = assertNF . normal++-- | Produced a list of disjunctions of conjunctive clauses.+unionEquations :: AtomF a  => MS (S.Set a) () -> [[a]]+unionEquations m =+    -- get states+    let sts = map snd $ runMS m S.empty+    -- unique states+    in map S.toList . S.toList . S.fromList $ sts+

@@ -0,0 +1,8 @@+{-# LANGUAGE MultiParamTypeClasses #-}+module RSolve.Solver where+import RSolve.Logic+import RSolve.MultiState++class AtomF a => CtxSolver s a where+    -- | Give a atom formula and solve it+    solve :: a -> MS s ()

@@ -0,0 +1,92 @@+-- import RSolve.Options.Example+-- import RSolve.HM.Example+++-- test1 =+--     putStrLn "HM unification"   >>+--     hmUnificationExample        >>+--     putStrLn "4-option puzzles" >>+--     optionExample++-- main = print 233+++-- 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++import RSolve.HM+import RSolve.PropLogic+import RSolve.MultiState+import RSolve.Solver+import Control.Monad++import qualified Data.Set as S++import Data.List (delete)+import Control.Monad++data Value = A | B | C | D+    deriving (Show, Eq, Ord, Enum)++data At = At {at_l :: String, at_r :: Value}+    deriving (Show, Eq, Ord)++instance AtomF At where+    notA At {at_l = lhs, at_r = rhs} =+        let wholeSet  = enumFrom (toEnum 0) :: [Value]+            contrasts = delete rhs wholeSet+        in [At {at_l = lhs, at_r = rhs'} | rhs' <- contrasts]++infix 6 <==>+s <==> v = Atom $ At s v+equations = do+    assert $ "a" <==> A :||: "a" <==> B+    assert $ "b" <==> C :||: "b" <==> D+    assert $ Not ("a" <==> A)+    assert $ Not ("a" <==> B :=>: "b" <==> C)+++infixl 6 <=>+a <=> b = Atom $ Unif {lhs=a, rhs=b, neq=False}+solu = do+    a <- newTVar+    b <- newTVar+    c <- newTVar+    d <- newTVar+    let [eqs] = unionEquations $+                do+                assert $ TVar a <=> TForall (S.fromList ["s"]) ((TFresh "s") :-> (TFresh "s" :* TFresh "s"))+                assert $ TVar a <=> (TVar b :-> (TVar c :* TVar d))+                assert $ TVar d <=> TNom 1+    forM_ eqs solve+    a <- prune $ TVar a+    b <- prune $ TVar b+    c <- prune $ TVar c+    return (a, b, c)++test :: Eq a => String -> a -> a -> IO ()+test msg a b+    | a == b = return ()+    | otherwise = print msg++main = do+    forM (unionEquations equations) $ \xs ->+        case xs of+            [a, b] -> print xs+            _      -> return ()++    let (a, b, c):_ = map fst $ runMS solu emptyTCEnv+    test "1 failed" (show a) "@t1 -> @t1 * @t1"+    test "2 failed" (show b) "@t1"+    test "3 failed" (show c) "@t1"