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

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

IsVariable V

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

Return an infinite list of variations on v

newtype V

Constructors

V String

Instances

Eq V

Data V

Ord V

Read V

Show V

IsString V

Pretty V

IsVariable V

JustApply ApAtom

IsFirstOrder EqFormula

IsFirstOrder ApFormula

IsFirstOrder Formula

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

Ord FName

Show FName

IsString FName

Pretty FName

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

Unify (SkAtom, SkAtom)

type TVarOf (Term function v) = v

type FunOf (Term function v) = function

type UTermOf (SkAtom, SkAtom) = TermOf SkAtom

type FTerm = Term FName V

A term type with no Skolem functions

testTerm :: Test