{-# 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 (Partial p v -> DataType
Partial p v -> Constr
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 {p} {v}. (Data p, Data v) => Typeable (Partial p v)
forall p v. (Data p, Data v) => Partial p v -> DataType
forall p v. (Data p, Data v) => Partial p v -> Constr
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 (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 -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Partial p v))
gmapMo :: 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)
gmapMp :: forall (m :: Type -> Type).
MonadPlus 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)
gmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Partial p v -> m (Partial p v)
$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)
gmapQi :: forall u. Int -> (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
gmapQ :: forall u. (forall d. Data d => d -> u) -> Partial p v -> [u]
$cgmapQ :: forall p v u.
(Data p, Data v) =>
(forall d. Data d => d -> u) -> Partial p v -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Partial p v -> r
$cgmapQl :: forall p v r r'.
(Data p, Data v) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Partial p v -> r
gmapT :: (forall b. Data b => b -> b) -> Partial p v -> Partial p v
$cgmapT :: forall p v.
(Data p, Data v) =>
(forall b. Data b => b -> b) -> Partial p v -> 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))
$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))
dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Partial p v))
$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))
dataTypeOf :: Partial p v -> DataType
$cdataTypeOf :: forall p v. (Data p, Data v) => Partial p v -> DataType
toConstr :: Partial p v -> Constr
$ctoConstr :: forall p v. (Data p, Data v) => Partial p v -> Constr
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)
$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)
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)
$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)
Data, Partial p v -> Partial p v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
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
$c== :: forall p v. (Eq p, Eq v) => Partial p v -> Partial p v -> Bool
Eq, 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
<$ :: forall a b. a -> Partial p b -> Partial p a
$c<$ :: forall p a b. a -> Partial p b -> Partial p a
fmap :: forall a b. (a -> b) -> Partial p a -> Partial p b
$cfmap :: forall p a b. (a -> b) -> Partial p a -> Partial p b
Functor, 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
$cto :: forall p v x. Rep (Partial p v) x -> Partial p v
$cfrom :: forall p v x. Partial p v -> Rep (Partial p v) x
Generic, 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
$cto1 :: forall p a. Rep1 (Partial p) a -> Partial p a
$cfrom1 :: forall p a. Partial p a -> Rep1 (Partial p) a
Generic1, forall a. Partial p a -> Bool
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 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
product :: forall a. Num a => Partial p a -> a
$cproduct :: forall p a. Num a => Partial p a -> a
sum :: forall a. Num a => Partial p a -> a
$csum :: forall p a. Num a => Partial p a -> a
minimum :: forall a. Ord a => Partial p a -> a
$cminimum :: forall p a. Ord a => Partial p a -> a
maximum :: forall a. Ord a => Partial p a -> a
$cmaximum :: forall p a. Ord a => Partial p a -> a
elem :: forall a. Eq a => a -> Partial p a -> Bool
$celem :: forall p a. Eq a => a -> Partial p a -> Bool
length :: forall a. Partial p a -> Int
$clength :: forall p a. Partial p a -> Int
null :: forall a. Partial p a -> Bool
$cnull :: forall p a. Partial p a -> Bool
toList :: forall a. Partial p a -> [a]
$ctoList :: forall p a. Partial p a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Partial p a -> a
$cfoldl1 :: forall p a. (a -> a -> a) -> Partial p a -> a
foldr1 :: forall a. (a -> a -> a) -> Partial p a -> a
$cfoldr1 :: forall p a. (a -> a -> a) -> Partial p a -> a
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
$cfoldl :: forall p b a. (b -> a -> 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
$cfoldr :: forall p a b. (a -> b -> b) -> b -> Partial p a -> b
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
$cfoldMap :: forall p m a. Monoid m => (a -> m) -> Partial p a -> m
fold :: forall m. Monoid m => Partial p m -> m
$cfold :: forall p m. Monoid m => Partial p m -> m
Foldable, 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 (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Partial p a -> f (Partial p b)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
Partial p (m a) -> m (Partial p a)
$csequence :: forall p (m :: Type -> Type) a.
Monad m =>
Partial p (m a) -> m (Partial p a)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Partial p a -> m (Partial p b)
$cmapM :: forall p (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Partial p a -> m (Partial p b)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Partial p (f a) -> f (Partial p a)
$csequenceA :: forall p (f :: Type -> Type) a.
Applicative f =>
Partial p (f a) -> f (Partial p a)
traverse :: 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)
Traversable, Partial p v -> Partial p v -> Bool
Partial p v -> Partial p v -> Ordering
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
min :: 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
max :: Partial p v -> Partial p v -> Partial p v
$cmax :: forall p v.
(Ord p, Ord v) =>
Partial p v -> Partial p v -> Partial p v
>= :: 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
$c< :: forall p v. (Ord p, Ord v) => Partial p v -> Partial p v -> Bool
compare :: Partial p v -> Partial p v -> Ordering
$ccompare :: forall p v.
(Ord p, Ord v) =>
Partial p v -> Partial p v -> Ordering
Ord, Int -> Partial p v -> ShowS
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
showList :: [Partial p v] -> ShowS
$cshowList :: forall p v. (Show p, Show v) => [Partial p v] -> ShowS
show :: Partial p v -> String
$cshow :: forall p v. (Show p, Show v) => Partial p v -> String
showsPrec :: Int -> Partial p v -> ShowS
$cshowsPrec :: forall p v. (Show p, Show v) => Int -> 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 = forall p v. p -> v -> Partial p v
Partial (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 (PartialWithErr e p v -> DataType
PartialWithErr e p v -> Constr
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 {e} {p} {v}.
(Data e, Data p, Data v) =>
Typeable (PartialWithErr e p v)
forall e p v.
(Data e, Data p, Data v) =>
PartialWithErr e p v -> DataType
forall e p v.
(Data e, Data p, Data v) =>
PartialWithErr e p v -> Constr
forall e p v.
(Data e, Data p, Data v) =>
(forall b. Data b => b -> b)
-> PartialWithErr e p v -> PartialWithErr e p v
forall e p v u.
(Data e, Data p, Data v) =>
Int -> (forall d. Data d => d -> u) -> PartialWithErr e p v -> u
forall e p v u.
(Data e, Data p, Data v) =>
(forall d. Data d => d -> u) -> PartialWithErr e p v -> [u]
forall e p v r r'.
(Data e, Data p, Data v) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r
forall e p v r r'.
(Data e, Data p, Data v) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r
forall e p v (m :: Type -> Type).
(Data e, Data p, Data v, 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 e, Data p, Data v, 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 e, Data p, Data v) =>
(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 e, Data p, Data v) =>
(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 e, Data p, Data v, 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 e, Data p, Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (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)
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)
gmapMo :: 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 e, Data p, Data v, 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)
$cgmapMp :: forall e p v (m :: Type -> Type).
(Data e, Data p, Data v, MonadPlus 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)
$cgmapM :: forall e p v (m :: Type -> Type).
(Data e, Data p, Data v, Monad m) =>
(forall d. Data d => d -> m d)
-> PartialWithErr e p v -> m (PartialWithErr e p v)
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> PartialWithErr e p v -> u
$cgmapQi :: forall e p v u.
(Data e, Data p, Data v) =>
Int -> (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]
$cgmapQ :: forall e p v u.
(Data e, Data p, Data v) =>
(forall d. Data d => d -> u) -> PartialWithErr e p v -> [u]
gmapQr :: 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 e, Data p, Data v) =>
(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
$cgmapQl :: forall e p v r r'.
(Data e, Data p, Data v) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PartialWithErr e p v -> r
gmapT :: (forall b. Data b => b -> b)
-> PartialWithErr e p v -> PartialWithErr e p v
$cgmapT :: forall e p v.
(Data e, Data p, Data v) =>
(forall b. Data b => b -> b)
-> PartialWithErr e p v -> 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))
$cdataCast2 :: forall e p v (t :: Type -> Type -> Type) (c :: Type -> Type).
(Data e, Data p, Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> 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))
$cdataCast1 :: forall e p v (t :: Type -> Type) (c :: Type -> Type).
(Data e, Data p, Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PartialWithErr e p v))
dataTypeOf :: PartialWithErr e p v -> DataType
$cdataTypeOf :: forall e p v.
(Data e, Data p, Data v) =>
PartialWithErr e p v -> DataType
toConstr :: PartialWithErr e p v -> Constr
$ctoConstr :: forall e p v.
(Data e, Data p, Data v) =>
PartialWithErr e p v -> Constr
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)
$cgunfold :: forall e p v (c :: Type -> Type).
(Data e, Data p, Data v) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> 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)
$cgfoldl :: forall e p v (c :: Type -> Type).
(Data e, Data p, Data v) =>
(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)
Data, PartialWithErr e p v -> PartialWithErr e p v -> Bool
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
/= :: 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
Eq, 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
<$ :: forall a b. a -> PartialWithErr e p b -> PartialWithErr e p a
$c<$ :: forall e p a b. a -> PartialWithErr e p b -> PartialWithErr e p a
fmap :: forall a b.
(a -> b) -> PartialWithErr e p a -> PartialWithErr e p b
$cfmap :: forall e p a b.
(a -> b) -> PartialWithErr e p a -> PartialWithErr e p b
Functor, 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
$cto :: forall e p v x.
Rep (PartialWithErr e p v) x -> PartialWithErr e p v
$cfrom :: forall e p v x.
PartialWithErr e p v -> Rep (PartialWithErr e p v) x
Generic, 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
$cto1 :: forall e p a. Rep1 (PartialWithErr e p) a -> PartialWithErr e p a
$cfrom1 :: forall e p a. PartialWithErr e p a -> Rep1 (PartialWithErr e p) a
Generic1, forall a. PartialWithErr e p a -> Bool
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 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
product :: forall a. Num a => PartialWithErr e p a -> a
$cproduct :: forall e p a. Num a => PartialWithErr e p a -> a
sum :: forall a. Num a => PartialWithErr e p a -> a
$csum :: forall e p a. Num a => PartialWithErr e p a -> a
minimum :: forall a. Ord a => PartialWithErr e p a -> a
$cminimum :: forall e p a. Ord a => PartialWithErr e p a -> a
maximum :: forall a. Ord a => PartialWithErr e p a -> a
$cmaximum :: forall e p a. Ord a => PartialWithErr e p a -> a
elem :: forall a. Eq a => a -> PartialWithErr e p a -> Bool
$celem :: forall e p a. Eq a => a -> PartialWithErr e p a -> Bool
length :: forall a. PartialWithErr e p a -> Int
$clength :: forall e p a. PartialWithErr e p a -> Int
null :: forall a. PartialWithErr e p a -> Bool
$cnull :: forall e p a. PartialWithErr e p a -> Bool
toList :: forall a. PartialWithErr e p a -> [a]
$ctoList :: forall e p a. PartialWithErr e p a -> [a]
foldl1 :: forall a. (a -> a -> a) -> PartialWithErr e p a -> a
$cfoldl1 :: forall e p a. (a -> a -> a) -> PartialWithErr e p a -> a
foldr1 :: forall a. (a -> a -> a) -> PartialWithErr e p a -> a
$cfoldr1 :: forall e p a. (a -> a -> a) -> PartialWithErr e p a -> a
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
$cfoldl :: forall e p b a. (b -> a -> 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
$cfoldr :: forall e p a b. (a -> b -> b) -> b -> PartialWithErr e p a -> b
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
$cfoldMap :: forall e p m a. Monoid m => (a -> m) -> PartialWithErr e p a -> m
fold :: forall m. Monoid m => PartialWithErr e p m -> m
$cfold :: forall e p m. Monoid m => PartialWithErr e p m -> m
Foldable, 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 (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> PartialWithErr e p a -> f (PartialWithErr e p b)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
PartialWithErr e p (m a) -> m (PartialWithErr e p a)
$csequence :: forall e p (m :: Type -> Type) a.
Monad m =>
PartialWithErr e p (m a) -> m (PartialWithErr e p a)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> PartialWithErr e p a -> m (PartialWithErr e p b)
$cmapM :: forall e p (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> PartialWithErr e p a -> m (PartialWithErr e p b)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
PartialWithErr e p (f a) -> f (PartialWithErr e p a)
$csequenceA :: forall e p (f :: Type -> Type) a.
Applicative f =>
PartialWithErr e p (f a) -> f (PartialWithErr e p a)
traverse :: 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)
Traversable, PartialWithErr e p v -> PartialWithErr e p v -> Bool
PartialWithErr e p v -> PartialWithErr e p v -> Ordering
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
min :: 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
max :: PartialWithErr e p v
-> PartialWithErr e p v -> PartialWithErr e p v
$cmax :: forall e p v.
(Ord p, Ord v, Ord e) =>
PartialWithErr e p v
-> PartialWithErr e p v -> PartialWithErr e p v
>= :: 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
$c< :: forall e p v.
(Ord p, Ord v, Ord e) =>
PartialWithErr e p v -> PartialWithErr e p v -> Bool
compare :: PartialWithErr e p v -> PartialWithErr e p v -> Ordering
$ccompare :: forall e p v.
(Ord p, Ord v, Ord e) =>
PartialWithErr e p v -> PartialWithErr e p v -> Ordering
Ord, Int -> PartialWithErr e p v -> ShowS
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
showList :: [PartialWithErr e p v] -> ShowS
$cshowList :: forall e p v.
(Show p, Show v, Show e) =>
[PartialWithErr e p v] -> ShowS
show :: PartialWithErr e p v -> String
$cshow :: forall e p v.
(Show p, Show v, Show e) =>
PartialWithErr e p v -> String
showsPrec :: Int -> PartialWithErr e p v -> ShowS
$cshowsPrec :: forall e p v.
(Show p, Show v, Show e) =>
Int -> 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 $bUnassigned :: forall p v. PartExpr p v
$mUnassigned :: forall {r} {p} {v}.
PartExpr p v -> ((# #) -> r) -> ((# #) -> r) -> r
Unassigned = Err ()

pattern PE :: p -> v -> PartExpr p v
pattern $bPE :: forall p v. p -> v -> PartExpr p v
$mPE :: forall {r} {p} {v}.
PartExpr p v -> (p -> v -> r) -> ((# #) -> r) -> r
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 forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred p BaseBoolType
p of
    Just Bool
False -> forall p v. PartExpr p v
Unassigned
    Maybe Bool
_ -> 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 = forall e p v. Partial p v -> PartialWithErr e p v
NoErr forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall p v. PartExpr p v
Unassigned
maybePartExpr sym
sym (Just a
r) = 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 = 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 =
     forall (m :: Type -> Type) a. Monad m => a -> m a
return 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 <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
px Pred sym
c
        forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! 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 <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
py forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
c)
        forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! 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 <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (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)
       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 [] = forall (m :: Type -> Type) a. Monad m => a -> m a
return 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
       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 = 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 = forall sym (m :: Type -> Type) a.
(sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
PartialT forall a b. (a -> b) -> a -> b
$ \sym
sym Pred sym
p -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap PartExpr (Pred sym) a -> PartExpr (Pred sym) b
resolve (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 = forall p v. PartExpr p v
Unassigned
          resolve (PE Pred sym
q a
x) = 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 = forall sym (m :: Type -> Type) a.
(sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
PartialT forall a b. (a -> b) -> a -> b
$ \sym
_ Pred sym
p -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! 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 forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a -> b
f -> PartialT sym m a
mx forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x -> 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 = 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 =
    forall sym (m :: Type -> Type) a.
(sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
PartialT forall a b. (a -> b) -> a -> b
$ \sym
sym Pred sym
p -> do
      PartExpr (Pred sym) a
pr <- 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 -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall p v. PartExpr p v
Unassigned
        PE Pred sym
q a
r -> 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 = forall sym (m :: Type -> Type) a.
(sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
PartialT forall a b. (a -> b) -> a -> b
$ \sym
_ Pred sym
_ -> 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 = forall sym (m :: Type -> Type) a.
(sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
PartialT forall a b. (a -> b) -> a -> b
$ \sym
_ Pred sym
p -> forall p v. p -> v -> PartExpr p v
PE Pred sym
p 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 = forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall sym (m :: Type -> Type) a.
(sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
PartialT forall a b. (a -> b) -> a -> b
$ \sym
_ Pred sym
_ -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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  = forall (m :: Type -> Type) sym a. Applicative m => PartialT sym m a
returnUnassigned
returnMaybe (Just a
a) = forall sym (m :: Type -> Type) a.
(sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
PartialT forall a b. (a -> b) -> a -> b
$ \sym
_ Pred sym
p -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (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 = forall (m :: Type -> Type) sym a. Applicative m => PartialT sym m a
returnUnassigned
returnPartial (PE SymExpr sym BaseBoolType
q a
a) = forall sym (m :: Type -> Type) a.
(sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
PartialT forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym BaseBoolType
p -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall (p :: BaseType -> Type) a.
IsExpr p =>
p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
mkPE forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym SymExpr sym BaseBoolType
p SymExpr sym BaseBoolType
q forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> 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 = forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m) =>
PartExpr (Pred sym) a -> PartialT sym m a
returnPartial (forall (p :: BaseType -> Type) a.
IsExpr p =>
p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
mkPE Pred sym
q ())