From 9891f8f1486c7edaeef2abc1abfd2007dee14f35 Mon Sep 17 00:00:00 2001 From: Johann Rosain Date: Sun, 5 Oct 2025 18:28:51 +0200 Subject: [PATCH 1/4] Add: proof-certification folder with instructions on how to certify proofs with Goeland --- .gitignore | 2 ++ .../LambdaPi}/CCC.lp | 0 .../LambdaPi}/FOL.lp | 0 .../LambdaPi}/GS3.lp | 0 .../LambdaPi}/ICC.lp | 0 .../LambdaPi}/LL.lp | 0 .../LambdaPi}/LL_ND.lp | 0 proof-certification/LambdaPi/Makefile | 20 +++++++++++++++++++ .../LambdaPi}/ND.lp | 0 .../LambdaPi}/ND_eps.lp | 0 .../LambdaPi}/ND_eps_aux.lp | 0 .../LambdaPi}/ND_eps_full.lp | 0 proof-certification/LambdaPi/README.md | 12 +++++++++++ .../LambdaPi}/lambdapi.pkg | 0 proof-certification/README.md | 5 +++++ 15 files changed, 39 insertions(+) rename {LambdaPi => proof-certification/LambdaPi}/CCC.lp (100%) rename {LambdaPi => proof-certification/LambdaPi}/FOL.lp (100%) rename {LambdaPi => proof-certification/LambdaPi}/GS3.lp (100%) rename {LambdaPi => proof-certification/LambdaPi}/ICC.lp (100%) rename {LambdaPi => proof-certification/LambdaPi}/LL.lp (100%) rename {LambdaPi => proof-certification/LambdaPi}/LL_ND.lp (100%) create mode 100644 proof-certification/LambdaPi/Makefile rename {LambdaPi => proof-certification/LambdaPi}/ND.lp (100%) rename {LambdaPi => proof-certification/LambdaPi}/ND_eps.lp (100%) rename {LambdaPi => proof-certification/LambdaPi}/ND_eps_aux.lp (100%) rename {LambdaPi => proof-certification/LambdaPi}/ND_eps_full.lp (100%) create mode 100644 proof-certification/LambdaPi/README.md rename {LambdaPi => proof-certification/LambdaPi}/lambdapi.pkg (100%) create mode 100644 proof-certification/README.md diff --git a/.gitignore b/.gitignore index e489e562..d35987c0 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,5 @@ +*.lpo + .direnv [Pp]roblems [Oo]utput diff --git a/LambdaPi/CCC.lp b/proof-certification/LambdaPi/CCC.lp similarity index 100% rename from LambdaPi/CCC.lp rename to proof-certification/LambdaPi/CCC.lp diff --git a/LambdaPi/FOL.lp b/proof-certification/LambdaPi/FOL.lp similarity index 100% rename from LambdaPi/FOL.lp rename to proof-certification/LambdaPi/FOL.lp diff --git a/LambdaPi/GS3.lp b/proof-certification/LambdaPi/GS3.lp similarity index 100% rename from LambdaPi/GS3.lp rename to proof-certification/LambdaPi/GS3.lp diff --git a/LambdaPi/ICC.lp b/proof-certification/LambdaPi/ICC.lp similarity index 100% rename from LambdaPi/ICC.lp rename to proof-certification/LambdaPi/ICC.lp diff --git a/LambdaPi/LL.lp b/proof-certification/LambdaPi/LL.lp similarity index 100% rename from LambdaPi/LL.lp rename to proof-certification/LambdaPi/LL.lp diff --git a/LambdaPi/LL_ND.lp b/proof-certification/LambdaPi/LL_ND.lp similarity index 100% rename from LambdaPi/LL_ND.lp rename to proof-certification/LambdaPi/LL_ND.lp diff --git a/proof-certification/LambdaPi/Makefile b/proof-certification/LambdaPi/Makefile new file mode 100644 index 00000000..4a6ba9f7 --- /dev/null +++ b/proof-certification/LambdaPi/Makefile @@ -0,0 +1,20 @@ +.POSIX: +SRC = +OBJ = $(SRC:.lp=.lpo) +.SUFFIXES: + +all: $(OBJ) + +install: $(OBJ) lambdapi.pkg + lambdapi install lambdapi.pkg $(OBJ) $(SRC) + +uninstall: + lambdapi uninstall lambdapi.pkg + +clean: + rm -f $(OBJ) + +.SUFFIXES: .lp .lpo + +.lp.lpo: + lambdapi check --gen-obj $< diff --git a/LambdaPi/ND.lp b/proof-certification/LambdaPi/ND.lp similarity index 100% rename from LambdaPi/ND.lp rename to proof-certification/LambdaPi/ND.lp diff --git a/LambdaPi/ND_eps.lp b/proof-certification/LambdaPi/ND_eps.lp similarity index 100% rename from LambdaPi/ND_eps.lp rename to proof-certification/LambdaPi/ND_eps.lp diff --git a/LambdaPi/ND_eps_aux.lp b/proof-certification/LambdaPi/ND_eps_aux.lp similarity index 100% rename from LambdaPi/ND_eps_aux.lp rename to proof-certification/LambdaPi/ND_eps_aux.lp diff --git a/LambdaPi/ND_eps_full.lp b/proof-certification/LambdaPi/ND_eps_full.lp similarity index 100% rename from LambdaPi/ND_eps_full.lp rename to proof-certification/LambdaPi/ND_eps_full.lp diff --git a/proof-certification/LambdaPi/README.md b/proof-certification/LambdaPi/README.md new file mode 100644 index 00000000..1caa76e3 --- /dev/null +++ b/proof-certification/LambdaPi/README.md @@ -0,0 +1,12 @@ +# Proof Certification Using Goéland+LambdaPi + +To output a LambdaPi proof of a problem file `problem.p`, use the `-olp` option: +``` +./_build/goeland -olp problem.p +``` + +Assuming you are at the root of your local clone of this GitHub repo, checking this file +can be done using the following command: +``` +lambdapi check --lib-root . --map-dir Logic.Goeland:proof-certification/LambdaPi problem.lp +``` diff --git a/LambdaPi/lambdapi.pkg b/proof-certification/LambdaPi/lambdapi.pkg similarity index 100% rename from LambdaPi/lambdapi.pkg rename to proof-certification/LambdaPi/lambdapi.pkg diff --git a/proof-certification/README.md b/proof-certification/README.md new file mode 100644 index 00000000..a851dab1 --- /dev/null +++ b/proof-certification/README.md @@ -0,0 +1,5 @@ +# Proof Certification + +This directory contains all the files that are necessary for Goéland to translate its +proof in different languages. We provide a small documentation of their usage: +* for LambdaPi, see [this file](LambdaPi/README.md) From 41a214c2ce0e115722640a6ae57da587647a1be0 Mon Sep 17 00:00:00 2001 From: Johann Rosain Date: Sun, 5 Oct 2025 18:29:15 +0200 Subject: [PATCH 2/4] Add: use lambdapi to check the test-suite --- devtools/run-test-suite.py | 109 ++++++++++++++++++++++--------------- 1 file changed, 66 insertions(+), 43 deletions(-) diff --git a/devtools/run-test-suite.py b/devtools/run-test-suite.py index 771f2919..68556ab0 100644 --- a/devtools/run-test-suite.py +++ b/devtools/run-test-suite.py @@ -13,7 +13,7 @@ class Parser: RES = "% result: " ENV = "% env: " EXIT_CODE = "% exit: " - no_rocq_check = False + no_check = False def __init__(self, filename): self.filename = filename @@ -24,7 +24,7 @@ def __init__(self, filename): 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 + self.no_check = True def parseGen(self, pat): with open(self.filename) as f: @@ -48,23 +48,20 @@ def parseEnv(self): def parseExitCode(self): self.expectedExitCode = self.parseGen(self.EXIT_CODE).strip() - def getCommandLine(self): - arguments = self.arguments - if not self.no_rocq_check: - arguments += " -context -orocq" + def getCommandLine(self, checker_args): + arguments = self.arguments + checker_args 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 + chk_str = "" + if self.no_check: + chk_str = " (no check)" + return self.arguments + chk_str def sanitize(s): return s.encode('utf-8', errors='ignore').decode(errors='ignore') 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) @@ -87,6 +84,28 @@ def getRelevantOutput(output): def isExecutable(prog) : return shutil.which(prog) is not None +def makeGenericCheck(command, extension, cleanup_always, cleanup_compile_success, f, output): + check_lines = getRelevantOutput(output) + check_success = False + filename = os.getcwd() + "/" + os.path.basename(f)[:-2].replace("-", "_") + + with open(f"{filename}.{extension}", "w") as chk_file: + chk_file.write("\n".join(check_lines)) + + result = run(f"{command} {filename}.{extension}", stdout=PIPE, stderr=PIPE, universal_newlines=True, shell=True, encoding='utf-8') + check_success = result.returncode == 0 + + for ext in cleanup_always: + os.remove(f"{filename}.{ext}") + + if not check_success: + return False, result.stderr + else: + for ext in cleanup_compile_success: + os.remove(f"{filename}.{ext}") + + return True, None + def getRocqCompiler() : if isExecutable("rocq"): return "rocq compile" @@ -96,35 +115,29 @@ def getRocqCompiler() : 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)) + check_status, err = makeGenericCheck(getRocqCompiler(), "v", ["glob"], ["v", "vo", "vok", "vos"], f, output) - result = run(f"{rocq} {filename}.v", stdout=PIPE, stderr=PIPE, universal_newlines=True, shell=True, encoding='utf-8') - compile_success = result.returncode == 0 + if not check_status: + print(f"ROCQ check has failed.") + print(f"Reason: {err}") + exit(1) - try: - os.remove(f"{filename}.glob") - except FileNotFoundError: - pass +def makeLambdapiCheck(f, output): + lp_command = "lambdapi check --lib-root .. --map-dir Logic.Goeland:../proof-certification/LambdaPi" + check_status, err = makeGenericCheck(lp_command, "lp", [], ["lp"], f, output) - 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): + # As the lambdapi output does not manage equality, we tolerate fails for the problems + # of the test suite that have equality. + lp_tolerated_fails = ["TEST_EQ.p", "TEST_EQ2.p", "sankalp.p"] + + if not check_status: + if os.path.basename(f) in lp_tolerated_fails: + print(f"LAMBDAPI check has failed, but it was expected.") + else: + print(f"LAMBDAPI check has failed") + exit(1) + +def runWithExpected(f, parser, checker_args, check_fun): """ Runs Goéland on [f] using the parsed command line, then checks if the output corresponds to the expected one. This function manages: @@ -132,9 +145,10 @@ def runWithExpected(f, parser): - 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). + result, we run a checker (specified by checker_args and check_fun) to check that the proof is indeed valid + (except for files in the no-chk folder). """ - output, err, exit_code = runProver(f, parser.getCommandLine()) + output, err, exit_code = runProver(f, parser.getCommandLine("")) if err != "": print(f"Runtime error: {err}") @@ -155,15 +169,22 @@ def runWithExpected(f, parser): print(f"Error: expected '{parser.expectedResult}', got: '{actual}'") exit(1) else: - if parser.no_rocq_check: return - makeRocqCheck(f, output) + if parser.no_check: return + output, _, _ = runProver(f, parser.getCommandLine(checker_args)) + check_fun(f, output) return print(f"Unknown error: got\n{output}") exit(1) +def runWithRocqChk(f, parser): + runWithExpected(f, parser, " -context -orocq", makeRocqCheck) + +def runWithLpChk(f, parser): + runWithExpected(f, parser, " -olp", makeLambdapiCheck) + def compareOutputs(f, parser): - output, err, exit_code = runProver(f, parser.getCommandLine()) + output, err, exit_code = runProver(f, parser.getCommandLine("")) if err != "" or exit_code != 0: print(f"Runtime error: {err}") @@ -195,4 +216,6 @@ def compareOutputs(f, parser): if (os.path.exists(os.path.splitext(f)[0] + ".out")) : compareOutputs(f, parser) else : - runWithExpected(f, parser) + print(f"{f}\t{parser.getArgsForPrinting()}") + runWithRocqChk(f, parser) + runWithLpChk(f, parser) From 63789de42621b7321cc849a6d924f4388a73a5b6 Mon Sep 17 00:00:00 2001 From: Johann Rosain Date: Sun, 5 Oct 2025 18:29:43 +0200 Subject: [PATCH 3/4] Fix: use new printer system to have a valid lambdapi output --- proof-certification/LambdaPi/Makefile | 2 +- src/AST/formsDef.go | 32 +- src/AST/modular-printing.go | 78 ++- src/AST/printers.go | 6 + src/AST/quantifiers.go | 4 +- src/AST/termsDef.go | 7 +- src/Mods/CertifUtils/context.go | 128 +++++ src/Mods/CertifUtils/sanitizer.go | 49 ++ src/Mods/CertifUtils/utils.go | 50 ++ src/Mods/gs3/proof.go | 2 +- src/Mods/gs3/sequent.go | 3 +- src/Mods/lambdapi/context.go | 214 +------- .../lambdapi/{utils.go => local_context.go} | 79 ++- src/Mods/lambdapi/output.go | 146 ++++-- src/Mods/lambdapi/proof.go | 492 +++++++++--------- src/Mods/rocq/context.go | 84 +-- src/Mods/rocq/output.go | 1 + src/Mods/rocq/proof.go | 20 +- src/main.go | 2 + 19 files changed, 754 insertions(+), 645 deletions(-) create mode 100644 src/Mods/CertifUtils/context.go create mode 100644 src/Mods/CertifUtils/sanitizer.go create mode 100644 src/Mods/CertifUtils/utils.go rename src/Mods/lambdapi/{utils.go => local_context.go} (50%) diff --git a/proof-certification/LambdaPi/Makefile b/proof-certification/LambdaPi/Makefile index 4a6ba9f7..0aa80a08 100644 --- a/proof-certification/LambdaPi/Makefile +++ b/proof-certification/LambdaPi/Makefile @@ -1,5 +1,5 @@ .POSIX: -SRC = +SRC = CCC.lp FOL.lp GS3.lp ICC.lp LL.lp LL_ND.lp ND_eps_aux.lp ND_eps_full.lp ND_eps.lp ND.lp OBJ = $(SRC:.lp=.lpo) .SUFFIXES: diff --git a/src/AST/formsDef.go b/src/AST/formsDef.go index ed4183d3..49cb6962 100644 --- a/src/AST/formsDef.go +++ b/src/AST/formsDef.go @@ -38,6 +38,7 @@ package AST import ( "fmt" + "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" ) @@ -467,11 +468,11 @@ func (e Equ) GetMetas() Lib.Set[Meta] { } func (e Equ) ToString() string { - return fmt.Sprintf("%s %s %s", + return printer.Str(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 { @@ -526,7 +527,11 @@ func (e Equ) GetChildFormulas() Lib.List[Form] { } func (e Equ) ReplaceMetaByTerm(meta Meta, term Term) Form { - return MakeEqu(e.GetIndex(), e.f1.ReplaceMetaByTerm(meta, term), e.f2.ReplaceMetaByTerm(meta, term)) + return MakeEqu( + e.GetIndex(), + e.f1.ReplaceMetaByTerm(meta, term), + e.f2.ReplaceMetaByTerm(meta, term), + ) } // ----------------------------------------------------------------------------- @@ -579,11 +584,11 @@ func (i Imp) GetMetas() Lib.Set[Meta] { } func (i Imp) ToString() string { - return fmt.Sprintf("%s %s %s", + return printer.Str(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 { @@ -641,7 +646,11 @@ func (i Imp) GetChildFormulas() Lib.List[Form] { } func (i Imp) ReplaceMetaByTerm(meta Meta, term Term) Form { - return MakeImp(i.GetIndex(), i.f1.ReplaceMetaByTerm(meta, term), i.f2.ReplaceMetaByTerm(meta, term)) + return MakeImp( + i.GetIndex(), + i.f1.ReplaceMetaByTerm(meta, term), + i.f2.ReplaceMetaByTerm(meta, term), + ) } // ----------------------------------------------------------------------------- @@ -704,10 +713,10 @@ func (n Not) Copy() Form { } func (n Not) ToString() string { - return fmt.Sprintf("%s%s", + return printer.Str(fmt.Sprintf("%s%s", printer.StrConn(ConnNot), printer.Str(printer.SurroundChild(n.f.ToString())), - ) + )) } func (n Not) ReplaceTermByTerm(old Term, new Term) (Form, bool) { @@ -845,11 +854,10 @@ func (p Pred) GetArgs() Lib.List[Term] { return p.args } func (p Pred) RenameVariables() Form { return p } func (p Pred) ToString() string { - return printer.OnFunctionalArgs( + return printer.StrFunctional( p.id, - Lib.ListToString(p.tys, Lib.WithSep(printer.StrConn(SepTyArgs)), Lib.WithEmpty("")), - printer.StrConn(SepArgsTyArgs), - p.args, + Lib.ListMap(p.tys, Ty.ToString), + Lib.ListMap(p.args, Term.ToString), ) } diff --git a/src/AST/modular-printing.go b/src/AST/modular-printing.go index edef7192..d4ea4976 100644 --- a/src/AST/modular-printing.go +++ b/src/AST/modular-printing.go @@ -63,12 +63,13 @@ import ( 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 + 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 + actionOnFunctional func(id Id, tys Lib.List[string], args Lib.List[string]) string } func (p PrinterAction) Compose(oth PrinterAction) PrinterAction { @@ -87,6 +88,9 @@ func (p PrinterAction) Compose(oth PrinterAction) PrinterAction { actionOnTypedVar: func(pair Lib.Pair[string, Ty]) string { return oth.actionOnTypedVar(Lib.MkPair(p.actionOnTypedVar(pair), pair.Snd)) }, + actionOnFunctional: func(id Id, tys Lib.List[string], args Lib.List[string]) string { + return p.actionOnFunctional(id, tys, args) // we can't compose that + }, } } @@ -114,6 +118,10 @@ func (p PrinterAction) StrTyVar(pair Lib.Pair[string, Ty]) string { return p.Str(p.actionOnTypedVar(pair)) } +func (p PrinterAction) StrFunctional(i Id, tys, args Lib.List[string]) string { + return p.Str(p.actionOnFunctional(i, tys, args)) +} + 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 } @@ -125,8 +133,17 @@ func MkPrinterAction( actionOnMeta func(string, int) string, actionOnType func(string) string, actionOnTypedVar func(Lib.Pair[string, Ty]) string, + actionOnFunctional func(id Id, tys Lib.List[string], args Lib.List[string]) string, ) PrinterAction { - return PrinterAction{genericAction, actionOnId, actionOnBoundVar, actionOnMeta, actionOnType, actionOnTypedVar} + return PrinterAction{ + genericAction, + actionOnId, + actionOnBoundVar, + actionOnMeta, + actionOnType, + actionOnTypedVar, + actionOnFunctional, + } } type Connective int @@ -149,7 +166,10 @@ func (p *PrinterConnective) StrConn(conn Connective) string { 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) })) + 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 { @@ -161,7 +181,12 @@ func (p *PrinterConnective) StrConn(conn Connective) string { } 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 fmt.Sprintf( + "Connective %d not found in %s, trying in %s", + conn, + p.name, + default_connective.name, + ) })) return default_connective.StrConn(conn) } @@ -186,13 +211,23 @@ type Printer struct { *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. +func (c PrinterConnective) DefaultOnFunctionalArgs( + id Id, + tys Lib.List[string], + args Lib.List[string], +) string { infix := Lib.MkListV(Id_eq) - is_infix := Lib.ListMem(i, infix) - arguments := Lib.ListToString(args, Lib.WithSep(p.StrConn(SepArgs)), Lib.WithEmpty("")) + is_infix := Lib.ListMem(id, infix) + types := Lib.ListToString( + Lib.ListMap(tys, Lib.MkString), + Lib.WithSep(c.StrConn(SepTyArgs)), + Lib.WithEmpty(""), + ) + arguments := Lib.ListToString( + Lib.ListMap(args, Lib.MkString), + Lib.WithSep(c.StrConn(SepArgs)), + Lib.WithEmpty(""), + ) if is_infix { // We expect to have between two and three arguments in an infix function @@ -205,12 +240,17 @@ func (p Printer) OnFunctionalArgs(i Id, tys, con string, args Lib.List[Term]) st )) } st := args.Len() - 2 - return fmt.Sprintf("%s %s %s", args.At(st).ToString(), i.ToString(), args.At(st+1).ToString()) + return fmt.Sprintf( + "%s %s %s", + args.At(st), + id.ToString(), + args.At(st+1), + ) } else { - if len(tys) > 0 { - arguments = tys + con + arguments + if tys.Len() > 0 { + arguments = types + c.StrConn(SepArgsTyArgs) + arguments } - return fmt.Sprintf("%s%s", i.ToString(), p.SurroundArgs(arguments)) + return fmt.Sprintf("%s%s", id.ToString(), c.SurroundArgs(arguments)) } } diff --git a/src/AST/printers.go b/src/AST/printers.go index dffbe26e..c48c4b3f 100644 --- a/src/AST/printers.go +++ b/src/AST/printers.go @@ -75,6 +75,9 @@ func RemoveSuperfluousParenthesesAction(connectives PrinterConnective) PrinterAc 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 }, + actionOnFunctional: func(id Id, tys Lib.List[string], args Lib.List[string]) string { + return connectives.DefaultOnFunctionalArgs(id, tys, args) + }, } } @@ -91,5 +94,8 @@ func SanitizerAction(connectives PrinterConnective, forbidden_chars []string) Pr 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 }, + actionOnFunctional: func(id Id, tys Lib.List[string], args Lib.List[string]) string { + return connectives.DefaultOnFunctionalArgs(id, tys, args) + }, } } diff --git a/src/AST/quantifiers.go b/src/AST/quantifiers.go index a7e8a958..2b88cee6 100644 --- a/src/AST/quantifiers.go +++ b/src/AST/quantifiers.go @@ -81,7 +81,7 @@ func (q quantifier) GetMetas() Lib.Set[Meta] { } func (q quantifier) ToString() string { - return fmt.Sprintf( + return printer.Str(fmt.Sprintf( "%s %s%s%s", printer.StrConn(q.symbol), printer.SurroundQuantified( @@ -91,7 +91,7 @@ func (q quantifier) ToString() string { ), printer.StrConn(SepVarsForm), printer.Str(q.subForm.ToString()), - ) + )) } func (q quantifier) GetChildFormulas() Lib.List[Form] { diff --git a/src/AST/termsDef.go b/src/AST/termsDef.go index 5ceef280..83994bb6 100644 --- a/src/AST/termsDef.go +++ b/src/AST/termsDef.go @@ -118,11 +118,10 @@ type Fun struct { } func (f Fun) ToString() string { - return printer.OnFunctionalArgs( + return printer.StrFunctional( f.p, - Lib.ListToString(f.tys, Lib.WithSep(printer.StrConn(SepTyArgs)), Lib.WithEmpty("")), - printer.StrConn(SepArgsTyArgs), - f.args, + Lib.ListMap(f.tys, Ty.ToString), + Lib.ListMap(f.args, Term.ToString), ) } diff --git a/src/Mods/CertifUtils/context.go b/src/Mods/CertifUtils/context.go new file mode 100644 index 00000000..c5322cb7 --- /dev/null +++ b/src/Mods/CertifUtils/context.go @@ -0,0 +1,128 @@ +/** +* 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. +**/ +package CertifUtils + +/** + * This file provides a function that returns the context of a proof (the symbols appearing in it). + **/ + +import ( + "github.com/GoelandProver/Goeland/AST" + "github.com/GoelandProver/Goeland/Glob" + "github.com/GoelandProver/Goeland/Lib" + "github.com/GoelandProver/Goeland/Typing" +) + +type OrderedConPair Lib.Pair[AST.Id, AST.Ty] + +func (p OrderedConPair) Equals(oth any) bool { + if op, is_op := oth.(OrderedConPair); is_op { + return p.Fst.Equals(op.Fst) && p.Snd.Equals(op.Snd) + } + return false +} + +func (p OrderedConPair) Less(oth any) bool { + if op, is_op := oth.(OrderedConPair); is_op { + return p.Fst.Less(op.Fst) + } + return false +} + +func GetContextFromFormula(root AST.Form) Lib.List[Lib.Pair[AST.Id, AST.Ty]] { + out_list := Lib.NewList[Lib.Pair[AST.Id, AST.Ty]]() + for _, p := range getContextFromFormula(root).Elements().GetSlice() { + out_list.Append(Lib.MkPair(p.Fst, p.Snd)) + } + return out_list +} + +func getContextFromFormula(root AST.Form) Lib.Set[OrderedConPair] { + aux := func(children Lib.List[AST.Form]) Lib.Set[OrderedConPair] { + res := Lib.EmptySet[OrderedConPair]() + for _, child := range children.GetSlice() { + res = res.Union(getContextFromFormula(child)) + } + return res + } + + switch nf := root.(type) { + case AST.Top, AST.Bot: + return Lib.EmptySet[OrderedConPair]() + case AST.All, AST.Ex, AST.And, AST.Or, AST.Imp, AST.Equ, AST.Not: + return aux(root.GetChildFormulas()) + case AST.Pred: + res := Lib.EmptySet[OrderedConPair]() + if !nf.GetID().Equals(AST.Id_eq) { + 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()) + } + + res = res.Add(OrderedConPair(Lib.MkPair(nf.GetID(), ty))) + } + for _, term := range nf.GetArgs().GetSlice() { + res = res.Union(getContextFromTerm(term)) + } + return res + } + Glob.Anomaly("CertifUtils", "Reached an impossible case") + return Lib.EmptySet[OrderedConPair]() +} + +func getContextFromTerm(trm AST.Term) Lib.Set[OrderedConPair] { + fun, isFun := trm.(AST.Fun) + if !isFun { + return Lib.EmptySet[OrderedConPair]() + } + + 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()) + } + + res := Lib.Singleton(OrderedConPair(Lib.MkPair(fun.GetID(), ty))) + for _, term := range fun.GetArgs().GetSlice() { + res = res.Union(getContextFromTerm(term)) + } + + return res +} diff --git a/src/Mods/CertifUtils/sanitizer.go b/src/Mods/CertifUtils/sanitizer.go new file mode 100644 index 00000000..3549646a --- /dev/null +++ b/src/Mods/CertifUtils/sanitizer.go @@ -0,0 +1,49 @@ +/** +* 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. +**/ +package CertifUtils + +/** + * This file provides a function that returns the context of a proof (the symbols appearing in it). + **/ + +import ( + "github.com/GoelandProver/Goeland/Glob" + "strings" +) + +func SanitizedTheoremName() string { + problemName := Glob.GetProblemName() + for _, s := range []string{".", "=", "+", "-"} { + problemName = strings.ReplaceAll(problemName, s, "_") + } + return problemName +} diff --git a/src/Mods/CertifUtils/utils.go b/src/Mods/CertifUtils/utils.go new file mode 100644 index 00000000..3a0726f5 --- /dev/null +++ b/src/Mods/CertifUtils/utils.go @@ -0,0 +1,50 @@ +/** +* 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. +**/ +package CertifUtils + +/** + * This file provides utility functions for proof certification + **/ + +import ( + "github.com/GoelandProver/Goeland/AST" +) + +func IsPredEqual(f AST.Form) bool { + if not, isNot := f.(AST.Not); isNot { + f = not.GetForm() + } + if p, isPred := f.(AST.Pred); isPred { + return p.GetID().Equals(AST.Id_eq) + } + return false +} diff --git a/src/Mods/gs3/proof.go b/src/Mods/gs3/proof.go index 6f534e4e..1db316f1 100644 --- a/src/Mods/gs3/proof.go +++ b/src/Mods/gs3/proof.go @@ -383,7 +383,7 @@ func makeProofStructFrom(f, nf AST.Form, rule Rule) Search.ProofStruct { nf, Lib.NewList[AST.Term]()), ))} - proofStruct.Rule_name = ruleToTableauxString(rule) + proofStruct.Rule_name = rule.ToString() return proofStruct } diff --git a/src/Mods/gs3/sequent.go b/src/Mods/gs3/sequent.go index 103ff7bf..309a106c 100644 --- a/src/Mods/gs3/sequent.go +++ b/src/Mods/gs3/sequent.go @@ -278,7 +278,8 @@ func proofStructRuleToGS3Rule(rule string) Rule { } return mapping[rule] } -func ruleToTableauxString(rule Rule) string { + +func (rule Rule) ToString() string { mapping := map[Rule]string{ NNOT: "ALPHA_NOT_NOT", NOR: "ALPHA_NOT_OR", diff --git a/src/Mods/lambdapi/context.go b/src/Mods/lambdapi/context.go index 50102369..25b5c368 100644 --- a/src/Mods/lambdapi/context.go +++ b/src/Mods/lambdapi/context.go @@ -33,11 +33,11 @@ package lambdapi import ( "fmt" - "strings" "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" + "github.com/GoelandProver/Goeland/Mods/CertifUtils" "github.com/GoelandProver/Goeland/Mods/dmt" ) @@ -51,7 +51,11 @@ func makeContextIfNeeded(root AST.Form, metaList Lib.List[AST.Meta]) string { } // if AST.EmptyGlobalContext() { - resultString += strings.Join(getContextFromFormula(root), "\n") + "\n" + contextual_symbols := CertifUtils.GetContextFromFormula(root) + for _, p := range contextual_symbols.GetSlice() { + addToGlobalEnv(Lib.MkPair(p.Fst.ToString(), p.Snd)) + resultString += fmt.Sprintf("symbol %s : %s;\n", p.Fst.ToString(), p.Snd.ToString()) + } if metaList.Len() > 0 { resultString += contextualizeMetas(metaList) @@ -66,213 +70,15 @@ func makeContextIfNeeded(root AST.Form, metaList Lib.List[AST.Meta]) string { return resultString } -func getContextAsString(root AST.Form) string { - types, arrows, others := GlobContextPairs() - ids := getIdsFromFormula(root) - - final := types - - for _, arrow := range arrows { - for _, id := range ids { - if id.Fst == arrow.Fst { - found := false - for _, fin := range final { - if fin.Fst == id.Snd { - found = true - } - } - - if !found { - final = append(final, Glob.MakePair(id.Snd, arrow.Snd)) - } - } - } - } - - for _, other := range others { - for _, id := range ids { - if id.Fst == other.Fst { - found := false - for _, fin := range final { - if fin.Fst == id.Snd { - found = true - } - } - - if !found { - final = append(final, Glob.MakePair(id.Snd, other.Snd)) - } - } - } - } - - result := "" - - for _, fin := range final { - result += "symbol " + fin.Fst + " : " + mapDefault(fin.Snd) + ";\n" - } - - return result -} - -func GlobContextPairs() (types, arrows, others []Glob.Pair[string, string]) { - return []Glob.Pair[string, string]{}, []Glob.Pair[string, string]{}, []Glob.Pair[string, string]{} - // context := AST.GetGlobalContext() - // for k, v := range context { - // if k != "=" && k[0] != '$' { - // switch typed := v[0].App.(type) { - // case AST.TypeArrow: - // primitives := typed.GetPrimitives() - // typesStr := "" - - // for i, prim := range primitives { - // if i != len(primitives)-1 { - // typesStr += "τ (" + prim.ToString() + ") → " - // } else { - // typesStr += prim.ToString() - // } - // } - // arrows = append(arrows, Glob.MakePair(k, typesStr)) - // case AST.QuantifiedType: - // primitives := typed.GetPrimitives() - // typesStr := "" - // contextualized := []string{} - - // for i, prim := range primitives { - // if i != len(primitives)-1 { - // switch typedPrim := prim.(type) { - // case AST.TypeVar: - // str := AST.SimpleStringMappable(typedPrim.ToString()) - // symbol := addToContext(&str) - // typesStr += "τ (" + symbol + ") → " - // contextualized = append(contextualized, symbol) - // case AST.TypeHint: - // typesStr += "τ (" + prim.ToString() + ") → " - // } - // } else { - // typesStr += prim.ToString() - // } - // } - // arrows = append(arrows, Glob.MakePair(k, fmt.Sprintf("Π (%s : Type), %s", strings.Join(contextualized, " : Type), ("), typesStr))) - // case AST.TypeHint: - // if k == typed.ToString() { - // types = append(types, Glob.MakePair(k, "Type")) - // } else { - // others = append(others, Glob.MakePair(k, fmt.Sprintf("τ (%s)", typed.ToString()))) - // } - // } - // } - // } - - // return types, arrows, others -} - func contextPreamble() string { return "require open Logic.Goeland.FOL Logic.Goeland.LL Logic.Goeland.ND Logic.Goeland.ND_eps Logic.Goeland.ND_eps_full Logic.Goeland.ND_eps_aux Logic.Goeland.LL_ND Logic.Goeland.GS3;" } -func getContextFromFormula(root AST.Form) []string { - result := []string{} - - switch nf := root.(type) { - case AST.All: - result = getContextFromFormula(nf.GetForm()) - case AST.Ex: - result = getContextFromFormula(nf.GetForm()) - case AST.And: - for _, f := range nf.GetChildFormulas().GetSlice() { - result = append(result, clean(result, getContextFromFormula(f))...) - } - case AST.Or: - for _, f := range nf.GetChildFormulas().GetSlice() { - result = append(result, clean(result, getContextFromFormula(f))...) - } - case AST.Imp: - result = clean(result, getContextFromFormula(nf.GetF1())) - result = append(result, clean(result, getContextFromFormula(nf.GetF2()))...) - case AST.Equ: - result = clean(result, getContextFromFormula(nf.GetF1())) - result = append(result, clean(result, getContextFromFormula(nf.GetF2()))...) - case AST.Not: - 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().ToString()))) - } - for _, term := range nf.GetArgs().GetSlice() { - result = append(result, clean(result, getContextFromTerm(term))...) - } - } - return result -} - -func getIdsFromFormula(root AST.Form) []Glob.Pair[string, string] { - result := []Glob.Pair[string, string]{} - - switch nf := root.(type) { - case AST.All: - result = getIdsFromFormula(nf.GetForm()) - case AST.Ex: - result = getIdsFromFormula(nf.GetForm()) - case AST.And: - for _, f := range nf.GetChildFormulas().GetSlice() { - result = append(result, getIdsFromFormula(f)...) - } - case AST.Or: - for _, f := range nf.GetChildFormulas().GetSlice() { - result = append(result, getIdsFromFormula(f)...) - } - case AST.Imp: - result = getIdsFromFormula(nf.GetF1()) - result = append(result, getIdsFromFormula(nf.GetF2())...) - case AST.Equ: - result = getIdsFromFormula(nf.GetF1()) - result = append(result, getIdsFromFormula(nf.GetF2())...) - case AST.Not: - result = getIdsFromFormula(nf.GetForm()) - case AST.Pred: - 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.ToString())) - } - } - return result -} - -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().ToString()))) - for _, term := range fun.GetArgs().GetSlice() { - result = append(result, clean(result, getContextFromTerm(term))...) - } - } - return result -} - -// Returns everything in add not in set -func clean(set, add []string) []string { - result := []string{} - for _, str := range add { - found := false - for _, s := range set { - if s == str { - found = true - break - } - } - if !found { - result = append(result, str) - } - } - return result -} - func contextualizeMetas(metaList Lib.List[AST.Meta]) string { - result := []string{} + result := "" for _, meta := range metaList.GetSlice() { - result = append(result, meta.ToString()) + addToGlobalEnv(Lib.MkPair(meta.ToString(), meta.GetTy())) + result += fmt.Sprintf("symbol %s : %s;\n", meta.ToString(), meta.GetTy().ToString()) } - return "symbol " + strings.Join(result, " ") + " : τ (ι);" + return result } diff --git a/src/Mods/lambdapi/utils.go b/src/Mods/lambdapi/local_context.go similarity index 50% rename from src/Mods/lambdapi/utils.go rename to src/Mods/lambdapi/local_context.go index 5e6421c8..a4eb1830 100644 --- a/src/Mods/lambdapi/utils.go +++ b/src/Mods/lambdapi/local_context.go @@ -34,60 +34,51 @@ package lambdapi import ( "fmt" + "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" + "github.com/GoelandProver/Goeland/Lib" ) -var varCounter int +var global_env Lib.List[Lib.Pair[string, AST.Ty]] = Lib.NewList[Lib.Pair[string, AST.Ty]]() -func getIncreasedCounter() int { - varCounter++ - return varCounter - 1 +func toLocalVar(i int) string { + return fmt.Sprintf("v%d", i) } -var context Glob.Map[Glob.Basic, Glob.String] = *Glob.NewMap[Glob.Basic, Glob.String]() - -func addToContext(key Glob.Basic) string { - if _, ok := context.GetExists(key); !ok { - context.Set(key, Glob.String(fmt.Sprintf("v%v", getIncreasedCounter()))) - } - - return string(context.Get(key)) +func addToLocalContext(form AST.Form, local_con Lib.List[AST.Form]) (string, Lib.List[AST.Form]) { + index := local_con.Len() + local_con.Append(form) + return toLocalVar(index), local_con } -func getFromContext(key Glob.Basic) string { - return string(context.Get(key)) -} +func getFromLocalContext(form AST.Form, local_con Lib.List[AST.Form]) string { + opt_int := Lib.ListIndexOf(form, local_con) -func toLambdaString(element Glob.Basic, str string) string { - return fmt.Sprintf("λ (%s : ϵ (%s))", addToContext(element), str) + switch index := opt_int.(type) { + case Lib.Some[int]: + return toLocalVar(index.Val) + case Lib.None[int]: + debug(Lib.MkLazy(func() string { + return fmt.Sprintf( + "Trying to find %s in local context %s", + form.ToString(), + Lib.ListToString(local_con, Lib.WithEmpty("{}")), + ) + })) + Glob.Anomaly("LambdaPi", "a formula was not found in the local context while translating") + } + return "" } -func toLambdaIntroString(element Glob.Basic, typeStr string) string { - return fmt.Sprintf("λ (%s : τ (%s))", addToContext(element), mapDefault(typeStr)) +func addToGlobalEnv(p Lib.Pair[string, AST.Ty]) { + global_env.Append(p) } -// 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{} - -// for _, element := range children { -// strArr = append(strArr, toCorrectString(element)) -// } - -// if len(strArr) == 0 && emptyValue != "" { -// strArr = append(strArr, emptyValue) -// } - -// return strings.Join(strArr, separator) -// } +func searchGlobalEnv(ty AST.Ty) Lib.Option[string] { + for _, p := range global_env.GetSlice() { + if p.Snd.Equals(ty) { + return Lib.MkSome(p.Fst) + } + } + return Lib.MkNone[string]() +} diff --git a/src/Mods/lambdapi/output.go b/src/Mods/lambdapi/output.go index 1e121be0..01d44ff0 100644 --- a/src/Mods/lambdapi/output.go +++ b/src/Mods/lambdapi/output.go @@ -32,6 +32,8 @@ package lambdapi import ( + "fmt" + "regexp" "strings" "github.com/GoelandProver/Goeland/AST" @@ -42,60 +44,146 @@ import ( ) var contextEnabled bool = false +var debug Glob.Debugger -// 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"} +var LambdapiOutputProofStruct = &Search.OutputProofStruct{ + ProofOutput: MakeLambdapiOutput, + Name: "Lambdapi", + Extension: ".lp", +} // ---------------------------------------------------------------------------- // Plugin initialisation and main function to call. // Section: init -// Functions: MakeRocqOutput -// Main functions of the rocq module. +// Functions: MakeLambdapiOutput +// Main functions of the lambdapi module. // TODO: // * Write the context for TFF problems +func InitDebugger() { + debug = Glob.CreateDebugger("LambdaPi") +} + func MakeLambdapiOutput(prf []Search.ProofStruct, meta Lib.List[AST.Meta]) string { if len(prf) == 0 { Glob.Fatal("LambdaPi", "Nothing to output") - return "" } - // FIXME: set the AST printer to (to be defined soon) LPPrinter + connectives := LambdapiPrinterConnectives() + printer := AST.Printer{PrinterAction: LambdapiPrinterAction(), PrinterConnective: &connectives} + AST.SetPrinter(printer) // Transform tableaux's proof in GS3 proof return MakeLambdaPiProof(gs3.MakeGS3Proof(prf), meta) } +func LambdapiPrinterConnectives() AST.PrinterConnective { + return AST.MkPrinterConnective( + "LambdapiPrinterConnectives", + map[AST.Connective]string{ + AST.ConnAll: "∀α λ", + AST.ConnEx: "∃α λ", + AST.ConnAnd: " ∧ ", + AST.ConnOr: " ∨ ", + AST.ConnImp: "⇒", + AST.ConnEqu: "⇔", + AST.ConnTop: "⊤", + AST.ConnBot: "⊥", + AST.ConnNot: "¬ ", + + AST.ConnPi: "∀", + AST.ConnMap: "→", + AST.ConnProd: "→", + + AST.SepArgs: " ", + AST.SepTyArgs: " ", + AST.SepArgsTyArgs: " ", + AST.SepVarsForm: ", ", + AST.SepTyVars: " ", + AST.SepVarTy: "", + + AST.SurQuantStart: "", + AST.SurQuantEnd: "", + AST.SurFunctionalStart: " ", + AST.SurFunctionalEnd: "", + }, + ) +} + +func LambdapiPrinterAction() AST.PrinterAction { + connectives := LambdapiPrinterConnectives() + + sanitize_type := func(ty_str string) string { + replace := map[string]string{ + "$i": "τ (ι)", + "$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 + } + lambdapi_action := AST.MkPrinterAction( + func(s string) string { + reg := regexp.MustCompile("([^∀∃]*)(∀α|∃α) λ ([^,]+), ([^∀∃]*)") + matches := reg.FindAllStringSubmatch(s, -1) + + if len(matches) == 0 { + return s + } + + // Properly format quantifiers: Q λ (X1 : t1), Q λ (X2 : t2), ... instead of + // Q λ (X1 : t1) (X2 : t2) ..., ... + result_string := "" + for _, match := range matches { + result_string += match[1] + quantifier := match[2] + variables := match[3] + ed := match[4] + variables_list := strings.Split(variables, ") (") + for i, variable := range variables_list { + prefix := "(" + suffix := ")" + if i == 0 { + prefix = "" + } + if i == len(variables_list)-1 { + suffix = "" + } + result_string += quantifier + " λ " + prefix + variable + suffix + ", " + } + result_string += ed + } + return result_string + }, + 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())) + }, + func(id AST.Id, tys Lib.List[string], args Lib.List[string]) string { + if strings.Contains(id.GetName(), "sko") { + return id.ToString() + } else { + return connectives.DefaultOnFunctionalArgs(id, tys, args) + } + }, + ) + lambdapi_action = lambdapi_action.Compose(AST.SanitizerAction(connectives, []string{"@"})) + return lambdapi_action.Compose(AST.RemoveSuperfluousParenthesesAction(connectives)) +} + var MakeLambdaPiProof = func(proof *gs3.GS3Sequent, meta Lib.List[AST.Meta]) string { contextString := makeContextIfNeeded(proof.GetTargetForm(), meta) proofString := makeLambdaPiProofFromGS3(proof) return contextString + "\n" + proofString } -func mapDefault(str string) string { - result := strings.ReplaceAll(strings.ReplaceAll(strings.ReplaceAll(strings.ReplaceAll(str, "$i", "ι"), "$o", "Prop"), "->", "→"), "*", "→") - return result -} - // Context flag utility function func GetContextEnabled() bool { return contextEnabled diff --git a/src/Mods/lambdapi/proof.go b/src/Mods/lambdapi/proof.go index 4db3d34d..02adbe26 100644 --- a/src/Mods/lambdapi/proof.go +++ b/src/Mods/lambdapi/proof.go @@ -38,89 +38,102 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" + "github.com/GoelandProver/Goeland/Mods/CertifUtils" "github.com/GoelandProver/Goeland/Mods/gs3" ) func makeLambdaPiProofFromGS3(proof *gs3.GS3Sequent) string { - axioms, conjecture := processMainFormula(proof.GetTargetForm()) - var resultingString string - - resultingString = makeTheorem(axioms, conjecture) - formula := proof.GetTargetForm() - - formulaStr := formula.ToString() - resultingString += fmt.Sprintf("λ (%s : ϵ %s),\n", addToContext(formula), formulaStr) - proofStr := makeProofStep(proof) - resultingString += proofStr - - return resultingString + ";\n" + axioms, conjecture := processMainFormula(formula) + + resulting_string, to_introduce := makeTheorem(axioms, conjecture) + context := Lib.NewList[AST.Form]() + resulting_string += "begin\n " + str, local_context := assume(to_introduce, context) + if to_introduce.Len() != 1 { + proof = proof.Child(0) + } + return resulting_string + str + makeProofStep(proof, local_context) + "end;\n" } -func makeProofStep(proof *gs3.GS3Sequent) string { +func makeProofStep(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { var resultingString string switch proof.Rule() { - // Closure. case gs3.AX: - resultingString = closureAxiom(proof) - - // Alpha rules + resultingString = closureAxiom(proof, context) case gs3.NNOT: - resultingString = alphaNotNot(proof) + resultingString = alphaNotNot(proof, context) case gs3.AND: - resultingString = alphaAnd(proof) + resultingString = alphaAnd(proof, context) case gs3.NOR: - resultingString = alphaNotOr(proof) + resultingString = alphaNotOr(proof, context) case gs3.NIMP: - resultingString = alphaNotImp(proof) - - // Beta rules + resultingString = alphaNotImp(proof, context) case gs3.OR: - resultingString = betaOr(proof) + resultingString = betaOr(proof, context) case gs3.NAND: - resultingString = betaNotAnd(proof) + resultingString = betaNotAnd(proof, context) case gs3.IMP: - resultingString = betaImp(proof) + resultingString = betaImp(proof, context) case gs3.EQU: - resultingString = betaEqu(proof) + resultingString = betaEqu(proof, context) case gs3.NEQU: - resultingString = betaNotEqu(proof) - - // Delta rules + resultingString = betaNotEqu(proof, context) case gs3.EX: - resultingString = deltaEx(proof) + resultingString = deltaEx(proof, context) case gs3.NALL: - resultingString = deltaNotAll(proof) - - // Gamma rules + resultingString = deltaNotAll(proof, context) case gs3.ALL: - resultingString = gammaAll(proof) + resultingString = gammaAll(proof, context) case gs3.NEX: - resultingString = gammaNotEx(proof) + resultingString = gammaNotEx(proof, context) + default: + Glob.Fatal( + "LambdaPi", + fmt.Sprintf("Translation of rule %s not implemented yet", proof.Rule().ToString()), + ) + } - // Weakening rule - case gs3.W: - Glob.Fatal("LP", "Trying to do a weakening rule but it's not implemented yet") + return resultingString +} + +func assume(formulas Lib.List[AST.Form], context Lib.List[AST.Form]) (string, Lib.List[AST.Form]) { + resulting_string := " assume" + for _, form := range formulas.GetSlice() { + val, con := addToLocalContext(form, context) + resulting_string += fmt.Sprintf(" %s", val) + context = con } + return resulting_string + ";\n", context +} - return "//" + proof.GetTargetForm().ToString() + "\n" + resultingString +func refine(lemma string, arguments Lib.List[string], in_con string, goals int) string { + arguments_string := strings.Join(arguments.GetSlice(), " ") + goals_string := strings.Repeat("_ ", goals) + return fmt.Sprintf(" refine %s %s %s %s\n", lemma, arguments_string, goals_string, in_con) } -func closureAxiom(proof *gs3.GS3Sequent) string { - target, notTarget := getPosAndNeg(proof.GetTargetForm()) +func closureAxiom(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + if CertifUtils.IsPredEqual(proof.GetTargetForm()) { + Glob.Fatal("LambdaPi", "congruence closure is not implemented yet") + } + target, notTarget := getPosAndNeg(proof.GetTargetForm()) result := "" - switch target.(type) { case AST.Pred: - result = fmt.Sprintf("GS3axiom (%s) (%s) (%s)\n", target.ToString(), getFromContext(target), getFromContext(notTarget)) + result = refine("GS3axiom", Lib.MkListV( + "("+target.ToString()+")", + getFromLocalContext(target, context), + getFromLocalContext(notTarget, context), + ), "", 0) case AST.Top: - result = fmt.Sprintf("GS3ntop (%s)\n", getFromContext(notTarget)) + result = refine("GS3ntop", Lib.MkListV(getFromLocalContext(notTarget, context)), "", 0) case AST.Bot: - result = fmt.Sprintf("GS3bot (%s)\n", getFromContext(target)) + result = refine("GS3bot", Lib.MkListV(getFromLocalContext(target, context)), "", 0) } - return result + return result + ";" } func getPosAndNeg(target AST.Form) (pos, neg AST.Form) { @@ -130,230 +143,244 @@ func getPosAndNeg(target AST.Form) (pos, neg AST.Form) { return target, AST.MakerNot(target) } -func allRules(rule string, target AST.Form, composingForms Lib.List[AST.Form], nexts []*gs3.GS3Sequent, children []Lib.List[AST.Form]) string { - result := rule + "\n" - - for _, composingForm := range composingForms.GetSlice() { - result += "(" + composingForm.ToString() + ")\n" - } - - result += getRecursionUnivStr(nexts, children) - - result += fmt.Sprintf("(%s)\n", getFromContext(target)) - - return result -} - -func allRulesQuantUniv( - rule string, - target AST.Form, - composingForms Lib.List[AST.Form], - nexts []*gs3.GS3Sequent, - children []Lib.List[AST.Form], - vars Lib.List[AST.TypedVar], - termGen AST.Term, +func refineGenericRule( + lemma string, + proof *gs3.GS3Sequent, + remaining_goals int, + context Lib.List[AST.Form], ) string { - - quant := "" - typeStr := "" - // 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, " + composingForms.At(0).ToString() + ")\n" - - varStrs := []string{} - for _, singleVar := range vars.GetSlice() { - varStrs = append(varStrs, toLambdaIntroString(singleVar, "")) + formulas_list := Lib.NewList[string]() + + // If a term was generated, get its type and place the stuff in the right order: the type of + // the generated term, the formula and then the term. + if gs3.IsGammaRule(proof.Rule()) || gs3.IsDeltaRule(proof.Rule()) { + ty := getTypeOfFirstBoundVar(proof.GetTargetForm()) + formated_child := getFormattedChild(proof.GetTargetForm()) + formulas_list = Lib.MkListV( + "("+strings.ReplaceAll(ty.ToString(), "τ", "")+")", + "("+formated_child+")", + ) + if gs3.IsGammaRule(proof.Rule()) { + // FIXME: use an option type instead of nil + if proof.TermGenerated() != nil { + formulas_list.Append(getFormattedTerm(proof.TermGenerated())) + } else { + // Try to find something in the global env, otherwise: fail + // FIXME: we should also try to find something in the local (term) environment + // (this does not exist yet) + switch term := searchGlobalEnv(ty).(type) { + case Lib.Some[string]: + formulas_list.Append(term.Val) + default: + Glob.Fatal("LambdaPi", fmt.Sprintf( + "no term of type %s available to instantiate the universal formula %s.", + ty.ToString(), + proof.GetTargetForm().ToString(), + )) + } + } + } + } else { + child_formulas := proof.GetTargetForm().GetChildFormulas() + switch f := proof.GetTargetForm().(type) { + case AST.Not: + child_formulas = f.GetForm().GetChildFormulas() + } + for _, form := range child_formulas.GetSlice() { + formulas_list.Append("(" + form.ToString() + ")") + } } - result = fmt.Sprintf(result, strings.Join(varStrs, ", "+quant+" ")) - result += "(" + termGen.ToString() + ")\n" - - result += getRecursionUnivStr(nexts, children) - - result += fmt.Sprintf("(%s)\n", getFromContext(target)) + result_string := refine( + lemma, + formulas_list, + getFromLocalContext(proof.GetTargetForm(), context), + remaining_goals, + ) - return result + if remaining_goals <= 1 { + result_string = result_string[:len(result_string)-1] + ";\n" + assumptions, con := assume(proof.GetResultFormulasOfChild(0), Lib.ListCpy(context)) + if gs3.IsDeltaRule(proof.Rule()) { + assumptions = fmt.Sprintf( + "assume %s;", + getFormattedTerm(proof.TermGenerated()), + ) + assumptions + } + result_string += assumptions + result_string += makeProofStep(proof.Child(0), con) + } else { + for i := 0; i < remaining_goals; i++ { + result_string += "{\n" + assumptions, con := assume(proof.GetResultFormulasOfChild(i), Lib.ListCpy(context)) + result_string += assumptions + result_string += makeProofStep(proof.Child(i), con) + result_string += "}\n" + } + result_string = result_string[:len(result_string)-1] + ";\n" + } + return result_string } -func getRecursionUnivStr(nexts []*gs3.GS3Sequent, children []Lib.List[AST.Form]) (result string) { - for i, next := range nexts { - result += "(\n" - for _, childForm := range children[i].GetSlice() { - result += toLambdaString(childForm, childForm.ToString()) + ",\n" +func getFormattedTerm(term AST.Term) string { + switch t := term.(type) { + case AST.Fun: + if strings.Contains(t.GetName(), "sko") { + return t.GetID().ToString() } - proofStr := makeProofStep(next) - result += proofStr - result += ")\n" } - return result + return term.ToString() } -func allRulesQuantExist( - rule string, - target AST.Form, - composingForms Lib.List[AST.Form], - nexts []*gs3.GS3Sequent, - children []Lib.List[AST.Form], - vars Lib.List[AST.TypedVar], - termGen AST.Term, -) string { - quant := "" - typeStr := "" - // 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, " + composingForms.At(0).ToString() + ")\n" - - varStrs := []string{} - for _, singleVar := range vars.GetSlice() { - varStrs = append(varStrs, toLambdaIntroString(singleVar, "")) +func getTypeOfFirstBoundVar(form AST.Form) AST.Ty { + getTySafe := func(var_list Lib.List[AST.TypedVar]) AST.Ty { + if var_list.Empty() { + debug(Lib.MkLazy(func() string { + return fmt.Sprintf( + "Formula %s has no bound variable, cannot get its type", + form.ToString(), + ) + })) + Glob.Anomaly("LambdaPi", "No bound variable.") + } + return var_list.At(0).GetTy() } - result = fmt.Sprintf(result, strings.Join(varStrs, ", "+quant+" ")) - result += getRecursionExistStr(nexts, children, termGen) - - result += fmt.Sprintf("(%s)\n", getFromContext(target)) + switch f := form.(type) { + case AST.Not: + switch nf := f.GetForm().(type) { + case AST.All: + return getTySafe(nf.GetVarList()) + case AST.Ex: + return getTySafe(nf.GetVarList()) + } + case AST.All: + return getTySafe(f.GetVarList()) + case AST.Ex: + return getTySafe(f.GetVarList()) + } - return result + debug(Lib.MkLazy(func() string { + return fmt.Sprintf( + "Called getTypeOfFirstBoundVar of %s which should have been a quantified formula (or a negation of such a formula)", + form.ToString(), + ) + })) + Glob.Anomaly("LambdaPi", "Not a quantifier formula") + return nil } -func getRecursionExistStr(nexts []*gs3.GS3Sequent, children []Lib.List[AST.Form], termGen AST.Term) (result string) { - for i, next := range nexts { - result += "(\n" - typesStr := "" - if _, ok := termGen.(AST.Fun); ok { - typesStr = mapDefault("") - } - result += toLambdaIntroString(termGen, typesStr) + ",\n" - for _, childForm := range children[i].GetSlice() { - result += toLambdaString(childForm, childForm.ToString()) + ",\n" +// Gets the child formula as a λ (bound_var : ty), P +func getFormattedChild(form AST.Form) string { + format := func(var_list Lib.List[AST.TypedVar], f AST.Form, maker func(Lib.List[AST.TypedVar], AST.Form) AST.Form) string { + f = maker(var_list.Slice(1, var_list.Len()), f) + return fmt.Sprintf( + "λ (%s : %s), %s", + var_list.At(0).GetName(), + var_list.At(0).GetTy().ToString(), + f.ToString(), + ) + } + + switch f := form.(type) { + case AST.Not: + switch nf := f.GetForm().(type) { + case AST.All: + return format(nf.GetVarList(), nf.GetForm(), func(vl Lib.List[AST.TypedVar], f AST.Form) AST.Form { + if !vl.Empty() { + f = AST.MakerAll(vl, f) + } + return f + }) + case AST.Ex: + return format(nf.GetVarList(), nf.GetForm(), func(vl Lib.List[AST.TypedVar], f AST.Form) AST.Form { + if !vl.Empty() { + f = AST.MakerEx(vl, f) + } + return f + }) } - proofStr := makeProofStep(next) - result += proofStr - result += ")\n" + case AST.All: + return format(f.GetVarList(), f.GetForm(), func(vl Lib.List[AST.TypedVar], f AST.Form) AST.Form { + if !vl.Empty() { + f = AST.MakerAll(vl, f) + } + return f + }) + case AST.Ex: + return format(f.GetVarList(), f.GetForm(), func(vl Lib.List[AST.TypedVar], f AST.Form) AST.Form { + if !vl.Empty() { + f = AST.MakerEx(vl, f) + } + return f + }) } - return result -} -func alphaNotNot(proof *gs3.GS3Sequent) string { - composingForms := proof.GetTargetForm().GetChildFormulas().At(0).GetChildFormulas() - return allRules("GS3nnot", proof.GetTargetForm(), composingForms, proof.Children(), proof.GetResultFormulasOfChildren()) + Glob.Anomaly("LambdaPi", "Not a quantifier formula") + return "" } -func alphaAnd(proof *gs3.GS3Sequent) string { - return allRules("GS3and", proof.GetTargetForm(), proof.GetTargetForm().GetChildFormulas(), proof.Children(), proof.GetResultFormulasOfChildren()) +func refineUnaryRule(lemma string, proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineGenericRule(lemma, proof, 1, context) } -func alphaNotOr(proof *gs3.GS3Sequent) string { - composingForms := proof.GetTargetForm().GetChildFormulas().At(0).GetChildFormulas() - return allRules("GS3nor", proof.GetTargetForm(), composingForms, proof.Children(), proof.GetResultFormulasOfChildren()) +func refineBinaryRule(lemma string, proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineGenericRule(lemma, proof, 2, context) } -func alphaNotImp(proof *gs3.GS3Sequent) string { - composingForms := proof.GetTargetForm().GetChildFormulas().At(0).GetChildFormulas() - return allRules("GS3nimp", proof.GetTargetForm(), composingForms, proof.Children(), proof.GetResultFormulasOfChildren()) +func alphaNotNot(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineUnaryRule("GS3nnot", proof, context) } -func betaOr(proof *gs3.GS3Sequent) string { - return allRules("GS3or", proof.GetTargetForm(), proof.GetTargetForm().GetChildFormulas(), proof.Children(), proof.GetResultFormulasOfChildren()) +func alphaAnd(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineUnaryRule("GS3and", proof, context) } -func betaNotAnd(proof *gs3.GS3Sequent) string { - composingForms := proof.GetTargetForm().GetChildFormulas().At(0).GetChildFormulas() - return allRules("GS3nand", proof.GetTargetForm(), composingForms, proof.Children(), proof.GetResultFormulasOfChildren()) +func alphaNotOr(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineUnaryRule("GS3nor", proof, context) } -func betaImp(proof *gs3.GS3Sequent) string { - return allRules("GS3imp", proof.GetTargetForm(), proof.GetTargetForm().GetChildFormulas(), proof.Children(), proof.GetResultFormulasOfChildren()) +func alphaNotImp(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineUnaryRule("GS3nimp", proof, context) } -func betaEqu(proof *gs3.GS3Sequent) string { - return allRules("GS3equ", proof.GetTargetForm(), proof.GetTargetForm().GetChildFormulas(), proof.Children(), proof.GetResultFormulasOfChildren()) +func betaOr(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineBinaryRule("GS3or", proof, context) } -func betaNotEqu(proof *gs3.GS3Sequent) string { - composingForms := proof.GetTargetForm().GetChildFormulas().At(0).GetChildFormulas() - return allRules("GS3nequ", proof.GetTargetForm(), composingForms, proof.Children(), proof.GetResultFormulasOfChildren()) +func betaNotAnd(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineBinaryRule("GS3nand", proof, context) } -func deltaEx(proof *gs3.GS3Sequent) string { - var formulaEx AST.Ex - if form, ok := proof.GetTargetForm().(AST.Ex); ok { - formulaEx = form - } - - return allRulesQuantExist( - "GS3ex", - proof.GetTargetForm(), - proof.GetTargetForm().GetChildFormulas(), - proof.Children(), - proof.GetResultFormulasOfChildren(), - formulaEx.GetVarList(), - proof.TermGenerated(), - ) +func betaImp(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineBinaryRule("GS3imp", proof, context) } -func deltaNotAll(proof *gs3.GS3Sequent) string { - var formulaAll AST.All - if notForm, ok := proof.GetTargetForm().(AST.Not); ok { - if form, ok := notForm.GetForm().(AST.All); ok { - formulaAll = form - } - } - composingForms := proof.GetTargetForm().GetChildFormulas().At(0).GetChildFormulas() +func betaEqu(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineBinaryRule("GS3equ", proof, context) +} - return allRulesQuantExist("GS3nall", proof.GetTargetForm(), composingForms, proof.Children(), proof.GetResultFormulasOfChildren(), formulaAll.GetVarList(), proof.TermGenerated()) +func betaNotEqu(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineBinaryRule("GS3nequ", proof, context) } -func gammaAll(proof *gs3.GS3Sequent) string { - var formulaAll AST.All - if form, ok := proof.GetTargetForm().(AST.All); ok { - formulaAll = form - } +func deltaEx(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineUnaryRule("GS3ex", proof, context) +} - return allRulesQuantUniv( - "GS3all", - proof.GetTargetForm(), - proof.GetTargetForm().GetChildFormulas(), - proof.Children(), - proof.GetResultFormulasOfChildren(), - formulaAll.GetVarList(), - proof.TermGenerated(), - ) +func deltaNotAll(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineUnaryRule("GS3nall", proof, context) } -func gammaNotEx(proof *gs3.GS3Sequent) string { - var formulaEx AST.Ex - if notForm, ok := proof.GetTargetForm().(AST.Not); ok { - if form, ok := notForm.GetForm().(AST.Ex); ok { - formulaEx = form - } - } - composingForms := proof.GetTargetForm().GetChildFormulas().At(0).GetChildFormulas() +func gammaAll(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineUnaryRule("GS3all", proof, context) +} - return allRulesQuantUniv("GS3nex", proof.GetTargetForm(), composingForms, proof.Children(), proof.GetResultFormulasOfChildren(), formulaEx.GetVarList(), proof.TermGenerated()) +func gammaNotEx(proof *gs3.GS3Sequent, context Lib.List[AST.Form]) string { + return refineUnaryRule("GS3nex", proof, context) } -// Processes the formula that was proven by Goéland. +// Split the axiom & conjecture formula from the root formula. func processMainFormula(form AST.Form) (Lib.List[AST.Form], AST.Form) { formList := Lib.NewList[AST.Form]() switch nf := form.(type) { @@ -368,20 +395,19 @@ 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(), ".", "_"), "=", "_"), "+", "_") +func makeTheorem(axioms Lib.List[AST.Form], conjecture AST.Form) (string, Lib.List[AST.Form]) { + problemName := CertifUtils.SanitizedTheoremName() axioms = Lib.ListCpy(axioms) axioms.Append(AST.MakerNot(conjecture)) formattedProblem := makeImpChain(axioms) - return "symbol goeland_" + problemName + " : \nϵ " + formattedProblem.ToString() + " → ϵ ⊥ ≔ \n" + return "symbol goeland_" + problemName + " : \n" + formattedProblem + " → ϵ ⊥ ≔ \n", axioms } // If [F1, F2, F3] is a formlist, then this function returns F1 -> (F2 -> F3). -func makeImpChain(forms Lib.List[AST.Form]) AST.Form { - last := forms.Len() - 1 - form := forms.At(last) - for i := last - 1; i >= 0; i-- { - form = AST.MakerImp(forms.At(i), form) +func makeImpChain(forms Lib.List[AST.Form]) string { + imp_chain := []string{} + for _, form := range forms.GetSlice() { + imp_chain = append(imp_chain, fmt.Sprintf("ϵ (%s)", form.ToString())) } - return form + return strings.Join(imp_chain, " → ") } diff --git a/src/Mods/rocq/context.go b/src/Mods/rocq/context.go index 15d16e86..27d185e3 100644 --- a/src/Mods/rocq/context.go +++ b/src/Mods/rocq/context.go @@ -43,9 +43,8 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" + "github.com/GoelandProver/Goeland/Mods/CertifUtils" "github.com/GoelandProver/Goeland/Mods/dmt" - "github.com/GoelandProver/Goeland/Typing" - "slices" ) func makeContextIfNeeded(root AST.Form, metaList Lib.List[AST.Meta]) string { @@ -62,7 +61,10 @@ func makeContextIfNeeded(root AST.Form, metaList Lib.List[AST.Meta]) string { } // if AST.EmptyGlobalContext() { - resultingString += strings.Join(getContextFromFormula(root), "\n") + "\n" + contextual_symbols := CertifUtils.GetContextFromFormula(root) + for _, p := range contextual_symbols.GetSlice() { + resultingString += fmt.Sprintf("Parameter %s : %s.\n", p.Fst.ToString(), p.Snd.ToString()) + } if metaList.Len() > 0 { resultingString += contextualizeMetas(metaList) @@ -94,82 +96,6 @@ func contextPreamble() string { return str } -func getContextFromFormula(root AST.Form) []string { - result := []string{} - switch nf := root.(type) { - case AST.All: - result = getContextFromFormula(nf.GetForm()) - case AST.Ex: - result = getContextFromFormula(nf.GetForm()) - case AST.And: - for _, f := range nf.GetChildFormulas().GetSlice() { - result = append(result, clean(result, getContextFromFormula(f))...) - } - case AST.Or: - for _, f := range nf.GetChildFormulas().GetSlice() { - result = append(result, clean(result, getContextFromFormula(f))...) - } - case AST.Imp: - result = clean(result, getContextFromFormula(nf.GetF1())) - result = append(result, clean(result, getContextFromFormula(nf.GetF2()))...) - case AST.Equ: - result = clean(result, getContextFromFormula(nf.GetF1())) - result = append(result, clean(result, getContextFromFormula(nf.GetF2()))...) - case AST.Not: - result = clean(result, getContextFromFormula(nf.GetForm())) - case AST.Pred: - if !nf.GetID().Equals(AST.Id_eq) { - 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))...) - } - } - return result -} - -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, - fmt.Sprintf("Parameter %s : %s.", fun.GetID().ToString(), ty.ToString())) - for _, term := range fun.GetArgs().GetSlice() { - result = append(result, clean(result, getContextFromTerm(term))...) - } - } - return result -} - -// Returns everything in add not in set -func clean(set, add []string) []string { - result := []string{} - for _, str := range add { - found := slices.Contains(set, str) - if !found { - result = append(result, str) - } - } - return result -} - func contextualizeMetas(metaList Lib.List[AST.Meta]) string { result := []string{} for _, meta := range metaList.GetSlice() { diff --git a/src/Mods/rocq/output.go b/src/Mods/rocq/output.go index 1b75f8f5..b4716c03 100644 --- a/src/Mods/rocq/output.go +++ b/src/Mods/rocq/output.go @@ -121,6 +121,7 @@ func RocqPrinterAction() AST.PrinterAction { func(typed_var Lib.Pair[string, AST.Ty]) string { return fmt.Sprintf("(%s : %s)", typed_var.Fst, sanitize_type(typed_var.Snd.ToString())) }, + connectives.DefaultOnFunctionalArgs, ) rocq_action = rocq_action.Compose(AST.SanitizerAction(connectives, []string{"@"})) return rocq_action.Compose(AST.RemoveSuperfluousParenthesesAction(connectives)) diff --git a/src/Mods/rocq/proof.go b/src/Mods/rocq/proof.go index e6c27212..f0588249 100644 --- a/src/Mods/rocq/proof.go +++ b/src/Mods/rocq/proof.go @@ -43,6 +43,7 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" + "github.com/GoelandProver/Goeland/Mods/CertifUtils" "github.com/GoelandProver/Goeland/Mods/dmt" "github.com/GoelandProver/Goeland/Mods/gs3" ) @@ -111,7 +112,7 @@ func makeStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], constantsCre // 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()) { + if !CertifUtils.IsPredEqual(proof.GetTargetForm()) { Glob.Anomaly("rocq", fmt.Sprintf( "Index of %s not found in { %s }", proof.GetTargetForm().ToString(), @@ -123,7 +124,7 @@ func makeStep(proof *gs3.GS3Sequent, hypotheses Lib.List[AST.Form], constantsCre switch proof.Rule() { // Closure. case gs3.AX: - if isPredEqual(proof.GetTargetForm()) { + if CertifUtils.IsPredEqual(proof.GetTargetForm()) { resultingString = "congruence." } else { resultingString = "auto." @@ -253,10 +254,7 @@ 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 := Glob.GetProblemName() - for _, s := range []string{".", "=", "+", "-"} { - problemName = strings.ReplaceAll(problemName, s, "_") - } + problemName := CertifUtils.SanitizedTheoremName() axiomsWithConj := Lib.ListCpy(axioms) axiomsWithConj.Append(AST.MakerNot(AST.MakerNot(conjecture))) formattedProblem := makeImpChain(axiomsWithConj) @@ -303,16 +301,6 @@ func introNames(il []int, sep ...string) string { return strings.Join(Glob.MapTo(il, func(_ int, f int) string { return introName(f) }), s) } -func isPredEqual(f AST.Form) bool { - if not, isNot := f.(AST.Not); isNot { - f = not.GetForm() - } - if p, isPred := f.(AST.Pred); isPred { - return p.GetID().Equals(AST.Id_eq) - } - return false -} - func addTermGenerated(constantsCreated []AST.Term, term AST.Term) ([]AST.Term, string) { if term == nil { dummy++ diff --git a/src/main.go b/src/main.go index 4f51ef7d..09522373 100644 --- a/src/main.go +++ b/src/main.go @@ -56,6 +56,7 @@ import ( "github.com/GoelandProver/Goeland/Mods/dmt" equality "github.com/GoelandProver/Goeland/Mods/equality/bse" "github.com/GoelandProver/Goeland/Mods/gs3" + "github.com/GoelandProver/Goeland/Mods/lambdapi" "github.com/GoelandProver/Goeland/Parser" "github.com/GoelandProver/Goeland/Search" "github.com/GoelandProver/Goeland/Search/incremental" @@ -222,6 +223,7 @@ func initDebuggers() { Unif.InitDebugger() Engine.InitDebugger() gs3.InitDebugger() + lambdapi.InitDebugger() } // FIXME: eventually, we would want to add an "interpretation" layer between elab and internal representation that does this From 3510b6363822373442a3d7bee6acbba45336e670 Mon Sep 17 00:00:00 2001 From: Johann Rosain Date: Wed, 8 Oct 2025 10:06:06 +0200 Subject: [PATCH 4/4] Upd: update contributing to include test-suite instructions (and special instructions for lambdapi) --- CONTRIBUTING.md | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 6dce2662..4ba42610 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -8,11 +8,12 @@ wish to contribute to Goéland, you should start by [forking](https://github.com/GoelandProver/Goeland/fork) the repository. Then, you can work on on your feature/bug fix/enhancement in your local repository. -Once you deem your work satisfactory, you should [open a pull -request](#working-with-pull-requests) targeting -master. Then, one of the maintainer will review your code as soon as -possible. If you have no feedback for a few days, do not hesitate to ping one of -them. The current maintainers are: @jcailler, @jrosain. +Once you deem your work satisfactory and have properly updated the test suite +(c.f. [Managing the test suite](#managing-the-test-suite)), you should [open a pull +request](#working-with-pull-requests) **targeting master**. Then, one +of the maintainer will review your code as soon as possible. If you have no feedback for a +few days, do not hesitate to ping one of them. The current maintainers are: @jcailler, +@jrosain. Your code is expected to (i) build, (ii) satisfy the unit tests and (iii) not prove countertheorems. This check *does not* run automatically. One of the @@ -39,6 +40,25 @@ have a very descriptive error as it will make things easier to debug. Note that, by default, neither of these options `panic`. You have to activate the `-debug` flag in order for them to panic and you to have a backtrace. +### Managing the test suite + +In order to have a systematic testing of Goéland, we have a [test +suite](devtools/test-suite) that contains: +- basic test files to check functionalities, +- bug files that correspond to a reported bug that has been resolved, and +- output files that test the output of Goéland. + +When you add a new functionality to Goéland, you must add some files to the +[basic](devtools/test-suite/basic) folder that tests your newly implemented +functionalities. If your pull request fixes a bug, you must add the bug file to the +[bugs](devtools/test-suite/bugs) folder. Beware that we run the Rocq and Lambdapi output +on the test suite, so you should think about whether a problem is checkable or not. If +it's not, add them in the corresponding `no_chk` instead. The current not-checkable +problems are problems involving a typed context. Moreover, if your problem includes +equalities, the Lambdapi check may fail. If so, add your problem to the +`lp_tolerate_fails` variable in the `run-test-suite` file. + + ## For Maintainers By default, a pull request that modifies the go source code has the `needs:ci`