    {-# LANGUAGE UndecidableInstances #-}
    {-|
    Module           : What4.Solver.Partial
    Description      : Representation of partial values
    Copyright        : (c) Galois, Inc 2014-2020
    License          : BSD3
    Maintainer       : Langston Barrett <langston@galois.com>

    Often, various operations on values are only partially defined (in the case of
    Crucible expressions, consider loading a value from a pointer - this is only
    defined in the case that the pointer is valid and non-null). The 'PartExpr'
    type allows for packaging values together with predicates that express their
    partiality: the value is only valid if the predicate is true.

    -}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE DeriveFoldable #-}
    {-# LANGUAGE DeriveFunctor #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE DeriveTraversable #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE PatternSynonyms #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeOperators #-}

    module What4.Partial
     ( -- ** Partial
       Partial(..)
     , partialPred
     , partialValue

       -- ** PartialWithErr
     , PartialWithErr(..)

       -- ** PartExpr
     , PartExpr
     , pattern PE
     , pattern Unassigned
     , mkPE
     , justPartExpr
     , maybePartExpr
     , joinMaybePE

       -- ** PartialT
     , PartialT(..)
     , runPartialT
     , returnUnassigned
     , returnMaybe
     , returnPartial
     , addCondition
     , mergePartial
     , mergePartials
     ) where

    #if !MIN_VERSION_base(4,13,0)
    import Control.Monad.Fail( MonadFail )
    import qualified Control.Monad.Fail
    #endif

    import GHC.Generics (Generic, Generic1)
    import Data.Data (Data)
    import Control.Monad.IO.Class
    import Control.Monad.Trans.Class

    import What4.BaseTypes
    import What4.Interface (IsExprBuilder, SymExpr, IsExpr, Pred)
    import What4.Interface (truePred, andPred, notPred, itePred, asConstantPred)

    import Control.Lens.TH (makeLenses)
    import Data.Bifunctor.TH (deriveBifunctor, deriveBifoldable, deriveBitraversable)
    import Data.Eq.Deriving (deriveEq1, deriveEq2)
    import Data.Ord.Deriving (deriveOrd1, deriveOrd2)
    import Text.Show.Deriving (deriveShow1, deriveShow2)

    ------------------------------------------------------------------------
    -- ** Partial

    -- | A partial value represents a value that may or may not be valid.
    --
    -- The '_partialPred' field represents a predicate (optionally with additional
    -- provenance information) embodying the value's partiality.
    data Partial p v =
      Partial { forall p v. Partial p v -> p
    _partialPred  :: !p
              , forall p v. Partial p v -> v
    _partialValue :: !v
              }
      deriving (Typeable (Partial p v)
    Typeable (Partial p v)
    -> (forall (c :: Type -> Type).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> Partial p v -> c (Partial p v))
    -> (forall (c :: Type -> Type).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c (Partial p v))
    -> (Partial p v -> Constr)
    -> (Partial p v -> DataType)
    -> (forall (t :: Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c (Partial p v)))
    -> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c (Partial p v)))
    -> ((forall b. Data b => b -> b) -> Partial p v -> Partial p v)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Partial p v -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Partial p v -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Partial p v -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> Partial p v -> u)
    -> (forall (m :: Type -> Type).
        Monad m =>
        (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v))
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v))
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v))
    -> Data (Partial p v)
    Partial p v -> Constr
    Partial p v -> DataType
    (forall b. Data b => b -> b) -> Partial p v -> Partial p v
    forall a.
    Typeable a
    -> (forall (c :: Type -> Type).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: Type -> Type).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: Type -> Type).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Partial p v -> u
    forall u. (forall d. Data d => d -> u) -> Partial p v -> [u]
    forall {p} {v}. (Data p, Data v) => Typeable (Partial p v)
    forall p v. (Data p, Data v) => Partial p v -> Constr
    forall p v. (Data p, Data v) => Partial p v -> DataType
    forall p v.
    (Data p, Data v) =>
    (forall b. Data b => b -> b) -> Partial p v -> Partial p v
    forall p v u.
    (Data p, Data v) =>
    Int -> (forall d. Data d => d -> u) -> Partial p v -> u
    forall p v u.
    (Data p, Data v) =>
    (forall d. Data d => d -> u) -> Partial p v -> [u]
    forall p v r r'.
    (Data p, Data v) =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Partial p v -> r
    forall p v r r'.
    (Data p, Data v) =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Partial p v -> r
    forall p v (m :: Type -> Type).
    (Data p, Data v, Monad m) =>
    (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v)
    forall p v (m :: Type -> Type).
    (Data p, Data v, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v)
    forall p v (c :: Type -> Type).
    (Data p, Data v) =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Partial p v)
    forall p v (c :: Type -> Type).
    (Data p, Data v) =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Partial p v -> c (Partial p v)
    forall p v (t :: Type -> Type) (c :: Type -> Type).
    (Data p, Data v, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (Partial p v))
    forall p v (t :: Type -> Type -> Type) (c :: Type -> Type).
    (Data p, Data v, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Partial p v))
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Partial p v -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Partial p v -> r
    forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v)
    forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v)
    forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Partial p v)
    forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Partial p v -> c (Partial p v)
    forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Partial p v))
    forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Partial p v))
    $cgfoldl :: forall p v (c :: Type -> Type).
    (Data p, Data v) =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Partial p v -> c (Partial p v)
    gfoldl :: forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Partial p v -> c (Partial p v)
    $cgunfold :: forall p v (c :: Type -> Type).
    (Data p, Data v) =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Partial p v)
    gunfold :: forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Partial p v)
    $ctoConstr :: forall p v. (Data p, Data v) => Partial p v -> Constr
    toConstr :: Partial p v -> Constr
    $cdataTypeOf :: forall p v. (Data p, Data v) => Partial p v -> DataType
    dataTypeOf :: Partial p v -> DataType
    $cdataCast1 :: forall p v (t :: Type -> Type) (c :: Type -> Type).
    (Data p, Data v, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (Partial p v))
    dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Partial p v))
    $cdataCast2 :: forall p v (t :: Type -> Type -> Type) (c :: Type -> Type).
    (Data p, Data v, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Partial p v))
    dataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Partial p v))
    $cgmapT :: forall p v.
    (Data p, Data v) =>
    (forall b. Data b => b -> b) -> Partial p v -> Partial p v
    gmapT :: (forall b. Data b => b -> b) -> Partial p v -> Partial p v
    $cgmapQl :: forall p v r r'.
    (Data p, Data v) =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Partial p v -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Partial p v -> r
    $cgmapQr :: forall p v r r'.
    (Data p, Data v) =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Partial p v -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Partial p v -> r
    $cgmapQ :: forall p v u.
    (Data p, Data v) =>
    (forall d. Data d => d -> u) -> Partial p v -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Partial p v -> [u]
    $cgmapQi :: forall p v u.
    (Data p, Data v) =>
    Int -> (forall d. Data d => d -> u) -> Partial p v -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Partial p v -> u
    $cgmapM :: forall p v (m :: Type -> Type).
    (Data p, Data v, Monad m) =>
    (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v)
    gmapM :: forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v)
    $cgmapMp :: forall p v (m :: Type -> Type).
    (Data p, Data v, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v)
    gmapMp :: forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v)
    $cgmapMo :: forall p v (m :: Type -> Type).
    (Data p, Data v, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v)
    gmapMo :: forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v)
    Data, Partial p v -> Partial p v -> Bool
    (Partial p v -> Partial p v -> Bool)
    -> (Partial p v -> Partial p v -> Bool) -> Eq (Partial p v)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall p v. (Eq p, Eq v) => Partial p v -> Partial p v -> Bool
    $c== :: forall p v. (Eq p, Eq v) => Partial p v -> Partial p v -> Bool
    == :: Partial p v -> Partial p v -> Bool
    $c/= :: forall p v. (Eq p, Eq v) => Partial p v -> Partial p v -> Bool
    /= :: Partial p v -> Partial p v -> Bool
    Eq, (forall a b. (a -> b) -> Partial p a -> Partial p b)
    -> (forall a b. a -> Partial p b -> Partial p a)
    -> Functor (Partial p)
    forall a b. a -> Partial p b -> Partial p a
    forall a b. (a -> b) -> Partial p a -> Partial p b
    forall p a b. a -> Partial p b -> Partial p a
    forall p a b. (a -> b) -> Partial p a -> Partial p b
    forall (f :: Type -> Type).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall p a b. (a -> b) -> Partial p a -> Partial p b
    fmap :: forall a b. (a -> b) -> Partial p a -> Partial p b
    $c<$ :: forall p a b. a -> Partial p b -> Partial p a
    <$ :: forall a b. a -> Partial p b -> Partial p a
    Functor, (forall x. Partial p v -> Rep (Partial p v) x)
    -> (forall x. Rep (Partial p v) x -> Partial p v)
    -> Generic (Partial p v)
    forall x. Rep (Partial p v) x -> Partial p v
    forall x. Partial p v -> Rep (Partial p v) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall p v x. Rep (Partial p v) x -> Partial p v
    forall p v x. Partial p v -> Rep (Partial p v) x
    $cfrom :: forall p v x. Partial p v -> Rep (Partial p v) x
    from :: forall x. Partial p v -> Rep (Partial p v) x
    $cto :: forall p v x. Rep (Partial p v) x -> Partial p v
    to :: forall x. Rep (Partial p v) x -> Partial p v
    Generic, (forall a. Partial p a -> Rep1 (Partial p) a)
    -> (forall a. Rep1 (Partial p) a -> Partial p a)
    -> Generic1 (Partial p)
    forall a. Rep1 (Partial p) a -> Partial p a
    forall a. Partial p a -> Rep1 (Partial p) a
    forall p a. Rep1 (Partial p) a -> Partial p a
    forall p a. Partial p a -> Rep1 (Partial p) a
    forall k (f :: k -> Type).
    (forall (a :: k). f a -> Rep1 f a)
    -> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
    $cfrom1 :: forall p a. Partial p a -> Rep1 (Partial p) a
    from1 :: forall a. Partial p a -> Rep1 (Partial p) a
    $cto1 :: forall p a. Rep1 (Partial p) a -> Partial p a
    to1 :: forall a. Rep1 (Partial p) a -> Partial p a
    Generic1, (forall m. Monoid m => Partial p m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Partial p a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Partial p a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Partial p a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Partial p a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Partial p a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Partial p a -> b)
    -> (forall a. (a -> a -> a) -> Partial p a -> a)
    -> (forall a. (a -> a -> a) -> Partial p a -> a)
    -> (forall a. Partial p a -> [a])
    -> (forall a. Partial p a -> Bool)
    -> (forall a. Partial p a -> Int)
    -> (forall a. Eq a => a -> Partial p a -> Bool)
    -> (forall a. Ord a => Partial p a -> a)
    -> (forall a. Ord a => Partial p a -> a)
    -> (forall a. Num a => Partial p a -> a)
    -> (forall a. Num a => Partial p a -> a)
    -> Foldable (Partial p)
    forall a. Eq a => a -> Partial p a -> Bool
    forall a. Num a => Partial p a -> a
    forall a. Ord a => Partial p a -> a
    forall m. Monoid m => Partial p m -> m
    forall a. Partial p a -> Bool
    forall a. Partial p a -> Int
    forall a. Partial p a -> [a]
    forall a. (a -> a -> a) -> Partial p a -> a
    forall p a. Eq a => a -> Partial p a -> Bool
    forall p a. Num a => Partial p a -> a
    forall p a. Ord a => Partial p a -> a
    forall m a. Monoid m => (a -> m) -> Partial p a -> m
    forall p m. Monoid m => Partial p m -> m
    forall p a. Partial p a -> Bool
    forall p a. Partial p a -> Int
    forall p a. Partial p a -> [a]
    forall b a. (b -> a -> b) -> b -> Partial p a -> b
    forall a b. (a -> b -> b) -> b -> Partial p a -> b
    forall p a. (a -> a -> a) -> Partial p a -> a
    forall p m a. Monoid m => (a -> m) -> Partial p a -> m
    forall p b a. (b -> a -> b) -> b -> Partial p a -> b
    forall p a b. (a -> b -> b) -> b -> Partial p a -> b
    forall (t :: Type -> Type).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall p m. Monoid m => Partial p m -> m
    fold :: forall m. Monoid m => Partial p m -> m
    $cfoldMap :: forall p m a. Monoid m => (a -> m) -> Partial p a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Partial p a -> m
    $cfoldMap' :: forall p m a. Monoid m => (a -> m) -> Partial p a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Partial p a -> m
    $cfoldr :: forall p a b. (a -> b -> b) -> b -> Partial p a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Partial p a -> b
    $cfoldr' :: forall p a b. (a -> b -> b) -> b -> Partial p a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Partial p a -> b
    $cfoldl :: forall p b a. (b -> a -> b) -> b -> Partial p a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Partial p a -> b
    $cfoldl' :: forall p b a. (b -> a -> b) -> b -> Partial p a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Partial p a -> b
    $cfoldr1 :: forall p a. (a -> a -> a) -> Partial p a -> a
    foldr1 :: forall a. (a -> a -> a) -> Partial p a -> a
    $cfoldl1 :: forall p a. (a -> a -> a) -> Partial p a -> a
    foldl1 :: forall a. (a -> a -> a) -> Partial p a -> a
    $ctoList :: forall p a. Partial p a -> [a]
    toList :: forall a. Partial p a -> [a]
    $cnull :: forall p a. Partial p a -> Bool
    null :: forall a. Partial p a -> Bool
    $clength :: forall p a. Partial p a -> Int
    length :: forall a. Partial p a -> Int
    $celem :: forall p a. Eq a => a -> Partial p a -> Bool
    elem :: forall a. Eq a => a -> Partial p a -> Bool
    $cmaximum :: forall p a. Ord a => Partial p a -> a
    maximum :: forall a. Ord a => Partial p a -> a
    $cminimum :: forall p a. Ord a => Partial p a -> a
    minimum :: forall a. Ord a => Partial p a -> a
    $csum :: forall p a. Num a => Partial p a -> a
    sum :: forall a. Num a => Partial p a -> a
    $cproduct :: forall p a. Num a => Partial p a -> a
    product :: forall a. Num a => Partial p a -> a
    Foldable, Functor (Partial p)
    Foldable (Partial p)
    Functor (Partial p)
    -> Foldable (Partial p)
    -> (forall (f :: Type -> Type) a b.
        Applicative f =>
        (a -> f b) -> Partial p a -> f (Partial p b))
    -> (forall (f :: Type -> Type) a.
        Applicative f =>
        Partial p (f a) -> f (Partial p a))
    -> (forall (m :: Type -> Type) a b.
        Monad m =>
        (a -> m b) -> Partial p a -> m (Partial p b))
    -> (forall (m :: Type -> Type) a.
        Monad m =>
        Partial p (m a) -> m (Partial p a))
    -> Traversable (Partial p)
    forall p. Functor (Partial p)
    forall p. Foldable (Partial p)
    forall p (m :: Type -> Type) a.
    Monad m =>
    Partial p (m a) -> m (Partial p a)
    forall p (f :: Type -> Type) a.
    Applicative f =>
    Partial p (f a) -> f (Partial p a)
    forall p (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Partial p a -> m (Partial p b)
    forall p (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Partial p a -> f (Partial p b)
    forall (t :: Type -> Type).
    Functor t
    -> Foldable t
    -> (forall (f :: Type -> Type) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: Type -> Type) a.
        Applicative f =>
        t (f a) -> f (t a))
    -> (forall (m :: Type -> Type) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: Type -> Type) a.
    Monad m =>
    Partial p (m a) -> m (Partial p a)
    forall (f :: Type -> Type) a.
    Applicative f =>
    Partial p (f a) -> f (Partial p a)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Partial p a -> m (Partial p b)
    forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Partial p a -> f (Partial p b)
    $ctraverse :: forall p (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Partial p a -> f (Partial p b)
    traverse :: forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Partial p a -> f (Partial p b)
    $csequenceA :: forall p (f :: Type -> Type) a.
    Applicative f =>
    Partial p (f a) -> f (Partial p a)
    sequenceA :: forall (f :: Type -> Type) a.
    Applicative f =>
    Partial p (f a) -> f (Partial p a)
    $cmapM :: forall p (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Partial p a -> m (Partial p b)
    mapM :: forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Partial p a -> m (Partial p b)
    $csequence :: forall p (m :: Type -> Type) a.
    Monad m =>
    Partial p (m a) -> m (Partial p a)
    sequence :: forall (m :: Type -> Type) a.
    Monad m =>
    Partial p (m a) -> m (Partial p a)
    Traversable, Eq (Partial p v)
    Eq (Partial p v)
    -> (Partial p v -> Partial p v -> Ordering)
    -> (Partial p v -> Partial p v -> Bool)
    -> (Partial p v -> Partial p v -> Bool)
    -> (Partial p v -> Partial p v -> Bool)
    -> (Partial p v -> Partial p v -> Bool)
    -> (Partial p v -> Partial p v -> Partial p v)
    -> (Partial p v -> Partial p v -> Partial p v)
    -> Ord (Partial p v)
    Partial p v -> Partial p v -> Bool
    Partial p v -> Partial p v -> Ordering
    Partial p v -> Partial p v -> Partial p v
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall {p} {v}. (Ord p, Ord v) => Eq (Partial p v)
    forall p v. (Ord p, Ord v) => Partial p v -> Partial p v -> Bool
    forall p v.
    (Ord p, Ord v) =>
    Partial p v -> Partial p v -> Ordering
    forall p v.
    (Ord p, Ord v) =>
    Partial p v -> Partial p v -> Partial p v
    $ccompare :: forall p v.
    (Ord p, Ord v) =>
    Partial p v -> Partial p v -> Ordering
    compare :: Partial p v -> Partial p v -> Ordering
    $c< :: forall p v. (Ord p, Ord v) => Partial p v -> Partial p v -> Bool
    < :: Partial p v -> Partial p v -> Bool
    $c<= :: forall p v. (Ord p, Ord v) => Partial p v -> Partial p v -> Bool
    <= :: Partial p v -> Partial p v -> Bool
    $c> :: forall p v. (Ord p, Ord v) => Partial p v -> Partial p v -> Bool
    > :: Partial p v -> Partial p v -> Bool
    $c>= :: forall p v. (Ord p, Ord v) => Partial p v -> Partial p v -> Bool
    >= :: Partial p v -> Partial p v -> Bool
    $cmax :: forall p v.
    (Ord p, Ord v) =>
    Partial p v -> Partial p v -> Partial p v
    max :: Partial p v -> Partial p v -> Partial p v
    $cmin :: forall p v.
    (Ord p, Ord v) =>
    Partial p v -> Partial p v -> Partial p v
    min :: Partial p v -> Partial p v -> Partial p v
    Ord, Int -> Partial p v -> ShowS
    [Partial p v] -> ShowS
    Partial p v -> String
    (Int -> Partial p v -> ShowS)
    -> (Partial p v -> String)
    -> ([Partial p v] -> ShowS)
    -> Show (Partial p v)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall p v. (Show p, Show v) => Int -> Partial p v -> ShowS
    forall p v. (Show p, Show v) => [Partial p v] -> ShowS
    forall p v. (Show p, Show v) => Partial p v -> String
    $cshowsPrec :: forall p v. (Show p, Show v) => Int -> Partial p v -> ShowS
    showsPrec :: Int -> Partial p v -> ShowS
    $cshow :: forall p v. (Show p, Show v) => Partial p v -> String
    show :: Partial p v -> String
    $cshowList :: forall p v. (Show p, Show v) => [Partial p v] -> ShowS
    showList :: [Partial p v] -> ShowS
    Show)

    makeLenses ''Partial

    $(deriveBifunctor     ''Partial)
    $(deriveBifoldable    ''Partial)
    $(deriveBitraversable ''Partial)
    $(deriveEq1           ''Partial)
    $(deriveEq2           ''Partial)
    $(deriveOrd1          ''Partial)
    $(deriveOrd2          ''Partial)
    $(deriveShow1         ''Partial)
    $(deriveShow2         ''Partial)

    -- | Create a 'Partial' expression from a value that is always defined.
    total :: IsExprBuilder sym
          => sym
          -> v
          -> Partial (Pred sym) v
    total :: forall sym v. IsExprBuilder sym => sym -> v -> Partial (Pred sym) v
    total sym
    sym = SymExpr sym BaseBoolType
    -> v -> Partial (SymExpr sym BaseBoolType) v
    forall p v. p -> v -> Partial p v
    Partial (sym -> SymExpr sym BaseBoolType
    forall sym. IsExprBuilder sym => sym -> Pred sym
    truePred sym
    sym)

    ------------------------------------------------------------------------
    -- ** PartialWithErr

    -- | Either a partial value, or a straight-up error.
    data PartialWithErr e p v =
        NoErr (Partial p v)
      | Err e
      deriving (Typeable (PartialWithErr e p v)
    Typeable (PartialWithErr e p v)
    -> (forall (c :: Type -> Type).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g)
        -> PartialWithErr e p v
        -> c (PartialWithErr e p v))
    -> (forall (c :: Type -> Type).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c (PartialWithErr e p v))
    -> (PartialWithErr e p v -> Constr)
    -> (PartialWithErr e p v -> DataType)
    -> (forall (t :: Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c (PartialWithErr e p v)))
    -> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c (PartialWithErr e p v)))
    -> ((forall b. Data b => b -> b)
        -> PartialWithErr e p v -> PartialWithErr e p v)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r)
    -> (forall u.
        (forall d. Data d => d -> u) -> PartialWithErr e p v -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> PartialWithErr e p v -> u)
    -> (forall (m :: Type -> Type).
        Monad m =>
        (forall d. Data d => d -> m d)
        -> PartialWithErr e p v -> m (PartialWithErr e p v))
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> PartialWithErr e p v -> m (PartialWithErr e p v))
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> PartialWithErr e p v -> m (PartialWithErr e p v))
    -> Data (PartialWithErr e p v)
    PartialWithErr e p v -> Constr
    PartialWithErr e p v -> DataType
    (forall b. Data b => b -> b)
    -> PartialWithErr e p v -> PartialWithErr e p v
    forall a.
    Typeable a
    -> (forall (c :: Type -> Type).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: Type -> Type).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: Type -> Type).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u.
    Int -> (forall d. Data d => d -> u) -> PartialWithErr e p v -> u
    forall u.
    (forall d. Data d => d -> u) -> PartialWithErr e p v -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r
    forall {e} {p} {v}.
    (Data p, Data v, Data e) =>
    Typeable (PartialWithErr e p v)
    forall e p v.
    (Data p, Data v, Data e) =>
    PartialWithErr e p v -> Constr
    forall e p v.
    (Data p, Data v, Data e) =>
    PartialWithErr e p v -> DataType
    forall e p v.
    (Data p, Data v, Data e) =>
    (forall b. Data b => b -> b)
    -> PartialWithErr e p v -> PartialWithErr e p v
    forall e p v u.
    (Data p, Data v, Data e) =>
    Int -> (forall d. Data d => d -> u) -> PartialWithErr e p v -> u
    forall e p v u.
    (Data p, Data v, Data e) =>
    (forall d. Data d => d -> u) -> PartialWithErr e p v -> [u]
    forall e p v r r'.
    (Data p, Data v, Data e) =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r
    forall e p v r r'.
    (Data p, Data v, Data e) =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r
    forall e p v (m :: Type -> Type).
    (Data p, Data v, Data e, Monad m) =>
    (forall d. Data d => d -> m d)
    -> PartialWithErr e p v -> m (PartialWithErr e p v)
    forall e p v (m :: Type -> Type).
    (Data p, Data v, Data e, MonadPlus m) =>
    (forall d. Data d => d -> m d)
    -> PartialWithErr e p v -> m (PartialWithErr e p v)
    forall e p v (c :: Type -> Type).
    (Data p, Data v, Data e) =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (PartialWithErr e p v)
    forall e p v (c :: Type -> Type).
    (Data p, Data v, Data e) =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> PartialWithErr e p v
    -> c (PartialWithErr e p v)
    forall e p v (t :: Type -> Type) (c :: Type -> Type).
    (Data p, Data v, Data e, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (PartialWithErr e p v))
    forall e p v (t :: Type -> Type -> Type) (c :: Type -> Type).
    (Data p, Data v, Data e, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (PartialWithErr e p v))
    forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> PartialWithErr e p v -> m (PartialWithErr e p v)
    forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PartialWithErr e p v -> m (PartialWithErr e p v)
    forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (PartialWithErr e p v)
    forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> PartialWithErr e p v
    -> c (PartialWithErr e p v)
    forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (PartialWithErr e p v))
    forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (PartialWithErr e p v))
    $cgfoldl :: forall e p v (c :: Type -> Type).
    (Data p, Data v, Data e) =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> PartialWithErr e p v
    -> c (PartialWithErr e p v)
    gfoldl :: forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> PartialWithErr e p v
    -> c (PartialWithErr e p v)
    $cgunfold :: forall e p v (c :: Type -> Type).
    (Data p, Data v, Data e) =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (PartialWithErr e p v)
    gunfold :: forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (PartialWithErr e p v)
    $ctoConstr :: forall e p v.
    (Data p, Data v, Data e) =>
    PartialWithErr e p v -> Constr
    toConstr :: PartialWithErr e p v -> Constr
    $cdataTypeOf :: forall e p v.
    (Data p, Data v, Data e) =>
    PartialWithErr e p v -> DataType
    dataTypeOf :: PartialWithErr e p v -> DataType
    $cdataCast1 :: forall e p v (t :: Type -> Type) (c :: Type -> Type).
    (Data p, Data v, Data e, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (PartialWithErr e p v))
    dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (PartialWithErr e p v))
    $cdataCast2 :: forall e p v (t :: Type -> Type -> Type) (c :: Type -> Type).
    (Data p, Data v, Data e, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (PartialWithErr e p v))
    dataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (PartialWithErr e p v))
    $cgmapT :: forall e p v.
    (Data p, Data v, Data e) =>
    (forall b. Data b => b -> b)
    -> PartialWithErr e p v -> PartialWithErr e p v
    gmapT :: (forall b. Data b => b -> b)
    -> PartialWithErr e p v -> PartialWithErr e p v
    $cgmapQl :: forall e p v r r'.
    (Data p, Data v, Data e) =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r
    $cgmapQr :: forall e p v r r'.
    (Data p, Data v, Data e) =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r
    $cgmapQ :: forall e p v u.
    (Data p, Data v, Data e) =>
    (forall d. Data d => d -> u) -> PartialWithErr e p v -> [u]
    gmapQ :: forall u.
    (forall d. Data d => d -> u) -> PartialWithErr e p v -> [u]
    $cgmapQi :: forall e p v u.
    (Data p, Data v, Data e) =>
    Int -> (forall d. Data d => d -> u) -> PartialWithErr e p v -> u
    gmapQi :: forall u.
    Int -> (forall d. Data d => d -> u) -> PartialWithErr e p v -> u
    $cgmapM :: forall e p v (m :: Type -> Type).
    (Data p, Data v, Data e, Monad m) =>
    (forall d. Data d => d -> m d)
    -> PartialWithErr e p v -> m (PartialWithErr e p v)
    gmapM :: forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> PartialWithErr e p v -> m (PartialWithErr e p v)
    $cgmapMp :: forall e p v (m :: Type -> Type).
    (Data p, Data v, Data e, MonadPlus m) =>
    (forall d. Data d => d -> m d)
    -> PartialWithErr e p v -> m (PartialWithErr e p v)
    gmapMp :: forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PartialWithErr e p v -> m (PartialWithErr e p v)
    $cgmapMo :: forall e p v (m :: Type -> Type).
    (Data p, Data v, Data e, MonadPlus m) =>
    (forall d. Data d => d -> m d)
    -> PartialWithErr e p v -> m (PartialWithErr e p v)
    gmapMo :: forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PartialWithErr e p v -> m (PartialWithErr e p v)
    Data, PartialWithErr e p v -> PartialWithErr e p v -> Bool
    (PartialWithErr e p v -> PartialWithErr e p v -> Bool)
    -> (PartialWithErr e p v -> PartialWithErr e p v -> Bool)
    -> Eq (PartialWithErr e p v)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall e p v.
    (Eq p, Eq v, Eq e) =>
    PartialWithErr e p v -> PartialWithErr e p v -> Bool
    $c== :: forall e p v.
    (Eq p, Eq v, Eq e) =>
    PartialWithErr e p v -> PartialWithErr e p v -> Bool
    == :: PartialWithErr e p v -> PartialWithErr e p v -> Bool
    $c/= :: forall e p v.
    (Eq p, Eq v, Eq e) =>
    PartialWithErr e p v -> PartialWithErr e p v -> Bool
    /= :: PartialWithErr e p v -> PartialWithErr e p v -> Bool
    Eq, (forall a b.
     (a -> b) -> PartialWithErr e p a -> PartialWithErr e p b)
    -> (forall a b. a -> PartialWithErr e p b -> PartialWithErr e p a)
    -> Functor (PartialWithErr e p)
    forall a b. a -> PartialWithErr e p b -> PartialWithErr e p a
    forall a b.
    (a -> b) -> PartialWithErr e p a -> PartialWithErr e p b
    forall e p a b. a -> PartialWithErr e p b -> PartialWithErr e p a
    forall e p a b.
    (a -> b) -> PartialWithErr e p a -> PartialWithErr e p b
    forall (f :: Type -> Type).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall e p a b.
    (a -> b) -> PartialWithErr e p a -> PartialWithErr e p b
    fmap :: forall a b.
    (a -> b) -> PartialWithErr e p a -> PartialWithErr e p b
    $c<$ :: forall e p a b. a -> PartialWithErr e p b -> PartialWithErr e p a
    <$ :: forall a b. a -> PartialWithErr e p b -> PartialWithErr e p a
    Functor, (forall x. PartialWithErr e p v -> Rep (PartialWithErr e p v) x)
    -> (forall x. Rep (PartialWithErr e p v) x -> PartialWithErr e p v)
    -> Generic (PartialWithErr e p v)
    forall x. Rep (PartialWithErr e p v) x -> PartialWithErr e p v
    forall x. PartialWithErr e p v -> Rep (PartialWithErr e p v) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall e p v x.
    Rep (PartialWithErr e p v) x -> PartialWithErr e p v
    forall e p v x.
    PartialWithErr e p v -> Rep (PartialWithErr e p v) x
    $cfrom :: forall e p v x.
    PartialWithErr e p v -> Rep (PartialWithErr e p v) x
    from :: forall x. PartialWithErr e p v -> Rep (PartialWithErr e p v) x
    $cto :: forall e p v x.
    Rep (PartialWithErr e p v) x -> PartialWithErr e p v
    to :: forall x. Rep (PartialWithErr e p v) x -> PartialWithErr e p v
    Generic, (forall a. PartialWithErr e p a -> Rep1 (PartialWithErr e p) a)
    -> (forall a. Rep1 (PartialWithErr e p) a -> PartialWithErr e p a)
    -> Generic1 (PartialWithErr e p)
    forall a. Rep1 (PartialWithErr e p) a -> PartialWithErr e p a
    forall a. PartialWithErr e p a -> Rep1 (PartialWithErr e p) a
    forall e p a. Rep1 (PartialWithErr e p) a -> PartialWithErr e p a
    forall e p a. PartialWithErr e p a -> Rep1 (PartialWithErr e p) a
    forall k (f :: k -> Type).
    (forall (a :: k). f a -> Rep1 f a)
    -> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
    $cfrom1 :: forall e p a. PartialWithErr e p a -> Rep1 (PartialWithErr e p) a
    from1 :: forall a. PartialWithErr e p a -> Rep1 (PartialWithErr e p) a
    $cto1 :: forall e p a. Rep1 (PartialWithErr e p) a -> PartialWithErr e p a
    to1 :: forall a. Rep1 (PartialWithErr e p) a -> PartialWithErr e p a
    Generic1, (forall m. Monoid m => PartialWithErr e p m -> m)
    -> (forall m a. Monoid m => (a -> m) -> PartialWithErr e p a -> m)
    -> (forall m a. Monoid m => (a -> m) -> PartialWithErr e p a -> m)
    -> (forall a b. (a -> b -> b) -> b -> PartialWithErr e p a -> b)
    -> (forall a b. (a -> b -> b) -> b -> PartialWithErr e p a -> b)
    -> (forall b a. (b -> a -> b) -> b -> PartialWithErr e p a -> b)
    -> (forall b a. (b -> a -> b) -> b -> PartialWithErr e p a -> b)
    -> (forall a. (a -> a -> a) -> PartialWithErr e p a -> a)
    -> (forall a. (a -> a -> a) -> PartialWithErr e p a -> a)
    -> (forall a. PartialWithErr e p a -> [a])
    -> (forall a. PartialWithErr e p a -> Bool)
    -> (forall a. PartialWithErr e p a -> Int)
    -> (forall a. Eq a => a -> PartialWithErr e p a -> Bool)
    -> (forall a. Ord a => PartialWithErr e p a -> a)
    -> (forall a. Ord a => PartialWithErr e p a -> a)
    -> (forall a. Num a => PartialWithErr e p a -> a)
    -> (forall a. Num a => PartialWithErr e p a -> a)
    -> Foldable (PartialWithErr e p)
    forall a. Eq a => a -> PartialWithErr e p a -> Bool
    forall a. Num a => PartialWithErr e p a -> a
    forall a. Ord a => PartialWithErr e p a -> a
    forall m. Monoid m => PartialWithErr e p m -> m
    forall a. PartialWithErr e p a -> Bool
    forall a. PartialWithErr e p a -> Int
    forall a. PartialWithErr e p a -> [a]
    forall a. (a -> a -> a) -> PartialWithErr e p a -> a
    forall m a. Monoid m => (a -> m) -> PartialWithErr e p a -> m
    forall b a. (b -> a -> b) -> b -> PartialWithErr e p a -> b
    forall a b. (a -> b -> b) -> b -> PartialWithErr e p a -> b
    forall e p a. Eq a => a -> PartialWithErr e p a -> Bool
    forall e p a. Num a => PartialWithErr e p a -> a
    forall e p a. Ord a => PartialWithErr e p a -> a
    forall e p m. Monoid m => PartialWithErr e p m -> m
    forall e p a. PartialWithErr e p a -> Bool
    forall e p a. PartialWithErr e p a -> Int
    forall e p a. PartialWithErr e p a -> [a]
    forall e p a. (a -> a -> a) -> PartialWithErr e p a -> a
    forall e p m a. Monoid m => (a -> m) -> PartialWithErr e p a -> m
    forall e p b a. (b -> a -> b) -> b -> PartialWithErr e p a -> b
    forall e p a b. (a -> b -> b) -> b -> PartialWithErr e p a -> b
    forall (t :: Type -> Type).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall e p m. Monoid m => PartialWithErr e p m -> m
    fold :: forall m. Monoid m => PartialWithErr e p m -> m
    $cfoldMap :: forall e p m a. Monoid m => (a -> m) -> PartialWithErr e p a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> PartialWithErr e p a -> m
    $cfoldMap' :: forall e p m a. Monoid m => (a -> m) -> PartialWithErr e p a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> PartialWithErr e p a -> m
    $cfoldr :: forall e p a b. (a -> b -> b) -> b -> PartialWithErr e p a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> PartialWithErr e p a -> b
    $cfoldr' :: forall e p a b. (a -> b -> b) -> b -> PartialWithErr e p a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> PartialWithErr e p a -> b
    $cfoldl :: forall e p b a. (b -> a -> b) -> b -> PartialWithErr e p a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> PartialWithErr e p a -> b
    $cfoldl' :: forall e p b a. (b -> a -> b) -> b -> PartialWithErr e p a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> PartialWithErr e p a -> b
    $cfoldr1 :: forall e p a. (a -> a -> a) -> PartialWithErr e p a -> a
    foldr1 :: forall a. (a -> a -> a) -> PartialWithErr e p a -> a
    $cfoldl1 :: forall e p a. (a -> a -> a) -> PartialWithErr e p a -> a
    foldl1 :: forall a. (a -> a -> a) -> PartialWithErr e p a -> a
    $ctoList :: forall e p a. PartialWithErr e p a -> [a]
    toList :: forall a. PartialWithErr e p a -> [a]
    $cnull :: forall e p a. PartialWithErr e p a -> Bool
    null :: forall a. PartialWithErr e p a -> Bool
    $clength :: forall e p a. PartialWithErr e p a -> Int
    length :: forall a. PartialWithErr e p a -> Int
    $celem :: forall e p a. Eq a => a -> PartialWithErr e p a -> Bool
    elem :: forall a. Eq a => a -> PartialWithErr e p a -> Bool
    $cmaximum :: forall e p a. Ord a => PartialWithErr e p a -> a
    maximum :: forall a. Ord a => PartialWithErr e p a -> a
    $cminimum :: forall e p a. Ord a => PartialWithErr e p a -> a
    minimum :: forall a. Ord a => PartialWithErr e p a -> a
    $csum :: forall e p a. Num a => PartialWithErr e p a -> a
    sum :: forall a. Num a => PartialWithErr e p a -> a
    $cproduct :: forall e p a. Num a => PartialWithErr e p a -> a
    product :: forall a. Num a => PartialWithErr e p a -> a
    Foldable, Functor (PartialWithErr e p)
    Foldable (PartialWithErr e p)
    Functor (PartialWithErr e p)
    -> Foldable (PartialWithErr e p)
    -> (forall (f :: Type -> Type) a b.
        Applicative f =>
        (a -> f b) -> PartialWithErr e p a -> f (PartialWithErr e p b))
    -> (forall (f :: Type -> Type) a.
        Applicative f =>
        PartialWithErr e p (f a) -> f (PartialWithErr e p a))
    -> (forall (m :: Type -> Type) a b.
        Monad m =>
        (a -> m b) -> PartialWithErr e p a -> m (PartialWithErr e p b))
    -> (forall (m :: Type -> Type) a.
        Monad m =>
        PartialWithErr e p (m a) -> m (PartialWithErr e p a))
    -> Traversable (PartialWithErr e p)
    forall e p. Functor (PartialWithErr e p)
    forall e p. Foldable (PartialWithErr e p)
    forall e p (m :: Type -> Type) a.
    Monad m =>
    PartialWithErr e p (m a) -> m (PartialWithErr e p a)
    forall e p (f :: Type -> Type) a.
    Applicative f =>
    PartialWithErr e p (f a) -> f (PartialWithErr e p a)
    forall e p (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> PartialWithErr e p a -> m (PartialWithErr e p b)
    forall e p (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> PartialWithErr e p a -> f (PartialWithErr e p b)
    forall (t :: Type -> Type).
    Functor t
    -> Foldable t
    -> (forall (f :: Type -> Type) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: Type -> Type) a.
        Applicative f =>
        t (f a) -> f (t a))
    -> (forall (m :: Type -> Type) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: Type -> Type) a.
    Monad m =>
    PartialWithErr e p (m a) -> m (PartialWithErr e p a)
    forall (f :: Type -> Type) a.
    Applicative f =>
    PartialWithErr e p (f a) -> f (PartialWithErr e p a)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> PartialWithErr e p a -> m (PartialWithErr e p b)
    forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> PartialWithErr e p a -> f (PartialWithErr e p b)
    $ctraverse :: forall e p (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> PartialWithErr e p a -> f (PartialWithErr e p b)
    traverse :: forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> PartialWithErr e p a -> f (PartialWithErr e p b)
    $csequenceA :: forall e p (f :: Type -> Type) a.
    Applicative f =>
    PartialWithErr e p (f a) -> f (PartialWithErr e p a)
    sequenceA :: forall (f :: Type -> Type) a.
    Applicative f =>
    PartialWithErr e p (f a) -> f (PartialWithErr e p a)
    $cmapM :: forall e p (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> PartialWithErr e p a -> m (PartialWithErr e p b)
    mapM :: forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> PartialWithErr e p a -> m (PartialWithErr e p b)
    $csequence :: forall e p (m :: Type -> Type) a.
    Monad m =>
    PartialWithErr e p (m a) -> m (PartialWithErr e p a)
    sequence :: forall (m :: Type -> Type) a.
    Monad m =>
    PartialWithErr e p (m a) -> m (PartialWithErr e p a)
    Traversable, Eq (PartialWithErr e p v)
    Eq (PartialWithErr e p v)
    -> (PartialWithErr e p v -> PartialWithErr e p v -> Ordering)
    -> (PartialWithErr e p v -> PartialWithErr e p v -> Bool)
    -> (PartialWithErr e p v -> PartialWithErr e p v -> Bool)
    -> (PartialWithErr e p v -> PartialWithErr e p v -> Bool)
    -> (PartialWithErr e p v -> PartialWithErr e p v -> Bool)
    -> (PartialWithErr e p v
        -> PartialWithErr e p v -> PartialWithErr e p v)
    -> (PartialWithErr e p v
        -> PartialWithErr e p v -> PartialWithErr e p v)
    -> Ord (PartialWithErr e p v)
    PartialWithErr e p v -> PartialWithErr e p v -> Bool
    PartialWithErr e p v -> PartialWithErr e p v -> Ordering
    PartialWithErr e p v
    -> PartialWithErr e p v -> PartialWithErr e p v
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall {e} {p} {v}.
    (Ord p, Ord v, Ord e) =>
    Eq (PartialWithErr e p v)
    forall e p v.
    (Ord p, Ord v, Ord e) =>
    PartialWithErr e p v -> PartialWithErr e p v -> Bool
    forall e p v.
    (Ord p, Ord v, Ord e) =>
    PartialWithErr e p v -> PartialWithErr e p v -> Ordering
    forall e p v.
    (Ord p, Ord v, Ord e) =>
    PartialWithErr e p v
    -> PartialWithErr e p v -> PartialWithErr e p v
    $ccompare :: forall e p v.
    (Ord p, Ord v, Ord e) =>
    PartialWithErr e p v -> PartialWithErr e p v -> Ordering
    compare :: PartialWithErr e p v -> PartialWithErr e p v -> Ordering
    $c< :: forall e p v.
    (Ord p, Ord v, Ord e) =>
    PartialWithErr e p v -> PartialWithErr e p v -> Bool
    < :: PartialWithErr e p v -> PartialWithErr e p v -> Bool
    $c<= :: forall e p v.
    (Ord p, Ord v, Ord e) =>
    PartialWithErr e p v -> PartialWithErr e p v -> Bool
    <= :: PartialWithErr e p v -> PartialWithErr e p v -> Bool
    $c> :: forall e p v.
    (Ord p, Ord v, Ord e) =>
    PartialWithErr e p v -> PartialWithErr e p v -> Bool
    > :: PartialWithErr e p v -> PartialWithErr e p v -> Bool
    $c>= :: forall e p v.
    (Ord p, Ord v, Ord e) =>
    PartialWithErr e p v -> PartialWithErr e p v -> Bool
    >= :: PartialWithErr e p v -> PartialWithErr e p v -> Bool
    $cmax :: forall e p v.
    (Ord p, Ord v, Ord e) =>
    PartialWithErr e p v
    -> PartialWithErr e p v -> PartialWithErr e p v
    max :: PartialWithErr e p v
    -> PartialWithErr e p v -> PartialWithErr e p v
    $cmin :: forall e p v.
    (Ord p, Ord v, Ord e) =>
    PartialWithErr e p v
    -> PartialWithErr e p v -> PartialWithErr e p v
    min :: PartialWithErr e p v
    -> PartialWithErr e p v -> PartialWithErr e p v
    Ord, Int -> PartialWithErr e p v -> ShowS
    [PartialWithErr e p v] -> ShowS
    PartialWithErr e p v -> String
    (Int -> PartialWithErr e p v -> ShowS)
    -> (PartialWithErr e p v -> String)
    -> ([PartialWithErr e p v] -> ShowS)
    -> Show (PartialWithErr e p v)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall e p v.
    (Show p, Show v, Show e) =>
    Int -> PartialWithErr e p v -> ShowS
    forall e p v.
    (Show p, Show v, Show e) =>
    [PartialWithErr e p v] -> ShowS
    forall e p v.
    (Show p, Show v, Show e) =>
    PartialWithErr e p v -> String
    $cshowsPrec :: forall e p v.
    (Show p, Show v, Show e) =>
    Int -> PartialWithErr e p v -> ShowS
    showsPrec :: Int -> PartialWithErr e p v -> ShowS
    $cshow :: forall e p v.
    (Show p, Show v, Show e) =>
    PartialWithErr e p v -> String
    show :: PartialWithErr e p v -> String
    $cshowList :: forall e p v.
    (Show p, Show v, Show e) =>
    [PartialWithErr e p v] -> ShowS
    showList :: [PartialWithErr e p v] -> ShowS
    Show)

    $(deriveBifunctor     ''PartialWithErr)
    $(deriveBifoldable    ''PartialWithErr)
    $(deriveBitraversable ''PartialWithErr)
    $(deriveEq1           ''PartialWithErr)
    $(deriveEq2           ''PartialWithErr)
    $(deriveOrd1          ''PartialWithErr)
    $(deriveOrd2          ''PartialWithErr)
    $(deriveShow1         ''PartialWithErr)
    $(deriveShow2         ''PartialWithErr)

    ------------------------------------------------------------------------
    -- ** PartExpr

    -- | A 'PartExpr' is a 'PartialWithErr' that provides no information about what
    -- went wrong. Its name is historic.
    type PartExpr p v = PartialWithErr () p v

    pattern Unassigned :: PartExpr p v
    pattern $mUnassigned :: forall {r} {p} {v}.
    PartExpr p v -> ((# #) -> r) -> ((# #) -> r) -> r
    $bUnassigned :: forall p v. PartExpr p v
    Unassigned = Err ()

    pattern PE :: p -> v -> PartExpr p v
    pattern $mPE :: forall {r} {p} {v}.
    PartExpr p v -> (p -> v -> r) -> ((# #) -> r) -> r
    $bPE :: forall p v. p -> v -> PartExpr p v
    PE p v = NoErr (Partial p v)

    -- Claim that the above two patterns are exhaustive for @PartExpr p v@
    {-# COMPLETE Unassigned, PE #-}

    mkPE :: IsExpr p => p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
    mkPE :: forall (p :: BaseType -> Type) a.
    IsExpr p =>
    p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
    mkPE p BaseBoolType
    p a
    v =
      case p BaseBoolType -> Maybe Bool
    forall (e :: BaseType -> Type).
    IsExpr e =>
    e BaseBoolType -> Maybe Bool
    asConstantPred p BaseBoolType
    p of
        Just Bool
    False -> PartExpr (p BaseBoolType) a
    forall p v. PartExpr p v
    Unassigned
        Maybe Bool
    _ -> p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
    forall p v. p -> v -> PartExpr p v
    PE p BaseBoolType
    p a
    v

    -- | Create a part expression from a value that is always defined.
    justPartExpr :: IsExprBuilder sym => sym -> v -> PartExpr (Pred sym) v
    justPartExpr :: forall sym v.
    IsExprBuilder sym =>
    sym -> v -> PartExpr (Pred sym) v
    justPartExpr sym
    sym = Partial (SymExpr sym BaseBoolType) v
    -> PartialWithErr () (SymExpr sym BaseBoolType) v
    forall e p v. Partial p v -> PartialWithErr e p v
    NoErr (Partial (SymExpr sym BaseBoolType) v
     -> PartialWithErr () (SymExpr sym BaseBoolType) v)
    -> (v -> Partial (SymExpr sym BaseBoolType) v)
    -> v
    -> PartialWithErr () (SymExpr sym BaseBoolType) v
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . sym -> v -> Partial (SymExpr sym BaseBoolType) v
    forall sym v. IsExprBuilder sym => sym -> v -> Partial (Pred sym) v
    total sym
    sym

    -- | Create a part expression from a maybe value.
    maybePartExpr :: IsExprBuilder sym
                  => sym -> Maybe a -> PartExpr (Pred sym) a
    maybePartExpr :: forall sym a.
    IsExprBuilder sym =>
    sym -> Maybe a -> PartExpr (Pred sym) a
    maybePartExpr sym
    _ Maybe a
    Nothing = PartExpr (SymExpr sym BaseBoolType) a
    forall p v. PartExpr p v
    Unassigned
    maybePartExpr sym
    sym (Just a
    r) = sym -> a -> PartExpr (SymExpr sym BaseBoolType) a
    forall sym v.
    IsExprBuilder sym =>
    sym -> v -> PartExpr (Pred sym) v
    justPartExpr sym
    sym a
    r

    -- | @'joinMaybePE' = 'Data.Maybe.fromMaybe' 'Unassigned'@.
    joinMaybePE :: Maybe (PartExpr p v) -> PartExpr p v
    joinMaybePE :: forall p v. Maybe (PartExpr p v) -> PartExpr p v
    joinMaybePE Maybe (PartExpr p v)
    Nothing = PartExpr p v
    forall p v. PartExpr p v
    Unassigned
    joinMaybePE (Just PartExpr p v
    pe) = PartExpr p v
    pe

    ------------------------------------------------------------------------
    -- *** Merge

    -- | If-then-else on partial expressions.
    mergePartial :: (IsExprBuilder sym, MonadIO m) =>
      sym ->
      (Pred sym -> a -> a -> PartialT sym m a)
        {- ^ Operation to combine inner values. The 'Pred' parameter is the
             if-then-else condition. -} ->
      Pred sym {- ^ condition to merge on -} ->
      PartExpr (Pred sym) a {- ^ 'if' value -}  ->
      PartExpr (Pred sym) a {- ^ 'then' value -} ->
      m (PartExpr (Pred sym) a)

    {-# SPECIALIZE mergePartial ::
          IsExprBuilder sym =>
          sym ->
          (Pred sym -> a -> a -> PartialT sym IO a) ->
          Pred sym ->
          PartExpr (Pred sym) a ->
          PartExpr (Pred sym) a ->
          IO (PartExpr (Pred sym) a)   #-}

    mergePartial :: forall sym (m :: Type -> Type) a.
    (IsExprBuilder sym, MonadIO m) =>
    sym
    -> (Pred sym -> a -> a -> PartialT sym m a)
    -> Pred sym
    -> PartExpr (Pred sym) a
    -> PartExpr (Pred sym) a
    -> m (PartExpr (Pred sym) a)
    mergePartial sym
    _ Pred sym -> a -> a -> PartialT sym m a
    _ Pred sym
    _ PartExpr (Pred sym) a
    Unassigned PartExpr (Pred sym) a
    Unassigned =
         PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return PartExpr (Pred sym) a
    forall p v. PartExpr p v
    Unassigned
    mergePartial sym
    sym Pred sym -> a -> a -> PartialT sym m a
    _ Pred sym
    c (PE Pred sym
    px a
    x) PartExpr (Pred sym) a
    Unassigned =
         do Pred sym
    p <- IO (Pred sym) -> m (Pred sym)
    forall a. IO a -> m a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO (Pred sym) -> m (Pred sym)) -> IO (Pred sym) -> m (Pred sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    andPred sym
    sym Pred sym
    px Pred sym
    c
            PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a))
    -> PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a)
    forall a b. (a -> b) -> a -> b
    $! Pred sym -> a -> PartExpr (Pred sym) a
    forall (p :: BaseType -> Type) a.
    IsExpr p =>
    p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
    mkPE Pred sym
    p a
    x
    mergePartial sym
    sym Pred sym -> a -> a -> PartialT sym m a
    _ Pred sym
    c PartExpr (Pred sym) a
    Unassigned (PE Pred sym
    py a
    y) =
         do Pred sym
    p <- IO (Pred sym) -> m (Pred sym)
    forall a. IO a -> m a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    andPred sym
    sym Pred sym
    py (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Pred sym -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym Pred sym
    c)
            PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a))
    -> PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a)
    forall a b. (a -> b) -> a -> b
    $! Pred sym -> a -> PartExpr (Pred sym) a
    forall (p :: BaseType -> Type) a.
    IsExpr p =>
    p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
    mkPE Pred sym
    p a
    y
    mergePartial sym
    sym Pred sym -> a -> a -> PartialT sym m a
    f Pred sym
    c (PE Pred sym
    px a
    x) (PE Pred sym
    py a
    y) =
        do Pred sym
    p <- IO (Pred sym) -> m (Pred sym)
    forall a. IO a -> m a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
    itePred sym
    sym Pred sym
    c Pred sym
    px Pred sym
    py)
           sym -> Pred sym -> PartialT sym m a -> m (PartExpr (Pred sym) a)
    forall sym (m :: Type -> Type) a.
    sym -> Pred sym -> PartialT sym m a -> m (PartExpr (Pred sym) a)
    runPartialT sym
    sym Pred sym
    p (Pred sym -> a -> a -> PartialT sym m a
    f Pred sym
    c a
    x a
    y)

    -- | Merge a collection of partial values in an if-then-else tree.
    --   For example, if we merge a list like @[(xp,x),(yp,y),(zp,z)]@,
    --   we get a value that is morally equivalent to:
    --   @if xp then x else (if yp then y else (if zp then z else undefined))@.
    mergePartials :: (IsExprBuilder sym, MonadIO m) =>
      sym ->
      (Pred sym -> a -> a -> PartialT sym m a)
        {- ^ Operation to combine inner values.
             The 'Pred' parameter is the if-then-else condition.
         -} ->
      [(Pred sym, PartExpr (Pred sym) a)]      {- ^ values to merge -} ->
      m (PartExpr (Pred sym) a)
    mergePartials :: forall sym (m :: Type -> Type) a.
    (IsExprBuilder sym, MonadIO m) =>
    sym
    -> (Pred sym -> a -> a -> PartialT sym m a)
    -> [(Pred sym, PartExpr (Pred sym) a)]
    -> m (PartExpr (Pred sym) a)
    mergePartials sym
    sym Pred sym -> a -> a -> PartialT sym m a
    f = [(Pred sym, PartExpr (Pred sym) a)] -> m (PartExpr (Pred sym) a)
    go
      where
      go :: [(Pred sym, PartExpr (Pred sym) a)] -> m (PartExpr (Pred sym) a)
    go [] = PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return PartExpr (Pred sym) a
    forall p v. PartExpr p v
    Unassigned
      go ((Pred sym
    c,PartExpr (Pred sym) a
    x):[(Pred sym, PartExpr (Pred sym) a)]
    xs) =
        do PartExpr (Pred sym) a
    y <- [(Pred sym, PartExpr (Pred sym) a)] -> m (PartExpr (Pred sym) a)
    go [(Pred sym, PartExpr (Pred sym) a)]
    xs
           sym
    -> (Pred sym -> a -> a -> PartialT sym m a)
    -> Pred sym
    -> PartExpr (Pred sym) a
    -> PartExpr (Pred sym) a
    -> m (PartExpr (Pred sym) a)
    forall sym (m :: Type -> Type) a.
    (IsExprBuilder sym, MonadIO m) =>
    sym
    -> (Pred sym -> a -> a -> PartialT sym m a)
    -> Pred sym
    -> PartExpr (Pred sym) a
    -> PartExpr (Pred sym) a
    -> m (PartExpr (Pred sym) a)
    mergePartial sym
    sym Pred sym -> a -> a -> PartialT sym m a
    f Pred sym
    c PartExpr (Pred sym) a
    x PartExpr (Pred sym) a
    y

    ------------------------------------------------------------------------
    -- *** PartialT

    -- | A monad transformer which enables symbolic partial computations to run by
    -- maintaining a predicate on the value.
    newtype PartialT sym m a =
      PartialT { forall sym (m :: Type -> Type) a.
    PartialT sym m a -> sym -> Pred sym -> m (PartExpr (Pred sym) a)
    unPartial :: sym -> Pred sym -> m (PartExpr (Pred sym) a) }

    -- | Run a partial computation.
    runPartialT :: sym -- ^ Solver interface
                -> Pred sym -- ^ Initial condition
                -> PartialT sym m a -- ^ Computation to run.
                -> m (PartExpr (Pred sym) a)
    runPartialT :: forall sym (m :: Type -> Type) a.
    sym -> Pred sym -> PartialT sym m a -> m (PartExpr (Pred sym) a)
    runPartialT sym
    sym Pred sym
    p PartialT sym m a
    f = PartialT sym m a
    -> sym -> Pred sym -> m (PartialWithErr () (Pred sym) a)
    forall sym (m :: Type -> Type) a.
    PartialT sym m a -> sym -> Pred sym -> m (PartExpr (Pred sym) a)
    unPartial PartialT sym m a
    f sym
    sym Pred sym
    p

    instance Functor m => Functor (PartialT sym m) where
      fmap :: forall a b. (a -> b) -> PartialT sym m a -> PartialT sym m b
    fmap a -> b
    f PartialT sym m a
    mx = (sym -> Pred sym -> m (PartExpr (Pred sym) b)) -> PartialT sym m b
    forall sym (m :: Type -> Type) a.
    (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    PartialT ((sym -> Pred sym -> m (PartExpr (Pred sym) b))
     -> PartialT sym m b)
    -> (sym -> Pred sym -> m (PartExpr (Pred sym) b))
    -> PartialT sym m b
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym Pred sym
    p -> (PartExpr (Pred sym) a -> PartExpr (Pred sym) b)
    -> m (PartExpr (Pred sym) a) -> m (PartExpr (Pred sym) b)
    forall a b. (a -> b) -> m a -> m b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap PartExpr (Pred sym) a -> PartExpr (Pred sym) b
    resolve (PartialT sym m a -> sym -> Pred sym -> m (PartExpr (Pred sym) a)
    forall sym (m :: Type -> Type) a.
    PartialT sym m a -> sym -> Pred sym -> m (PartExpr (Pred sym) a)
    unPartial PartialT sym m a
    mx sym
    sym Pred sym
    p)
        where resolve :: PartExpr (Pred sym) a -> PartExpr (Pred sym) b
    resolve PartExpr (Pred sym) a
    Unassigned = PartExpr (Pred sym) b
    forall p v. PartExpr p v
    Unassigned
              resolve (PE Pred sym
    q a
    x) = Pred sym -> b -> PartExpr (Pred sym) b
    forall p v. p -> v -> PartExpr p v
    PE Pred sym
    q (a -> b
    f a
    x)

    -- We depend on the monad transformer as partialT explicitly orders
    -- the calls to the functions in (<*>).  This ordering allows us to
    -- avoid having any requirements that sym implement a partial interface.
    instance (IsExpr (SymExpr sym), Monad m) => Applicative (PartialT sym m) where
      pure :: forall a. a -> PartialT sym m a
    pure a
    a = (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    forall sym (m :: Type -> Type) a.
    (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    PartialT ((sym -> Pred sym -> m (PartExpr (Pred sym) a))
     -> PartialT sym m a)
    -> (sym -> Pred sym -> m (PartExpr (Pred sym) a))
    -> PartialT sym m a
    forall a b. (a -> b) -> a -> b
    $ \sym
    _ Pred sym
    p -> PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a))
    -> PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a)
    forall a b. (a -> b) -> a -> b
    $! Pred sym -> a -> PartExpr (Pred sym) a
    forall (p :: BaseType -> Type) a.
    IsExpr p =>
    p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
    mkPE Pred sym
    p a
    a
      PartialT sym m (a -> b)
    mf <*> :: forall a b.
    PartialT sym m (a -> b) -> PartialT sym m a -> PartialT sym m b
    <*> PartialT sym m a
    mx = PartialT sym m (a -> b)
    mf PartialT sym m (a -> b)
    -> ((a -> b) -> PartialT sym m b) -> PartialT sym m b
    forall a b.
    PartialT sym m a -> (a -> PartialT sym m b) -> PartialT sym m b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a -> b
    f -> PartialT sym m a
    mx PartialT sym m a -> (a -> PartialT sym m b) -> PartialT sym m b
    forall a b.
    PartialT sym m a -> (a -> PartialT sym m b) -> PartialT sym m b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a
    x -> b -> PartialT sym m b
    forall a. a -> PartialT sym m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (a -> b
    f a
    x)

    instance (IsExpr (SymExpr sym), Monad m) => Monad (PartialT sym m) where
      return :: forall a. a -> PartialT sym m a
    return = a -> PartialT sym m a
    forall a. a -> PartialT sym m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure
      PartialT sym m a
    m >>= :: forall a b.
    PartialT sym m a -> (a -> PartialT sym m b) -> PartialT sym m b
    >>= a -> PartialT sym m b
    h =
        (sym -> Pred sym -> m (PartExpr (Pred sym) b)) -> PartialT sym m b
    forall sym (m :: Type -> Type) a.
    (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    PartialT ((sym -> Pred sym -> m (PartExpr (Pred sym) b))
     -> PartialT sym m b)
    -> (sym -> Pred sym -> m (PartExpr (Pred sym) b))
    -> PartialT sym m b
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym Pred sym
    p -> do
          PartExpr (Pred sym) a
    pr <- PartialT sym m a -> sym -> Pred sym -> m (PartExpr (Pred sym) a)
    forall sym (m :: Type -> Type) a.
    PartialT sym m a -> sym -> Pred sym -> m (PartExpr (Pred sym) a)
    unPartial PartialT sym m a
    m sym
    sym Pred sym
    p
          case PartExpr (Pred sym) a
    pr of
            PartExpr (Pred sym) a
    Unassigned -> PartExpr (Pred sym) b -> m (PartExpr (Pred sym) b)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure PartExpr (Pred sym) b
    forall p v. PartExpr p v
    Unassigned
            PE Pred sym
    q a
    r -> PartialT sym m b -> sym -> Pred sym -> m (PartExpr (Pred sym) b)
    forall sym (m :: Type -> Type) a.
    PartialT sym m a -> sym -> Pred sym -> m (PartExpr (Pred sym) a)
    unPartial (a -> PartialT sym m b
    h a
    r) sym
    sym Pred sym
    q

    #if !MIN_VERSION_base(4,13,0)
      fail msg = PartialT $ \_ _ -> fail msg
    #endif

    instance (IsExpr (SymExpr sym), MonadFail m) => MonadFail (PartialT sym m) where
      fail :: forall a. String -> PartialT sym m a
    fail String
    msg = (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    forall sym (m :: Type -> Type) a.
    (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    PartialT ((sym -> Pred sym -> m (PartExpr (Pred sym) a))
     -> PartialT sym m a)
    -> (sym -> Pred sym -> m (PartExpr (Pred sym) a))
    -> PartialT sym m a
    forall a b. (a -> b) -> a -> b
    $ \sym
    _ Pred sym
    _ -> String -> m (PartExpr (Pred sym) a)
    forall a. String -> m a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail String
    msg

    instance IsExpr (SymExpr sym) => MonadTrans (PartialT sym) where
      lift :: forall (m :: Type -> Type) a. Monad m => m a -> PartialT sym m a
    lift m a
    m = (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    forall sym (m :: Type -> Type) a.
    (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    PartialT ((sym -> Pred sym -> m (PartExpr (Pred sym) a))
     -> PartialT sym m a)
    -> (sym -> Pred sym -> m (PartExpr (Pred sym) a))
    -> PartialT sym m a
    forall a b. (a -> b) -> a -> b
    $ \sym
    _ Pred sym
    p -> Pred sym -> a -> PartExpr (Pred sym) a
    forall p v. p -> v -> PartExpr p v
    PE Pred sym
    p (a -> PartExpr (Pred sym) a) -> m a -> m (PartExpr (Pred sym) a)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> m a
    m

    instance (IsExpr (SymExpr sym), MonadIO m) => MonadIO (PartialT sym m) where
      liftIO :: forall a. IO a -> PartialT sym m a
    liftIO = m a -> PartialT sym m a
    forall (m :: Type -> Type) a. Monad m => m a -> PartialT sym m a
    forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m a -> PartialT sym m a)
    -> (IO a -> m a) -> IO a -> PartialT sym m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IO a -> m a
    forall a. IO a -> m a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO

    -- | End the partial computation and just return the unassigned value.
    returnUnassigned :: Applicative m => PartialT sym m a
    returnUnassigned :: forall (m :: Type -> Type) sym a. Applicative m => PartialT sym m a
    returnUnassigned = (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    forall sym (m :: Type -> Type) a.
    (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    PartialT ((sym -> Pred sym -> m (PartExpr (Pred sym) a))
     -> PartialT sym m a)
    -> (sym -> Pred sym -> m (PartExpr (Pred sym) a))
    -> PartialT sym m a
    forall a b. (a -> b) -> a -> b
    $ \sym
    _ Pred sym
    _ -> PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure PartExpr (Pred sym) a
    forall p v. PartExpr p v
    Unassigned

    -- | Lift a 'Maybe' value to a partial expression.
    returnMaybe :: (IsExpr (SymExpr sym), Applicative m) =>  Maybe a -> PartialT sym m a
    returnMaybe :: forall sym (m :: Type -> Type) a.
    (IsExpr (SymExpr sym), Applicative m) =>
    Maybe a -> PartialT sym m a
    returnMaybe Maybe a
    Nothing  = PartialT sym m a
    forall (m :: Type -> Type) sym a. Applicative m => PartialT sym m a
    returnUnassigned
    returnMaybe (Just a
    a) = (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    forall sym (m :: Type -> Type) a.
    (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    PartialT ((sym -> Pred sym -> m (PartExpr (Pred sym) a))
     -> PartialT sym m a)
    -> (sym -> Pred sym -> m (PartExpr (Pred sym) a))
    -> PartialT sym m a
    forall a b. (a -> b) -> a -> b
    $ \sym
    _ Pred sym
    p -> PartExpr (Pred sym) a -> m (PartExpr (Pred sym) a)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Pred sym -> a -> PartExpr (Pred sym) a
    forall (p :: BaseType -> Type) a.
    IsExpr p =>
    p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
    mkPE Pred sym
    p a
    a)

    -- | Return a partial expression.
    --
    -- This joins the partial expression with the current constraints on the
    -- current computation.
    returnPartial :: (IsExprBuilder sym, MonadIO m)
                  => PartExpr (Pred sym) a
                  -> PartialT sym m a
    returnPartial :: forall sym (m :: Type -> Type) a.
    (IsExprBuilder sym, MonadIO m) =>
    PartExpr (Pred sym) a -> PartialT sym m a
    returnPartial PartExpr (SymExpr sym BaseBoolType) a
    Unassigned = PartialT sym m a
    forall (m :: Type -> Type) sym a. Applicative m => PartialT sym m a
    returnUnassigned
    returnPartial (PE SymExpr sym BaseBoolType
    q a
    a) = (sym
     -> SymExpr sym BaseBoolType
     -> m (PartExpr (SymExpr sym BaseBoolType) a))
    -> PartialT sym m a
    forall sym (m :: Type -> Type) a.
    (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
    PartialT ((sym
      -> SymExpr sym BaseBoolType
      -> m (PartExpr (SymExpr sym BaseBoolType) a))
     -> PartialT sym m a)
    -> (sym
        -> SymExpr sym BaseBoolType
        -> m (PartExpr (SymExpr sym BaseBoolType) a))
    -> PartialT sym m a
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym BaseBoolType
    p -> IO (PartExpr (SymExpr sym BaseBoolType) a)
    -> m (PartExpr (SymExpr sym BaseBoolType) a)
    forall a. IO a -> m a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (SymExpr sym BaseBoolType
    -> a -> PartExpr (SymExpr sym BaseBoolType) a
    forall (p :: BaseType -> Type) a.
    IsExpr p =>
    p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
    mkPE (SymExpr sym BaseBoolType
     -> a -> PartExpr (SymExpr sym BaseBoolType) a)
    -> IO (SymExpr sym BaseBoolType)
    -> IO (a -> PartExpr (SymExpr sym BaseBoolType) a)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    andPred sym
    sym SymExpr sym BaseBoolType
    p SymExpr sym BaseBoolType
    q IO (a -> PartExpr (SymExpr sym BaseBoolType) a)
    -> IO a -> IO (PartExpr (SymExpr sym BaseBoolType) a)
    forall a b. IO (a -> b) -> IO a -> IO b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> a -> IO a
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure a
    a)

    -- | Add an extra condition to the current partial computation.
    addCondition :: (IsExprBuilder sym, MonadIO m)
                 => Pred sym
                 -> PartialT sym m ()
    addCondition :: forall sym (m :: Type -> Type).
    (IsExprBuilder sym, MonadIO m) =>
    Pred sym -> PartialT sym m ()
    addCondition Pred sym
    q = PartExpr (Pred sym) () -> PartialT sym m ()
    forall sym (m :: Type -> Type) a.
    (IsExprBuilder sym, MonadIO m) =>
    PartExpr (Pred sym) a -> PartialT sym m a
    returnPartial (Pred sym -> () -> PartExpr (Pred sym) ()
    forall (p :: BaseType -> Type) a.
    IsExpr p =>
    p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
    mkPE Pred sym
    q ())