Logic.hs

-------------------------------------------------------------------------
-- |
-- Module      : Control.Monad.Logic
-- Copyright   : (c) 2007-2014 Dan Doel,
--               (c) 2011-2013 Edward Kmett,
--               (c) 2014      Roman Cheplyaka,
--               (c) 2020-2021 Andrew Lelechenko,
--               (c) 2020-2021 Kevin Quick
-- License     : BSD3
-- Maintainer  : Andrew Lelechenko <andrew.lelechenko@gmail.com>
--
-- Adapted from the paper
-- <http://okmij.org/ftp/papers/LogicT.pdf Backtracking, Interleaving, and Terminating Monad Transformers>
-- by Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry.
-- Note that the paper uses 'MonadPlus' vocabulary
-- ('Control.Monad.mzero' and 'Control.Monad.mplus'),
-- while examples below prefer 'empty' and '<|>'
-- from 'Alternative'.
-------------------------------------------------------------------------

{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE Trustworthy           #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Avoid restricted function" #-}

module Control.Monad.Logic (
    module Control.Monad.Logic.Class,
    -- * The Logic monad
    Logic,
    logic,
    runLogic,
    observe,
    observeMany,
    observeAll,
    -- * The LogicT monad transformer
    LogicT(..),
    runLogicT,
    observeT,
    observeManyT,
    observeAllT,
    fromLogicT,
    fromLogicTWith,
    hoistLogicT,
    embedLogicT
  ) where

import Prelude (error, (-))

import Control.Applicative (Alternative(..), Applicative, liftA2, pure, (<*>), (*>))
import Control.Exception (Exception, evaluate, throw)
import Control.Monad (join, MonadPlus(..), Monad(..), fail)
import Control.Monad.Catch (MonadThrow, MonadCatch, throwM, catch)
import Control.Monad.Error.Class (MonadError(..))
import qualified Control.Monad.Fail as Fail
import Control.Monad.Identity (Identity(..))
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Reader.Class (MonadReader(..))
import Control.Monad.State.Class (MonadState(..))
import Control.Monad.Trans (MonadTrans(..))
import Control.Monad.Zip (MonadZip (..))

import Data.Bool (Bool (..), otherwise)
import Data.Eq (Eq, (==))
import qualified Data.Foldable as F
import Data.Function (($), (.), const, on)
import Data.Functor (Functor(..), (<$>))
import Data.Int
import qualified Data.List as L
import Data.Maybe (Maybe(..), maybe)
import Data.Monoid (Monoid (..))
import Data.Ord (Ord, (<=), (>), compare)
import Data.Semigroup (Semigroup (..))
import qualified Data.Traversable as T
import System.IO.Unsafe (unsafePerformIO)
import Text.Show (Show, showsPrec, showParen, showString, shows)
import Text.Read (Read, readPrec, Lexeme (Ident), parens, lexP, prec, readListPrec, readListPrecDefault)

#if MIN_VERSION_base(4,17,0)
import GHC.IsList (IsList(..))
#else
import GHC.Exts (IsList(..))
#endif

#if MIN_VERSION_base(4,18,0)
import qualified Data.Foldable1 as F1
#endif

import Control.Monad.Logic.Class

-------------------------------------------------------------------------
-- | A monad transformer for performing backtracking computations
-- layered over another monad @m@.
--
-- When @m@ is 'Identity', 'LogicT' @m@ becomes isomorphic to a list
-- (see 'Logic'). Thus 'LogicT' @m@ for non-trivial @m@ can be imagined
-- as a list, pattern matching on which causes monadic effects.
--
-- It's important to remember that 'LogicT' on its own is just
-- a lawful list monad transformer, adding a nondeterministic effect,
-- and its 'Monad' instance behaves just as @instance@ 'Monad' @[]@:
--
-- >>> :set -XOverloadedLists
-- >>> observeMany 9 $ do {x <- [100,200] :: Logic Int; fmap (+x) [1..]}
-- [101,102,103,104,105,106,107,108,109]
-- >>> observeMany 9 $ do {[100,200] >>= \x -> fmap (+x) [1..] :: Logic Int}
-- [101,102,103,104,105,106,107,108,109]
--
-- One should explicitly use methods of 'MonadLogic' such as '(>>-)' and 'interleave'
-- to get fair conjunction / disjunction:
--
-- >>> observeMany 9 $ do {[100,200] >>- \x -> fmap (+x) [1..] :: Logic Int}
-- [101,201,102,202,103,203,104,204,105]
--
-- @since 0.2
newtype LogicT m a =
    LogicT { unLogicT :: forall r. (a -> m r -> m r) -> m r -> m r }

-------------------------------------------------------------------------
-- | Extracts the first result from a 'LogicT' computation,
-- failing if there are no results at all.
--
-- @since 0.2
#if !MIN_VERSION_base(4,13,0)
observeT :: Monad m => LogicT m a -> m a
#else
observeT :: Fail.MonadFail m => LogicT m a -> m a
#endif
observeT lt = unLogicT lt (const . return) (fail "No answer.")

-------------------------------------------------------------------------
-- | Extracts all results from a 'LogicT' computation, unless blocked by the
-- underlying monad.
--
-- For example, given
--
-- >>> let nats = pure 0 <|> fmap (+ 1) nats
--
-- some monads (like 'Identity', 'Control.Monad.Reader.Reader',
-- 'Control.Monad.Writer.Writer', and 'Control.Monad.State.State')
-- will be productive:
--
-- >>> take 5 $ runIdentity (observeAllT nats)
-- [0,1,2,3,4]
--
-- but others (like 'Control.Monad.Except.ExceptT',
-- and 'Control.Monad.Cont.ContT') will not:
--
-- >>> take 20 <$> runExcept (observeAllT nats)
--
-- In general, if the underlying monad manages control flow then
-- 'observeAllT' may be unproductive under infinite branching,
-- and 'observeManyT' should be used instead.
--
-- @since 0.2
observeAllT :: Applicative m => LogicT m a -> m [a]
observeAllT m = unLogicT m (fmap . (:)) (pure [])

-------------------------------------------------------------------------
-- | Extracts up to a given number of results from a 'LogicT' computation.
--
-- @since 0.2
observeManyT :: Monad m => Int -> LogicT m a -> m [a]
observeManyT n m
    | n <= 0 = return []
    | n == 1 = unLogicT m (\a _ -> return [a]) (return [])
    | otherwise = unLogicT (msplit m) sk (return [])
  where
    sk Nothing _ = return []
    sk (Just (a, m')) _ = (a:) <$> observeManyT (n-1) m'

-------------------------------------------------------------------------
-- | Runs a 'LogicT' computation with the specified initial success and
-- failure continuations.
--
-- The second argument ("success continuation") takes one result of
-- the 'LogicT' computation and the monad to run for any subsequent
-- matches.
--
-- The third argument ("failure continuation") is called when the
-- 'LogicT' cannot produce any more results.
--
-- For example:
--
-- >>> yieldWords = foldr ((<|>) . pure) empty
-- >>> showEach wrd nxt = putStrLn wrd >> nxt
-- >>> runLogicT (yieldWords ["foo", "bar"]) showEach (putStrLn "none!")
-- foo
-- bar
-- none!
-- >>> runLogicT (yieldWords []) showEach (putStrLn "none!")
-- none!
-- >>> showFirst wrd _ = putStrLn wrd
-- >>> runLogicT (yieldWords ["foo", "bar"]) showFirst (putStrLn "none!")
-- foo
--
-- @since 0.2
runLogicT :: LogicT m a -> (a -> m r -> m r) -> m r -> m r
runLogicT (LogicT r) = r

-- | Convert from 'LogicT' to an arbitrary logic-like monad transformer,
-- such as <https://hackage.haskell.org/package/list-t list-t>
-- or <https://hackage.haskell.org/package/logict-sequence logict-sequence>
--
-- For example, to show a representation of the structure of a `LogicT`
-- computation, @l@, over a data-like `Monad` (such as @[]@,
-- @Data.Sequence.Seq@, etc.), you could write
--
-- @
-- import ListT (ListT)
--
-- 'Text.Show.show' $ fromLogicT @ListT l
-- @
--
-- @since 0.8.0.0
fromLogicT :: (Alternative (t m), MonadTrans t, Monad m, Monad (t m))
  => LogicT m a -> t m a
fromLogicT = fromLogicTWith lift

-- | Convert from @'LogicT' m@ to an arbitrary logic-like monad,
-- such as @[]@.
--
-- Examples:
--
-- @
-- 'fromLogicT' = fromLogicTWith d
-- 'hoistLogicT' f = fromLogicTWith ('lift' . f)
-- 'embedLogicT' f = 'fromLogicTWith' f
-- @
--
-- The first argument should be a
-- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html monad morphism>.
-- to produce sensible results.
--
-- @since 0.8.0.0
fromLogicTWith :: (Applicative m, Monad n, Alternative n)
  => (forall x. m x -> n x) -> LogicT m a -> n a
fromLogicTWith p (LogicT f) = join . p $
  f (\a v -> pure (pure a <|> join (p v))) (pure empty)

-- | Convert a 'LogicT' computation from one underlying monad to another.
-- For example,
--
-- @
-- hoistLogicT lift :: LogicT m a -> LogicT (StateT m) a
-- @
--
-- The first argument should be a
-- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html monad morphism>.
-- to produce sensible results.
--
-- @since 0.8.0.0
hoistLogicT :: (Applicative m, Monad n) => (forall x. m x -> n x) -> LogicT m a -> LogicT n a
hoistLogicT f = fromLogicTWith (lift . f)

-- | Convert a 'LogicT' computation from one underlying monad to another.
--
-- The first argument should be a
-- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html monad morphism>.
-- to produce sensible results.
--
-- @since 0.8.0.0
embedLogicT :: Applicative m => (forall a. m a -> LogicT n a) -> LogicT m b -> LogicT n b
embedLogicT f = fromLogicTWith f

-------------------------------------------------------------------------
-- | The basic 'Logic' monad, for performing backtracking computations
-- returning values (e.g. 'Logic' @a@ will return values of type @a@).
--
-- It's important to remember that 'Logic' on its own is just
-- a lawful list monad, behaving exactly as @instance@ 'Monad' @[]@.
-- One should explicitly use methods of 'MonadLogic' such as '(>>-)' and 'interleave'
-- to get fair conjunction / disjunction. Note that usual
-- lists have an instance of 'MonadLogic', so maybe you don't need 'Logic' at all.
--
-- __Technical perspective.__
-- 'Logic' is a
-- <http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html Boehm-Berarducci encoding>
-- of lists. Speaking plainly, its type is identical (up to 'Identity' wrappers)
-- to 'Data.List.foldr' applied to a given list. And this list itself can be reconstructed
-- by supplying @(:)@ and @[]@.
--
-- > import Data.Functor.Identity
-- >
-- > fromList :: [a] -> Logic a
-- > fromList xs = LogicT $ \cons nil -> foldr cons nil xs
-- >
-- > toList :: Logic a -> [a]
-- > toList (LogicT fld) = runIdentity $ fld (\x (Identity xs) -> Identity (x : xs)) (Identity [])
--
-- Here is a systematic derivation of the isomorphism. We start with observing
-- that @[a]@ is isomorphic to a fix point of a non-recursive
-- base algebra @Fix@ (@ListF@ @a@):
--
-- > newtype Fix f = Fix (f (Fix f))
-- > data ListF a r = ConsF a r | NilF deriving (Functor)
-- >
-- > cata :: Functor f => (f r -> r) -> Fix f -> r
-- > cata f = go where go (Fix x) = f (fmap go x)
-- >
-- > from :: [a] -> Fix (ListF a)
-- > from = foldr (\a acc -> Fix (ConsF a acc)) (Fix NilF)
-- >
-- > to :: Fix (ListF a) -> [a]
-- > to = cata (\case ConsF a r -> a : r; NilF -> [])
--
-- Further, @Fix@ (@ListF@ @a@) is isomorphic to Boehm-Berarducci encoding @ListC@ @a@:
--
-- > newtype ListC a = ListC (forall r. (ListF a r -> r) -> r)
-- >
-- > from :: Fix (ListF a) -> ListC a
-- > from xs = ListC (\f -> cata f xs)
-- >
-- > to :: ListC a -> Fix (ListF a)
-- > to (ListC f) = f Fix
--
-- Finally, @ListF@ @a@ @r@ → @r@ is isomorphic to a pair (@a@ → @r@ → @r@, @r@),
-- so @ListC@ is isomorphic to the 'Logic' type modulo 'Identity' wrappers:
--
-- > newtype Logic a = Logic (forall r. (a -> r -> r) -> r -> r)
--
-- And wrapping every occurence of @r@ into @m@ gives us 'LogicT':
--
-- > newtype LogicT m a = Logic (forall r. (a -> m r -> m r) -> m r -> m r)
--
-- @since 0.5.0
type Logic = LogicT Identity

-------------------------------------------------------------------------
-- | A smart constructor for 'Logic' computations.
--
-- @since 0.5.0
logic :: (forall r. (a -> r -> r) -> r -> r) -> Logic a
logic f = LogicT $ \k -> Identity .
                         f (\a -> runIdentity . k a . Identity) .
                         runIdentity

-------------------------------------------------------------------------
-- | Extracts the first result from a 'Logic' computation, failing if
-- there are no results.
--
-- >>> observe (pure 5 <|> pure 3 <|> empty)
-- 5
--
-- >>> observe empty
-- *** Exception: No answer.
--
-- Since 'Logic' is isomorphic to a list, 'observe' is analogous to 'Data.List.head'.
--
-- @since 0.2
observe :: Logic a -> a
observe lt = runIdentity $ unLogicT lt (const . pure) (error "No answer.")

-------------------------------------------------------------------------
-- | Extracts all results from a 'Logic' computation.
--
-- >>> observeAll (pure 5 <|> empty <|> empty <|> pure 3 <|> empty)
-- [5,3]
--
-- 'observeAll' reveals a half of the isomorphism between 'Logic'
-- and lists. See description of 'runLogic' for the other half.
--
-- @since 0.2
observeAll :: Logic a -> [a]
observeAll = runIdentity . observeAllT

-------------------------------------------------------------------------
-- | Extracts up to a given number of results from a 'Logic' computation.
--
-- >>> let nats = pure 0 <|> fmap (+ 1) nats
-- >>> observeMany 5 nats
-- [0,1,2,3,4]
--
-- Since 'Logic' is isomorphic to a list, 'observeMany' is analogous to 'Data.List.take'.
--
-- @since 0.2
observeMany :: Int -> Logic a -> [a]
observeMany i = L.take i . observeAll
-- Implementing 'observeMany' using 'observeManyT' is quite costly,
-- because it calls 'msplit' multiple times.

-------------------------------------------------------------------------
-- | Runs a 'Logic' computation with the specified initial success and
-- failure continuations.
--
-- >>> runLogic empty (+) 0
-- 0
--
-- >>> runLogic (pure 5 <|> pure 3 <|> empty) (+) 0
-- 8
--
-- When invoked with @(:)@ and @[]@ as arguments, reveals
-- a half of the isomorphism between 'Logic' and lists.
-- See description of 'observeAll' for the other half.
--
-- @since 0.2
runLogic :: Logic a -> (a -> r -> r) -> r -> r
runLogic l s f = runIdentity $ unLogicT l si fi
 where
 si = fmap . s
 fi = Identity f

instance Functor (LogicT f) where
    fmap f lt = LogicT $ \sk fk -> unLogicT lt (sk . f) fk

instance Applicative (LogicT f) where
    pure a = LogicT $ \sk fk -> sk a fk
    f <*> a = LogicT $ \sk fk -> unLogicT f (\g fk' -> unLogicT a (sk . g) fk') fk
    m *> k = LogicT $ \sk fk -> unLogicT m (const $ unLogicT k sk) fk

instance Alternative (LogicT f) where
    empty = LogicT $ \_ fk -> fk
    f1 <|> f2 = LogicT $ \sk fk -> unLogicT f1 sk (unLogicT f2 sk fk)

instance Monad (LogicT m) where
    return = pure
    m >>= f = LogicT $ \sk fk -> unLogicT m (\a fk' -> unLogicT (f a) sk fk') fk
    (>>) = (*>)
#if !MIN_VERSION_base(4,13,0)
    fail = Fail.fail
#endif

-- | @since 0.6.0.3
instance Fail.MonadFail (LogicT m) where
    fail _ = LogicT $ \_ fk -> fk

instance MonadPlus (LogicT m) where
  mzero = empty
  mplus = (<|>)

-- | @since 0.7.0.3
instance Semigroup (LogicT m a) where
  (<>) = mplus
#if MIN_VERSION_base(4,18,0)
  sconcat = F1.foldr1 mplus
#else
  sconcat = F.foldr1 mplus
#endif

-- | @since 0.7.0.3
instance Monoid (LogicT m a) where
  mempty = empty
  mappend = (<>)
  mconcat = F.asum

instance MonadTrans LogicT where
    lift m = LogicT $ \sk fk -> m >>= \a -> sk a fk

instance (MonadIO m) => MonadIO (LogicT m) where
    liftIO = lift . liftIO

instance {-# OVERLAPPABLE #-} (Monad m) => MonadLogic (LogicT m) where
    -- 'msplit' is quite costly even if the base 'Monad' is 'Identity'.
    -- Try to avoid it.
    msplit m = lift $ unLogicT m ssk (return Nothing)
     where
     ssk a fk = return $ Just (a, lift fk >>= reflect)
    once m = LogicT $ \sk fk -> unLogicT m (\a _ -> sk a fk) fk
    lnot m = LogicT $ \sk fk -> unLogicT m (\_ _ -> fk) (sk () fk)

-- | @since 0.8.2.0
instance {-# INCOHERENT #-} MonadLogic Logic where
    -- Same as in the generic instance above
    msplit m = lift $ unLogicT m ssk (return Nothing)
     where
     ssk a fk = return $ Just (a, lift fk >>= reflect)
    once m = LogicT $ \sk fk -> unLogicT m (\a _ -> sk a fk) fk
    lnot m = LogicT $ \sk fk -> unLogicT m (\_ _ -> fk) (sk () fk)

    m >>- f
      | isConstantFailure f = empty
      -- Otherwise apply the default definition from Control.Monad.Logic.Class
      | otherwise = msplit m >>= maybe empty (\(a, m') -> interleave (f a) (m' >>- f))

data MyException = MyException
  deriving (Show)

instance Exception MyException

isConstantFailure :: (a -> Logic b) -> Bool
isConstantFailure f = unsafePerformIO $ do
  let eval foo = runIdentity (unLogicT foo (const $ const $ Identity False) (Identity True))
  evaluate (eval (f (throw MyException))) `catch` (\MyException -> pure False)

-- | @since 0.5.0
instance {-# OVERLAPPABLE #-} (Applicative m, F.Foldable m) => F.Foldable (LogicT m) where
    foldMap f m = F.fold $ unLogicT m (fmap . mappend . f) (pure mempty)

-- | @since 0.5.0
instance {-# INCOHERENT #-} F.Foldable Logic where
    foldr f z m = runLogic m f z

-- A much simpler logic monad representation used to define the Traversable and
-- MonadZip instances. This is essentially the same as ListT from the list-t
-- package, but it uses a slightly more efficient representation: MLView m a is
-- more compact than Maybe (a, ML m a), and the additional laziness in the
-- latter appears to be incidental/historical.
newtype ML m a = ML (m (MLView m a))
  deriving (Functor, F.Foldable, T.Traversable)

data MLView m a = EmptyML | ConsML a (ML m a)
  deriving (Functor, F.Foldable)

instance T.Traversable m => T.Traversable (MLView m) where
  traverse _ EmptyML = pure EmptyML
  traverse f (ConsML x (ML m))
    = liftA2 (\y ym -> ConsML y (ML ym)) (f x) (T.traverse (T.traverse f) m)
  {- The derived instance would write the second case as
   -
   -   traverse f (ConsML x xs) = liftA2 ConsML (f x) (traverse @(ML m) f xs)
   -
   - Inlining the inner traverse gives
   -
   -   traverse f (ConsML x (ML m)) = liftA2 ConsML (f x) (ML <$> traverse (traverse f) m)
   -
   - revealing fmap under liftA2. We fuse those into a single application of liftA2,
   - in case fmap isn't free.
  -}

toML :: Applicative m => LogicT m a -> ML m a
toML (LogicT q) = ML $ q (\a m -> pure $ ConsML a (ML m)) (pure EmptyML)

fromML :: Monad m => ML m a -> LogicT m a
fromML (ML m) = lift m >>= \case
  EmptyML -> empty
  ConsML a xs -> pure a <|> fromML xs

-- | @since 0.5.0
instance {-# OVERLAPPING #-} T.Traversable (LogicT Identity) where
  traverse g l = runLogic l (\a ft -> cons <$> g a <*> ft) (pure empty)
    where
      cons a l' = pure a <|> l'

-- | @since 0.8.0.0
instance {-# OVERLAPPABLE #-} (Monad m, T.Traversable m) => T.Traversable (LogicT m) where
  traverse f = fmap fromML . T.traverse f . toML

zipWithML :: MonadZip m => (a -> b -> c) -> ML m a -> ML m b -> ML m c
zipWithML f = go
    where
      go (ML m1) (ML m2) =
        ML $ mzipWith zv m1 m2
      zv (a `ConsML` as) (b `ConsML` bs) = f a b `ConsML` go as bs
      zv _ _ = EmptyML

unzipML :: MonadZip m => ML m (a, b) -> (ML m a, ML m b)
unzipML (ML m)
    | (l, r) <- munzip (fmap go m)
    = (ML l, ML r)
    where
      go EmptyML = (EmptyML, EmptyML)
      go ((a, b) `ConsML` listab)
        = (a `ConsML` la, b `ConsML` lb)
        where
          -- If the underlying munzip is careful not to leak memory, then we
          -- don't want to defeat it. We need to be sure that la and lb are
          -- realized as selector thunks. Hopefully the CPSish conversion
          -- doesn't muck anything up at another level.
          {-# NOINLINE remains #-}
          {-# NOINLINE la #-}
          {-# NOINLINE lb #-}
          remains = unzipML listab
          (la, lb) = remains

-- | @since 0.8.0.0
instance MonadZip m => MonadZip (LogicT m) where
  mzipWith f xs ys = fromML $ zipWithML f (toML xs) (toML ys)
  munzip xys = case unzipML (toML xys) of
    (xs, ys) -> (fromML xs, fromML ys)

instance MonadReader r m => MonadReader r (LogicT m) where
    ask = lift ask
    local f (LogicT m) = LogicT $ \sk fk -> do
        env <- ask
        local f $ m ((local (const env) .) . sk) (local (const env) fk)

instance MonadState s m => MonadState s (LogicT m) where
    get = lift get
    put = lift . put

-- | @since 0.4
instance MonadError e m => MonadError e (LogicT m) where
  throwError = lift . throwError
  catchError m h = LogicT $ \sk fk -> let
      handle r = r `catchError` \e -> unLogicT (h e) sk fk
    in handle $ unLogicT m (\a -> sk a . handle) fk

-- | @since 0.8.2.0
instance MonadThrow m => MonadThrow (LogicT m) where
  throwM = lift . throwM

-- | @since 0.8.2.0
instance MonadCatch m => MonadCatch (LogicT m) where
  catch m h = LogicT $ \sk fk -> let
      handle r = r `catch` \e -> unLogicT (h e) sk fk
    in handle $ unLogicT m (\a -> sk a . handle) fk

-- | @since 0.8.2.0
instance IsList (Logic a) where
  type Item (Logic a) = a
  fromList xs = LogicT $ \cons nil -> L.foldr cons nil xs
  toList = observeAll

-- | @since 0.8.2.0
instance Eq a => Eq (Logic a) where
  (==) = (==) `on` observeAll

-- | @since 0.8.2.0
instance Ord a => Ord (Logic a) where
  compare = compare `on` observeAll

-- | @since 0.8.2.0
instance Show a => Show (Logic a) where
  showsPrec p xs = showParen (p > 10) $
    showString "fromList " . shows (toList xs)

-- | @since 0.8.2.0
instance Read a => Read (Logic a) where
  readPrec = parens $ prec 10 $ do
    Ident "fromList" <- lexP
    xs <- readPrec
    return (fromList xs)

  readListPrec = readListPrecDefault