mirror of
https://github.com/SebastianWendel/nixpkgs.git
synced 2024-09-20 20:39:04 +02:00
agda-TotalParserCombinators: new package
This commit is contained in:
Mateusz Kowalczyk
parent
4d2a3933a4
commit
4ed56b013f
|
|
@ -0,0 +1,213 @@
|
|||
|
||||
Context:
|
||||
|
||||
[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
|
||||
]
|
||||
|
|
@ -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 ];
|
||||
};
|
||||
})
|
||||
|
|
@ -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 {
|
||||
|
|
|
|||
Loading…
Reference in a new issue