| Copyright | (C) 2017-18 Jakub Daniel |
|---|---|
| License | BSD-style (see the file LICENSE) |
| Maintainer | Jakub Daniel <jakub.daniel@protonmail.com> |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Expression
Description
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).
Synopsis
- 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) :: Type
- data Sort
- type DynamicallySortedFix f = DynamicallySorted (IFix f)
- data DynamicallySorted (d :: Sort -> *) where
- DynamicallySorted :: forall (s :: Sort) d. Sing s -> d s -> DynamicallySorted d
- data DynamicSort where
- DynamicSort :: forall (s :: Sort). Sing s -> DynamicSort
- withSort :: forall a (s :: Sort). Sing s -> (SingI s => a) -> a
- toStaticSort :: forall (s :: Sort). SingI s => DynamicSort -> Maybe (Sing s)
- toDynamicallySorted :: forall d (s :: Sort). SingI s => d s -> DynamicallySorted d
- toStaticallySorted :: forall d (s :: Sort). SingI s => DynamicallySorted d -> Maybe (d s)
- parseSort :: Parser DynamicSort
- 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)))
- type QFLiaF = ArithmeticF :+: (IfThenElseF :+: QFLogicF)
- type LiaF = ExistentialF BooleanSort :+: (ExistentialF IntegralSort :+: (UniversalF BooleanSort :+: (UniversalF IntegralSort :+: QFLiaF)))
- type QFALiaF = ArrayF :+: QFLiaF
- type ALiaF = ExistentialF BooleanSort :+: (ExistentialF IntegralSort :+: (UniversalF BooleanSort :+: (UniversalF IntegralSort :+: QFALiaF)))
- type Var = IFix VarF
- type QFLogic = IFix QFLogicF
- type QFLia = IFix QFLiaF
- type Lia = IFix LiaF
- type QFALia = IFix QFALiaF
- type ALia = IFix ALiaF
- class BoundedLattice a => ComplementedLattice a where
- complement :: a -> a
- type VariableName = String
- data VarF a (s :: Sort) where
- Var :: VariableName -> Sing s -> VarF a s
- data ConjunctionF a (s :: Sort) where
- And :: [a BooleanSort] -> ConjunctionF a BooleanSort
- data DisjunctionF a (s :: Sort) where
- Or :: [a BooleanSort] -> DisjunctionF a BooleanSort
- data NegationF a (s :: Sort) where
- Not :: a BooleanSort -> NegationF a BooleanSort
- data UniversalF (v :: Sort) a (s :: Sort) where
- Forall :: [Var v] -> a BooleanSort -> UniversalF v a BooleanSort
- data ExistentialF (v :: Sort) a (s :: Sort) where
- Exists :: [Var v] -> a BooleanSort -> ExistentialF v a BooleanSort
- newtype Substitution f = Substitution {
- runSubstitution :: forall (s :: Sort). IFix f s -> Maybe (IFix f s)
- substitute :: (IFunctor f, IEq1 f) => IFix f s -> Substitution f -> IFix f s
- for :: forall f (s :: Sort). (IFunctor f, IEq1 f) => IFix f s -> IFix f s -> Substitution f
- var :: forall f s. (VarF :<: f, SingI s) => VariableName -> IFix f s
- dynvar :: forall f (s :: Sort). VarF :<: f => VariableName -> Sing s -> DynamicallySortedFix f
- true :: ConjunctionF :<: f => IFix f BooleanSort
- false :: DisjunctionF :<: f => IFix f BooleanSort
- and :: ConjunctionF :<: f => [IFix f BooleanSort] -> IFix f BooleanSort
- or :: DisjunctionF :<: f => [IFix f BooleanSort] -> IFix f BooleanSort
- not :: NegationF :<: f => IFix f BooleanSort -> IFix f BooleanSort
- forall :: UniversalF v :<: f => [Var v] -> IFix f BooleanSort -> IFix f BooleanSort
- exists :: ExistentialF v :<: f => [Var v] -> IFix f BooleanSort -> IFix f BooleanSort
- (.&.) :: ConjunctionF :<: f => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort
- (.|.) :: DisjunctionF :<: f => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort
- (.->.) :: (DisjunctionF :<: f, NegationF :<: f) => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort
- (.<-.) :: (DisjunctionF :<: f, NegationF :<: f) => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort
- (.<->.) :: (ConjunctionF :<: f, DisjunctionF :<: f, NegationF :<: f) => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort
- (./=.) :: forall f s. (NegationF :<: f, EqualityF :<: f, SingI s) => IFix f s -> IFix f s -> IFix f BooleanSort
- literals :: (ConjunctionF :<: f, DisjunctionF :<: f) => IFix f BooleanSort -> [IFix f BooleanSort]
- conjuncts :: ConjunctionF :<: f => IFix f BooleanSort -> [IFix f BooleanSort]
- disjuncts :: DisjunctionF :<: f => IFix f BooleanSort -> [IFix f BooleanSort]
- vars :: (VarF :<: f, IFoldable f, IFunctor f) => IFix f s -> [DynamicallySorted Var]
- freevars :: (IFunctor f, MaybeQuantified f) => IFix f s -> [DynamicallySorted Var]
- freenames :: forall f (s :: Sort). (VarF :<: f, IFunctor f, IFoldable f) => IFix f s -> VariableNamePool
- class MaybeQuantified f
- isQuantified :: MaybeQuantified f => IFix f s -> Bool
- isQuantifierFree :: MaybeQuantified f => IFix f s -> Bool
- class (NegationF :<: f, HasDual f f) => NNF f
- nnf :: forall f. NNF f => IFix f BooleanSort -> IFix f BooleanSort
- class (VarF :<: f, NegationF :<: f, IFunctor f, IFoldable f, ITraversable f, HasDual f f, MaybeQuantified' f f) => Prenex f
- prenex :: forall f. Prenex f => IFix f BooleanSort -> IFix f BooleanSort
- class (VarF :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, IFoldable f, ITraversable f) => Flatten f
- flatten :: forall f. Flatten f => IFix f BooleanSort -> IFix f BooleanSort
- 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
- unstore :: forall f. Unstore f => IFix f BooleanSort -> IFix f BooleanSort
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) :: Type #
The singleton kind-indexed data family.
Instances
| data Sing (a :: Bool) | |
| data Sing (a :: Ordering) | |
| data Sing (n :: Nat) | |
| data Sing (n :: Symbol) | |
Defined in Data.Singletons.TypeLits.Internal | |
| data Sing (a :: ()) | |
Defined in Data.Singletons.Prelude.Instances | |
| data Sing (a :: Void) | |
Defined in Data.Singletons.Prelude.Instances | |
| data Sing (a :: All) | |
| data Sing (a :: Any) | |
| data Sing (a :: Sort) Source # | |
Defined in Data.Expression.Sort data Sing (a :: Sort) where
| |
| data Sing (b :: [a]) | |
| data Sing (b :: Maybe a) | |
| data Sing (b :: Min a) | |
| data Sing (b :: Max a) | |
| data Sing (b :: First a) | |
| data Sing (b :: Last a) | |
| data Sing (a :: WrappedMonoid m) | |
Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where
| |
| data Sing (b :: Option a) | |
| data Sing (b :: Identity a) | |
| data Sing (b :: First a) | |
| data Sing (b :: Last a) | |
| data Sing (b :: Dual a) | |
| data Sing (b :: Sum a) | |
| data Sing (b :: Product a) | |
| data Sing (b :: Down a) | |
| data Sing (b :: NonEmpty a) | |
| data Sing (b :: Endo a) | |
| data Sing (b :: MinInternal a) | |
Defined in Data.Singletons.Prelude.Foldable data Sing (b :: MinInternal a) where
| |
| data Sing (b :: MaxInternal a) | |
Defined in Data.Singletons.Prelude.Foldable data Sing (b :: MaxInternal a) where
| |
| data Sing (c :: Either a b) | |
| data Sing (c :: (a, b)) | |
| data Sing (c :: Arg a b) | |
| data Sing (f :: k1 ~> k2) | |
| data Sing (b :: StateL s a) | |
| data Sing (b :: StateR s a) | |
| data Sing (d :: (a, b, c)) | |
| data Sing (c :: Const a b) | |
| data Sing (e :: (a, b, c, d)) | |
| data Sing (f :: (a, b, c, d, e)) | |
| data Sing (g :: (a, b, c, d, e, f)) | |
Defined in Data.Singletons.Prelude.Instances | |
| data Sing (h :: (a, b, c, d, e, f, g)) | |
Defined in Data.Singletons.Prelude.Instances | |
A universe of recognized sorts
Constructors
| BooleanSort | booleans (true, false) |
| IntegralSort | integers (..., -1, 0, 1, ...) |
| ArraySort Sort Sort | arrays indexed by |
Instances
type DynamicallySortedFix f = DynamicallySorted (IFix f) Source #
An expression of some sort (obtained for example during parsing)
data DynamicallySorted (d :: Sort -> *) where Source #
A value of some sort
Constructors
| DynamicallySorted :: forall (s :: Sort) d. Sing s -> d s -> DynamicallySorted d |
Instances
| (forall (s :: Sort). Eq (d s)) => Eq (DynamicallySorted d) Source # | |
Defined in Data.Expression.Sort Methods (==) :: DynamicallySorted d -> DynamicallySorted d -> Bool # (/=) :: DynamicallySorted d -> DynamicallySorted d -> Bool # | |
| (forall (s :: Sort). Show (d s)) => Show (DynamicallySorted d) Source # | |
Defined in Data.Expression.Sort Methods showsPrec :: Int -> DynamicallySorted d -> ShowS # show :: DynamicallySorted d -> String # showList :: [DynamicallySorted d] -> ShowS # | |
data DynamicSort where Source #
Some sort (obtained for example during parsing)
Constructors
| DynamicSort :: forall (s :: Sort). Sing s -> DynamicSort |
Instances
| Eq DynamicSort Source # | |
Defined in Data.Expression.Sort | |
withSort :: forall a (s :: Sort). Sing s -> (SingI s => a) -> a Source #
Turn implicit sort parameter into explicit one
toStaticSort :: forall (s :: Sort). SingI s => DynamicSort -> Maybe (Sing s) Source #
Tries to convert some sort (DynamicSort) to a requested sort.
toDynamicallySorted :: forall d (s :: Sort). SingI s => d s -> DynamicallySorted d Source #
Converts a statically sorted expression to a dynamically sorted one.
toStaticallySorted :: forall d (s :: Sort). SingI s => DynamicallySorted d -> Maybe (d s) Source #
Tries to convert an expression (DynamicallySorted) of some sort to an expression of requested sort.
Performs no conversions.
parseSort :: Parser DynamicSort Source #
Parser that accepts sort definitions such as bool, int, array int int, array int (array ...).
type QFLiaF = ArithmeticF :+: (IfThenElseF :+: QFLogicF) Source #
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))) Source #
A functor much like QFLiaF with quantifiers over booleans and integers
type ALiaF = ExistentialF BooleanSort :+: (ExistentialF IntegralSort :+: (UniversalF BooleanSort :+: (UniversalF IntegralSort :+: QFALiaF))) Source #
A functor much like QFALiaF with quantifiers over booleans and integers
A language consisting solely of variables (useful for listing variables outside of any particular context, such as bound variables of quantified formula)
class BoundedLattice a => ComplementedLattice a where Source #
Bounded lattices that support complementing elements
complement . complement = id
Methods
complement :: a -> a Source #
Instances
| ComplementedLattice (ALia BooleanSort) Source # | |
Defined in Data.Expression Methods complement :: ALia BooleanSort -> ALia BooleanSort Source # | |
| ComplementedLattice (QFALia BooleanSort) Source # | |
Defined in Data.Expression Methods complement :: QFALia BooleanSort -> QFALia BooleanSort Source # | |
| ComplementedLattice (Lia BooleanSort) Source # | |
Defined in Data.Expression Methods complement :: Lia BooleanSort -> Lia BooleanSort Source # | |
| ComplementedLattice (QFLia BooleanSort) Source # | |
Defined in Data.Expression Methods complement :: QFLia BooleanSort -> QFLia BooleanSort Source # | |
| ComplementedLattice (QFLogic BooleanSort) Source # | |
Defined in Data.Expression Methods complement :: QFLogic BooleanSort -> QFLogic BooleanSort Source # | |
type VariableName = String Source #
Type of names assigned to variables
data VarF a (s :: Sort) where Source #
A functor representing a sorted variable, each variable is identified by its name and sort
Constructors
| Var :: VariableName -> Sing s -> VarF a s |
Instances
data ConjunctionF a (s :: Sort) where Source #
A functor representing a logical connective for conjunction
Constructors
| And :: [a BooleanSort] -> ConjunctionF a BooleanSort |
Instances
data DisjunctionF a (s :: Sort) where Source #
A functor representing a logical connective for disjunction
Constructors
| Or :: [a BooleanSort] -> DisjunctionF a BooleanSort |
Instances
data NegationF a (s :: Sort) where Source #
A functor representing a logical connective for negation
Constructors
| Not :: a BooleanSort -> NegationF a BooleanSort |
Instances
data UniversalF (v :: Sort) a (s :: Sort) where Source #
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
data ExistentialF (v :: Sort) a (s :: Sort) where Source #
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
newtype Substitution f Source #
Substitution that given an expression produces replacement if the expression is to be replaced or nothing otherwise.
Constructors
| Substitution | |
Fields
| |
Instances
| Semigroup (Substitution f) Source # | |
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) Source # | |
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 Source #
Executes a substitution.
for :: forall f (s :: Sort). (IFunctor f, IEq1 f) => IFix f s -> IFix f s -> Substitution f Source #
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 Source #
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
dynvar :: forall f (s :: Sort). VarF :<: f => VariableName -> Sing s -> DynamicallySortedFix f Source #
Like var except it hides the sort inside DynamicallySortedFix
true :: ConjunctionF :<: f => IFix f BooleanSort Source #
Logical tautology
false :: DisjunctionF :<: f => IFix f BooleanSort Source #
Logical contradiction
and :: ConjunctionF :<: f => [IFix f BooleanSort] -> IFix f BooleanSort Source #
A smart constructor for variadic conjunction
or :: DisjunctionF :<: f => [IFix f BooleanSort] -> IFix f BooleanSort Source #
A smart constructor for variadic disjunction
not :: NegationF :<: f => IFix f BooleanSort -> IFix f BooleanSort Source #
A smart constructor for negation
forall :: UniversalF v :<: f => [Var v] -> IFix f BooleanSort -> IFix f BooleanSort Source #
A smart constructor for universally quantified formulae
exists :: ExistentialF v :<: f => [Var v] -> IFix f BooleanSort -> IFix f BooleanSort Source #
A smart constructor for existentially quantified formulae
(.&.) :: ConjunctionF :<: f => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infixr 6 Source #
A smart constructor for binary conjunction
(.|.) :: DisjunctionF :<: f => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infixr 5 Source #
A smart constructor for binary disjunction
(.->.) :: (DisjunctionF :<: f, NegationF :<: f) => IFix f BooleanSort -> IFix f BooleanSort -> IFix f BooleanSort infixr 4 Source #
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 Source #
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 Source #
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 Source #
A smart constructor for disequality
literals :: (ConjunctionF :<: f, DisjunctionF :<: f) => IFix f BooleanSort -> [IFix f BooleanSort] Source #
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] Source #
conjuncts decomposes a conjunction into conjuncts.
disjuncts :: DisjunctionF :<: f => IFix f BooleanSort -> [IFix f BooleanSort] Source #
disjuncts decomposes a disjunction into disjuncts.
vars :: (VarF :<: f, IFoldable f, IFunctor f) => IFix f s -> [DynamicallySorted Var] Source #
Collects a list of all variables occurring in an expression (bound or free).
freevars :: (IFunctor f, MaybeQuantified f) => IFix f s -> [DynamicallySorted Var] Source #
Collects a list of all free variables occurring in an expression.
freenames :: forall f (s :: Sort). (VarF :<: f, IFunctor f, IFoldable f) => IFix f s -> VariableNamePool Source #
class MaybeQuantified f Source #
Minimal complete definition
isQuantified', freevars'
Instances
isQuantified :: MaybeQuantified f => IFix f s -> Bool Source #
Test whether an expression contains a quantifier.
isQuantifierFree :: MaybeQuantified f => IFix f s -> Bool Source #
Tests whether an expression is free of any quantifier.
nnf :: forall f. NNF f => IFix f BooleanSort -> IFix f BooleanSort Source #
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 Source #
prenex :: forall f. Prenex f => IFix f BooleanSort -> IFix f BooleanSort Source #
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 Source #
flatten :: forall f. Flatten f => IFix f BooleanSort -> IFix f BooleanSort Source #
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 Source #
unstore :: forall f. Unstore f => IFix f BooleanSort -> IFix f BooleanSort Source #
Replaces store with an instance of its axiomatization.