fix dk output

Makefile

@@ -41,7 +41,7 @@ SOURCES = log.ml version.ml config.dummy misc.ml heap.ml globals.ml error.ml \
 
 COQSRC = zenon.v zenon_coqbool.v zenon_equiv.v zenon_induct.v zenon_focal.v zenon_arith.v zenon_arith_reals.v
 
-DKSRC = cc.dk dk_bool.dk dk_logic.dk dk_tuple.dk basics_minimal.dk zen.dk zenon_focal.dk
+DKSRC = cc.dk dk_bool.dk dk_logic.dk dk_tuple.dk basics_minimal.dk zen.dk zenon_focal.dk zenon.dk
 
 DOCSRC =
 

dkprint.ml

@@ -1,10 +1,56 @@
 open Printf
 open Dkterm
 
+(* taken on 19/07/24 from
+https://github.com/Deducteam/Dedukti/blob/master/parsing/lexer.mll *)
+let forbidden_idents = [
+  "(;"
+  ; ";)"
+  ; "."
+  ; ","
+  ; ":"
+  ; "=="
+  ; "["
+  ; "]"
+  ; "{"
+  ; "}"
+  ; "("
+  ; ")"
+  ; "-->"
+  ; "->"
+  ; "=>"
+  ; ":="
+  ; "Type"
+  ; "def"
+  ; "defac"
+  ; "defacu"
+  ; "injective"
+  ; "thm"
+  ; "private"
+  ; "require"
+  ; "assert"
+  ; "#NAME"
+  ; "#REQUIRE"
+  ; "#EVAL"
+  ; "#INFER"
+  ; "#CHECK"
+  ; "#CHECKNOT"
+  ; "#ASSERT"
+  ; "#ASSERTNOT"
+  ; "#PRINT"
+  ; "#GDT"
+  ]
+
+let escape_name s =
+  let id_regex = Str.regexp "^[a-zA-Z_][a-zA-Z0-9_]*$" in
+  if Str.string_match id_regex s 0
+    && List.for_all ((<>) s) forbidden_idents
+    then s else "{|" ^ s ^ "|}"
+
 let rec print_dk_type o t =
   match t with
-  | Dktypetype -> fprintf o "zen.type"
-  | Dktypeprop -> fprintf o "zen.prop"
+  | Dktypetype -> fprintf o "zenon.type"
+  | Dktypeprop -> fprintf o "zenon.prop"
   | Dkarrow (l, r) ->
      begin
        List.iter (fun x -> fprintf o "%a -> " print_dk_type x) l;
@@ -15,21 +61,28 @@ let rec print_dk_type o t =
 	     (get_var_newname var) print_dk_type t1 print_dk_type t2
   | Dkpi _ -> assert false
   | Dkproof (t) ->
-     fprintf o "zen.proof (%a)" print_dk_term t
-  | t -> fprintf o "zen.term (%a)" print_dk_zentype t
+     fprintf o "zenon.proof (%a)" print_dk_term t
+  | t -> fprintf o "zenon.term (%a)" print_dk_zentype t
 
 and print_dk_zentype o t =
   match t with
-  | Dktypeiota -> fprintf o "zen.iota"
+  | Dktypeiota -> fprintf o "zenon.iota"
   | t -> print_dk_term o t
 
 and print_dk_cst o t =
   match t with
   | "Is_true" -> fprintf o "dk_logic.ebP"
   | "FOCAL.ifthenelse" -> fprintf o "dk_bool.ite"
-  | s -> if !Globals.signature_name = "" then fprintf o "%s" s else
-    if Mltoll.is_meta s then fprintf o "zen.select (zen.iota)" else
-      fprintf o "%s.%s" !Globals.signature_name s
+  | s ->
+     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);
+         if !Globals.conjecture <> ""
+            && not !Globals.check_axiom && Typetptp.is_axiom s then
+           fprintf o " __negated_conjecture_proof__"
+       end
 
 and print_dk_term o t =
   match t with
@@ -49,164 +102,164 @@ and print_dk_term o t =
        List.iter (fun x -> fprintf o " (%a)" print_dk_term x) l;
 (*       fprintf o "\n ";*)
      end
-  | Dkseq -> fprintf o "zen.seq"
+  | Dkseq -> fprintf o "zenon.seq"
   | Dknot (t) ->
-     fprintf o "zen.not\n (%a)" print_dk_term t
+     fprintf o "zenon.not\n (%a)" print_dk_term t
   | Dkand (t1, t2) ->
-     fprintf o "zen.and\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.and\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkor (t1, t2) ->
-     fprintf o "zen.or\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.or\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkimply (t1, t2) ->
-     fprintf o "zen.imp\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.imp\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkequiv (t1, t2) ->
-     fprintf o "zen.eqv\n (%a) (%a)" print_dk_term t1 print_dk_term t2
+     fprintf o "zenon.eqv\n (%a) (%a)" print_dk_term t1 print_dk_term t2
   | Dkforall (t1, t2) ->
-     fprintf o "zen.forall (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
+     fprintf o "zenon.forall (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
   | Dkexists (t1, t2) ->
-     fprintf o "zen.exists (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
+     fprintf o "zenon.exists (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2
   | Dkforalltype (t) ->
-     fprintf o "zen.foralltype\n (%a)" print_dk_term t
+     fprintf o "zenon.foralltype\n (%a)" print_dk_term t
   | Dkexiststype (t) ->
-     fprintf o "zen.existstype\n (%a)" print_dk_term t
-  | Dktrue -> fprintf o "zen.True"
-  | Dkfalse -> fprintf o "zen.False"
+     fprintf o "zenon.existstype\n (%a)" print_dk_term t
+  | Dktrue -> fprintf o "zenon.True"
+  | Dkfalse -> fprintf o "zenon.False"
   | Dkequal (t1, t2, t3) ->
-     fprintf o "zen.equal (%a)\n (%a)\n (%a)"
+     fprintf o "zenon.equal (%a)\n (%a)\n (%a)"
 	     print_dk_zentype t1
 	     print_dk_term t2
 	     print_dk_term t3
-  | DkRfalse (pr) -> fprintf o "zen.Rfalse\n (%a)" print_dk_term pr
-  | DkRnottrue (pr) -> fprintf o "zen.Rnottrue\n (%a)" print_dk_term pr
+  | DkRfalse (pr) -> fprintf o "zenon.Rfalse\n (%a)" print_dk_term pr
+  | DkRnottrue (pr) -> fprintf o "zenon.Rnottrue\n (%a)" print_dk_term pr
   | DkRaxiom (p, pr1, pr2) ->
-     fprintf o "zen.Raxiom\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Raxiom\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnoteq (a, t, pr) ->
-     fprintf o "zen.Rnoteq\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnoteq\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term t
 	     print_dk_term pr
   | DkReqsym (a, t, u, pr1, pr2) ->
-     fprintf o "zen.Reqsym\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Reqsym\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term t
 	     print_dk_term u
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRcut (p, pr1, pr2) ->
-     fprintf o "zen.Rcut\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rcut\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotnot (p, pr1, pr2) ->
-     fprintf o "zen.Rnotnot\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotnot\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRand (p, q, pr1, pr2) ->
-     fprintf o "zen.Rand\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rand\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRor (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Ror\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Ror\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRimply (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Rimply\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rimply\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRequiv (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Requiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Requiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRnotand (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Rnotand\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotand\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRnotor (p, q, pr1, pr2) ->
-     fprintf o "zen.Rnotor\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotor\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotimply (p, q, pr1, pr2) ->
-     fprintf o "zen.Rnotimply\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotimply\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotequiv (p, q, pr1, pr2, pr3) ->
-     fprintf o "zen.Rnotequiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotequiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term q
 	     print_dk_term pr1
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRex (a, p, pr1, pr2) ->
-     fprintf o "zen.Rex\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rex\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRall (a, p, t, pr1, pr2) ->
-     fprintf o "zen.Rall\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rall\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotex (a, p, t, pr1, pr2) ->
-     fprintf o "zen.Rnotex\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotex\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotall (a, p, pr1, pr2) ->
-     fprintf o "zen.Rnotall\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotall\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRextype (p, pr1, pr2) ->
-     fprintf o "zen.Rextype\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rextype\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRalltype (p, a, pr1, pr2) ->
-     fprintf o "zen.Ralltype\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Ralltype\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_zentype a
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotextype (p, a, pr1, pr2) ->
-     fprintf o "zen.Rnotextype\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotextype\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_zentype a
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRnotalltype (p, pr1, pr2) ->
-     fprintf o "zen.Rnotalltype\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rnotalltype\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_term p
 	     print_dk_term pr1
 	     print_dk_term pr2
   | DkRsubst  (a, p, t1, t2, pr1, pr2, pr3) ->
-     fprintf o "zen.Rsubst\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rsubst\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t1
@@ -215,7 +268,7 @@ and print_dk_term o t =
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRconglr (a, p, t1, t2, pr1, pr2, pr3) ->
-     fprintf o "zen.Rconglr\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rconglr\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t1
@@ -224,7 +277,7 @@ and print_dk_term o t =
 	     print_dk_term pr2
 	     print_dk_term pr3
   | DkRcongrl (a, p, t1, t2, pr1, pr2, pr3) ->
-     fprintf o "zen.Rcongrl\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
+     fprintf o "zenon.Rcongrl\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n"
 	     print_dk_zentype a
 	     print_dk_term p
 	     print_dk_term t1

globals.ml

@@ -31,7 +31,7 @@ let debug_rwrt = ref false;;
 
 let output_sig = ref false;;
 let signature_name = ref "";;
-let neg_conj = ref "";;
+let conjecture = ref "";;
 let check_axiom = ref false;;
 
 let begin_comment() =

globals.mli

@@ -31,7 +31,7 @@ val debug_rwrt : bool ref;;
 
 val output_sig : bool ref;;
 val signature_name : string ref;;
-val neg_conj : string ref;;
+val conjecture : string ref;;
 val check_axiom : bool ref;;
 
 val begin_comment : unit -> string;;

lltodk.ml

@@ -1033,7 +1033,7 @@ let output oc phrases llp =
   let dkname = List.hd name in
   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;
   fprintf oc "\n";
   if !Globals.signature_name = "" then List.iter (print_line oc) dkctx;
@@ -1059,9 +1059,14 @@ let output_term oc phrases _ llp =
   let dkgoal = translate_expr ngoal in
   let prooftree = extract_prooftree llp in
   let dkproof = make_proof_term (List.hd goal) prooftree in
-  if !Globals.signature_name = "" then () else fprintf oc "def delta : zen.proof (%a) \n := \n " print_dk_term dkgoal;
-  fprintf oc "zen.nnpp (%a)\n\n(%a)"
-	  print_dk_term dkgoal
-	  print_dk_term dkproof;
-    if !Globals.signature_name = "" then () else fprintf oc ".";
+  fprintf oc "#REQUIRE zenon.\n";
+  if !Globals.signature_name <> "" then
+    fprintf oc "#REQUIRE %s.\n" !Globals.signature_name;
+  fprintf oc "\n[] S.%s ↪ " goal_name;
+  let n = !Globals.conjecture in
+  if n <> "" then
+    fprintf oc "__negated_conjecture_proof__ : proof (not %s) =>\n" n;
+  fprintf oc "zenon.nnpp (%a)\n(%a)"
+    print_dk_term dkgoal print_dk_term dkproof;
+  if !Globals.signature_name <> "" then fprintf oc ".";
   []

lltolp.ml

@@ -1064,15 +1064,15 @@ let output_term oc phrases _ llp =
   if !Globals.signature_name <> "" then
     fprintf oc "require %s as S;\n" !Globals.signature_name;
   fprintf oc "\nrule S.%s ↪ " goal_name;
-  let n = !Globals.neg_conj in
-  if n <> "" then fprintf oc "λ %s,\n" n;
+  if !Globals.conjecture <> "" then
+    fprintf oc "λ __negated_conjecture_proof__,";
   begin
     match dkgoal with
-    | Some g -> fprintf oc "\n  nnpp (%a)\n    (%a);\n"
-	          print_dk_term g
-	          print_dk_term dkproof
-    | None -> fprintf oc "\n %a;\n"
-	        print_dk_term dkproof
+    | Some g ->
+       fprintf oc "\n  nnpp (%a)\n    (%a);\n"
+         print_dk_term g print_dk_term dkproof
+    | None ->
+       fprintf oc "\n %a;\n" print_dk_term dkproof
   end;
   []