Ticket #4462: 2010-11-01_GHC7_signatures.patch

File 2010-11-01_GHC7_signatures.patch, 12.7 KB (added by wkahl, 3 years ago)

Agda patch for GHC-7 compilation

Line 
11 patch for repository http://code.haskell.org/Agda:
2
3Mon Nov  1 20:36:47 EDT 2010  Wolfram Kahl <kahl@cas.mcmaster.ca>
4  * Added local type signatures for GHC-7
5
6New patches:
7
8[Added local type signatures for GHC-7
9Wolfram Kahl <kahl@cas.mcmaster.ca>**20101102003647
10 Ignore-this: 518a5d8c7ba9e8ca81a8cf3805708b0b
11] hunk ./src/full/Agda/Syntax/Scope/Base.hs 169
12       blockOfLines "names"   (map pr $ Map.toList names) ++
13       blockOfLines "modules" (map pr $ Map.toList mods)
14     where
15+      pr :: (Show a, Show b) => (a,b) -> String
16       pr (x, y) = show x ++ " --> " ++ show y
17 
18 instance Show AbstractName where
19hunk ./src/full/Agda/Syntax/Scope/Base.hs 466
20 scopeLookup :: forall a. InScope a => C.QName -> ScopeInfo -> [a]
21 scopeLookup q scope = nub $ findName q root ++ imports
22   where
23+    this    :: A.ModuleName
24     this    = scopeCurrent scope
25hunk ./src/full/Agda/Syntax/Scope/Base.hs 468
26+
27+    current :: Scope
28     current = moduleScope this
29hunk ./src/full/Agda/Syntax/Scope/Base.hs 471
30+
31+    root    :: Scope
32     root    = mergeScopes $ current : map moduleScope (scopeParents current)
33 
34     tag = inScopeTag :: InScopeTag a
35hunk ./src/full/Agda/Syntax/Scope/Base.hs 477
36 
37+    splitName :: C.QName -> [(C.QName, C.QName)]
38     splitName (C.QName x) = []
39     splitName (C.Qual x q) = (C.QName x, q) : do
40       (m, r) <- splitName q
41hunk ./src/full/Agda/Syntax/Scope/Base.hs 483
42       return (C.Qual x m, r)
43 
44+    imported :: C.QName -> [A.ModuleName]
45     imported q = maybe [] (:[]) $ Map.lookup q $ scopeImports root
46 
47     topImports :: [a]
48hunk ./src/full/Agda/Syntax/Scope/Base.hs 498
49       x <- findName x (restrictPrivate $ moduleScope m)
50       return x
51 
52+    moduleScope :: A.ModuleName -> Scope
53     moduleScope name = case Map.lookup name (scopeModules scope) of
54       Nothing -> __IMPOSSIBLE__
55       Just s  -> s
56hunk ./src/full/Agda/Syntax/Scope/Base.hs 503
57 
58+    lookupName :: forall a. InScope a => C.Name -> Scope -> [a]
59     lookupName x s = maybe [] id $ Map.lookup x (allNamesInScope s)
60 
61hunk ./src/full/Agda/Syntax/Scope/Base.hs 506
62+    findName :: forall a. InScope a => C.QName -> Scope -> [a]
63     findName (C.QName x)  s = lookupName x s
64     findName (C.Qual x q) s = do
65         m <- nub $ mods ++ defs -- record types will appear bot as a mod and a def
66hunk ./src/full/Agda/Syntax/Scope/Base.hs 513
67         Just s' <- return $ Map.lookup m (scopeModules scope)
68         findName q (restrictPrivate s')
69       where
70+        mods, defs :: [ModuleName]
71         mods = amodName <$> lookupName x s
72         -- Qualified constructors are qualified by their datatype rather than a module
73         defs = mnameFromList . qnameToList . anameName <$> lookupName x s
74hunk ./src/full/Agda/Syntax/Scope/Base.hs 546
75       []    -> Nothing
76       x : _ -> Just x
77 
78+    unique :: forall a . [a] -> Bool
79     unique []      = __IMPOSSIBLE__
80     unique [_]     = True
81     unique (_:_:_) = False
82
83Context:
84
85[Fixed issue 355
86frelindb@chalmers.se**20101101171839
87 Ignore-this: 97d99d0a92b7b4626d573f382def0669
88]
89[removed update-cabal dependency for prof and fix-whitespace make targets
90ulfn@chalmers.se**20101029074749
91 Ignore-this: aff54f00033f9ca0c66fbb3d6a2d49c4
92   and made fix-whitespace work without configuring first
93]
94[the compiler now inserts coercions that play well with ghc rewrite rules (I hope)
95ulfn@chalmers.se**20101029074005
96 Ignore-this: 16e80e2e3c7eeb1544ab7a5f133c6be0
97]
98[Highlighting on after go-to-definition to file in different project.
99Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101026220414
100 Ignore-this: 46fa2f789e14852239f269882847cd49
101 + Previously, if one jumped to a definition in a file in a different
102   "project" (under a different top-level directory), then one had to
103   load the file in order to get syntax highlighting. Now highlighting
104   is loaded automatically (in the common case: file not modified, file
105   not already loaded by Emacs, etc.), and the proof state is not reset
106   (usually).
107]
108[Fixed bug: agda2-goals-action was sometimes invoked for the wrong buffer.
109Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101025171154
110 Ignore-this: 707ed4df468d581d892c3f31004bc7af
111]
112[Made it possible to infer ♯_ using the intro command.
113Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101025161056
114 Ignore-this: 881586b7b939348d9ec10d898d382f4e
115]
116[Included .el files in the strict whitespace regime.
117Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101027143240
118 Ignore-this: 85f2dadd5e84d53c59392fc9e35d6418
119]
120[Removed unused rule.
121Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101027134958
122 Ignore-this: 4b2487e201e89e5cdfad73ebef2a5fbb
123]
124[Fixed issue 352 by writing a program which fixes whitespace issues.
125Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101027133434
126 Ignore-this: e2ea20262286cc69fa074686686d396b
127 + The Agda build can fail on Windows if CPP-processed files don't end
128   with newline characters.
129 + Whenever a patch is recorded the program checks that there are no
130   whitespace issues.
131 + One can fix these issues by running "make fix-whitespace". This can
132   be done automatically by darcs record if a line
133     record prehook make fix-whitespace
134   is added to _darcs/prefs/defaults.
135 + I took the liberty of imposing the additional condition that there
136   must be no trailing white space, or trailing empty lines.
137]
138[Converted some files from Latin-1 to UTF-8.
139Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101027121247
140 Ignore-this: 58138f503f4034b22b7ee89762303428
141]
142[First draft of HCAR entry for November 2010.
143Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101025090454
144 Ignore-this: 1e6d87afc31ec9388fa28165984315d
145]
146[dropped unnecessary coercions for nat literals
147ulfn@chalmers.se**20101021093647
148 Ignore-this: c09fe261b8814b696e560e6147573677
149   and made Nat-Integer conversions more rewrite-friendly
150]
151[Minor simplifications.
152Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101018142022
153 Ignore-this: 4724e0736139455f592ab95db6f43592
154]
155[The first non-empty line can no longer be indented using TAB.
156Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101018141624
157 Ignore-this: ffd805cfbc591f8c528970a2fbf9788d
158 + (With the default settings.)
159]
160[Fixed bug in eri-calculate-indentation-points.
161Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101018135421
162 Ignore-this: ed0a4c7c4cf91dc61f26c78ddd478a50
163 + Bogus results were sometimes returned when the function was invoked
164   on the first line of a buffer.
165]
166[Updated some comments.
167Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101018135016
168 Ignore-this: ea7309566d7d5cdd582eceee469cb874
169]
170[Fixed bug in eri-new-indentation-point.
171Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101018133600
172 Ignore-this: 61f0ada4776d5df08d6a1e22461015b1
173 + Bogus results were sometimes returned when the function was invoked
174   at or before the first line containing text.
175]
176[Added save-excursion in eri-calculate-indentation-points-on-line.
177Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101018132700
178 Ignore-this: ba038f38cfae342697462571e145a33
179]
180[Removed agda2-indentation.
181Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101018125657
182 Ignore-this: 9346242956ae91af7fdf814bce37497d
183]
184[Fixed compiler bug: no function was generated for INFINITY, only a type.
185Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101020184358
186 Ignore-this: 81d662d6a8dbc968c8db904ea32754ac
187]
188[Fixed problem with agda2-restart: GHCi has become harder to kill.
189Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101020134359
190 Ignore-this: 1d3275a1e7046b4dfda2013feeb232e1
191]
192[Removed use of the TupleSections extension.
193Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101018130001
194 Ignore-this: ae1b33d582ec9ab26c40a4eb02d62f2e
195 + Perhaps Agda can now be built using GHC 6.10.
196]
197[Typo in successful test case module name.
198andreas.abel@ifi.lmu.de**20101016155146]
199[Making eta-expansion even lazier.
200andreas.abel@ifi.lmu.de**20101015184808
201 In conversion test, only eta-expand when comparing a record against a neutral
202 or another record, no longer when comparing against a meta variable.
203]
204[No change. Some comments and debug prints for MetaVar code.
205andreas.abel@ifi.lmu.de**20101015175257]
206[Fixed issue 331.  Meta-variables created by performKill had not been eta-expanded.
207andreas.abel@ifi.lmu.de**20101015162336
208 Just added one line to MetaVars/Occurs.hs, the rest is refactoring.
209]
210[Added online to 2-2-10 release notes on projections preserve guardedness.
211andreas.abel@ifi.lmu.de**20101015153146]
212[Made eta-expansion of metavars more lazy in MetaVars.hs/etaExpandListeners. Solves issue 348.
213andreas.abel@ifi.lmu.de**20101015153050]
214[Projections preserve guardedness in the productivity (=termination) checker.
215andreas.abel@ifi.lmu.de**20101014075721]
216[Fixed issue 347 (eta expanding meta var forgets irrelevant record fields).
217andreas.abel@ifi.lmu.de**20101011172612
218 While this fix is indispensible for the soundness of Agda, note that some
219 meta-variables which had been soundly resolved before, dont resolve any more.
220 record R : Set where
221   constructor mkR
222   field
223     fromR : A
224 reflR : (r : R) -> r == r
225 reflR r = refl  -- unsolved metas here, only (refl {a = r}) works
226]
227[Failing test cases: record constructors do not count as structural increase.
228andreas.abel@ifi.lmu.de**20101005133033]
229[Fixed issue 345, internal error in Auto
230Fredrik Lindblad <frelindb@chalmers.se>**20101005083341
231 Ignore-this: 148bf7d44f7d0bf03118fd16dbedd5a6
232]
233[Release notes for irrelevant declarations and projections.
234andreas.abel@ifi.lmu.de**20101004170425]
235[Fixed issue 344: highlighting of field names.
236Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101004135914
237 Ignore-this: 6df1203751a6683686c23d9c96e147ba
238]
239[Updated an entry: record patterns did not exist before Agda 2.2.8.
240Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101004135527
241 Ignore-this: 86bc4abd4bb55310ec8a47fc1f9ff9ef
242]
243[Termination checker: stripping of a record constructor is no longer counted as decrease.
244andreas.abel@ifi.lmu.de**20101004100900]
245[Started release notes for 2.2.10.
246andreas.abel@ifi.lmu.de**20101004085937]
247[Failing test for termination checking translated record pattern. (see issue 334)
248andreas.abel@ifi.lmu.de**20101002192955]
249[Termination checker understands now record projections.
250andreas.abel@ifi.lmu.de**20101002192314
251 Added a field funProjection to Function definitions which indicates
252 whether the function is a projection and which argument is the record
253 argument.  The termination checker knows that proj r <= r.
254]
255[Compile DontCare as error instead of ().
256andreas.abel@ifi.lmu.de**20101001133559]
257[Fixed issue 342 (type checking constructors turned Funs into Pis).
258andreas.abel@ifi.lmu.de**20101001133519]
259[move the __IMPOSSIBLE__ triggered by the impossible failing test to a separate file
260ulfn@chalmers.se**20100930100615
261 Ignore-this: fe13424136446099202517ba44bbdcad
262   to prevent the line number in the error message from changing
263]
264[missing error message for failing test
265ulfn@chalmers.se**20100930095858
266 Ignore-this: 906099a500bbc7b067a6972ee1f75675
267]
268[added projections for irrelevant record fields (with --irrelevant-projections)
269ulfn@chalmers.se**20100930095832
270 Ignore-this: 595a7cc87104ac1360bd2d2e7ab4267b
271]
272[Compiler now ignores irrelevant definitions and irrelevant arguments.
273andreas.abel@ifi.lmu.de**20100929193203]
274[Fixed typo.
275andreas.abel@ifi.lmu.de**20100929181610]
276[Minor factorization of duplicated code.
277andreas.abel@ifi.lmu.de**20100929181122]
278[Spotted opportunity for irrelevance in examples/simple-lib (two dots ;-)).
279andreas.abel@ifi.lmu.de**20100929150655]
280[.err file to testcase
281andreas.abel@ifi.lmu.de**20100929145205]
282[Testcase for bad irrelevant projections.
283andreas.abel@ifi.lmu.de**20100929145143]
284[Preliminary fix of issue 337 (generation of with functions in the presence of irrelevance).
285andreas.abel@ifi.lmu.de**20100929144945]
286[Added irrelevant function and axiom declarations .ident : Type
287andreas.abel@ifi.lmu.de**20100929084645
288 These can only be used in irrelevant positions. 
289 They can use other irrelevant declarations.
290]
291[Test case for absurd matching on irrelevant empty type.
292andreas.abel@ifi.lmu.de**20100928201747]
293[Test cases for untyped and typed lambda, demonstrating that \ x is not \ (x : _)
294andreas.abel@ifi.lmu.de**20100928173706]
295[Typesig, comment, and some factoring for function TC.Rules.Term.checkArguments'.
296andreas.abel@ifi.lmu.de**20100928151619]
297[Bumped version to 2.2.9.
298Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100927203646
299 Ignore-this: d8e25eefb66fc2fac2cd3cab5b5367b
300]
301[TAG 2.2.8
302Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100927162925
303 Ignore-this: 24db4b37e559935c9cd6f81f8a90a6f7
304]
305Patch bundle hash:
3060de125353f868a3b072c51337b7b51127091db03