Data.Logic.ATP.Term

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.

Variables

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

Minimal complete definition

variant, prefix

Methods

variant :: v -> Set v -> v

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

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

IsVariable String

Methods

variant :: String -> Set String -> String

prefix :: String -> String -> String

IsVariable V

Methods

variant :: V -> Set V -> V

prefix :: String -> V -> V

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

Return an infinite list of variations on v

newtype V

Constructors

V String

Instances

Eq V

Methods

(==) :: V -> V -> Bool

(/=) :: V -> V -> Bool

Data V

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 :: (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

Ord V

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

Read V

Methods

readsPrec :: Int -> ReadS V

readList :: ReadS [V]

readPrec :: ReadPrec V

readListPrec :: ReadPrec [V]

Show V

Methods

showsPrec :: Int -> V -> ShowS

show :: V -> String

showList :: [V] -> ShowS

IsString V

Methods

fromString :: String -> V

Pretty V

Methods

pPrintPrec :: PrettyLevel -> Rational -> V -> Doc

pPrint :: V -> Doc

pPrintList :: PrettyLevel -> [V] -> Doc

IsVariable V

Methods

variant :: V -> Set V -> V

prefix :: String -> V -> V

JustApply ApAtom

IsFirstOrder EqFormula

IsFirstOrder ApFormula

IsFirstOrder Formula

Monad m => Unify m (SkAtom, SkAtom)

Associated Types

type UTermOf (SkAtom, SkAtom) :: *

Methods

unify' :: (SkAtom, SkAtom) -> StateT (Map (TVarOf (UTermOf (SkAtom, SkAtom))) (UTermOf (SkAtom, SkAtom))) m ()

type UTermOf (SkAtom, SkAtom)

type UTermOf (SkAtom, SkAtom) = TermOf SkAtom

Functions

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

Instances

IsFunction FName

IsFunction Function

type Arity = Int

newtype FName

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

Eq FName

Methods

(==) :: FName -> FName -> Bool

(/=) :: FName -> FName -> Bool

Ord FName

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

Show FName

Methods

showsPrec :: Int -> FName -> ShowS

show :: FName -> String

showList :: [FName] -> ShowS

IsString FName

Methods

fromString :: String -> FName

Pretty FName

Methods

pPrintPrec :: PrettyLevel -> Rational -> FName -> Doc

pPrint :: FName -> Doc

pPrintList :: PrettyLevel -> [FName] -> Doc

IsFunction FName

JustApply ApAtom

IsFirstOrder EqFormula

IsFirstOrder ApFormula

Terms

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

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

Minimal complete definition

vt, fApp, foldTerm

Associated Types

type TVarOf term

The associated variable type

type FunOf term

The associated function type

Methods

vt :: TVarOf term -> term

Build a term which is a variable reference.

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

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

foldTerm :: (TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r

A fold over instances of IsTerm.

Instances

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

Associated Types

type TVarOf (Term function v) :: *

type FunOf (Term function v) :: *

Methods

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

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

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

zipTerms

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

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

associativityTerm :: IsTerm term => term -> Associativity

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

Implementation of pPrint for any term

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

Format a function application: F(x,y)

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

Implementation of show for any term

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

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

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

data Term function v

Constructors

Var v

FApply function [Term function v]

Instances

JustApply ApAtom

IsFirstOrder EqFormula

IsFirstOrder ApFormula

IsFirstOrder Formula

Monad m => Unify m (SkAtom, SkAtom)

Associated Types

type UTermOf (SkAtom, SkAtom) :: *

Methods

unify' :: (SkAtom, SkAtom) -> StateT (Map (TVarOf (UTermOf (SkAtom, SkAtom))) (UTermOf (SkAtom, SkAtom))) m ()

(Eq function, Eq v) => Eq (Term function v)

Methods

(==) :: Term function v -> Term function v -> Bool

(/=) :: Term function v -> Term function v -> Bool

(Data function, Data v) => Data (Term function v)

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 :: (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)

(Ord function, Ord v) => Ord (Term function v)

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

(Read function, Read v) => Read (Term function v)

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)

Methods

showsPrec :: Int -> Term function v -> ShowS

show :: Term function v -> String

showList :: [Term function v] -> ShowS

(IsVariable v, IsFunction function) => IsString (Term function v)

Methods

fromString :: String -> Term function v

IsTerm (Term function v) => Pretty (Term function v)

Methods

pPrintPrec :: PrettyLevel -> Rational -> Term function v -> Doc

pPrint :: Term function v -> Doc

pPrintList :: PrettyLevel -> [Term function v] -> Doc

(IsFunction function, IsVariable v) => HasFixity (Term function v)

Methods

precedence :: Term function v -> Precedence

associativity :: Term function v -> Associativity

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

Associated Types

type TVarOf (Term function v) :: *

type FunOf (Term function v) :: *

Methods

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

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

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

type TVarOf (Term function v)

type TVarOf (Term function v) = v

type FunOf (Term function v)

type FunOf (Term function v) = function

type UTermOf (SkAtom, SkAtom)

type UTermOf (SkAtom, SkAtom) = TermOf SkAtom

type FTerm = Term FName V

A term type with no Skolem functions

testTerm :: Test