module AbsHOL where

-- Haskell module generated by the BNF converter

newtype Idents = Idents String deriving (Eq,Ord,Show)
newtype PredId = PredId String deriving (Eq,Ord,Show)
newtype FunctId = FunctId String deriving (Eq,Ord,Show)
data PROGRAM =
   PROGRAM [SENT]
  deriving (Eq,Ord,Show)

data DEF =
   DefSent Idents SENT
  deriving (Eq,Ord,Show)

data SENT =
   ASentPred PredId [TERMS]
 | TrueSent
 | FalseSent
 | IdentSent Idents
 | ASentEq TERM TERM
 | NegSent SENT
 | IfSent SENT SENT SENT
 | AndSent SENT SENT
 | OrSent SENT SENT
 | ImpSent SENT SENT
 | LetSent [DEF] SENT
 | ForallSent [TERM] SENT
 | ExistsSent [TERM] SENT
  deriving (Eq,Ord,Show)

data TERM =
   FunctTerm FunctId [TERMS]
 | ConstVarTerm Idents
  deriving (Eq,Ord,Show)

data TERMS =
   Terms [TERM]
  deriving (Eq,Ord,Show)