1 patch for repository http://code.haskell.org/Agda: Sun Sep 23 19:34:40 CEST 2012 Dominique Devriese * Fix dependency on directory-1.2 which does not currently compile on GHC 7.4 New patches: [Fix dependency on directory-1.2 which does not currently compile on GHC 7.4 Dominique Devriese **20120923173440 Ignore-this: bb79cc9d226417054e957e2009af5dc0 ] hunk ./Agda.cabal 92 if flag(old-time) build-depends: old-time >= 1.0 && < 1.2, directory >= 1.0 && < 1.2 - if !flag(old-time) + if !flag(old-time) && impl(ghc >= 7.6) build-depends: time == 1.4.*, directory == 1.2.* hunk ./Agda.cabal 95 + if !flag(old-time) && impl(ghc < 7.6) + build-depends: time == 1.4.*, + directory == 1.1.* build-tools: happy >= 1.15 && < 2, alex >= 2.3.1 && < 3.1 Context: [Testcase ensuring proper treatment of irrelevant indices in data types. Andreas Abel **20120921134550 Ignore-this: d88b693817f9a73561e147d3decd562e ] [Propagate irrelevance info to dot patterns. Andreas Abel **20120920151230 Ignore-this: a11952721e0973d8f755384d4914902c ] [Forcing should not overwrite irrelevance. Andreas Abel **20120920151140 Ignore-this: 6f08857c568d6887d1e6dcf9ac84ad2a ] [Added new builtin Size< (SIZELT) to enable new style of sized types. Andreas Abel **20120920082336 Ignore-this: 1ab629046008c4ea8c7bcbdcda67219a Seems to work for inductive types, but for corecursion we first need a proper implementation of copatterns in the core. (See test/succeed/SizedCoinductiveRecords). ] [Fixed unbound deBruijn indices in termination checker. Andreas Abel **20120920080434 Ignore-this: 7ea2d1faeb7b4957254459f73e7357fc Function clauses are opened properly now. Adopted code from Coverage.Match. ] [Refined positivity analysis: recognizes co- and contravariance now. Andreas Abel **20120920080323 Ignore-this: 8226fabbd9ab0ceac986baafbc030f83 This info is used by polarity checker. ] [Positivity refactoring: renamed Positive to StrictPos and Negative to Mixed. Andreas Abel **20120920070044 Ignore-this: fdbc232b015e82dc7b257c31ba498f56 To prepare for a finer analysis. ] [Named the fields of the Permutation record. Andreas Abel **20120919214917 Ignore-this: b694eed455940e3394d9a50a18b4b64 ] [Fixed: definition created for absurd lambdas violated Clause invariants. Andreas Abel **20120919214810 Ignore-this: a1262cbb71aba1214d83dd3cf48345db ] [Refactoring: moved argOccurrence and polarity from Defn to Definition. Andreas Abel **20120919174430 Ignore-this: 1bf531d78b3147aab9dfede6993caf6a Now it is easier to assign polarity and positivity info to builtins. ] [A test case ensuring we get the reduced constructor type in reification (InternalToAbstract). Andreas Abel **20120918131156 Ignore-this: 575007d778495ec66082db65ecd154c ] [Rollback removal of phantom arguments from testsuite. Andreas Abel **20120918123108 Ignore-this: 44dc996d68936e5c7a3efdbf06bf570f ] [Inessential changes to files in the testuite. Andreas Abel **20120918122843 Ignore-this: 40a841b3e70cd63eff2ba100044e3d10 ] [Started to remove uses of phantom arguments in testsuite. Andreas Abel **20120918122731 Ignore-this: 253914c84a0813a256668e3eb8087a52 ] [Addition of polarity Nonvariant and relevance UnusedArg. Fixing issue 44 and 691. Andreas Abel **20120918122216 Ignore-this: 44cbedc4b2487959d6e6b42109fe9ffa Agda thus recognizes unused arguments in defined functions. See release notes. ] [Fixed most of the contexts for printing tc.with debug messages. Andreas Abel **20120917151503 Ignore-this: f4d18b86502ff8c1e3b9116da8b4c983 ] [Fixed and extended documentation for permuations. Andreas Abel **20120911184829 Ignore-this: 5b337848a41601652b78af843be80928 ] [Code for new polarity Nonvariant. However, it is unused still, so no outside effect. Andreas Abel **20120910092918 Ignore-this: 5799c470dcfa7f5874e43898ca47ffaf ] [Tests for algebraic properties of Relevance composition. Andreas Abel **20120918085848 Ignore-this: 291a24718e6566cd780555a8092b4121 ] [Fixed a bug I introduced with the fix of 611. Andreas Abel **20120918074753 Ignore-this: c2ce5a8761c24b77589440a182d44608 Constructor parameters should only be skipped during reification if the first regular constructor argument is not hidden. Otherwise, a parameter could be confused with a hidden argument of the same name, as in Data.Star. data Star {i : Level} ... where ... : {i : I}.... ] [A test case refuting that we can make constant functions into irrelevant functions. Andreas Abel **20120915210231 Ignore-this: 6b27c69679d9c54bed607b4034f8567c (Without running into problems with the current constraint solver.) ] [Added a comment why builtin FLAT must be monotone in its argument. Andreas Abel **20120915205912 Ignore-this: e36f4b05eef3cefc14fa115532a474e ] [Additional debug messages printing type of with function in raw. Andreas Abel **20120915205735 Ignore-this: c0472041547731ea6dfaed18b7f3becc ] [New auxiliary function that checks whether an Internal.Pattern can block a match. Andreas Abel **20120915205604 Ignore-this: e81096a682240a8acf953aef435ae5fd ] [Cleaned up import list in Termination.hs. Andreas Abel **20120915205226 Ignore-this: 7534a65bcb383f3b831935904efd1c1d ] [Bugfix in InstanceArguments: Candidates blocked by an unsolved meta were discarded too early. Andreas Abel **20120915204759 Ignore-this: 5245f960469441ed987235fe3efc4072 ] [Subtyping: allow conversion of an irrelevant function to a relevant function. Andreas Abel **20120914113304 Ignore-this: 1ab77b4184e17100f8c5c52dd5ed8bf7 ] [Properly propagate irrelevance info to meta-var creation. Andreas Abel **20120913092156 Ignore-this: e2a49b059ab23b76a904708c6023dfb5 Fixes new case test/succeed/Issue168-irrelevant.agda. ] [Fixed a bug in the positivity analysis for data type indices. Andreas Abel **20120913075235 Ignore-this: 6f202a42387dac4be466bfc8d7096807 ] [A Show instance for Comparison. Andreas Abel **20120913074959 Ignore-this: 5015e66828ebbd9ed23d6497d4e6d3dd ] [Extended debug message for conversion of irrelevant terms. Andreas Abel **20120913074530 Ignore-this: b1e4289914ebe121eccbea5eaffe45ac ] [Auxiliary function to compute variable list from Internal.Pattern. Andreas Abel **20120913074400 Ignore-this: 2bac64bb62d34ad763d12544d2a08af8 ] [Signature auxiliary functions. Andreas Abel **20120911185313 Ignore-this: 8eeb5b6e4dfc93e02650cca189f098a8 ] [Micro-optimization: downFrom instead of reversal. Andreas Abel **20120911185231 Ignore-this: ed4ac8f0b5dcb7f1ed0e8d954dc630f4 ] [Debug message for with type moved to tc.with.type. Andreas Abel **20120911185057 Ignore-this: e8366bcf421f141f5cd11dd3164a26da ] [Auxiliary functions to manipulate Arg components. Andreas Abel **20120911184714 Ignore-this: a9857ce9854f8b9a07d594e111c50f40 ] [Removed an optimization in getPolarity' to accustom non-variance. Andreas Abel **20120910092630 Ignore-this: 5c554a706d7788d5a4f3aa2459fa025b ] [Some changes to polarity computation for sized types. Andreas Abel **20120910092412 Ignore-this: d3edb6ada431256398567ad60f4c4e54 ] [New auxiliary function getArcOccurrences. Andreas Abel **20120910092107 Ignore-this: b0546de1da0d8ae1283f3362c6789b38 ] [Removed commented-out line. Andreas Abel **20120910091944 Ignore-this: b609db0614ef0fbb999476caaac51b92 ] [Positivity checker now considers a function argument that is matched upon as used (Negative). Andreas Abel **20120907182258 Ignore-this: 8174318dd088c48f31e41b2f13238ffa No visible change on the test suite. This change is necessary for a better polarity analysis. ] [Adding Lift to Common.Level. (Taken from std-lib.) Andreas Abel **20120907180222 Ignore-this: d2cbb1fdfa322f07697b2d8a36304e2a ] [Failing test case to secure against unsound polarity analysis for data parameters. Andreas Abel **20120907180109 Ignore-this: 1af342276e9c6f73d6df6f82b3a8be24 ] [Added functionality to free variable collection: possible to ignore variables in the sort annotations in types. Andreas Abel **20120907175531 Ignore-this: 4cd0207b3dca90667210c359d2b42b11 ] [Added fail test associated with the fix of issue 690. Andrés Sicard-Ramírez **20120907123441 Ignore-this: 4cdc8cb825a8ba3de647cb26fc648985 ] [Support for GHC 7.6.1. Nils Anders Danielsson **20120907121117 Ignore-this: 69d48c1560be1f56912d2733070058e0 ] [Fixing issue 690. Positivity checker now also looks in data type indices for occurrences of data type parameters. Andreas Abel **20120906172744 Ignore-this: ba80a5796551c82008d05b778214fd65 That prevents, e.g., equality to be classified as strictly positive in its left argument. ] [Removing an unnecessary instantiateFull in the termination checker. Andreas Abel **20120905142945 Ignore-this: 13b7f5bffea76760df3b23c01f47889d ] [Fixing issue 655: definitions of the form `name = expr' should not produce unsolved metas. Andreas Abel **20120904211627 Ignore-this: ba59fd00f87bbfe81c583a094ccc99bd ] [New pretty priniting Doc: equals. Andreas Abel **20120904211405 Ignore-this: 5f8fc34c40ff41cdab4e52f5129099c7 ] [Cosmetic refactoring --- common subexpression. Andreas Abel **20120904210354 Ignore-this: e3a8f018ab8e1e6c06fd291dfcb49052 ] [Prevent no-builtin-level errors in termination checkers use of unLevelView. Andreas Abel **20120904210213 Ignore-this: 4916546da7bfe06f3c2fa509aebce383 ] [Whitespaces in example file. Andreas Abel **20120904205908 Ignore-this: 762b2d07fa7baec78d9fe6998aebd746 ] [Whitespaces in test suite files. Andreas Abel **20120904205548 Ignore-this: 5aaf8049f5d1f33e04247a55a2bcbb1b ] [Fixed bug: \GTH generated θ rather than Θ. Nils Anders Danielsson **20120824111708 Ignore-this: ed99d3fe833432c4c8a2351a7dfdc115 ] [Added test case for -Werror override (issue 687). Stevan Andjelkovic **20120821100044 Ignore-this: 6e3b5286a5bfab5ec7d03dc85e4e790c ] [Make -Werror overridable. Stevan Andjelkovic **20120820131605 Ignore-this: 8b0eb262399e00dc26949e19278886e1 ] [Updated tested-with fields. Nils Anders Danielsson **20120817213508 Ignore-this: 4000c80bf3b3a7dd922e5f9a8cc5b912 ] [Removed -O flag from Cabal file. Nils Anders Danielsson **20120817192059 Ignore-this: 74baad28b1429d587aae26c93463836c ] [Restored old, more performant termination check for the non --copatterns case. Andreas Abel **20120818192917 Ignore-this: a85964b4bc2042ff5230dbe031dbdb2b ] [Some more debug printing for instance search. Andreas Abel **20120818183729 Ignore-this: cc4f9ddd1098d3ec9b3e0a9a30e3ddf6 ] [Workaround for Emacs 24.2 warning. Nils Anders Danielsson **20120817183511 Ignore-this: 5c8a7a5e596ebce3fe8bd18d2216f2bd ] [Fix for issue 685 (wrong order of scope checking for pattern lets). Andreas Abel **20120816172502 Ignore-this: e42be16a6555a1bc1c260ee049f79fe8 ] [Support for haskeline 0.7.*. Nils Anders Danielsson **20120810125101 Ignore-this: 28f6bf62777937b40b2131f9b344d86d ] [Release note documenting the fix for issue 679. Andreas Abel **20120802164528 Ignore-this: 80208f41c5911482dd45079845baef51 ] [Fixing issue 679 by a strategy change: do not always eagerly introduce implicit arguments. Andreas Abel **20120731185240 Ignore-this: afa89c2949d79ff4097024c9d0bc71f0 Trailing implicit arguments on the lhs are now only introduced: * if other clauses have trailing implicits, to restore uniform arity * for checking the where clauses Trailing implicit arguments in with expressions are now only introduced if the type of with expressions thus becomes a data or record type. (This is necessary to enable pattern match on with expressions.) As one consequence, goals are now displayed with hidden quantification instead of with fresh metas. ] [Removed uncommented duplicate code. Andreas Abel **20120731184138 Ignore-this: b09c6dc1dbd4f935c4ed7b3a9bd1593 ] [Cosmetics, removed unused bind/return. Andreas Abel **20120731184016 Ignore-this: b08bfd2d92267323ad10a3542accdbee ] [Coercion for lambdas but not for hidden lambdas. Andreas Abel **20120731183902 Ignore-this: 2778d9cfc0b85807bd2847241ca7778e ] [Made the coerce function, a stub so far, a bit smarter. Andreas Abel **20120731183512 Ignore-this: 726635cb06b8192abf4b1a0c7a3cf0f4 It now inserts implicit arguments, if safe to do so. ] [Make TypeChecking.Implicit importable in e.e. InstanceArguments. Andreas Abel **20120731183215 Ignore-this: 94041bc3fc3145170f78b0b7ec54af9a ] [New refinement of telView to take partial telescope off type. Andreas Abel **20120731182821 Ignore-this: c1e8726ae0477e3832f39c23958546b4 ] [Type synonym for A.Patterns. Andreas Abel **20120731182357 Ignore-this: 317581d1c2e84c85394b15bc2866425f ] [Handle introduction of only implicit lambdas by refine tactic. Andreas Abel **20120731182319 Ignore-this: b485a6ef7a25e3f8b64890a71deb8bb8 Produced a parse error before. (That never surfaced it guess, due to eager introduction of hidden fun spaces.) ] [Refactor: Moved ExpandHidden type to Monad.Base. Andreas Abel **20120731065338 Ignore-this: ffef6647db56c24bb3dbe3d20371a52f ] [Factored out implicitArgs from checkArguments. Andreas Abel **20120730205147 Ignore-this: c0b9ead6d91e2f3741373f0d33367167 implicitArgs can be used to create implicit arguments for eliminating hidden/instance function types. ] [Refactor: One more use of ifBlocked. Andreas Abel **20120729201046 Ignore-this: 521086bd03e70883e8f4b36c27f56543 ] [Introduced a combinator for checking whether a term/type is blocked. Andreas Abel **20120729200120 Ignore-this: 9759f821d47fd51d6d437935721fd277 Refactored some code to use this combinator instead of a case distinction. ] [Retired duplicate function telViewM. Andreas Abel **20120729184752 Ignore-this: 7a88f8565c3c300f1b1a536a831c19b7 ] [Constructor parameters are now reconstructed by the --without-K check. Nils Anders Danielsson **20120726221755 Ignore-this: bf5482910a0d21d677600d956c41ba1 ] [Replaced ` with \` in some Haddock comments. Nils Anders Danielsson **20120726075732 Ignore-this: c99326bafcd839f8c3a47f73786ffdf0 ] [Avoid creating the info window to the right of the code window. Nils Anders Danielsson **20120605133318 Ignore-this: 41c019e083299bc9eb76240289af53a0 ] [If AgdaInfo was selected, then a /second/ AgdaInfo window was displayed. Nils Anders Danielsson **20120605132218 Ignore-this: ceca9c7385fc2d31d7750b305a7149ab ] [Fixed internal error when unsolved size constraints in type signature. Andreas Abel **20120726083731 Ignore-this: 3d9076c3412686d6e207af6e88e6c464 ] [Fixed issue 678. Coverage checking no longer bound to left-to-right splitting order. Andreas Abel **20120726073626 Ignore-this: 2567cf8b3a56b972e2bd38fd3c7dcb71 If there are several variables blocking a match, the coverage checker no longer only tries to split the first variable. It will now split the first variable that can actually be split. ] [Fixed error message changed by patch for issue 680. Andreas Abel **20120724224120 Ignore-this: df5881efe523057ce6a61dc617d37aac ] [Fixed context to display coverage errors. Andreas Abel **20120724221345 Ignore-this: 19879f0c228c1a444edd4297a0c47fd ] [Printing of shape irrelevance annotation .. in non-dependent function types. Andreas Abel **20120724161949 Ignore-this: bb4223fca423a3533f7cc3ea023c2884 ] [Fix issue 680: compare neutral levels correctly. Dominique Devriese **20120724082318 Ignore-this: f1156dbf5ef0fc5a12b0dcf8d7d34dc3 ] [interface version needs a bump for 676 fix ulfn@chalmers.se**20120712104122 Ignore-this: 74fdfd727b7e8ce8138f91a8baecb55e ] [fixed issue 676: functions with absurd clauses can't be projection like ulfn@chalmers.se**20120712095434 Ignore-this: 23c002713ae4a5325d8b0582d3aed7b1 ] [Fixed issue 675: Qualified constructors should also work in hidden and instance patterns. Andreas Abel **20120711131307 Ignore-this: 800ef55a890f611825d4c37c77714487 ] [Replaced foldl by fold' where it made sense. Heap savings neglegible. Andreas Abel **20120707104924 Ignore-this: 4e8e76805eacf293afd050bbd3b9d2a0 ] [Fixed issue 674. Modules with instance arguments can now be opened. Andreas Abel **20120707092237 Ignore-this: c6027955c846de1c32f7e4782e04f243 Old code tried to access names that were already in scope, due to open, but not yet in the signature. Now this error is caught. New code also avoid looking up the same symbol three times. ] [Concrete.appView now also recognizes instances args. Andreas Abel **20120707074803 Ignore-this: 1363e156a680d69835f303b0c4e15213 This fixes part of issue 674: We can now process: open M {{inst}} bla ] [QuickCheck 2.5 support (patch by Dirk Ullrich) ulfn@chalmers.se**20120703143544 Ignore-this: bc72ae967d30a372c770cd37682c1343 ] [Fixed issue 672: print parentheses around applied extended lambda. Andreas Abel **20120702072417 Ignore-this: 5385410ec8045727a37494d383c3537a ?? {(x ??? xs) ??? x} v is now printed as (?? {(x ??? xs) ??? x}) v such that it can be parsed. An alternative would be to change the parser, but that is not trivial: To accept ?? {(x ??? xs) ??? x} v, extended lambda would have to be parsed very different from ordinary lambda. ] [Fixed issue 671: Panic after pattern-let. Andreas Abel **20120701180019 Ignore-this: 383bf3589471efa7e714a5c3cf7552bc Now properly reparing the context after checkLeftHandSide. ] [Fixing issue 670: Making sure that constructor found by instance search is not applied to parameters. Andreas Abel **20120701173544 Ignore-this: adbbcde514a1fa48c2b70c88e83eff61 ] [Fixing a debug print message. (Minor) Andreas Abel **20120701173441 Ignore-this: ccb272b6c54f513a357c730ec00fbd3a ] [Skip check whether value equal to instantiation when giving to irrelevant meta. Andreas Abel **20120630055513 Ignore-this: 4bf47a99926909df657e0bd82daba122 This fixes the buggy behavior originally reported in issue 670. Issue 670 is deeper and stays open. ] [Fixed a bug in reifying a constructor with only parameter arguments (like refl). Andreas Abel **20120629203320 Ignore-this: 42e05065843e9cd449ceaf84ee66ee48 ] [Copattern translation now works also if clauses of a group are not adjacent. Andreas Abel **20120629175229 Ignore-this: 456fef54f1b4de60173ef873818a3b36 ] [Coinductive constructors are only guarding for definitions which are delayed, i.e., defined by copattern matches. Andreas Abel **20120619184622 Ignore-this: 2b29b474443c9cc103a1a1ce0e497ec0 ] [Testcase to ensure that inductive records are treated as such by the termination checker. Andreas Abel **20120619184420 Ignore-this: e15ade66d3f84f02ec22d7d611cd0b04 ] [Use Common.Coinduction in test case instead of copied definitions. Andreas Abel **20120619184233 Ignore-this: 464346adabe09528eb9afc4b1b102146 ] [Fixed haddock issue. Andrés Sicard-Ramírez **20120611150013 Ignore-this: d289c4560459a7a825038654c306bffb ] [Replaced NubList again by a simple list of TerminationErrors. Andreas Abel **20120619145805 Ignore-this: 12544720d368c0ec74ccda6e1fc49ca3 ] [Termination checker now correctly rejects infinite objects in a mu-nu type, if defined via copatterns. Andreas Abel **20120619145205 Ignore-this: 382329378a3d7a4970167ba861faf218 The termination checker now only counts coconstructors as guarding if they belong to the record type that is mutually recursive with the target type of the function it is currently checking. For example, this code, taken from Nisse and Thorstens PAR 2010 note, is no longer accepted (see test/fail/ColistMutual.agda): mutual data CoList (A : Set) : Set where [] : CoList A _∷_ : (x : A)(xs : ∞CoList A) → CoList A record ∞CoList (A : Set) : Set where coinductive field out : CoList A open ∞CoList data Tree : Set where node : CoList Tree → Tree mutual bad : Tree bad = node (node [] ∷ bads) bads : ∞CoList Tree out bads = bad ∷ bads In this case, the coconstructor for ∞CoList does not guard function bad, since it has target Tree which is not mutually recursive with ∞CoList. To achieve this with minimal changes to the termination checker, it now checks each function in a mutual block individually. Caveat: this leads to a 15% loss in performance on the standard library. The performance loss is only transitional during the experimentation stage. If the new termination technique solves the problems of the previous termination checker, we can implement a new call graph generation which does not have the current waste of performance. ] [Use Data.Function.on instead of hand-knitted one. Andreas Abel **20120619143004 Ignore-this: 7a988f752cb3735dc54e808348a1fdf6 ] [isRecordConstructor now also returns the name of the record. Andreas Abel **20120619093000 Ignore-this: b7503d4e13dfbc576a101fdc702e0bb2 ] [New: terminatesFilter: termination check only one function in a callgraph. Andreas Abel **20120619092837 Ignore-this: 77b38500f813368aba077c73335b41b8 ] [Tiny refactor: take suc from conf. Andreas Abel **20120619074257 Ignore-this: 60c0713249592706fa469b6ed5807e89 ] [Updated interaction test output for positivity checker. Andreas Abel **20120619070444 Ignore-this: eca24bd77d79c6db8bec0c01ccfdec1b ] [Some comments and refactoring in the termination checker. Andreas Abel **20120619070308 Ignore-this: 346200c4bb78c8dfc1d3ba0842b50c7a ] [Refactor: replaced collectCalls by mapM', which is a generalization of mapM_ to a monoidal result. Andreas Abel **20120618124123 Ignore-this: 86814f775dbc45b9b7026c48d5b554f7 This is just for code comprehension. No visual outside effect. ] [Store which data/record/fun is mutually recursive with which def. Andreas Abel **20120618120526 Ignore-this: 3799a03d379f4f5eca565ca826b9db92 Obtained from the occurrence graph via strongly connected components. No visible effects on the outside yet. ] [Coinductive records. Andreas Abel **20120615103221 Ignore-this: 28bc2c1b0dd83a2b7a582ad280ceecc6 Added new keywords 'inductive' and 'coinductive' that can appear as first declaration in a record definition. record Stream (A : Set) : Set where coinductive field head : A tail : Stream A Default is 'inductive' for backwards compatibility but maybe we want 'coinductive' as default? Members of a coinductive record can be defined via copattern matching. Copattern translation does not yet check whether the record is not inductive, thus, termination checking is yet unsound. Will be fixed later. ] [Custom Show and a HasRange instance for Induction. Andreas Abel **20120615093605 Ignore-this: 65a5d886a1bbaa88acddff688930045d ] [More tuple auxiliary functions. Andreas Abel **20120615093428 Ignore-this: 5374c3b3c1a0910c3f4fbacbe74c379 Lazy matching idea taken from Data.Tuple.HT. ] [Introduced type alias Abstract.Field. Andreas Abel **20120615093134 Ignore-this: 226ee6255badefaffffecc1adeb81e0d ] [Removed unused type alias Concrete.Field. Andreas Abel **20120615091048 Ignore-this: 245c83514c684e545792840406617201 ] [Store in signature whether a record type is recursive. Andreas Abel **20120610214811 Ignore-this: 9987a34c3840457e1824eb2de004be2b Projections of recursive record types are not size-preserving. This fixes a bug in the termination checker. ] [Only eta expand implicit patterns of guarded record types. Andreas Abel **20120610160619 Ignore-this: 97c76e9092a9e937be3140c63636b36c Otherwise, we loop. ] [Tiny optimization: use lazy monadic conjunction. Andreas Abel **20120610160454 Ignore-this: afa423dfcc7b5db9f5c30bd335df5562 ] [Termination checking for shallow copatterns. Andreas Abel **20120609232210 Ignore-this: 23eebe69efaa39926c676eebed4ef802 For delayed definitions, we start by assuming guardedness, which is preserved by projection of guarded record types, but not by projection of unguarded types. ] [Extended positivity check so that it spots unguarded recursive record types. Andreas Abel **20120609231529 Ignore-this: c5292a0fce6be3a058e851408dc0d766 No eta-laws are applied to records of unguarded record type. This fixes issue 402. TODO: add pragma NO_ETA to mark ungarded records in the source. (The silent automatic classification is not very nice.) ] [Library functions: Monadic conditional execution if Maybe is Just. Andreas Abel **20120609230212 Ignore-this: fbe5879607fb711eed3ef87e8f137578 ] [Added a comment to explain allPaths. Andreas Abel **20120609230117 Ignore-this: 5a36d7d41d9697f219bfe5ef85f76716 ] [Refactoring: generalized result of isDataOrRecord. Andreas Abel **20120609124928 Ignore-this: ce42280149fcf738e95bde4010a11934 ] [Refactoring: added a new Occurrence GuardPos which means strictly positive and under an INF. Andreas Abel **20120609120807 Ignore-this: 78274dae864685849502ac1a6bb7373 No changes visible on the outside. ] [Refactoring: computing occurrences in positivity checker could now refer to builtin INF. Andreas Abel **20120609120401 Ignore-this: 14c756bf61077c89598abbe94df54ca9 This is to prepare for a positivity check for recursive records. Main change: made occurrences monadic, for a reader monad. ] [Moved coinductionKit to TypeChecking.Monad.Builtin to avoid a further module cycle. Andreas Abel **20120609115711 Ignore-this: fd516a4619d55d58336a2b6b26af14af ] [Fixed bad module path in testcase succeed/Issue387. Andreas Abel **20120609105658 Ignore-this: a2c570830380ea717cc3db2d989e9708 ] [Updated error location for issue 183. Andreas Abel **20120607190240 Ignore-this: 15b98ece2bb9276337125d941f032ce ] [Fixing issue 387: do not check record fields twice anymore. Andreas Abel **20120607190158 Ignore-this: 2decc4c54dc7e4fe8176ee4696eee866 Instead, reuse the already checked type of the record constructor to construct the record projections. Gives also small performance benefit, since less metas are created. ] [Updated error message after fix for \ _ -> identifier naming. Andreas Abel **20120605181701 Ignore-this: fbff03a4bb60de895a58e1501ff0167d ] [When type-checking a \ _ -> ..., take name from type instead of using _. Andreas Abel **20120605161140 Ignore-this: 451b174466d65a227ecfa41c0986f22c Fixes Issue630. ] [Release notes and some code clean-up for let patterns. Andreas Abel **20120605135846 Ignore-this: 5b27c9fe11d906c063c87dfb747a9ba3 This closes issue 627. ] [Removed question. Nils Anders Danielsson **20120605122258 Ignore-this: e6f825ba6cab4c83d263cbef93deb5a8 ] [Implemented let bindings for irrefutable patterns (i.e. record patterns). Andreas Abel **20120605105630 Ignore-this: 7ee8e90e9816cbcbb81f8c80ed639a44 Example: let x , y = t in u Release notes will follow. ] [Concrete to abstract for let pattern bindings. Andreas Abel **20120604135343 Ignore-this: 92feb725710b3971ec04709cf7669f85 T.C. not yet implemented. ] [Fixed error message for Issue87. Andreas Abel **20120604114724 Ignore-this: bb71ee73aa307806365d2d82418156a3 ] [Refactoring: Merged the three parsers for pattern, lhs, and copatterns into one code. Andreas Abel **20120604101014 Ignore-this: 8bf763a3b4106ed9b33061c35bb002a2 The module Syntax.Concrete.Copatterns is now obsolete and has been removed. ] [Better error message for unsupported let syntax where lhs is a pattern. Andreas Abel **20120602080925 Ignore-this: 527ba8fde3d9b87b4004f4686527fd39 This is a first step towards implementing let (x , y) = e syntax. See issue 627. ] [typo in error message for inaccessible patterns noam.zeilberger@gmail.com**20120603153940 Ignore-this: 43bf7d4bcb951b2a9fc0d951ea376cc2 ] [Fixed issue 661: Constructor application checking was not invoked when constructor came from a module application. Andreas Abel **20120601093007 Ignore-this: c28a77354e20a9ef5d84f3b1663e12aa ] [Added a trivial Reify instance for A.Expr. Andreas Abel **20120601092804 Ignore-this: 6139601caf5b2a80d38980e0688105b1 ] [Fixed issue 659: Better error message when universe consistency in sorts causes type conversion to fail. Andreas Abel **20120531124515 Ignore-this: 4a87a3c0db90d8405aca6da24b54c019 ] [Adam found the problem causing files using pattern synonyms not to be cached. Stevan Andjelkovic **20120528134818 Ignore-this: 35eaf5dc49ad53f533d9135288be8a2f ] [Disallow pattern synonyms in mutual blocks. Stevan Andjelkovic **20120528125831 Ignore-this: cfd72102ae94cb4cf024d41b6b0734e0 ] [Added diagnostic message for broken interface files (-vimport.iface:5). Nils Anders Danielsson **20120525160822 Ignore-this: b32a4d84f4d9e62470ef51ef879a8459 ] [Added ($+$). Nils Anders Danielsson **20120525160628 Ignore-this: fedf6e019d09fe98728a267dde55f1b7 ] [Support for implicit arguments for case-splitting pattern matching lambdas csfnf@swansea.ac.uk**20120524121328 Ignore-this: 66f331a39e4a2dbf48210247230fe565 ] [Case-splitting for parameterised pattern-matching lambdas csfnf@swansea.ac.uk**20120516155653 Ignore-this: 784165d539d043d7fbb2390d176e7d3 ] [Allow eta-expansion of frozen metas. Fixes issue 658. Andreas Abel **20120523205316 Ignore-this: e8c536130166b36a3ca479ddd89a1f6c ] [Reactivated go-to-definition for ambiguous constructors used under sharp. Nils Anders Danielsson **20120523180256 Ignore-this: ba915b3e10c1c6577a2d153b0a2837ff ] ["Impossible" errors should not lead to termination of the Agda process. Nils Anders Danielsson **20120523120901 Ignore-this: cfb86eea9c348ff5585cf018e221dd76 ] [Tried to fix a potential bug. Nils Anders Danielsson **20120523115232 Ignore-this: 3084a7302d969110f96f8de58bcfff0f ] [Added some comments. Nils Anders Danielsson **20120523115139 Ignore-this: bc7f6774f81152fb038ad8b29288d47 ] [Execute `solveAll' actions with the lowest priority. Guilhem Moulin **20120523074232 Ignore-this: 3c19a5d7d264bfa1d3ebf85caa656ba7 This fixes Issue 654. ] [Make the ranges precisely correspond to all the parsed tokens. Guilhem Moulin **20120522215011 Ignore-this: 9b7402433e04444460b9f262c95ab238 This fixes Issue 626. ] [Support for mtl 2.1 and containers 0.5. Nils Anders Danielsson **20120509134532 Ignore-this: 641242540f0f83590d233341c305f28e ] [[issue 643] fixed: problem with display forms for record projections ulfn@chalmers.se**20120516141313 Ignore-this: d09a4e45ad214527ecf595521590484d ] [[issue 642] fixed display form issues with open public in parameterised modules ulfn@chalmers.se**20120516124226 Ignore-this: f1ebb0f6a5e6f0bb58dcab58177dace7 ] [[interaction test] |& only works in bash 4, using 2>&1 | instead ulfn@chalmers.se**20120516102355 Ignore-this: baaa7d2bd9b2eff8c1cf2b40ef123625 ] [Updated fix for issue 637. Nils Anders Danielsson **20120515133459 Ignore-this: 32fe67e4a351b5e2861087bba18e63c4 ] [Fixed bug: Some highlighting wasn't interrupted by buffer modifications. Nils Anders Danielsson **20120515130718 Ignore-this: 38845c2e9656f9206ec1e18ddaf43ef4 + Moved agda2-highlight-in-progress and agda2-highlight-load-and-delete-action to agda2-highlight.el. ] [Fixed issue 637. Nils Anders Danielsson **20120515122517 Ignore-this: 9ed73dd3b4e4abaa85871c49ec4ffe85 ] [Documented retrieveCoconstructor. Nils Anders Danielsson **20120514092807 Ignore-this: ba73ef4bf194ade6d42198ed593cb177 ] [Added a comment inserted by the HCAR editor, Janis Voigtländer. Nils Anders Danielsson **20120514085221 Ignore-this: 93e8d23b9af4becdddf240763f55a214 ] [Fixed issue 636. Andreas Abel **20120514062824 Ignore-this: e526936d0cfa16a3f141efa24da150f2 ] [Copattern matches are translated as delayed function definition. Andreas Abel **20120512222036 Ignore-this: 1d8d8ae1f46986b6dd651ac16cd1e2a8 This enables depth-one copattern matches without running into divergence. The termination checker is not up to this yet. The use of Delayed for things not generated by \sharp makes retrieveCoconstructor in Highlighting.Generate loop. I cannot debug this, since the generated function universeBi is involved whose code I cannot inspect. ] [Fixed issue 631: instance search was considering wrong candidates when type conversion postponed. Andreas Abel **20120510185541 Ignore-this: 9d6a118e6de8ceb083465d69420df988 ] [Test case to prevent overzealous pruning. Andreas Abel **20120509220305 Ignore-this: 645251acd28c3330343e2634efde2fe4 ] [Undid an optimization in my fix for 629 which lead to unsound pruning. Andreas Abel **20120509214717 Ignore-this: 90e134504494a78b5cd6c096a2578db4 This was discovered by library-test. ] [Fixed issue 629 by attempting pruning for all lhss that are not solvable. Andreas Abel **20120509212632 Ignore-this: 6de3ff7c031d147f6dce4be74dd75a06 Issues with imprecise free variable analyses due to not unfolded defs remain, as described in the comments to issue 629. ] [Copattern translation can now handle variable patterns in copatterns. Andreas Abel **20120509090346 Ignore-this: 4acc431641215ff25898e9629fc5e993 ] [Added to Utils.Tuple: map only over fst or snd component. Andreas Abel **20120509090218 Ignore-this: 826396931f111733b44e8f0604f3f1c3 ] [Added an item. Nils Anders Danielsson **20120509143124 Ignore-this: 673a8ca19b7f79bec4e94ad24be78fda ] [Added a version constraint for the Win32 package. Nils Anders Danielsson **20120509133839 Ignore-this: 5e17b976d1b7b451dfe4001a084d1d99 ] [[issue 628] the NATDIVSUCAUX builtin is no longer broken ulfn@chalmers.se**20120509113125 Ignore-this: 59e1573705d9491c08dc0e64db32480f ] [benchmark run ulfn@chalmers.se**20120509110238 Ignore-this: 41a1dde29d5cb37c392f13180395deb7 ] [[issue 453] updated test/fail and test/interaction outputs to account for fewer metas generated ulfn@chalmers.se**20120509105615 Ignore-this: 31d56ac9114cf323cc718be1f33dc3ec ] [[issue 453] fixed, the cause was unnecessary generation of sort metas ulfn@chalmers.se**20120509105259 Ignore-this: a7bff15af743b699d2b4d5379f27867 ] [Copatterns mixed with variable patterns are now translated, if only one clause per pattern. Andreas Abel **20120508214302 Ignore-this: 16775cf861a75ae8617c3cbc547c646e ] [Copatterns: Optimized lhsToPath by introducing an accumulator. Andreas Abel **20120508144143 Ignore-this: a7942e5a0bd45834f7808d12fd8962e ] [[issue 620] added test case ulfn@chalmers.se**20120508065829 Ignore-this: 370cae61399a201b2fb936ce6a53aa94 ] [fix pretty printing of qualified operators darinmorrison@gmail.com**20120508022519 Ignore-this: 4f804e931ed0d352fea5d92862c1bccb ] [Fixed a highlighting bug: Some tokens were not always highlighted. Nils Anders Danielsson **20120507171606 Ignore-this: e434dda34baecfadfc7107178b7c3419 ] [updated Error-in-imported-module and Issue388 interaction tests after fix for issue 622 james@cs.ioc.ee**20120507122542 Ignore-this: d5ccdbcc5734a1207dca45319573d67b ] [Tried to fix issue 622, with some help from Guilhem Moulin. Nils Anders Danielsson **20120507114727 Ignore-this: 17cd4c50d331da4527b6971db4c33b90 ] [Added lastTag. Nils Anders Danielsson **20120507094745 Ignore-this: 39da47f70b4bdece5c41eeb47a9f7869 ] [Tried to make Agda build under GHC 6.12.3. Nils Anders Danielsson **20120507112744 Ignore-this: fbf1b5f5bc189aad8643af653ef89a47 ] [modified benchmarch/emacs to work on OS X james@cs.ioc.ee**20120506060926 Ignore-this: f91688322edc9553e7d0f67cc20e6fbb ] [Removed temporary note. Nils Anders Danielsson **20120506075237 Ignore-this: 955b7b03ea0e515d6a52dab3c984653b ] [The default highlighting level is now "non-interactive". Nils Anders Danielsson **20120505233931 Ignore-this: 841705bdf00db25062f5d21ba61f41a1 + If interactive highlighting becomes much faster we may want to change the default again. ] [Modified a comment, made a cosmetic change. Nils Anders Danielsson **20120505232709 Ignore-this: cb2f9031e2481c2d7cc779af55826c60 ] [Optimised non-interactive highlighting. Nils Anders Danielsson **20120505232340 Ignore-this: 2a98b494d2ae0e0fc628429c27985ec4 + Passing large chunks of highlighting data via files seems to be much quicker than sending the data through agda2-ghci-filter. ] [Removed outdated comment. Nils Anders Danielsson **20120505220450 Ignore-this: 3a05e33acadb1c0877fbeb217070932e ] [Added agda2-measure-load-time and an Emacs mode benchmark script. Nils Anders Danielsson **20120505115909 Ignore-this: 3dfe60b2c6f4696e29f99d6db1970402 ] [Changed the default "being type-checked" background to light blue. Nils Anders Danielsson **20120505063351 Ignore-this: 7912a4e80c314a61eb533ebcc7161128 ] [Tried to make the test suite work on case-insensitive file systems. Nils Anders Danielsson **20120505062636 Ignore-this: f31ef788832de4b6d61c4b703e3f049e ] [Added forgotten LANGUAGE pragma TypeSynonymInstances. Andreas Abel **20120504184715 Ignore-this: c55a9cd62a33180053c15d706de849c4 ] [Addressed some warnings emitted by the Emacs byte-compiler. Nils Anders Danielsson **20120504174959 Ignore-this: f44814a64d09d13c347a7909535f8983 + The only remaining warnings are the "cl package required at runtime" ones. ] [Replaced some uses of error with putStrLn. Nils Anders Danielsson **20120504170556 Ignore-this: 7762413e875f929602f46b85ce2c1c5 ] [New configuration variable: agda2-highlight-level. Nils Anders Danielsson **20120504170349 Ignore-this: 297b14588a3ef3e664b5f6b1be7785ce ] [Terminal I/O should use the character encoding specified by the locale. Nils Anders Danielsson **20120504170124 Ignore-this: 91262adbb2f632b7fbeb56c3fee20a9d ] [Removed A.Utils.IO.Locale and support for versions of base prior to 4.2. Nils Anders Danielsson **20120504170124 Ignore-this: f9ab39edb5f7c0acaee06406f9606442 ] [Various changes related to interactive highlighting. Nils Anders Danielsson **20120504170107 Ignore-this: 793929b1c1f4c024f804f78c605c99f2 ] [Removed Agda.Interaction.Highlighting.Precise.TypeChecked. Nils Anders Danielsson **20120501203406 Ignore-this: ce7f1045ac80ca0b8ffef68bfcde8bc3 ] [Resolved conflicts. Nils Anders Danielsson **20120501195412 Ignore-this: 1982f61d903aaec404593319a36b91ff ] [Renamed agda2-highlight-annotations to agda2-highlight-add-annotations. Nils Anders Danielsson **20120430193048 Ignore-this: 3dac1a1ef4a8401f58008f225b033416 ] [Interactive syntax highlighting. Guilhem Moulin **20120427184631 Ignore-this: 5faed9df692d058b6bb1e2e391305a1 Dynamically highlight the Agda modules, on a per-mutual-block basis. The highlighting information is directly piped over to Emacs instead of being written into a temporary file. ] [Noted that geniplate-0.6.0.0 doesn't build under GHC 7.4.1. Nils Anders Danielsson **20120430172303 Ignore-this: c091ceec13eda1e32bc7cccad1dde891 ] [Rolled back most of 'Removed Agda.Syntax.Internal.Generic...'. Nils Anders Danielsson **20120425115255 Ignore-this: 831820182fc825e74da4d7a3d9508cfd ] [Removed Agda.Syntax.Internal.Generic in favour of geniplate. Nils Anders Danielsson **20120425114951 Ignore-this: 487aa1447b37bb187b108d382a0cbdb4 + This seems to lead to a small but noticeable slowdown. ] [Removed the dependency on syb. Nils Anders Danielsson **20120422200603 Ignore-this: 781ba15e42aef423941ec67f813d34df + Removed all Data instances. + Removed Agda.Compiler.MAlonzo.gshow'. ] [Removed Agda.Utils.Generics, which was unused. Nils Anders Danielsson **20120422200405 Ignore-this: 5cb55f8e18f5b5d2865a2b8ffcf81568 ] [Stopped using syb in Agda.Compiler.MAlonzo.Pretty. Nils Anders Danielsson **20120422200253 Ignore-this: fa70978f0e70c6fafd66cc507697f0f8 ] [Removed Agda.Syntax.Strict. Nils Anders Danielsson **20120422181654 Ignore-this: a8b6897d817af9c8af26cab3d80a33c5 + This module was unused (except for some superfluous constraints), and it depended on syb. ] [Replaced some uses of Map.unionWith with Map.insertWith. Nils Anders Danielsson **20120422172735 Ignore-this: 4f8396eb23db22bbd8578cc587c58b39 ] [Switched from SYB to Geniplate in syntax highlighting code. Nils Anders Danielsson **20120422172448 Ignore-this: 5efc45b304e8c7039132169850768a02 + This makes the standard library type-check roughly 10% faster. ] [Added a clarifying comment. Nils Anders Danielsson **20120504154419 Ignore-this: d50301c819516ecd1ed66bfd618490a3 ] [Added some SetRange instances. Nils Anders Danielsson **20120504130100 Ignore-this: fca2d8de1403f646cab5f7f792ad9324 ] [Don't force people to use font-lock mode. Nils Anders Danielsson **20120502140303 Ignore-this: d5a10b096fc2457e9785c17386505bce ] [Fixing issue with the highlighting of comments in Emacs. Guilhem Moulin **20120427184650 Ignore-this: 83b4d9accc3a9a7beedbed567123fc3c ] [Added sorted. Nils Anders Danielsson **20120502130139 Ignore-this: 3704e6f094f068421b01bb62ee3df30f ] [Removed a redundant check for self-assignment in the occurs check. Andreas Abel **20120504142640 Ignore-this: 58e7f66e729934b8f30ab40342e7c813 ] [Bring back the error message for failing occurs check that was disabled by the fix for issue 442. Andreas Abel **20120504141729 Ignore-this: a65b3e6f86737e1d0df050ca971b2f93 If a constraint asks to construct an infinite term, fail instead of postponing! ] [Enhanced pruning by makeing hasBadRigid more precise. Andreas Abel **20120504114320 Ignore-this: 762ab7e24dcd0e317891d9546471b60d Any argument to a metavariable which has a forbidden variable in a non-eliminateable position (e.g. as an argument to a type constructor) can be pruned. Before it was just a forbidden variable in head position. (Which is a special case of a non-eliminateable position.) ] [Raise instance for de Bruijn indices. Andreas Abel **20120504113107 Ignore-this: 133b4974b21ee8d451d315ffb5ad4aa1 ] [Made test case for Issue 442 more precise. Andreas Abel **20120504112810 Ignore-this: e46d53b512578e7ba64ac2caf6ca63fb ] [[issue 618] fixed incorrect compiled flat (MAlonzo) introduced by issue 616 fix ulfn@chalmers.se**20120504063720 Ignore-this: 74284f465b3c055932c77d788620a187 ] [specify SHELL=bash in top-level and lib-succeed Makefile as some shells don't have the time command james@cs.ioc.ee**20120502203932 Ignore-this: e09a02d444fb73c41ac5d0a70ee537d ] [Final version of HCAR entry. Nils Anders Danielsson **20120502082541 Ignore-this: f9a5c9200883b06c510ac5b14c13dc06 ] [Updated HCAR entry draft. Nils Anders Danielsson **20120501190828 Ignore-this: a92d8484953efaa23b3b4e9aeed33cb2 ] [New option --show-irrelevant. Andreas Abel **20120430115208 Ignore-this: c98c73de9f1d768af0d6e4e85673bb4c Irrelevant arguments are printed as _ by default now. Optimized reification a bit to not reify implicit arguments which do not show up in the final result anyway. Restructured release notes: separate new options, new syntax (language), new type checking. (WAS: Language) ] [Moved localState to Utils.Monad and introduced bracket_. Andreas Abel **20120430112835 Ignore-this: a6ec8e2396416893baf13530ff384c70 ] [Retired unused and outdated functions in Utils.Monad. Andreas Abel **20120430105832 Ignore-this: 7d6a0285d3705f5b3714b126876e398 ] [TermCheck: Removed unused imports. Andreas Abel **20120430105548 Ignore-this: cb5cf04c7316d213ab1c7e16a2592025 ] [Clarified a mysterious error message. Andreas Abel **20120430095410 Ignore-this: 2dc9a51d7b9f75f725f968460495508e ] [fixed issue 616: flat was not considered projection-like ulfn@chalmers.se**20120430083747 Ignore-this: 7ad6ad6c0250146199013107c13e6dba ] [added missing error message for test/fail/SkipParametersInConstructorReification.agda ulfn@chalmers.se**20120430083543 Ignore-this: 91912106e90efb07baabc936c3445369 ] [cleanup for test/succeed/Issue561.agda ulfn@chalmers.se**20120430083459 Ignore-this: b20564fe4d970685e4ba15dd253419b8 ] [[fix-agda-whitespace] print which files have bad whitespace ulfn@chalmers.se**20120430083200 Ignore-this: 8cf7bc1c8fdb5b821a39c344e8c52b05 ] [specialized implementations of Functor and Applicative for TCM ulfn@chalmers.se**20120426083047 Ignore-this: 715c20bd1539af4247e16ad464de9f21 ] [changed the signature from Data.Map to Data.HashMap.Strict ulfn@chalmers.se**20120425150731 Ignore-this: 260f2073733e91f6de59e86dc6fe34e0 results in minor, but observable performance improvements ] [Outline of HCAR draft for May 2012. Nils Anders Danielsson **20120427172406 Ignore-this: cbc5d0b23c2739f7fd6a0238ba3739df ] [Rollback void to compile under GHC 6.12.1. Andreas Abel **20120426100310 Ignore-this: cf28fc229436a4185b40bef4aa0b5ebf ] [Fixed issue 614. Nils Anders Danielsson **20120425130126 Ignore-this: 51ed032e73ae3ccf29fb902341df18ff ] [Added allMetas. Nils Anders Danielsson **20120425112709 Ignore-this: dfb187682053257d6aee91c40d67b7fd ] [Made time profiling much faster, at the cost of some redundant code. Nils Anders Danielsson **20120425111336 Ignore-this: 3cede0a5eeb6d0df115c60e95d96f539 ] [Added missing require statement. Nils Anders Danielsson **20120423161420 Ignore-this: 63483555f9cea7ddcc8232e6e96d1e32 ] [Fixed issue 613. Nils Anders Danielsson **20120423155341 Ignore-this: 7121379abcc33f055a8730269672d14 ] [Modified some doc-strings. Nils Anders Danielsson **20120422224623 Ignore-this: 672a7cb1d8662d1fcd9deb607dcc5030 ] [The Emacs mode's version must now match the Agda executable's. Nils Anders Danielsson **20120422224548 Ignore-this: 3dd551e1c77941cc9b495a03f613b791 ] [New semantics of agda2-program-args: --ghci-interaction is always added. Nils Anders Danielsson **20120422221025 Ignore-this: ad2f24752f8b0f35c09b34f96ec1037b ] [Updated release notes, added section called "Installation". Nils Anders Danielsson **20120422220245 Ignore-this: bdda7dd321b5a3b383496c91110b8713 ] [document Emacs mode changes divipp@gmail.com**20120421013904 Ignore-this: 4d51afc335235291b1e106ec8e86a223 Update README and the release notes. - the agda executable is used instead of ghci - no haskell-mode dependency ] [Updated outdated comment. Nils Anders Danielsson **20120422164632 Ignore-this: d06c0600c9eedf9229225fba5853d315 ] [Stopped using compressed files in most of Generate. Nils Anders Danielsson **20120421124539 Ignore-this: d23b242deb18ba15978009555cbec0fd + Exception: highlightAsTypeChecked. ] [Tried using compressed files in Generate. Nils Anders Danielsson **20120421124055 Ignore-this: c2ea3c91c3f00fd4d805b914cccc6ed9 + The effect on batch-mode performance seems to be negligible, but an experiment carried out together with Guilhem Molin indicates that operations working directly on compressed files may be worthwhile in the context of interactive highlighting. ] [Added operations working directly with CompressedFiles. Nils Anders Danielsson **20120421123235 Ignore-this: 37acf0c9b4550a29f8b3f55b50932b40 ] [Changed the types of singleton and several, removed getRanges(A). Nils Anders Danielsson **20120421114334 Ignore-this: dbf1dac0ddc5df810a35ce2969841fd9 ] [Moved InteractionOutputCallback to Agda.Interaction.Response. Nils Anders Danielsson **20120421095029 Ignore-this: b9ba519ab6624c2aff35f48d65fe62ce ] [I heard that discarding results of monadic computations causes warnings now, thus. Andreas Abel **20120421171941 Ignore-this: f6d8b40b28c16166ad4f95580568e374 Inserted the void function where I deleted a _ <- ] [Fixed bug in printing (reification) of projection-like functions. Andreas Abel **20120421163536 Ignore-this: 538360e682e43c39f12e1a82191605f Non-hidden arguments which were omitted in internal syntax due to projection-likeness also got omitted during printing to abstract syntax, unless --show-implicit. ] [Reify: only name first constructor argument if it is hidden *and* the data type has parameters. Andreas Abel **20120421150450 Ignore-this: e102be1ec8c989a0c9e4638c87e43a2d ] [Debug printing for coerce. Andreas Abel **20120421150330 Ignore-this: 24469c2b36115d9320b0fdbd8ed373d2 ] [Refactoring: integrate blockTerm into coerce. Andreas Abel **20120421114846 Ignore-this: 15e45fad47dacd1caf9bd181f6b7704d ] [Fixed a type checking problem with explicit lambda for --experimental-irrelevance. Andreas Abel **20120421110158 Ignore-this: d810916053f232a0d2e6be9c95dfe4cd ] [Refactoring: introduced a coerce function which may hold coercive subtyping. Andreas Abel **20120421105242 Ignore-this: a73579d7aa2c89f32d5dd2234b11c02d ] [Fixed path for agda binary. Test suite was running with stale binary. Andreas Abel **20120421111738 Ignore-this: 41d9855fba648e75389e0f0961bf14 ] [Refactoring: a use of when_. Andreas Abel **20120421105310 Ignore-this: 543381e3474f300ab87d51ae6aa5fb50 ] [Reformatting: introduced a Types section in Conversion. Andreas Abel **20120421105036 Ignore-this: 2a016982920d5509479dabccb83cba48 ] [Utils.Monad: added when_ and unless_, removed <.> which is called <=< in Control.Monad. Andreas Abel **20120421102354 Ignore-this: d96335a4ec75f32dad45546ac7620156 ] [Tiny refactoring: errors UnequalHiding and UnequalRelevance expect now Terms instead of Types. Andreas Abel **20120421092823 Ignore-this: a2cefeea5cb8e8388e17eb18b58fceaa ] [Simplified the comparison of function types (using absBody instead of piApply). Andreas Abel **20120420221531 Ignore-this: cf2713afb119eabead01f5191ba5aaa4 ] [Updated a stale comment about guardConstraint. Andreas Abel **20120420202955 Ignore-this: a002e403c006f2307d2306b34721d9de ] [Skip parameter arguments to constructors during reification, even if --show-implicit. Andreas Abel **20120420161534 Ignore-this: c22c97dcfc455b5ddb9f7fccaabb78ab This is connected to issue 611. ] [Refactoring step: apps as instance of napps. Andreas Abel **20120420145326 Ignore-this: 49406114da12741a84e5fc75e6d6ceb5 ] [Refactoring step: apps as instance of foldl. Andreas Abel **20120420144730 Ignore-this: 52204012a91fb2e4bb59048be844840b ] [Refactoring step: curry apps. Andreas Abel **20120420143800 Ignore-this: a6141f1016cafc3f4dc2515ede6b6ccc ] [Haskell-mode is not needed any more divipp@gmail.com**20120420183556 Ignore-this: 69e94b38cf3e7de15705f9b9dc4d9b28 Agda does not depend on Haskell-mode any more! This patch also adds the agda2-program-name customization variable and renames the agda2-agda-executable-options customization variable to agda2-program-args. ] [rename agda2-ghci-options to agda2-agda-executable-options divipp@gmail.com**20120420162802 Ignore-this: 1e5a88917dbde38d33d87db71d935707 ] [delete agda2-fix-ghci-for-windows divipp@gmail.com**20120420160425 Ignore-this: 3ca4c84b1ee08cfd8054f0002040fa31 This fix for Windows called "ghc --interactive" instead of "ghci". With the new "agda" backend this fix is not needed any more (I guess). ] [refactoring: let ==> where divipp@gmail.com**20120420152200 Ignore-this: 4be24e9c5986d46d703a2beecce8b379 ] [delete unused local function definition divipp@gmail.com**20120420150853 Ignore-this: 6afcc863d39ff27bbdb57a407c0cbcc1 ] [Removed an outdated comment. Nils Anders Danielsson **20120420185012 Ignore-this: b00ad5909ddc69989448a54c6dff9b70 ] [Updated the tested-with field. Nils Anders Danielsson **20120420185004 Ignore-this: d12d5c6d0dc669c237a61b14871ab716 ] [Removed the Agda-executable package. Nils Anders Danielsson **20120420184837 Ignore-this: 7a12e5e35ae221743ba5052f780e2f7e ] [Fixed broken Haddock comment. Nils Anders Danielsson **20120420155712 Ignore-this: d001412bbcff79cd0a6ae1df3dc190d9 ] [Added .UnsolvedConstraint to the CSS file. Nils Anders Danielsson **20120420152733 Ignore-this: 56c76c2a86843dfe5e7533d0b9534ac6 ] [Updated copyright year range. Nils Anders Danielsson **20120420152255 Ignore-this: 2f5d5e49c83713e4abceb750eff7cafc ] [follow stPersistent loss fix divipp@gmail.com**20120420004324 Ignore-this: 1a829051f6efbb2d5c70c3b8093cee47 ] [fix stPersistent loss divipp@gmail.com**20120420004318 Ignore-this: 9021d27461e67afb388060be9c5cc5c0 When an error happens during typechecking the stPersistent part of TCMState should be kept. ] [remove unused agdaghci executable divipp@gmail.com**20120419012548 Ignore-this: 781c99e040d10f9a90148ada8e74a9e2 ] [merge agdaghci into the agda binary divipp@gmail.com**20120419012147 Ignore-this: 4ef240762c6ceddea20be34b2482f5c4 Two new command line options for agda: --ghci-interaction mimic ghci behaviour with :mod +Agda.Interaction.GhciTop (used in the Emacs frontend) --interaction-test=FILE mimic ghci behaviour with :mod +Agda.Interaction.GhciTop (used in interaction tests) ] [accept omisson of ExitFailure exceptions divipp@gmail.com**20120418165435 Ignore-this: 3be1662aad077b832a03ef5b8e28ff2c ExitFailure exception are missing in agdaghci output. This is ok because the emitted elisp commands report the error anyway. ] [run interaction tests with agdaghci divipp@gmail.com**20120418164810 Ignore-this: 89e56708ab43a12a84eb8ce073747ede Interaction tests with ".in" extension are interpreted with agdaghci; interaction tests with ".in_ghci" extension are interpreted with ghci. agdaghci interprets interaction tests faster. Also we can test agdaghci in this way. Currenty only one test case is interpreted with ghci which cannot be interpreted with agdaghci at the moment. ] [put back CPP directives divipp@gmail.com**20120418164534 Ignore-this: cb41c214d7dd9a1af4e59cad910d67e3 ] [improve agdaghci divipp@gmail.com**20120418163613 Ignore-this: 3e3ce97b099da04a6c4de6033c263e83 * parsing of parenthesis is more forgiving * one-line comments are accepted * empty lines are accepted * clean exit at the end of input * with the --currentfile command line option one can set the current file * expressions interpreted if --currentfile is set: top_command, goal_command, currentFile * do not print promt if --currentfile is set With these changes agdaghci can interpret most of the intactive tests. ] [remove unneded imports divipp@gmail.com**20120409104650 Ignore-this: 1c70b76ef36515c92448896abeee658b ] [do not call ghci in the Emacs frontend divipp@gmail.com**20120409010805 Ignore-this: f9b0514600eb4f36b4f0f851af56c0c9 Call a dedicated executable instead which mimics ghci. ] [Removed --reinstall. Nils Anders Danielsson **20120420150723 Ignore-this: 41240f3f8025b28c66b5b4d19e010be0 ] [compareAtom literal speedup. james@place.org**20120418200253 Ignore-this: 934a8f73056211e8cccefb2e64416ed9 compareAtom would reduce a pair of LitInts to constructor form a level at a time and compare them recursively; this patch only reduces to constructor form when one side of the comparison is a nonliteral. Speeds up things like 'million : 1000 * 1000 ≡ 1000000 ; million = refl' by orders of magnitude. ] [Constructor application now pushes type in even when underscore values for the parameters are supplied. (Fixes issue 611.) Andreas Abel **20120418210632 Ignore-this: 8a188d441220e8bf04a0bc81e74a4e4c ] [fixed missing builtin check for nat constructors when using literals ulfn@chalmers.se**20120418163716 Ignore-this: 55e2757e6f92e056807ab968ab4262d0 ] [Added agda2-comment-dwim-rest-of-buffer. Nils Anders Danielsson **20120418150211 Ignore-this: d45759a5f1477d53b7f49c19481dee13 ] [Test case for with in irrelevant declarations. Andreas Abel **20120418130519 Ignore-this: e93ad25c8fb119515b8d0184ba5dffd2 ] [When checking a DontCare term, keep DontCare. (Fixes Issue 610-4). Andreas Abel **20120418125852 Ignore-this: bb6cfbfeeeecf063559ae580d73df6e9 ] [Declaration in irrelevant context (e.g. where modules) must be irrelevant as well. Andreas Abel **20120418123748 Ignore-this: e1476e4992ded03ce0a2e073868e1925 Fixes part of issue 610. ] [Added agda2-queue.el. Nils Anders Danielsson **20120416152620 Ignore-this: 766dbd311606a6811f9d31b711b0f064 ] [finish "replace HighlightingOutput by InteractionOutputCallback" divipp@gmail.com**20120408053849 Ignore-this: b58ea6d45ee835225bcda2860320280a (I didn't take into account that 'darcs replace' supports --token-chars.) ] [improve comments divipp@gmail.com**20120408052252 Ignore-this: 1bcef3c05efa77e5e38734ad63c19f5d ] [add more structure to give results divipp@gmail.com**20120407170948 Ignore-this: 377119bbfd8d4d3736f74b22f56dc6c4 Previously the give result was a String with some inner structure. Now it is a proper ADT with three constructors. ] [make the Response data type more informative divipp@gmail.com**20120322163633 Ignore-this: d5f102506e4161f46a302c924d460957 ] [Fixed compilation with GHC 7.2.2. Andrés Sicard-Ramírez **20120408155607 Ignore-this: 88bdbebfae6156237e7d6b15ae0603fa ] [A translation of copatterns into nested record expressions. Andreas Abel **20120407155131 Ignore-this: f4ce65b1cc3ca718163f09d91fd5e74e This translation handles only the simplest cases of copattern lhs yet. No with, rewrite, where, absurd clauses. fst f = e1 snd f = e2 is rewritten to f = record { fst = e1; snd = e2 } Deep destructor patterns are supported. See test/succeed/Copatterns.agda for a simple example. The highlighting does not fully work yet, maybe some corrupt range info!? ] [Conflict resolution for the copattern patches after Ulf's qualified mixfix ops. Andreas Abel **20120407154549 Ignore-this: 3b2b2c298231732dafebe07f166ca21 ] [Monadic mapping over pairs (utilities). Andreas Abel **20120407154318 Ignore-this: c266fe72e5931ef9e0581b996396394d ] [Updating the reorganization of Internal (conflict resolution). Andreas Abel **20120407154142 Ignore-this: b684153250b9aeac0fd47479cf0eab7d ] [Naming the components of Clause. Andreas Abel **20120407154038 Ignore-this: 42850fbbf7b451216c247f24eb6d75bf ] [Add a comment for QuoteGoal constructor. Andreas Abel **20120407154013 Ignore-this: 6ae30214094d02e9c304eab58cb0db1e ] [Internal refactoring: notSoNiceDeclaration takes only one declaration, not a list. Andreas Abel **20120407153902 Ignore-this: 2130f7f46c406c5f77ee66ef56be3e1b ] [Reorganization of Syntax.Internal: put functions in proper sections. Andreas Abel **20120402062734 Ignore-this: c32df08b962579cf9146cad083870a48 ] [Merged copattern patches with pattern synonym patch. Andreas Abel **20120309211035] [Resolved conflicts with new-highlighting patches. Andreas Abel **20120130212340] [Towards flexible arity in defined functions. Refactoring step: ProblemRest. Andreas Abel **20111125174342 Introduced a new component to Problem data type which stores overhanging user patterns and the type they eliminate. ] [Added test for a possible new feature: functions with flexible arity. Andreas Abel **20111124173200] [Scope checking definitions by copatterns implemented. Andreas Abel **20111124163042] [Refactoring step: Added LHSCore to abstract syntax. Andreas Abel **20111124151403] [Parsing copatterns. Andreas Abel **20111123155247 Seems to recognize them, but then abstract syntax does not support them yet. ] [Introduced LHSCore data type. Andreas Abel **20111123123846 Refactoring step. No observable change of Agda functionality. Test suite runs. ] [Start of copattern parsing implementation. james@cs.ioc.ee**20111122122008 Ignore-this: bd84a357f87c6c76544cca0bd8d63d8d Incomplete! Breaks compilation of Agda! ] [New option --copatterns. Andreas Abel **20111122094816 Example file for definition by copatterns in test/features. ] [Interaction test to ensure refine does not add extra parentheses. Andreas Abel **20120407082824 Ignore-this: e6a44ec6fb1efb755945d037f098628f See (invalid) issue 606. ] [benchmark run ulfn@chalmers.se**20120406082221 Ignore-this: 26a3f69e3b8827ce049f9bb1195fe866 ] [fixed issue 597: allowing qualified mixfix operators ulfn@chalmers.se**20120406081708 Ignore-this: 96087f8ef5ed9134eb0dd19e70b09d90 To use an operator qualified you qualify the first token. For instance import Data.Bool as Bool z = Bool.if true then 0 else 1 ] [Added --reinstall to the install-lib and install-prof-lib targets. Nils Anders Danielsson **20120405092037 Ignore-this: b60de3df860eb8885f530345badca126 ] [Rollback cabal flag --force-reinstall in Makefile. Andreas Abel **20120404154238 Ignore-this: 55d47617f4a3e146a117b7934a3a2802 cabal-install 0.10.x does not know this flag. (I am not willing to upgrade only for this flag.) Also, I cannot reproduce the behavior; make install-bin always installs new binaries. rolling back: Wed Apr 4 14:18:54 CEST 2012 ulfn@chalmers.se * use --force-reinstall in the Makefile to make cabal actually do something when recompiling Agda M ./Makefile -1 +1 ] [fixed issue 580 by disallowing private record fields ulfn@chalmers.se**20120404141335 Ignore-this: 9d98417d0366f855fdbcf7fa5b17ea8f ] [Refine, emacs: C-u C-c C-r will insert a pattern matching lambda instead of a standard lambda. wjedynak@gmail.com**20120403184011 Ignore-this: 7126043ae8a42fde7c9e54ce1e799f7f ] [whitespace ulfn@chalmers.se**20120404134850 Ignore-this: 76a70cb5dea86693ee897f8447382691 ] [fixed issue 561: MAlonzo not adding imports for Data.Char primitives ulfn@chalmers.se**20120404134757 Ignore-this: 61a6946f673d424224705c13d27fba54 ] [use --force-reinstall in the Makefile to make cabal actually do something when recompiling Agda ulfn@chalmers.se**20120404121854 Ignore-this: 5b7f663233eadd4fbef2b92a1b60da03 ] [patch-for-issue-600 makoto.takeyama@aist.go.jp**20120404060936 Ignore-this: 7734ee3c678568036461669a1b20d801 ] [emacs-mode: fixes an edge case in the goal annotation procedure. wjedynak@gmail.com**20120403233247 Ignore-this: 6a83bc298c61259dd382808477232942 ] [emacs-mode: fixes a problem with nested comments - see issue 601. wjedynak@gmail.com**20120403233114 Ignore-this: f2099dade38db20f4585f316162bfa0b ] [removed -v from some test cases in test/succeed ulfn@chalmers.se**20120404120552 Ignore-this: 7dcb8e511f1045659e4b7e7cab49809d ] [cosmetic change ulfn@chalmers.se**20120404120447 Ignore-this: eb72e8d81b71d3a75f5c84be33d70da7 ] [fixed issue 602: record projections are positive in their argument ulfn@chalmers.se**20120404120405 Ignore-this: 27d98a28c0e4991c6c59f7be1b3c7a5b ] [benchmark run ulfn@chalmers.se**20120329102116 Ignore-this: d39c2992c560b3de75ab8925f8f34c6b ] [Big overhaul of internal representation of irrelevant subterms. andreas.abel@ifi.lmu.de**20120403141629 Ignore-this: 2c41af95e243dd3969f1b6a4a7b29940 DontCare is not longer inserted everywhere. Irrelevant subterms are distinguished by the Relevance field in Arg. DontCare has been rededicated to an internal represent of the irrelevance axiom: .DontCare : .A -> A It is used to guard the content of irrelevant projections. The previous solution, to use a user-postulated builtin irrelevance axiom, does not work since we cannot supply the type A; it is gone due to the erasure of parameters in projections. The dummy (sort Prop) solution failed in the presence of 'with'. This was raised in issue 596 which is now fixed. Since Arg is now used to distinguish irrelevant subterms, it has been split into Arg and Dom. Dom is used in Pi-types, contexts and telescopes where the relevance flag does not apply to the subterm (function domain) itself, but is an information about the function type variance. Arg is used whenever the relevance flag applies to the term under Arg itself. Since Arg has been used for many things, there are cases where both Dom and Arg can be used. In case of doubt, use Arg. ] [Added an example: , x , , , y. Nils Anders Danielsson **20120402163303 Ignore-this: dca011516795c7cc7e7a396f75205cef ] [Moved some old mixfix parser prototype files. Nils Anders Danielsson **20120402161918 Ignore-this: 33e3da4ae6f676a12e3e871a4315b1f2 ] [Removed some potentially confusing comments. Nils Anders Danielsson **20120402081912 Ignore-this: ce07062eb2a35878c8e5aa2088603ef3 ] [Type signatures and comments explaining what is considered projection-like. Andreas Abel **20120402074141 Ignore-this: 44fa673bc2d40dd4fc3103bd4caedf24 ] [Move stripDontCare from Tc.MetaVars to S.Internal. Andreas Abel **20120331112550 Ignore-this: fbbbfc142426d1856a1d63e01dba7b23 ] [Other half of renaming checkAllVars to inverseSubst. Andreas Abel **20120331104704 Ignore-this: bcfe1e4ba550206db4c45e6c2ae1da51 Ended up in wrong patch. Should fix issue 594 (broken build). ] [Tc.MetaVars: The linearity check now skips variables of a singleton type. Andreas Abel **20120330201323 Ignore-this: bbfb467c482e35c92fbb7c02caa431b5 This fixes issue 593 part 2. ] [Tc.MetaVars: Rename rename to substitute, which is more appropriate now. Andreas Abel **20120330201041 Ignore-this: e80cd47aeff0234e7a4bcfb3f8574aae ] [When eta-expanding a level meta in --type-in-type, skip occurs check. Andreas Abel **20120330200753 Ignore-this: 5780b0b19187ee6ce23dd163863c94 Small optimization. ] [A failed test case to make sure we do not solve all non-linear constraints. Andreas Abel **20120330200305 Ignore-this: e815aa1404582aa76706fe58367585d0 ] [Records library: generalized an interface, using new Either map functions. Andreas Abel **20120330200214 Ignore-this: b2811f407514c945931ca56d2d710350 ] [Comment on some stale comment. Andreas Abel **20120330200042 Ignore-this: 6a7b915f2146e369ae6c2f3b2e5ac5f9 ] [Map functions for the Either type. Andreas Abel **20120330200009 Ignore-this: f9733acd32299e2a896203ca006f3a8e ] [Removed map'. Nils Anders Danielsson **20120330164951 Ignore-this: eec967549f1bad0637eaa5cb7bed007f ] [Fixed bug. Nils Anders Danielsson **20120330141722 Ignore-this: 6b3d8c09d8f9e6787583de7f891882dd ] [Tried to simplify the lexer's grammar. Nils Anders Danielsson **20120330135250 Ignore-this: 97b80a47b61d44af7cb0f38fc5189cdd ] [Fixed bug. Nils Anders Danielsson **20120330135209 Ignore-this: 228336db3f2ed23caacc331e11b284f ] [Changed the parser interface. Nils Anders Danielsson **20120330130818 Ignore-this: 6674ebbc92ea649791e3f69d2085d4b4 ] [Added combinators based on Johnson's "Memoization in Top-Down Parsing". Nils Anders Danielsson **20120330130801 Ignore-this: 844235cde839326f7d4c16cbb8a304e2 ] [Removed a comment. Nils Anders Danielsson **20120329214436 Ignore-this: 41829bfd12902b9446729350344b6691 ] [Support for cyclic precedence graphs. Nils Anders Danielsson **20120329205432 Ignore-this: 9d2e2deb1e6b4f5a106c06eff027892e + Made the expression grammar left recursive. + Switched from Memoised to MemoisedCPS as the parser backend. This backend is quite a bit slower, but Memoised cannot handle left recursion. ] [Disabled a slow assertion (a test of acyclicity). Nils Anders Danielsson **20120329205344 Ignore-this: 33f764a17bc663013c6f1874c1b989b7 ] [Added simpleGraph, improved acyclicGraph, optimised prop_list. Nils Anders Danielsson **20120329161633 Ignore-this: fc6283e7de394985e76678347ef72063 ] [Renamed memoParse to parse. Nils Anders Danielsson **20120329153249 Ignore-this: a972182697e73feee68a3b0bd6c5cf89 ] [Brought code up to date, removed some superfluous import statements. Nils Anders Danielsson **20120329153133 Ignore-this: a08ebd332d88a5766fe314028080f40c ] [Added adjust. Nils Anders Danielsson **20120329153050 Ignore-this: 9a3940c02348936f7c72c30a1bdfb920 ] [Implemented Wrapped and Paired as GADTs. Nils Anders Danielsson **20120329152926 Ignore-this: fbd40394e59f3817b43bf3bd9bef2204 ] [Minor change to the Parser class. Nils Anders Danielsson **20120328222248 Ignore-this: 69665de026395c3034bae25d056e18b9 ] [Eta expand variables of singleton types that would fail occurs check. Andreas Abel **20120330144609 Ignore-this: fea071f28c6eb7ca9316bc00be35adf9 Fixing issue 593. ] [Optimization: skip occurs check when eta-expanding a meta-variable. Andreas Abel **20120329153334 Ignore-this: 8ee1f9bc972c0f088ea2ff74051816e7 ] [Clean-up in TypeChecking.Monad.Context. Andreas Abel **20120329152103 Ignore-this: 6d171fd7c493b79aa3580dfdfc989d08 ] [Rolled back '[rolled back fix to 473]' and made the code compile. Nils Anders Danielsson **20120329093908 Ignore-this: ff2f5cbd4b0c0c3c5a5f75e7f3a1e07 ] [Release notes for solving with record patterns. (Issue 456.) Andreas Abel **20120329082328 Ignore-this: f1e525033a4b685d6e8fa55b6e788779 ] [Update FindInScope constraint's list of remaining candidates after resolution attempt (for better performance). Dominique Devriese **20120328120925 Ignore-this: 43f416e7059795d2844adfb9a5717870 ] [Fixed a syntax error... Nils Anders Danielsson **20120328181309 Ignore-this: 57d758fe508e3e1840db995a3802a212 ] [Included another string in the benchmark. Nils Anders Danielsson **20120328180720 Ignore-this: 40717194f3acf02c2f4aa4aab61f2db7 ] [Support for base 4.5 and incremental 0.2. Nils Anders Danielsson **20120328180418 Ignore-this: b7008af16c5c2632b53a9fe7ec942bf6 ] [Added support for haskell-src-exts 1.12 and 1.13. Nils Anders Danielsson **20120328151154 Ignore-this: 6db2ecfc03daeb3b8bdd7bffe765dbc2 ] [Completed Andreas' fix for issue 479. Nils Anders Danielsson **20120327174328 Ignore-this: 4e3c5da2f18e6d872c3388116c7dd62c ] [Removed unnecessary use of fromIntegral. Nils Anders Danielsson **20120327173421 Ignore-this: 4dc33aef16367b4c7096f1889bba8c2c ] [Record pattern unification for irrelevant arguments. Andreas Abel **20120327163110 Ignore-this: 433ebf8bc472f5046527ad30e30b53a2 This completes the fix for 456. ] [Interface version bump for new UnsolvedConstraint highlighting info (unused so far). andreas.abel@ifi.lmu.de**20120327111037 Ignore-this: 6c2b079ccd78cdcab1f7e49dfa9ff4c4 ] [Added highlighting for unsolved emptyness constraints. Andreas Abel **20120327092041 Ignore-this: 5d1ef5f83836c8ae8d08c08fa8cf8ff6 Added range info to emptyness constraints. Unsolved e.c.s are highlighted as unsolved metas. TODO: distinguish these two causes of unsolvedness properly in the highlighting mechanisms. ] [Extending Miller patterns to record patterns. Andreas Abel **20120327001237 Ignore-this: 248b1604599cd8b4bb92ccfc869943b We can now solve metas _1 (x , y) applied to record patterns. This fixes issues 376 and 456. TODO: irrelevant record patterns. ] [Refactorings for Internal syntax variables and variable lists. Andreas Abel **20120326213014 Ignore-this: 80a3edf47ae00dad1ce8a6736abf41 Added a smart constructor @var i@ for @Var i []@. Added an utility downFrom which helps generate variable lists without double reversing. ] [Refactoring the Miller pattern check: now returns a partial substitution. Andreas Abel **20120326164421 Ignore-this: 8c7f16f4255c800d69e07c7294d101c Changes nothing. ] [Internal change: new function TypeChecking.Context.escapeContextToTopLevel. Andreas Abel **20120326153022 Ignore-this: 5ef313d2d1253185bfcd4d6b05e9e03b Clarifies code a bit. Tiny change. ] [Added missing call to $(setup_$*). Nils Anders Danielsson **20120326175851 Ignore-this: 558127e7fbe4334ad7149ec7cf4f957b ] [Fixed issue 591. Nils Anders Danielsson **20120326175822 Ignore-this: 7a0b4da564fcd9c3ee457eeacabe90d3 + I think that Agda's handling of options is too complicated. This fix makes it even more complicated. ] [Interaction test cases must now reside in test/interaction. Nils Anders Danielsson **20120326174202 Ignore-this: e71b98f6fffd343fb35fa90ab46ee7f7 + Not in its subdirectories. ] [Minor simplification. Nils Anders Danielsson **20120326173451 Ignore-this: 29861c1936fe213bf8a8e7d6d523a40c ] [Removed comments. Nils Anders Danielsson **20120326171209 Ignore-this: d90470b42c593e58adb1d205dd0acd55 ] [Added missing CPP pragma. Nils Anders Danielsson **20120326165811 Ignore-this: 50f6266ff31a4b12e96add6a562a997 ] [split GhciTop.hs into InteractionTop.hs and GhciTop.hs divipp@gmail.com**20120321143214 Ignore-this: 52cead4f40030b508f33b2d7d2e3b164 The motivation is that InteractionTop.hs is a pure module which contains most of the information, and the new GhciTop.hs is a relatively small module which imports InteractionTop.hs and which contains the impure part (the global 'theState' mutable variable created by unsafePerformIO). A proper interactive frontend can import the pure InteractionTop.hs only so it will have a global state, so it could serve multiple Agda source file editing at the same time. ] [fix newtype deriving in InteractionTop.hs (previously GhciTop.hs) divipp@gmail.com**20120321140227 Ignore-this: 26b67b06def1597d50f9bdcd57f90baf ] [use __IMPOSSIBLE__ instead of a dummy default of HighlightingOutput divipp@gmail.com**20120321132434 Ignore-this: 223ff3875c44a714cc703560cfeef87 ] [replace HighlightingOutput by InteractionOutputCallback divipp@gmail.com**20120321131423 Ignore-this: 93705e01e4cab8026082425938d3f229 ] [replace voidHighlightingOutput to defaultHighlightingOutput divipp@gmail.com**20120321131055 Ignore-this: 663212fd91e3d7e691baeb4ef3fc2a97 ] [documentation of GhciTop.hs refacftorings divipp@gmail.com**20120321130312 Ignore-this: 94bab57e1ddc8d9e84818299a2abc39a Documentation added for top level functions and record fields introduced in the two recent GhciTop.hs refactoring patches. ] [Do not generate constraints when instance search for irrelevant metas. Andreas Abel **20120321105739 Ignore-this: 5dae562fedd4f5b8f83f28dee4b7b90c This fixes a bug when trying to give interactively a term to an irrelevant goal in some situations. ] [Do not run new meta occurs check on interaction metas. Andreas Abel **20120321095611 Ignore-this: 3952a30c02752426827367b5bbe505bf Fixes issue 589. ] [Added one (deep) strictness annotation. Nils Anders Danielsson **20120320160326 Ignore-this: 7d180af73d0c8c37f779b6b7917d53d4 + This change seems to have a noticeable, positive effect on the time required to check the standard library. + The patch adds a dependency on deepseq, which is in the Haskell Platform. ] [Fixed issue 588. Nils Anders Danielsson **20120319132405 Ignore-this: 6f2487053aaa94e5b70da44232aea66c ] [Added KillRange instances for concrete declarations, expressions etc. Nils Anders Danielsson **20120319131830 Ignore-this: 914e95e91537066aa397858ce9928d0b ] [improve GhciTop.hs divipp@gmail.com**20120319054633 Ignore-this: fd5e678dff63fcee1bc86ffb887cc5d8 major changes: - get rid of the redundant outputFunction field in CommandState cosmetic changes: - rename State to InteractionState - define InteractionState as a record instead of a tuple - use Rank2Types in the type of liftCommandMT - remove trailing whitespaces ] [Main refactoring of GhciTop.hs divipp@gmail.com**20120316131140 Ignore-this: 1d3e76977eee439e67d35ac670235819 Changes: - Use the global state 'theState' as less as possible. - Add a callback functions which is called instead of sending the interactive output to stdout. In this way the output sending can be much cheaper if the Agda libraries are statically linked to an application. - Emit the interactive output as ADT values instead of an elisp string. This helps to port Agda interaction to other editors. ] [fixed issue 546: type signatures should not see through abstract! ulfn@chalmers.se**20120316152519 Ignore-this: 2da7e8997e7241ed2abd8ffd7713afd5 ] [fixed issue 564: display forms interacting badly with levels ulfn@chalmers.se**20120316142833 Ignore-this: fdadd7ea6d58a92db464a62d33ec5b8a ] [benchmark run ulfn@chalmers.se**20120216120159 Ignore-this: 1c2963dadd471888fa0342282cd06425 ] [Removed shift/reduce conflict introduced by record update syntax. Andreas Abel **20120316140311 This fixes issue 549. ] [Release notes and more examples for fix 585. Andreas Abel **20120315173606] [Issue 533 is fixed. Andreas Abel **20120315151514] [Do not run metaOccurs check for metas coming from postponed type checking problems. Andreas Abel **20120315150257 This improves the fix for issue 585. ] [Try to solve left-over constraints after each mutual block. Andreas Abel **20120315133403 Fixed the 479 fix (postponed emptyness constraints). ] [Don't instantiate metas during emptyness check. Postpone emptyness check. Andreas Abel **20120315105343 This fixes issue 479. ] [Rolled back "Don't include..." and "Refactored...". Nils Anders Danielsson **20120314161452 Ignore-this: 6e325d4605aa4f3f8c3a34073baabd45 + These patches made the code slightly more complicated (I'm not 100% certain that the first one did not introduce any inconsistencies) and did not seem to have a major effect on performance. ] [Don't include definitions from other mutual blocks in positivity graph. Nils Anders Danielsson **20120313151337 Ignore-this: df2e9ff210666fbd74b4dbbb65c92c4d + Not as ADef nodes. ] [Refactored occurrences to use a reader monad. Nils Anders Danielsson **20120313145504 Ignore-this: f16f574990505c1b2cb5318d8762503e ] [Occurs check now also goes into definitions of current mutual block. Andreas Abel **20120313165614 Ignore-this: 95edc6896d9147e532d7b73f661faf74 This fixes issue 585. (Which is probably as old as Agda 2.) ] [Fixed broken test. Nils Anders Danielsson **20120313152341 Ignore-this: db2474d5cd9b7582ca86a08786e8bb88 ] [Forgotten .flags file for test fail Issue586. Andreas Abel **20120313150157 Ignore-this: 6abfef192ca8e50ea1a06a941992d2 ] [remove TMPDIR and run cleanup after choosing to keep old error message in interaction test james@cs.ioc.ee**20120308210846 Ignore-this: 546877fa3f02b86aab020fa90fc1f1c2 ] [Release notes on NO_TERMINATION_CHECK updated to --safe mode. Andreas Abel **20120312161806 Ignore-this: 4b959bab753a6aed6ab8de9884e4ffa7 ] [NO_TERMINATION_CHECK not allowed in --safe mode. Andreas Abel **20120312161403 Ignore-this: 3cb79b34d266547ce8494bcc63402851 ] [Fixed a problem about --safe flag complaining about type signatures. Andreas Abel **20120312161214 Ignore-this: f5f4844fee9d9ba63a8ff1e618c02a80 It thought they were postulates. ] [Add support for pattern synonyms, version 2 adam.gundry@strath.ac.uk**20120309153730 Ignore-this: d724422c285022f30b9a9fff0100337d ] [Use instance search to solve irrelevant metas. Andreas Abel **20120309145344 Ignore-this: dcca667a5859f8c695edea401af8439e This is another part of the fix of Issue 351. ] [Distinguish between relevant and irrelevant metas. Andreas Abel **20120309133218 Ignore-this: 8be76f5e773c5c77704c41c3cae061c8 Greedily grab solution for irrelevant metas if stumbling over it. This partially fixes issue 351. ] [Test cases for NO_TERMINATION_CHECK. Andreas Abel **20120308180310 Ignore-this: 2653a4412a236ff223bc63f9c9f619d7 ] [Internal change: Renamed variable rec to something else. Andreas Abel **20120308180245 Ignore-this: f07883e0f759f43630019e3a3bb247a3 rec is a keyword in some Haskell extensions. ] [New pragma {-# NO_TERMINATION_CHECK #-} for individual definitions. Andreas Abel **20120308180057 Ignore-this: f6b06ddc0e001ce52c272175a825997d Turns off termination checker for mutual blocks or single functions. Fixes historical issue 16 (feature request). ] [fix lib-succeed Makefile to correctly delete agdai files james@cs.ioc.ee**20120308095731 Ignore-this: 66e1e659b9bc41a92266c4a8eda290dc ] [Now we generate the name x instead of y (in certain cases). Nils Anders Danielsson **20120307105654 Ignore-this: 84dd230371edad683d4db83927f52e08 ] [Support for subscript suffices. Now x₁ is generated rather than x1. Nils Anders Danielsson **20120307105632 Ignore-this: 702ce630dc1c18fad4dbde00778e433a ] [Fixed read -n issue in test suite makefiles. Andreas Abel **20120307084738] [Missing boot file Errors.hs-boot. Andreas Abel **20120306173440] [Capture errors when printing debug messages. Andreas Abel **20120306145823 Ignore-this: 5129be2294fa1664b569e8fb6cea5238 This fixes issue 578. ] ["Fixed" issue 563. Nils Anders Danielsson **20120227154100 Ignore-this: d6d572d7acb1e04ef8202d35c2cc24e8 ] [fixed Level import in test/succeed/Issue574.agda ulfn@chalmers.se**20120227115413 Ignore-this: eb429e321e8d20868d24a0e4d04de597 ] [[js backend] fixed definition order bug ulfn@chalmers.se**20120218225735 Ignore-this: 8c40716924e3cda37f87cc7e6b6785f4 ] [Fixed issue 574. Andreas Abel **20120225170205 From a level maximum [i1, i2, ..., x1 + j1, x2 + j2, ...] with natural numbers i.. j.. we can remove all number i.. that are less than the maximum of the js (not minimum). ] [Added forgotten Makefile for test/lib-succeed. Andreas Abel **20120225150446] [Undo some accidental changes to Makefile. Andreas Abel **20120225150035] [Interaction test suite now also interactive. Andreas Abel **20120225134823 Prompts for whether you want to keep the old error or accept the new error, just like test/fail. Sorry, Nisse, still uses read -n. ] [Better names in case splits. Andreas Abel **20120225134645 When splitting a variable x of data type d, all the recursive occurrences in the generated constructor pattern get name variants of x instead of the default. Also changed the suffix scheme from y y' y0 y1 to y y1 y2 y3 etc. Joint work with Andres Loeh. ;-) ] [Enable debug messages also for interactive commands. Andreas Abel **20120225103749 Default verbosity for interaction is 0, for batch 1. But now, commands are no longer executed silently if the user wanted debug messages as specified by OPTIONS pragma. ] [Significant speed-up for instance argument resolution: keep list of candidates that is successively refined, prevent recursive resolution which was unintentionally being done in some cases. Dominique Devriese **20120224141722 Ignore-this: b7d748afc93cae975b5e2851e3548e9f ] [Added a suite of successful tests that depend on the standard library. Andreas Abel **20120224210726 Ignore-this: 64054d29f0e6f6988a57d54a1d72706 These tests are run after the standard library test. Put your test case in test/lib-succeed. Add sparingly, only if shrinking is totally unreasonable! ] [Fixed a bug in size constraint solving (example by Ramana Kumar). Andreas Abel **20120224205833 Prettier printing of unsolvable size constraints. ] [Added a new GenericDocError for preformatted error messages. Andreas Abel **20120224205652] [Rolled back most of "Failed attempt to exclude private things...". Nils Anders Danielsson **20120223165907 Ignore-this: 93a0f5238f5ccccacb221745f37f2291 ] [Failed attempt to exclude private things when applying modules. Nils Anders Danielsson **20120223165715 Ignore-this: 72d72433ef318dafcb457434519a647a + When the user writes open M e or module X = M e there is little point in including private things in the generated modules, with some exceptions. However, the exceptions are quite important. For instance, consider module X = M A using (c), where c is a constructor of the datatype D. If we do not include "D A" as a private member of X, then we cannot (in general, with the current setup) fill in all the "Defn" fields for X.c. This could perhaps be fixed, but there may be other exceptions which I have not thought of, so I will roll back (most of) this patch. ] [Fixed improper printing of bound variable in sort checking of data. Andreas Abel **20120222214425] [take into account constraints again during instance argument resolution Dominique Devriese **20120222203103 Ignore-this: 9d13d61aee9e4d6bd87e4e4844ea6d09 ] [Show candidates for unresolved instance arguments constraints. steven.keuchel@gmail.com**20120221164719 Ignore-this: 6625291edf4f1d3c2de79be5d6683c40 ] [Make instance argument resolution consider candidates which still require implicit arguments. Dominique Devriese **20120221154302 Ignore-this: 67115c3a8291715c3c15732f743355ad Instance arguments resolution will now consider candidates which still need expect arguments. For example: record Eq (A : Set) : Set where field eq : A → A → Bool open Eq {{...}} eqFin : {n : ℕ} → Eq (Fin n) eqFin = record { eq = primEqFin } testFin : Bool testFin = eq fin1 fin2 The type-checker will now resolve the instance argument of the eq function to eqFin {_}. This is only done for implicit arguments, not instance arguments, so that the instance search stays non-recursive. ] [Correct expected error message for failing test case Issue551a.agda Dominique Devriese **20120221152835 Ignore-this: 788298954184d8978439e8f87d83cc39 ] [New menu entry: Information about the character at point. Nils Anders Danielsson **20120221195352 Ignore-this: 11c06beae4b277b6221df6e29b9bf32a ] [Added a header. Nils Anders Danielsson **20120221195335 Ignore-this: 2427f985d396c545b2e0078c0c98e7bb ] [Record declarations are no longer seen as mutual blocks. Nils Anders Danielsson **20120221193604 Ignore-this: 40495282d373a980c174c804bc93df12 ] [The positivity checker (and more) is now only run once per mutual block. Nils Anders Danielsson **20120221164108 Ignore-this: c02d62bd07614ac05df950300ff308e7 ] [Generalized newArgsMeta. Andreas Abel **20120221150813] [Fixed issue 569. Nils Anders Danielsson **20120221141503 Ignore-this: 9dfdfa6903793d3a648609ab28542aa1 ] [Simplify projection-like function treatment in solution of FindInScope cocnstraints Dominique Devriese **20120220172557 Ignore-this: 5a261bb900794e6f74b8b19a90bcde5a ] [Optimised transitiveClosure. Fixed bug (?) in nodes. Nils Anders Danielsson **20120220230742 Ignore-this: 909958a9b0ca58742ac22e5d452a761 + The transitiveClosure function now operates on one strongly connected component at a time. + Modified some uses of Map.union, which is claimed to be more efficient if the first argument is larger than the second. + The standard library type-checks with roughly 15% less memory now. + Previously the nodes function only returned nodes with at least one incoming or outgoing edge. ] [Removed trailing whitespace. Nils Anders Danielsson **20120220223328 Ignore-this: 31362c89590280e48391dd36d82a8e12 ] [Added elementsUnlessEmpty. Nils Anders Danielsson **20120220215052 Ignore-this: af2c7ea42332e3a3fc673ccf7eec61a9 ] [Added sccs, sccs', acyclic. Nils Anders Danielsson **20120220061455 Ignore-this: cf4b41d0e69be0b805eff4924fa34658 ] [Use -vtc.pos.graph:50 to see the positivity graphs' transitive closures. Nils Anders Danielsson **20120219203957 Ignore-this: 7fabc9a24919c6e40a0435ea564d6236 ] [Added some comments. Nils Anders Danielsson **20120219203728 Ignore-this: e0d067cf0c5ea950ded60fccd662057d ] [Removed unused error file. Nils Anders Danielsson **20120218114148 Ignore-this: de156661c885ae56d1b22e2b1f2485c1 ] [Prettier output for FindInScope constraints. steven.keuchel@gmail.com**20120220171518 Ignore-this: d6a6ad59e5872bbe58d426b9d9ccf54e ] [Restored behavior of OPTION --no-irrelevant-projections. Andreas Abel **20120220172250 It now actually does not generate projections for irrelevant record fields. ] [Use -vtc.decl.mutual:20 to see which mutual blocks are checked. Nils Anders Danielsson **20120217150659 Ignore-this: 8aa9b1bd8aa4c4355a29c10e23da0ba0 ] [Renamed currentMutualBlock to currentOrFreshMutualBlock. Nils Anders Danielsson **20120217143837 Ignore-this: 839a1fa4136a05dbc9a633add675e0c3 + The previous name led me to believe that currentMutualBlock did not modify the state. ] [Use the native Hashable instance for TypeRep introduced in hashable 1.1.2.3 patrick@parcs.ath.cx**20120215162257 Ignore-this: 41a6dee6d9705db4224c73379716a2cb Loading IO.agda now takes 31 seconds down from 38 seconds, a ~%20 improvement. ] [Fixed bug: Emacs jumped to errors after highlighting had been aborted. Nils Anders Danielsson **20120215191056 Ignore-this: a828f16b2ca16bc704b40630f5cb0c72 ] [Fixed bug: No highlighting after go-to-definition to new file. Nils Anders Danielsson **20120203231032 Ignore-this: c184ca10e274c1f7fdbd837be51441c6 ] [Reset local variable scope when checking with-clauses. Andreas Abel **20120214223212 This fixes issue 562. ] [Fixed issue 298b. No quick instantiations of size metas! Andreas Abel **20120214132343 Ignore-this: 49bc48e3acd072b285c9785a090ca716 ] [Internal change: Lazy monadic conjunction. Andreas Abel **20120214092022 Ignore-this: b00e020faab31a8a11a2cf716f286423 Added andM :: Monad m => [m Bool] -> m Bool to Agda.Utils.Monad. Typical uses: andM l (lazy) vs. and $ sequence l (strict) andM $ map f l (lazy) vs. and <$> mapM f l (strict) ] [Removed implicit args. from SizedBTree test case. Andreas Abel **20120213171149 Ignore-this: af35d93eac7f85832b8590345055c48 ] [A successful test for the combination of sized types and termination depth. Andreas Abel **20120213170941 Ignore-this: 2da1bd5bcfefa7b2b4dd46d0f466773c ] [Fixed polarity computation. Must be done after positivity check. Andreas Abel **20120213142233 Ignore-this: e1dd626b0a43014c0378107d890516ca Now, e.g., List is correctly recognized as covariant. This should fix some problems with sized types. ] [fixed issue 566: equal levels not comparing equal ulfn@chalmers.se**20120213120739 Ignore-this: 1f709f3f75d1e7a360286a1b15de601c ] [Workaround for the "Marker does not point anywhere" message. Nils Anders Danielsson **20120204165455 Ignore-this: de98819d9440b98014fd9985664c019c ] [Made an error message more informative. Nils Anders Danielsson **20120204165410 Ignore-this: a15171f8ad4de6d5d75354744d32ce6f ] [Info buffer: Point is now (again) moved to the top when APPEND is nil. Nils Anders Danielsson **20120203231229 Ignore-this: 4256db26b9fbc572898315432f315626 ] [Removed unnecessary calls to makeSilent. Nils Anders Danielsson **20120203225945 Ignore-this: a0bdc74b00a04e0f9fe572b54d7068de ] [fixed issue 552: new unifications weren't applied to the current substitution ulfn@chalmers.se**20120203155425 Ignore-this: 14998e1aa8a7044ac8a5d228c85d3c60 ] [fixed issue 530 ulfn@chalmers.se**20120203150756 Ignore-this: 585717373cecacbb1f21e4ea05b65a43 ] [Fixed bug: Highlighting was sometimes updated when it shouldn't. Nils Anders Danielsson **20120203092948 Ignore-this: 6e2431bfeff5a1f65e7714f86c126a0c ] [Fixed bug: Highlighting info files were written when they shouldn't be. Nils Anders Danielsson **20120131194046 Ignore-this: a076165f9e88fd825cb653d0d09aa1ae ] [Support for .lagda files in test/interaction. Nils Anders Danielsson **20120202092447 Ignore-this: f55c09ccdcfac2e80ae3a2a951f6848f ] [Agda info buffer: Unmapped 'g', switched to compilation major mode. Nils Anders Danielsson **20120131152211 Ignore-this: 9f372c9f86ae36e06f9915bf97ab021 ] [Fixed bug: Killed Agda info buffers were not recreated automatically. Nils Anders Danielsson **20120131145255 Ignore-this: 90165b92bab1468ba0bf65f6873f4b5c ] [Debug messages are now printed in a buffer called *Agda debug*. Nils Anders Danielsson **20120131134257 Ignore-this: de4371f4cdf2a8184de1fbcbe268a3b2 ] [Support for Emacs 24. Nils Anders Danielsson **20120131122342 Ignore-this: cac6376c917c6a55ccb23f5bba177af7 ] [Fixed issue 557. Andreas Abel **20120130212222 Function "absurd" generated for absurd lambda now applied to contextTelescope. ] [Made Agda build under GHC 7.4.1 rc2. Nils Anders Danielsson **20120129170850 Ignore-this: c0579fc14a0b53a4f3aa76874f427b4 ] [Changed the default for agda2-highlight-typechecks-face. Nils Anders Danielsson **20120129002733 Ignore-this: 6f46d1af86a3a87c473255d3b1ffe776 + I hope that the new face makes it a bit easier to locate the expression which is currently being type-checked. ] [Extended interactive highlighting to patterns. Nils Anders Danielsson **20120129000812 Ignore-this: 945e6d556dec2b5f2039f11bb7964 ] [Fixed bug: Highlighting of errors was sometimes overwritten. Nils Anders Danielsson **20120128233715 Ignore-this: 562f2afd5e79fa2b8884025616a71e4d ] [If text is appended to the info buffer, then point is placed at the end. Nils Anders Danielsson **20120128225944 Ignore-this: ef802c033b2334cfe9e8eb0bbc76c55a + This patch also makes the append functionality more smooth/efficient: previously the buffer was initialised every time something was written to it. ] [Fixed problem: Some commands were not echoed in the *ghci* buffer. Nils Anders Danielsson **20120128225944 Ignore-this: fbf348c5841a221a56967eb6c9dc2e3b ] [Fixed bug: Interactive highlighting aborted when ? turned into {!!}. Nils Anders Danielsson **20120128225944 Ignore-this: 5e247712ec2fef964d924d5805eb2b59 + Identified another problem (see TODO note in agda2-mode.el). ] [Emacs mode: Info about which module is currently being type-checked. Nils Anders Danielsson **20120128225944 Ignore-this: 41ff45ece8809d0a66d8c585ff920545 ] [Various changes related to interactive highlighting. Nils Anders Danielsson **20120128174349 Ignore-this: 1ee14a750688c55329497b327c7548c4 + This feature is not quite ready for deployment yet. ] [Modified a comment. Nils Anders Danielsson **20120128155553 Ignore-this: 7c19f557321dd427ff5122aab59f2232 ] [Removed writeFileAndSync. Nils Anders Danielsson **20120128125109 Ignore-this: 32518ea90bb33940babb1cd0509f28cf ] [Added writeFileAndSync. Nils Anders Danielsson **20120128125025 Ignore-this: 1a0d46065f66d7f1c30a6ac334e7edfa ] [Incremental Syntax Highlighting Guilhem Moulin **20120127153714 Ignore-this: 546a016b3aa0ee145f6b355ded67ecb4 ] [Experimental, incomplete, unfinished support for incremental highlighting. Nils Anders Danielsson **20110913040410 Ignore-this: cedff32884fd6e04ee8cdc808166c737 ] [Updated a test case. Nils Anders Danielsson **20120125145308 Ignore-this: 4e14d7f9cd8367185cfb9f60990fc0df ] [Reactivated a test case. Nils Anders Danielsson **20120125144754 Ignore-this: abf42e8fe4f8236b229aff6c016461dd ] [Modified the way in which test/fail/Makefile searches for test cases. Nils Anders Danielsson **20120125144159 Ignore-this: 4c1d8f73dc1dc70eb183179ba27222ec ] [Minor simplification. Nils Anders Danielsson **20120125142647 Ignore-this: b39aeb318dea402fbe2ff4c1e1bf2cf8 ] [Fixed bug related to module nesting levels. Nils Anders Danielsson **20120125141850 Ignore-this: 7421a8ddd7e573fe981a350c4233f53d ] [Improve fix for Issue 558, to also take into account projection like functions working on Axiom arguments. Dominique Devriese **20120124102743 Ignore-this: 7174970a44054be41b196dfbe3a57d6e ] [Fix issue #558: correctly handle projection functions in instance argument resolution: drop parameter arguments. Dominique Devriese **20120123210438 Ignore-this: 3d6c04f228a2bd75a160e6f332bfd110 ] [The "Checking..." messages are now indented (based on nesting level). Nils Anders Danielsson **20120123164621 Ignore-this: a299ad5f94fafb43fa7c41c267ab5936 ] [Made debug printouts more well-behaved. Nils Anders Danielsson **20120123152713 Ignore-this: 49f202125f5c82d2020eb88bf998ca1a + Tried to establish the invariant that debug printouts use the reportS/reportSLn/reportSDoc functions. This makes it easier to control them. + Added forkTCM, which is used by the new function Agda.Compiler.CallCompiler.callCompiler to feed compiler progress info to reportSLn. ] [Emacs mode: Commands are no longer broken over several lines. Nils Anders Danielsson **20120123152628 Ignore-this: 3d33860b94bafe5db4ae832dddab823d + The quote function now replaces newline characters with \n. + Remaining newline characters, if any, are replaced by spaces. ] [The Emacs mode now uses -v0 (by default). Nils Anders Danielsson **20120123145350 Ignore-this: 326b9c4427743268695513ca985e3dba + {-# OPTIONS -v... #-} is still supported. ] [Emacs mode: Debug messages are no longer printed out as plain text. Nils Anders Danielsson **20120123142727 Ignore-this: 22ff08daf85b580eda987d6b10d051e5 + Debug messages are wrapped in (agda2-verbose ...). ] [Updated expected outputs for interaction tests. Nils Anders Danielsson **20120123142657 Ignore-this: 473e471d85244e2495305f8d6b66ed8a ] [Replaced a call to putStrLn with a call to LocIO.putStrLn. Nils Anders Danielsson **20120123135020 Ignore-this: 8eb94b8a2011bf287ca69a9fff396332 ] [Another test case for issue 553. Nils Anders Danielsson **20120118110153 Ignore-this: 257208219298d1eb5e76daae7567b226 ] [Projection-like functions may not deeply match. Andreas Abel **20120117192929 This fixes issue 553. ] [Again fixing .err file (issue 554). andreas.abel@ifi.lmu.de**20120117154036 Ignore-this: 7301ca635af7989cb5068142c537fb6 ] [Fixed a comment. Nils Anders Danielsson **20120117135026 Ignore-this: ad8fe5119c0e9b25313d7efa7f068aa4 ] [Made envModuleNestingLevel work also when modules are skipped. Nils Anders Danielsson **20120117133627 Ignore-this: 67acced61c7f98f7a7fdca05505326a7 ] [Fixed a comment annotation. Nils Anders Danielsson **20120117131806 Ignore-this: 376e49d4fe7bffd9afe446984082d772 ] [Added envEmacs and envModuleNestingLevel. Nils Anders Danielsson **20120117124601 Ignore-this: 7a3b9a795264afdc828cd0f94b850c60 ] [Added the optional argument "append" to agda2-info-action. Nils Anders Danielsson **20120117122617 Ignore-this: 75f477f26eb738f6bf9afb2b3af7e472 + Modified display_info' in a similar way. ] [Checking the parameters of data and record definitions in new mutual style. Andreas Abel **20120117110921 This fixes issue 555. ] [Tried to fix issue 556. Nils Anders Danielsson **20120116191401 Ignore-this: e9a5fb513b1a9a1974a73c6924944a37 ] [Proper error message if data declaration gives more parameters than the type of the data type allows. Andreas Abel **20120113130640 Ignore-this: e71e11943f6302a00c73a15b565900e8 Fixes issue 555. Question: Do we want to also catch when less parameters than declared are given? See test/succeed/Issue555{a,b}.agda ] [Corrected error message of Issue551a. Andreas Abel **20120113122738 Ignore-this: fd66d01c09478f65520e74f70f305f94 ] [Release notes for builtin IRRAXIOM. Andreas Abel **20120112160315 Ignore-this: 4a42a8020b043715482174f3b67725 ] [Irrelevant record projections now use irrelevance axiom. Andreas Abel **20120112124600 Ignore-this: c4a75afae44e1b3e96b70404690e56a Added {-# BUILTIN IRRAXIOM irrAxiom #-} for postulate .irrAxiom : {a : Level}{A : Set a} -> .A -> A Irrelevant projections will produce something guarded by irrAxiom. This fixes issue 543. ] [Renamed primRelvance to primRelevance. Andreas Abel **20120112100217 Ignore-this: 395e97734c89b7a353b509a43065b95a Internal change, has no effect on Agda's behavior. ] [Instance search now ignores irrelevant stuff. Andreas Abel **20120111171803 Ignore-this: 394d3da2c140e3cc3f4a7b5701694807 This fixes Issue 551. ] [Regard let-bindings in instance search. Andreas Abel **20120111141805 Ignore-this: fbf562ccb127ed8e42824dc7b99e39aa This fixes issue 550. ] [Fixed issue 544. Nils Anders Danielsson **20120107231745 Ignore-this: 6e54d96a6d857cb8ea3052820fc5104a ] [Fix for issue 545. Nils Anders Danielsson **20120107225948 Ignore-this: 46a952ea24ef39dacf06b6811218e7be ] [In -v0 mode MAlonzo now throws away GHC progress info printed to stdout. Nils Anders Danielsson **20120103204002 Ignore-this: ff507a71e426f19bdb6a64fb6988dda5 ] [Fixed issue 539. Nils Anders Danielsson **20120103195041 Ignore-this: 90dd5a1e39ce59988cd05ff31fd011b7 + The range for "A" in "A.B.x" now includes the first dot (and similarly for "B"). ] [Updated benchmark code (the standard library has been changed). Nils Anders Danielsson **20111228213350 Ignore-this: 6581e7f9cc7cd548fbb9d67c8a1b5a3 ] [Epic 0.9 seems to work. Nils Anders Danielsson **20111228210605 Ignore-this: 5a752667f2329ddc26a118b7adb38b70 + Thanks to Dirk Ullrich for suggesting this change. ] [Support for GHC 7.4. Nils Anders Danielsson **20111228201856 Ignore-this: b068ade9c7200e72f199115ba1149680 + Thanks to Dirk Ullrich and Andrés Sicard-Ramírez for suggesting some of the changes. ] [Initial outline of the release notes for Agda 2.3.2. Nils Anders Danielsson **20111206182928 Ignore-this: 83be566340141a1e2250b8cad0b83ed8 ] [Comment on concrete pattern syntax. Andreas Abel **20111123155127] [Some comments on concrete and abstract syntax data types. Andreas Abel **20111123123714] [bumped version to 2.3.1 and put back -Werror ulfn@chalmers.se**20111123092520 Ignore-this: aeed0e31846af3905ca1b0739d098614 ] [TAG 2.3.0 ulfn@chalmers.se**20111123082405 Ignore-this: 4c903b4c3c6d853d95df4032f2efe090 ] Patch bundle hash: 26764c72266d9a323bc77a9867974935785cde19