diff options
Diffstat (limited to 'nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile')
| -rw-r--r-- | nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile | 259 |
1 files changed, 0 insertions, 259 deletions
diff --git a/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile b/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile deleted file mode 100644 index 46743cba3b67..000000000000 --- a/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile +++ /dev/null @@ -1,259 +0,0 @@ - -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 -] |