Data.Expression

Usage:

You can build expressions in predefined languages (QFLogic, QFLia, QFALia, Lia, ALia) using the smart constructors such as var, and, or, not, forall, exists (or operators .&., .|., .->., .<-., .<->.) or you can define your own sorted language as a fixpoint (IFix) of a sum (:+:) of indexed functors (IFunctor).

Documentation

module Data.Expression.Arithmetic

module Data.Expression.Array

module Data.Expression.Equality

module Data.Expression.IfThenElse

module Data.Expression.Parser

data family Sing (a :: k) :: *

The singleton kind-indexed data family.

Instances

data Sing (z :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Bool) where

• SFalse :: Sing False
• STrue :: Sing True

data Sing (z :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Ordering) where

• SLT :: Sing LT
• SEQ :: Sing EQ
• SGT :: Sing GT

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: Sing n

data Sing (z :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: ()) where

• STuple0 :: Sing ()

data Sing (z :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Void)

data Sing (z :: Sort)

Defined in Data.Expression.Sort

data Sing (z :: Sort) where

• SBooleanSort :: Sing BooleanSort
• SIntegralSort :: Sing IntegralSort
• SArraySort :: Sing (ArraySort n n)

data Sing (z :: [a])

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: [a]) where

• SNil :: Sing ([] :: [a])
• SCons :: Sing (n1 ': n2)

data Sing (z :: Maybe a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Maybe a) where

• SNothing :: Sing (Nothing :: Maybe a)
• SJust :: Sing (Just n)

data Sing (z :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: NonEmpty a) where

• (:%|) :: Sing (n1 :| n2)

data Sing (z :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Either a b) where

• SLeft :: Sing (Left n :: Either a b)
• SRight :: Sing (Right n :: Either a b)

data Sing (z :: (a, b))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b)) where

• STuple2 :: Sing ((,) n1 n2)

data Sing (f :: k1 ~> k2)

Defined in Data.Singletons.Internal

data Sing (f :: k1 ~> k2) = SLambda {

• applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)

}

data Sing (z :: (a, b, c))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c)) where

• STuple3 :: Sing ((,,) n1 n2 n3)

data Sing (z :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d)) where

• STuple4 :: Sing ((,,,) n1 n2 n3 n4)

data Sing (z :: (a, b, c, d, e))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e)) where

• STuple5 :: Sing ((,,,,) n1 n2 n3 n4 n5)

data Sing (z :: (a, b, c, d, e, f))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e, f)) where

• STuple6 :: Sing ((,,,,,) n1 n2 n3 n4 n5 n6)

data Sing (z :: (a, b, c, d, e, f, g))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e, f, g)) where

• STuple7 :: Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

data Sort

A universe of recognized sorts

Constructors

BooleanSort

booleans (true, false)

IntegralSort

integers (..., -1, 0, 1, ...)

ArraySort Sort Sort

arrays indexed by index sort, containing elements of element sort

Instances

Eq Sort

Defined in Data.Expression.Sort

Methods

(==) :: Sort -> Sort -> Bool

(/=) :: Sort -> Sort -> Bool

Show Sort

Defined in Data.Expression.Sort

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

SDecide Sort => SDecide Sort

Defined in Data.Expression.Sort

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SingKind Sort

Defined in Data.Expression.Sort

Associated Types

type Demote Sort = (r :: *)

Methods

fromSing :: Sing a -> Demote Sort

toSing :: Demote Sort -> SomeSing Sort

SingI BooleanSort

Defined in Data.Expression.Sort

Methods

sing :: Sing BooleanSort

SingI IntegralSort

Defined in Data.Expression.Sort

Methods

sing :: Sing IntegralSort

IEq1 IfThenElseF

Defined in Data.Expression.IfThenElse

Methods

ieq1 :: IEq a => IfThenElseF a j -> IfThenElseF a j -> Bool

IEq1 ArrayF

Defined in Data.Expression.Array

Methods

ieq1 :: IEq a => ArrayF a j -> ArrayF a j -> Bool

IEq1 ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

ieq1 :: IEq a => ArithmeticF a j -> ArithmeticF a j -> Bool

IEq1 NegationF

Defined in Data.Expression

Methods

ieq1 :: IEq a => NegationF a j -> NegationF a j -> Bool

IEq1 DisjunctionF

Defined in Data.Expression

Methods

ieq1 :: IEq a => DisjunctionF a j -> DisjunctionF a j -> Bool

IEq1 ConjunctionF

Defined in Data.Expression

Methods

ieq1 :: IEq a => ConjunctionF a j -> ConjunctionF a j -> Bool

IFoldable IfThenElseF

Defined in Data.Expression.IfThenElse

Methods

ifold :: Monoid m => IfThenElseF (Const m) i' -> Const m i'

IFoldable ArrayF

Defined in Data.Expression.Array

Methods

ifold :: Monoid m => ArrayF (Const m) i' -> Const m i'

IFoldable ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

ifold :: Monoid m => ArithmeticF (Const m) i' -> Const m i'

IFoldable NegationF

Defined in Data.Expression

Methods

ifold :: Monoid m => NegationF (Const m) i' -> Const m i'

IFoldable DisjunctionF

Defined in Data.Expression

Methods

ifold :: Monoid m => DisjunctionF (Const m) i' -> Const m i'

IFoldable ConjunctionF

Defined in Data.Expression

Methods

ifold :: Monoid m => ConjunctionF (Const m) i' -> Const m i'

IFunctor IfThenElseF

Defined in Data.Expression.IfThenElse

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). IfThenElseF a i' -> IfThenElseF b i'

index :: IfThenElseF a i' -> Sing i'

IFunctor ArrayF

Defined in Data.Expression.Array

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ArrayF a i' -> ArrayF b i'

index :: ArrayF a i' -> Sing i'

IFunctor ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ArithmeticF a i' -> ArithmeticF b i'

index :: ArithmeticF a i' -> Sing i'

IFunctor NegationF

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). NegationF a i' -> NegationF b i'

index :: NegationF a i' -> Sing i'

IFunctor DisjunctionF

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). DisjunctionF a i' -> DisjunctionF b i'

index :: DisjunctionF a i' -> Sing i'

IFunctor ConjunctionF

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ConjunctionF a i' -> ConjunctionF b i'

index :: ConjunctionF a i' -> Sing i'

ITraversable IfThenElseF

Defined in Data.Expression.IfThenElse

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). IfThenElseF a i' -> f (IfThenElseF b i')

ITraversable ArrayF

Defined in Data.Expression.Array

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ArrayF a i' -> f (ArrayF b i')

ITraversable ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ArithmeticF a i' -> f (ArithmeticF b i')

ITraversable NegationF

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). NegationF a i' -> f (NegationF b i')

ITraversable DisjunctionF

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). DisjunctionF a i' -> f (DisjunctionF b i')

ITraversable ConjunctionF

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ConjunctionF a i' -> f (ConjunctionF b i')

IShow IfThenElseF

Defined in Data.Expression.IfThenElse

Methods

ishow :: IfThenElseF (Const String) i -> Const String i

IShow ArrayF

Defined in Data.Expression.Array

Methods

ishow :: ArrayF (Const String) i -> Const String i

IShow ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

ishow :: ArithmeticF (Const String) i -> Const String i

IShow NegationF

Defined in Data.Expression

Methods

ishow :: NegationF (Const String) i -> Const String i

IShow DisjunctionF

Defined in Data.Expression

Methods

ishow :: DisjunctionF (Const String) i -> Const String i

IShow ConjunctionF

Defined in Data.Expression

Methods

ishow :: ConjunctionF (Const String) i -> Const String i

IShow (EqualityF :: (k -> *) -> Sort -> *)

Defined in Data.Expression.Equality

Methods

ishow :: EqualityF (Const String) i -> Const String i

IShow (VarF :: (k -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ishow :: VarF (Const String) i -> Const String i

IShow (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ishow :: ExistentialF v (Const String) i -> Const String i

IShow (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ishow :: UniversalF v (Const String) i -> Const String i

IEq1 (EqualityF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression.Equality

Methods

ieq1 :: IEq a => EqualityF a j -> EqualityF a j -> Bool

IEq1 (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ieq1 :: IEq a => ExistentialF v a j -> ExistentialF v a j -> Bool

IEq1 (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ieq1 :: IEq a => UniversalF v a j -> UniversalF v a j -> Bool

IEq1 (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ieq1 :: IEq a => VarF a j -> VarF a j -> Bool

IFoldable (EqualityF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression.Equality

Methods

ifold :: Monoid m => EqualityF (Const m) i' -> Const m i'

IFoldable (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ifold :: Monoid m => ExistentialF v (Const m) i' -> Const m i'

IFoldable (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ifold :: Monoid m => UniversalF v (Const m) i' -> Const m i'

IFoldable (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ifold :: Monoid m => VarF (Const m) i' -> Const m i'

IFunctor (EqualityF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression.Equality

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). EqualityF a i' -> EqualityF b i'

index :: EqualityF a i' -> Sing i'

IFunctor (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ExistentialF v a i' -> ExistentialF v b i'

index :: ExistentialF v a i' -> Sing i'

IFunctor (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). UniversalF v a i' -> UniversalF v b i'

index :: UniversalF v a i' -> Sing i'

IFunctor (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). VarF a i' -> VarF b i'

index :: VarF a i' -> Sing i'

ITraversable (EqualityF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression.Equality

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). EqualityF a i' -> f (EqualityF b i')

ITraversable (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ExistentialF v a i' -> f (ExistentialF v b i')

ITraversable (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). UniversalF v a i' -> f (UniversalF v b i')

ITraversable (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). VarF a i' -> f (VarF b i')

MaybeQuantified (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g => ExistentialF v (IFix g) s -> Const Any s

freevars' :: ExistentialF v (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

MaybeQuantified (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g => UniversalF v (IFix g) s -> Const Any s

freevars' :: UniversalF v (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

MaybeQuantified (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g => VarF (IFix g) s -> Const Any s

freevars' :: VarF (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

(SingI n1, SingI n2) => SingI (ArraySort n1 n2 :: Sort)

Defined in Data.Expression.Sort

Methods

sing :: Sing (ArraySort n1 n2)

JoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

JoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

JoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

JoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

JoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

MeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

MeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

MeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

MeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

MeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

meet :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

Lattice (ALia BooleanSort)

Defined in Data.Expression

Lattice (QFALia BooleanSort)

Defined in Data.Expression

Lattice (Lia BooleanSort)

Defined in Data.Expression

Lattice (QFLia BooleanSort)

Defined in Data.Expression

Lattice (QFLogic BooleanSort)

Defined in Data.Expression

BoundedJoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort

BoundedJoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLia BooleanSort

BoundedJoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLogic BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

top :: QFALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

top :: Lia BooleanSort

BoundedMeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

top :: QFLia BooleanSort

BoundedMeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

top :: QFLogic BooleanSort

BoundedLattice (ALia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFALia BooleanSort)

Defined in Data.Expression

BoundedLattice (Lia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLogic BooleanSort)

Defined in Data.Expression

ComplementedLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

complement :: ALia BooleanSort -> ALia BooleanSort

ComplementedLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFALia BooleanSort -> QFALia BooleanSort

ComplementedLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

complement :: Lia BooleanSort -> Lia BooleanSort

ComplementedLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLia BooleanSort -> QFLia BooleanSort

ComplementedLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLogic BooleanSort -> QFLogic BooleanSort

IfThenElseF :<: f => Parseable IfThenElseF f

Defined in Data.Expression.IfThenElse

Methods

parser :: Proxy IfThenElseF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

ArrayF :<: f => Parseable ArrayF f

Defined in Data.Expression.Array

Methods

parser :: Proxy ArrayF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

ArithmeticF :<: f => Parseable ArithmeticF f

Defined in Data.Expression.Arithmetic

Methods

parser :: Proxy ArithmeticF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

NegationF :<: f => Parseable NegationF f

Defined in Data.Expression

Methods

parser :: Proxy NegationF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

DisjunctionF :<: f => Parseable DisjunctionF f

Defined in Data.Expression

Methods

parser :: Proxy DisjunctionF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

ConjunctionF :<: f => Parseable ConjunctionF f

Defined in Data.Expression

Methods

parser :: Proxy ConjunctionF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

(EqualityF :: (Sort -> *) -> Sort -> *) :<: f => Parseable (EqualityF :: (k -> *) -> Sort -> *) f

Defined in Data.Expression.Equality

Methods

parser :: Proxy EqualityF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

(ExistentialF v :<: f, SingI v) => Parseable (ExistentialF v :: (Sort -> *) -> Sort -> *) f

Defined in Data.Expression

Methods

parser :: Proxy (ExistentialF v) -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

(UniversalF v :<: f, SingI v) => Parseable (UniversalF v :: (Sort -> *) -> Sort -> *) f

Defined in Data.Expression

Methods

parser :: Proxy (UniversalF v) -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

(VarF :: (Sort -> *) -> Sort -> *) :<: f => Parseable (VarF :: k -> Sort -> *) f

Defined in Data.Expression

Methods

parser :: Proxy VarF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

data Sing (z :: Sort)

Defined in Data.Expression.Sort

data Sing (z :: Sort) where

• SBooleanSort :: Sing BooleanSort
• SIntegralSort :: Sing IntegralSort
• SArraySort :: Sing (ArraySort n n)

type Demote Sort

Defined in Data.Expression.Sort

type Demote Sort = Sort

data DynamicallySorted (f :: (Sort -> *) -> Sort -> *) where

An expression of some sort (obtained for example during parsing)

Constructors

DynamicallySorted :: forall (s :: Sort) f. Sing s -> IFix f s -> DynamicallySorted f

Instances

IEq1 f => Eq (DynamicallySorted f)

Defined in Data.Expression.Sort

Methods

(==) :: DynamicallySorted f -> DynamicallySorted f -> Bool

(/=) :: DynamicallySorted f -> DynamicallySorted f -> Bool

(IFunctor f, IShow f) => Show (DynamicallySorted f)

Defined in Data.Expression.Sort

Methods

showsPrec :: Int -> DynamicallySorted f -> ShowS

show :: DynamicallySorted f -> String

showList :: [DynamicallySorted f] -> ShowS

data DynamicSort where

Some sort (obtained for example during parsing)

Constructors

DynamicSort :: forall (s :: Sort). Sing s -> DynamicSort

Instances

Eq DynamicSort

Defined in Data.Expression.Sort

Methods

(==) :: DynamicSort -> DynamicSort -> Bool

(/=) :: DynamicSort -> DynamicSort -> Bool

toStaticSort :: forall (s :: Sort). SingI s => DynamicSort -> Maybe (Sing s)

Tries to convert some sort (DynamicSort) to a requested sort.

toDynamicallySorted :: forall f (s :: Sort). SingI s => IFix f s -> DynamicallySorted f

Converts a statically sorted expression to a dynamically sorted one.

toStaticallySorted :: forall f (s :: Sort). SingI s => DynamicallySorted f -> Maybe (IFix f s)

Tries to convert an expression (DynamicallySorted) of some sort to an expression of requested sort. Performs no conversions.

parseSort :: Parser DynamicSort

Parser that accepts sort definitions such as bool, int, array int int, array int (array ...).

module Data.Expression.Utils.Indexed.Eq

module Data.Expression.Utils.Indexed.Foldable

module Data.Expression.Utils.Indexed.Functor

module Data.Expression.Utils.Indexed.Show

module Data.Expression.Utils.Indexed.Sum

module Data.Expression.Utils.Indexed.Traversable

type QFLogicF = EqualityF :+: (ConjunctionF :+: (DisjunctionF :+: (NegationF :+: VarF)))

A functor representing propositional logic embedded in first order logic (quantifier-free, boolean variables aka propositions, logical connectives and, or, not, equality of propositions)

type QFLiaF = ArithmeticF :+: (IfThenElseF :+: QFLogicF)

A functor representing the language of quantifier-free linear integer arithmetic theory in first order logic (integer constants, integer variables, addition, multiplication, divisibility, ordering)

type LiaF = ExistentialF BooleanSort :+: (ExistentialF IntegralSort :+: (UniversalF BooleanSort :+: (UniversalF IntegralSort :+: QFLiaF)))

A functor much like QFLiaF with quantifiers over booleans and integers

type QFALiaF = ArrayF :+: QFLiaF

A functor representing the language of quantifier-free linear integer arithmetic and array theories in first order logic (much like QFLiaF with additional array variables, select, and store)

type ALiaF = ExistentialF BooleanSort :+: (ExistentialF IntegralSort :+: (UniversalF BooleanSort :+: (UniversalF IntegralSort :+: QFALiaF)))

A functor much like QFALiaF with quantifiers over booleans and integers

type Var = IFix VarF

A language consisting solely of variables (useful for listing variables outside of any particular context, such as bound variables of quantified formula)

type QFLogic = IFix QFLogicF

A language obtained as fixpoint of QFLogicF

type QFLia = IFix QFLiaF

A language obtained as fixpoint of QFLiaF

type Lia = IFix LiaF

A language obtained as fixpoint of LiaF

type QFALia = IFix QFALiaF

A language obtained as fixpoint of QFALiaF

type ALia = IFix ALiaF

A language obtained as fixpoint of ALiaF

class BoundedLattice a => ComplementedLattice a where

Bounded lattices that support complementing elements

complement . complement = id

Minimal complete definition

complement

Methods

complement :: a -> a

Instances

ComplementedLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

complement :: ALia BooleanSort -> ALia BooleanSort

ComplementedLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFALia BooleanSort -> QFALia BooleanSort

ComplementedLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

complement :: Lia BooleanSort -> Lia BooleanSort

ComplementedLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLia BooleanSort -> QFLia BooleanSort

ComplementedLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLogic BooleanSort -> QFLogic BooleanSort

type VariableName = String

Type of names assigned to variables

data VarF a (s :: Sort) where

A functor representing a sorted variable, each variable is identified by its name and sort

Constructors

Var :: VariableName -> Sing s -> VarF a s

Instances

IShow (VarF :: (k -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ishow :: VarF (Const String) i -> Const String i

IEq1 (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ieq1 :: IEq a => VarF a j -> VarF a j -> Bool

IFoldable (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ifold :: Monoid m => VarF (Const m) i' -> Const m i'

IFunctor (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). VarF a i' -> VarF b i'

index :: VarF a i' -> Sing i'

ITraversable (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). VarF a i' -> f (VarF b i')

MaybeQuantified (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g => VarF (IFix g) s -> Const Any s

freevars' :: VarF (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

JoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

JoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

JoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

JoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

JoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

MeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

MeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

MeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

MeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

MeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

meet :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

Lattice (ALia BooleanSort)

Defined in Data.Expression

Lattice (QFALia BooleanSort)

Defined in Data.Expression

Lattice (Lia BooleanSort)

Defined in Data.Expression

Lattice (QFLia BooleanSort)

Defined in Data.Expression

Lattice (QFLogic BooleanSort)

Defined in Data.Expression

BoundedJoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort

BoundedJoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLia BooleanSort

BoundedJoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLogic BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

top :: QFALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

top :: Lia BooleanSort

BoundedMeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

top :: QFLia BooleanSort

BoundedMeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

top :: QFLogic BooleanSort

BoundedLattice (ALia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFALia BooleanSort)

Defined in Data.Expression

BoundedLattice (Lia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLogic BooleanSort)

Defined in Data.Expression

ComplementedLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

complement :: ALia BooleanSort -> ALia BooleanSort

ComplementedLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFALia BooleanSort -> QFALia BooleanSort

ComplementedLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

complement :: Lia BooleanSort -> Lia BooleanSort

ComplementedLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLia BooleanSort -> QFLia BooleanSort

ComplementedLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLogic BooleanSort -> QFLogic BooleanSort

(VarF :: (Sort -> *) -> Sort -> *) :<: f => Parseable (VarF :: k -> Sort -> *) f

Defined in Data.Expression

Methods

parser :: Proxy VarF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

data ConjunctionF a (s :: Sort) where

A functor representing a logical connective for conjunction

Constructors

And :: [a BooleanSort] -> ConjunctionF a BooleanSort

Instances

IEq1 ConjunctionF

Defined in Data.Expression

Methods

ieq1 :: IEq a => ConjunctionF a j -> ConjunctionF a j -> Bool

IFoldable ConjunctionF

Defined in Data.Expression

Methods

ifold :: Monoid m => ConjunctionF (Const m) i' -> Const m i'

IFunctor ConjunctionF

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ConjunctionF a i' -> ConjunctionF b i'

index :: ConjunctionF a i' -> Sing i'

ITraversable ConjunctionF

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ConjunctionF a i' -> f (ConjunctionF b i')

IShow ConjunctionF

Defined in Data.Expression

Methods

ishow :: ConjunctionF (Const String) i -> Const String i

JoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

JoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

JoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

JoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

JoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

MeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

MeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

MeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

MeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

MeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

meet :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

Lattice (ALia BooleanSort)

Defined in Data.Expression

Lattice (QFALia BooleanSort)

Defined in Data.Expression

Lattice (Lia BooleanSort)

Defined in Data.Expression

Lattice (QFLia BooleanSort)

Defined in Data.Expression

Lattice (QFLogic BooleanSort)

Defined in Data.Expression

BoundedJoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort

BoundedJoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLia BooleanSort

BoundedJoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLogic BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

top :: QFALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

top :: Lia BooleanSort

BoundedMeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

top :: QFLia BooleanSort

BoundedMeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

top :: QFLogic BooleanSort

BoundedLattice (ALia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFALia BooleanSort)

Defined in Data.Expression

BoundedLattice (Lia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLogic BooleanSort)

Defined in Data.Expression

ComplementedLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

complement :: ALia BooleanSort -> ALia BooleanSort

ComplementedLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFALia BooleanSort -> QFALia BooleanSort

ComplementedLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

complement :: Lia BooleanSort -> Lia BooleanSort

ComplementedLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLia BooleanSort -> QFLia BooleanSort

ComplementedLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLogic BooleanSort -> QFLogic BooleanSort

ConjunctionF :<: f => Parseable ConjunctionF f

Defined in Data.Expression

Methods

parser :: Proxy ConjunctionF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

data DisjunctionF a (s :: Sort) where

A functor representing a logical connective for disjunction

Constructors

Or :: [a BooleanSort] -> DisjunctionF a BooleanSort

Instances

IEq1 DisjunctionF

Defined in Data.Expression

Methods

ieq1 :: IEq a => DisjunctionF a j -> DisjunctionF a j -> Bool

IFoldable DisjunctionF

Defined in Data.Expression

Methods

ifold :: Monoid m => DisjunctionF (Const m) i' -> Const m i'

IFunctor DisjunctionF

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). DisjunctionF a i' -> DisjunctionF b i'

index :: DisjunctionF a i' -> Sing i'

ITraversable DisjunctionF

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). DisjunctionF a i' -> f (DisjunctionF b i')

IShow DisjunctionF

Defined in Data.Expression

Methods

ishow :: DisjunctionF (Const String) i -> Const String i

JoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

JoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

JoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

JoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

JoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

MeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

MeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

MeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

MeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

MeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

meet :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

Lattice (ALia BooleanSort)

Defined in Data.Expression

Lattice (QFALia BooleanSort)

Defined in Data.Expression

Lattice (Lia BooleanSort)

Defined in Data.Expression

Lattice (QFLia BooleanSort)

Defined in Data.Expression

Lattice (QFLogic BooleanSort)

Defined in Data.Expression

BoundedJoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort

BoundedJoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLia BooleanSort

BoundedJoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLogic BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

top :: QFALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

top :: Lia BooleanSort

BoundedMeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

top :: QFLia BooleanSort

BoundedMeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

top :: QFLogic BooleanSort

BoundedLattice (ALia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFALia BooleanSort)

Defined in Data.Expression

BoundedLattice (Lia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLogic BooleanSort)

Defined in Data.Expression

ComplementedLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

complement :: ALia BooleanSort -> ALia BooleanSort

ComplementedLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFALia BooleanSort -> QFALia BooleanSort

ComplementedLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

complement :: Lia BooleanSort -> Lia BooleanSort

ComplementedLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLia BooleanSort -> QFLia BooleanSort

ComplementedLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLogic BooleanSort -> QFLogic BooleanSort

DisjunctionF :<: f => Parseable DisjunctionF f

Defined in Data.Expression

Methods

parser :: Proxy DisjunctionF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

data NegationF a (s :: Sort) where

A functor representing a logical connective for negation

Constructors

Not :: a BooleanSort -> NegationF a BooleanSort

Instances

IEq1 NegationF

Defined in Data.Expression

Methods

ieq1 :: IEq a => NegationF a j -> NegationF a j -> Bool

IFoldable NegationF

Defined in Data.Expression

Methods

ifold :: Monoid m => NegationF (Const m) i' -> Const m i'

IFunctor NegationF

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). NegationF a i' -> NegationF b i'

index :: NegationF a i' -> Sing i'

ITraversable NegationF

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). NegationF a i' -> f (NegationF b i')

IShow NegationF

Defined in Data.Expression

Methods

ishow :: NegationF (Const String) i -> Const String i

JoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

JoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

JoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

JoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

JoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

MeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

MeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

MeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

MeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

MeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

meet :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

Lattice (ALia BooleanSort)

Defined in Data.Expression

Lattice (QFALia BooleanSort)

Defined in Data.Expression

Lattice (Lia BooleanSort)

Defined in Data.Expression

Lattice (QFLia BooleanSort)

Defined in Data.Expression

Lattice (QFLogic BooleanSort)

Defined in Data.Expression

BoundedJoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort

BoundedJoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLia BooleanSort

BoundedJoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLogic BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

top :: QFALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

top :: Lia BooleanSort

BoundedMeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

top :: QFLia BooleanSort

BoundedMeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

top :: QFLogic BooleanSort

BoundedLattice (ALia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFALia BooleanSort)

Defined in Data.Expression

BoundedLattice (Lia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLogic BooleanSort)

Defined in Data.Expression

ComplementedLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

complement :: ALia BooleanSort -> ALia BooleanSort

ComplementedLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFALia BooleanSort -> QFALia BooleanSort

ComplementedLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

complement :: Lia BooleanSort -> Lia BooleanSort

ComplementedLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLia BooleanSort -> QFLia BooleanSort

ComplementedLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLogic BooleanSort -> QFLogic BooleanSort

NegationF :<: f => Parseable NegationF f

Defined in Data.Expression

Methods

parser :: Proxy NegationF -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

data UniversalF (v :: Sort) a (s :: Sort) where

A functor representing a mono-sorted universal quantifier binding a number of variables within a formula

Constructors

Forall :: [Var v] -> a BooleanSort -> UniversalF v a BooleanSort

Instances

IShow (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ishow :: UniversalF v (Const String) i -> Const String i

IEq1 (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ieq1 :: IEq a => UniversalF v a j -> UniversalF v a j -> Bool

IFoldable (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ifold :: Monoid m => UniversalF v (Const m) i' -> Const m i'

IFunctor (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). UniversalF v a i' -> UniversalF v b i'

index :: UniversalF v a i' -> Sing i'

ITraversable (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). UniversalF v a i' -> f (UniversalF v b i')

MaybeQuantified (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g => UniversalF v (IFix g) s -> Const Any s

freevars' :: UniversalF v (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

JoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

JoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

MeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

MeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

Lattice (ALia BooleanSort)

Defined in Data.Expression

Lattice (Lia BooleanSort)

Defined in Data.Expression

BoundedJoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

top :: Lia BooleanSort

BoundedLattice (ALia BooleanSort)

Defined in Data.Expression

BoundedLattice (Lia BooleanSort)

Defined in Data.Expression

ComplementedLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

complement :: ALia BooleanSort -> ALia BooleanSort

ComplementedLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

complement :: Lia BooleanSort -> Lia BooleanSort

(UniversalF v :<: f, SingI v) => Parseable (UniversalF v :: (Sort -> *) -> Sort -> *) f

Defined in Data.Expression

Methods

parser :: Proxy (UniversalF v) -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

data ExistentialF (v :: Sort) a (s :: Sort) where

A functor representing a mono-sorted existential quantifier binding a number of variables within a formula

Constructors

Exists :: [Var v] -> a BooleanSort -> ExistentialF v a BooleanSort

Instances

IShow (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ishow :: ExistentialF v (Const String) i -> Const String i

IEq1 (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ieq1 :: IEq a => ExistentialF v a j -> ExistentialF v a j -> Bool

IFoldable (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

ifold :: Monoid m => ExistentialF v (Const m) i' -> Const m i'

IFunctor (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ExistentialF v a i' -> ExistentialF v b i'

index :: ExistentialF v a i' -> Sing i'

ITraversable (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ExistentialF v a i' -> f (ExistentialF v b i')

MaybeQuantified (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g => ExistentialF v (IFix g) s -> Const Any s

freevars' :: ExistentialF v (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

JoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

JoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

MeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

MeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

Lattice (ALia BooleanSort)

Defined in Data.Expression

Lattice (Lia BooleanSort)

Defined in Data.Expression

BoundedJoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

top :: Lia BooleanSort

BoundedLattice (ALia BooleanSort)

Defined in Data.Expression

BoundedLattice (Lia BooleanSort)

Defined in Data.Expression

ComplementedLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

complement :: ALia BooleanSort -> ALia BooleanSort

ComplementedLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

complement :: Lia BooleanSort -> Lia BooleanSort

(ExistentialF v :<: f, SingI v) => Parseable (ExistentialF v :: (Sort -> *) -> Sort -> *) f

Defined in Data.Expression

Methods

parser :: Proxy (ExistentialF v) -> Parser (DynamicallySorted f) -> Parser (DynamicallySorted f)

newtype Substitution f

Substitution that given an expression produces replacement if the expression is to be replaced or nothing otherwise.

Constructors

Substitution

Fields

• runSubstitution :: forall (s :: Sort). IFix f s -> Maybe (IFix f s)

Instances

Semigroup (Substitution f)

Defined in Data.Expression

Methods

(<>) :: Substitution f -> Substitution f -> Substitution f

sconcat :: NonEmpty (Substitution f) -> Substitution f

stimes :: Integral b => b -> Substitution f -> Substitution f

Monoid (Substitution f)

Defined in Data.Expression

Methods

mempty :: Substitution f

mappend :: Substitution f -> Substitution f -> Substitution f

mconcat :: [Substitution f] -> Substitution f

substitute :: (IFunctor f, IEq1 f) => IFix f s -> Substitution f -> IFix f s

Executes a substitution.

for :: forall f (s :: Sort). (IFunctor f, IEq1 f) => IFix f s -> IFix f s -> Substitution f

A simple constructor of substitutions that replaces the latter expression with the former.

var :: forall f s. (VarF :<: f, SingI s) => VariableName -> IFix f s

A smart constructor for variables of any sort in any language Takes the variable name and infers the target language and sort from context.

var "a" :: Lia 'IntegralSort

true :: ConjunctionF :<: f => IFix f BooleanSort

Logical tautology

false :: DisjunctionF :<: f => IFix f BooleanSort

Logical contradiction

and :: ConjunctionF :<: f => [IFix f BooleanSort] -> IFix f BooleanSort

A smart constructor for variadic conjunction

or :: DisjunctionF :<: f => [IFix f BooleanSort] -> IFix f BooleanSort

A smart constructor for variadic disjunction

not :: NegationF :<: f => IFix f BooleanSort -> IFix f BooleanSort

A smart constructor for negation

forall :: UniversalF v :<: f => [Var v] -> IFix f BooleanSort -> IFix f BooleanSort

A smart constructor for universally quantified formulae

exists :: ExistentialF v :<: f => [Var v] -> IFix f BooleanSort -> IFix f BooleanSort

A smart constructor for existentially quantified formulae

(.&.) :: ConjunctionF :<: f => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infixr 6

A smart constructor for binary conjunction

(.|.) :: DisjunctionF :<: f => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infixr 5

A smart constructor for binary disjunction

(.->.) :: (DisjunctionF :<: f, NegationF :<: f) => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infixr 4

A smart constructor for implication (an abbreviation for not a .|. b)

(.<-.) :: (DisjunctionF :<: f, NegationF :<: f) => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infixl 4

A smart constructor for reversed implication (an abbreviation for a .|. not b)

(.<->.) :: (ConjunctionF :<: f, DisjunctionF :<: f, NegationF :<: f) => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infix 3

A smart constructor for if-and-only-if connective

(./=.) :: forall f s. (NegationF :<: f, EqualityF :<: f, SingI s) => IFix f s -> IFix f s -> IFix f BooleanSort infix 7

A smart constructor for disequality

literals :: (ConjunctionF :<: f, DisjunctionF :<: f) => IFix f BooleanSort -> [IFix f BooleanSort]

literals decomposes a boolean combination (formed with conjunctions and disjunctions, preferably in negation normal form) into its constituents.

conjuncts :: ConjunctionF :<: f => IFix f BooleanSort -> [IFix f BooleanSort]

conjuncts decomposes a conjunction into conjuncts.

disjuncts :: DisjunctionF :<: f => IFix f BooleanSort -> [IFix f BooleanSort]

disjuncts decomposes a disjunction into disjuncts.

vars :: (VarF :<: f, IFoldable f, IFunctor f) => IFix f s -> [DynamicallySorted VarF]

Collects a list of all variables occurring in an expression (bound or free).

freevars :: (IFunctor f, MaybeQuantified f) => IFix f s -> [DynamicallySorted VarF]

Collects a list of all free variables occurring in an expression.

class MaybeQuantified f

Minimal complete definition

isQuantified', freevars'

Instances

(IFunctor f, IFoldable f) => MaybeQuantified (f :: (k -> *) -> k -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g => f (IFix g) s -> Const Any s

freevars' :: f (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

MaybeQuantified (ExistentialF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g => ExistentialF v (IFix g) s -> Const Any s

freevars' :: ExistentialF v (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

MaybeQuantified (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g => UniversalF v (IFix g) s -> Const Any s

freevars' :: UniversalF v (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

MaybeQuantified (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g => VarF (IFix g) s -> Const Any s

freevars' :: VarF (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

(MaybeQuantified f, MaybeQuantified g) => MaybeQuantified (f :+: g :: (k -> *) -> k -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g0 => (f :+: g) (IFix g0) s -> Const Any s

freevars' :: (f :+: g) (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

isQuantified :: MaybeQuantified f => IFix f s -> Bool

Test whether an expression contains a quantifier.

isQuantifierFree :: MaybeQuantified f => IFix f s -> Bool

Tests whether an expression is free of any quantifier.

class (NegationF :<: f, HasDual f f) => NNF f

Instances

(NegationF :<: f, HasDual f f) => NNF f

Defined in Data.Expression

nnf :: forall f. NNF f => IFix f BooleanSort -> IFix f BooleanSort

Propagates negation toward boolean atoms (across conjunction, disjunction, quantifiers).

class (VarF :<: f, NegationF :<: f, IFunctor f, IFoldable f, ITraversable f, HasDual f f, MaybeQuantified' f f) => Prenex f

Instances

((VarF :: (Sort -> *) -> Sort -> *) :<: f, NegationF :<: f, IFunctor f, IFoldable f, ITraversable f, HasDual f f, MaybeQuantified' f f) => Prenex f

Defined in Data.Expression

prenex :: forall f. Prenex f => IFix f BooleanSort -> IFix f BooleanSort

Puts an expression into prenex form (quantifier prefix and a quantifier-free formula).

class (VarF :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, IFoldable f, ITraversable f) => Flatten f

Instances

((VarF :: (Sort -> *) -> Sort -> *) :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, IFoldable f, ITraversable f) => Flatten f

Defined in Data.Expression

flatten :: forall f. Flatten f => IFix f BooleanSort -> IFix f BooleanSort

Replaces non-variable and non-constant arguments to uninterpreted functions (such as select and store) with a fresh bound (universally or existentially) variable that is bound to the original term.

class (VarF :<: f, EqualityF :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, Forall f f, Axiomatized f f, IFoldable f, ITraversable f) => Unstore f

Instances

((VarF :: (Sort -> *) -> Sort -> *) :<: f, (EqualityF :: (Sort -> *) -> Sort -> *) :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, Forall f f, Axiomatized f f, IFoldable f, ITraversable f) => Unstore f

Defined in Data.Expression

unstore :: forall f. Unstore f => IFix f BooleanSort -> IFix f BooleanSort

Replaces store with an instance of its axiomatization.