pristine:cd411b442e38b64dbabbf58129ba68c6fc6fd2b9a80950a856528116853500cf Starting with inventory: 0000002740-92fc69a8f26fc73d60fb36dde0a612f7abf7f4a9495fdb6fda38945b4f1aaac3 [TAG Code corresponding to the paper "Total Parser Combinators" (4). Nils Anders Danielsson **20100928013815 Ignore-this: 45ccc28373ed3974047315613eb14833 ] hash: 0000001933-6878dae609f276921234159cdcbdcdb0e5d9572d4360332af7fb8595e6df40a1 [Added an alternative backend for TotalRecognisers.Simple. Nils Anders Danielsson **20101020183743 Ignore-this: a111a89e0c237e132b649561000f53d6 ] hash: 0000005384-8e89a9eef9b514e17c5258606cd4da01c6a7cc13fcd5b570c40a13ea371856af [Updated code to reflect changes to library API. Nils Anders Danielsson **20101107162658 Ignore-this: 9e38a10a9997c9825ece6ad9f871b673 ] hash: 0000000572-196f098bd54bcd740ab10f7ccfd3ad497834e98eeca20257c164c1604a0777d6 [Modified a comment. Nils Anders Danielsson **20101223202647 Ignore-this: 16ea5dc01a4cbe0fe38714b2e4b7ff6 ] hash: 0000000311-d345c100cf6fa4eef9db0ced8f103eb6fe04e275ef7bb0875f21ce4580bb8ffb [Modified some comments. Nils Anders Danielsson **20101225101051 Ignore-this: e812d8c3e9720895c368f7a286f8315c ] hash: 0000000389-756bcc2475bc797c231f0d4b0cc145f2e6df3099b6e05d8a09cda6ddf1972c19 [Unified And, AsymmetricChoice and Not. Nils Anders Danielsson **20101225103109 Ignore-this: 5ae8b80e1505fe6e707bb2307d22688c ] hash: 0000031300-caf20590bb4d84e931da2d73e67d116c6d795755a4630391408b4ef098662bd8 [Made some _≈[_]P_ constructors conditionally coinductive. Nils Anders Danielsson **20101227123827 Ignore-this: f521f70475403697229051b62343a080 + The structure of the soundness proof was also changed. ] hash: 0000034446-4ee92ad48ef3cd538806bda9ce2e5d8d37a682103b5a9078ff752622483f0096 [Simplified the soundness proof. Nils Anders Danielsson **20101227123839 Ignore-this: fb6826dd9836e34fc3bfdce2928ba13d ] hash: 0000038039-0efefd099fc2db748c00908695ef2270ce36d0d61bccf14d37f1f4141de15124 [Switched back to deep simplification, now with a proper proof. Nils Anders Danielsson **20101227125434 Ignore-this: ccc46e82f6f9c6c2a27ddb43d315f7dd ] hash: 0000007001-c97badaec7ec26ffdb00dcd5cdcfbd34cf75e578ef3b91e781c8927a14a5c98e [The simplifier now applies the token-bind rule more often. Nils Anders Danielsson **20101227165413 Ignore-this: 40132fa6f19602886bbe29aadd8a683c ] hash: 0000008829-5ea50d7111f2cf201b6bcddcf57a45e3b76edbb99c3930267df2932b12b3724a [Documented that the deep simplifier misses every second layer. Nils Anders Danielsson **20101228121910 Ignore-this: 8a0baf25b12f63f8748dbc1d16affacf ] hash: 0000001029-5c3fff93d6d79938169f3795ae99855ef24f1ecc0415eb972ca89f6b0e529ec9 [The deep simplifier no longer skips layers. Nils Anders Danielsson **20101228141138 Ignore-this: 733a4a4a9aa0f890ad1740ecfc6a599f ] hash: 0000005823-b29e7be075f1cea835e99a0060d2ebf2bc626a0307a618f436ce6e4cf96eb6cf [Proved that uses of subst can be erased. Nils Anders Danielsson **20101228153621 Ignore-this: f503ba495b923ae521718b6957167128 ] hash: 0000002827-0a84c4e5f922fd93f749a843b691688168e0c5b738049dfbe63f0ae6efdf4bac [Added TotalParserCombinators.Force. Nils Anders Danielsson **20101228153638 Ignore-this: 3b6ff6ea20df0c1293494f06845d17eb ] hash: 0000004774-1e44eb654b5ede50cf59bd051d0bae1b08041671cd8338fe273c03a912194eba [Renamed same-bag/set to (initial-bag-)cong. Nils Anders Danielsson **20101228170706 Ignore-this: dd3ce43d77dde74cc2428d2568dd2d30 ] hash: 0000008399-644f79821ecb631893bcd1d1adaabae7b83a9ccc46a8e4b9edaed31763110fec [Rearranged the code. Nils Anders Danielsson **20101228172209 Ignore-this: 50fa29406d0f150669ff3feec4dbe513 ] hash: 0000052193-77ff5515211f5b5ce1a76374e595964fd3cc5d68caed07a9b7496916f52446f4 [Added an example: a right recursive expression grammar. Nils Anders Danielsson **20101228173159 Ignore-this: 9a4d732b451cca08ba19aac5d115c678 ] hash: 0000001899-392a8ac101eb61934dd7087a173f661e632be32c9c05ef0f7f138ffbec68bfc1 [Modified the outline. Nils Anders Danielsson **20101228173414 Ignore-this: f8866e69f6d1a344e79fb6f708dfa4c ] hash: 0000000900-6af4c646e5bc5554711eb3eb61f99b5e617fc6cbe4029c8631c3483ed5339ab3 [The first constructor in a simplified parser can no longer be a cast. Nils Anders Danielsson **20101228175822 Ignore-this: ce3e38cc0b9a096aa436655c9013ae97 ] hash: 0000007213-3ca1b8268a665ca9825151f7b6e16dced79b84d471997d50234c51cb220a890b [Deep simplification no longer adds casts. Nils Anders Danielsson **20101228192850 Ignore-this: 2ba016825adfa3a1e36922869eabfd39 ] hash: 0000005944-eb4dd5469c04081961288b7d566e34ce4477be3fb8f98d881554d5ea9eed8a33 [Made simplify₁ public and changed its type. Nils Anders Danielsson **20101228235603 Ignore-this: d39b8453a15089126261e098080223c6 ] hash: 0000014980-5d9e5eca28c86c4af7f170f19b5cf8b2a2e6144e040eff7f5e39a7836e26b4e3 [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. ] hash: 0000006469-5c81654e0c497079cd8d3b33ceed9aab05c71606c25514e72943bccc6afecc30 [Added a simplifying backend. Nils Anders Danielsson **20101229012716 Ignore-this: 9ac7ae21cd44c099633678a994fb9a3 ] hash: 0000009978-5ce8acf578de229e90b6d8c14256142373e201b54fa313d9ae3a3c8ba0d858f0 [Added TotalRecognisers.LeftRecursion.MatchingParentheses. Nils Anders Danielsson **20110118102146 Ignore-this: 13a3bc91425364e26c3047561655bb25 ] hash: 0000005089-21b91dc1ac496bc6602f7826d7218ff86963056762c47d54cf64043b1f8dea40 [Simplified TotalRecognisers.LeftRecursion.MatchingParentheses. Nils Anders Danielsson **20110118102159 Ignore-this: 1e01a8092b0c0124979ffc5fe17a245c ] hash: 0000006907-81e5ac62f6f436fb2d7dd833c8913695b985f916e4e2287614f17540e45c3377 [Updated code to reflect changes to library API. Nils Anders Danielsson **20110313002106 Ignore-this: 94799ba1ae411e59fd8c6c7eac3b8dfb ] hash: 0000039599-59142e7107de6ef9fb3fb48a2c6d090e42a493c0ef03bdac0f692ed182a66fac [Proved that many constructions preserve various preorders. Nils Anders Danielsson **20110313012617 Ignore-this: 8008efaff967c228448baa33b82edb81 ] hash: 0000017986-6916830ab2c6e29cdc17e069b847be3d1ed2870b78edc0fc847657a21ae4d236 [Updated code to reflect changes to Agda. Nils Anders Danielsson **20110512124425 Ignore-this: 97b154661679f574f6ab914583b14580 ] hash: 0000035830-69bc9ecc55758292aa2b3872b04d281e90ce05926a1abfd7593466ee3cd917b2 [Updated code to reflect changes to library API. Nils Anders Danielsson **20110517220158 Ignore-this: ea9771a5014a25cb20afc2118638f8b5 ] hash: 0000027989-552ee0354c59c301dd64fef90a4b3004bc8d8b7f6bc3e6aa1c70057ebe15747e [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. ] hash: 0000010585-3e3b2b0b82d47e095e9e45cf90130a8bb3d05ca900af0016ff316b74cd3734b0 [Rolled back addition of inversion lemmas. Nils Anders Danielsson **20110930150912 Ignore-this: 9c9b083f0afcf95aaaa55a01d871274e ] hash: 0000010384-b80006e6736b1b4c8cca3ed8fd61f393849b849dedae41d1b622c88dcc201b81 [Updated code to reflect changes to Agda and the library API. Nils Anders Danielsson **20111003170117 Ignore-this: cbdd35172e372779e12642985cf17268 ] hash: 0000008827-7ea0f2f33b420596b36c879a30aadaaf65d9646314ed6a53fa2a080b1b3b4063 [Updated code to reflect change to library API. Nils Anders Danielsson **20111006160229 Ignore-this: 5359da54e7e6e0f92983fa3ecaccebf3 ] hash: 0000020260-289a9bbd9f7db822bd6efda99dd907fe750a1cbff9bc6ff1c72e8d5b2596e784 [Modified a comment. Nils Anders Danielsson **20120215103319 Ignore-this: e57d4911f692f8a96a80017d910efc5f ] hash: 0000000330-32962c68cf06e206352e6c4115f0ea0fa0423968a47db2f17b899ca50e5fc95c [Updated code to reflect changes to Agda. Nils Anders Danielsson **20120215103344 Ignore-this: 467716429d5553cd122722108ea82a08 ] hash: 0000001230-089900321c219d3fdfdfcbb47eed5fc523fb8dc3fbd0c3022922338c95749198 [Updated code to reflect changes to Agda. Nils Anders Danielsson **20120316125416 Ignore-this: e77d817d8b391c3b4806119d10848eb3 ] hash: 0000005901-c1e539105bda39affc6a65e95f4646602e15ca409b608ec9045d3b4e5783620b [Turned _◇_ into a constructor. Nils Anders Danielsson **20120316125431 Ignore-this: 41b492c3106a575f28f146253f78a5ae ] hash: 0000000466-66b756aa9f1f4e5593a5b85234459f75bbfd3c356ebd158647bfdc712423ae03 [Updated code to reflect changes to Agda and the library API. Nils Anders Danielsson **20130228122951 Ignore-this: 761dc4d85683a59cc3667a8706c88093 ] hash: 0000002207-33b00ba6df6a5ff3c32524dbbea6054d6a60c8c49d21860fe9f8eb124fb02dcb