|
1 |
|
2 abstract class Term |
|
3 case class Var(s: String) extends Term |
|
4 case class Fun(s: String, ts: List[Term]) extends Term |
|
5 |
|
6 |
|
7 abstract class Form |
|
8 object True extends Form |
|
9 object False extends Form |
|
10 case class Pred(s: String, ts: List[Term]) extends Form |
|
11 case class Imp(f1: Form, f2: Form) extends Form |
|
12 case class Says(p: String, f: Form) extends Form |
|
13 case class And(f1: Form, f2: Form) extends Form |
|
14 case class Or(f1: Form, f2: Form) extends Form |
|
15 case class Controls(p: String, f: Form) extends Form |
|
16 |
|
17 case class Judgement(Gamma: List[Form], F: Form) { |
|
18 def lhs = Gamma |
|
19 def rhs = F |
|
20 } |
|
21 |
|
22 val Alice = "Alice" |
|
23 val Bob = "Bob" |
|
24 val Send = Pred("Send", Nil) |
|
25 |
|
26 val Gamma = |
|
27 List( Imp(Says(Bob, Send), Send), |
|
28 Says(Bob, Imp(Says(Alice, Send), Send)), |
|
29 Says(Alice, Send) ) |
|
30 |
|
31 val goal = Judgement(Gamma, Send) |
|
32 |
|
33 def sc () = { println ("Yes!") } |
|
34 |
|
35 class Main { |
|
36 |
|
37 def prove(j: Judgement, sc: () => Unit) : Unit = j match { |
|
38 case Judgement(lhs, rhs) => |
|
39 { if (lhs.exists(f => f == rhs)) sc () |
|
40 else prove1(lhs, rhs, sc) |
|
41 } |
|
42 } |
|
43 |
|
44 def partitions [A] (l: List[A]): List[(A, List[A])] = |
|
45 l.map (s => (s, l - s)) |
|
46 |
|
47 def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = |
|
48 rhs match { |
|
49 case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) |
|
50 /*case Says(p, f) => prove(Judgement(lhs, f), sc)*/ |
|
51 /*case Controls(p, f) => prove(Judgement(lhs, f), sc)*/ |
|
52 case Or(f1, f2) => { prove(Judgement(lhs, f1), sc); |
|
53 prove(Judgement(lhs, f2), sc) } |
|
54 case And(f1, f2) => prove(Judgement(lhs, f1), |
|
55 () => prove(Judgement(lhs, f2), sc)) |
|
56 case _ => { for ((f, lhs_rest) <- partitions(lhs)) |
|
57 prove2(f, lhs_rest, rhs, sc) } |
|
58 } |
|
59 |
|
60 def prove2(f: Form, lhs_rest: List[Form], rhs: Form, sc: () => Unit) : Unit = |
|
61 f match { |
|
62 case Imp(f1, f2) => |
|
63 prove(Judgement(lhs_rest, f1), |
|
64 () => prove(Judgement(f2::lhs_rest, rhs), sc)) |
|
65 case Says(p, Imp(f1, f2)) => |
|
66 prove(Judgement(lhs_rest, Says(p, f1)), |
|
67 () => prove(Judgement(Says(p, f2)::lhs_rest, rhs), sc)) |
|
68 case Controls(p, f) => |
|
69 prove(Judgement(lhs_rest, Says(p, f)), |
|
70 () => prove(Judgement(f::lhs_rest, rhs), sc)) |
|
71 case _ => () |
|
72 } |
|
73 |
|
74 } |
|
75 |
|
76 val main = new Main |
|
77 val Foo = Pred("Foo", Nil) |
|
78 |
|
79 main.prove (Judgement (Gamma, And(Foo, Send)), sc) |
|
80 main.prove (Judgement (Nil, Foo), sc) |
|
81 main.prove (Judgement (Nil, Imp(Send, Send)), sc) |
|
82 main.prove (Judgement (Gamma, Send), sc) |
|
83 main.prove (Judgement (Gamma, Foo), sc) |
|
84 |
|
85 val F1 = Imp(Says(Bob, Send), Send) |
|
86 val F2 = Says(Bob, Imp(Says(Alice, Send), Send)) |
|
87 val F3 = Says(Alice, Send) |
|
88 |
|
89 main.prove (Judgement (Nil, Imp(F1, Imp(F2, Imp(F3, Send)))), sc) |
|
90 |
|
91 val Server = "Server" |
|
92 |
|
93 def Sends(p: String, q: String, f: Form) : Form = |
|
94 Imp(Says(p, f), Says(q, f)) |
|
95 |
|
96 def Enc(f: Form, k: Form) : Form = Imp(k, f) |
|
97 |
|
98 def Connect(p: String, q: String) : Form = |
|
99 Pred("Connect", List(Var(p), Var(q))) |
|
100 |
|
101 val Msg = Pred("Msg", Nil) |
|
102 val Kas = Pred("Kas", Nil) |
|
103 val Kbs = Pred("Kbs", Nil) |
|
104 val Kab = Pred("Kab", Nil) |
|
105 |
|
106 val Gamma_big = |
|
107 List( Says(Alice, Kas), |
|
108 Says(Bob, Kbs), |
|
109 Says(Alice, Msg), |
|
110 Says(Alice, Connect(Alice, Bob)), |
|
111 Sends(Alice, Server, Connect(Alice, Bob)), |
|
112 Says(Server, Imp(Connect(Alice, Bob), Enc(Kab, Kas))), |
|
113 Says(Server, Imp(Connect(Alice, Bob), Enc(Enc(Kab, Kbs), Kas))), |
|
114 Sends(Server, Alice, Enc(Kab, Kas)), |
|
115 Sends(Server, Alice, Enc(Enc(Kab, Kbs), Kas)), |
|
116 Sends(Alice, Bob, Enc(Kab, Kbs)), |
|
117 Sends(Alice, Bob, Enc(Msg, Kab)) |
|
118 ) |
|
119 |
|
120 |
|
121 main.prove (Judgement(Gamma_big, Says(Bob, Msg)), sc) |