# RSolve

[![](https://img.shields.io/hackage/v/RSolve.svg)](https://hackage.haskell.org/package/RSolve)

NOTE: NO LONGER for general logic programming, this package is now dedicated for the simple propositional logic.

The README is going to get updated.

## Propositional Logic

RSolve uses [disjunctive normal form](https://en.wikipedia.org/wiki/Disjunctive_normal_form) to solve logic problems.

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).


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
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 $ Not ("a" <==> A)

main =
  let equationGroups = unionEquations equations
  in forM equationGroups print
```
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}]
```

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.

When do we need a solver? For instance, type checking&inference.

In this case, we need type checking environments to represent the checking states:

```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
```

For sure we also need to represent the type:

```haskell
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)
```

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)
```

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"
```