atp-haskell-1.13: Translation from Ocaml to Haskell of John Harrison's ATP code

Safe HaskellNone
LanguageHaskell98

Data.Logic.ATP.Quantified

Contents

Description

IsQuantified is a subclass of IsPropositional of formula types that support existential and universal quantification.

Synopsis

Documentation

data Quant Source

The two types of quantification

Constructors

(:!:)

for_all

(:?:)

exists

Instances

class (IsPropositional formula, IsVariable (VarOf formula)) => IsQuantified formula where Source

Class of quantified formulas.

Associated Types

type VarOf formula Source

Methods

quant :: Quant -> VarOf formula -> formula -> formula Source

foldQuantified :: (Quant -> VarOf formula -> formula -> r) -> (formula -> BinOp -> formula -> r) -> (formula -> r) -> (Bool -> r) -> (AtomOf formula -> r) -> formula -> r Source

Instances

for_all :: IsQuantified formula => VarOf formula -> formula -> formula Source

(∀) :: IsQuantified formula => VarOf formula -> formula -> formula infixr 1 Source

∀ can't be a function when -XUnicodeSyntax is enabled.

exists :: IsQuantified formula => VarOf formula -> formula -> formula Source

(∃) :: IsQuantified formula => VarOf formula -> formula -> formula infixr 1 Source

precedenceQuantified :: forall formula. IsQuantified formula => formula -> Precedence Source

associativityQuantified :: forall formula. IsQuantified formula => formula -> Associativity Source

prettyQuantified :: forall fof v. (IsQuantified fof, v ~ VarOf fof) => Side -> PrettyLevel -> Rational -> fof -> Doc Source

Implementation of Pretty for IsQuantified types.

showQuantified :: IsQuantified formula => Side -> Int -> formula -> ShowS Source

Implementation of showsPrec for IsQuantified types.

zipQuantified :: IsQuantified formula => (Quant -> VarOf formula -> formula -> Quant -> VarOf formula -> formula -> Maybe r) -> (formula -> BinOp -> formula -> formula -> BinOp -> formula -> Maybe r) -> (formula -> formula -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (AtomOf formula -> AtomOf formula -> Maybe r) -> formula -> formula -> Maybe r Source

Combine two formulas if they are similar.

convertQuantified :: forall f1 f2. (IsQuantified f1, IsQuantified f2) => (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2 Source

Convert any instance of IsQuantified to any other by specifying the result type.

onatomsQuantified :: IsQuantified formula => (AtomOf formula -> AtomOf formula) -> formula -> formula Source

overatomsQuantified :: IsQuantified fof => (AtomOf fof -> r -> r) -> fof -> r -> r Source

Concrete instance of a quantified formula type

data QFormula v atom Source

Constructors

F 
T 
Atom atom 
Not (QFormula v atom) 
And (QFormula v atom) (QFormula v atom) 
Or (QFormula v atom) (QFormula v atom) 
Imp (QFormula v atom) (QFormula v atom) 
Iff (QFormula v atom) (QFormula v atom) 
Forall v (QFormula v atom) 
Exists v (QFormula v atom) 

Instances

IsFirstOrder EqFormula Source 
IsFirstOrder ApFormula Source 
IsFirstOrder Formula Source 
(Eq v, Eq atom) => Eq (QFormula v atom) Source 
(Data v, Data atom) => Data (QFormula v atom) Source 
(Ord v, Ord atom) => Ord (QFormula v atom) Source 
(Read v, Read atom) => Read (QFormula v atom) Source 
IsQuantified (QFormula v atom) => Show (QFormula v atom) Source 
(HasApply atom, IsTerm term, (~) * term (TermOf atom), (~) * v (TVarOf term)) => Pretty (QFormula v atom) Source 
IsQuantified (QFormula v atom) => HasFixity (QFormula v atom) Source 
(HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsFormula (QFormula v atom) Source 
(HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsLiteral (QFormula v atom) Source 
(IsFormula (QFormula v atom), HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsPropositional (QFormula v atom) Source 
(IsPropositional (QFormula v atom), IsVariable v, IsAtom atom) => IsQuantified (QFormula v atom) Source 
type AtomOf (QFormula v atom) = atom Source 
type VarOf (QFormula v atom) = v Source