AS.der.hs

{-# 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 }