1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc Wed Apr 04 16:05:52 2012 +0200
1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc Wed Apr 04 16:29:16 2012 +0100
1.3 @@ -21,10 +21,13 @@
1.4 | "unknown" => Role_Unknown
1.5 | thing => raise (UNRECOGNISED_ROLE thing)
1.6
1.7 +fun extract_quant_info (Quant (quantifier, vars, tptp_formula)) =
1.8 + (quantifier, vars, tptp_formula)
1.9 +
1.10 %%
1.11 %name TPTP
1.12 %term AMPERSAND | AT_SIGN | CARET | COLON | COMMA | EQUALS | EXCLAMATION
1.13 - | LET | ARROW | IF | IFF | IMPLIES | INCLUDE
1.14 + | LET | ARROW | FI | IFF | IMPLIES | INCLUDE
1.15 | LAMBDA | LBRKT | LPAREN | MAP_TO | MMINUS | NAND
1.16 | NEQUALS | XOR | NOR | PERIOD | PPLUS | QUESTION | RBRKT | RPAREN
1.17 | TILDE | TOK_FALSE | TOK_I | TOK_O | TOK_INT | TOK_REAL | TOK_RAT | TOK_TRUE
1.18 @@ -40,6 +43,8 @@
1.19 | SUBTYPE | LET_TERM
1.20 | THF | TFF | FOF | CNF
1.21 | ITE_F | ITE_T
1.22 + | LET_TF | LET_FF | LET_FT | LET_TT
1.23 +
1.24 %nonterm
1.25 annotations of annotation option
1.26 | name of string
1.27 @@ -116,9 +121,6 @@
1.28 | tff_tuple_list of tptp_formula list
1.29 | tff_sequent of tptp_formula
1.30 | tff_conditional of tptp_formula
1.31 - | tff_defined_var of tptp_let
1.32 - | tff_let_list of tptp_let list
1.33 - | tptp_let of tptp_formula
1.34 | tff_xprod_type of tptp_type
1.35 | tff_mapping_type of tptp_type
1.36 | tff_atomic_type of tptp_type
1.37 @@ -144,8 +146,6 @@
1.38 | thf_tuple_list of tptp_formula list
1.39 | thf_sequent of tptp_formula
1.40 | thf_conditional of tptp_formula
1.41 - | thf_defined_var of tptp_let
1.42 - | thf_let_list of tptp_let list
1.43 | thf_let of tptp_formula
1.44 | thf_atom of tptp_formula
1.45 | thf_union_type of tptp_type
1.46 @@ -183,6 +183,15 @@
1.47 | tptp_file of tptp_problem
1.48 | tptp of tptp_problem
1.49
1.50 + | thf_let_defn of tptp_let list
1.51 + | tff_let of tptp_formula
1.52 + | tff_let_term_defn of tptp_let list
1.53 + | tff_let_formula_defn of tptp_let list
1.54 + | tff_quantified_type of tptp_type
1.55 + | tff_monotype of tptp_type
1.56 + | tff_type_arguments of tptp_type list
1.57 + | let_term of tptp_term
1.58 +
1.59 %pos int
1.60 %eop EOF
1.61 %noshift EOF
1.62 @@ -196,7 +205,7 @@
1.63
1.64 %left AT_SIGN
1.65 %nonassoc IFF XOR
1.66 -%right IMPLIES IF
1.67 +%right IMPLIES FI
1.68 %nonassoc EQUALS NEQUALS
1.69 %right VLINE NOR
1.70 %left AMPERSAND NAND
1.71 @@ -218,88 +227,488 @@
1.72
1.73 Parser for TPTP languages. Latest version of the language spec can
1.74 be obtained from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html
1.75 + This implements version 5.3.0.
1.76 *)
1.77
1.78 +tptp : tptp_file (( tptp_file ))
1.79 +
1.80 +tptp_file : tptp_input tptp_file (( tptp_input :: tptp_file ))
1.81 + | COMMENT tptp_file (( tptp_file ))
1.82 + | (( [] ))
1.83 +
1.84 +tptp_input : annotated_formula (( annotated_formula ))
1.85 + | include_ (( include_ ))
1.86 +
1.87 +annotated_formula : thf_annotated (( thf_annotated ))
1.88 + | tff_annotated (( tff_annotated ))
1.89 + | fof_annotated (( fof_annotated ))
1.90 + | cnf_annotated (( cnf_annotated ))
1.91 +
1.92 +thf_annotated : THF LPAREN name COMMA formula_role COMMA thf_formula annotations RPAREN PERIOD ((
1.93 + Annotated_Formula ((file_name, THFleft + 1, THFright + 1),
1.94 + THF, name, formula_role, thf_formula, annotations)
1.95 +))
1.96 +
1.97 +tff_annotated : TFF LPAREN name COMMA formula_role COMMA tff_formula annotations RPAREN PERIOD ((
1.98 + Annotated_Formula ((file_name, TFFleft + 1, TFFright + 1),
1.99 + TFF, name, formula_role, tff_formula, annotations)
1.100 +))
1.101 +
1.102 +fof_annotated : FOF LPAREN name COMMA formula_role COMMA fof_formula annotations RPAREN PERIOD ((
1.103 + Annotated_Formula ((file_name, FOFleft + 1, FOFright + 1),
1.104 + FOF, name, formula_role, fof_formula, annotations)
1.105 +))
1.106 +
1.107 +cnf_annotated : CNF LPAREN name COMMA formula_role COMMA cnf_formula annotations RPAREN PERIOD ((
1.108 + Annotated_Formula ((file_name, CNFleft + 1, CNFright + 1),
1.109 + CNF, name, formula_role, cnf_formula, annotations)
1.110 +))
1.111 +
1.112 annotations : COMMA general_term optional_info (( SOME (general_term, optional_info) ))
1.113 | (( NONE ))
1.114
1.115 -optional_info : COMMA useful_info (( useful_info ))
1.116 - | (( [] ))
1.117 +formula_role : LOWER_WORD (( classify_role LOWER_WORD ))
1.118
1.119 -useful_info : general_list (( general_list ))
1.120
1.121 -general_list : LBRKT general_terms RBRKT (( general_terms ))
1.122 - | LBRKT RBRKT (( [] ))
1.123 +(* THF formulas *)
1.124
1.125 -general_terms : general_term COMMA general_terms (( general_term :: general_terms ))
1.126 - | general_term (( [general_term] ))
1.127 +thf_formula : thf_logic_formula (( thf_logic_formula ))
1.128 + | thf_sequent (( thf_sequent ))
1.129
1.130 -general_term : general_data (( General_Data general_data ))
1.131 - | general_data COLON general_term (( General_Term (general_data, general_term) ))
1.132 - | general_list (( General_List general_list ))
1.133 +thf_logic_formula : thf_binary_formula (( thf_binary_formula ))
1.134 + | thf_unitary_formula (( thf_unitary_formula ))
1.135 + | thf_type_formula (( THF_typing thf_type_formula ))
1.136 + | thf_subtype (( THF_type thf_subtype ))
1.137
1.138 -atomic_word : LOWER_WORD (( LOWER_WORD ))
1.139 - | SINGLE_QUOTED (( SINGLE_QUOTED ))
1.140 - | THF (( "thf" ))
1.141 - | TFF (( "tff" ))
1.142 - | FOF (( "fof" ))
1.143 - | CNF (( "cnf" ))
1.144 - | INCLUDE (( "include" ))
1.145 +thf_binary_formula : thf_binary_pair (( thf_binary_pair ))
1.146 + | thf_binary_tuple (( thf_binary_tuple ))
1.147 + | thf_binary_type (( THF_type thf_binary_type ))
1.148
1.149 -variable_ : UPPER_WORD (( UPPER_WORD ))
1.150 +thf_binary_pair : thf_unitary_formula thf_pair_connective thf_unitary_formula ((
1.151 + Fmla (thf_pair_connective, [thf_unitary_formula1, thf_unitary_formula2])
1.152 +))
1.153
1.154 -general_function: atomic_word LPAREN general_terms RPAREN (( Application (atomic_word, general_terms) ))
1.155 +thf_binary_tuple : thf_or_formula (( thf_or_formula ))
1.156 + | thf_and_formula (( thf_and_formula ))
1.157 + | thf_apply_formula (( thf_apply_formula ))
1.158
1.159 -general_data : atomic_word (( Atomic_Word atomic_word ))
1.160 - | general_function (( general_function ))
1.161 - | variable_ (( V variable_ ))
1.162 - | number (( Number number ))
1.163 - | DISTINCT_OBJECT (( Distinct_Object DISTINCT_OBJECT ))
1.164 - | formula_data (( formula_data ))
1.165 +thf_or_formula : thf_unitary_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_unitary_formula1, thf_unitary_formula2]) ))
1.166 + | thf_or_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_or_formula, thf_unitary_formula]) ))
1.167
1.168 -number : integer (( (Int_num, integer) ))
1.169 - | REAL (( (Real_num, REAL) ))
1.170 - | RATIONAL (( (Rat_num, RATIONAL) ))
1.171 +thf_and_formula : thf_unitary_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_unitary_formula1, thf_unitary_formula2]) ))
1.172 + | thf_and_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_and_formula, thf_unitary_formula]) ))
1.173
1.174 -integer: UNSIGNED_INTEGER (( UNSIGNED_INTEGER ))
1.175 - | SIGNED_INTEGER (( SIGNED_INTEGER ))
1.176 +thf_apply_formula : thf_unitary_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_unitary_formula1, thf_unitary_formula2]) ))
1.177 + | thf_apply_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_apply_formula, thf_unitary_formula]) ))
1.178
1.179 -file_name : SINGLE_QUOTED (( SINGLE_QUOTED ))
1.180 +thf_unitary_formula : thf_quantified_formula (( thf_quantified_formula ))
1.181 + | thf_unary_formula (( thf_unary_formula ))
1.182 + | thf_atom (( thf_atom ))
1.183 + | thf_conditional (( thf_conditional ))
1.184 + | thf_let (( thf_let ))
1.185 + | LPAREN thf_logic_formula RPAREN (( thf_logic_formula ))
1.186
1.187 -formula_data : DTHF LPAREN thf_formula RPAREN (( Formula_Data (THF, thf_formula) ))
1.188 - | DTFF LPAREN tff_formula RPAREN (( Formula_Data (TFF, tff_formula) ))
1.189 - | DFOF LPAREN fof_formula RPAREN (( Formula_Data (FOF, fof_formula) ))
1.190 - | DCNF LPAREN cnf_formula RPAREN (( Formula_Data (CNF, cnf_formula) ))
1.191 - | DFOT LPAREN term RPAREN (( Term_Data term ))
1.192 +thf_quantified_formula : thf_quantifier LBRKT thf_variable_list RBRKT COLON thf_unitary_formula ((
1.193 + Quant (thf_quantifier, thf_variable_list, thf_unitary_formula)
1.194 +))
1.195 +
1.196 +thf_variable_list : thf_variable (( [thf_variable] ))
1.197 + | thf_variable COMMA thf_variable_list (( thf_variable :: thf_variable_list ))
1.198 +
1.199 +thf_variable : thf_typed_variable (( thf_typed_variable ))
1.200 + | variable_ (( (variable_, NONE) ))
1.201 +
1.202 +thf_typed_variable : variable_ COLON thf_top_level_type (( (variable_, SOME thf_top_level_type) ))
1.203 +
1.204 +thf_unary_formula : thf_unary_connective LPAREN thf_logic_formula RPAREN ((
1.205 + Fmla (thf_unary_connective, [thf_logic_formula])
1.206 +))
1.207 +
1.208 +thf_atom : term (( Atom (THF_Atom_term term) ))
1.209 + | thf_conn_term (( Atom (THF_Atom_conn_term thf_conn_term) ))
1.210 +
1.211 +thf_conditional : ITE_F LPAREN thf_logic_formula COMMA thf_logic_formula COMMA thf_logic_formula RPAREN ((
1.212 + Conditional (thf_logic_formula1, thf_logic_formula2, thf_logic_formula3)
1.213 +))
1.214 +
1.215 +thf_let : LET_TF LPAREN thf_let_defn COMMA thf_formula RPAREN ((
1.216 + Let (thf_let_defn, thf_formula)
1.217 +))
1.218 +
1.219 +(*FIXME here could check that fmla is of right form (TPTP BNF L130-134)*)
1.220 +thf_let_defn : thf_quantified_formula ((
1.221 + let
1.222 + val (_, vars, fmla) = extract_quant_info thf_quantified_formula
1.223 + in [Let_fmla (hd vars, fmla)]
1.224 + end
1.225 +))
1.226 +
1.227 +thf_type_formula : thf_typeable_formula COLON thf_top_level_type (( (thf_typeable_formula, thf_top_level_type) ))
1.228 +
1.229 +thf_typeable_formula : thf_atom (( thf_atom ))
1.230 + | LPAREN thf_logic_formula RPAREN (( thf_logic_formula ))
1.231 +
1.232 +thf_subtype : constant SUBTYPE constant (( Subtype(constant1, constant2) ))
1.233 +
1.234 +thf_top_level_type : thf_logic_formula (( Fmla_type thf_logic_formula ))
1.235 +
1.236 +thf_unitary_type : thf_unitary_formula (( Fmla_type thf_unitary_formula ))
1.237 +
1.238 +thf_binary_type : thf_mapping_type (( thf_mapping_type ))
1.239 + | thf_xprod_type (( thf_xprod_type ))
1.240 + | thf_union_type (( thf_union_type ))
1.241 +
1.242 +thf_mapping_type : thf_unitary_type ARROW thf_unitary_type (( Fn_type(thf_unitary_type1, thf_unitary_type2) ))
1.243 + | thf_unitary_type ARROW thf_mapping_type (( Fn_type(thf_unitary_type, thf_mapping_type) ))
1.244 +
1.245 +thf_xprod_type : thf_unitary_type TIMES thf_unitary_type (( Prod_type(thf_unitary_type1, thf_unitary_type2) ))
1.246 + | thf_xprod_type TIMES thf_unitary_type (( Prod_type(thf_xprod_type, thf_unitary_type) ))
1.247 +
1.248 +thf_union_type : thf_unitary_type PLUS thf_unitary_type (( Sum_type(thf_unitary_type1, thf_unitary_type2) ))
1.249 + | thf_union_type PLUS thf_unitary_type (( Sum_type(thf_union_type, thf_unitary_type) ))
1.250 +
1.251 +thf_sequent : thf_tuple GENTZEN_ARROW thf_tuple (( Sequent(thf_tuple1, thf_tuple2) ))
1.252 + | LPAREN thf_sequent RPAREN (( thf_sequent ))
1.253 +
1.254 +thf_tuple : LBRKT RBRKT (( [] ))
1.255 + | LBRKT thf_tuple_list RBRKT (( thf_tuple_list ))
1.256 +
1.257 +thf_tuple_list : thf_logic_formula (( [thf_logic_formula] ))
1.258 + | thf_logic_formula COMMA thf_tuple_list (( thf_logic_formula :: thf_tuple_list ))
1.259 +
1.260 +
1.261 +(* TFF Formulas *)
1.262 +
1.263 +tff_formula : tff_logic_formula (( tff_logic_formula ))
1.264 + | tff_typed_atom (( Atom (TFF_Typed_Atom tff_typed_atom) ))
1.265 + | tff_sequent (( tff_sequent ))
1.266 +
1.267 +tff_logic_formula : tff_binary_formula (( tff_binary_formula ))
1.268 + | tff_unitary_formula (( tff_unitary_formula ))
1.269 +
1.270 +tff_binary_formula : tff_binary_nonassoc (( tff_binary_nonassoc ))
1.271 + | tff_binary_assoc (( tff_binary_assoc ))
1.272 +
1.273 +tff_binary_nonassoc : tff_unitary_formula binary_connective tff_unitary_formula (( Fmla (binary_connective, [tff_unitary_formula1, tff_unitary_formula2]) ))
1.274 +
1.275 +tff_binary_assoc : tff_or_formula (( tff_or_formula ))
1.276 + | tff_and_formula (( tff_and_formula ))
1.277 +
1.278 +tff_or_formula : tff_unitary_formula VLINE tff_unitary_formula (( Fmla (Interpreted_Logic Or, [tff_unitary_formula1, tff_unitary_formula2]) ))
1.279 + | tff_or_formula VLINE tff_unitary_formula (( Fmla (Interpreted_Logic Or, [tff_or_formula, tff_unitary_formula]) ))
1.280 +
1.281 +tff_and_formula : tff_unitary_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_unitary_formula1, tff_unitary_formula2]) ))
1.282 + | tff_and_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_and_formula, tff_unitary_formula]) ))
1.283 +
1.284 +tff_unitary_formula : tff_quantified_formula (( tff_quantified_formula ))
1.285 + | tff_unary_formula (( tff_unary_formula ))
1.286 + | atomic_formula (( atomic_formula ))
1.287 + | tff_conditional (( tff_conditional ))
1.288 + | tff_let (( tff_let ))
1.289 + | LPAREN tff_logic_formula RPAREN (( tff_logic_formula ))
1.290 +
1.291 +tff_quantified_formula : fol_quantifier LBRKT tff_variable_list RBRKT COLON tff_unitary_formula ((
1.292 + Quant (fol_quantifier, tff_variable_list, tff_unitary_formula)
1.293 +))
1.294 +
1.295 +tff_variable_list : tff_variable (( [tff_variable] ))
1.296 + | tff_variable COMMA tff_variable_list (( tff_variable :: tff_variable_list ))
1.297 +
1.298 +tff_variable : tff_typed_variable (( tff_typed_variable ))
1.299 + | variable_ (( (variable_, NONE) ))
1.300 +
1.301 +tff_typed_variable : variable_ COLON tff_atomic_type (( (variable_, SOME tff_atomic_type) ))
1.302 +
1.303 +tff_unary_formula : unary_connective tff_unitary_formula (( Fmla (unary_connective, [tff_unitary_formula]) ))
1.304 + | fol_infix_unary (( fol_infix_unary ))
1.305 +
1.306 +tff_conditional : ITE_F LPAREN tff_logic_formula COMMA tff_logic_formula COMMA tff_logic_formula RPAREN ((
1.307 + Conditional (tff_logic_formula1, tff_logic_formula2, tff_logic_formula3)
1.308 +))
1.309 +
1.310 +tff_let : LET_TF LPAREN tff_let_term_defn COMMA tff_formula RPAREN ((Let (tff_let_term_defn, tff_formula) ))
1.311 + | LET_FF LPAREN tff_let_formula_defn COMMA tff_formula RPAREN (( Let (tff_let_formula_defn, tff_formula) ))
1.312 +
1.313 +(*FIXME here could check that fmla is of right form (TPTP BNF L210-214)*)
1.314 +(*FIXME why "term" if using "Let_fmla"?*)
1.315 +tff_let_term_defn : tff_quantified_formula ((
1.316 + let
1.317 + val (_, vars, fmla) = extract_quant_info tff_quantified_formula
1.318 + in [Let_fmla (hd vars, fmla)]
1.319 + end
1.320 +))
1.321 +
1.322 +(*FIXME here could check that fmla is of right form (TPTP BNF L215-217)*)
1.323 +tff_let_formula_defn : tff_quantified_formula ((
1.324 + let
1.325 + val (_, vars, fmla) = extract_quant_info tff_quantified_formula
1.326 + in [Let_fmla (hd vars, fmla)]
1.327 + end
1.328 +))
1.329 +
1.330 +tff_sequent : tff_tuple GENTZEN_ARROW tff_tuple (( Sequent (tff_tuple1, tff_tuple2) ))
1.331 + | LPAREN tff_sequent RPAREN (( tff_sequent ))
1.332 +
1.333 +tff_tuple : LBRKT RBRKT (( [] ))
1.334 + | LBRKT tff_tuple_list RBRKT (( tff_tuple_list ))
1.335 +
1.336 +tff_tuple_list : tff_logic_formula COMMA tff_tuple_list (( tff_logic_formula :: tff_tuple_list ))
1.337 + | tff_logic_formula (( [tff_logic_formula] ))
1.338 +
1.339 +tff_typed_atom : tff_untyped_atom COLON tff_top_level_type (( (fst tff_untyped_atom, SOME tff_top_level_type) ))
1.340 + | LPAREN tff_typed_atom RPAREN (( tff_typed_atom ))
1.341 +
1.342 +tff_untyped_atom : functor_ (( (functor_, NONE) ))
1.343 + | system_functor (( (system_functor, NONE) ))
1.344 +
1.345 +tff_top_level_type : tff_atomic_type (( tff_atomic_type ))
1.346 + | tff_mapping_type (( tff_mapping_type ))
1.347 + | tff_quantified_type (( tff_quantified_type ))
1.348 +
1.349 +tff_quantified_type : DEP_PROD LBRKT tff_variable_list RBRKT COLON tff_monotype ((
1.350 + Fmla_type (Quant (Dep_Prod, tff_variable_list, THF_type tff_monotype))
1.351 +))
1.352 + | LPAREN tff_quantified_type RPAREN (( tff_quantified_type ))
1.353 +
1.354 +tff_monotype : tff_atomic_type (( tff_atomic_type ))
1.355 + | LPAREN tff_mapping_type RPAREN (( tff_mapping_type ))
1.356 +
1.357 +tff_unitary_type : tff_atomic_type (( tff_atomic_type ))
1.358 + | LPAREN tff_xprod_type RPAREN (( tff_xprod_type ))
1.359 +
1.360 +tff_atomic_type : atomic_word (( Atom_type atomic_word ))
1.361 + | defined_type (( Defined_type defined_type ))
1.362 + | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map THF_type tff_type_arguments))) ))
1.363 + | variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) ))
1.364 +
1.365 +tff_type_arguments : tff_atomic_type (( [tff_atomic_type] ))
1.366 + | tff_atomic_type COMMA tff_type_arguments (( tff_atomic_type :: tff_type_arguments ))
1.367 +
1.368 +tff_mapping_type : tff_unitary_type ARROW tff_atomic_type (( Fn_type(tff_unitary_type, tff_atomic_type) ))
1.369 + | LPAREN tff_mapping_type RPAREN (( tff_mapping_type ))
1.370 +
1.371 +tff_xprod_type : tff_atomic_type TIMES tff_atomic_type (( Prod_type(tff_atomic_type1, tff_atomic_type2) ))
1.372 + | tff_xprod_type TIMES tff_atomic_type (( Prod_type(tff_xprod_type, tff_atomic_type) ))
1.373 + | LPAREN tff_xprod_type RPAREN (( tff_xprod_type ))
1.374 +
1.375 +
1.376 +(* FOF Formulas *)
1.377 +
1.378 +fof_formula : fof_logic_formula (( fof_logic_formula ))
1.379 + | fof_sequent (( fof_sequent ))
1.380 +
1.381 +fof_logic_formula : fof_binary_formula (( fof_binary_formula ))
1.382 + | fof_unitary_formula (( fof_unitary_formula ))
1.383 +
1.384 +fof_binary_formula : fof_binary_nonassoc (( fof_binary_nonassoc ))
1.385 + | fof_binary_assoc (( fof_binary_assoc ))
1.386 +
1.387 +fof_binary_nonassoc : fof_unitary_formula binary_connective fof_unitary_formula ((
1.388 + Fmla (binary_connective, [fof_unitary_formula1, fof_unitary_formula2] )
1.389 +))
1.390 +
1.391 +fof_binary_assoc : fof_or_formula (( fof_or_formula ))
1.392 + | fof_and_formula (( fof_and_formula ))
1.393 +
1.394 +fof_or_formula : fof_unitary_formula VLINE fof_unitary_formula (( Fmla (Interpreted_Logic Or, [fof_unitary_formula1, fof_unitary_formula2]) ))
1.395 + | fof_or_formula VLINE fof_unitary_formula (( Fmla (Interpreted_Logic Or, [fof_or_formula, fof_unitary_formula]) ))
1.396 +
1.397 +fof_and_formula : fof_unitary_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_unitary_formula1, fof_unitary_formula2]) ))
1.398 + | fof_and_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_and_formula, fof_unitary_formula]) ))
1.399 +
1.400 +fof_unitary_formula : fof_quantified_formula (( fof_quantified_formula ))
1.401 + | fof_unary_formula (( fof_unary_formula ))
1.402 + | atomic_formula (( atomic_formula ))
1.403 + | LPAREN fof_logic_formula RPAREN (( fof_logic_formula ))
1.404 +
1.405 +fof_quantified_formula : fol_quantifier LBRKT fof_variable_list RBRKT COLON fof_unitary_formula ((
1.406 + Quant (fol_quantifier, map (fn v => (v, NONE)) fof_variable_list, fof_unitary_formula)
1.407 +))
1.408 +
1.409 +fof_variable_list : variable_ (( [variable_] ))
1.410 + | variable_ COMMA fof_variable_list (( variable_ :: fof_variable_list ))
1.411 +
1.412 +fof_unary_formula : unary_connective fof_unitary_formula (( Fmla (unary_connective, [fof_unitary_formula]) ))
1.413 + | fol_infix_unary (( fol_infix_unary ))
1.414 +
1.415 +fof_sequent : fof_tuple GENTZEN_ARROW fof_tuple (( Sequent (fof_tuple1, fof_tuple2) ))
1.416 + | LPAREN fof_sequent RPAREN (( fof_sequent ))
1.417 +
1.418 +fof_tuple : LBRKT RBRKT (( [] ))
1.419 + | LBRKT fof_tuple_list RBRKT (( fof_tuple_list ))
1.420 +
1.421 +fof_tuple_list : fof_logic_formula (( [fof_logic_formula] ))
1.422 + | fof_logic_formula COMMA fof_tuple_list (( fof_logic_formula :: fof_tuple_list ))
1.423 +
1.424 +
1.425 +(* CNF Formulas *)
1.426 +
1.427 +cnf_formula : LPAREN disjunction RPAREN (( disjunction ))
1.428 + | disjunction (( disjunction ))
1.429 +
1.430 +disjunction : literal (( literal ))
1.431 + | disjunction VLINE literal (( Fmla (Interpreted_Logic Or, [disjunction, literal]) ))
1.432 +
1.433 +literal : atomic_formula (( atomic_formula ))
1.434 + | TILDE atomic_formula (( Fmla (Interpreted_Logic Not, [atomic_formula]) ))
1.435 + | fol_infix_unary (( fol_infix_unary ))
1.436 +
1.437 +
1.438 +(* Special Formulas *)
1.439 +
1.440 +thf_conn_term : thf_pair_connective (( thf_pair_connective ))
1.441 + | assoc_connective (( assoc_connective ))
1.442 + | thf_unary_connective (( thf_unary_connective ))
1.443 +
1.444 +fol_infix_unary : term infix_inequality term (( Pred (infix_inequality, [term1, term2]) ))
1.445 +
1.446 +
1.447 +(* Connectives - THF *)
1.448 +
1.449 +thf_quantifier : fol_quantifier (( fol_quantifier ))
1.450 + | CARET (( Lambda ))
1.451 + | DEP_PROD (( Dep_Prod ))
1.452 + | DEP_SUM (( Dep_Sum ))
1.453 + | INDEF_CHOICE (( Epsilon ))
1.454 + | DEFIN_CHOICE (( Iota ))
1.455 +
1.456 +thf_pair_connective : infix_equality (( infix_equality ))
1.457 + | infix_inequality (( infix_inequality ))
1.458 + | binary_connective (( binary_connective ))
1.459 +
1.460 +thf_unary_connective : unary_connective (( unary_connective ))
1.461 + | OPERATOR_FORALL (( Interpreted_Logic Op_Forall ))
1.462 + | OPERATOR_EXISTS (( Interpreted_Logic Op_Exists ))
1.463 +
1.464 +
1.465 +(* Connectives - THF and TFF
1.466 +instead of subtype_sign use token SUBTYPE
1.467 +*)
1.468 +
1.469 +
1.470 +(* Connectives - FOF *)
1.471 +
1.472 +fol_quantifier : EXCLAMATION (( Forall ))
1.473 + | QUESTION (( Exists ))
1.474 +
1.475 +binary_connective : IFF (( Interpreted_Logic Iff ))
1.476 + | IMPLIES (( Interpreted_Logic If ))
1.477 + | FI (( Interpreted_Logic Fi ))
1.478 + | XOR (( Interpreted_Logic Xor ))
1.479 + | NOR (( Interpreted_Logic Nor ))
1.480 + | NAND (( Interpreted_Logic Nand ))
1.481 +
1.482 +assoc_connective : VLINE (( Interpreted_Logic Or ))
1.483 + | AMPERSAND (( Interpreted_Logic And ))
1.484 +
1.485 +unary_connective : TILDE (( Interpreted_Logic Not ))
1.486 +
1.487 +
1.488 +(* The sequent arrow
1.489 +use token GENTZEN_ARROW
1.490 +*)
1.491 +
1.492 +
1.493 +(* Types for THF and TFF *)
1.494 +
1.495 +defined_type : ATOMIC_DEFINED_WORD ((
1.496 + case ATOMIC_DEFINED_WORD of
1.497 + "$oType" => Type_Bool
1.498 + | "$o" => Type_Bool
1.499 + | "$iType" => Type_Ind
1.500 + | "$i" => Type_Ind
1.501 + | "$tType" => Type_Type
1.502 + | "$real" => Type_Real
1.503 + | "$rat" => Type_Rat
1.504 + | "$int" => Type_Int
1.505 + | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
1.506 +))
1.507
1.508 system_type : ATOMIC_SYSTEM_WORD (( ATOMIC_SYSTEM_WORD ))
1.509
1.510 -defined_type : ATOMIC_DEFINED_WORD ((
1.511 +
1.512 +(* First-order atoms *)
1.513 +
1.514 +atomic_formula : plain_atomic_formula (( plain_atomic_formula ))
1.515 + | defined_atomic_formula (( defined_atomic_formula ))
1.516 + | system_atomic_formula (( system_atomic_formula ))
1.517 +
1.518 +plain_atomic_formula : plain_term (( Pred plain_term ))
1.519 +
1.520 +defined_atomic_formula : defined_plain_formula (( defined_plain_formula ))
1.521 + | defined_infix_formula (( defined_infix_formula ))
1.522 +
1.523 +defined_plain_formula : defined_plain_term (( Pred defined_plain_term ))
1.524 +
1.525 +(*FIXME not used*)
1.526 +defined_prop : ATOMIC_DEFINED_WORD ((
1.527 case ATOMIC_DEFINED_WORD of
1.528 - "$i" => Type_Ind
1.529 - | "$o" => Type_Bool
1.530 - | "$iType" => Type_Ind
1.531 - | "$oType" => Type_Bool
1.532 - | "$int" => Type_Int
1.533 - | "$real" => Type_Real
1.534 - | "$rat" => Type_Rat
1.535 - | "$tType" => Type_Type
1.536 - | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
1.537 + "$true" => "$true"
1.538 + | "$false" => "$false"
1.539 + | thing => raise UNRECOGNISED_SYMBOL ("defined_prop", thing)
1.540 ))
1.541
1.542 +(*FIXME not used*)
1.543 +defined_pred : ATOMIC_DEFINED_WORD ((
1.544 + case ATOMIC_DEFINED_WORD of
1.545 + "$distinct" => "$distinct"
1.546 + | "$ite_f" => "$ite_f"
1.547 + | "$less" => "$less"
1.548 + | "$lesseq" => "$lesseq"
1.549 + | "$greater" => "$greater"
1.550 + | "$greatereq" => "$greatereq"
1.551 + | "$is_int" => "$is_int"
1.552 + | "$is_rat" => "$is_rat"
1.553 + | thing => raise UNRECOGNISED_SYMBOL ("defined_pred", thing)
1.554 +))
1.555 +
1.556 +defined_infix_formula : term defined_infix_pred term ((Pred (defined_infix_pred, [term1, term2])))
1.557 +
1.558 +defined_infix_pred : infix_equality (( infix_equality ))
1.559 +
1.560 +infix_equality : EQUALS (( Interpreted_Logic Equals ))
1.561 +
1.562 +infix_inequality : NEQUALS (( Interpreted_Logic NEquals ))
1.563 +
1.564 +system_atomic_formula : system_term (( Pred system_term ))
1.565 +
1.566 +
1.567 +(* First-order terms *)
1.568 +
1.569 +term : function_term (( function_term ))
1.570 + | variable_ (( Term_Var variable_ ))
1.571 + | conditional_term (( conditional_term ))
1.572 + | let_term (( let_term ))
1.573 +
1.574 +function_term : plain_term (( Term_Func plain_term ))
1.575 + | defined_term (( defined_term ))
1.576 + | system_term (( Term_Func system_term ))
1.577 +
1.578 +plain_term : constant (( (constant, []) ))
1.579 + | functor_ LPAREN arguments RPAREN (( (functor_, arguments) ))
1.580 +
1.581 +constant : functor_ (( functor_ ))
1.582 +
1.583 functor_ : atomic_word (( Uninterpreted atomic_word ))
1.584
1.585 -arguments : term (( [term] ))
1.586 - | term COMMA arguments (( term :: arguments ))
1.587 +defined_term : defined_atom (( defined_atom ))
1.588 + | defined_atomic_term (( defined_atomic_term ))
1.589
1.590 -system_functor : ATOMIC_SYSTEM_WORD (( System ATOMIC_SYSTEM_WORD ))
1.591 -system_constant : system_functor (( system_functor ))
1.592 -system_term : system_constant (( (system_constant, []) ))
1.593 - | system_functor LPAREN arguments RPAREN (( (system_functor, arguments) ))
1.594 +defined_atom : number (( Term_Num number ))
1.595 + | DISTINCT_OBJECT (( Term_Distinct_Object DISTINCT_OBJECT ))
1.596
1.597 +defined_atomic_term : defined_plain_term (( Term_Func defined_plain_term ))
1.598 +
1.599 +defined_plain_term : defined_constant (( (defined_constant, []) ))
1.600 + | defined_functor LPAREN arguments RPAREN (( (defined_functor, arguments) ))
1.601 +
1.602 +defined_constant : defined_functor (( defined_functor ))
1.603 +
1.604 +(*FIXME must the ones other than the first batch be included here?*)
1.605 defined_functor : ATOMIC_DEFINED_WORD ((
1.606 case ATOMIC_DEFINED_WORD of
1.607 - "$sum" => Interpreted_ExtraLogic Sum
1.608 + "$uminus" => Interpreted_ExtraLogic UMinus
1.609 + | "$sum" => Interpreted_ExtraLogic Sum
1.610 | "$difference" => Interpreted_ExtraLogic Difference
1.611 | "$product" => Interpreted_ExtraLogic Product
1.612 | "$quotient" => Interpreted_ExtraLogic Quotient
1.613 @@ -316,7 +725,6 @@
1.614 | "$to_int" => Interpreted_ExtraLogic To_Int
1.615 | "$to_rat" => Interpreted_ExtraLogic To_Rat
1.616 | "$to_real" => Interpreted_ExtraLogic To_Real
1.617 - | "$uminus" => Interpreted_ExtraLogic UMinus
1.618
1.619 | "$i" => TypeSymbol Type_Ind
1.620 | "$o" => TypeSymbol Type_Bool
1.621 @@ -339,296 +747,46 @@
1.622 | "$is_int" => Interpreted_ExtraLogic Is_Int
1.623 | "$is_rat" => Interpreted_ExtraLogic Is_Rat
1.624
1.625 + | "$distinct" => Interpreted_ExtraLogic Distinct
1.626 +
1.627 | thing => raise UNRECOGNISED_SYMBOL ("defined_functor", thing)
1.628 ))
1.629
1.630 -defined_constant : defined_functor (( defined_functor ))
1.631 +system_term : system_constant (( (system_constant, []) ))
1.632 + | system_functor LPAREN arguments RPAREN (( (system_functor, arguments) ))
1.633
1.634 -defined_plain_term : defined_constant (( (defined_constant, []) ))
1.635 - | defined_functor LPAREN arguments RPAREN (( (defined_functor, arguments) ))
1.636 -defined_atomic_term : defined_plain_term (( Term_Func defined_plain_term ))
1.637 -defined_atom : number (( Term_Num number ))
1.638 - | DISTINCT_OBJECT (( Term_Distinct_Object DISTINCT_OBJECT ))
1.639 -defined_term : defined_atom (( defined_atom ))
1.640 - | defined_atomic_term (( defined_atomic_term ))
1.641 -constant : functor_ (( functor_ ))
1.642 -plain_term : constant (( (constant, []) ))
1.643 - | functor_ LPAREN arguments RPAREN (( (functor_, arguments) ))
1.644 -function_term : plain_term (( Term_Func plain_term ))
1.645 - | defined_term (( defined_term ))
1.646 - | system_term (( Term_Func system_term ))
1.647 +system_constant : system_functor (( system_functor ))
1.648 +
1.649 +system_functor : ATOMIC_SYSTEM_WORD (( System ATOMIC_SYSTEM_WORD ))
1.650 +
1.651 +variable_ : UPPER_WORD (( UPPER_WORD ))
1.652 +
1.653 +arguments : term (( [term] ))
1.654 + | term COMMA arguments (( term :: arguments ))
1.655
1.656 conditional_term : ITE_T LPAREN tff_logic_formula COMMA term COMMA term RPAREN ((
1.657 Term_Conditional (tff_logic_formula, term1, term2)
1.658 ))
1.659
1.660 -term : function_term (( function_term ))
1.661 - | variable_ (( Term_Var variable_ ))
1.662 - | conditional_term (( conditional_term ))
1.663
1.664 -system_atomic_formula : system_term (( Pred system_term ))
1.665 -infix_equality : EQUALS (( Interpreted_Logic Equals ))
1.666 -infix_inequality : NEQUALS (( Interpreted_Logic NEquals ))
1.667 -defined_infix_pred : infix_equality (( infix_equality ))
1.668 -defined_infix_formula : term defined_infix_pred term ((Pred (defined_infix_pred, [term1, term2])))
1.669 -defined_prop : ATOMIC_DEFINED_WORD ((
1.670 - case ATOMIC_DEFINED_WORD of
1.671 - "$true" => "$true"
1.672 - | "$false" => "$false"
1.673 - | thing => raise UNRECOGNISED_SYMBOL ("defined_prop", thing)
1.674 -))
1.675 -defined_pred : ATOMIC_DEFINED_WORD ((
1.676 - case ATOMIC_DEFINED_WORD of
1.677 - "$distinct" => "$distinct"
1.678 - | "$ite_f" => "$ite_f"
1.679 - | "$less" => "$less"
1.680 - | "$lesseq" => "$lesseq"
1.681 - | "$greater" => "$greater"
1.682 - | "$greatereq" => "$greatereq"
1.683 - | "$is_int" => "$is_int"
1.684 - | "$is_rat" => "$is_rat"
1.685 - | thing => raise UNRECOGNISED_SYMBOL ("defined_pred", thing)
1.686 -))
1.687 -defined_plain_formula : defined_plain_term (( Pred defined_plain_term ))
1.688 -defined_atomic_formula : defined_plain_formula (( defined_plain_formula ))
1.689 - | defined_infix_formula (( defined_infix_formula ))
1.690 -plain_atomic_formula : plain_term (( Pred plain_term ))
1.691 -atomic_formula : plain_atomic_formula (( plain_atomic_formula ))
1.692 - | defined_atomic_formula (( defined_atomic_formula ))
1.693 - | system_atomic_formula (( system_atomic_formula ))
1.694 +let_term : LET_FT LPAREN tff_let_formula_defn COMMA term RPAREN ((Term_Let (tff_let_formula_defn, term) ))
1.695 + | LET_TT LPAREN tff_let_term_defn COMMA term RPAREN ((Term_Let (tff_let_term_defn, term) ))
1.696
1.697 -assoc_connective : VLINE (( Interpreted_Logic Or ))
1.698 - | AMPERSAND (( Interpreted_Logic And ))
1.699 -binary_connective : IFF (( Interpreted_Logic Iff ))
1.700 - | IMPLIES (( Interpreted_Logic If ))
1.701 - | IF (( Interpreted_Logic Fi ))
1.702 - | XOR (( Interpreted_Logic Xor ))
1.703 - | NOR (( Interpreted_Logic Nor ))
1.704 - | NAND (( Interpreted_Logic Nand ))
1.705
1.706 -fol_quantifier : EXCLAMATION (( Forall ))
1.707 - | QUESTION (( Exists ))
1.708 -thf_unary_connective : unary_connective (( unary_connective ))
1.709 - | OPERATOR_FORALL (( Interpreted_Logic Op_Forall ))
1.710 - | OPERATOR_EXISTS (( Interpreted_Logic Op_Exists ))
1.711 -thf_pair_connective : infix_equality (( infix_equality ))
1.712 - | infix_inequality (( infix_inequality ))
1.713 - | binary_connective (( binary_connective ))
1.714 -thf_quantifier : fol_quantifier (( fol_quantifier ))
1.715 - | CARET (( Lambda ))
1.716 - | DEP_PROD (( Dep_Prod ))
1.717 - | DEP_SUM (( Dep_Sum ))
1.718 - | INDEF_CHOICE (( Epsilon ))
1.719 - | DEFIN_CHOICE (( Iota ))
1.720 -fol_infix_unary : term infix_inequality term (( Pred (infix_inequality, [term1, term2]) ))
1.721 -thf_conn_term : thf_pair_connective (( thf_pair_connective ))
1.722 - | assoc_connective (( assoc_connective ))
1.723 - | thf_unary_connective (( thf_unary_connective ))
1.724 -literal : atomic_formula (( atomic_formula ))
1.725 - | TILDE atomic_formula (( Fmla (Interpreted_Logic Not, [atomic_formula]) ))
1.726 - | fol_infix_unary (( fol_infix_unary ))
1.727 -disjunction : literal (( literal ))
1.728 - | disjunction VLINE literal (( Fmla (Interpreted_Logic Or, [disjunction, literal]) ))
1.729 -cnf_formula : LPAREN disjunction RPAREN (( disjunction ))
1.730 - | disjunction (( disjunction ))
1.731 -fof_tuple_list : fof_logic_formula (( [fof_logic_formula] ))
1.732 - | fof_logic_formula COMMA fof_tuple_list (( fof_logic_formula :: fof_tuple_list ))
1.733 -fof_tuple : LBRKT RBRKT (( [] ))
1.734 - | LBRKT fof_tuple_list RBRKT (( fof_tuple_list ))
1.735 -fof_sequent : fof_tuple GENTZEN_ARROW fof_tuple (( Sequent (fof_tuple1, fof_tuple2) ))
1.736 - | LPAREN fof_sequent RPAREN (( fof_sequent ))
1.737 -unary_connective : TILDE (( Interpreted_Logic Not ))
1.738 -fof_unary_formula : unary_connective fof_unitary_formula (( Fmla (unary_connective, [fof_unitary_formula]) ))
1.739 - | fol_infix_unary (( fol_infix_unary ))
1.740 -fof_variable_list : variable_ (( [variable_] ))
1.741 - | variable_ COMMA fof_variable_list (( variable_ :: fof_variable_list ))
1.742 -fof_quantified_formula : fol_quantifier LBRKT fof_variable_list RBRKT COLON fof_unitary_formula ((
1.743 - Quant (fol_quantifier, map (fn v => (v, NONE)) fof_variable_list, fof_unitary_formula)
1.744 -))
1.745 -fof_unitary_formula : fof_quantified_formula (( fof_quantified_formula ))
1.746 - | fof_unary_formula (( fof_unary_formula ))
1.747 - | atomic_formula (( atomic_formula ))
1.748 - | LPAREN fof_logic_formula RPAREN (( fof_logic_formula ))
1.749 -fof_and_formula : fof_unitary_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_unitary_formula1, fof_unitary_formula2]) ))
1.750 - | fof_and_formula AMPERSAND fof_unitary_formula (( Fmla (Interpreted_Logic And, [fof_and_formula, fof_unitary_formula]) ))
1.751 -fof_or_formula : fof_unitary_formula VLINE fof_unitary_formula (( Fmla (Interpreted_Logic Or, [fof_unitary_formula1, fof_unitary_formula2]) ))
1.752 - | fof_or_formula VLINE fof_unitary_formula (( Fmla (Interpreted_Logic Or, [fof_or_formula, fof_unitary_formula]) ))
1.753 -fof_binary_assoc : fof_or_formula (( fof_or_formula ))
1.754 - | fof_and_formula (( fof_and_formula ))
1.755 -fof_binary_nonassoc : fof_unitary_formula binary_connective fof_unitary_formula ((
1.756 - Fmla (binary_connective, [fof_unitary_formula1, fof_unitary_formula2] )
1.757 -))
1.758 -fof_binary_formula : fof_binary_nonassoc (( fof_binary_nonassoc ))
1.759 - | fof_binary_assoc (( fof_binary_assoc ))
1.760 -fof_logic_formula : fof_binary_formula (( fof_binary_formula ))
1.761 - | fof_unitary_formula (( fof_unitary_formula ))
1.762 -fof_formula : fof_logic_formula (( fof_logic_formula ))
1.763 - | fof_sequent (( fof_sequent ))
1.764 +(* Formula sources
1.765 +Don't currently use following non-terminals:
1.766 +source, sources, dag_source, inference_record, inference_rule, parent_list,
1.767 +parent_info, parent_details, internal_source, intro_type, external_source,
1.768 +file_source, file_info, theory, theory_name, creator_source, creator_name.
1.769 +*)
1.770
1.771
1.772 -tff_tuple : LBRKT RBRKT (( [] ))
1.773 - | LBRKT tff_tuple_list RBRKT (( tff_tuple_list ))
1.774 -tff_tuple_list : tff_logic_formula COMMA tff_tuple_list (( tff_logic_formula :: tff_tuple_list ))
1.775 - | tff_logic_formula (( [tff_logic_formula] ))
1.776 -tff_sequent : tff_tuple GENTZEN_ARROW tff_tuple (( Sequent (tff_tuple1, tff_tuple2) ))
1.777 - | LPAREN tff_sequent RPAREN (( tff_sequent ))
1.778 -tff_conditional : ITE_F LPAREN tff_logic_formula COMMA tff_logic_formula COMMA tff_logic_formula RPAREN ((
1.779 - Conditional (tff_logic_formula1, tff_logic_formula2, tff_logic_formula3)
1.780 -))
1.781 -tff_defined_var : variable_ LET tff_logic_formula (( Let_fmla ((variable_, NONE), tff_logic_formula) ))
1.782 - | variable_ LET_TERM term (( Let_term ((variable_, NONE), term) ))
1.783 - | LPAREN tff_defined_var RPAREN (( tff_defined_var ))
1.784 -tff_let_list : tff_defined_var (( [tff_defined_var] ))
1.785 - | tff_defined_var COMMA tff_let_list (( tff_defined_var :: tff_let_list ))
1.786 -tptp_let : LET LBRKT tff_let_list RBRKT COLON tff_unitary_formula ((
1.787 - Let (tff_let_list, tff_unitary_formula)
1.788 -))
1.789 -tff_xprod_type : tff_atomic_type TIMES tff_atomic_type (( Prod_type(tff_atomic_type1, tff_atomic_type2) ))
1.790 - | tff_xprod_type TIMES tff_atomic_type (( Prod_type(tff_xprod_type, tff_atomic_type) ))
1.791 - | LPAREN tff_xprod_type RPAREN (( tff_xprod_type ))
1.792 -tff_mapping_type : tff_unitary_type ARROW tff_atomic_type (( Fn_type(tff_unitary_type, tff_atomic_type) ))
1.793 - | LPAREN tff_mapping_type RPAREN (( tff_mapping_type ))
1.794 -tff_atomic_type : atomic_word (( Atom_type atomic_word ))
1.795 - | defined_type (( Defined_type defined_type ))
1.796 -tff_unitary_type : tff_atomic_type (( tff_atomic_type ))
1.797 - | LPAREN tff_xprod_type RPAREN (( tff_xprod_type ))
1.798 -tff_top_level_type : tff_atomic_type (( tff_atomic_type ))
1.799 - | tff_mapping_type (( tff_mapping_type ))
1.800 -tff_untyped_atom : functor_ (( (functor_, NONE) ))
1.801 - | system_functor (( (system_functor, NONE) ))
1.802 -tff_typed_atom : tff_untyped_atom COLON tff_top_level_type (( (fst tff_untyped_atom, SOME tff_top_level_type) ))
1.803 - | LPAREN tff_typed_atom RPAREN (( tff_typed_atom ))
1.804 +(* Useful info fields *)
1.805
1.806 -tff_unary_formula : unary_connective tff_unitary_formula (( Fmla (unary_connective, [tff_unitary_formula]) ))
1.807 - | fol_infix_unary (( fol_infix_unary ))
1.808 -tff_typed_variable : variable_ COLON tff_atomic_type (( (variable_, SOME tff_atomic_type) ))
1.809 -tff_variable : tff_typed_variable (( tff_typed_variable ))
1.810 - | variable_ (( (variable_, NONE) ))
1.811 -tff_variable_list : tff_variable (( [tff_variable] ))
1.812 - | tff_variable COMMA tff_variable_list (( tff_variable :: tff_variable_list ))
1.813 -tff_quantified_formula : fol_quantifier LBRKT tff_variable_list RBRKT COLON tff_unitary_formula ((
1.814 - Quant (fol_quantifier, tff_variable_list, tff_unitary_formula)
1.815 -))
1.816 -tff_unitary_formula : tff_quantified_formula (( tff_quantified_formula ))
1.817 - | tff_unary_formula (( tff_unary_formula ))
1.818 - | atomic_formula (( atomic_formula ))
1.819 - | tptp_let (( tptp_let ))
1.820 - | variable_ (( Pred (Uninterpreted variable_, []) ))
1.821 - | tff_conditional (( tff_conditional ))
1.822 - | LPAREN tff_logic_formula RPAREN (( tff_logic_formula ))
1.823 -tff_and_formula : tff_unitary_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_unitary_formula1, tff_unitary_formula2]) ))
1.824 - | tff_and_formula AMPERSAND tff_unitary_formula (( Fmla (Interpreted_Logic And, [tff_and_formula, tff_unitary_formula]) ))
1.825 -tff_or_formula : tff_unitary_formula VLINE tff_unitary_formula (( Fmla (Interpreted_Logic Or, [tff_unitary_formula1, tff_unitary_formula2]) ))
1.826 - | tff_or_formula VLINE tff_unitary_formula (( Fmla (Interpreted_Logic Or, [tff_or_formula, tff_unitary_formula]) ))
1.827 -tff_binary_assoc : tff_or_formula (( tff_or_formula ))
1.828 - | tff_and_formula (( tff_and_formula ))
1.829 -tff_binary_nonassoc : tff_unitary_formula binary_connective tff_unitary_formula (( Fmla (binary_connective, [tff_unitary_formula1, tff_unitary_formula2]) ))
1.830 -tff_binary_formula : tff_binary_nonassoc (( tff_binary_nonassoc ))
1.831 - | tff_binary_assoc (( tff_binary_assoc ))
1.832 -tff_logic_formula : tff_binary_formula (( tff_binary_formula ))
1.833 - | tff_unitary_formula (( tff_unitary_formula ))
1.834 -tff_formula : tff_logic_formula (( tff_logic_formula ))
1.835 - | tff_typed_atom (( Atom (TFF_Typed_Atom tff_typed_atom) ))
1.836 - | tff_sequent (( tff_sequent ))
1.837 +optional_info : COMMA useful_info (( useful_info ))
1.838 + | (( [] ))
1.839
1.840 -thf_tuple : LBRKT RBRKT (( [] ))
1.841 - | LBRKT thf_tuple_list RBRKT (( thf_tuple_list ))
1.842 -thf_tuple_list : thf_logic_formula (( [thf_logic_formula] ))
1.843 - | thf_logic_formula COMMA thf_tuple_list (( thf_logic_formula :: thf_tuple_list ))
1.844 -thf_sequent : thf_tuple GENTZEN_ARROW thf_tuple (( Sequent(thf_tuple1, thf_tuple2) ))
1.845 - | LPAREN thf_sequent RPAREN (( thf_sequent ))
1.846 -thf_conditional : ITE_F LPAREN thf_logic_formula COMMA thf_logic_formula COMMA thf_logic_formula RPAREN ((
1.847 - Conditional (thf_logic_formula1, thf_logic_formula2, thf_logic_formula3)
1.848 -))
1.849 -thf_defined_var : thf_variable LET thf_logic_formula (( Let_fmla (thf_variable, thf_logic_formula) ))
1.850 - | LPAREN thf_defined_var RPAREN (( thf_defined_var ))
1.851 -thf_let_list : thf_defined_var (( [thf_defined_var] ))
1.852 - | thf_defined_var COMMA thf_let_list (( thf_defined_var :: thf_let_list ))
1.853 -thf_let : LET LBRKT thf_let_list RBRKT COLON thf_unitary_formula ((
1.854 - Let (thf_let_list, thf_unitary_formula)
1.855 -))
1.856 -thf_atom : term (( Atom (THF_Atom_term term) ))
1.857 - | thf_conn_term (( Atom (THF_Atom_conn_term thf_conn_term) ))
1.858 -thf_union_type : thf_unitary_type PLUS thf_unitary_type (( Sum_type(thf_unitary_type1, thf_unitary_type2) ))
1.859 - | thf_union_type PLUS thf_unitary_type (( Sum_type(thf_union_type, thf_unitary_type) ))
1.860 -thf_xprod_type : thf_unitary_type TIMES thf_unitary_type (( Prod_type(thf_unitary_type1, thf_unitary_type2) ))
1.861 - | thf_xprod_type TIMES thf_unitary_type (( Prod_type(thf_xprod_type, thf_unitary_type) ))
1.862 -thf_mapping_type : thf_unitary_type ARROW thf_unitary_type (( Fn_type(thf_unitary_type1, thf_unitary_type2) ))
1.863 - | thf_unitary_type ARROW thf_mapping_type (( Fn_type(thf_unitary_type, thf_mapping_type) ))
1.864 -thf_binary_type : thf_mapping_type (( thf_mapping_type ))
1.865 - | thf_xprod_type (( thf_xprod_type ))
1.866 - | thf_union_type (( thf_union_type ))
1.867 -thf_unitary_type : thf_unitary_formula (( Fmla_type thf_unitary_formula ))
1.868 -thf_top_level_type : thf_logic_formula (( Fmla_type thf_logic_formula ))
1.869 -thf_subtype : constant SUBTYPE constant (( Subtype(constant1, constant2) ))
1.870 -thf_typeable_formula : thf_atom (( thf_atom ))
1.871 - | LPAREN thf_logic_formula RPAREN (( thf_logic_formula ))
1.872 -thf_type_formula : thf_typeable_formula COLON thf_top_level_type (( (thf_typeable_formula, thf_top_level_type) ))
1.873 -thf_unary_formula : thf_unary_connective LPAREN thf_logic_formula RPAREN ((
1.874 - Fmla (thf_unary_connective, [thf_logic_formula])
1.875 -))
1.876 -thf_typed_variable : variable_ COLON thf_top_level_type (( (variable_, SOME thf_top_level_type) ))
1.877 -thf_variable : thf_typed_variable (( thf_typed_variable ))
1.878 - | variable_ (( (variable_, NONE) ))
1.879 -thf_variable_list : thf_variable (( [thf_variable] ))
1.880 - | thf_variable COMMA thf_variable_list (( thf_variable :: thf_variable_list ))
1.881 -thf_quantified_formula : thf_quantifier LBRKT thf_variable_list RBRKT COLON thf_unitary_formula ((
1.882 - Quant (thf_quantifier, thf_variable_list, thf_unitary_formula)
1.883 -))
1.884 -thf_unitary_formula : thf_quantified_formula (( thf_quantified_formula ))
1.885 - | thf_unary_formula (( thf_unary_formula ))
1.886 - | thf_atom (( thf_atom ))
1.887 - | thf_let (( thf_let ))
1.888 - | thf_conditional (( thf_conditional ))
1.889 - | LPAREN thf_logic_formula RPAREN (( thf_logic_formula ))
1.890 -thf_apply_formula : thf_unitary_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_unitary_formula1, thf_unitary_formula2]) ))
1.891 - | thf_apply_formula AT_SIGN thf_unitary_formula (( Fmla (Interpreted_ExtraLogic Apply, [thf_apply_formula, thf_unitary_formula]) ))
1.892 -thf_and_formula : thf_unitary_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_unitary_formula1, thf_unitary_formula2]) ))
1.893 - | thf_and_formula AMPERSAND thf_unitary_formula (( Fmla (Interpreted_Logic And, [thf_and_formula, thf_unitary_formula]) ))
1.894 -thf_or_formula : thf_unitary_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_unitary_formula1, thf_unitary_formula2]) ))
1.895 - | thf_or_formula VLINE thf_unitary_formula (( Fmla (Interpreted_Logic Or, [thf_or_formula, thf_unitary_formula]) ))
1.896 -thf_binary_tuple : thf_or_formula (( thf_or_formula ))
1.897 - | thf_and_formula (( thf_and_formula ))
1.898 - | thf_apply_formula (( thf_apply_formula ))
1.899 -thf_binary_pair : thf_unitary_formula thf_pair_connective thf_unitary_formula ((
1.900 - Fmla (thf_pair_connective, [thf_unitary_formula1, thf_unitary_formula2])
1.901 -))
1.902 -thf_binary_formula : thf_binary_pair (( thf_binary_pair ))
1.903 - | thf_binary_tuple (( thf_binary_tuple ))
1.904 - | thf_binary_type (( THF_type thf_binary_type ))
1.905 -thf_logic_formula : thf_binary_formula (( thf_binary_formula ))
1.906 - | thf_unitary_formula (( thf_unitary_formula ))
1.907 - | thf_type_formula (( THF_typing thf_type_formula ))
1.908 - | thf_subtype (( THF_type thf_subtype ))
1.909 -thf_formula : thf_logic_formula (( thf_logic_formula ))
1.910 - | thf_sequent (( thf_sequent ))
1.911 -
1.912 -formula_role : LOWER_WORD (( classify_role LOWER_WORD ))
1.913 -
1.914 -thf_annotated : THF LPAREN name COMMA formula_role COMMA thf_formula annotations RPAREN PERIOD ((
1.915 - Annotated_Formula ((file_name, THFleft + 1, THFright + 1),
1.916 - THF, name, formula_role, thf_formula, annotations)
1.917 -))
1.918 -
1.919 -tff_annotated : TFF LPAREN name COMMA formula_role COMMA tff_formula annotations RPAREN PERIOD ((
1.920 - Annotated_Formula ((file_name, TFFleft + 1, TFFright + 1),
1.921 - TFF, name, formula_role, tff_formula, annotations)
1.922 -))
1.923 -
1.924 -fof_annotated : FOF LPAREN name COMMA formula_role COMMA fof_formula annotations RPAREN PERIOD ((
1.925 - Annotated_Formula ((file_name, FOFleft + 1, FOFright + 1),
1.926 - FOF, name, formula_role, fof_formula, annotations)
1.927 -))
1.928 -
1.929 -cnf_annotated : CNF LPAREN name COMMA formula_role COMMA cnf_formula annotations RPAREN PERIOD ((
1.930 - Annotated_Formula ((file_name, CNFleft + 1, CNFright + 1),
1.931 - CNF, name, formula_role, cnf_formula, annotations)
1.932 -))
1.933 -
1.934 -annotated_formula : cnf_annotated (( cnf_annotated ))
1.935 - | fof_annotated (( fof_annotated ))
1.936 - | tff_annotated (( tff_annotated ))
1.937 - | thf_annotated (( thf_annotated ))
1.938 +useful_info : general_list (( general_list ))
1.939
1.940 include_ : INCLUDE LPAREN file_name formula_selection RPAREN PERIOD ((
1.941 Include (file_name, formula_selection)
1.942 @@ -640,14 +798,56 @@
1.943 name_list : name COMMA name_list (( name :: name_list ))
1.944 | name (( [name] ))
1.945
1.946 +
1.947 +(* Non-logical data *)
1.948 +
1.949 +general_term : general_data (( General_Data general_data ))
1.950 + | general_data COLON general_term (( General_Term (general_data, general_term) ))
1.951 + | general_list (( General_List general_list ))
1.952 +
1.953 +general_data : atomic_word (( Atomic_Word atomic_word ))
1.954 + | general_function (( general_function ))
1.955 + | variable_ (( V variable_ ))
1.956 + | number (( Number number ))
1.957 + | DISTINCT_OBJECT (( Distinct_Object DISTINCT_OBJECT ))
1.958 + | formula_data (( formula_data ))
1.959 +
1.960 +general_function: atomic_word LPAREN general_terms RPAREN (( Application (atomic_word, general_terms) ))
1.961 +
1.962 +formula_data : DTHF LPAREN thf_formula RPAREN (( Formula_Data (THF, thf_formula) ))
1.963 + | DTFF LPAREN tff_formula RPAREN (( Formula_Data (TFF, tff_formula) ))
1.964 + | DFOF LPAREN fof_formula RPAREN (( Formula_Data (FOF, fof_formula) ))
1.965 + | DCNF LPAREN cnf_formula RPAREN (( Formula_Data (CNF, cnf_formula) ))
1.966 + | DFOT LPAREN term RPAREN (( Term_Data term ))
1.967 +
1.968 +general_list : LBRKT general_terms RBRKT (( general_terms ))
1.969 + | LBRKT RBRKT (( [] ))
1.970 +
1.971 +general_terms : general_term COMMA general_terms (( general_term :: general_terms ))
1.972 + | general_term (( [general_term] ))
1.973 +
1.974 +
1.975 +(* General purpose *)
1.976 +
1.977 name : atomic_word (( atomic_word ))
1.978 | integer (( integer ))
1.979
1.980 -tptp_input : annotated_formula (( annotated_formula ))
1.981 - | include_ (( include_ ))
1.982 +(*FIXME -- "THF" onwards*)
1.983 +atomic_word : LOWER_WORD (( LOWER_WORD ))
1.984 + | SINGLE_QUOTED (( SINGLE_QUOTED ))
1.985 + | THF (( "thf" ))
1.986 + | TFF (( "tff" ))
1.987 + | FOF (( "fof" ))
1.988 + | CNF (( "cnf" ))
1.989 + | INCLUDE (( "include" ))
1.990
1.991 -tptp_file : tptp_input tptp_file (( tptp_input :: tptp_file ))
1.992 - | COMMENT tptp_file (( tptp_file ))
1.993 - | (( [] ))
1.994 +(*atomic_defined_word and atomic_system_word are picked up by lex*)
1.995
1.996 -tptp : tptp_file (( tptp_file ))
1.997 +integer: UNSIGNED_INTEGER (( UNSIGNED_INTEGER ))
1.998 + | SIGNED_INTEGER (( SIGNED_INTEGER ))
1.999 +
1.1000 +number : integer (( (Int_num, integer) ))
1.1001 + | REAL (( (Real_num, REAL) ))
1.1002 + | RATIONAL (( (Rat_num, RATIONAL) ))
1.1003 +
1.1004 +file_name : SINGLE_QUOTED (( SINGLE_QUOTED ))