Add lambda-terms to FOL

backup/backup2/prooflib/Library.scala

@@ -0,0 +1,106 @@
+package lisa.prooflib
+
+import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.SCProofChecker
+import lisa.kernel.proof.SCProofCheckerJudgement
+import lisa.kernel.proof.SequentCalculus
+import lisa.prooflib.ProofTacticLib.ProofTactic
+import lisa.utils.KernelHelpers.{_, given}
+import lisa.utils.{_, given}
+
+import scala.collection.mutable.Stack as stack
+
+/**
+ * A class abstracting a [[lisa.kernel.proof.RunningTheory]] providing utility functions and a convenient syntax
+ * to write and use Theorems and Definitions.
+ * @param theory The inner RunningTheory
+ */
+abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.ProofsHelpers {
+
+  val theory: RunningTheory
+  given library: this.type = this
+  given RunningTheory = theory
+
+  export lisa.kernel.proof.SCProof
+
+  val K = lisa.utils.K
+  val SC: SequentCalculus.type = K.SC
+  private[prooflib] val F = lisa.fol.FOL
+  import F.{given}
+
+  var last: Option[JUSTIFICATION] = None
+
+  // Options for files
+  private[prooflib] var _withCache: Boolean = false
+  def withCache(using file: sourcecode.File, om: OutputManager)(): Unit =
+    if last.nonEmpty then om.output(OutputManager.WARNING("Warning: withCache option should be used before the first definition or theorem."))
+    else _withCache = true
+
+  private[prooflib] var _draft: Option[sourcecode.File] = None
+  def draft(using file: sourcecode.File, om: OutputManager)(): Unit =
+    if last.nonEmpty then om.output(OutputManager.WARNING("Warning: draft option should be used before the first definition or theorem."))
+    else _draft = Some(file)
+  def isDraft = _draft.nonEmpty
+
+  val knownDefs: scala.collection.mutable.Map[F.Constant[?], Option[JUSTIFICATION]] = scala.collection.mutable.Map.empty
+  val shortDefs: scala.collection.mutable.Map[F.Constant[?], Option[JUSTIFICATION]] = scala.collection.mutable.Map.empty
+
+  def addSymbol(s: F.Constant[?]): Unit = 
+    theory.addSymbol(s.underlying)
+    knownDefs.update(s, None)
+
+  def getDefinition(label: F.Constant[?]): Option[JUSTIFICATION] = knownDefs.get(label) match {
+    case None => throw new UserLisaException.UndefinedSymbolException("Unknown symbol", label, this)
+    case Some(value) => value
+  }
+  def getShortDefinition(label: F.Constant[?]): Option[JUSTIFICATION] = shortDefs.get(label) match {
+    case None => throw new UserLisaException.UndefinedSymbolException("Unknown symbol", label, this)
+    case Some(value) => value
+  }
+
+  /**
+   * An alias to create a Theorem
+   */
+  def makeTheorem(name: String, statement: K.Sequent, proof: K.SCProof, justifications: Seq[theory.Justification]): K.Judgement[theory.Theorem] =
+    theory.theorem(name, statement, proof, justifications)
+
+  // DEFINITION Syntax
+
+  /*
+  /**
+   * Allows to create a definition by shortcut of a function symbol:
+   */
+  def makeSimpleFunctionDefinition(symbol: String, expression: K.LambdaTermTerm): K.Judgement[theory.FunctionDefinition] = {
+    import K.*
+    val LambdaTermTerm(vars, body) = expression
+
+    val out: VariableLabel = VariableLabel(freshId((vars.map(_.id) ++ body.schematicTermLabels.map(_.id)).toSet, "y"))
+    val proof: SCProof = simpleFunctionDefinition(expression, out)
+    theory.functionDefinition(symbol, LambdaTermFormula(vars, out === body), out, proof, out === body, Nil)
+  }
+    */
+
+  /**
+   * Allows to create a definition by shortcut of a predicate symbol:
+   */
+  def makeSimpleDefinition(symbol: String, expression: K.Expression): K.Judgement[theory.Definition] =
+    theory.definition(symbol, expression)
+
+
+  /**
+   * Prints a short representation of the given theorem or definition
+   */
+  def show(using om: OutputManager)(thm: JUSTIFICATION) = {
+    if (thm.withSorry) om.output(thm.repr, Console.YELLOW)
+    else om.output(thm.repr, Console.GREEN)
+  }
+
+  /**
+   * Prints a short representation of the last theorem or definition introduced
+   */
+  def show(using om: OutputManager): Unit = last match {
+    case Some(value) => show(value)
+    case None => throw new NoSuchElementException("There is nothing to show: No theorem or definition has been proved yet.")
+  }
+
+}

backup/backup2/prooflib/OutputManager.scala

@@ -0,0 +1,52 @@
+package lisa.prooflib
+
+import lisa.utils.KernelHelpers.{_, given}
+import lisa.utils.{_, given}
+
+import java.io.PrintWriter
+import java.io.StringWriter
+
+abstract class OutputManager {
+
+  given OutputManager = this
+
+  def output(s: String): Unit = stringWriter.write(s + "\n")
+  def output(s: String, color: String): Unit = stringWriter.write(Console.RESET + color + s + "\n" + Console.RESET)
+  val stringWriter: StringWriter
+
+  def finishOutput(exception: Exception): Nothing
+
+  def lisaThrow(le: LisaException): Nothing =
+    le match {
+      case ule: UserLisaException =>
+        ule.fixTrace()
+        output(ule.showError)
+        finishOutput(ule)
+
+      case e: LisaException.InvalidKernelJustificationComputation =>
+        e.proof match {
+          case Some(value) => output(lisa.prooflib.ProofPrinter.prettyProof(value))
+          case None => ()
+        }
+        output(e.underlying.repr)
+        finishOutput(e)
+
+    }
+
+  def log(e: Exception): Unit = {
+    stringWriter.write("\n[" + Console.RED + "Error" + Console.RESET + "] ")
+    e.printStackTrace(PrintWriter(stringWriter))
+    output(Console.RESET)
+  }
+
+}
+object OutputManager {
+  def RED(s: String): String = Console.RED + s + Console.RESET
+  def GREEN(s: String): String = Console.GREEN + s + Console.RESET
+  def BLUE(s: String): String = Console.BLUE + s + Console.RESET
+  def YELLOW(s: String): String = Console.YELLOW + s + Console.RESET
+  def CYAN(s: String): String = Console.CYAN + s + Console.RESET
+  def MAGENTA(s: String): String = Console.MAGENTA + s + Console.RESET
+
+  def WARNING(s: String): String = Console.YELLOW + "⚠ " + s + Console.RESET
+}

lisa-utils/src/main/scala/lisa/utils/parsing/ProofPrinter.scala → backup/backup2/prooflib/ProofPrinter.scala

@@ -1,14 +1,12 @@
-package lisa.utils.parsing
+package lisa.prooflib
 
 import lisa.kernel.proof.SCProofCheckerJudgement
 import lisa.prooflib.BasicStepTactic.SUBPROOF
 import lisa.prooflib.Library
 import lisa.prooflib.*
 import lisa.utils.*
 
-//temporary - get merged wit regular printer in time
 object ProofPrinter {
-
   private def spaceSeparator(compact: Boolean): String = if (compact) "" else " "
 
   private def commaSeparator(compact: Boolean, symbol: String = ","): String = s"$symbol${spaceSeparator(compact)}"

backup/backup2/prooflib/ProofTacticLib.scala

@@ -0,0 +1,66 @@
+package lisa.prooflib
+
+import lisa.fol.FOL as F
+import lisa.prooflib.*
+import lisa.utils.K
+import lisa.utils.UserLisaException
+import lisa.prooflib.ProofPrinter
+
+object ProofTacticLib {
+  type Arity = Int & Singleton
+
+  /**
+   * A ProofTactic is an object that relies on a step of premises and which can be translated into pure Sequent Calculus.
+   */
+  trait ProofTactic {
+    val name: String = this.getClass.getName.split('$').last
+    given ProofTactic = this
+
+  }
+
+  trait OnlyProofTactic {
+    def apply(using lib: Library, proof: lib.Proof): proof.ProofTacticJudgement
+  }
+
+  trait ProofSequentTactic {
+    def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement
+  }
+
+  trait ProofFactTactic {
+    def apply(using lib: Library, proof: lib.Proof)(premise: proof.Fact): proof.ProofTacticJudgement
+  }
+  trait ProofFactSequentTactic {
+    def apply(using lib: Library, proof: lib.Proof)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement
+  }
+
+  class UnapplicableProofTactic(val tactic: ProofTactic, proof: Library#Proof, errorMessage: String)(using sourcecode.Line, sourcecode.File) extends UserLisaException(errorMessage) {
+    override def fixTrace(): Unit = {
+      val start = getStackTrace.indexWhere(elem => {
+        !elem.getClassName.contains(tactic.name)
+      }) + 1
+      setStackTrace(getStackTrace.take(start))
+    }
+
+    def showError: String = {
+      val source = scala.io.Source.fromFile(file.value)
+      val textline = source.getLines().drop(line.value - 1).next().dropWhile(c => c.isWhitespace)
+      source.close()
+      Console.RED + proof.owningTheorem.prettyGoal + Console.RESET + "\n" +
+        ProofPrinter.prettyProof(proof, 2) + "\n" +
+        "  " * (1 + proof.depth) + Console.RED + textline + Console.RESET + "\n\n" +
+        s"   Proof tactic ${tactic.name} used in.(${file.value.split("/").last.split("\\\\").last}:${line.value}) did not succeed:\n" +
+        "   " + errorMessage
+    }
+  }
+
+  class UnimplementedProof(val theorem: Library#THM)(using sourcecode.Line, sourcecode.File) extends UserLisaException("Unimplemented Theorem") {
+    def showError: String = s"Theorem ${theorem.name}"
+  }
+  case class UnexpectedProofTacticFailureException(failure: Library#Proof#InvalidProofTactic, errorMessage: String)(using sourcecode.Line, sourcecode.File)
+      extends lisa.utils.LisaException(errorMessage) {
+    def showError: String = "A proof tactic used in another proof tactic returned an unexpected error. This may indicate an implementation error in either of the two tactics.\n" +
+      "Status of the proof at time of the error is:" +
+      ProofPrinter.prettyProof(failure.proof)
+  }
+
+}