author | Christian Urban <christian.urban@kcl.ac.uk> |
Wed, 23 Mar 2022 00:09:08 +0000 | |
changeset 463 | 421397f267b9 |
parent 312 | 8b0b414e71b0 |
permissions | -rw-r--r-- |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
import scala.language.implicitConversions |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
import scala.language.reflectiveCalls |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
import scala.annotation.tailrec |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
abstract class Rexp |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
6 |
case object ZERO extends Rexp |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
7 |
case object ONE extends Rexp |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
case class CHAR(c: Char) extends Rexp |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
case class ALT(r1: Rexp, r2: Rexp) extends Rexp |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
case class SEQ(r1: Rexp, r2: Rexp) extends Rexp |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
case class STAR(r: Rexp) extends Rexp |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
case class RECD(x: String, r: Rexp) extends Rexp |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
abstract class Val |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
15 |
case object Empty extends Val |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
case class Chr(c: Char) extends Val |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
case class Sequ(v1: Val, v2: Val) extends Val |
13
62fe79ee2726
fixed the scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
18 |
case class Left(v: Val) extends Val |
62fe79ee2726
fixed the scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
19 |
case class Right(v: Val) extends Val |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
case class Stars(vs: List[Val]) extends Val |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
case class Rec(x: String, v: Val) extends Val |
312
8b0b414e71b0
added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents:
211
diff
changeset
|
22 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
// some convenience for typing in regular expressions |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
def charlist2rexp(s : List[Char]): Rexp = s match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
26 |
case Nil => ONE |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
case c::Nil => CHAR(c) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
case c::s => SEQ(CHAR(c), charlist2rexp(s)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
implicit def string2rexp(s : String) : Rexp = charlist2rexp(s.toList) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
implicit def RexpOps(r: Rexp) = new { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
def | (s: Rexp) = ALT(r, s) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
def % = STAR(r) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
def ~ (s: Rexp) = SEQ(r, s) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
implicit def stringOps(s: String) = new { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
def | (r: Rexp) = ALT(s, r) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
def | (r: String) = ALT(s, r) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
def % = STAR(s) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
def ~ (r: Rexp) = SEQ(s, r) |
81
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
43 |
def ~ (r: String) = SEQ(s, r) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
def $ (r: Rexp) = RECD(s, r) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
|
62
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
47 |
def pretty(r: Rexp) : String = r match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
48 |
case ZERO => "0" |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
49 |
case ONE => "e" |
62
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
50 |
case CHAR(c) => c.toString |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
51 |
case ALT(r1, r2) => "(" ++ pretty(r1) ++ " | " + pretty(r2) ++ ")" |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
52 |
case SEQ(r1, r2) => pretty(r1) ++ pretty(r2) |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
53 |
case STAR(r) => "(" ++ pretty(r) ++ ")*" |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
54 |
case RECD(x, r) => "(" ++ x ++ " : " ++ pretty(r) ++ ")" |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
55 |
} |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
56 |
|
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
57 |
def vpretty(v: Val) : String = v match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
58 |
case Empty => "()" |
62
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
59 |
case Chr(c) => c.toString |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
60 |
case Left(v) => "Left(" ++ vpretty(v) ++ ")" |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
61 |
case Right(v) => "Right(" ++ vpretty(v) ++ ")" |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
62 |
case Sequ(v1, v2) => vpretty(v1) ++ " ~ " ++ vpretty(v2) |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
63 |
case Stars(vs) => vs.flatMap(vpretty).mkString("[", ",", "]") |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
64 |
case Rec(x, v) => "(" ++ x ++ ":" ++ vpretty(v) ++ ")" |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
65 |
} |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
66 |
|
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
67 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
68 |
// size of a regular expressions - for testing purposes |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
69 |
def size(r: Rexp) : Int = r match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
70 |
case ZERO => 1 |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
71 |
case ONE => 1 |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
72 |
case CHAR(_) => 1 |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
73 |
case ALT(r1, r2) => 1 + size(r1) + size(r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
74 |
case SEQ(r1, r2) => 1 + size(r1) + size(r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
75 |
case STAR(r) => 1 + size(r) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
76 |
case RECD(_, r) => 1 + size(r) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
77 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
78 |
|
48
652861c9473f
added a function for calculating values
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
41
diff
changeset
|
79 |
// extracts a set of candidate values from a "non-starred" regular expression |
652861c9473f
added a function for calculating values
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
41
diff
changeset
|
80 |
def values(r: Rexp) : Set[Val] = r match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
81 |
case ZERO => Set() |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
82 |
case ONE => Set(Empty) |
48
652861c9473f
added a function for calculating values
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
41
diff
changeset
|
83 |
case CHAR(c) => Set(Chr(c)) |
62
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
84 |
case ALT(r1, r2) => (for (v1 <- values(r1)) yield Left(v1)) ++ |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
85 |
(for (v2 <- values(r2)) yield Right(v2)) |
48
652861c9473f
added a function for calculating values
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
41
diff
changeset
|
86 |
case SEQ(r1, r2) => for (v1 <- values(r1); v2 <- values(r2)) yield Sequ(v1, v2) |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
87 |
case STAR(r) => Set(Empty) ++ values(r) // to do more would cause the set to be infinite |
48
652861c9473f
added a function for calculating values
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
41
diff
changeset
|
88 |
case RECD(_, r) => values(r) |
652861c9473f
added a function for calculating values
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
41
diff
changeset
|
89 |
} |
652861c9473f
added a function for calculating values
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
41
diff
changeset
|
90 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
91 |
// zeroable function: tests whether the regular |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
92 |
// expression cannot regognise any string |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
93 |
def zeroable (r: Rexp) : Boolean = r match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
94 |
case ZERO => true |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
95 |
case ONE => false |
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
96 |
case CHAR(_) => false |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
97 |
case ALT(r1, r2) => zeroable(r1) && zeroable(r2) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
98 |
case SEQ(r1, r2) => zeroable(r1) || zeroable(r2) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
99 |
case STAR(_) => false |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
100 |
case RECD(_, r1) => zeroable(r1) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
101 |
} |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
102 |
|
34
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
103 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
104 |
// nullable function: tests whether the regular |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
105 |
// expression can recognise the empty string |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
106 |
def nullable (r: Rexp) : Boolean = r match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
107 |
case ZERO => false |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
108 |
case ONE => true |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
109 |
case CHAR(_) => false |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
110 |
case ALT(r1, r2) => nullable(r1) || nullable(r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
111 |
case SEQ(r1, r2) => nullable(r1) && nullable(r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
112 |
case STAR(_) => true |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
113 |
case RECD(_, r1) => nullable(r1) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
114 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
115 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
116 |
// derivative of a regular expression w.r.t. a character |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
117 |
def der (c: Char, r: Rexp) : Rexp = r match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
118 |
case ZERO => ZERO |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
119 |
case ONE => ZERO |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
120 |
case CHAR(d) => if (c == d) ONE else ZERO |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
121 |
case ALT(r1, r2) => ALT(der(c, r1), der(c, r2)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
122 |
case SEQ(r1, r2) => |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
123 |
if (nullable(r1)) ALT(SEQ(der(c, r1), r2), der(c, r2)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
124 |
else SEQ(der(c, r1), r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
125 |
case STAR(r) => SEQ(der(c, r), STAR(r)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
126 |
case RECD(_, r1) => der(c, r1) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
127 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
128 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
129 |
// derivative w.r.t. a string (iterates der) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
130 |
def ders (s: List[Char], r: Rexp) : Rexp = s match { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
131 |
case Nil => r |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
132 |
case c::s => ders(s, der(c, r)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
133 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
134 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
135 |
// extracts a string from value |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
136 |
def flatten(v: Val) : String = v match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
137 |
case Empty => "" |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
138 |
case Chr(c) => c.toString |
13
62fe79ee2726
fixed the scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
139 |
case Left(v) => flatten(v) |
62fe79ee2726
fixed the scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
140 |
case Right(v) => flatten(v) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
141 |
case Sequ(v1, v2) => flatten(v1) + flatten(v2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
142 |
case Stars(vs) => vs.map(flatten).mkString |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
143 |
case Rec(_, v) => flatten(v) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
144 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
145 |
|
77
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
146 |
def flattens(v: Val) : List[String] = v match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
147 |
case Empty => List("") |
77
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
148 |
case Chr(c) => List(c.toString) |
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
149 |
case Left(v) => flattens(v) |
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
150 |
case Right(v) => flattens(v) |
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
151 |
case Sequ(v1, v2) => flattens(v1) ::: flattens(v2) |
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
152 |
case Stars(vs) => vs.flatMap(flattens) |
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
153 |
case Rec(_, v) => flattens(v) |
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
154 |
} |
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
155 |
|
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
156 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
157 |
// extracts an environment from a value |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
158 |
def env(v: Val) : List[(String, String)] = v match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
159 |
case Empty => Nil |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
160 |
case Chr(c) => Nil |
13
62fe79ee2726
fixed the scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
161 |
case Left(v) => env(v) |
62fe79ee2726
fixed the scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
162 |
case Right(v) => env(v) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
163 |
case Sequ(v1, v2) => env(v1) ::: env(v2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
164 |
case Stars(vs) => vs.flatMap(env) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
165 |
case Rec(x, v) => (x, flatten(v))::env(v) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
166 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
167 |
|
48
652861c9473f
added a function for calculating values
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
41
diff
changeset
|
168 |
// injection part |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
169 |
def mkeps(r: Rexp) : Val = r match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
170 |
case ONE => Empty |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
171 |
case ALT(r1, r2) => |
13
62fe79ee2726
fixed the scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
172 |
if (nullable(r1)) Left(mkeps(r1)) else Right(mkeps(r2)) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
173 |
case SEQ(r1, r2) => Sequ(mkeps(r1), mkeps(r2)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
174 |
case STAR(r) => Stars(Nil) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
175 |
case RECD(x, r) => Rec(x, mkeps(r)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
176 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
177 |
|
34
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
178 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
179 |
def inj(r: Rexp, c: Char, v: Val) : Val = (r, v) match { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
180 |
case (STAR(r), Sequ(v1, Stars(vs))) => Stars(inj(r, c, v1)::vs) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
181 |
case (SEQ(r1, r2), Sequ(v1, v2)) => Sequ(inj(r1, c, v1), v2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
182 |
case (SEQ(r1, r2), Left(Sequ(v1, v2))) => Sequ(inj(r1, c, v1), v2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
183 |
case (SEQ(r1, r2), Right(v2)) => Sequ(mkeps(r1), inj(r2, c, v2)) |
13
62fe79ee2726
fixed the scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
184 |
case (ALT(r1, r2), Left(v1)) => Left(inj(r1, c, v1)) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
185 |
case (ALT(r1, r2), Right(v2)) => Right(inj(r2, c, v2)) |
211
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
186 |
case (CHAR(d), Empty) => Chr(d) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
187 |
case (RECD(x, r1), _) => Rec(x, inj(r1, c, v)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
188 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
189 |
|
211
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
190 |
def prj(r: Rexp, c: Char, v: Val) : Val = (r, v) match { |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
191 |
case (STAR(r), Sequ(v1, Stars(vs))) => Stars(prj(r, c, v1)::vs) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
192 |
case (SEQ(r1, r2), Sequ(v1, v2)) => |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
193 |
if (flatten(v1) == "") Right(prj(r2, c, v2)) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
194 |
else { if (nullable(r1)) Left(Sequ(prj(r1, c, v1), v2)) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
195 |
else Sequ(prj(r1, c, v1), v2) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
196 |
} |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
197 |
case (ALT(r1, r2), Left(v1)) => Left(prj(r1, c, v1)) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
198 |
case (ALT(r1, r2), Right(v2)) => Right(prj(r2, c, v2)) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
199 |
case (CHAR(d), _) => Empty |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
200 |
case (RECD(x, r1), _) => Rec(x, prj(r1, c, v)) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
201 |
} |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
202 |
|
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
203 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
204 |
// main lexing function (produces a value) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
205 |
def lex(r: Rexp, s: List[Char]) : Val = s match { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
206 |
case Nil => if (nullable(r)) mkeps(r) else throw new Exception("Not matched") |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
207 |
case c::cs => inj(r, c, lex(der(c, r), cs)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
208 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
209 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
210 |
def lexing(r: Rexp, s: String) : Val = lex(r, s.toList) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
211 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
212 |
|
34
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
213 |
|
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
214 |
// some "rectification" functions for simplification |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
215 |
def F_ID(v: Val): Val = v |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
216 |
def F_RIGHT(f: Val => Val) = (v:Val) => Right(f(v)) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
217 |
def F_LEFT(f: Val => Val) = (v:Val) => Left(f(v)) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
218 |
def F_ALT(f1: Val => Val, f2: Val => Val) = (v:Val) => v match { |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
219 |
case Right(v) => Right(f2(v)) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
220 |
case Left(v) => Left(f1(v)) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
221 |
} |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
222 |
def F_SEQ(f1: Val => Val, f2: Val => Val) = (v:Val) => v match { |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
223 |
case Sequ(v1, v2) => Sequ(f1(v1), f2(v2)) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
224 |
} |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
225 |
def F_SEQ_Empty1(f1: Val => Val, f2: Val => Val) = (v:Val) => Sequ(f1(Empty), f2(v)) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
226 |
def F_SEQ_Empty2(f1: Val => Val, f2: Val => Val) = (v:Val) => Sequ(f1(v), f2(Empty)) |
34
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
227 |
def F_RECD(f: Val => Val) = (v:Val) => v match { |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
228 |
case Rec(x, v) => Rec(x, f(v)) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
229 |
} |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
230 |
def F_ERROR(v: Val): Val = throw new Exception("error") |
13
62fe79ee2726
fixed the scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
231 |
|
34
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
232 |
// simplification of regular expressions returning also an |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
233 |
// rectification function; no simplification under STAR |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
234 |
def simp(r: Rexp): (Rexp, Val => Val) = r match { |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
235 |
case ALT(r1, r2) => { |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
236 |
val (r1s, f1s) = simp(r1) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
237 |
val (r2s, f2s) = simp(r2) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
238 |
(r1s, r2s) match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
239 |
case (ZERO, _) => (r2s, F_RIGHT(f2s)) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
240 |
case (_, ZERO) => (r1s, F_LEFT(f1s)) |
34
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
241 |
case _ => if (r1s == r2s) (r1s, F_LEFT(f1s)) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
242 |
else (ALT (r1s, r2s), F_ALT(f1s, f2s)) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
243 |
} |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
244 |
} |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
245 |
case SEQ(r1, r2) => { |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
246 |
val (r1s, f1s) = simp(r1) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
247 |
val (r2s, f2s) = simp(r2) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
248 |
(r1s, r2s) match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
249 |
case (ZERO, _) => (ZERO, F_ERROR) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
250 |
case (_, ZERO) => (ZERO, F_ERROR) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
251 |
case (ONE, _) => (r2s, F_SEQ_Empty1(f1s, f2s)) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
252 |
case (_, ONE) => (r1s, F_SEQ_Empty2(f1s, f2s)) |
34
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
253 |
case _ => (SEQ(r1s,r2s), F_SEQ(f1s, f2s)) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
254 |
} |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
255 |
} |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
256 |
case RECD(x, r1) => { |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
257 |
val (r1s, f1s) = simp(r1) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
258 |
(RECD(x, r1s), F_RECD(f1s)) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
259 |
} |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
260 |
case r => (r, F_ID) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
261 |
} |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
262 |
|
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
263 |
def lex_simp(r: Rexp, s: List[Char]) : Val = s match { |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
264 |
case Nil => if (nullable(r)) mkeps(r) else throw new Exception("Not matched") |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
265 |
case c::cs => { |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
266 |
val (r_simp, f_simp) = simp(der(c, r)) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
267 |
inj(r, c, f_simp(lex_simp(r_simp, cs))) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
268 |
} |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
269 |
} |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
270 |
|
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
271 |
def lexing_simp(r: Rexp, s: String) : Val = lex_simp(r, s.toList) |
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
13
diff
changeset
|
272 |
|
211
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
273 |
lexing(("a" | "ab") ~ ("b" | ""), "ab") |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
274 |
lexing_simp(("a" | "ab") ~ ("b" | ""), "ab") |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
275 |
|
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
276 |
|
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
277 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
278 |
// brute force search infrastructure |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
279 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
280 |
// enumerates regular expressions until a certain depth |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
281 |
def enum(n: Int, s: String) : Set[Rexp] = n match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
282 |
case 0 => Set(ZERO, ONE) ++ s.toSet.map(CHAR) |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
283 |
case n => { |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
284 |
val rs = enum(n - 1, s) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
285 |
rs ++ |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
286 |
(for (r1 <- rs; r2 <- rs) yield ALT(r1, r2)) ++ |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
287 |
(for (r1 <- rs; r2 <- rs) yield SEQ(r1, r2)) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
288 |
} |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
289 |
} |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
290 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
291 |
def ordr(v1: Val, r: Rexp, v2: Val) : Boolean = (v1, r, v2) match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
292 |
case (Empty, ONE, Empty) => true |
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
293 |
case (Chr(c1), CHAR(c2), Chr(c3)) if (c1 == c2 && c1 == c3) => true |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
294 |
case (Left(v1), ALT(r1, r2), Left(v2)) => ordr(v1, r1, v2) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
295 |
case (Right(v1), ALT(r1, r2), Right(v2)) => ordr(v1, r2, v2) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
296 |
case (Left(v1), ALT(r1, r2), Right(v2)) => flatten(v2).length <= flatten(v1).length |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
297 |
case (Right(v1), ALT(r1, r2), Left(v2)) => flatten(v2).length < flatten(v1).length |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
298 |
case (Sequ(v1, v2), SEQ(r1, r2), Sequ(v3, v4)) if (v1 == v3) => ordr(v2, r2, v4) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
299 |
case (Sequ(v1, v2), SEQ(r1, r2), Sequ(v3, v4)) if (v1 != v3) => ordr(v1, r1, v3) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
300 |
case _ => false |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
301 |
} |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
302 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
303 |
def ord(v1: Val, v2: Val) : Boolean = (v1, v2) match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
304 |
case (Empty, Empty) => true |
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
305 |
case (Chr(c1), Chr(c2)) if (c1 == c2) => true |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
306 |
case (Left(v1), Left(v2)) => ord(v1, v2) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
307 |
case (Right(v1), Right(v2)) => ord(v1, v2) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
308 |
case (Left(v1), Right(v2)) => flatten(v2).length <= flatten(v1).length |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
309 |
case (Right(v1), Left(v2)) => flatten(v2).length < flatten(v1).length |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
310 |
case (Sequ(v1, v2), Sequ(v3, v4)) if (v1 == v3) => ord(v2, v4) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
311 |
case (Sequ(v1, v2), Sequ(v3, v4)) if (v1 != v3) => ord(v1, v3) |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
312 |
case _ => false |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
313 |
} |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
314 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
315 |
// exhaustively tests values of a regular expression |
211
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
316 |
def vfilter1(f: Rexp => Val => Boolean)(r: Rexp) : Set[(Rexp, Val)] = { |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
317 |
val vs = values(r) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
318 |
for (v <- vs; if (f(r)(v))) yield (r, v) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
319 |
} |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
320 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
321 |
def vfilter2(f: Rexp => Val => Val => Boolean)(r: Rexp) : Set[(Rexp, Val, Val)] = { |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
322 |
val vs = values(r) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
323 |
for (v1 <- vs; v2 <- vs; if (f(r)(v1)(v2))) yield (r, v1, v2) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
324 |
} |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
325 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
326 |
def vfilter3(f: Rexp => Val => Val => Val => Boolean)(r: Rexp) : Set[(Rexp, Val, Val, Val)] = { |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
327 |
val vs = values(r) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
328 |
for (v1 <- vs; v2 <- vs; v3 <- vs; if (f(r)(v1)(v2)(v3))) yield (r, v1, v2, v3) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
329 |
} |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
330 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
331 |
// number of test cases |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
332 |
enum(3, "a").size |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
333 |
enum(2, "ab").size |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
334 |
enum(2, "abc").size |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
335 |
//enum(3, "ab").size |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
336 |
|
211
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
337 |
// test for inj/prj |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
338 |
def injprj_test(r:Rexp)(v:Val) : Boolean = |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
339 |
if (flatten(v) != "") (inj(r, 'a', prj(r, 'a', v)) != v) else false |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
340 |
|
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
341 |
val injprj_tst = enum(2, "ab").flatMap(vfilter1(injprj_test)) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
342 |
val injprj_smallest = injprj_tst.toList.sortWith { (x,y) => size(x._1) < size(y._1) }.head |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
343 |
|
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
344 |
prj(CHAR('b'), 'a', Chr('b')) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
345 |
inj(CHAR('b'), 'a', Empty) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
346 |
|
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
347 |
prj(SEQ(ALT(ONE,ONE),CHAR('a')), 'a', Sequ(Right(Empty),Chr('a'))) |
0fa636821349
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
348 |
inj(SEQ(ALT(ONE,ONE),CHAR('a')), 'a', Right(Empty)) |
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
349 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
350 |
// tests for totality |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
351 |
def totality_test(r: Rexp)(v1: Val)(v2: Val) : Boolean = |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
352 |
!(ord(v1, v2) || ord(v2, v1)) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
353 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
354 |
enum(2, "ab").flatMap(vfilter2(totality_test)) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
355 |
enum(3, "a").flatMap(vfilter2(totality_test)) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
356 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
357 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
358 |
//tests for transitivity (simple transitivity fails) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
359 |
def transitivity_test(r: Rexp)(v1: Val)(v2: Val)(v3: Val) : Boolean = |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
360 |
ord(v1, v2) && ord(v2, v3) && !ord(v1, v3) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
361 |
|
81
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
362 |
val test0 = enum(3, "a").flatMap(vfilter3(transitivity_test)) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
363 |
val test0_smallest = test0.toList.sortWith { (x,y) => size(x._1) < size(y._1) }.head |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
364 |
|
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
365 |
pretty(test0_smallest._1) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
366 |
vpretty(test0_smallest._2) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
367 |
vpretty(test0_smallest._3) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
368 |
vpretty(test0_smallest._4) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
369 |
|
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
370 |
/* Counter example for simple transitivity: |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
371 |
|
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
372 |
r = a | ((a | a)(a | e)) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
373 |
|
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
374 |
v1 = Left(a) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
375 |
v2 = Right(Left(a) ~ Right(())) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
376 |
v3 = Right(Right(a) ~ Left(a)) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
377 |
|
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
378 |
*/ |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
379 |
|
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
380 |
def is_seq(v: Val) : Boolean = v match { |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
381 |
case Seq(_, _) => true |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
382 |
case _ => false |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
383 |
} |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
384 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
385 |
def transitivity_test_extended(r: Rexp)(v1: Val)(v2: Val)(v3: Val) : Boolean = { |
81
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
386 |
//flatten(v1).size >= flatten(v2).size && |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
387 |
//flatten(v2).size >= flatten(v3).size && |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
388 |
is_seq(v1) && |
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
389 |
ord(v1, v2) && ord(v2, v3) && !ord(v1, v3) |
77
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
390 |
} |
4b4c677501e7
proved some basic properties (totality and trichonomity) for the orderings
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
75
diff
changeset
|
391 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
392 |
// smallest(?) example where simple transitivity fails |
81
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
393 |
val test1 = enum(3, "a").flatMap(vfilter3(transitivity_test_extended)) |
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
394 |
val test1_smallest = test1.toList.sortWith { (x,y) => size(x._1) < size(y._1) }.head |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
395 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
396 |
pretty(test1_smallest._1) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
397 |
vpretty(test1_smallest._2) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
398 |
vpretty(test1_smallest._3) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
399 |
vpretty(test1_smallest._4) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
400 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
401 |
ord(test1_smallest._2, test1_smallest._3) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
402 |
ord(test1_smallest._3, test1_smallest._4) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
403 |
ord(test1_smallest._2, test1_smallest._4) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
404 |
ordr(test1_smallest._3, test1_smallest._1, test1_smallest._4) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
405 |
|
81
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
406 |
/* Counter example for extended transitivity: |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
407 |
|
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
408 |
r = ((e | e)(e | a)) | a |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
409 |
|
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
410 |
v1 = Left(Right(()) ~ Right(a)) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
411 |
v2 = Right(a) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
412 |
v3 = Left(Left(()) ~ Left(())) |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
413 |
|
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
414 |
*/ |
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
415 |
|
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
416 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
417 |
// with flatten test |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
418 |
enum(3, "a").flatMap(vfilter3(transitivity_test_extended)) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
419 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
420 |
//injection tests |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
421 |
def injection_test(r: Rexp)(c: Char)(v1: Val)(v2: Val) : Boolean = { |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
422 |
v1 != v2 && |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
423 |
ord(v1, v2) && |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
424 |
ord(inj(r, c, v2), inj(r, c, v1)) && |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
425 |
flatten(v1) == flatten(v2) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
426 |
} |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
427 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
428 |
def injection_testA(r: Rexp)(c: Char)(v1: Val)(v2: Val) : Boolean = { |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
429 |
v1 != v2 && |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
430 |
ord(v1, v2) && |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
431 |
ord(inj(r, c, v2), inj(r, c, v1)) && |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
432 |
flatten(v1).length == flatten(v2).length |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
433 |
} |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
434 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
435 |
def injection_test2(r: Rexp)(c: Char)(v1: Val)(v2: Val) : Boolean = { |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
436 |
v1 != v2 && |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
437 |
ord(v1, v2) && |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
438 |
ord(inj(r, c, v2), inj(r, c, v1)) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
439 |
} |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
440 |
def vfilter4(f: Rexp => Char => Val => Val => Boolean)(c: Char)(r: Rexp) : Set[(Rexp, Rexp, Val, Val)] = { |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
441 |
val r_der = der(c, r) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
442 |
val vs = values(r_der) |
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
443 |
for (v1 <- vs; v2 <- vs; if (f(r)(c)(v1)(v2))) yield (r, r_der, v1, v2) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
444 |
} |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
445 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
446 |
enum(3, "a").flatMap(vfilter4(injection_test)('a')) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
447 |
enum(3, "a").flatMap(vfilter4(injection_testA)('a')) |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
448 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
449 |
val test2 = enum(3, "a").flatMap(vfilter4(injection_test2)('a')) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
450 |
val test2_smallest = test2.toList.sortWith { (x,y) => size(x._1) < size(y._1) }.head |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
451 |
|
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
452 |
pretty(test2_smallest._1) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
453 |
pretty(test2_smallest._2) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
454 |
vpretty(test2_smallest._3) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
455 |
vpretty(test2_smallest._4) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
456 |
vpretty(inj(test2_smallest._1, 'a', test2_smallest._3)) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
457 |
vpretty(inj(test2_smallest._1, 'a', test2_smallest._4)) |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
458 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
459 |
// Lexing Rules for a Small While Language |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
460 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
461 |
def PLUS(r: Rexp) = r ~ r.% |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
462 |
val SYM = "a" | "b" | "c" | "d" | "e" | "f" | "g" | "h" | "i" | "j" | "k" | "l" | "m" | "n" | "o" | "p" | "q" | "r" | "s" | "t" | "u" | "v" | "w" | "x" | "y" | "z" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
463 |
val DIGIT = "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
464 |
val ID = SYM ~ (SYM | DIGIT).% |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
465 |
val NUM = PLUS(DIGIT) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
466 |
val KEYWORD : Rexp = "skip" | "while" | "do" | "if" | "then" | "else" | "read" | "write" | "true" | "false" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
467 |
val SEMI: Rexp = ";" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
468 |
val OP: Rexp = ":=" | "==" | "-" | "+" | "*" | "!=" | "<" | ">" | "<=" | ">=" | "%" | "/" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
469 |
val WHITESPACE = PLUS(" " | "\n" | "\t") |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
470 |
val RPAREN: Rexp = ")" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
471 |
val LPAREN: Rexp = "(" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
472 |
val BEGIN: Rexp = "{" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
473 |
val END: Rexp = "}" |
41
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
474 |
val STRING: Rexp = "\"" ~ SYM.% ~ "\"" |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
475 |
|
38
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
476 |
|
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
477 |
val WHILE_REGS = (("k" $ KEYWORD) | |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
478 |
("i" $ ID) | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
479 |
("o" $ OP) | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
480 |
("n" $ NUM) | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
481 |
("s" $ SEMI) | |
41
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
482 |
("str" $ STRING) | |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
483 |
("p" $ (LPAREN | RPAREN)) | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
484 |
("b" $ (BEGIN | END)) | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
485 |
("w" $ WHITESPACE)).% |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
486 |
|
38
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
487 |
/* |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
488 |
val WHILE_REGS = (KEYWORD | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
489 |
ID | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
490 |
OP | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
491 |
NUM | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
492 |
SEMI | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
493 |
LPAREN | RPAREN | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
494 |
BEGIN | END | |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
495 |
WHITESPACE).% |
38
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
496 |
*/ |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
497 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
498 |
// Some Tests |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
499 |
//============ |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
500 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
501 |
def time[T](code: => T) = { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
502 |
val start = System.nanoTime() |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
503 |
val result = code |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
504 |
val end = System.nanoTime() |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
505 |
println((end - start)/1.0e9) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
506 |
result |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
507 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
508 |
|
49
c616ec6b1e3c
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
48
diff
changeset
|
509 |
val r1 = ("a" | "ab") ~ ("bcd" | "c") |
c616ec6b1e3c
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
48
diff
changeset
|
510 |
println(lexing(r1, "abcd")) |
c616ec6b1e3c
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
48
diff
changeset
|
511 |
println(values(r1).mkString("\n")) |
c616ec6b1e3c
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
48
diff
changeset
|
512 |
println(values(r1).map(flatten).mkString("\n")) |
c616ec6b1e3c
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
48
diff
changeset
|
513 |
|
c616ec6b1e3c
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
48
diff
changeset
|
514 |
val r2 = ("" | "a") ~ ("ab" | "b") |
c616ec6b1e3c
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
48
diff
changeset
|
515 |
println(lexing(r2, "ab")) |
c616ec6b1e3c
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
48
diff
changeset
|
516 |
println(values(r2).mkString("\n")) |
c616ec6b1e3c
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
48
diff
changeset
|
517 |
println(values(r2).toList.map(flatten).mkString("\n")) |
c616ec6b1e3c
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
48
diff
changeset
|
518 |
|
62
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
519 |
//Some experiments |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
520 |
//================ |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
521 |
|
66
eb97e8361211
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
62
diff
changeset
|
522 |
val f0 = ("ab" | "b" | "cb") |
eb97e8361211
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
62
diff
changeset
|
523 |
val f1 = der('a', f0) |
eb97e8361211
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
62
diff
changeset
|
524 |
val f2 = der('b', f1) |
eb97e8361211
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
62
diff
changeset
|
525 |
val g2 = mkeps(f2) |
eb97e8361211
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
62
diff
changeset
|
526 |
val g1 = inj(f1, 'b', g2) |
eb97e8361211
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
62
diff
changeset
|
527 |
val g0 = inj(f0, 'a', g1) |
eb97e8361211
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
62
diff
changeset
|
528 |
|
eb97e8361211
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
62
diff
changeset
|
529 |
lex((("" | "a") ~ ("ab" | "b")), "ab".toList) |
eb97e8361211
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
62
diff
changeset
|
530 |
lex((("" | "a") ~ ("b" | "ab")), "ab".toList) |
eb97e8361211
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
62
diff
changeset
|
531 |
lex((("" | "a") ~ ("c" | "ab")), "ab".toList) |
eb97e8361211
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
62
diff
changeset
|
532 |
|
62
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
533 |
val reg0 = ("" | "a") ~ ("ab" | "b") |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
534 |
val reg1 = der('a', reg0) |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
535 |
val reg2 = der('b', reg1) |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
536 |
println(List(reg0, reg1, reg2).map(pretty).mkString("\n")) |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
537 |
println(lexing(reg0, "ab")) |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
538 |
|
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
539 |
val val0 = values(reg0) |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
540 |
val val1 = values(reg1) |
a6bb0152ccc2
updated some rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
49
diff
changeset
|
541 |
val val2 = values(reg2) |
49
c616ec6b1e3c
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
48
diff
changeset
|
542 |
|
48
652861c9473f
added a function for calculating values
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
41
diff
changeset
|
543 |
|
38
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
544 |
// Two Simple Tests |
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
545 |
//=================== |
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
546 |
println("prog0 test") |
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
547 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
548 |
val prog0 = """read n""" |
38
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
549 |
println(env(lexing_simp(WHILE_REGS, prog0))) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
550 |
|
38
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
551 |
println("prog1 test") |
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
552 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
553 |
val prog1 = """read n; write (n)""" |
38
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
554 |
println(env(lexing_simp(WHILE_REGS, prog1))) |
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
555 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
556 |
|
38
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
557 |
// Big Test |
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
558 |
//========== |
41
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
559 |
/* |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
560 |
val prog2 = """ |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
561 |
i := 2; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
562 |
max := 100; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
563 |
while i < max do { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
564 |
isprime := 1; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
565 |
j := 2; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
566 |
while (j * j) <= i + 1 do { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
567 |
if i % j == 0 then isprime := 0 else skip; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
568 |
j := j + 1 |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
569 |
}; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
570 |
if isprime == 1 then write i else skip; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
571 |
i := i + 1 |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
572 |
}""" |
41
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
573 |
*/ |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
574 |
val prog2 = """ |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
575 |
write "fib"; |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
576 |
read n; |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
577 |
minus1 := 0; |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
578 |
minus2 := 1; |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
579 |
while n > 0 do { |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
580 |
temp := minus2; |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
581 |
minus2 := minus1 + minus2; |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
582 |
minus1 := temp; |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
583 |
n := n - 1 |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
584 |
}; |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
585 |
write "result"; |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
586 |
write minus2 |
4f8a9ed0f26d
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
38
diff
changeset
|
587 |
""" |
38
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
588 |
|
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
589 |
println("Tokens") |
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
590 |
println(env(lexing_simp(WHILE_REGS, prog2))) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
591 |
|
38
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
592 |
for (i <- 1 to 80) { |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
593 |
print(i.toString + ": ") |
38
b48939cca0cf
slightly polished the scala file re.scala
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
34
diff
changeset
|
594 |
time(lexing_simp(WHILE_REGS, prog2 * i)) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
595 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
596 |
|
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
597 |
|
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
598 |
val a0 = (ONE | "a") ~ (ONE | "ab") |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
599 |
val a1 = der('a', a0) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
600 |
pretty(a1) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
601 |
val m = mkeps(a1) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
602 |
vpretty(m) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
603 |
val v = inj(a0, 'a', m) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
604 |
vpretty(v) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
605 |
|
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
606 |
val a0 = (ONE | "a") ~ (ONE | "ab") |
74
dfa9dbb8f8e6
updated from the session today
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
73
diff
changeset
|
607 |
val a1 = der('a', a0) |
73
6e035162345a
solved one case
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
66
diff
changeset
|
608 |
pretty(a1) |
74
dfa9dbb8f8e6
updated from the session today
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
73
diff
changeset
|
609 |
values(a1).toList |
dfa9dbb8f8e6
updated from the session today
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
73
diff
changeset
|
610 |
val List(u2,_,u1) = values(a1).toList |
dfa9dbb8f8e6
updated from the session today
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
73
diff
changeset
|
611 |
vpretty(u1) |
dfa9dbb8f8e6
updated from the session today
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
73
diff
changeset
|
612 |
vpretty(u2) |
dfa9dbb8f8e6
updated from the session today
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
73
diff
changeset
|
613 |
vpretty(inj(a0,'a',u1)) |
dfa9dbb8f8e6
updated from the session today
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
73
diff
changeset
|
614 |
vpretty(inj(a0,'a',u2)) |
73
6e035162345a
solved one case
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
66
diff
changeset
|
615 |
|
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
616 |
lexing(a0, "ab") |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
617 |
val aa = der('a', a0) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
618 |
pretty(aa) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
619 |
val ab = der('b', aa) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
620 |
pretty(ab) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
621 |
nullable(ab) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
622 |
val m = mkeps(ab) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
623 |
vpretty(m) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
624 |
val vb = inj(aa, 'b', m) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
625 |
vpretty(vb) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
626 |
val va = inj(a0, 'a', vb) |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
627 |
vpretty(va) |
78
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
628 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
629 |
|
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
630 |
/* ord is not transitive in general: counter-example |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
631 |
* |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
632 |
* (1) Left(Right(Right(()))) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
633 |
* (2) Right(Left(()) ~ Left(())) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
634 |
* (3) Right(Right(()) ~ Right(a)) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
635 |
* |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
636 |
* (1) > (2); (2) > (3) but not (1) > (3) |
279d0bc48308
updated the Isabelle theories with the totality proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
77
diff
changeset
|
637 |
*/ |