pristine:3faad318e0c151dbe399f009ab0e17d2b55caf4c87e76545275b31ca08976947 Starting with inventory: 0000240793-b42f3840f018fbe42cd6dafdc21d8417cb563bf0bdb63e9c69678d0b1cc266b1 [TAG 2.3.2 andreas.abel@ifi.lmu.de**20121112002455 Ignore-this: 47f901c8b3f0c10c935a645e75cef8da ] hash: 0000168554-a2538a309c7b45f1194151a536627bcfe0249c45648e7352993f861ff3b82f50 [Bumped version number to 2.3.3. andreas.abel@ifi.lmu.de**20121112013740 Ignore-this: c9d622fe77a8ad4c2339cf538b2e5776 ] hash: 0000000513-03bcc9615a85afdc3f9db1120411bf5803b9c104579ed844b07b681a96d974bc [Removed unnecessary GADTs pragma. Andrés Sicard-Ramírez **20121110162146 Ignore-this: df35bc750050539f74e34ff2ac6da28a ] hash: 0000000363-538812a76f721937338156fe1d3279b8676c95b78f813f7d2e7b0859cf9658ca [Restored -Werror in Agda.cabal (disabled for release). Andreas Abel **20121112020236 Ignore-this: 7db1b446424ebf593ca557ddb29ee91c ] hash: 0000000335-9474973d49ccf1c2b0f8d45df6d9a7ffee165e62cd2ad25ebeab70e57bf3179e [Release notes stub for Version 2.3.4. Andreas Abel **20121112020941 Ignore-this: 701ca09fa212c2d8ef58bef3a4884c9e ] hash: 0000000734-e1bf3272106bff410b69fbf9c0834fbc8c5d9efdf9b603a3347bfa8889c922ac [Exclude mtl-2.1. It is severly bugged. Andreas Abel **20121113160958 Ignore-this: 3c48faf3942573b4896f7f3b9291ed1e Agda will just <> if you install it in a system with mtl-2.1. Can you spot the bug in mtl-2.1? state :: (s -> (a, s)) -> m a state f = do s <- get let ~(a, s) = f s put s return a modify :: MonadState s m => (s -> s) -> m () modify f = state (\s -> ((), f s)) I wonder how this passed the testsuite of Eward (which testsuite?). Another instance of the reason why recursive-by-default let is harmful... ] hash: 0000000774-2c341eabf13fe0e9fcb38ad25ef5287151c0084f59784374edef68c24183fd0e [Fixed issue 754 (internal error due to ill-formed sparse matrices). Andreas Abel **20121113185126 Ignore-this: 859f0996e9420e128c0e83bf1eedbf2b Supremum and infinium of two different-shaped matrices now implemented. ] hash: 0000006444-e06137932462870758400a8b7b49a1ce10de3e2e2d455a692327e73b5dfd4e21 [Complain if private is used without effect. (Issue 760.) Andreas Abel **20121117165850 Ignore-this: 863d7e2afc9bf2df1487522d74475df0 ] hash: 0000010910-4e88de71a3cef8fc23ab5d4126bc1111bf447b4e3df11f1ce2f036f1f29e821d [Removed unused IsAbstract field from NiceModuleMacro. Andreas Abel **20121117234357 Ignore-this: 5a13106fe51449555ec86ea3d92ed929 ] hash: 0000002942-6ad0a5fee39ec55739949bae0e42e9e9fd60a979d0fffd2dbb1b66ff01aab5a6 [Fixed issue 755. Polarity info should not be available for abstract definitions. Andreas Abel **20121118155500 Ignore-this: 493d0bb5bb7ee5204c48b5c8d32f3460 ] hash: 0000002637-d635616ad6339bdf2265af7add9343bf929283c6496b75cc129863b7d7f9ce46 [A debug printout for checking declarations. Andreas Abel **20121118155610 Ignore-this: fe04b1abacc35b508da1886f6cad1bad ] hash: 0000000302-6092ccef816bd29b407131ee0a49228becdbc6c243daf68b1964e0893389018d [Added sym and trans to test/Common.Equality. Andreas Abel **20121118160538 Ignore-this: 6028da6dbf3c1f367c6eb814bdbefe15 ] hash: 0000003613-0d860e2c4be6a0b86c1a019fa0b43117639193430361b3ca355fe384a09f29d2 [A use of unless. Andreas Abel **20121118160738 Ignore-this: 90e19045647b84629f158cd969bb1594 ] hash: 0000000262-55d6fae5b5648abca789eca3309bd7d9088335d7fcd973bb2ce93a9a209a321c [Moved notInScope to Base. Andreas Abel **20121118164525 Ignore-this: b5dd9606a65df1c002bff9dbd6a7fe8c ] hash: 0000000987-90f94cd2d17fdc7ebd177bb3b82722e52a3fdd0a43591bd328144979785279f9 [Fixed eta-contraction for abstract record values (see issue 759). Andreas Abel **20121118185013 Ignore-this: 88dc8767504acd455c69b90020617098 ] hash: 0000002868-2e1ca60c3544c1fbe9a6e4557f5fbec6ce0e52a96346bab28a3a22f160387501 [Single out verbosity levels 0 and 1. (Attempt to optimize reportS). Andreas Abel **20121118204756 Ignore-this: 2544751089256efab78b6263410b074a ] hash: 0000002188-5eefbce41bbde8850291cad58b351efb09034c039ed3fbf4c26dafefd0ec272d [Deactivated debug messages in eta contractions. Andreas Abel **20121118205039 Ignore-this: 3551f2e60a4c6a6be230757879043655 Seems to save 5% on std-lib. ] hash: 0000000897-5a27a4bb62136132bc05eef5690005498fde5ff90cb13b6ae469bf9b4ff68532 [Rolled back special verbosity for 0 and 1. (Did not perform better.) Andreas Abel **20121118210211 Ignore-this: efa2e6a304ba6139752e78ba877b8af8 ] hash: 0000002189-cbc8a653d72c673438b1f4ac5890eb0c134381fb3f20ec3e34aea1acd72ad5c1 [Added AGDA_TEST_FLAGS to Makefile debug output. Andreas Abel **20121118211018 Ignore-this: 342c7f039e9563637b618e96233088f6 ] hash: 0000001150-d28d9d4c96c7fc99a5e261914ad5332a513c8c025f33ba7e6bb8468ac22ea698 [Abstract record declarations are now treated as abstract data declarations. (Issue 759) Andreas Abel **20121118215532 Ignore-this: c9e5008493456d72d2bc6f99ddb554a1 Now there is a better error message when one tries to construct an abstract record. ] hash: 0000003374-4933ebac23b730a61baaca9f2b15ad052bbcaf4882258b1127272b467ab12518 [Fixed a typo in UselessPrivate error message. Andreas Abel **20121118224018 Ignore-this: ddf37eb16eb1471b5d0c60cfa72481c2 ] hash: 0000001668-e2fa1e8716d1cdff56b5812ee2a531289406cedc76638ee5684897f372b2a7dc [Allowed abstract mutual. (Issue 761) Andreas Abel **20121118224320 Ignore-this: 3e9a41150ae1fa0945e2c454a58bc6b0 Disallowed redundant abstract (like in abstract abstract). Changed error message about useless abstract. ] hash: 0000005561-fe4d65153a2380e0f120be1614a852e40bc490a49907c3d68dc18da5368c984c [Edit made by the HCAR editor, Janis Voigtländer. Nils Anders Danielsson **20121119094142 Ignore-this: 2d2d2a2a71af92e106fa212b167b7c41 ] hash: 0000000352-a2547d1dd574037a33f25e075f727e93b29546968f6637590f178febb1a43ac8 [Revert the commenting-out of some tests. Andreas Abel **20121119105514 Ignore-this: e689d96b76cbf00d8d67e043feea9284 ] hash: 0000000486-59bed458a93b2425667b213449b5825b5bb9dfd726b0fa62d2acae93663dadaa [Fixed showPat. Andrés Sicard-Ramírez **20121119013638 Ignore-this: 2b48207fa3baf7e603b0a52903a47e82 ] hash: 0000000244-a5e00294ce64dabe20a51c3eb702f106e2ceb3e3456a1bd6ff322a17d80b2ccc [Cosmetic change (?), contributed by John Wiegley (?). Nils Anders Danielsson **20121120100807 Ignore-this: aab42a36c68842b4a0ed6f32cece1998 ] hash: 0000000371-f4404338ee5837f07f10f622e7d597928328067ad38c2e45395791e0025fac3d [Fixed issue 765. Nils Anders Danielsson **20121122160703 Ignore-this: 6f49e40ddb739b6288e0cac92878bf2a ] hash: 0000002266-15cc8b38ca070c1b04382553cf42d7bd76fd84a4b4454b8a30c0cd724cd66692 [Some comments in Concrete.Definitions. Andreas Abel **20121122161429 Ignore-this: c9ea5c9031af1a342d85c2dac5decdfa ] hash: 0000001217-5eec02a682b96a4a565c35f840e83a7590290ec43eadd403788d3702b94de928 [IMPOSSIBLE instead of error in ConcreteToAbstract. Andreas Abel **20121122161508 Ignore-this: 3058021df4fc6db13605e95ab6012117 ] hash: 0000000370-b0ee1caecf7ee4b7549893c80fdc8bf76d9bc35e3b462a5167eecec2c62dc553 [Use modifyMetaStore in updateMetaVar. Andreas Abel **20121122161545 Ignore-this: 1a9b113af12557bd75b9f815ac727cbf ] hash: 0000000344-d02a2859b418e7b3f78a5afc66ff00dc6e23f7219d946e672a815df3836c342e [An unused unfreeseMeta function. Andreas Abel **20121122161911 Ignore-this: a7e520e4d9776724cabb68e88a1f1667 ] hash: 0000000542-569599ca1cb144b2a52333a4f14afe5dfbeb6ec4a33143daef1b89b7d85d2b19 [An attempt to fix issue 729 by introducing FunDef with NoTypeSig. Andreas Abel **20121122161335 Ignore-this: 974353834d83b01d12d4dce6cd234054 ] hash: 0000013140-57cc7ce1f5884dda1b0c1293cc2c70824b10c366ea3d0fbd9839ac79a1ed3796 [Rolled back fix attempt for 729, having a better idea. Andreas Abel **20121122162131 Ignore-this: 4702c12613f4552849c3b2eaa1e342c5 ] hash: 0000013129-4f3bba8229c1adfa7c790020671ce9f93f07ee9998ebd873609ac6d179ba5b64 [Started to make types in type signatures optional (another attempt to fix 729). Andreas Abel **20121122164811 Ignore-this: 3bea61061f4f2ed01fb8cc97bd89f3e8 ] hash: 0000004603-ce49df4a11624848e6cc06544bf7545f9db8804ef5f9fa67b78af1063aa2112b [Rolled back second fix attempt for 729 which makes types in types sigs optional. Andreas Abel **20121122164926 Ignore-this: cacea57b500dfe89dac67401916e294c ] hash: 0000004604-398fd776291cddd79d6feec338c6cd9679179db6b2c0a6ccfc0c42ce9095e2ca [Fixed issue 729 by thawing the type of an abstract alias before checking. Andreas Abel **20121122173800 Ignore-this: 35b9c996795cdf21d85201067a07c787 ] hash: 0000003612-720c23c6eabfcb89ee2df23bf9c4e75f5c8606f2a1edca02c31ce78a6bd5719f [LaTeX-backend: add two new colour schemes to agda.sty (b/w and conor). Stevan Andjelkovic **20121123154729 Ignore-this: 7b4efff033952c5d4f68ec5d6b91cd65 ] hash: 0000007328-9c242b0e0dbcf529a77196634cdcf9a3f85a2ed184a6181076d7003ba813c6f5 [eliminate a hack in InteractionTop.hs by putting 'stInteractionOutputCallback' into 'PersistentTCState' divipp@gmail.com**20121217124756 Ignore-this: 9c932442a8b9e9c099b575ce07c47ee1 ] hash: 0000011427-b4bbd5876b44db2a9a0c7092d8a39b0dc9d467b80462e986509d9eab121a759c [A new benchmark file. Nils Anders Danielsson **20121218130118 Ignore-this: 39039eb30c7c62f685b68d7e9958def2 ] hash: 0000005594-21902774f38f69fa5cda4773b6029dcf90e7a199ba1e7bafaecff5d52e659168 [Patch for allowing hashable-1.2.x Dirk Ullrich **20121215154704 Ignore-this: b880357f43c4e7ce46c92c49915dda2 ] hash: 0000001247-ae3872ed6933c97fa10ed098ad9d33119011ad158057a5198623561d47f58d27 [Fix issue 773: make instance arguments examples work again. Dominique Devriese **20121225222236 Ignore-this: 2d82a154811ef47e7942abd2c404ef96 ] hash: 0000008047-3e869742d055d8fb281db230f1c742d2ede01133a96ef65385c69fe61ec858cb [Patch for hashable-1.2.x simplified. Dirk Ullrich **20121222221956 Ignore-this: e3822d98932ad1bbb05cb26ef39b1e73 Instances for hashable-1.x can be defined by using `hashWithSalt', too. ] hash: 0000001067-39d1c31ee8db802df3bd5cef3fef6cf6486b2412a834d412bf5e5ffd601bd784 [Fixed issue 784. Andreas Abel **20130120204611 Ignore-this: e77705e68affd1f06aad288e425d175a ] hash: 0000065077-6ed391079879771b7721c354d17b7b9cd19df05fda87445966fe6e5a1218bbdf [Bump the Win32 version requirement for ghc-7.6 Jason Dagit **20130119052027 Ignore-this: 20ffa91e820ac39e0d6daa8f3e2e413c ] hash: 0000000233-70fa81393a4ffb75ce92c44ff6ef42cb1464dcfd156e0e2275c011015697982f [Explicitly set stdout to utf8 Jason Dagit **20130119052112 Ignore-this: b5459c1f61d3ff263623f8b88885d428 ] hash: 0000000212-9207335e082c1f0f70577517b31dfa3a4bf9d0fa54924a9bf78db920786de22d [Restored old lower bound for Win32. Nils Anders Danielsson **20130128134429 Ignore-this: 3c63ecdae66e8a5a0c3eb054b306143 ] hash: 0000000255-7c3dfa1ac512170e6439a9c6deeab095a97f4542036c6fc56e10219c8c9558d8 [Use UTF-8 also for stdin (when --interaction is used). Nils Anders Danielsson **20130128134526 Ignore-this: d4d4bff88ab1bd274344578d513320d3 ] hash: 0000000434-f3ed7fe5adb98a35906c31a6c580c5bf01cfbd823f40585b749306a0416bf591 [Latex-backend: fix escaping of ~, ^ and \ Stevan Andjelkovic **20130127195655 Ignore-this: 8e9c110d7d22ee0dfdf02d7ae501056c ] hash: 0000000408-41b762f536afdfab49a888f0351139e059b37b6f247fb6421eb70a48020cb8dd [Fixed Issue794 by disabling an "optimization" for compiling irrelevant arguments. Andreas Abel **20130216133146 Ignore-this: f54b8908bc70ec542f02bf409d30cb51 ] hash: 0000000961-1842686817a76b129e6f67d38fa49efe558f6745527413c1ecf31bf0db8471ba [Disabled matrix-shaped orders in the termination checker. Fixes issue 787. Andreas Abel **20130218132050 Ignore-this: baeb8f786702a36da37d1f15b76f50a0 Matrix-shaped orders do not work together correctly with the idempotency check from size-change termination. Research is needed how these two features could be integrated. It seems best to remove matrix-shaped orders for now. The standard library does not use them. ] hash: 0000002694-4d545eae640bd8c5fef55ce8fe03bf1d872ba3975c8e9b31ef9e8a5064621d59 [Release notes for removal of matrix-shaped orders in termination checker (Issue 787). Andreas Abel **20130218151648 Ignore-this: 190ef6c481e5372f519e54bc73eaa1da ] hash: 0000000454-e0f2dc362af1f380ef85c94f8ba2eb136b24969eb411faeeaa960b9965f2ba4e [Removed error on failing occurs check, because it is not always sound to throw it. Fixes issue 795. Andreas Abel **20130218153438 Ignore-this: 9156d7d0077a56bb21ef087fa2daf09e I think it had been disabled before, but I had reenabled it in May 2012. Now constraint solving is more complete. However, because the error is not thrown even in situations where it would be justified, instance search is weaker now. (See last example in test/fail/Issue723.) ] hash: 0000003674-bb0a0d5de390299d6999c60c88d90b3766e055d2bf9805e9ab81ee28c9fe0b29 [Test case for issue 795. Andreas Abel **20130218154828 Ignore-this: 9941a3cff6432e92be519f28495fa4f2 ] hash: 0000002167-37d4318dae59d46386720e156dbf670d785f1cfda9172eeff59a91c733586150 [Fixed issue 797. Print location of unsolved emptyness constraint. Andreas Abel **20130219155420 Ignore-this: eb1f3077f44f598d19432e19660060db ] hash: 0000001882-48c98967740d790eaf041dbffde5a8f9436a3145160568eaaa39c0f8c7ba4173 [Factorize Arg. Guilhem Moulin **20130219161229 Ignore-this: 3a5d21da7e75a23275bf2c8c1243c383 ] hash: 0000172019-e53d86dcb49a5a1c5bfb187381d55a5b6653ba1888887ce16fba30bdc69468a1 [Fixed KillRange instances for Relevance and ArgInfo. andreas.abel@ifi.lmu.de**20130219170725 Ignore-this: 4db13bf7476f0daa3d991c38d20db419 ] hash: 0000001782-a2b9c2deff5a7a0ec77030ce147d420f679f3c6b9808b1a42c45ab5d89087d9f [Constructor-headedness (injectivity check) no longer ignores abstract. Fixes 796. Andreas Abel **20130219230923 Ignore-this: ca3e16a140bddfc815ebe60ed0973c9d Effect: less programs will type-check, however, changing an abstract definition in one module will not break type-checking a module importing the first one (at least not due to failing constructor-headedness). ] hash: 0000003554-bf110fda3f36e7a14db820d9db9be2b0d65f412a3d1cc5fece25d342822f33be [Updated error message in connection with issue 795. Andreas Abel **20130219231101 Ignore-this: 99367532eb019a5970d0dbfb07a4bf34 ] hash: 0000000287-67a8a032d0250ac6941e1bff1b835b98b0b038f0b8a38c0e2746964d386d200b [Fixed issue 780 (internal error in getTypeMeta). Andreas Abel **20130220000500 Ignore-this: 63a3b8e026311e9a3d69ea2bd68d316c By disabling instance search for irrelevant sort metas. (Not intended anyway.) ] hash: 0000000580-b73bb37845b338c18283e6898e1fb9e1633aff4754b9f7b0c56007bdf0cb7f45 [Initial mode is now ConcreteMode, not AbstractMode (fixes original case of issue 796). Andreas Abel **20130220234349 Ignore-this: 84b2d7abdc88efa295d28d1212600d9e That is in accordance to my intuition (abstract is not the default). ] hash: 0000002273-a1a8c17d4e0f60a2ddac6028a695063ca3a466ea4100ebce5cea0165010e52ba [Simplified allRight auxiliary function. Andreas Abel **20121201212708 Ignore-this: e4494f45f1baa4aaa91778f5211a02c4 ] hash: 0000001276-d13e2ba2de2586bad8e03529ea1ea20dc9c12d8ea76a1c4cbde5eae314bb2658 [Fixed issue 782, lexing of keyword 'to' in 'renaming' directive. Andreas Abel **20130221093347 Ignore-this: 83a09eb5dd557850634cfc80c7c2837d ] hash: 0000001400-84b62e0b24f09b92a1141e081a8431e53d9342750f39a4f2c2cb7d9a1f527bb0 [Issue 4 is fixed (again) by making 'ConcreteMode' the default (issue 796). Andreas Abel **20130221094354 Ignore-this: 8760dbeaefcafacb849af35a23a5f0ad ] hash: 0000000974-2b0accf786d328c6896c804fe17cd702784b967003653365f6ff021222f8e3e4 [Fixed issue 799. Andreas Abel **20130226035226 Ignore-this: 860b20e1858721352f782d023e30f6a5 Agda had ignored hidden underscores following a constructor even if these were more than the parameters of the data type. ] hash: 0000002631-df8166e6ab4c9fffb308a0463b82e595ad79f458825278382aac5017739b1502 [Fixed a problem with free variables in type checking extended lambdas. Andreas Abel **20130226152254 Ignore-this: de5e611a144f34602adfc4664522ab31 This surfaced in connection with issue 778. The problem was that in the presence of where-blocks the wrong number of free variables was picked. ] hash: 0000002945-2cfd71c5c4d871b10c83b893c71ca4ff993602fc18dea63a7ba2b92d4122a809 [Refactor: put abstractToConcrete into TCM for debugging purposes. Andreas Abel **20130226214441 Ignore-this: cec96b341b3334f9203d4f2b8b8f3f34 ] hash: 0000004715-0d38a9f68f7a3e22caafa138c9a91b8ec62e95ab179da83dec730c94c89e557f [Fixed a problem with debug messages for 'with' causing a panic. Andreas Abel **20130226214624 Ignore-this: f67ead53fb1ee02aa4877dc3423c3f98 ] hash: 0000001665-974befa7829317834eb9488dd4467c20cc124da82a170d4eec5fa35f39369b1e [Refactoring: pulled getDefFreeVars out (InternalToAbstract). Andreas Abel **20130227093829 Ignore-this: 7e299fe87cf25c8292b61c94e480c0e ] hash: 0000001343-87f015dabe40010336e3b101d0c539757d6d5480d3d26559a9b213153cf3407d [Fixed issue 801 by doing termination checking before injectivity checking. Andreas Abel **20130227103636 Ignore-this: 53f28e17c7b23876fe306d1a9821f468 ] hash: 0000002983-7443385d952fe25be9d123b0de8c379445d75760080b5fb0fc4ed4c27e873bb5 [No longer unfold functions which fail the termination check (fixes issue 653). Andreas Abel **20130227120321 Ignore-this: a927b1b5affc58c24587fb3a081fb443 The problem was that the positivity checker looped. Now termination checking is done first. ] hash: 0000007008-0c3e7602b071fb26f14ac2a41ebc59390faf1526812241902de441cbc34070aa [Issue 385 is fixed along with 653. Andreas Abel **20130227121513 Ignore-this: 6d70f2e3214c50c2e78fcec64ee328b7 ] hash: 0000000808-49a24f3d5f1dfb290335ee8bc468ed4c2a2c4a97d1a52c246219d298ef8bb58d [Fixed issue 802. Index arguments of data types should always have polarity Mixed. Andreas Abel **20130227155149 Ignore-this: ccf98ca3daecace8fbea599b692177f2 ] hash: 0000001411-a6e1b0e19165846bf22e18aabc532b390d9727d29d00ef6d3d127d3f85fe6ae3 [Fix the last faulty patch (ProjP sneaked in there) addressing Issue802. Andreas Abel **20130227184349 Ignore-this: 65372e83f1f2ef5d3d96976c2f2182a1 ] hash: 0000000283-9fab1b6cc25e2b2c6afcdbbeb859256ba27fe4c445bb50ae46cd5d8fc6218818 [Fixed issue 800. With display form problem (permuted args). Andreas Abel **20130228105212 Ignore-this: 386c8c823452ba5800ffc791900481c7 ] hash: 0000005292-49a878004d4220499195e81022512437704caec99d8310af3c7f405cf22643f0 [Stopped using 'reportX "" 0' inside verboseS blocks. Nils Anders Danielsson **20130215150527 Ignore-this: 20937035682a51f554b492a245c8d6c1 ] hash: 0000003327-ae73d2c622d0da85fa4c3b1fe7d7b23bbce456d7dfb07375c9c9f5bb5d17d426 [All debug messages at level 1 are now displayed in the Agda info buffer. Nils Anders Danielsson **20130218155744 Ignore-this: 68a4fdee3a0ff5021748704194954ca2 ] hash: 0000005683-1f89b1d67440e860c08eab7da3015f5d263cdcb26e44ff622bb4ed55045cab64 [Added SplitError constructor to TypeError, avoided use of GenericError. Nils Anders Danielsson **20130218164006 Ignore-this: 54b1a05d0d1869144e49327c2a0cc238 ] hash: 0000004383-04cb4c0a53e5eb1d88dc2892d3715b319059e416b9e0dd9d9e0898442556cc5e [Modified the pretty-printing of CoverageCantSplitOn errors. Nils Anders Danielsson **20130218164257 Ignore-this: 19a23364d6f552682a16bd558c755a9d ] hash: 0000125367-c53842433f6a97b2bcdd85c6937f151cb6d3da29e2d5d87732d816ae80eb1d14 [Added a second test case for issue 802. Nils Anders Danielsson **20130228115850 Ignore-this: cd4d87faf34425c9887ac640b181b6ca ] hash: 0000000587-4198c3cddb00641ec64080d0e04bf0c4550629fc45d68d2a248c7bac798bb82e [Fixed issue 804, NO_TERMINATION_CHECK is now accepted also within mutual block. Andreas Abel **20130228161322 Ignore-this: 6c04b11e3550093a9d6c1b84b4488cf7 ] hash: 0000002159-92047c755444be825c2413fb8de8af71ae45a7ef47d38c3665cb48bf38bfbdb9 [Removed absolute path from test output. Nils Anders Danielsson **20130228164312 Ignore-this: 4e3ad0d8af718070e22c0b8e71c78824 ] hash: 0000001389-943bbe1983b4d82c2665ad1e88750c1d033940b443492cd97c5bb8c03d9bb5ab [The Epic backend no longer prints the epic package's version number. Nils Anders Danielsson **20130228165453 Ignore-this: 2760edb08025b4f79eb11be4c657e13b ] hash: 0000000571-fc5dd8cf63c33167d49f5a415023a7853d77b01ad08acdd4abb31f29ea971722 [Refactor: use case in inferHead instead of top-level pattern matching. Andreas Abel **20130301123815 Ignore-this: d1a5c5aba1ca2628730b7db5c3644e1d ] hash: 0000002842-6e2210bdc7a5cce17dca39738c66d5f100bf6b08c299fd1526ed73110d191e69 [Added Args to Syntax.Abstract. Andreas Abel **20130301125554 Ignore-this: a3ee7c75474f27bb723162fb1ffd9c6f ] hash: 0000000407-9229c2a3d938d681f9704a6eca23c76d6a5f2aa8caa0632e10d9b83930b35f93 [Refactor: put application cases of checkExpr into checkApplication. Andreas Abel **20130301125931 Ignore-this: 5daae86ff311d0f4c74e4517178fb9a4 This reduces the monster checkExpr a bit. ] hash: 0000008862-9b6042cf79e93dfb529b8f5c4f09f1275722f8c017a3e7e878cb7ee2cd34b6ff [Refactor Syntax.Common: added lenses for Hiding and Relevance. Andreas Abel **20130301170703 Ignore-this: 7b34f615de19934bfb44be631101903a ] hash: 0000054463-133e2c6e19a15e135e26be9b976cde9f0b4aafca38927dcab16108f3b9b207cc [More characters. Contributed by John Wiegley. Nils Anders Danielsson **20130304185118 Ignore-this: 80ec1fecf2dd0b3974a334849b0d7a6a ] hash: 0000005594-0743432ac140e5416a3c67ea15a139fdccfbd0e5f61a23c30ae4baf1a86db78c [Documented the new key translations in the release notes. Nils Anders Danielsson **20130304185618 Ignore-this: e637f4d32b055c176439dcd9fd628af5 ] hash: 0000000353-9147909a676792cc4977bcb0967dfc3b9895ef8856b3cfad430ee142bab93015 [Fix for issue 778 (improved extended lambda implementation) csfnf@swansea.ac.uk**20130304195236 Ignore-this: 9d449c13c5de411176124fb0d97272b9 ] hash: 0000006365-c90b22793c73e78b6418e45d1d13cbae64fd299bf9da9fd6de28b27a2f7d5bef [Make test/lib-succeed/Issue784 work with latest std-lib csfnf@swansea.ac.uk**20130304170350 Ignore-this: 2b00ba0ebc562b3ee97e16d141a3cd42 ] hash: 0000005256-8bc3b95d5bea253da69686b64aeb7874d4cb98b7b0140ac7cc2041a8e37fb1e3 [Refactor: Unifier's FlexibleVars are now Arg Nats instead of just Nats. Andreas Abel **20130305001458 Ignore-this: 7d0e3998d29f8feb1fae65767a0c3e68 ] hash: 0000002190-c6a91e5de4ea9d23e702f5fb916a34ec0a67681d0b4c74143f5e835b91039fdb [Refactor: changed FlexibleVars to dedicated decoration (instead of Arg). Andreas Abel **20130305110156 Ignore-this: 2497a6c3883f1df211afa74c3f188a00 ] hash: 0000003618-451bb946b6389e17117f92a229393ee3abcf6f6bb8fc65e11e9be3089aab015a [Inessential: added debug message. Andreas Abel **20130305111357 Ignore-this: fa0c10695a4cef1ade0fd458fb3e5fb0 ] hash: 0000000692-45af19817300bc5a480f0bca9cd2e807dab0a85658bdb3f7131034c665b4a208 [Addressing issue 811: assign earlier variables during unification. Andreas Abel **20130305112753 Ignore-this: 63f6a17a834700c3556f9673193f4487 The goal is better splitting behavior, dotting later rather than earlier variables. But also, we want to dot hidden variables rather than visible ones. This does not work perfectly yet, but the behavior is no worse than the current one. A full solution would probably need a global look at all flexible variables!? ] hash: 0000006776-48e843cbea8918df9593a7154450d7d0b9567935cf3a6bd34ac8dafaa54fe65f [Removed debug printing in test case 778b. Andreas Abel **20130305112940 Ignore-this: 196c6d2db1980303cbe7acf2da386455 ] hash: 0000000466-85ce187697d91e0d5ecb08115c1f61c670af08ea0c7dc7f1228a12d854c4fbb5 [Verbosity info in test case. Andreas Abel **20130305113035 Ignore-this: 40b1c9d244dfbd8feb9e32aba098b9a ] hash: 0000000388-f4e4a83ea6a73c6796c2c7a12c9161c6273e8abc9fd83efd9a6e67372e712678 [More verbosity info. Andreas Abel **20130305113145 Ignore-this: b2321c03ee9b461d8ee34459e41be8ff ] hash: 0000000639-4ed0189ed77757b7576bab49fbf1bd2969a63121b975fded5a058635d82a54eb [Fixed issue 814 (crash in elimView in case of unapplied projection). Andreas Abel **20130305115741 Ignore-this: c020497ae66b9b7332945239842144f4 ] hash: 0000001643-7d8c62e8b0bb26700c2ce79f757d51f4baa6adc2844fff01e2574029555536ff [Fixed issue 810: intro tactic for constructors skips hidden abstractions. Andreas Abel **20130305155213 Ignore-this: 5b2cbe416c14c8e65e70061f75fda348 ] hash: 0000004074-200e7a08078cd7a1611fd2d845b59e2f2719bea19713e78fa0f57c4b0da695c3 [Add blackbold B and 0-9 to agda-input.el Stevan Andjelkovic **20130305164058 Ignore-this: 10319bf95e1a1aa38f260858269bb054 ] hash: 0000000707-2b3388e76865f62206d9e05b70428a6b8289b359dd5bdd2a508b60b8c00727ba [Allowed QuickCheck-2.6. Andrés Sicard-Ramírez **20130307153732 Ignore-this: c3d9dcf1a8936f00f8de4d411d55811b ] hash: 0000000266-80031fcc4d773958c6a423e9ad8664b50ce15db8a93029588ce255abc7aca101 [Minimal fix for 818: error message instead of panic when with clause has wrong number of arguments. Andreas Abel **20130308202059 Ignore-this: 647dc2def08d5c3a79c56d126ec8022f ] hash: 0000001607-1281d2e6ee51bcd3036812b48a20bcdac468a8571ba42a58b42e8f43951bdfc1 [Comment on WildP and undone attempt to fix 819. Andreas Abel **20130314065503 Ignore-this: 9453878950f48ae43343b9ab9b5e3d50 ] hash: 0000000764-d414e3d139e9b3a0569b89b77331fc030491c8520f2307fb04c215467d459adc [Factored out function checkAbsurdLambda. Andreas Abel **20130315001944 Ignore-this: 67e124620a738f7b35233a3be89915a8 ] hash: 0000006657-6391ed504f604d4dd3942a1e20ff89056e532e7e4fd8d725e66c79e5a696f198 [Refactor: use LensHiding (function visible). Andreas Abel **20130315002104 Ignore-this: a30b1582dc0c636856524af9418d88e ] hash: 0000000602-670d211401223d97c71c1c82ff5fa9ca2a89487464be2de897b4633d0290d728 [Factored out checkExtendedLambda. Andreas Abel **20130315003555 Ignore-this: 92c4abe3130dcba3f88084dcd4221c49 ] hash: 0000003482-64efe4125be6c7b3870124382bf92b70c4a38af870d0f171e8c47c2c3a9be1a2 [Factored out checkRecordExpression and checkRecordUpdate. Andreas Abel **20130315005921 Ignore-this: 31165ad98c0471532678bc5b7b7f659a ] hash: 0000011249-8e939af9da116a4604ba0040dc2bd512e294ca0cf8ae6a4a4ba802517796abb7 [Removed a stale comment. Andreas Abel **20130315010002 Ignore-this: e01f0148382d6a20200057a5d242c083 ] hash: 0000000380-a584df22c49079443803fba0999d30352350fd0298bca20c8916b24969b3ba01 [Unified 4 definitions of unScope. Andreas Abel **20130315015459 Ignore-this: 95caf229066582e0e8b957fe6de9f4b7 ] hash: 0000001482-cfa25cdf3bb7541c83b52f3602f6633d77209b994c82e281f5218f1fcaefe893 [Refactor: fused checkMeta and inferMeta into checkOrInferMeta. Andreas Abel **20130315090009 Ignore-this: bcc04c99b4aa1673dc8e8dec585f6172 ] hash: 0000001823-d8d7edf2da08f835e0fc554bc646b7924565791396d1ab204528884498c75d5b [Comment and type signature for domainFree. Andreas Abel **20130315090700 Ignore-this: 68520650a39510a82f4ebfa66ab53662 ] hash: 0000000376-d4b3bd5e720d705939b1475eaecf3562673ebdc88f0cc83a3189c46c274f9adf [Fixed issue 807 (connected to issue 655). Andreas Abel **20130315103554 Ignore-this: 632affa77c14dcc6c437ac18e1ec71e1 Problem was a circumvention of the code that generates helper functions for coinduction when checking an alias. New solution for 655: Added new flag envExpandLast to type checking context, which is turned off when checking aliases. ] hash: 0000004962-2140b71b4be4ea14b2fff9031f41a416233b2a4c7c396742db47d9329227bd42 [Another test case for issue 807. Andreas Abel **20130315104604 Ignore-this: 9cd5864552a9df9104d478208d02228c ] hash: 0000000708-cb35c93a572a461b43d840191b19eb30d7947d61cbbf4fdb735c198fa0936224 [Fixed issue 821: invalid IMPOSSIBLE in comparison of spines. Andreas Abel **20130315112601 Ignore-this: a89e91dcd3895455bce9bf43a734f4d6 ] hash: 0000008945-605e34d31b81a4e94dc7f50fe39bfaeb52f35dbcae15cc9e07ff934d3c3112c9 [Reactivated flexible function arity (issue 727). Andreas Abel **20130315122054 Ignore-this: 6454bd465721be1c577d3f0ee147f721 Compilers probably need to be updated to this feature. ] hash: 0000004581-e1048a4bf8d37b827a5842da04841bda27fe37df14c61d60e002cf7765499694 [Release notes for flexible function arity. Andreas Abel **20130315123053 Ignore-this: 236764161f49f1637030334af09c904b ] hash: 0000000619-1266c8f12b566c38959bf974507b42919fcea74584c1b9e5db473cc5120704bc [Russels paradox with --type-in-type, by Paolo Capriotti. Andreas Abel **20130315124305 Ignore-this: 6b69e43c3a5ac42c0c46477d70a0fd86 ] hash: 0000001055-0fd21a0b7d299e44ff9c2839f9dbb368347af7130be1d2be61f4c1615432d5d1 [Fixed compilation. Andrés Sicard-Ramírez **20130315144015 Ignore-this: 3ccc460fe0eb8cec3590fd27b56e4d8a ] hash: 0000000197-cbcab2f6962eb84e33ac26e886835541b5cb223671f9789aa7e0df1a39457290 [Tried to fix broken jump-to-position-mentioned-in-info-buffer functionality. Nils Anders Danielsson **20130315123954 Ignore-this: 158378b3c25e763792c8996501981513 ] hash: 0000000814-e6364a47183fd997d01418c3600416dc8cec7683387ad4a7f175afa4fb9a072a [Testcases to ensure --no-termination-check prevents disabling of reductions. Andreas Abel **20130320150710 Ignore-this: 1297fc9ecad0cf28e9e76dd2f2a53407 For instance, in the positivity checker. ] hash: 0000001743-82b4dcf83d0fa95fbd7cacc3183b2d80b0c9f869d1c46b568a870aa57fa6fe7c [Fixed issue 826, unfolding corecursion now instantiates metas. Andreas Abel **20130320161342 Ignore-this: 10b0dfd7263cc01b631af83858a64702 ] hash: 0000003311-a1e70525abbfa6fad62defc422ba02b37ae1810af5d22cd8073182a13e6b3442 [Put agda.sty in latex dir instead of current dir csfnf@swansea.ac.uk**20130319143334 Ignore-this: 4038edb6f68f7fb48ecfeff2ebb0b73b ] hash: 0000000986-43bb33c5e977b0c8992545dd9d4defdb80fe2a536d72193d674e492be462a26f [Fixed issue 822. Andreas Abel **20130321083828 Ignore-this: ce10bd962c65857f26e07b8ed8321f5a Parsing patterns went wrong in the presence of ambiguous names of different kinds. If one defined a name first as non-constructor and then as constructor, it would not accept it as possible constructor. ] hash: 0000002235-3cf11cc49a100af1596f4c692536e60b2fa44e46aace953854d2e194688af152 [When resolving an ambiguous name in a pattern, ignore defined names and fields (see issue 822). Andreas Abel **20130321092839 Ignore-this: f6dd880eb2bb3f9fc03bdb4113043115 This allows constructor names in pattern which are ambiguous in the sense that they also have a non-constructor definition. ] hash: 0000003495-0e07ec0f77074b00cac192ae3a54a4b14aeccfd3462539af135ed233c9663236 [Keep track in record patterns whether they are eta-expanded implicit patterns (reduces issue 825 to 824). Andreas Abel **20130321135527 Ignore-this: edc0be7d227f46a4a1c46634e2790d7 In strip for with clauses, eta expand implicit pattern on the fly if parent clause has expanded implicit pattern. ] hash: 0000011870-fe16b7af45d5eddb68a0a95ca02125c344b58f09633c563e586a530f10a2f9b4 [Tiny refactor: added patNoRange for PatRange noRange. Andreas Abel **20130321144036 Ignore-this: 47df2d4174a97bcc341a32aa192e6316 ] hash: 0000003386-6a72997d38aac34644991edaf0421b1a9d10735f132046511228df51f340351c [Fixing issue 665 and 824. Fold back eta-expanded implicit patterns in with-clauses, if they meet a dot-pattern of the parent clause. Andreas Abel **20130321181203 Ignore-this: ad6c213f1488053ca44c8fe578791626 ] hash: 0000002103-6d31673516fb7604430baf9b5b0b0fa0834a5e97be119b1985c1be167c9991c1 [Fixed issue 635: only eta-expand implicit patterns of record type with a constructor. Andreas Abel **20130321221639 Ignore-this: 17b6b6c4362a5052b9c8d7ec2ac05374 Otherwise, case splitting might emit recCon-NOT-PRINTED patterns that cannot be parsed. ] hash: 0000003658-59faddfbd6d09d07725c0c43852664a8bd5e12dc6b7028bebd88a68bc6ba0adc [Better error message if invoking case split in a goal that is already solved (see issue 289). Andreas Abel **20130322090709 Ignore-this: ca9657e0088a614edb0ed9718af0fe03 ] hash: 0000002931-bc6a5a97d4dcd5d481f980a933aaae3abe4cb554f132383d81ed6bfcbf9ee7f5 [Release notes and test case for the restriction of eta-expanding implicit patterns to the case of record types with constructor (issue 473, 635). Andreas Abel **20130322092510 Ignore-this: c8d0e82c74d8c08f7c4faaaca36e3f37 ] hash: 0000002335-72c5a335443d48c2d074ba20325a4ae77299e3fcddc227944a524079dc62be15 [Fixed issue 279-3 (constructor from instantiated module assigned wrong parameters on lhs). Andreas Abel **20130322121202 Ignore-this: c381ac455666933086cde9e6fbd74b45 Fixed by adding an extra check for the parameters. ] hash: 0000003218-6eb5b585db73e395ee40de32f1f3691fc66431af1b5e6e59488f5d914df6ebe7 [A prettyTCM instance for Internal.Pattern (debugging only). Andreas Abel **20130322184513 Ignore-this: ab5576ba4bd50bd9896e6db8d63cd898 ] hash: 0000001688-61ae789e664e6d4912aeb610533422101c4af5403bd43f0f4813a667321b1e9e [Print name of the function when incomplete matching during evaluation. Andreas Abel **20130322185031 Ignore-this: d0f6c706fbeb096f1528f68665e118fe ] hash: 0000002069-b6298251826d679c8ed51bb51bd889201b6199e8522de32105acd78313b51d6b [Fixed issue 827: incomplete case tree caused by record pattern translation. Andreas Abel **20130322185311 Ignore-this: db28870f546533e8a4bd9e63c1fc6f50 Solution: expand catch-alls if a record match is on the same column. ] hash: 0000006771-73260499118219ad1d9f8432b23bb607f8142bacbad464e7bbceb0190138b164 [Fixing issue 829: need to keep original clause in catch-all expansion. Andreas Abel **20130324125756 Ignore-this: 16dd9b9e7bbada11ea61cec0abf7656a Bug was introduced in fix for 827. ] hash: 0000001674-1a5f443f5697692d721055dcf708736e22ec3355cd906a789a88a3700fa85348 [Fix for issue 641: -v is now reset when a file is reloaded (in Emacs). Nils Anders Danielsson **20130324164811 Ignore-this: 5dcb806b4ebf580c89502543459bd6bd ] hash: 0000000893-27a9670f3dc944eb77d50a05060c56c65d28568bec499b690a1f989d82436d14 [Input methods for missing linear logic operators jeanphilippe.bernardy@gmail.com**20130328103755 Ignore-this: 142e9194613d1e22efbe87bbd8bd9df9 ] hash: 0000000275-ae6cad2c36b8e1602395cd150d97f2d23f9a51d73ece1ea0772fcbbc117a2627 [Changed the bindings for ⊸ and ⅋. Nils Anders Danielsson **20130403125717 Ignore-this: fdddf91783309453c7c9293da2ad3e61 ] hash: 0000003497-cd24d14789adb329f8cf0ba0d06706e5fd092ecbd91479b310972c6304e4994f [Fixed bug: GHC options were given in reverse order. Nils Anders Danielsson **20130405221250 Ignore-this: b8c5e4fc5e5306f65888731c86139292 ] hash: 0000001140-b678b31fc28759f697bd38887b76416696384bbd5124ee5ccc970cef8be82160 [Fixed issue 830. Andreas Abel **20130413110718 Ignore-this: ac17b77ed29368b0ef7fc87992a6d0dc When checking that sort of constructor type fits in data sort, constructor type was not unfolded. ] hash: 0000001018-878274230453ea8fc64b6a1dcb8197f96c5a355e701ef19f3e872e88b553d5e2 [Fix issue 833 by fixing the type-checking for section arguments. Dominique Devriese **20130412125806 Ignore-this: 57166bd710682777c9f44752420ce4fa ] hash: 0000000957-0e1e6acc2680bca7cf6a6bc6888fec9c76c0c78ca2d7c08477ec3fb16c4e2e3d [Made "cabal haddock" work. Nils Anders Danielsson **20130422122046 Ignore-this: c6a704c420ca677a19715b6a61591512 ] hash: 0000000585-b84947c6a95ed67a881623d0bd99e0882599d0e02131f1dffa07adbdf7dc7cf1 [Text is now inserted at the end of the *agda2* buffer. Nils Anders Danielsson **20130422122707 Ignore-this: a84c0d3c5d14640951012270fd4f60e3 ] hash: 0000000454-3a84a2a21e18ed1cddd66f9e9cbfbee1d9416935d6e09b47cb4991f01678d24f [The function inactivate-input-method is obsolete in Emacs 24.3. Nils Anders Danielsson **20130422122717 Ignore-this: 1a65e9fecd737c51bccdfac4efda6982 ] hash: 0000000438-9046f87d10e097bbf87e0b1606c076adc856c39aeea3e9000f6c63f71c3596ac [Initial draft of HCAR entry for May 2013. Nils Anders Danielsson **20130430084603 Ignore-this: 8be6ac868c8ff14c4352d56c5295ea9f ] hash: 0000002018-11291df8ac45a6d4ec5737213a68894b2c75436643d5d6a57fb874b29420adae [Fixed issue 841. In interactive refine, new holes could be numbered wrongly. Andreas Abel **20130501093706 Ignore-this: 9ea862e4a5715c87b264a7c2b93cfc84 Fixed by improving position information for speculated new metas. Now, the appended new metas are located at the end of the hole, making sure they get numbered last. ] hash: 0000006918-3ea11603de039321cf4b489e04032d80317b0967a464cb28f707bfe4b739ecd9 [Refactor: Inlined some single-use local definitions and added a comment. Andreas Abel **20130501100818 Ignore-this: f3b4cc75d4d8be93d346ac82968a786 ] hash: 0000000935-27ad5e3cfed2de8c15c8d4a170a70c8bec9c9ec77e2f1ddadaf116e4104a94f3 [Data module imports in successful test cases. Andreas Abel **20130501190123 Ignore-this: ebf47147c08577791faa900b90ffd69d This is neccessary if we want to fix Issue 836. ] hash: 0000000725-5a394f9dd4e4a10b16443178ba069c00778cbbd2a8d21094203df7185041f2fc [Fixed issue 842: Too short lhs in function with varying arity. Andreas Abel **20130503100729 Ignore-this: 4953c77273f6f55493c2fcb5412fa7ae ] hash: 0000002376-ead983c35a82a7e2ac552e38484bd540736f15186f4c69bd7b10c924425f2ff2 [WontFix issue 836: constructors/fields also qualified by data/record name. Andreas Abel **20130502121532 Ignore-this: d74e76dddcced131b9b7d2231cbc4701 ] hash: 0000001580-b8bf13b7f4148e938ea81025e0846b32a44287ade1a1278dc13314275d5cee3f [Fixed issue 843: incorrect translation of let-bound patterns into projections. Andreas Abel **20130506150241 Ignore-this: 7c50007f9957283053828f2f15262fc6 ] hash: 0000001771-c0fbc4bf4d143c0a7d4c9bf2c74ec2728e854f395f992d9d909761c3f8e5ac5c [Fixed issue 847: body of abstract definitions was ignored during termination checking. Andreas Abel **20130514141551 Ignore-this: e8358745d4a1f9691665191060593161 ] hash: 0000000761-d103a5575c5c0512d5ed5ef514500985c905cbb891ca167f5e1ce72dd1ca69f8 [Fixed Issue 848: allow anonymous module in where clause. Andreas Abel **20130514142851 Ignore-this: 5fd3ea98005d705e9b55667f47111d12 ] hash: 0000000430-2824022ddc2859cd503fc818ac4db63e4a46ed76cb9ec58d5bdee6c75fd20524 [Cosmetic change. Nils Anders Danielsson **20130430084758 Ignore-this: c6a163958afb759009ec5543b9d89c6b ] hash: 0000000459-7e04723b34f6ac288c234c2f05435c5a095c0b85f4e881332c0b55822b6d937c [Fixed issue 847 (in a slightly different way). Nils Anders Danielsson **20130514145149 Ignore-this: 9a57f8cdc16512578a6ee43a264566e1 ] hash: 0000001689-f05d5e904fd5046b7d0bba22709307d915aad1a8bf713165bd1704ccb054262f [Fixed issue 849: coverage checker unsound. Andreas Abel **20130514164531 Ignore-this: 971f11eeb68c7a9bc66569e2bf80525b A dot pattern which could not be parsed into a pattern used to match any constructor pattern. This lets functions with missing clauses pass the coverage checker. ] hash: 0000001776-3cc37db4923b28b57db7e74362c07c5c3e453e8b91e1d9264cafa44db71d4061 [Some debug messages for record eta-contraction for analyzing issue 846. Andreas Abel **20130514165616 Ignore-this: 8ea90de417cace0676ff2138c1bc7eec ] hash: 0000001051-5c325ba8e322254935298eaae74547b3fe67d015156951c3cece8752d9b24e51 [Fixed issue 846: Improved conversion check for pi-types, which makes instance search smarter. Andreas Abel **20130514221149 Ignore-this: c2e81a410a3bd2e8c2d36bbd31d935c0 The problem with 846 was that some hole was instantiated by some ill-typed record constructor (under unsolved constraints), leading to a crash during attempted eta-reduction. ] hash: 0000011920-57c2a4dcd6f3f5128f4a39072f21e6f2bdee4673540e28b4fae1fb4aff529b89 [Forgotten changed errors (fix of issue 846). Andreas Abel **20130514225035 Ignore-this: 8fb8393ebf9ffd626c4dec5b400245bb ] hash: 0000000233-69fa668276c93771c0f6d4d9899b0b4ef93b3c4f3a9359f1cf22e360bd6f4d27 [Improved on fix for 846, restoring unsolved metas for fail/Issue399. Andreas Abel **20130514234452 Ignore-this: f567b92e70c94336a08318476ec11c4e Stealing constraints is the answer! ] hash: 0000002897-8d55f909116ad73bb28462c1467d46b8e78a378d2268354aec07e6d050ef985f [Finished new postponement strategy for conversion checking dependent things. Andreas Abel **20130515091241 Ignore-this: 7627b7701686b9f24574faaced40dcb2 If check2 depends on equality check1 of two terms, and check1 gets stuck, we no longer postpone check2, but we rather created a blocked version of one of the two terms and use this in check2. This allows the conversion check to proceed a bit further in some cases, e.g. f : (x y : Nat) -> C x y f a1 b1 =?= f a2 b2 If we get stuck on a1 =?= a2, we now still try b1 =?= b2, substituting for x a version of a1 which is blocked by problem a1 =?= a2. ] hash: 0000005926-b86cddcbf8d4c12ddf39218af218aae343b14f5970415a947650bc78741689a1 [Added a toy benchmark. Nils Anders Danielsson **20130515125606 Ignore-this: 8d9dcf3abc4c78eeb4c5e822c3341631 ] hash: 0000000485-2c0bf33f45994988bb64e20820d532c3f659b703dc4f0ae30b91eb5f32ea98ac [Improved fix for issue 848: open anonymous where-module. Andreas Abel **20130517090622 Ignore-this: 8ded8ca2c5baaf99c9afaf240aaf61fe ] hash: 0000001010-afcbc42c04bde8694416f8ca82647ffe822bf1388b198e741d67b6fe4dcffc4b [Avoid termination-checking non-recursive definitions. Andrea Vezzosi **20130518002211 Ignore-this: 233c7a88bce80d2588f6e57a07ef91d5 ] hash: 0000005419-91205b923e5eba84e1c04431367a8a83061b4ebc426410f8b3b34d40248e79ff [Refactored Andrea Vezzosi's cyclicity test (pre-termination check). Andreas Abel **20130518224420 Ignore-this: 51972aea350d631d56b94e97568bb69c Code to extract used definitions reimplemented in Syntax.Internal.Defs. ] hash: 0000009268-bcf698cf420d91d15c3d63df95e793b35b544701e5e8d914a258b6a334ff9377 [Refactor: use Foldable.mapM_, of course. Andreas Abel **20130518234506 Ignore-this: 8ebce5dd05a2cc152b42ade9f89dcf7a ] hash: 0000000618-d31e08c0485e6b6b24cc5e8ab8a9f106cc629b5f8e60385a80c752a6c4c1e14e [Refactor: better interface for getDefs, exposing the Monoid. Andreas Abel **20130519000611 Ignore-this: 97773d78f9bcc284cbd448ac30cb9322 ] hash: 0000002796-24f311575a189c97b907eade06fe013ce5e47486349238cf4bad4d10d8201be7 [Lazy printing of callInfo in termination checker. Andreas Abel **20130519145334 Ignore-this: ef6f70d89c30f68f641928bf5c61566b Saves 12% on the std-lib! Suggested by Andrea Vezzosi. ] hash: 0000002099-c3f7df0fdfadb92c9d05abea5fb6c47be67597f7e184c4928c4b3d775aafcfc7 [Reverted an incorrect (?) modification. Nils Anders Danielsson **20130519151843 Ignore-this: 368bf04b86dbc6b2639e535df25bac30 ] hash: 0000000588-491e1cccc6b9b83581cbccfe352882e9dd9963d9cc36de36a6af8c7133a43ccd [Commented and compacted the code of the compiled clause matcher. Andreas Abel **20130519171910 Ignore-this: 8087193f4f96f654a9625071d0e29def This involves a slight, but according to my experiments, insignificant deoptimization: There might be more test for the empty stack and more prepends of the empty list to the stack which might not get optimized away by GHC. However, the code is shorter, more comprehensible, and avoids cut-n-paste now. ] hash: 0000008440-01b659381e230fe386f01fa7cf72236ff76959bbd2fc3c66e86e43ee3a6fbe46 [Compiled clause matcher: slightly optimized stack pushes. Andreas Abel **20130519175214 Ignore-this: 97df18232a9a757b05a062232d8bdcc2 ] hash: 0000005971-e3702bbdac1d847f3f6c2949a0662fdad9bd1af8ccad5d164df385c5b2cf9609 [Irritating error message oscillation (Issue720). Andreas Abel **20130519172046 Ignore-this: 77f9eda9874373b9f8415d8939f21bee Rollback of a changed error message contained in the last patch. ] hash: 0000001094-6cb391f756eefd8a03c35d645481d1e68eb907eb0d6eb8678502e07d801087dc [A simplifier (issue 850). Andreas Abel **20130519204433 Ignore-this: 6e28bfb63120e32fdb2b5fdef370c156 The simplifier only unfolds definitions if later a constructor/literal pattern is matched. ] hash: 0000014581-4f20321d2ab063379826c932769068c1d0b00ff1f23de735ae17c17039def0da [Put the simplifier behind the normalize command C-c C-n for experimentation purposes. Andreas Abel **20130519205010 Ignore-this: 50d9c7be8fa3bcd305dcbe9690912b98 ] hash: 0000000647-3153bac83ea4a11731770ee5895e2f4d637b0504721eddb9b617ce32ad0e021c [Fixed compilation of Agda (bad code in last patch). Andreas Abel **20130520092951 Ignore-this: c1428bdbe51caf9c80caab034918f510 ] hash: 0000000701-ec039e46bd798d47830f91a3a56d9a44a32a62e2d48c871bbd4bbac357868741 [Switched to simplification (instead of normalisation) in emacs interaction. Andreas Abel **20130520103315 Ignore-this: ae266d841c7feaca1b3682d5ff565bbd This is for experimentation purposes. Key-bindings for full normalisation should also be added. ] hash: 0000000480-6733b4b19a566ceac31f380f650317b957ad92fecbfac19e8f42be6c8354b8df [Fixed issue 852: report all (generated) calls failing termination checking. Andreas Abel **20130520144457 Ignore-this: 9a261e21e050c161365a870477d66541 Behavior is not back to what it was before the lasy callInfo generation suggested by Andrea Vezzosi, but we keep the performance gains! ] hash: 0000006241-1fed3973991cdf610ea996c0330a0bee2d7de036c55f7895f98503595968a4ed