1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc Fri Mar 09 15:38:55 2012 +0000
1.3 @@ -0,0 +1,653 @@
1.4 +open TPTP_Syntax
1.5 +
1.6 +exception UNRECOGNISED_SYMBOL of string * string
1.7 +
1.8 +exception UNRECOGNISED_ROLE of string
1.9 +fun classify_role role =
1.10 + case role of
1.11 + "axiom" => Role_Axiom
1.12 + | "hypothesis" => Role_Hypothesis
1.13 + | "definition" => Role_Definition
1.14 + | "assumption" => Role_Assumption
1.15 + | "lemma" => Role_Lemma
1.16 + | "theorem" => Role_Theorem
1.17 + | "conjecture" => Role_Conjecture
1.18 + | "negated_conjecture" => Role_Negated_Conjecture
1.19 + | "plain" => Role_Plain
1.20 + | "fi_domain" => Role_Fi_Domain
1.21 + | "fi_functors" => Role_Fi_Functors
1.22 + | "fi_predicates" => Role_Fi_Predicates
1.23 + | "type" => Role_Type
1.24 + | "unknown" => Role_Unknown
1.25 + | thing => raise (UNRECOGNISED_ROLE thing)
1.26 +
1.27 +%%
1.28 +%name TPTP
1.29 +%term AMPERSAND | AT_SIGN | CARET | COLON | COMMA | EQUALS | EXCLAMATION
1.30 + | LET | ARROW | IF | IFF | IMPLIES | INCLUDE
1.31 + | LAMBDA | LBRKT | LPAREN | MAP_TO | MMINUS | NAND
1.32 + | NEQUALS | XOR | NOR | PERIOD | PPLUS | QUESTION | RBRKT | RPAREN
1.33 + | TILDE | TOK_FALSE | TOK_I | TOK_O | TOK_INT | TOK_REAL | TOK_RAT | TOK_TRUE
1.34 + | TOK_TYPE | VLINE | EOF | DTHF | DFOF | DCNF | DFOT | DTFF | REAL of string
1.35 + | RATIONAL of string | SIGNED_INTEGER of string | UNSIGNED_INTEGER of string
1.36 + | DOT_DECIMAL of string | SINGLE_QUOTED of string | UPPER_WORD of string
1.37 + | LOWER_WORD of string | COMMENT of string
1.38 + | DISTINCT_OBJECT of string
1.39 + | DUD | INDEF_CHOICE | DEFIN_CHOICE
1.40 + | OPERATOR_FORALL | OPERATOR_EXISTS
1.41 + | PLUS | TIMES | GENTZEN_ARROW | DEP_SUM | DEP_PROD
1.42 + | ATOMIC_DEFINED_WORD of string | ATOMIC_SYSTEM_WORD of string
1.43 + | SUBTYPE | LET_TERM
1.44 + | THF | TFF | FOF | CNF
1.45 + | ITE_F | ITE_T
1.46 +%nonterm
1.47 + annotations of annotation option
1.48 + | name of string
1.49 + | name_list of string list
1.50 + | formula_selection of string list
1.51 + | optional_info of general_term list
1.52 + | general_list of general_list | general_terms of general_term list
1.53 + | general_term of general_term
1.54 +
1.55 + | atomic_word of string
1.56 + | general_data of general_data | variable_ of string
1.57 + | number of number_kind * string | formula_data of general_data
1.58 + | integer of string
1.59 + | identifier of string
1.60 + | general_function of general_data | useful_info of general_list
1.61 + | file_name of string
1.62 + | functor_ of symbol
1.63 + | term of tptp_term
1.64 + | arguments of tptp_term list
1.65 + | defined_functor of symbol
1.66 + | system_functor of symbol
1.67 + | system_constant of symbol
1.68 + | system_term of symbol * tptp_term list
1.69 + | defined_constant of symbol
1.70 + | defined_plain_term of symbol * tptp_term list
1.71 + | defined_atomic_term of tptp_term
1.72 + | defined_atom of tptp_term
1.73 + | defined_term of tptp_term
1.74 + | constant of symbol
1.75 + | plain_term of symbol * tptp_term list
1.76 + | function_term of tptp_term
1.77 + | conditional_term of tptp_term
1.78 + | system_atomic_formula of tptp_formula
1.79 + | infix_equality of symbol
1.80 + | infix_inequality of symbol
1.81 + | defined_infix_pred of symbol
1.82 + | defined_infix_formula of tptp_formula
1.83 + | defined_prop of string
1.84 + | defined_pred of string
1.85 + | defined_plain_formula of tptp_formula
1.86 + | defined_atomic_formula of tptp_formula
1.87 + | plain_atomic_formula of tptp_formula
1.88 + | atomic_formula of tptp_formula
1.89 + | unary_connective of symbol
1.90 +
1.91 + | defined_type of tptp_base_type
1.92 + | system_type of string
1.93 + | assoc_connective of symbol
1.94 + | binary_connective of symbol
1.95 + | fol_quantifier of quantifier
1.96 + | thf_unary_connective of symbol
1.97 + | thf_pair_connective of symbol
1.98 + | thf_quantifier of quantifier
1.99 + | fol_infix_unary of tptp_formula
1.100 + | thf_conn_term of symbol
1.101 + | literal of tptp_formula
1.102 + | disjunction of tptp_formula
1.103 + | cnf_formula of tptp_formula
1.104 + | fof_tuple_list of tptp_formula list
1.105 + | fof_tuple of tptp_formula list
1.106 + | fof_sequent of tptp_formula
1.107 + | fof_unary_formula of tptp_formula
1.108 + | fof_variable_list of string list
1.109 + | fof_quantified_formula of tptp_formula
1.110 + | fof_unitary_formula of tptp_formula
1.111 + | fof_and_formula of tptp_formula
1.112 + | fof_or_formula of tptp_formula
1.113 + | fof_binary_assoc of tptp_formula
1.114 + | fof_binary_nonassoc of tptp_formula
1.115 + | fof_binary_formula of tptp_formula
1.116 + | fof_logic_formula of tptp_formula
1.117 + | fof_formula of tptp_formula
1.118 + | tff_tuple of tptp_formula list
1.119 + | tff_tuple_list of tptp_formula list
1.120 + | tff_sequent of tptp_formula
1.121 + | tff_conditional of tptp_formula
1.122 + | tff_defined_var of tptp_let
1.123 + | tff_let_list of tptp_let list
1.124 + | tptp_let of tptp_formula
1.125 + | tff_xprod_type of tptp_type
1.126 + | tff_mapping_type of tptp_type
1.127 + | tff_atomic_type of tptp_type
1.128 + | tff_unitary_type of tptp_type
1.129 + | tff_top_level_type of tptp_type
1.130 + | tff_untyped_atom of symbol * tptp_type option
1.131 + | tff_typed_atom of symbol * tptp_type option
1.132 + | tff_unary_formula of tptp_formula
1.133 + | tff_typed_variable of string * tptp_type option
1.134 + | tff_variable of string * tptp_type option
1.135 + | tff_variable_list of (string * tptp_type option) list
1.136 + | tff_quantified_formula of tptp_formula
1.137 + | tff_unitary_formula of tptp_formula
1.138 + | tff_and_formula of tptp_formula
1.139 + | tff_or_formula of tptp_formula
1.140 + | tff_binary_assoc of tptp_formula
1.141 + | tff_binary_nonassoc of tptp_formula
1.142 + | tff_binary_formula of tptp_formula
1.143 + | tff_logic_formula of tptp_formula
1.144 + | tff_formula of tptp_formula
1.145 +
1.146 + | thf_tuple of tptp_formula list
1.147 + | thf_tuple_list of tptp_formula list
1.148 + | thf_sequent of tptp_formula
1.149 + | thf_conditional of tptp_formula
1.150 + | thf_defined_var of tptp_let
1.151 + | thf_let_list of tptp_let list
1.152 + | thf_let of tptp_formula
1.153 + | thf_atom of tptp_formula
1.154 + | thf_union_type of tptp_type
1.155 + | thf_xprod_type of tptp_type
1.156 + | thf_mapping_type of tptp_type
1.157 + | thf_binary_type of tptp_type
1.158 + | thf_unitary_type of tptp_type
1.159 + | thf_top_level_type of tptp_type
1.160 + | thf_subtype of tptp_type
1.161 + | thf_typeable_formula of tptp_formula
1.162 + | thf_type_formula of tptp_formula * tptp_type
1.163 + | thf_unary_formula of tptp_formula
1.164 + | thf_typed_variable of string * tptp_type option
1.165 + | thf_variable of string * tptp_type option
1.166 + | thf_variable_list of (string * tptp_type option) list
1.167 + | thf_quantified_formula of tptp_formula
1.168 + | thf_unitary_formula of tptp_formula
1.169 + | thf_apply_formula of tptp_formula
1.170 + | thf_and_formula of tptp_formula
1.171 + | thf_or_formula of tptp_formula
1.172 + | thf_binary_tuple of tptp_formula
1.173 + | thf_binary_pair of tptp_formula
1.174 + | thf_binary_formula of tptp_formula
1.175 + | thf_logic_formula of tptp_formula
1.176 + | thf_formula of tptp_formula
1.177 + | formula_role of role
1.178 +
1.179 + | cnf_annotated of tptp_line
1.180 + | fof_annotated of tptp_line
1.181 + | tff_annotated of tptp_line
1.182 + | thf_annotated of tptp_line
1.183 + | annotated_formula of tptp_line
1.184 + | include_ of tptp_line
1.185 + | tptp_input of tptp_line
1.186 + | tptp_file of tptp_problem
1.187 + | tptp of tptp_problem
1.188 +
1.189 +%pos int
1.190 +%eop EOF
1.191 +%noshift EOF
1.192 +%arg (file_name) : string
1.193 +
1.194 +%nonassoc LET
1.195 +%nonassoc RPAREN
1.196 +%nonassoc DUD
1.197 +%right COMMA
1.198 +%left COLON
1.199 +
1.200 +%left AT_SIGN
1.201 +%nonassoc IFF XOR
1.202 +%right IMPLIES IF
1.203 +%nonassoc EQUALS NEQUALS
1.204 +%right VLINE NOR
1.205 +%left AMPERSAND NAND
1.206 +%right ARROW
1.207 +%left PLUS
1.208 +%left TIMES
1.209 +
1.210 +%right OPERATOR_FORALL OPERATOR_EXISTS
1.211 +
1.212 +%nonassoc EXCLAMATION QUESTION LAMBDA CARET
1.213 +%nonassoc TILDE
1.214 +%pure
1.215 +%start tptp
1.216 +%verbose
1.217 +%%
1.218 +
1.219 +(* Title: HOL/TPTP/TPTP_Parser/tptp.yacc
1.220 + Author: Nik Sultana, Cambridge University Computer Laboratory
1.221 +
1.222 + Parser for TPTP languages. Latest version of the language spec can
1.223 + be obtained from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html
1.224 +*)
1.225 +
1.226 +annotations : COMMA general_term optional_info (( SOME (general_term, optional_info) ))
1.227 + | (( NONE ))
1.228 +
1.229 +optional_info : COMMA useful_info (( useful_info ))
1.230 + | (( [] ))
1.231 +
1.232 +useful_info : general_list (( general_list ))
1.233 +
1.234 +general_list : LBRKT general_terms RBRKT (( general_terms ))
1.235 + | LBRKT RBRKT (( [] ))
1.236 +
1.237 +general_terms : general_term COMMA general_terms (( general_term :: general_terms ))
1.238 + | general_term (( [general_term] ))
1.239 +
1.240 +general_term : general_data (( General_Data general_data ))
1.241 + | general_data COLON general_term (( General_Term (general_data, general_term) ))
1.242 + | general_list (( General_List general_list ))
1.243 +
1.244 +atomic_word : LOWER_WORD (( LOWER_WORD ))
1.245 + | SINGLE_QUOTED (( SINGLE_QUOTED ))
1.246 + | THF (( "thf" ))
1.247 + | TFF (( "tff" ))
1.248 + | FOF (( "fof" ))
1.249 + | CNF (( "cnf" ))
1.250 + | INCLUDE (( "include" ))
1.251 +
1.252 +variable_ : UPPER_WORD (( UPPER_WORD ))
1.253 +
1.254 +general_function: atomic_word LPAREN general_terms RPAREN (( Application (atomic_word, general_terms) ))
1.255 +
1.256 +general_data : atomic_word (( Atomic_Word atomic_word ))
1.257 + | general_function (( general_function ))
1.258 + | variable_ (( V variable_ ))
1.259 + | number (( Number number ))
1.260 + | DISTINCT_OBJECT (( Distinct_Object DISTINCT_OBJECT ))
1.261 + | formula_data (( formula_data ))
1.262 +
1.263 +number : integer (( (Int_num, integer) ))
1.264 + | REAL (( (Real_num, REAL) ))
1.265 + | RATIONAL (( (Rat_num, RATIONAL) ))
1.266 +
1.267 +integer: UNSIGNED_INTEGER (( UNSIGNED_INTEGER ))
1.268 + | SIGNED_INTEGER (( SIGNED_INTEGER ))
1.269 +
1.270 +file_name : SINGLE_QUOTED (( SINGLE_QUOTED ))
1.271 +
1.272 +formula_data : DTHF LPAREN thf_formula RPAREN (( Formula_Data (THF, thf_formula) ))
1.273 + | DTFF LPAREN tff_formula RPAREN (( Formula_Data (TFF, tff_formula) ))
1.274 + | DFOF LPAREN fof_formula RPAREN (( Formula_Data (FOF, fof_formula) ))
1.275 + | DCNF LPAREN cnf_formula RPAREN (( Formula_Data (CNF, cnf_formula) ))
1.276 + | DFOT LPAREN term RPAREN (( Term_Data term ))
1.277 +
1.278 +system_type : ATOMIC_SYSTEM_WORD (( ATOMIC_SYSTEM_WORD ))
1.279 +
1.280 +defined_type : ATOMIC_DEFINED_WORD ((
1.281 + case ATOMIC_DEFINED_WORD of
1.282 + "$i" => Type_Ind
1.283 + | "$o" => Type_Bool
1.284 + | "$iType" => Type_Ind
1.285 + | "$oType" => Type_Bool
1.286 + | "$int" => Type_Int
1.287 + | "$real" => Type_Real
1.288 + | "$rat" => Type_Rat
1.289 + | "$tType" => Type_Type
1.290 + | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
1.291 +))
1.292 +
1.293 +functor_ : atomic_word (( Uninterpreted atomic_word ))
1.294 +
1.295 +arguments : term (( [term] ))
1.296 + | term COMMA arguments (( term :: arguments ))
1.297 +
1.298 +system_functor : ATOMIC_SYSTEM_WORD (( System ATOMIC_SYSTEM_WORD ))
1.299 +system_constant : system_functor (( system_functor ))
1.300 +system_term : system_constant (( (system_constant, []) ))
1.301 + | system_functor LPAREN arguments RPAREN (( (system_functor, arguments) ))
1.302 +
1.303 +defined_functor : ATOMIC_DEFINED_WORD ((
1.304 + case ATOMIC_DEFINED_WORD of
1.305 + "$sum" => Interpreted_ExtraLogic Sum
1.306 + | "$difference" => Interpreted_ExtraLogic Difference
1.307 + | "$product" => Interpreted_ExtraLogic Product
1.308 + | "$quotient" => Interpreted_ExtraLogic Quotient
1.309 + | "$quotient_e" => Interpreted_ExtraLogic Quotient_E
1.310 + | "$quotient_t" => Interpreted_ExtraLogic Quotient_T
1.311 + | "$quotient_f" => Interpreted_ExtraLogic Quotient_F
1.312 + | "$remainder_e" => Interpreted_ExtraLogic Remainder_E
1.313 + | "$remainder_t" => Interpreted_ExtraLogic Remainder_T
1.314 + | "$remainder_f" => Interpreted_ExtraLogic Remainder_F
1.315 + | "$floor" => Interpreted_ExtraLogic Floor
1.316 + | "$ceiling" => Interpreted_ExtraLogic Ceiling
1.317 + | "$truncate" => Interpreted_ExtraLogic Truncate
1.318 + | "$round" => Interpreted_ExtraLogic Round
1.319 + | "$to_int" => Interpreted_ExtraLogic To_Int
1.320 + | "$to_rat" => Interpreted_ExtraLogic To_Rat
1.321 + | "$to_real" => Interpreted_ExtraLogic To_Real
1.322 + | "$uminus" => Interpreted_ExtraLogic UMinus
1.323 +
1.324 + | "$i" => TypeSymbol Type_Ind
1.325 + | "$o" => TypeSymbol Type_Bool
1.326 + | "$iType" => TypeSymbol Type_Ind
1.327 + | "$oType" => TypeSymbol Type_Bool
1.328 + | "$int" => TypeSymbol Type_Int
1.329 + | "$real" => TypeSymbol Type_Real
1.330 + | "$rat" => TypeSymbol Type_Rat
1.331 + | "$tType" => TypeSymbol Type_Type
1.332 +
1.333 + | "$true" => Interpreted_Logic True
1.334 + | "$false" => Interpreted_Logic False
1.335 +
1.336 + | "$less" => Interpreted_ExtraLogic Less
1.337 + | "$lesseq" => Interpreted_ExtraLogic LessEq
1.338 + | "$greatereq" => Interpreted_ExtraLogic GreaterEq
1.339 + | "$greater" => Interpreted_ExtraLogic Greater
1.340 + | "$evaleq" => Interpreted_ExtraLogic EvalEq
1.341 +
1.342 + | "$is_int" => Interpreted_ExtraLogic Is_Int
1.343 + | "$is_rat" => Interpreted_ExtraLogic Is_Rat
1.344 +
1.345 + | thing => raise UNRECOGNISED_SYMBOL ("defined_functor", thing)
1.346 +))
1.347 +
1.348 +defined_constant : defined_functor (( defined_functor ))
1.349 +
1.350 +defined_plain_term : defined_constant (( (defined_constant, []) ))
1.351 + | defined_functor LPAREN arguments RPAREN (( (defined_functor, arguments) ))
1.352 +defined_atomic_term : defined_plain_term (( Term_Func defined_plain_term ))
1.353 +defined_atom : number (( Term_Num number ))
1.354 + | DISTINCT_OBJECT (( Term_Distinct_Object DISTINCT_OBJECT ))
1.355 +defined_term : defined_atom (( defined_atom ))
1.356 + | defined_atomic_term (( defined_atomic_term ))
1.357 +constant : functor_ (( functor_ ))
1.358 +plain_term : constant (( (constant, []) ))
1.359 + | functor_ LPAREN arguments RPAREN (( (functor_, arguments) ))
1.360 +function_term : plain_term (( Term_Func plain_term ))
1.361 + | defined_term (( defined_term ))
1.362 + | system_term (( Term_Func system_term ))
1.363 +
1.364 +conditional_term : ITE_T LPAREN tff_logic_formula COMMA term COMMA term RPAREN ((
1.365 + Term_Conditional (tff_logic_formula, term1, term2)
1.366 +))
1.367 +
1.368 +term : function_term (( function_term ))
1.369 + | variable_ (( Term_Var variable_ ))
1.370 + | conditional_term (( conditional_term ))
1.371 +
1.372 +system_atomic_formula : system_term (( Pred system_term ))
1.373 +infix_equality : EQUALS (( Interpreted_Logic Equals ))
1.374 +infix_inequality : NEQUALS (( Interpreted_Logic NEquals ))
1.375 +defined_infix_pred : infix_equality (( infix_equality ))
1.376 +defined_infix_formula : term defined_infix_pred term ((Pred (defined_infix_pred, [term1, term2])))
1.377 +defined_prop : ATOMIC_DEFINED_WORD ((
1.378 + case ATOMIC_DEFINED_WORD of
1.379 + "$true" => "$true"
1.380 + | "$false" => "$false"
1.381 + | thing => raise UNRECOGNISED_SYMBOL ("defined_prop", thing)
1.382 +))
1.383 +defined_pred : ATOMIC_DEFINED_WORD ((
1.384 + case ATOMIC_DEFINED_WORD of
1.385 + "$distinct" => "$distinct"
1.386 + | "$ite_f" => "$ite_f"
1.387 + | "$less" => "$less"
1.388 + | "$lesseq" => "$lesseq"
1.389 + | "$greater" => "$greater"
1.390 + | "$greatereq" => "$greatereq"
1.391 + | "$is_int" => "$is_int"
1.392 + | "$is_rat" => "$is_rat"
1.393 + | thing => raise UNRECOGNISED_SYMBOL ("defined_pred", thing)
1.394 +))
1.395 +defined_plain_formula : defined_plain_term (( Pred defined_plain_term ))
1.396 +defined_atomic_formula : defined_plain_formula (( defined_plain_formula ))
1.397 + | defined_infix_formula (( defined_infix_formula ))
1.398 +plain_atomic_formula : plain_term (( Pred plain_term ))
1.399 +atomic_formula : plain_atomic_formula (( plain_atomic_formula ))
1.400 + | defined_atomic_formula (( defined_atomic_formula ))
1.401 + | system_atomic_formula (( system_atomic_formula ))
1.402 +
1.403 +assoc_connective : VLINE (( Interpreted_Logic Or ))
1.404 + | AMPERSAND (( Interpreted_Logic And ))
1.405 +binary_connective : IFF (( Interpreted_Logic Iff ))
1.406 + | IMPLIES (( Interpreted_Logic If ))
1.407 + | IF (( Interpreted_Logic Fi ))
1.408 + | XOR (( Interpreted_Logic Xor ))
1.409 + | NOR (( Interpreted_Logic Nor ))
1.410 + | NAND (( Interpreted_Logic Nand ))
1.411 +
1.412 +fol_quantifier : EXCLAMATION (( Forall ))
1.413 + | QUESTION (( Exists ))
1.414 +thf_unary_connective : unary_connective (( unary_connective ))
1.415 + | OPERATOR_FORALL (( Interpreted_Logic Op_Forall ))
1.416 + | OPERATOR_EXISTS (( Interpreted_Logic Op_Exists ))
1.417 +thf_pair_connective : infix_equality (( infix_equality ))
1.418 + | infix_inequality (( infix_inequality ))
1.419 + | binary_connective (( binary_connective ))
1.420 +thf_quantifier : fol_quantifier (( fol_quantifier ))
1.421 + | CARET (( Lambda ))
1.422 + | DEP_PROD (( Dep_Prod ))
1.423 + | DEP_SUM (( Dep_Sum ))
1.424 + | INDEF_CHOICE (( Epsilon ))
1.425 + | DEFIN_CHOICE (( Iota ))
1.426 +fol_infix_unary : term infix_inequality term (( Pred (infix_inequality, [term1, term2]) ))
1.427 +thf_conn_term : thf_pair_connective (( thf_pair_connective ))
1.428 + | assoc_connective (( assoc_connective ))
1.429 + | thf_unary_connective (( thf_unary_connective ))
1.430 +literal : atomic_formula (( atomic_formula ))
1.431 + | TILDE atomic_formula (( Fmla (Interpreted_Logic Not, [atomic_formula]) ))
1.432 + | fol_infix_unary (( fol_infix_unary ))
1.433 +disjunction : literal (( literal ))
1.434 + | disjunction VLINE literal (( Fmla (Interpreted_Logic Or, [disjunction, literal]) ))
1.435 +cnf_formula : LPAREN disjunction RPAREN (( disjunction ))
1.436 + | disjunction (( disjunction ))
1.437 +fof_tuple_list : fof_logic_formula (( [fof_logic_formula] ))
1.438 + | fof_logic_formula COMMA fof_tuple_list (( fof_logic_formula :: fof_tuple_list ))
1.439 +fof_tuple : LBRKT RBRKT (( [] ))
1.440 + | LBRKT fof_tuple_list RBRKT (( fof_tuple_list ))
1.441 +fof_sequent : fof_tuple GENTZEN_ARROW fof_tuple (( Sequent (fof_tuple1, fof_tuple2) ))
1.442 + | LPAREN fof_sequent RPAREN (( fof_sequent ))
1.443 +unary_connective : TILDE (( Interpreted_Logic Not ))
1.444 +fof_unary_formula : unary_connective fof_unitary_formula (( Fmla (unary_connective, [fof_unitary_formula]) ))
1.445 + | fol_infix_unary (( fol_infix_unary ))
1.446 +fof_variable_list : variable_ (( [variable_] ))
1.447 + | variable_ COMMA fof_variable_list (( variable_ :: fof_variable_list ))
1.448 +fof_quantified_formula : fol_quantifier LBRKT fof_variable_list RBRKT COLON fof_unitary_formula ((
1.449 + Quant (fol_quantifier, map (fn v => (v, NONE)) fof_variable_list, fof_unitary_formula)
1.450 +))
1.451 +fof_unitary_formula : fof_quantified_formula (( fof_quantified_formula ))
1.452 + | fof_unary_formula (( fof_unary_formula ))
1.453 + | atomic_formula (( atomic_formula ))
1.454 + | LPAREN fof_logic_formula RPAREN (( fof_logic_formula ))
1.455 +fof_and_formula : fof_unitary_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_unitary_formula1, fof_unitary_formula2]) ))
1.456 + | fof_and_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_and_formula, fof_unitary_formula]) ))
1.457 +fof_or_formula : fof_unitary_formula VLINE fof_unitary_formula (( Fmla (Interpreted_Logic Or, [fof_unitary_formula1, fof_unitary_formula2]) ))
1.458 + | fof_or_formula VLINE fof_unitary_formula (( Fmla (Interpreted_Logic Or, [fof_or_formula, fof_unitary_formula]) ))
1.459 +fof_binary_assoc : fof_or_formula (( fof_or_formula ))
1.460 + | fof_and_formula (( fof_and_formula ))
1.461 +fof_binary_nonassoc : fof_unitary_formula binary_connective fof_unitary_formula ((
1.462 + Fmla (binary_connective, [fof_unitary_formula1, fof_unitary_formula2] )
1.463 +))
1.464 +fof_binary_formula : fof_binary_nonassoc (( fof_binary_nonassoc ))
1.465 + | fof_binary_assoc (( fof_binary_assoc ))
1.466 +fof_logic_formula : fof_binary_formula (( fof_binary_formula ))
1.467 + | fof_unitary_formula (( fof_unitary_formula ))
1.468 +fof_formula : fof_logic_formula (( fof_logic_formula ))
1.469 + | fof_sequent (( fof_sequent ))
1.470 +
1.471 +
1.472 +tff_tuple : LBRKT RBRKT (( [] ))
1.473 + | LBRKT tff_tuple_list RBRKT (( tff_tuple_list ))
1.474 +tff_tuple_list : tff_logic_formula COMMA tff_tuple_list (( tff_logic_formula :: tff_tuple_list ))
1.475 + | tff_logic_formula (( [tff_logic_formula] ))
1.476 +tff_sequent : tff_tuple GENTZEN_ARROW tff_tuple (( Sequent (tff_tuple1, tff_tuple2) ))
1.477 + | LPAREN tff_sequent RPAREN (( tff_sequent ))
1.478 +tff_conditional : ITE_F LPAREN tff_logic_formula COMMA tff_logic_formula COMMA tff_logic_formula RPAREN ((
1.479 + Conditional (tff_logic_formula1, tff_logic_formula2, tff_logic_formula3)
1.480 +))
1.481 +tff_defined_var : variable_ LET tff_logic_formula (( Let_fmla ((variable_, NONE), tff_logic_formula) ))
1.482 + | variable_ LET_TERM term (( Let_term ((variable_, NONE), term) ))
1.483 + | LPAREN tff_defined_var RPAREN (( tff_defined_var ))
1.484 +tff_let_list : tff_defined_var (( [tff_defined_var] ))
1.485 + | tff_defined_var COMMA tff_let_list (( tff_defined_var :: tff_let_list ))
1.486 +tptp_let : LET LBRKT tff_let_list RBRKT COLON tff_unitary_formula ((
1.487 + Let (tff_let_list, tff_unitary_formula)
1.488 +))
1.489 +tff_xprod_type : tff_atomic_type TIMES tff_atomic_type (( Prod_type(tff_atomic_type1, tff_atomic_type2) ))
1.490 + | tff_xprod_type TIMES tff_atomic_type (( Prod_type(tff_xprod_type, tff_atomic_type) ))
1.491 + | LPAREN tff_xprod_type RPAREN (( tff_xprod_type ))
1.492 +tff_mapping_type : tff_unitary_type ARROW tff_atomic_type (( Fn_type(tff_unitary_type, tff_atomic_type) ))
1.493 + | LPAREN tff_mapping_type RPAREN (( tff_mapping_type ))
1.494 +tff_atomic_type : atomic_word (( Atom_type atomic_word ))
1.495 + | defined_type (( Defined_type defined_type ))
1.496 +tff_unitary_type : tff_atomic_type (( tff_atomic_type ))
1.497 + | LPAREN tff_xprod_type RPAREN (( tff_xprod_type ))
1.498 +tff_top_level_type : tff_atomic_type (( tff_atomic_type ))
1.499 + | tff_mapping_type (( tff_mapping_type ))
1.500 +tff_untyped_atom : functor_ (( (functor_, NONE) ))
1.501 + | system_functor (( (system_functor, NONE) ))
1.502 +tff_typed_atom : tff_untyped_atom COLON tff_top_level_type (( (fst tff_untyped_atom, SOME tff_top_level_type) ))
1.503 + | LPAREN tff_typed_atom RPAREN (( tff_typed_atom ))
1.504 +
1.505 +tff_unary_formula : unary_connective tff_unitary_formula (( Fmla (unary_connective, [tff_unitary_formula]) ))
1.506 + | fol_infix_unary (( fol_infix_unary ))
1.507 +tff_typed_variable : variable_ COLON tff_atomic_type (( (variable_, SOME tff_atomic_type) ))
1.508 +tff_variable : tff_typed_variable (( tff_typed_variable ))
1.509 + | variable_ (( (variable_, NONE) ))
1.510 +tff_variable_list : tff_variable (( [tff_variable] ))
1.511 + | tff_variable COMMA tff_variable_list (( tff_variable :: tff_variable_list ))
1.512 +tff_quantified_formula : fol_quantifier LBRKT tff_variable_list RBRKT COLON tff_unitary_formula ((
1.513 + Quant (fol_quantifier, tff_variable_list, tff_unitary_formula)
1.514 +))
1.515 +tff_unitary_formula : tff_quantified_formula (( tff_quantified_formula ))
1.516 + | tff_unary_formula (( tff_unary_formula ))
1.517 + | atomic_formula (( atomic_formula ))
1.518 + | tptp_let (( tptp_let ))
1.519 + | variable_ (( Pred (Uninterpreted variable_, []) ))
1.520 + | tff_conditional (( tff_conditional ))
1.521 + | LPAREN tff_logic_formula RPAREN (( tff_logic_formula ))
1.522 +tff_and_formula : tff_unitary_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_unitary_formula1, tff_unitary_formula2]) ))
1.523 + | tff_and_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_and_formula, tff_unitary_formula]) ))
1.524 +tff_or_formula : tff_unitary_formula VLINE tff_unitary_formula (( Fmla (Interpreted_Logic Or, [tff_unitary_formula1, tff_unitary_formula2]) ))
1.525 + | tff_or_formula VLINE tff_unitary_formula (( Fmla (Interpreted_Logic Or, [tff_or_formula, tff_unitary_formula]) ))
1.526 +tff_binary_assoc : tff_or_formula (( tff_or_formula ))
1.527 + | tff_and_formula (( tff_and_formula ))
1.528 +tff_binary_nonassoc : tff_unitary_formula binary_connective tff_unitary_formula (( Fmla (binary_connective, [tff_unitary_formula1, tff_unitary_formula2]) ))
1.529 +tff_binary_formula : tff_binary_nonassoc (( tff_binary_nonassoc ))
1.530 + | tff_binary_assoc (( tff_binary_assoc ))
1.531 +tff_logic_formula : tff_binary_formula (( tff_binary_formula ))
1.532 + | tff_unitary_formula (( tff_unitary_formula ))
1.533 +tff_formula : tff_logic_formula (( tff_logic_formula ))
1.534 + | tff_typed_atom (( Atom (TFF_Typed_Atom tff_typed_atom) ))
1.535 + | tff_sequent (( tff_sequent ))
1.536 +
1.537 +thf_tuple : LBRKT RBRKT (( [] ))
1.538 + | LBRKT thf_tuple_list RBRKT (( thf_tuple_list ))
1.539 +thf_tuple_list : thf_logic_formula (( [thf_logic_formula] ))
1.540 + | thf_logic_formula COMMA thf_tuple_list (( thf_logic_formula :: thf_tuple_list ))
1.541 +thf_sequent : thf_tuple GENTZEN_ARROW thf_tuple (( Sequent(thf_tuple1, thf_tuple2) ))
1.542 + | LPAREN thf_sequent RPAREN (( thf_sequent ))
1.543 +thf_conditional : ITE_F LPAREN thf_logic_formula COMMA thf_logic_formula COMMA thf_logic_formula RPAREN ((
1.544 + Conditional (thf_logic_formula1, thf_logic_formula2, thf_logic_formula3)
1.545 +))
1.546 +thf_defined_var : thf_variable LET thf_logic_formula (( Let_fmla (thf_variable, thf_logic_formula) ))
1.547 + | LPAREN thf_defined_var RPAREN (( thf_defined_var ))
1.548 +thf_let_list : thf_defined_var (( [thf_defined_var] ))
1.549 + | thf_defined_var COMMA thf_let_list (( thf_defined_var :: thf_let_list ))
1.550 +thf_let : LET LBRKT thf_let_list RBRKT COLON thf_unitary_formula ((
1.551 + Let (thf_let_list, thf_unitary_formula)
1.552 +))
1.553 +thf_atom : term (( Atom (THF_Atom_term term) ))
1.554 + | thf_conn_term (( Atom (THF_Atom_conn_term thf_conn_term) ))
1.555 +thf_union_type : thf_unitary_type PLUS thf_unitary_type (( Sum_type(thf_unitary_type1, thf_unitary_type2) ))
1.556 + | thf_union_type PLUS thf_unitary_type (( Sum_type(thf_union_type, thf_unitary_type) ))
1.557 +thf_xprod_type : thf_unitary_type TIMES thf_unitary_type (( Prod_type(thf_unitary_type1, thf_unitary_type2) ))
1.558 + | thf_xprod_type TIMES thf_unitary_type (( Prod_type(thf_xprod_type, thf_unitary_type) ))
1.559 +thf_mapping_type : thf_unitary_type ARROW thf_unitary_type (( Fn_type(thf_unitary_type1, thf_unitary_type2) ))
1.560 + | thf_unitary_type ARROW thf_mapping_type (( Fn_type(thf_unitary_type, thf_mapping_type) ))
1.561 +thf_binary_type : thf_mapping_type (( thf_mapping_type ))
1.562 + | thf_xprod_type (( thf_xprod_type ))
1.563 + | thf_union_type (( thf_union_type ))
1.564 +thf_unitary_type : thf_unitary_formula (( Fmla_type thf_unitary_formula ))
1.565 +thf_top_level_type : thf_logic_formula (( Fmla_type thf_logic_formula ))
1.566 +thf_subtype : constant SUBTYPE constant (( Subtype(constant1, constant2) ))
1.567 +thf_typeable_formula : thf_atom (( thf_atom ))
1.568 + | LPAREN thf_logic_formula RPAREN (( thf_logic_formula ))
1.569 +thf_type_formula : thf_typeable_formula COLON thf_top_level_type (( (thf_typeable_formula, thf_top_level_type) ))
1.570 +thf_unary_formula : thf_unary_connective LPAREN thf_logic_formula RPAREN ((
1.571 + Fmla (thf_unary_connective, [thf_logic_formula])
1.572 +))
1.573 +thf_typed_variable : variable_ COLON thf_top_level_type (( (variable_, SOME thf_top_level_type) ))
1.574 +thf_variable : thf_typed_variable (( thf_typed_variable ))
1.575 + | variable_ (( (variable_, NONE) ))
1.576 +thf_variable_list : thf_variable (( [thf_variable] ))
1.577 + | thf_variable COMMA thf_variable_list (( thf_variable :: thf_variable_list ))
1.578 +thf_quantified_formula : thf_quantifier LBRKT thf_variable_list RBRKT COLON thf_unitary_formula ((
1.579 + Quant (thf_quantifier, thf_variable_list, thf_unitary_formula)
1.580 +))
1.581 +thf_unitary_formula : thf_quantified_formula (( thf_quantified_formula ))
1.582 + | thf_unary_formula (( thf_unary_formula ))
1.583 + | thf_atom (( thf_atom ))
1.584 + | thf_let (( thf_let ))
1.585 + | thf_conditional (( thf_conditional ))
1.586 + | LPAREN thf_logic_formula RPAREN (( thf_logic_formula ))
1.587 +thf_apply_formula : thf_unitary_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_unitary_formula1, thf_unitary_formula2]) ))
1.588 + | thf_apply_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_apply_formula, thf_unitary_formula]) ))
1.589 +thf_and_formula : thf_unitary_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_unitary_formula1, thf_unitary_formula2]) ))
1.590 + | thf_and_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_and_formula, thf_unitary_formula]) ))
1.591 +thf_or_formula : thf_unitary_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_unitary_formula1, thf_unitary_formula2]) ))
1.592 + | thf_or_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_or_formula, thf_unitary_formula]) ))
1.593 +thf_binary_tuple : thf_or_formula (( thf_or_formula ))
1.594 + | thf_and_formula (( thf_and_formula ))
1.595 + | thf_apply_formula (( thf_apply_formula ))
1.596 +thf_binary_pair : thf_unitary_formula thf_pair_connective thf_unitary_formula ((
1.597 + Fmla (thf_pair_connective, [thf_unitary_formula1, thf_unitary_formula2])
1.598 +))
1.599 +thf_binary_formula : thf_binary_pair (( thf_binary_pair ))
1.600 + | thf_binary_tuple (( thf_binary_tuple ))
1.601 + | thf_binary_type (( THF_type thf_binary_type ))
1.602 +thf_logic_formula : thf_binary_formula (( thf_binary_formula ))
1.603 + | thf_unitary_formula (( thf_unitary_formula ))
1.604 + | thf_type_formula (( THF_typing thf_type_formula ))
1.605 + | thf_subtype (( THF_type thf_subtype ))
1.606 +thf_formula : thf_logic_formula (( thf_logic_formula ))
1.607 + | thf_sequent (( thf_sequent ))
1.608 +
1.609 +formula_role : LOWER_WORD (( classify_role LOWER_WORD ))
1.610 +
1.611 +thf_annotated : THF LPAREN name COMMA formula_role COMMA thf_formula annotations RPAREN PERIOD ((
1.612 + Annotated_Formula ((file_name, THFleft + 1, THFright + 1),
1.613 + THF, name, formula_role, thf_formula, annotations)
1.614 +))
1.615 +
1.616 +tff_annotated : TFF LPAREN name COMMA formula_role COMMA tff_formula annotations RPAREN PERIOD ((
1.617 + Annotated_Formula ((file_name, TFFleft + 1, TFFright + 1),
1.618 + TFF, name, formula_role, tff_formula, annotations)
1.619 +))
1.620 +
1.621 +fof_annotated : FOF LPAREN name COMMA formula_role COMMA fof_formula annotations RPAREN PERIOD ((
1.622 + Annotated_Formula ((file_name, FOFleft + 1, FOFright + 1),
1.623 + FOF, name, formula_role, fof_formula, annotations)
1.624 +))
1.625 +
1.626 +cnf_annotated : CNF LPAREN name COMMA formula_role COMMA cnf_formula annotations RPAREN PERIOD ((
1.627 + Annotated_Formula ((file_name, CNFleft + 1, CNFright + 1),
1.628 + CNF, name, formula_role, cnf_formula, annotations)
1.629 +))
1.630 +
1.631 +annotated_formula : cnf_annotated (( cnf_annotated ))
1.632 + | fof_annotated (( fof_annotated ))
1.633 + | tff_annotated (( tff_annotated ))
1.634 + | thf_annotated (( thf_annotated ))
1.635 +
1.636 +include_ : INCLUDE LPAREN file_name formula_selection RPAREN PERIOD ((
1.637 + Include (file_name, formula_selection)
1.638 +))
1.639 +
1.640 +formula_selection : COMMA LBRKT name_list RBRKT (( name_list ))
1.641 + | (( [] ))
1.642 +
1.643 +name_list : name COMMA name_list (( name :: name_list ))
1.644 + | name (( [name] ))
1.645 +
1.646 +name : atomic_word (( atomic_word ))
1.647 + | integer (( integer ))
1.648 +
1.649 +tptp_input : annotated_formula (( annotated_formula ))
1.650 + | include_ (( include_ ))
1.651 +
1.652 +tptp_file : tptp_input tptp_file (( tptp_input :: tptp_file ))
1.653 + | COMMENT tptp_file (( tptp_file ))
1.654 + | (( [] ))
1.655 +
1.656 +tptp : tptp_file (( tptp_file ))