259 lines
8.8 KiB
Text
259 lines
8.8 KiB
Text
|
|
Context:
|
|
|
|
[Updated the code in response to changes to Agda.
|
|
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150319181310
|
|
Ignore-this: 52b9ff613d7f10b0c8f45591a0759d07
|
|
]
|
|
|
|
[Rolled back most of "Updated the code in response to changes to Agda".
|
|
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150319101420
|
|
Ignore-this: c2ea7bdf79848235fa3ea64ebda116eb
|
|
* One of the Agda changes has been reverted.
|
|
]
|
|
|
|
[Removed an outdated comment.
|
|
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150217162945
|
|
Ignore-this: 3ff7732335750305fe220e65693f0cbf
|
|
]
|
|
|
|
[Added the simplification "nonempty (return x) → fail".
|
|
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150217161718
|
|
Ignore-this: 56ad6a68c314446d8986a8c1b49655d0
|
|
]
|
|
|
|
[Added Nonempty.nonempty-return.
|
|
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150217161629
|
|
Ignore-this: 68829d3f9a248272c46848daa05ccfe3
|
|
]
|
|
|
|
[Updated the copyright year range.
|
|
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150212154744
|
|
Ignore-this: 3410a12ca1f9de825b00e692b136d500
|
|
]
|
|
|
|
[Updated the code in response to changes to Agda.
|
|
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150212152207
|
|
Ignore-this: 683b5eeca5fa9c8490bceaf68c23a204
|
|
]
|
|
|
|
[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
|
|
]
|