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 Sends(p: String, q: String, f: Form) extends Form

case class Enc(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, Enc(f1, f2)) => 

      prove(j.lhs |- Says(p, f1), 

            () => prove(j.lhs |- Says(p, 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 Sends(p, q, f) => prove(j.lhs + (p says f) |- (q says f), 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 Sends(p, q, f) => 

      prove(lhs_rest |- (p says f), 

            () => prove(lhs_rest + (q says f) |- rhs, sc))

    case Enc(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, Enc(f1, f2)) => 

      prove(lhs_rest |- Says(p, f2), 

            () => prove(lhs_rest + Says(p, f1) |- 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_obtain_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) |- Email)

println("Server Example")

def Connect(p: String, q: String) : Form =

  Pred("Connect", List(Var(p), Var(q)))

val A = "A"

val B = "B"

val S = "S"

val CAB = Connect(A, B)

val Msg = Pred("Msg", Nil)

val KAS = Pred("Kas", Nil)

val KBS = Pred("Kbs", Nil)

val KAB = Pred("Kab", Nil)

val Gamma_big : Set[Form] = 

  Set( A says CAB,

       Sends(A, S, CAB), 

       S says (CAB -> Enc(KAB, KAS)),

       S says (CAB -> Enc(Enc(KAB, KBS), KAS)),

       Sends(S, A, Enc(KAB, KAS)),

       Sends(S, A, Enc(Enc(KAB, KBS), KAS)),

       Sends(A, B, Enc(KAB, KBS)),

       Sends(A, B, Enc(Msg, KAB)),

       A says KAS,

       B says KBS,

       S says KAS,

       A says (Enc(Msg, KAB))

     )

run (Gamma_big |- (B says Msg))