expressions-0.1.1: Expressions and Formulas a la carte

Copyright (C) 2017-18 Jakub Daniel BSD-style (see the file LICENSE) Jakub Daniel experimental None 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

# Documentation

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

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

A functor much like QFLiaF with quantifiers over booleans and integers

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)

A functor much like QFALiaF with quantifiers over booleans and integers

type Var = IFix VarF Source #

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

A language obtained as fixpoint of QFLogicF

A language obtained as fixpoint of QFLiaF

type Lia = IFix LiaF Source #

A language obtained as fixpoint of LiaF

A language obtained as fixpoint of QFALiaF

type ALia = IFix ALiaF Source #

A language obtained as fixpoint of ALiaF

class BoundedLattice a => ComplementedLattice a where Source #

Bounded lattices that support complementing elements

complement . complement = id

Minimal complete definition

complement

Methods

complement :: a -> a Source #

Instances

 Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods

Type of names assigned to variables

data VarF a s 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

 IShow Sort k (VarF (k -> *)) Source # Methodsishow :: f (Const k String) i -> Const (VarF (k -> *)) String i Source # IFoldable Sort (VarF (Sort -> *)) Source # Methodsifold :: Monoid m => f (Const (VarF (Sort -> *)) m) i' -> Const (VarF (Sort -> *)) m i' Source # IEq1 Sort (VarF (Sort -> *)) Source # Methodsieq1 :: IEq (VarF (Sort -> *)) a => f a j -> f a j -> Bool Source # IFunctor Sort (VarF (Sort -> *)) Source # Methodsimap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #index :: f a i' -> Sing (VarF (Sort -> *)) i' Source # Source # Methodsitraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source # Source # MethodsisQuantified' :: MaybeQuantified (VarF (Sort -> *)) g => f (IFix (VarF (Sort -> *)) g) s -> Const (VarF (Sort -> *)) Any sfreevars' :: f (Const (VarF (Sort -> *)) [DynamicallySorted (VarF (Sort -> *))]) s -> Const (VarF (Sort -> *)) [DynamicallySorted (VarF (Sort -> *))] s Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Source # Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Source # Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods (:<:) Sort (VarF (Sort -> *)) f => Parseable (k -> Sort -> *) (VarF k) f Source # Methodsparser :: Proxy (VarF k) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #

data ConjunctionF a s where Source #

A functor representing a logical connective for conjunction

Constructors

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

Instances

 Source # Methodsifold :: Monoid m => f (Const ConjunctionF m) i' -> Const ConjunctionF m i' Source # Source # Methodsieq1 :: IEq ConjunctionF a => f a j -> f a j -> Bool Source # Source # Methodsimap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #index :: f a i' -> Sing ConjunctionF i' Source # Source # Methodsitraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source # Source # Methodsishow :: f (Const k String) i -> Const ConjunctionF String i Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Source # Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Source # Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods (:<:) Sort ConjunctionF f => Parseable ((Sort -> *) -> Sort -> *) ConjunctionF f Source # Methods

data DisjunctionF a s where Source #

A functor representing a logical connective for disjunction

Constructors

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

Instances

 Source # Methodsifold :: Monoid m => f (Const DisjunctionF m) i' -> Const DisjunctionF m i' Source # Source # Methodsieq1 :: IEq DisjunctionF a => f a j -> f a j -> Bool Source # Source # Methodsimap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #index :: f a i' -> Sing DisjunctionF i' Source # Source # Methodsitraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source # Source # Methodsishow :: f (Const k String) i -> Const DisjunctionF String i Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Source # Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Source # Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods (:<:) Sort DisjunctionF f => Parseable ((Sort -> *) -> Sort -> *) DisjunctionF f Source # Methods

data NegationF a s where Source #

A functor representing a logical connective for negation

Constructors

 Not :: a BooleanSort -> NegationF a BooleanSort

Instances

 Source # Methodsifold :: Monoid m => f (Const NegationF m) i' -> Const NegationF m i' Source # Source # Methodsieq1 :: IEq NegationF a => f a j -> f a j -> Bool Source # Source # Methodsimap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #index :: f a i' -> Sing NegationF i' Source # Source # Methodsitraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source # Source # Methodsishow :: f (Const k String) i -> Const NegationF String i Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Source # Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Source # Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods (:<:) Sort NegationF f => Parseable ((Sort -> *) -> Sort -> *) NegationF f Source # Methods

data UniversalF v a s 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

 Source # Methodsishow :: f (Const k String) i -> Const (UniversalF v) String i Source # Source # Methodsifold :: Monoid m => f (Const (UniversalF v) m) i' -> Const (UniversalF v) m i' Source # Source # Methodsieq1 :: IEq (UniversalF v) a => f a j -> f a j -> Bool Source # Source # Methodsimap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #index :: f a i' -> Sing (UniversalF v) i' Source # Source # Methodsitraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source # Source # MethodsisQuantified' :: MaybeQuantified (UniversalF v) g => f (IFix (UniversalF v) g) s -> Const (UniversalF v) Any sfreevars' :: f (Const (UniversalF v) [DynamicallySorted (VarF (Sort -> *))]) s -> Const (UniversalF v) [DynamicallySorted (VarF (Sort -> *))] s Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Methods Source # Methods ((:<:) Sort (UniversalF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (UniversalF v) f Source # Methodsparser :: Proxy (UniversalF v) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #

data ExistentialF v a s 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

 Source # Methodsishow :: f (Const k String) i -> Const (ExistentialF v) String i Source # Source # Methodsifold :: Monoid m => f (Const (ExistentialF v) m) i' -> Const (ExistentialF v) m i' Source # Source # Methodsieq1 :: IEq (ExistentialF v) a => f a j -> f a j -> Bool Source # Source # Methodsimap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #index :: f a i' -> Sing (ExistentialF v) i' Source # Source # Methodsitraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source # Source # MethodsisQuantified' :: MaybeQuantified (ExistentialF v) g => f (IFix (ExistentialF v) g) s -> Const (ExistentialF v) Any sfreevars' :: f (Const (ExistentialF v) [DynamicallySorted (VarF (Sort -> *))]) s -> Const (ExistentialF v) [DynamicallySorted (VarF (Sort -> *))] s Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Source # Source # Methods Source # Methods ((:<:) Sort (ExistentialF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (ExistentialF v) f Source # Methodsparser :: Proxy (ExistentialF v) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #

newtype Substitution f Source #

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

Constructors

 Substitution FieldsrunSubstitution :: forall s. IFix f s -> Maybe (IFix f s)

Instances

 Source # Methodsmappend :: 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. (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


Logical tautology

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

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 decomposes a boolean combination (formed with conjunctions and disjunctions, preferably in negation normal form) into its constituents.

conjuncts decomposes a conjunction into conjuncts.

disjuncts decomposes a disjunction into disjuncts.

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

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

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

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

class MaybeQuantified f Source #

Minimal complete definition

isQuantified', freevars'

Instances

 (IFunctor k f, IFoldable k f) => MaybeQuantified k f Source # MethodsisQuantified' :: MaybeQuantified f g => f (IFix f g) s -> Const f Any sfreevars' :: f (Const f [DynamicallySorted (VarF (Sort -> *))]) s -> Const f [DynamicallySorted (VarF (Sort -> *))] s Source # MethodsisQuantified' :: MaybeQuantified (ExistentialF v) g => f (IFix (ExistentialF v) g) s -> Const (ExistentialF v) Any sfreevars' :: f (Const (ExistentialF v) [DynamicallySorted (VarF (Sort -> *))]) s -> Const (ExistentialF v) [DynamicallySorted (VarF (Sort -> *))] s Source # MethodsisQuantified' :: MaybeQuantified (UniversalF v) g => f (IFix (UniversalF v) g) s -> Const (UniversalF v) Any sfreevars' :: f (Const (UniversalF v) [DynamicallySorted (VarF (Sort -> *))]) s -> Const (UniversalF v) [DynamicallySorted (VarF (Sort -> *))] s Source # MethodsisQuantified' :: MaybeQuantified (VarF (Sort -> *)) g => f (IFix (VarF (Sort -> *)) g) s -> Const (VarF (Sort -> *)) Any sfreevars' :: f (Const (VarF (Sort -> *)) [DynamicallySorted (VarF (Sort -> *))]) s -> Const (VarF (Sort -> *)) [DynamicallySorted (VarF (Sort -> *))] s (MaybeQuantified k f, MaybeQuantified k g) => MaybeQuantified k ((:+:) k (k -> *) f g) Source # MethodsisQuantified' :: MaybeQuantified ((k :+: (k -> *)) f g) g => f (IFix ((k :+: (k -> *)) f g) g) s -> Const ((k :+: (k -> *)) f g) Any sfreevars' :: f (Const ((k :+: (k -> *)) f g) [DynamicallySorted (VarF (Sort -> *))]) s -> Const ((k :+: (k -> *)) f g) [DynamicallySorted (VarF (Sort -> *))] s

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.

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

Instances

 ((:<:) Sort NegationF f, HasDual f f) => NNF f Source #

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 #

Instances

 ((:<:) Sort (VarF (Sort -> *)) f, (:<:) Sort NegationF f, IFunctor Sort f, IFoldable Sort f, ITraversable Sort 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 #

Instances

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

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

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 Source #

Instances

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

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

Replaces store with an instance of its axiomatization.