{-# 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 ())