diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/prove.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/prove.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,121 @@
+
+abstract class Term
+case class Var(s: String) extends Term
+case class Fun(s: String, ts: List[Term]) extends Term
+
+
+abstract class Form
+object True extends Form
+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 Controls(p: String, f: Form) extends Form
+
+case class Judgement(Gamma: List[Form], F: Form) {
+  def lhs = Gamma
+  def rhs = F
+}
+
+val Alice = "Alice"
+val Bob = "Bob"
+val Send = Pred("Send", Nil)
+
+val Gamma = 
+  List( Imp(Says(Bob, Send), Send),
+        Says(Bob, Imp(Says(Alice, Send), Send)),
+        Says(Alice, Send) )
+
+val goal = Judgement(Gamma, Send)
+
+def sc () = { println ("Yes!") }
+
+class Main {
+
+def prove(j: Judgement, sc: () => Unit) : Unit = j match {
+  case Judgement(lhs, rhs) => 
+    { if (lhs.exists(f => f == rhs))  sc () 
+      else prove1(lhs, rhs, sc) 
+    }
+}
+
+def partitions [A] (l: List[A]): List[(A, List[A])]  = 
+  l.map (s => (s, l - 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, f) => prove(Judgement(lhs, f), sc)*/
+    /*case Controls(p, f) => prove(Judgement(lhs, f), 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 Imp(f1, f2) => 
+      prove(Judgement(lhs_rest, f1), 
+            () => 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 Controls(p, f) =>
+      prove(Judgement(lhs_rest, Says(p, f)),
+            () => prove(Judgement(f::lhs_rest, rhs), sc))
+    case _ => ()
+  }
+
+}
+  
+val main = new Main
+val Foo = Pred("Foo", Nil)
+
+main.prove (Judgement (Gamma, And(Foo, Send)), sc)
+main.prove (Judgement (Nil, Foo), sc)
+main.prove (Judgement (Nil, Imp(Send, Send)), sc)
+main.prove (Judgement (Gamma, Send), sc)
+main.prove (Judgement (Gamma, Foo), sc)
+
+val F1 = Imp(Says(Bob, Send), Send)
+val F2 = Says(Bob, Imp(Says(Alice, Send), Send))
+val F3 = Says(Alice, Send)
+
+main.prove (Judgement (Nil, Imp(F1, Imp(F2, Imp(F3, Send)))), sc)
+
+val Server = "Server"
+
+def Sends(p: String, q: String, f: Form) : Form =
+  Imp(Says(p, f), Says(q, f))
+
+def Enc(f: Form, k: Form) : Form = Imp(k, f)
+
+def Connect(p: String, q: String) : Form =
+  Pred("Connect", List(Var(p), Var(q)))
+
+val Msg = Pred("Msg", Nil)
+val Kas = Pred("Kas", Nil)
+val Kbs = Pred("Kbs", Nil)
+val Kab = Pred("Kab", Nil)
+
+val Gamma_big = 
+  List( Says(Alice, Kas),
+        Says(Bob, Kbs),
+        Says(Alice, Msg),
+        Says(Alice, Connect(Alice, Bob)),
+        Sends(Alice, Server, Connect(Alice, Bob)),
+        Says(Server, Imp(Connect(Alice, Bob), Enc(Kab, Kas))),
+        Says(Server, Imp(Connect(Alice, Bob), Enc(Enc(Kab, Kbs), Kas))),
+        Sends(Server, Alice, Enc(Kab, Kas)),
+        Sends(Server, Alice, Enc(Enc(Kab, Kbs), Kas)),
+        Sends(Alice, Bob, Enc(Kab, Kbs)),
+        Sends(Alice, Bob, Enc(Msg, Kab))
+      )
+
+
+main.prove (Judgement(Gamma_big, Says(Bob, Msg)), sc)