diff --git a/doc/dune b/doc/dune index 1a162620a..f48b317b6 100644 --- a/doc/dune +++ b/doc/dune @@ -12,7 +12,7 @@ ; Dolmen languages dolmen_ae dolmen_dimacs dolmen_icnf dolmen_zf ; tptp - dolmen_tptp dolmen_tptp_v6_3_0 + dolmen_tptp dolmen_tptp_v6_3_0 dolmen_tptp_v8_2_0 ; smtlib2 dolmen_smtlib2 dolmen_smtlib2_poly dolmen_smtlib2_v6 dolmen_smtlib2_v6_script dolmen_smtlib2_v6_response diff --git a/src/classes/dune b/src/classes/dune index 9f446742a..01860d77f 100644 --- a/src/classes/dune +++ b/src/classes/dune @@ -13,7 +13,7 @@ dolmen_smtlib2_poly dolmen_smtlib2_v6 dolmen_smtlib2_v6_script dolmen_smtlib2_v6_response ; TPTP & versions - dolmen_tptp dolmen_tptp_v6_3_0 + dolmen_tptp dolmen_tptp_v6_3_0 dolmen_tptp_v8_2_0 ; Menhir deps menhirLib) (modules Logic Response) diff --git a/src/classes/logic.ml b/src/classes/logic.ml index 225ac6801..24d88e52d 100644 --- a/src/classes/logic.ml +++ b/src/classes/logic.ml @@ -80,6 +80,7 @@ module Make "psmt2", Smtlib2 `Poly; "tptp", Tptp `Latest; "tptp-6.3.0", Tptp `V6_3_0; + "tptp-8.2.0", Tptp `V8_2_0; "zf", Zf; ] @@ -113,6 +114,8 @@ module Make (module Dolmen_tptp.Latest.Make(L)(I)(T)(S) : S); Tptp `V6_3_0, ".p", (module Dolmen_tptp.V6_3_0.Make(L)(I)(T)(S) : S); + Tptp `V8_2_0, ".p", + (module Dolmen_tptp.V8_2_0.Make(L)(I)(T)(S) : S); (* Zipperposition format *) Zf, ".zf", diff --git a/src/interface/id.ml b/src/interface/id.ml index db07c78f6..86bc16979 100644 --- a/src/interface/id.ml +++ b/src/interface/id.ml @@ -32,7 +32,10 @@ module type Logic = sig (** The usual namespace for terms. *) val attr : namespace - (** Namespace used for attributes (also called annotations) in smtlib. *) + (** Namespace used for attributes, such as: + - annotations in smtlib + - formula roles in tptp + *) val decl : namespace (** Namespace used for declaration identifiers (for instance used diff --git a/src/interface/stmt.ml b/src/interface/stmt.ml index a00fae9aa..4bd28be10 100644 --- a/src/interface/stmt.ml +++ b/src/interface/stmt.ml @@ -248,14 +248,15 @@ module type Logic = sig (** {2 TPTP Statements} *) - val tpi : ?loc:location -> ?annot:term -> id -> string -> term -> t - val thf : ?loc:location -> ?annot:term -> id -> string -> term -> t - val tff : ?loc:location -> ?annot:term -> id -> string -> term -> t - val fof : ?loc:location -> ?annot:term -> id -> string -> term -> t - val cnf : ?loc:location -> ?annot:term -> id -> string -> term -> t + val tpi : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val thf : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val tff : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val tcf : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val fof : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val cnf : ?loc:location -> ?annot:term -> id -> role:term -> term -> t (** TPTP directives. [tptp name role t] instructs the prover to register a new directive with the given name, role and term. Current tptp roles are: - - ["axiom", "hypothesis", "definition", "lemma", "theorem"] acts + - ["axiom", "hypothesis", "definition", "lemma", "theorem", "corollary"] acts as new assertions/declartions - ["assumption", "conjecture"] are proposition that need to be proved, and then can be used to prove other propositions. They are equivalent @@ -272,7 +273,7 @@ module type Logic = sig - ["type"] declares a new symbol and its type - ["plain", "unknown", "fi_domain", "fi_functors", "fi_predicates"] are valid roles with no specified semantics - - any other role is an error + - any other role is translated as an `Other` statement. *) (** {2 Zipperposition statements} *) diff --git a/src/interface/term.ml b/src/interface/term.ml index 21f866e92..8a875e750 100644 --- a/src/interface/term.ml +++ b/src/interface/term.ml @@ -93,6 +93,9 @@ module type Logic = sig val implies_t : ?loc:location -> unit -> t val pi_t : ?loc:location -> unit -> t val sigma_t : ?loc:location -> unit -> t + val subtype_t : ?loc:location -> unit -> t + val choice_t : ?loc:location -> unit -> t + val description_t : ?loc:location -> unit -> t (** Standard logical connectives viewed as terms. [implies_t] is usual right implication, i.e [apply implies_t \[p; q\] ] is "p implies q", while [apply implied_t \[p; q \]] means "p is implied by q" or @@ -163,6 +166,9 @@ module type Logic = sig are n-ary instead of binary mostly because they are in smtlib (and that is subsumes the binary case). *) + val tuple : ?loc:location -> t list -> t + (** Create a tuple of terms. *) + val apply : ?loc:location -> t -> t list -> t (** Application constructor, seen as higher order application rather than first-order application for the following reasons: diff --git a/src/languages/dune.common b/src/languages/dune.common index 6a2cec176..e7e8ceac2 100644 --- a/src/languages/dune.common +++ b/src/languages/dune.common @@ -12,7 +12,7 @@ ) (menhir - (flags (--explain --exn-carries-state --external-tokens Tokens)) + (flags (--explain --strict --exn-carries-state --external-tokens Tokens)) (modules tokens parser) (merge_into parser) ) @@ -23,7 +23,7 @@ (:parser parser.mly) (:msg syntax.messages)) (action (with-stdout-to %{target} - (run menhir --external-tokens Tokens %{tokens} + (run menhir --external-tokens Tokens %{tokens} --strict %{parser} --base %{parser} --compile-errors %{msg}))) ) @@ -34,7 +34,7 @@ (deps (:tokens tokens.mly) (:parser parser.mly)) (action (with-stdout-to %{target} - (run menhir --external-tokens Tokens %{tokens} + (run menhir --external-tokens Tokens %{tokens} --strict %{parser} --base %{parser} --list-errors))) ) @@ -44,7 +44,7 @@ (:parser parser.mly) (:msg syntax.messages)) (action (with-stdout-to %{target} - (run menhir --external-tokens Tokens %{tokens} + (run menhir --external-tokens Tokens %{tokens} --strict %{parser} --base %{parser} --update-errors %{msg}))) ) @@ -56,7 +56,7 @@ (:updated updated.messages) ) (action (with-stdout-to %{target} - (run menhir --external-tokens Tokens %{tokens} + (run menhir --external-tokens Tokens %{tokens} --strict %{parser} --base %{parser} --merge-errors %{new} --merge-errors %{updated}))) ) diff --git a/src/languages/tptp/dolmen_tptp.ml b/src/languages/tptp/dolmen_tptp.ml index 1f0629312..aeb53f16b 100644 --- a/src/languages/tptp/dolmen_tptp.ml +++ b/src/languages/tptp/dolmen_tptp.ml @@ -4,11 +4,13 @@ type version = [ | `Latest | `V6_3_0 + | `V8_2_0 ] (* Alias the sub-libraries *) module V6_3_0 = Dolmen_tptp_v6_3_0 +module V8_2_0 = Dolmen_tptp_v8_2_0 (* Alias for the latest module *) -module Latest = V6_3_0 +module Latest = V8_2_0 diff --git a/src/languages/tptp/dune b/src/languages/tptp/dune index 529e683fb..2567ec621 100644 --- a/src/languages/tptp/dune +++ b/src/languages/tptp/dune @@ -2,6 +2,6 @@ (library (name dolmen_tptp) (public_name dolmen.tptp) - (libraries dolmen_tptp_v6_3_0) + (libraries dolmen_tptp_v6_3_0 dolmen_tptp_v8_2_0) (modules Dolmen_tptp) ) diff --git a/src/languages/tptp/v6.3.0/ast.ml b/src/languages/tptp/v6.3.0/ast.ml index 55ca8bffe..63954ce92 100644 --- a/src/languages/tptp/v6.3.0/ast.ml +++ b/src/languages/tptp/v6.3.0/ast.ml @@ -16,6 +16,9 @@ module type Id = sig (** Names used to refer to tptp phrases. These are used in declarations and include statement. *) + val attr : namespace + (** Namespace for attributes, such as formula roles. *) + val mk : namespace -> string -> t (** Make an identifier *) @@ -135,11 +138,11 @@ module type Statement = sig (** Include directive. Given the filename, and a list of names to import (an empty list means import everything). *) - val tpi : ?loc:location -> ?annot:term -> id -> string -> term -> t - val thf : ?loc:location -> ?annot:term -> id -> string -> term -> t - val tff : ?loc:location -> ?annot:term -> id -> string -> term -> t - val fof : ?loc:location -> ?annot:term -> id -> string -> term -> t - val cnf : ?loc:location -> ?annot:term -> id -> string -> term -> t + val tpi : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val thf : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val tff : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val fof : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val cnf : ?loc:location -> ?annot:term -> id -> role:term -> term -> t (** TPTP statements, used for instance as [tff ~loc ~annot name role t]. Instructs the prover to register a new directive with the given name, role and term. Current tptp roles are: diff --git a/src/languages/tptp/v6.3.0/parser.mly b/src/languages/tptp/v6.3.0/parser.mly index 2ba780a99..10633996a 100644 --- a/src/languages/tptp/v6.3.0/parser.mly +++ b/src/languages/tptp/v6.3.0/parser.mly @@ -44,27 +44,32 @@ annotated_formula: tpi_annotated: | TPI LEFT_PAREN s=name COMMA r=formula_role COMMA f=tpi_formula annot=annotations RIGHT_PAREN DOT - { let loc = L.mk_pos $startpos $endpos in S.tpi ~loc ?annot s r f } + { let role = let loc = L.mk_pos $startpos(r) $endpos(r) in T.const ~loc (I.mk I.attr r) in + let loc = L.mk_pos $startpos $endpos in S.tpi ~loc ?annot s ~role f } thf_annotated: | THF LEFT_PAREN s=name COMMA r=formula_role COMMA f=thf_formula annot=annotations RIGHT_PAREN DOT - { let loc = L.mk_pos $startpos $endpos in S.thf ~loc ?annot s r f } + { let role = let loc = L.mk_pos $startpos(r) $endpos(r) in T.const ~loc (I.mk I.attr r) in + let loc = L.mk_pos $startpos $endpos in S.thf ~loc ?annot s ~role f } tff_annotated: | TFF LEFT_PAREN s=name COMMA r=formula_role COMMA f=tff_formula annot=annotations RIGHT_PAREN DOT - { let loc = L.mk_pos $startpos $endpos in S.tff ~loc ?annot s r f } + { let role = let loc = L.mk_pos $startpos(r) $endpos(r) in T.const ~loc (I.mk I.attr r) in + let loc = L.mk_pos $startpos $endpos in S.tff ~loc ?annot s ~role f } fof_annotated: | FOF LEFT_PAREN s=name COMMA r=formula_role COMMA f=fof_formula annot=annotations RIGHT_PAREN DOT - { let loc = L.mk_pos $startpos $endpos in S.fof ~loc ?annot s r f } + { let role = let loc = L.mk_pos $startpos(r) $endpos(r) in T.const ~loc (I.mk I.attr r) in + let loc = L.mk_pos $startpos $endpos in S.fof ~loc ?annot s ~role f } cnf_annotated: | CNF LEFT_PAREN s=name COMMA r=formula_role COMMA f=cnf_formula annot=annotations RIGHT_PAREN DOT - { let loc = L.mk_pos $startpos $endpos in S.cnf ~loc ?annot s r f } + { let role = let loc = L.mk_pos $startpos(r) $endpos(r) in T.const ~loc (I.mk I.attr r) in + let loc = L.mk_pos $startpos $endpos in S.cnf ~loc ?annot s ~role f } annotations: | COMMA s=source i=optional_info diff --git a/src/languages/tptp/v8.2.0/ast.ml b/src/languages/tptp/v8.2.0/ast.ml new file mode 100644 index 000000000..53c961b5a --- /dev/null +++ b/src/languages/tptp/v8.2.0/ast.ml @@ -0,0 +1,174 @@ + +(* This file is free software, part of dolmen. See file "LICENSE" for more information *) + +module type Id = sig + + type t + (** The type of identifiers *) + + type namespace + (** The type for namespaces. *) + + val term : namespace + (** Usual namespace, used for temrs, types and propositions. *) + + val decl : namespace + (** Names used to refer to tptp phrases. These are used + in declarations and include statement. *) + + val attr : namespace + (** Namespace for attributes, such as formula roles. *) + + val mk : namespace -> string -> t + (** Make an identifier *) + +end + +module type Term = sig + + type t + (** The type of terms. *) + + type id + (** The type of identifiers *) + + type location + (** The type of locations attached to terms. *) + + val eq_t : ?loc:location -> unit -> t + val neq_t : ?loc:location -> unit -> t + val not_t : ?loc:location -> unit -> t + val or_t : ?loc:location -> unit -> t + val and_t : ?loc:location -> unit -> t + val xor_t : ?loc:location -> unit -> t + val nor_t : ?loc:location -> unit -> t + val nand_t : ?loc:location -> unit -> t + val equiv_t : ?loc:location -> unit -> t + val implies_t : ?loc:location -> unit -> t + val implied_t : ?loc:location -> unit -> t + val pi_t : ?loc:location -> unit -> t + val sigma_t : ?loc:location -> unit -> t + val subtype_t : ?loc:location -> unit -> t + val data_t : ?loc:location -> unit -> t + val choice_t : ?loc:location -> unit -> t + val description_t : ?loc:location -> unit -> t + (** Predefined symbols in tptp. Symbols as standalone terms are necessary + for parsing tptp's THF. {!implied_t} is reverse implication, and + {!data_t} is used in tptp's annotations. {!pi_t} and {!sigma_t} are + the encoding of forall and exists quantifiers as constant in higher-order + logic. *) + + val colon : ?loc:location -> t -> t -> t + (** Juxtaposition of terms, usually used for annotating terms with their type. *) + + val var : ?loc:location -> id -> t + (** Make a variable (in tptp, variable are syntaxically different from constants). *) + + val const : ?loc:location -> id -> t + (** Make a constant. *) + + val distinct : ?loc:location -> id -> t + (** Make a constant whose name possibly contain special characters + (All 'distinct' constants name are enclosed in quotes). *) + + val int : ?loc:location -> string -> t + val rat : ?loc:location -> string -> t + val real : ?loc:location -> string -> t + (** Constants that are syntaxically recognised as numbers. *) + + val apply : ?loc:location -> t -> t list -> t + (** Application. *) + + val tuple : ?loc:location -> t list -> t + (** Tuple of terms. *) + + val union : ?loc:location -> t -> t -> t + (** Union of types. *) + + val product : ?loc:location -> t -> t -> t + (** Product of types, used for function types with more than one argument. *) + + val arrow : ?loc:location -> t -> t -> t + (** Function type constructor. *) + + val subtype : ?loc:location -> t -> t -> t + (** Comparison of type (used in tptp's THF). *) + + val pi : ?loc:location -> t list -> t -> t + (** Dependant type constructor, used for polymorphic function types. *) + + val letin : ?loc:location -> t list -> t -> t + (** Local binding for terms. *) + + val forall : ?loc:location -> t list -> t -> t + (** Universal propositional quantification. *) + + val exists : ?loc:location -> t list -> t -> t + (** Existencial porpositional quantification. *) + + val lambda : ?loc:location -> t list -> t -> t + (** Function construction. *) + + val choice : ?loc:location -> t list -> t -> t + (** Indefinite description, also called choice operator. *) + + val description : ?loc:location -> t list -> t -> t + (** Definite description. *) + + val sequent : ?loc:location -> t list -> t list -> t + (** Sequents as terms, used as [sequents hyps goals]. *) + +end + +module type Statement = sig + + type t + (** The type of statements. *) + + type id + (** The type of identifiers *) + + type term + (** The type of terms used in statements. *) + + type location + (** The type of locations attached to statements. *) + + val annot : ?loc:location -> term -> term list -> term + (** Terms as annotations for statements. *) + + val include_ : ?loc:location -> string -> id list -> t + (** Include directive. Given the filename, and a list of + names to import (an empty list means import everything). *) + + val tpi : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val thf : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val tff : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val tcf : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val fof : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + val cnf : ?loc:location -> ?annot:term -> id -> role:term -> term -> t + (** TPTP statements, used for instance as [tff ~loc ~annot name role t]. + Instructs the prover to register a new directive with the given name, + role and term. Current tptp roles are: + - ["axiom", "hypothesis", "definition", "lemma", "theorem"] acts + as new assertions/declartions + - ["assumption", "conjecture"] are proposition that need to be proved, + and then can be used to prove other propositions. They are equivalent + to the following sequence of smtlib statements: + {ul + {- [push 1]} + {- [assert (not t)]} + {- [check_sat]} + {- [pop 1]} + {- [assert t]} + } + - ["negated_conjecture"] is the same as ["conjecture"], but the given proposition + is false (i.e its negation is the proposition to prove). + - ["type"] declares a new symbol and its type + - ["plain", "unknown", "fi_domain", "fi_functors", "fi_predicates"] are valid + roles with no specified semantics + - any other role is an error + *) + +end + diff --git a/src/languages/tptp/v8.2.0/dolmen_tptp_v8_2_0.ml b/src/languages/tptp/v8.2.0/dolmen_tptp_v8_2_0.ml new file mode 100644 index 000000000..17a9ca4fe --- /dev/null +++ b/src/languages/tptp/v8.2.0/dolmen_tptp_v8_2_0.ml @@ -0,0 +1,20 @@ + +(* This file is free software, part of dolmen. See file "LICENSE" formore information *) + +module type Id = Ast.Id +module type Term = Ast.Term +module type Statement = Ast.Statement + +module Make + (L : Dolmen_intf.Location.S) + (I : Id) + (T : Term with type location := L.t and type id := I.t) + (S : Statement with type location := L.t and type id := I.t and type term := T.t) = + Dolmen_std.Transformer.Make(L)(struct + type token = Tokens.token + type statement = S.t + let env = ["TPTP"] + let incremental = true + let error s = Syntax_messages.message s + end)(Lexer)(Parser.Make(L)(I)(T)(S)) + diff --git a/src/languages/tptp/v8.2.0/dolmen_tptp_v8_2_0.mli b/src/languages/tptp/v8.2.0/dolmen_tptp_v8_2_0.mli new file mode 100644 index 000000000..fb25cdb32 --- /dev/null +++ b/src/languages/tptp/v8.2.0/dolmen_tptp_v8_2_0.mli @@ -0,0 +1,18 @@ + +(* This file is free software, part of dolmen. See file "LICENSE" formore information *) + +(** TPTP language input *) + +module type Id = Ast.Id +module type Term = Ast.Term +module type Statement = Ast.Statement +(** Implementation requirement for the TPTP format. *) + +module Make + (L : Dolmen_intf.Location.S) + (I : Id) + (T : Term with type location := L.t and type id := I.t) + (S : Statement with type location := L.t and type id := I.t and type term := T.t) : + Dolmen_intf.Language.S with type statement = S.t and type file := L.file +(** Functor to generate a parser for the TPTP format. *) + diff --git a/src/languages/tptp/v8.2.0/dune b/src/languages/tptp/v8.2.0/dune new file mode 100644 index 000000000..24ae20413 --- /dev/null +++ b/src/languages/tptp/v8.2.0/dune @@ -0,0 +1,20 @@ + +; Language library definition +(library + (name dolmen_tptp_v8_2_0) + (public_name dolmen.tptp.v8_2_0) + (instrumentation (backend bisect_ppx)) + (libraries dolmen_std dolmen_intf menhirLib) + (modules Dolmen_tptp_v8_2_0 Tokens Lexer Parser Ast Syntax_messages) + ; The tptp parser generated by merlin is **big**, and in particular, contains + ; a set of mutually recursive functions that takes about ~30k loc. Flambda + ; exhibits a quadratic behaviour when trying to compute the invariants + ; parameters of such a definition, which makes it take about ~15minutes to + ; compile parser.ml + ; Therefore, we compile this library with -Oclassic to keep a reasonable + ; compilation time + (ocamlopt_flags ((:standard -Oclassic) \ (-O3))) +) + +; Common include +(include ../../dune.common) diff --git a/src/languages/tptp/v8.2.0/lexer.mll b/src/languages/tptp/v8.2.0/lexer.mll new file mode 100644 index 000000000..78589ae18 --- /dev/null +++ b/src/languages/tptp/v8.2.0/lexer.mll @@ -0,0 +1,258 @@ +(* +Copyright (c) 2013, Simon Cruanes +Copyright (c) 2016, Guillaume Bury +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +Redistributions of source code must retain the above copyright notice, this +list of conditions and the following disclaimer. Redistributions in binary +form must reproduce the above copyright notice, this list of conditions and the +following disclaimer in the documentation and/or other materials provided with +the distribution. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*) + +(** {1 TPTP Lexer} *) + +{ + exception Error + + open Tokens + + module T = Dolmen_std.Tok + + let reserved s = + T.descr s + ~kind:"reserved word" + ~hint:"reserved words cannot be used as identifiers" + + let descr t : T.descr = + match (t: token) with + | EOF -> T.descr ~kind:"end of file token" "" + | DASH -> reserved "-" + | DOT -> reserved "." + | COMMA -> reserved "," + | COLON -> reserved ":" + | LEFT_PAREN -> reserved "(" + | RIGHT_PAREN -> reserved ")" + | LEFT_BRACKET -> reserved "[" + | RIGHT_BRACKET -> reserved "]" + | LEFT_CURLY -> reserved "{" + | RIGHT_CURLY -> reserved "-" + | CNF -> reserved "cnf" + | FOF -> reserved "fof" + | TFF -> reserved "tff" + | TCF -> reserved "tcf" + | THF -> reserved "thf" + | TPI -> reserved "tpi" + | INCLUDE -> reserved "include" + | LAMBDA -> reserved "^" + | APPLY -> reserved "@" + | DEFINITE_DESCRIPTION_OP -> reserved "@-" + | INDEFINITE_DESCRIPTION_OP -> reserved "@+" + | DEFINITE_DESCRIPTION_TERM -> reserved "@@-" + | INDEFINITE_DESCRIPTION_TERM -> reserved "@@+" + | EQUAL_TERM -> reserved "@=" + | FORALL_TY -> reserved "!>" + | FORALL -> reserved "!" + | EXISTS_TY -> reserved "?*" + | EXISTS -> reserved "?" + + | PI -> reserved "!!" + | SIGMA -> reserved "??" + + | LESS -> reserved "<" + | ARROW -> reserved ">" + | SUBTYPE -> reserved "<<" + + | HASH -> reserved "#" + + | STAR -> reserved "*" + | PLUS -> reserved "+" + + | XOR -> reserved "<~>" + | EQUIV -> reserved "<=>" + | IMPLY -> reserved "=>" + | LEFT_IMPLY -> reserved "<=" + + | NOT -> reserved "~" + | AND -> reserved "&" + | VLINE -> reserved "|" + | NOTAND -> reserved "~&" + | NOTVLINE -> reserved "~|" + + | EQUAL -> reserved "=" + | NOT_EQUAL -> reserved "!=" + | ASSIGNMENT -> reserved ":=" + | IDENTICAL -> reserved "==" + | GENTZEN_ARROW -> reserved "-->" + + | LET -> reserved "$let" + + | DOLLAR_THF -> reserved "$thf" + | DOLLAR_TFF -> reserved "$tff" + | DOLLAR_FOF -> reserved "$fof" + | DOLLAR_CNF -> reserved "$cnf" + | DOLLAR_FOT -> reserved "$fot" + + | LOWER_WORD s -> T.descr ~kind:"lower word" s + | UPPER_WORD s -> T.descr ~kind:"upper_word" s + | SINGLE_QUOTED s -> T.descr ~kind:"single-quoted word" s + | DISTINCT_OBJECT s -> T.descr ~kind:"distinct object" s + | DOLLAR_WORD s -> T.descr ~kind:"dollar word" s + | DOLLAR_DOLLAR_WORD s -> T.descr ~kind:"double dollar word" s + | REAL s -> T.descr ~kind:"real literal" s + | RATIONAL s -> T.descr ~kind:"rational literal" s + | INTEGER s -> T.descr ~kind:"integer literal" s + +} + +let printable_char = [^ '\n'] +let not_star_slash = ([^ '*']* '*'+ [^ '/' '*'])* [^ '*']* +let comment_line = ['%' '#'] printable_char* +let comment_block = '/' '*' not_star_slash '*' '/' +let comment = comment_line | comment_block + +let sq_char = [^ '\\' '''] | "\\\\" | "\\'" +let do_char = [^ '"' '\\' ] | "\\\\" | "\\\"" +let single_quoted = ''' sq_char+ ''' +let distinct_object = '"' do_char* '"' + +let zero_numeric = '0' +let non_zero_numeric = ['1' - '9'] +let numeric = ['0' - '9'] +let sign = ['+' '-'] + +let dot_decimal = '.' numeric + +let positive_decimal = non_zero_numeric numeric* +let decimal = zero_numeric | positive_decimal +let unsigned_integer = decimal +let signed_integer = sign unsigned_integer +let integer = signed_integer | unsigned_integer +let decimal_fraction = decimal dot_decimal +let decimal_exponent = (decimal | decimal_fraction) ['e' 'E'] integer +let unsigned_real = decimal_fraction | decimal_exponent +let signed_real = sign unsigned_real +let real = signed_real | unsigned_real +let unsigned_rational = decimal '/' positive_decimal +let signed_rational = sign unsigned_rational +let rational = signed_rational | unsigned_rational + +let lower_alpha = ['a' - 'z'] +let upper_alpha = ['A' - 'Z'] +let alpha_numeric = lower_alpha | upper_alpha | numeric | '_' + +let upper_word = upper_alpha alpha_numeric* +let lower_word = lower_alpha alpha_numeric* +let dollar_word = '$' lower_word +let dollar_dollar_word = "$$" lower_word + +rule token newline = parse + | comment + { String.iter (function + | '\n' -> newline lexbuf + | _ -> () + ) (Lexing.lexeme lexbuf); + token newline lexbuf } + + | '\n' { newline lexbuf; token newline lexbuf } + | [' ' '\t' '\r'] { token newline lexbuf } + | eof { EOF } + + | '-' { DASH } + | '.' { DOT } + | ',' { COMMA } + | ':' { COLON } + + | '(' { LEFT_PAREN } + | ')' { RIGHT_PAREN } + | '[' { LEFT_BRACKET } + | ']' { RIGHT_BRACKET } + | '{' { LEFT_CURLY } + | '}' { RIGHT_CURLY } + + | '^' { LAMBDA } + | '@' { APPLY } + | "@+" { INDEFINITE_DESCRIPTION_OP } + | "@@+" { INDEFINITE_DESCRIPTION_TERM } + | "@-" { DEFINITE_DESCRIPTION_OP } + | "@@-" { DEFINITE_DESCRIPTION_TERM } + | "@=" { EQUAL_TERM } + | "!>" { FORALL_TY } + | '!' { FORALL } + | "?*" { EXISTS_TY } + | '?' { EXISTS } + + | "!!" { PI } + | "??" { SIGMA } + + | '<' { LESS } + | '>' { ARROW } + | "<<" { SUBTYPE } + + | '#' { HASH } + + | '*' { STAR } + | '+' { PLUS } + + | "<~>" { XOR } + | "<=>" { EQUIV } + | "=>" { IMPLY } + | "<=" { LEFT_IMPLY } + + | '~' { NOT } + | '&' { AND } + | '|' { VLINE } + | "~&" { NOTAND } + | "~|" { NOTVLINE } + + | '=' { EQUAL } + | "!=" { NOT_EQUAL } + | ":=" { ASSIGNMENT } + | "==" { IDENTICAL } + | "-->" { GENTZEN_ARROW } + + + | lower_word { + match Lexing.lexeme lexbuf with + | "cnf" -> CNF + | "fof" -> FOF + | "tff" -> TFF + | "tcf" -> TCF + | "thf" -> THF + | "tpi" -> TPI + | "include" -> INCLUDE + | s -> LOWER_WORD(s) + } + | dollar_word { + match Lexing.lexeme lexbuf with + | "$cnf" -> DOLLAR_CNF + | "$fof" -> DOLLAR_FOF + | "$tff" -> DOLLAR_TFF + | "$thf" -> DOLLAR_THF + | "$fot" -> DOLLAR_FOT + | "$let" -> LET + | s -> DOLLAR_WORD(s) + } + | upper_word { UPPER_WORD(Lexing.lexeme lexbuf) } + | dollar_dollar_word { DOLLAR_DOLLAR_WORD(Lexing.lexeme lexbuf) } + | single_quoted { SINGLE_QUOTED(Lexing.lexeme lexbuf) } + | distinct_object { DISTINCT_OBJECT(Lexing.lexeme lexbuf) } + | integer { INTEGER(Lexing.lexeme lexbuf) } + | rational { RATIONAL(Lexing.lexeme lexbuf) } + | real { REAL(Lexing.lexeme lexbuf) } + + | _ { raise Error } + diff --git a/src/languages/tptp/v8.2.0/parser.mly b/src/languages/tptp/v8.2.0/parser.mly new file mode 100644 index 000000000..0d42fb724 --- /dev/null +++ b/src/languages/tptp/v8.2.0/parser.mly @@ -0,0 +1,1276 @@ + +(* This file is free software, part of dolmem. See file "LICENSE" for more information *) + +%parameter +%parameter +%parameter +%parameter + +%start file +%start input + +%{ + + let pp_num_list fmt (l, singular, plural) = + let n = List.length l in + Format.fprintf fmt "%d %s" n (if n = 1 then singular else plural) + + let mismatched_lists ~loc l1 l2 = + let msg = Format.dprintf + "@[@[Expected@ two@ lists@ of@ the@ same@ size,@ but@ got:@]@ \ + - @[%a@]@ - @[%a@]@]" + pp_num_list l1 pp_num_list l2 + in + raise (L.Syntax_error (loc, `Regular msg)) + +%} + +%% + +/* Hand-written following syntax.bnf */ + +/* Complete file, i.e Top-level declarations */ + +file: + | l=tptp_input* EOF { l } + +input: + | i=tptp_input + { Some i } + | EOF + { None } + +tptp_input: + | i=annotated_formula + | i=include_ + { i } + +/* ******************** */ +/* Top-level statements */ + +annotated_formula: + | f=thf_annotated + | f=tff_annotated + | f=tcf_annotated + | f=fof_annotated + | f=cnf_annotated + | f=tpi_annotated + { f } + +tpi_annotated: + | TPI LEFT_PAREN s=name COMMA role=formula_role COMMA + f=tpi_formula annot=annotations RIGHT_PAREN DOT + { let loc = L.mk_pos $startpos $endpos in S.tpi ~loc ?annot s ~role f } + +thf_annotated: + | THF LEFT_PAREN s=name COMMA role=formula_role COMMA + f=thf_formula annot=annotations RIGHT_PAREN DOT + { let loc = L.mk_pos $startpos $endpos in S.thf ~loc ?annot s ~role f } + +tff_annotated: + | TFF LEFT_PAREN s=name COMMA role=formula_role COMMA + f=tff_formula annot=annotations RIGHT_PAREN DOT + { let loc = L.mk_pos $startpos $endpos in S.tff ~loc ?annot s ~role f } + +tcf_annotated: + | TCF LEFT_PAREN s=name COMMA role=formula_role COMMA + f=tcf_formula annot=annotations RIGHT_PAREN DOT + { let loc = L.mk_pos $startpos $endpos in S.tcf ~loc ?annot s ~role f } + +fof_annotated: + | FOF LEFT_PAREN s=name COMMA role=formula_role COMMA + f=fof_formula annot=annotations RIGHT_PAREN DOT + { let loc = L.mk_pos $startpos $endpos in S.fof ~loc ?annot s ~role f } + +cnf_annotated: + | CNF LEFT_PAREN s=name COMMA role=formula_role COMMA + f=cnf_formula annot=annotations RIGHT_PAREN DOT + { let loc = L.mk_pos $startpos $endpos in S.cnf ~loc ?annot s ~role f } + +annotations: + | COMMA s=source i=optional_info + { let loc = L.mk_pos $startpos $endpos in Some (S.annot ~loc s i) } + | { None } + +tpi_formula: + | f=fof_formula { f } + +formula_role: + | s=LOWER_WORD + { let loc = L.mk_pos $startpos $endpos in + let id = I.mk I.attr s in + T.const ~loc id } + | s=LOWER_WORD DASH g=general_term + { let t = + let loc = L.mk_pos $startpos(s) $endpos(s) in + let id = I.mk I.attr s in + T.const ~loc id + in + let loc = L.mk_pos $startpos $endpos in + T.colon ~loc t g + } + + +/* ************ */ +/* THF formulas */ + +thf_formula: + | f=thf_logic_formula + | f=thf_atom_typing + | f=thf_subtype + { f } + +thf_logic_formula: + | f=thf_unitary_formula + | f=thf_unary_formula + | f=thf_binary_formula + | f=thf_defined_infix + | f=thf_definition + | f=thf_sequent + { f } + +thf_binary_formula: + | f=thf_binary_nonassoc + | f=thf_binary_assoc + | f=thf_binary_type + { f } + +thf_binary_nonassoc: + | f=thf_unit_formula c=nonassoc_connective g=thf_unit_formula + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc c [f; g] } + +thf_binary_assoc: + | f=thf_or_formula + | f=thf_and_formula + | f=thf_apply_formula + { f } + +thf_or_formula: + | f=thf_unit_formula VLINE g=thf_unit_formula + | f=thf_or_formula VLINE g=thf_unit_formula + { let op = let loc = L.mk_pos $startpos($2) $endpos($2) in T.or_t ~loc () in + let loc = L.mk_pos $startpos $endpos in T.apply ~loc op [f; g] } + +thf_and_formula: + | f=thf_unit_formula AND g=thf_unit_formula + | f=thf_and_formula AND g=thf_unit_formula + { let op = let loc = L.mk_pos $startpos($2) $endpos($2) in T.and_t ~loc () in + let loc = L.mk_pos $startpos $endpos in T.apply ~loc op [f; g] } + +thf_apply_formula: + | f=thf_unit_formula APPLY g=thf_unit_formula + | f=thf_apply_formula APPLY g=thf_unit_formula + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f [g] } + +thf_unit_formula: + /* we use an explicit precedence here to solve a shift/reduce conflict, see tokens.mly */ + | f=thf_unitary_formula %prec quantifier_prec + | f=thf_unary_formula + | f=thf_defined_infix + { f } + +thf_preunit_formula: + | f=thf_unitary_formula + | f=thf_prefix_unary + { f } + +thf_unitary_formula: + | f=variable + | f=thf_quantified_formula + | f=thf_atomic_formula + | LEFT_PAREN f=thf_logic_formula RIGHT_PAREN + { f } + +thf_quantified_formula: + | quant=thf_quantification f=thf_unit_formula + { let loc = Some (L.mk_pos $startpos $endpos) in + let q, l = quant in + q ?loc l f } + +thf_quantification: + | q=thf_quantifier LEFT_BRACKET l=thf_variable_list RIGHT_BRACKET COLON + { q, l } + +thf_variable_list: + | v=thf_typed_variable + { [ v ] } + | v=thf_typed_variable COMMA l=thf_variable_list + { v :: l } + +thf_typed_variable: + | c=variable COLON ty=thf_top_level_type + { let loc = L.mk_pos $startpos $endpos in T.colon ~loc c ty } + +thf_unary_formula: + | f=thf_prefix_unary + | f=thf_infix_unary + { f } + +thf_prefix_unary: + | c=thf_unary_connective f=thf_preunit_formula + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc c [f] } + +thf_infix_unary: + | LEFT_PAREN f=thf_unitary_term s=infix_inequality g=thf_unitary_term RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc s [f; g] } + +thf_atomic_formula: + | f=thf_plain_atomic + | f=thf_defined_atomic + | f=thf_system_atomic + | f=thf_fof_function + { f } + +thf_plain_atomic: + | f=constant + | f=thf_tuple + { f } + +thf_defined_atomic: + | f=defined_constant + | f=thf_defined_term + | f=nhf_long_connective + | f=thf_let + | LEFT_PAREN f=thf_conn_term RIGHT_PAREN + { f } + +thf_defined_term: + | f=defined_term + | f=th1_defined_term + { f } + +thf_defined_infix: + | f=thf_unitary_formula c=defined_infix_pred g=thf_unitary_formula + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc c [f; g] } + +thf_system_atomic: + | f=system_constant + { f } + +thf_let: + | LET LEFT_PAREN tys=thf_let_types COMMA defs=thf_let_defns COMMA f=thf_logic_formula RIGHT_PAREN + { let bound = + let loc = L.mk_pos $startpos(tys) $endpos(defs) in + try List.map2 (fun var ty -> T.colon ~loc var ty) defs tys + with Invalid_argument _ -> + mismatched_lists ~loc + (defs, "bound variable", "bound variables") + (tys, "type", "types") + in + let loc = L.mk_pos $startpos $endpos in + T.letin ~loc bound f + } + +thf_let_types: + | t=thf_atom_typing + { [t] } + | LEFT_BRACKET l=thf_atom_typing_list RIGHT_BRACKET + { l } + +thf_atom_typing_list: + | t=thf_atom_typing + { [t] } + | t=thf_atom_typing COMMA l=thf_atom_typing_list + { t :: l } + +thf_let_defns: + | t=thf_let_defn + { [t] } + | LEFT_BRACKET l=thf_let_defn_list RIGHT_BRACKET + { l } + +thf_let_defn: + | x=thf_logic_formula a=assignment t=thf_logic_formula + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc a [x; t] } + +thf_let_defn_list: + | t=thf_let_defn + { [t] } + | t=thf_let_defn COMMA l=thf_let_defn_list + { t :: l } + +thf_unitary_term: + | f=thf_atomic_formula + | f=variable + | LEFT_PAREN f=thf_logic_formula RIGHT_PAREN + { f } + +thf_conn_term: + | c=nonassoc_connective + | c=assoc_connective + | c=infix_equality + | c=infix_inequality + | c=thf_unary_connective + { c } + +thf_tuple: + | LEFT_BRACKET RIGHT_BRACKET + { let loc = L.mk_pos $startpos $endpos in T.tuple ~loc [] } + | LEFT_BRACKET l=thf_formula_list RIGHT_BRACKET + { let loc = L.mk_pos $startpos $endpos in T.tuple ~loc l } + +thf_fof_function: + | f=_functor LEFT_PAREN l=thf_arguments RIGHT_PAREN + | f=defined_functor LEFT_PAREN l=thf_arguments RIGHT_PAREN + | f=system_functor LEFT_PAREN l=thf_arguments RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f l } + +thf_arguments: + | l=thf_formula_list + { l } + +thf_formula_list: + | f=thf_logic_formula + { [f] } + | f=thf_logic_formula COMMA l=thf_formula_list + { f :: l } + +thf_atom_typing: + | t=untyped_atom COLON ty=thf_top_level_type + { let loc = L.mk_pos $startpos $endpos in T.colon ~loc t ty } + | LEFT_PAREN t=thf_atom_typing RIGHT_PAREN + { t } + +thf_top_level_type: + | t=thf_unitary_type + | t=thf_mapping_type + | t=thf_apply_type + { t } + +thf_unitary_type: + | f=thf_unitary_formula + { f } + +thf_apply_type: + | t=thf_apply_formula + { t } + +thf_binary_type: + | t=thf_mapping_type + | t=thf_xprod_type + | t=thf_union_type + { t } + +thf_mapping_type: + | a=thf_unitary_type ARROW b=thf_unitary_type + | a=thf_unitary_type ARROW b=thf_mapping_type + { let loc = L.mk_pos $startpos $endpos in T.arrow ~loc a b } + +thf_xprod_type: + | a=thf_unitary_type STAR b=thf_unitary_type + | a=thf_xprod_type STAR b=thf_unitary_type + { let loc = L.mk_pos $startpos $endpos in T.product ~loc a b } + +thf_union_type: + | a=thf_unitary_type PLUS b=thf_unitary_type + | a=thf_union_type PLUS b=thf_unitary_type + { let loc = L.mk_pos $startpos $endpos in T.union ~loc a b } + +thf_subtype: + | a=untyped_atom subtype_sign b=atom + { let loc = L.mk_pos $startpos $endpos in T.subtype ~loc a b } + +thf_definition: + | x=thf_atomic_formula eq=identical e=thf_logic_formula + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc eq [x; e] } + +thf_sequent: + | hyp=thf_tuple gentzen_arrow goal=thf_tuple + { let loc = L.mk_pos $startpos $endpos in T.sequent ~loc [hyp] [goal] } + + +/* *********** */ +/* TFF formula */ + +tff_formula: + | f=tff_logic_formula + | f=tff_atom_typing + | f=tff_subtype + { f } + +tff_logic_formula: + | f=tff_unitary_formula + | f=tff_unary_formula + | f=tff_binary_formula + | f=tff_defined_infix + | f=txf_definition + | f=txf_sequent + { f } + +tff_binary_formula: + | f=tff_binary_nonassoc + | f=tff_binary_assoc + { f } + +tff_binary_nonassoc: + | f=tff_unit_formula c=nonassoc_connective g=tff_unit_formula + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc c [f; g] } + +tff_binary_assoc: + | f=tff_or_formula + | f=tff_and_formula + { f } + +tff_or_formula: + | f=tff_unit_formula VLINE g=tff_unit_formula + | f=tff_or_formula VLINE g=tff_unit_formula + { let op = let loc = L.mk_pos $startpos($2) $endpos($2) in T.or_t ~loc () in + let loc = L.mk_pos $startpos $endpos in T.apply ~loc op [f; g] } + +tff_and_formula: + | f=tff_unit_formula AND g=tff_unit_formula + | f=tff_and_formula AND g=tff_unit_formula + { let op = let loc = L.mk_pos $startpos($2) $endpos($2) in T.and_t ~loc () in + let loc = L.mk_pos $startpos $endpos in T.apply ~loc op [f; g] } + +tff_unit_formula: + | f=tff_unitary_formula + | f=tff_unary_formula + | f=tff_defined_infix + { f } + +tff_preunit_formula: + | f=tff_unitary_formula + | f=tff_prefix_unary + { f } + +tff_unitary_formula: + | f=tff_quantified_formula + | f=tff_atomic_formula + | f=txf_unitary_formula + | LEFT_PAREN f=tff_logic_formula RIGHT_PAREN + { f } + +txf_unitary_formula: + | v=variable + { v } + +tff_quantified_formula: + | q=fof_quantifier LEFT_BRACKET l=tff_variable_list RIGHT_BRACKET COLON f=tff_unit_formula + { let loc = Some (L.mk_pos $startpos $endpos) in q ?loc l f } + +tff_variable_list: + | v=tff_variable + { [ v ] } + | v=tff_variable COMMA l=tff_variable_list + { v :: l } + +tff_variable: + | v=tff_typed_variable + | v=variable + { v } + +tff_typed_variable: + | v=variable COLON ty=tff_atomic_type + { let loc = L.mk_pos $startpos $endpos in T.colon ~loc v ty } + +tff_unary_formula: + | f=tff_prefix_unary + | f=tff_infix_unary + { f } + +tff_prefix_unary: + | u=tff_unary_connective f=tff_preunit_formula + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc u [f] } + +tff_infix_unary: + | LEFT_PAREN f=tff_unitary_term e=infix_inequality g=tff_unitary_term RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc e [f; g] } + +tff_atomic_formula: + | f=tff_plain_atomic + | f=tff_defined_atomic + | f=tff_system_atomic + { f } + +tff_plain_atomic: + | c=constant + { c } + | f=_functor LEFT_PAREN l=tff_arguments RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f l } + +tff_defined_atomic: + | t=tff_defined_plain + { t } + +tff_defined_plain: + | c=defined_constant + { c } + | f=defined_functor LEFT_PAREN l=tff_arguments RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f l } + | f=nxf_atom + | f=txf_let + { f } + +tff_defined_infix: + | LEFT_PAREN f=tff_unitary_term p=defined_infix_pred g=tff_unitary_term RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc p [f; g] } + +tff_system_atomic: + | c=system_constant + { c } + | f=system_functor LEFT_PAREN l=tff_arguments RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f l } + +txf_let: + | LET LEFT_PAREN tys=txf_let_types COMMA defs=txf_let_defns COMMA body=tff_term RIGHT_PAREN + { let bound = + let loc = L.mk_pos $startpos(tys) $endpos(defs) in + try List.map2 (fun var ty -> T.colon ~loc var ty) defs tys + with Invalid_argument _ -> + mismatched_lists ~loc + (defs, "bound variable", "bound variables") + (tys, "type", "types") + in + let loc = L.mk_pos $startpos $endpos in + T.letin ~loc bound body + } + +txf_let_types: + | t=tff_atom_typing + { [t] } + | RIGHT_BRACKET l=tff_atom_typing_list RIGHT_PAREN + { l } + +tff_atom_typing_list: + | t=tff_atom_typing + { [t] } + | t=tff_atom_typing COMMA l=tff_atom_typing_list + { t :: l } + +txf_let_defns: + | t=txf_let_defn + { [t] } + | LEFT_BRACKET l=txf_let_defn_list RIGHT_BRACKET + { l } + +txf_let_defn: + | x=txf_let_LHS eq=assignment e=tff_term + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc eq [x; e] } + +txf_let_LHS: + | t=tff_plain_atomic + | t=txf_tuple + { t } + +txf_let_defn_list: + | t=txf_let_defn + { [t] } + | t=txf_let_defn COMMA l=txf_let_defn_list + { t :: l } + +nxf_atom: + | c=nxf_long_connective APPLY LEFT_PAREN l=tff_arguments RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc c l } + +tff_term: + | f=tff_logic_formula + | f=defined_term + | f=txf_tuple + { f } + +tff_unitary_term: + | f=tff_atomic_formula + | f=defined_term + | f=txf_tuple + | f=variable + | LEFT_PAREN f=tff_logic_formula RIGHT_PAREN + { f } + +txf_tuple: + | LEFT_BRACKET RIGHT_BRACKET + { let loc = L.mk_pos $startpos $endpos in T.tuple ~loc [] } + | LEFT_BRACKET l=tff_arguments RIGHT_BRACKET + { let loc = L.mk_pos $startpos $endpos in T.tuple ~loc l } + +tff_arguments: + | t=tff_term + { [t] } + | t=tff_term COMMA l=tff_arguments + { t :: l } + +tff_atom_typing: + | t=untyped_atom COLON ty=tff_top_level_type + { let loc = L.mk_pos $startpos $endpos in T.colon ~loc t ty } + +tff_top_level_type: + | t=tff_atomic_type + | t=tff_non_atomic_type + { t } + +tff_non_atomic_type: + | t=tff_mapping_type + | t=tf1_quantified_type + | LEFT_PAREN t=tff_non_atomic_type RIGHT_PAREN + { t } + +tf1_quantified_type: + | FORALL_TY LEFT_BRACKET l=tff_variable_list RIGHT_BRACKET COLON t=tff_monotype + { let loc = L.mk_pos $startpos $endpos in T.forall ~loc l t } + +tff_monotype: + | t=tff_atomic_type + | LEFT_PAREN t=tff_mapping_type RIGHT_PAREN + | t=tf1_quantified_type + { t } + +tff_unitary_type: + | t=tff_atomic_type + | LEFT_PAREN t=tff_xprod_type RIGHT_PAREN + { t } + +tff_atomic_type: + | t=type_constant + | t=defined_type + | t=variable + | LEFT_PAREN t=tff_atomic_type RIGHT_PAREN + | t=txf_tuple_type + { t } + | f=type_functor LEFT_PAREN l=tff_type_arguments RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f l } + +tff_type_arguments: + | t=tff_atomic_type + { [t] } + | t=tff_atomic_type COMMA l=tff_type_arguments + { t :: l } + +tff_mapping_type: + | a=tff_unitary_type ARROW b=tff_atomic_type + { let loc = L.mk_pos $startpos $endpos in T.arrow ~loc a b } + +tff_xprod_type: + | a=tff_unitary_type STAR b=tff_atomic_type + | a=tff_xprod_type STAR b=tff_atomic_type + { let loc = L.mk_pos $startpos $endpos in T.product ~loc a b } + +txf_tuple_type: + | LEFT_BRACKET t=tff_type_list RIGHT_BRACKET + { t } + +tff_type_list: + | t=tff_top_level_type + { t } + | t=tff_top_level_type COMMA l=tff_type_list + { let loc = L.mk_pos $startpos $endpos in T.product ~loc t l } + +tff_subtype: + | a=untyped_atom subtype_sign b=atom + { let loc = L.mk_pos $startpos $endpos in T.subtype ~loc a b } + +txf_definition: + | a=tff_atomic_formula eq=identical b=tff_term + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc eq [a; b] } + +txf_sequent: + | hyp=txf_tuple GENTZEN_ARROW goal=txf_tuple + { let loc = L.mk_pos $startpos $endpos in T.sequent ~loc [hyp] [goal] } + +/* ************ */ +/* NHF formulas */ + +nhf_long_connective: + | LEFT_CURLY c=ntf_connective_name RIGHT_CURLY + { c } + | LEFT_CURLY c=ntf_connective_name LEFT_PAREN l=nhf_parameter_list RIGHT_PAREN RIGHT_CURLY + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc c l } + +nhf_parameter_list: + | t=nhf_parameter + { [t] } + | t=nhf_parameter COMMA l=nhf_parameter_list + { t :: l } + +nhf_parameter: + | t=ntf_index + | t=nhf_key_pair + { t } + +nhf_key_pair: + | t=thf_definition + { t } + +nxf_long_connective: + | LEFT_CURLY c=ntf_connective_name RIGHT_CURLY + { c } + | LEFT_CURLY c=ntf_connective_name LEFT_PAREN l=nxf_parameter_list RIGHT_PAREN RIGHT_CURLY + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc c l } + +nxf_parameter_list: + | t=nxf_parameter + { [t] } + | t=nxf_parameter COMMA l=nxf_parameter_list + { t :: l } + +nxf_parameter: + | t=ntf_index + | t=nxf_key_pair + { t } + +nxf_key_pair: + | t=txf_definition + { t } + +ntf_connective_name: + | c=def_or_sys_constant + { c } + +ntf_index: + | HASH t=tff_unitary_term + { t } + +ntf_short_connective: + /* TODO: make these ast builtins ? requires to find names for these */ + | LEFT_BRACKET DOT RIGHT_BRACKET + { let c = I.mk I.term "[.]" in + let loc = L.mk_pos $startpos $endpos in T.const ~loc c } + | LESS DOT ARROW + { let c = I.mk I.term "<.>" in + let loc = L.mk_pos $startpos $endpos in T.const ~loc c } + | LEFT_CURLY DOT RIGHT_CURLY + { let c = I.mk I.term "{.}" in + let loc = L.mk_pos $startpos $endpos in T.const ~loc c } + | LEFT_PAREN DOT RIGHT_PAREN + { let c = I.mk I.term "(.)" in + let loc = L.mk_pos $startpos $endpos in T.const ~loc c } + + +/* ************ */ +/* TCF formulas */ + +tcf_formula: + | t=tcf_logic_formula + | t=tff_atom_typing + { t } + +tcf_logic_formula: + | t=tcf_quantified_formula + | t=cnf_formula + { t } + +tcf_quantified_formula: + | FORALL LEFT_BRACKET l=tff_variable_list RIGHT_BRACKET COLON t=tcf_logic_formula + { let loc = L.mk_pos $startpos $endpos in T.forall ~loc l t } + + +/* ************ */ +/* FOF formulas */ + +fof_formula: + | f=fof_logic_formula + | f=fof_sequent + { f } + +fof_logic_formula: + | f=fof_binary_formula + | f=fof_unary_formula + | f=fof_unitary_formula + { f } + +fof_binary_formula: + | f=fof_binary_nonassoc + | f=fof_binary_assoc + { f } + +fof_binary_nonassoc: + | f=fof_unit_formula c=nonassoc_connective g=fof_unit_formula + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc c [f; g] } + +fof_binary_assoc: + | f=fof_or_formula + | f=fof_and_formula + { f } + +fof_or_formula: + | f=fof_unit_formula VLINE g=fof_unit_formula + | f=fof_or_formula VLINE g=fof_unit_formula + { let op = let loc = L.mk_pos $startpos($2) $endpos($2) in T.or_t ~loc () in + let loc = L.mk_pos $startpos $endpos in T.apply ~loc op [f; g] } + +fof_and_formula: + | f=fof_unit_formula AND g=fof_unit_formula + | f=fof_and_formula AND g=fof_unit_formula + { let op = let loc = L.mk_pos $startpos($2) $endpos($2) in T.and_t ~loc () in + let loc = L.mk_pos $startpos $endpos in T.apply ~loc op [f; g] } + +fof_unary_formula: + | c=unary_connective f=fof_unit_formula + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc c [f] } + | t=fof_infix_unary + { t } + +fof_infix_unary: + | a=fof_term f=infix_inequality b=fof_term + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f [a; b] } + +fof_unit_formula: + | t=fof_unitary_formula + | t=fof_unary_formula + { t } + +fof_unitary_formula: + | f=fof_quantified_formula + | f=fof_atomic_formula + | LEFT_PAREN f=fof_logic_formula RIGHT_PAREN + { f } + +fof_quantified_formula: + | q=fof_quantifier LEFT_BRACKET l=fof_variable_list RIGHT_BRACKET COLON f=fof_unit_formula + { let loc = Some (L.mk_pos $startpos $endpos) in q ?loc l f } + +fof_variable_list: + | v=variable + { [ v ] } + | v=variable COMMA l=fof_variable_list + { v :: l } + +fof_atomic_formula: + | t=fof_plain_atomic_formula + | t=fof_defined_atomic_formula + | t=fof_system_atomic_formula + { t } + +fof_plain_atomic_formula: + | t=fof_plain_term + { t } + +fof_defined_atomic_formula: + | t=fof_defined_plain_formula + | t=fof_defined_infix_formula + { t } + +fof_defined_plain_formula: + | t=fof_defined_plain_term + { t } + +fof_defined_infix_formula: + | a=fof_term f=defined_infix_pred b=fof_term + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f [a; b] } + +fof_system_atomic_formula: + | t=fof_system_term + { t } + +fof_plain_term: + | c=constant + { c } + | f=_functor LEFT_PAREN l=fof_arguments RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f l } + +fof_defined_term: + | t=defined_term + | t=fof_defined_atomic_term + { t } + +fof_defined_atomic_term: + | t=fof_defined_plain_term + { t } + +fof_defined_plain_term: + | c=defined_constant + { c } + | f=defined_functor LEFT_PAREN l=fof_arguments RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f l } + +fof_system_term: + | c=system_constant + { c } + | f=system_functor LEFT_PAREN l=fof_arguments RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f l } + +fof_arguments: + | t=fof_term + { [t] } + | t=fof_term COMMA l=fof_arguments + { t :: l } + +fof_term: + | t=fof_function_term + { t } + | v=variable + { v } + +fof_function_term: + | t=fof_plain_term + | t=fof_defined_term + | t=fof_system_term + { t } + +fof_sequent: + | hyp=fof_formula_tuple GENTZEN_ARROW goal=fof_formula_tuple + { let loc = L.mk_pos $startpos $endpos in T.sequent ~loc hyp goal } + | LEFT_PAREN t=fof_sequent RIGHT_PAREN + { t } + +fof_formula_tuple: + | LEFT_CURLY RIGHT_CURLY + { [] } + | LEFT_CURLY l=fof_formula_tuple_list RIGHT_CURLY + { l } + +fof_formula_tuple_list: + | f=fof_logic_formula + { [ f ] } + | f=fof_logic_formula COMMA l=fof_formula_tuple_list + { f :: l } + + +/* ************ */ +/* CNF Formulas */ + +cnf_formula: + | f=cnf_disjunction + | LEFT_PAREN f=cnf_formula RIGHT_PAREN + { f } + +cnf_disjunction: + | x=cnf_literal + { x } + | f=cnf_disjunction VLINE x=cnf_literal + { let op = let loc = L.mk_pos $startpos($2) $endpos($2) in T.or_t ~loc () in + let loc = L.mk_pos $startpos $endpos in T.apply ~loc op [f; x] } + +cnf_literal: + | f=fof_atomic_formula + { f } + | NOT f=fof_atomic_formula + | NOT LEFT_PAREN f=fof_atomic_formula RIGHT_PAREN + { let c = let loc = L.mk_pos $startpos($1) $endpos($1) in T.not_t ~loc () in + let loc = L.mk_pos $startpos $endpos in T.apply ~loc c [f] } + | f=fof_infix_unary + { f } + + +/* *********** */ +/* Connectives */ + +%inline thf_quantifier: + | q=fof_quantifier + | q=th0_quantifier + | q=th1_quantifier + { q } + +%inline thf_unary_connective: + | c=unary_connective + | c=ntf_short_connective + { c } + +%inline th1_quantifier: + | FORALL_TY + { T.forall } + | EXISTS_TY + { T.exists } + +%inline th0_quantifier: + | LAMBDA + { T.lambda } + | INDEFINITE_DESCRIPTION_OP + { T.choice } + | DEFINITE_DESCRIPTION_OP + { T.description } + +%inline subtype_sign: + | SUBTYPE + { () } + +%inline tff_unary_connective: + | c=unary_connective + | c=ntf_short_connective + { c } + +%inline fof_quantifier: + | EXISTS + { T.exists } + | FORALL + { T.forall } + +%inline nonassoc_connective: + | EQUIV + { let loc = L.mk_pos $startpos $endpos in T.equiv_t ~loc () } + | IMPLY + { let loc = L.mk_pos $startpos $endpos in T.implies_t ~loc () } + | LEFT_IMPLY + { let loc = L.mk_pos $startpos $endpos in T.implied_t ~loc () } + | XOR + { let loc = L.mk_pos $startpos $endpos in T.xor_t ~loc () } + | NOTVLINE + { let loc = L.mk_pos $startpos $endpos in T.nor_t ~loc () } + | NOTAND + { let loc = L.mk_pos $startpos $endpos in T.nand_t ~loc () } + +%inline assoc_connective: + | VLINE + { let loc = L.mk_pos $startpos $endpos in T.or_t ~loc () } + | AND + { let loc = L.mk_pos $startpos $endpos in T.and_t ~loc () } + +%inline unary_connective: + | NOT + { let loc = L.mk_pos $startpos $endpos in T.not_t ~loc () } + +%inline gentzen_arrow: + | GENTZEN_ARROW + { () } + +%inline assignment: + | ASSIGNMENT + { let loc = L.mk_pos $startpos $endpos in T.eq_t ~loc () } + +%inline identical: + | IDENTICAL + { let loc = L.mk_pos $startpos $endpos in T.neq_t ~loc () } + + +/* ********************* */ +/* Types for THF and TFF */ + +%inline type_constant: + | t=type_functor + { t } + +%inline type_functor: + | a=atomic_word + { a } + +%inline defined_type: + | a=atomic_defined_word + { a } + + +/* ****************** */ +/* Common definitions */ + +%inline atom: + | c=untyped_atom + | c=defined_constant + { c } + +%inline untyped_atom: + | c=constant + | c=system_constant + { c } + +%inline defined_infix_pred: + | f=infix_equality + { f } + +%inline infix_equality: + | EQUAL + { let loc = L.mk_pos $startpos $endpos in T.eq_t ~loc () } + +%inline infix_inequality: + | NOT_EQUAL + { let loc = L.mk_pos $startpos $endpos in T.neq_t ~loc () } + +%inline constant: + | f=_functor + { f } + +%inline _functor: + | a=atomic_word + { a } + +%inline defined_constant: + | f=defined_functor + { f } + +%inline defined_functor: + | a=atomic_defined_word + { a } + +%inline system_constant: + | f=system_functor + { f } + +%inline system_functor: + | a=atomic_system_word + { a } + +%inline def_or_sys_constant: + | c=defined_constant + | c=system_constant + { c } + +%inline th1_defined_term: + | PI + { let loc = L.mk_pos $startpos $endpos in T.pi_t ~loc () } + | SIGMA + { let loc = L.mk_pos $startpos $endpos in T.sigma_t ~loc () } + | DEFINITE_DESCRIPTION_TERM + { let loc = L.mk_pos $startpos $endpos in T.description_t ~loc () } + | INDEFINITE_DESCRIPTION_TERM + { let loc = L.mk_pos $startpos $endpos in T.choice_t ~loc () } + | EQUAL_TERM + { let loc = L.mk_pos $startpos $endpos in T.eq_t ~loc () } + +%inline defined_term: + | t=number + | t=distinct_object + { t } + +%inline variable: + | v=UPPER_WORD + { let loc = L.mk_pos $startpos $endpos in T.var ~loc (I.mk I.term v) } + + +/* *************** */ +/* Formula sources */ + +%inline source: + | t=general_term + { t } + +%inline optional_info: + | COMMA i=useful_info + { i } + | { [] } + +%inline useful_info: + | l=general_list + { l } + + +/* ****************** */ +/* Include directives */ + +include_: + | INCLUDE LEFT_PAREN f=file_name l=include_optionals RIGHT_PAREN DOT + { let loc = L.mk_pos $startpos $endpos in S.include_ ~loc f l } + +include_optionals: + | COMMA l=formula_selection + { l } + /* TODO: figure out the semantics of `space_name` */ + | COMMA l=formula_selection COMMA space_name + { l } + | { [] } + +formula_selection: + | LEFT_BRACKET l=name_list RIGHT_BRACKET + { l } + | STAR + { [] } + +name_list: + | n=name + { [n] } + | n=name COMMA l=name_list + { n :: l } + +%inline space_name: + | n=name + { n } + + +/* **************** */ +/* Non-logical data */ + +general_term: + | d=general_data + { d } + | d=general_data COLON t=general_term + { let loc = L.mk_pos $startpos $endpos in T.colon ~loc d t } + | l=general_list + { let f = let loc = L.mk_pos $startpos $endpos in T.data_t ~loc () in + let loc = L.mk_pos $startpos $endpos in T.apply ~loc f l } + +general_data: + | d=atomic_word + | d=general_function + | d=variable + | d=number + | d=distinct_object + | d=formula_data + { d } + +general_function: + | f=atomic_word LEFT_PAREN l=general_terms RIGHT_PAREN + { let loc = L.mk_pos $startpos $endpos in T.apply ~loc f l } + +formula_data: + | DOLLAR_THF LEFT_PAREN f=thf_formula RIGHT_PAREN + | DOLLAR_TFF LEFT_PAREN f=tff_formula RIGHT_PAREN + | DOLLAR_FOF LEFT_PAREN f=fof_formula RIGHT_PAREN + | DOLLAR_CNF LEFT_PAREN f=cnf_formula RIGHT_PAREN + | DOLLAR_FOT LEFT_PAREN f=fof_term RIGHT_PAREN + { f } + +general_list: + | LEFT_BRACKET RIGHT_BRACKET + { [] } + | LEFT_BRACKET l=general_terms RIGHT_BRACKET + { l } + +general_terms: + | t=general_term + { [ t ] } + | t=general_term COMMA l=general_terms + { t :: l } + + +/* General purposes */ + +/* + name: + | n=atomic_word + | n=integer + + This production has been expanded to + produce ids instead of terms. +*/ +name: + | s=LOWER_WORD + | s=SINGLE_QUOTED + | s=INTEGER + { I.mk I.decl s } + +%inline atomic_word: + | s=LOWER_WORD + | s=SINGLE_QUOTED + { let loc = L.mk_pos $startpos $endpos in + T.const ~loc (I.mk I.term s) } + +%inline atomic_defined_word: + | s=DOLLAR_WORD + { let loc = L.mk_pos $startpos $endpos in + T.const ~loc (I.mk I.term s) } + +%inline atomic_system_word: + | s=DOLLAR_DOLLAR_WORD + { let loc = L.mk_pos $startpos $endpos in + T.const ~loc (I.mk I.term s) } + +%inline number: + | n=integer + | n=rational + | n=real + { n } + +file_name: + | s=SINGLE_QUOTED + { let n = String.length s in String.sub s 1 (n - 2) } + + +/* *************************************** */ +/* Wrapper around some lexical definitions */ + +%inline distinct_object: + | s=DISTINCT_OBJECT + { let loc = L.mk_pos $startpos $endpos in + T.distinct ~loc (I.mk I.term s) } + +%inline integer: + | n=INTEGER + { let loc = L.mk_pos $startpos $endpos in T.int ~loc n } + +%inline rational: + | n=RATIONAL + { let loc = L.mk_pos $startpos $endpos in T.rat ~loc n } + +%inline real: + | n=REAL + { let loc = L.mk_pos $startpos $endpos in T.real ~loc n } + + diff --git a/src/languages/tptp/v8.2.0/syntax.bnf b/src/languages/tptp/v8.2.0/syntax.bnf new file mode 100644 index 000000000..e174064b7 --- /dev/null +++ b/src/languages/tptp/v8.2.0/syntax.bnf @@ -0,0 +1,694 @@ +%------------------------------------------------------------------------------ +%----README ... this header provides important meta- and usage information +%---- +%----Intended uses of the various parts of the TPTP syntax are explained +%----in the TPTP technical manual, linked from www.tptp.org. +%---- +%----Four kinds of separators are used, to indicate different types of rules: +%---- ::= is used for regular grammar rules, for syntactic parsing. +%---- :== is used for semantic grammar rules. These define specific values +%---- that make semantic sense when more general syntactic rules apply. +%---- ::- is used for rules that produce tokens. +%---- ::: is used for rules that define character classes used in the +%---- construction of tokens. +%---- +%----White space may occur between any two tokens. White space is not specified +%----in the grammar, but there are some restrictions to ensure that the grammar +%----is compatible with standard Prolog: a should be readable with +%----read/1. +%---- +%----The syntax of comments is defined by the rule. Comments may +%----occur between any two tokens, but do not act as white space. Comments +%----will normally be discarded at the lexical level, but may be processed +%----by systems that understand them (e.g., if the system comment convention +%----is followed). +%---- +%----Four languages are defined first - THF, TFF, FOF, and CNF. Depending on +%----your need, you can implement just the one(s) you need. The common rules +%----for atoms, terms, etc, come after the definitions of the languages, and +%----they are all needed for all four languages (except for the core THF0, +%----which is a defined subset of THF). +%----Top of Page--------------------------------------------------------------- +%----Files. Empty file is OK. + ::= * + ::= | + +%----Formula records + ::= | | | + | +%----Future languages may include ... english | efof | tfof | mathml | ... + ::= tpi(,,). + ::= + ::= thf(,,). + ::= tff(,,). + ::= fof(,,). + ::= cnf(,,). + ::= , | +%----In derivations the annotated formulae names must be unique, so that +%----parent references (see ) are unambiguous. + +%----Types for problems. +%----Note: The previous from ... +%---- ::= - +%----... is now gone. Parsers may choose to be tolerant of it for backwards +%----compatibility. + ::= + :== axiom | hypothesis | definition | assumption | + lemma | theorem | corollary | conjecture | + negated_conjecture | plain | fi_domain | fi_functors | + fi_predicates | type | unknown +%----"axiom"s are accepted, without proof. There is no guarantee that the +%----axioms of a problem are consistent. +%----"hypothesis"s are assumed to be true for a particular problem, and are +%----used like "axiom"s. +%----"definition"s are intended to define symbols. They are either universally +%----quantified equations, or universally quantified equivalences with an +%----atomic lefthand side. They can be treated like "axiom"s. +%----"assumption"s can be used like axioms, but must be discharged before a +%----derivation is complete. +%----"lemma"s and "theorem"s have been proven from the "axiom"s. They can be +%----used like "axiom"s in problems, and a problem containing a non-redundant +%----"lemma" or theorem" is ill-formed. They can also appear in derivations. +%----"theorem"s are more important than "lemma"s from the user perspective. +%----"conjecture"s are to be proven from the "axiom"(-like) formulae. A problem +%----is solved only when all "conjecture"s are proven. +%----"negated_conjecture"s are formed from negation of a "conjecture" (usually +%----in a FOF to CNF conversion). +%----"plain"s have no specified user semantics. +%----"fi_domain", "fi_functors", and "fi_predicates" are used to record the +%----domain, interpretation of functors, and interpretation of predicates, for +%----a finite interpretation. +%----"type" defines the type globally for one symbol; treat as $true. +%----"unknown"s have unknown role, and this is an error situation. +%----Top of Page--------------------------------------------------------------- +%----THF formulae. + ::= | + ::= | | + | + ::= | | +%---- should not be used at the top level. It is needed here +%----for other uses of . + +%----Only some binary connectives can be written without ()s. +%----There's no precedence among binary connectives + ::= + + ::= | | + + ::= | + + ::= & | + & + ::= @ | + @ +%---- are in ()s or do not have a at +%----the top level. Essentially, any lambda expression that "has enough ()s" to +%----be used inside a larger lambda expression. However, lambda notation might +%----not be used. + ::= | | + | | | + () +%----Note that allows s as terms, which will fail +%----type checking. The user must take care with this liberal syntax! + ::= [] : + +%----@ (denoting apply) is left-associative and lambda is right-associative. +%----^ [X] : ^ [Y] : f @ g (where f is a and g is a +%----) should be parsed as: (^ [X] : (^ [Y] : f)) @ g. +%----That is, g is not in the scope of either lambda. + ::= | , + ::= | + ::= : +%----Unary connectives bind more tightly than binary. The negated formula +%----must be ()ed because a ~ is also a term. + ::= () +%---- can also be | | +%---- | , but they are syntactically +%----captured by . + ::= | + ::= $ite_f(,, + ) +%----This is the original, but not working + ::= $let_tf(,) | + $let_ff(,) + ::= + ::= + :== ! [] : | + + :== = | + () + :== ! [] : | + + :== <=> | + () +%----A must be a , or an application of a to +%----pairwise distinct variables that appear in the . + :== | + +%----This is my experimentation +% ::= (,) +% ::= $let_tf | $let_ff +% ::= +% :== ! [] : | +% +% ::= | +% ::= = +% ::= <=> +% %----A must be a , or an application of a to +% %----pairwise distinct variables that appear in the . +% ::= | + +%----A is an assertion that the formula is in this type. + ::= : + ::= | () + ::= +%----In a formula with role 'type', is a global declaration +%----that is in this thf_top_level_type>, i.e., the rule is ... + :== : +%----All symbols must be typed exactly one before use, and all atomic types +%----must be declared (of type $tType) before use. + +%---- appears after ":", where a type is being specified +%----for a term or variable. includes , +%----so the syntax allows just about any lambda expression with "enough" +%----parentheses to serve as a type. The expected use of this flexibility is +%----parametric polymorphism in types, expressed with lambda abstraction. +%----Mapping is right-associative: o > o > o means o > (o > o). +%----Xproduct is left-associative: o * o * o means (o * o) * o. +%----Union is left-associative: o + o + o means (o + o) + o. + ::= + ::= + ::= | | + + ::= | + + ::= | + + ::= | + + +%----Sequents using the Gentzen arrow + ::= | + () + +%----s are syntactic sugar for lists, either the empty list, or a +%----term as the head and a list as a tail. The internal representation is not +%----specified, but see the Wikipedia page ... +%---- http://en.wikipedia.org/wiki/Church_encoding#List_encodings +%----for some possibilities. + ::= [] | [] + ::= | + , + +%----Top of Page--------------------------------------------------------------- +%----TFF formulae. +%----TFF is like FOF except that predicate and function symbols must be typed +%----exactly once at top level (with formula role "type"), and variables must +%----be typed when they are bound in quantifier lists. s are +%----just like FOF. See the proposal linked from the TPTP web page for details +%----of the semantics. + ::= | | +%----This is where used to be + ::= | + ::= | + ::= + + ::= | + ::= | + + ::= & | + & + ::= | | + | | | + () + ::= [] : + + ::= | , + ::= | + ::= : + ::= | + + ::= $ite_f(,, + ) + ::= $let_tf(,) | + $let_ff(,) +%----The LHS of a or a must be +%----flat with pairwise distinct variable arguments, and the variables on the +%----LHS must be those bound in the . + ::= ! [] : | + + ::= = | () + ::= ! [] : | + + ::= <=> | + () + + ::= | + () + ::= [] | [] + ::= | + , + +%---- can appear only at top level + ::= : | + () + ::= | +%----Subtypes have been removed +% ::= | +% () + +%----See for commentary. is TFF1. + ::= | | + | () + ::= !> [] : + ::= | () + ::= | () + ::= | | + () | + ::= | + , +%----For consistency with (the analogue in thf), +%---- should also allow (), but that causes +%----ambiguity. +%----For Josef Urban, change to , and leave +%----out (to avoid conflict on . + ::= + ::= | + + +%----The types of the s and s are: +%---- : $real +%---- : $rat +%---- : $int +%---- : $int +%---- : $i +%---- $true : $o +%---- $false : $o + +%----Top of Page--------------------------------------------------------------- +%----FOF formulae. + ::= | + ::= | +%----Future answer variable ideas | + ::= | +%----Only some binary connectives are associative +%----There's no precedence among binary connectives + ::= + +%----Associative connectives & and | are in + ::= | + ::= | + + ::= & | + & +%---- are in ()s or do not have a at +%----the top level. + ::= | | + | () + ::= [] : + + ::= | , + ::= | + + +%----Top of Page--------------------------------------------------------------- +%----This section is the FOFX syntax. Not yet in use. +% ::= := [] : +% ::= | +% , +% ::= := | +% :- | () +% +% ::= $ite_f(,, +% ) +% +% ::= $ite_t(,,) + + ::= | + () + + ::= [] | [] + ::= | + , + +%----Top of Page--------------------------------------------------------------- +%----CNF formulae (variables implicitly universally quantified) + ::= () | + ::= | + ::= | ~ | + +%----Top of Page--------------------------------------------------------------- +%----Special formulae + ::= | | + + ::= + +%----Connectives - THF + ::= | ^ | !> | ?* | @+ | @- + ::= | | + + ::= | !! | ?? +%----Connectives - THF and TFF + ::= +%----Connectives - FOF + ::= ! | ? + ::= <=> | => | <= | <~> | ~ | ~& + ::= | & + ::= ~ +%----The seqent arrow + ::= --> + +%----Types for THF and TFF + ::= + :== $oType | $o | $iType | $i | $tType | + $real | $rat | $int +%----$oType/$o is the Boolean type, i.e., the type of $true and $false. +%----$iType/$i is non-empty type of individuals, which may be finite or +%----infinite. $tType is the type of all types. $real is the type of s. +%----$rat is the type of s. $int is the type of s +%----and s. + :== + +%----First order atoms + ::= | | + + ::= + :== | () + :== + :== +%----Using removes a reduce/reduce ambiguity in lex/yacc. +%----Note: "defined" means a word starting with one $ and "system" means $$. + ::= | + ::= + :== | () + :== + :== $true | $false +%----Pure CNF should not use $true or $false in problems, and use $false only +%----at the roots of a refutation. + :== + :== $distinct | + $less | $lesseq | $greater | $greatereq | + $is_int | $is_rat +%----$distinct means that each of it's constant arguments are pairwise !=. It +%----is part of the TFF syntax. It can be used only as a fact, not under any +%----connective. + ::= + ::= + ::= = + ::= != +%----Some systems still interpret equal/2 as equality. The use of equal/2 +%----for other purposes is therefore discouraged. Please refrain from either +%----use. Use infix '=' for equality. Note: != is equivalent +%----to ~ = +%----System terms have system specific interpretations + ::= +%----s are used for evaluable predicates that are +%----available in particular tools. The predicate names are not controlled +%----by the TPTP syntax, so use with due care. The same is true for +%----s. + +%----First order terms + ::= | | | + + ::= | | + ::= | () + ::= + ::= +%----Defined terms have TPTP specific interpretations + ::= | + ::= | + ::= +%----None yet | +%----None yet ::= +%----None yet ::= + ::= | () + ::= + :== + ::= + :== $uminus | $sum | $difference | $product | + $quotient | $quotient_e | $quotient_t | $quotient_f | + $remainder_e | $remainder_t | $remainder_f | + $floor | $ceiling | $truncate | $round | + $to_int | $to_rat | $to_real +%----System terms have system specific interpretations + ::= | () + ::= + ::= +%----Variables, and only variables, start with uppercase + ::= +%----Arguments recurse back up to terms (this is the FOF world here) + ::= | , +%----Principal symbols are predicates, functions, variables + :== | +%----Conditional terms should be used by only TFF. + ::= $ite_t(,,) +%----Let terms should be used by only TFF. $let_ft is for use when there is +%----a $ite_t in the + ::= $let_ft(,) | + $let_tt(,) + +%----Top of Page--------------------------------------------------------------- +%----Formula sources + ::= + :== | | | + unknown | [] +%----Alternative sources are recorded like this, thus allowing representation +%----of alternative derivations with shared parts. + :== | , +%----Only a can be a , i.e., derived formulae can be +%----identified by a or an + :== | + :== inference(,, + ) + :== +%----Examples are deduction | modus_tollens | modus_ponens | rewrite | +% resolution | paramodulation | factorization | +% cnf_conversion | cnf_refutation | ... +%---- can be empty in cases when there is a justification +%----for a tautologous theorem. In case when a tautology is introduced as +%----a leaf, e.g., for splitting, then use an . + :== [] | [] + :== | , + :== + :== : | + :== introduced() + :== definition | axiom_of_choice | tautology | assumption +%----This should be used to record the symbol being defined, or the function +%----for the axiom of choice + :== | | + :== file() + :== , | + :== theory() + :== equality | ac +%----More theory names may be added in the future. The is +%----used to store, e.g., which axioms of equality have been implicitly used, +%----e.g., theory(equality,[rst]). Standard format still to be decided. + :== creator() + :== + +%----Useful info fields + ::= , | + ::= + :== [] | [] + :== | , + :== | | +%----Useful info for formula records + :== | + :== description() + :== iquote() +%----s are used for recording exactly what the system output about +%----the inference step. In the future it is planned to encode this information +%----in standardized forms as in each . +%----Useful info for inference records + :== | | + | + :== status() | +%----These are the success status values from the SZS ontology. The most +%----commonly used values are: +%---- thm - Every model of the parent formulae is a model of the inferred +%---- formula. Regular logical consequences. +%---- cth - Every model of the parent formulae is a model of the negation of +%---- the inferred formula. Used for negation of conjectures in FOF to +%---- CNF conversion. +%---- esa - There exists a model of the parent formulae iff there exists a +%---- model of the inferred formula. Used for Skolemization steps. +%----For the full hierarchy see the SZSOntology file distributed with the TPTP. + :== suc | unp | sap | esa | sat | fsa | thm | eqv | tac | + wec | eth | tau | wtc | wth | cax | sca | tca | wca | + cup | csp | ecs | csa | cth | ceq | unc | wcc | ect | + fun | uns | wuc | wct | scc | uca | noc +%---- is used to record standard information associated with an +%----arbitrary inference rule. The is the same as the +%---- of the . The indicates +%----the information being recorded in the . The +%----are (loosely) set by TPTP conventions, and include esplit, sr_split, and +%----discharge. + :== (,) +%----An lists the names of assumptions upon which this +%----inferred formula depends. These must be discharged in a completed proof. + :== assumptions([]) +%----A record names a file in which the inference recorded here +%----is recorded as a proof by refutation. + :== refutation() +%----A provides information about a newly introduced symbol. + :== new_symbols(,[]) + :== | + , + +%----Include directives + ::= include(). + ::= ,[] | + ::= | , + +%----Non-logical data + ::= | : | + + ::= | | + | | | + + ::= () +%----A bind() term is used to record a variable binding in an +%----inference, as an element of the list. + :== bind(,) + ::= $thf() | $tff() | + $fof() | $cnf() | + $fot() + ::= [] | [] + ::= | , + +%----General purpose + ::= | +%----Integer names are expected to be unsigned + ::= | +%---- tokens do not include their outer quotes, therefore the +%---- cat and the 'cat' +%----are the same. Quotes must be removed from a +%----if doing so produces a . Note that s +%----and s are not s, so '123' and 123, and 'X' and X, +%----are different. + ::= + ::= + ::= | | +%----Numbers are always interpreted as themselves, and are thus implicitly +%----distinct if they have different values, e.g., 1 != 2 is an implicit axiom. +%----All numbers are base 10 at the moment. + ::= + ::= +%----Top of Page--------------------------------------------------------------- +%----Rules from here on down are for defining tokens (terminal symbols) of the +%----grammar, assuming they will be recognized by a lexical scanner. +%----A ::- rule defines a token, a ::: rule defines a macro that is not a +%----token. Usual regexp notation is used. Single characters are always placed +%----in []s to disable any special meanings (for uniformity this is done to +%----all characters, not only those with special meanings). + +%----These are tokens that appear in the syntax rules above. No rules +%----defined here because they appear explicitly in the syntax rules, +%----except that , , denote "|", "*", "+", respectively. +%----Keywords: fof cnf thf tff include +%----Punctuation: ( ) , . [ ] : +%----Operators: ! ? ~ & | <=> => <= <~> ~| ~& * + +%----Predicates: = != $true $false + +%----For lex/yacc there cannot be spaces on either side of the | here + ::- | + ::- [%]* + ::: [/][*][*][*]*[/] + ::: ([^*]*[*][*]*[^/*])*[^*]* +%----Defined comments are a convention used for annotations that are used as +%----additional input for systems. They look like comments, but start with %$ +%----or /*$. A wily user of the syntax can notice the $ and extract information +%----from the "comment" and pass that on as input to the system. They are +%----analogous to pragmas in programming languages. To extract these separately +%----from regular comments, the rules are: +%---- ::- | +%---- ::: [%]* +%---- ::: [/][*][*][*]*[/] +%----A string that matches both and should be +%----recognized as , so put these before . +%----Defined comments that are in use include: +%---- TO BE ANNOUNCED +%----System comments are a convention used for annotations that may used as +%----additional input to a specific system. They look like comments, but start +%----with %$$ or /*$$. A wily user of the syntax can notice the $$ and extract +%----information from the "comment" and pass that on as input to the system. +%----The specific system for which the information is intended should be +%----identified after the $$, e.g., /*$$Otter 3.3: Demodulator */ +%----To extract these separately from regular comments, the rules are: +%---- ::- | +%---- ::: [%]* +%---- ::: [/][*][*][*]*[/] +%----A string that matches both and should +%----be recognized as , so put these before . + + ::- * +%----s contain visible characters. \ is the escape character for +%----' and \, i.e., \' is not the end of the . +%----The token does not include the outer quotes, e.g., 'cat' and cat are the +%----same. See for information about stripping the quotes. + + ::- * +%---Space and visible characters upto ~, except " and \ +%----s contain visible characters. \ is the escape character +%----for " and \, i.e., \" is not the end of the . +%----s are different from (but may be equal to) other tokens, +%----e.g., "cat" is different from 'cat' and cat. Distinct objects are always +%----interpreted as themselves, so if they are different they are unequal, +%----e.g., "Apple" != "Microsoft" is implicit. + + ::- + ::- + ::- * + ::- * + +%----Tokens used in syntax, and cannot be character classes + ::- [|] + ::- [*] + ::- [+] + ::- [>] + ::- [<] + +%----Numbers. Signs are made part of the same token here. + ::- (|) + ::- + ::- (|) + ::- (|) + ::- + ::- + ::- (|) + ::- + ::- + ::- (|) + ::- * + ::- (|) + ::- + ::- * + ::- (|) + ::- + ::- * + +%----Character classes + ::: [%] + ::: ["] + ::: ([\40-\41\43-\133\135-\176]|[\\]["\\]) + ::: ['] +%---Space and visible characters upto ~, except ' and \ + ::: ([\40-\46\50-\133\135-\176]|[\\]['\\]) + ::: [+-] + ::: [.] + ::: [Ee] + ::: [/] + ::: [0] + ::: [1-9] + ::: [0-9] + ::: [a-z] + ::: [A-Z] + ::: (|||[_]) + ::: [$] + ::: . +%---- is any printable ASCII character, codes 32 (space) to 126 +%----(tilde). does not include tabs, newlines, bells, etc. The +%----use of . does not not exclude tab, so this is a bit loose. + ::: [.\n] +%----Top of Page--------------------------------------------------------------- + diff --git a/src/languages/tptp/v8.2.0/syntax.bnf.new b/src/languages/tptp/v8.2.0/syntax.bnf.new new file mode 100644 index 000000000..6ff8f0d4a --- /dev/null +++ b/src/languages/tptp/v8.2.0/syntax.bnf.new @@ -0,0 +1,690 @@ +%----v8.2.0.0 (TPTP version.internal development number) +%----v8.2.0.1 - Added required ()s around , , +%---- , and . For TFF the ()s are really needed for +%---- only TXF, but TXF uses the same grammar rules. +%-------------------------------------------------------------------------------------------------- +%----README ... this header provides important meta- and usage information +%---- +%----Intended uses of the various parts of the TPTP syntax are explained in the TPTP technical +%----manual, linked from www.tptp.org. +%---- +%----Four kinds of separators are used, to indicate different types of rules: +%---- ::= is used for regular grammar rules, for syntactic parsing. +%---- :== is used for semantic grammar rules. These define specific values that make semantic +%---- sense when more general syntactic rules apply. +%---- ::- is used for rules that produce tokens. +%---- ::: is used for rules that define character classes used in the construction of tokens. +%---- +%----White space may occur between any two tokens. White space is not specified in the grammar, but +%----there are some restrictions to ensure that the grammar is compatible with standard Prolog: a +%---- should be readable with read/1. +%---- +%----The syntax of comments is defined by the rule. Comments may occur between any two +%----tokens, but do not act as white space. Comments will normally be discarded at the lexical +%----level, but may be processed by systems that understand them (e.g., if the system comment +%----convention is followed). +%---- +%----Multiple languages are defined. Depending on your need, you can implement just the one(s) you +%----need. The common rules for atoms, terms, etc, come after the definitions of the languages, and +%----mostly all needed for all the languages. +%----Top of Page----------------------------------------------------------------------------------- +%----Files. Empty file is OK. + ::= * + ::= | + +%----Formula records + ::= | | | | + | +%----Future languages may include ... english | efof | tfof | mathml | ... + ::= tpi(,,). + ::= + ::= thf(,,). + ::= tff(,,). + ::= tcf(,,). + ::= fof(,,). + ::= cnf(,,). + ::= , | +%----In derivations the annotated formulae names must be unique, so that parent references (see +%----) are unambiguous. + +%----Types for problems. +%----Note: The previous from ... +%---- ::= - +%----... is now gone. Parsers may choose to be tolerant of it for backwards compatibility. + ::= | - + :== axiom | hypothesis | definition | assumption | lemma | theorem | + corollary | conjecture | negated_conjecture | plain | type | + interpretation | fi_domain | fi_functors | fi_predicates | unknown +%----"axiom"s are accepted, without proof. There is no guarantee that the axioms of a problem are +%----consistent. "hypothesis"s are assumed to be true for a particular problem, and are used like +%----"axiom"s. "definition"s are intended to define symbols. They are either universally quantified +%----equations, or universally quantified equivalences with an atomic lefthand side. They can be +%----treated like "axiom"s. "assumption"s can be used like axioms, but must be discharged before a +%----derivation is complete. "lemma"s and "theorem"s have been proven from the "axiom"s. They can +%----be used like "axiom"s in problems, and a problem containing a non-redundant "lemma" or +%----"theorem" is ill-formed. They can also appear in derivations. "theorem"s are more important +%----than "lemma"s from the user perspective. "conjecture"s are to be proven from the +%----"axiom"(-like) formulae. A problem is solved only when all "conjecture"s are proven. +%----"negated_conjecture"s are formed from negation of a "conjecture" (usually in a FOF to CNF +%----conversion). "plain"s have no specified user semantics. "interpretation"s record all aspects +%----of an interpretation. "fi_domain", "fi_functors", and "fi_predicates" are are thge old way of +%----recording the domain, interpretation of functors, and interpretation of predicates, for a +%----finite interpretation. "type" defines the type globally for one symbol; treat as $true. +%----"unknown"s have unknown role, and this is an error situation. +%----Top of Page----------------------------------------------------------------------------------- +%----THF formulae. + ::= | | + ::= | | | + | | + ::= | | +%----There's no precedence among binary connectives + ::= + ::= | | + ::= | + + ::= & | + & +%----@ (denoting apply) is left-associative and lambda is right-associative. +%----^ [X] : ^ [Y] : f @ g (where f is a and g is a ) +%----should be parsed as: (^ [X] : (^ [Y] : f)) @ g. That is, g is not in the scope of either +%----lambda. + ::= @ | + @ + ::= | | + ::= | + ::= | | | + () +%----All variables must be quantified + ::= + ::= [] : + ::= | , + ::= : + ::= | + ::= + ::= ( ) + ::= | | | + + ::= | +%---- includes because tuples can be formulae +%----in logic definitions + ::= | | () | + | +% +%---- is omitted from because $ite is +%----read simply as a + ::= | +%----The ()s are really optional. I have reformated the TPTP to include them so, e.g., +%----! [X:foo] a = X is formatted as ! [X:foo] (a = X) to save the lives of parsers that would +%----parse it as (! [X:foo] a) = X and throw an error. +% ::= ( ) + ::= +%----Defined terms can't be formulae. See TFF. FIX HERE. + ::= + +%---- is written and read as a +% ::= $ite(,, ) + ::= $let(,, ) + ::= | [] + ::= | , + ::= | [] + ::= + ::= | , + + ::= | | () + ::= | | | + | +%----Note that syntactically this allows (p @ =), but for = the first argument must be known to +%----infer the type of =, so that's not allowed, i.e., only (= @ p). + ::= [] | [] + +%----Allows first-order style in THF. + ::= () | () | + () +%----Arguments recurse back up to formulae (this is the THF world here) + ::= + ::= | , + +%---- appears after ":", where a type is being specified +%----for a term or variable. includes , +%----so the syntax is very loose, but trying to be more specific about +%----s (ala the semantic rule) leads to reduce/reduce +%----conflicts. + ::= : | () + ::= | | +%----Removed along with adding to , for +%----TH1 polymorphic types with binary after quantification. +%---- | () + ::= + :== | + :== | | | | + () + :== !> [] : + + ::= + ::= | | +%----Mapping is right-associative: o > o > o means o > (o > o). + ::= | + +%----Xproduct is left-associative: o * o * o means (o * o) * o. Xproduct +%----can be replaced by tuple types. + ::= | + +%----Union is left-associative: o + o + o means (o + o) + o. + ::= | + +%----Tuple types, e.g., [a,b,c], are allowed (by the loose syntax) as tuples. + ::= + +%----These are also used for NHF logic definitions + ::= + ::= + +%----Top of Page----------------------------------------------------------------------------------- +%----TFF formulae. + ::= | | + ::= | | | + | | +%---- up here to avoid confusion in a = b | p, for TXF. +%----For plain TFF it can be in + + ::= | + ::= + ::= | + ::= | + + ::= & | + & + ::= | | + ::= | + ::= | | + | () + ::= + ::= [] : +%----Quantified formulae bind tightly, so cannot include infix formulae + + ::= | , + ::= | + ::= : + ::= | +%FOR PLAIN TFF + ::= + ::= ( ) + +%FOR PLAIN TFF ::= + ::= | | + ::= | () + :== | () + ::= +%---To avoid confusion in TXF a = b | p | + ::= | () | | + +% +%---- is omitted from because $ite is +%----read simply as a + :== | () | + | | +%----This is the only one that is strictly a formula, type $o. In TXF, if the +%----LHS/RHS is a formula that does not look like a term, then it must be ()ed +%----per . If you put an un()ed formula that looks like a term +%----it will be interpreted as a term. + ::= ( ) + ::= | () + :== | () +%---- is written and read as a + :== $ite(,,) + ::= $let(,,) + ::= | [] + ::= | , + ::= | [] + ::= + ::= | + ::= | , + ::= @ () + + ::= | | + ::= | | | | + () + ::= [] | [] + + ::= | , + +%---- can appear only at top level. + ::= : | () + ::= | + ::= | | () + ::= !> [] : + ::= | () | + ::= | () + ::= | | | + () | () | + + ::= | , + ::= + ::= | + +%----For TXF only + ::= [] + ::= | , + + ::= + +%----These are also used for NXF logic definitions + ::= + ::= + +%----Top of Page----------------------------------------------------------------------------------- +%----Typed non-classical here +%----Have to duplicate NHF and NXF because they lead to and + ::= {} | {()} + ::= | , + ::= | + ::= + + ::= {} | {()} + ::= | , + ::= | + ::= + + ::= + ::= + ::= [.] | . | {.} | (.) +%----Short connectives are unary operators, cannot be indexed +%---- | [] | | +%---- {} + +%----NXF logic specifications. Captured by +%----NHF logic specifications are captured by + :== + :== + :== | [] + :== | , + :== | + +%----Top of Page----------------------------------------------------------------------------------- +%----TCF formulae. + ::= | + ::= | + ::= ! [] : + +%----Top of Page----------------------------------------------------------------------------------- +%----FOF formulae. + ::= | + ::= | | +%----Future answer variable ideas | + ::= | +%----Only some binary connectives are associative +%----There's no precedence among binary connectives + ::= +%----Associative connectives & and | are in + ::= | + ::= | + + ::= & | + & + ::= | +%---- != is equivalent to ~ = + ::= +%---- are in ()s or do not have a connective + ::= | + ::= | | () +%----All variables must be quantified + ::= [] : + ::= | , + ::= | | + + ::= + :== | () + ::= | + ::= + :== | () + ::= +%----System terms have system specific interpretations + ::= +%----s are used for evaluable predicates that are +%----available in particular tools. The predicate names are not controlled by +%----the TPTP syntax, so use with due care. Same for s. + +%----FOF terms. + ::= | () +%----Defined terms have TPTP specific interpretations + ::= | + ::= +%----None yet | +%----None yet ::= +%----None yet ::= + ::= | () +%----System terms have system specific interpretations + ::= | () +%----Arguments recurse back to terms (this is the FOF world here) + ::= | , +%----These are terms used as arguments. Not the entry point for terms because +%---- is also used as . The +%----is used in , which is also used as +%----. + ::= | + ::= | | + +%----Top of Page----------------------------------------------------------------------------------- +%----This section is the FOFX syntax. Not yet in use. + ::= | + () + + ::= {} | {} + ::= | , + +%----Top of Page----------------------------------------------------------------------------------- +%----CNF formulae (variables implicitly universally quantified) + ::= | ( ) + ::= | + ::= | ~ | + ~ () | + +%----Top of Page----------------------------------------------------------------------------------- +%----Connectives - THF + ::= | | + ::= | +%----TH0 quantifiers are also available in TH1 + ::= !> | ?* + ::= ^ | @+ | @- +%----Connectives - THF and TFF + ::= << +%----Connectives - TFF + ::= | +%----Connectives - FOF + ::= ! | ? + ::= <=> | => | <= | <~> | ~ | ~& + ::= | & + ::= ~ +%----The seqent arrow + ::= --> + ::= := + ::= == + +%----Types for THF and TFF + ::= + ::= + ::= + :== $oType | $o | $iType | $i | $tType | $real | $rat | $int +%----$oType/$o is the Boolean type, i.e., the type of $true and $false. +%----$iType/$i is non-empty type of individuals, which may be finite or +%----infinite. $tType is the type of all types. $real is the type of s. +%----$rat is the type of s. $int is the type of s +%----and s. + :== + +%----For all language types + ::= | + ::= | + + :== + :== + :== + :== $true | $false + :== + :== $distinct | + $less | $lesseq | $greater | $greatereq | $is_int | $is_rat | + $box | $dia +%----$distinct means that each of it's constant arguments are pairwise !=. It is part of the TFF +%----syntax. It can be used only as a fact in an axiom (not a conjecture), and not under any +%----connective. + ::= + :== + :== + ::= = + ::= != + + ::= + ::= + ::= + ::= + :== $uminus | $sum | $difference | $product | + $quotient | $quotient_e | $quotient_t | $quotient_f | + $remainder_e | $remainder_t | $remainder_f | + $floor | $ceiling | $truncate | $round | + $to_int | $to_rat | $to_real + ::= + ::= + ::= | + ::= !! | ?? | @@+ | @@- | @= + ::= | + ::= +%----Top of Page----------------------------------------------------------------------------------- +%----Formula sources + ::= + :== | | | unknown | + [] +%----Alternative sources are recorded like this, thus allowing representation +%----of alternative derivations with shared parts. + :== | , +%----Only a can be a , i.e., derived formulae can be +%----identified by a or an + :== | + :== inference(,, ) + :== +%----Examples are deduction | modus_tollens | modus_ponens | rewrite | resolution | +%---- paramodulation | factorization | cnf_conversion | cnf_refutation | ... +%---- can be empty in cases when there is a justification +%----for a tautologous theorem. In case when a tautology is introduced as +%----a leaf, e.g., for splitting, then use an . + :== [] | [] + :== | , + :== + :== : | + :== introduced() + :== definition | axiom_of_choice | tautology | assumption +%----This should be used to record the symbol being defined, or the function +%----for the axiom of choice + :== | | + :== file() + :== , | + :== theory() + :== equality | ac +%----More theory names may be added in the future. The is +%----used to store, e.g., which axioms of equality have been implicitly used, +%----e.g., theory(equality,[rst]). Standard format still to be decided. + :== creator() + :== + +%----Useful info fields + ::= , | + ::= + :== [] | [] + :== | , + :== | | +%----Useful info for formula records + :== | + :== description() + :== iquote() +%----s are used for recording exactly what the system output about +%----the inference step. In the future it is planned to encode this information +%----in standardized forms as in each . +%----Useful info for inference records + :== | | | + + :== status() | +%----These are the success status values from the SZS ontology. The most +%----commonly used values are: +%---- thm - Every model of the parent formulae is a model of the inferred formula. Regular logical +%---- consequences. +%---- cth - Every model of the parent formulae is a model of the negation of the inferred formula. +%---- Used for negation of conjectures in FOF to CNF conversion. +%---- esa - There exists a model of the parent formulae iff there exists a model of the inferred +%---- formula. Used for Skolemization steps. +%----For the full hierarchy see the SZSOntology file distributed with the TPTP. + :== suc | unp | sap | esa | sat | fsa | thm | eqv | tac | wec | eth | tau | + wtc | wth | cax | sca | tca | wca | cup | csp | ecs | csa | cth | ceq | + unc | wcc | ect | fun | uns | wuc | wct | scc | uca | noc +%---- is used to record standard information associated with an arbitrary inference +%----rule. The is the same as the of the . The +%---- indicates the information being recorded in the . The +%---- are (loosely) set by TPTP conventions, and include esplit, sr_split, and +%----discharge. + :== (,) +%----An lists the names of assumptions upon which this +%----inferred formula depends. These must be discharged in a completed proof. + :== assumptions([]) +%----A record names a file in which the inference recorded here +%----is recorded as a proof by refutation. + :== refutation() +%----A provides information about a newly introduced symbol. + :== new_symbols(,[]) + :== | , +%----Principal symbols are predicates, functions, variables + :== | + +%----Include directives + ::= include(). + ::= | , | ,, + ::= [] | + ::= | , + ::= + +%----Non-logical data + ::= | : | + ::= | | | | + | + ::= () +%----A bind() term is used to record a variable binding in an +%----inference, as an element of the list. + :== bind(,) | bind_type(,) + :== $thf() | $tff() + ::= $thf() | $tff() | $fof() | + $cnf() | $fot() + ::= [] | [] + ::= | , + +%----General purpose + ::= | +%----Integer names are expected to be unsigned + ::= | +%---- tokens do not include their outer quotes, therefore the +%---- cat and the 'cat' are the same. Quotes must be +%----removed from a if doing so produces a +%----. Note that s and s are not s, so '123' and 123, +%----and 'X' and X, are different. + ::= + ::= + ::= | | +%----Numbers are always interpreted as themselves, and are thus implicitly +%----distinct if they have different values, e.g., 1 != 2 is an implicit axiom. +%----All numbers are base 10 at the moment. + ::= + ::= +%----Top of Page----------------------------------------------------------------------------------- +%----Rules from here on down are for defining tokens (terminal symbols) of the grammar, assuming +%----they will be recognized by a lexical scanner. +%----A ::- rule defines a token, a ::: rule defines a macro that is not a token. Usual regexp +%----notation is used. Single characters are always placed in []s to disable any special meanings +%----(for uniformity this is done to all characters, not only those with special meanings). + +%----These are tokens that appear in the syntax rules above. No rules defined here because they +%----appear explicitly in the syntax rules, except that , , denote "|", "*", +%----"+", respectively. +%----Keywords: fof cnf thf tff include +%----Punctuation: ( ) , . [ ] : +%----Operators: ! ? ~ & | <=> => <= <~> ~| ~& * + +%----Predicates: = != $true $false + +%----For lex/yacc there cannot be spaces on either side of the | here + ::- | + ::- [%]* + ::: [/][*][*][*]*[/] + ::: ([^*]*[*][*]*[^/*])*[^*]* +%----Defined comments are a convention used for annotations that are used as additional input for +%----systems. They look like comments, but start with %$ or /*$. A wily user of the syntax can +%----notice the $ and extract information from the "comment" and pass that on as input to the +%----system. They are analogous to pragmas in programming languages. To extract these separately +%----from regular comments, the rules are: +%---- ::- | +%---- ::: [%]* +%---- ::: [/][*][*][*]*[/] +%----A string that matches both and should be recognized as +%----, so put these before . Defined comments that are in use include: +%---- TO BE ANNOUNCED +%----System comments are a convention used for annotations that may used as additional input to a +%----specific system. They look like comments, but start with %$$ or /*$$. A wily user of the +%----syntax can notice the $$ and extract information from the "comment" and pass that on as input +%----to the system. The specific system for which the information is intended should be identified +%----after the $$, e.g., /*$$Otter 3.3: Demodulator */ To extract these separately from regular +%----comments, the rules are: +%---- ::- | +%---- ::: [%]* +%---- ::: [/][*][*][*]*[/] +%----A string that matches both and should +%----be recognized as , so put these before . + + ::- * +%----s contain visible characters. \ is the escape character for ' and \, i.e., +%----\' is not the end of the . The token does not include the outer quotes, e.g., +%----'cat' and cat are the same. See for information about stripping the quotes. + + ::- * +%---Space and visible characters upto ~, except " and \ distinct_object>s contain visible +%----characters. \ is the escape character for " and \, i.e., \" is not the end of the +%----. s are different from (but may be equal to) other tokens, +%----e.g., "cat" is different from 'cat' and cat. Distinct objects are always interpreted as +%----themselves, so if they are different they are unequal, e.g., "Apple" != "Microsoft" is +%----implicit. + + ::- * + ::- * + ::- * + ::- * + +%----Tokens used in syntax, and cannot be character classes + ::- [|] + ::- [*] + ::- [+] + ::- [>] + ::- [<] + ::- [#] + +%----Numbers. Signs are made part of the same token here. + ::- (|) + ::- + ::- (|) + ::- (|) + ::- + ::- + ::- (|) + ::- + ::- + ::- (|) + ::- * + ::- (|) + ::- + ::- * + ::- (|) + ::- + ::- * + + ::- + ::- + +%----Character classes + ::: [%] + ::: ["] + ::: ([\40-\41\43-\133\135-\176]|[\\]["\\]) + ::: ['] +%---Space and visible characters upto ~, except ' and \ + ::: ([\40-\46\50-\133\135-\176]|[\\]['\\]) + ::: [+-] + ::: [.] + ::: [Ee] + ::: [/] + ::: [\\] +%% ::: [|] + ::: [0] + ::: [1-9] + ::: [0-9] + ::: [a-z] + ::: [A-Z] + ::: (|||[_]) + ::: [$] + ::: . +%---- is any printable ASCII character, codes 32 (space) to 126 (tilde). +%---- does not include tabs, newlines, bells, etc. The use of . does not not +%----exclude tab, so this is a bit loose. + ::: [.\n] +%----Top of Page----------------------------------------------------------------------------------- diff --git a/src/languages/tptp/v8.2.0/syntax.messages b/src/languages/tptp/v8.2.0/syntax.messages new file mode 100644 index 000000000..e69de29bb diff --git a/src/languages/tptp/v8.2.0/tokens.mly b/src/languages/tptp/v8.2.0/tokens.mly new file mode 100644 index 000000000..c104ca330 --- /dev/null +++ b/src/languages/tptp/v8.2.0/tokens.mly @@ -0,0 +1,98 @@ + +(* This file is free software, part of dolmen. See file "LICENSE" for more information *) + +/* Token declarations for Tptp parser */ + +%token EOF + +%token DASH +%token DOT +%token COMMA +%token COLON + +%token LEFT_PAREN +%token RIGHT_PAREN +%token LEFT_BRACKET +%token RIGHT_BRACKET +%token LEFT_CURLY +%token RIGHT_CURLY + +%token CNF +%token FOF +%token TFF +%token TCF +%token THF +%token TPI +%token INCLUDE + +%token LAMBDA +%token APPLY +%token DEFINITE_DESCRIPTION_OP +%token DEFINITE_DESCRIPTION_TERM +%token INDEFINITE_DESCRIPTION_OP +%token INDEFINITE_DESCRIPTION_TERM +%token EQUAL_TERM +%token FORALL_TY +%token FORALL +%token EXISTS_TY +%token EXISTS + +%token PI +%token SIGMA + +%token LESS +%token ARROW +%token SUBTYPE + +%token HASH + +%token STAR +%token PLUS + +%token XOR +%token EQUIV +%token IMPLY +%token LEFT_IMPLY + +%token NOT +%token AND +%token VLINE +%token NOTAND +%token NOTVLINE + +%token EQUAL +%token NOT_EQUAL +%token ASSIGNMENT +%token IDENTICAL +%token GENTZEN_ARROW + +%token LET + +%token DOLLAR_THF +%token DOLLAR_TFF +%token DOLLAR_FOF +%token DOLLAR_CNF +%token DOLLAR_FOT + +%token LOWER_WORD +%token UPPER_WORD +%token SINGLE_QUOTED +%token DISTINCT_OBJECT +%token DOLLAR_WORD +%token DOLLAR_DOLLAR_WORD +%token REAL +%token RATIONAL +%token INTEGER + + +/* priority to solve shift/reduce conflcits, and ensure that + "! [X] X = a" + is parsed as + "! [X] (X = a)" +*/ +%nonassoc quantifier_prec +%nonassoc EQUAL + + +%% + diff --git a/src/loop/typer.ml b/src/loop/typer.ml index bb5757269..41b6cc34a 100644 --- a/src/loop/typer.ml +++ b/src/loop/typer.ml @@ -1599,6 +1599,46 @@ module Typer(State : State.S) = struct ~st:(State.get ty_state st).typer ~var_infer ~sym_infer ~poly ~warnings ~file builtins + | Some "tcf" when (match v with + | `Latest | `V8_2_0 -> true + | `V6_3_0 -> false + ) -> + let var_infer = T.{ + var_hook = ignore; + infer_unbound_vars = No_inference; + infer_type_vars_in_binding_pos = true; + infer_term_vars_in_binding_pos = + Wildcard (Any_base { + allowed = [Dolmen.Std.Expr.Ty.base]; + preferred = Dolmen.Std.Expr.Ty.base; + }); + } in + let sym_infer = T.{ + sym_hook = ignore; + infer_type_csts = true; + infer_term_csts = Wildcard (Arrow { + arg_shape = Any_base { + allowed = [Dolmen.Std.Expr.Ty.base]; + preferred = Dolmen.Std.Expr.Ty.base; + }; + ret_shape = Any_base { + allowed = [ + Dolmen.Std.Expr.Ty.base; + Dolmen.Std.Expr.Ty.prop; + ]; + preferred = Dolmen.Std.Expr.Ty.base; + }; + }); + } in + let builtins = Dolmen_type.Base.merge [ + additional_builtins; + Tptp_Core.parse v; + Tptp_Arith.parse v; + ] in + T.empty_env ~order:First_order + ~st:(State.get ty_state st).typer + ~var_infer ~sym_infer ~poly + ~warnings ~file builtins | bad_kind -> let builtins = Dolmen_type.Base.noop in let env = @@ -2043,7 +2083,7 @@ module Make | `Get_assignment | `Get_assertions | `Echo of string - | `Other of Dolmen.Std.Id.t * Dolmen.Std.Statement.term list + | `Other of Dolmen.Std.Statement.term * Dolmen.Std.Statement.term list ] type set_info = [ @@ -2147,7 +2187,7 @@ module Make Format.fprintf fmt "@[echo: %s@]" s | `Other (name, args) -> Format.fprintf fmt "@[other/%a: %a@]" - Dolmen.Std.Id.print name + Dolmen.Std.Term.print name (Format.pp_print_list Dolmen.Std.Term.print) args | `Set_logic (s, logic) -> Format.fprintf fmt diff --git a/src/loop/typer_intf.ml b/src/loop/typer_intf.ml index 5eb5402bb..cd2434b9e 100644 --- a/src/loop/typer_intf.ml +++ b/src/loop/typer_intf.ml @@ -249,7 +249,7 @@ module type S = sig | `Get_assignment | `Get_assertions | `Echo of string - | `Other of Dolmen.Std.Id.t * Dolmen.Std.Statement.term list + | `Other of Dolmen.Std.Statement.term * Dolmen.Std.Statement.term list ] (** Various info getters *) diff --git a/src/standard/expr.ml b/src/standard/expr.ml index bdd7b2b37..52c03fd3c 100644 --- a/src/standard/expr.ml +++ b/src/standard/expr.ml @@ -77,8 +77,9 @@ and term_descr = | Match of term * (pattern * term) list and binder = - | Let_seq of (term_var * term) list + | Let_seq of (term_var * term) list | Let_par of (term_var * term) list + | Let_match of term list * (term * term) list | Lambda of ty_var list * term_var list | Exists of ty_var list * term_var list | Forall of ty_var list * term_var list diff --git a/src/standard/extensions.ml b/src/standard/extensions.ml index a469bf6de..9436375cd 100644 --- a/src/standard/extensions.ml +++ b/src/standard/extensions.ml @@ -35,7 +35,9 @@ module Smtlib2 = struct let statement s = let mk ?loc sexprs = - Statement.other ?loc Id.(mk Decl s) sexprs + let id = Id.(mk Decl s) in + let name = Term.const id in + Statement.other ?loc name sexprs in if List.exists (fun { active; stmts; name = _; } -> active && List.mem s stmts) (exts ()) diff --git a/src/standard/statement.ml b/src/standard/statement.ml index 53d84878d..1297c7a0a 100644 --- a/src/standard/statement.ml +++ b/src/standard/statement.ml @@ -57,7 +57,7 @@ type local = { } type other = { - name : Id.t; + name : term; args : term list; } @@ -320,7 +320,7 @@ let rec print_descr fmt = function | Other { name; args; } -> Format.fprintf fmt "@[other/%a: %a@]" - Id.print name + Term.print name (Misc.print_list ~print_sep:Format.fprintf ~sep:"@ " ~print:Term.print) args | Echo s -> Format.fprintf fmt "echo: %s" s @@ -594,9 +594,9 @@ let include_ ?loc s l = let attrs = List.map Term.const l in mk ?loc ~attrs (Include s) -let tptp ?loc ?annot kind id role body = +let tptp ?loc ?annot kind id ~role body = let attrs = - Term.apply (Term.const Id.tptp_role) [Term.const Id.(mk Attr role)] :: + Term.apply (Term.const Id.tptp_role) [role] :: Term.apply (Term.const Id.tptp_kind) [Term.const Id.(mk Attr kind)] :: match annot with | None -> [] | Some t -> [t] @@ -604,41 +604,45 @@ let tptp ?loc ?annot kind id role body = let ok descr = mk ~id ?loc ~attrs descr in let other () = match body with - | `Term t -> other ~id ?loc ~attrs Id.(mk Decl role) [t] - | `Clause l -> other ~id ?loc ~attrs Id.(mk Decl role) l + | `Term t -> other ~id ?loc ~attrs role [t] + | `Clause l -> other ~id ?loc ~attrs role l in - match role with - | "axiom" - | "hypothesis" - | "definition" - | "lemma" - | "theorem" - | "assumption" - | "negated_conjecture" -> - begin match body with - | `Term t -> ok (Antecedent t) - | `Clause l -> ok (Clause l) - end - | "conjecture" -> - begin match body with - | `Term t -> ok (Consequent t) - | `Clause _ -> other () - end - | "type" -> - begin match body with - | `Term { Term.term = Term.Colon ({ Term.term = Term.Symbol s; _ }, ty ) ; _ } -> - ok (Decls { recursive = false; - contents = [abstract ?loc s ty]; }) - | _ -> other () - end - | _ -> other () - -let tpi ?loc ?annot id role t = tptp ?loc ?annot "tpi" id role (`Term t) -let thf ?loc ?annot id role t = tptp ?loc ?annot "thf" id role (`Term t) -let tff ?loc ?annot id role t = tptp ?loc ?annot "tff" id role (`Term t) -let fof ?loc ?annot id role t = tptp ?loc ?annot "fof" id role (`Term t) - -let cnf ?loc ?annot id role t = + match (role : Term.t) with + | { term = Symbol { ns = Attr; name = Simple "axiom" }; _ } + | { term = Symbol { ns = Attr; name = Simple "hypothesis" }; _ } + | { term = Symbol { ns = Attr; name = Simple "definition" }; _ } + | { term = Symbol { ns = Attr; name = Simple "lemma" }; _ } + | { term = Symbol { ns = Attr; name = Simple "theorem" }; _ } + | { term = Symbol { ns = Attr; name = Simple "corollary" }; _ } + | { term = Symbol { ns = Attr; name = Simple "assumption" }; _ } + (* assumptions can be treated as axioms, but should be discharged/proved before + being used in proofs. See later if we need a separate representation for these. *) + | { term = Symbol { ns = Attr; name = Simple "negated_conjecture" }; _ } -> + begin match body with + | `Term t -> ok (Antecedent t) + | `Clause l -> ok (Clause l) + end + | { term = Symbol { ns = Attr; name = Simple "conjecture" }; _ } -> + begin match body with + | `Term t -> ok (Consequent t) + | `Clause _ -> other () + end + | { term = Symbol { ns = Attr; name = Simple "type" }; _ } -> + begin match body with + | `Term { Term.term = Term.Colon ({ Term.term = Term.Symbol s; _ }, ty ) ; _ } -> + ok (Decls { recursive = false; + contents = [abstract ?loc s ty]; }) + | _ -> other () + end + | _ -> other () + +let tpi ?loc ?annot id ~role t = tptp ?loc ?annot "tpi" id ~role (`Term t) +let thf ?loc ?annot id ~role t = tptp ?loc ?annot "thf" id ~role (`Term t) +let tff ?loc ?annot id ~role t = tptp ?loc ?annot "tff" id ~role (`Term t) +let tcf ?loc ?annot id ~role t = tptp ?loc ?annot "tcf" id ~role (`Term t) +let fof ?loc ?annot id ~role t = tptp ?loc ?annot "fof" id ~role (`Term t) + +let cnf ?loc ?annot id ~role t = let rec split_or t = match t with | { Term.term = Term.App @@ -646,6 +650,6 @@ let cnf ?loc ?annot id role t = Misc.list_concat_map split_or l | _ -> [t] in - tptp ?loc ?annot "cnf" id role (`Clause (split_or t)) + tptp ?loc ?annot "cnf" id ~role (`Clause (split_or t)) diff --git a/src/standard/statement.mli b/src/standard/statement.mli index d64f8a1ed..93f32f925 100644 --- a/src/standard/statement.mli +++ b/src/standard/statement.mli @@ -82,7 +82,7 @@ type local = { hyps: term list; goals: term list } (** Local hypothesis and consequents used by [Prove]. *) type other = { - name : Id.t; + name : term; (** The name of the statement, used to determine its semantics. For instance, it might be `plain` or `minimize`. *) args : term list; @@ -185,7 +185,7 @@ include Dolmen_intf.Stmt.Logic (** {2 Additional functions} *) -val other : ?id:Id.t -> ?loc:location -> ?attrs:term list -> Id.t -> term list -> t +val other : ?id:Id.t -> ?loc:location -> ?attrs:term list -> term -> term list -> t (** Create an 'Other' statement. *) val add_attrs : term list -> t -> t diff --git a/src/standard/term.ml b/src/standard/term.ml index 904257e65..76703462c 100644 --- a/src/standard/term.ml +++ b/src/standard/term.ml @@ -23,10 +23,13 @@ type builtin = | Lt | Leq (* arithmetic comparisons *) | Gt | Geq (* arithmetic comparisons *) + | Tuple (* Tuples *) | Subtype (* Function type constructor and subtyping relation *) | Product | Union (* Product and union of types (not set theory) *) | Pi | Sigma (* Higher-order constant to encode forall and exists quantifiers *) + | Choice (* Higher-order constant to encode choice/indefinite description binding *) + | Description (* Higher-order constant to encode definite description binding *) | Not (* Propositional negation *) | And | Or (* Conjunction and disjunction *) @@ -87,6 +90,7 @@ let infix_builtin = function | Eq | And | Or | Nand | Xor | Nor | Imply | Implied | Equiv + | Tuple | Product | Union | Sequent | Subtype | Adt_check | Adt_project | Record_access @@ -121,11 +125,14 @@ let builtin_to_string = function | Leq -> "≤" | Gt -> ">" | Geq -> "≥" + | Tuple -> "," | Subtype -> "⊂" | Product -> "*" | Union -> "∪" | Pi -> "Π" | Sigma -> "Σ" + | Choice -> "ε" + | Description -> "@" | Not -> "¬" | And -> "∧" | Or -> "∨" @@ -380,6 +387,9 @@ let implied_t = builtin Implied let pi_t = builtin Pi let sigma_t = builtin Sigma +let choice_t = builtin Choice +let description_t = builtin Description + let void = builtin Void let true_ = builtin True let false_ = builtin False @@ -388,6 +398,7 @@ let wildcard = builtin Wildcard let ite_t = builtin Ite let sequent_t = builtin Sequent +let tuple_t = builtin Tuple let union_t = builtin Union let product_t = builtin Product let subtype_t = builtin Subtype @@ -438,6 +449,7 @@ let tertiary t = (fun ?loc x y z -> apply ?loc (t ?loc ()) [x; y; z]) let eq = binary eq_t let neq = nary neq_t +let tuple = nary tuple_t (* {2 Logical connectives} *) diff --git a/src/standard/term.mli b/src/standard/term.mli index d973238cb..7e8bbdc91 100644 --- a/src/standard/term.mli +++ b/src/standard/term.mli @@ -68,6 +68,8 @@ type builtin = | Geq (** Arithmetic "greater or equal" comparison. *) + | Tuple + (** Tuples *) | Subtype (** Subtyping relation *) | Product @@ -78,7 +80,11 @@ type builtin = | Pi (** Pi: higher-order encoding of the forall quantifier as a constant. *) | Sigma - (** Sigma: higher-order envoding of the exists quantifier of a constant. *) + (** Sigma: higher-order encoding of the exists quantifier as a constant. *) + | Choice + (** Choice: higher-order encoding of the indefinite description binding as a constant. *) + | Description + (** Choice: higher-order encoding of the definite description binding as a constant. *) | Not (** Propositional negation *) diff --git a/tests/parsing/tptp/v6.3.0/flags.dune b/tests/parsing/tptp/v6.3.0/flags.dune index 8f865d4f8..761acbded 100644 --- a/tests/parsing/tptp/v6.3.0/flags.dune +++ b/tests/parsing/tptp/v6.3.0/flags.dune @@ -1 +1 @@ ---type=false +--type=false --lang=tptp-6.3.0 diff --git a/tests/parsing/tptp/v8.2.0/SYN000+1.p b/tests/parsing/tptp/v8.2.0/SYN000+1.p new file mode 100644 index 000000000..bad48e6c9 --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000+1.p @@ -0,0 +1,99 @@ +%------------------------------------------------------------------------------ +% File : SYN000+1 : TPTP v8.2.0. Released v4.0.0. +% Domain : Syntactic +% Problem : Basic TPTP FOF syntax +% Version : Biased. +% English : Basic TPTP FOF syntax that you can't survive without parsing. + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Theorem +% Rating : 0.19 v8.2.0, 0.17 v8.1.0, 0.19 v7.4.0, 0.17 v7.0.0, 0.20 v6.4.0, 0.19 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.33 v6.0.0, 0.43 v5.5.0, 0.48 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.40 v5.1.0, 0.43 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.1, 0.78 v4.0.0 +% Syntax : Number of formulae : 12 ( 5 unt; 0 def) +% Number of atoms : 31 ( 3 equ) +% Maximal formula atoms : 5 ( 2 avg) +% Number of connectives : 28 ( 9 ~; 10 |; 3 &) +% ( 1 <=>; 3 =>; 1 <=; 1 <~>) +% Maximal formula depth : 7 ( 4 avg) +% Maximal term depth : 4 ( 2 avg) +% Number of predicates : 16 ( 13 usr; 10 prp; 0-3 aty) +% Number of functors : 8 ( 8 usr; 5 con; 0-3 aty) +% Number of variables : 13 ( 5 !; 8 ?) +% SPC : FOF_THM_RFO_SEQ + +% Comments : +%------------------------------------------------------------------------------ +%----Propositional +fof(propositional,axiom, + ( ( p0 + & ~ q0 ) + => ( r0 + | ~ s0 ) ) ). + +%----First-order +fof(first_order,axiom, + ! [X] : + ( ( p(X) + | ~ q(X,a) ) + => ? [Y,Z] : + ( r(X,f(Y),g(X,f(Y),Z)) + & ~ s(f(f(f(b)))) ) ) ). + +%----Equality +fof(equality,axiom, + ? [Y] : + ! [X,Z] : + ( f(Y) = g(X,f(Y),Z) + | f(f(f(b))) != a + | X = f(Y) ) ). + +%----True and false +fof(true_false,axiom, + ( $true + | $false ) ). + +%----Quoted symbols +fof(single_quoted,axiom, + ( 'A proposition' + | 'A predicate'(a) + | p('A constant') + | p('A function'(a)) + | p('A \'quoted \\ escape\'') ) ). + +%----Connectives - seen |, &, =>, ~ already +fof(useful_connectives,axiom, + ! [X] : + ( ( p(X) + <= ~ q(X,a) ) + <=> ? [Y,Z] : + ( r(X,f(Y),g(X,f(Y),Z)) + <~> ~ s(f(f(f(b)))) ) ) ). + +%----Annotated formula names +fof(123,axiom, + ! [X] : + ( ( p(X) + | ~ q(X,a) ) + => ? [Y,Z] : + ( r(X,f(Y),g(X,f(Y),Z)) + & ~ s(f(f(f(b)))) ) ) ). + +%----Roles +fof(role_hypothesis,hypothesis, + p(h) ). + +fof(role_conjecture,conjecture, + ? [X] : p(X) ). + +%----Include directive +include('Axioms/SYN000+0.ax'). + +%----Comments +/* This + is a block + comment. +*/ + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/SYN000+2.p b/tests/parsing/tptp/v8.2.0/SYN000+2.p new file mode 100644 index 000000000..6d810768e --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000+2.p @@ -0,0 +1,97 @@ +%------------------------------------------------------------------------------ +% File : SYN000+2 : TPTP v8.2.0. Bugfixed v7.1.0. +% Domain : Syntactic +% Problem : Advanced TPTP FOF syntax +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : 0.80 v8.2.0, 0.67 v8.1.0, 0.50 v7.5.0, 1.00 v7.4.0, 0.33 v7.3.0, 0.67 v7.1.0 +% Syntax : Number of formulae : 17 ( 16 unt; 1 def) +% Number of atoms : 19 ( 2 equ) +% Maximal formula atoms : 3 ( 1 avg) +% Number of connectives : 4 ( 2 ~; 0 |; 0 &) +% ( 0 <=>; 0 =>; 0 <=; 0 <~>) +% ( 1 ~|; 1 ~&} +% Maximal formula depth : 5 ( 2 avg) +% Maximal term depth : 2 ( 1 avg) +% Number of predicates : 7 ( 6 usr; 2 prp; 0-3 aty) +% Number of functors : 10 ( 8 usr; 8 con; 0-3 aty) +% Number of variables : 8 ( 8 !; 0 ?) +% SPC : FOF_SAT_RFO_SEQ + +% Comments : +% Bugfixes : v4.0.1 - Added more numbers, particularly rationals. +% : v4.1.1 - Removed rationals with negative denominators. +% : v7.1.0 - Removed numbers +%------------------------------------------------------------------------------ +%----Quoted symbols +fof(distinct_object,axiom, + "An Apple" != "A \"Microsoft \\ escape\"" ). + +%----Connectives - seen |, &, =>, ~ already +fof(never_used_connectives,axiom, + ! [X] : + ( ( p(X) + ~| ~ q(X,a) ) + ~& p(X) ) ). + +%----Roles +fof(role_definition,definition, + ! [X] : f(d) = f(X) ). + +fof(role_assumption,assumption, + p(a) ). + +fof(role_lemma,lemma, + p(l) ). + +fof(role_theorem,theorem, + p(t) ). + +fof(role_unknown,unknown, + p(u) ). + +%----Selective include directive +include('Axioms/SYN000+0.ax',[ia1,ia3]). + +%----Source +fof(source_unknown,axiom, + ! [X] : p(X), + unknown ). + +fof(source,axiom, + ! [X] : p(X), + file('SYN000-1.p') ). + +fof(source_name,axiom, + ! [X] : p(X), + file('SYN000-1.p',source_unknown) ). + +fof(source_copy,axiom, + ! [X] : p(X), + source_unknown ). + +fof(source_introduced_assumption,axiom, + ! [X] : p(X), + introduced(assumption,[from,the,world]) ). + +fof(source_inference,axiom, + p(a), + inference(magic,[status(thm),assumptions([source_introduced_assumption])],[theory(equality),source_unknown]) ). + +fof(source_inference_with_bind,axiom, + p(a), + inference(magic,[status(thm)],[theory(equality),source_unknown:[bind(X,$fot(a))]]) ). + +%----Useful info +fof(useful_info,axiom, + ! [X] : p(X), + unknown, + [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2,"A distinct object",$fof( p(X) | ~ q(X,a) | r(X,f(Y),g(X,f(Y),Z)) | ~ s(f(f(f(b)))) ),data(name):[colon,list,2],[simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]] ). + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/SYN000-1.p b/tests/parsing/tptp/v8.2.0/SYN000-1.p new file mode 100644 index 000000000..928c23117 --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000-1.p @@ -0,0 +1,83 @@ +%------------------------------------------------------------------------------ +% File : SYN000-1 : TPTP v8.2.0. Released v4.0.0. +% Domain : Syntactic +% Problem : Basic TPTP CNF syntax +% Version : Biased. +% English : Basic TPTP CNF syntax that you can't survive without parsing. + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Unsatisfiable +% Rating : 0.10 v8.1.0, 0.16 v7.5.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.17 v7.0.0, 0.27 v6.2.0, 0.40 v6.1.0, 0.36 v6.0.0, 0.50 v5.4.0, 0.55 v5.3.0, 0.56 v5.2.0, 0.62 v5.1.0, 0.65 v5.0.0, 0.64 v4.1.0, 0.62 v4.0.1, 0.64 v4.0.0 +% Syntax : Number of clauses : 11 ( 5 unt; 6 nHn; 7 RR) +% Number of literals : 27 ( 3 equ; 8 neg) +% Maximal clause size : 5 ( 2 avg) +% Maximal term depth : 4 ( 2 avg) +% Number of predicates : 16 ( 13 usr; 10 prp; 0-3 aty) +% Number of functors : 8 ( 8 usr; 5 con; 0-3 aty) +% Number of variables : 11 ( 5 sgn) +% SPC : CNF_UNS_RFO_SEQ_NHN + +% Comments : +%------------------------------------------------------------------------------ +%----Propositional +cnf(propositional,axiom, + ( p0 + | ~ q0 + | r0 + | ~ s0 ) ). + +%----First-order +cnf(first_order,axiom, + ( p(X) + | ~ q(X,a) + | r(X,f(Y),g(X,f(Y),Z)) + | ~ s(f(f(f(b)))) ) ). + +%----Equality +cnf(equality,axiom, + ( f(Y) = g(X,f(Y),Z) + | f(f(f(b))) != a + | X = f(Y) ) ). + +%----True and false +cnf(true_false,axiom, + ( $true + | $false ) ). + +%----Quoted symbols +cnf(single_quoted,axiom, + ( 'A proposition' + | 'A predicate'(Y) + | p('A constant') + | p('A function'(a)) + | p('A \'quoted \\ escape\'') ) ). + +%----Connectives - seen them all already + +%----Annotated formula names +cnf(123,axiom, + ( p(X) + | ~ q(X,a) + | r(X,f(Y),g(X,f(Y),Z)) + | ~ s(f(f(f(b)))) ) ). + +%----Roles - seen axiom already +cnf(role_hypothesis,hypothesis, + p(h) ). + +cnf(role_negated_conjecture,negated_conjecture, + ~ p(X) ). + +%----Include directive +include('Axioms/SYN000-0.ax'). + +%----Comments +/* This + is a block + comment. +*/ + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/SYN000-2.p b/tests/parsing/tptp/v8.2.0/SYN000-2.p new file mode 100644 index 000000000..53ccfec8a --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000-2.p @@ -0,0 +1,86 @@ +%------------------------------------------------------------------------------ +% File : SYN000-2 : TPTP v8.2.0. Bugfixed v7.1.0. +% Domain : Syntactic +% Problem : Advanced TPTP CNF syntax +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : 0.80 v8.2.0, 0.78 v8.1.0, 0.86 v7.5.0, 0.88 v7.4.0, 0.70 v7.3.0, 0.56 v7.1.0 +% Syntax : Number of clauses : 16 ( 16 unt; 0 nHn; 9 RR) +% Number of literals : 16 ( 2 equ; 1 neg) +% Maximal clause size : 1 ( 1 avg) +% Maximal term depth : 2 ( 1 avg) +% Number of predicates : 7 ( 6 usr; 2 prp; 0-3 aty) +% Number of functors : 10 ( 8 usr; 8 con; 0-3 aty) +% Number of variables : 7 ( 7 sgn) +% SPC : CNF_SAT_RFO_EQU_NUE + +% Comments : +% Bugfixes : v4.0.1 - Added more numbers, particularly rationals. +% : v4.1.1 - Removed rationals with negative denominators. +% : v7.1.0 - Removed numbers +%------------------------------------------------------------------------------ +%----Quoted symbols +cnf(distinct_object,axiom, + "An Apple" != "A \"Microsoft \\ escape\"" ). + +%----Roles - seen axiom already +cnf(role_definition,definition, + f(d) = f(X) ). + +cnf(role_assumption,assumption, + p(a) ). + +cnf(role_lemma,lemma, + p(l) ). + +cnf(role_theorem,theorem, + p(t) ). + +cnf(role_unknown,unknown, + p(u) ). + +%----Selective include directive +include('Axioms/SYN000-0.ax',[ia1,ia3]). + +%----Source +cnf(source_unknown,axiom, + p(X), + unknown ). + +cnf(source,axiom, + p(X), + file('SYN000-1.p') ). + +cnf(source_name,axiom, + p(X), + file('SYN000-1.p',source_unknown) ). + +cnf(source_copy,axiom, + p(X), + source_unknown ). + +cnf(source_introduced_assumption,axiom, + p(X), + introduced(assumption,[from,the,world]) ). + +cnf(source_inference,axiom, + p(a), + inference(magic,[status(thm),assumptions([source_introduced_assumption])],[theory(equality),source_unknown]) ). + +cnf(source_inference_with_bind,axiom, + p(a), + inference(magic,[status(thm)],[theory(equality),source_unknown:[bind(X,$fot(a))]]) ). + +%----Useful info +cnf(useful_info,axiom, + p(X), + unknown, + [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2,"A distinct object",$cnf( p(X) | ~ q(X,a) | r(X,f(Y),g(X,f(Y),Z)) | ~ s(f(f(f(b)))) ),data(name):[colon,list,2],[simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]] ). + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/SYN000-3.p b/tests/parsing/tptp/v8.2.0/SYN000-3.p new file mode 100644 index 000000000..cf6d15ff2 --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000-3.p @@ -0,0 +1,84 @@ +%------------------------------------------------------------------------------ +% File : SYN000-3 : TPTP v8.2.0. Released v8.0.0. +% Domain : Syntactic +% Problem : Typed TPTP CNF syntax +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : ? v8.0.0 +% Syntax : Number of clauses : 8 ( 2 unt; 6 nHn; 4 RR) +% Number of literals : 24 ( 3 equ; 8 neg) +% Maximal clause size : 5 ( 3 avg) +% Maximal term depth : 4 ( 2 avg) +% Number of types : 1 ( 0 usr) +% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<) +% Number of predicates : 13 ( 10 usr; 7 prp; 0-3 aty) +% Number of functors : 8 ( 8 usr; 5 con; 0-3 aty) +% Number of variables : 11 ( 0 sgn 11 !; 0 ?; 11 :) +% SPC : TCF_SAT_RFO_EQU_NUE + +% Comments : +%------------------------------------------------------------------------------ +%----Propositional +tcf(propositional,axiom, + ( p0 + | ~ q0 + | r0 + | ~ s0 ) ). + +%----First-order +tcf(first_order_tcf,axiom, + ! [X: $i,Y: $i,Z: $i] : + ( p(X) + | ~ q(X,a) + | r(X,f(Y),g(X,f(Y),Z)) + | ~ s(f(f(f(b)))) ) ). + +%----Equality +tcf(equality,axiom, + ! [X: $i,Y: $i,Z: $i] : + ( f(Y) = g(X,f(Y),Z) + | f(f(f(b))) != a + | X = f(Y) ) ). + +% ( ( f(Y) = g(X,f(Y),Z) ) +% | ( f(f(f(b))) != a ) +% | ( X = f(Y) ) ) ). + +%----True and false +tcf(true_false,axiom, + ( $true + | $false ) ). + +%----Quoted symbols +tcf(single_quoted,axiom, + ! [Y: $i] : + ( 'A proposition' + | 'A predicate'(Y) + | p('A constant') + | p('A function'(a)) + | p('A \'quoted \\ escape\'') ) ). + +%----Connectives - seen them all already + +%----Annotated formula names +tcf(123,axiom, + ! [X: $i,Y: $i,Z: $i] : + ( p(X) + | ~ q(X,a) + | r(X,f(Y),g(X,f(Y),Z)) + | ~ s(f(f(f(b)))) ) ). + +%----Roles - seen axiom already +tcf(role_hypothesis,hypothesis, + p(h) ). + +tcf(role_negated_conjecture,negated_conjecture, + ! [X: $i] : ~ p(X) ). + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/SYN000^1.p b/tests/parsing/tptp/v8.2.0/SYN000^1.p new file mode 100644 index 000000000..4bc2a84a0 --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000^1.p @@ -0,0 +1,187 @@ +%------------------------------------------------------------------------------ +% File : SYN000^1 : TPTP v8.2.0. Released v3.7.0. +% Domain : Syntactic +% Problem : Basic TPTP TH0 syntax +% Version : Biased. +% English : Basic TPTP TH0 that you can't survive without parsing. + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Theorem +% Rating : 0.30 v8.2.0, 0.23 v8.1.0, 0.18 v7.5.0, 0.29 v7.4.0, 0.11 v7.2.0, 0.12 v7.0.0, 0.14 v6.4.0, 0.17 v6.3.0, 0.20 v6.2.0, 0.57 v6.1.0, 0.29 v6.0.0, 0.43 v5.5.0, 0.50 v5.4.0, 0.60 v5.1.0, 0.20 v4.1.0, 0.00 v3.7.0 +% Syntax : Number of formulae : 42 ( 8 unt; 27 typ; 0 def) +% Number of atoms : 35 ( 4 equ; 0 cnn) +% Maximal formula atoms : 5 ( 2 avg) +% Number of connectives : 96 ( 9 ~; 10 |; 3 &; 68 @) +% ( 1 <=>; 3 =>; 1 <=; 1 <~>) +% Maximal formula depth : 11 ( 5 avg) +% Number of types : 3 ( 1 usr) +% Number of type conns : 26 ( 26 >; 0 *; 0 +; 0 <<) +% Number of symbols : 29 ( 26 usr; 16 con; 0-3 aty) +% Number of variables : 18 ( 4 ^; 6 !; 8 ?; 18 :) +% SPC : TH0_THM_EQU_NAR + +% Comments : +%------------------------------------------------------------------------------ +%----Propositional +thf(p0_type,type, + p0: $o ). + +thf(q0_type,type, + q0: $o ). + +thf(r0_type,type, + r0: $o ). + +thf(s0_type,type, + s0: $o ). + +thf(propositional,axiom, + ( ( p0 + & ~ q0 ) + => ( r0 + | ~ s0 ) ) ). + +%----First-order +thf(a_type,type, + a: $i ). + +thf(b_type,type, + b: $i ). + +thf(h_type,type, + h: $i ). + +thf(f_type,type, + f: $i > $i ). + +thf(g_type,type, + g: $i > $i > $i > $i ). + +thf(p_type,type, + p: $i > $o ). + +thf(q_type,type, + q: $i > $i > $o ). + +thf(r_type,type, + r: $i > $i > $i > $o ). + +thf(s_type,type, + s: $i > $o ). + +thf(first_order,axiom, + ! [X: $i] : + ( ( ( p @ X ) + | ~ ( q @ X @ a ) ) + => ? [Y: $i,Z: $i] : + ( ( r @ X @ ( f @ Y ) @ ( g @ X @ ( f @ Y ) @ Z ) ) + & ~ ( s @ ( f @ ( f @ ( f @ b ) ) ) ) ) ) ). + +%----Equality +thf(equality,axiom, + ? [Y: $i] : + ! [X: $i,Z: $i] : + ( ( ( f @ Y ) + = ( g @ X @ ( f @ Y ) @ Z ) ) + | ( ( f @ ( f @ ( f @ b ) ) ) + != a ) + | ( X + = ( f @ Y ) ) ) ). + +%----True and false +thf(true_false,axiom, + ( $true + | $false ) ). + +thf(quoted_proposition_type,type, + 'A proposition': $o ). + +thf(quoted_predicate_type,type, + 'A predicate': $i > $o ). + +thf(quoted_constant_type,type, + 'A constant': $i ). + +thf(quoted_function_type,type, + 'A function': $i > $i ). + +thf(quoted_escape_type,type, + 'A \'quoted \\ escape\'': $i ). + +%----Quoted symbols +thf(single_quoted,axiom, + ( 'A proposition' + | ( 'A predicate' @ a ) + | ( p @ 'A constant' ) + | ( p @ ( 'A function' @ a ) ) + | ( p @ 'A \'quoted \\ escape\'' ) ) ). + +%----Connectives - seen |, &, =>, ~ already +thf(useful_connectives,axiom, + ! [X: $i] : + ( ( ( p @ X ) + <= ~ ( q @ X @ a ) ) + <=> ? [Y: $i,Z: $i] : + ( ( r @ X @ ( f @ Y ) @ ( g @ X @ ( f @ Y ) @ Z ) ) + <~> ~ ( s @ ( f @ ( f @ ( f @ b ) ) ) ) ) ) ). + +%----Lambda terms +thf(l1_type,type, + l1: $i > ( $i > $o ) > $o ). + +thf(l2_type,type, + l2: ( $i > ( $i > $i ) > $i ) > $o ). + +thf(lambda_defn,axiom, + ( l1 + = ( ^ [C: $i,P: $i > $o] : ( P @ C ) ) ) ). + +thf(lambda_use,axiom, + ( l2 + @ ^ [C: $i,F: $i > $i] : ( F @ C ) ) ). + +%----New types +thf(new_type,type, + new: $tType ). + +thf(newc_type,type, + newc: new ). + +thf(newf_type,type, + newf: new > $i > new ). + +thf(newp_type,type, + newp: new > $i > $o ). + +thf(new_axiom,axiom, + ! [X: new] : ( newp @ ( newf @ newc @ a ) @ a ) ). + +%----Annotated formula names +thf(123,axiom, + ! [X: $i] : + ( ( ( p @ X ) + | ~ ( q @ X @ a ) ) + => ? [Y: $i,Z: $i] : + ( ( r @ X @ ( f @ Y ) @ ( g @ X @ ( f @ Y ) @ Z ) ) + & ~ ( s @ ( f @ ( f @ ( f @ b ) ) ) ) ) ) ). + +%----Roles +thf(role_hypothesis,hypothesis, + p @ h ). + +thf(role_conjecture,conjecture, + ? [X: $i] : ( p @ X ) ). + +%----Include directive +include('Axioms/SYN000^0.ax'). + +%----Comments +/* This + is a block + comment. +*/ + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/SYN000^2.p b/tests/parsing/tptp/v8.2.0/SYN000^2.p new file mode 100644 index 000000000..a572491d4 --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000^2.p @@ -0,0 +1,310 @@ +%------------------------------------------------------------------------------ +% File : SYN000^2 : TPTP v8.2.0. Bugfixed v8.1.1. +% Domain : Syntactic +% Problem : Advanced TPTP TH0 syntax +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : 1.00 v8.2.0 +% Syntax : Number of formulae : 63 ( 26 unt; 27 typ; 1 def) +% Number of atoms : 76 ( 9 equ; 3 cnn) +% Maximal formula atoms : 7 ( 2 avg) +% Number of connectives : 124 ( 3 ~; 9 |; 2 &; 105 @) +% ( 0 <=>; 2 =>; 0 <=; 0 <~>) +% ( 1 ~|; 2 ~&} +% Maximal formula depth : 9 ( 4 avg) +% Number of X terms : 19 ( 5 []; 6 ite; 8 let) +% Number arithmetic : 32 ( 7 atm; 0 fun; 13 num; 12 var) +% Number of types : 6 ( 1 usr; 3 ari) +% Number of type conns : 33 ( 30 >; 3 *; 0 +; 0 <<) +% Number of symbols : 54 ( 30 usr; 31 con; 0-4 aty) +% Number of variables : 27 ( 1 ^; 23 !; 1 ?; 27 :) +% ( 0 !>; 0 ?*; 1 @-; 1 @+) +% SPC : TH0_SAT_EQU_ARI + +% Comments : +% Bugfixes : v4.0.1 - Fixed connective_terms and pi_sigma_operators so they're +% well typed. +% : v4.0.1 - Added more numbers, particularly rationals. +% : v4.1.1 - Removed rationals with negative denominators. +% : v4.1.1 - Fixed p_real_type +% : v5.5.0 - Fixed tff to thf in 4 formulae +% : v8.1.1 - Changed $ite to applications +%------------------------------------------------------------------------------ +%----Quoted symbols +thf(distinct_object,axiom, + ( "An Apple" != "A \"Microsoft \\ escape\"" ) ). +% "An Apple" != "A \"Microsoft \\ escape\"" ). + +%----Numbers +thf(p_int_type,type, + p_int: $int > $o ). + +thf(p_rat_type,type, + p_rat: $rat > $o ). + +thf(p_real_type,type, + p_real: $real > $o ). + +thf(integers,axiom, + ( ( p_int @ 123 ) + | ( p_int @ -123 ) ) ). + +thf(rationals,axiom, + ( ( p_rat @ 123/456 ) + | ( p_rat @ -123/456 ) + | ( p_rat @ 123/456 ) ) ). + +thf(reals,axiom, + ( ( p_real @ 123.456 ) + | ( p_real @ -123.456 ) + | ( p_real @ 123.456E78 ) + | ( p_real @ 123.456e78 ) + | ( p_real @ -123.456E78 ) + | ( p_real @ 123.456E-78 ) + | ( p_real @ -123.456E-78 ) ) ). + +%----Types for stuff below +thf(a_type,type, + a: $i ). + +thf(b_type,type, + b: $i ). + +thf(f_type,type, + f: $i > $i ). + +thf(g_type,type, + g: ( $i * $i ) > $i ). + +thf(h_type,type, + h: ( $i * $i * $i ) > $i ). + +thf(p_type,type, + p: $i > $o ). + +thf(q_type,type, + q: $i > $i > $o ). + +thf(tt_type,type, + tt: $tType ). + +thf(dt_type,type, + dt: + [$i,tt,$int] ). + +thf(pt_type,type, + pt: [tt,$i] > $o ). + +thf(ft_type,type, + ft: $o > [$i,tt,$int] > [tt,$i] ). + +thf(ptt_type,type, + ptt: [$int,$i,$o] > $o > $i > $o ). + +%----Tuples +thf(tuples_1,axiom, + pt @ ( ft @ $true @ dt ) ). + +thf(tuples_2,axiom, + ( p + = ( ^ [X: $i] : ( ptt @ [33,a,$true] @ ( q @ a @ b ) ) ) ) ). + +%----Types for stuff below +thf(il_type,type, + il: $int ). + +thf(jl_type,type, + jl: $int ). + +thf(fl_type,type, + fl: $int > $int > $int > $int > $rat ). + +thf(pl_type,type, + pl: $rat > $o ). + +thf(ql_type,type, + ql: $int > $int > $o ). + +thf(fll_type,type, + fll: $int > $int > $int > $int > $int ). + +thf(pll_type,type, + pll: $int > $o ). + +thf(max_type,type, + max: $int > $int > $int ). + +thf(pc_type,type, + pc: [$int,$int] > $o ). + +thf(dc_type,type, + dc: + [$int,$int] ). + +%----Conditional constructs. +thf(ite_1,axiom, + ! [X: $int,Y: $int] : ( $ite @ ( $greater @ X @ Y ) @ ( pll @ X ) @ ( pll @ Y ) ) ). + +thf(ite_2,axiom, + ! [X: $int,Y: $int] : ( pll @ ( $ite @ ( $greater @ X @ Y ) @ X @ Y ) ) ). + +thf(max_defn,axiom, + ! [X: $int,Y: $int] : + ( ( max @ X @ Y ) + = ( $ite @ ( $greatereq @ X @ Y ) @ X @ Y ) ) ). + +thf(max_property,axiom, + ! [X: $int,Y: $int] : + ( $ite + @ ( ( max @ X @ Y ) + = X ) + @ ( $greatereq @ X @ Y ) + @ ( $greatereq @ Y @ X ) ) ). + +thf(ite_tuple_1,axiom, + ! [X: $int,Y: $int] : ( pc @ ( $ite @ ( $greater @ X @ Y ) @ [X,Y] @ [Y,X] ) ) ). + +thf(ite_tuple_2,axiom, + ! [X: $int,Y: $int] : + ( dc + = ( $ite @ ( $greater @ X @ Y ) @ [X,Y] @ [Y,X] ) ) ). + +%----Let binders. +thf(let_1,axiom, + $let( + ff: $int > $int > $rat, + ff @ X @ Y:= fl @ X @ X @ Y @ Y, + pl @ ( ff @ il @ jl ) ) ). + +thf(let_2,axiom, + $let( + ff: $int > $int > $rat, + ff:= ^ [X: $int,Y: $int] : ( fl @ X @ X @ Y @ Y ), + pl @ ( ff @ il @ jl ) ) ). + +thf(let_tuple_1,axiom, + $let( + [ a: $int, + b: $int ], + [ a:= b, + b:= a ], + ql @ a @ b ) ). + +thf(let_tuple_2,axiom, + $let( + [ ff: $int > $int > $int, + gg: $int > $int ], + [ ff @ X @ Y:= fll @ X @ X @ Y @ Y, + gg @ Z:= fll @ Z @ Z @ Z @ Z ], + pll @ ( ff @ il @ ( gg @ il ) ) ) ). + +thf(let_tuple_3,axiom, + $let( + ff: $int > $int > $int, + ff @ X @ Y:= fll @ X @ X @ Y @ Y, + $let( + gg: $int > $int, + gg @ Z:= ff @ Z @ Z, + pll @ ( gg @ il ) ) ) ). + +thf(let_tuple_4,axiom, + $let( + [ a: $int, + b: $int ], + [a,b]:= + [27,28], + qll @ a @ b ) ). + +thf(let_tuple_5,axiom, + $let( + d: + [$int,$int], + d:= + [27,28], + pc @ d ) ). + +%----Connective terms +thf(connective_terms,axiom, + ! [P: $o,C: $i] : + ( ( (&) @ ( p @ C ) @ P ) + = ( (~) @ ( (~&) @ ( p @ C ) @ P ) ) ) ). + +%----Connectives - seen |, &, =>, ~ already +thf(description_choice,axiom, + ( ? [X: $i] : + ( ( p @ X ) + & ! [Y: $i] : + ( ( p @ Y ) + => ( X = Y ) ) ) + => ( ( @-[X: $i] : ( p @ X ) ) + = ( @+[X: $i] : ( p @ X ) ) ) ) ). + +thf(never_used_connectives,axiom, + ! [X: $i] : + ( ( ( p @ X ) + ~| ~ ( q @ X @ a ) ) + ~& ( p @ X ) ) ). + +%----Roles +thf(role_definition,definition, + ! [X: $i] : + ( ( f @ a ) + = ( f @ X ) ) ). + +thf(role_assumption,assumption, + p @ a ). + +thf(role_lemma,lemma, + p @ a ). + +thf(role_theorem,theorem, + p @ a ). + +thf(role_unknown,unknown, + p @ a ). + +%----Selective include directive +include('Axioms/SYN000^0.ax',[ia1_type,ia1,ia3_type,ia3]). + +%----Source +thf(source_unknown,axiom, + ! [X: $i] : ( p @ X ), + unknown ). + +thf(source,axiom, + ! [X: $i] : ( p @ X ), + file('SYN000-1.p') ). + +thf(source_name,axiom, + ! [X: $i] : ( p @ X ), + file('SYN000-1.p',source_unknown) ). + +thf(source_copy,axiom, + ! [X: $i] : ( p @ X ), + source_unknown ). + +thf(source_introduced_assumption,axiom, + ! [X: $i] : ( p @ X ), + introduced(assumption,[from,the,world]) ). + +thf(source_inference,axiom, + p @ a, + inference(magic,[status(thm),assumptions([source_introduced_assumption])],[theory(equality),source_unknown]) ). + +thf(source_inference_with_bind,axiom, + p @ a, + inference(magic,[status(thm)],[theory(equality),source_unknown:[bind(X,$fot(a))]]) ). + +%----Useful info +thf(useful_info,axiom, + ! [X: $i] : ( p @ X ), + unknown, + [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2,"A distinct object",$thf( ( p @ X ) | ~ ( q @ X @ a ) ),data(name):[colon,list,2],[simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]] ). + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/SYN000^3.p b/tests/parsing/tptp/v8.2.0/SYN000^3.p new file mode 100644 index 000000000..af4cc2ef4 --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000^3.p @@ -0,0 +1,102 @@ +%------------------------------------------------------------------------------ +% File : SYN000^3 : TPTP v8.2.0. Released v7.1.0. +% Domain : Syntactic +% Problem : TPTP TH1 syntax +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : 1.00 v7.1.0 +% Syntax : Number of formulae : 16 ( 2 unt; 11 typ; 0 def) +% Number of atoms : 12 ( 7 equ; 0 cnn) +% Maximal formula atoms : 2 ( 2 avg) +% Number of connectives : 40 ( 0 ~; 0 |; 0 &; 36 @) +% ( 0 <=>; 0 =>; 0 <=; 0 <~>) +% Maximal formula depth : 5 ( 3 avg) +% Number of types : 4 ( 2 usr) +% Number of type conns : 18 ( 18 >; 0 *; 0 +; 0 <<) +% Number of symbols : 15 ( 9 usr; 6 con; 0-5 aty; 1 @=) +% ( 1 !!; 1 ??; 1 @@+; 1 @@-) +% Number of variables : 12 ( 4 ^; 4 !; 0 ?; 12 :) +% ( 4 !>; 0 ?*; 0 @-; 0 @+) +% SPC : TH1_SAT_EQU_NAR + +% Comments : +%------------------------------------------------------------------------------ +thf(bird_type,type, + bird: $tType ). + +thf(tweety_type,type, + tweety: bird ). + +%----Type constructors +thf(list_type,type, + list: $tType > $tType ). + +thf(map_type,type, + map: $tType > $tType > $tType ). + +%----Polymorphic symbols +thf(bird_lookup_type,type, + bird_lookup: + !>[A: $tType,B: $tType] : ( ( map @ A @ B ) > A > B ) ). + +thf(bird_update_type,type, + bird_update: + !>[A: $tType,B: $tType] : ( ( map @ A @ B ) > A > B > ( map @ A @ B ) ) ). + +%----Use of polymorphic symbols +thf(bird_lookup_update_same,axiom, + ! [RangeType: $tType,Map: map @ bird @ RangeType,Key: bird,Value: RangeType] : + ( ( bird_lookup @ bird @ RangeType @ ( bird_update @ bird @ RangeType @ Map @ Key @ Value ) @ Key ) + = Value ) ). + +%----Universal and existential quantification - !! and ?? +thf(a_type,type, + a_type: $tType ). + +thf(apply_both_type,type, + apply_both: a_type > a_type ). + +thf(the_function_type,type, + the_function: a_type > a_type > a_type ). + +thf(can_prove_this,axiom, + ( !! @ a_type + @ ^ [Y: a_type] : + ( ( the_function @ Y @ Y ) + = ( apply_both @ Y ) ) ) ). + +thf(cant_prove_this,axiom, + ( ?? @ a_type + @ ^ [Y: a_type] : + ( ( the_function @ Y @ Y ) + = ( apply_both @ Y ) ) ) ). + +%----Definite and indefinite description - @@+ and @@- +thf(has_fixed_point_type,type, + has_fixed_point: a_type > a_type ). + +thf(broken_fixed_point,axiom, + ( ( has_fixed_point + @ ( @@+ @ a_type + @ ^ [Y: a_type] : + ( ( has_fixed_point @ Y ) + = Y ) ) ) + = ( @@- @ a_type + @ ^ [Y: a_type] : + ( ( has_fixed_point @ Y ) + = Y ) ) ) ). + +%----Equality - @= +thf(is_symmetric_type,type, + is_symmetric: ( ( $i > a_type ) > ( $i > a_type ) > $o ) > $o ). + +thf(is_symmetric_property,conjecture, + is_symmetric @ ( @= @ ( $i > a_type ) ) ). + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/SYN000_1.p b/tests/parsing/tptp/v8.2.0/SYN000_1.p new file mode 100644 index 000000000..8b04b6ec4 --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000_1.p @@ -0,0 +1,171 @@ +%------------------------------------------------------------------------------ +% File : SYN000_1 : TPTP v8.2.0. Released v5.0.0. +% Domain : Syntactic +% Problem : Basic TPTP TF0 syntax without arithmetic +% Version : Biased. +% English : Basic TPTP TF0 syntax that you can't survive without parsing. + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Theorem +% Rating : 0.11 v8.2.0, 0.10 v8.1.0, 0.18 v7.5.0, 0.38 v7.4.0, 0.20 v7.3.0, 0.17 v7.1.0, 0.00 v6.0.0, 0.40 v5.5.0, 0.25 v5.4.0, 0.33 v5.2.0, 0.67 v5.0.0 +% Syntax : Number of formulae : 38 ( 6 unt; 25 typ; 0 def) +% Number of atoms : 32 ( 3 equ) +% Maximal formula atoms : 5 ( 0 avg) +% Number of connectives : 28 ( 9 ~; 10 |; 3 &) +% ( 1 <=>; 3 =>; 1 <=; 1 <~>) +% Maximal formula depth : 7 ( 4 avg) +% Maximal term depth : 4 ( 2 avg) +% Number of types : 3 ( 1 usr) +% Number of type conns : 17 ( 10 >; 7 *; 0 +; 0 <<) +% Number of predicates : 17 ( 14 usr; 10 prp; 0-3 aty) +% Number of functors : 10 ( 10 usr; 6 con; 0-3 aty) +% Number of variables : 14 ( 6 !; 8 ?; 14 :) +% SPC : TF0_THM_EQU_NAR + +% Comments : +%------------------------------------------------------------------------------ +%----Propositional +tff(p0_type,type, + p0: $o ). + +tff(q0_type,type, + q0: $o ). + +tff(r0_type,type, + r0: $o ). + +tff(s0_type,type, + s0: $o ). + +tff(propositional,axiom, + ( ( p0 + & ~ q0 ) + => ( r0 + | ~ s0 ) ) ). + +%----First-order +tff(a_type,type, + a: $i ). + +tff(b_type,type, + b: $i ). + +tff(h_type,type, + h: $i ). + +tff(f_type,type, + f: $i > $i ). + +tff(g_type,type, + g: ( $i * $i * $i ) > $i ). + +tff(p_type,type, + p: $i > $o ). + +tff(q_type,type, + q: ( $i * $i ) > $o ). + +tff(r_type,type, + r: ( $i * $i * $i ) > $o ). + +tff(s_type,type, + s: $i > $o ). + +tff(first_order,axiom, + ! [X: $i] : + ( ( p(X) + | ~ q(X,a) ) + => ? [Y: $i,Z: $i] : + ( r(X,f(Y),g(X,f(Y),Z)) + & ~ s(f(f(f(b)))) ) ) ). + +%----Equality +tff(equality,axiom, + ? [Y: $i] : + ! [X: $i,Z: $i] : + ( ( f(Y) = g(X,f(Y),Z) ) + | ( f(f(f(b))) != a ) + | ( X = f(Y) ) ) ). + +%----True and false +tff(true_false,axiom, + ( $true + | $false ) ). + +tff(quoted_proposition_type,type, + 'A proposition': $o ). + +tff(quoted_predicate_type,type, + 'A predicate': $i > $o ). + +tff(quoted_constant_type,type, + 'A constant': $i ). + +tff(quoted_function_type,type, + 'A function': $i > $i ). + +tff(quoted_escape_type,type, + 'A \'quoted \\ escape\'': $i ). + +%----Quoted symbols +tff(single_quoted,axiom, + ( 'A proposition' + | 'A predicate'(a) + | p('A constant') + | p('A function'(a)) + | p('A \'quoted \\ escape\'') ) ). + +%----Connectives - seen |, &, =>, ~ already +tff(useful_connectives,axiom, + ! [X: $i] : + ( ( p(X) + <= ~ q(X,a) ) + <=> ? [Y: $i,Z: $i] : + ( r(X,f(Y),g(X,f(Y),Z)) + <~> ~ s(f(f(f(b)))) ) ) ). + +%----New types +tff(new_type,type, + new: $tType ). + +tff(newc_type,type, + newc: new ). + +tff(newf_type,type, + newf: ( new * $i ) > new ). + +tff(newp_type,type, + newp: ( new * $i ) > $o ). + +tff(new_axiom,axiom, + ! [X: new] : newp(newf(newc,a),a) ). + +%----Annotated formula names +tff(123,axiom, + ! [X: $i] : + ( ( p(X) + | ~ q(X,a) ) + => ? [Y: $i,Z: $i] : + ( r(X,f(Y),g(X,f(Y),Z)) + & ~ s(f(f(f(b)))) ) ) ). + +%----Roles +tff(role_hypothesis,hypothesis, + p(h) ). + +tff(role_conjecture,conjecture, + ? [X: $i] : p(X) ). + +%----Include directive +include('Axioms/SYN000_0.ax'). + +%----Comments +/* This + is a block + comment. +*/ + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/SYN000_2.p b/tests/parsing/tptp/v8.2.0/SYN000_2.p new file mode 100644 index 000000000..a6569edc7 --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000_2.p @@ -0,0 +1,119 @@ +%------------------------------------------------------------------------------ +% File : SYN000_2 : TPTP v8.2.0. Bugfixed v5.5.1. +% Domain : Syntactic +% Problem : Advanced TPTP TF0 syntax without arithmetic +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : 0.67 v8.2.0, 1.00 v7.4.0, 0.67 v7.2.0, 1.00 v6.0.0 +% Syntax : Number of formulae : 24 ( 16 unt; 7 typ; 1 def) +% Number of atoms : 19 ( 2 equ) +% Maximal formula atoms : 3 ( 0 avg) +% Number of connectives : 4 ( 2 ~; 0 |; 0 &) +% ( 0 <=>; 0 =>; 0 <=; 0 <~>) +% ( 1 ~|; 1 ~&} +% Maximal formula depth : 5 ( 2 avg) +% Maximal term depth : 2 ( 1 avg) +% Number of types : 2 ( 0 usr) +% Number of type conns : 9 ( 5 >; 4 *; 0 +; 0 <<) +% Number of predicates : 5 ( 4 usr; 2 prp; 0-2 aty) +% Number of functors : 7 ( 5 usr; 4 con; 0-3 aty) +% Number of variables : 8 ( 8 !; 0 ?; 8 :) +% SPC : TF0_SAT_EQU_NAR + +% Comments : +% Bugfixes : v5.5.1 - Fixed let_binders. +%------------------------------------------------------------------------------ +%----Quoted symbols +tff(distinct_object,axiom, + "An Apple" != "A \"Microsoft \\ escape\"" ). + +%----Types for stuff below +tff(a_type,type, + a: $i ). + +tff(b_type,type, + b: $i ). + +tff(f_type,type, + f: $i > $i ). + +tff(g_type,type, + g: ( $i * $i ) > $i ). + +tff(h_type,type, + h: ( $i * $i * $i ) > $i ). + +tff(p_type,type, + p: $i > $o ). + +tff(q_type,type, + q: ( $i * $i ) > $o ). + +%----Rare connectives +tff(never_used_connectives,axiom, + ! [X: $i] : + ( ( p(X) + ~| ~ q(X,a) ) + ~& p(X) ) ). + +%----Roles +tff(role_definition,definition, + ! [X: $i] : f(a) = f(X) ). + +tff(role_assumption,assumption, + p(a) ). + +tff(role_lemma,lemma, + p(a) ). + +tff(role_theorem,theorem, + p(a) ). + +tff(role_unknown,unknown, + p(a) ). + +%----Selective include directive +include('Axioms/SYN000_0.ax',[ia1,ia3]). + +%----Source +tff(source_unknown,axiom, + ! [X: $i] : p(X), + unknown ). + +tff(source,axiom, + ! [X: $i] : p(X), + file('SYN000-1.p') ). + +tff(source_name,axiom, + ! [X: $i] : p(X), + file('SYN000-1.p',source_unknown) ). + +tff(source_copy,axiom, + ! [X: $i] : p(X), + source_unknown ). + +tff(source_introduced_assumption,axiom, + ! [X: $i] : p(X), + introduced(assumption,[from,the,world]) ). + +tff(source_inference,axiom, + p(a), + inference(magic,[status(thm),assumptions([source_introduced_assumption])],[theory(equality),source_unknown]) ). + +tff(source_inference_with_bind,axiom, + p(a), + inference(magic,[status(thm)],[theory(equality),source_unknown:[bind(X,$fot(a))]]) ). + +%----Useful info +tff(useful_info,axiom, + ! [X: $i] : p(X), + unknown, + [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2,"A distinct object",$tff( p(X) | ~ ( q(X,a) ) ),data(name):[colon,list,2],[simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]] ). + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/SYN000_3.p b/tests/parsing/tptp/v8.2.0/SYN000_3.p new file mode 100644 index 000000000..6e0f3e36f --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000_3.p @@ -0,0 +1,86 @@ +%------------------------------------------------------------------------------ +% File : SYN000_3 : TPTP v8.2.0. Released v7.1.0. +% Domain : Syntactic +% Problem : TPTP TF1 syntax +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : 0.86 v8.1.0, 1.00 v7.5.0, 0.93 v7.4.0, 1.00 v7.1.0 +% Syntax : Number of formulae : 14 ( 2 unt; 10 typ; 0 def) +% Number of atoms : 6 ( 5 equ) +% Maximal formula atoms : 2 ( 0 avg) +% Number of connectives : 3 ( 1 ~; 0 |; 0 &) +% ( 0 <=>; 2 =>; 0 <=; 0 <~>) +% Maximal formula depth : 9 ( 6 avg) +% Maximal term depth : 3 ( 1 avg) +% Number of types : 3 ( 2 usr) +% Number of type conns : 12 ( 7 >; 5 *; 0 +; 0 <<) +% Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty) +% Number of functors : 7 ( 7 usr; 1 con; 0-5 aty) +% Number of variables : 22 ( 17 !; 0 ?; 22 :) +% ( 5 !>; 0 ?*; 0 @-; 0 @+) +% SPC : TF1_SAT_EQU_NAR + +% Comments : +%------------------------------------------------------------------------------ +tff(beverage_type,type, + beverage: $tType ). + +tff(syrup_type,type, + syrup: $tType ). + +%----Type constructor +tff(cup_of_type,type, + cup_of: $tType > $tType ). + +tff(full_cup_type,type, + full_cup: beverage > cup_of(beverage) ). + +tff(coffee_type,type, + coffee: beverage ). + +tff(help_stay_awake_type,type, + help_stay_awake: cup_of(beverage) > $o ). + +%----Polymorphic symbol +tff(mixture_type,type, + mixture: + !>[BeverageOrSyrup: $tType] : ( ( BeverageOrSyrup * syrup ) > BeverageOrSyrup ) ). + +%----Use of polymorphic symbol +tff(mixture_of_coffee_help_stay_awake,axiom, + ! [S: syrup] : help_stay_awake(full_cup(mixture(beverage,coffee,S))) ). + +%----Type constructor +tff(map,type, + map: ( $tType * $tType ) > $tType ). + +%----Polymorphic symbols +tff(lookup,type, + lookup: + !>[A: $tType,B: $tType] : ( ( map(A,B) * A ) > B ) ). + +tff(update,type, + update: + !>[A: $tType,B: $tType] : ( ( map(A,B) * A * B ) > map(A,B) ) ). + +%----Use of polymorphic symbols +tff(lookup_update_same,axiom, + ! [A: $tType,B: $tType,M: map(A,B),K: A,V: B] : lookup(A,B,update(A,B,M,K,V),K) = V ). + +tff(lookup_update_diff,axiom, + ! [A: $tType,B: $tType,M: map(A,B),V: B,K: A,L: A] : + ( ( K != L ) + => ( lookup(A,B,update(A,B,M,K,V),L) = lookup(A,B,M,L) ) ) ). + +tff(map_ext,axiom, + ! [A: $tType,B: $tType,M: map(A,B),N: map(A,B)] : + ( ! [K: A] : lookup(A,B,M,K) = lookup(A,B,N,K) + => ( M = N ) ) ). + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/SYN000_4.p b/tests/parsing/tptp/v8.2.0/SYN000_4.p new file mode 100644 index 000000000..632ee796e --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000_4.p @@ -0,0 +1,202 @@ +%------------------------------------------------------------------------------ +% File : SYN000_4 : TPTP v8.2.0. Released v7.1.0. +% Domain : Syntactic +% Problem : TPTP TXF syntax +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : ? v7.1.0 +% Syntax : Number of formulae : 43 ( 13 unt; 28 typ; 0 def) +% Number of atoms : 35 ( 4 equ) +% Maximal formula atoms : 3 ( 0 avg) +% Number of connectives : 2 ( 2 ~; 0 |; 0 &) +% ( 0 <=>; 0 =>; 0 <=; 0 <~>) +% Maximal formula depth : 4 ( 2 avg) +% Maximal term depth : 3 ( 1 avg) +% Number of FOOLs : 16 ( 16 fml; 0 var) +% Number of X terms : 16 ( 6 []; 6 ite; 4 let) +% Number arithmetic : 24 ( 7 atm; 0 fun; 3 num; 14 var) +% Number of types : 5 ( 1 usr; 2 ari) +% Number of type conns : 33 ( 18 >; 15 *; 0 +; 0 <<) +% Number of predicates : 21 ( 17 usr; 4 prp; 0-3 aty) +% Number of functors : 18 ( 16 usr; 10 con; 0-4 aty) +% Number of variables : 16 ( 16 !; 0 ?; 16 :) +% SPC : TX0_SAT_EQU_ARI + +% Comments : +%------------------------------------------------------------------------------ +%----Formulae as terms +tff(p1_type,type, + p1: ( $i * $o * $int ) > $o ). + +tff(q1_type,type, + q1: ( $int * $i ) > $o ). + +tff(me_type,type, + me: $i ). + +tff(fool_1,axiom, + ! [X: $int] : + p1(me, + ! [Y: $i] : q1(X,Y), + 27) ). + +tff(p2_type,type, + p2: $i > $o ). + +tff(q2_type,type, + q2: $o > $o ). + +tff(fool_2,axiom, + q2(~ p2(me) != q2($true)) ). + +%----Tuples +tff(tt_type,type, + tt: $tType ). + +tff(a_type,type, + a: $i ). + +tff(at_type,type, + at: tt ). + +tff(dt_type,type, + dt: + [$i,tt,$i] ). + +tff(pt_type,type, + pt: [tt,$i] > $o ). + +tff(ft_type,type, + ft: ( $i * [$i,tt,$i] ) > [tt,$i] ). + +tff(tuple_1,axiom, + pt(ft(a,dt)) ). + +tff(tuple_2,axiom, + pt(ft(a,[a,at,a])) ). + +%----Tuples with Booleans +tff(pt1_type,type, + pt1: ( [$int,$i,$o] * $o * $int ) > $o ). + +tff(qt1_type,type, + qt1: ( $int * $i ) > $o ). + +tff(tuples_1,axiom, + ! [X: $int] : + pt1([33,me,$true], + ! [Y: $i] : qt1(X,Y), + 27) ). + +%----Conditional expressions +tff(pc1_type,type, + pc1: $int > $o ). + +tff(qc1_type,type, + qc1: $int > $o ). + +tff(max_type,type, + max: ( $int * $int ) > $int ). + +tff(ite_1,axiom, + ! [X: $int,Y: $int] : + $ite($greater(X,Y),pc1(X),pc1(Y)) ). + +tff(ite_2,axiom, + ! [X: $int,Y: $int] : + qc1($ite($greater(X,Y),X,Y)) ). + +tff(max_defn,axiom, + ! [X: $int,Y: $int] : + max(X,Y) = $ite($greatereq(X,Y),X,Y) ). + +tff(max_property,axiom, + ! [X: $int,Y: $int] : + $ite(max(X,Y) = X,$greatereq(X,Y),$greatereq(Y,X)) ). + +%----Conditional expressions with tuples +tff(pct1_type,type, + pct1: [$int,$int] > $o ). + +tff(dct1_type,type, + dct1: + [$int,$int] ). + +tff(ite_3,axiom, + ! [X: $int,Y: $int] : + pct1($ite($greater(X,Y),[X,Y],[Y,X])) ). + +tff(ite_4,axiom, + ! [X: $int,Y: $int] : + dct1 = $ite($greater(X,Y),[X,Y],[Y,X]) ). + +%----Let expressions +tff(pl1_type,type, + pl1: $int > $o ). + +tff(let_1,axiom, + $let( + c: $int, + c:= 27, + pl1(c) ) ). + +tff(il2_type,type, + il2: $int ). + +tff(jl2_type,type, + jl2: $int ). + +tff(fl2_type,type, + fl2: ( $int * $int * $int * $int ) > $rat ). + +tff(pl2_type,type, + pl2: $rat > $o ). + +tff(let_2,axiom, + $let( + ff: ( $int * $int ) > $rat, + ff(X,Y):= fl2(X,X,Y,Y), + pl2(ff(il2,jl2)) ) ). + +%----Let expression with tuples (and shadowing) +tff(al3_type,type, + al3: $int ). + +tff(bl3_type,type, + bl3: $int ). + +tff(pl3_type,type, + pl3: ( $int * $int ) > $o ). + +tff(let_tuple_1,axiom, + $let( + [ al3: $int, + bl3: $int ], + [ al3:= bl3, + bl3:= al3 ], + pl3(al3,bl3) ) ). + +tff(il4_type,type, + il4: $int ). + +tff(fl4_type,type, + fl4: ( $int * $int * $int * $int ) > $int ). + +tff(pl4_type,type, + pl4: $int > $o ). + +tff(let_tuple_2,axiom, + $let( + [ ff: ( $int * $int ) > $int, + gg: $int > $int ], + [ ff(X,Y):= fl4(X,X,Y,Y), + gg(Z):= fl4(Z,Z,Z,Z) ], + pl4(ff(il4,gg(il4))) ) ). + +%------------------------------------------------------------------------------- diff --git a/tests/parsing/tptp/v8.2.0/SYN000_5.p b/tests/parsing/tptp/v8.2.0/SYN000_5.p new file mode 100644 index 000000000..9f966cee4 --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/SYN000_5.p @@ -0,0 +1,310 @@ +%------------------------------------------------------------------------------ +% File : SYN000_5 : TPTP v8.2.0. Bugfixed v5.5.1. +% Domain : Syntactic +% Problem : TF0 syntax with arithmetic +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Theorem +% Rating : 0.62 v7.5.0, 0.60 v7.4.0, 0.62 v7.3.0, 0.67 v7.0.0, 0.57 v6.4.0, 0.33 v6.3.0, 0.71 v6.2.0, 1.00 v6.0.0 +% Syntax : Number of formulae : 83 ( 70 unt; 6 typ; 0 def) +% Number of atoms : 91 ( 4 equ) +% Maximal formula atoms : 7 ( 1 avg) +% Number of connectives : 14 ( 0 ~; 10 |; 1 &) +% ( 0 <=>; 3 =>; 0 <=; 0 <~>) +% Maximal formula depth : 7 ( 1 avg) +% Maximal term depth : 3 ( 1 avg) +% Number arithmetic : 196 ( 19 atm; 54 fun; 109 num; 14 var) +% Number of types : 4 ( 0 usr; 3 ari) +% Number of type conns : 3 ( 3 >; 0 *; 0 +; 0 <<) +% Number of predicates : 10 ( 3 usr; 0 prp; 1-2 aty) +% Number of functors : 41 ( 3 usr; 24 con; 0-2 aty) +% Number of variables : 14 ( 3 !; 11 ?; 14 :) +% SPC : TF0_THM_EQU_ARI + +% Comments : +% Bugfixes : v5.5.1 - Removed $evaleq. +%------------------------------------------------------------------------------ +%----Types for what follows +tff(p_int_type,type, + p_int: $int > $o ). + +tff(p_rat_type,type, + p_rat: $rat > $o ). + +tff(p_real_type,type, + p_real: $real > $o ). + +tff(a_int,type, + a_int: $int ). + +tff(a_rat,type, + a_rat: $rat ). + +tff(a_real,type, + a_real: $real ). + +%----Numbers +tff(integers,axiom, + ( p_int(123) + | p_int(-123) ) ). + +tff(rationals,axiom, + ( p_rat(123/456) + | p_rat(-123/456) + | p_rat(123/456) ) ). + +tff(reals,axiom, + ( p_real(123.456) + | p_real(-123.456) + | p_real(123.456E78) + | p_real(123.456e78) + | p_real(-123.456E78) + | p_real(123.456E-78) + | p_real(-123.456E-78) ) ). + +%----Variables +tff(variables_int,axiom, + ! [X: $int] : + ? [Y: $int] : + ( p_int(X) + => p_int(Y) ) ). + +tff(variables_rat,axiom, + ! [X: $rat] : + ? [Y: $rat] : + ( p_rat(X) + => p_rat(Y) ) ). + +tff(variables_real,axiom, + ! [X: $real] : + ? [Y: $real] : + ( p_real(X) + => p_real(Y) ) ). + +%----Arithmetic relations +tff(less_int,axiom, + $less(a_int,3) ). + +tff(less_rat,axiom, + $less(a_rat,3/9) ). + +tff(less_real,axiom, + $less(a_real,3.3) ). + +tff(lesseq_int,axiom, + $lesseq(a_int,3) ). + +tff(lesseq_rat,axiom, + $lesseq(a_rat,3/9) ). + +tff(lesseq_real,axiom, + $lesseq(a_real,3.3) ). + +tff(greater_int,axiom, + $greater(a_int,-3) ). + +tff(greater_rat,axiom, + $greater(a_rat,-3/9) ). + +tff(greater_real,axiom, + $greater(a_real,-3.3) ). + +tff(greatereq_int,axiom, + $greatereq(a_int,-3) ). + +tff(greatereq_rat,axiom, + $greatereq(a_rat,-3/9) ). + +tff(greatereq_real,axiom, + $greatereq(a_real,-3.3) ). + +tff(equal_int,axiom, + a_int = 0 ). + +tff(equal_rat,axiom, + a_rat = 0/1 ). + +tff(equal_real,axiom, + a_real = 0.0 ). + +%----Arithmetic functions +tff(uminus_int,axiom, + p_int($uminus(3)) ). + +tff(uminus_rat,axiom, + p_rat($uminus(3/9)) ). + +tff(uminus_real,axiom, + p_real($uminus(3.3)) ). + +tff(sum_int,axiom, + p_int($sum(3,3)) ). + +tff(sum_rat,axiom, + p_rat($sum(3/9,3/9)) ). + +tff(sum_real,axiom, + p_real($sum(3.3,3.3)) ). + +tff(difference_int,axiom, + p_int($difference(3,3)) ). + +tff(difference_rat,axiom, + p_rat($difference(3/9,3/9)) ). + +tff(difference_real,axiom, + p_real($difference(3.3,3.3)) ). + +tff(product_int,axiom, + p_int($product(3,3)) ). + +tff(product_rat,axiom, + p_rat($product(3/9,3/9)) ). + +tff(product_real,axiom, + p_real($product(3.3,3.3)) ). + +tff(quotient_rat,axiom, + p_rat($quotient(3/9,3/9)) ). + +tff(quotient_real,axiom, + p_real($quotient(3.3,3.3)) ). + +tff(quotient_e_int,axiom, + p_int($quotient_e(3,3)) ). + +tff(quotient_e_rat,axiom, + p_rat($quotient_e(3/9,3/9)) ). + +tff(quotient_e_real,axiom, + p_real($quotient_e(3.3,3.3)) ). + +tff(quotient_t_int,axiom, + p_int($quotient_t(3,3)) ). + +tff(quotient_t_rat,axiom, + p_rat($quotient_t(3/9,3/9)) ). + +tff(quotient_t_real,axiom, + p_real($quotient_t(3.3,3.3)) ). + +tff(quotient_f_int,axiom, + p_int($quotient_f(3,3)) ). + +tff(quotient_f_rat,axiom, + p_rat($quotient_f(3/9,3/9)) ). + +tff(quotient_f_real,axiom, + p_real($quotient_f(3.3,3.3)) ). + +tff(remainder_e_int,axiom, + p_int($remainder_e(3,3)) ). + +tff(remainder_e_rat,axiom, + p_rat($remainder_e(3/9,3/9)) ). + +tff(remainder_e_real,axiom, + p_real($remainder_e(3.3,3.3)) ). + +tff(remainder_t_int,axiom, + p_int($remainder_t(3,3)) ). + +tff(remainder_t_rat,axiom, + p_rat($remainder_t(3/9,3/9)) ). + +tff(remainder_t_real,axiom, + p_real($remainder_t(3.3,3.3)) ). + +tff(remainder_f_int,axiom, + p_int($remainder_f(3,3)) ). + +tff(remainder_f_rat,axiom, + p_rat($remainder_f(3/9,3/9)) ). + +tff(remainder_f_real,axiom, + p_real($remainder_f(3.3,3.3)) ). + +tff(floor_int,axiom, + p_int($floor(3)) ). + +tff(floor_rat,axiom, + p_rat($floor(3/9)) ). + +tff(floor_real,axiom, + p_real($floor(3.3)) ). + +tff(ceiling_int,axiom, + p_int($ceiling(3)) ). + +tff(ceiling_rat,axiom, + p_rat($ceiling(3/9)) ). + +tff(ceiling_real,axiom, + p_real($ceiling(3.3)) ). + +tff(truncate_int,axiom, + p_int($truncate(3)) ). + +tff(truncate_rat,axiom, + p_rat($truncate(3/9)) ). + +tff(truncate_real,axiom, + p_real($truncate(3.3)) ). + +%----Recognizing numbers +tff(is_int_int,axiom, + ? [X: $int] : $is_int(X) ). + +tff(is_int_rat,axiom, + ? [X: $rat] : $is_int(X) ). + +tff(is_int_real,axiom, + ? [X: $real] : $is_int(X) ). + +tff(is_rat_rat,axiom, + ? [X: $rat] : $is_rat(X) ). + +tff(is_rat_real,axiom, + ? [X: $real] : $is_rat(X) ). + +%----Coercion +tff(to_int_int,axiom, + p_int($to_int(3)) ). + +tff(to_int_rat,axiom, + p_int($to_int(3/9)) ). + +tff(to_int_real,axiom, + p_int($to_int(3.3)) ). + +tff(to_rat_int,axiom, + p_rat($to_rat(3)) ). + +tff(to_rat_rat,axiom, + p_rat($to_rat(3/9)) ). + +tff(to_rat_real,axiom, + p_rat($to_rat(3.3)) ). + +tff(to_real_int,axiom, + p_real($to_real(3)) ). + +tff(to_real_rat,axiom, + p_real($to_real(3/9)) ). + +tff(to_real_real,axiom, + p_real($to_real(3.3)) ). + +%----A conjecture to prove +tff(mixed,conjecture, + ? [X: $int,Y: $rat,Z: $real] : + ( ( Y = $to_rat($sum(X,2)) ) + & ( $less($to_int(Y),3) + | $greater($to_real(Y),3.3) ) ) ). + +%------------------------------------------------------------------------------ diff --git a/tests/parsing/tptp/v8.2.0/flags b/tests/parsing/tptp/v8.2.0/flags new file mode 100644 index 000000000..391acee8b --- /dev/null +++ b/tests/parsing/tptp/v8.2.0/flags @@ -0,0 +1 @@ +--lang=tptp-8.2.0