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) ++ ")"