import scala.language.implicitConversions
import scala.language.reflectiveCalls
import scala.util._

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
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: Set[Form], f: Form) {
  def lhs = gamma
  def rhs = f
}

// some syntactic sugar
implicit def FormOps(f1: Form) = new {
  def -> (f2: Form) = Imp(f1, f2)
}
implicit def StringOps(p: String) = new {
  def says (f: Form) = Says(p, f)
}
implicit def SetFormOps(gamma: Set[Form]) = new {
  def |- (f: Form) : Judgement = Judgement(gamma, f)
}

val Admin = "Admin"
val Bob = "Bob"
val Del = Pred("del_file", Nil)

val Gamma: Set[Form] = 
  Set( (Admin says Del) -> Del,
       Admin says ((Bob says Del) -> Del),
       Bob says Del )

val goal = Gamma |- Del // request: provable or not?

def partitions[A](s: Set[A]): Set[(A, Set[A])]  = 
  s.map (e => (e, s - e))


def prove(j: Judgement, sc: () => Unit) : Unit = {
  if (j.lhs.contains(j.rhs))  sc ()   // Axiom rule 
  else { 
    prove1(j, sc);
    for ((f, lhs_rest) <- partitions(j.lhs)) prove2(f, lhs_rest, j.rhs, sc)
  }
}

def prove1(j: Judgement, sc: () => Unit) : Unit = 
  j.rhs match {
    case True => sc ()
    case False => ()
    case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
    case Says(p, f1) => prove(j.lhs |- f1, sc) 
    case Or(f1, f2) => 
      { prove(j.lhs |- f1, sc);
        prove(j.lhs |- f2, sc) }
    case And(f1, f2) => 
      prove(j.lhs |- f1, 
            () => prove(j.lhs |- f2, sc))
    case _ => ()
  }

def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = 
  f match {
    case True => prove(lhs_rest |- rhs, sc)
    case False => sc ()
    case And(f1, f2) =>
      prove(lhs_rest + f1 + f2 |- rhs, sc)
    case Imp(f1, f2) => 
      prove(lhs_rest |- f1, 
            () => prove(lhs_rest + f2 |- rhs, sc))
    case Or(f1, f2) => 
      prove(lhs_rest + f1 |- rhs, 
            () => prove(lhs_rest + f2 |- rhs, sc))
    case Says(p, Imp(f1, f2)) => 
      prove(lhs_rest |- Says(p, f1), 
            () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) 
    case _ => ()
  }

// function that calls prove and returns immediately once a proof is found
def run (j : Judgement) : Unit = {
  def sc () = { println ("Yes!"); throw new Exception }
  Try(prove(j, sc)) getOrElse ()
} 

run (goal)

run (Set[Form]() |- False -> Del)
run (Set[Form]() |- True -> Del)
run (Set[Form]() |- Del -> True)
run (Set[Form]() |- Del -> Del)
run (Set[Form]() |- Del -> Or(False, Del))


val Gamma1 : Set[Form] = 
  Set( Admin says ((Bob says Del) -> Del),
       Bob says Del )

val goal1 = Gamma1 |- Del // not provable
run (goal1)


val f1 = "P" says Pred("F1", Nil)
val f2 = "Q" says Pred("F2", Nil)
run (Set[Form](And(f1, f2)) |- And(f2, f1))


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 = (HoD says Chr_Staff) -> Chr_Staff
val Policy_Lib = And(Chr_Staff, AtLib) -> Email
val HoD_says = HoD says Chr_Staff

run (Set[Form](AtLib, Policy_HoD, Policy_Lib, HoD_says) |- Email)