Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Logic.ATP.Term

Contents

Variables
Functions
Terms

Description

A Term is a expression representing a domain element. It is composed of variables which can be bound to domain elements, or functions which can be applied to terms to yield other domain elements.

Synopsis

class (Ord v, IsString v, Pretty v, Show v) => IsVariable v where
- variant :: v -> Set v -> v
- prefix :: String -> v -> v
variants :: IsVariable v => v -> [v]
newtype V = V String
class (IsString function, Ord function, Pretty function, Show function) => IsFunction function
type Arity = Int
newtype FName = FName String
class (Eq term, Ord term, Pretty term, Show term, IsString term, HasFixity term, IsVariable (TVarOf term), IsFunction (FunOf term)) => IsTerm term where
- type TVarOf term
- type FunOf term
- vt :: TVarOf term -> term
- fApp :: FunOf term -> [term] -> term
- foldTerm :: (TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
zipTerms :: (IsTerm term1, v1 ~ TVarOf term1, function1 ~ FunOf term1, IsTerm term2, v2 ~ TVarOf term2, function2 ~ FunOf term2) => (v1 -> v2 -> Maybe r) -> (function1 -> [term1] -> function2 -> [term2] -> Maybe r) -> term1 -> term2 -> Maybe r
convertTerm :: (IsTerm term1, v1 ~ TVarOf term1, f1 ~ FunOf term1, IsTerm term2, v2 ~ TVarOf term2, f2 ~ FunOf term2) => (v1 -> v2) -> (f1 -> f2) -> term1 -> term2
precedenceTerm :: IsTerm term => term -> Precedence
associativityTerm :: IsTerm term => term -> Associativity
prettyTerm :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term, HasFixity term, Pretty v, Pretty function) => PrettyLevel -> Rational -> term -> Doc
prettyFunctionApply :: (function ~ FunOf term, IsTerm term, HasFixity term) => PrettyLevel -> function -> [term] -> Doc
showTerm :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term, Pretty v, Pretty function) => term -> String
showFunctionApply :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term) => function -> [term] -> String
funcs :: (IsTerm term, function ~ FunOf term) => term -> Set (function, Arity)
data Term function v
- = Var v
- | FApply function [Term function v]
type FTerm = Term FName V
testTerm :: Test

Variables

class (Ord v, IsString v, Pretty v, Show v) => IsVariable v where Source #

Methods

variant :: v -> Set v -> v Source #

Return a variable based on v but different from any set element. The result may be v itself if v is not a member of the set.

prefix :: String -> v -> v Source #

Modify a variable by adding a prefix. This unfortunately assumes that v is "string-like" but at least one algorithm in Harrison currently requires this.

Instances

Instances details

IsVariable V Source #
Instance details Defined in Data.Logic.ATP.Term Methods variant :: V -> Set V -> V Source # prefix :: String -> V -> V Source #
IsVariable String Source #
Instance details Defined in Data.Logic.ATP.Term Methods variant :: String -> Set String -> String Source # prefix :: String -> String -> String Source #

variants :: IsVariable v => v -> [v] Source #

Return an infinite list of variations on v

newtype V Source #

Constructors

V String

Instances

Instances details

JustApply ApAtom Source #
Instance details Defined in Data.Logic.ATP.Apply
IsFirstOrder ApFormula Source #
Instance details Defined in Data.Logic.ATP.FOL
IsFirstOrder EqFormula Source #
Instance details Defined in Data.Logic.ATP.FOL
IsFirstOrder Formula Source #
Instance details Defined in Data.Logic.ATP.Skolem
IsVariable V Source #
Instance details Defined in Data.Logic.ATP.Term Methods variant :: V -> Set V -> V Source # prefix :: String -> V -> V Source #
Data V Source #
Instance details Defined in Data.Logic.ATP.Term Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> V -> c V # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c V # toConstr :: V -> Constr # dataTypeOf :: V -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c V) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V) # gmapT :: (forall b. Data b => b -> b) -> V -> V # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r # gmapQ :: (forall d. Data d => d -> u) -> V -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> V -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> V -> m V # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> V -> m V # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> V -> m V #
IsString V Source #
Instance details Defined in Data.Logic.ATP.Term Methods fromString :: String -> V #
Read V Source #
Instance details Defined in Data.Logic.ATP.Term Methods readsPrec :: Int -> ReadS V # readList :: ReadS [V] # readPrec :: ReadPrec V # readListPrec :: ReadPrec [V] #
Show V Source #
Instance details Defined in Data.Logic.ATP.Term Methods showsPrec :: Int -> V -> ShowS # show :: V -> String # showList :: [V] -> ShowS #
Eq V Source #
Instance details Defined in Data.Logic.ATP.Term Methods (==) :: V -> V -> Bool # (/=) :: V -> V -> Bool #
Ord V Source #
Instance details Defined in Data.Logic.ATP.Term Methods compare :: V -> V -> Ordering # (<) :: V -> V -> Bool # (<=) :: V -> V -> Bool # (>) :: V -> V -> Bool # (>=) :: V -> V -> Bool # max :: V -> V -> V # min :: V -> V -> V #
Pretty V Source #
Instance details Defined in Data.Logic.ATP.Term Methods pPrintPrec :: PrettyLevel -> Rational -> V -> Doc # pPrint :: V -> Doc # pPrintList :: PrettyLevel -> [V] -> Doc #
MonadFail m => Unify m (SkAtom, SkAtom) Source #
Instance details Defined in Data.Logic.ATP.Unif Associated Types type UTermOf (SkAtom, SkAtom) Source # Methods unify' :: (SkAtom, SkAtom) -> StateT (Map (TVarOf (UTermOf (SkAtom, SkAtom))) (UTermOf (SkAtom, SkAtom))) m () Source #
type UTermOf (SkAtom, SkAtom) Source #
Instance details Defined in Data.Logic.ATP.Unif type UTermOf (SkAtom, SkAtom) = TermOf SkAtom

Functions

class (IsString function, Ord function, Pretty function, Show function) => IsFunction function Source #

Instances

Instances details

IsFunction Function Source #
Instance details Defined in Data.Logic.ATP.Skolem
IsFunction FName Source #
Instance details Defined in Data.Logic.ATP.Term

type Arity = Int Source #

newtype FName Source #

A simple type to use as the function parameter of Term. The only reason to use this instead of String is to get nicer pretty printing.

Constructors

FName String

Instances

Instances details

JustApply ApAtom Source #
Instance details Defined in Data.Logic.ATP.Apply
IsFirstOrder ApFormula Source #
Instance details Defined in Data.Logic.ATP.FOL
IsFirstOrder EqFormula Source #
Instance details Defined in Data.Logic.ATP.FOL
IsFunction FName Source #
Instance details Defined in Data.Logic.ATP.Term
IsString FName Source #
Instance details Defined in Data.Logic.ATP.Term Methods fromString :: String -> FName #
Show FName Source #
Instance details Defined in Data.Logic.ATP.Term Methods showsPrec :: Int -> FName -> ShowS # show :: FName -> String # showList :: [FName] -> ShowS #
Eq FName Source #
Instance details Defined in Data.Logic.ATP.Term Methods (==) :: FName -> FName -> Bool # (/=) :: FName -> FName -> Bool #
Ord FName Source #
Instance details Defined in Data.Logic.ATP.Term Methods compare :: FName -> FName -> Ordering # (<) :: FName -> FName -> Bool # (<=) :: FName -> FName -> Bool # (>) :: FName -> FName -> Bool # (>=) :: FName -> FName -> Bool # max :: FName -> FName -> FName # min :: FName -> FName -> FName #
Pretty FName Source #
Instance details Defined in Data.Logic.ATP.Term Methods pPrintPrec :: PrettyLevel -> Rational -> FName -> Doc # pPrint :: FName -> Doc # pPrintList :: PrettyLevel -> [FName] -> Doc #

Terms

class (Eq term, Ord term, Pretty term, Show term, IsString term, HasFixity term, IsVariable (TVarOf term), IsFunction (FunOf term)) => IsTerm term where Source #

A term is an expression representing a domain element, either as a variable reference or a function applied to a list of terms.

Associated Types

type TVarOf term Source #

The associated variable type

type FunOf term Source #

The associated function type

Methods

vt :: TVarOf term -> term Source #

Build a term which is a variable reference.

fApp :: FunOf term -> [term] -> term Source #

Build a term by applying terms to an atomic function (FunOf term).

foldTerm Source #

Arguments

:: (TVarOf term -> r)	Variable references are dispatched here
-> (FunOf term -> [term] -> r)	Function applications are dispatched here
-> term
-> r

A fold over instances of IsTerm.

Instances

Instances details

(IsFunction function, IsVariable v) => IsTerm (Term function v) Source #

Instance details

Defined in Data.Logic.ATP.Term

Associated Types

type TVarOf (Term function v) Source #

type FunOf (Term function v) Source #

Methods

vt :: TVarOf (Term function v) -> Term function v Source #

fApp :: FunOf (Term function v) -> [Term function v] -> Term function v Source #

foldTerm :: (TVarOf (Term function v) -> r) -> (FunOf (Term function v) -> [Term function v] -> r) -> Term function v -> r Source #

zipTerms Source #

Arguments

:: (IsTerm term1, v1 ~ TVarOf term1, function1 ~ FunOf term1, IsTerm term2, v2 ~ TVarOf term2, function2 ~ FunOf term2)
=> (v1 -> v2 -> Maybe r)	Combine two variables
-> (function1 -> [term1] -> function2 -> [term2] -> Maybe r)	Combine two function applications
-> term1
-> term2
-> Maybe r	Result for dissimilar terms is `Nothing`.

Combine two terms if they are similar (i.e. two variables or two function applications.)

convertTerm Source #

Arguments

:: (IsTerm term1, v1 ~ TVarOf term1, f1 ~ FunOf term1, IsTerm term2, v2 ~ TVarOf term2, f2 ~ FunOf term2)
=> (v1 -> v2)	convert a variable
-> (f1 -> f2)	convert a function
-> term1
-> term2

Convert between two instances of IsTerm

precedenceTerm :: IsTerm term => term -> Precedence Source #

associativityTerm :: IsTerm term => term -> Associativity Source #

prettyTerm :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term, HasFixity term, Pretty v, Pretty function) => PrettyLevel -> Rational -> term -> Doc Source #

Implementation of pPrint for any term

prettyFunctionApply :: (function ~ FunOf term, IsTerm term, HasFixity term) => PrettyLevel -> function -> [term] -> Doc Source #

Format a function application: F(x,y)

showTerm :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term, Pretty v, Pretty function) => term -> String Source #

Implementation of show for any term

showFunctionApply :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term) => function -> [term] -> String Source #

Build an expression for a function application: fApp (F) [x, y]

funcs :: (IsTerm term, function ~ FunOf term) => term -> Set (function, Arity) Source #

data Term function v Source #

Constructors

Var v
FApply function [Term function v]

Instances

Instances details

JustApply ApAtom Source #
Instance details Defined in Data.Logic.ATP.Apply
IsFirstOrder ApFormula Source #
Instance details Defined in Data.Logic.ATP.FOL
IsFirstOrder EqFormula Source #
Instance details Defined in Data.Logic.ATP.FOL
IsFirstOrder Formula Source #
Instance details Defined in Data.Logic.ATP.Skolem
MonadFail m => Unify m (SkAtom, SkAtom) Source #
Instance details Defined in Data.Logic.ATP.Unif Associated Types type UTermOf (SkAtom, SkAtom) Source # Methods unify' :: (SkAtom, SkAtom) -> StateT (Map (TVarOf (UTermOf (SkAtom, SkAtom))) (UTermOf (SkAtom, SkAtom))) m () Source #
(IsFunction function, IsVariable v) => HasFixity (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term Methods precedence :: Term function v -> Precedence Source # associativity :: Term function v -> Associativity Source #
(IsFunction function, IsVariable v) => IsTerm (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term Associated Types type TVarOf (Term function v) Source # type FunOf (Term function v) Source # Methods vt :: TVarOf (Term function v) -> Term function v Source # fApp :: FunOf (Term function v) -> [Term function v] -> Term function v Source # foldTerm :: (TVarOf (Term function v) -> r) -> (FunOf (Term function v) -> [Term function v] -> r) -> Term function v -> r Source #
(Data v, Data function) => Data (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term function v -> c (Term function v) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Term function v) # toConstr :: Term function v -> Constr # dataTypeOf :: Term function v -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Term function v)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Term function v)) # gmapT :: (forall b. Data b => b -> b) -> Term function v -> Term function v # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term function v -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term function v -> r # gmapQ :: (forall d. Data d => d -> u) -> Term function v -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Term function v -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term function v -> m (Term function v) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term function v -> m (Term function v) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term function v -> m (Term function v) #
(IsVariable v, IsFunction function) => IsString (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term Methods fromString :: String -> Term function v #
(Read v, Read function) => Read (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term Methods readsPrec :: Int -> ReadS (Term function v) # readList :: ReadS [Term function v] # readPrec :: ReadPrec (Term function v) # readListPrec :: ReadPrec [Term function v] #
(IsVariable v, IsFunction function) => Show (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term Methods showsPrec :: Int -> Term function v -> ShowS # show :: Term function v -> String # showList :: [Term function v] -> ShowS #
(Eq v, Eq function) => Eq (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term Methods (==) :: Term function v -> Term function v -> Bool # (/=) :: Term function v -> Term function v -> Bool #
(Ord v, Ord function) => Ord (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term Methods compare :: Term function v -> Term function v -> Ordering # (<) :: Term function v -> Term function v -> Bool # (<=) :: Term function v -> Term function v -> Bool # (>) :: Term function v -> Term function v -> Bool # (>=) :: Term function v -> Term function v -> Bool # max :: Term function v -> Term function v -> Term function v # min :: Term function v -> Term function v -> Term function v #
IsTerm (Term function v) => Pretty (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term Methods pPrintPrec :: PrettyLevel -> Rational -> Term function v -> Doc # pPrint :: Term function v -> Doc # pPrintList :: PrettyLevel -> [Term function v] -> Doc #
type FunOf (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term type FunOf (Term function v) = function
type TVarOf (Term function v) Source #
Instance details Defined in Data.Logic.ATP.Term type TVarOf (Term function v) = v
type UTermOf (SkAtom, SkAtom) Source #
Instance details Defined in Data.Logic.ATP.Unif type UTermOf (SkAtom, SkAtom) = TermOf SkAtom

type FTerm = Term FName V Source #

A term type with no Skolem functions

testTerm :: Test Source #