Theory.Model.Formula

Types and operations for handling sorted first-order logic

Formulas

data Connective

Logical connectives.

Constructors

And

Or

Imp

Iff

Instances

Bounded Connective

Enum Connective

Eq Connective

Data Connective

Ord Connective

Show Connective

Typeable Connective

Binary Connective

NFData Connective

data Quantifier

Quantifiers.

Constructors

All

Ex

Instances

Bounded Quantifier

Enum Quantifier

Eq Quantifier

Data Quantifier

Ord Quantifier

Show Quantifier

Typeable Quantifier

Binary Quantifier

NFData Quantifier

data Formula s c v

First-order formulas in locally nameless representation with hints for the names/sorts of quantified variables.

Constructors

Ato (Atom (VTerm c (BVar v)))

TF !Bool

Not (Formula s c v)

Conn !Connective (Formula s c v) (Formula s c v)

Qua !Quantifier s (Formula s c v)

Instances

Apply LNFormula

HasFrees LNFormula

Foldable (Formula s c)

Eq (Formula (String, LSort) Name LVar)

Ord (Formula (String, LSort) Name LVar)

Show (Formula (String, LSort) Name LVar)

(Binary s_1627466130, Binary c_1627466131, Binary v_1627466132) => Binary (Formula s_1627466130 c_1627466131 v_1627466132)

(NFData s_1627466130, NFData c_1627466131, NFData v_1627466132) => NFData (Formula s_1627466130 c_1627466131 v_1627466132)

type LNFormula = Formula (String, LSort) Name LVar

type LFormula c = Formula (String, LSort) c LVar

LFormula are FOL formulas with sorts abused to denote both a hint for the name of the bound variable, as well as the variable's actual sort.

quantify :: (Ord c, Ord v, Eq v) => v -> Formula s c v -> Formula s c v

Introduce a bound variable for a free variable.

openFormula :: (MonadFresh m, Ord c) => LFormula c -> Maybe (Quantifier, m (LVar, LFormula c))

openFormula f returns Just (v,Q,f') if f = Q v. f' modulo alpha renaming and Nothing otherwise. v is always chosen to be fresh.

openFormulaPrefix :: (MonadFresh m, Ord c) => LFormula c -> m ([LVar], Quantifier, LFormula c)

openFormulaPrefix f returns Just (vs,Q,f') if f = Q v_1 .. v_k. f' modulo alpha renaming and Nothing otherwise. vs is always chosen to be fresh.

More convenient constructors

lfalse :: Formula a s v

Logically false.

ltrue :: Formula a s v

Logically true.

(.&&.) :: Formula a s v -> Formula a s v -> Formula a s v

(.||.) :: Formula a s v -> Formula a s v -> Formula a s v

(.==>.) :: Formula a s v -> Formula a s v -> Formula a s v

(.<=>.) :: Formula a s v -> Formula a s v -> Formula a s v

exists :: (Ord c, Ord v, Eq v) => s -> v -> Formula s c v -> Formula s c v

Create a existential quantification with a sort hint for the bound variable.

forall :: (Ord c, Ord v, Eq v) => s -> v -> Formula s c v -> Formula s c v

Create a universal quantification with a sort hint for the bound variable.

General Transformations

mapAtoms :: (Integer -> Atom (VTerm c (BVar v)) -> Atom (VTerm c1 (BVar v1))) -> Formula s c v -> Formula s c1 v1

Change the representation of atoms.

foldFormula :: (Atom (VTerm c (BVar v)) -> b) -> (Bool -> b) -> (b -> b) -> (Connective -> b -> b -> b) -> (Quantifier -> s -> b -> b) -> Formula s c v -> b

Fold a formula.

Pretty-Printing

prettyLNFormula :: HighlightDocument d => LNFormula -> d

Pretty print a logical formula