content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./TPTP/AS.der.hs
  Description :  Abstract syntax for TPTP 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
  
  Definition of abstract syntax for TPTP taken from [1]
  
  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).
  
  [2] C. Kaliszyk, G. Sutcliffe and F. Rabe:
      TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism
      <https://kwarc.info/people/frabe/Research/KRS_thf1_16.pdf>
      Note: for further information on TF0, TF1, TH0 and TH1
  -}
  
  module TPTP.AS where
  
  import Common.Id as Id
  import Common.IRI
  import Syntax.AS_Structured ()
  import qualified Common.AS_Annotation as AS_Anno
  
  import Data.Data
  
  -- DrIFT command
  {-! global: GetRange !-}
  
  newtype BASIC_SPEC = Basic_spec [AS_Anno.Annoted TPTP]
                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- Files
  
  -- %----Files. Empty file is OK.
  -- <TPTP_file>            ::= <TPTP_input>*<Paste>
  newtype TPTP = TPTP [TPTP_input]
                 deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <TPTP_input>           ::= <annotated_formula> | <include>
  data TPTP_input = Annotated_formula Annotated_formula
                  | TPTP_include Include
                  | TPTP_comment Comment
                  | TPTP_defined_comment DefinedComment
                  | TPTP_system_comment SystemComment
                    deriving (Show, Ord, Eq, Data, Typeable)
  
  -- Comments
  
  data Comment = Comment_line Token
               | Comment_block Token
                 deriving (Show, Eq, Ord, Data, Typeable)
  
  data DefinedComment = Defined_comment_line Token
                      | Defined_comment_block Token
                        deriving (Show, Eq, Ord, Data, Typeable)
  
  data SystemComment = System_comment_line Token
                     | System_comment_block Token
                       deriving (Show, Eq, Ord, Data, Typeable)
  
  -- %----Formula records
  -- <annotated_formula>    ::= <thf_annotated> | <tfx_annotated> | <tff_annotated> |
  --                            <tcf_annotated> | <fof_annotated> | <cnf_annotated> |
  --                            <tpi_annotated>
  data Annotated_formula = AF_THF_Annotated THF_annotated
                         | AF_TFX_Annotated TFX_annotated
                         | AF_TFF_Annotated TFF_annotated
                         | AF_TCF_Annotated TCF_annotated
                         | AF_FOF_Annotated FOF_annotated
                         | AF_CNF_Annotated CNF_annotated
                         | AF_TPI_Annotated TPI_annotated
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tpi_annotated>        ::= tpi(<name>,<formula_role>,<tpi_formula><annotations>).
  data TPI_annotated = TPI_annotated Name Formula_role TPI_formula Annotations
                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tpi_formula>          ::= <fof_formula>
  type TPI_formula = FOF_formula
  
  -- <thf_annotated>        ::= thf(<name>,<formula_role>,<thf_formula>
  --                            <annotations>).
  data THF_annotated = THF_annotated Name Formula_role THF_formula Annotations
                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tfx_annotated>        ::= tfx(<name>,<formula_role>,<tfx_formula>
  --                            <annotations>).
  data TFX_annotated = TFX_annotated Name Formula_role TFX_formula Annotations
                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_annotated>        ::= tff(<name>,<formula_role>,<tff_formula>
  --                            <annotations>).
  data TFF_annotated = TFF_annotated Name Formula_role TFF_formula Annotations
                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tcf_annotated>        ::= tcf(<name>,<formula_role>,<tcf_formula>
  --                            <annotations>).
  data TCF_annotated = TCF_annotated Name Formula_role TCF_formula Annotations
                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_annotated>        ::= fof(<name>,<formula_role>,<fof_formula>
  --                            <annotations>).
  data FOF_annotated = FOF_annotated Name Formula_role FOF_formula Annotations
                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <cnf_annotated>        ::= cnf(<name>,<formula_role>,<cnf_formula>
  --                            <annotations>).
  data CNF_annotated = CNF_annotated Name Formula_role CNF_formula Annotations
                       deriving (Show, Ord, Eq, Data, Typeable)
  
  name :: Annotated_formula -> Name
  name f = case f of
    AF_THF_Annotated (THF_annotated n _ _ _) -> n
    AF_TFX_Annotated (TFX_annotated n _ _ _) -> n
    AF_TFF_Annotated (TFF_annotated n _ _ _) -> n
    AF_TCF_Annotated (TCF_annotated n _ _ _) -> n
    AF_FOF_Annotated (FOF_annotated n _ _ _) -> n
    AF_CNF_Annotated (CNF_annotated n _ _ _) -> n
    AF_TPI_Annotated (TPI_annotated n _ _ _) -> n
  
  formulaRole :: Annotated_formula -> Formula_role
  formulaRole f = case f of
    AF_THF_Annotated (THF_annotated _ r _ _) -> r
    AF_TFX_Annotated (TFX_annotated _ r _ _) -> r
    AF_TFF_Annotated (TFF_annotated _ r _ _) -> r
    AF_TCF_Annotated (TCF_annotated _ r _ _) -> r
    AF_FOF_Annotated (FOF_annotated _ r _ _) -> r
    AF_CNF_Annotated (CNF_annotated _ r _ _) -> r
    AF_TPI_Annotated (TPI_annotated _ r _ _) -> r
  
  annotations :: Annotated_formula -> Annotations
  annotations f = case f of
    AF_THF_Annotated (THF_annotated _ _ _ a) -> a
    AF_TFX_Annotated (TFX_annotated _ _ _ a) -> a
    AF_TFF_Annotated (TFF_annotated _ _ _ a) -> a
    AF_TCF_Annotated (TCF_annotated _ _ _ a) -> a
    AF_FOF_Annotated (FOF_annotated _ _ _ a) -> a
    AF_CNF_Annotated (CNF_annotated _ _ _ a) -> a
    AF_TPI_Annotated (TPI_annotated _ _ _ a) -> a
  
  -- <annotations>          ::= ,<source><optional_info> | <null>
  newtype Annotations = Annotations (Maybe (Source, Optional_info))
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  -- Types for problems
  
  -- %----Types for problems.
  -- <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
  data Formula_role = Axiom
                    | Hypothesis
                    | Definition
                    | Assumption
                    | Lemma
                    | Theorem
                    | Corollary
                    | Conjecture
                    | Negated_conjecture
                    | Plain
                    | Type
                    | Fi_domain
                    | Fi_functors
                    | Fi_predicates
                    | Unknown
                    | Other_formula_role Token
                      -- ^ For future updates. Should not be used.
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----THF formulae.
  -- <thf_formula>          ::= <thf_logic_formula> | <thf_sequent>
  data THF_formula = THFF_logic THF_logic_formula
                   | THFF_sequent THF_sequent
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_logic_formula>    ::= <thf_binary_formula> | <thf_unitary_formula> |
  --                            <thf_type_formula> | <thf_subtype>
  data THF_logic_formula = THFLF_binary THF_binary_formula
                         | THFLF_unitary THF_unitary_formula
                         | THFLF_type THF_type_formula
                         | THFLF_subtype THF_subtype
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_binary_formula>   ::= <thf_binary_pair> | <thf_binary_tuple>
  data THF_binary_formula = THFBF_pair THF_binary_pair
                          | THFBF_tuple THF_binary_tuple
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----Only some binary connectives can be written without ()s.
  -- %----There's no precedence among binary connectives
  -- <thf_binary_pair>      ::= <thf_unitary_formula> <thf_pair_connective>
  --                            <thf_unitary_formula>
  data THF_binary_pair = THF_binary_pair THF_pair_connective THF_unitary_formula THF_unitary_formula
                         deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_binary_tuple>     ::= <thf_or_formula> | <thf_and_formula> |
  --                            <thf_apply_formula>
  data THF_binary_tuple = THFBT_or THF_or_formula
                        | THFBT_and THF_and_formula
                        | THFBT_apply THF_apply_formula
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_or_formula>       ::= <thf_unitary_formula> <vline> <thf_unitary_formula> |
  --                            <thf_or_formula> <vline> <thf_unitary_formula>
  
  type THF_or_formula = [THF_unitary_formula]
  
  -- <thf_and_formula>      ::= <thf_unitary_formula> & <thf_unitary_formula> |
  --                            <thf_and_formula> & <thf_unitary_formula>
  type THF_and_formula = [THF_unitary_formula]
  
  -- <thf_apply_formula>    ::= <thf_unitary_formula> @ <thf_unitary_formula> |
  --                            <thf_apply_formula> @ <thf_unitary_formula>
  type THF_apply_formula = [THF_unitary_formula]
  
  -- <thf_unitary_formula>  ::= <thf_quantified_formula> | <thf_unary_formula> |
  --                            <thf_atom> | <thf_conditional> | <thf_let> |
  --                            <thf_tuple> | (<thf_logic_formula>)
  data THF_unitary_formula = THFUF_quantified THF_quantified_formula
                           | THFUF_unary THF_unary_formula
                           | THFUF_atom THF_atom
                           | THFUF_conditional THF_conditional
                           | THFUF_let THF_let
                           | THFUF_tuple THF_tuple
                           | THFUF_logic THF_logic_formula
                             deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_quantified_formula> ::= <thf_quantification> <thf_unitary_formula>
  data THF_quantified_formula = THF_quantified_formula THF_quantification THF_unitary_formula
                                deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_quantification>   ::= <thf_quantifier> [<thf_variable_list>] :
  data THF_quantification = THF_quantification THF_quantifier THF_variable_list
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_variable_list>    ::= <thf_variable> | <thf_variable>,<thf_variable_list>
  type THF_variable_list = [THF_variable]
  
  -- <thf_variable>         ::= <thf_typed_variable> | <variable>
  data THF_variable = THFV_typed THF_typed_variable
                    | THFV_variable Variable
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_typed_variable>   ::= <variable> : <thf_top_level_type>
  data THF_typed_variable = THF_typed_variable Variable THF_top_level_type
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_unary_formula>    ::= <thf_unary_connective> (<thf_logic_formula>)
  data THF_unary_formula = THF_unary_formula THF_unary_connective THF_logic_formula
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_atom>             ::= <thf_function> | <variable> | <defined_term> |
  --                            <thf_conn_term>
  data THF_atom = THF_atom_function THF_function
                | THF_atom_variable Variable
                | THF_atom_defined Defined_term
                | THF_atom_conn THF_conn_term
                  deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_function>         ::= <atom> | <functor>(<thf_arguments>) |
  --                            <defined_functor>(<thf_arguments>) |
  --                            <system_functor>(<thf_arguments>)
  data THF_function = THFF_atom Atom
                    | THFF_functor TPTP_functor THF_arguments
                    | THFF_defined Defined_functor THF_arguments
                    | THFF_system System_functor THF_arguments
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_conn_term>        ::= <thf_pair_connective> | <assoc_connective> |
  --                            <thf_unary_connective>
  data THF_conn_term = THFC_pair THF_pair_connective
                     | THFC_assoc Assoc_connective
                     | THFC_unary THF_unary_connective
                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_conditional>      ::= $ite(<thf_logic_formula>,<thf_logic_formula>,
  --                             <thf_logic_formula>)
  data THF_conditional = THF_conditional THF_logic_formula THF_logic_formula THF_logic_formula --  $ite
                         deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----The LHS of a term or formula binding must be a non-variable term that
  -- %----is flat with pairwise distinct variable arguments, and the variables in
  -- %----the LHS must be exactly those bound in the universally quantified variable
  -- %----list, in the same order. Let definitions are not recursive: a non-variable
  -- %----symbol introduced in the LHS of a let definition cannot occur in the RHS.
  -- %----If a symbol with the same signature as the one in the LHS of the binding
  -- %----is declared above the let expression (at the top level or in an
  -- %----encompassing let) then it can be used in the RHS of the binding, but it is
  -- %----not accessible in the term or formula of the let expression. Let
  -- %----expressions can be eliminated by a simple definition expansion.
  -- <thf_let>              ::= $let(<thf_unitary_formula>,<thf_formula>)
  -- <thf_let>              :== $let(<thf_let_defns>,<thf_formula>)
  data THF_let = THF_let THF_let_defns THF_formula
                 deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_let_defns>        :== <thf_let_defn> | [<thf_let_defn_list>]
  data THF_let_defns = THFLD_single THF_let_defn
                     | THFLD_many THF_let_defn_list
                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_let_defn_list>    :== <thf_let_defn> | <thf_let_defn>,<thf_let_defn_list>
  type THF_let_defn_list = [THF_let_defn]
  
  -- <thf_let_defn>         :== <thf_let_quantified_defn> | <thf_let_plain_defn>
  data THF_let_defn = THFLD_quantified THF_let_quantified_defn
                    | THFLD_plain THF_let_plain_defn
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_let_quantified_defn> :== <thf_quantification> (<thf_let_plain_defn>)
  data THF_let_quantified_defn = THF_let_quantified_defn THF_quantification THF_let_plain_defn
                                 deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_let_plain_defn>   :== <thf_let_defn_LHS> <assignment> <thf_formula>
  data THF_let_plain_defn = THF_let_plain_defn THF_let_defn_LHS THF_formula
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <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
  data THF_let_defn_LHS = THFLDL_constant Constant
                        | THFLDL_functor TPTP_functor FOF_arguments
                        | THFLDL_tuple THF_tuple
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_arguments>        ::= <thf_formula_list>
  type THF_arguments = THF_formula_list
  
  -- <thf_type_formula>     ::= <thf_typeable_formula> : <thf_top_level_type>
  -- <thf_type_formula>     :== <constant> : <thf_top_level_type>
  data THF_type_formula = THFTF_typeable THF_typeable_formula THF_top_level_type
                        | THFTF_constant Constant THF_top_level_type
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_typeable_formula> ::= <thf_atom> | (<thf_logic_formula>)
  data THF_typeable_formula = THFTF_atom THF_atom
                            | THFTF_logic THF_logic_formula
                              deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_subtype>          ::= <thf_atom> <subtype_sign> <thf_atom>
  data THF_subtype = THF_subtype THF_atom THF_atom
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  
  -- %----<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>
  data THF_top_level_type = THFTLT_unitary THF_unitary_type
                          | THFTLT_mapping THF_mapping_type
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_unitary_type>     ::= <thf_unitary_formula> | (<thf_binary_type>)
  data THF_unitary_type = THFUT_unitary THF_unitary_formula
                        | THFUT_binary THF_binary_type
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- Each of these binary types has at least two (!) list entries.
  -- <thf_binary_type>      ::= <thf_mapping_type> | <thf_xprod_type> |
  --                            <thf_union_type>
  data THF_binary_type = THFBT_mapping THF_mapping_type
                       | THFBT_xprod THF_xprod_type
                       | THFBT_union THF_union_type
                         deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_mapping_type>     ::= <thf_unitary_type> <arrow> <thf_unitary_type> |
  --                            <thf_unitary_type> <arrow> <thf_mapping_type>
  type THF_mapping_type = [THF_unitary_type] -- right associative
  
  -- <thf_xprod_type>       ::= <thf_unitary_type> <star> <thf_unitary_type> |
  --                            <thf_xprod_type> <star> <thf_unitary_type>
  type THF_xprod_type = [THF_unitary_type] -- left associative
  
  -- <thf_union_type>       ::= <thf_unitary_type> <plus> <thf_unitary_type> |
  --                            <thf_union_type> <plus> <thf_unitary_type>
  type THF_union_type = [THF_unitary_type] -- right associative
  
  -- %----Sequents using the Gentzen arrow
  -- <thf_sequent>          ::= <thf_tuple> <gentzen_arrow> <thf_tuple> |
  --                            (<thf_sequent>)
  data THF_sequent = THFS_plain THF_tuple THF_tuple
                   | THFS_parens THF_sequent
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_tuple>            ::= [] | [<thf_formula_list>]
  newtype THF_tuple = THF_tuple THF_formula_list
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_formula_list>     ::= <thf_logic_formula> |
  --                            <thf_logic_formula>,<thf_formula_list>
  type THF_formula_list = [THF_logic_formula]
  
  -- NOTE: not used by parser
  -- %----New material for modal logic semantics, not integrated yet
  -- <logic_defn_rule>      :== <logic_defn_LHS> <assignment> <logic_defn_RHS>-
  -- data Logic_defn_rule = Logic_defn_rule Logic_defn_LHS Logic_defn_RHS
  --                        deriving (Show, Ord, Eq, Data, Typeable)
  
  -- NOTE: not used by parser
  -- <logic_defn_LHS>       :== <logic_defn_value> | <thf_top_level_type>  | <name>
  -- <logic_defn_LHS>       :== $constants | $quantification | $consequence |
  --                            $modalities
  --                            %----The $constants, $quantification, and $consequence apply to all of the
  --                            %----$modalities. Each of these may be specified only once, but not necessarily
  --                            %----all in a single annotated formula.-
  -- data Logic_defn_LHS = Logic_defn_LHS_value Logic_defn_value
  --                     | Logic_defn_LHS_THF_Top_level_type THF_top_level_type
  --                     | Logic_defn_LHS_name Name
  --                     | LDLC_constants
  --                     | LDLC_quantification
  --                     | LDLC_consequence
  --                     | LDLC_modalities
  --                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- NOTE: not used by parser
  -- <logic_defn_RHS>       :== <logic_defn_value> | <thf_unitary_formula>-
  -- data Logic_defn_RHS = Logic_defn_RHS_value Logic_defn_value
  --                     | Logic_defn_RNG_THF_Unitary_forumla THF_unitary_formula
  --                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- NOTE: not used by parser
  -- <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-
  -- data 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
  --                       deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----TFX formulae
  -- <tfx_formula>          ::= <tfx_logic_formula> | <thf_sequent>
  data TFX_formula = TFXF_logic TFX_logic_formula
                   | TFXF_sequent THF_sequent
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tfx_logic_formula>    ::= <thf_logic_formula>
  -- % <tfx_logic_formula>    ::= <thf_binary_formula> | <thf_unitary_formula> |
  -- %                            <tff_typed_atom> | <tff_subtype>
  data TFX_logic_formula = TFXLF_binary THF_binary_formula
                         | TFXLF_unitary THF_unitary_formula
                         | TFXLF_typed TFF_typed_atom
                         | TFXLF_subtype TFF_subtype
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----TFF formulae.
  -- <tff_formula>          ::= <tff_logic_formula> | <tff_typed_atom> |
  --                            <tff_sequent>
  data TFF_formula = TFFF_logic TFF_logic_formula
                   | TFFF_atom TFF_typed_atom
                   | TFFF_sequent TFF_sequent
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_logic_formula>    ::= <tff_binary_formula> | <tff_unitary_formula> |
  --                            <tff_subtype>
  data TFF_logic_formula = TFFLF_binary TFF_binary_formula
                         | TFFLF_unitary TFF_unitary_formula
                         | TFFLF_subtype TFF_subtype
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_binary_formula>   ::= <tff_binary_nonassoc> | <tff_binary_assoc>
  data TFF_binary_formula = TFFBF_nonassoc TFF_binary_nonassoc
                          | TFFBF_assoc TFF_binary_assoc
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_binary_nonassoc>  ::= <tff_unitary_formula> <binary_connective>
  --                            <tff_unitary_formula>
  data TFF_binary_nonassoc = TFF_binary_nonassoc Binary_connective TFF_unitary_formula TFF_unitary_formula
                             deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_binary_assoc>     ::= <tff_or_formula> | <tff_and_formula>
  data TFF_binary_assoc = TFFBA_or TFF_or_formula
                        | TFFBA_and TFF_and_formula
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_or_formula>       ::= <tff_unitary_formula> <vline> <tff_unitary_formula> |
  --                            <tff_or_formula> <vline> <tff_unitary_formula>
  type TFF_or_formula = [TFF_unitary_formula]
  
  -- <tff_and_formula>      ::= <tff_unitary_formula> & <tff_unitary_formula> |
  --                            <tff_and_formula> & <tff_unitary_formula>
  type TFF_and_formula = [TFF_unitary_formula]
  
  -- <tff_unitary_formula>  ::= <tff_quantified_formula> | <tff_unary_formula> |
  --                            <tff_atomic_formula> | <tff_conditional> |
  --                            <tff_let> | (<tff_logic_formula>)
  data TFF_unitary_formula = TFFUF_quantified TFF_quantified_formula
                           | TFFUF_unary TFF_unary_formula
                           | TFFUF_atomic TFF_atomic_formula
                           | TFFUF_conditional TFF_conditional
                           | TFFUF_let TFF_let
                           | TFFUF_logic TFF_logic_formula
                             deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_quantified_formula> ::= <fof_quantifier> [<tff_variable_list>] :
  --                            <tff_unitary_formula>
  data TFF_quantified_formula = TFF_quantified_formula FOF_quantifier TFF_variable_list TFF_unitary_formula
                                deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_variable_list>    ::= <tff_variable> | <tff_variable>,<tff_variable_list>
  type TFF_variable_list = [TFF_variable]
  
  -- <tff_variable>         ::= <tff_typed_variable> | <variable>
  data TFF_variable = TFFV_typed TFF_typed_variable
                    | TFFV_variable Variable
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_typed_variable>   ::= <variable> : <tff_atomic_type>
  data TFF_typed_variable = TFF_typed_variable Variable TFF_atomic_type
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_unary_formula>    ::= <unary_connective> <tff_unitary_formula> |
  --                            <fof_infix_unary>
  data TFF_unary_formula = TFFUF_connective Unary_connective TFF_unitary_formula
                         | TFFUF_infix FOF_infix_unary
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_atomic_formula>   ::= <fof_atomic_formula>
  type TFF_atomic_formula = FOF_atomic_formula
  
  -- <tff_conditional>      ::= $ite_f(<tff_logic_formula>,<tff_logic_formula>,
  --                            <tff_logic_formula>)
  data TFF_conditional = TFF_conditional TFF_logic_formula TFF_logic_formula TFF_logic_formula --  $ite_f
                         deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_let>              ::= $let_tf(<tff_let_term_defns>,<tff_formula>) |
  --                            $let_ff(<tff_let_formula_defns>,<tff_formula>)
  data TFF_let = TFF_let_term_defns TFF_let_term_defns TFF_formula
               | TFF_let_formula_defns TFF_let_formula_defns TFF_formula
                 deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----See the commentary for <thf_let>.
  -- <tff_let_term_defns>   ::= <tff_let_term_defn> | [<tff_let_term_list>]
  data TFF_let_term_defns = TFFLTD_single TFF_let_term_defn
                          | TFFLTD_many TFF_let_term_list
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_let_term_list>    ::= <tff_let_term_defn> |
  --                            <tff_let_term_defn>,<tff_let_term_list>
  type TFF_let_term_list = [TFF_let_term_defn]
  
  -- <tff_let_term_defn>    ::= ! [<tff_variable_list>] : <tff_let_term_defn> |
  --                            <tff_let_term_binding>
  data TFF_let_term_defn = TFFLTD_variable TFF_variable_list TFF_let_term_defn
                         | TFFLTD_binding TFF_let_term_binding
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_let_term_binding> ::= <fof_plain_term> = <fof_term> |
  --                            (<tff_let_term_binding>)
  data TFF_let_term_binding = TFFLTB_plain FOF_plain_term FOF_term
                            | TFFLTB_binding TFF_let_term_binding
                              deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_let_formula_defns> ::= <tff_let_formula_defn> | [<tff_let_formula_list>]
  data TFF_let_formula_defns = TFFLFD_single TFF_let_formula_defn
                             | TFFLFD_many TFF_let_formula_list
                               deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_let_formula_list> ::= <tff_let_formula_defn> |
  --                            <tff_let_formula_defn>,<tff_let_formula_list>
  type TFF_let_formula_list = [TFF_let_formula_defn]
  
  -- <tff_let_formula_defn> ::= ! [<tff_variable_list>] : <tff_let_formula_defn> |
  --                            <tff_let_formula_binding>
  data TFF_let_formula_defn = TFFLFD_variable TFF_variable_list TFF_let_formula_defn
                            | TFFLFD_binding TFF_let_formula_binding
                              deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_let_formula_binding> ::= <fof_plain_atomic_formula> <=>
  --                            <tff_unitary_formula> | (<tff_let_formula_binding>)
  data TFF_let_formula_binding = TFFLFB_plain FOF_plain_atomic_formula TFF_unitary_formula
                               | TFFLFB_binding TFF_let_formula_binding
                                 deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_sequent>          ::= <tff_formula_tuple> <gentzen_arrow>
  --                            <tff_formula_tuple> | (<tff_sequent>)
  data TFF_sequent = TFFS_plain TFF_formula_tuple TFF_formula_tuple
                   | TFFS_parens TFF_sequent
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_formula_tuple>    ::= [] | [<tff_formula_tuple_list>]
  newtype TFF_formula_tuple = TFF_formula_tuple TFF_formula_tuple_list
                              deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_formula_tuple_list> ::= <tff_logic_formula> |
  --                            <tff_logic_formula>,<tff_formula_tuple_list>
  type TFF_formula_tuple_list = [TFF_logic_formula]
  
  -- %----<tff_typed_atom> can appear only at top level
  -- <tff_typed_atom>       ::= <untyped_atom> : <tff_top_level_type> |
  --                            (<tff_typed_atom>)
  data TFF_typed_atom = TFFTA_plain Untyped_atom TFF_top_level_type
                      | TFFTA_parens TFF_typed_atom
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_subtype>          ::= <untyped_atom> <subtype_sign> <atom>
  data TFF_subtype = TFF_subtype Untyped_atom Atom
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----See <thf_top_level_type> for commentary.
  -- <tff_top_level_type>   ::= <tff_atomic_type> | <tff_mapping_type> |
  --                            <tf1_quantified_type> | (<tff_top_level_type>)
  data TFF_top_level_type = TFFTLT_atomic TFF_atomic_type
                          | TFFTLT_mapping TFF_mapping_type
                          | TFFTLT_quantified TF1_quantified_type
                          | TFFTLT_parens TFF_top_level_type
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tf1_quantified_type>  ::= !> [<tff_variable_list>] : <tff_monotype>
  data TF1_quantified_type = TF1_quantified_type TFF_variable_list TFF_monotype
                             deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_monotype>         ::= <tff_atomic_type> | (<tff_mapping_type>)
  data TFF_monotype = TFFMT_atomic TFF_atomic_type
                    | TFFMT_mapping TFF_mapping_type
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_unitary_type>     ::= <tff_atomic_type> | (<tff_xprod_type>)
  data TFF_unitary_type = TFFUT_atomic TFF_atomic_type
                        | TFFUT_xprod TFF_xprod_type
                          deriving (Show, Ord, Eq, Data, Typeable)
  -- <tff_atomic_type>      ::= <type_constant> | <defined_type> |
  --                            <type_functor>(<tff_type_arguments>) | <variable>
  data TFF_atomic_type = TFFAT_constant Type_constant
                       | TFFAT_defined Defined_type
                       | TFFAT_functor Type_functor TFF_type_arguments
                       | TFFAT_variable Variable
                         deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_type_arguments>   ::= <tff_atomic_type> |
  --                            <tff_atomic_type>,<tff_type_arguments>
  type TFF_type_arguments = [TFF_atomic_type]
  
  -- %----For consistency with <thf_unitary_type> (the analogue in thf),
  -- %----<tff_atomic_type> should also allow (<tff_atomic_type>), but that causes
  -- %----ambiguity.
  -- <tff_mapping_type>     ::= <tff_unitary_type> <arrow> <tff_atomic_type>
  data TFF_mapping_type = TFF_mapping_type TFF_unitary_type TFF_atomic_type
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tff_xprod_type>       ::= <tff_unitary_type> <star> <tff_atomic_type> |
  --                            <tff_xprod_type> <star> <tff_atomic_type>
  data TFF_xprod_type = TFF_xprod_type TFF_unitary_type [TFF_atomic_type]
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  
  -- %----TCF formulae.
  -- <tcf_formula>          ::= <tcf_logic_formula> | <tff_typed_atom>
  data TCF_formula = TCFF_logic TCF_logic_formula
                   | TCFF_atom TFF_typed_atom
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tcf_logic_formula>    ::= <tcf_quantified_formula> | <cnf_formula>
  data TCF_logic_formula = TCFLF_quantified TCF_quantified_formula
                         | TCFLF_cnf CNF_formula
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <tcf_quantified_formula> ::= ! [<tff_variable_list>] : <cnf_formula>
  data TCF_quantified_formula = TCF_quantified TFF_variable_list CNF_formula
                                deriving (Show, Ord, Eq, Data, Typeable)
  
  
  -- %----FOF formulae.
  -- <fof_formula>          ::= <fof_logic_formula> | <fof_sequent>
  data FOF_formula = FOFF_logic FOF_logic_formula
                   | FOFF_sequent FOF_sequent
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_logic_formula>    ::= <fof_binary_formula> | <fof_unitary_formula>
  data FOF_logic_formula = FOFLF_binary FOF_binary_formula
                         | FOFLF_unitary FOF_unitary_formula
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----Future answer variable ideas | <answer_formula>
  -- <fof_binary_formula>   ::= <fof_binary_nonassoc> | <fof_binary_assoc>
  data FOF_binary_formula = FOFBF_nonassoc FOF_binary_nonassoc
                          | FOFBF_assoc FOF_binary_assoc
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----Only some binary connectives are associative
  -- %----There's no precedence among binary connectives
  -- <fof_binary_nonassoc>  ::= <fof_unitary_formula> <binary_connective>
  --                            <fof_unitary_formula>
  data FOF_binary_nonassoc = FOF_binary_nonassoc Binary_connective FOF_unitary_formula FOF_unitary_formula
                             deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----Associative connectives & and | are in <binary_assoc>
  -- <fof_binary_assoc>     ::= <fof_or_formula> | <fof_and_formula>
  data FOF_binary_assoc = FOFBA_or FOF_or_formula
                        | FOFBA_and FOF_and_formula
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_or_formula>       ::= <fof_unitary_formula> <vline> <fof_unitary_formula> |
  --                            <fof_or_formula> <vline> <fof_unitary_formula>
  type FOF_or_formula = [FOF_unitary_formula]
  
  -- <fof_and_formula>      ::= <fof_unitary_formula> & <fof_unitary_formula> |
  --                            <fof_and_formula> & <fof_unitary_formula>
  type FOF_and_formula = [FOF_unitary_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>)
  data FOF_unitary_formula = FOFUF_quantified FOF_quantified_formula
                           | FOFUF_unary FOF_unary_formula
                           | FOFUF_atomic FOF_atomic_formula
                           | FOFUF_logic FOF_logic_formula
                             deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_quantified_formula> ::= <fof_quantifier> [<fof_variable_list>] :
  --                            <fof_unitary_formula>
  data FOF_quantified_formula = FOF_quantified_formula FOF_quantifier FOF_variable_list FOF_unitary_formula
                                deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_variable_list>    ::= <variable> | <variable>,<fof_variable_list>
  type FOF_variable_list = [Variable]
  
  -- <fof_unary_formula>    ::= <unary_connective> <fof_unitary_formula> |
  --                            <fof_infix_unary>
  data FOF_unary_formula = FOFUF_connective Unary_connective FOF_unitary_formula
                         | FOFUF_infix FOF_infix_unary
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_infix_unary>      ::= <fof_term> <infix_inequality> <fof_term>
  data FOF_infix_unary = FOF_infix_unary FOF_term FOF_term
                         deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_atomic_formula>   ::= <fof_plain_atomic_formula> |
  --                            <fof_defined_atomic_formula> |
  --                            <fof_system_atomic_formula>
  data FOF_atomic_formula = FOFAT_plain FOF_plain_atomic_formula
                          | FOFAT_defined FOF_defined_atomic_formula
                          | FOFAT_system FOF_system_atomic_formula
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_plain_atomic_formula> ::= <fof_plain_term>
  -- <fof_plain_atomic_formula> :== <proposition> | <predicate>(<fof_arguments>)
  data FOF_plain_atomic_formula = FOFPAF_proposition Proposition
                                | FOFPAF_predicate Predicate FOF_arguments
                                  deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_defined_atomic_formula> ::= <fof_defined_plain_formula> |
  --                            <fof_defined_infix_formula>
  data FOF_defined_atomic_formula = FOFDAF_plain FOF_defined_plain_formula
                                  | FOFDAF_infix FOF_defined_infix_formula
                                    deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_defined_plain_formula> ::= <fof_defined_plain_term>
  -- <fof_defined_plain_formula> :== <defined_proposition> |
  --                            <defined_predicate>(<fof_arguments>)
  data FOF_defined_plain_formula = FOFDPF_proposition Defined_proposition
                                 | FOFDPF_predicate Defined_predicate FOF_arguments
                                   deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_defined_infix_formula> ::= <fof_term> <defined_infix_pred> <fof_term>
  data FOF_defined_infix_formula = FOF_defined_infix_formula Defined_infix_pred FOF_term FOF_term
                                   deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----System terms have system specific interpretations
  -- <fof_system_atomic_formula> ::= <fof_system_term>
  -- %----<fof_system_atomic_formula>s are used for evaluable predicates that are
  -- %----available in particular tools. The predicate names are not controlled
  -- %----by the TPTP syntax, so use with due care. The same is true for
  -- %----<fof_system_term>s.
  newtype FOF_system_atomic_formula = FOF_system_atomic_formula FOF_system_term
                                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----FOF terms.
  -- <fof_plain_term>       ::= <constant> | <functor>(<fof_arguments>)
  data FOF_plain_term = FOFPT_constant Constant
                      | FOFPT_functor TPTP_functor FOF_arguments
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----Defined terms have TPTP specific interpretations
  -- <fof_defined_term>     ::= <defined_term> | <fof_defined_atomic_term>
  data FOF_defined_term = FOFDT_term Defined_term
                        | FOFDT_atomic FOF_defined_atomic_term
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_defined_atomic_term>  ::= <fof_defined_plain_term>
  -- %----None yet             | <defined_infix_term>
  data FOF_defined_atomic_term = FOFDAT_plain FOF_defined_plain_term
                               --  | FOFDAT_indix Defined_infix_term
                                 deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----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.
  data FOF_defined_plain_term = FOFDPT_constant Defined_constant
                              | FOFDPT_functor Defined_functor FOF_arguments
                                deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----System terms have system specific interpretations
  -- <fof_system_term>      ::= <system_constant> | <system_functor>(<fof_arguments>)
  data FOF_system_term = FOFST_constant System_constant
                       | FOFST_functor System_functor FOF_arguments
                         deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----Arguments recurse back up to terms (this is the FOF world here)
  -- <fof_arguments>        ::= <fof_term> | <fof_term>,<fof_arguments>
  type FOF_arguments = [FOF_term]
  
  -- %----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>
  data FOF_term = FOFT_function FOF_function_term
                | FOFT_variable Variable
                | FOFT_conditional TFF_conditional_term
                | FOFT_let TFF_let_term
                  deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %% 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>
  data FOF_function_term = FOFFT_plain FOF_plain_term
                         | FOFFT_defined FOF_defined_term
                         | FOFFT_system FOF_system_term
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----Conditional terms should be used by only TFF.
  -- <tff_conditional_term> ::= $ite_t(<tff_logic_formula>,<fof_term>,<fof_term>)
  data TFF_conditional_term = TFF_conditional_term TFF_logic_formula FOF_term FOF_term
                              deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----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>)
  data TFF_let_term = TFFLT_formula TFF_let_formula_defns FOF_term
                    | TFFLT_term TFF_let_term_defns FOF_term
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  {-
  %----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>)
  data FOF_sequent = FOFS_plain FOF_formula_tuple FOF_formula_tuple
                   | FOFS_parens FOF_sequent
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_formula_tuple>    ::= [] | [<fof_formula_tuple_list>]
  newtype FOF_formula_tuple = FOF_formula_tuple FOF_formula_tuple_list
                              deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <fof_formula_tuple_list> ::= <fof_logic_formula> |
  --                            <fof_logic_formula>,<fof_formula_tuple_list>
  type FOF_formula_tuple_list = [FOF_logic_formula]
  
  
  -- %----CNF formulae (variables implicitly universally quantified)
  -- <cnf_formula>          ::= <disjunction> | (<disjunction>)
  data CNF_formula = CNFF_plain Disjunction
                   | CNFF_parens Disjunction
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <disjunction>          ::= <literal> | <disjunction> <vline> <literal>
  newtype Disjunction = Disjunction [Literal]
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <literal>              ::= <fof_atomic_formula> | ~ <fof_atomic_formula> |
  --                            <fof_infix_unary>
  data Literal = Lit_atomic FOF_atomic_formula
               | Lit_negative FOF_atomic_formula
               | Lit_fof_infix FOF_infix_unary
                 deriving (Show, Ord, Eq, Data, Typeable)
  
  
  
  -- %----Connectives - THF
  -- <thf_quantifier>       ::= <fof_quantifier> | <th0_quantifier> |
  --                            <th1_quantifier>
  data THF_quantifier = THFQ_fof FOF_quantifier
                      | THFQ_th0 TH0_quantifier
                      | THFQ_th1 TH1_quantifier
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  
  -- %----TH0 quantifiers are also available in TH1
  -- <th1_quantifier>       ::= !> | ?*
  data TH1_quantifier = TH1_DependentProduct       -- !>
                      | TH1_DependentSum           -- ?*
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <th0_quantifier>       ::= ^ | @+ | @-
  data TH0_quantifier = TH0_LambdaBinder           -- ^
                      | TH0_IndefiniteDescription  -- @+
                      | TH0_DefiniteDescription    -- @-
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_pair_connective>  ::= <infix_equality> | <infix_inequality> |
  --                            <binary_connective> | <assignment>
  data THF_pair_connective = THF_infix_equality
                           | Infix_inequality
                           | THFPC_binary Binary_connective
                           | THF_assignment
                             deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <thf_unary_connective> ::= <unary_connective> | <th1_unary_connective>
  data THF_unary_connective = THFUC_unary Unary_connective
                            | THFUC_th1 TH1_unary_connective
                              deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <th1_unary_connective> ::= !! | ?? | @@+ | @@- | @=
  data TH1_unary_connective = TH1_PiForAll                -- !!
                            | TH1_PiSigmaExists           -- ??
                            | TH1_PiIndefiniteDescription -- @@+
                            | TH1_PiDefiniteDescription   -- @@-
                            | TH1_PiEquality              -- @=
                              deriving (Show, Ord, Eq, Data, Typeable)
  
  
  -- %----Connectives - TFF
  -- % <tff_pair_connective>  ::= <binary_connective> | <assignment>
  -- Note: not used
  -- data TFF_pair_connective = TFFPC_binary Binary_connective
  --                          | TFFPC_assignment TFF_assignment
  --                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----Connectives - FOF
  -- <fof_quantifier>       ::= ! | ?
  data FOF_quantifier = ForAll -- !
                      | Exists -- ?
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <binary_connective>    ::= <=> | => | <= | <~> | ~<vline> | ~&
  data Binary_connective = Equivalence
                         | Implication
                         | ReverseImplication
                         | XOR
                         | NOR
                         | NAND
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <assoc_connective>     ::= <vline> | &
  data Assoc_connective = OR
                        | AND
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <unary_connective>     ::= ~
  data Unary_connective = NOT deriving (Show, Ord, Eq, Data, Typeable)
  
  
  -- %----Types for THF and TFF
  -- <type_constant>        ::= <type_functor>
  type Type_constant = Type_functor
  
  -- <type_functor>         ::= <atomic_word>
  type Type_functor = Token
  
  -- <defined_type>         ::= <atomic_defined_word>
  -- <defined_type>         :== $oType | $o | $iType | $i | $tType |
  --                            $real | $rat | $int
  data Defined_type = OType --  $oType/$o is the Boolean type, i.e., the type of $true and $false.
                    | O     --  $oType/$o is the Boolean type, i.e., the type of $true and $false.
                    | IType --  $iType/$i is non-empty type of individuals, which may be finite or infinite.
                    | I     --  $iType/$i is non-empty type of individuals, which may be finite or infinite.
                    | TType --  $tType is the type (kind) of all types.
                    | Real  --  $real is the type of <real>s.
                    | Rat   --  $rat is the type of <rational>s.
                    | Int   --  $int is the type of <signed_integer>s and <unsigned_integer>s.
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <system_type>          :== <atomic_system_word>
  -- Note: not used
  -- type System_type = Token
  
  -- %----For all language types
  -- <atom>                 ::= <untyped_atom> | <defined_constant>
  data Atom = Atom_untyped Untyped_atom
            | Atom_constant Defined_constant
              deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <untyped_atom>         ::= <constant> | <system_constant>
  data Untyped_atom = UA_constant Constant
                    | UA_system System_constant
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  type Proposition = Predicate
  type Predicate = Token
  
  -- <defined_proposition>  :== <atomic_defined_word>
  -- <defined_proposition>  :== $true | $false
  data Defined_proposition = TPTP_true
                           | TPTP_false
                             deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <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
  -- %----$distinct means that each of it's constant arguments are pairwise !=. It
  -- %----is part of the TFF syntax. It can be used only as a fact, not under any
  -- %----connective.
  data 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
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <defined_infix_pred>   ::= <infix_equality> | <assignment>
  -- <infix_equality>       ::= =
  -- <infix_inequality>     ::= !=
  data Defined_infix_pred = Defined_infix_equality
                          | Defined_assignment
                            deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <constant>             ::= <functor>
  type Constant = TPTP_functor
  
  -- <functor>              ::= <atomic_word>
  type TPTP_functor = Token
  
  -- <system_constant>      ::= <system_functor>
  type System_constant = System_functor
  
  -- <system_functor>       ::= <atomic_system_word>
  type System_functor = Token
  
  -- <defined_constant>     ::= <defined_functor>
  type Defined_constant = Defined_functor
  
  -- <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
  data 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
                       | DF_atomic_defined_word Atomic_defined_word
                         deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <defined_term>         ::= <number> | <distinct_object>
  data Defined_term = DT_number Number
                    | DT_object Distinct_object
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <variable>             ::= <upper_word>
  type Variable = Token
  
  
  -- %----Formula sources
  -- <source>               ::= <general_term>
  -- <source>               :== <dag_source> | <internal_source> |
  --                            <external_source> | unknown | [<sources>]
  data Source = Source_DAG DAG_source
              | Source_internal Internal_source
              | Source_external External_source
              | Unknown_source
              | Source_many Sources
                deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----Alternative sources are recorded like this, thus allowing representation
  -- %----of alternative derivations with shared parts.
  -- <sources>              :== <source> | <source>,<sources>
  type Sources = [Source]
  
  -- %----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>
  data DAG_source = DAGS_name Name
                  | DAGS_record Inference_record
                    deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <inference_record>     :== inference(<inference_rule>,<useful_info>,
  --                            <inference_parents>)
  data Inference_record = Inference_record Inference_rule Useful_info Inference_parents
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <inference_rule>       :== <atomic_word>
  -- %----Examples are          deduction | modus_tollens | modus_ponens | rewrite |
  -- %                          resolution | paramodulation | factorization |
  -- %                          cnf_conversion | cnf_refutation | ...
  type Inference_rule = Token
  
  -- %----<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>]
  type Inference_parents = Parent_list
  
  -- <parent_list>          :== <parent_info> | <parent_info>,<parent_list>
  type Parent_list = [Parent_info]
  
  -- <parent_info>          :== <source><parent_details>
  data Parent_info = Parent_info Source Parent_details
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <parent_details>       :== :<general_list> | <null>
  type Parent_details = Maybe General_list
  
  -- <internal_source>      :== introduced(<intro_type><optional_info>)
  data Internal_source = Internal_source Intro_type Optional_info
                         deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <intro_type>           :== definition | axiom_of_choice | tautology | assumption
  -- %----This should be used to record the symbol being defined, or the function
  -- %----for the axiom of choice
  data Intro_type = IntroTypeDefinition
                  | AxiomOfChoice
                  | Tautology
                  | IntroTypeAssumption
                    deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <external_source>      :== <file_source> | <theory> | <creator_source>
  data External_source = ExtSrc_file File_source
                       | ExtSrc_theory Theory
                       | ExtSrc_creator Creator_source
                         deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <file_source>          :== file(<file_name><file_info>)
  data File_source = File_source File_name File_info
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <file_info>            :== ,<name> | <null>
  type File_info = Maybe Name
  
  -- <theory>               :== theory(<theory_name><optional_info>)
  data Theory = Theory Theory_name Optional_info
                deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <theory_name>          :== equality | ac
  data Theory_name = TN_equality
                   | TN_ac
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----More theory names may be added in the future. The <optional_info> is
  -- %----used to store, e.g., which axioms of equality have been implicitly used,
  -- %----e.g., theory(equality,[rst]). Standard format still to be decided.
  -- <creator_source>       :== creator(<creator_name><optional_info>)
  data Creator_source = Creator_source Creator_name Optional_info
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <creator_name>         :== <atomic_word>
  type Creator_name = Token
  
  
  -- %----Useful info fields
  -- <optional_info>        ::= ,<useful_info> | <null>
  type Optional_info = Maybe Useful_info
  
  -- <useful_info>          ::= <general_list>
  -- <useful_info>          :== [] | [<info_items>]
  data Useful_info = UI_items Info_items
                   | UI_general_list General_list
                     deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <info_items>           :== <info_item> | <info_item>,<info_items>
  type Info_items = [Info_item]
  
  -- <info_item>            :== <formula_item> | <inference_item> |
  --                            <general_function>
  data Info_item = Info_formula Formula_item
                 | Info_inference Inference_item
                 | Info_general General_function
                   deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----Useful info for formula records
  -- <formula_item>         :== <description_item> | <iquote_item>
  data Formula_item = FI_description Description_item
                    | FI_iquote Iquote_item
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <description_item>     :== description(<atomic_word>)
  type Description_item = Token
  
  -- <iquote_item>          :== iquote(<atomic_word>)
  -- %----<iquote_item>s are used for recording exactly what the system output about
  -- %----the inference step. In the future it is planned to encode this information
  -- %----in standardized forms as <parent_details> in each <inference_record>.
  -- %----Useful info for inference records
  type Iquote_item = Token
  
  -- <inference_item>       :== <inference_status> | <assumptions_record> |
  --                            <new_symbol_record> | <refutation>
  data Inference_item = Inf_status Inference_status
                      | Inf_assumption Assumptions_record
                      | Inf_symbol New_symbol_record
                      | Inf_refutation Refutation
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <inference_status>     :== status(<status_value>) | <inference_info>
  data Inference_status = Inf_value Status_value
                        | Inf_info Inference_info
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----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
  data 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
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----<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>)
  data Inference_info = Inference_info Inference_rule Atomic_word General_list
                        deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----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>])
  type Assumptions_record = Name_list
  
  -- %----A <refutation> record names a file in which the inference recorded here
  -- %----is recorded as a proof by refutation.
  -- <refutation>           :== refutation(<file_source>)
  type Refutation = File_source
  
  -- %----A <new_symbol_record> provides information about a newly introduced symbol.
  -- <new_symbol_record>    :== new_symbols(<atomic_word>,[<new_symbol_list>])
  data New_symbol_record = New_symbol_record Atomic_word  New_symbol_list
                           deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <new_symbol_list>      :== <principal_symbol> |
  --                            <principal_symbol>,<new_symbol_list>
  type New_symbol_list = [Principal_symbol]
  
  -- %----Principal symbols are predicates, functions, variables
  -- <principal_symbol>   :== <functor> | <variable>
  data Principal_symbol = PS_functor TPTP_functor
                        | PS_variable Variable
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- %----Include directives
  -- <include>              ::= include(<file_name><formula_selection>).
  data Include = Include File_name Formula_selection
                 deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <formula_selection>    ::= ,[<name_list>] | <null>
  type Formula_selection = Maybe [Name]
  
  -- <name_list>            ::= <name> | <name>,<name_list>
  type Name_list = [Name]
  
  
  -- %----Non-logical data
  -- <general_term>         ::= <general_data> | <general_data>:<general_term> |
  --                            <general_list>
  data General_term = GT_data General_data
                    | GT_DataTerm General_data General_term
                    | GT_list General_list
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <general_data>         ::= <atomic_word> | <general_function> |
  --                            <variable> | <number> | <distinct_object> |
  --                            <formula_data>
  data General_data = GD_atomic_word Atomic_word
                    | GD_general_function General_function
                    | GD_variable Variable
                    | GD_number Number
                    | GD_distinct_object Distinct_object
                    | GD_formula_data Formula_data
  -- %----A <general_data> bind() term is used to record a variable binding in an
  -- %----inference, as an element of the <parent_details> list.
  -- <general_data>         :== bind(<variable>,<formula_data>)
                    | GD_bind Variable Formula_data -- only used in inference
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <general_function>     ::= <atomic_word>(<general_terms>)
  data General_function = General_function Atomic_word General_terms
                          deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <formula_data>         ::= $thf(<thf_formula>) | $tff(<tff_formula>) |
  --                            $fof(<fof_formula>) | $cnf(<cnf_formula>) |
  --                            $fot(<fof_term>)
  -- only used in inference
  data Formula_data = FD_THF THF_formula
                    | FD_TFF TFF_formula
                    | FD_FOF FOF_formula
                    | FD_CNF CNF_formula
                    | FD_FOT FOF_term
                      deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <general_list>         ::= [] | [<general_terms>]
  type General_list = [General_term]
  
  -- <general_terms>        ::= <general_term> | <general_term>,<general_terms>
  type General_terms = [General_term]
  
  
  -- %----General purpose
  -- <name>                 ::= <atomic_word> | <integer>
  -- %----Integer names are expected to be unsigned
  data Name = NameString Token
            | NameInteger Integer
              deriving (Show, Ord, Eq, Data, Typeable)
  
  -- <atomic_word>          ::= <lower_word> | <single_quoted>
  type Atomic_word = Token
  
  -- <atomic_defined_word>  ::= <dollar_word>
  type Atomic_defined_word = Token
  
  -- <atomic_system_word>   ::= <dollar_dollar_word>
  type Atomic_system_word = Token
  
  -- <number>               ::= <integer> | <rational> | <real>
  data Number = NumInteger Integer
              | NumRational Rational
              | NumReal Double
                deriving (Show, Ord, Eq, Data, Typeable)
  
  
  -- <distinct_object>      ::- <double_quote><do_char>*<double_quote>
  type Distinct_object = Token
  
  -- <file_name>            ::= <single_quoted>
  type File_name = IRI
  
  
  set_formula_role :: Annotated_formula -> Formula_role -> Annotated_formula
  set_formula_role (AF_THF_Annotated (THF_annotated n _ f an)) role =
       (AF_THF_Annotated (THF_annotated n role f an))
  set_formula_role (AF_TFX_Annotated (TFX_annotated n _ f an)) role =
       (AF_TFX_Annotated (TFX_annotated n role f an))
  set_formula_role (AF_TFF_Annotated (TFF_annotated n _ f an)) role =
       (AF_TFF_Annotated (TFF_annotated n role f an))
  set_formula_role (AF_TCF_Annotated (TCF_annotated n _ f an)) role =
       (AF_TCF_Annotated (TCF_annotated n role f an))
  set_formula_role (AF_FOF_Annotated (FOF_annotated n _ f an)) role =
       (AF_FOF_Annotated (FOF_annotated n role f an))
  set_formula_role (AF_CNF_Annotated (CNF_annotated n _ f an)) role =
       (AF_CNF_Annotated (CNF_annotated n role f an))
  set_formula_role (AF_TPI_Annotated (TPI_annotated n _ f an)) role =
       (AF_TPI_Annotated (TPI_annotated n role f an))
  
  adjust_formula_role :: AS_Anno.Named Annotated_formula -> AS_Anno.Named Annotated_formula
  adjust_formula_role anno_sen = 
    let sen1 = AS_Anno.sentence anno_sen
        sen2 = if AS_Anno.isAxiom anno_sen
               then set_formula_role sen1 Axiom
               else sen1
    in anno_sen { AS_Anno.sentence = sen2 }                
  
  