Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
IsQuantified
is a subclass of IsPropositional
of formula
types that support existential and universal quantification.
Synopsis
- data Quant
- class (IsPropositional formula, IsVariable (VarOf formula)) => IsQuantified formula where
- for_all :: IsQuantified formula => VarOf formula -> formula -> formula
- (∀) :: IsQuantified formula => VarOf formula -> formula -> formula
- exists :: IsQuantified formula => VarOf formula -> formula -> formula
- (∃) :: IsQuantified formula => VarOf formula -> formula -> formula
- precedenceQuantified :: forall formula. IsQuantified formula => formula -> Precedence
- associativityQuantified :: forall formula. IsQuantified formula => formula -> Associativity
- prettyQuantified :: forall fof v. (IsQuantified fof, v ~ VarOf fof) => Side -> PrettyLevel -> Rational -> fof -> Doc
- showQuantified :: IsQuantified formula => Side -> Int -> formula -> ShowS
- 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
- convertQuantified :: forall f1 f2. (IsQuantified f1, IsQuantified f2) => (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2
- onatomsQuantified :: IsQuantified formula => (AtomOf formula -> AtomOf formula) -> formula -> formula
- overatomsQuantified :: IsQuantified fof => (AtomOf fof -> r -> r) -> fof -> r -> r
- data QFormula v atom
Documentation
The two types of quantification
Instances
Data Quant Source # | |
Defined in Data.Logic.ATP.Quantified gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quant -> c Quant # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quant # dataTypeOf :: Quant -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quant) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant) # gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r # gmapQ :: (forall d. Data d => d -> u) -> Quant -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Quant -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quant -> m Quant # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant # | |
Show Quant Source # | |
Eq Quant Source # | |
Ord Quant Source # | |
class (IsPropositional formula, IsVariable (VarOf formula)) => IsQuantified formula where Source #
Class of quantified formulas.
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
(IsPropositional (QFormula v atom), IsVariable v, IsAtom atom) => IsQuantified (QFormula v atom) Source # | |
Defined in Data.Logic.ATP.Quantified quant :: Quant -> VarOf (QFormula v atom) -> QFormula v atom -> QFormula v atom Source # foldQuantified :: (Quant -> VarOf (QFormula v atom) -> QFormula v atom -> r) -> (QFormula v atom -> BinOp -> QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r Source # |
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
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 ApFormula Source # | |
Defined in Data.Logic.ATP.FOL | |
IsFirstOrder EqFormula Source # | |
Defined in Data.Logic.ATP.FOL | |
IsFirstOrder Formula Source # | |
Defined in Data.Logic.ATP.Skolem | |
(HasApply atom, v ~ TVarOf (TermOf atom)) => IsFormula (QFormula v atom) Source # | |
Defined in Data.Logic.ATP.Quantified true :: QFormula v atom Source # false :: QFormula v atom Source # asBool :: QFormula v atom -> Maybe Bool Source # atomic :: AtomOf (QFormula v atom) -> QFormula v atom Source # overatoms :: (AtomOf (QFormula v atom) -> r -> r) -> QFormula v atom -> r -> r Source # onatoms :: (AtomOf (QFormula v atom) -> AtomOf (QFormula v atom)) -> QFormula v atom -> QFormula v atom Source # | |
(HasApply atom, v ~ TVarOf (TermOf atom)) => IsLiteral (QFormula v atom) Source # | |
Defined in Data.Logic.ATP.Quantified naiveNegate :: QFormula v atom -> QFormula v atom Source # foldNegation :: (QFormula v atom -> r) -> (QFormula v atom -> r) -> QFormula v atom -> r Source # foldLiteral' :: (QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r Source # | |
IsQuantified (QFormula v atom) => HasFixity (QFormula v atom) Source # | |
Defined in Data.Logic.ATP.Quantified precedence :: QFormula v atom -> Precedence Source # associativity :: QFormula v atom -> Associativity Source # | |
(IsFormula (QFormula v atom), HasApply atom, v ~ TVarOf (TermOf atom)) => IsPropositional (QFormula v atom) Source # | |
Defined in Data.Logic.ATP.Quantified (.|.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source # (.&.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source # (.<=>.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source # (.=>.) :: QFormula v atom -> QFormula v atom -> QFormula v atom Source # foldPropositional' :: (QFormula v atom -> r) -> (QFormula v atom -> BinOp -> QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r Source # foldCombination :: (QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> QFormula v atom -> r Source # | |
(IsPropositional (QFormula v atom), IsVariable v, IsAtom atom) => IsQuantified (QFormula v atom) Source # | |
Defined in Data.Logic.ATP.Quantified quant :: Quant -> VarOf (QFormula v atom) -> QFormula v atom -> QFormula v atom Source # foldQuantified :: (Quant -> VarOf (QFormula v atom) -> QFormula v atom -> r) -> (QFormula v atom -> BinOp -> QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r Source # | |
(Data atom, Data v) => Data (QFormula v atom) Source # | |
Defined in Data.Logic.ATP.Quantified gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QFormula v atom -> c (QFormula v atom) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (QFormula v atom) # toConstr :: QFormula v atom -> Constr # dataTypeOf :: QFormula v atom -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (QFormula v atom)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (QFormula v atom)) # gmapT :: (forall b. Data b => b -> b) -> QFormula v atom -> QFormula v atom # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r # gmapQ :: (forall d. Data d => d -> u) -> QFormula v atom -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> QFormula v atom -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> QFormula v atom -> m (QFormula v atom) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QFormula v atom -> m (QFormula v atom) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QFormula v atom -> m (QFormula v atom) # | |
(Read atom, Read v) => Read (QFormula v atom) Source # | |
IsQuantified (QFormula v atom) => Show (QFormula v atom) Source # | |
(Eq atom, Eq v) => Eq (QFormula v atom) Source # | |
(Ord atom, Ord v) => Ord (QFormula v atom) Source # | |
Defined in Data.Logic.ATP.Quantified compare :: QFormula v atom -> QFormula v atom -> Ordering # (<) :: QFormula v atom -> QFormula v atom -> Bool # (<=) :: QFormula v atom -> QFormula v atom -> Bool # (>) :: QFormula v atom -> QFormula v atom -> Bool # (>=) :: QFormula v atom -> QFormula v atom -> Bool # max :: QFormula v atom -> QFormula v atom -> QFormula v atom # min :: QFormula v atom -> QFormula v atom -> QFormula v atom # | |
(HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Pretty (QFormula v atom) Source # | |
Defined in Data.Logic.ATP.Quantified pPrintPrec :: PrettyLevel -> Rational -> QFormula v atom -> Doc # pPrint :: QFormula v atom -> Doc # pPrintList :: PrettyLevel -> [QFormula v atom] -> Doc # | |
type AtomOf (QFormula v atom) Source # | |
Defined in Data.Logic.ATP.Quantified | |
type VarOf (QFormula v atom) Source # | |
Defined in Data.Logic.ATP.Quantified |