1 patch for repository http://code.haskell.org/Agda: Mon Nov 1 20:36:47 EDT 2010 Wolfram Kahl * Added local type signatures for GHC-7 New patches: [Added local type signatures for GHC-7 Wolfram Kahl **20101102003647 Ignore-this: 518a5d8c7ba9e8ca81a8cf3805708b0b ] hunk ./src/full/Agda/Syntax/Scope/Base.hs 169 blockOfLines "names" (map pr $ Map.toList names) ++ blockOfLines "modules" (map pr $ Map.toList mods) where + pr :: (Show a, Show b) => (a,b) -> String pr (x, y) instance Show AbstractName where hunk ./src/full/Agda/Syntax/Scope/Base.hs 466 scopeLookup :: forall a. InScope a => C.QName -> ScopeInfo -> [a] scopeLookup q scope where + this :: A.ModuleName this hunk ./src/full/Agda/Syntax/Scope/Base.hs 468 + + current :: Scope current hunk ./src/full/Agda/Syntax/Scope/Base.hs 471 + + root :: Scope root tag hunk ./src/full/Agda/Syntax/Scope/Base.hs 477 + splitName :: C.QName -> [(C.QName, C.QName)] splitName (C.QName x) splitName (C.Qual x q) (m, r) <- splitName q hunk ./src/full/Agda/Syntax/Scope/Base.hs 483 return (C.Qual x m, r) + imported :: C.QName -> [A.ModuleName] imported q topImports :: [a] hunk ./src/full/Agda/Syntax/Scope/Base.hs 498 x <- findName x (restrictPrivate $ moduleScope m) return x + moduleScope :: A.ModuleName -> Scope moduleScope name Nothing -> __IMPOSSIBLE__ Just s -> s hunk ./src/full/Agda/Syntax/Scope/Base.hs 503 + lookupName :: forall a. InScope a => C.Name -> Scope -> [a] lookupName x s hunk ./src/full/Agda/Syntax/Scope/Base.hs 506 + findName :: forall a. InScope a => C.QName -> Scope -> [a] findName (C.QName x) s findName (C.Qual x q) s m <- nub $ mods ++ defs -- record types will appear bot as a mod and a def hunk ./src/full/Agda/Syntax/Scope/Base.hs 513 Just s' <- return $ Map.lookup m (scopeModules scope) findName q (restrictPrivate s') where + mods, defs :: [ModuleName] mods -- Qualified constructors are qualified by their datatype rather than a module defs hunk ./src/full/Agda/Syntax/Scope/Base.hs 546 [] -> Nothing x : _ -> Just x + unique :: forall a . [a] -> Bool unique [] unique [_] unique (_:_:_) Context: [Fixed issue 355 frelindb@chalmers.se**20101101171839 Ignore-this: 97d99d0a92b7b4626d573f382def0669 ] [removed update-cabal dependency for prof and fix-whitespace make targets ulfn@chalmers.se**20101029074749 Ignore-this: aff54f00033f9ca0c66fbb3d6a2d49c4 and made fix-whitespace work without configuring first ] [the compiler now inserts coercions that play well with ghc rewrite rules (I hope) ulfn@chalmers.se**20101029074005 Ignore-this: 16e80e2e3c7eeb1544ab7a5f133c6be0 ] [Highlighting on after go-to-definition to file in different project. Nils Anders Danielsson **20101026220414 Ignore-this: 46fa2f789e14852239f269882847cd49 + Previously, if one jumped to a definition in a file in a different "project" (under a different top-level directory), then one had to load the file in order to get syntax highlighting. Now highlighting is loaded automatically (in the common case: file not modified, file not already loaded by Emacs, etc.), and the proof state is not reset (usually). ] [Fixed bug: agda2-goals-action was sometimes invoked for the wrong buffer. Nils Anders Danielsson **20101025171154 Ignore-this: 707ed4df468d581d892c3f31004bc7af ] [Made it possible to infer ♯_ using the intro command. Nils Anders Danielsson **20101025161056 Ignore-this: 881586b7b939348d9ec10d898d382f4e ] [Included .el files in the strict whitespace regime. Nils Anders Danielsson **20101027143240 Ignore-this: 85f2dadd5e84d53c59392fc9e35d6418 ] [Removed unused rule. Nils Anders Danielsson **20101027134958 Ignore-this: 4b2487e201e89e5cdfad73ebef2a5fbb ] [Fixed issue 352 by writing a program which fixes whitespace issues. Nils Anders Danielsson **20101027133434 Ignore-this: e2ea20262286cc69fa074686686d396b + The Agda build can fail on Windows if CPP-processed files don't end with newline characters. + Whenever a patch is recorded the program checks that there are no whitespace issues. + One can fix these issues by running "make fix-whitespace". This can be done automatically by darcs record if a line record prehook make fix-whitespace is added to _darcs/prefs/defaults. + I took the liberty of imposing the additional condition that there must be no trailing white space, or trailing empty lines. ] [Converted some files from Latin-1 to UTF-8. Nils Anders Danielsson **20101027121247 Ignore-this: 58138f503f4034b22b7ee89762303428 ] [First draft of HCAR entry for November 2010. Nils Anders Danielsson **20101025090454 Ignore-this: 1e6d87afc31ec9388fa28165984315d ] [dropped unnecessary coercions for nat literals ulfn@chalmers.se**20101021093647 Ignore-this: c09fe261b8814b696e560e6147573677 and made Nat-Integer conversions more rewrite-friendly ] [Minor simplifications. Nils Anders Danielsson **20101018142022 Ignore-this: 4724e0736139455f592ab95db6f43592 ] [The first non-empty line can no longer be indented using TAB. Nils Anders Danielsson **20101018141624 Ignore-this: ffd805cfbc591f8c528970a2fbf9788d + (With the default settings.) ] [Fixed bug in eri-calculate-indentation-points. Nils Anders Danielsson **20101018135421 Ignore-this: ed0a4c7c4cf91dc61f26c78ddd478a50 + Bogus results were sometimes returned when the function was invoked on the first line of a buffer. ] [Updated some comments. Nils Anders Danielsson **20101018135016 Ignore-this: ea7309566d7d5cdd582eceee469cb874 ] [Fixed bug in eri-new-indentation-point. Nils Anders Danielsson **20101018133600 Ignore-this: 61f0ada4776d5df08d6a1e22461015b1 + Bogus results were sometimes returned when the function was invoked at or before the first line containing text. ] [Added save-excursion in eri-calculate-indentation-points-on-line. Nils Anders Danielsson **20101018132700 Ignore-this: ba038f38cfae342697462571e145a33 ] [Removed agda2-indentation. Nils Anders Danielsson **20101018125657 Ignore-this: 9346242956ae91af7fdf814bce37497d ] [Fixed compiler bug: no function was generated for INFINITY, only a type. Nils Anders Danielsson **20101020184358 Ignore-this: 81d662d6a8dbc968c8db904ea32754ac ] [Fixed problem with agda2-restart: GHCi has become harder to kill. Nils Anders Danielsson **20101020134359 Ignore-this: 1d3275a1e7046b4dfda2013feeb232e1 ] [Removed use of the TupleSections extension. Nils Anders Danielsson **20101018130001 Ignore-this: ae1b33d582ec9ab26c40a4eb02d62f2e + Perhaps Agda can now be built using GHC 6.10. ] [Typo in successful test case module name. andreas.abel@ifi.lmu.de**20101016155146] [Making eta-expansion even lazier. andreas.abel@ifi.lmu.de**20101015184808 In conversion test, only eta-expand when comparing a record against a neutral or another record, no longer when comparing against a meta variable. ] [No change. Some comments and debug prints for MetaVar code. andreas.abel@ifi.lmu.de**20101015175257] [Fixed issue 331. Meta-variables created by performKill had not been eta-expanded. andreas.abel@ifi.lmu.de**20101015162336 Just added one line to MetaVars/Occurs.hs, the rest is refactoring. ] [Added online to 2-2-10 release notes on projections preserve guardedness. andreas.abel@ifi.lmu.de**20101015153146] [Made eta-expansion of metavars more lazy in MetaVars.hs/etaExpandListeners. Solves issue 348. andreas.abel@ifi.lmu.de**20101015153050] [Projections preserve guardedness in the productivity (=termination) checker. andreas.abel@ifi.lmu.de**20101014075721] [Fixed issue 347 (eta expanding meta var forgets irrelevant record fields). andreas.abel@ifi.lmu.de**20101011172612 While this fix is indispensible for the soundness of Agda, note that some meta-variables which had been soundly resolved before, dont resolve any more. record R : Set where constructor mkR field fromR : A reflR : (r : R) -> r = r reflR r ] [Failing test cases: record constructors do not count as structural increase. andreas.abel@ifi.lmu.de**20101005133033] [Fixed issue 345, internal error in Auto Fredrik Lindblad **20101005083341 Ignore-this: 148bf7d44f7d0bf03118fd16dbedd5a6 ] [Release notes for irrelevant declarations and projections. andreas.abel@ifi.lmu.de**20101004170425] [Fixed issue 344: highlighting of field names. Nils Anders Danielsson **20101004135914 Ignore-this: 6df1203751a6683686c23d9c96e147ba ] [Updated an entry: record patterns did not exist before Agda 2.2.8. Nils Anders Danielsson **20101004135527 Ignore-this: 86bc4abd4bb55310ec8a47fc1f9ff9ef ] [Termination checker: stripping of a record constructor is no longer counted as decrease. andreas.abel@ifi.lmu.de**20101004100900] [Started release notes for 2.2.10. andreas.abel@ifi.lmu.de**20101004085937] [Failing test for termination checking translated record pattern. (see issue 334) andreas.abel@ifi.lmu.de**20101002192955] [Termination checker understands now record projections. andreas.abel@ifi.lmu.de**20101002192314 Added a field funProjection to Function definitions which indicates whether the function is a projection and which argument is the record argument. The termination checker knows that proj r <] [Compile DontCare as error instead of (). andreas.abel@ifi.lmu.de**20101001133559] [Fixed issue 342 (type checking constructors turned Funs into Pis). andreas.abel@ifi.lmu.de**20101001133519] [move the __IMPOSSIBLE__ triggered by the impossible failing test to a separate file ulfn@chalmers.se**20100930100615 Ignore-this: fe13424136446099202517ba44bbdcad to prevent the line number in the error message from changing ] [missing error message for failing test ulfn@chalmers.se**20100930095858 Ignore-this: 906099a500bbc7b067a6972ee1f75675 ] [added projections for irrelevant record fields (with --irrelevant-projections) ulfn@chalmers.se**20100930095832 Ignore-this: 595a7cc87104ac1360bd2d2e7ab4267b ] [Compiler now ignores irrelevant definitions and irrelevant arguments. andreas.abel@ifi.lmu.de**20100929193203] [Fixed typo. andreas.abel@ifi.lmu.de**20100929181610] [Minor factorization of duplicated code. andreas.abel@ifi.lmu.de**20100929181122] [Spotted opportunity for irrelevance in examples/simple-lib (two dots ;-)). andreas.abel@ifi.lmu.de**20100929150655] [.err file to testcase andreas.abel@ifi.lmu.de**20100929145205] [Testcase for bad irrelevant projections. andreas.abel@ifi.lmu.de**20100929145143] [Preliminary fix of issue 337 (generation of with functions in the presence of irrelevance). andreas.abel@ifi.lmu.de**20100929144945] [Added irrelevant function and axiom declarations .ident : Type andreas.abel@ifi.lmu.de**20100929084645 These can only be used in irrelevant positions. They can use other irrelevant declarations. ] [Test case for absurd matching on irrelevant empty type. andreas.abel@ifi.lmu.de**20100928201747] [Test cases for untyped and typed lambda, demonstrating that \ x is not \ (x : _) andreas.abel@ifi.lmu.de**20100928173706] [Typesig, comment, and some factoring for function TC.Rules.Term.checkArguments'. andreas.abel@ifi.lmu.de**20100928151619] [Bumped version to 2.2.9. Nils Anders Danielsson **20100927203646 Ignore-this: d8e25eefb66fc2fac2cd3cab5b5367b ] [TAG 2.2.8 Nils Anders Danielsson **20100927162925 Ignore-this: 24db4b37e559935c9cd6f81f8a90a6f7 ] Patch bundle hash: 0de125353f868a3b072c51337b7b51127091db03