abstract class Term 

case class Var(s: String) extends Term 

case class Const(s: String) extends Term 

case class Fun(s: String, ts: List[Term]) extends Term

abstract class Form {

  def -> (that: Form) = Imp(this, that)

}

case object True extends Form

case object False extends Form

case class Pred(s: String, ts: List[Term]) extends Form

case class Imp(f1: Form, f2: Form) extends Form

case class Says(p: String, f: Form) extends Form 

case class And(f1: Form, f2: Form) extends Form 

case class Or(f1: Form, f2: Form) extends Form 

case class Judgement(Gamma: List[Form], F: Form) {

  def lhs = Gamma

  def rhs = F

}

val Admin = "Admin"

val Bob = "Bob"

val Del = Pred("del_file", Nil)

val Gamma = 

  List( Says(Admin, Del) -> Del,

        Says(Admin, Says(Bob, Del) -> Del),

        Says(Bob, Del) )

val goal = Judgement(Gamma, Del) // request: provable or not?

def partitions[A](ls: List[A]): List[(A, List[A])]  = 

  ls.map (s => (s, ls diff List(s)))

def prove(j: Judgement, sc: () => Unit) : Unit = {

  if (j.lhs.contains(j.rhs))  sc()   // Axiom rule 

  else prove1(j.lhs, j.rhs, sc) 

}

def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = 

  rhs match {

    case True => sc ()

    case False => ()

    case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) 

    case Says(p, f1) => prove(Judgement(lhs, f1), sc) 

    case Or(f1, f2) => 

      { prove(Judgement(lhs, f1), sc);

        prove(Judgement(lhs, f2), sc) }

    case And(f1, f2) => 

      prove(Judgement(lhs, f1), 

            () => prove(Judgement(lhs, f2), sc))

    case _ => { for ((f, lhs_rest) <- partitions(lhs))

                  prove2(f, lhs_rest, rhs, sc) }

  }

def prove2(f: Form, lhs_rest: List[Form], rhs: Form, sc: () => Unit) : Unit = 

  f match {

    case True => prove(Judgement(lhs_rest, rhs), sc)

    case False => sc()

    case And(f1, f2) =>

      prove(Judgement(f1::f2::lhs_rest, rhs), sc)

    case Imp(f1, f2) => 

      prove(Judgement(lhs_rest, f1), 

            () => prove(Judgement(f2::lhs_rest, rhs), sc))

    case Or(f1, f2) => 

      prove(Judgement(f1::lhs_rest, rhs), 

            () => prove(Judgement(f2::lhs_rest, rhs), sc))

    case Says(p, Imp(f1, f2)) => 

      prove(Judgement(lhs_rest, Says(p, f1)), 

            () => prove(Judgement(Says(p, f2)::lhs_rest, rhs), sc)) 

    case _ => ()

  }

// function that calls prove and returns immediately once a proof is found

def run (j : Judgement) : Unit = {

  try { 

    def sc () = { println ("Yes!"); throw new Exception }

    prove(j, sc) 

  }

  catch { case e: Exception => () }

} 

run (Judgement (Nil, False -> Del))

run (Judgement (Nil, True -> Del))

run (Judgement (Nil, Del -> True))

run (goal)

val Gamma1 = 

  List( Says(Admin, Says(Bob, Del) -> Del),

        Says(Bob, Del) )

val goal1 = Judgement(Gamma1, Del) // not provable

run (goal1)

run (Judgement(Nil, Del -> Del))

run (Judgement(Nil, Del -> Or(False, Del)))

val Chr = "Christian"

val HoD = "Peter"

val Email = Pred("may_btain_email", List(Const(Chr)))

val AtLib = Pred("is_at_library", List(Const(Chr)))

val Chr_Staff = Pred("is_staff", List(Const(Chr)))

val Policy_HoD = Says(HoD, Chr_Staff) -> Chr_Staff

val Policy_Lib = And(Chr_Staff, AtLib) -> Email

val HoD_says = Says(HoD, Chr_Staff)

run (Judgement (List(AtLib, Policy_HoD, Policy_Lib, HoD_says), Email))