Finished proof checker, have to deal with definitions and beta reduti…

…ons.

lisa-kernel/src/main/scala/lisa/kernel/lambdafol/Syntax.scala

@@ -34,10 +34,31 @@ private[lambdafol] trait Syntax {
 
   sealed trait Type {
     def ->(to: Type): Arrow = Arrow(this, to)
+    val isFunctional: Boolean
+    val isPredicate: Boolean
+    val depth: Int 
   }
-  case object Term extends Type
-  case object Formula extends Type
-  sealed case class Arrow(from: Type, to: Type) extends Type
+  case object Term extends Type {
+    val isFunctional = true
+    val isPredicate = false
+    val depth = 0
+  }
+  case object Formula extends Type {
+    val isFunctional = false
+    val isPredicate = true
+    val depth = 0
+  }
+  sealed case class Arrow(from: Type, to: Type) extends Type {
+    val isFunctional = from == Term && to.isFunctional
+    val isPredicate = from == Term && to.isPredicate
+    val depth = 1+to.depth
+  }
+
+  def depth(t:Type): Int = t match {
+    case Arrow(a, b) => 1 + depth(b)
+    case _ => 0
+  }
+
 
   def legalApplication(typ1: Type, typ2: Type): Option[Type] = {
     typ1 match {
@@ -114,6 +135,7 @@ private[lambdafol] trait Syntax {
       case Application(Application(`equality`, arg1), arg2) => Some((arg1, arg2))
       case _ => None
     }
+    def apply(arg1: Expression, arg2: Expression): Expression = equality(arg1)(arg2)
   }
 
   object Neg {
@@ -135,6 +157,7 @@ private[lambdafol] trait Syntax {
       case Application(Application(`iff`, arg1), arg2) => Some((arg1, arg2))
       case _ => None
     }
+    def apply(arg1: Expression, arg2: Expression): Expression = iff(arg1)(arg2)
   }
   object And {
     def unapply (e: Expression): Option[(Expression, Expression)] = e match {

lisa-kernel/src/main/scala/lisa/kernel/lambdaproof/Judgement.scala

@@ -0,0 +1,76 @@
+package lisa.kernel.lambdaproof
+
+import lisa.kernel.lambdaproof.RunningTheory
+
+/**
+ * The judgement (or verdict) of a proof checking procedure.
+ * Typically, see [[SCProofChecker.checkSingleSCStep]] and [[SCProofChecker.checkSCProof]].
+ */
+sealed abstract class SCProofCheckerJudgement {
+  import SCProofCheckerJudgement._
+  val proof: SCProof
+
+  /**
+   * Whether this judgement is positive -- the proof is concluded to be valid;
+   * or negative -- the proof checker couldn't certify the validity of this proof.
+   * @return An instance of either [[SCValidProof]] or [[SCInvalidProof]]
+   */
+  def isValid: Boolean = this match {
+    case _: SCValidProof => true
+    case _: SCInvalidProof => false
+  }
+}
+
+object SCProofCheckerJudgement {
+
+  /**
+   * A positive judgement.
+   */
+  case class SCValidProof(proof: SCProof, val usesSorry: Boolean = false) extends SCProofCheckerJudgement
+
+  /**
+   * A negative judgement.
+   * @param path The path of the error, expressed as indices
+   * @param message The error message that hints about the first error encountered
+   */
+  case class SCInvalidProof(proof: SCProof, path: Seq[Int], message: String) extends SCProofCheckerJudgement
+}
+
+/**
+ * The judgement (or verdict) of a running theory.
+ */
+sealed abstract class RunningTheoryJudgement[+J <: RunningTheory#Justification] {
+  import RunningTheoryJudgement._
+
+  /**
+   * Whether this judgement is positive -- the justification could be imported into the running theory;
+   * or negative -- the justification is not suitable to be imported in the theory.
+   * @return An instance of either [[ValidJustification]] or [[InvalidJustification]]
+   */
+  def isValid: Boolean = this match {
+    case _: ValidJustification[_] => true
+    case _: InvalidJustification[_] => false
+  }
+  def get: J = this match {
+    case ValidJustification(just) => just
+    case InvalidJustification(message, error) =>
+      throw InvalidJustificationException(message, error)
+  }
+}
+
+object RunningTheoryJudgement {
+
+  /**
+   * A positive judgement.
+   */
+  case class ValidJustification[J <: RunningTheory#Justification](just: J) extends RunningTheoryJudgement[J]
+
+  /**
+   * A negative judgement.
+   * @param error If the justification is rejected because the proof is wrong, will contain the error in the proof.
+   * @param message The error message that hints about the first error encountered
+   */
+  case class InvalidJustification[J <: RunningTheory#Justification](message: String, error: Option[SCProofCheckerJudgement.SCInvalidProof]) extends RunningTheoryJudgement[J]
+
+  case class InvalidJustificationException(message: String, error: Option[SCProofCheckerJudgement.SCInvalidProof]) extends Exception(message)
+}