expressions-0.1.2: Expressions and Formulae a la carte

Copyright(C) 2017-18 Jakub Daniel
LicenseBSD-style (see the file LICENSE)
MaintainerJakub Daniel <jakub.daniel@protonmail.com>
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

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

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

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 :+: 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 QFALiaF = ArrayF :+: QFLiaF Source #

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

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)

type QFLogic = IFix QFLogicF Source #

A language obtained as fixpoint of QFLogicF

type QFLia = IFix QFLiaF Source #

A language obtained as fixpoint of QFLiaF

type Lia = IFix LiaF Source #

A language obtained as fixpoint of LiaF

type QFALia = IFix QFALiaF Source #

A language obtained as fixpoint of QFALiaF

type ALia = IFix ALiaF Source #

A language obtained as fixpoint of ALiaF

type VariableName = String Source #

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 # 

Methods

ishow :: f (Const k String) i -> Const (VarF (k -> *)) String i Source #

IFoldable Sort (VarF (Sort -> *)) Source # 

Methods

ifold :: Monoid m => f (Const (VarF (Sort -> *)) m) i' -> Const (VarF (Sort -> *)) m i' Source #

IEq1 Sort (VarF (Sort -> *)) Source # 

Methods

ieq1 :: IEq (VarF (Sort -> *)) a => f a j -> f a j -> Bool Source #

IFunctor Sort (VarF (Sort -> *)) Source # 

Methods

imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #

index :: f a i' -> Sing (VarF (Sort -> *)) i' Source #

ITraversable Sort (VarF (Sort -> *)) Source # 

Methods

itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #

MaybeQuantified Sort (VarF (Sort -> *)) Source # 

Methods

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

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

JoinSemiLattice (ALia BooleanSort) Source # 
JoinSemiLattice (QFALia BooleanSort) Source # 
JoinSemiLattice (Lia BooleanSort) Source # 
JoinSemiLattice (QFLia BooleanSort) Source # 
JoinSemiLattice (QFLogic BooleanSort) Source # 
MeetSemiLattice (ALia BooleanSort) Source # 
MeetSemiLattice (QFALia BooleanSort) Source # 
MeetSemiLattice (Lia BooleanSort) Source # 
MeetSemiLattice (QFLia BooleanSort) Source # 
MeetSemiLattice (QFLogic BooleanSort) Source # 
Lattice (ALia BooleanSort) Source # 
Lattice (QFALia BooleanSort) Source # 
Lattice (Lia BooleanSort) Source # 
Lattice (QFLia BooleanSort) Source # 
Lattice (QFLogic BooleanSort) Source # 
BoundedJoinSemiLattice (ALia BooleanSort) Source # 
BoundedJoinSemiLattice (QFALia BooleanSort) Source # 
BoundedJoinSemiLattice (Lia BooleanSort) Source # 
BoundedJoinSemiLattice (QFLia BooleanSort) Source # 
BoundedJoinSemiLattice (QFLogic BooleanSort) Source # 
BoundedMeetSemiLattice (ALia BooleanSort) Source # 

Methods

top :: ALia BooleanSort #

BoundedMeetSemiLattice (QFALia BooleanSort) Source # 
BoundedMeetSemiLattice (Lia BooleanSort) Source # 

Methods

top :: Lia BooleanSort #

BoundedMeetSemiLattice (QFLia BooleanSort) Source # 
BoundedMeetSemiLattice (QFLogic BooleanSort) Source # 
BoundedLattice (ALia BooleanSort) Source # 
BoundedLattice (QFALia BooleanSort) Source # 
BoundedLattice (Lia BooleanSort) Source # 
BoundedLattice (QFLia BooleanSort) Source # 
BoundedLattice (QFLogic BooleanSort) Source # 
ComplementedLattice (ALia BooleanSort) Source # 
ComplementedLattice (QFALia BooleanSort) Source # 
ComplementedLattice (Lia BooleanSort) Source # 
ComplementedLattice (QFLia BooleanSort) Source # 
ComplementedLattice (QFLogic BooleanSort) Source # 
(:<:) Sort (VarF (Sort -> *)) f => Parseable (k -> Sort -> *) (VarF k) f Source # 

data ConjunctionF a s where Source #

A functor representing a logical connective for conjunction

Constructors

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

Instances

IFoldable Sort ConjunctionF Source # 

Methods

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

IEq1 Sort ConjunctionF Source # 

Methods

ieq1 :: IEq ConjunctionF a => f a j -> f a j -> Bool Source #

IFunctor Sort ConjunctionF Source # 

Methods

imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #

index :: f a i' -> Sing ConjunctionF i' Source #

ITraversable Sort ConjunctionF Source # 

Methods

itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #

IShow Sort Sort ConjunctionF Source # 
JoinSemiLattice (ALia BooleanSort) Source # 
JoinSemiLattice (QFALia BooleanSort) Source # 
JoinSemiLattice (Lia BooleanSort) Source # 
JoinSemiLattice (QFLia BooleanSort) Source # 
JoinSemiLattice (QFLogic BooleanSort) Source # 
MeetSemiLattice (ALia BooleanSort) Source # 
MeetSemiLattice (QFALia BooleanSort) Source # 
MeetSemiLattice (Lia BooleanSort) Source # 
MeetSemiLattice (QFLia BooleanSort) Source # 
MeetSemiLattice (QFLogic BooleanSort) Source # 
Lattice (ALia BooleanSort) Source # 
Lattice (QFALia BooleanSort) Source # 
Lattice (Lia BooleanSort) Source # 
Lattice (QFLia BooleanSort) Source # 
Lattice (QFLogic BooleanSort) Source # 
BoundedJoinSemiLattice (ALia BooleanSort) Source # 
BoundedJoinSemiLattice (QFALia BooleanSort) Source # 
BoundedJoinSemiLattice (Lia BooleanSort) Source # 
BoundedJoinSemiLattice (QFLia BooleanSort) Source # 
BoundedJoinSemiLattice (QFLogic BooleanSort) Source # 
BoundedMeetSemiLattice (ALia BooleanSort) Source # 

Methods

top :: ALia BooleanSort #

BoundedMeetSemiLattice (QFALia BooleanSort) Source # 
BoundedMeetSemiLattice (Lia BooleanSort) Source # 

Methods

top :: Lia BooleanSort #

BoundedMeetSemiLattice (QFLia BooleanSort) Source # 
BoundedMeetSemiLattice (QFLogic BooleanSort) Source # 
BoundedLattice (ALia BooleanSort) Source # 
BoundedLattice (QFALia BooleanSort) Source # 
BoundedLattice (Lia BooleanSort) Source # 
BoundedLattice (QFLia BooleanSort) Source # 
BoundedLattice (QFLogic BooleanSort) Source # 
ComplementedLattice (ALia BooleanSort) Source # 
ComplementedLattice (QFALia BooleanSort) Source # 
ComplementedLattice (Lia BooleanSort) Source # 
ComplementedLattice (QFLia BooleanSort) Source # 
ComplementedLattice (QFLogic BooleanSort) Source # 
(:<:) Sort ConjunctionF f => Parseable ((Sort -> *) -> Sort -> *) ConjunctionF f Source # 

data DisjunctionF a s where Source #

A functor representing a logical connective for disjunction

Constructors

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

Instances

IFoldable Sort DisjunctionF Source # 

Methods

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

IEq1 Sort DisjunctionF Source # 

Methods

ieq1 :: IEq DisjunctionF a => f a j -> f a j -> Bool Source #

IFunctor Sort DisjunctionF Source # 

Methods

imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #

index :: f a i' -> Sing DisjunctionF i' Source #

ITraversable Sort DisjunctionF Source # 

Methods

itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #

IShow Sort Sort DisjunctionF Source # 
JoinSemiLattice (ALia BooleanSort) Source # 
JoinSemiLattice (QFALia BooleanSort) Source # 
JoinSemiLattice (Lia BooleanSort) Source # 
JoinSemiLattice (QFLia BooleanSort) Source # 
JoinSemiLattice (QFLogic BooleanSort) Source # 
MeetSemiLattice (ALia BooleanSort) Source # 
MeetSemiLattice (QFALia BooleanSort) Source # 
MeetSemiLattice (Lia BooleanSort) Source # 
MeetSemiLattice (QFLia BooleanSort) Source # 
MeetSemiLattice (QFLogic BooleanSort) Source # 
Lattice (ALia BooleanSort) Source # 
Lattice (QFALia BooleanSort) Source # 
Lattice (Lia BooleanSort) Source # 
Lattice (QFLia BooleanSort) Source # 
Lattice (QFLogic BooleanSort) Source # 
BoundedJoinSemiLattice (ALia BooleanSort) Source # 
BoundedJoinSemiLattice (QFALia BooleanSort) Source # 
BoundedJoinSemiLattice (Lia BooleanSort) Source # 
BoundedJoinSemiLattice (QFLia BooleanSort) Source # 
BoundedJoinSemiLattice (QFLogic BooleanSort) Source # 
BoundedMeetSemiLattice (ALia BooleanSort) Source # 

Methods

top :: ALia BooleanSort #

BoundedMeetSemiLattice (QFALia BooleanSort) Source # 
BoundedMeetSemiLattice (Lia BooleanSort) Source # 

Methods

top :: Lia BooleanSort #

BoundedMeetSemiLattice (QFLia BooleanSort) Source # 
BoundedMeetSemiLattice (QFLogic BooleanSort) Source # 
BoundedLattice (ALia BooleanSort) Source # 
BoundedLattice (QFALia BooleanSort) Source # 
BoundedLattice (Lia BooleanSort) Source # 
BoundedLattice (QFLia BooleanSort) Source # 
BoundedLattice (QFLogic BooleanSort) Source # 
ComplementedLattice (ALia BooleanSort) Source # 
ComplementedLattice (QFALia BooleanSort) Source # 
ComplementedLattice (Lia BooleanSort) Source # 
ComplementedLattice (QFLia BooleanSort) Source # 
ComplementedLattice (QFLogic BooleanSort) Source # 
(:<:) Sort DisjunctionF f => Parseable ((Sort -> *) -> Sort -> *) DisjunctionF f Source # 

data NegationF a s where Source #

A functor representing a logical connective for negation

Constructors

Not :: a BooleanSort -> NegationF a BooleanSort 

Instances

IFoldable Sort NegationF Source # 

Methods

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

IEq1 Sort NegationF Source # 

Methods

ieq1 :: IEq NegationF a => f a j -> f a j -> Bool Source #

IFunctor Sort NegationF Source # 

Methods

imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #

index :: f a i' -> Sing NegationF i' Source #

ITraversable Sort NegationF Source # 

Methods

itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #

IShow Sort Sort NegationF Source # 

Methods

ishow :: f (Const k String) i -> Const NegationF String i Source #

JoinSemiLattice (ALia BooleanSort) Source # 
JoinSemiLattice (QFALia BooleanSort) Source # 
JoinSemiLattice (Lia BooleanSort) Source # 
JoinSemiLattice (QFLia BooleanSort) Source # 
JoinSemiLattice (QFLogic BooleanSort) Source # 
MeetSemiLattice (ALia BooleanSort) Source # 
MeetSemiLattice (QFALia BooleanSort) Source # 
MeetSemiLattice (Lia BooleanSort) Source # 
MeetSemiLattice (QFLia BooleanSort) Source # 
MeetSemiLattice (QFLogic BooleanSort) Source # 
Lattice (ALia BooleanSort) Source # 
Lattice (QFALia BooleanSort) Source # 
Lattice (Lia BooleanSort) Source # 
Lattice (QFLia BooleanSort) Source # 
Lattice (QFLogic BooleanSort) Source # 
BoundedJoinSemiLattice (ALia BooleanSort) Source # 
BoundedJoinSemiLattice (QFALia BooleanSort) Source # 
BoundedJoinSemiLattice (Lia BooleanSort) Source # 
BoundedJoinSemiLattice (QFLia BooleanSort) Source # 
BoundedJoinSemiLattice (QFLogic BooleanSort) Source # 
BoundedMeetSemiLattice (ALia BooleanSort) Source # 

Methods

top :: ALia BooleanSort #

BoundedMeetSemiLattice (QFALia BooleanSort) Source # 
BoundedMeetSemiLattice (Lia BooleanSort) Source # 

Methods

top :: Lia BooleanSort #

BoundedMeetSemiLattice (QFLia BooleanSort) Source # 
BoundedMeetSemiLattice (QFLogic BooleanSort) Source # 
BoundedLattice (ALia BooleanSort) Source # 
BoundedLattice (QFALia BooleanSort) Source # 
BoundedLattice (Lia BooleanSort) Source # 
BoundedLattice (QFLia BooleanSort) Source # 
BoundedLattice (QFLogic BooleanSort) Source # 
ComplementedLattice (ALia BooleanSort) Source # 
ComplementedLattice (QFALia BooleanSort) Source # 
ComplementedLattice (Lia BooleanSort) Source # 
ComplementedLattice (QFLia BooleanSort) Source # 
ComplementedLattice (QFLogic BooleanSort) Source # 
(:<:) Sort NegationF f => Parseable ((Sort -> *) -> Sort -> *) NegationF f Source # 

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

IShow Sort Sort (UniversalF v) Source # 

Methods

ishow :: f (Const k String) i -> Const (UniversalF v) String i Source #

IFoldable Sort (UniversalF v) Source # 

Methods

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

IEq1 Sort (UniversalF v) Source # 

Methods

ieq1 :: IEq (UniversalF v) a => f a j -> f a j -> Bool Source #

IFunctor Sort (UniversalF v) Source # 

Methods

imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #

index :: f a i' -> Sing (UniversalF v) i' Source #

ITraversable Sort (UniversalF v) Source # 

Methods

itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #

MaybeQuantified Sort (UniversalF v) Source # 
JoinSemiLattice (ALia BooleanSort) Source # 
JoinSemiLattice (Lia BooleanSort) Source # 
MeetSemiLattice (ALia BooleanSort) Source # 
MeetSemiLattice (Lia BooleanSort) Source # 
Lattice (ALia BooleanSort) Source # 
Lattice (Lia BooleanSort) Source # 
BoundedJoinSemiLattice (ALia BooleanSort) Source # 
BoundedJoinSemiLattice (Lia BooleanSort) Source # 
BoundedMeetSemiLattice (ALia BooleanSort) Source # 

Methods

top :: ALia BooleanSort #

BoundedMeetSemiLattice (Lia BooleanSort) Source # 

Methods

top :: Lia BooleanSort #

BoundedLattice (ALia BooleanSort) Source # 
BoundedLattice (Lia BooleanSort) Source # 
ComplementedLattice (ALia BooleanSort) Source # 
ComplementedLattice (Lia BooleanSort) Source # 
((:<:) Sort (UniversalF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (UniversalF v) f 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

IShow Sort Sort (ExistentialF v) Source # 

Methods

ishow :: f (Const k String) i -> Const (ExistentialF v) String i Source #

IFoldable Sort (ExistentialF v) Source # 

Methods

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

IEq1 Sort (ExistentialF v) Source # 

Methods

ieq1 :: IEq (ExistentialF v) a => f a j -> f a j -> Bool Source #

IFunctor Sort (ExistentialF v) Source # 

Methods

imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i' Source #

index :: f a i' -> Sing (ExistentialF v) i' Source #

ITraversable Sort (ExistentialF v) Source # 

Methods

itraverse :: Applicative f => (forall i'. a i' -> f (b i')) -> forall i'. t a i' -> f (t b i') Source #

MaybeQuantified Sort (ExistentialF v) Source # 
JoinSemiLattice (ALia BooleanSort) Source # 
JoinSemiLattice (Lia BooleanSort) Source # 
MeetSemiLattice (ALia BooleanSort) Source # 
MeetSemiLattice (Lia BooleanSort) Source # 
Lattice (ALia BooleanSort) Source # 
Lattice (Lia BooleanSort) Source # 
BoundedJoinSemiLattice (ALia BooleanSort) Source # 
BoundedJoinSemiLattice (Lia BooleanSort) Source # 
BoundedMeetSemiLattice (ALia BooleanSort) Source # 

Methods

top :: ALia BooleanSort #

BoundedMeetSemiLattice (Lia BooleanSort) Source # 

Methods

top :: Lia BooleanSort #

BoundedLattice (ALia BooleanSort) Source # 
BoundedLattice (Lia BooleanSort) Source # 
ComplementedLattice (ALia BooleanSort) Source # 
ComplementedLattice (Lia BooleanSort) Source # 
((:<:) Sort (ExistentialF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (ExistentialF v) f Source # 

newtype Substitution f Source #

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

Constructors

Substitution 

Fields

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

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

Methods

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

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

MaybeQuantified Sort (ExistentialF v) Source # 
MaybeQuantified Sort (UniversalF v) Source # 
MaybeQuantified Sort (VarF (Sort -> *)) Source # 

Methods

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

freevars' :: 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 # 

Methods

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

freevars' :: 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.