FirstOrderTheory.Syntax

Documentation

data Literal

Instances

Eq Literal

Ord Literal

Show Literal

data Atom

Instances

Eq Atom

Ord Atom

Show Atom

data Term

Instances

Eq Term

Ord Term

Show Term

atomArgs :: Atom -> [Term]

Return the terms that are arguments to the predicate of the input atom

predicateName :: Atom -> Name

Return the name of the predicate of the input atom

isFunctionWithName :: Name -> Term -> Bool

Returns True if the input term is a function with the give name, and false otherwise

isNeg :: Literal -> Bool

Returns false if the literal is an atomic formula and true if the literal is the negation of an atomic formula

getAtom :: Literal -> Atom

Returns the atomic formula of the given literal

varName :: Term -> Name

Return the name of the input variable, throws error if input term is not a variable

intVal :: Term -> Int

Returns the integer value of an Integer constant or an error if the input is not an integer

funcArgs :: Term -> [Term]

Returns the input function's argument list, throws error if input term is not a function

lit :: Atom -> Literal

nLit :: Atom -> Literal

atom :: Name -> [Term] -> Atom

Returns a new atom

func :: Name -> [Term] -> Term

var :: Name -> Term

intConst :: Int -> Term