nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile
Mateusz Kowalczyk d466b40bb3 agda-TotalParserCombinators: update darcs revision
Fixes the package for new Agda version
2014-12-03 17:13:48 +00:00

224 lines
7.5 KiB
Plaintext

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
]