-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Grammar and typeclass for first order theories
--   
--   Grammar and typeclass for first order theories
@package FirstOrderTheory
@version 0.1.0.4

module FirstOrderTheory.Utils
type Name = String
type Arity = Int
type Sort = String

-- | Make a new sort with the input name
sort :: String -> Sort

module FirstOrderTheory.Syntax
data Literal
data Atom
data Term

-- | Return the terms that are arguments to the predicate of the input atom
atomArgs :: Atom -> [Term]

-- | Return the name of the predicate of the input atom
predicateName :: Atom -> Name

-- | Returns True if the input term is a function with the give name, and
--   false otherwise
isFunctionWithName :: Name -> Term -> Bool

-- | Returns false if the literal is an atomic formula and true if the
--   literal is the negation of an atomic formula
isNeg :: Literal -> Bool

-- | Returns the atomic formula of the given literal
getAtom :: Literal -> Atom

-- | Return the name of the input variable, throws error if input term is
--   not a variable
varName :: Term -> Name

-- | Returns the integer value of an Integer constant or an error if the
--   input is not an integer
intVal :: Term -> Int

-- | Returns the input function's argument list, throws error if input term
--   is not a function
funcArgs :: Term -> [Term]
lit :: Atom -> Literal
nLit :: Atom -> Literal

-- | Returns a new atom
atom :: Name -> [Term] -> Atom
func :: Name -> [Term] -> Term
var :: Name -> Term
intConst :: Int -> Term
instance Eq Term
instance Ord Term
instance Eq Atom
instance Ord Atom
instance Eq Literal
instance Ord Literal
instance Show Term
instance Show Atom
instance Show Literal

module FirstOrderTheory.Theory

-- | Description of a decidable first order theory
class FirstOrderTheory t
theoryName :: FirstOrderTheory t => t -> String
sorts :: FirstOrderTheory t => t -> Set Sort
predicates :: FirstOrderTheory t => t -> Set PredicateDecl
functions :: FirstOrderTheory t => t -> Set FunctionDecl
decideSat :: FirstOrderTheory t => t -> Set Literal -> (Bool, Set Literal)
data PredicateDecl
data FunctionDecl

-- | Specify a new predicate declaration
predicateDecl :: Name -> Arity -> [Sort] -> PredicateDecl

-- | Specify a new function declaration
functionDecl :: Name -> Arity -> [Sort] -> Sort -> FunctionDecl
instance Eq PredicateDecl
instance Ord PredicateDecl
instance Eq FunctionDecl
instance Ord FunctionDecl