grisette-0.11.0.0: Symbolic evaluation as a library

Copyright	(c) Sirui Lu 2021-2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Safe-Inferred
Language	Haskell2010

Grisette.Internal.Core.Data.UnionBase

Contents

The union data structure.

Description

Synopsis

data UnionBase a where
- UnionSingle :: forall a. a -> UnionBase a
- UnionIf :: forall a. a -> !Bool -> !SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithLeftMost :: Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
ifWithStrategy :: MergingStrategy a -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a
fullReconstruct :: MergingStrategy a -> UnionBase a -> UnionBase a

The union data structure.

Please consider using Union instead.

data UnionBase a where Source #

The base union implementation, which is an if-then-else tree structure.

Constructors

UnionSingle :: forall a. a -> UnionBase a	A single value
UnionIf	A if value
Fields :: forall a. a Cached leftmost value -> !Bool Is merged invariant already maintained? -> !SymBool If condition -> UnionBase a True branch -> UnionBase a False branch -> UnionBase a

Instances

Instances details

Eq1 UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

liftEq :: (a -> b -> Bool) -> UnionBase a -> UnionBase b -> Bool #

Show1 UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> UnionBase a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [UnionBase a] -> ShowS #

NFData1 UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

liftRnf :: (a -> ()) -> UnionBase a -> () #

Applicative UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

pure :: a -> UnionBase a #

(<*>) :: UnionBase (a -> b) -> UnionBase a -> UnionBase b #

liftA2 :: (a -> b -> c) -> UnionBase a -> UnionBase b -> UnionBase c #

(*>) :: UnionBase a -> UnionBase b -> UnionBase b #

(<*) :: UnionBase a -> UnionBase b -> UnionBase a #

Functor UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

fmap :: (a -> b) -> UnionBase a -> UnionBase b #

(<$) :: a -> UnionBase b -> UnionBase a #

Monad UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

(>>=) :: UnionBase a -> (a -> UnionBase b) -> UnionBase b #

(>>) :: UnionBase a -> UnionBase b -> UnionBase b #

return :: a -> UnionBase a #

PlainUnion UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

singleView :: UnionBase a -> Maybe a Source #

ifView :: UnionBase a -> Maybe (SymBool, UnionBase a, UnionBase a) Source #

toGuardedList :: UnionBase a -> [(SymBool, a)] Source #

overestimateUnionValues :: Mergeable a => UnionBase a -> [a] Source #

Mergeable1 UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

liftRootStrategy :: MergingStrategy a -> MergingStrategy (UnionBase a) Source #

PPrint1 UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

liftPFormatPrec :: (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> Int -> UnionBase a -> Doc ann Source #

liftPFormatList :: (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> [UnionBase a] -> Doc ann Source #

SimpleMergeable1 UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a Source #

SymBranching UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

mrgIfWithStrategy :: MergingStrategy a -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a Source #

mrgIfPropagatedStrategy :: SymBool -> UnionBase a -> UnionBase a -> UnionBase a Source #

TryMerge UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

tryMergeWithStrategy :: MergingStrategy a -> UnionBase a -> UnionBase a Source #

AllSyms1 UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> UnionBase a -> [SomeSym] -> [SomeSym] Source #

Hashable1 UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

liftHashWithSalt :: (Int -> a -> Int) -> Int -> UnionBase a -> Int #

Generic1 UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Associated Types

type Rep1 UnionBase

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

type Rep1 UnionBase = D1 ('MetaData "UnionBase" "Grisette.Internal.Internal.Decl.Core.Data.UnionBase" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "UnionSingle" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1) :+: C1 ('MetaCons "UnionIf" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1 :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SymBool) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 UnionBase) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 UnionBase)))))

Methods

from1 :: UnionBase a -> Rep1 UnionBase a #

to1 :: Rep1 UnionBase a -> UnionBase a #

Lift a => Lift (UnionBase a :: Type) Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

lift :: Quote m => UnionBase a -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => UnionBase a -> Code m (UnionBase a) #

(Mergeable a, Serial a) => Binary (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

put :: UnionBase a -> Put #

get :: Get (UnionBase a) #

putList :: [UnionBase a] -> Put #

(Mergeable a, Serial a) => Serial (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

serialize :: MonadPut m => UnionBase a -> m () #

deserialize :: MonadGet m => m (UnionBase a) #

(Mergeable a, Serial a) => Serialize (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

put :: Putter (UnionBase a) #

get :: Get (UnionBase a) #

NFData a => NFData (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

rnf :: UnionBase a -> () #

Generic (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Associated Types

type Rep (UnionBase a)

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

type Rep (UnionBase a) = D1 ('MetaData "UnionBase" "Grisette.Internal.Internal.Decl.Core.Data.UnionBase" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "UnionSingle" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "UnionIf" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SymBool) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (UnionBase a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (UnionBase a))))))

Methods

from :: UnionBase a -> Rep (UnionBase a) x #

to :: Rep (UnionBase a) x -> UnionBase a #

Show a => Show (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

showsPrec :: Int -> UnionBase a -> ShowS #

show :: UnionBase a -> String #

showList :: [UnionBase a] -> ShowS #

Eq a => Eq (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

(==) :: UnionBase a -> UnionBase a -> Bool #

(/=) :: UnionBase a -> UnionBase a -> Bool #

Mergeable a => Mergeable (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

rootStrategy :: MergingStrategy (UnionBase a) Source #

sortIndices :: UnionBase a -> [DynamicSortedIdx] Source #

PPrint a => PPrint (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

pformat :: UnionBase a -> Doc ann Source #

pformatPrec :: Int -> UnionBase a -> Doc ann Source #

pformatList :: [UnionBase a] -> Doc ann Source #

Mergeable a => SimpleMergeable (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

Methods

mrgIte :: SymBool -> UnionBase a -> UnionBase a -> UnionBase a Source #

AllSyms a => AllSyms (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

allSymsS :: UnionBase a -> [SomeSym] -> [SomeSym] Source #

allSyms :: UnionBase a -> [SomeSym] Source #

Hashable a => Hashable (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase

Methods

hashWithSalt :: Int -> UnionBase a -> Int #

hash :: UnionBase a -> Int #

type Rep1 UnionBase Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

type Rep1 UnionBase = D1 ('MetaData "UnionBase" "Grisette.Internal.Internal.Decl.Core.Data.UnionBase" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "UnionSingle" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1) :+: C1 ('MetaCons "UnionIf" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1 :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SymBool) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 UnionBase) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 UnionBase)))))

type Rep (UnionBase a) Source #

Instance details

Defined in Grisette.Internal.Internal.Decl.Core.Data.UnionBase

type Rep (UnionBase a) = D1 ('MetaData "UnionBase" "Grisette.Internal.Internal.Decl.Core.Data.UnionBase" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "UnionSingle" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "UnionIf" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SymBool) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (UnionBase a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (UnionBase a))))))

ifWithLeftMost :: Bool -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a Source #

Build UnionIf with leftmost cache correctly maintained.

Usually you should never directly try to build a UnionIf with its constructor.

ifWithStrategy :: MergingStrategy a -> SymBool -> UnionBase a -> UnionBase a -> UnionBase a Source #

Use a specific strategy to build a UnionIf value.

The merged invariant will be maintained in the result.

fullReconstruct :: MergingStrategy a -> UnionBase a -> UnionBase a Source #

Fully reconstruct a Union to maintain the merged invariant.