blob: 1c195ee97fa4884baa17532532edbabd5a0e4334 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
|
Context:
[Updated the copyright year range.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20141128223227
Ignore-this: 31d3f5e4fdd6fbfad9758d9bfd0d3a3e
]
[Updated the code in response to changes to Agda and the library.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20141128223205
Ignore-this: 6392ec67aab2c534a7195abed55be47
]
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20140425121055
Ignore-this: 54d80fd647cb897eef85f57e9172f7db
]
[Workaround for (possible) Agda bug.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20140228200347
Ignore-this: b17884ad17a3bdb7faff678622365a8
]
[Updated code to reflect changes to library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20130307134644
Ignore-this: 50d070a22a6796b9acdf19d44ba5de16
]
[Updated code to reflect changes to Agda and the library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20130228122951
Ignore-this: 761dc4d85683a59cc3667a8706c88093
]
[Turned _◇_ into a constructor.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120316125431
Ignore-this: 41b492c3106a575f28f146253f78a5ae
]
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120316125416
Ignore-this: e77d817d8b391c3b4806119d10848eb3
]
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120215103344
Ignore-this: 467716429d5553cd122722108ea82a08
]
[Modified a comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120215103319
Ignore-this: e57d4911f692f8a96a80017d910efc5f
]
[Updated code to reflect change to library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20111006160229
Ignore-this: 5359da54e7e6e0f92983fa3ecaccebf3
]
[Updated code to reflect changes to Agda and the library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20111003170117
Ignore-this: cbdd35172e372779e12642985cf17268
]
[Rolled back addition of inversion lemmas.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110930150912
Ignore-this: 9c9b083f0afcf95aaaa55a01d871274e
]
[Added inversion lemmas, implemented other lemmas using these lemmas.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110930150842
Ignore-this: 19b832c3f9e14d1e713b5911c094a130
+ This change was a response to a change to Agda's pattern matching
machinery. Subsequently the machinery was made more liberal again,
making this change unnecessary.
]
[Updated code to reflect changes to library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110517220158
Ignore-this: ea9771a5014a25cb20afc2118638f8b5
]
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110512124425
Ignore-this: 97b154661679f574f6ab914583b14580
]
[Proved that many constructions preserve various preorders.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110313012617
Ignore-this: 8008efaff967c228448baa33b82edb81
]
[Updated code to reflect changes to library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110313002106
Ignore-this: 94799ba1ae411e59fd8c6c7eac3b8dfb
]
[Simplified TotalRecognisers.LeftRecursion.MatchingParentheses.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110118102159
Ignore-this: 1e01a8092b0c0124979ffc5fe17a245c
]
[Added TotalRecognisers.LeftRecursion.MatchingParentheses.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110118102146
Ignore-this: 13a3bc91425364e26c3047561655bb25
]
[Added a simplifying backend.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101229012716
Ignore-this: 9ac7ae21cd44c099633678a994fb9a3
]
[Fixed another "bug" in the deep simplifier.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101229010854
Ignore-this: e258adf963436ef715242db23c6808e
+ Sometimes the first layer of bind's right-hand argument was not
simplified.
]
[Made simplify₁ public and changed its type.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228235603
Ignore-this: d39b8453a15089126261e098080223c6
]
[Deep simplification no longer adds casts.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228192850
Ignore-this: 2ba016825adfa3a1e36922869eabfd39
]
[The first constructor in a simplified parser can no longer be a cast.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228175822
Ignore-this: ce3e38cc0b9a096aa436655c9013ae97
]
[Modified the outline.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228173414
Ignore-this: f8866e69f6d1a344e79fb6f708dfa4c
]
[Added an example: a right recursive expression grammar.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228173159
Ignore-this: 9a4d732b451cca08ba19aac5d115c678
]
[Rearranged the code.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228172209
Ignore-this: 50fa29406d0f150669ff3feec4dbe513
]
[Renamed same-bag/set to (initial-bag-)cong.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228170706
Ignore-this: dd3ce43d77dde74cc2428d2568dd2d30
]
[Added TotalParserCombinators.Force.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228153638
Ignore-this: 3b6ff6ea20df0c1293494f06845d17eb
]
[Proved that uses of subst can be erased.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228153621
Ignore-this: f503ba495b923ae521718b6957167128
]
[The deep simplifier no longer skips layers.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228141138
Ignore-this: 733a4a4a9aa0f890ad1740ecfc6a599f
]
[Documented that the deep simplifier misses every second layer.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228121910
Ignore-this: 8a0baf25b12f63f8748dbc1d16affacf
]
[The simplifier now applies the token-bind rule more often.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227165413
Ignore-this: 40132fa6f19602886bbe29aadd8a683c
]
[Switched back to deep simplification, now with a proper proof.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227125434
Ignore-this: ccc46e82f6f9c6c2a27ddb43d315f7dd
]
[Simplified the soundness proof.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227123839
Ignore-this: fb6826dd9836e34fc3bfdce2928ba13d
]
[Made some _≈[_]P_ constructors conditionally coinductive.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227123827
Ignore-this: f521f70475403697229051b62343a080
+ The structure of the soundness proof was also changed.
]
[Unified And, AsymmetricChoice and Not.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101225103109
Ignore-this: 5ae8b80e1505fe6e707bb2307d22688c
]
[Modified some comments.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101225101051
Ignore-this: e812d8c3e9720895c368f7a286f8315c
]
[Modified a comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101223202647
Ignore-this: 16ea5dc01a4cbe0fe38714b2e4b7ff6
]
[Updated code to reflect changes to library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101107162658
Ignore-this: 9e38a10a9997c9825ece6ad9f871b673
]
[Added an alternative backend for TotalRecognisers.Simple.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101020183743
Ignore-this: a111a89e0c237e132b649561000f53d6
]
[TAG Code corresponding to the paper "Total Parser Combinators" (4).
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100928013815
Ignore-this: 45ccc28373ed3974047315613eb14833
]
|