From 4ed56b013fd3e85937c32c6ab305c512ec4bde10 Mon Sep 17 00:00:00 2001 From: Mateusz Kowalczyk Date: Sat, 27 Sep 2014 03:23:22 +0100 Subject: [PATCH] agda-TotalParserCombinators: new package --- .../agda/TotalParserCombinators/contextfile | 213 ++++++++++++++++++ .../agda/TotalParserCombinators/default.nix | 25 ++ pkgs/top-level/all-packages.nix | 2 + 3 files changed, 240 insertions(+) create mode 100644 pkgs/development/libraries/agda/TotalParserCombinators/contextfile create mode 100644 pkgs/development/libraries/agda/TotalParserCombinators/default.nix diff --git a/pkgs/development/libraries/agda/TotalParserCombinators/contextfile b/pkgs/development/libraries/agda/TotalParserCombinators/contextfile new file mode 100644 index 000000000000..1d211f397af9 --- /dev/null +++ b/pkgs/development/libraries/agda/TotalParserCombinators/contextfile @@ -0,0 +1,213 @@ + +Context: + +[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 +] diff --git a/pkgs/development/libraries/agda/TotalParserCombinators/default.nix b/pkgs/development/libraries/agda/TotalParserCombinators/default.nix new file mode 100644 index 000000000000..6b0a63066b2f --- /dev/null +++ b/pkgs/development/libraries/agda/TotalParserCombinators/default.nix @@ -0,0 +1,25 @@ +{ stdenv, agda, fetchdarcs, AgdaStdlib }: + +agda.mkDerivation (self: rec { + version = "2014-09-27"; + name = "TotalParserCombinators-${version}"; + + src = fetchdarcs { + url = "http://www.cse.chalmers.se/~nad/repos/parser-combinators.code/"; + context = ./contextfile; + sha256 = "1rb8prqqp4dnz9s83ays7xfvpqs0n20vl1bg2zlg5si171j9rd4i"; + }; + + buildDepends = [ AgdaStdlib ]; + everythingFile = "TotalParserCombinators.agda"; + sourceDirectories = []; + topSourceDirectories = [ "../$sourceRoot" ]; + + meta = with stdenv.lib; { + homepage = "http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.html"; + description = "A monadic parser combinator library which guarantees termination of parsing"; + license = stdenv.lib.licenses.mit; + platforms = stdenv.lib.platforms.unix; + maintainers = with maintainers; [ fuuzetsu ]; + }; +}) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 6be18fea575b..ac8ab1830f8c 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -6801,6 +6801,8 @@ let categories = callPackage ../development/libraries/agda/categories {}; + TotalParserCombinators = callPackage ../development/libraries/agda/TotalParserCombinators {}; + ### DEVELOPMENT / LIBRARIES / JAVA atermjava = callPackage ../development/libraries/java/aterm {