Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix dk output #37

Merged
merged 6 commits into from
Jul 19, 2024
Merged

fix dk output #37

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
45be898
fix dk output
fblanqui Jul 19, 2024
8bcb560
wip
fblanqui Jul 19, 2024
18608bf
wip
fblanqui Jul 19, 2024
282a4b5
wip
fblanqui Jul 19, 2024
5d70d16
wip
fblanqui Jul 19, 2024
91d5327
wip
fblanqui Jul 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =

Expand Down
147 changes: 100 additions & 47 deletions dkprint.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion globals.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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() =
Expand Down
2 changes: 1 addition & 1 deletion globals.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;;
Expand Down
21 changes: 15 additions & 6 deletions lltodk.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -1058,10 +1058,19 @@ let output_term oc phrases _ llp =
in
let dkgoal = translate_expr ngoal in
let prooftree = extract_prooftree llp in
let goal_name = (List.hd llp).name 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
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";
fprintf oc "zenon.nnpp (%a)\n(%a)"
print_dk_term dkgoal print_dk_term dkproof;
if !Globals.signature_name <> "" then fprintf oc ".";
[]
14 changes: 7 additions & 7 deletions lltolp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
[]

Loading