Rules

src/main/scala/com/melvic/chi/Parser.scala

@@ -3,6 +3,7 @@ package com.melvic.chi
 import com.melvic.chi.ast.Proof.Variable
 import com.melvic.chi.ast.Proposition._
 import com.melvic.chi.ast.{Proposition, Signature}
+import com.melvic.chi.out.Fault
 
 import scala.util.parsing.combinator._
 import scala.util.parsing.input.CharSequenceReader

src/main/scala/com/melvic/chi/ast/Proof.scala

@@ -10,6 +10,13 @@ object Proof {
   final case class Conjunction(components: List[Proof]) extends Proof
   final case class PRight(proof: Proof) extends Proof
   final case class PLeft(proof: Proof) extends Proof
+
+  /**
+    * A proof that utilizes both components, unlike what [[PRight]] and [[PLeft]] are for.
+    * Each component is a pair: the components name and the component itself.
+    */
+  final case class Disjunction(name: String, left: (String, Proof), right: (String, Proof)) extends Proof
+
   final case class Abstraction(domain: Proof, codomain: Proof) extends Proof
   final case class Application(functionName: String, params: List[Proof]) extends Proof
 
@@ -18,6 +25,8 @@ object Proof {
     val indent = level.map(singleIndent * _).getOrElse("")
     val nextLine = level.map(_ => "\n").getOrElse("")
     val nextLevel = level.map(_ + 1)
+    val bodyIndent = if (indent.nonEmpty) indent + singleIndent else singleIndent * 2
+
     val proofString = proof match {
       case TUnit             => "()"
       case Variable(name, _) => name
@@ -28,14 +37,18 @@ object Proof {
         "(" + nextLine + termsString + nextLine + indent + ")"
       case PRight(term) => s"Right(${Proof.show(term, None)})"
       case PLeft(term)  => s"Left(${Proof.show(term, None)})"
+      case Disjunction(name, (leftName, left), (rightName, right)) =>
+        val leftCase = s"case Left($leftName) => ${show(left, None)}"
+        val rightCase = s"case Right($rightName) => ${show(right, None)}"
+        s"$name match {\n${bodyIndent}$leftCase\n$bodyIndent$rightCase\n  }"
       case Abstraction(params: Conjunction, codomain) =>
-        val bodyIndent = if (indent.nonEmpty) indent + singleIndent else singleIndent * 2
         s"{ case ${show(params, None)} =>\n$bodyIndent${show(codomain, None)}\n  }"
       case Abstraction(domain, codomain) =>
         s"${Proof.show(domain, None)} => $nextLine${Proof.show(codomain, nextLevel)}"
       case Application(functionName, params) =>
         s"$functionName($nextLine${params.map(Proof.show(_, nextLevel)).mkString(", " + nextLine)}$nextLine$indent)"
     }
+
     s"$indent$proofString"
   }
 }

src/main/scala/com/melvic/chi/ast/Proposition.scala

@@ -27,7 +27,13 @@ object Proposition {
     */
   final case class Conjunction(components: List[Proposition]) extends Proposition
 
+  /**
+    * Logical disjunction. Note that we may also end up supporting a list of components, just
+    * like with conjunction, in the future (when adding support for languages that allow primitive
+    * union types)
+    */
   final case class Disjunction(left: Proposition, right: Proposition) extends Proposition
+
   final case class Implication(antecedent: Proposition, consequent: Proposition) extends Proposition
 
   def fold[A](proposition: Proposition, init: A)(f: (A, Atom) => A): A =

src/main/scala/com/melvic/chi/env/Environment.scala → src/main/scala/com/melvic/chi/env/Env.scala

@@ -4,31 +4,36 @@ import com.melvic.chi.ast.Proof.{TUnit, Variable}
 import com.melvic.chi.ast.Proposition._
 import com.melvic.chi.ast.{Proof, Proposition}
 
-object Environment {
+/**
+  * The set of assumptions and discharged formulae.
+  */
+final case class Env(proofs: List[Proof])
 
-  /**
-    * The set of assumptions and discharged formulae.
-    */
-  type Environment = List[Proof]
+object Env {
+  def default: Env = Env(List(TUnit))
 
-  def default: Environment = List(TUnit)
+  def fromList(proofs: List[Proof]): Env =
+    Env(proofs)
 
-  def fromList(list: List[Proof]): Environment = list ++ default
+  def fromListWithDefault(proofs: List[Proof]): Env =
+    fromList(proofs ++ Env.default.proofs)
 
-  def findAtom(atom: Atom)(implicit env: Environment): Option[Proof] =
-    env.find {
-      case Variable(_, `atom`)                 => true
-      case Variable(_, Implication(_, `atom`)) => true
-      case _                                   => false
-    }
+  def find(predicate: PartialFunction[Proof, Boolean])(implicit env: Env): Option[Proof] =
+    filter(predicate).headOption
+
+  def filter(predicate: PartialFunction[Proof, Boolean])(implicit env: Env): List[Proof] =
+    env.proofs.filter(predicate.orElse(_ => false))
+
+  def filterByConsequent(consequent: Proposition)(implicit env: Env): List[Proof] =
+    filter { case Variable(_, Implication(_, `consequent`)) => true }
 
-  def discharge(env: Environment, proof: Proof): Environment =
-    env.filterNot(_ == proof)
+  def without(proof: Proof)(implicit env: Env): Env =
+    fromList(env.proofs.filterNot(_ == proof))
 
   /**
     * Assigns a variable to the proposition and registers it into the environment
     */
-  def register(proposition: Proposition)(implicit env: Environment): (Proof, Environment) =
+  def register(proposition: Proposition)(implicit env: Env): (Proof, Env) =
     proposition match {
       case Atom(value) => registerSingle(value.toLowerCase.head.toString, proposition)
       case Conjunction(components) =>
@@ -43,20 +48,20 @@ object Environment {
     }
 
   def registerSingle(base: String, proposition: Proposition)(
-      implicit env: Environment
-  ): (Proof, Environment) = {
+      implicit env: Env
+  ): (Proof, Env) = {
     val variable = Variable(generateName(base), proposition)
-    (variable, variable :: env)
+    (variable, fromList(variable :: env.proofs))
   }
 
   /**
     * Generates a variable name
     * @param base the base or root name of the variable
     * @param count used as a suffix to distinguish variables with the same base
     */
-  private def generateName(base: String, count: Int = 0)(implicit env: Environment): String = {
+  private def generateName(base: String, count: Int = 0)(implicit env: Env): String = {
     val name = base + (if (count == 0) "" else count.toString)
-    val nameOpt = env.find {
+    val nameOpt = env.proofs.find {
       case Variable(`name`, _) => true
       case _                   => false
     }

src/main/scala/com/melvic/chi/eval/Evaluate.scala

@@ -0,0 +1,76 @@
+package com.melvic.chi.eval
+
+import com.melvic.chi.Parser
+import com.melvic.chi.ast.Proof.{PLeft, PRight, TUnit, Variable}
+import com.melvic.chi.ast.Proposition._
+import com.melvic.chi.ast.{Definition, Proof, Proposition, Signature}
+import com.melvic.chi.env.Env
+import com.melvic.chi.out.Fault.UnknownPropositions
+import com.melvic.chi.out.Result.Result
+import com.melvic.chi.out.{Fault, Result}
+
+object Evaluate {
+  //noinspection SpellCheckingInspection
+  def proposition(proposition: Proposition)(implicit env: Env): Result[Proof] =
+    proposition match {
+      case PUnit                    => Result.success(TUnit)
+      case atom: Atom               => deduce(atom)
+      case Conjunction(components) => Rule.conjunctionIntroduction(components)
+      case Disjunction(left, right) =>
+        Evaluate
+          .proposition(left)
+          .map(PLeft)
+          .orElse(Evaluate.proposition(right).map(PRight))
+      case Implication(antecedent, consequent) => Rule.implicationIntroduction(antecedent, consequent)
+    }
+
+  def signature(signature: Signature): Result[Definition] = {
+    val Signature(name, typeParams, params, proposition) = signature
+
+    val unknownTypes = Proposition.filter(proposition) {
+      case PUnit => false
+      case atom =>
+        !typeParams.map(Identifier).contains(atom)
+    }
+
+    if (unknownTypes.nonEmpty) Result.fail(UnknownPropositions(unknownTypes))
+    else
+      Evaluate
+        .proposition(proposition)(Env.fromListWithDefault(params))
+        .map(Definition(signature, _))
+  }
+
+  def signatureString(functionCode: String): Result[Definition] =
+    Parser.parseSignature(functionCode).flatMap(Evaluate.signature)
+
+  def deduce(atom: Atom)(implicit env: Env): Result[Proof] =
+    Rule
+      .assumption(atom)
+      .orElse(deduceImplication(atom))
+      .orElse(deduceConjunction(atom))
+
+  def deduceImplication(atom: Atom)(implicit env: Env): Result[Proof] = {
+    val implicationOpt = Env.filterByConsequent(atom).headOption
+    implicationOpt
+      .toRight(Fault.cannotProve(atom))
+      .flatMap {
+        case variable @ Variable(functionName, Implication(antecedent, _)) =>
+          val newEnv = Env.without(variable)
+          Evaluate
+            .proposition(antecedent)(newEnv)
+            .map(Rule.implicationElimination(functionName, _))
+            .orElse(deduce(atom)(newEnv))
+      }
+  }
+
+  def deduceConjunction(atom: Atom)(implicit env: Env): Result[Proof] = {
+    val disjunctionOpt = Env.find {
+      case Variable(_, _: Disjunction) => true
+    }
+    disjunctionOpt.toRight(Fault.cannotProve(atom))
+      .flatMap {
+        case variable @ Variable(name, disjunction: Disjunction) =>
+          Rule.disjunctionElimination(name, disjunction, atom)(Env.without(variable))
+      }
+  }
+}