[WIP] Add Tptp v8.2

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

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)

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",

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

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} *)

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:

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})))
 )
 

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
 

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)
 )

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:

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