Portability | GHC only |
---|---|
Maintainer | Simon Meier <iridcode@gmail.com> |
Safe Haskell | None |
Types and operations for handling sorted first-order logic
- data Connective
- data Quantifier
- data Formula s c v
- type LNFormula = Formula (String, LSort) Name LVar
- type LFormula c = Formula (String, LSort) c LVar
- quantify :: (Ord c, Ord v, Eq v) => v -> Formula s c v -> Formula s c v
- openFormula :: (MonadFresh m, Ord c) => LFormula c -> Maybe (Quantifier, m (LVar, LFormula c))
- openFormulaPrefix :: (MonadFresh m, Ord c) => LFormula c -> m ([LVar], Quantifier, LFormula c)
- lfalse :: Formula a s v
- ltrue :: 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 -> Formula a s v
- exists :: (Ord c, Ord v, Eq v) => s -> v -> Formula s c v -> Formula s c v
- forall :: (Ord c, Ord v, Eq v) => s -> v -> Formula s c v -> Formula s c v
- mapAtoms :: (Integer -> Atom (VTerm c (BVar v)) -> Atom (VTerm c1 (BVar v1))) -> Formula s c v -> Formula s c1 v1
- foldFormula :: (Atom (VTerm c (BVar v)) -> b) -> (Bool -> b) -> (b -> b) -> (Connective -> b -> b -> b) -> (Quantifier -> s -> b -> b) -> Formula s c v -> b
- prettyLNFormula :: HighlightDocument d => LNFormula -> d
Formulas
data Connective Source
Logical connectives.
data Quantifier Source
Quantifiers.
First-order formulas in locally nameless representation with hints for the names/sorts of quantified variables.
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) |
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
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
prettyLNFormula :: HighlightDocument d => LNFormula -> dSource
Pretty print a logical formula