diff --git a/.github/workflows/full-ci.yml b/.github/workflows/full-ci.yml index 111b1a24..018987fb 100644 --- a/.github/workflows/full-ci.yml +++ b/.github/workflows/full-ci.yml @@ -86,9 +86,19 @@ jobs: - uses: actions/checkout@v5 with: ref: ${{ github.event.pull_request.head.sha }} + - uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixos-unstable - uses: actions/setup-go@v3 with: go-version: ${{ env.goVersion }} - run: go install golang.org/x/tools/cmd/goyacc@latest - run: cd src && make - - run: cd devtools && make test-suite + - uses: rrbutani/use-nix-shell-action@v1 + with: + file: shell.nix + script: | + cd devtools + make test-suite + + diff --git a/devtools/run-test-suite.py b/devtools/run-test-suite.py index 5e135669..771f2919 100644 --- a/devtools/run-test-suite.py +++ b/devtools/run-test-suite.py @@ -5,6 +5,7 @@ import sys import re import difflib +import shutil from subprocess import PIPE, run class Parser: @@ -12,6 +13,7 @@ class Parser: RES = "% result: " ENV = "% env: " EXIT_CODE = "% exit: " + no_rocq_check = False def __init__(self, filename): self.filename = filename @@ -20,6 +22,10 @@ def __init__(self, filename): self.parseEnv() self.parseExitCode() + args_avoid_chk = ["-proof", "-otptp", "-osctptp"] + if "no_chk" in filename or self.expectedExitCode != "" or any(arg in self.arguments for arg in args_avoid_chk) or self.expectedResult == "NOT VALID": + self.no_rocq_check = True + def parseGen(self, pat): with open(self.filename) as f: for line in f.readlines(): @@ -43,23 +49,103 @@ def parseExitCode(self): self.expectedExitCode = self.parseGen(self.EXIT_CODE).strip() def getCommandLine(self): - return self.env + " ../src/_build/goeland " + self.arguments + " " + self.filename + arguments = self.arguments + if not self.no_rocq_check: + arguments += " -context -orocq" + return self.env + " ../src/_build/goeland " + arguments + " " + self.filename + + def getArgsForPrinting(self): + rocq_chk_str = "" + if self.no_rocq_check: + rocq_chk_str = " (no Rocq check)" + return self.arguments + rocq_chk_str def sanitize(s): return s.encode('utf-8', errors='ignore').decode(errors='ignore') -def runProver(command): - print(f"Launching: {command}") +def runProver(f, command): + print(f"{f}\t{parser.getArgsForPrinting()}") result = run(command, stdout=PIPE, stderr=PIPE, universal_newlines=True, shell=True, encoding='utf-8') return (sanitize(result.stdout), sanitize(result.stderr), result.returncode) +def getRelevantOutput(output): + relevantLines = [] + ok = -1 + for line in output.split("\n"): + if re.search("% SZS output start", line): + ok = 1 + elif re.search("% SZS output end", line): + ok = -1 + elif ok == 0: + if len(line.strip()) > 0: + relevantLines.append(line.strip()) + else: + ok -= 1 + + return relevantLines + +def isExecutable(prog) : + return shutil.which(prog) is not None + +def getRocqCompiler() : + if isExecutable("rocq"): + return "rocq compile" + elif isExecutable("coqc"): + return "coqc" + else: + raise Exception("No Rocq executable found on the system") + +def makeRocqCheck(f, output): + rocq = getRocqCompiler() + rocq_lines = getRelevantOutput(output) + compile_success = False + filename = os.getcwd() + "/" + os.path.basename(f)[:-2].replace("-", "_") + with open(f"{filename}.v", "w") as tmp: + tmp.write("\n".join(rocq_lines)) + + result = run(f"{rocq} {filename}.v", stdout=PIPE, stderr=PIPE, universal_newlines=True, shell=True, encoding='utf-8') + compile_success = result.returncode == 0 + + try: + os.remove(f"{filename}.glob") + except FileNotFoundError: + pass + + if not compile_success: + print(f"ROCQ compile has failed.") + print(f"Reason: {result.stderr}") + exit(1) + else: + try: + os.remove(f"{filename}.v") + os.remove(f"{filename}.vo") + os.remove(f"{filename}.vok") + os.remove(f"{filename}.vos") + except FileNotFoundError: + pass + def runWithExpected(f, parser): - output, err, exit_code = runProver(parser.getCommandLine()) + """ + Runs Goéland on [f] using the parsed command line, then checks if the output corresponds to the expected one. + This function manages: + - error codes (e.g., it can detect whether Goéland exits with error code i + - results (e.g., VALID, NOT VALID). + + If Goéland runs into an unexpected error, we report it. Moreover, if the kind of expected return is a VALID + result, we run Rocq to check that the proof is indeed valid (except for files in the no-chk folder). + """ + output, err, exit_code = runProver(f, parser.getCommandLine()) if err != "": print(f"Runtime error: {err}") exit(1) + if parser.expectedExitCode != '': + if int(parser.expectedExitCode) != exit_code: + print(f"Error: expected exit code '{parser.expectedExitCode}', got: '{exit_code}'") + exit(1) + else: return + search = re.compile(".*% RES : (.*)$") for line in output.split("\n"): res = search.match(line) @@ -69,37 +155,21 @@ def runWithExpected(f, parser): print(f"Error: expected '{parser.expectedResult}', got: '{actual}'") exit(1) else: + if parser.no_rocq_check: return + makeRocqCheck(f, output) return - if parser.expectedExitCode != '': - if int(parser.expectedExitCode) != exit_code: - print(f"Error: expected exit code '{parser.expectedExitCode}', got: '{exit_code}'") - exit(1) - else: return - print(f"Unknown error: got\n{output}") exit(1) def compareOutputs(f, parser): - output, err, _ = runProver(parser.getCommandLine()) + output, err, exit_code = runProver(f, parser.getCommandLine()) - if err != "": + if err != "" or exit_code != 0: print(f"Runtime error: {err}") exit(1) - relevantLines = [] - ok = -1 - for line in output.split("\n"): - if re.search("% SZS output start", line): - ok = 1 - elif re.search("% SZS output end", line): - ok = -1 - elif ok == 0: - if len(line.strip()) > 0: - relevantLines.append(line.strip()) - else: - ok -= 1 - + relevantLines = getRelevantOutput(output) relevantExpectedLines = [] with open(os.path.splitext(f)[0] + ".out") as f: @@ -119,7 +189,7 @@ def compareOutputs(f, parser): if __name__ == "__main__": outputTest = ["-proof", "-otptp", "-osctptp"] - for f in glob.glob("test-suite/**/*.p"): + for f in sorted(glob.glob("test-suite/**/*.p")): parser = Parser(f) if (os.path.exists(os.path.splitext(f)[0] + ".out")) : diff --git a/devtools/test-suite/bugs/bug_52-1.p b/devtools/test-suite/bugs/bug_52-1.p new file mode 100644 index 00000000..0c3cd848 --- /dev/null +++ b/devtools/test-suite/bugs/bug_52-1.p @@ -0,0 +1,3 @@ +% result: VALID + +fof(rocq_output_test,conjecture,! [X]: (p(X) | ~p(X))). diff --git a/devtools/test-suite/bugs/bug_52-3.p b/devtools/test-suite/bugs/bug_52-3.p new file mode 100644 index 00000000..4026b2be --- /dev/null +++ b/devtools/test-suite/bugs/bug_52-3.p @@ -0,0 +1,4 @@ +% tests for the presence of metavariables +% result: VALID + +fof(rocq_output_test,conjecture,? [X]: (p(X) | ~p(X))). diff --git a/devtools/test-suite/bugs_no_chk/bug_52-2.p b/devtools/test-suite/bugs_no_chk/bug_52-2.p new file mode 100644 index 00000000..f054cf22 --- /dev/null +++ b/devtools/test-suite/bugs_no_chk/bug_52-2.p @@ -0,0 +1,13 @@ +% TODO: move this file to bugs once we enable typed GS3 proofs +% result: VALID + +tff(nat_type,type,nat : $tType). +tff(zero_nat,type,zero : nat). +tff(succ_nat,type,succ : nat > nat). +tff(list_type,type,list : $tType > $tType). +tff(nil_list,type,nil : !> [A]: list(A)). +tff(cons_list,type,cons : !> [A]: ((A * list(A)) > list(A))). +tff(p_type,type,p : !> [A : $tType]: (list(A) > $o)). + +tff(rocq_output_test,conjecture,! [A: $tType, X : A]: + ((succ(zero) = succ(zero)) | (p(A,cons(A,X,nil(A))) | ~p(A,cons(A,X,nil(A)))))). diff --git a/devtools/test-suite/basic/Axioms/SYN000+0.ax b/devtools/test-suite/no_chk/Axioms/SYN000+0.ax similarity index 100% rename from devtools/test-suite/basic/Axioms/SYN000+0.ax rename to devtools/test-suite/no_chk/Axioms/SYN000+0.ax diff --git a/devtools/test-suite/basic/Axioms/SYN000_0.ax b/devtools/test-suite/no_chk/Axioms/SYN000_0.ax similarity index 100% rename from devtools/test-suite/basic/Axioms/SYN000_0.ax rename to devtools/test-suite/no_chk/Axioms/SYN000_0.ax diff --git a/devtools/test-suite/basic/fol_syntax_chk.p b/devtools/test-suite/no_chk/fol_syntax_chk.p similarity index 100% rename from devtools/test-suite/basic/fol_syntax_chk.p rename to devtools/test-suite/no_chk/fol_syntax_chk.p diff --git a/devtools/test-suite/basic/tf0_syntax_chk.p b/devtools/test-suite/no_chk/tf0_syntax_chk.p similarity index 100% rename from devtools/test-suite/basic/tf0_syntax_chk.p rename to devtools/test-suite/no_chk/tf0_syntax_chk.p diff --git a/devtools/test-suite/proofs/example_sctptp.out b/devtools/test-suite/proofs/example_sctptp.out index 18621ff5..b99a1dfc 100644 --- a/devtools/test-suite/proofs/example_sctptp.out +++ b/devtools/test-suite/proofs/example_sctptp.out @@ -1,29 +1,29 @@ -fof(c_example_sctptp_p, conjecture, ((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))). +fof(c_example_sctptp_p, conjecture, (! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))). -fof(f8, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~((! [X4] : (p(X4)))), ~((? [Y6] : (~(p(Y6))))), ~((~((? [Y6] : (~(p(Y6))))) => (! [X4] : (p(X4))))), ~(p(Sko_0)), ~(~(p(Sko_0))), p(Sko_0)] --> [], inference(leftHyp, [status(thm), 6], [])). +fof(f8, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~(! [X4]: p(X4)), ~(? [Y6]: ~p(Y6)), ~(~(? [Y6]: ~p(Y6)) => (! [X4]: p(X4))), ~p(Sko_0), ~~p(Sko_0), p(Sko_0)] --> [], inference(leftHyp, [status(thm), 6], [])). -fof(f7, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~((! [X4] : (p(X4)))), ~((? [Y6] : (~(p(Y6))))), ~((~((? [Y6] : (~(p(Y6))))) => (! [X4] : (p(X4))))), ~(p(Sko_0)), ~(~(p(Sko_0)))] --> [], inference(leftNotNot, [status(thm), 5], [f8])). +fof(f7, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~(! [X4]: p(X4)), ~(? [Y6]: ~p(Y6)), ~(~(? [Y6]: ~p(Y6)) => (! [X4]: p(X4))), ~p(Sko_0), ~~p(Sko_0)] --> [], inference(leftNotNot, [status(thm), 5], [f8])). -fof(f6, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~((! [X4] : (p(X4)))), ~((? [Y6] : (~(p(Y6))))), ~((~((? [Y6] : (~(p(Y6))))) => (! [X4] : (p(X4))))), ~(p(Sko_0))] --> [], inference(leftNotEx, [status(thm), 2, $fot(Sko_0)], [f7])). +fof(f6, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~(! [X4]: p(X4)), ~(? [Y6]: ~p(Y6)), ~(~(? [Y6]: ~p(Y6)) => (! [X4]: p(X4))), ~p(Sko_0)] --> [], inference(leftNotEx, [status(thm), 2, $fot(Sko_0)], [f7])). -fof(f4, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~((! [X4] : (p(X4)))), ~((? [Y6] : (~(p(Y6))))), ~((~((? [Y6] : (~(p(Y6))))) => (! [X4] : (p(X4)))))] --> [], inference(leftNotAll, [status(thm), 1, 'Sko_0'], [f6])). +fof(f4, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~(! [X4]: p(X4)), ~(? [Y6]: ~p(Y6)), ~(~(? [Y6]: ~p(Y6)) => (! [X4]: p(X4)))] --> [], inference(leftNotAll, [status(thm), 1, 'Sko_0'], [f6])). -fof(f11, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), (! [X4] : (p(X4))), ~(~((? [Y6] : (~(p(Y6)))))), ~(((! [X4] : (p(X4))) => ~((? [Y6] : (~(p(Y6))))))), (? [Y6] : (~(p(Y6)))), ~(p(Sko_1)), p(Sko_1)] --> [], inference(leftHyp, [status(thm), 6], [])). +fof(f11, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ! [X4]: p(X4), ~~(? [Y6]: ~p(Y6)), ~((! [X4]: p(X4)) => ~(? [Y6]: ~p(Y6))), ? [Y6]: ~p(Y6), ~p(Sko_1), p(Sko_1)] --> [], inference(leftHyp, [status(thm), 6], [])). -fof(f10, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), (! [X4] : (p(X4))), ~(~((? [Y6] : (~(p(Y6)))))), ~(((! [X4] : (p(X4))) => ~((? [Y6] : (~(p(Y6))))))), (? [Y6] : (~(p(Y6)))), ~(p(Sko_1))] --> [], inference(leftForall, [status(thm), 1, $fot(Sko_1)], [f11])). +fof(f10, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ! [X4]: p(X4), ~~(? [Y6]: ~p(Y6)), ~((! [X4]: p(X4)) => ~(? [Y6]: ~p(Y6))), ? [Y6]: ~p(Y6), ~p(Sko_1)] --> [], inference(leftForall, [status(thm), 1, $fot(Sko_1)], [f11])). -fof(f9, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), (! [X4] : (p(X4))), ~(~((? [Y6] : (~(p(Y6)))))), ~(((! [X4] : (p(X4))) => ~((? [Y6] : (~(p(Y6))))))), (? [Y6] : (~(p(Y6))))] --> [], inference(leftExists, [status(thm), 4, 'Sko_1'], [f10])). +fof(f9, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ! [X4]: p(X4), ~~(? [Y6]: ~p(Y6)), ~((! [X4]: p(X4)) => ~(? [Y6]: ~p(Y6))), ? [Y6]: ~p(Y6)] --> [], inference(leftExists, [status(thm), 4, 'Sko_1'], [f10])). -fof(f5, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), (! [X4] : (p(X4))), ~(~((? [Y6] : (~(p(Y6)))))), ~(((! [X4] : (p(X4))) => ~((? [Y6] : (~(p(Y6)))))))] --> [], inference(leftNotNot, [status(thm), 2], [f9])). +fof(f5, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ! [X4]: p(X4), ~~(? [Y6]: ~p(Y6)), ~((! [X4]: p(X4)) => ~(? [Y6]: ~p(Y6)))] --> [], inference(leftNotNot, [status(thm), 2], [f9])). -fof(f3ext2, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~((~((? [Y6] : (~(p(Y6))))) => (! [X4] : (p(X4)))))] --> [], inference(leftNotImplies, [status(thm), 1], [f4])). +fof(f3ext2, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~(~(? [Y6]: ~p(Y6)) => (! [X4]: p(X4)))] --> [], inference(leftNotImplies, [status(thm), 1], [f4])). -fof(f3ext1, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~(((! [X4] : (p(X4))) => ~((? [Y6] : (~(p(Y6)))))))] --> [], inference(leftNotImplies, [status(thm), 1], [f5])). +fof(f3ext1, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~((! [X4]: p(X4)) => ~(? [Y6]: ~p(Y6)))] --> [], inference(leftNotImplies, [status(thm), 1], [f5])). -fof(f3, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6)))))))] --> [], inference(leftNotIff, [status(thm), 0], [f3ext1, f3ext2])). +fof(f3, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6)))] --> [], inference(leftNotIff, [status(thm), 0], [f3ext1, f3ext2])). -fof(f2, plain, [((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))] --> [((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))], inference(hyp, [status(thm), 0], [])). +fof(f2, plain, [(! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))] --> [(! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))], inference(hyp, [status(thm), 0], [])). -fof(f1, plain, [] --> [((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6)))))), ~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6)))))))], inference(rightNot, [status(thm), 1], [f2])). +fof(f1, plain, [] --> [(! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6)), ~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6)))], inference(rightNot, [status(thm), 1], [f2])). -fof(f0, plain, [] --> [((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))], inference(cut, [status(thm), 1], [f1, f3])). \ No newline at end of file +fof(f0, plain, [] --> [(! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))], inference(cut, [status(thm), 1], [f1, f3])). diff --git a/devtools/test-suite/proofs/example_sctptp.p b/devtools/test-suite/proofs/example_sctptp.p index 25b76bce..d877b98f 100644 --- a/devtools/test-suite/proofs/example_sctptp.p +++ b/devtools/test-suite/proofs/example_sctptp.p @@ -1,7 +1,5 @@ -% args: -no_id -osctptp +% args: -osctptp % result: VALID fof(test_sctptp, conjecture, (! [X] : p(X)) <=> (~(? [Y] : ~p(Y)))). - - \ No newline at end of file diff --git a/devtools/test-suite/proofs/example_tptp.out b/devtools/test-suite/proofs/example_tptp.out index f574adc7..3ae286e7 100644 --- a/devtools/test-suite/proofs/example_tptp.out +++ b/devtools/test-suite/proofs/example_tptp.out @@ -1,29 +1,29 @@ -fof(c_example_tptp_p, conjecture, ((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))). +fof(c_example_tptp_p, conjecture, (! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))). -fof(f8, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~((! [X4] : (p(X4)))), ~((? [Y6] : (~(p(Y6))))), ~((~((? [Y6] : (~(p(Y6))))) => (! [X4] : (p(X4))))), ~(p(sko_0)), ~(~(p(sko_0))), p(sko_0)] --> [], inference(leftHyp, [status(thm), 6], [])). +fof(f8, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~(! [X4]: p(X4)), ~(? [Y6]: ~p(Y6)), ~(~(? [Y6]: ~p(Y6)) => (! [X4]: p(X4))), ~p(sko_0), ~~p(sko_0), p(sko_0)] --> [], inference(leftHyp, [status(thm), 6], [])). -fof(f7, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~((! [X4] : (p(X4)))), ~((? [Y6] : (~(p(Y6))))), ~((~((? [Y6] : (~(p(Y6))))) => (! [X4] : (p(X4))))), ~(p(sko_0)), ~(~(p(sko_0)))] --> [], inference(leftNotNot, [status(thm), 5], [f8])). +fof(f7, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~(! [X4]: p(X4)), ~(? [Y6]: ~p(Y6)), ~(~(? [Y6]: ~p(Y6)) => (! [X4]: p(X4))), ~p(sko_0), ~~p(sko_0)] --> [], inference(leftNotNot, [status(thm), 5], [f8])). -fof(f6, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~((! [X4] : (p(X4)))), ~((? [Y6] : (~(p(Y6))))), ~((~((? [Y6] : (~(p(Y6))))) => (! [X4] : (p(X4))))), ~(p(sko_0))] --> [], inference(leftNotEx, [status(thm), 2, $fot(sko_0)], [f7])). +fof(f6, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~(! [X4]: p(X4)), ~(? [Y6]: ~p(Y6)), ~(~(? [Y6]: ~p(Y6)) => (! [X4]: p(X4))), ~p(sko_0)] --> [], inference(leftNotEx, [status(thm), 2, $fot(sko_0)], [f7])). -fof(f4, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~((! [X4] : (p(X4)))), ~((? [Y6] : (~(p(Y6))))), ~((~((? [Y6] : (~(p(Y6))))) => (! [X4] : (p(X4)))))] --> [], inference(leftNotAll, [status(thm), 1, 'sko_0'], [f6])). +fof(f4, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~(! [X4]: p(X4)), ~(? [Y6]: ~p(Y6)), ~(~(? [Y6]: ~p(Y6)) => (! [X4]: p(X4)))] --> [], inference(leftNotAll, [status(thm), 1, 'sko_0'], [f6])). -fof(f11, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), (! [X4] : (p(X4))), ~(~((? [Y6] : (~(p(Y6)))))), ~(((! [X4] : (p(X4))) => ~((? [Y6] : (~(p(Y6))))))), (? [Y6] : (~(p(Y6)))), ~(p(sko_1)), p(sko_1)] --> [], inference(leftHyp, [status(thm), 6], [])). +fof(f11, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ! [X4]: p(X4), ~~(? [Y6]: ~p(Y6)), ~((! [X4]: p(X4)) => ~(? [Y6]: ~p(Y6))), ? [Y6]: ~p(Y6), ~p(sko_1), p(sko_1)] --> [], inference(leftHyp, [status(thm), 6], [])). -fof(f10, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), (! [X4] : (p(X4))), ~(~((? [Y6] : (~(p(Y6)))))), ~(((! [X4] : (p(X4))) => ~((? [Y6] : (~(p(Y6))))))), (? [Y6] : (~(p(Y6)))), ~(p(sko_1))] --> [], inference(leftForall, [status(thm), 1, $fot(sko_1)], [f11])). +fof(f10, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ! [X4]: p(X4), ~~(? [Y6]: ~p(Y6)), ~((! [X4]: p(X4)) => ~(? [Y6]: ~p(Y6))), ? [Y6]: ~p(Y6), ~p(sko_1)] --> [], inference(leftForall, [status(thm), 1, $fot(sko_1)], [f11])). -fof(f9, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), (! [X4] : (p(X4))), ~(~((? [Y6] : (~(p(Y6)))))), ~(((! [X4] : (p(X4))) => ~((? [Y6] : (~(p(Y6))))))), (? [Y6] : (~(p(Y6))))] --> [], inference(leftExists, [status(thm), 4, 'sko_1'], [f10])). +fof(f9, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ! [X4]: p(X4), ~~(? [Y6]: ~p(Y6)), ~((! [X4]: p(X4)) => ~(? [Y6]: ~p(Y6))), ? [Y6]: ~p(Y6)] --> [], inference(leftExists, [status(thm), 4, 'sko_1'], [f10])). -fof(f5, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), (! [X4] : (p(X4))), ~(~((? [Y6] : (~(p(Y6)))))), ~(((! [X4] : (p(X4))) => ~((? [Y6] : (~(p(Y6)))))))] --> [], inference(leftNotNot, [status(thm), 2], [f9])). +fof(f5, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ! [X4]: p(X4), ~~(? [Y6]: ~p(Y6)), ~((! [X4]: p(X4)) => ~(? [Y6]: ~p(Y6)))] --> [], inference(leftNotNot, [status(thm), 2], [f9])). -fof(f3ext2, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~((~((? [Y6] : (~(p(Y6))))) => (! [X4] : (p(X4)))))] --> [], inference(leftNotImplies, [status(thm), 1], [f4])). +fof(f3ext2, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~(~(? [Y6]: ~p(Y6)) => (! [X4]: p(X4)))] --> [], inference(leftNotImplies, [status(thm), 1], [f4])). -fof(f3ext1, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))), ~(((! [X4] : (p(X4))) => ~((? [Y6] : (~(p(Y6)))))))] --> [], inference(leftNotImplies, [status(thm), 1], [f5])). +fof(f3ext1, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))), ~((! [X4]: p(X4)) => ~(? [Y6]: ~p(Y6)))] --> [], inference(leftNotImplies, [status(thm), 1], [f5])). -fof(f3, plain, [~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6)))))))] --> [], inference(leftNotIff, [status(thm), 0], [f3ext1, f3ext2])). +fof(f3, plain, [~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6)))] --> [], inference(leftNotIff, [status(thm), 0], [f3ext1, f3ext2])). -fof(f2, plain, [((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))] --> [((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))], inference(hyp, [status(thm), 0], [])). +fof(f2, plain, [(! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))] --> [(! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))], inference(hyp, [status(thm), 0], [])). -fof(f1, plain, [] --> [((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6)))))), ~(((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6)))))))], inference(rightNot, [status(thm), 1], [f2])). +fof(f1, plain, [] --> [(! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6)), ~((! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6)))], inference(rightNot, [status(thm), 1], [f2])). -fof(f0, plain, [] --> [((! [X4] : (p(X4))) <=> ~((? [Y6] : (~(p(Y6))))))], inference(cut, [status(thm), 1], [f1, f3])). \ No newline at end of file +fof(f0, plain, [] --> [(! [X4]: p(X4)) <=> ~(? [Y6]: ~p(Y6))], inference(cut, [status(thm), 1], [f1, f3])). diff --git a/devtools/test-suite/proofs/example_tptp.p b/devtools/test-suite/proofs/example_tptp.p index a7835d7c..7c6928d5 100644 --- a/devtools/test-suite/proofs/example_tptp.p +++ b/devtools/test-suite/proofs/example_tptp.p @@ -1,4 +1,4 @@ -% args: -no_id -otptp +% args: -otptp % result: VALID fof(test_tptp, conjecture, diff --git a/devtools/test-suite/proofs/flatten-1.out b/devtools/test-suite/proofs/flatten-1.out index 8f7c127f..def47b3c 100644 --- a/devtools/test-suite/proofs/flatten-1.out +++ b/devtools/test-suite/proofs/flatten-1.out @@ -1,7 +1,7 @@ -[0] ALPHA_NOT_NOT : ~(~((p_1 & q_2 & ~(p_1)))) - -> [1] (p_1 & q_2 & ~(p_1)) +[0] ALPHA_NOT_NOT : ~~(p & q & ~p) + -> [1] p & q & ~p -[1] ALPHA_AND : (p_1 & q_2 & ~(p_1)) - -> [2] p_1, q_2, ~(p_1) +[1] ALPHA_AND : p & q & ~p + -> [2] p, q, ~p -[2] CLOSURE : p_1 +[2] CLOSURE : p diff --git a/devtools/test-suite/proofs/flatten-2.out b/devtools/test-suite/proofs/flatten-2.out index 09a62e72..4de193ea 100644 --- a/devtools/test-suite/proofs/flatten-2.out +++ b/devtools/test-suite/proofs/flatten-2.out @@ -1,7 +1,7 @@ -[0] ALPHA_NOT_OR : ~((p_1 | q_2 | ~(p_1))) - -> [1] ~(p_1), ~(q_2), ~(~(p_1)) +[0] ALPHA_NOT_OR : ~(p | q | ~p) + -> [1] ~p, ~q, ~~p -[1] ALPHA_NOT_NOT : ~(~(p_1)) - -> [2] p_1 +[1] ALPHA_NOT_NOT : ~~p + -> [2] p -[2] CLOSURE : p_1 +[2] CLOSURE : p diff --git a/devtools/test-suite/proofs/tf1_basic_thm-2.out b/devtools/test-suite/proofs/tf1_basic_thm-2.out index b87de471..9f8a3e0e 100644 --- a/devtools/test-suite/proofs/tf1_basic_thm-2.out +++ b/devtools/test-suite/proofs/tf1_basic_thm-2.out @@ -1,28 +1,28 @@ -[0] ALPHA_AND : ((! [A13]: ((maybe(A13) ; head(A13;nil(A13;)) = none(A13;)))) & (! [A15 X17 XS19]: ((maybe(A15) ; head(A15;cons(A15;X17, XS19)) = some(A15;X17)))) & ~((! [A21 X23 Y25 Z27]: ((maybe(A21) ; head(A21;cons(A21;X23, cons(A21;Y25, cons(A21;Z27, nil(A21;))))) = some(A21;X23)))))) - -> [1] (! [A13]: ((maybe(A13) ; head(A13;nil(A13;)) = none(A13;)))), (! [A15 X17 XS19]: ((maybe(A15) ; head(A15;cons(A15;X17, XS19)) = some(A15;X17)))), ~((! [A21 X23 Y25 Z27]: ((maybe(A21) ; head(A21;cons(A21;X23, cons(A21;Y25, cons(A21;Z27, nil(A21;))))) = some(A21;X23))))) +[0] ALPHA_AND : (! [A13]: head(A13 ; nil(A13 ; )) = none(A13 ; )) & (! [A15, X17, XS19]: head(A15 ; cons(A15 ; X17, XS19)) = some(A15 ; X17)) & ~(! [A21, X23, Y25, Z27]: head(A21 ; cons(A21 ; X23, cons(A21 ; Y25, cons(A21 ; Z27, nil(A21 ; ))))) = some(A21 ; X23)) + -> [1] ! [A13]: head(A13 ; nil(A13 ; )) = none(A13 ; ), ! [A15, X17, XS19]: head(A15 ; cons(A15 ; X17, XS19)) = some(A15 ; X17), ~(! [A21, X23, Y25, Z27]: head(A21 ; cons(A21 ; X23, cons(A21 ; Y25, cons(A21 ; Z27, nil(A21 ; ))))) = some(A21 ; X23)) -[1] DELTA_NOT_FORALL : ~((! [A21 X23 Y25 Z27]: ((maybe(A21) ; head(A21;cons(A21;X23, cons(A21;Y25, cons(A21;Z27, nil(A21;))))) = some(A21;X23))))) - -> [2] ~((! [X23 Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;X23))))) +[1] DELTA_NOT_FORALL : ~(! [A21, X23, Y25, Z27]: head(A21 ; cons(A21 ; X23, cons(A21 ; Y25, cons(A21 ; Z27, nil(A21 ; ))))) = some(A21 ; X23)) + -> [2] ~(! [X23, Y25, Z27]: head(skoTy@29 ; cons(skoTy@29 ; X23, cons(skoTy@29 ; Y25, cons(skoTy@29 ; Z27, nil(skoTy@29 ; ))))) = some(skoTy@29 ; X23)) -[2] DELTA_NOT_FORALL : ~((! [X23 Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;X23))))) - -> [3] ~((! [Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23))))) +[2] DELTA_NOT_FORALL : ~(! [X23, Y25, Z27]: head(skoTy@29 ; cons(skoTy@29 ; X23, cons(skoTy@29 ; Y25, cons(skoTy@29 ; Z27, nil(skoTy@29 ; ))))) = some(skoTy@29 ; X23)) + -> [3] ~(! [Y25, Z27]: head(skoTy@29 ; cons(skoTy@29 ; skolem@X23@0, cons(skoTy@29 ; Y25, cons(skoTy@29 ; Z27, nil(skoTy@29 ; ))))) = some(skoTy@29 ; skolem@X23@0)) -[3] DELTA_NOT_FORALL : ~((! [Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23))))) - -> [4] ~((! [Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23))))) +[3] DELTA_NOT_FORALL : ~(! [Y25, Z27]: head(skoTy@29 ; cons(skoTy@29 ; skolem@X23@0, cons(skoTy@29 ; Y25, cons(skoTy@29 ; Z27, nil(skoTy@29 ; ))))) = some(skoTy@29 ; skolem@X23@0)) + -> [4] ~(! [Z27]: head(skoTy@29 ; cons(skoTy@29 ; skolem@X23@0, cons(skoTy@29 ; skolem@Y25@1, cons(skoTy@29 ; Z27, nil(skoTy@29 ; ))))) = some(skoTy@29 ; skolem@X23@0)) -[4] DELTA_NOT_FORALL : ~((! [Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23))))) - -> [5] ~((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;skolem@Z27, nil(skoTy;))))) = some(skoTy;skolem@X23))) +[4] DELTA_NOT_FORALL : ~(! [Z27]: head(skoTy@29 ; cons(skoTy@29 ; skolem@X23@0, cons(skoTy@29 ; skolem@Y25@1, cons(skoTy@29 ; Z27, nil(skoTy@29 ; ))))) = some(skoTy@29 ; skolem@X23@0)) + -> [5] ~(head(skoTy@29 ; cons(skoTy@29 ; skolem@X23@0, cons(skoTy@29 ; skolem@Y25@1, cons(skoTy@29 ; skolem@Z27@2, nil(skoTy@29 ; ))))) = some(skoTy@29 ; skolem@X23@0)) -[5] GAMMA_FORALL : (! [A13]: ((maybe(A13) ; head(A13;nil(A13;)) = none(A13;)))) - -> [6] (maybe(A13_1) ; head(A13_1;nil(A13_1;)) = none(A13_1;)) +[5] GAMMA_FORALL : ! [A13]: head(A13 ; nil(A13 ; )) = none(A13 ; ) + -> [6] head(A13 ; nil(A13 ; )) = none(A13 ; ) -[6] GAMMA_FORALL : (! [A15 X17 XS19]: ((maybe(A15) ; head(A15;cons(A15;X17, XS19)) = some(A15;X17)))) - -> [7] (! [X17 XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X17, XS19)) = some(skoTy;X17)))) +[6] GAMMA_FORALL : ! [A15, X17, XS19]: head(A15 ; cons(A15 ; X17, XS19)) = some(A15 ; X17) + -> [7] ! [X17, XS19]: head(skoTy@29 ; cons(skoTy@29 ; X17, XS19)) = some(skoTy@29 ; X17) -[7] GAMMA_FORALL : (! [X17 XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X17, XS19)) = some(skoTy;X17)))) - -> [8] (! [XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, XS19)) = some(skoTy;skolem@X23)))) +[7] GAMMA_FORALL : ! [X17, XS19]: head(skoTy@29 ; cons(skoTy@29 ; X17, XS19)) = some(skoTy@29 ; X17) + -> [8] ! [XS19]: head(skoTy@29 ; cons(skoTy@29 ; skolem@X23@0, XS19)) = some(skoTy@29 ; skolem@X23@0) -[8] GAMMA_FORALL : (! [XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, XS19)) = some(skoTy;skolem@X23)))) - -> [9] (maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;skolem@Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)) +[8] GAMMA_FORALL : ! [XS19]: head(skoTy@29 ; cons(skoTy@29 ; skolem@X23@0, XS19)) = some(skoTy@29 ; skolem@X23@0) + -> [9] head(skoTy@29 ; cons(skoTy@29 ; skolem@X23@0, cons(skoTy@29 ; skolem@Y25@1, cons(skoTy@29 ; skolem@Z27@2, nil(skoTy@29 ; ))))) = some(skoTy@29 ; skolem@X23@0) -[9] CLOSURE : (maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;skolem@Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)) +[9] CLOSURE : head(skoTy@29 ; cons(skoTy@29 ; skolem@X23@0, cons(skoTy@29 ; skolem@Y25@1, cons(skoTy@29 ; skolem@Z27@2, nil(skoTy@29 ; ))))) = some(skoTy@29 ; skolem@X23@0) diff --git a/devtools/test-suite/proofs/tf1_basic_thm-2.p b/devtools/test-suite/proofs/tf1_basic_thm-2.p index f4838a46..a814c1b8 100644 --- a/devtools/test-suite/proofs/tf1_basic_thm-2.p +++ b/devtools/test-suite/proofs/tf1_basic_thm-2.p @@ -1,4 +1,4 @@ -% args: -proof -no_id +% args: -proof % result: VALID tff(list_type,type, diff --git a/devtools/test-suite/proofs/tf1_basic_thm.out b/devtools/test-suite/proofs/tf1_basic_thm.out index 39c81f0d..3a5ce077 100644 --- a/devtools/test-suite/proofs/tf1_basic_thm.out +++ b/devtools/test-suite/proofs/tf1_basic_thm.out @@ -1,16 +1,16 @@ -[0] ALPHA_AND : ((! [A14]: ((maybe(A14) ; head(A14;nil(A14;)) = none(A14;)))) & (! [A16 X18 XS20]: ((maybe(A16) ; head(A16;cons(A16;X18, XS20)) = some(A16;X18)))) & ~((maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1)))) - -> [1] (! [A14]: ((maybe(A14) ; head(A14;nil(A14;)) = none(A14;)))), (! [A16 X18 XS20]: ((maybe(A16) ; head(A16;cons(A16;X18, XS20)) = some(A16;X18)))), ~((maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1))) +[0] ALPHA_AND : (! [A14]: head(A14 ; nil(A14 ; )) = none(A14 ; )) & (! [A16, X18, XS20]: head(A16 ; cons(A16 ; X18, XS20)) = some(A16 ; X18)) & ~(head($int ; cons($int ; 1, cons($int ; 2, cons($int ; 3, nil($int ; ))))) = some($int ; 1)) + -> [1] ! [A14]: head(A14 ; nil(A14 ; )) = none(A14 ; ), ! [A16, X18, XS20]: head(A16 ; cons(A16 ; X18, XS20)) = some(A16 ; X18), ~(head($int ; cons($int ; 1, cons($int ; 2, cons($int ; 3, nil($int ; ))))) = some($int ; 1)) -[1] GAMMA_FORALL : (! [A14]: ((maybe(A14) ; head(A14;nil(A14;)) = none(A14;)))) - -> [2] (maybe(A14_1) ; head(A14_1;nil(A14_1;)) = none(A14_1;)) +[1] GAMMA_FORALL : ! [A14]: head(A14 ; nil(A14 ; )) = none(A14 ; ) + -> [2] head(A14 ; nil(A14 ; )) = none(A14 ; ) -[2] GAMMA_FORALL : (! [A16 X18 XS20]: ((maybe(A16) ; head(A16;cons(A16;X18, XS20)) = some(A16;X18)))) - -> [3] (! [X18 XS20]: ((maybe($int) ; head($int;cons($int;X18, XS20)) = some($int;X18)))) +[2] GAMMA_FORALL : ! [A16, X18, XS20]: head(A16 ; cons(A16 ; X18, XS20)) = some(A16 ; X18) + -> [3] ! [X18, XS20]: head($int ; cons($int ; X18, XS20)) = some($int ; X18) -[3] GAMMA_FORALL : (! [X18 XS20]: ((maybe($int) ; head($int;cons($int;X18, XS20)) = some($int;X18)))) - -> [4] (! [XS20]: ((maybe($int) ; head($int;cons($int;1, XS20)) = some($int;1)))) +[3] GAMMA_FORALL : ! [X18, XS20]: head($int ; cons($int ; X18, XS20)) = some($int ; X18) + -> [4] ! [XS20]: head($int ; cons($int ; 1, XS20)) = some($int ; 1) -[4] GAMMA_FORALL : (! [XS20]: ((maybe($int) ; head($int;cons($int;1, XS20)) = some($int;1)))) - -> [5] (maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1)) +[4] GAMMA_FORALL : ! [XS20]: head($int ; cons($int ; 1, XS20)) = some($int ; 1) + -> [5] head($int ; cons($int ; 1, cons($int ; 2, cons($int ; 3, nil($int ; ))))) = some($int ; 1) -[5] CLOSURE : (maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1)) +[5] CLOSURE : head($int ; cons($int ; 1, cons($int ; 2, cons($int ; 3, nil($int ; ))))) = some($int ; 1) diff --git a/devtools/test-suite/proofs/tf1_basic_thm.p b/devtools/test-suite/proofs/tf1_basic_thm.p index c2ed4f90..5718a0f8 100644 --- a/devtools/test-suite/proofs/tf1_basic_thm.p +++ b/devtools/test-suite/proofs/tf1_basic_thm.p @@ -1,4 +1,4 @@ -% args: -proof -no_id +% args: -proof % result: VALID tff(list_type,type, diff --git a/shell.nix b/shell.nix index 121645eb..97d4cf1a 100644 --- a/shell.nix +++ b/shell.nix @@ -7,6 +7,7 @@ pkgs.mkShell { gotools python314 rocq-core + rocqPackages.stdlib ocamlPackages.lambdapi ]; } diff --git a/src/AST/form-list.go b/src/AST/form-list.go index b8287b76..4472f744 100644 --- a/src/AST/form-list.go +++ b/src/AST/form-list.go @@ -48,15 +48,6 @@ func LsSubstByTerm(formulas Lib.List[Form], meta Meta, term Term) Lib.List[Form] return formulas } -// ex-name: ToMappableStringSlice -func LsToMappableStringSlice(formulas Lib.List[Form]) []MappableString { - forms := []MappableString{} - for _, form := range formulas.GetSlice() { - forms = append(forms, form.(MappableString)) - } - return forms -} - func FlattenAnd(formulas Lib.List[Form]) Lib.List[Form] { result := Lib.NewList[Form]() diff --git a/src/AST/formsDef.go b/src/AST/formsDef.go index 48f5a7e6..ed4183d3 100644 --- a/src/AST/formsDef.go +++ b/src/AST/formsDef.go @@ -37,8 +37,7 @@ package AST import ( - "strings" - + "fmt" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" ) @@ -88,7 +87,7 @@ type All struct { } func MakeAllSimple(i int, vars Lib.List[TypedVar], forms Form, metas Lib.Set[Meta]) All { - return All{makeQuantifier(i, vars, forms, metas, AllQuant)} + return All{makeQuantifier(i, vars, forms, metas, ConnAll)} } func MakeAll(i int, vars Lib.List[TypedVar], forms Form) All { @@ -143,7 +142,7 @@ type Ex struct { } func MakeExSimple(i int, vars Lib.List[TypedVar], forms Form, metas Lib.Set[Meta]) Ex { - return Ex{makeQuantifier(i, vars, forms, metas, ExQuant)} + return Ex{makeQuantifier(i, vars, forms, metas, ConnEx)} } func MakeEx(i int, vars Lib.List[TypedVar], forms Form) Ex { @@ -194,7 +193,6 @@ func (e Ex) ReplaceMetaByTerm(meta Meta, term Term) Form { // Or type Or struct { - *MappedString index int forms Lib.List[Form] metas Lib.Cache[Lib.Set[Meta], Or] @@ -203,10 +201,7 @@ type Or struct { /** Constructors **/ func MakeOrSimple(i int, forms Lib.List[Form], metas Lib.Set[Meta]) Or { - fms := &MappedString{} - or := Or{fms, i, forms, Lib.MkCache(metas, Or.forceGetMetas)} - fms.MappableString = &or - return or + return Or{i, forms, Lib.MkCache(metas, Or.forceGetMetas)} } func MakeOr(i int, forms Lib.List[Form]) Or { @@ -249,31 +244,18 @@ func (o Or) Equals(f any) bool { } func (o Or) Copy() Form { - fms := &MappedString{} - or := Or{ - fms, + return Or{ o.index, Lib.ListCpy(o.forms), o.metas.Copy(Lib.Set[Meta].Copy), } - fms.MappableString = &or - return or } func (o Or) ToString() string { - return o.MappedString.ToString() -} - -func (o Or) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - return "(%s)" -} - -func (o Or) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - return " " + mapping[OrConn] + " ", "" -} - -func (o Or) GetChildrenForMappedString() []MappableString { - return LsToMappableStringSlice(o.GetChildFormulas()) + return o.forms.ToString( + func(f Form) string { return printer.Str(printer.SurroundChild(f.ToString())) }, + Lib.WithSep(printer.StrConn(ConnOr)), Lib.WithEmpty(""), + ) } func (o Or) ReplaceTermByTerm(old Term, new Term) (Form, bool) { @@ -315,7 +297,6 @@ func (o Or) ReplaceMetaByTerm(meta Meta, term Term) Form { // And type And struct { - *MappedString index int forms Lib.List[Form] metas Lib.Cache[Lib.Set[Meta], And] @@ -324,10 +305,7 @@ type And struct { /** Constructors **/ func MakeAndSimple(i int, forms Lib.List[Form], metas Lib.Set[Meta]) And { - fms := &MappedString{} - and := And{fms, i, forms, Lib.MkCache(metas, And.forceGetMetas)} - fms.MappableString = &and - return and + return And{i, forms, Lib.MkCache(metas, And.forceGetMetas)} } func MakeAndSimpleBinary(i int, forms Lib.List[Form], metas Lib.Set[Meta]) And { @@ -390,31 +368,18 @@ func (a And) Equals(other any) bool { } func (a And) Copy() Form { - fms := &MappedString{} - and := And{ - fms, + return And{ a.index, Lib.ListCpy(a.forms), a.metas.Copy(Lib.Set[Meta].Copy), } - fms.MappableString = &and - return and } func (a And) ToString() string { - return a.MappedString.ToString() -} - -func (a And) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - return "(%s)" -} - -func (a And) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - return " " + mapping[AndConn] + " ", "" -} - -func (a And) GetChildrenForMappedString() []MappableString { - return LsToMappableStringSlice(a.GetChildFormulas()) + return a.forms.ToString( + func(f Form) string { return printer.Str(printer.SurroundChild(f.ToString())) }, + Lib.WithSep(printer.StrConn(ConnAnd)), Lib.WithEmpty(""), + ) } func (a And) ReplaceTermByTerm(old Term, new Term) (Form, bool) { @@ -456,23 +421,18 @@ func (a And) ReplaceMetaByTerm(meta Meta, term Term) Form { // Equivalence type Equ struct { - *MappedString index int f1, f2 Form metas Lib.Cache[Lib.Set[Meta], Equ] } func MakeEquSimple(i int, firstForm, secondForm Form, metas Lib.Set[Meta]) Equ { - fms := &MappedString{} - equ := Equ{ - fms, + return Equ{ i, firstForm, secondForm, Lib.MkCache(metas, Equ.forceGetMetas), } - fms.MappableString = &equ - return equ } func MakeEqu(i int, firstForm, secondForm Form) Equ { @@ -483,32 +443,16 @@ func MakerEqu(firstForm, secondForm Form) Equ { return MakeEqu(MakerIndexFormula(), firstForm, secondForm) } -func (e Equ) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - return "(%s)" -} - -func (e Equ) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - return " " + mapping[EquConn] + " ", "" -} - -func (e Equ) GetChildrenForMappedString() []MappableString { - return LsToMappableStringSlice(e.GetChildFormulas()) -} - func (e Equ) GetIndex() int { return e.index } func (e Equ) GetF1() Form { return e.f1.Copy() } func (e Equ) GetF2() Form { return e.f2.Copy() } func (e Equ) Copy() Form { - fms := &MappedString{} - equ := Equ{ - fms, + return Equ{ e.index, e.GetF1(), e.GetF2(), e.metas.Copy(Lib.Set[Meta].Copy), } - fms.MappableString = &equ - return equ } func (e Equ) forceGetMetas() Lib.Set[Meta] { @@ -522,7 +466,13 @@ func (e Equ) GetMetas() Lib.Set[Meta] { return e.metas.Get(e) } -func (e Equ) ToString() string { return e.ToMappedString(DefaultMapString, true) } +func (e Equ) ToString() string { + return fmt.Sprintf("%s %s %s", + printer.Str(printer.SurroundChild(e.f1.ToString())), + printer.StrConn(ConnEqu), + printer.Str(printer.SurroundChild(e.f2.ToString())), + ) +} func (e Equ) Equals(f any) bool { oth, isEqu := f.(Equ) @@ -583,23 +533,18 @@ func (e Equ) ReplaceMetaByTerm(meta Meta, term Term) Form { // Implication type Imp struct { - *MappedString index int f1, f2 Form metas Lib.Cache[Lib.Set[Meta], Imp] } func MakeImpSimple(i int, firstForm, secondForm Form, metas Lib.Set[Meta]) Imp { - fms := &MappedString{} - imp := Imp{ - fms, + return Imp{ i, firstForm, secondForm, Lib.MkCache(metas, Imp.forceGetMetas), } - fms.MappableString = &imp - return imp } func MakeImp(i int, firstForm, secondForm Form) Imp { @@ -610,32 +555,16 @@ func MakerImp(firstForm, secondForm Form) Imp { return MakeImp(MakerIndexFormula(), firstForm, secondForm) } -func (i Imp) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - return "(%s)" -} - -func (i Imp) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - return " " + mapping[ImpConn] + " ", "" -} - -func (i Imp) GetChildrenForMappedString() []MappableString { - return LsToMappableStringSlice(i.GetChildFormulas()) -} - func (i Imp) GetIndex() int { return i.index } func (i Imp) GetF1() Form { return i.f1.Copy() } func (i Imp) GetF2() Form { return i.f2.Copy() } func (i Imp) Copy() Form { - fms := &MappedString{} - imp := Imp{ - fms, + return Imp{ i.index, i.GetF1(), i.GetF2(), i.metas.Copy(Lib.Set[Meta].Copy), } - fms.MappableString = &imp - return imp } func (i Imp) forceGetMetas() Lib.Set[Meta] { @@ -649,7 +578,13 @@ func (i Imp) GetMetas() Lib.Set[Meta] { return i.metas.Get(i) } -func (i Imp) ToString() string { return i.ToMappedString(DefaultMapString, true) } +func (i Imp) ToString() string { + return fmt.Sprintf("%s %s %s", + printer.Str(printer.SurroundChild(i.f1.ToString())), + printer.StrConn(ConnImp), + printer.Str(printer.SurroundChild(i.f2.ToString())), + ) +} func (i Imp) Equals(other any) bool { if typed, ok := other.(Imp); ok { @@ -713,7 +648,6 @@ func (i Imp) ReplaceMetaByTerm(meta Meta, term Term) Form { // Not type Not struct { - *MappedString index int f Form metas Lib.Cache[Lib.Set[Meta], Not] @@ -722,10 +656,7 @@ type Not struct { /** Constructors **/ func MakeNotSimple(i int, form Form, metas Lib.Set[Meta]) Not { - fms := &MappedString{} - not := Not{fms, i, form, Lib.MkCache(metas, Not.forceGetMetas)} - fms.MappableString = ¬ - return not + return Not{i, form, Lib.MkCache(metas, Not.forceGetMetas)} } func MakeNot(i int, form Form) Not { @@ -773,19 +704,10 @@ func (n Not) Copy() Form { } func (n Not) ToString() string { - return n.MappedString.ToString() -} - -func (n Not) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - return mapping[NotConn] + "(%s)" -} - -func (n Not) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - return "", "" -} - -func (n Not) GetChildrenForMappedString() []MappableString { - return LsToMappableStringSlice(n.GetChildFormulas()) + return fmt.Sprintf("%s%s", + printer.StrConn(ConnNot), + printer.Str(printer.SurroundChild(n.f.ToString())), + ) } func (n Not) ReplaceTermByTerm(old Term, new Term) (Form, bool) { @@ -865,7 +787,6 @@ func getDeepFormWithoutNot(form Form, isEven bool) (Form, bool) { // Predicates type Pred struct { - *MappedString index int id Id tys Lib.List[Ty] @@ -880,17 +801,13 @@ func MakePredSimple( terms Lib.List[Term], metas Lib.Set[Meta], ) Pred { - fms := &MappedString{} - pred := Pred{ - fms, + return Pred{ index, id, tys, terms, Lib.MkCache(metas, Pred.forceGetMetas), } - fms.MappableString = &pred - return pred } func MakePred( @@ -928,41 +845,12 @@ func (p Pred) GetArgs() Lib.List[Term] { return p.args } func (p Pred) RenameVariables() Form { return p } func (p Pred) ToString() string { - return p.MappedString.ToString() -} - -func (p Pred) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - if p.tys.Empty() && p.GetArgs().Empty() { - return p.GetID().ToMappedString(mapping, displayTypes) + "%s" - } - args := []string{} - - if !p.tys.Empty() { - if tv := Lib.ListToString(p.tys, Lib.WithEmpty(mapping[PredEmpty])); tv != "" { - args = append(args, tv) - } - } - - args = append(args, "%s") - - if p.GetID().GetName() == "=" { - return "(" + strings.Join(args, " "+mapping[PredTypeVarSep]+" ") + ")" - } - - return p.GetID().ToMappedString(mapping, displayTypes) + "(" + strings.Join(args, " "+mapping[PredTypeVarSep]+" ") + ")" -} - -func (p Pred) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - if p.GetID().GetName() == "=" { - return " = ", mapping[PredEmpty] - } - - return ", ", mapping[PredEmpty] -} - -func (p Pred) GetChildrenForMappedString() []MappableString { - mappableStringList := Lib.ListMap(p.GetArgs(), Glob.To[MappableString]) - return mappableStringList.GetSlice() + return printer.OnFunctionalArgs( + p.id, + Lib.ListToString(p.tys, Lib.WithSep(printer.StrConn(SepTyArgs)), Lib.WithEmpty("")), + printer.StrConn(SepArgsTyArgs), + p.args, + ) } func (p Pred) Copy() Form { @@ -1110,33 +998,18 @@ func (p Pred) ReplaceMetaByTerm(meta Meta, term Term) Form { // True and False type Top struct { - *MappedString index int } func MakeTop(i int) Top { - fms := &MappedString{} - top := Top{fms, i} - fms.MappableString = &top - return top + return Top{i} } func MakerTop() Top { return MakeTop(MakerIndexFormula()) } -func (t Top) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - return "%s" -} - -func (t Top) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - return "", mapping[TopType] -} - -func (t Top) GetChildrenForMappedString() []MappableString { - return LsToMappableStringSlice(t.GetChildFormulas()) -} - +func (Top) ToString() string { return printer.StrConn(ConnTop) } func (t Top) Copy() Form { return MakeTop(t.GetIndex()) } func (Top) Equals(f any) bool { _, isTop := f.(Top); return isTop } func (Top) GetMetas() Lib.Set[Meta] { return Lib.EmptySet[Meta]() } @@ -1153,33 +1026,18 @@ func (t Top) ReplaceMetaByTerm(meta Meta, term Term) Form { return t } /* Bot (always false) definition */ type Bot struct { - *MappedString index int } func MakeBot(i int) Bot { - fms := &MappedString{} - bot := Bot{fms, i} - fms.MappableString = &bot - return bot + return Bot{i} } func MakerBot() Bot { return MakeBot(MakerIndexFormula()) } -func (b Bot) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - return "%s" -} - -func (b Bot) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - return "", mapping[BotType] -} - -func (b Bot) GetChildrenForMappedString() []MappableString { - return LsToMappableStringSlice(b.GetChildFormulas()) -} - +func (Bot) ToString() string { return printer.StrConn(ConnBot) } func (b Bot) Copy() Form { return MakeBot(b.GetIndex()) } func (Bot) Equals(f any) bool { _, isBot := f.(Bot); return isBot } func (Bot) GetMetas() Lib.Set[Meta] { return Lib.EmptySet[Meta]() } diff --git a/src/AST/formula.go b/src/AST/formula.go index dc14eff9..05ceb63b 100644 --- a/src/AST/formula.go +++ b/src/AST/formula.go @@ -51,7 +51,8 @@ type Form interface { GetChildFormulas() Lib.List[Form] Lib.Copyable[Form] - MappableString + Lib.Stringable + Lib.Comparable ReplaceTermByTerm(old Term, new Term) (Form, bool) SubstTy(old TyGenVar, new Ty) Form diff --git a/src/AST/maker.go b/src/AST/maker.go index c67aa8f4..427701e2 100644 --- a/src/AST/maker.go +++ b/src/AST/maker.go @@ -68,7 +68,7 @@ func Init() { Reset() Id_eq = MakerId("=") EmptyPredEq = MakerPred(Id_eq, Lib.NewList[Ty](), Lib.NewList[Term]()) - initDefaultMap() + initPrinters() initTPTPNativeTypes() } diff --git a/src/AST/mapped_strings.go b/src/AST/mapped_strings.go deleted file mode 100644 index 1496913e..00000000 --- a/src/AST/mapped_strings.go +++ /dev/null @@ -1,172 +0,0 @@ -/** -* Copyright 2022 by the authors (see AUTHORS). -* -* Goéland is an automated theorem prover for first order logic. -* -* This software is governed by the CeCILL license under French law and -* abiding by the rules of distribution of free software. You can use, -* modify and/ or redistribute the software under the terms of the CeCILL -* license as circulated by CEA, CNRS and INRIA at the following URL -* "http://www.cecill.info". -* -* As a counterpart to the access to the source code and rights to copy, -* modify and redistribute granted by the license, users are provided only -* with a limited warranty and the software's author, the holder of the -* economic rights, and the successive licensors have only limited -* liability. -* -* In this respect, the user's attention is drawn to the risks associated -* with loading, using, modifying and/or developing or reproducing the -* software by the user in light of its specific status of free software, -* that may mean that it is complicated to manipulate, and that also -* therefore means that it is reserved for developers and experienced -* professionals having in-depth computer knowledge. Users are therefore -* encouraged to load and test the software's suitability as regards their -* requirements in conditions enabling the security of their systems and/or -* data to be ensured and, more generally, to use and operate it in the -* same conditions as regards security. -* -* The fact that you are presently reading this means that you have had -* knowledge of the CeCILL license and that you accept its terms. -**/ - -/** -* This file provides things. -**/ - -package AST - -import ( - "fmt" - "strings" - - "github.com/GoelandProver/Goeland/Glob" - "github.com/GoelandProver/Goeland/Lib" -) - -type FormulaType int -type MapString map[FormulaType]string - -const ( - AndConn FormulaType = iota - OrConn - ImpConn - EquConn - NotConn - TopType - BotType - AllQuant - ExQuant - AllTypeQuant - QuantVarOpen - QuantVarClose - QuantVarSep - PredEmpty - PredTypeVarSep - TypeVarType -) - -var DefaultMapString = make(map[FormulaType]string) - -func initDefaultMap() { - if Glob.IsPrettyPrint() { - DefaultMapString[AndConn] = "∧" - DefaultMapString[OrConn] = "∨" - DefaultMapString[ImpConn] = "⇒" - DefaultMapString[EquConn] = "⇔" - DefaultMapString[NotConn] = "¬" - DefaultMapString[TopType] = "⊤" - DefaultMapString[BotType] = "⊥" - DefaultMapString[AllQuant] = "∀" - DefaultMapString[ExQuant] = "∃" - DefaultMapString[AllTypeQuant] = "∀" - DefaultMapString[PredEmpty] = "∅" - } else { - DefaultMapString[AndConn] = "&" - DefaultMapString[OrConn] = "|" - DefaultMapString[ImpConn] = "=>" - DefaultMapString[EquConn] = "<=>" - DefaultMapString[NotConn] = "~" - DefaultMapString[TopType] = "$true" - DefaultMapString[BotType] = "$false" - DefaultMapString[AllQuant] = "!" - DefaultMapString[ExQuant] = "?" - DefaultMapString[AllTypeQuant] = ">!" - DefaultMapString[PredEmpty] = "" - } - DefaultMapString[QuantVarOpen] = "[" - DefaultMapString[QuantVarClose] = "]" - DefaultMapString[QuantVarSep] = ":" - DefaultMapString[PredTypeVarSep] = ";" - DefaultMapString[TypeVarType] = "$tType" -} - -type MappableString interface { - Glob.Stringable - Lib.Comparable - - ToMappedString(MapString, bool) string - ToMappedStringSurround(MapString, bool) string - //Return the separator for each child as 1st return, and if there are no children, return the value as 2nd return - ToMappedStringChild(MapString, bool) (separator string, emptyValue string) - GetChildrenForMappedString() []MappableString -} - -type MappedString struct { - MappableString -} - -func (fms MappedString) ToString() string { - return fms.ToMappedString(DefaultMapString, true) -} - -func (fms MappedString) ToMappedString(mapping MapString, displayType bool) string { - surround := fms.ToMappedStringSurround(mapping, displayType) - separator, emptyValue := fms.ToMappedStringChild(mapping, displayType) - children := ListToMappedString(fms.GetChildrenForMappedString(), separator, emptyValue, mapping, displayType) - return fmt.Sprintf(surround, children) -} - -func ListToMappedString[T MappableString](sgbl []T, separator, emptyValue string, mapping MapString, displayTypes bool) string { - strArr := []string{} - - for _, element := range sgbl { - strArr = append(strArr, element.ToMappedString(mapping, displayTypes)) - } - - if len(strArr) == 0 && emptyValue != "" { - strArr = append(strArr, emptyValue) - } - - return strings.Join(strArr, separator) -} - -type SimpleStringMappable string - -func (ssm *SimpleStringMappable) ToString() string { - return string(*ssm) -} - -func (ssm *SimpleStringMappable) Equals(other any) bool { - if typed, ok := other.(*SimpleStringMappable); ok { - return string(*typed) == string(*ssm) - } - - return false -} - -func (ssm *SimpleStringMappable) ToMappedString(MapString, bool) string { - return string(*ssm) -} - -func (ssm *SimpleStringMappable) ToMappedStringSurround(MapString, bool) string { - return "" -} - -func (ssm *SimpleStringMappable) ToMappedStringChild(MapString, bool) (separator string, emptyValue string) { - return "", "" -} - -func (ssm *SimpleStringMappable) GetChildrenForMappedString() []MappableString { - return []MappableString{} -} diff --git a/src/AST/modular-printing.go b/src/AST/modular-printing.go new file mode 100644 index 00000000..edef7192 --- /dev/null +++ b/src/AST/modular-printing.go @@ -0,0 +1,365 @@ +/** +* Copyright 2022 by the authors (see AUTHORS). +* +* Goéland is an automated theorem prover for first order logic. +* +* This software is governed by the CeCILL license under French law and +* abiding by the rules of distribution of free software. You can use, +* modify and/ or redistribute the software under the terms of the CeCILL +* license as circulated by CEA, CNRS and INRIA at the following URL +* "http://www.cecill.info". +* +* As a counterpart to the access to the source code and rights to copy, +* modify and redistribute granted by the license, users are provided only +* with a limited warranty and the software's author, the holder of the +* economic rights, and the successive licensors have only limited +* liability. +* +* In this respect, the user's attention is drawn to the risks associated +* with loading, using, modifying and/or developing or reproducing the +* software by the user in light of its specific status of free software, +* that may mean that it is complicated to manipulate, and that also +* therefore means that it is reserved for developers and experienced +* professionals having in-depth computer knowledge. Users are therefore +* encouraged to load and test the software's suitability as regards their +* requirements in conditions enabling the security of their systems and/or +* data to be ensured and, more generally, to use and operate it in the +* same conditions as regards security. +* +* The fact that you are presently reading this means that you have had +* knowledge of the CeCILL license and that you accept its terms. +**/ + +/** + * This file provides: + * 1. an interface of modular printers + * 2. printers for multiple outputs (default one, TPTP, Rocq, etc) + * + * A modular printer is composed of two objects: + * - the PrinterAction object that defines a *function* to apply on e.g., ids, variables, everything, etc + * so that generic transformation of stuff can be applied. These actions can be composed (e.g., if you + * wish to avoid printing IDs and also sanitize your string, you can get a PrinterAction that does both + * by using noIdAction.Compose(sanitizeAction)). Note that the operations are not always commutative, + * it is your responsibility to ensure that stuff is composed in the right order. + * + * - the PrinterConnective object that defines all the connectives and a printer for them. A PrinterConnective + * can inherit from another one, and if a connective isn't defined for it, it will search for it in its parent + * connective. All PrinterConnective should inherit from the default one (where everything is defined) by default. + * + * If you wish to implement a new printer, simply provide a PrinterAction and a PrinterConnective to it. +**/ + +package AST + +import ( + "fmt" + "unicode" + "unicode/utf8" + + "github.com/GoelandProver/Goeland/Glob" + "github.com/GoelandProver/Goeland/Lib" +) + +var printer_debug Glob.Debugger + +type PrinterAction struct { + genericAction func(string) string // Always executed + actionOnId func(Id) string + actionOnBoundVar func(string, int) string + actionOnMeta func(string, int) string + actionOnType func(string) string + actionOnTypedVar func(Lib.Pair[string, Ty]) string +} + +func (p PrinterAction) Compose(oth PrinterAction) PrinterAction { + return PrinterAction{ + genericAction: func(s string) string { return oth.genericAction(p.genericAction(s)) }, + actionOnId: func(i Id) string { return oth.actionOnId(MakeId(i.index, p.actionOnId(i))) }, + actionOnBoundVar: func(name string, index int) string { + return oth.actionOnBoundVar(p.actionOnBoundVar(name, index), index) + }, + actionOnMeta: func(name string, index int) string { + return oth.actionOnMeta(p.actionOnMeta(name, index), index) + }, + actionOnType: func(name string) string { + return oth.actionOnType(p.actionOnType(name)) + }, + actionOnTypedVar: func(pair Lib.Pair[string, Ty]) string { + return oth.actionOnTypedVar(Lib.MkPair(p.actionOnTypedVar(pair), pair.Snd)) + }, + } +} + +func (p PrinterAction) Str(s string) string { + return p.genericAction(s) +} + +func (p PrinterAction) StrId(i Id) string { + return p.Str(p.actionOnId(i)) +} + +func (p PrinterAction) StrBound(name string, index int) string { + return p.Str(p.actionOnBoundVar(name, index)) +} + +func (p PrinterAction) StrMeta(name string, index int) string { + return p.Str(p.actionOnMeta(name, index)) +} + +func (p PrinterAction) StrTy(name string) string { + return p.Str(p.actionOnType(name)) +} + +func (p PrinterAction) StrTyVar(pair Lib.Pair[string, Ty]) string { + return p.Str(p.actionOnTypedVar(pair)) +} + +func PrinterIdentity(x string) string { return x } +func PrinterIdentityPair[T any](p Lib.Pair[string, T]) string { return p.Fst } +func PrinterIdentity2[T any](s string, _ T) string { return s } + +func MkPrinterAction( + genericAction func(string) string, + actionOnId func(Id) string, + actionOnBoundVar func(string, int) string, + actionOnMeta func(string, int) string, + actionOnType func(string) string, + actionOnTypedVar func(Lib.Pair[string, Ty]) string, +) PrinterAction { + return PrinterAction{genericAction, actionOnId, actionOnBoundVar, actionOnMeta, actionOnType, actionOnTypedVar} +} + +type Connective int + +type PrinterConnective struct { + name string + connectives map[Connective]string + inherit Lib.Option[PrinterConnective] +} + +func (p *PrinterConnective) StrConn(conn Connective) string { + var default_connective PrinterConnective + switch connective := p.inherit.(type) { + case Lib.None[PrinterConnective]: + default_connective = DefaultPrinterConnectives() + p.inherit = Lib.MkSome(default_connective) + case Lib.Some[PrinterConnective]: + default_connective = connective.Val + } + + if val, ok := p.connectives[conn]; ok { + printer_debug( + Lib.MkLazy(func() string { return fmt.Sprintf("Found connective %d in %s as %s", conn, p.name, val) })) + return val + } else { + if p.name == DefaultPrinterConnectives().name { + Glob.Anomaly( + "printer", + fmt.Sprintf("Connective %d not found in default connective", conn), + ) + } + } + + printer_debug(Lib.MkLazy(func() string { + return fmt.Sprintf("Connective %d not found in %s, trying in %s", conn, p.name, default_connective.name) + })) + return default_connective.StrConn(conn) +} + +func (p PrinterConnective) SurroundQuantified(s string) string { + return fmt.Sprintf("%s%s%s", p.StrConn(SurQuantStart), s, p.StrConn(SurQuantEnd)) +} + +func (p PrinterConnective) SurroundArgs(s string) string { + if len(s) == 0 { + return s + } + return fmt.Sprintf("%s%s%s", p.StrConn(SurFunctionalStart), s, p.StrConn(SurFunctionalEnd)) +} + +func (p PrinterConnective) SurroundChild(s string) string { + return fmt.Sprintf("%s%s%s", p.StrConn(SurComplexChildStart), s, p.StrConn(SurComplexChildEnd)) +} + +type Printer struct { + PrinterAction + *PrinterConnective +} + +func (p Printer) OnFunctionalArgs(i Id, tys, con string, args Lib.List[Term]) string { + // Hard-coding of the infix functionals. + // It'd maybe be useful to have an [Infix] generic action but I don't see how to do + // that for now. + infix := Lib.MkListV(Id_eq) + is_infix := Lib.ListMem(i, infix) + arguments := Lib.ListToString(args, Lib.WithSep(p.StrConn(SepArgs)), Lib.WithEmpty("")) + + if is_infix { + // We expect to have between two and three arguments in an infix function + // as it might have a type argument. + if args.Len() < 2 || args.Len() > 3 { + Glob.Anomaly("Printer", fmt.Sprintf( + "invalid number of infix arguments: expected 2 or 3, got %d (in %s)", + args.Len(), + arguments, + )) + } + st := args.Len() - 2 + return fmt.Sprintf("%s %s %s", args.At(st).ToString(), i.ToString(), args.At(st+1).ToString()) + } else { + if len(tys) > 0 { + arguments = tys + con + arguments + } + return fmt.Sprintf("%s%s", i.ToString(), p.SurroundArgs(arguments)) + } +} + +func MkPrinterConnective(name string, connective_map map[Connective]string) PrinterConnective { + return PrinterConnective{ + name: name, + connectives: connective_map, + inherit: Lib.MkNone[PrinterConnective](), + } +} + +const ( + // Formula connectives + ConnAll Connective = iota + ConnEx + ConnAnd + ConnOr + ConnImp + ConnEqu + ConnNot + ConnTop + ConnBot + + // Type connectives + ConnPi + ConnMap + ConnProd + + SepVarsForm // separator between variables and a formula in quantifiers + SepArgs // separator of arguments in functionals + SepTyArgs // separator of type arguments in functionals + SepArgsTyArgs // separator between type arguments and arguments in functionals + SepTyVars // separator between typed variables (in quantifiers) + SepVarTy // separator between a var and its type (in quantifiers) + + SurQuantStart // Stuff that surrounds the variables of quantifiers + SurQuantEnd + SurFunctionalStart // Stuff that surrounds the arguments of functionals + SurFunctionalEnd + SurComplexChildStart // Surrounds "complex" child of formula/type (e.g. (A * B) > C) + SurComplexChildEnd +) + +func DefaultPrinterConnectives() PrinterConnective { + return MkPrinterConnective( + "DefaultPrinterConnective", + map[Connective]string{ + ConnAll: "!", + ConnEx: "?", + ConnAnd: " & ", + ConnOr: " | ", + ConnImp: "=>", + ConnEqu: "<=>", + ConnNot: "~", + ConnTop: "$true", + ConnBot: "$false", + + ConnPi: "!>", + ConnMap: ">", + ConnProd: "*", + + SepVarsForm: ": ", + SepArgs: ", ", + SepTyArgs: ", ", + SepArgsTyArgs: " ; ", + SepTyVars: ", ", + SepVarTy: ": ", + + SurQuantStart: "[", + SurQuantEnd: "]", + SurFunctionalStart: "(", + SurFunctionalEnd: ")", + SurComplexChildStart: "(", + SurComplexChildEnd: ")", + }, + ) +} + +var ( + printer Printer + PrettyPrinter Printer + PrintIDAction PrinterAction + + QuoteID PrinterAction +) + +func initPrinters() { + printer_debug = Glob.CreateDebugger("printer") + + default_connectives := DefaultPrinterConnectives() + printer = Printer{RemoveSuperfluousParenthesesAction(default_connectives), &default_connectives} + + prettyPrinterConnectives := MkPrinterConnective( + "PrettyPrinterConnective", + map[Connective]string{ + ConnAll: "∀", + ConnEx: "∃", + ConnAnd: " ∧ ", + ConnOr: " ∨ ", + ConnImp: "⇒", + ConnEqu: "⇔", + ConnNot: "¬", + ConnTop: "⊤", + ConnBot: "⊥", + + ConnPi: "Π", + ConnMap: "→", + ConnProd: "×", + }, + ) + + PrettyPrinter = Printer{ + RemoveSuperfluousParenthesesAction(prettyPrinterConnectives), + &prettyPrinterConnectives, + } + + PrintIDAction = PrinterAction{ + genericAction: PrinterIdentity, + actionOnId: func(i Id) string { return fmt.Sprintf("%s_%d", i.name, i.index) }, + actionOnBoundVar: PrinterIdentity2[int], + actionOnMeta: PrinterIdentity2[int], + actionOnType: PrinterIdentity, + actionOnTypedVar: PrinterIdentityPair[Ty], + } + + QuoteID = PrinterAction{ + genericAction: PrinterIdentity, + actionOnId: func(i Id) string { + r, _ := utf8.DecodeRuneInString(i.name) + if unicode.IsUpper(r) { + return fmt.Sprintf("'%s'", i.name) + } + return i.name + }, + actionOnBoundVar: PrinterIdentity2[int], + actionOnMeta: PrinterIdentity2[int], + actionOnType: PrinterIdentity, + actionOnTypedVar: PrinterIdentityPair[Ty], + } +} + +func ComposePrinter(p PrinterAction) { + printer.PrinterAction = printer.Compose(p) +} + +func GetPrinter() Printer { + return printer +} + +func SetPrinter(p Printer) { + printer = p +} diff --git a/src/AST/printers.go b/src/AST/printers.go new file mode 100644 index 00000000..dffbe26e --- /dev/null +++ b/src/AST/printers.go @@ -0,0 +1,95 @@ +/** +* Copyright 2022 by the authors (see AUTHORS). +* +* Goéland is an automated theorem prover for first order logic. +* +* This software is governed by the CeCILL license under French law and +* abiding by the rules of distribution of free software. You can use, +* modify and/ or redistribute the software under the terms of the CeCILL +* license as circulated by CEA, CNRS and INRIA at the following URL +* "http://www.cecill.info". +* +* As a counterpart to the access to the source code and rights to copy, +* modify and redistribute granted by the license, users are provided only +* with a limited warranty and the software's author, the holder of the +* economic rights, and the successive licensors have only limited +* liability. +* +* In this respect, the user's attention is drawn to the risks associated +* with loading, using, modifying and/or developing or reproducing the +* software by the user in light of its specific status of free software, +* that may mean that it is complicated to manipulate, and that also +* therefore means that it is reserved for developers and experienced +* professionals having in-depth computer knowledge. Users are therefore +* encouraged to load and test the software's suitability as regards their +* requirements in conditions enabling the security of their systems and/or +* data to be ensured and, more generally, to use and operate it in the +* same conditions as regards security. +* +* The fact that you are presently reading this means that you have had +* knowledge of the CeCILL license and that you accept its terms. +**/ + +/** + * This file stores the different printers we have in Goeland. + **/ + +package AST + +import ( + "github.com/GoelandProver/Goeland/Lib" + "strings" +) + +func RemoveSuperfluousParenthesesAction(connectives PrinterConnective) PrinterAction { + return PrinterAction{ + genericAction: func(s string) string { + if len(s) == 0 { + return s + } + + complexChildStart := connectives.StrConn(SurComplexChildStart) + complexChildEnd := connectives.StrConn(SurComplexChildEnd) + if s[:len(complexChildStart)] == complexChildStart && + s[len(s)-len(complexChildEnd):] == complexChildEnd { + tentative_str := s[len(complexChildStart) : len(s)-len(complexChildEnd)] + is_open := 0 + for i, char := range tentative_str { + if len(complexChildStart) <= i && tentative_str[i-len(complexChildStart):i] == complexChildStart { + is_open += 1 + } + if len(complexChildEnd) <= i && tentative_str[i-len(complexChildEnd):i] == complexChildEnd { + is_open -= 1 + } + if char == ' ' && is_open == 0 { + return s + } + } + return tentative_str + } + + return s + }, + actionOnId: func(i Id) string { return i.name }, + actionOnBoundVar: func(s string, index int) string { return s }, + actionOnMeta: func(s string, index int) string { return s }, + actionOnType: func(s string) string { return s }, + actionOnTypedVar: func(p Lib.Pair[string, Ty]) string { return p.Fst }, + } +} + +func SanitizerAction(connectives PrinterConnective, forbidden_chars []string) PrinterAction { + return PrinterAction{ + genericAction: func(s string) string { + for _, c := range forbidden_chars { + s = strings.ReplaceAll(s, c, "_") + } + return s + }, + actionOnId: func(i Id) string { return i.name }, + actionOnBoundVar: func(s string, index int) string { return s }, + actionOnMeta: func(s string, index int) string { return s }, + actionOnType: func(s string) string { return s }, + actionOnTypedVar: func(p Lib.Pair[string, Ty]) string { return p.Fst }, + } +} diff --git a/src/AST/quantifiers.go b/src/AST/quantifiers.go index 5ceabff2..a7e8a958 100644 --- a/src/AST/quantifiers.go +++ b/src/AST/quantifiers.go @@ -38,33 +38,26 @@ package AST import ( "fmt" - "strings" "github.com/GoelandProver/Goeland/Lib" ) type quantifier struct { - *MappedString metas Lib.Cache[Lib.Set[Meta], quantifier] index int varList Lib.List[TypedVar] subForm Form - symbol FormulaType + symbol Connective } -func makeQuantifier(i int, vars Lib.List[TypedVar], subForm Form, metas Lib.Set[Meta], symbol FormulaType) quantifier { - fms := &MappedString{} - qua := quantifier{ - fms, +func makeQuantifier(i int, vars Lib.List[TypedVar], subForm Form, metas Lib.Set[Meta], symbol Connective) quantifier { + return quantifier{ Lib.MkCache(metas, quantifier.forceGetMetas), i, vars, subForm, symbol, } - fms.MappableString = &qua - - return qua } func (q quantifier) GetIndex() int { @@ -88,33 +81,17 @@ func (q quantifier) GetMetas() Lib.Set[Meta] { } func (q quantifier) ToString() string { - return q.MappedString.ToString() -} - -func (q quantifier) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - return " ", "" -} - -var varSeparator = " " - -func ChangeVarSeparator(sep string) string { - old := varSeparator - varSeparator = sep - return old -} - -func (q quantifier) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - varStrings := []string{} - - str := mapping[QuantVarOpen] - str += ListToMappedString(q.GetVarList().GetSlice(), varSeparator, "", mapping, false) - varStrings = append(varStrings, str+mapping[QuantVarClose]) - - return "(" + mapping[q.symbol] + " " + strings.Join(varStrings, " ") + mapping[QuantVarSep] + " (%s))" -} - -func (q quantifier) GetChildrenForMappedString() []MappableString { - return LsToMappableStringSlice(q.GetChildFormulas()) + return fmt.Sprintf( + "%s %s%s%s", + printer.StrConn(q.symbol), + printer.SurroundQuantified( + Lib.ListMap(q.varList, func(t TypedVar) Lib.Pair[string, Ty] { + return Lib.MkPair(t.name, t.ty) + }).ToString(printer.StrTyVar, Lib.WithSep(printer.StrConn(SepTyVars)), Lib.WithEmpty("")), + ), + printer.StrConn(SepVarsForm), + printer.Str(q.subForm.ToString()), + ) } func (q quantifier) GetChildFormulas() Lib.List[Form] { diff --git a/src/AST/term.go b/src/AST/term.go index 116efe92..bfe5f5f3 100644 --- a/src/AST/term.go +++ b/src/AST/term.go @@ -42,7 +42,8 @@ import ( /* Term */ type Term interface { - MappableString + Lib.Comparable + Lib.Stringable Lib.Copyable[Term] GetIndex() int GetName() string @@ -59,38 +60,23 @@ type Term interface { /*** Makers ***/ func MakeId(i int, s string) Id { - fms := &MappedString{} - id := Id{fms, i, s} - fms.MappableString = &id - return id + return Id{i, s} } func MakeQuotedId(i int, s string) Id { - fms := &MappedString{} - id := Id{fms, i, "" + s + "'"} - fms.MappableString = &id - return id + return Id{i, "" + s + "'"} } func MakeVar(i int, s string) Var { - fms := &MappedString{} - newVar := Var{fms, i, s} - fms.MappableString = &newVar - return newVar + return Var{i, s} } func MakeMeta(index, occurence int, s string, f int, ty Ty) Meta { - fms := &MappedString{} - meta := Meta{fms, index, occurence, s, f, ty} - fms.MappableString = &meta - return meta + return Meta{index, occurence, s, f, ty} } func MakeFun(p Id, ty_args Lib.List[Ty], args Lib.List[Term], metas Lib.Set[Meta]) Fun { - fms := &MappedString{} - fun := Fun{fms, p, ty_args, args, Lib.MkCache(metas, Fun.forceGetMetas)} - fms.MappableString = fun - return fun + return Fun{p, ty_args, args, Lib.MkCache(metas, Fun.forceGetMetas)} } /*** Functions **/ diff --git a/src/AST/termsDef.go b/src/AST/termsDef.go index beade5e8..5ceef280 100644 --- a/src/AST/termsDef.go +++ b/src/AST/termsDef.go @@ -37,10 +37,7 @@ package AST import ( - "fmt" "strings" - "unicode" - "unicode/utf8" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" @@ -50,7 +47,6 @@ import ( // Predicates / functions symbols type Id struct { - *MappedString index int name string } @@ -63,39 +59,7 @@ func (i Id) Copy() Term { return MakeId(i.GetIndex(), i.GetName() func (Id) ToMeta() Meta { return MakeEmptyMeta() } func (Id) GetMetas() Lib.Set[Meta] { return Lib.EmptySet[Meta]() } func (Id) GetMetaList() Lib.List[Meta] { return Lib.NewList[Meta]() } - -var ToStringId = func(i Id) string { - return fmt.Sprintf("%s_%d", i.GetName(), i.GetIndex()) -} - -func (i Id) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - return "%s" -} - -func (i Id) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - return "", ToStringId(i) -} - -func NoIdToString(i Id) string { - return fmt.Sprintf("%s", i.GetName()) -} - -func QuotedToString(i Id) string { - if i.GetName() == "Goeland_I" || strings.Contains(i.GetName(), "Sko_") { - return fmt.Sprintf("%s", i.GetName()) - } else { - r, _ := utf8.DecodeRuneInString(i.GetName()) - if unicode.IsUpper(r) { - return fmt.Sprintf("'%s'", i.GetName()) - } else { - return fmt.Sprintf("%s", i.GetName()) - } - } -} - -func (i Id) GetChildrenForMappedString() []MappableString { - return []MappableString{} -} +func (i Id) ToString() string { return printer.StrId(i) } func (i Id) Equals(t any) bool { if typed, ok := t.(Id); ok { @@ -147,55 +111,19 @@ func (i Id) Less(u any) bool { // n-ary functions type Fun struct { - *MappedString p Id tys Lib.List[Ty] args Lib.List[Term] metas Lib.Cache[Lib.Set[Meta], Fun] } -func (f Fun) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - return f.ToMappedStringSurroundWithId(f.GetID().ToMappedString(mapping, displayTypes), mapping, displayTypes) -} - -func (f Fun) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - return ", ", mapping[PredEmpty] -} - -func (f Fun) ToMappedStringSurroundWithId(idString string, mapping MapString, displayTypes bool) string { - if f.tys.Empty() && f.GetArgs().Empty() { - return idString + "%s" - } - - args := []string{} - if !f.tys.Empty() { - if tv := Lib.ListToString(f.tys, Lib.WithEmpty(mapping[PredEmpty])); tv != "" { - args = append(args, tv) - } - } - - args = append(args, "%s") - - str := idString + "(" + strings.Join(args, mapping[PredTypeVarSep]) + ")" - - return str -} - -func ToFlatternStringSurrountWithId(f Fun, idString string, mapping MapString, displayTypes bool) string { - if f.GetArgs().Len() == 0 { - return idString + "%s" - } - args := []string{} - args = append(args, "%s") - - str := idString + "_" + strings.Join(args, mapping[PredTypeVarSep]) - - return str -} - -func (f Fun) GetChildrenForMappedString() []MappableString { - mappableList := Lib.ListMap(f.GetArgs(), Glob.To[MappableString]) - return mappableList.GetSlice() +func (f Fun) ToString() string { + return printer.OnFunctionalArgs( + f.p, + Lib.ListToString(f.tys, Lib.WithSep(printer.StrConn(SepTyArgs)), Lib.WithEmpty("")), + printer.StrConn(SepArgsTyArgs), + f.args, + ) } func (f Fun) GetID() Id { return f.p.Copy().(Id) } @@ -332,11 +260,11 @@ func (f Fun) Less(u any) bool { // Bound variables type Var struct { - *MappedString index int name string } +func (v Var) ToString() string { return printer.StrBound(v.name, v.index) } func (v Var) GetIndex() int { return v.index } func (v Var) GetName() string { return v.name } func (v Var) IsMeta() bool { return false } @@ -366,26 +294,6 @@ func (v Var) ReplaceSubTermBy(original_term, new_term Term) Term { func (v Var) SubstTy(TyGenVar, Ty) Term { return v } -func (v Var) ToMappedString(map_ MapString, type_ bool) string { - return v.GetName() -} - -func (v Var) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - return "%s" -} - -func (v Var) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - if displayTypes { - return "", fmt.Sprintf("%s_%d", v.GetName(), v.GetIndex()) - } else { - return "", v.GetName() - } -} - -func (v Var) GetChildrenForMappedString() []MappableString { - return []MappableString{} -} - func (v Var) Less(u any) bool { switch t := u.(type) { case Term: @@ -400,7 +308,6 @@ func (v Var) Less(u any) bool { // Meta/Free variables type Meta struct { - *MappedString index int occurence int name string @@ -408,7 +315,8 @@ type Meta struct { ty Ty } -func (m Meta) GetFormula() int { return m.formula } +func (m Meta) ToString() string { return printer.StrMeta(m.name, m.index) } +func (m Meta) GetFormula() int { return m.formula } func (m Meta) GetName() string { return m.name } func (m Meta) GetIndex() int { return m.index } @@ -420,22 +328,6 @@ func (m Meta) GetMetas() Lib.Set[Meta] { return Lib.Singleton(m) } func (m Meta) GetMetaList() Lib.List[Meta] { return Lib.MkListV(m) } func (m Meta) GetTy() Ty { return m.ty } -func (m Meta) ToMappedStringSurround(mapping MapString, displayTypes bool) string { - return "%s" -} - -func (m Meta) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - if displayTypes { - return "", fmt.Sprintf("%s_%d : %s", m.GetName(), m.GetIndex(), m.ty.ToString()) - } else { - return "", fmt.Sprintf("%s_%d", m.GetName(), m.GetIndex()) - } -} - -func (m Meta) GetChildrenForMappedString() []MappableString { - return []MappableString{} -} - func (m Meta) Equals(t any) bool { if typed, ok := t.(Meta); ok { return typed.GetIndex() == m.GetIndex() diff --git a/src/AST/ty-syntax.go b/src/AST/ty-syntax.go index 8df32395..5ea889c8 100644 --- a/src/AST/ty-syntax.go +++ b/src/AST/ty-syntax.go @@ -53,10 +53,10 @@ type TyGenVar interface { } type Ty interface { + Lib.Stringable + Lib.Comparable + Lib.Copyable[Ty] isTy() - ToString() string - Equals(any) bool - Copy() Ty SubstTy(TyGenVar, Ty) Ty } @@ -65,8 +65,10 @@ type tyVar struct { repr string } -func (tyVar) isTy() {} -func (v tyVar) ToString() string { return v.repr } +func (tyVar) isTy() {} +func (v tyVar) ToString() string { + return printer.StrBound(v.repr, 0) +} func (v tyVar) Equals(oth any) bool { if ov, ok := oth.(tyVar); ok { return v.repr == ov.repr @@ -82,9 +84,11 @@ type TyBound struct { index int } -func (TyBound) isTy() {} -func (TyBound) isGenVar() {} -func (b TyBound) ToString() string { return b.name } +func (TyBound) isTy() {} +func (TyBound) isGenVar() {} +func (b TyBound) ToString() string { + return printer.StrBound(b.name, b.index) +} func (b TyBound) Equals(oth any) bool { if bv, ok := oth.(TyBound); ok { return b.name == bv.name @@ -107,9 +111,11 @@ type TyMeta struct { formula int // for compatibility with term metas } -func (TyMeta) isTy() {} -func (TyMeta) isGenVar() {} -func (m TyMeta) ToString() string { return fmt.Sprintf("%s_%d", m.name, m.index) } +func (TyMeta) isTy() {} +func (TyMeta) isGenVar() {} +func (m TyMeta) ToString() string { + return printer.StrMeta(m.name, m.index) +} func (m TyMeta) Equals(oth any) bool { if om, ok := oth.(TyMeta); ok { return m.name == om.name && m.index == om.index @@ -145,10 +151,13 @@ type TyConstr struct { func (TyConstr) isTy() {} func (c TyConstr) ToString() string { - if c.args.Len() == 0 { - return c.symbol + if c.args.Empty() { + return printer.StrTy(c.symbol) } - return c.symbol + "(" + Lib.ListToString(c.args, Lib.WithEmpty("")) + ")" + return fmt.Sprintf("%s%s", + printer.StrTy(c.symbol), + printer.SurroundArgs(Lib.ListToString(c.args, Lib.WithSep(printer.StrConn(SepArgs)), Lib.WithEmpty(""))), + ) } func (c TyConstr) Equals(oth any) bool { @@ -185,7 +194,10 @@ type TyProd struct { func (TyProd) isTy() {} func (p TyProd) ToString() string { - return "(" + Lib.ListToString(p.args, Lib.WithSep(" * "), Lib.WithEmpty("")) + ")" + return p.args.ToString( + func(ty Ty) string { return printer.Str(printer.SurroundChild(ty.ToString())) }, + Lib.WithSep(printer.StrConn(ConnProd)), Lib.WithEmpty(""), + ) } func (p TyProd) GetTys() Lib.List[Ty] { @@ -215,7 +227,11 @@ type TyFunc struct { func (TyFunc) isTy() {} func (f TyFunc) ToString() string { - return f.in.ToString() + " > " + f.out.ToString() + return fmt.Sprintf("%s %s %s", + printer.Str(printer.SurroundChild(f.in.ToString())), + printer.StrConn(ConnMap), + printer.Str(printer.SurroundChild(f.out.ToString())), + ) } func (f TyFunc) Equals(oth any) bool { if of, ok := oth.(TyFunc); ok { @@ -239,7 +255,15 @@ type TyPi struct { func (TyPi) isTy() {} func (p TyPi) ToString() string { - return "!> [" + p.vars.ToString(func(s string) string { return s }, Lib.WithEmpty("")) + "] : (" + p.ty.ToString() + ")" + return fmt.Sprintf( + "%s %s%s%s", + printer.StrConn(ConnPi), + printer.SurroundQuantified( + p.vars.ToString(PrinterIdentity, Lib.WithSep(printer.StrConn(SepTyVars)), Lib.WithEmpty("")), + ), + printer.StrConn(SepVarsForm), + printer.Str(p.ty.ToString()), + ) } func (p TyPi) Equals(oth any) bool { if op, ok := oth.(TyPi); ok { @@ -465,3 +489,22 @@ func TermToTy(trm Term) Ty { ) return nil } + +func mkDefaultFunctionalType(number_of_arguments int, out_type Ty) Ty { + if number_of_arguments == 0 { + return out_type + } + tys := Lib.MkList[Ty](number_of_arguments) + for i := 0; i < number_of_arguments; i++ { + tys.Upd(i, TIndividual()) + } + return MkTyFunc(MkTyProd(tys), out_type) +} + +func MkDefaultPredType(number_of_arguments int) Ty { + return mkDefaultFunctionalType(number_of_arguments, TProp()) +} + +func MkDefaultFunctionType(number_of_arguments int) Ty { + return mkDefaultFunctionalType(number_of_arguments, TIndividual()) +} diff --git a/src/AST/typed-vars.go b/src/AST/typed-vars.go index d3e42e6c..05254f77 100644 --- a/src/AST/typed-vars.go +++ b/src/AST/typed-vars.go @@ -37,7 +37,7 @@ package AST import ( - "fmt" + "github.com/GoelandProver/Goeland/Lib" ) type TypedVar struct { @@ -59,7 +59,7 @@ func (v TypedVar) Equals(oth any) bool { } func (v TypedVar) ToString() string { - return fmt.Sprintf("%s : %s", v.name, v.ty.ToString()) + return printer.StrTyVar(Lib.MkPair(v.name, v.ty)) } func (v TypedVar) GetName() string { @@ -105,29 +105,3 @@ func MakerTypedVar(name string, ty Ty) TypedVar { return vr } } - -// ----------------------------------------------------------------------------- -// Mappable string interface - -func (v TypedVar) GetChildrenForMappedString() []MappableString { - return []MappableString{} -} - -func (v TypedVar) ToMappedString(map_ MapString, type_ bool) string { - if type_ { - return fmt.Sprintf("%s : %s", v.name, v.ty.ToString()) - } - return v.name -} - -func (v TypedVar) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) { - if displayTypes { - return "", fmt.Sprintf("%s : %s", v.name, v.ty.ToString()) - } else { - return "", v.name - } -} - -func (TypedVar) ToMappedStringSurround(_ MapString, _ bool) string { - return "%s" -} diff --git a/src/Core/Sko/interface.go b/src/Core/Sko/interface.go index b94c1d5f..8ef14586 100644 --- a/src/Core/Sko/interface.go +++ b/src/Core/Sko/interface.go @@ -62,7 +62,7 @@ type Skolemization interface { */ func genFreshSymbol(existingSymbols *Lib.Set[AST.Id], x AST.TypedVar) AST.Id { symbol := AST.MakerNewId( - fmt.Sprintf("skolem@%v", x.GetName()), + fmt.Sprintf("skolem@%v@%d", x.GetName(), existingSymbols.Cardinal()), ) *existingSymbols = existingSymbols.Add(symbol) diff --git a/src/Core/form_and_terms.go b/src/Core/form_and_terms.go index fc05cc52..0a9e3234 100644 --- a/src/Core/form_and_terms.go +++ b/src/Core/form_and_terms.go @@ -38,7 +38,6 @@ package Core import ( "github.com/GoelandProver/Goeland/AST" - "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" ) @@ -81,7 +80,7 @@ func (fat FormAndTerms) Equals(fat2 FormAndTerms) bool { } func (fat FormAndTerms) ToString() string { - return fat.GetForm().ToMappedString(AST.DefaultMapString, Glob.GetTypeProof()) + return fat.GetForm().ToString() } func (fat FormAndTerms) SubstituteBy( diff --git a/src/Core/skolemisation.go b/src/Core/skolemisation.go index 66238d50..e8947805 100644 --- a/src/Core/skolemisation.go +++ b/src/Core/skolemisation.go @@ -32,6 +32,7 @@ package Core import ( + "fmt" "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Core/Sko" "github.com/GoelandProver/Goeland/Glob" @@ -128,6 +129,7 @@ func realSkolemize( if AST.IsTType(x.GetTy()) { id := AST.MakerId("skoTy") + id = AST.MakerId(fmt.Sprintf("skoTy@%d", id.GetIndex())) res = deltaForm.SubstTy(x.ToTyBoundVar(), AST.MkTyConst(id.ToString())) } else { selectedSkolemization, res = selectedSkolemization.Skolemize( diff --git a/src/Mods/equality/bse/equality_problem.go b/src/Mods/equality/bse/equality_problem.go index 78c35bc6..803d84e1 100644 --- a/src/Mods/equality/bse/equality_problem.go +++ b/src/Mods/equality/bse/equality_problem.go @@ -85,7 +85,7 @@ func (ep EqualityProblem) AxiomsToTPTPString() string { } func (ep EqualityProblem) ToTPTPString() string { - return ep.GetS().ToMappedString(AST.DefaultMapString, false) + " = " + ep.GetT().ToMappedString(AST.DefaultMapString, false) + return ep.GetS().ToString() + " = " + ep.GetT().ToString() } /* Apply a substitution on an equality problem */ diff --git a/src/Mods/equality/bse/equality_problem_list.go b/src/Mods/equality/bse/equality_problem_list.go index 4491dff3..fce98743 100644 --- a/src/Mods/equality/bse/equality_problem_list.go +++ b/src/Mods/equality/bse/equality_problem_list.go @@ -150,7 +150,7 @@ func (epml EqualityProblemMultiList) GetMetasToTPTPString() string { if metas.Cardinal() > 0 { result = "? [" for _, meta := range metas.Elements().GetSlice() { - result += meta.ToMappedString(AST.DefaultMapString, false) + ", " + result += meta.ToString() + ", " } result = result[:len(result)-2] + "] : " } diff --git a/src/Mods/equality/eqStruct/term_pair.go b/src/Mods/equality/eqStruct/term_pair.go index 8009e621..0b79f0bb 100644 --- a/src/Mods/equality/eqStruct/term_pair.go +++ b/src/Mods/equality/eqStruct/term_pair.go @@ -94,7 +94,7 @@ func (tp TermPair) ToString() string { return tp.GetT1().ToString() + " ≈ " + tp.GetT2().ToString() } func (tp TermPair) ToTPTPString() string { - return tp.GetT1().ToMappedString(AST.DefaultMapString, false) + " = " + tp.GetT2().ToMappedString(AST.DefaultMapString, false) + return tp.GetT1().ToString() + " = " + tp.GetT2().ToString() } func MakeTermPair(t1, t2 AST.Term) TermPair { return TermPair{t1.Copy(), t2.Copy()} diff --git a/src/Mods/lambdapi/context.go b/src/Mods/lambdapi/context.go index 953fb17f..50102369 100644 --- a/src/Mods/lambdapi/context.go +++ b/src/Mods/lambdapi/context.go @@ -197,7 +197,7 @@ func getContextFromFormula(root AST.Form) []string { result = append(result, getContextFromFormula(nf.GetForm())...) case AST.Pred: if !nf.GetID().Equals(AST.Id_eq) { - result = append(result, mapDefault(fmt.Sprintf("symbol %s;", nf.GetID().ToMappedString(lambdaPiMapConnectors, false)))) + result = append(result, mapDefault(fmt.Sprintf("symbol %s;", nf.GetID().ToString()))) } for _, term := range nf.GetArgs().GetSlice() { result = append(result, clean(result, getContextFromTerm(term))...) @@ -231,9 +231,9 @@ func getIdsFromFormula(root AST.Form) []Glob.Pair[string, string] { case AST.Not: result = getIdsFromFormula(nf.GetForm()) case AST.Pred: - result = append(result, Glob.MakePair(nf.GetID().GetName(), nf.GetID().ToMappedString(lambdaPiMapConnectors, false))) + result = append(result, Glob.MakePair(nf.GetID().GetName(), nf.GetID().ToString())) for _, f := range nf.GetArgs().GetSlice() { - result = append(result, Glob.MakePair(f.GetName(), f.ToMappedString(lambdaPiMapConnectors, false))) + result = append(result, Glob.MakePair(f.GetName(), f.ToString())) } } return result @@ -243,7 +243,7 @@ func getContextFromTerm(trm AST.Term) []string { result := []string{} if fun, isFun := trm.(AST.Fun); isFun { - result = append(result, mapDefault(fmt.Sprintf("symbol %s;", fun.GetID().ToMappedString(lambdaPiMapConnectors, false)))) + result = append(result, mapDefault(fmt.Sprintf("symbol %s;", fun.GetID().ToString()))) for _, term := range fun.GetArgs().GetSlice() { result = append(result, clean(result, getContextFromTerm(term))...) } @@ -272,7 +272,7 @@ func clean(set, add []string) []string { func contextualizeMetas(metaList Lib.List[AST.Meta]) string { result := []string{} for _, meta := range metaList.GetSlice() { - result = append(result, meta.ToMappedString(lambdaPiMapConnectors, false)) + result = append(result, meta.ToString()) } return "symbol " + strings.Join(result, " ") + " : τ (ι);" } diff --git a/src/Mods/lambdapi/formDecorator.go b/src/Mods/lambdapi/formDecorator.go index 267effde..e7847d3a 100644 --- a/src/Mods/lambdapi/formDecorator.go +++ b/src/Mods/lambdapi/formDecorator.go @@ -32,137 +32,137 @@ package lambdapi import ( - "fmt" + _ "fmt" - "github.com/GoelandProver/Goeland/AST" - "github.com/GoelandProver/Goeland/Lib" + _ "github.com/GoelandProver/Goeland/AST" + _ "github.com/GoelandProver/Goeland/Lib" ) -type DecoratedAll struct { - AST.All -} - -func MakeDecoratedAll(all AST.All) DecoratedAll { - if typed, ok := all.Copy().(AST.All); ok { - all = typed - } - decorated := DecoratedAll{all} - decorated.MappedString.MappableString = decorated - return decorated -} - -func (da DecoratedAll) ToMappedStringSurround(mapping AST.MapString, displayTypes bool) string { - return QuantifierToMappedString(mapping[AST.AllQuant], da.GetVarList()) -} - -func QuantifierToMappedString(quant string, varList Lib.List[AST.TypedVar]) string { - if varList.Len() == 0 { - return "%s" - } else { - result := "(" + quant + " (" + toLambdaIntroString(varList.At(0), "") + ", %s))" - result = fmt.Sprintf(result, QuantifierToMappedString(quant, varList.Slice(1, varList.Len()))) - return result - } -} - -type DecoratedEx struct { - AST.Ex -} - -func MakeDecoratedEx(ex AST.Ex) DecoratedEx { - if typed, ok := ex.Copy().(AST.Ex); ok { - ex = typed - } - decorated := DecoratedEx{ex} - decorated.MappedString.MappableString = decorated - return decorated -} - -func (de DecoratedEx) ToMappedStringSurround(mapping AST.MapString, displayTypes bool) string { - return QuantifierToMappedString(mapping[AST.ExQuant], de.GetVarList()) -} - -type DecoratedVar struct { - AST.Var -} - -func MakeDecoratedVar(newVar AST.Var) DecoratedVar { - if typed, ok := newVar.Copy().(AST.Var); ok { - newVar = typed - } - decorated := DecoratedVar{newVar} - decorated.MappedString.MappableString = decorated - return decorated -} - -func (da DecoratedVar) ToMappedStringChild(mapping AST.MapString, displayTypes bool) (separator, emptyValue string) { - emptyValue = getFromContext(da.Var) - return "", emptyValue -} - -type DecoratedPred struct { - AST.Pred -} - -func MakeDecoratedPred(newPred AST.Pred) DecoratedPred { - if typed, ok := newPred.Copy().(AST.Pred); ok { - newPred = typed - } - decorated := DecoratedPred{newPred} - decorated.MappedString.MappableString = decorated - return decorated -} - -func (dp DecoratedPred) ToMappedStringChild(mapping AST.MapString, displayTypes bool) (separator, emptyValue string) { - _, emptyValue = dp.Pred.ToMappedStringChild(mapping, displayTypes) - return " ", emptyValue -} - -type DecoratedFun struct { - AST.Fun -} - -func MakeDecoratedFun(newFun AST.Fun) DecoratedFun { - if typed, ok := newFun.Copy().(AST.Fun); ok { - newFun = typed - } - decorated := DecoratedFun{newFun} - decorated.MappedString.MappableString = decorated - return decorated -} - -func (df DecoratedFun) ToMappedStringChild(mapping AST.MapString, displayTypes bool) (separator, emptyValue string) { - return " ", mapping[AST.PredEmpty] -} - -func (df DecoratedFun) ToMappedStringSurround(mapping AST.MapString, displayTypes bool) string { - result := df.Fun.ToMappedStringSurround(mapping, displayTypes) - - possible, exists := context.GetExists(df.Fun) - if exists { - if result[:6] == "skolem" { - result = string(possible) + "%s" - } else { - result = df.Fun.ToMappedStringSurroundWithId(string(possible), mapping, displayTypes) - } - } - - return result -} - -func decorateForm(form AST.MappableString) AST.MappableString { - switch typed := form.(type) { - case AST.All: - return MakeDecoratedAll(typed) - case AST.Ex: - return MakeDecoratedEx(typed) - case AST.Var: - return MakeDecoratedVar(typed) - case AST.Pred: - return MakeDecoratedPred(typed) - case AST.Fun: - return MakeDecoratedFun(typed) - default: - return typed - } -} +// type DecoratedAll struct { +// AST.All +// } + +// func MakeDecoratedAll(all AST.All) DecoratedAll { +// if typed, ok := all.Copy().(AST.All); ok { +// all = typed +// } +// decorated := DecoratedAll{all} +// decorated.MappedString.MappableString = decorated +// return decorated +// } + +// func (da DecoratedAll) ToMappedStringSurround(mapping AST.MapString, displayTypes bool) string { +// return QuantifierToMappedString(mapping[AST.AllQuant], da.GetVarList()) +// } + +// func QuantifierToMappedString(quant string, varList Lib.List[AST.TypedVar]) string { +// if varList.Len() == 0 { +// return "%s" +// } else { +// result := "(" + quant + " (" + toLambdaIntroString(varList.At(0), "") + ", %s))" +// result = fmt.Sprintf(result, QuantifierToMappedString(quant, varList.Slice(1, varList.Len()))) +// return result +// } +// } + +// type DecoratedEx struct { +// AST.Ex +// } + +// func MakeDecoratedEx(ex AST.Ex) DecoratedEx { +// if typed, ok := ex.Copy().(AST.Ex); ok { +// ex = typed +// } +// decorated := DecoratedEx{ex} +// decorated.MappedString.MappableString = decorated +// return decorated +// } + +// func (de DecoratedEx) ToMappedStringSurround(mapping AST.MapString, displayTypes bool) string { +// return QuantifierToMappedString(mapping[AST.ExQuant], de.GetVarList()) +// } + +// type DecoratedVar struct { +// AST.Var +// } + +// func MakeDecoratedVar(newVar AST.Var) DecoratedVar { +// if typed, ok := newVar.Copy().(AST.Var); ok { +// newVar = typed +// } +// decorated := DecoratedVar{newVar} +// decorated.MappedString.MappableString = decorated +// return decorated +// } + +// func (da DecoratedVar) ToMappedStringChild(mapping AST.MapString, displayTypes bool) (separator, emptyValue string) { +// emptyValue = getFromContext(da.Var) +// return "", emptyValue +// } + +// type DecoratedPred struct { +// AST.Pred +// } + +// func MakeDecoratedPred(newPred AST.Pred) DecoratedPred { +// if typed, ok := newPred.Copy().(AST.Pred); ok { +// newPred = typed +// } +// decorated := DecoratedPred{newPred} +// decorated.MappedString.MappableString = decorated +// return decorated +// } + +// func (dp DecoratedPred) ToMappedStringChild(mapping AST.MapString, displayTypes bool) (separator, emptyValue string) { +// _, emptyValue = dp.Pred.ToMappedStringChild(mapping, displayTypes) +// return " ", emptyValue +// } + +// type DecoratedFun struct { +// AST.Fun +// } + +// func MakeDecoratedFun(newFun AST.Fun) DecoratedFun { +// if typed, ok := newFun.Copy().(AST.Fun); ok { +// newFun = typed +// } +// decorated := DecoratedFun{newFun} +// decorated.MappedString.MappableString = decorated +// return decorated +// } + +// func (df DecoratedFun) ToMappedStringChild(mapping AST.MapString, displayTypes bool) (separator, emptyValue string) { +// return " ", mapping[AST.PredEmpty] +// } + +// func (df DecoratedFun) ToMappedStringSurround(mapping AST.MapString, displayTypes bool) string { +// result := df.Fun.ToMappedStringSurround(mapping, displayTypes) + +// possible, exists := context.GetExists(df.Fun) +// if exists { +// if result[:6] == "skolem" { +// result = string(possible) + "%s" +// } else { +// result = df.Fun.ToMappedStringSurroundWithId(string(possible), mapping, displayTypes) +// } +// } + +// return result +// } + +// func decorateForm(form AST.MappableString) AST.MappableString { +// switch typed := form.(type) { +// case AST.All: +// return MakeDecoratedAll(typed) +// case AST.Ex: +// return MakeDecoratedEx(typed) +// case AST.Var: +// return MakeDecoratedVar(typed) +// case AST.Pred: +// return MakeDecoratedPred(typed) +// case AST.Fun: +// return MakeDecoratedFun(typed) +// default: +// return typed +// } +// } diff --git a/src/Mods/lambdapi/output.go b/src/Mods/lambdapi/output.go index 0e171326..1e121be0 100644 --- a/src/Mods/lambdapi/output.go +++ b/src/Mods/lambdapi/output.go @@ -43,24 +43,24 @@ import ( var contextEnabled bool = false -var lambdaPiMapConnectors = map[AST.FormulaType]string{ - AST.AndConn: "∧", - AST.OrConn: "∨", - AST.ImpConn: "⇒", - AST.EquConn: "⇔", - AST.NotConn: "¬", - AST.TopType: "⊤", - AST.BotType: "⊥", - AST.AllQuant: "∀α", - AST.ExQuant: "∃α", - AST.AllTypeQuant: "∀", - AST.QuantVarOpen: "(", - AST.QuantVarClose: ")", - AST.QuantVarSep: " ", - AST.PredEmpty: "", - AST.PredTypeVarSep: ") (", - AST.TypeVarType: "Type", -} +// var lambdaPiMapConnectors = map[AST.FormulaType]string{ +// AST.AndConn: "∧", +// AST.OrConn: "∨", +// AST.ImpConn: "⇒", +// AST.EquConn: "⇔", +// AST.NotConn: "¬", +// AST.TopType: "⊤", +// AST.BotType: "⊥", +// AST.AllQuant: "∀α", +// AST.ExQuant: "∃α", +// AST.AllTypeQuant: "∀", +// AST.QuantVarOpen: "(", +// AST.QuantVarClose: ")", +// AST.QuantVarSep: " ", +// AST.PredEmpty: "", +// AST.PredTypeVarSep: ") (", +// AST.TypeVarType: "Type", +// } var LambdapiOutputProofStruct = &Search.OutputProofStruct{ProofOutput: MakeLambdapiOutput, Name: "Lambdapi", Extension: ".lp"} @@ -79,6 +79,8 @@ func MakeLambdapiOutput(prf []Search.ProofStruct, meta Lib.List[AST.Meta]) strin return "" } + // FIXME: set the AST printer to (to be defined soon) LPPrinter + // Transform tableaux's proof in GS3 proof return MakeLambdaPiProof(gs3.MakeGS3Proof(prf), meta) } diff --git a/src/Mods/lambdapi/proof.go b/src/Mods/lambdapi/proof.go index 8f740adb..4db3d34d 100644 --- a/src/Mods/lambdapi/proof.go +++ b/src/Mods/lambdapi/proof.go @@ -49,7 +49,7 @@ func makeLambdaPiProofFromGS3(proof *gs3.GS3Sequent) string { formula := proof.GetTargetForm() - formulaStr := toCorrectString(formula) + formulaStr := formula.ToString() resultingString += fmt.Sprintf("λ (%s : ϵ %s),\n", addToContext(formula), formulaStr) proofStr := makeProofStep(proof) resultingString += proofStr @@ -103,7 +103,7 @@ func makeProofStep(proof *gs3.GS3Sequent) string { Glob.Fatal("LP", "Trying to do a weakening rule but it's not implemented yet") } - return "//" + toCorrectString(proof.GetTargetForm()) + "\n" + resultingString + return "//" + proof.GetTargetForm().ToString() + "\n" + resultingString } func closureAxiom(proof *gs3.GS3Sequent) string { @@ -113,7 +113,7 @@ func closureAxiom(proof *gs3.GS3Sequent) string { switch target.(type) { case AST.Pred: - result = fmt.Sprintf("GS3axiom (%s) (%s) (%s)\n", toCorrectString(target), getFromContext(target), getFromContext(notTarget)) + result = fmt.Sprintf("GS3axiom (%s) (%s) (%s)\n", target.ToString(), getFromContext(target), getFromContext(notTarget)) case AST.Top: result = fmt.Sprintf("GS3ntop (%s)\n", getFromContext(notTarget)) case AST.Bot: @@ -134,7 +134,7 @@ func allRules(rule string, target AST.Form, composingForms Lib.List[AST.Form], n result := rule + "\n" for _, composingForm := range composingForms.GetSlice() { - result += "(" + toCorrectString(composingForm) + ")\n" + result += "(" + composingForm.ToString() + ")\n" } result += getRecursionUnivStr(nexts, children) @@ -156,18 +156,19 @@ func allRulesQuantUniv( quant := "" typeStr := "" - switch target.(type) { - case AST.All: - quant = lambdaPiMapConnectors[AST.AllQuant] - case AST.Not: - quant = lambdaPiMapConnectors[AST.ExQuant] - } + // FIXME get printer + // switch target.(type) { + // case AST.Ex: + // quant = AST.ConnAll + // case AST.Not: + // quant = AST.ConnEx + // } typeStr = mapDefault(typeStr) result := rule + "\n" result += "(" + typeStr + ")\n" - result += "(%s, " + toCorrectString(composingForms.At(0)) + ")\n" + result += "(%s, " + composingForms.At(0).ToString() + ")\n" varStrs := []string{} for _, singleVar := range vars.GetSlice() { @@ -175,7 +176,7 @@ func allRulesQuantUniv( } result = fmt.Sprintf(result, strings.Join(varStrs, ", "+quant+" ")) - result += "(" + toCorrectString(termGen) + ")\n" + result += "(" + termGen.ToString() + ")\n" result += getRecursionUnivStr(nexts, children) @@ -188,7 +189,7 @@ func getRecursionUnivStr(nexts []*gs3.GS3Sequent, children []Lib.List[AST.Form]) for i, next := range nexts { result += "(\n" for _, childForm := range children[i].GetSlice() { - result += toLambdaString(childForm, toCorrectString(childForm)) + ",\n" + result += toLambdaString(childForm, childForm.ToString()) + ",\n" } proofStr := makeProofStep(next) result += proofStr @@ -208,18 +209,19 @@ func allRulesQuantExist( ) string { quant := "" typeStr := "" - switch target.(type) { - case AST.Ex: - quant = lambdaPiMapConnectors[AST.ExQuant] - case AST.Not: - quant = lambdaPiMapConnectors[AST.AllQuant] - } + // FIXME get printer + // switch target.(type) { + // case AST.Ex: + // quant = AST.ConnAll + // case AST.Not: + // quant = AST.ConnEx + // } typeStr = mapDefault(typeStr) result := rule + "\n" result += "(" + typeStr + ")\n" - result += "(%s, " + toCorrectString(composingForms.At(0)) + ")\n" + result += "(%s, " + composingForms.At(0).ToString() + ")\n" varStrs := []string{} for _, singleVar := range vars.GetSlice() { @@ -243,7 +245,7 @@ func getRecursionExistStr(nexts []*gs3.GS3Sequent, children []Lib.List[AST.Form] } result += toLambdaIntroString(termGen, typesStr) + ",\n" for _, childForm := range children[i].GetSlice() { - result += toLambdaString(childForm, toCorrectString(childForm)) + ",\n" + result += toLambdaString(childForm, childForm.ToString()) + ",\n" } proofStr := makeProofStep(next) result += proofStr @@ -371,7 +373,7 @@ func makeTheorem(axioms Lib.List[AST.Form], conjecture AST.Form) string { axioms = Lib.ListCpy(axioms) axioms.Append(AST.MakerNot(conjecture)) formattedProblem := makeImpChain(axioms) - return "symbol goeland_" + problemName + " : \nϵ " + toCorrectString(formattedProblem) + " → ϵ ⊥ ≔ \n" + return "symbol goeland_" + problemName + " : \nϵ " + formattedProblem.ToString() + " → ϵ ⊥ ≔ \n" } // If [F1, F2, F3] is a formlist, then this function returns F1 -> (F2 -> F3). diff --git a/src/Mods/lambdapi/utils.go b/src/Mods/lambdapi/utils.go index 803f16d5..5e6421c8 100644 --- a/src/Mods/lambdapi/utils.go +++ b/src/Mods/lambdapi/utils.go @@ -33,9 +33,7 @@ package lambdapi import ( "fmt" - "strings" - "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" ) @@ -46,9 +44,9 @@ func getIncreasedCounter() int { return varCounter - 1 } -var context Glob.Map[AST.MappableString, Glob.String] = *Glob.NewMap[AST.MappableString, Glob.String]() +var context Glob.Map[Glob.Basic, Glob.String] = *Glob.NewMap[Glob.Basic, Glob.String]() -func addToContext(key AST.MappableString) string { +func addToContext(key Glob.Basic) string { if _, ok := context.GetExists(key); !ok { context.Set(key, Glob.String(fmt.Sprintf("v%v", getIncreasedCounter()))) } @@ -56,40 +54,40 @@ func addToContext(key AST.MappableString) string { return string(context.Get(key)) } -func getFromContext(key AST.MappableString) string { +func getFromContext(key Glob.Basic) string { return string(context.Get(key)) } -func toLambdaString(element AST.MappableString, str string) string { +func toLambdaString(element Glob.Basic, str string) string { return fmt.Sprintf("λ (%s : ϵ (%s))", addToContext(element), str) } -func toLambdaIntroString(element AST.MappableString, typeStr string) string { +func toLambdaIntroString(element Glob.Basic, typeStr string) string { return fmt.Sprintf("λ (%s : τ (%s))", addToContext(element), mapDefault(typeStr)) } -func toCorrectString(element AST.MappableString) string { - isNotSkolem := len(element.ToString()) <= 5 || element.ToString()[:6] != "skolem" - element = decorateForm(element) - surround := element.ToMappedStringSurround(lambdaPiMapConnectors, false) - separator, emptyValue := element.ToMappedStringChild(lambdaPiMapConnectors, false) - children := "" - if isNotSkolem { - children = ListToMappedString(element.GetChildrenForMappedString(), separator, emptyValue) - } - return fmt.Sprintf(surround, children) -} +// func toCorrectString(element AST.MappableString) string { +// isNotSkolem := len(element.ToString()) <= 5 || element.ToString()[:6] != "skolem" +// element = decorateForm(element) +// surround := element.ToMappedStringSurround(lambdaPiMapConnectors, false) +// separator, emptyValue := element.ToMappedStringChild(lambdaPiMapConnectors, false) +// children := "" +// if isNotSkolem { +// children = ListToMappedString(element.GetChildrenForMappedString(), separator, emptyValue) +// } +// return fmt.Sprintf(surround, children) +// } -func ListToMappedString[T AST.MappableString](children []T, separator, emptyValue string) string { - strArr := []string{} +// func ListToMappedString[T AST.MappableString](children []T, separator, emptyValue string) string { +// strArr := []string{} - for _, element := range children { - strArr = append(strArr, toCorrectString(element)) - } +// for _, element := range children { +// strArr = append(strArr, toCorrectString(element)) +// } - if len(strArr) == 0 && emptyValue != "" { - strArr = append(strArr, emptyValue) - } +// if len(strArr) == 0 && emptyValue != "" { +// strArr = append(strArr, emptyValue) +// } - return strings.Join(strArr, separator) -} +// return strings.Join(strArr, separator) +// } diff --git a/src/Mods/rocq/context.go b/src/Mods/rocq/context.go index 3ec82ed9..15d16e86 100644 --- a/src/Mods/rocq/context.go +++ b/src/Mods/rocq/context.go @@ -44,6 +44,8 @@ import ( "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Mods/dmt" + "github.com/GoelandProver/Goeland/Typing" + "slices" ) func makeContextIfNeeded(root AST.Form, metaList Lib.List[AST.Meta]) string { @@ -117,8 +119,16 @@ func getContextFromFormula(root AST.Form) []string { result = clean(result, getContextFromFormula(nf.GetForm())) case AST.Pred: if !nf.GetID().Equals(AST.Id_eq) { - result = append(result, mapDefault( - fmt.Sprintf("Parameter %s.", nf.GetID().ToMappedString(rocqMapConnectors(), false)))) + oty := Typing.QueryGlobalEnv(nf.GetID().GetName()) + var ty AST.Ty + switch rty := oty.(type) { + case Lib.Some[AST.Ty]: + ty = rty.Val + case Lib.None[AST.Ty]: + ty = AST.MkDefaultPredType(nf.GetArgs().Len()) + } + + result = append(result, fmt.Sprintf("Parameter %s : %s.", nf.GetID().ToString(), ty.ToString())) } for _, term := range nf.GetArgs().GetSlice() { result = append(result, clean(result, getContextFromTerm(term))...) @@ -130,9 +140,17 @@ func getContextFromFormula(root AST.Form) []string { func getContextFromTerm(trm AST.Term) []string { result := []string{} if fun, isFun := trm.(AST.Fun); isFun { + oty := Typing.QueryGlobalEnv(fun.GetName()) + var ty AST.Ty + switch rty := oty.(type) { + case Lib.Some[AST.Ty]: + ty = rty.Val + case Lib.None[AST.Ty]: + ty = AST.MkDefaultFunctionType(fun.GetArgs().Len()) + } + result = append(result, - mapDefault(fmt.Sprintf( - "Parameter %s.", fun.GetID().ToMappedString(rocqMapConnectors(), false)))) + fmt.Sprintf("Parameter %s : %s.", fun.GetID().ToString(), ty.ToString())) for _, term := range fun.GetArgs().GetSlice() { result = append(result, clean(result, getContextFromTerm(term))...) } @@ -144,13 +162,7 @@ func getContextFromTerm(trm AST.Term) []string { func clean(set, add []string) []string { result := []string{} for _, str := range add { - found := false - for _, s := range set { - if s == str { - found = true - break - } - } + found := slices.Contains(set, str) if !found { result = append(result, str) } @@ -161,12 +173,12 @@ func clean(set, add []string) []string { func contextualizeMetas(metaList Lib.List[AST.Meta]) string { result := []string{} for _, meta := range metaList.GetSlice() { - result = append(result, meta.ToMappedString(rocqMapConnectors(), false)) + result = append(result, meta.ToString()) } return "Parameters " + strings.Join(result, " ") + " : goeland_U." } -var lemmas = `Require Export Classical. +var lemmas = `From Stdlib Require Import Classical. Lemma goeland_notnot : forall P : Prop, P -> (~ P -> False). diff --git a/src/Mods/rocq/output.go b/src/Mods/rocq/output.go index fec5e8ef..1b75f8f5 100644 --- a/src/Mods/rocq/output.go +++ b/src/Mods/rocq/output.go @@ -37,6 +37,7 @@ package rocq import ( + "fmt" "strings" "github.com/GoelandProver/Goeland/AST" @@ -53,53 +54,84 @@ var RocqOutputProofStruct = &Search.OutputProofStruct{ProofOutput: MakeRocqOutpu // ---------------------------------------------------------------------------- // Plugin initialisation and main function to call. -// Section: init -// Functions: MakeRocqOutput -// Main functions of the rocq module. -// TODO: -// * Write the context for TFF problems - func MakeRocqOutput(prf []Search.ProofStruct, meta Lib.List[AST.Meta]) string { if len(prf) == 0 { Glob.Fatal("Rocq", "Nothing to output") return "" } + // Setup Rocq printer + connectives := RocqPrinterConnectives() + printer := AST.Printer{PrinterAction: RocqPrinterAction(), PrinterConnective: &connectives} + AST.SetPrinter(printer) + // Transform tableaux's proof in GS3 proof return MakeRocqProof(gs3.MakeGS3Proof(prf), meta) } +func RocqPrinterConnectives() AST.PrinterConnective { + return AST.MkPrinterConnective( + "RocqPrinterConnective", + map[AST.Connective]string{ + AST.ConnAll: "forall", + AST.ConnEx: "exists", + AST.ConnAnd: " /\\ ", + AST.ConnOr: " \\/ ", + AST.ConnImp: "->", + AST.ConnEqu: "<->", + AST.ConnTop: "True", + AST.ConnBot: "False", + + AST.ConnPi: "forall", + AST.ConnMap: "->", + + AST.SepVarsForm: ", ", + AST.SepTyArgs: ", ", + AST.SepArgsTyArgs: ", ", + AST.SepTyVars: " ", + AST.SepVarTy: "", + + AST.SurQuantStart: "", + AST.SurQuantEnd: "", + }, + ) +} + +func RocqPrinterAction() AST.PrinterAction { + connectives := RocqPrinterConnectives() + + sanitize_type := func(ty_str string) string { + replace := map[string]string{ + "$i": "goeland_U", + "$o": "Prop", + "$tType": "Type", + // FIXME: define a replacement for every defined stuff + } + for k, v := range replace { + ty_str = strings.ReplaceAll(ty_str, k, v) + } + return ty_str + } + rocq_action := AST.MkPrinterAction( + AST.PrinterIdentity, + func(i AST.Id) string { return i.GetName() }, + AST.PrinterIdentity2[int], + func(metaName string, index int) string { return fmt.Sprintf("%s_%d", metaName, index) }, + sanitize_type, + func(typed_var Lib.Pair[string, AST.Ty]) string { + return fmt.Sprintf("(%s : %s)", typed_var.Fst, sanitize_type(typed_var.Snd.ToString())) + }, + ) + rocq_action = rocq_action.Compose(AST.SanitizerAction(connectives, []string{"@"})) + return rocq_action.Compose(AST.RemoveSuperfluousParenthesesAction(connectives)) +} + var MakeRocqProof = func(proof *gs3.GS3Sequent, meta Lib.List[AST.Meta]) string { contextString := makeContextIfNeeded(proof.GetTargetForm(), meta) proofString := makeRocqProofFromGS3(proof) return contextString + "\n" + proofString } -// Replace defined symbols by Rocq's defined symbols. -func mapDefault(str string) string { - return strings.ReplaceAll(strings.ReplaceAll(str, "$i", "goeland_U"), "$o", "Prop") -} -func rocqMapConnectors() map[AST.FormulaType]string { - return map[AST.FormulaType]string{ - AST.AndConn: "/\\", - AST.OrConn: "\\/", - AST.ImpConn: "->", - AST.EquConn: "<->", - AST.NotConn: "~", - AST.TopType: "True", - AST.BotType: "False", - AST.AllQuant: "forall", - AST.ExQuant: "exists", - AST.AllTypeQuant: "forall", - AST.QuantVarOpen: "(", - AST.QuantVarClose: ")", - AST.QuantVarSep: ",", - AST.PredEmpty: "", - AST.PredTypeVarSep: ",", - AST.TypeVarType: "Type", - } -} - // Context flag utility function func GetContextEnabled() bool { return contextEnabled diff --git a/src/Mods/rocq/proof.go b/src/Mods/rocq/proof.go index 2120519c..e6c27212 100644 --- a/src/Mods/rocq/proof.go +++ b/src/Mods/rocq/proof.go @@ -108,11 +108,16 @@ func makeStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], constantsCre case Lib.Some[int]: actualTarget = t.Val case Lib.None[int]: - Glob.Anomaly("coq", fmt.Sprintf( - "Index of %s not found in %s", - proof.GetTargetForm().ToString(), - Lib.ListToString(hypotheses), - )) + // If the target formula is an equality, it _does not_ target any formula of the context, + // it simply tells us to close by congruence. Hence, we don't raise an anomaly if the + // target form is an equality. + if !isPredEqual(proof.GetTargetForm()) { + Glob.Anomaly("rocq", fmt.Sprintf( + "Index of %s not found in { %s }", + proof.GetTargetForm().ToString(), + Lib.ListToString(hypotheses, Lib.WithSep(" ;; "), Lib.WithEmpty("")), + )) + } } switch proof.Rule() { @@ -248,12 +253,14 @@ func processMainFormula(form AST.Form) (Lib.List[AST.Form], AST.Form) { // Prints the theorem's name & properly formats the first formula. func makeTheorem(axioms Lib.List[AST.Form], conjecture AST.Form) string { - problemName := strings.ReplaceAll(strings.ReplaceAll(strings.ReplaceAll(Glob.GetProblemName(), ".", "_"), "=", "_"), "+", "_") + problemName := Glob.GetProblemName() + for _, s := range []string{".", "=", "+", "-"} { + problemName = strings.ReplaceAll(problemName, s, "_") + } axiomsWithConj := Lib.ListCpy(axioms) axiomsWithConj.Append(AST.MakerNot(AST.MakerNot(conjecture))) formattedProblem := makeImpChain(axiomsWithConj) - return "Theorem goeland_proof_of_" + problemName + " : " + - mapDefault(formattedProblem.ToMappedString(rocqMapConnectors(), Glob.GetTypeProof())) + ".\n" + return "Theorem goeland_proof_of_" + problemName + " : " + formattedProblem.ToString() + ".\n" } // If [F1, F2, F3] is a formlist, then this function returns F1 -> (F2 -> F3). @@ -322,7 +329,7 @@ func getRealConstantName(constantsCreated []AST.Term, term AST.Term) string { if fun, isFun := term.(AST.Fun); isFun { res := "" if isGroundTerm(fun.GetID()) { - res = fun.GetID().ToMappedString(rocqMapConnectors(), Glob.GetTypeProof()) + res = fun.GetID().ToString() subterms := make([]string, 0) for _, t := range fun.GetArgs().GetSlice() { subterms = append(subterms, getRealConstantName(constantsCreated, t)) @@ -346,7 +353,7 @@ func findInConstants(constantsCreated []AST.Term, term AST.Term) string { return getConstantName(term.(AST.Fun).GetID()) } if isGroundTerm(term) { - return "(" + term.ToMappedString(rocqMapConnectors(), Glob.GetTypeProof()) + ")" + return "(" + term.ToString() + ")" } return "goeland_I" } diff --git a/src/Mods/tptp/output.go b/src/Mods/tptp/output.go index 66e4fa65..586f9510 100644 --- a/src/Mods/tptp/output.go +++ b/src/Mods/tptp/output.go @@ -37,8 +37,6 @@ package tptp import ( - "strings" - "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" @@ -61,7 +59,10 @@ func MakeTptpOutput(prf []Search.ProofStruct, meta Lib.List[AST.Meta]) string { return "" } + // FIXME: set AST's printer to be the one of TPTP + if Glob.IsSCTPTPOutput() { + // FIXME: the one of TSTP here prefix_const = "Sko_" } @@ -70,33 +71,6 @@ func MakeTptpOutput(prf []Search.ProofStruct, meta Lib.List[AST.Meta]) string { } var MakeTptpProof = func(proof *gs3.GS3Sequent, meta Lib.List[AST.Meta]) string { - old := AST.ChangeVarSeparator(", ") proofString := makeTptpProofFromGS3(proof) - AST.ChangeVarSeparator(old) return proofString } - -// Replace defined symbols by TSTP's defined symbols. -func mapDefault(str string) string { - return strings.ReplaceAll(strings.ReplaceAll(strings.ReplaceAll(str, " : $i", ""), " : $o", ""), " : , ", " : ") -} -func tptpMapConnectors() map[AST.FormulaType]string { - return map[AST.FormulaType]string{ - AST.AndConn: "&", - AST.OrConn: "|", - AST.ImpConn: "=>", - AST.EquConn: "<=>", - AST.NotConn: "~", - AST.TopType: "$true", - AST.BotType: "$false", - AST.AllQuant: "!", - AST.ExQuant: "?", - AST.AllTypeQuant: "!", - AST.QuantVarOpen: "[", - AST.QuantVarClose: "] : ", - AST.QuantVarSep: ",", - AST.PredEmpty: "", - AST.PredTypeVarSep: ",", - AST.TypeVarType: "Type", - } -} diff --git a/src/Mods/tptp/proof.go b/src/Mods/tptp/proof.go index fd48c167..53a18f01 100644 --- a/src/Mods/tptp/proof.go +++ b/src/Mods/tptp/proof.go @@ -141,7 +141,7 @@ func makeStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], new_current_ if isPredEqual(proof.GetTargetForm()) { resultingString = fmt.Sprintf("fof("+prefix_step+"%d, plain, [%s] --> [], inference(%s, [status(thm)], [%s])).", proof.GetId(), - mapDefault(AST.ListToMappedString(hypotheses.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(hypotheses, Lib.WithEmpty("")), "congruence", "") } else { @@ -149,7 +149,7 @@ func makeStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], new_current_ resultingString = fmt.Sprintf("fof("+prefix_step+"%d, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s])).", proof.GetId(), - mapDefault(AST.ListToMappedString(hypotheses.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(hypotheses, Lib.WithEmpty("")), "leftHyp", targetPos, "") @@ -192,7 +192,7 @@ func makeStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], new_current_ // Weakening rule case gs3.W: if proof.TermGenerated() != nil { - resultingString = fmt.Sprintf("leftWeaken %s", findInConstants(proof.TermGenerated()).ToMappedString(tptpMapConnectors(), Glob.GetTypeProof())) + resultingString = fmt.Sprintf("leftWeaken %s", findInConstants(proof.TermGenerated()).ToString()) } else { resultingString, childrenHypotheses, next_child_weakened_id = weakenStep(proof, hypotheses, target, "leftWeaken") } @@ -216,7 +216,7 @@ func alphaStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int, resultingString := fmt.Sprintf("fof(%s%d, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s])).", prefix_step, proof.GetId(), - mapDefault(AST.ListToMappedString(hypotheses.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(hypotheses, Lib.WithEmpty("")), format, target, Glob.IntListToString(children_id, prefix_step)) @@ -242,7 +242,7 @@ func betaStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int, resultingString := fmt.Sprintf("fof(%s%d, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s])).", prefix_step, proof.GetId(), - mapDefault(AST.ListToMappedString(hypotheses.GetSlice(), ", ", "", tptpMapConnectors(), false)), + Lib.ListToString(hypotheses, Lib.WithEmpty("")), format, target, Glob.IntListToString(children_id, prefix_step)) @@ -265,10 +265,10 @@ func deltaStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int, resultingString := fmt.Sprintf("fof(%s%d, plain, [%s] --> [], inference(%s, [status(thm), %d, '%s'], [%s])).", prefix_step, proof.GetId(), - mapDefault(AST.ListToMappedString(hypotheses.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(hypotheses, Lib.WithEmpty("")), format, target, - new_term.ToMappedString(tptpMapConnectors(), Glob.GetTypeProof()), + new_term.ToString(), Glob.IntListToString(children_id, prefix_step)) newHypotheses := Lib.ListCpy(hypotheses) @@ -290,10 +290,10 @@ func gammaStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int, resultingString := fmt.Sprintf("fof(%s%d, plain, [%s] --> [], inference(%s, [status(thm), %d, $fot(%s)], [%s])).", prefix_step, proof.GetId(), - mapDefault(AST.ListToMappedString(hypotheses.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(hypotheses, Lib.WithEmpty("")), format, target, - findInConstants(proof.TermGenerated()).ToMappedString(tptpMapConnectors(), Glob.GetTypeProof()), + findInConstants(proof.TermGenerated()).ToString(), Glob.IntListToString(children_id, prefix_step)) newHypotheses := Lib.ListCpy(hypotheses) @@ -312,7 +312,7 @@ func weakenStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int resultingString := fmt.Sprintf("fof(%s%d, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s%d])).", prefix_step, proof.GetId(), - mapDefault(AST.ListToMappedString(hypotheses.GetSlice(), ", ", "", tptpMapConnectors(), false)), + Lib.ListToString(hypotheses, Lib.WithEmpty("")), format, target, prefix_step, @@ -355,7 +355,7 @@ func EquStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int) ( resultingString = fmt.Sprintf("fof(%s%d, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s])).", prefix_step, proof.GetId(), - mapDefault(AST.ListToMappedString(hypotheses.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(hypotheses, Lib.WithEmpty("")), "leftIff", target, s1_id) + resultingString @@ -367,7 +367,7 @@ func EquStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int) ( newHyp = Lib.ListAdd(newHyp, []AST.Form{A_imp_B, B_imp_A}...) resultingString = fmt.Sprintf("fof(%s, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s, %s])).\n\n", s1_id, - mapDefault(AST.ListToMappedString(newHyp.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(newHyp, Lib.WithEmpty("")), "leftImp2", get(A_imp_B, newHyp), s2_id, @@ -379,7 +379,7 @@ func EquStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int) ( newHypS2 = Lib.ListAdd(newHypS2, notA.Copy()) resultingString = fmt.Sprintf("fof(%s, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s%d, %s])).\n\n", s2_id, - mapDefault(AST.ListToMappedString(newHypS2.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(newHypS2, Lib.WithEmpty("")), "leftImp2", get(B_imp_A, newHypS2), prefix_step, @@ -393,7 +393,7 @@ func EquStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int) ( targetPosS2 := findIndexPos(A, newHypS2Closure, get(A, newHypS2Closure)) resultingString = fmt.Sprintf("fof(%s, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s])).\n\n", s2_closure_id, - mapDefault(AST.ListToMappedString(newHypS2Closure.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(newHypS2Closure, Lib.WithEmpty("")), "leftHyp", targetPosS2, "") + resultingString @@ -404,7 +404,7 @@ func EquStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int) ( newHypS3 = Lib.ListAdd(newHypS3, B) resultingString = fmt.Sprintf("fof(%s, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s, %s%d])).\n\n", s3_id, - mapDefault(AST.ListToMappedString(newHypS3.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(newHypS3, Lib.WithEmpty("")), "leftImp2", get(B_imp_A, newHypS3), s3_closure_id, @@ -418,7 +418,7 @@ func EquStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int) ( targetPosS3 := findIndexPos(B, newHypS3Closure, get(B, newHypS3Closure)) resultingString = fmt.Sprintf("fof(%s, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s])).\n\n", s3_closure_id, - mapDefault(AST.ListToMappedString(newHypS3Closure.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(newHypS3Closure, Lib.WithEmpty("")), "leftHyp", targetPosS3, "") + resultingString @@ -453,7 +453,7 @@ func NotEquStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int resultingString = fmt.Sprintf("fof(%s%d, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s, %s])).", prefix_step, proof.GetId(), - mapDefault(AST.ListToMappedString(hypotheses.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(hypotheses, Lib.WithEmpty("")), "leftNotIff", target, s1_id, @@ -464,7 +464,7 @@ func NotEquStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int newHyp1 = Lib.ListAdd(newHyp1, not_A_imp_B.Copy()) resultingString = fmt.Sprintf("fof(%s, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s%d])).\n\n", s1_id, - mapDefault(AST.ListToMappedString(newHyp1.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(newHyp1, Lib.WithEmpty("")), "leftNotImplies", get(not_A_imp_B, newHyp1), prefix_step, @@ -476,7 +476,7 @@ func NotEquStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], target int newHyp2 = Lib.ListAdd(newHyp2, not_B_imp_A.Copy()) resultingString = fmt.Sprintf("fof(%s, plain, [%s] --> [], inference(%s, [status(thm), %d], [%s%d])).\n\n", s2_id, - mapDefault(AST.ListToMappedString(newHyp2.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(newHyp2, Lib.WithEmpty("")), "leftNotImplies", get(not_B_imp_A, newHyp2), prefix_step, @@ -498,10 +498,10 @@ func processMainFormula(form AST.Form) (Lib.List[AST.Form], AST.Form) { last := nf.GetChildFormulas().Len() - 1 formList = Lib.MkListV(nf.GetChildFormulas().Get(0, last)...) switch f := nf.GetChildFormulas().At(last).(type) { - case AST.Not: - form = f.GetForm() - default: - form = f + case AST.Not: + form = f.GetForm() + default: + form = f } } return formList, form @@ -513,10 +513,11 @@ func makeTheorem(axioms Lib.List[AST.Form], conjecture AST.Form) string { problemName := strings.ReplaceAll(strings.ReplaceAll(strings.ReplaceAll(Glob.GetProblemName(), ".", "_"), "=", "_"), "+", "_") for _, ax := range axioms.GetSlice() { - resulting_string = resulting_string + "fof(" + fmt.Sprintf("ax%d", ax.GetIndex()) + ", axiom, " + mapDefault(ax.ToMappedString(tptpMapConnectors(), Glob.GetTypeProof())) + ").\n\n" + resulting_string = resulting_string + "fof(" + fmt.Sprintf("ax%d", ax.GetIndex()) + ", axiom, " + + ax.ToString() + ").\n\n" } - resulting_string = resulting_string + "fof(c_" + problemName + ", conjecture, " + mapDefault(conjecture.ToMappedString(tptpMapConnectors(), Glob.GetTypeProof())) + ").\n\n" + resulting_string = resulting_string + "fof(c_" + problemName + ", conjecture, " + conjecture.ToString() + ").\n\n" return resulting_string } @@ -529,9 +530,9 @@ func performFirstStep(axioms Lib.List[AST.Form], conjecture AST.Form, hypothesis // Cut initial formula, |- ~c, c step cutFormNot := fmt.Sprintf("fof("+prefix_step+"%d, plain, [%s] --> [%s, %s], inference(%s, [status(thm), %d], [%s])).", cutFormNotId, - mapDefault(AST.ListToMappedString(axioms.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), - mapDefault(conjecture.ToMappedString(tptpMapConnectors(), false)), - mapDefault(AST.MakerNot(conjecture).ToMappedString(tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(axioms, Lib.WithEmpty("")), + conjecture.ToString(), + AST.MakerNot(conjecture).ToString(), "rightNot", 1, prefix_step+strconv.Itoa(cutFormHypId)) @@ -539,8 +540,8 @@ func performFirstStep(axioms Lib.List[AST.Form], conjecture AST.Form, hypothesis // Cut initial formula, c |- c step cutFormHyp := fmt.Sprintf("fof("+prefix_step+"%d, plain, [%s] --> [%s], inference(%s, [status(thm), %d], [%s])).", cutFormHypId, - mapDefault(AST.ListToMappedString(append(axioms.GetSlice(), conjecture), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), - mapDefault(conjecture.ToMappedString(tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(Lib.MkListV(append(axioms.GetSlice(), conjecture)...), Lib.WithEmpty("")), + conjecture.ToString(), "hyp", axioms.Len(), // 0, @@ -550,8 +551,8 @@ func performFirstStep(axioms Lib.List[AST.Form], conjecture AST.Form, hypothesis // indexHyp, _ := hypothesis.GetIndexOf(AST.MakerNot(conjecture)) startForm := fmt.Sprintf("fof(f%d, plain, [%s] --> [%s], inference(cut, [status(thm), %d], [%s%d, %s%d])).\n\n", nextId, - mapDefault(AST.ListToMappedString(axioms.GetSlice(), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), - mapDefault(conjecture.ToMappedString(tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(axioms, Lib.WithEmpty("")), + conjecture.ToString(), 1, //indexHyp, prefix_step, @@ -580,8 +581,8 @@ func performCutAxiomStep(axioms Lib.List[AST.Form], conjecture AST.Form) string prefix_axiom_cut, i, // AST.ListToMappedString(axioms.GetElements(0, i), ", ", "", tptpMapConnectors(), GetTypeProof()), - mapDefault(AST.ListToMappedString(axioms.Get(0, i), ", ", "", tptpMapConnectors(), Glob.GetTypeProof())), - mapDefault(conjecture.ToMappedString(tptpMapConnectors(), Glob.GetTypeProof())), + Lib.ListToString(Lib.MkListV(axioms.Get(0, i)...), Lib.WithEmpty("")), + conjecture.ToString(), 0, //i, "ax", diff --git a/src/Search/proof.go b/src/Search/proof.go index 6d292ee7..e7bcecad 100644 --- a/src/Search/proof.go +++ b/src/Search/proof.go @@ -286,7 +286,7 @@ func IntFormAndTermsListToIntIntStringPairList(fl []IntFormAndTermsList) []IntIn func ProofStructListToJsonProofStructList(ps []ProofStruct) []JsonProofStruct { res := []JsonProofStruct{} for _, p := range ps { - new_json_element := JsonProofStruct{p.GetFormula().GetForm().ToMappedString(AST.DefaultMapString, Glob.GetTypeProof()), p.GetIdDMT(), p.Node_id, p.Rule, p.Rule_name, IntFormAndTermsListToIntIntStringPairList(p.Result_formulas), proofStructChildrenToJsonProofStructChildren(p.Children)} + new_json_element := JsonProofStruct{p.GetFormula().GetForm().ToString(), p.GetIdDMT(), p.Node_id, p.Rule, p.Rule_name, IntFormAndTermsListToIntIntStringPairList(p.Result_formulas), proofStructChildrenToJsonProofStructChildren(p.Children)} res = append(res, new_json_element) } return res diff --git a/src/Unif/parsing.go b/src/Unif/parsing.go index 69dd16be..c8a80fc6 100644 --- a/src/Unif/parsing.go +++ b/src/Unif/parsing.go @@ -38,23 +38,11 @@ import ( ) type TermForm struct { - *AST.MappedString index int t AST.Term } -func (t TermForm) ToMappedStringSurround(mapping AST.MapString, displayTypes bool) string { - return "%s" -} - -func (t TermForm) ToMappedStringChild(mapping AST.MapString, displayTypes bool) (separator, emptyValue string) { - return "", t.t.ToMappedString(mapping, displayTypes) -} - -func (t TermForm) GetChildrenForMappedString() []AST.MappableString { - return AST.LsToMappableStringSlice(t.GetChildFormulas()) -} - +func (t TermForm) ToString() string { return t.ToString() } func (t TermForm) GetTerm() AST.Term { return t.t.Copy() } func (t TermForm) Copy() AST.Form { return makeTermForm(t.GetIndex(), t.GetTerm()) } func (t TermForm) RenameVariables() AST.Form { return t } @@ -118,10 +106,7 @@ func MakerTermForm(t AST.Term) TermForm { } func makeTermForm(i int, t AST.Term) TermForm { - fms := &AST.MappedString{} - tf := TermForm{fms, i, t.Copy()} - fms.MappableString = &tf - return tf + return TermForm{i, t.Copy()} } /* Parses a formulae to a sequence of instructions. */ diff --git a/src/main.go b/src/main.go index 06fde085..4f51ef7d 100644 --- a/src/main.go +++ b/src/main.go @@ -202,9 +202,10 @@ func initEverything() { Glob.InitLogs() // Always init debuggers before options initDebuggers() + // Always init AST before options (for printers) + AST.Init() initOpts() runtime.GOMAXPROCS(Glob.GetCoreLimit()) - AST.Init() Typing.Init() } diff --git a/src/options.go b/src/options.go index 33a87396..21b8b135 100644 --- a/src/options.go +++ b/src/options.go @@ -206,7 +206,7 @@ func buildOptions() { "pretty", false, "Should only be used with the -proof parameter. Enables UTF-8 characters in prints for a pretty proof", - func(bool) { Glob.DisplayPretty() }, + func(bool) { AST.SetPrinter(AST.PrettyPrinter) }, func(bool) {}) (&option[bool]{}).init( "dmt", @@ -390,16 +390,16 @@ func buildOptions() { }, func(bool) {}) (&option[bool]{}).init( - "no_id", + "print-id", false, - "Disables the id in the ToString", - func(bool) { AST.ToStringId = AST.NoIdToString }, + "Enables id printing", + func(bool) { AST.ComposePrinter(AST.PrintIDAction) }, func(bool) {}) (&option[bool]{}).init( "quoted_pred", false, "Print predicates between quotes if they start by a capital letter (TPTP compliance)", - func(bool) { AST.ToStringId = AST.QuotedToString }, + func(bool) { AST.ComposePrinter(AST.QuoteID) }, func(bool) {}) (&option[bool]{}).init( "quiet",