Correct lambdapi and dedukti outputs for GDV (#53)

* Take -gdv into account also for the Dedukti output

* Add requirements in the lambdapi output even when the -gdv flag is on

Author: gburel

dkprint.ml

@@ -77,8 +77,13 @@ and print_dk_cst o t =
      if Mltoll.is_meta s then fprintf o "zenon.select (zenon.iota)"
      else
        begin
-         if !Globals.signature_name = "" then fprintf o "%s" (escape_name s)
-         else fprintf o "%s.%s" !Globals.signature_name (escape_name s);
+         let prefix =
+         if !Globals.signature_name = "" then
+           if !Globals.gdv then "Signature."
+           else ""
+         else !Globals.signature_name ^ "."
+         in
+         fprintf o "%s%s" prefix  (escape_name s);
          if !Globals.conjecture <> ""
             && not !Globals.check_axiom && Typetptp.is_axiom s then
            fprintf o " __negated_conjecture_proof__"

lltodk.ml

@@ -1034,9 +1034,9 @@ let output oc phrases llp =
   let prooftree = extract_prooftree llp in
   let dkproof = make_proof_term (List.hd goal) prooftree in
   fprintf oc "#REQUIRE zenon;\n\n";
-  if !Globals.signature_name = "" then List.iter (print_line oc) dksigs;
+  if !Globals.ctx_flag then List.iter (print_line oc) dksigs;
   fprintf oc "\n";
-  if !Globals.signature_name = "" then List.iter (print_line oc) dkctx;
+  if !Globals.ctx_flag then List.iter (print_line oc) dkctx;
   fprintf oc "\n";
   List.iter (print_line oc) dkrules;
   fprintf oc "\n";
@@ -1062,18 +1062,18 @@ let output_term oc phrases _ llp =
   let dkproof = make_proof_term (List.hd goal) prooftree in
   fprintf oc "#REQUIRE zenon.\n";
   let sig_name = !Globals.signature_name in
-  if sig_name <> "" then
-    begin
+  if sig_name <> "" then begin
       fprintf oc "#REQUIRE %s.\n" !Globals.signature_name;
-      fprintf oc "\n[] %s.%s --> " !Globals.signature_name goal_name
-    end
+      fprintf oc "\n[] %s.%s --> " !Globals.signature_name goal_name end
+  else if !Globals.gdv then
+    fprintf oc "\n[] Signature.%s --> " goal_name
   else fprintf oc "\n[] %s --> " goal_name;
   if !Globals.conjecture <> "" then
     fprintf oc "__negated_conjecture_proof__ : \
                 zenon.proof (zenon.not %slambdapi__conjecture) =>\n"
-      (if sig_name <> "" then sig_name^"." else "");
+      (if sig_name <> "" then sig_name^"." else if !Globals.gdv then "Signature." else "");
   fprintf oc "zenon.nnpp (%a)\n(%a)"
     print_dk_term dkgoal print_dk_term dkproof;
-  if sig_name <> "" then fprintf oc ".";
+  if !Globals.gdv then fprintf oc ".";
   fprintf oc "\n";
   []

lltolp.ml

@@ -1059,13 +1059,12 @@ let output_term oc phrases _ llp =
   let prooftree = extract_prooftree llp in
   let goal_name = (List.hd llp).name in
   let dkproof = make_proof_term (List.hd goal) prooftree in
+  fprintf oc "require open Stdlib.Prop Stdlib.Set Stdlib.Eq Stdlib.FOL \
+              Logic.Zenon.Main;\n";
   if !Globals.gdv then
     fprintf oc "\nrule F.%s ↪ " goal_name
-  else begin
-      fprintf oc "require open Stdlib.Prop Stdlib.Set Stdlib.Eq Stdlib.FOL \
-                  Logic.Zenon.Main;\n";
-      fprintf oc "\nsymbol %s ≔ " goal_name
-    end;
+  else
+      fprintf oc "\nsymbol %s ≔ " goal_name;
   if !Globals.conjecture <> "" then
     fprintf oc "λ __negated_conjecture_proof__,";
   begin

main.ml

@@ -218,7 +218,7 @@ let argspec = [
   "-sig", Arg.String (fun s -> Globals.signature_name := s),
               "<n>            set the module path of the signature";
   "-gdv", Arg.Set Globals.gdv,
-              " use the format expected by GDV for the lambdapi output";
+              " use the format expected by GDV for the lambdapi and dedukti outputs";
   "-odkterm", Arg.Unit (fun () -> proof_level := Proof_dkterm;
 				  opt_level := 0;
 				  Globals.output_dk := true),