module FirstOrderTheory.Syntax( Literal, Atom, Term, NNFFormula, nnfLit, nnfCon, nnfDis, toPropositionalCNF, negateLit, atomArgs, predicateName, isFunctionWithName, isNeg, getAtom, varName, intVal, funcArgs, lit, nLit, atom, func, var, intConst) where import Data.List as L import Proper.CNF import Proper.Formula import FirstOrderTheory.Utils -- |A quantifier free formla in negation normal form data NNFFormula = Con NNFFormula NNFFormula | Dis NNFFormula NNFFormula | LF Literal deriving (Eq, Ord, Show) -- |Returns a NNF Formula consisting of only the input literal nnfLit :: Literal -> NNFFormula nnfLit l = LF l -- |Returns the conjunction of two NNF formulas nnfCon l r = Con l r -- |Return the disjunction of two NNF formulas nnfDis l r = Dis l r -- | Convert NNFFormula to propositional formula in -- conjunctive normal form toPropositionalCNF :: NNFFormula -> CNF Literal toPropositionalCNF formula = toCNF \$ toProperFormula formula toProperFormula :: NNFFormula -> Formula Literal toProperFormula (LF l) = val l toProperFormula (Con l r) = con (toProperFormula l) (toProperFormula r) toProperFormula (Dis l r) = dis (toProperFormula l) (toProperFormula l) data Literal = Lit Atom | Neg Atom deriving (Eq, Ord) lit = Lit nLit = Neg -- |Returns false if the literal is an atomic formula and true if the -- literal is the negation of an atomic formula isNeg :: Literal -> Bool isNeg (Neg _) = True isNeg _ = False -- |Return the negation of the input literal negateLit (Lit a) = Neg a negateLit (Neg a) = Lit a -- |Returns the atomic formula of the given literal getAtom :: Literal -> Atom getAtom (Neg a) = a getAtom (Lit a) = a instance Show Literal where show (Lit p) = show p show (Neg p) = "~" ++ show p data Atom = Atom Name [Term] deriving (Eq, Ord) -- |Returns a new atom atom = Atom -- |Return the terms that are arguments to the predicate of the input atom atomArgs (Atom _ args) = args -- |Return the name of the predicate of the input atom predicateName (Atom n _) = n instance Show Atom where show (Atom name args) = name ++ "[" ++ (L.intercalate ", " \$ L.map show args) ++ "]" data Term = Function Name [Term] | Variable Name | Integer Int deriving (Eq, Ord) func = Function var = Variable intConst = Integer -- |Returns True if the input term is a function with the give name, -- and false otherwise isFunctionWithName n (Function m _) = n == m isFunctionWithName _ _ = False -- |Return the name of the input variable, -- throws error if input term is not a variable varName (Variable n) = n -- |Returns the input function's argument list, -- throws error if input term is not a function funcArgs (Function _ args) = args -- |Returns the integer value of an Integer constant or an error -- if the input is not an integer intVal (Integer i) = i instance Show Term where show (Integer val) = show val show (Variable name) = name show (Function name args) = name ++ "(" ++ (L.intercalate ", " \$ L.map show args) ++ ")"