From 30b0c340e94c6e981d3115c554ab9bc97f8b8971 Mon Sep 17 00:00:00 2001 From: Florian Cassayre Date: Thu, 23 Jun 2022 14:02:38 +0200 Subject: [PATCH] Tidy examples --- .../masterproject/examples/frontInteractiveProof1.scala | 9 +++++++++ .../masterproject/examples/frontInteractiveProof2.scala | 4 ++++ .../florian/masterproject/examples/frontSolver.scala | 4 +--- 3 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof1.scala b/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof1.scala index 9d03b76..03696c0 100644 --- a/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof1.scala +++ b/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof1.scala @@ -1,5 +1,7 @@ package me.cassayre.florian.masterproject.examples +import lisa.kernel.proof.SCProofChecker + import scala.util.chaining.* import me.cassayre.florian.masterproject.front.fol.FOL.{*, given} import me.cassayre.florian.masterproject.front.proof.Proof.{*, given} @@ -56,4 +58,11 @@ import me.cassayre.florian.masterproject.front.theory.SetTheory.* p.asTheorem() } + + println("=== Reconstruction ===") + println("(t0):") + println(KernelPrinter.prettyJudgedProof(SCProofChecker.checkSCProof(reconstructSCProofForTheorem(t0)))) + println() + println("(t1):") + println(KernelPrinter.prettyJudgedProof(SCProofChecker.checkSCProof(reconstructSCProofForTheorem(t1)))) } diff --git a/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof2.scala b/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof2.scala index cfb0db9..e2f0477 100644 --- a/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof2.scala +++ b/src/main/scala/me/cassayre/florian/masterproject/examples/frontInteractiveProof2.scala @@ -1,5 +1,6 @@ package me.cassayre.florian.masterproject.examples +import lisa.kernel.proof.SCProofChecker import me.cassayre.florian.masterproject.front.fol.FOL.{*, given} import me.cassayre.florian.masterproject.front.parser.FrontMacro.{*, given} import me.cassayre.florian.masterproject.front.printer.FrontPositionedPrinter.* @@ -157,4 +158,7 @@ import scala.util.chaining.* asTheorem() } + + println("=== Reconstruction ===") + println(KernelPrinter.prettyJudgedProof(SCProofChecker.checkSCProof(reconstructSCProofForTheorem(thmUnionAny)))) } diff --git a/src/main/scala/me/cassayre/florian/masterproject/examples/frontSolver.scala b/src/main/scala/me/cassayre/florian/masterproject/examples/frontSolver.scala index 8667026..d2baaa1 100644 --- a/src/main/scala/me/cassayre/florian/masterproject/examples/frontSolver.scala +++ b/src/main/scala/me/cassayre/florian/masterproject/examples/frontSolver.scala @@ -21,9 +21,7 @@ import scala.util.chaining.* val theorem: Theorem = ProofMode(sequent).tap(_(propositionalSolver)).asTheorem() val scProof: SCProof = reconstructSCProofForTheorem(theorem) - println(KernelPrinter.prettyProof(scProof)) - println() - assert(SCProofChecker.checkSCProof(scProof).isValid) + println(KernelPrinter.prettyJudgedProof(SCProofChecker.checkSCProof(scProof))) } testSolve(sequent"?a |- ?a")