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, 259 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile b/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile new file mode 100644 index 000000000000..46743cba3b67 --- /dev/null +++ b/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile @@ -0,0 +1,259 @@ + +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 +] |