content: {- |
  Module      :  ./TPTP/Parse.hs
  Description :  A Parser for the TPTP Syntax v6.4.0.11
  Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Eugen Kuksa <kuksa@iks.cs.ovgu.de>
  Stability   :  provisional
  Portability :  portable
  
  A Parser for the TPTP Input Syntax v6.4.0.11 taken from
  <http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>
  
  References
  
  [1] G. Sutcliffe et al.: The TPTP language grammar in BNF.
      <http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>
  
      Note: The implemented version is saved at TPTP/Documents/SyntaxBNF.html
  
      Note: The names of the data types are aligned with the names of the
      grammar rules at this reference page (modulo case).
  -}
  
  module TPTP.Parser ( parseBasicSpec
                     , annotated_formula
                     ) where
  
  import TPTP.AS hiding (name, formulaRole, annotations)
  import TPTP.Common
  
  import qualified Common.AnnoState as AnnoState
  import qualified Common.AS_Annotation as Annotation
  import Common.DebugParser
  import Common.GlobalAnnotations (PrefixMap)
  import Common.Id (Token (..))
  import Common.IRI (IRI (..), iriCurie)
  import qualified Common.Lexer as Lexer (pToken)
  import Common.Parsec
  
  import Control.Monad (liftM)
  import qualified Control.Monad.Fail as Fail
  import Data.Char (isAlphaNum, isSpace, ord)
  import Prelude hiding (exp, exponent)
  import Text.ParserCombinators.Parsec
  
  {- -----------------------------------------------------------------------------
  Debug
  ----------------------------------------------------------------------------- -}
  
  parserTrace :: String -> CharParser st a -> CharParser st a
  parserTrace = parserTraceId
  
  {- -----------------------------------------------------------------------------
  Logic components
  ----------------------------------------------------------------------------- -}
  
  parseBasicSpec :: PrefixMap -> AnnoState.AParser st BASIC_SPEC
  parseBasicSpec _ = parserTrace "parseBasicSpec" (liftM Basic_spec (many1 $ AnnoState.allAnnoParser tptp_file)
    <|> do
      file <- tptp_file
      return $ Basic_spec [Annotation.emptyAnno file]
    )
  
  {- -----------------------------------------------------------------------------
  Files. Empty file is OK
  ----------------------------------------------------------------------------- -}
  
  -- <TPTP_file>            ::= <TPTP_input>*
  tptp_file :: CharParser st TPTP
  tptp_file = parserTrace "tptp_file" (do
      skip
      inputs <- many1 tptp_input
      return $ TPTP inputs
    <?> "TPTP_file"
    )
  
  -- <TPTP_input>           ::= <annotated_formula> | <include>
  tptp_input :: CharParser st TPTP_input
  tptp_input = parserTrace "tptp_input" (
    skip >> (liftM Annotated_formula annotated_formula
      <|> liftM TPTP_include include
      <|> liftM TPTP_system_comment system_comment
      <|> liftM TPTP_defined_comment defined_comment
      <|> liftM TPTP_comment comment
      <?> "TPTP_input")
    )
  
  {- -----------------------------------------------------------------------------
  Formula records
  ----------------------------------------------------------------------------- -}
  
  -- <annotated_formula>    ::= <thf_annotated> | <tfx_annotated> | <tff_annotated> |
  --                            <tcf_annotated> | <fof_annotated> | <cnf_annotated> |
  --                            <tpi_annotated>
  annotated_formula :: CharParser st Annotated_formula
  annotated_formula = parserTrace "annotated_formula" (
    skip >> (thf_annotated
      <|> tfx_annotated
      <|> tff_annotated
      <|> tcf_annotated
      <|> fof_annotated
      <|> cnf_annotated
      <|> tpi_annotated
      <?> "annotated_formula")
    )
  
  -- <tpi_annotated>        ::= tpi(<name>,<formula_role>,<tpi_formula><annotations>).
  tpi_annotated :: CharParser st Annotated_formula
  tpi_annotated = parserTrace "tpi_annotated" (formulaAnnotated "tpi" tpi_formula
    (\ n r f a -> AF_TPI_Annotated $ TPI_annotated n r f a)
    )
  
  -- <tpi_formula>          ::= <fof_formula>
  tpi_formula :: CharParser st TPI_formula
  tpi_formula = parserTrace "tpi_formula" (fof_formula <?> "tpi_formula"
    )
  
  -- <thf_annotated>        ::= thf(<name>,<formula_role>,<thf_formula>
  --                            <annotations>).
  thf_annotated :: CharParser st Annotated_formula
  thf_annotated = parserTrace "thf_annotated" (formulaAnnotated "thf" thf_formula
    (\ n r f a -> AF_THF_Annotated $ THF_annotated n r f a)
    )
  
  -- <tfx_annotated>        ::= tfx(<name>,<formula_role>,<tfx_formula>
  --                            <annotations>).
  tfx_annotated :: CharParser st Annotated_formula
  tfx_annotated = parserTrace "tfx_annotated" (formulaAnnotated "tfx" tfx_formula
    (\ n r f a -> AF_TFX_Annotated $ TFX_annotated n r f a)
    )
  
  -- <tff_annotated>        ::= tff(<name>,<formula_role>,<tff_formula>
  --                            <annotations>).
  tff_annotated :: CharParser st Annotated_formula
  tff_annotated = parserTrace "tff_annotated" (formulaAnnotated "tff" tff_formula
    (\ n r f a -> AF_TFF_Annotated $ TFF_annotated n r f a)
    )
  
  -- <tcf_annotated>        ::= tcf(<name>,<formula_role>,<tcf_formula>
  --                            <annotations>).
  tcf_annotated :: CharParser st Annotated_formula
  tcf_annotated = parserTrace "tcf_annotated" (formulaAnnotated "tcf" tcf_formula
    (\ n r f a -> AF_TCF_Annotated $ TCF_annotated n r f a)
    )
  
  -- <fof_annotated>        ::= fof(<name>,<formula_role>,<fof_formula>
  --                            <annotations>).
  fof_annotated :: CharParser st Annotated_formula
  fof_annotated = parserTrace "fof_annotated" (formulaAnnotated "fof" fof_formula
    (\ n r f a -> AF_FOF_Annotated $ FOF_annotated n r f a)
    )
  
  -- <cnf_annotated>        ::= cnf(<name>,<formula_role>,<cnf_formula>
  --                            <annotations>).
  cnf_annotated :: CharParser st Annotated_formula
  cnf_annotated = parserTrace "cnf_annotated" (formulaAnnotated "cnf" cnf_formula
    (\ n r f a -> AF_CNF_Annotated $ CNF_annotated n r f a)
    )
  
  formulaAnnotated :: String
                   -> CharParser st a
                   -> (Name -> Formula_role -> a -> Annotations -> Annotated_formula)
                   -> CharParser st Annotated_formula
  formulaAnnotated keyword formula constructor = do
    strTok keyword
    (n, r, f, a) <- parens (do
      n <- name
      commaT
      r <- formula_role
      commaT
      f <- formula
      a <- annotations
      return (n, r, f, a))
    dotT
    return $ constructor n r f a
  
  -- <annotations>          ::= ,<source><optional_info> | <null>
  annotations :: CharParser st Annotations
  annotations = parserTrace "annotations" (liftM Annotations annotations' <?> "annotations"
    )
    where
      annotations' = optionMaybe $ do
        commaT
        s <- source
        oi <- optional_info
        return (s, oi)
  
  {- -----------------------------------------------------------------------------
  Types for problems.
  ----------------------------------------------------------------------------- -}
  
  -- %----Types for problems.
  -- %----Note: The previous <source_type> from ...
  -- %----   <formula_role> ::= <user_role>-<source>
  -- %----... is now gone. Parsers may choose to be tolerant of it for backwards
  -- %----compatibility.
  -- <formula_role>         ::= <lower_word>
  -- <formula_role>         :== axiom | hypothesis | definition | assumption |
  --                            lemma | theorem | corollary | conjecture |
  --                            negated_conjecture | plain | type |
  --                            fi_domain | fi_functors | fi_predicates | unknown
  formula_role :: CharParser st Formula_role
  formula_role = parserTrace "formula_role" (constantsChoice
     [("axiom", Axiom),
      ("hypothesis", Hypothesis),
      ("definition", Definition),
      ("assumption", Assumption),
      ("lemma", Lemma),
      ("theorem", Theorem),
      ("corollary", Corollary),
      ("conjecture", Conjecture),
      ("negated_conjecture", Negated_conjecture),
      ("plain", Plain),
      ("type", Type),
      ("fi_domain", Fi_domain),
      ("fi_functors", Fi_functors),
      ("fi_predicates", Fi_predicates),
      ("unknown", Unknown)]
     <?> "formula_role"
    )
  
  
  
  {- -----------------------------------------------------------------------------
  THF formulae
  ----------------------------------------------------------------------------- -}
  -- <thf_formula>          ::= <thf_logic_formula> | <thf_sequent>
  thf_formula :: CharParser st THF_formula
  thf_formula = parserTrace "thf_formula" (liftM THFF_logic thf_logic_formula
    <|> liftM THFF_sequent thf_sequent
    <?> "thf_formula"
    )
  
  -- <thf_logic_formula>    ::= <thf_binary_formula> | <thf_unitary_formula> |
  --                            <thf_type_formula> | <thf_subtype>
  thf_logic_formula :: CharParser st THF_logic_formula
  thf_logic_formula = parserTrace "thf_logic_formula" (
    liftM THFLF_type thf_type_formula
    <|> do
      f <- thf_unitary_formula
      (liftM THFLF_binary (thf_binary_formula f)
        <|> return (THFLF_unitary f))
    <|> liftM THFLF_subtype thf_subtype
    <?> "thf_logic_formula"
    )
  
  -- <thf_binary_formula>   ::= <thf_binary_pair> | <thf_binary_tuple>
  thf_binary_formula :: THF_unitary_formula -> CharParser st THF_binary_formula
  thf_binary_formula f = parserTrace "thf_binary_formula" (
    liftM THFBF_pair (thf_binary_pair f)
    <|> liftM THFBF_tuple (thf_binary_tuple f)
    <?> "thf_binary_formula"
    )
  
  -- <thf_binary_pair>      ::= <thf_unitary_formula> <thf_pair_connective>
  --                            <thf_unitary_formula>
  thf_binary_pair :: THF_unitary_formula -> CharParser st THF_binary_pair
  thf_binary_pair f1 = parserTrace "thf_binary_pair" (do
      pc <- try thf_pair_connective
      f2 <- thf_unitary_formula
      return $ THF_binary_pair pc f1 f2
    <?> "thf_binary_pair"
    )
  
  -- <thf_binary_tuple>     ::= <thf_or_formula> | <thf_and_formula> |
  --                            <thf_apply_formula>
  thf_binary_tuple :: THF_unitary_formula -> CharParser st THF_binary_tuple
  thf_binary_tuple f = parserTrace "thf_binary_tuple" (
    (liftM THFBT_or (thf_or_formula f)
     <|> liftM THFBT_and (thf_and_formula f)
     <|> liftM THFBT_apply (thf_apply_formula f))
    <?> "thf_binary_tuple"
    )
  
  -- <thf_or_formula>       ::= <thf_unitary_formula> <vline> <thf_unitary_formula> |
  --                            <thf_or_formula> <vline> <thf_unitary_formula>
  thf_or_formula :: THF_unitary_formula -> CharParser st THF_or_formula
  thf_or_formula f = parserTrace "thf_or_formula" (do
      try vline
      fs <- thf_unitary_formula `sepBy1` vline
      return $ f : fs
    <?> "thf_or_formula"
    )
  
  -- <thf_and_formula>      ::= <thf_unitary_formula> & <thf_unitary_formula> |
  --                            <thf_and_formula> & <thf_unitary_formula>
  thf_and_formula :: THF_unitary_formula -> CharParser st THF_and_formula
  thf_and_formula f = parserTrace "thf_and_formula" (do
      try andT
      fs <- thf_unitary_formula `sepBy1` andT
      return $ f : fs
    <?> "thf_and_formula"
    )
  
  -- <thf_apply_formula>    ::= <thf_unitary_formula> @ <thf_unitary_formula> |
  --                            <thf_apply_formula> @ <thf_unitary_formula>
  thf_apply_formula :: THF_unitary_formula -> CharParser st THF_apply_formula
  thf_apply_formula f = parserTrace "thf_apply_formula" (do
      try $ charTok '@'
      fs <- thf_unitary_formula `sepBy1` charTok '@'
      return $ f : fs
    <?> "thf_apply_formula"
    )
  
  -- <thf_unitary_formula>  ::= <thf_quantified_formula> | <thf_unary_formula> |
  --                            <thf_atom> | <thf_conditional> | <thf_let> |
  --                            <thf_tuple> | (<thf_logic_formula>)
  thf_unitary_formula :: CharParser st THF_unitary_formula
  thf_unitary_formula = parserTrace "thf_unitary_formula" (
    liftM THFUF_logic (parens thf_logic_formula)
    <|> liftM THFUF_quantified thf_quantified_formula
    <|> liftM THFUF_unary thf_unary_formula
    <|> liftM THFUF_conditional thf_conditional
    <|> liftM THFUF_let thf_let
    <|> liftM THFUF_atom thf_atom
    <|> liftM THFUF_tuple thf_tuple
    <?> "thf_unitary_formula"
    )
  
  -- <thf_quantified_formula> ::= <thf_quantification> <thf_unitary_formula>
  thf_quantified_formula :: CharParser st THF_quantified_formula
  thf_quantified_formula = parserTrace "thf_quantified_formula" (do
      q <- thf_quantification
      f <- thf_unitary_formula
      return $ THF_quantified_formula q f
    <?> "thf_quantified_formula"
    )
  
  -- <thf_quantification>   ::= <thf_quantifier> [<thf_variable_list>] :
  -- %----@ (denoting apply) is left-associative and lambda is right-associative.
  -- %----^ [X] : ^ [Y] : f @ g (where f is a <thf_apply_formula> and g is a
  -- %----<thf_unitary_formula>) should be parsed as: (^ [X] : (^ [Y] : f)) @ g.
  -- %----That is, g is not in the scope of either lambda.
  thf_quantification :: CharParser st THF_quantification
  thf_quantification = parserTrace "thf_quantification" (do
      q <- try thf_quantifier
      vars <- brackets thf_variable_list
      colonT
      return $ THF_quantification q vars
    <?> "thf_quantification"
    )
  
  -- <thf_variable_list>    ::= <thf_variable> | <thf_variable>,<thf_variable_list>
  thf_variable_list :: CharParser st THF_variable_list
  thf_variable_list = parserTrace "thf_variable_list" (sepByComma1 thf_variable <?> "thf_variable_list"
    )
  
  -- <thf_variable>         ::= <thf_typed_variable> | <variable>
  thf_variable :: CharParser st THF_variable
  thf_variable = parserTrace "thf_variable" (liftM THFV_typed thf_typed_variable <|> liftM THFV_variable variable
    <?> "thf_variable"
    )
  
  -- <thf_typed_variable>   ::= <variable> : <thf_top_level_type>
  thf_typed_variable :: CharParser st THF_typed_variable
  thf_typed_variable = parserTrace "thf_typed_variable" (do
      v <- try (variable << colonT)
      tlt <- thf_top_level_type
      return $ THF_typed_variable v tlt
    <?> "thf_typed_variable"
    )
  
  -- %----Unary connectives bind more tightly than binary. The negated formula
  -- %----must be ()ed because a ~ is also a term.
  -- <thf_unary_formula>    ::= <thf_unary_connective> (<thf_logic_formula>)
  thf_unary_formula :: CharParser st THF_unary_formula
  thf_unary_formula = parserTrace "thf_unary_formula" (do
      uc <- try (thf_unary_connective << oParenT)
      arg <- thf_logic_formula << cParenT
      return $ THF_unary_formula uc arg
    <?> "thf_unary_formula"
    )
  
  -- <thf_atom>             ::= <thf_function> | <variable> | <defined_term> |
  --                            <thf_conn_term>
  thf_atom :: CharParser st THF_atom
  thf_atom = parserTrace "thf_atom" (
    liftM THF_atom_function thf_function
    <|> liftM THF_atom_variable variable
    <|> liftM THF_atom_defined defined_term
    <|> liftM THF_atom_conn thf_conn_term
    <?> "thf_atom"
    )
  
  -- <thf_function>         ::= <thf_plain_term> | <thf_defined_term> |
  --                            <thf_system_term>
  -- <thf_function>         ::= <atom> | <functor>(<thf_arguments>) |
  --                            <defined_functor>(<thf_arguments>) |
  --                            <system_functor>(<thf_arguments>)
  thf_function :: CharParser st THF_function
  thf_function = parserTrace "thf_function" (do
      f <- try (functor << oParenT)
      args <- thf_arguments
      return $ THFF_functor f args
    <|> liftM THFF_atom atom
    <|> do
      f <- try (defined_functor << oParenT)
      args <- thf_arguments
      return $ THFF_defined f args
    <|> do
      f <- try (system_functor << oParenT)
      args <- thf_arguments
      return $ THFF_system f args
    <?> "thf_function"
    )
  
  -- <thf_conn_term>        ::= <thf_pair_connective> | <assoc_connective> |
  --                            <thf_unary_connective>
  thf_conn_term :: CharParser st THF_conn_term
  thf_conn_term = parserTrace "thf_conn_term" (
    liftM THFC_pair thf_pair_connective
    <|> liftM THFC_assoc assoc_connective
    <|> liftM THFC_unary thf_unary_connective
    <?> "thf_conn_term"
    )
  
  -- <thf_conditional>      ::= $ite(<thf_logic_formula>,<thf_logic_formula>,
  --                             <thf_logic_formula>)
  thf_conditional :: CharParser st THF_conditional
  thf_conditional = parserTrace "thf_conditional" (do
      try (strTok "$ite" << oParenT)
      lf_if <- thf_logic_formula
      commaT
      lf_then <- thf_logic_formula
      commaT
      lf_else <- thf_logic_formula
      cParenT
      return $ THF_conditional lf_if lf_then lf_else
    <?> "thf_conditional"
    )
  
  -- <thf_let>              ::= $let(<thf_unitary_formula>,<thf_formula>)
  -- <thf_let>              :== $let(<thf_let_defns>,<thf_formula>)
  thf_let :: CharParser st THF_let
  thf_let = parserTrace "thf_let" (do
    try (strTok "$let" << oParenT)
    lds <- thf_let_defns
    commaT
    f <- thf_formula
    return $ THF_let lds f
    <?> "thf_let"
    )
  
  -- <thf_let_defns>        :== <thf_let_defn> | [<thf_let_defn_list>]
  thf_let_defns :: CharParser st THF_let_defns
  thf_let_defns = parserTrace "thf_let_defns" (
    liftM THFLD_many (brackets thf_let_defn_list)
    <|> liftM THFLD_single thf_let_defn
    <?> "thf_let_defns"
    )
  
  -- <thf_let_defn_list>    :== <thf_let_defn> | <thf_let_defn>,<thf_let_defn_list>
  thf_let_defn_list :: CharParser st THF_let_defn_list
  thf_let_defn_list = parserTrace "thf_let_defn_list" (
    sepByComma1 thf_let_defn
    <?> "thf_let_defn_list"
    )
  
  -- <thf_let_defn>         :== <thf_let_quantified_defn> | <thf_let_plain_defn>
  thf_let_defn :: CharParser st THF_let_defn
  thf_let_defn = parserTrace "thf_let_defn" (
    liftM THFLD_quantified thf_let_quantified_defn
    <|> liftM THFLD_plain thf_let_plain_defn
    <?> "thf_let_defn"
    )
  
  -- <thf_let_quantified_defn> :== <thf_quantification> (<thf_let_plain_defn>)
  thf_let_quantified_defn :: CharParser st THF_let_quantified_defn
  thf_let_quantified_defn = parserTrace "thf_let_quantified_defn" (do
      q <- thf_quantification
      lpd <- parens thf_let_plain_defn
      return $ THF_let_quantified_defn q lpd
    <?> "thf_let_quantified_defn"
    )
  
  -- <thf_let_plain_defn>   :== <thf_let_defn_LHS> <assignment> <thf_formula>
  thf_let_plain_defn :: CharParser st THF_let_plain_defn
  thf_let_plain_defn = parserTrace "thf_let_plain_defn" (do
      lhs <- thf_let_defn_LHS
      assignment
      f <- thf_formula
      return $ THF_let_plain_defn lhs f
    <?> "thf_let_plain_defn"
    )
  
  -- <thf_let_defn_LHS>     :== <thf_plain_term> | <thf_tuple>
  -- <thf_let_defn_LHS>     :== <constant> | <functor>(<fof_arguments>) |
  --                            <thf_tuple>
  -- %----The <fof_arguments> must all be <variable>s, and the <thf_tuple> may
  -- %----contain only <constant>s and <functor>(<fof_arguments>)s
  thf_let_defn_LHS :: CharParser st THF_let_defn_LHS
  thf_let_defn_LHS = parserTrace "thf_let_defn_LHS" (liftM THFLDL_tuple thf_tuple
    <|> do
      f <- try (functor << oParenT)
      args <- fof_arguments
      if onlyVariables args
      then return $ THFLDL_functor f args
      else Fail.fail "thf_let_defn_LHS: The <fof_arguments> must all be <variable>s."
    <|> liftM THFLDL_constant constant
    <?> "thf_let_defn_LHS"
    )
    where
      onlyVariables :: FOF_arguments -> Bool
      onlyVariables = all isVariable
  
      isVariable :: FOF_term -> Bool
      isVariable t = case t of
        FOFT_variable _ -> True
        _ -> False
  
  -- <thf_arguments>        ::= <thf_formula_list>
  thf_arguments :: CharParser st THF_arguments
  thf_arguments = parserTrace "thf_arguments" (thf_formula_list <?> "thf_arguments"
    )
  
  -- The thf_type_formula rule is ambiguous in the following.
  -- Here, it is split into
  -- thf_type_formula_typeable and
  -- thf_type_formula_constant
  -- <thf_type_formula>     ::= <thf_typeable_formula> : <thf_top_level_type>
  -- <thf_type_formula>     :== <constant> : <thf_top_level_type>
  thf_type_formula :: CharParser st THF_type_formula
  thf_type_formula = parserTrace "thf_type_formula" (thf_type_formula_constant <|> thf_type_formula_typeable
    <?> "thf_type_formula"
    )
    where
      -- <thf_type_formula>     ::= <thf_typeable_formula> : <thf_top_level_type>
      thf_type_formula_typeable :: CharParser st THF_type_formula
      thf_type_formula_typeable = parserTrace "thf_type_formula_typeable" (do
          tf <- try (thf_typeable_formula << colonT)
          tlt <- thf_top_level_type
          return $ THFTF_typeable tf tlt
        <?> "thf_type_formula"
        )
  
      -- <thf_type_formula>     :== <constant> : <thf_top_level_type>
      thf_type_formula_constant :: CharParser st THF_type_formula
      thf_type_formula_constant = parserTrace "thf_type_formula_constant" (do
          c <- try (constant << colonT)
          tlt <- thf_top_level_type
          return $ THFTF_constant c tlt
        <?> "thf_type_formula"
        )
  
  -- <thf_typeable_formula> ::= <thf_atom> | (<thf_logic_formula>)
  thf_typeable_formula :: CharParser st THF_typeable_formula
  thf_typeable_formula = parserTrace "thf_typeable_formula" (
    liftM THFTF_logic (parens thf_logic_formula) <|> liftM THFTF_atom (thf_atom)
    <?> "thf_typeable_formula"
    )
  
  -- <thf_subtype>          ::= <thf_atom> <subtype_sign> <thf_atom>
  thf_subtype :: CharParser st THF_subtype
  thf_subtype = parserTrace "thf_subtype" ((do
    c1 <- try (thf_atom << subtype_sign)
    c2 <- thf_atom
    return $ THF_subtype c1 c2)
    <?> "thf_subtype"
    )
  
  
  -- %----<thf_top_level_type> appears after ":", where a type is being specified
  -- %----for a term or variable. <thf_unitary_type> includes <thf_unitary_formula>,
  -- %----so the syntax allows just about any lambda expression with "enough"
  -- %----parentheses to serve as a type. The expected use of this flexibility is
  -- %----parametric polymorphism in types, expressed with lambda abstraction.
  -- %----Mapping is right-associative: o > o > o means o > (o > o).
  -- %----Xproduct is left-associative: o * o * o means (o * o) * o.
  -- %----Union is left-associative: o + o + o means (o + o) + o.
  -- <thf_top_level_type>   ::= <thf_unitary_type> | <thf_mapping_type>
  thf_top_level_type :: CharParser st THF_top_level_type
  thf_top_level_type = parserTrace "thf_top_level_type" (
    liftM THFTLT_mapping thf_mapping_type
    <|> liftM THFTLT_unitary thf_unitary_type
    <?> "thf_top_level_type"
    )
  
  -- <thf_unitary_type>     ::= <thf_unitary_formula> | (<thf_binary_type>)
  thf_unitary_type :: CharParser st THF_unitary_type
  thf_unitary_type = parserTrace "thf_unitary_type" (
    liftM THFUT_binary (parens thf_binary_type)
    <|> liftM THFUT_unitary thf_unitary_formula
    <?> "thf_unitary_type"
    )
  
  -- <thf_binary_type>      ::= <thf_mapping_type> | <thf_xprod_type> |
  --                            <thf_union_type>
  thf_binary_type :: CharParser st THF_binary_type
  thf_binary_type = parserTrace "thf_binary_type" (
    liftM THFBT_mapping thf_mapping_type
    <|> liftM THFBT_xprod thf_xprod_type
    <|> liftM THFBT_union thf_union_type
    <?> "thf_binary_type"
    )
  
  -- <thf_mapping_type>     ::= <thf_unitary_type> <arrow> <thf_unitary_type> |
  --                            <thf_unitary_type> <arrow> <thf_mapping_type>
  thf_mapping_type :: CharParser st THF_mapping_type
  thf_mapping_type = parserTrace "thf_mapping_type" (do
      t <- try (thf_unitary_type << arrowT)
      ts <- thf_unitary_type `sepBy1` arrowT
      return $ t : ts
    <?> "thf_mapping_type"
    )
  
  -- <thf_xprod_type>       ::= <thf_unitary_type> <star> <thf_unitary_type> |
  --                            <thf_xprod_type> <star> <thf_unitary_type>
  thf_xprod_type :: CharParser st THF_xprod_type
  thf_xprod_type = parserTrace "thf_xprod_type" (do
      t <- try (thf_unitary_type << starT)
      ts <- thf_unitary_type `sepBy1` starT
      return $ t : ts
    <?> "thf_xprod_type"
    )
  
  -- <thf_union_type>       ::= <thf_unitary_type> <plus> <thf_unitary_type> |
  --                            <thf_union_type> <plus> <thf_unitary_type>
  thf_union_type :: CharParser st THF_union_type
  thf_union_type = parserTrace "thf_union_type" (do
      t <- try (thf_unitary_type << plusT)
      ts <- thf_unitary_type `sepBy1` plusT
      return $ t : ts
    <?> "thf_union_type"
    )
  
  -- <thf_sequent>          ::= <thf_tuple> <gentzen_arrow> <thf_tuple> |
  --                            (<thf_sequent>)
  thf_sequent :: CharParser st THF_sequent
  thf_sequent = parserTrace "thf_sequent" (do
      t1 <- try (thf_tuple << gentzen_arrow)
      t2 <- thf_tuple
      return $ THFS_plain t1 t2
    <|> liftM THFS_parens (parens thf_sequent)
    <?> "thf_sequent"
    )
  
  -- <thf_tuple>            ::= [] | [<thf_formula_list>]
  thf_tuple :: CharParser st THF_tuple
  thf_tuple = parserTrace "thf_tuple" (
    liftM THF_tuple (emptyBrackets <|> brackets thf_formula_list)
    <?> "thf_tuple"
    )
  
  -- <thf_formula_list>     ::= <thf_logic_formula> |
  --                            <thf_logic_formula>,<thf_formula_list>
  thf_formula_list :: CharParser st THF_formula_list
  thf_formula_list = parserTrace "thf_formula_list" (sepByComma1 thf_logic_formula <?> "thf_formula_list"
    )
  
  
  -- NOTE: not used
  -- %----New material for modal logic semantics, not integrated yet
  -- -- <logic_defn_rule>      :== <logic_defn_LHS> <assignment> <logic_defn_RHS>
  -- logic_defn_rule :: CharParser st Logic_defn_rule
  -- logic_defn_rule = (do
  --   lhs <- logic_defn_LHS
  --   assignment
  --   rhs <- logic_defn_RHS
  --   return $ Logic_defn_rule lhs rhs)
  --   <?> "logic_defn_rule"
  --
  -- NOTE: not used
  -- -- <logic_defn_LHS>       :== <logic_defn_value> | <thf_top_level_type>  | <name>
  -- -- <logic_defn_LHS>       :== $constants | $quantification | $consequence |
  -- --                            $modalities
  -- logic_defn_LHS :: CharParser st Logic_defn_LHS
  -- logic_defn_LHS = (constantsChoice
  --   [("$constants", LDLC_constants),
  --    ("$quantification", LDLC_quantification),
  --    ("$consequence", LDLC_consequence),
  --    ("$modalities", LDLC_modalities)])
  --   <|> liftM Logic_defn_LHS_value logic_defn_value
  --   <|> liftM Logic_defn_LHS_THF_Top_level_type thf_top_level_type
  --   <|> liftM Logic_defn_LHS_name name
  --   <?> "logic_defn_LHS"
  --
  -- NOTE: not used
  -- -- <logic_defn_RHS>       :== <logic_defn_value> | <thf_unitary_formula>
  -- logic_defn_RHS :: CharParser st Logic_defn_RHS
  -- logic_defn_RHS = logic_defn_value' <|> thf_unitary_formula'
  --   <?> "logic_defn_RHS"
  --   where
  --     logic_defn_value' = liftM Logic_defn_RHS_value logic_defn_value
  --     thf_unitary_formula' =
  --       liftM Logic_defn_RNG_THF_Unitary_forumla thf_unitary_formula
  --
  -- NOTE: not used
  -- -- <logic_defn_value>     :== <defined_constant>
  -- -- <logic_defn_value>     :== $rigid | $flexible |
  --                            -- $constant | $varying | $cumulative | $decreasing |
  --                            -- $local | $global |
  --                            -- $modal_system_K | $modal_system_T | $modal_system_D |
  --                            -- $modal_system_S4 | $modal_system_S5 |
  --                            -- $modal_axiom_K | $modal_axiom_T | $modal_axiom_B |
  --                            -- $modal_axiom_D | $modal_axiom_4 | $modal_axiom_5
  -- logic_defn_value :: CharParser st Logic_defn_value
  -- logic_defn_value = constantsChoice
  --   [("$rigid", Rigid),
  --    ("$flexible", Flexible),
  --    ("$constant", Constant),
  --    ("$varying", Varying),
  --    ("$cumulative", Cumulative),
  --    ("$decreasing", Decreasing),
  --    ("$local", Local),
  --    ("$global", Global),
  --    ("$modal_system_K", Modal_system_K),
  --    ("$modal_system_T", Modal_system_T),
  --    ("$modal_system_D", Modal_system_D),
  --    ("$modal_system_S4", Modal_system_S4),
  --    ("$modal_system_S5", Modal_system_S5),
  --    ("$modal_axiom_K", Modal_axiom_K),
  --    ("$modal_axiom_T", Modal_axiom_T),
  --    ("$modal_axiom_B", Modal_axiom_B),
  --    ("$modal_axiom_D", Modal_axiom_D),
  --    ("$modal_axiom_4", Modal_axiom_4),
  --    ("$modal_axiom_5", Modal_axiom_5)]
  --   <?> "logic_defn_value"
  --
  
  {- -----------------------------------------------------------------------------
  TFX formulae
  ----------------------------------------------------------------------------- -}
  -- <tfx_formula>          ::= <tfx_logic_formula> | <thf_sequent>
  tfx_formula :: CharParser st TFX_formula
  tfx_formula = parserTrace "tfx_formula" (
    liftM TFXF_logic tfx_logic_formula
    <|> liftM TFXF_sequent thf_sequent
    <?> "tfx_formula"
    )
  
  -- <tfx_logic_formula>    ::= <thf_logic_formula>
  -- % <tfx_logic_formula>    ::= <thf_binary_formula> | <thf_unitary_formula> |
  -- %                            <tff_typed_atom> | <tff_subtype>
  tfx_logic_formula :: CharParser st TFX_logic_formula
  tfx_logic_formula = parserTrace "tfx_logic_formula" (
    liftM TFXLF_unitary thf_unitary_formula
    <|> liftM TFXLF_typed tff_typed_atom
    <|> liftM TFXLF_subtype tff_subtype
    <|> do
      f <- thf_unitary_formula
      liftM TFXLF_binary (thf_binary_formula f)
    <?> "tfx_logic_formula"
    )
  
  {- -----------------------------------------------------------------------------
  TFF formulae
  ----------------------------------------------------------------------------- -}
  -- <tff_formula>          ::= <tff_logic_formula> | <tff_typed_atom> |
  --                            <tff_sequent>
  tff_formula :: CharParser st TFF_formula
  tff_formula = parserTrace "tff_formula" (
    liftM TFFF_atom tff_typed_atom
    <|> liftM TFFF_logic tff_logic_formula
    <|> liftM TFFF_sequent tff_sequent
    <?> "tff_formula"
    )
  
  -- <tff_logic_formula>    ::= <tff_binary_formula> | <tff_unitary_formula>
  -- <tff_logic_formula>    ::= <tff_binary_formula> | <tff_unitary_formula> |
  --                            <tff_subtype>
  tff_logic_formula :: CharParser st TFF_logic_formula
  tff_logic_formula = parserTrace "tff_logic_formula" (
    liftM TFFLF_subtype tff_subtype
    <|> do
      f <- tff_unitary_formula
      (liftM TFFLF_binary (tff_binary_formula f)
        <|> return (TFFLF_unitary f))
    <?> "tff_logic_formula"
    )
  
  -- <tff_binary_formula>   ::= <tff_binary_nonassoc> | <tff_binary_assoc>
  tff_binary_formula :: TFF_unitary_formula -> CharParser st TFF_binary_formula
  tff_binary_formula f = parserTrace "tff_binary_formula" (
    liftM TFFBF_nonassoc (tff_binary_nonassoc f)
    <|> liftM TFFBF_assoc (tff_binary_assoc f)
    <?> "tff_binary_formula"
    )
  
  -- <tff_binary_nonassoc>  ::= <tff_unitary_formula> <binary_connective>
  --                            <tff_unitary_formula>
  tff_binary_nonassoc :: TFF_unitary_formula -> CharParser st TFF_binary_nonassoc
  tff_binary_nonassoc f1 = parserTrace "tff_binary_nonassoc" (do
      bc <- try binary_connective
      f2 <- tff_unitary_formula
      return $ TFF_binary_nonassoc bc f1 f2
    <?> "tff_binary_nonassoc"
    )
  
  -- <tff_binary_assoc>     ::= <tff_or_formula> | <tff_and_formula>
  tff_binary_assoc :: TFF_unitary_formula -> CharParser st TFF_binary_assoc
  tff_binary_assoc f = parserTrace "tff_binary_assoc" (
    liftM TFFBA_or (tff_or_formula f)
    <|> liftM TFFBA_and (tff_and_formula f)
    <?> "tff_binary_assoc"
    )
  
  -- <tff_or_formula>       ::= <tff_unitary_formula> <vline> <tff_unitary_formula> |
  --                            <tff_or_formula> <vline> <tff_unitary_formula>
  tff_or_formula :: TFF_unitary_formula -> CharParser st TFF_or_formula
  tff_or_formula f = parserTrace "tff_or_formula" (do
      try vline
      fs <- tff_unitary_formula `sepBy1` vline
      return $ f : fs
    <?> "tff_or_formula"
    )
  
  -- <tff_and_formula>      ::= <tff_unitary_formula> & <tff_unitary_formula> |
  --                            <tff_and_formula> & <tff_unitary_formula>
  tff_and_formula :: TFF_unitary_formula -> CharParser st TFF_and_formula
  tff_and_formula f = parserTrace "tff_and_formula" (do
      try andT
      fs <- tff_unitary_formula `sepBy1` andT
      return $ f : fs
    <?> "tff_and_formula"
    )
  
  --- <tff_unitary_formula>  ::= <tff_quantified_formula> | <tff_unary_formula> |
  ---                            <atomic_formula> | <tff_conditional> | <tff_let> |
  ---                            (<tff_logic_formula>)
  -- <tff_unitary_formula>  ::= <tff_quantified_formula> | <tff_unary_formula> |
  --                            <tff_atomic_formula> | <tff_conditional> |
  --                            <tff_let> | (<tff_logic_formula>)
  tff_unitary_formula :: CharParser st TFF_unitary_formula
  tff_unitary_formula = parserTrace "tff_unitary_formula" (
    liftM TFFUF_quantified tff_quantified_formula
    <|> liftM TFFUF_unary tff_unary_formula
    <|> liftM TFFUF_atomic tff_atomic_formula
    <|> liftM TFFUF_conditional tff_conditional
    <|> liftM TFFUF_let tff_let
    -- <|> liftM TFFUF_logic (try $ parens tff_logic_formula) -- TODO: remove
    <|> liftM TFFUF_logic (parens tff_logic_formula) -- TODO: add try (above line)
    <?> "tff_unitary_formula"
    )
  
  -- <tff_quantified_formula> ::= <fof_quantifier> [<tff_variable_list>] :
  --                            <tff_unitary_formula>
  tff_quantified_formula :: CharParser st TFF_quantified_formula
  tff_quantified_formula = parserTrace "tff_quantified_formula" (do
      q <- try fof_quantifier
      vars <- brackets tff_variable_list
      colonT
      f <- tff_unitary_formula
      return $ TFF_quantified_formula q vars f
    <?> "tff_quantified_formula"
    )
  
  -- <tff_variable_list>    ::= <tff_variable> | <tff_variable>,<tff_variable_list>
  tff_variable_list :: CharParser st TFF_variable_list
  tff_variable_list = parserTrace "tff_variable_list" (sepByComma1 tff_variable <?> "tff_variable_list"
    )
  
  -- <tff_variable>         ::= <tff_typed_variable> | <variable>
  tff_variable :: CharParser st TFF_variable
  tff_variable = parserTrace "tff_variable" (
    liftM TFFV_typed tff_typed_variable
    <|> liftM TFFV_variable variable
    <?> "tff_variable"
    )
  
  -- <tff_typed_variable>   ::= <variable> : <tff_atomic_type>
  tff_typed_variable :: CharParser st TFF_typed_variable
  tff_typed_variable = parserTrace "tff_typed_variable" (do
      v <- try (variable << colonT)
      at <- tff_atomic_type
      return $ TFF_typed_variable v at
    <?> "tff_typed_variable"
    )
  
  -- <tff_unary_formula>    ::= <unary_connective> <tff_unitary_formula> |
  --                            <fof_infix_unary>
  tff_unary_formula :: CharParser st TFF_unary_formula
  tff_unary_formula = parserTrace "tff_unary_formula" (do
      uc <- try unary_connective
      uf <- tff_unitary_formula
      return $ TFFUF_connective uc uf
    <|> liftM TFFUF_infix fof_infix_unary
    <?> "tff_unary_formula"
    )
  
  -- <tff_atomic_formula>   ::= <fof_atomic_formula>
  tff_atomic_formula :: CharParser st TFF_atomic_formula
  tff_atomic_formula = parserTrace "tff_atomic_formula" (fof_atomic_formula
    <?> "tff_atomic_formula"
    )
  
  -- <tff_conditional>      ::= $ite_f(<tff_logic_formula>,<tff_logic_formula>,
  --                            <tff_logic_formula>)
  tff_conditional :: CharParser st TFF_conditional
  tff_conditional = parserTrace "tff_conditional" ((do
    strTok "$ite_f"
    parens $ do
      lf_if <- tff_logic_formula
      commaT
      lf_then <- tff_logic_formula
      commaT
      lf_else <- tff_logic_formula
      return $ TFF_conditional lf_if lf_then lf_else)
    <?> "tff_conditional"
    )
  
  -- <tff_let>              ::= $let_tf(<tff_let_term_defns>,<tff_formula>) |
  --                            $let_ff(<tff_let_formula_defns>,<tff_formula>)
  tff_let :: CharParser st TFF_let
  tff_let = parserTrace "tff_let" (do
      strTok "$let_tf"
      parens $ do
        ltds <- tff_let_term_defns
        commaT
        f <- tff_formula
        return $ TFF_let_term_defns ltds f
    <|> do
      strTok "$let_ff"
      parens $ do
        lfds <- tff_let_formula_defns
        commaT
        f <- tff_formula
        return $ TFF_let_formula_defns lfds f
    <?> "tff_let"
    )
  
  -- <tff_let_term_defns>   ::= <tff_let_term_defn> | [<tff_let_term_list>]
  tff_let_term_defns :: CharParser st TFF_let_term_defns
  tff_let_term_defns = parserTrace "tff_let_term_defns" (
    liftM TFFLTD_single tff_let_term_defn
    <|> liftM TFFLTD_many (brackets tff_let_term_list)
    <?> "tff_let_term_defns"
    )
  
  -- <tff_let_term_list>    ::= <tff_let_term_defn> |
  --                            <tff_let_term_defn>,<tff_let_term_list>
  tff_let_term_list :: CharParser st TFF_let_term_list
  tff_let_term_list = parserTrace "tff_let_term_list" (sepByComma1 tff_let_term_defn
    <?> "tff_let_term_list"
    )
  
  -- <tff_let_term_defn>    ::= ! [<tff_variable_list>] : <tff_let_term_defn> |
  --                            <tff_let_term_binding>
  tff_let_term_defn :: CharParser st TFF_let_term_defn
  tff_let_term_defn = parserTrace "tff_let_term_defn" (do
      charTok '!' >> notFollowedBy (oneOf "!=>")
      vars <- brackets tff_variable_list
      colonT
      ltd <- tff_let_term_defn
      return $ TFFLTD_variable vars ltd
    <|> liftM TFFLTD_binding tff_let_term_binding
    <?> "tff_let_term_defn"
    )
  
  -- <tff_let_term_binding> ::= <fof_plain_term> = <fof_term> |
  --                            (<tff_let_term_binding>)
  tff_let_term_binding :: CharParser st TFF_let_term_binding
  tff_let_term_binding = parserTrace "tff_let_term_binding" (do
      pt <- try (fof_plain_term << charTok '=')
      t <- fof_term
      return $ TFFLTB_plain pt t
    <|> liftM TFFLTB_binding (parens tff_let_term_binding)
    <?> "tff_let_term_binding"
    )
  -- <tff_let_formula_defns> ::= <tff_let_formula_defn> | [<tff_let_formula_list>]
  -- <tff_let_formula_defns> ::= <tff_let_formula_defn> | [<tff_let_formula_list>]
  tff_let_formula_defns :: CharParser st TFF_let_formula_defns
  tff_let_formula_defns = parserTrace "tff_let_formula_defns" (
    liftM TFFLFD_single tff_let_formula_defn
    <|> liftM TFFLFD_many (brackets tff_let_formula_list)
    <?> "tff_let_formula_defns"
    )
  
  -- <tff_let_formula_list> ::= <tff_let_formula_defn> |
  --                            <tff_let_formula_defn>,<tff_let_formula_list>
  tff_let_formula_list :: CharParser st TFF_let_formula_list
  tff_let_formula_list = parserTrace "tff_let_formula_list" (sepByComma1 tff_let_formula_defn <?> "tff_let_formula_list"
    )
  
  -- <tff_let_formula_defn> ::= ! [<tff_variable_list>] : <tff_let_formula_defn> |
  --                            <tff_let_formula_binding>
  tff_let_formula_defn :: CharParser st TFF_let_formula_defn
  tff_let_formula_defn = parserTrace "tff_let_formula_defn" (do
      charTok '!' >> notFollowedBy (oneOf "!=>")
      vars <- brackets tff_variable_list
      colonT
      lfd <- tff_let_formula_defn
      return $ TFFLFD_variable vars lfd
    <|> liftM TFFLFD_binding tff_let_formula_binding
    <?> "tff_let_formula_defn"
    )
  
  -- <tff_let_formula_binding> ::= <plain_atomic_formula> <=> <tff_unitary_formula> |
  --                            (<tff_let_formula_binding>)
  -- <tff_let_formula_binding> ::= <fof_plain_atomic_formula> <=>
  --                            <tff_unitary_formula> | (<tff_let_formula_binding>)
  tff_let_formula_binding :: CharParser st TFF_let_formula_binding
  tff_let_formula_binding = parserTrace "tff_let_formula_binding" (do
      paf <- try (fof_plain_atomic_formula << strTok "<=>")
      uf <- tff_unitary_formula
      return $ TFFLFB_plain paf uf
    <|> liftM TFFLFB_binding (parens tff_let_formula_binding)
    <?> "tff_let_formula_binding"
    )
  
  -- <tff_sequent>          ::= <tff_formula_tuple> <gentzen_arrow>
  --                            <tff_formula_tuple> | (<tff_sequent>)
  tff_sequent :: CharParser st TFF_sequent
  tff_sequent = parserTrace "tff_sequent" (do
      t1 <- try (tff_formula_tuple << gentzen_arrow)
      t2 <- tff_formula_tuple
      return $ TFFS_plain t1 t2
    <|> liftM TFFS_parens (parens tff_sequent)
    <?> "tff_sequent"
    )
  
  -- <tff_formula_tuple>    ::= [] | [<tff_formula_tuple_list>]
  tff_formula_tuple :: CharParser st TFF_formula_tuple
  tff_formula_tuple = parserTrace "tff_formula_tuple" (
    liftM TFF_formula_tuple (emptyBrackets <|> brackets tff_formula_tuple_list)
    <?> "tff_formula_tuple"
    )
  
  -- <tff_formula_tuple_list> ::= <tff_logic_formula> |
  --                            <tff_logic_formula>,<tff_formula_tuple_list>
  tff_formula_tuple_list :: CharParser st TFF_formula_tuple_list
  tff_formula_tuple_list = parserTrace "tff_formula_tuple_list" (
    sepByComma1 tff_logic_formula
    <?> "tff_formula_tuple_list"
    )
  
  -- <tff_typed_atom>       ::= <untyped_atom> : <tff_top_level_type> |
  --                            (<tff_typed_atom>)
  tff_typed_atom :: CharParser st TFF_typed_atom
  tff_typed_atom = parserTrace "tff_typed_atom" (do
      ua <- try (untyped_atom << colonT)
      tlt <- tff_top_level_type
      return $ TFFTA_plain ua tlt
    <|> liftM TFFTA_parens (try (parens tff_typed_atom)) -- TODO: remove
    -- <|> liftM TFFTA_parens (parens tff_typed_atom) -- TODO: add try (above line)
    <?> "tff_typed_atom"
    )
  
  -- <tff_subtype>          ::= <untyped_atom> <subtype_sign> <atom>
  tff_subtype :: CharParser st TFF_subtype
  tff_subtype = parserTrace "tff_subtype" (do
      ua <- try (untyped_atom << subtype_sign)
      a <- atom
      return $ TFF_subtype ua a
    <?> "tff_subtype"
    )
  
  -- <tff_top_level_type>   ::= <tff_atomic_type> | <tff_mapping_type> |
  --                            <tf1_quantified_type> | (<tff_top_level_type>)
  tff_top_level_type :: CharParser st TFF_top_level_type
  tff_top_level_type = parserTrace "tff_top_level_type" (
    liftM TFFTLT_mapping tff_mapping_type
    <|> liftM TFFTLT_quantified tf1_quantified_type
    <|> liftM TFFTLT_atomic tff_atomic_type
    -- <|> liftM TFFTLT_parens (try (parens tff_top_level_type)) -- TODO: remove
    <|> liftM TFFTLT_parens (parens tff_top_level_type) -- TODO: add try (above line)
    <?> "tff_top_level_type"
    )
  
  -- <tf1_quantified_type>  ::= !> [<tff_variable_list>] : <tff_monotype>
  tf1_quantified_type :: CharParser st TF1_quantified_type
  tf1_quantified_type = parserTrace "tf1_quantified_type" (do
      strTok "!>"
      vars <- brackets tff_variable_list
      colonT
      mt <- tff_monotype
      return $ TF1_quantified_type vars mt
    <?> "tf1_quantified_type"
    )
  
  -- <tff_monotype>         ::= <tff_atomic_type> | (<tff_mapping_type>)
  tff_monotype :: CharParser st TFF_monotype
  tff_monotype = parserTrace "tff_monotype" (
    liftM TFFMT_atomic tff_atomic_type
    <|> liftM TFFMT_mapping (parens tff_mapping_type)
    <?> "tff_monotype"
    )
  
  -- <tff_unitary_type>     ::= <tff_atomic_type> | (<tff_xprod_type>)
  tff_unitary_type :: CharParser st TFF_unitary_type
  tff_unitary_type = parserTrace "tff_unitary_type" (
    liftM TFFUT_xprod (parens tff_xprod_type)
    <|> liftM TFFUT_atomic tff_atomic_type
    <?> "tff_unitary_type"
    )
  
  -- <tff_atomic_type>      ::= <atomic_word> | <defined_type> |
  --                            <atomic_word>(<tff_type_arguments>) | <variable>
  -- <tff_atomic_type>      ::= <type_constant> | <defined_type> |
  --                            <type_functor>(<tff_type_arguments>) | <variable>
  tff_atomic_type :: CharParser st TFF_atomic_type
  tff_atomic_type = parserTrace "tff_atomic_type" (
    functor_args
    <|> liftM TFFAT_constant type_constant
    <|> liftM TFFAT_defined defined_type
    <|> liftM TFFAT_variable variable
    <?> "tff_atomic_type"
    )
    where
      functor_args = do
        aw <- try (type_functor << oParenT)
        args <- tff_type_arguments << cParenT
        return $ TFFAT_functor aw args
  
  -- <tff_type_arguments>   ::= <tff_atomic_type> |
  --                            <tff_atomic_type>,<tff_type_arguments>
  tff_type_arguments :: CharParser st TFF_type_arguments
  tff_type_arguments = parserTrace "tff_type_arguments" (
    sepByComma1 tff_atomic_type
    <?> "tff_type_arguments"
    )
  
  -- <tff_mapping_type>     ::= <tff_unitary_type> <arrow> <tff_atomic_type>
  tff_mapping_type :: CharParser st TFF_mapping_type
  tff_mapping_type = parserTrace "tff_mapping_type" (do
      t1 <- try (tff_unitary_type << arrowT)
      t2 <- tff_atomic_type
      return $ TFF_mapping_type t1 t2
    <?> "tff_mapping_type"
    )
  
  -- <tff_xprod_type>       ::= <tff_unitary_type> <star> <tff_atomic_type> |
  --                            <tff_xprod_type> <star> <tff_atomic_type>
  tff_xprod_type :: CharParser st TFF_xprod_type
  tff_xprod_type = parserTrace "tff_xprod_type" (do
      ut <- try (tff_unitary_type << starT)
      ats <- tff_atomic_type `sepBy1` starT
      return $ TFF_xprod_type ut ats
    <?> "tff_xprod_type"
    )
  
  
  {- -----------------------------------------------------------------------------
  TCF formulae
  ----------------------------------------------------------------------------- -}
  
  -- <tcf_formula>          ::= <tcf_logic_formula> | <tff_typed_atom>
  tcf_formula :: CharParser st TCF_formula
  tcf_formula = parserTrace "tcf_formula" (
    liftM TCFF_logic tcf_logic_formula
    <|> liftM TCFF_atom tff_typed_atom
    <?> "tcf_formula"
    )
  
  -- <tcf_logic_formula>    ::= <tcf_quantified_formula> | <cnf_formula>
  tcf_logic_formula :: CharParser st TCF_logic_formula
  tcf_logic_formula = parserTrace "tcf_logic_formula" (
    liftM TCFLF_quantified tcf_quantified_formula
    <|> liftM TCFLF_cnf cnf_formula
    <?> "tcf_logic_formula"
    )
  
  -- <tcf_quantified_formula> ::= ! [<tff_variable_list>] : <cnf_formula>
  tcf_quantified_formula :: CharParser st TCF_quantified_formula
  tcf_quantified_formula = parserTrace "tcf_quantified_formula" (do
      charTok '!' >> notFollowedBy (oneOf "!=>")
      vars <- brackets tff_variable_list
      colonT
      f <- cnf_formula
      return $ TCF_quantified vars f
    <?> "tcf_quantified_formula"
    )
  
  {- -----------------------------------------------------------------------------
  FOF formulae
  ----------------------------------------------------------------------------- -}
  -- <fof_formula>          ::= <fof_logic_formula> | <fof_sequent>
  fof_formula :: CharParser st FOF_formula
  fof_formula = parserTrace "fof_formula" (
    liftM FOFF_logic fof_logic_formula
    <|> liftM FOFF_sequent fof_sequent
    <?> "fof_formula"
    )
  
  -- <fof_logic_formula>    ::= <fof_binary_formula> | <fof_unitary_formula>
  fof_logic_formula :: CharParser st FOF_logic_formula
  fof_logic_formula = parserTrace "fof_logic_formula" (do
      f <- fof_unitary_formula
      (liftM FOFLF_binary (fof_binary_formula f)
        <|> return (FOFLF_unitary f))
    <?> "fof_logic_formula"
    )
  
  -- %----Future answer variable ideas | <answer_formula>
  -- <fof_binary_formula>   ::= <fof_binary_nonassoc> | <fof_binary_assoc>
  fof_binary_formula :: FOF_unitary_formula -> CharParser st FOF_binary_formula
  fof_binary_formula f = parserTrace "fof_binary_formula" (
    liftM FOFBF_nonassoc (fof_binary_nonassoc f)
    <|> liftM FOFBF_assoc (fof_binary_assoc f)
    <?> "fof_binary_formula"
    )
  
  -- %----Only some binary connectives are associative
  -- %----There's no precedence among binary connectives
  -- <fof_binary_nonassoc>  ::= <fof_unitary_formula> <binary_connective>
  --                            <fof_unitary_formula>
  fof_binary_nonassoc :: FOF_unitary_formula -> CharParser st FOF_binary_nonassoc
  fof_binary_nonassoc f1 = parserTrace "fof_binary_nonassoc" (do
      bc <- try binary_connective
      f2 <- fof_unitary_formula
      return $ FOF_binary_nonassoc bc f1 f2
    <?> "fof_binary_nonassoc"
    )
  
  -- <fof_binary_assoc>     ::= <fof_or_formula> | <fof_and_formula>
  fof_binary_assoc :: FOF_unitary_formula -> CharParser st FOF_binary_assoc
  fof_binary_assoc f = parserTrace "fof_binary_assoc" (
    liftM FOFBA_or (fof_or_formula f)
    <|> liftM FOFBA_and (fof_and_formula f)
    <?> "fof_binary_assoc"
    )
  
  -- <fof_or_formula>       ::= <fof_unitary_formula> <vline> <fof_unitary_formula> |
  --                            <fof_or_formula> <vline> <fof_unitary_formula>
  fof_or_formula :: FOF_unitary_formula -> CharParser st FOF_or_formula
  fof_or_formula f = parserTrace "fof_or_formula" (do
      try vline
      fs <- fof_unitary_formula `sepBy1` vline
      return $ f : fs
    <?> "fof_or_formula"
    )
  
  -- <fof_and_formula>      ::= <fof_unitary_formula> & <fof_unitary_formula> |
  --                            <fof_and_formula> & <fof_unitary_formula>
  fof_and_formula :: FOF_unitary_formula -> CharParser st FOF_and_formula
  fof_and_formula f = parserTrace "fof_and_formula" (do
      try andT
      fs <- fof_unitary_formula `sepBy1` andT
      return $ f : fs
    <?> "fof_and_formula"
    )
  
  -- %----<fof_unitary_formula> are in ()s or do not have a <binary_connective> at
  -- %----the top level.
  -- <fof_unitary_formula>  ::= <fof_quantified_formula> | <fof_unary_formula> |
  --                            <fof_atomic_formula> | (<fof_logic_formula>)
  fof_unitary_formula :: CharParser st FOF_unitary_formula
  fof_unitary_formula = parserTrace "fof_unitary_formula" (
    liftM FOFUF_logic (parens fof_logic_formula)
    <|> liftM FOFUF_unary fof_unary_formula
    <|> liftM FOFUF_quantified fof_quantified_formula
    <|> liftM FOFUF_atomic fof_atomic_formula
    <?> "fof_unitary_formula"
    )
  
  -- <fof_quantified_formula> ::= <fof_quantifier> [<fof_variable_list>] :
  --                            <fof_unitary_formula>
  fof_quantified_formula :: CharParser st FOF_quantified_formula
  fof_quantified_formula = parserTrace "fof_quantified_formula" (do
    q <- try fof_quantifier
    vars <- brackets fof_variable_list
    colonT
    f <- fof_unitary_formula
    return $ FOF_quantified_formula q vars f
    )
  
  
  -- <fof_variable_list>    ::= <variable> | <variable>,<fof_variable_list>
  fof_variable_list :: CharParser st FOF_variable_list
  fof_variable_list = parserTrace "fof_variable_list" (sepByComma1 variable <?> "fof_variable_list"
    )
  
  -- <fof_unary_formula>    ::= <unary_connective> <fof_unitary_formula> |
  --                            <fof_infix_unary>
  fof_unary_formula :: CharParser st FOF_unary_formula
  fof_unary_formula = parserTrace "fof_unary_formula" (do
      uc <- try unary_connective
      uf <- fof_unitary_formula
      return $ FOFUF_connective uc uf
    <|> liftM FOFUF_infix fof_infix_unary
    <?> "fof_unary_formula"
    )
  
  -- <fof_infix_unary>      ::= <fof_term> <infix_inequality> <fof_term>
  fof_infix_unary :: CharParser st FOF_infix_unary
  fof_infix_unary = parserTrace "fof_infix_unary" (do
      t1 <- try (fof_term << infix_inequality)
      t2 <- fof_term
      return $ FOF_infix_unary t1 t2
    <?> "fof_infix_unary"
    )
  
  -- <fof_atomic_formula>   ::= <fof_plain_atomic_formula> |
  --                            <fof_defined_atomic_formula> |
  --                            <fof_system_atomic_formula>
  fof_atomic_formula :: CharParser st FOF_atomic_formula
  fof_atomic_formula = parserTrace "fof_atomic_formula" (
    liftM FOFAT_defined fof_defined_atomic_formula
    <|> liftM FOFAT_system fof_system_atomic_formula
    <|> liftM FOFAT_plain fof_plain_atomic_formula
    <?> "fof_atomic_formula"
    )
  
  -- <fof_plain_atomic_formula> ::= <fof_plain_term>
  -- <fof_plain_atomic_formula> :== <proposition> | <predicate>(<fof_arguments>)
  fof_plain_atomic_formula :: CharParser st FOF_plain_atomic_formula
  fof_plain_atomic_formula = parserTrace "fof_plain_atomic_formula" (do
      p <- try (predicate << oParenT)
      args <- fof_arguments << cParenT
      return $ FOFPAF_predicate p args
    <|> liftM FOFPAF_proposition proposition
    <?> "fof_plain_atomic_formula"
    )
  
  -- <fof_defined_atomic_formula> ::= <fof_defined_plain_formula> |
  --                            <fof_defined_infix_formula>
  fof_defined_atomic_formula :: CharParser st FOF_defined_atomic_formula
  fof_defined_atomic_formula = parserTrace "fof_defined_atomic_formula" (
    liftM FOFDAF_plain fof_defined_plain_formula
    <|> liftM FOFDAF_infix fof_defined_infix_formula
    <?> "fof_defined_atomic_formula"
    )
  
  -- <fof_defined_plain_formula> ::= <fof_defined_plain_term>
  -- <fof_defined_plain_formula> :== <defined_proposition> |
  --                            <defined_predicate>(<fof_arguments>)
  fof_defined_plain_formula :: CharParser st FOF_defined_plain_formula
  fof_defined_plain_formula = parserTrace "fof_defined_plain_formula" (do
      p <- try (defined_predicate << oParenT)
      args <- fof_arguments << cParenT
      return $ FOFDPF_predicate p args
    <|> liftM FOFDPF_proposition defined_proposition
    <?> "fof_defined_plain_formula"
    )
  
  -- <fof_defined_infix_formula> ::= <fof_term> <defined_infix_pred> <fof_term>
  fof_defined_infix_formula :: CharParser st FOF_defined_infix_formula
  fof_defined_infix_formula = parserTrace "fof_defined_infix_formula" (do
      (t1, i) <- try $ do
        t1 <- fof_term
        i <- defined_infix_pred
        return (t1, i)
      t2 <- fof_term
      return $ FOF_defined_infix_formula i t1 t2
    <?> "fof_defined_infix_formula"
    )
  
  -- %----System terms have system specific interpretations
  -- <fof_system_atomic_formula> ::= <fof_system_term>
  fof_system_atomic_formula :: CharParser st FOF_system_atomic_formula
  fof_system_atomic_formula = parserTrace "fof_system_atomic_formula" (
    liftM FOF_system_atomic_formula fof_system_term
    <?> "fof_system_atomic_formula"
    )
  
  -- <fof_plain_term>       ::= <constant> | <functor>(<fof_arguments>)
  fof_plain_term :: CharParser st FOF_plain_term
  fof_plain_term = parserTrace "fof_plain_term" (do
      f <- try (functor << oParenT)
      args <- fof_arguments << cParenT
      return $ FOFPT_functor f args
    <|> liftM FOFPT_constant constant
    <?> "fof_plain_term"
    )
  
  -- %----Defined terms have TPTP specific interpretations
  -- <fof_defined_term>     ::= <defined_term> | <fof_defined_atomic_term>
  fof_defined_term :: CharParser st FOF_defined_term
  fof_defined_term = parserTrace "fof_defined_term" (
    liftM FOFDT_term defined_term
    <|> liftM FOFDT_atomic fof_defined_atomic_term
    <?> "fof_defined_term"
    )
  
  -- <fof_defined_atomic_term>  ::= <fof_defined_plain_term>
  -- %----None yet             | <defined_infix_term>
  fof_defined_atomic_term :: CharParser st FOF_defined_atomic_term
  fof_defined_atomic_term = parserTrace "fof_defined_atomic_term" (
    liftM FOFDAT_plain fof_defined_plain_term
    <?> "fof_defined_atomic_term"
    )
  
  -- %----None yet <defined_infix_term> ::= <fof_term> <defined_infix_func> <fof_term>
  -- data Defined_infix_term = Defined_infix_term Defined_infix_func FOF_term FOF_term
  --                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----None yet <defined_infix_func> ::=
  -- data Defined_infix_func =
  
  -- <fof_defined_plain_term>   ::= <defined_constant> |
  --                            <defined_functor>(<fof_arguments>)
  -- %----Add $tuple for tuples, because [<fof_arguments>] doesn't work.
  fof_defined_plain_term :: CharParser st FOF_defined_plain_term
  fof_defined_plain_term = parserTrace "fof_defined_plain_term" (do
      f <- try (defined_functor << oParenT)
      args <- fof_arguments << cParenT
      return $ FOFDPT_functor f args
    <|> liftM FOFDPT_constant defined_constant
    <?> "fof_defined_plain_term"
    )
  
  -- %----System terms have system specific interpretations
  -- <fof_system_term>      ::= <system_constant> | <system_functor>(<fof_arguments>)
  fof_system_term :: CharParser st FOF_system_term
  fof_system_term = parserTrace "fof_system_term" (do
      f <- try (system_functor << oParenT)
      args <- fof_arguments << cParenT
      return $ FOFST_functor f args
    <|> liftM FOFST_constant system_constant
    <?> "fof_system_term"
    )
  
  -- %----Arguments recurse back up to terms (this is the FOF world here)
  -- <fof_arguments>        ::= <fof_term> | <fof_term>,<fof_arguments>
  fof_arguments :: CharParser st FOF_arguments
  fof_arguments = parserTrace "fof_arguments" (
    sepByComma1 fof_term
    <?> "fof_arguments"
    )
  
  -- %----These are terms used as arguments. Not the entry point for terms because
  -- %----<fof_plain_term> is also used as <fof_plain_atomic_formula>
  -- <fof_term>             ::= <fof_function_term> | <variable> |
  --                            <tff_conditional_term> | <tff_let_term>
  fof_term :: CharParser st FOF_term
  fof_term = parserTrace "fof_term" (
    liftM FOFT_let tff_let_term
    <|> liftM FOFT_conditional tff_conditional_term
    <|> liftM FOFT_variable variable
    <|> liftM FOFT_function fof_function_term
    <?> "fof_term"
    )
  
  -- %% DAMN THIS JUST WON'T WORK | <tuple_term>
  -- %----<tuple_term> is for TFF only, but it's here because it's used in
  -- %----<fof_atomic_formula>, which is also used as <tff_atomic_formula>.
  -- % <tuple_term>           ::= [] | [<fof_arguments>]
  -- <fof_function_term>    ::= <fof_plain_term> | <fof_defined_term> |
  --                            <fof_system_term>
  fof_function_term :: CharParser st FOF_function_term
  fof_function_term = parserTrace "fof_function_term" (
    liftM FOFFT_system fof_system_term
    <|> liftM FOFFT_defined fof_defined_term
    <|> liftM FOFFT_plain fof_plain_term
    <?> "fof_function_term"
    )
  
  -- %----Conditional terms should be used by only TFF.
  -- <tff_conditional_term> ::= $ite_t(<tff_logic_formula>,<fof_term>,<fof_term>)
  tff_conditional_term :: CharParser st TFF_conditional_term
  tff_conditional_term = parserTrace "tff_conditional_term" (do
      strTok "$ite_t"
      oParenT
      f_if <- tff_logic_formula
      commaT
      t_then <- fof_term
      commaT
      t_else <- fof_term
      cParenT
      return $ TFF_conditional_term f_if t_then t_else
    <?> "tff_conditional_term"
    )
  
  -- %----Let terms should be used by only TFF. $let_ft is for use when there is
  -- %----a $ite_t in the <fof_term>. See the commentary for $let_tf and $let_ff.
  -- <tff_let_term>         ::= $let_ft(<tff_let_formula_defns>,<fof_term>) |
  --                            $let_tt(<tff_let_term_defns>,<fof_term>)
  tff_let_term :: CharParser st TFF_let_term
  tff_let_term = parserTrace "tff_let_term" (do
      strTok "$let_ft"
      oParenT
      defns <- tff_let_formula_defns
      commaT
      t <- fof_term
      cParenT
      return $ TFFLT_formula defns t
    <|> do
      strTok "$let_tt"
      oParenT
      defns <- tff_let_term_defns
      commaT
      t <- fof_term
      cParenT
      return $ TFFLT_term defns t
    <?> "tff_let_term"
    )
  
  
  -- %----This section is the FOFX syntax. Not yet in use.
  -- % <fof_let>            ::= := [<fof_let_list>] : <fof_unitary_formula>
  -- % <fof_let_list>       ::= <fof_defined_var> |
  -- %                          <fof_defined_var>,<fof_let_list>
  -- % <fof_defined_var>    ::= <variable> := <fof_logic_formula> |
  -- %                          <variable> :- <fof_term> | (<fof_defined_var>)
  -- %
  -- % <fof_conditional>    ::= $ite_f(<fof_logic_formula>,<fof_logic_formula>,
  -- %                          <fof_logic_formula>)
  -- %
  -- % <fof_conditional_term> ::= $ite_t(<fof_logic_formula>,<fof_term>,<fof_term>)
  
  -- <fof_sequent>          ::= <fof_formula_tuple> <gentzen_arrow>
  --                            <fof_formula_tuple> | (<fof_sequent>)
  fof_sequent :: CharParser st FOF_sequent
  fof_sequent = parserTrace "fof_sequent" (do
      ft1 <- try (fof_formula_tuple << gentzen_arrow)
      ft2 <- fof_formula_tuple
      return $ FOFS_plain ft1 ft2
    <|> liftM FOFS_parens (parens fof_sequent)
    <?> "fof_sequent"
    )
  
  -- <fof_formula_tuple>    ::= [] | [<fof_formula_tuple_list>]
  fof_formula_tuple :: CharParser st FOF_formula_tuple
  fof_formula_tuple = parserTrace "fof_formula_tuple" (
    liftM FOF_formula_tuple (emptyBrackets <|> brackets fof_formula_tuple_list)
    <?> "fof_formula_tuple"
    )
  
  -- <fof_formula_tuple_list> ::= <fof_logic_formula> |
  --                            <fof_logic_formula>,<fof_formula_tuple_list>
  fof_formula_tuple_list :: CharParser st FOF_formula_tuple_list
  fof_formula_tuple_list = parserTrace "fof_formula_tuple_list" (
    sepByComma1 fof_logic_formula
    <?> "fof_formula_tuple_list"
    )
  
  {- -----------------------------------------------------------------------------
  CNF formulae (variables implicitly universally quantified)
  ----------------------------------------------------------------------------- -}
  -- <cnf_formula>          ::= <disjunction> | (<disjunction>)
  cnf_formula :: CharParser st CNF_formula
  cnf_formula = parserTrace "cnf_formula" (
    liftM CNFF_parens (parens disjunction)
    <|> liftM CNFF_plain disjunction
    <?> "cnf_formula"
    )
  
  -- <disjunction>          ::= <literal> | <disjunction> <vline> <literal>
  disjunction :: CharParser st Disjunction
  disjunction = parserTrace "disjunction" (
    liftM Disjunction (literal `sepBy1` vline)
    <?> "disjunction"
    )
  
  -- <literal>              ::= <fof_atomic_formula> | ~ <fof_atomic_formula> |
  --                            <fof_infix_unary>
  literal :: CharParser st Literal
  literal = parserTrace "literal" (
    liftM Lit_fof_infix fof_infix_unary
    <|> not_fof_atomic_formula
    <|> liftM Lit_atomic fof_atomic_formula
    <?> "literal"
    )
    where
      not_fof_atomic_formula = do
        charTok '~'
        liftM Lit_negative fof_atomic_formula
  
  -- %----Connectives - THF
  -- <thf_quantifier>       ::= <fof_quantifier> | <th0_quantifier> |
  --                            <th1_quantifier>
  thf_quantifier :: CharParser st THF_quantifier
  thf_quantifier = parserTrace "thf_quantifier" (
    liftM THFQ_fof fof_quantifier
    <|> liftM THFQ_th0 th0_quantifier
    <|> liftM THFQ_th1 th1_quantifier
    <?> "thf_quantifier"
    )
  
  -- %----TH0 quantifiers are also available in TH1
  -- <th1_quantifier>       ::= !> | ?*
  th1_quantifier :: CharParser st TH1_quantifier
  th1_quantifier = parserTrace "th1_quantifier" (
    (strTok "!>" >> return TH1_DependentProduct)
    <|> (strTok "?*" >> return TH1_DependentSum)
    <?> "th1_quantifier"
    )
  
  -- <th0_quantifier>       ::= ^ | @+ | @-
  th0_quantifier :: CharParser st TH0_quantifier
  th0_quantifier = parserTrace "th0_quantifier" (
    (strTok "^" >> return TH0_LambdaBinder)
    <|> (strTok "@+" >> return TH0_IndefiniteDescription)
    <|> (strTok "@-" >> return TH0_DefiniteDescription)
    <?> "th0_quantifier"
    )
  
  
  -- <thf_pair_connective>  ::= <infix_equality> | <infix_inequality> |
  --                            <binary_connective> | <assignment>
  thf_pair_connective :: CharParser st THF_pair_connective
  thf_pair_connective = parserTrace "thf_pair_connective" (
    (infix_equality >> return THF_infix_equality)
    <|> liftM THFPC_binary binary_connective
    <|> (infix_inequality >> return Infix_inequality)
    <|> (assignment >> return THF_assignment)
    <?> "thf_pair_connective"
    )
  
  -- <thf_unary_connective> ::= <unary_connective> | <th1_unary_connective>
  thf_unary_connective :: CharParser st THF_unary_connective
  thf_unary_connective = parserTrace "thf_unary_connective" (
    liftM THFUC_th1 th1_unary_connective
    <|> liftM THFUC_unary unary_connective
    <?> "thf_unary_connective"
    )
  
  -- <th1_unary_connective> ::= !! | ?? | @@+ | @@- | @=
  th1_unary_connective :: CharParser st TH1_unary_connective
  th1_unary_connective = parserTrace "th1_unary_connective" (
    (strTok "!!" >> return TH1_PiForAll)
    <|> (strTok "??" >> return TH1_PiSigmaExists)
    <|> (strTok "@@+" >> return TH1_PiIndefiniteDescription)
    <|> (strTok "@@-" >> return TH1_PiDefiniteDescription)
    <|> (strTok "@=" >> return TH1_PiEquality)
    <?> "th1_unary_connective"
    )
  
  -- %----Connectives - THF and TFF
  -- <subtype_sign>         ::= <<
  subtype_sign :: CharParser st Token
  subtype_sign = parserTrace "subtype_sign" (
    strTok "<<" <?> "subtype_sign"
    )
  
  -- %----Connectives - TFF
  -- % <tff_pair_connective>  ::= <binary_connective> | <assignment>
  -- Note: not used
  -- tff_pair_connective :: CharParser st TFF_pair_connective
  -- tff_pair_connective = parserTrace "tff_pair_connective" (
  --   liftM TFFPC_binary binary_connective
  --   <|> liftM TFFPC_assignment tff_assignment
  --   <?> "tff_pair_connective"
  --   )
  
  -- %----Connectives - FOF
  -- <fof_quantifier>       ::= ! | ?
  fof_quantifier :: CharParser st FOF_quantifier
  fof_quantifier = parserTrace "fof_quantifier" (
    (charTok '!' >> notFollowedBy (oneOf "!=>") >> return ForAll)
    <|> (charTok '?' >> notFollowedBy (oneOf "?*") >> return Exists)
    <?> "fof_quantifier"
    )
  
  -- <binary_connective>    ::= <=> | => | <= | <~> | ~<vline> | ~&
  binary_connective :: CharParser st Binary_connective
  binary_connective = parserTrace "binary_connective" ((strTok "<=>" >> return Equivalence)
    <|> (strTok "=>" >> return Implication)
    <|> (strTok "<=" >> return ReverseImplication)
    <|> (strTok "<~>" >> return XOR)
    <|> (strTok "~|" >> return NOR)
    <|> (strTok "~&" >> return NAND)
    <?> "binary_connective"
    )
  
  -- <assoc_connective>     ::= <vline> | &
  assoc_connective :: CharParser st Assoc_connective
  assoc_connective = parserTrace "assoc_connective" (
    (vline >> return OR)
    <|> (andT >> return AND)
    <?> "assoc_connective"
    )
  
  -- <unary_connective>     ::= ~
  unary_connective :: CharParser st Unary_connective
  unary_connective = parserTrace "unary_connective" (
    (charTok '~' >> return NOT)
    <?> "unary_connective"
    )
  
  -- %----The seqent arrow
  -- <gentzen_arrow>        ::= -->
  gentzen_arrow :: CharParser st Token
  gentzen_arrow = parserTrace "gentzen_arrow" (
    strTok "-->"
    <?> "gentzen_arrow"
    )
  
  -- <assignment>           ::= :=
  assignment :: CharParser st Token
  assignment = parserTrace "assignment" (
    strTok ":="
    <?> "assignment"
    )
  
  {- -----------------------------------------------------------------------------
  Types for THF and TFF
  ----------------------------------------------------------------------------- -}
  -- -<type_constant>        ::= <type_functor>
  type_constant :: CharParser st Type_constant
  type_constant = parserTrace "type_constant" (
    type_functor
    <?> "type_constant"
    )
  
  -- <type_functor>         ::= <atomic_word>
  type_functor :: CharParser st Type_functor
  type_functor = parserTrace "type_functor" (
    atomic_word
    <?> "type_functor"
    )
  
  -- <defined_type>         ::= <atomic_defined_word>
  -- <defined_type>         :== $oType | $o | $iType | $i | $tType |
  --                            $real | $rat | $int
  defined_type :: CharParser st Defined_type
  defined_type = parserTrace "defined_type" (constantsChoice
    [("$oType", OType),
     ("$o", O),
     ("$iType", IType),
     ("$int", Int),
     ("$i", I),
     ("$tType", TType),
     ("$real", Real),
     ("$rat", Rat)]
    <?> "defined_type"
    )
  
  -- NOTE: unused
  -- <system_type>          :== <atomic_system_word>
  -- system_type :: CharParser st Token
  -- system_type = pToken atomic_system_word <?> "system_type"
  --
  
  
  {- -----------------------------------------------------------------------------
  For all language types
  ----------------------------------------------------------------------------- -}
  -- <atom_>                 ::= <untyped_atom> | <defined_constant>
  atom :: CharParser st Atom
  atom = parserTrace "atom" (
    liftM Atom_constant defined_constant
    <|> liftM Atom_untyped untyped_atom
    <?> "atom"
    )
  
  -- <untyped_atom>         ::= <constant> | <system_constant>
  untyped_atom :: CharParser st Untyped_atom
  untyped_atom = parserTrace "untyped_atom" (
    liftM UA_system system_constant
    <|> liftM UA_constant constant
    <?> "untyped_atom"
    )
  
  -- <proposition>          :== <predicate>
  proposition :: CharParser st Proposition
  proposition = parserTrace "proposition" (predicate <?> "proposition"
    )
  
  -- <predicate>            :== <atomic_word>
  predicate :: CharParser st Predicate
  predicate = parserTrace "predicate" (atomic_word <?> "predicate"
    )
  
  -- <defined_proposition>  :== <atomic_defined_word>
  -- <defined_proposition>  :== $true | $false
  defined_proposition :: CharParser st Defined_proposition
  defined_proposition = parserTrace "defined_prop" (
    constantsChoice [("$true", TPTP_true), ("$false", TPTP_false)]
    <?> "defined_prop"
    )
  
  -- <defined_predicate>    :== <atomic_defined_word>
  -- <defined_predicate>    :== $distinct |
  --                            $less | $lesseq | $greater | $greatereq |
  --                            $is_int | $is_rat |
  --                            $box_P | $box_i | $box_int | $box |
  --                            $dia_P | $dia_i | $dia_int | $dia
  defined_predicate :: CharParser st Defined_predicate
  defined_predicate = parserTrace "defined_pred" (constantsChoice
    [("$distinct", Distinct),
     ("$lesseq", Lesseq),
     ("$less", Less),
     ("$greatereq", Greatereq),
     ("$greater", Greater),
     ("$is_int", Is_int),
     ("$is_rat", Is_rat),
     ("$box_P", Box_P),
     ("$box_int", Box_int),
     ("$box_i", Box_i),
     ("$box", Box),
     ("$dia_P", Dia_P),
     ("$dia_int", Dia_int),
     ("$dia_i", Dia_i),
     ("$dia", Dia)]
    <?> "defined_pred"
    )
  
  -- <defined_infix_pred>   ::= <infix_equality> | <assignment>
  defined_infix_pred :: CharParser st Defined_infix_pred
  defined_infix_pred = parserTrace "defined_infix_pred" (
    (infix_equality >> return Defined_infix_equality)
    <|> (assignment >> return Defined_assignment)
    <?> "defined_infix_pred"
    )
  
  -- <infix_equality>       ::= =
  infix_equality :: CharParser st Token
  infix_equality = parserTrace "infix_equality" (
    parseIfNot (strTok "=>") (charTok '=')
    <?> "infix_equality"
    )
  
  -- <infix_inequality>     ::= !=
  infix_inequality :: CharParser st Token
  infix_inequality = parserTrace "infix_inequality" (
    strTok "!="
    <?> "infix_inequality"
    )
  
  -- <constant>             ::= <functor>
  constant :: CharParser st Constant
  constant = parserTrace "constant" (
    functor
    <?> "constant"
    )
  
  -- <functor>              ::= <atomic_word>
  functor :: CharParser st TPTP_functor
  functor = parserTrace "functor" (
    atomic_word
    <?> "functor"
    )
  
  -- <system_constant>      ::= <system_functor>
  system_constant :: CharParser st System_constant
  system_constant = parserTrace "system_constant" (
    system_functor
    <?> "system_constant"
    )
  
  -- <system_functor>       ::= <atomic_system_word>
  system_functor :: CharParser st System_functor
  system_functor = parserTrace "system_functor" (
    atomic_system_word
    <?> "system_functor"
    )
  
  -- <defined_constant>     ::= <defined_functor>
  defined_constant :: CharParser st Defined_constant
  defined_constant = parserTrace "defined_constant" (
    defined_functor
    <?> "defined_constant"
    )
  
  -- <defined_functor>      ::= <atomic_defined_word>
  -- <defined_functor>      :== $uminus | $sum | $difference | $product |
  --                            $quotient | $quotient_e | $quotient_t | $quotient_f |
  --                            $remainder_e | $remainder_t | $remainder_f |
  --                            $floor | $ceiling | $truncate | $round |
  --                            $to_int | $to_rat | $to_real
  defined_functor :: CharParser st Defined_functor
  defined_functor = parserTrace "defined_functor" (constantsChoice
    [("$uminus", Uminus),
     ("$sum", Sum),
     ("$difference", Difference),
     ("$product", Product),
     ("$quotient_e", Quotient_e),
     ("$quotient_t", Quotient_t),
     ("$quotient_f", Quotient_f),
     ("$quotient", Quotient),
     ("$remainder_e", Remainder_e),
     ("$remainder_t", Remainder_t),
     ("$remainder_f", Remainder_f),
     ("$floor", Floor),
     ("$ceiling", Ceiling),
     ("$truncate", Truncate),
     ("$round", Round),
     ("$to_int", To_int),
     ("$to_rat", To_rat),
     ("$to_real", To_real)]
    <|> liftM DF_atomic_defined_word atomic_defined_word
    <?> "defined_functor"
    )
  
  -- <defined_term>         ::= <defined_atom> | <defined_atomic_term>
  -- <defined_term>         ::= <number> | <distinct_object>
  defined_term :: CharParser st Defined_term
  defined_term = parserTrace "defined_term" (
    liftM DT_number number
    <|> liftM DT_object distinct_object
    <?> "defined_term"
    )
  
  -- <variable>             ::= <upper_word>
  variable :: CharParser st Variable
  variable = parserTrace "variable" (
    pToken upper_word
    <?> "variable"
    )
  
  {- -----------------------------------------------------------------------------
  Formula sources
  ----------------------------------------------------------------------------- -}
  -- <source>               ::= <general_term>
  -- <source>               :== <dag_source> | <internal_source> |
  --                            <external_source> | unknown | [<sources>]
  source :: CharParser st Source
  source = parserTrace "source" (
    liftM Source_external external_source
    <|> liftM Source_internal internal_source
    <|> liftM Source_DAG dag_source
    <|> (strTok "unknown" >> return Unknown_source)
    <|> liftM Source_many (brackets sources)
    <?> "source"
    )
  
  -- %----Alternative sources are recorded like this, thus allowing representation
  -- %----of alternative derivations with shared parts.
  -- <sources>              :== <source> | <source>,<sources>
  sources :: CharParser st Sources
  sources = parserTrace "sources" (
    sepByComma1 source
    <?> "sources"
    )
  
  -- %----Only a <dag_source> can be a <name>, i.e., derived formulae can be
  -- %----identified by a <name> or an <inference_record>
  -- <dag_source>           :== <name> | <inference_record>
  dag_source :: CharParser st DAG_source
  dag_source = parserTrace "dag_source" (
    liftM DAGS_record inference_record
    <|> liftM DAGS_name name
    <?> "dag_source"
    )
  
  -- <inference_record>     :== inference(<inference_rule>,<useful_info>,
  --                            <inference_parents>)
  inference_record :: CharParser st Inference_record
  inference_record = parserTrace "inference_record" (do
      try (strTok "inference" << oParenT)
      ir <- inference_rule
      commaT
      ui <- useful_info
      commaT
      ip <- inference_parents
      cParenT
      return $ Inference_record ir ui ip
    <?> "inference_record"
    )
  
  -- <inference_rule>       :== <atomic_word>
  -- %----Examples are          deduction | modus_tollens | modus_ponens | rewrite |
  -- %                          resolution | paramodulation | factorization |
  -- %                          cnf_conversion | cnf_refutation | ...
  inference_rule :: CharParser st Token
  inference_rule = parserTrace "inference_rule" (
    atomic_word
    <?> "inference_rule"
    )
  
  -- %----<inference_parents> can be empty in cases when there is a justification
  -- %----for a tautologous theorem. In case when a tautology is introduced as
  -- %----a leaf, e.g., for splitting, then use an <internal_source>.
  -- <inference_parents>    :== [] | [<parent_list>]
  inference_parents :: CharParser st Inference_parents
  inference_parents = parserTrace "inference_parents" (
    emptyBrackets
    <|> brackets parent_list
    <?> "inference_parents"
    )
  
  -- <parent_list>          :== <parent_info> | <parent_info>,<parent_list>
  parent_list :: CharParser st Parent_list
  parent_list = parserTrace "parent_list" (
    sepByComma1 parent_info
    <?> "parent_list"
    )
  
  -- <parent_info>          :== <source><parent_details>
  parent_info :: CharParser st Parent_info
  parent_info = parserTrace "parent_info" (do
      s <- source
      pd <- parent_details
      return $ Parent_info s pd
    <?> "parent_info"
    )
  
  -- <parent_details>       :== :<general_list> | <null>
  parent_details :: CharParser st Parent_details
  parent_details = parserTrace "parent_details" (do
      colonT
      liftM Just general_list
    <|> return Nothing
    <?> "parent_details"
    )
  
  -- <internal_source>      :== introduced(<intro_type><optional_info>)
  internal_source :: CharParser st Internal_source
  internal_source = parserTrace "internal_source" (do
      try (strTok "introduced" << oParenT)
      it <- intro_type
      oi <- optional_info
      cParenT
      return $ Internal_source it oi
    <?> "internal_source"
    )
  
  -- <intro_type>           :== definition | axiom_of_choice | tautology | assumption
  intro_type :: CharParser st Intro_type
  intro_type = parserTrace "intro_type" (
    constantsChoice
      [("definition", IntroTypeDefinition),
       ("axiom_of_choice", AxiomOfChoice),
       ("tautology", Tautology),
       ("assumption", IntroTypeAssumption)]
    <?> "intro_type"
    )
  
  -- <external_source>      :== <file_source> | <theory> | <creator_source>
  external_source :: CharParser st External_source
  external_source = parserTrace "external_source" (
    liftM ExtSrc_file file_source
    <|> liftM ExtSrc_theory theory
    <|> liftM ExtSrc_creator creator_source
    <?> "external_source"
    )
  
  -- <file_source>          :== file(<file_name><file_info>)
  file_source :: CharParser st File_source
  file_source = parserTrace "file_source" (do
      try (strTok "file" << oParenT)
      fn <- file_name
      fi <- file_info
      cParenT
      return $ File_source fn fi
    <?> "file_source"
    )
  
  -- <file_info>            :== ,<name> | <null>
  file_info :: CharParser st File_info
  file_info = parserTrace "file_info" (do
      commaT
      n <- name
      return $ Just n
    <|> return Nothing
    <?> "file_info"
    )
  
  -- <theory>               :== theory(<theory_name><optional_info>)
  theory :: CharParser st Theory
  theory = parserTrace "theory" (do
      try (strTok "theory" << oParenT)
      tn <- theory_name
      oi <- optional_info
      cParenT
      return $ Theory tn oi
    <?> "theory"
    )
  
  -- <theory_name>          :== equality | ac
  theory_name :: CharParser st Theory_name
  theory_name = parserTrace "theory_name" (
    (strTok "equality" >> return TN_equality)
    <|> (strTok "ac" >> return TN_ac)
    <?> "theory_name"
    )
  
  -- <creator_source>       :== creator(<creator_name><optional_info>)
  creator_source :: CharParser st Creator_source
  creator_source = parserTrace "creator_source" (do
      try (strTok "creator" << oParenT)
      cn <- creator_name
      oi <- optional_info
      cParenT
      return $ Creator_source cn oi
    <?> "creator_source"
    )
  
  -- <creator_name>         :== <atomic_word>
  creator_name :: CharParser st Token
  creator_name = parserTrace "creator_name" (
    atomic_word
    <?> "creator_name"
    )
  
  
  {- -----------------------------------------------------------------------------
  Useful info fields
  ----------------------------------------------------------------------------- -}
  -- <optional_info>        ::= ,<useful_info> | <null>
  optional_info :: CharParser st (Maybe Useful_info)
  optional_info = parserTrace "optional_info" (
    optionMaybe (charTok ',' >> useful_info)
    <?> "optional_info"
    )
  
  -- <useful_info>          ::= <general_list>
  -- <useful_info>          :== [] | [<info_items>]
  useful_info :: CharParser st Useful_info
  useful_info = parserTrace "useful_info" (
    liftM UI_items (emptyBrackets <|> try (brackets info_items))
    <|> liftM UI_general_list general_list
    <?> "useful_info"
    )
  
  -- <info_items>           :== <info_item> | <info_item>,<info_items>
  info_items :: CharParser st Info_items
  info_items = parserTrace "info_items" (
    sepByComma1 info_item
    <?> "info_items"
    )
  
  -- <info_item>            :== <formula_item> | <inference_item> |
  --                            <general_function>
  info_item :: CharParser st Info_item
  info_item = parserTrace "info_item" (
    liftM Info_formula formula_item
    <|> liftM Info_inference inference_item
    <|> liftM Info_general general_function
    <?> "info_item"
    )
  
  
  {- -----------------------------------------------------------------------------
  Useful info for formula records
  ----------------------------------------------------------------------------- -}
  -- <formula_item>         :== <description_item> | <iquote_item>
  formula_item :: CharParser st Formula_item
  formula_item = parserTrace "formula_item" (
    liftM FI_description description_item
    <|> liftM FI_iquote iquote_item
    <?> "formula_item"
    )
  
  -- <description_item>     :== description(<atomic_word>)
  description_item :: CharParser st Description_item
  description_item = parserTrace "description_item" (do
      try (strTok "description" << oParenT)
      atomic_word << cParenT
    <?> "description_item"
    )
  
  -- <iquote_item>          :== iquote(<atomic_word>)
  iquote_item :: CharParser st Iquote_item
  iquote_item = parserTrace "iquote_item" (do
      try (strTok "iquote" << oParenT)
      atomic_word << cParenT
    <?> "iquote_item"
    )
  
  -- <inference_item>       :== <inference_status> | <assumptions_record> |
  --                            <new_symbol_record> | <refutation>
  inference_item :: CharParser st Inference_item
  inference_item = parserTrace "inference_item" (
    liftM Inf_status inference_status
    <|> liftM Inf_assumption assumptions_record
    <|> liftM Inf_symbol new_symbol_record
    <|> liftM Inf_refutation refutation
    <?> "inference_item"
    )
  
  -- <inference_status>     :== status(<status_value>) | <inference_info>
  inference_status :: CharParser st Inference_status
  inference_status = parserTrace "inference_status" (do
      try (strTok "status" << oParenT)
      liftM Inf_value (status_value << cParenT)
    <|> liftM Inf_info inference_info
    <?> "inference_status"
    )
  
  -- %----These are the success status values from the SZS ontology. The most
  -- %----commonly used values are:
  -- %----  thm - Every model of the parent formulae is a model of the inferred
  -- %----        formula. Regular logical consequences.
  -- %----  cth - Every model of the parent formulae is a model of the negation of
  -- %----        the inferred formula. Used for negation of conjectures in FOF to
  -- %----        CNF conversion.
  -- %----  esa - There exists a model of the parent formulae iff there exists a
  -- %----        model of the inferred formula. Used for Skolemization steps.
  -- %----For the full hierarchy see the SZSOntology file distributed with the TPTP.
  -- <status_value>         :== suc | unp | sap | esa | sat | fsa | thm | eqv | tac |
  --                            wec | eth | tau | wtc | wth | cax | sca | tca | wca |
  --                            cup | csp | ecs | csa | cth | ceq | unc | wcc | ect |
  --                            fun | uns | wuc | wct | scc | uca | noc
  status_value :: CharParser st Status_value
  status_value = parserTrace "status_value" (
    constantsChoice
      [("suc", SUC), ("unp", UNP), ("sap", SAP), ("esa", ESA), ("sat", SAT),
       ("fsa", FSA), ("thm", THM), ("eqv", EQV), ("tac", TAC),
       ("wec", WEC), ("eth", ETH), ("tau", TAU), ("wtc", WTC), ("wth", WTH),
       ("cax", CAX), ("sca", SCA), ("tca", TCA), ("wca", WCA),
       ("cup", CUP), ("csp", CSP), ("ecs", ECS), ("csa", CSA), ("cth", CTH),
       ("ceq", CEQ), ("unc", UNC), ("wcc", WCC), ("ect", ECT),
       ("fun", FUN), ("uns", UNS), ("wuc", WUC), ("wct", WCT), ("scc", SCC),
       ("uca", UCA), ("noc", NOC)]
    <?> "status_value"
    )
  
  -- %----<inference_info> is used to record standard information associated with an
  -- %----arbitrary inference rule. The <inference_rule> is the same as the
  -- %----<inference_rule> of the <inference_record>. The <atomic_word> indicates
  -- %----the information being recorded in the <general_list>. The <atomic_word>
  -- %----are (loosely) set by TPTP conventions, and include esplit, sr_split, and
  -- %----discharge.
  -- <inference_info>       :== <inference_rule>(<atomic_word>,<general_list>)
  inference_info :: CharParser st Inference_info
  inference_info = parserTrace "inference_info" (do
      ir <- try (inference_rule << oParenT)
      aw <- atomic_word
      commaT
      gl <- general_list
      cParenT
      return $ Inference_info ir aw gl
    <?> "inference_info"
    )
  
  -- %----An <assumptions_record> lists the names of assumptions upon which this
  -- %----inferred formula depends. These must be discharged in a completed proof.
  -- <assumptions_record>   :== assumptions([<name_list>])
  assumptions_record :: CharParser st Assumptions_record
  assumptions_record = parserTrace "assumptions_record" (do
      try (strTok "assumptions" << oParenT)
      brackets name_list << cParenT
    <?> "assumptions_record"
    )
  
  -- %----A <refutation> record names a file in which the inference recorded here
  -- %----is recorded as a proof by refutation.
  -- <refutation>           :== refutation(<file_source>)
  refutation :: CharParser st Refutation
  refutation = parserTrace "refutation" (do
      try (strTok "refutation" << oParenT)
      file_source << cParenT
    <?> "refutation"
    )
  
  -- %----A <new_symbol_record> provides information about a newly introduced symbol.
  -- <new_symbol_record>    :== new_symbols(<atomic_word>,[<new_symbol_list>])
  new_symbol_record :: CharParser st New_symbol_record
  new_symbol_record = parserTrace "new_symbol_record" (do
      try (strTok "new_symbols" << oParenT)
      aw <- atomic_word
      nsl <- new_symbol_list
      cParenT
      return $ New_symbol_record aw nsl
    <?> "new_symbol_record"
    )
  
  -- <new_symbol_list>      :== <principal_symbol> |
  --                            <principal_symbol>,<new_symbol_list>
  new_symbol_list :: CharParser st New_symbol_list
  new_symbol_list = parserTrace "new_symbol_list" (
    sepByComma1 principal_symbol
    <?> "new_symbol_list"
    )
  
  -- %----Principal symbols are predicates, functions, variables
  -- <principal_symbol>   :== <functor> | <variable>
  principal_symbol :: CharParser st Principal_symbol
  principal_symbol = parserTrace "principal_symbol" (
    liftM PS_functor functor
    <|> liftM PS_variable variable
    <?> "principal_symbol"
    )
  
  {- -----------------------------------------------------------------------------
  Include directives
  ----------------------------------------------------------------------------- -}
  -- <include>              ::= include(<file_name><formula_selection>).
  include :: CharParser st Include
  include = parserTrace "include" (do
      try (strTok "include" << oParenT)
      fn <- file_name
      fs <- formula_selection
      cParenT
      dotT
      return $ Include fn fs
    <?> "include"
    )
  
  -- <formula_selection>    ::= ,[<name_list>] | <null>
  formula_selection :: CharParser st Formula_selection
  formula_selection = parserTrace "formula_selection" (
    optionMaybe (commaT >> brackets name_list)
    <?> "formula_selection"
    )
  
  -- <name_list>            ::= <name> | <name>,<name_list>
  name_list :: CharParser st Name_list
  name_list = parserTrace "name_list" (
    sepByComma1 name
    <?> "name_list"
    )
  
  
  {- -----------------------------------------------------------------------------
  Non-logical data
  ----------------------------------------------------------------------------- -}
  -- <general_term>         ::= <general_data> | <general_data>:<general_term> |
  --                            <general_list>
  general_term :: CharParser st General_term
  general_term = parserTrace "general_term" (do
      gd <- try (general_data << colonT)
      gt <- general_term
      return $ GT_DataTerm gd gt
    <|> liftM GT_data general_data
    <|> liftM GT_list general_list
    <?> "general_term"
    )
  
  -- <general_data>         ::= <atomic_word> | <general_function> |
  --                            <variable> | <number> | <distinct_object> |
  --                            <formula_data>
  -- <general_data>         :== bind(<variable>,<formula_data>)
  general_data :: CharParser st General_data
  general_data = parserTrace "general_data" (do
      try (strTok "bind" << oParenT)
      v <- variable
      commaT
      fd <- formula_data
      cParenT
      return $ GD_bind v fd
    <|> liftM GD_general_function general_function
    <|> liftM GD_atomic_word atomic_word
    <|> liftM GD_variable variable
    <|> liftM GD_number number
    <|> liftM GD_distinct_object distinct_object
    <|> liftM GD_formula_data formula_data
    <?> "general_data"
    )
  
  -- <general_function>     ::= <atomic_word>(<general_terms>)
  general_function :: CharParser st General_function
  general_function = parserTrace "general_function" (do
    aw <- try (atomic_word << oParenT)
    fd <- general_terms
    cParenT
    return $ General_function aw fd
    )
  
  -- <formula_data>         ::= $thf(<thf_formula>) | $tff(<tff_formula>) |
  --                            $fof(<fof_formula>) | $cnf(<cnf_formula>) |
  --                            $fot(<fof_term>)
  formula_data :: CharParser st Formula_data
  formula_data = parserTrace "formula_data" (
    xxx_data "$thf" FD_THF thf_formula
    <|> xxx_data "$tff" FD_TFF tff_formula
    <|> xxx_data "$fof" FD_FOF fof_formula
    <|> xxx_data "$cnf" FD_CNF cnf_formula
    <|> xxx_data "$fot" FD_FOT fof_term
    <?> "formula_data"
    )
    where
      xxx_data str constructor parser = do
        try (strTok str << oParenT)
        d <- parser
        cParenT
        return $ constructor d
  
  -- <general_list>         ::= [] | [<general_terms>]
  general_list :: CharParser st General_list
  general_list = parserTrace "general_list" (
    emptyBrackets
    <|> brackets general_terms
    <?> "general_list"
    )
  
  -- <general_terms>        ::= <general_term> | <general_term>,<general_terms>
  general_terms :: CharParser st General_terms
  general_terms = parserTrace "general_terms" (
    sepByComma1 general_term
    <?> "general_terms"
    )
  
  
  {- -----------------------------------------------------------------------------
  General purpose
  ----------------------------------------------------------------------------- -}
  -- <name>                 ::= <atomic_word> | <integer>
  name :: CharParser st Name
  name = parserTrace "name" (
    liftM NameString atomic_word
    <|> (liftM NameInteger $ liftM read integer)
    <?> "name"
    )
  
  -- <atomic_word>          ::= <lower_word> | <single_quoted>
  -- %----<single_quoted> tokens do not include their outer quotes, therefore the
  -- %----<lower_word> <atomic_word> cat and the <single_quoted> <atomic_word> 'cat'
  -- %----are the same. Quotes must be removed from a <single_quoted> <atomic_word>
  -- %----if doing so produces a <lower_word> <atomic_word>. Note that <numbers>s
  -- %----and <variable>s are not <lower_word>s, so '123' and 123, and 'X' and X,
  -- %----are different.
  atomic_word :: CharParser st Token
  atomic_word = parserTrace "atomic_word" (
    pToken lower_word
    <|> do
      s <- single_quoted
      let sNoQuotes = removeQuotes $ tokStr s
      case runParser lower_word () "" sNoQuotes of
        Right _ -> return $ s { tokStr = sNoQuotes }
        Left _ -> return s
    <?> "atomic_word"
    )
    where
      removeQuotes :: String -> String
      removeQuotes = init . tail
  
  -- <atomic_defined_word>  ::= <dollar_word>
  atomic_defined_word :: CharParser st Token
  atomic_defined_word = parserTrace "atomic_defined_word" (pToken dollar_word
    )
  
  
  -- <atomic_system_word>   ::= <dollar_dollar_word>
  atomic_system_word :: CharParser st Token
  atomic_system_word = parserTrace "atomic_system_word" (pToken dollar_dollar_word
    )
  
  -- <number>               ::= <integer> | <rational> | <real>
  number :: CharParser st Number
  number = parserTrace "number" (
    (liftM NumRational (liftM read rational) << skip)
    <|> (liftM NumReal (liftM read real) << skip)
    <|> (liftM NumInteger (liftM read integer) << skip)
    <?> "number"
    )
  
  -- <file_name>            ::= <single_quoted>
  file_name :: CharParser st File_name
  file_name = parserTrace "file_name" (
    single_quoted_file_name
    <|> unquoted_file_name
    <?> "file_name"
    )
  
  -- <null>                 ::=
  
  
  {- -----------------------------------------------------------------------------
  Comments
  ----------------------------------------------------------------------------- -}
  
  -- <comment>              ::- <comment_line>|<comment_block>
  comment :: CharParser st Comment
  comment = parserTrace "comment" (comment_line <|> comment_block <?> "comment"
    )
  
  -- <comment_line>         ::- [%]<printable_char>*
  comment_line :: CharParser st Comment
  comment_line = parserTrace "comment_line" (liftM Comment_line (commentLineWith "%" True) <?> "comment_line"
    )
  
  -- <comment_block>        ::: [/][*]<not_star_slash>[*][*]*[/]
  comment_block :: CharParser st Comment
  comment_block = parserTrace "comment_block" (liftM Comment_block (commentBlockWith "/*" True) <?> "comment_block"
    )
  
  -- %----  <defined_comment>    ::- <def_comment_line>|<def_comment_block>
  defined_comment :: CharParser st DefinedComment
  defined_comment = parserTrace "defined_comment" (def_comment_line <|> def_comment_block <?> "defined_comment"
    )
  
  -- %----  <def_comment_line>   ::: [%]<dollar><printable_char>*
  def_comment_line :: CharParser st DefinedComment
  def_comment_line = parserTrace "def_comment_line" (liftM Defined_comment_line (commentLineWith "%$" True)
    <?> "def_comment_line"
    )
  
  -- %----  <def_comment_block>  ::: [/][*]<dollar><not_star_slash>[*][*]*[/]
  def_comment_block :: CharParser st DefinedComment
  def_comment_block = parserTrace "def_comment_block" (liftM Defined_comment_block (commentBlockWith "/*$" True)
    <?> "def_comment_block"
    )
  
  -- %----  <system_comment>     ::- <sys_comment_line>|<sys_comment_block>
  system_comment :: CharParser st SystemComment
  system_comment = parserTrace "system_comment" (sys_comment_line <|> sys_comment_block <?> "system_comment"
    )
  
  -- %----  <sys_comment_line>   ::: [%]<dollar><dollar><printable_char>*
  sys_comment_line :: CharParser st SystemComment
  sys_comment_line = parserTrace "sys_comment_line" (liftM System_comment_line (commentLineWith "%$$" False)
    <?> "sys_comment_line"
    )
  
  -- %----  <sys_comment_block>  ::: [/][*]<dollar><dollar><not_star_slash>[*][*]*[/]
  sys_comment_block :: CharParser st SystemComment
  sys_comment_block = parserTrace "sys_comment_block" (liftM System_comment_block (commentBlockWith "/*$$" False)
    <?> "sys_comment_block"
    )
  
  commentLineWith :: String -> Bool -> CharParser st Token
  commentLineWith beginning restrict = (do
    tryString beginning
    if restrict then notFollowedBy (char '$') else return ()
    -- we use anyChar instead of printable_char for the comments to parse the whole tptp library
    pToken $ manyTill anyChar (char '\n'))
    <?> "commentLineWith"
  
  commentBlockWith :: String -> Bool -> CharParser st Token
  commentBlockWith beginning restrict = (do
    tryString beginning
    if restrict then notFollowedBy (char '$') >> return () else return ()
    -- we use anyChar instead of printable_char for the comments to parse the whole tptp library
    pToken $ manyTill anyChar (strTok "*/"))
    <?> "commentBlockWith"
  
  {- -----------------------------------------------------------------------------
  Word classes
  ----------------------------------------------------------------------------- -}
  
  -- <sq_char>            ::: ([\40-\46\50-\133\135-\176]|[\\]['\\])
  -- <single_quoted>      ::- <single_quote><sq_char><sq_char>*<single_quote>
  -- %---Space and visible characters upto ~, except ' and \
  single_quoted :: CharParser st Token
  single_quoted = parserTrace "single_quoted" (pToken (do
      char '\''
      s <- fmap concat $ many1 (tryString "\\\\" <|> tryString "\\'"
          <|> single (satisfy (\ c -> printable c && notElem c "'\\")))
      keyChar '\''
      return ( "'" ++ s ++ "'"))
    <?> "single_quoted"
    )
  
  -- For the include, we need the single quoted to be an IRI
  single_quoted_file_name :: CharParser st IRI
  single_quoted_file_name = parserTrace "single_quoted" (do
      char '\''
      s <- fmap concat $ many1 (tryString "\\\\" <|> tryString "\\'"
          <|> single (satisfy (\ c -> printable c && notElem c "'\\")))
      let s' = escapeTPTPFilePath s
      i <- case parse (iriCurie << eof) "" s' of
        Left err -> Fail.fail $ show err
        Right i -> return $ unescapeTPTPFileIRI i
      keyChar '\''
      skip
      return i
    <?> "single_quoted"
    )
  
  unquoted_file_name :: CharParser st IRI
  unquoted_file_name = parserTrace "single_quoted" (try (do
      -- a file name is always terminated by a comma or a closing parenthesis
      s <- lookAhead $ try $ manyTill anyChar $ try $ oneOf ",)"
      let s' = escapeTPTPFilePath s
      i <- case parse (iriCurie << eof) "" s' of
        Left err -> Fail.fail $ show err
        Right i -> return $ unescapeTPTPFileIRI i
      strTok s
      skip
      return i)
    <?> "single_quoted"
    )
  
  -- <do_char>              ::: ([\40-\41\43-\133\135-\176]|[\\]["\\])
  -- <distinct_object>      ::- <double_quote><do_char>*<double_quote>
  -- %---Space and visible characters upto ~, except " and \
  -- %----<distinct_object>s contain visible characters. \ is the escape character
  -- %----for " and \, i.e., \" is not the end of the <distinct_object>.
  -- %----<distinct_object>s are different from (but may be equal to) other tokens,
  -- %----e.g., "cat" is different from 'cat' and cat. Distinct objects are always
  -- %----interpreted as themselves, so if they are different they are unequal,
  -- %----e.g., "Apple" != "Microsoft" is implicit.
  distinct_object :: CharParser st Token
  distinct_object = parserTrace "distinct_object" (pToken (do
      char '"'
      s <- fmap concat $ many (tryString "\\\\" <|> tryString "\\\""
          <|> single (satisfy (\ c -> printable c && notElem c "\"\\")))
      keyChar '"'
      return ("\"" ++ s ++ "\""))
    <?> "distinct_object"
    )
  
  
  -- -- <dollar_word>          ::- <dollar><lower_word>
  dollar_word :: CharParser st String
  dollar_word = do
    prefix <- char '$' << notFollowedBy (char '$')
    word <- lower_word
    return (prefix : word)
  
  -- <dollar_dollar_word>   ::- <dollar><dollar><lower_word>
  dollar_dollar_word :: CharParser st String
  dollar_dollar_word = do
      prefix <- tryString "$$"
      word <- lower_word
      return (prefix ++ word)
    <?> "dollar_dollar_word"
  
  -- <upper_word>           ::- <upper_alpha><alpha_numeric>*
  upper_word :: CharParser st String
  upper_word = do
      u <- upper
      w <- many alpha_numeric
      return (u : w)
    <?> "upper_word"
  
  -- <lower_word>           ::- <lower_alpha><alpha_numeric>*
  lower_word :: CharParser st String
  lower_word = do
      l <- lower
      w <- many alpha_numeric
      return (l : w)
    <?> "lower_word"
  
  {- -----------------------------------------------------------------------------
  Numbers. Signs are made part of the same token here.
  ----------------------------------------------------------------------------- -}
  -- <real>                 ::- (<signed_real>|<unsigned_real>)
  real :: CharParser st String
  real = signed_real <|> unsigned_real <?> "real"
  
  -- <signed_real>          ::- <sign><unsigned_real>
  signed_real :: CharParser st String
  signed_real = try (do
      s <- sign
      r <- unsigned_real
      return (s : r))
    <?> "signed_real"
  
  -- <unsigned_real>        ::- (<decimal_fraction>|<decimal_exponent>)
  unsigned_real :: CharParser st String
  unsigned_real = decimal_exponent <|> decimal_fraction <?> "unsigned_real"
  
  -- <rational>             ::- (<signed_rational>|<unsigned_rational>)
  rational :: CharParser st String
  rational = signed_rational <|> unsigned_rational <?> "rational"
  
  -- <signed_rational>      ::- <sign><unsigned_rational>
  signed_rational :: CharParser st String
  signed_rational = try (do
      s <- sign
      r <- unsigned_rational
      return (s : r))
    <?> "signed_rational"
  
  -- <unsigned_rational>    ::- <decimal><slash><positive_decimal>
  unsigned_rational :: CharParser st String
  unsigned_rational = do
      d <- try (decimal << char '/')
      p <- positive_decimal
      return (d ++ "/" ++ p)
    <?> "unsigned_rational"
  
  -- <integer>              ::- (<signed_integer>|<unsigned_integer>)
  integer  :: CharParser st String
  integer = signed_integer <|> unsigned_integer <?> "integer"
  
  -- <signed_integer>       ::- <sign><unsigned_integer>
  signed_integer :: CharParser st String
  signed_integer = try (do
      s <- sign
      i <- unsigned_integer
      return (s : i))
    <?> "signed_integer"
  
  -- <unsigned_integer>     ::- <decimal>
  unsigned_integer :: CharParser st String
  unsigned_integer = decimal <?> "unsigned_integer"
  
  -- <decimal>              ::- (<zero_numeric>|<positive_decimal>)
  decimal :: CharParser st String
  decimal = single (char '0') <|> positive_decimal <?> "decimal"
  
  -- <positive_decimal>     ::- <non_zero_numeric><numeric>*
  positive_decimal :: CharParser st String
  positive_decimal = try (do
      nzn <- non_zero_numeric
      ns <- many digit
      return (nzn : ns))
    <?> "positive_decimal"
  
  -- <decimal_exponent>     ::- (<decimal>|<decimal_fraction>)<exponent><exp_integer>
  decimal_exponent :: CharParser st String
  decimal_exponent = try (do
      df <- try (decimal_fraction <|> decimal)
      exp <- single exponent
      exp_int <- exp_integer
      return (df ++ exp ++ exp_int))
    <?> "decimal_exponent"
  
  -- <decimal_fraction>     ::- <decimal><dot_decimal>
  decimal_fraction :: CharParser st String
  decimal_fraction = try (do
      dec <- decimal
      dd <- dot_decimal
      return (dec ++ dd))
    <?> "decimal_fraction"
  
  -- <dot_decimal>          ::- <dot><numeric><numeric>*
  dot_decimal :: CharParser st String
  dot_decimal = do
      dot <- char '.'
      num <- many1 digit
      return (dot : num)
    <?> "dot_decimal"
  
  -- <exp_integer>          ::- (<signed_exp_integer>|<unsigned_exp_integer>)
  exp_integer :: CharParser st String
  exp_integer = signed_exp_integer <|> unsigned_exp_integer <?> "exp_integer"
  
  -- <signed_exp_integer>   ::- <sign><unsigned_exp_integer>
  signed_exp_integer :: CharParser st String
  signed_exp_integer = try (do
      s <- sign
      d <- unsigned_exp_integer
      return (s : d))
    <?> "signed_exp_integer"
  
  -- <unsigned_exp_integer> ::- <numeric><numeric>*
  unsigned_exp_integer :: CharParser st String
  unsigned_exp_integer = many1 digit <?> "unsigned_exp_integer"
  
  
  {- -----------------------------------------------------------------------------
  Character classes
  ----------------------------------------------------------------------------- -}
  
  -- <sign>                 ::: [+-]
  sign :: CharParser st Char
  sign = oneOf "+-" <?> "sign"
  
  -- <exponent>             ::: [Ee]
  exponent :: CharParser st Char
  exponent = oneOf "Ee" <?> "exponent"
  
  -- <non_zero_numeric>     ::: [1-9]
  non_zero_numeric :: CharParser st Char
  non_zero_numeric = satisfy (\ c -> '1' <= c && c <= '9') <?> "non_zero_numeric"
  
  -- <alpha_numeric>        ::: (<lower_alpha>|<upper_alpha>|<numeric>|[_])
  alpha_numeric :: CharParser st Char
  alpha_numeric = satisfy (\ c -> isAlphaNum c || c == '_') <?> "alpha_numeric"
  
  -- <printable_char>       ::: .
  -- %----<printable_char> is any printable ASCII character, codes 32 (space) to 126
  -- %----(tilde). <printable_char> does not include tabs, newlines, bells, etc. The
  -- %----use of . does not not exclude tab, so this is a bit loose.
  -- printable_char :: CharParser st Char
  -- printable_char = satisfy printable <?> "printable_char"
  
  printable :: Char -> Bool
  -- the tab character is an unofficial extension
  printable c = (32 <= ord c && ord c <= 126) || c == '\t'
  
  -- NOTE: not used
  -- -- <viewable_char>        ::: [.\n]
  -- viewable_char :: CharParser st Char
  -- viewable_char = satisfy (\ c -> printable c || c == '\n')
  
  
  vline :: CharParser st Token
  vline = charTok '|'
  
  andT :: CharParser st Token
  andT = charTok '&'
  
  starT :: CharParser st Token
  starT = charTok '*'
  
  plusT :: CharParser st Token
  plusT = charTok '+'
  
  arrowT :: CharParser st Token
  arrowT = charTok '>'
  
  
  commaT :: CharParser st Token
  commaT = charTok ','
  
  dotT :: CharParser st Token
  dotT = charTok '.'
  
  colonT :: CharParser st Token
  colonT = charTok ':'
  
  {- -----------------------------------------------------------------------------
  Some lexer functions
  ----------------------------------------------------------------------------- -}
  skip :: CharParser st ()
  skip = skipMany $ forget (satisfy isSpace)
  
  pToken :: CharParser st String -> CharParser st Token
  pToken p = Lexer.pToken p << skip
  
  oBracketT :: CharParser st Token
  oBracketT = charTok '['
  
  cBracketT :: CharParser st Token
  cBracketT = charTok ']'
  
  brackets :: CharParser st a -> CharParser st a
  brackets p = oBracketT >> p << cBracketT
  
  oParenT :: CharParser st Token
  oParenT = charTok '('
  
  cParenT :: CharParser st Token
  cParenT = charTok ')'
  
  parens :: CharParser st a -> CharParser st a
  parens p = oParenT >> p << cParenT
  
  {- -----------------------------------------------------------------------------
  Some helper functions
  ----------------------------------------------------------------------------- -}
  
  strTok :: String -> CharParser st Token
  strTok s = parserTrace ("strTok " ++ show s) (pToken $ tryString s
    )
  
  charTok :: Char -> CharParser st Token
  charTok c = parserTrace ("charTok " ++ show c) (pToken $ single $ char c
    )
  
  constantsChoice :: [(String, a)] -> CharParser st a
  constantsChoice choices = choice $ map constantMapping choices
  
  constantMapping :: (String, a) -> CharParser st a
  constantMapping (s, c) = strTok s >> return c
  
  emptyBrackets :: CharParser st [a]
  emptyBrackets = try (oBracketT >> return [] << cBracketT)
  
  sepByComma1 :: CharParser st a -> CharParser st [a]
  sepByComma1 p = p `sepBy1` strTok ","
  
  -- Looks ahead without consuming input. Fails if @notToFind@ follows.
  -- Is only used to optimize performance.
  -- Apply it only to very short @notToFind@.
  parseIfNot :: Show a => CharParser st a -> CharParser st b -> CharParser st b
  parseIfNot notToFind p = lookAhead (notFollowedBy $ try notToFind) >> p
  
  skipAll :: CharParser st ()
  skipAll = skipMany (skipMany1 space <|>
                      forget ((comment >> return ()) <|>
                              (defined_comment >> return ()) <|>
                              (system_comment >> return ())))
  
  key :: CharParser st a -> CharParser st ()
  key = (>> skipAll)
  
  keyChar :: Char -> CharParser st ()
  keyChar = key . char
  