-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A general solver for equations
@package RSolve
@version 2.0.0.0

module RSolve.Logic
class (Show a, Ord a) => AtomF a

-- | Specifies how to handle the negations. For the finite and enumerable
--   solutions, we can return its supplmentary set.
notA :: AtomF a => a -> [a]

module RSolve.MapLike
class MapLike m k v | m -> k, m -> v
lookup :: MapLike m k v => k -> m -> Maybe v
(!) :: MapLike m k v => m -> k -> v
insert :: MapLike m k v => k -> v -> m -> m
adjust :: MapLike m k v => (v -> v) -> k -> m -> m
member :: MapLike m k v => k -> m -> Bool
update :: MapLike m k v => (v -> Maybe v) -> k -> m -> m
instance GHC.Classes.Ord k => RSolve.MapLike.MapLike (Data.Map.Internal.Map k v) k v
instance GHC.Classes.Eq k => RSolve.MapLike.MapLike [(k, v)] k v


-- | state monads extended to have branches Author: Taine Zhao(thautwarm)
--   Date: 2018-12 License: MIT
module RSolve.MultiState
newtype MS s a
MS :: (s -> [(a, s)]) -> MS s a
[runMS] :: MS s a -> s -> [(a, s)]
getMS :: MS s s
putMS :: s -> MS s ()
getsMS :: (s -> a) -> MS s a
modifyMS :: (s -> s) -> MS s ()
instance GHC.Base.Functor (RSolve.MultiState.MS s)
instance GHC.Base.Applicative (RSolve.MultiState.MS s)
instance Control.Monad.Fail.MonadFail (RSolve.MultiState.MS s)
instance GHC.Base.Monad (RSolve.MultiState.MS s)
instance GHC.Base.Alternative (RSolve.MultiState.MS s)


-- | Propositional logic infrastructures Author: Taine Zhao(thautwarm)
--   Date: 2019-08-03 License: MIT
module RSolve.PropLogic
class (Show a, Ord a) => AtomF a

-- | Specifies how to handle the negations. For the finite and enumerable
--   solutions, we can return its supplmentary set.
notA :: AtomF a => a -> [a]
data WFF a

-- | Atom formula, should be specified by the problem
Atom :: a -> WFF a
Not :: WFF a -> WFF a

-- | And
(:&&:) :: WFF a -> WFF a -> WFF a

-- | Or
(:||:) :: WFF a -> WFF a -> WFF a

-- | Implication
(:=>:) :: WFF a -> WFF a -> WFF a
infixl 5 :&&:
infixl 3 :||:
infixl 3 :=>:

-- | normalized WWF, where '[NF a]' the disjunctive normal form.
data NF a
AtomN :: a -> NF a
(:&&) :: NF a -> NF a -> NF a
(:||) :: NF a -> NF a -> NF a
infixl 5 :&&
infixl 3 :||
assertNF :: AtomF a => NF a -> MS (Set a) ()
normal :: AtomF a => WFF a -> NF a

-- | Use a propositinal logic formula to build logic equations
--   incrementally.
assert :: AtomF a => WFF a -> MS (Set a) ()

-- | Produced a list of disjunctions of conjunctive clauses.
unionEquations :: AtomF a => MS (Set a) () -> [[a]]
instance GHC.Classes.Ord a => GHC.Classes.Ord (RSolve.PropLogic.NF a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (RSolve.PropLogic.NF a)
instance GHC.Base.Functor RSolve.PropLogic.NF
instance GHC.Classes.Ord a => GHC.Classes.Ord (RSolve.PropLogic.WFF a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (RSolve.PropLogic.WFF a)
instance GHC.Base.Functor RSolve.PropLogic.WFF

module RSolve.Solver
class AtomF a => CtxSolver s a

-- | Give a atom formula and solve it
solve :: CtxSolver s a => a -> MS s ()


-- | HM unification implementations based on propositional logics, based on
--   nominal type system. Author: Taine Zhao(thautwarm) Date: 2019-08-04
--   License: MIT
module RSolve.HM
type Fix a = a -> a
data T
TVar :: Int -> T
TFresh :: String -> T
(:->) :: T -> T -> T
(:*) :: T -> T -> T
TForall :: Set String -> T -> T
TApp :: T -> T -> T
TNom :: Int -> T
infixl 6 :*
infixl 6 :->
deConsTOp :: T -> Maybe (T -> T -> T, T, T)
data Unif
Unif :: T -> T -> Bool -> Unif
[lhs] :: Unif -> T
[rhs] :: Unif -> T
[neq] :: Unif -> Bool
data TCEnv
TCEnv :: Map Int T -> Map Int T -> Set (T, T) -> TCEnv
[_noms] :: TCEnv -> Map Int T
[_tvars] :: TCEnv -> Map Int T
[_neqs] :: TCEnv -> Set (T, T)
emptyTCEnv :: TCEnv
tvars :: Lens' TCEnv (Map Int T)
noms :: Lens' TCEnv (Map Int T)
neqs :: Lens' TCEnv (Set (T, T))
newTVar :: MS TCEnv Int
newTNom :: MS TCEnv Int
loadTVar :: Int -> MS TCEnv T
occurIn :: Int -> T -> MS TCEnv Bool
free :: Map String T -> T -> T
prune :: T -> MS TCEnv T
update :: Int -> T -> MS TCEnv ()
addNEq :: (T, T) -> MS TCEnv ()
unify :: Fix (Unif -> MS TCEnv ())
instance RSolve.Solver.CtxSolver RSolve.HM.TCEnv RSolve.HM.Unif
instance GHC.Show.Show RSolve.HM.TCEnv
instance GHC.Classes.Ord RSolve.HM.Unif
instance GHC.Classes.Eq RSolve.HM.Unif
instance GHC.Classes.Ord RSolve.HM.T
instance GHC.Classes.Eq RSolve.HM.T
instance GHC.Show.Show RSolve.HM.Unif
instance RSolve.Logic.AtomF RSolve.HM.Unif
instance GHC.Show.Show RSolve.HM.T