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: 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( Imp(Says(Admin, Del), Del),
        Says(Admin, Imp(Says(Bob, Del), Del)),
        Says(Bob, Del) )

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

def prove(j: Judgement, sc: () => Unit) : Unit = {
  if (j.lhs.contains(j.rhs))  sc()   // Axiom rule 
  else prove1(j.lhs, j.rhs, sc) 
}

def partitions(ls: List[Form]): List[(Form, List[Form])]  = 
  ls.map (s => (s, ls - s))

def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = 
  rhs match {
    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 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 (goal)


run (Judgement(Nil, Imp(Del, Del)))

val Chr = "Christian"
val HoD = "Michael Luck"
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 = Imp(Says(HoD, Chr_Staff), Chr_Staff)
val Policy_Lib = Imp(And(Chr_Staff, AtLib), Email)
val HoD_says = Says(HoD, Chr_Staff)

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

// consider the cases for true and false