lltodk: use signature_name.conjecture (#50)

Author: fblanqui

.github/workflows/main.yml

@@ -8,7 +8,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        ocaml-version: [5.2.0, 5.1.1, 5.0.0, 4.14.1, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1]
+        ocaml-version: [5.4.1, 5.3.0, 5.2.1, 4.14.2] #5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1]
     runs-on: ubuntu-latest
     steps:
       - name: checking out lambdapi repo ...

dune-project

@@ -16,4 +16,6 @@
 method, generating Coq, Dedukti or Lambdapi proofs.")
  (depends
   (ocaml (>= 4.08.0))
+  ocamlfind
+  zarith
 ))

lltodk.ml

@@ -1061,17 +1061,19 @@ let output_term oc phrases _ llp =
   let goal_name = (List.hd llp).name in
   let dkproof = make_proof_term (List.hd goal) prooftree in
   fprintf oc "#REQUIRE zenon.\n";
-  if !Globals.signature_name <> "" then
+  let sig_name = !Globals.signature_name in
+  if sig_name <> "" then
     begin
       fprintf oc "#REQUIRE %s.\n" !Globals.signature_name;
       fprintf oc "\n[] %s.%s --> " !Globals.signature_name goal_name
     end
   else fprintf oc "\n[] %s --> " goal_name;
   if !Globals.conjecture <> "" then
     fprintf oc "__negated_conjecture_proof__ : \
-                zenon.proof (zenon.not Signature.conjecture) =>\n";
+                zenon.proof (zenon.not %slambdapi__conjecture) =>\n"
+      (if sig_name <> "" then sig_name^"." else "");
   fprintf oc "zenon.nnpp (%a)\n(%a)"
     print_dk_term dkgoal print_dk_term dkproof;
-  if !Globals.signature_name <> "" then fprintf oc ".";
+  if sig_name <> "" then fprintf oc ".";
   fprintf oc "\n";
   []

lpprint.ml

@@ -123,7 +123,7 @@ and print_dk_cst typ o (t, var_context) =
 
 and print_dk_term_aux o (t, var_context) =
   match t with
-  | Dkvar (v, t) as var ->
+  | Dkvar (_, t) as var ->
     let pvar = (escape_name (get_var_newname var)) in
     if not (List.mem pvar var_context)
     then fprintf o "select (%a)" print_dk_zentype_aux (t, var_context)

main.ml

@@ -11,12 +11,12 @@ open Expr;;
    https://tptp.org/cgi-bin/SeeTPTP?Category=Documents&File=SZSOntology
 *)
 type szs_success =
-    Success
+    Success [@warning "-37"]
   | Theorem
   | Unsatisfiable
 
 type szs_error =
-    NoSuccess
+    NoSuccess [@warning "-37"]
   | Unknown
   | ResourceOut
   | GaveUp

zenon_modulo.opam

@@ -12,9 +12,9 @@ bug-reports: "https://github.com/Deducteam/zenon_modulo/issues"
 depends: [
   "dune" {>= "3.7"}
   "ocaml" {>= "4.08.0"}
-  "odoc" {with-doc}
   "ocamlfind"
   "zarith"
+  "odoc" {with-doc}
 ]
 build: [
   ["dune" "subst"] {dev}