Context: [Updated the code in response to changes to Agda. Nils Anders Danielsson **20150319181310 Ignore-this: 52b9ff613d7f10b0c8f45591a0759d07 ] [Rolled back most of "Updated the code in response to changes to Agda". Nils Anders Danielsson **20150319101420 Ignore-this: c2ea7bdf79848235fa3ea64ebda116eb * One of the Agda changes has been reverted. ] [Removed an outdated comment. Nils Anders Danielsson **20150217162945 Ignore-this: 3ff7732335750305fe220e65693f0cbf ] [Added the simplification "nonempty (return x) → fail". Nils Anders Danielsson **20150217161718 Ignore-this: 56ad6a68c314446d8986a8c1b49655d0 ] [Added Nonempty.nonempty-return. Nils Anders Danielsson **20150217161629 Ignore-this: 68829d3f9a248272c46848daa05ccfe3 ] [Updated the copyright year range. Nils Anders Danielsson **20150212154744 Ignore-this: 3410a12ca1f9de825b00e692b136d500 ] [Updated the code in response to changes to Agda. Nils Anders Danielsson **20150212152207 Ignore-this: 683b5eeca5fa9c8490bceaf68c23a204 ] [Updated the copyright year range. Nils Anders Danielsson **20141128223227 Ignore-this: 31d3f5e4fdd6fbfad9758d9bfd0d3a3e ] [Updated the code in response to changes to Agda and the library. Nils Anders Danielsson **20141128223205 Ignore-this: 6392ec67aab2c534a7195abed55be47 ] [Updated code to reflect changes to Agda. Nils Anders Danielsson **20140425121055 Ignore-this: 54d80fd647cb897eef85f57e9172f7db ] [Workaround for (possible) Agda bug. Nils Anders Danielsson **20140228200347 Ignore-this: b17884ad17a3bdb7faff678622365a8 ] [Updated code to reflect changes to library API. Nils Anders Danielsson **20130307134644 Ignore-this: 50d070a22a6796b9acdf19d44ba5de16 ] [Updated code to reflect changes to Agda and the library API. Nils Anders Danielsson **20130228122951 Ignore-this: 761dc4d85683a59cc3667a8706c88093 ] [Turned _◇_ into a constructor. Nils Anders Danielsson **20120316125431 Ignore-this: 41b492c3106a575f28f146253f78a5ae ] [Updated code to reflect changes to Agda. Nils Anders Danielsson **20120316125416 Ignore-this: e77d817d8b391c3b4806119d10848eb3 ] [Updated code to reflect changes to Agda. Nils Anders Danielsson **20120215103344 Ignore-this: 467716429d5553cd122722108ea82a08 ] [Modified a comment. Nils Anders Danielsson **20120215103319 Ignore-this: e57d4911f692f8a96a80017d910efc5f ] [Updated code to reflect change to library API. Nils Anders Danielsson **20111006160229 Ignore-this: 5359da54e7e6e0f92983fa3ecaccebf3 ] [Updated code to reflect changes to Agda and the library API. Nils Anders Danielsson **20111003170117 Ignore-this: cbdd35172e372779e12642985cf17268 ] [Rolled back addition of inversion lemmas. Nils Anders Danielsson **20110930150912 Ignore-this: 9c9b083f0afcf95aaaa55a01d871274e ] [Added inversion lemmas, implemented other lemmas using these lemmas. Nils Anders Danielsson **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 **20110517220158 Ignore-this: ea9771a5014a25cb20afc2118638f8b5 ] [Updated code to reflect changes to Agda. Nils Anders Danielsson **20110512124425 Ignore-this: 97b154661679f574f6ab914583b14580 ] [Proved that many constructions preserve various preorders. Nils Anders Danielsson **20110313012617 Ignore-this: 8008efaff967c228448baa33b82edb81 ] [Updated code to reflect changes to library API. Nils Anders Danielsson **20110313002106 Ignore-this: 94799ba1ae411e59fd8c6c7eac3b8dfb ] [Simplified TotalRecognisers.LeftRecursion.MatchingParentheses. Nils Anders Danielsson **20110118102159 Ignore-this: 1e01a8092b0c0124979ffc5fe17a245c ] [Added TotalRecognisers.LeftRecursion.MatchingParentheses. Nils Anders Danielsson **20110118102146 Ignore-this: 13a3bc91425364e26c3047561655bb25 ] [Added a simplifying backend. Nils Anders Danielsson **20101229012716 Ignore-this: 9ac7ae21cd44c099633678a994fb9a3 ] [Fixed another "bug" in the deep simplifier. Nils Anders Danielsson **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 **20101228235603 Ignore-this: d39b8453a15089126261e098080223c6 ] [Deep simplification no longer adds casts. Nils Anders Danielsson **20101228192850 Ignore-this: 2ba016825adfa3a1e36922869eabfd39 ] [The first constructor in a simplified parser can no longer be a cast. Nils Anders Danielsson **20101228175822 Ignore-this: ce3e38cc0b9a096aa436655c9013ae97 ] [Modified the outline. Nils Anders Danielsson **20101228173414 Ignore-this: f8866e69f6d1a344e79fb6f708dfa4c ] [Added an example: a right recursive expression grammar. Nils Anders Danielsson **20101228173159 Ignore-this: 9a4d732b451cca08ba19aac5d115c678 ] [Rearranged the code. Nils Anders Danielsson **20101228172209 Ignore-this: 50fa29406d0f150669ff3feec4dbe513 ] [Renamed same-bag/set to (initial-bag-)cong. Nils Anders Danielsson **20101228170706 Ignore-this: dd3ce43d77dde74cc2428d2568dd2d30 ] [Added TotalParserCombinators.Force. Nils Anders Danielsson **20101228153638 Ignore-this: 3b6ff6ea20df0c1293494f06845d17eb ] [Proved that uses of subst can be erased. Nils Anders Danielsson **20101228153621 Ignore-this: f503ba495b923ae521718b6957167128 ] [The deep simplifier no longer skips layers. Nils Anders Danielsson **20101228141138 Ignore-this: 733a4a4a9aa0f890ad1740ecfc6a599f ] [Documented that the deep simplifier misses every second layer. Nils Anders Danielsson **20101228121910 Ignore-this: 8a0baf25b12f63f8748dbc1d16affacf ] [The simplifier now applies the token-bind rule more often. Nils Anders Danielsson **20101227165413 Ignore-this: 40132fa6f19602886bbe29aadd8a683c ] [Switched back to deep simplification, now with a proper proof. Nils Anders Danielsson **20101227125434 Ignore-this: ccc46e82f6f9c6c2a27ddb43d315f7dd ] [Simplified the soundness proof. Nils Anders Danielsson **20101227123839 Ignore-this: fb6826dd9836e34fc3bfdce2928ba13d ] [Made some _≈[_]P_ constructors conditionally coinductive. Nils Anders Danielsson **20101227123827 Ignore-this: f521f70475403697229051b62343a080 + The structure of the soundness proof was also changed. ] [Unified And, AsymmetricChoice and Not. Nils Anders Danielsson **20101225103109 Ignore-this: 5ae8b80e1505fe6e707bb2307d22688c ] [Modified some comments. Nils Anders Danielsson **20101225101051 Ignore-this: e812d8c3e9720895c368f7a286f8315c ] [Modified a comment. Nils Anders Danielsson **20101223202647 Ignore-this: 16ea5dc01a4cbe0fe38714b2e4b7ff6 ] [Updated code to reflect changes to library API. Nils Anders Danielsson **20101107162658 Ignore-this: 9e38a10a9997c9825ece6ad9f871b673 ] [Added an alternative backend for TotalRecognisers.Simple. Nils Anders Danielsson **20101020183743 Ignore-this: a111a89e0c237e132b649561000f53d6 ] [TAG Code corresponding to the paper "Total Parser Combinators" (4). Nils Anders Danielsson **20100928013815 Ignore-this: 45ccc28373ed3974047315613eb14833 ]