grisette-0.1.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Union

Description

 
Synopsis

The union data structure.

Please consider using UnionM instead.

data Union a Source #

The default union implementation.

Constructors

Single a

A single value

If

A if value

Fields

  • a

    Cached leftmost value

  • !Bool

    Is merged invariant already maintained?

  • !SymBool

    If condition

  • (Union a)

    True branch

  • (Union a)

    False branch

Instances

Instances details
Eq1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

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

Show1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

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

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

NFData1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

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

Mergeable1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

SimpleMergeable1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

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

UnionLike Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

UnionPrjOp Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Lift a => Lift (Union a :: Type) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

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

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

Generic (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Associated Types

type Rep (Union a) :: Type -> Type #

Methods

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

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

Show a => Show (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

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

show :: Union a -> String #

showList :: [Union a] -> ShowS #

NFData a => NFData (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

rnf :: Union a -> () #

Eq a => Eq (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

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

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

Mergeable a => Mergeable (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Mergeable a => SimpleMergeable (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

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

Hashable a => Hashable (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

hashWithSalt :: Int -> Union a -> Int #

hash :: Union a -> Int #

Generic1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Associated Types

type Rep1 Union :: k -> Type #

Methods

from1 :: forall (a :: k). Union a -> Rep1 Union a #

to1 :: forall (a :: k). Rep1 Union a -> Union a #

type Rep (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

type Rep1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

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

Build If with leftmost cache correctly maintained.

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

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

Use a specific strategy to build a If value.

The merged invariant will be maintained in the result.

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

Fully reconstruct a Union to maintain the merged invariant.