tamarin-prover-theory-0.8.5.0: Term manipulation library for the tamarin prover.

Portability GHC only Simon Meier None

Theory.Model.Formula

Description

Types and operations for handling sorted first-order logic

Synopsis

# Formulas

data Connective Source

Logical connectives.

Constructors

 And Or Imp Iff

data Quantifier Source

Quantifiers.

Constructors

 All Ex

data Formula s c v Source

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_1627543173, Binary c_1627543174, Binary v_1627543175) => Binary (Formula s_1627543173 c_1627543174 v_1627543175) (NFData s_1627543173, NFData c_1627543174, NFData v_1627543175) => NFData (Formula s_1627543173 c_1627543174 v_1627543175)

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

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 vSource

Introduce a bound variable for a free variable.

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

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

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 vSource

Logically false.

ltrue :: Formula a s vSource

Logically true.

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

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

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

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

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

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 vSource

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 v1Source

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

Fold a formula.

## Pretty-Printing

Pretty print a logical formula