-- 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.6

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

-- | A quantifier free formla in negation normal form
data NNFFormula

-- | Returns a NNF Formula consisting of only the input literal
nnfLit :: Literal -> NNFFormula

-- | Returns the conjunction of two NNF formulas
nnfCon :: NNFFormula -> NNFFormula -> NNFFormula

-- | Return the disjunction of two NNF formulas
nnfDis :: NNFFormula -> NNFFormula -> NNFFormula

-- | Convert NNFFormula to propositional formula in conjunctive normal form
toPropositionalCNF :: NNFFormula -> CNF Literal

-- | Return the negation of the input literal
negateLit :: Literal -> Literal

-- | 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 Eq NNFFormula
instance Ord NNFFormula
instance Show NNFFormula
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

-- | Returns a NNF Formula consisting of only the input literal
nnfLit :: Literal -> NNFFormula

-- | Returns the conjunction of two NNF formulas
nnfCon :: NNFFormula -> NNFFormula -> NNFFormula

-- | Return the disjunction of two NNF formulas
nnfDis :: NNFFormula -> NNFFormula -> NNFFormula

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