open TPTP_Syntax

exception UNRECOGNISED_SYMBOL of string * string

exception UNRECOGNISED_ROLE of string
fun classify_role role =
  case role of
    "axiom" => Role_Axiom
  | "hypothesis" => Role_Hypothesis
  | "definition" => Role_Definition
  | "assumption" => Role_Assumption
  | "lemma" => Role_Lemma
  | "theorem" => Role_Theorem
  | "conjecture" => Role_Conjecture
  | "negated_conjecture" => Role_Negated_Conjecture
  | "plain" => Role_Plain
  | "fi_domain" => Role_Fi_Domain
  | "fi_functors" => Role_Fi_Functors
  | "fi_predicates" => Role_Fi_Predicates
  | "type" => Role_Type
  | "unknown" => Role_Unknown
  | thing => raise (UNRECOGNISED_ROLE thing)

fun extract_quant_info (Quant (quantifier, vars, tptp_formula)) =
  (quantifier, vars, tptp_formula)

%%
%name TPTP
%term AMPERSAND | AT_SIGN | CARET | COLON | COMMA | EQUALS | EXCLAMATION
  | LET | ARROW | FI | IFF | IMPLIES | INCLUDE
  | LAMBDA | LBRKT | LPAREN | MAP_TO | MMINUS | NAND
  | NEQUALS | XOR | NOR | PERIOD | PPLUS | QUESTION | RBRKT | RPAREN
  | TILDE | TOK_FALSE | TOK_I | TOK_O | TOK_INT | TOK_REAL | TOK_RAT | TOK_TRUE
  | TOK_TYPE | VLINE | EOF | DTHF | DFOF | DCNF | DFOT | DTFF | REAL of string
  | RATIONAL of string | SIGNED_INTEGER of string | UNSIGNED_INTEGER of string
  | DOT_DECIMAL of string | SINGLE_QUOTED of string | UPPER_WORD of string
  | LOWER_WORD of string | COMMENT of string
  | DISTINCT_OBJECT of string
  | DUD | INDEF_CHOICE | DEFIN_CHOICE
  | OPERATOR_FORALL | OPERATOR_EXISTS
  | PLUS | TIMES | GENTZEN_ARROW | DEP_SUM | DEP_PROD
  | DOLLAR_WORD of string | DOLLAR_DOLLAR_WORD of string
  | SUBTYPE | LET_TERM
  | THF | TFF | FOF | CNF
  | ITE_F | ITE_T
  | LET_TF | LET_FF | LET_FT | LET_TT

%nonterm
    annotations of annotation option
  | name of string
  | name_list of string list
  | formula_selection of string list
  | optional_info of general_term list
  | general_list of general_list | general_terms of general_term list
  | general_term of general_term

  | atomic_word of string
  | general_data of general_data | variable_ of string
  | number of number_kind * string | formula_data of general_data
  | integer of string
  | identifier of string
  | general_function of general_data | useful_info of general_list
  | file_name of string
  | functor_ of symbol
  | term of tptp_term
  | arguments of tptp_term list
  | defined_functor of symbol
  | system_functor of symbol
  | system_constant of symbol
  | system_term of symbol * tptp_term list
  | defined_constant of symbol
  | defined_plain_term of symbol * tptp_term list
  | defined_atomic_term of tptp_term
  | defined_atom of tptp_term
  | defined_term of tptp_term
  | constant of symbol
  | plain_term of symbol * tptp_term list
  | function_term of tptp_term
  | conditional_term of tptp_term
  | system_atomic_formula of tptp_formula
  | infix_equality of symbol
  | infix_inequality of symbol
  | defined_infix_pred of symbol
  | defined_infix_formula of tptp_formula
  | defined_prop of string
  | defined_pred of string
  | defined_plain_formula of tptp_formula
  | defined_atomic_formula of tptp_formula
  | plain_atomic_formula of tptp_formula
  | atomic_formula of tptp_formula
  | unary_connective of symbol

  | defined_type of tptp_base_type
  | system_type of string
  | assoc_connective of symbol
  | binary_connective of symbol
  | fol_quantifier of quantifier
  | thf_unary_connective of symbol
  | thf_pair_connective of symbol
  | thf_quantifier of quantifier
  | fol_infix_unary of tptp_formula
  | thf_conn_term of symbol
  | literal of tptp_formula
  | disjunction of tptp_formula
  | cnf_formula of tptp_formula
  | fof_tuple_list of tptp_formula list
  | fof_tuple of tptp_formula list
  | fof_sequent of tptp_formula
  | fof_unary_formula of tptp_formula
  | fof_variable_list of string list
  | fof_quantified_formula of tptp_formula
  | fof_unitary_formula of tptp_formula
  | fof_and_formula of tptp_formula
  | fof_or_formula of tptp_formula
  | fof_binary_assoc of tptp_formula
  | fof_binary_nonassoc of tptp_formula
  | fof_binary_formula of tptp_formula
  | fof_logic_formula of tptp_formula
  | fof_formula of tptp_formula
  | tff_tuple of tptp_formula list
  | tff_tuple_list of tptp_formula list
  | tff_sequent of tptp_formula
  | tff_conditional of tptp_formula
  | tff_xprod_type of tptp_type
  | tff_mapping_type of tptp_type
  | tff_atomic_type of tptp_type
  | tff_unitary_type of tptp_type
  | tff_top_level_type of tptp_type
  | tff_untyped_atom of symbol * tptp_type option
  | tff_typed_atom of symbol * tptp_type option
  | tff_unary_formula of tptp_formula
  | tff_typed_variable of string * tptp_type option
  | tff_variable of string * tptp_type option
  | tff_variable_list of (string * tptp_type option) list
  | tff_quantified_formula of tptp_formula
  | tff_unitary_formula of tptp_formula
  | tff_and_formula of tptp_formula
  | tff_or_formula of tptp_formula
  | tff_binary_assoc of tptp_formula
  | tff_binary_nonassoc of tptp_formula
  | tff_binary_formula of tptp_formula
  | tff_logic_formula of tptp_formula
  | tff_formula of tptp_formula

  | thf_tuple of tptp_formula list
  | thf_tuple_list of tptp_formula list
  | thf_sequent of tptp_formula
  | thf_conditional of tptp_formula
  | thf_let of tptp_formula
  | thf_atom of tptp_formula
  | thf_union_type of tptp_type
  | thf_xprod_type of tptp_type
  | thf_mapping_type of tptp_type
  | thf_binary_type of tptp_type
  | thf_unitary_type of tptp_type
  | thf_top_level_type of tptp_type
  | thf_subtype of tptp_type
  | thf_typeable_formula of tptp_formula
  | thf_type_formula of tptp_formula * tptp_type
  | thf_unary_formula of tptp_formula
  | thf_typed_variable of string * tptp_type option
  | thf_variable of string * tptp_type option
  | thf_variable_list of (string * tptp_type option) list
  | thf_quantified_formula of tptp_formula
  | thf_unitary_formula of tptp_formula
  | thf_apply_formula of tptp_formula
  | thf_and_formula of tptp_formula
  | thf_or_formula of tptp_formula
  | thf_binary_tuple of tptp_formula
  | thf_binary_pair of tptp_formula
  | thf_binary_formula of tptp_formula
  | thf_logic_formula of tptp_formula
  | thf_formula of tptp_formula
  | formula_role of role

  | cnf_annotated of tptp_line
  | fof_annotated of tptp_line
  | tff_annotated of tptp_line
  | thf_annotated of tptp_line
  | annotated_formula of tptp_line
  | include_ of tptp_line
  | tptp_input of tptp_line
  | tptp_file of tptp_problem
  | tptp of tptp_problem

  | thf_let_term_defn of tptp_let
  | thf_let_formula_defn of tptp_let
  | tff_let of tptp_formula
  | tff_let_term_defn of tptp_let
  | tff_let_term_binding of tptp_term
  | tff_let_formula_defn of tptp_let
  | tff_let_formula_binding of tptp_formula
  | tff_quantified_type of tptp_type
  | tff_monotype of tptp_type
  | tff_type_arguments of tptp_type list
  | let_term of tptp_term
  | atomic_defined_word of string
  | atomic_system_word of string

%pos int
%eop EOF
%noshift EOF
%arg (this_file_name) : string

%nonassoc LET
%nonassoc RPAREN
%nonassoc DUD
%right COMMA
%left COLON

%left AT_SIGN
%nonassoc IFF XOR
%right IMPLIES FI
%nonassoc EQUALS NEQUALS
%right VLINE NOR
%left AMPERSAND NAND
%right ARROW
%left PLUS
%left TIMES

%right OPERATOR_FORALL OPERATOR_EXISTS

%nonassoc EXCLAMATION QUESTION LAMBDA CARET
%nonassoc TILDE
%pure
%start tptp
%verbose
%%

(*  Title:      HOL/TPTP/TPTP_Parser/tptp.yacc
    Author:     Nik Sultana, Cambridge University Computer Laboratory

 Parser for TPTP languages. Latest version of the language spec can
 be obtained from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html
 Our parser implements version 5.5.0 of that spec, except for the TPI
 language since its (parser) spec is still incomplete.
*)

tptp : tptp_file (( tptp_file ))

tptp_file : tptp_input tptp_file (( tptp_input :: tptp_file ))
          | COMMENT tptp_file    (( tptp_file ))
          |                      (( [] ))

tptp_input : annotated_formula (( annotated_formula ))
           | include_           (( include_ ))

annotated_formula : thf_annotated (( thf_annotated ))
                  | tff_annotated (( tff_annotated ))
                  | fof_annotated (( fof_annotated ))
                  | cnf_annotated (( cnf_annotated ))

thf_annotated : THF LPAREN name COMMA formula_role COMMA thf_formula annotations RPAREN PERIOD ((
  Annotated_Formula ((this_file_name, THFleft + 1, THFright + 1),
   THF, name, formula_role, thf_formula, annotations)
))

tff_annotated : TFF LPAREN name COMMA formula_role COMMA tff_formula annotations RPAREN PERIOD ((
  Annotated_Formula ((this_file_name, TFFleft + 1, TFFright + 1),
   TFF, name, formula_role, tff_formula, annotations)
))

fof_annotated : FOF LPAREN name COMMA formula_role COMMA fof_formula annotations RPAREN PERIOD ((
  Annotated_Formula ((this_file_name, FOFleft + 1, FOFright + 1),
   FOF, name, formula_role, fof_formula, annotations)
))

cnf_annotated : CNF LPAREN name COMMA formula_role COMMA cnf_formula annotations RPAREN PERIOD ((
  Annotated_Formula ((this_file_name, CNFleft + 1, CNFright + 1),
   CNF, name, formula_role, cnf_formula, annotations)
))

annotations : COMMA general_term optional_info (( SOME (general_term, optional_info) ))
            |                                  (( NONE ))

formula_role : LOWER_WORD (( classify_role LOWER_WORD ))


(* THF formulas *)

thf_formula : thf_logic_formula (( thf_logic_formula ))
            | thf_sequent       (( thf_sequent ))

thf_logic_formula : thf_binary_formula   (( thf_binary_formula ))
                  | thf_unitary_formula  (( thf_unitary_formula ))
                  | thf_type_formula     (( THF_typing thf_type_formula ))
                  | thf_subtype          (( Type_fmla thf_subtype ))

thf_binary_formula : thf_binary_pair   (( thf_binary_pair ))
                   | thf_binary_tuple  (( thf_binary_tuple ))
                   | thf_binary_type   (( Type_fmla thf_binary_type ))

thf_binary_pair : thf_unitary_formula thf_pair_connective thf_unitary_formula ((
  Fmla (thf_pair_connective, [thf_unitary_formula1, thf_unitary_formula2])
))

thf_binary_tuple : thf_or_formula    (( thf_or_formula ))
                 | thf_and_formula   (( thf_and_formula ))
                 | thf_apply_formula (( thf_apply_formula ))

thf_or_formula : thf_unitary_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_unitary_formula1, thf_unitary_formula2]) ))
               | thf_or_formula VLINE thf_unitary_formula      (( Fmla (Interpreted_Logic Or, [thf_or_formula, thf_unitary_formula]) ))

thf_and_formula : thf_unitary_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_unitary_formula1, thf_unitary_formula2]) ))
                | thf_and_formula AMPERSAND thf_unitary_formula     (( Fmla (Interpreted_Logic And, [thf_and_formula, thf_unitary_formula]) ))

thf_apply_formula : thf_unitary_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_unitary_formula1, thf_unitary_formula2]) ))
                  | thf_apply_formula AT_SIGN thf_unitary_formula   (( Fmla (Interpreted_ExtraLogic Apply, [thf_apply_formula, thf_unitary_formula]) ))

thf_unitary_formula : thf_quantified_formula (( thf_quantified_formula ))
                    | thf_unary_formula      (( thf_unary_formula ))
                    | thf_atom               (( thf_atom ))
                    | thf_conditional        (( thf_conditional ))
                    | thf_let                (( thf_let ))
                    | LPAREN thf_logic_formula RPAREN  (( thf_logic_formula ))

thf_quantified_formula : thf_quantifier LBRKT thf_variable_list RBRKT COLON thf_unitary_formula ((
  Quant (thf_quantifier, thf_variable_list, thf_unitary_formula)
))

thf_variable_list : thf_variable                          (( [thf_variable] ))
                  | thf_variable COMMA thf_variable_list  (( thf_variable :: thf_variable_list ))

thf_variable : thf_typed_variable (( thf_typed_variable ))
             | variable_          (( (variable_, NONE) ))

thf_typed_variable : variable_ COLON thf_top_level_type (( (variable_, SOME thf_top_level_type) ))

thf_unary_formula : thf_unary_connective LPAREN thf_logic_formula RPAREN ((
  Fmla (thf_unary_connective, [thf_logic_formula])
))

thf_atom : term          (( Atom (THF_Atom_term term) ))
         | thf_conn_term (( Atom (THF_Atom_conn_term thf_conn_term) ))

thf_conditional : ITE_F LPAREN thf_logic_formula COMMA thf_logic_formula COMMA thf_logic_formula RPAREN ((
  Conditional (thf_logic_formula1, thf_logic_formula2, thf_logic_formula3)
))

(*NOTE support for Let in THF is still broken (cf. the spec).
  When it gets fixed, look at how TFF support is encoded in this file
  (to possibly replicate some of the checks done there)*)
thf_let : LET_TF LPAREN thf_let_term_defn COMMA thf_formula RPAREN (( Let (thf_let_term_defn, thf_formula) ))
        | LET_FF LPAREN thf_let_formula_defn COMMA thf_formula RPAREN (( Let (thf_let_formula_defn, thf_formula) ))

(*FIXME here could check that fmla is of right form (TPTP BNF (v5.3.0) L130-134)
  i.e. it should have "=" or "<=>" at the top level.
  We deviate from the spec by not checking this here, but "Let" support in THF
  is still not fully specified.
*)
thf_let_term_defn : thf_quantified_formula ((
  let
    val (_, vars, fmla) = extract_quant_info thf_quantified_formula
  in Let_fmla (vars, fmla)
  end
))
(*NOTE "thf_let_formula_defn" has the same definition as "thf_let_term_defn" (as per the spec)*)
thf_let_formula_defn : thf_quantified_formula ((
  let
    val (_, vars, fmla) = extract_quant_info thf_quantified_formula
  in Let_fmla (vars, fmla)
  end
))

thf_type_formula : thf_typeable_formula COLON thf_top_level_type (( (thf_typeable_formula, thf_top_level_type) ))

thf_typeable_formula : thf_atom                         (( thf_atom ))
                     | LPAREN thf_logic_formula RPAREN  (( thf_logic_formula ))

thf_subtype : constant SUBTYPE constant (( Subtype(constant1, constant2) ))

thf_top_level_type : thf_logic_formula (( Fmla_type thf_logic_formula ))

thf_unitary_type : thf_unitary_formula (( Fmla_type thf_unitary_formula ))

thf_binary_type : thf_mapping_type (( thf_mapping_type ))
                | thf_xprod_type   (( thf_xprod_type ))
                | thf_union_type   (( thf_union_type ))

thf_mapping_type : thf_unitary_type ARROW thf_unitary_type (( Fn_type(thf_unitary_type1, thf_unitary_type2) ))
                 | thf_unitary_type ARROW thf_mapping_type (( Fn_type(thf_unitary_type, thf_mapping_type) ))

thf_xprod_type : thf_unitary_type TIMES thf_unitary_type   (( Prod_type(thf_unitary_type1, thf_unitary_type2) ))
               | thf_xprod_type TIMES thf_unitary_type     (( Prod_type(thf_xprod_type, thf_unitary_type) ))

thf_union_type : thf_unitary_type PLUS thf_unitary_type    (( Sum_type(thf_unitary_type1, thf_unitary_type2) ))
               | thf_union_type PLUS thf_unitary_type      (( Sum_type(thf_union_type, thf_unitary_type) ))

thf_sequent : thf_tuple GENTZEN_ARROW thf_tuple  (( Sequent(thf_tuple1, thf_tuple2) ))
            | LPAREN thf_sequent RPAREN          (( thf_sequent ))

thf_tuple : LBRKT RBRKT                (( [] ))
          | LBRKT thf_tuple_list RBRKT (( thf_tuple_list ))

thf_tuple_list : thf_logic_formula                      (( [thf_logic_formula] ))
               | thf_logic_formula COMMA thf_tuple_list (( thf_logic_formula :: thf_tuple_list ))


(* TFF Formulas *)

tff_formula : tff_logic_formula  (( tff_logic_formula ))
            | tff_typed_atom     (( Atom (TFF_Typed_Atom tff_typed_atom) ))
            | tff_sequent        (( tff_sequent ))

tff_logic_formula : tff_binary_formula   (( tff_binary_formula ))
                  | tff_unitary_formula  (( tff_unitary_formula ))

tff_binary_formula : tff_binary_nonassoc (( tff_binary_nonassoc ))
                   | tff_binary_assoc    (( tff_binary_assoc ))

tff_binary_nonassoc : tff_unitary_formula binary_connective tff_unitary_formula (( Fmla (binary_connective, [tff_unitary_formula1, tff_unitary_formula2]) ))

tff_binary_assoc : tff_or_formula  (( tff_or_formula ))
                 | tff_and_formula (( tff_and_formula ))

tff_or_formula : tff_unitary_formula VLINE tff_unitary_formula      (( Fmla (Interpreted_Logic Or, [tff_unitary_formula1, tff_unitary_formula2]) ))
               | tff_or_formula VLINE tff_unitary_formula           (( Fmla (Interpreted_Logic Or, [tff_or_formula, tff_unitary_formula]) ))

tff_and_formula : tff_unitary_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_unitary_formula1, tff_unitary_formula2]) ))
                | tff_and_formula AMPERSAND tff_unitary_formula     (( Fmla (Interpreted_Logic And, [tff_and_formula, tff_unitary_formula]) ))

tff_unitary_formula : tff_quantified_formula           (( tff_quantified_formula ))
                    | tff_unary_formula                (( tff_unary_formula ))
                    | atomic_formula                   (( atomic_formula ))
                    | tff_conditional                  (( tff_conditional ))
                    | tff_let                          (( tff_let ))
                    | LPAREN tff_logic_formula RPAREN  (( tff_logic_formula ))

tff_quantified_formula : fol_quantifier LBRKT tff_variable_list RBRKT COLON tff_unitary_formula ((
  Quant (fol_quantifier, tff_variable_list, tff_unitary_formula)
))

tff_variable_list : tff_variable                         (( [tff_variable] ))
                  | tff_variable COMMA tff_variable_list (( tff_variable :: tff_variable_list ))

tff_variable : tff_typed_variable (( tff_typed_variable ))
             | variable_          (( (variable_, NONE) ))

tff_typed_variable : variable_ COLON tff_atomic_type (( (variable_, SOME tff_atomic_type) ))

tff_unary_formula : unary_connective tff_unitary_formula (( Fmla (unary_connective, [tff_unitary_formula]) ))
                  | fol_infix_unary                      (( fol_infix_unary ))

tff_conditional : ITE_F LPAREN tff_logic_formula COMMA tff_logic_formula COMMA tff_logic_formula RPAREN ((
  Conditional (tff_logic_formula1, tff_logic_formula2, tff_logic_formula3)
))

tff_let : LET_TF LPAREN tff_let_term_defn COMMA tff_formula RPAREN ((Let (tff_let_term_defn, tff_formula) ))
        | LET_FF LPAREN tff_let_formula_defn COMMA tff_formula RPAREN (( Let (tff_let_formula_defn, tff_formula) ))


tff_let_term_defn : EXCLAMATION LBRKT tff_variable_list RBRKT COLON tff_let_term_binding (( Let_term (tff_variable_list, tff_let_term_binding) ))
                  | tff_let_term_binding (( Let_term ([], tff_let_term_binding) ))

tff_let_term_binding : term EQUALS term (( Term_Func (Interpreted_ExtraLogic Apply, [term1, term2]) ))
                     | LPAREN tff_let_term_binding RPAREN (( tff_let_term_binding ))

tff_let_formula_defn : EXCLAMATION LBRKT tff_variable_list RBRKT COLON tff_let_formula_binding (( Let_fmla (tff_variable_list, tff_let_formula_binding) ))
                  | tff_let_formula_binding (( Let_fmla ([], tff_let_formula_binding) ))

tff_let_formula_binding : atomic_formula IFF tff_unitary_formula (( Fmla (Interpreted_Logic Iff, [atomic_formula, tff_unitary_formula]) ))
                        | LPAREN tff_let_formula_binding RPAREN (( tff_let_formula_binding ))

tff_sequent : tff_tuple GENTZEN_ARROW tff_tuple (( Sequent (tff_tuple1, tff_tuple2) ))
            | LPAREN tff_sequent RPAREN         (( tff_sequent ))

tff_tuple : LBRKT RBRKT    (( [] ))
          | LBRKT tff_tuple_list RBRKT (( tff_tuple_list ))

tff_tuple_list : tff_logic_formula COMMA tff_tuple_list (( tff_logic_formula :: tff_tuple_list ))
               | tff_logic_formula                      (( [tff_logic_formula] ))

tff_typed_atom : tff_untyped_atom COLON tff_top_level_type (( (fst tff_untyped_atom, SOME tff_top_level_type) ))
               | LPAREN tff_typed_atom RPAREN              (( tff_typed_atom ))

tff_untyped_atom : functor_       (( (functor_, NONE) ))
                 | system_functor (( (system_functor, NONE) ))

tff_top_level_type : tff_atomic_type     (( tff_atomic_type ))
                   | tff_mapping_type    (( tff_mapping_type ))
                   | tff_quantified_type (( tff_quantified_type ))
                   | LPAREN tff_top_level_type RPAREN (( tff_top_level_type ))

tff_quantified_type : DEP_PROD LBRKT tff_variable_list RBRKT COLON tff_monotype ((
       Fmla_type (Quant (Dep_Prod, tff_variable_list, Type_fmla tff_monotype))
))

tff_monotype : tff_atomic_type                (( tff_atomic_type ))
             | LPAREN tff_mapping_type RPAREN (( tff_mapping_type ))

tff_unitary_type : tff_atomic_type               (( tff_atomic_type ))
                 | LPAREN tff_xprod_type RPAREN  (( tff_xprod_type ))

tff_atomic_type : atomic_word   (( Atom_type (atomic_word, []) ))
                | defined_type  (( Defined_type defined_type ))
                | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map Type_fmla tff_type_arguments))) ))
                | variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) ))

tff_type_arguments : tff_atomic_type   (( [tff_atomic_type]  ))
                   | tff_atomic_type COMMA tff_type_arguments (( tff_atomic_type :: tff_type_arguments ))

tff_mapping_type : tff_unitary_type ARROW tff_atomic_type (( Fn_type(tff_unitary_type, tff_atomic_type) ))

tff_xprod_type : tff_atomic_type TIMES tff_atomic_type (( Prod_type(tff_atomic_type1, tff_atomic_type2) ))
               | tff_xprod_type TIMES tff_atomic_type  (( Prod_type(tff_xprod_type, tff_atomic_type) ))


(* FOF Formulas *)

fof_formula : fof_logic_formula  (( fof_logic_formula ))
            | fof_sequent        (( fof_sequent ))

fof_logic_formula : fof_binary_formula   (( fof_binary_formula ))
                  | fof_unitary_formula  (( fof_unitary_formula ))

fof_binary_formula : fof_binary_nonassoc (( fof_binary_nonassoc ))
                   | fof_binary_assoc    (( fof_binary_assoc ))

fof_binary_nonassoc : fof_unitary_formula binary_connective fof_unitary_formula ((
  Fmla (binary_connective, [fof_unitary_formula1, fof_unitary_formula2] )
))

fof_binary_assoc : fof_or_formula  (( fof_or_formula ))
                 | fof_and_formula (( fof_and_formula ))

fof_or_formula : fof_unitary_formula VLINE fof_unitary_formula  (( Fmla (Interpreted_Logic Or, [fof_unitary_formula1, fof_unitary_formula2]) ))
               | fof_or_formula VLINE fof_unitary_formula       (( Fmla (Interpreted_Logic Or, [fof_or_formula, fof_unitary_formula]) ))

fof_and_formula : fof_unitary_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_unitary_formula1, fof_unitary_formula2]) ))
                | fof_and_formula AMPERSAND fof_unitary_formula     (( Fmla (Interpreted_Logic And, [fof_and_formula, fof_unitary_formula]) ))

fof_unitary_formula : fof_quantified_formula (( fof_quantified_formula ))
                    | fof_unary_formula      (( fof_unary_formula ))
                    | atomic_formula         (( atomic_formula ))
                    | LPAREN fof_logic_formula RPAREN (( fof_logic_formula ))

fof_quantified_formula : fol_quantifier LBRKT fof_variable_list RBRKT COLON fof_unitary_formula ((
  Quant (fol_quantifier, map (fn v => (v, NONE)) fof_variable_list, fof_unitary_formula)
))

fof_variable_list : variable_                          (( [variable_] ))
                  | variable_ COMMA fof_variable_list  (( variable_ :: fof_variable_list ))

fof_unary_formula : unary_connective fof_unitary_formula (( Fmla (unary_connective, [fof_unitary_formula]) ))
                  | fol_infix_unary                      (( fol_infix_unary ))

fof_sequent : fof_tuple GENTZEN_ARROW fof_tuple (( Sequent (fof_tuple1, fof_tuple2) ))
            | LPAREN fof_sequent RPAREN         (( fof_sequent ))

fof_tuple : LBRKT RBRKT                 (( [] ))
          | LBRKT fof_tuple_list RBRKT  (( fof_tuple_list ))

fof_tuple_list : fof_logic_formula                      (( [fof_logic_formula] ))
               | fof_logic_formula COMMA fof_tuple_list (( fof_logic_formula :: fof_tuple_list ))


(* CNF Formulas *)

cnf_formula : LPAREN disjunction RPAREN  (( disjunction ))
            | disjunction                (( disjunction ))

disjunction : literal                    (( literal ))
            | disjunction VLINE literal  (( Fmla (Interpreted_Logic Or, [disjunction, literal]) ))

literal : atomic_formula        (( atomic_formula ))
        | TILDE atomic_formula  (( Fmla (Interpreted_Logic Not, [atomic_formula]) ))
        | fol_infix_unary       (( fol_infix_unary ))


(* Special Formulas  *)

thf_conn_term : thf_pair_connective   (( thf_pair_connective ))
              | assoc_connective      (( assoc_connective ))
              | thf_unary_connective  (( thf_unary_connective ))

fol_infix_unary : term infix_inequality term (( Pred (infix_inequality, [term1, term2]) ))


(* Connectives - THF *)

thf_quantifier : fol_quantifier (( fol_quantifier ))
               | CARET          (( Lambda ))
               | DEP_PROD       (( Dep_Prod ))
               | DEP_SUM        (( Dep_Sum ))
               | INDEF_CHOICE   (( Epsilon ))
               | DEFIN_CHOICE   (( Iota ))

thf_pair_connective : infix_equality    (( infix_equality ))
                    | infix_inequality  (( infix_inequality ))
                    | binary_connective (( binary_connective ))

thf_unary_connective : unary_connective (( unary_connective ))
                     | OPERATOR_FORALL  (( Interpreted_Logic Op_Forall ))
                     | OPERATOR_EXISTS  (( Interpreted_Logic Op_Exists ))


(* Connectives - THF and TFF
instead of subtype_sign use token SUBTYPE
*)


(* Connectives - FOF *)

fol_quantifier : EXCLAMATION  (( Forall ))
               | QUESTION     (( Exists ))

binary_connective : IFF       (( Interpreted_Logic Iff ))
                  | IMPLIES   (( Interpreted_Logic If ))
                  | FI        (( Interpreted_Logic Fi ))
                  | XOR       (( Interpreted_Logic Xor ))
                  | NOR       (( Interpreted_Logic Nor ))
                  | NAND      (( Interpreted_Logic Nand ))

assoc_connective : VLINE      (( Interpreted_Logic Or ))
                 | AMPERSAND  (( Interpreted_Logic And ))

unary_connective : TILDE (( Interpreted_Logic Not ))


(* The sequent arrow
use token GENTZEN_ARROW
*)


(* Types for THF and TFF *)

defined_type : atomic_defined_word ((
  case atomic_defined_word of
    "$oType" => Type_Bool
  | "$o" => Type_Bool
  | "$iType" => Type_Ind
  | "$i" => Type_Ind
  | "$tType" => Type_Type
  | "$real" => Type_Real
  | "$rat" => Type_Rat
  | "$int" => Type_Int
  | "$_" => Type_Dummy
  | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
))

system_type : atomic_system_word (( atomic_system_word ))


(* First-order atoms *)

atomic_formula : plain_atomic_formula   (( plain_atomic_formula ))
               | defined_atomic_formula (( defined_atomic_formula ))
               | system_atomic_formula  (( system_atomic_formula ))

plain_atomic_formula : plain_term (( Pred plain_term ))

defined_atomic_formula : defined_plain_formula (( defined_plain_formula ))
                       | defined_infix_formula (( defined_infix_formula ))

defined_plain_formula : defined_plain_term (( Pred defined_plain_term ))

(*FIXME not used*)
defined_prop : atomic_defined_word ((
  case atomic_defined_word of
    "$true"  => "$true"
  | "$false" => "$false"
  | thing => raise UNRECOGNISED_SYMBOL ("defined_prop", thing)
))

(*FIXME not used*)
defined_pred : atomic_defined_word ((
  case atomic_defined_word of
    "$distinct"  => "$distinct"
  | "$ite_f" => "$ite_f"
  | "$less" => "$less"
  | "$lesseq" => "$lesseq"
  | "$greater" => "$greater"
  | "$greatereq" => "$greatereq"
  | "$is_int" => "$is_int"
  | "$is_rat" => "$is_rat"
  | thing => raise UNRECOGNISED_SYMBOL ("defined_pred", thing)
))

defined_infix_formula : term defined_infix_pred term ((Pred (defined_infix_pred, [term1, term2])))

defined_infix_pred : infix_equality  (( infix_equality ))

infix_equality : EQUALS    (( Interpreted_Logic Equals ))

infix_inequality : NEQUALS (( Interpreted_Logic NEquals ))

system_atomic_formula : system_term  (( Pred system_term ))


(* First-order terms *)

term : function_term     (( function_term ))
     | variable_         (( Term_Var variable_ ))
     | conditional_term  (( conditional_term ))
     | let_term          (( let_term ))

function_term : plain_term    (( Term_Func plain_term ))
              | defined_term  (( defined_term ))
              | system_term   (( Term_Func system_term ))

plain_term : constant                          (( (constant, []) ))
           | functor_ LPAREN arguments RPAREN  (( (functor_, arguments) ))

constant : functor_ (( functor_ ))

functor_ : atomic_word (( Uninterpreted atomic_word ))

defined_term : defined_atom        (( defined_atom ))
             | defined_atomic_term (( defined_atomic_term ))

defined_atom : number          (( Term_Num number ))
             | DISTINCT_OBJECT (( Term_Distinct_Object DISTINCT_OBJECT ))

defined_atomic_term : defined_plain_term (( Term_Func defined_plain_term ))

defined_plain_term : defined_constant                        (( (defined_constant, []) ))
                   | defined_functor LPAREN arguments RPAREN (( (defined_functor, arguments) ))

defined_constant : defined_functor (( defined_functor ))

(*FIXME would be nicer to split these up*)
defined_functor : atomic_defined_word ((
  case atomic_defined_word of
    "$uminus" => Interpreted_ExtraLogic UMinus
  | "$sum" => Interpreted_ExtraLogic Sum
  | "$difference" => Interpreted_ExtraLogic Difference
  | "$product" => Interpreted_ExtraLogic Product
  | "$quotient" => Interpreted_ExtraLogic Quotient
  | "$quotient_e" => Interpreted_ExtraLogic Quotient_E
  | "$quotient_t" => Interpreted_ExtraLogic Quotient_T
  | "$quotient_f" => Interpreted_ExtraLogic Quotient_F
  | "$remainder_e" => Interpreted_ExtraLogic Remainder_E
  | "$remainder_t" => Interpreted_ExtraLogic Remainder_T
  | "$remainder_f" => Interpreted_ExtraLogic Remainder_F
  | "$floor" => Interpreted_ExtraLogic Floor
  | "$ceiling" => Interpreted_ExtraLogic Ceiling
  | "$truncate" => Interpreted_ExtraLogic Truncate
  | "$round" => Interpreted_ExtraLogic Round
  | "$to_int" => Interpreted_ExtraLogic To_Int
  | "$to_rat" => Interpreted_ExtraLogic To_Rat
  | "$to_real" => Interpreted_ExtraLogic To_Real

  | "$i" => TypeSymbol Type_Ind
  | "$o" => TypeSymbol Type_Bool
  | "$iType" => TypeSymbol Type_Ind
  | "$oType" => TypeSymbol Type_Bool
  | "$int" => TypeSymbol Type_Int
  | "$real" => TypeSymbol Type_Real
  | "$rat" => TypeSymbol Type_Rat
  | "$tType" => TypeSymbol Type_Type
  | "$_" => TypeSymbol Type_Dummy

  | "$true" => Interpreted_Logic True
  | "$false" => Interpreted_Logic False

  | "$less" => Interpreted_ExtraLogic Less
  | "$lesseq" => Interpreted_ExtraLogic LessEq
  | "$greatereq" => Interpreted_ExtraLogic GreaterEq
  | "$greater" => Interpreted_ExtraLogic Greater
  | "$evaleq" => Interpreted_ExtraLogic EvalEq

  | "$is_int" => Interpreted_ExtraLogic Is_Int
  | "$is_rat" => Interpreted_ExtraLogic Is_Rat

  | "$distinct" => Interpreted_ExtraLogic Distinct

  | thing => raise UNRECOGNISED_SYMBOL ("defined_functor", thing)
))

system_term : system_constant                         (( (system_constant, []) ))
            | system_functor LPAREN arguments RPAREN  (( (system_functor, arguments) ))

system_constant : system_functor (( system_functor ))

system_functor : atomic_system_word (( System atomic_system_word ))

variable_ : UPPER_WORD  (( UPPER_WORD ))

arguments : term                  (( [term] ))
          | term COMMA arguments  (( term :: arguments ))

conditional_term : ITE_T LPAREN tff_logic_formula COMMA term COMMA term RPAREN ((
  Term_Conditional (tff_logic_formula, term1, term2)
))


let_term : LET_FT LPAREN tff_let_formula_defn COMMA term RPAREN ((Term_Let (tff_let_formula_defn, term) ))
         | LET_TT LPAREN tff_let_term_defn COMMA term RPAREN ((Term_Let (tff_let_term_defn, term) ))


(* Formula sources
Don't currently use following non-terminals:
source, sources, dag_source, inference_record, inference_rule, parent_list,
parent_info, parent_details, internal_source, intro_type, external_source,
file_source, file_info, theory, theory_name, creator_source, creator_name.
*)


(* Useful info fields *)

optional_info : COMMA useful_info (( useful_info ))
              |                   (( [] ))

useful_info : general_list (( general_list ))

include_ : INCLUDE LPAREN file_name formula_selection RPAREN PERIOD ((
  Include ((this_file_name, INCLUDEleft + 1, INCLUDEright + 1),
    file_name, formula_selection)
))

formula_selection : COMMA LBRKT name_list RBRKT   (( name_list  ))
                  |                               (( [] ))

name_list : name COMMA name_list   (( name :: name_list ))
          | name                   (( [name] ))


(* Non-logical data *)

general_term : general_data                    (( General_Data general_data ))
             | general_data COLON general_term (( General_Term (general_data, general_term) ))
             | general_list                    (( General_List general_list ))

general_data : atomic_word       (( Atomic_Word atomic_word ))
             | general_function  (( general_function ))
             | variable_         (( V variable_ ))
             | number            (( Number number ))
             | DISTINCT_OBJECT   (( Distinct_Object DISTINCT_OBJECT ))
             | formula_data      (( formula_data ))

general_function: atomic_word LPAREN general_terms RPAREN (( Application (atomic_word, general_terms) ))

formula_data : DTHF LPAREN thf_formula RPAREN (( Formula_Data (THF, thf_formula) ))
             | DTFF LPAREN tff_formula RPAREN (( Formula_Data (TFF, tff_formula) ))
             | DFOF LPAREN fof_formula RPAREN (( Formula_Data (FOF, fof_formula) ))
             | DCNF LPAREN cnf_formula RPAREN (( Formula_Data (CNF, cnf_formula) ))
             | DFOT LPAREN term RPAREN (( Term_Data term ))

general_list : LBRKT general_terms RBRKT (( general_terms ))
             | LBRKT RBRKT               (( [] ))

general_terms : general_term COMMA general_terms (( general_term :: general_terms ))
              | general_term                     (( [general_term] ))


(* General purpose *)

name : atomic_word (( atomic_word ))
     | integer     (( integer ))

atomic_word : LOWER_WORD    (( LOWER_WORD ))
            | SINGLE_QUOTED (( dequote SINGLE_QUOTED ))
            | THF           (( "thf" ))
            | TFF           (( "tff" ))
            | FOF           (( "fof" ))
            | CNF           (( "cnf" ))
            | INCLUDE       (( "include" ))

atomic_defined_word : DOLLAR_WORD (( DOLLAR_WORD ))

atomic_system_word : DOLLAR_DOLLAR_WORD (( DOLLAR_DOLLAR_WORD ))

integer: UNSIGNED_INTEGER (( UNSIGNED_INTEGER ))
       | SIGNED_INTEGER   (( SIGNED_INTEGER ))

number : integer          (( (Int_num, integer) ))
       | REAL             (( (Real_num, REAL) ))
       | RATIONAL         (( (Rat_num, RATIONAL) ))

file_name : SINGLE_QUOTED (( SINGLE_QUOTED ))