nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile

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
]