Fix lambdapi output by updating it with the new printer system

.gitignore

@@ -1,3 +1,5 @@
+*.lpo
+
 .direnv
 [Pp]roblems
 [Oo]utput

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`

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,45 +115,40 @@ 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:
     - 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).
+    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)

proof-certification/LambdaPi/Makefile

@@ -0,0 +1,20 @@
+.POSIX:
+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:
+
+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 $<

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
+```

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)

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),
 	)
 }