Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /bugs/trunk/bugs.0401-0600
ViewVC logotype

Annotation of /bugs/trunk/bugs.0401-0600

Parent Directory Parent Directory | Revision Log Revision Log


Revision 1345 - (view) (download)

1 : macqueen 944 Number: 401
2 :     Title: Imperative types in SML/NJ 0.66
3 :     Keywords: types, weak types, polymorphism
4 :     Submitter: Dave Berry <db@lfcs.edinburgh.ac.uk>
5 :     Date: 2/14/91
6 :     Version: 0.66
7 :     System:
8 :     Severity:
9 :     Problem:
10 :     The following program compiles under Poly/ML 1.86, but fails to compile
11 :     under SML/NJ 0.66.
12 :    
13 :    
14 :     fun create (x:int) (y:'_a) :'_a Array.array = Array.array (x, y)
15 :    
16 :     type ('a,'b) table = ('a*int*'b) list Array.array
17 :    
18 :     val defaultSize = 97
19 :    
20 :     fun createDefault (sample'value :'_a) :(string, '_a) table =
21 :     let val mt = [] : (string * int * '_a) list
22 :     in create defaultSize mt
23 :     end
24 :    
25 :    
26 :     It will compile if Array.array is used directly in place of the curried
27 :     version. It will also compile if createDefault is given an extra parameter,
28 :     either before or after the existing one.
29 :    
30 :     This is the simplest example I've run across of SML/NJ failing to type
31 :     correct SML use of imperative types. It's fairly simple in this case -
32 :     it only took me a day to get the case this simple - but I've come across
33 :     at least one other example that I've just given up on.
34 :    
35 :     I remember Dave MacQueen and mads Tofte discussing a bug in the SML/NJ
36 :     algorithm at the Edinburgh Workshop. Is there any chance of a fix?
37 :    
38 :     Dave.
39 :    
40 :    
41 :     From: jhr@cs.cornell.edu (John Reppy)
42 :     This problem was pointed out by Jim O'Toole. Anyway, it was fixed
43 :     in 0.67:
44 :    
45 :     Standard ML of New Jersey, Version 0.68-JHR, January 25, 1991
46 :     val it = () : unit
47 :     - fun create (x:int) (y:'_a) :'_a Array.array = Array.array (x, y)
48 :     = type ('a,'b) table = ('a*int*'b) list Array.array
49 :     = val defaultSize = 97
50 :     = fun createDefault (sample'value :'_a) :(string, '_a) table =
51 :     = let val mt = [] : (string * int * '_a) list
52 :     = in create defaultSize mt
53 :     = end;
54 :     val create = fn : int -> '1a -> '1a array
55 :     type ('a,'b) table = ('a * int * 'b) list array
56 :     val defaultSize = 97 : int
57 :     val createDefault = fn : '1a -> (string,'1a) table
58 :     -
59 :     Status: fixed in 0.67
60 :     ---------------------------------------------------------------------------
61 :     Number: 402
62 :     Title: local non-declarations
63 :     Keywords:
64 :     Submitter: Bernard Berthomieu (bernard@laas.laas.fr)
65 :     Date: 30/1/90
66 :     Version: 0.66
67 :     System: SUN Sparstation 1+, SunOS 4.0.3c
68 :     Severity: minor
69 :     Problem: some declarations not accepted
70 :     Code: local val x = 5 in 20 + x end;
71 :     Transcript: - local val x = 5 in 20 + x end;
72 :     std_in:1.21 Error: syntax error found at INT
73 :     Comments: Not sure this is a bug, but the SML documents are not clear
74 :     about this. According to my interpretation of the standard
75 :     grammar, this declaration should be equivalent to the following:
76 :     - local val x = 5 in val it = 20 + x end;
77 :     val it = 25 : int
78 :     Fix: expressions are considered as declarations ONLY at top level.
79 :     Status: not a bug
80 :     ---------------------------------------------------------------------------
81 :     Number: 403
82 :     Title: 0.0/0.0 not properly handled on Sparc
83 :     Keywords:
84 :     Submitter: Bernard Berthomieu (bernard@laas.laas.fr)
85 :     Date: 30/1/90
86 :     Version: 0.66
87 :     System: SUN Sparstation 1+, SunOS 4.0.3c
88 :     Severity: minor
89 :     Problem: 0.0/0.0 not properly handled
90 :     Code: 0.0/0.0
91 :     Transcript: - 0.0/0.0;
92 :     strange floating point error (* and sml exits *)
93 :     Comments: 0.0/0.0 is generally considered in implementations
94 :     of reals as an "invalid operation" rather than a "division
95 :     by zero" (exception code FPE_FLTOPERR_TRAP on SUNs OS 4.0).
96 :     I did not checked the effect of 0.0/0.0 on other targets
97 :     than SUN 4s, but it might have strange effects too;
98 :    
99 :     Submitter: Josh Hodas (hodas@cs.hmc.edu)
100 :     Date: 3/6/95
101 :     System(s) and Version: ???
102 :     SML/NJ Version: 0.93
103 :     Machine: Sparc 1000 / SunOs 5.3
104 :     Severity: minor
105 :     Problem: The 0.0/0.0 bug that generates "strange floating point
106 :     error 0x7" and exits to unix, which was (according to
107 :     the master bugs file) fixed in 0.68 has returned.
108 :    
109 :     Code: 0.0/0.0;
110 :     Transcript:
111 :    
112 :     Standard ML of New Jersey, Version 0.93, February 15, 1993
113 :     val it = () : unit
114 :     - 0.0/0.0;
115 :     strange floating point error, 0x7
116 :     Owner: John
117 :     Status: obsolete [new basis]
118 :     ---------------------------------------------------------------------------
119 :     Number: 404
120 :     Title: std_out not flushed on read from std_in
121 :     Keywords:
122 :     Submitter: Kim Dam Petersen (kimdam@sun.tfl.dk)
123 :     Date: 6/1/91
124 :     Version: 0.66
125 :     System: all
126 :     Severity: minor
127 :     Problem: std_out not flushed on read from std_in
128 :     Comments:
129 :     As printing on the standard output and error streams usually are
130 :     flushed automatically I would suggest that this should be part of the
131 :     standard behaviour of these stream.
132 :    
133 :     It seems that NJ/ML delays output flushing until the computation of a
134 :     top level expression has completed. As mentioned above flushing
135 :     should be performed immediately. A temporary solution in NJ/ML is
136 :     to redefine the `output' function, such that the predefined
137 :     `flush_out' is automatically called:
138 :    
139 :     val output = fn(s,t) => (output(s,t); flush_out s)
140 :    
141 :     Future call of `output' will print the text immediately.
142 :     Status: fixed in 0.71
143 :     ---------------------------------------------------------------------------
144 :     Number: 405
145 :     Title: identifiers starting with underscores are incorrectly allowed
146 :     Keywords:
147 :     Submitter: Mick Francis (Abstract Hardware)
148 :     Date: 8/1/91
149 :     Version: 0.66
150 :     System: all
151 :     Severity: minor
152 :     Problem: identifiers starting with underscores are incorrectly allowed
153 :     Status: fixed in 0.73
154 :     ---------------------------------------------------------------------------
155 :     Number: 406
156 :     Title: funny signatures in 0.71
157 :     Keywords:
158 :     Submitter: John Reppy
159 :     Date: 8/1/91
160 :     Version: 0.71
161 :     System: all
162 :     Severity: minor
163 :     Problem: Array.tabulate and String.chr have wrong types
164 :     in initial environment
165 :     Status: fixed in 0.73
166 :     ---------------------------------------------------------------------------
167 :     Number: 407
168 :     Title: create_v_v for SPARC
169 :     Keywords:
170 :     Submitter: Juergen Buntrock TUB, jubu@cs.tu-berlin.de
171 :     Date: 9/24/91
172 :     Version: 0.73
173 :     System: sun4c SUNOS 4.1.1
174 :     Severity: major
175 :     Problem:
176 :     The mask is not set in create_v_v (SPARC.prim.s)
177 :     segmentation fault
178 :     in collect_roots in callgc.c
179 :     Fix:
180 :     diff -c SPARC.prim.s.org SPARC.prim.s
181 :    
182 :     *** SPARC.prim.s.org Fri Aug 23 20:33:54 1991
183 :     --- SPARC.prim.s Tue Sep 24 19:11:30 1991
184 :     ***************
185 :     *** 476,481 ****
186 :     --- 476,483 ----
187 :     nop
188 :     4:
189 :     CONTINUE
190 :     + .word closmask /* reg. mask */
191 :     + .word 0
192 :    
193 :     3:
194 :     add %g0,0,%g0 /* nop to get PC adjust right */
195 :    
196 :     Status: fixed in 0.74
197 :     ---------------------------------------------------------------------------
198 :     Number: 408
199 :     Title: feedback from module system
200 :     Keywords:
201 :     Submitter: tmb@ai.mit.edu
202 :     Date: 08/03/91
203 :     Version: 0.70
204 :     System: Sun4/OS4.1.1
205 :     Severity: cosmetic, but important
206 :    
207 :     I have been playing around with building functors that abstract
208 :     various notions of "iteration", "array", "sequence", and "index"
209 :     (ultimately, this will hopefully provide a nicer alternative to the
210 :     equivalent data structures in the current SML library).
211 :    
212 :     In general, using the ML module and type system for this seems
213 :     straightforward and natural, and I'm much more pleased with the way I
214 :     can design this code in SML than with similar code that I have written
215 :     in Scheme, CommonLisp, and C++.
216 :    
217 :     However, I have also come across some cosmetic but (to me) important
218 :     problems with the NJ/SML module system.
219 :    
220 :     Some of the problems are that the system isn't telling me enough about
221 :     the identity of objects to allow me to debug the code without having
222 :     to guess much; something analogous to the LispMachine inspector and
223 :     mouse sensitivity would ultimately be very useful, but for the time
224 :     being, just reporting unique tags for objects instead of "?" would be
225 :     sufficient.
226 :    
227 :     Some of this might also be a question of style, but my ignorance is
228 :     partially due to the fact that the only uses of the module system that
229 :     I have seen have been rather simple and straightforward (even if they
230 :     involve lots of code).
231 :    
232 :     I'd appreciate your feedback.
233 :    
234 :     Thanks, Thomas.
235 :    
236 :     PS: I can send you the complete code if you are interested, but
237 :     it is still more of a sketch or prototype.
238 :    
239 :     = 1 ================================================================
240 :    
241 :     I have a functor which generates iteration constructs for some data
242 :     type that it is handed (e.g., it generates "fold", "apply", etc. for
243 :     lists and arrays). It is very confusing that the types that the system
244 :     reports for the functions generated by this functor involve types of
245 :     the form "('a,'b) value" and "('a,'b) index". It would be much better
246 :     if the types were reported in their true form.
247 :    
248 :     signature S = sig type ('a,'b) data end;
249 :     functor F(structure X:S) = struct fun f(x:('a,'b) X.data):('a,'b) X.data = x end;
250 :     structure A = struct type ('a,'b) data = 'b list end;
251 :     structure B = F(structure X=A);
252 :    
253 :     - B.f([1]);
254 :     val it = [1] : ('a,int) A.data
255 :     -
256 :    
257 :     What I would want is:
258 :    
259 :     - B.f([1]);
260 :     val it = [1] : int list
261 :     -
262 :    
263 :     Obviously, which form one wants depends on the exact use that a
264 :     functor is going to be put to. There should be a mechanism for me to
265 :     specify in the type binding which form of reporting I prefer.
266 :    
267 :     = 2 ================================================================
268 :    
269 :     Another problem that I have encountered is that it is nearly
270 :     impossible to figure out what goes wrong with complicated functor
271 :     applications with the current level of reporting: elements of
272 :     intermediate structures are now often only reported as
273 :     "?.KeyIndexing.foo", and it isn't helpful if the compiler tells you
274 :     that "?.KeyIndexing.foo" is a different type from "?.KeyIndexing.foo".
275 :    
276 :     It would be much more convenient if there was an option to the
277 :     compiler that would trace and report functor applications, and if the
278 :     printer gave unique identities to structures, even temporary ones.
279 :    
280 :     Something like:
281 :    
282 :     - use "foo";
283 :     [Applying functor F<10> to structure <1001> giving structure <347> bound to structure T]
284 :     [Applying functor G<11> to structure <66> giving structure <67> bound to structure T.M]
285 :     [Applying functor G<11> to structure <33> giving structure <68> bound to structure T.M]
286 :     - T.i;
287 :     val it = SOMETHING : <11>.my_type;
288 :     -
289 :    
290 :     Printing unique ID's for structures (and, for that matter, for other
291 :     objects) shouldn't be hard, and it makes debugging so much easier.
292 :    
293 :     = 3 ================================================================
294 :    
295 :     When writing signatures for functors that generate polymorphic
296 :     functions, I seem to have to define types that carry around one type
297 :     variable for each polymorphic type, e.g.:
298 :    
299 :     signature BASICACCESS =
300 :     sig
301 :     type ('a,'b) point
302 :     type ('a,'b) value
303 :     type ('a,'b) index
304 :     type ('a,'b) range
305 :     val first: ('a,'b) range -> ('a,'b) index
306 :     val succ: ('a,'b) index -> ('a,'b) index
307 :     val done: ('a,'b) index -> bool
308 :     val mkindex: ('a,'b) point * ('a,'b) range -> ('a,'b) index
309 :     val at: ('a,'b) index -> ('a,'b) value
310 :     end;
311 :    
312 :     Most of the polymorphic functions that get generated from BASICACCESS
313 :     structures will never need both type variables, while others may need
314 :     more than two.
315 :    
316 :     For example,
317 :    
318 :     structure BasicListIndex =
319 :     struct
320 :     type ('a,'b) point = 'a list
321 :     type ('a,'b) value = 'a
322 :     type ('a,'b) index = 'a list
323 :     type ('a,'b) range = 'a list
324 :     fun first x = x
325 :     val succ = tl
326 :     val done = null
327 :     fun mkindex(x,y) = x
328 :     fun at x = System.Unsafe.cast (hd x) (* bug in NJSML .70 type checker ? *)
329 :     end;
330 :    
331 :     structure BasicArrayIndex =
332 :     struct
333 :     type ('a,'b) point = int
334 :     type ('a,'b) index = int * int
335 :     type ('a,'b) range = int
336 :     fun first(limit:('a,'b) range):('a,'b) index = (0,limit)
337 :     fun succ((x,limit):('a,'b) index):('a,'b) index = (x+1,limit)
338 :     fun done((x,limit):('a,'b) index):bool = x>=limit
339 :     fun at x = x
340 :     fun mkindex(x,r) = (x,r)
341 :     fun index1((x,_):('a,'b) index) = x
342 :     end;
343 :    
344 :     Carrying around the dummy type variables on types like "('a,'b) point"
345 :     is a bother. Perhaps a simple solution would be to allow the user to
346 :     omit type variables if they are specified as wildcards, e.g., "type
347 :     ('_,'_) point = int" can be used simply as "val x : point" with the
348 :     compiler inserting the missing (wildcard) type variables by
349 :     convention.
350 :    
351 :     More generally, it would seem to be nice if type constructors could
352 :     take variable numbers of arguments, and if they could pass their
353 :     argument lists around as complete entities (analogous to passing
354 :     around tuples of arguments in ML).
355 :    
356 :     Another possibility would be to allow "free" type variables:
357 :    
358 :     type point = '_ list
359 :    
360 :     This would simply be syntactic sugar for
361 :    
362 :     type 'a point = 'a list
363 :    
364 :     and the compiler would implicitly provide a dummy argument to "point"
365 :     wherever it is used. However, this may break other parts of the type
366 :     or module system.
367 :    
368 :     Point 3 is really about a basic problem with the current
369 :     way signatures and functors handle types, not about "'_".
370 :    
371 :     Essentially, I want to write functors that generate objects
372 :     that are polymorphic in different ways, e.g., that sometimes
373 :     generate a function "f : 'a -> 'a" and sometimes "f : 'a -> 'b".
374 :    
375 :     The only way I could find of writing signatures for such functors is to
376 :     make both the LHS and the RHS types (e.g. type ('a,'b) arg; type
377 :     ('a,'b) result) that depend on two type variables and instantiate them
378 :     in the matching structures to the correct types. This causes a number
379 :     of problems that I mentioned in my previous message.
380 :    
381 :     Another possibility would be to allow a function of type "'a -> 'a"
382 :     to match a type specification "'a -> 'b", but that does not
383 :     currently work.
384 :    
385 :     Functors that generate functions that are polymorphic
386 :     in different ways are very important, and, one way or another,
387 :     SML must make this more convenient than it is right now.
388 :    
389 :     Thanks, Thomas.
390 :     = 4 ================================================================
391 :    
392 :     A related problem is that nongeneric weak type variables
393 :     generate an error even if they are never used:
394 :    
395 :     - val x: '0a t = 3;
396 :     std_in:3.1-3.16 Error: nongeneric weak type variable
397 :     x : '0aU t
398 :     -
399 :    
400 :     I think you can guess from the above structures and functors
401 :     how such non-generic weak type variables can pop up unexpectedly
402 :     (they are easy to fix for the user, by simply giving a type
403 :     to the value, but it seems odd for a user of, say structure
404 :     "Array2D" to have to specify some type as "(unit,int) array"
405 :     just to create an array of type "int array").
406 :    
407 :     = 5 ================================================================
408 :    
409 :     A minor problem with wildcard type variables:
410 :    
411 :     - type ('_,'_) a;
412 :     std_in:7.7-7.11 Error: duplicate type variable: '1
413 :     std_in:7.7-7.11 Error: duplicate type variable: '1
414 :     std_in:7.7-7.11 Error: duplicate type variable: '1
415 :     std_in:7.7-7.11 Error: duplicate type variable: '1
416 :     std_in:7.7-7.11 Error: duplicate type variable: '1
417 :     -
418 :    
419 :     I think the "'_" should refer to a new type variable every time it is
420 :     used (this is, after all, what "_" does in ML).
421 :    
422 :     Followup discussion:
423 :    
424 :     Dave MacQueen writes:
425 :     > What you are looking for may be rather difficult to do within the
426 :     > framework of the ML type system. At first glance it appears to
427 :     > require a serious innovation in the type system to capture an
428 :     > abstraction that could instantiate to both "f : 'a -> 'a" and
429 :     > "f : 'a -> 'b" (note that these two types have different numbers of
430 :     > bound variables).
431 :     >
432 :     > Do you have any suggestions as to how this could be done?
433 :    
434 :     I believe it is possible to express type constraints like this
435 :     with SML:
436 :    
437 :     signature S =
438 :     sig
439 :     type ('a,'b) from
440 :     type ('a,'b) to
441 :     val f : ('a,'b) from -> ('a,'b) to
442 :     end;
443 :    
444 :     structure X:S =
445 :     struct
446 :     type ('a,'b) from = 'a
447 :     type ('a,'b) to = 'a
448 :     fun f(x) = x
449 :     end;
450 :    
451 :     structure Y:S =
452 :     struct
453 :     type ('a,'b) from = 'a * 'b
454 :     type ('a,'b) to = 'a
455 :     fun f(x,y) = x
456 :     end;
457 :    
458 :     (These are actually not accepted by NJ/SML 0.70, even if the types for
459 :     "f" are fully specified in the structure definitions (you get a
460 :     different error message in that case), but I think that's a bug.)
461 :    
462 :     The main problem is that this use of types in signatures seems to have
463 :     been rather uncommon so far, so, at least NJ/SML has several
464 :     difficulties with it:
465 :    
466 :     * the type checker/module system (incorrectly?) rejects
467 :     some constructs like this
468 :    
469 :     * unused type variables need to be instantiated by
470 :     the user when they become weak; instead, the
471 :     language could automatically define such variables to
472 :     be "unit"
473 :    
474 :     * the type constructors "from" and "to" are really
475 :     auxilliary, and users of S most likely never want
476 :     to see them printed; the current system prints them
477 :    
478 :     * the writer of the signature "S" has to pick a maximum
479 :     number of auxilliary type variables used as arguments
480 :     to "from" and "to", but I believe that the actual maximum
481 :     number needed depends on the arguments given to the functor,
482 :     not on the functor itself
483 :    
484 :     I want to state again that I think this feature is important. Without
485 :     the ability to specify signatures that can match structures that are
486 :     polymorphic in different ways, it seems I would have to write
487 :     completely redundant versions of some functors.
488 :    
489 :     The context in which it came up was writing a functor that generates
490 :     iteration constructs for collections; for some collections, indexes
491 :     and values are different types, for others, they are the same type.
492 :    
493 :     Status: not a bug
494 :     ---------------------------------------------------------------------------
495 :     Number: 409
496 :     Title: type checking after functor application
497 :     Keywords:
498 :     Submitter: tmb@ai.mit.edu
499 :     Date: 08/05/91
500 :     Version: 0.70
501 :     System: Sun4/OS4.1.1
502 :     Severity: ?
503 :     Problem:
504 :    
505 :     Basically, I have something like:
506 :    
507 :     functor F(...) =
508 :     struct
509 :     structure A = G(...);
510 :     ...
511 :     open A
512 :     end;
513 :    
514 :     structure X = F(...);
515 :    
516 :     X.A.f arg; --> works
517 :     X.f arg; --> fails with a type error
518 :    
519 :     Comment:
520 :    
521 :     X.A.f and X.f must refer to the same value with the same type: A has
522 :     simply been opened at the end of structure X. I don't see how X.f
523 :     could ever behave differently from X.A.f.
524 :    
525 :     Sorry about the long code needed to reproduce the bug. I had several
526 :     guesses what the problem might be due to, but I have not been able
527 :     to reduce the code further than this. In particular, the problem
528 :     goes away if the last functor application is removed, i.e.,
529 :    
530 :     functor GeneralArray(structure Index:BASICACCESS) = struct ... end;
531 :     structure Arrays = GeneralArray(structure Index = BasicArrayIndex);
532 :    
533 :     is replaced with
534 :    
535 :     structure Arrays =
536 :     struct
537 :     structure Index:BASICACCESS = BasicArrayIndex
538 :     ... body of functor GeneralArray ...
539 :     end
540 :    
541 :     Also, don't try to make sense of the code. To isolate the bug this
542 :     far, I collapsed several types.
543 :    
544 :     Code: (file foo.sml)
545 :     signature BASICACCESS =
546 :     sig
547 :     type ('a,'b) index
548 :     type ('a,'b) range
549 :     val first: ('a,'b) range -> ('a,'b) index
550 :     val succ: ('a,'b) index -> ('a,'b) index
551 :     val done: ('a,'b) index -> bool
552 :     end;
553 :    
554 :     functor GeneralIteration(structure Access:BASICACCESS) =
555 :     struct
556 :     local
557 :     open Access
558 :     in
559 :     fun apply f r =
560 :     let
561 :     fun loop(i) = if done(i) then () else (f(i); loop(succ(i)))
562 :     in
563 :     loop(first(r))
564 :     end
565 :     end
566 :     end;
567 :    
568 :     functor GeneralArray(structure Index:BASICACCESS) =
569 :     struct
570 :     type ('a,'b) array = 'b Array.array * ('a,'b) Index.range
571 :    
572 :     structure ValueIndex =
573 :     struct
574 :     type ('a,'b) range = ('a,'b) array
575 :     type ('a,'b) index = 'b Array.array * ('a,'b)Index.index
576 :     fun first((a,r):('a,'b) range) = (a,Index.first(r))
577 :     fun succ((a,r):('a,'b) index) = (a,Index.succ(r))
578 :     fun done((a,r):('a,'b) index) = Index.done(r)
579 :     end
580 :    
581 :     structure Value = GeneralIteration(structure Access = ValueIndex)
582 :    
583 :     fun array(r:(unit,'1b) Index.range,initial):(unit,'1b) array =
584 :     (Array.array(100,initial),r)
585 :    
586 :     open Value
587 :     end;
588 :    
589 :     structure BasicArrayIndex =
590 :     struct
591 :     type ('a,'b) index = int * int
592 :     type ('a,'b) range = int
593 :     fun first(limit:('a,'b) range):('a,'b) index = (0,limit)
594 :     fun succ((x,limit):('a,'b) index):('a,'b) index = (x+1,limit)
595 :     fun done((x,limit):('a,'b) index):bool = x>=limit
596 :     end;
597 :    
598 :     structure Arrays = GeneralArray(structure Index = BasicArrayIndex);
599 :    
600 :     Transcript:
601 :     volterra$ sml
602 :     Standard ML of New Jersey, Version 0.70, 1 July 1991
603 :     val it = () : unit
604 :     - use "foo.sml";
605 :     [opening foo.sml]
606 :     signature BASICACCESS =
607 :     sig
608 :     type ('a,'b) index
609 :     type ('a,'b) range
610 :     val done : ('a,'b) index -> bool
611 :     val first : ('a,'b) range -> ('a,'b) index
612 :     val succ : ('a,'b) index -> ('a,'b) index
613 :     end
614 :     functor GeneralIteration : <sig>
615 :     functor GeneralArray : <sig>
616 :     structure BasicArrayIndex :
617 :     sig
618 :     eqtype ('a,'b) index
619 :     eqtype ('a,'b) range
620 :     val done : ('a,'b) index -> bool
621 :     val first : ('a,'b) range -> ('a,'b) index
622 :     val succ : ('a,'b) index -> ('a,'b) index
623 :     end
624 :     structure Arrays :
625 :     sig
626 :     structure Value : sig...end
627 :     structure ValueIndex : sig...end
628 :     eqtype ('a,'b) array
629 :     val apply : (('a,'b) ?.ValueIndex.index -> 'c) -> ('a,'b) ?.ValueIndex.range
630 :     -> unit
631 :     val array : (unit,'1a) BasicArrayIndex.range * '1a -> (unit,'1a) array
632 :     end
633 :     [closing foo.sml]
634 :     val it = () : unit
635 :     - val x = Arrays.array(100,0);
636 :     val x = (prim?,100) : (unit,int) Arrays.array
637 :     - Arrays.Value.Apply (fn a => a) x;
638 :     std_in:4.1-4.18 Error: unbound variable or constructor in structure: Apply
639 :     - Arrays.Value.apply (fn a => a) x;
640 :     val it = () : unit
641 :     - Arrays.apply (fn a => a) x;
642 :     std_in:2.1-2.26 Error: operator and operand don't agree (tycon mismatch)
643 :     operator domain: ('Z,int) ?.ValueIndex.range
644 :     operand: (unit,int) Arrays.array
645 :     in expression:
646 :     Arrays.apply ((fn <pat> => <exp>)) x
647 :     - volterra$
648 :    
649 :     Status: fixed in 0.73
650 :     ---------------------------------------------------------------------------
651 :     Number: 410
652 :     Title: inlining property not preserved in simple renaming
653 :     Keywords:
654 :     Submitter: Andrew Tolmach (apt@cs.princeton.edu)
655 :     Date: 8/6/91
656 :     Version: 0.73
657 :     Severity: minor
658 :     Problem:
659 :     If I use System.Unsafe.getvar directly, it is inlined, as expected.
660 :    
661 :     If I type
662 :    
663 :     val g = System.Unsafe.getvar
664 :    
665 :     then g does not have access INLINE.
666 :    
667 :     Dbm suggests that this is because g is being eta-expanded; I haven't found
668 :     where this happens in the source.
669 :    
670 :     In any case, I don't know why the initial definition of
671 :    
672 :    
673 :     val getvar = InLine.getvar
674 :    
675 :     inside the definition of System.Unsafe *does* manage to transfer the inline
676 :     property... Is it because there's something special about structure InLine?
677 :    
678 :     Fix: look for MARKexps around the rhs VALvar.
679 :     Tolmach: abstract syntax marking. The MARKexps surrounding the RHS of
680 :    
681 :     val a = System.Unsafe.getvar
682 :    
683 :     prevent the INLINE-ness of getvar being recognized by parse/corelang.sml valbind.
684 :     If I turn off marking, it works.
685 :     Tarditi: We should alter parse/corelang.sml valbind so that it recognizes this
686 :     case specially and properly assigns the INLINE property.
687 :    
688 :     Status: fixed in 0.74
689 :     ---------------------------------------------------------------------------
690 :     Number: 411
691 :     Title: Runbind
692 :     Keywords:
693 :     Submitter: John Reppy (jhr)
694 :     Date: 8/10/91
695 :     Version: 0.71
696 :     Problem: Runbind exception
697 :     Transcript:
698 :    
699 :     Standard ML of New Jersey, Version 0.71, 23 July 1991
700 :     val it = () : unit
701 :     - structure A = struct val x = 1 end;
702 :     structure A :
703 :     sig
704 :     val x : int
705 :     end
706 :     - structure B = struct structure A = A; val y = 2 end;
707 :     structure B :
708 :     sig
709 :     structure A : sig...end
710 :     val y : int
711 :     end
712 :     - open A;
713 :     open A
714 :     - open B;
715 :     open B
716 :     - x;
717 :    
718 :     uncaught exception Runbind
719 :    
720 :     Status: fixed in 0.73
721 :     ---------------------------------------------------------------------------
722 :     Number: 412
723 :     Title: Runbind
724 :     Keywords:
725 :     Submitter: Dave Tarditi
726 :     Date: 8/13/91
727 :     Version: 0.71
728 :     Problem:
729 :     Code:
730 :     structure A =
731 :     struct
732 :     val x = 5
733 :     structure B =
734 :     struct
735 :     val y = 5
736 :     end
737 :     end
738 :    
739 :     open A.B;
740 :     structure A = struct end;
741 :     y;
742 :     Comments: (Tarditi)
743 :     There's an incorrect assumption in checkopen, which tests whether
744 :     any value in a structure which has been rebound is still accessible.
745 :     Let the old structure be called S and the new environment be N. Let
746 :     the symbols bound in the environment of S be T. The assumption is
747 :     that if any symbol A in T is unbound in N, then all other symbols
748 :     in T are also unbound in N. This is clearly untrue, as the above
749 :     example shows, where x is unbound in the environment after the redefinition
750 :     of A but y is not.
751 :    
752 :     Status: fixed in 0.73
753 :     ---------------------------------------------------------------------------
754 :     Number: 413
755 :     Title: System and IO problems
756 :     Keywords:
757 :     Submitter: Emden Gansner
758 :     Date: 8/16/91
759 :     Version: 0.71
760 :     Problem:
761 :     The version of system in the System structure should have type string -> int
762 :    
763 :     The execute function in IO is incorrect as written. It passes the
764 :     the value of environ() to exec, but this is a list of SML strings
765 :     and exec expects a list of C strings. It should pass (map c_string environ())
766 :     instead.
767 :    
768 :     Finally, the execute function would be a lot more useful if it allowed
769 :     a list of arguments as well as program pathname.
770 :     Status: fixed in 0.74 (JHR)
771 :     ---------------------------------------------------------------------------
772 :     Number: 414
773 :     Title: getWD wrong
774 :     Keywords:
775 :     Submitter : Ian King <ik@sys.uea.ac.uk>
776 :     Date: 8/19/91
777 :     Version : 0.66
778 :     System : Sun 3/160 , Sun OS 4.1
779 :     Severity : Minor
780 :     Problem : The function getWD in structure System.Directory when called
781 :     with a unit gives an incoorect result.
782 :     Code : fun test path =
783 :     let
784 :     val cwd = System.Directory.getWD ()
785 :     in
786 :     { cd_in = fn () => (cd path),
787 :     cd_out = fn () => (cd cwd) }
788 :     end
789 :     Transcipt : val {cd_in,cd_out} = test "directoryname";
790 :     val cd_in = fn : unit -> unit
791 :     val cd_out = fn : unit -> unit
792 :    
793 :     cd_in ();
794 :     val it = () : unit;
795 :    
796 :     cd_out ();
797 :     uncaught exception NotDirectory
798 :    
799 :     Comments : This code executes correctly on a Sun Sparc machine. It does not
800 :     execute correctly on our Sun 3/160. Although I have marked the
801 :     bug as minor it is irritating because it crashes code which
802 :     needs to change directories such as loaders.
803 :     ** This is probably another example of bug #651 (JHR, 10/6/92) **
804 :     Status: fixed in 0.75
805 :     ---------------------------------------------------------------------------
806 :     Number: 415
807 :     Title: late error detection in parsing
808 :     Keywords:
809 :     Submitter: David N. Turner <dnt@dcs.ed.ac.uk>
810 :     Date: 9/17/91
811 :     Version: SML of NJ version 0.73
812 :     System: Sun4
813 :     Severity: minor
814 :     Problem:
815 :    
816 :     The following incorrect text doesn't generate an error,
817 :     the secondary prompt appears and the error is only signalled
818 :     after more text if typed in. Perhaps this is some kind of
819 :     parser lookahead problem?
820 :    
821 :     - if true then 365; (* My input *)
822 :     = (* nj-sml output *)
823 :     Owner: Andrew
824 :     Status: open
825 :     ---------------------------------------------------------------------------
826 :     Number: 416
827 :     Title: equality property checking in functor parameter matching
828 :     Keywords: modules, functors, signature matching, equality
829 :     Submitter: Simon Finn <simon@abstract-hardware-ltd.co.uk>
830 :     Date: 9/13/91
831 :     Version: ?
832 :     Severity: minor
833 :     Problem:
834 :     Try the following simple (?) exercise in semantics, provided by my
835 :     colleague Mike Crawley:
836 :    
837 :     signature PSIG =
838 :     sig
839 :     eqtype 'a symTab ;
840 :     datatype guide = G1 | G2 of guide symTab
841 :     end;
842 :    
843 :     (Q1) Is guide an eqtype? (in PSIG)
844 :     (A1) Yes, since we require the equality-principal signature.
845 :    
846 :     functor PFUN (structure S : sig type 'a symTab end) =
847 :     struct
848 :     open S;
849 :     datatype guide = G1 | G2 of guide symTab;
850 :     end;
851 :    
852 :     (Q2) Is guide an eqtype? (in the output signature of PFUN)
853 :     (A2) No, because symTab isn't and our signatures must respect equality
854 :    
855 :    
856 :     structure S = struct datatype 'a symTab = Empty end;
857 :     structure P = PFUN(structure S = S);
858 :    
859 :     (Q3) Is guide an eqtype? (in the signature of P)
860 :     (A3) No, because it wasn't in the functor.
861 :     Technically, this is because the realisation, \phi, used
862 :     to instantiate the body of the functor doesn't touch
863 :     the bound type names contained in the output signature
864 :     of the functor (except, possibly, for an alpha-conversion).
865 :    
866 :     P.G1 = P.G1;
867 :    
868 :     (Q4) Is this legal?
869 :     (A4) No, because P.guide is not an eqtype (see above).
870 :    
871 :     functor MFUN(structure X : PSIG) =
872 :     struct
873 :     val z = X.G1 = X.G1;
874 :     end;
875 :     structure M = MFUN(structure X = P);
876 :    
877 :     (Q5) Is this legal?
878 :     (A5) No, because MFUN demands that guide be an eqtype (see Q1),
879 :     but P.guide is not an eqtype (see Q3, Q4).
880 :    
881 :    
882 :     Both SMLNJ 0.66 and Poly/ML 1.88 get Q1 - Q4 right but get Q5 wrong.
883 :     Poly/ML 1.98 gets Q1 - Q5 right.
884 :    
885 :     Comment: Conjecture that this is a benign bug. Have not been able to
886 :     come up with version that is actually wrong.
887 :    
888 :     Fix: Could record equality properties inferred in parameter signature
889 :     instantiation in the signature (memoizing).
890 :    
891 :     Test: bug416.sml
892 :     Owner: dbm
893 :     Status: open
894 :     ---------------------------------------------------------------------------
895 :     Number: 417
896 :     Title: cosmetic error message suggestion
897 :     Keywords: error message
898 :     Submitter: Andy Koenig
899 :     Date: 9/12/91
900 :     Version: ?
901 :     Problem:
902 :     Minor suggestion for SML-NJ: in error messages, how about
903 :     printing infix functions as infix?
904 :    
905 :     Transcript:
906 :     - 3 + 4.0;
907 :     std_in:1.1-1.7 Error: operator and operand don't agree (tycon mismatch)
908 :     operator domain: int * int
909 :     operand: int * real
910 :     in expression:
911 :     + (3,4.0)
912 :     ^^^^^^^^^ Why not 3+4.0 ??
913 :     or at least op+ (3,4.0)
914 :    
915 :     Comment: use original code in error message instead of "pretty-printing"
916 :     abstract syntax
917 : macqueen 1345 Owner: dbm
918 :     Status: fixed
919 : macqueen 944 ---------------------------------------------------------------------------
920 :     Number: 418
921 :     Title: repeated type names in type declarations
922 :     Keywords:
923 :     Submitter: Andrzej Filinski <andrzej@cs.cmu.edu>
924 :     Date: 9/11/91
925 :     Version: 0.72
926 :     System: All
927 :     Severity: minor (but with potentially serious consequences)
928 :     Problem: Repeated type names in DATATYPE ... WITHTYPE ...
929 :     destroy type security.
930 :     Transcript: Standard ML of New Jersey, Version 0.72, 29 August 1991
931 :     val it = () : unit
932 :     - datatype t = T of int withtype t = string;
933 :     datatype t
934 :     con T : int -> t
935 :     type t = string
936 :     - T 65:string;
937 :     val it = "A" : string
938 :     -
939 :     Comments: Same problem with ABSTYPE...WITHTYPE. See also bug report 349.
940 :    
941 :     Status: fixed in 0.74
942 :     ---------------------------------------------------------------------------
943 :     Number: 419
944 :     Title: Runbind
945 :     Keywords:
946 :     Submitter: Venkatesh Akella akella@cs.utah.edu
947 :     Date: 8/27/91
948 :     Version: SML of NJ version 0.71
949 :     System: Sparc IPC, SunOS
950 :     Severity: major
951 :     Problem: Raises an uncaught exception Runbind when
952 :     a simple CML program running under SML version 0.71
953 :     (Version of CML being used is 0.95)
954 :     The bug can't be reproduced with CML version 0.90 running
955 :     under SML/NJ 0.66
956 :     Code:
957 :    
958 :     fun placeBuffer () =
959 :     let
960 :     val c = channel ()
961 :     val b = channel ()
962 :     val a = channel ()
963 :     fun input_int (s:string) =
964 :     fold (fn(a,r) => ord(a) - ord("0") + 10 * r) (tl (rev(explode s))) 0;
965 :    
966 :     fun P1 x = (CIO.print( "Waiting for Input on Channel a? \n");
967 :     let
968 :     val y = input_int(CIO.input_line std_in)
969 :     in
970 :     s__3 x y
971 :     end)
972 :     and
973 :     s__3 x y = ( ( send (c,y ) ; P1 y ))
974 :    
975 :     fun P2 z = (let val v = accept c in s__5 z v end)
976 :     and
977 :     s__5 z v =
978 :     ( (CIO.print (" Output on Channel b!"^Integer.makestring(v)^"\n");
979 :     P2 v ))
980 :     in
981 :     spawn (fn () => P1 4 );
982 :     spawn (fn () => P2 5 );
983 :     ()
984 :     end;
985 :    
986 :     Transcript:
987 :    
988 :     6 bliss /u/akella/compiler/cml/cml95/cml-0.9.5:: > cml
989 :     val it = true : bool
990 :     - System.Directory.cd "/u/akella/compiler/hop/example";
991 :     val it = () : unit
992 :     - use "test_buf.sml";
993 :     [opening test_buf.sml]
994 :     [closing test_buf.sml]
995 :    
996 :     uncaught exception Runbind
997 :     -
998 :    
999 :     Comments:
1000 :     The same bug was observed in SML/NJ version 0.66 too but in
1001 :     a different context. I had one integrated environment with
1002 :     SML 0.66, ML-yacc, ML-lex, CML(version 0.9) and my own code.
1003 :    
1004 :     Status: fixed in 0.74
1005 :     ---------------------------------------------------------------------------
1006 :     Number: 420
1007 :     Title: uncaught Nth while compiling
1008 :     Keywords:
1009 :     Submitter: Tsung-Min Kuo kuo@ecrc.de
1010 :     Date: 9/19/91
1011 :     Version: Version 0.66, 15 September 1990
1012 :     System: SPARCstation 1, SUNOS 4.0
1013 :     Severity: sever
1014 :     Problem: Compiler-generated exception : uncaught exception Nth
1015 :     Code:
1016 :     signature EXCHANGE_STRUCTURE =
1017 :     sig
1018 :     type tree
1019 :     val new_node : tree -> tree
1020 :     end
1021 :    
1022 :     structure ex : EXCHANGE_STRUCTURE =
1023 :     struct
1024 :     datatype tree = Subwindow of subwindow
1025 :     | Canvas of canvas
1026 :     | Frame of frame
1027 :     | Baseframe of baseframe
1028 :     | NULL
1029 :     withtype subwindow = {t_node: tree}
1030 :     and canvas = {subwindow: subwindow}
1031 :     and frame = {tree_node: tree}
1032 :     and baseframe = {frame: frame,foog:bool}
1033 :    
1034 :     exception Tube_Bug
1035 :    
1036 :     fun position (Canvas c) = position(Subwindow(#subwindow c))
1037 :     | position (Baseframe bf) = position(Frame (#frame bf))
1038 :     | position _ = raise Tube_Bug
1039 :    
1040 :     fun tn_set_position(t,p) = ()
1041 :     fun set_position (Subwindow sb) = tn_set_position(#t_node sb,0)
1042 :     | set_position (Frame f) = tn_set_position(#tree_node f,0)
1043 :     | set_position (Canvas c) = set_position(Subwindow(#subwindow c))
1044 :     | set_position (Baseframe bf) = set_position(Frame(#frame bf))
1045 :     | set_position _ = raise Tube_Bug
1046 :    
1047 :     fun components(Canvas c) = components(Subwindow (#subwindow c))
1048 :     | components(Baseframe bf) = components(Frame (#frame bf))
1049 :     | components _ = raise Tube_Bug
1050 :    
1051 :     fun bounding_box(Canvas c) = bounding_box(Subwindow (#subwindow c))
1052 :     | bounding_box(Baseframe bf) = bounding_box(Frame (#frame bf))
1053 :     | bounding_box _ = raise Tube_Bug
1054 :    
1055 :     fun tn_set_bounding_box(t,r) = ()
1056 :     fun set_bounding_box(Subwindow sb) = tn_set_bounding_box(#t_node sb,0)
1057 :     | set_bounding_box(Frame f) = tn_set_bounding_box(#tree_node f,0)
1058 :     | set_bounding_box(Canvas c) = set_bounding_box(Subwindow(#subwindow c))
1059 :     | set_bounding_box(Baseframe bf) = set_bounding_box(Frame(#frame bf))
1060 :     | set_bounding_box _ = raise Tube_Bug
1061 :    
1062 :     fun new_node tl =
1063 :     let
1064 :     val pos = position(Frame {tree_node = tl})
1065 :     in
1066 :     NULL
1067 :     end
1068 :     end
1069 :    
1070 :     Transcript:
1071 :     - use "bug";
1072 :     [opening bug]
1073 :     [closing bug]
1074 :    
1075 :     uncaught exception Nth
1076 :     -
1077 :     Comments: The enclosed code is a trimmed version of a big program, got in an
1078 :     attempt to isolate the error. As you can see, this program virtually
1079 :     does nothing and is full of redundancy. But whatever I did to try to
1080 :     cut it down, results in a good program happily accepted by compiler.
1081 :     Here are some of the things I have tried :
1082 :     * not use the signature constraint on the structure
1083 :     * delete any of the redundant function definitions, e.g."components"
1084 :     * remove the redundant call to function "position" in "new_node"
1085 :     * or, even call "position" with argument NULL
1086 :     * remove a clause from any function definition(I tried many of them)
1087 :     * flat the record, e.g. make type frame = tree
1088 :     * remove the boolean field in type "baseframe"
1089 :     * get rid of second argument of functions "tn_set_position" and
1090 :     "tn_set_bounding_box"
1091 :     * replace equal by equal, e.g. replace calls to "tn_set_position"
1092 :     by ()
1093 :     * replace recursive call by direct call, e.g. in "Canvas" clause of
1094 :     function "set_position"
1095 :     Conclusion: These are so diverse that I can not even guess any.
1096 :    
1097 :     Status: fixed in 0.73
1098 :     ---------------------------------------------------------------------------
1099 :     Number: 421
1100 :     Title: getWD under SPARC/Mach (same as 353)
1101 :     Keywords:
1102 :     Submitter: Fritz Knabe <Frederick_Knabe@ARCTIC.FOX.CS.CMU.edu>
1103 :     Date: 9/18/91
1104 :     Version: 0.73
1105 :     System: SPARC/Mach (CMU)
1106 :     Severity: minor
1107 :     Problem:
1108 :     System.Directory.getWD () is still broken for me in version 73
1109 :     on a Sparc. It raises a SystemCall exception.
1110 :     Transcript: (c/o Gene Rollins, 8/21/92)
1111 :     Standard ML of New Jersey, Version 0.88, August 14, 1992
1112 :     with SourceGroup 2.2 built on Mon Aug 17 23:23:16 EDT 1992
1113 :     - fun pwd() = System.system "pwd";
1114 :     val pwd = fn : unit -> int
1115 :     - fun cd x = (System.Directory.cd x; pwd()) handle any => (pwd(); raise any);
1116 :     val cd = fn : string -> int
1117 :     - fun ll () = System.system "ls -lL";
1118 :     val ll = fn : unit -> int
1119 :     - fun mkdir x = System.system ("mkdir " ^ x);
1120 :     val mkdir = fn : string -> int
1121 :     - pwd();
1122 :     /usr0/rollins
1123 :     val it = 0 : int
1124 :     - ll();
1125 :     total 0
1126 :     val it = 0 : int
1127 :     - mkdir "src";
1128 :     val it = 0 : int
1129 :     - mkdir "bin";
1130 :     val it = 0 : int
1131 :     - ll();
1132 :     total 2
1133 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1134 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1135 :     val it = 0 : int
1136 :     - cd "src";
1137 :     /usr0/rollins/src
1138 :     val it = 0 : int
1139 :     - cd "../bin";
1140 :     /usr0/rollins/bin
1141 :     val it = 0 : int
1142 :     - cd "../src";
1143 :     /usr0/rollins/src
1144 :     val it = 0 : int
1145 :     - cd "..";
1146 :     /usr0/rollins
1147 :     val it = 0 : int
1148 :     - cd "bin";
1149 :     /usr0/rollins/bin
1150 :     val it = 0 : int
1151 :     - cd "..";
1152 :     /usr0/rollins
1153 :     val it = 0 : int
1154 :     - ll();
1155 :     total 2
1156 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1157 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1158 :     val it = 0 : int
1159 :     - mkdir "tools";
1160 :     val it = 0 : int
1161 :     - cd "src";
1162 :     /usr0/rollins/src
1163 :     val it = 0 : int
1164 :     - cd "../tools";
1165 :     /usr0/rollins/src
1166 :    
1167 :     uncaught exception NotDirectory
1168 :     - cd "../bin";
1169 :     /usr0/rollins/bin
1170 :     val it = 0 : int
1171 :     - cd "../tools";
1172 :     /usr0/rollins/bin
1173 :    
1174 :     uncaught exception NotDirectory (* the rest is more of the same *)
1175 :     - cd "..";
1176 :     /usr0/rollins
1177 :     val it = 0 : int
1178 :     - cd "tools";
1179 :     /usr0/rollins/tools
1180 :     val it = 0 : int
1181 :     - cd "../src";
1182 :     /usr0/rollins/src
1183 :     val it = 0 : int
1184 :     - cd "../tools";
1185 :     /usr0/rollins/src
1186 :    
1187 :     uncaught exception NotDirectory
1188 :     - cd "..";
1189 :     /usr0/rollins
1190 :     val it = 0 : int
1191 :     - ll();
1192 :     total 3
1193 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1194 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1195 :     drwxr-xr-x 2 rollins 512 Aug 20 12:17 tools
1196 :     val it = 0 : int
1197 :     - mkdir "mo.mipsl";
1198 :     val it = 0 : int
1199 :     - ll();
1200 :     total 4
1201 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1202 :     drwxr-xr-x 2 rollins 512 Aug 20 12:18 mo.mipsl
1203 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1204 :     drwxr-xr-x 2 rollins 512 Aug 20 12:17 tools
1205 :     val it = 0 : int
1206 :     - cd "mo.mipsl";
1207 :     /usr0/rollins
1208 :    
1209 :     uncaught exception NotDirectory
1210 :     - cd "src";
1211 :     /usr0/rollins/src
1212 :     val it = 0 : int
1213 :     - cd "../mo.mipsl";
1214 :     /usr0/rollins/mo.mipsl
1215 :     val it = 0 : int
1216 :     - cd "../tools";
1217 :     /usr0/rollins/mo.mipsl
1218 :    
1219 :     uncaught exception NotDirectory
1220 :     - cd "../bin";
1221 :     /usr0/rollins/bin
1222 :     val it = 0 : int
1223 :     - cd "../mo.mipsl";
1224 :     /usr0/rollins/mo.mipsl
1225 :     val it = 0 : int
1226 :     - cd "..";
1227 :     /usr0/rollins
1228 :     val it = 0 : int
1229 :     - cd "mo.mipsl";
1230 :     /usr0/rollins
1231 :    
1232 :     uncaught exception NotDirectory
1233 :     - ll();
1234 :     total 4
1235 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1236 :     drwxr-xr-x 2 rollins 512 Aug 20 12:18 mo.mipsl
1237 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1238 :     drwxr-xr-x 2 rollins 512 Aug 20 12:17 tools
1239 :     val it = 0 : int
1240 :     - mkdir "zed";
1241 :     val it = 0 : int
1242 :     - ll();
1243 :     total 5
1244 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1245 :     drwxr-xr-x 2 rollins 512 Aug 20 12:18 mo.mipsl
1246 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1247 :     drwxr-xr-x 2 rollins 512 Aug 20 12:17 tools
1248 :     drwxr-xr-x 2 rollins 512 Aug 20 12:23 zed
1249 :     val it = 0 : int
1250 :     - cd "zed";
1251 :     /usr0/rollins/zed
1252 :     val it = 0 : int
1253 :     - cd "../tools";
1254 :     /usr0/rollins/zed
1255 :    
1256 :     uncaught exception NotDirectory
1257 :     - cd "../src";
1258 :     /usr0/rollins/src
1259 :     val it = 0 : int
1260 :     - cd "../zed";
1261 :     /usr0/rollins/zed
1262 :     val it = 0 : int
1263 :     - cd "..";
1264 :     /usr0/rollins
1265 :     val it = 0 : int
1266 :     - mkdir "moon";
1267 :     val it = 0 : int
1268 :     - cd "moon";
1269 :     /usr0/rollins
1270 :    
1271 :     uncaught exception NotDirectory
1272 :     - cd "src";
1273 :     /usr0/rollins/src
1274 :     val it = 0 : int
1275 :     - cd "../moon";
1276 :     /usr0/rollins/moon
1277 :     val it = 0 : int
1278 :     - cd "..";
1279 :     /usr0/rollins
1280 :     val it = 0 : int
1281 :     - ll();
1282 :     total 6
1283 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1284 :     drwxr-xr-x 2 rollins 512 Aug 20 12:18 mo.mipsl
1285 :     drwxr-xr-x 2 rollins 512 Aug 20 12:24 moon
1286 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1287 :     drwxr-xr-x 2 rollins 512 Aug 20 12:17 tools
1288 :     drwxr-xr-x 2 rollins 512 Aug 20 12:23 zed
1289 :     val it = 0 : int
1290 :     - mkdir "tooth";
1291 :     val it = 0 : int
1292 :     - ll();
1293 :     total 7
1294 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1295 :     drwxr-xr-x 2 rollins 512 Aug 20 12:18 mo.mipsl
1296 :     drwxr-xr-x 2 rollins 512 Aug 20 12:24 moon
1297 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1298 :     drwxr-xr-x 2 rollins 512 Aug 20 12:17 tools
1299 :     drwxr-xr-x 2 rollins 512 Aug 20 12:25 tooth
1300 :     drwxr-xr-x 2 rollins 512 Aug 20 12:23 zed
1301 :     val it = 0 : int
1302 :     - cd "tooth";
1303 :     /usr0/rollins/tooth
1304 :     val it = 0 : int
1305 :     - cd "../src";
1306 :     /usr0/rollins/src
1307 :     val it = 0 : int
1308 :     - cd "../tooth";
1309 :     /usr0/rollins/src
1310 :    
1311 :     uncaught exception NotDirectory
1312 :     - cd "..";
1313 :     /usr0/rollins
1314 :     val it = 0 : int
1315 :     - ll();
1316 :     total 7
1317 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1318 :     drwxr-xr-x 2 rollins 512 Aug 20 12:18 mo.mipsl
1319 :     drwxr-xr-x 2 rollins 512 Aug 20 12:24 moon
1320 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1321 :     drwxr-xr-x 2 rollins 512 Aug 20 12:17 tools
1322 :     drwxr-xr-x 2 rollins 512 Aug 20 12:25 tooth
1323 :     drwxr-xr-x 2 rollins 512 Aug 20 12:23 zed
1324 :     val it = 0 : int
1325 :     - cd "mzz";
1326 :     /usr0/rollins
1327 :    
1328 :     uncaught exception NotDirectory
1329 :     - mkdir "mzz";
1330 :     val it = 0 : int
1331 :     - cd "mzz";
1332 :     /usr0/rollins/mzz
1333 :     val it = 0 : int
1334 :     - cd "../src";
1335 :     /usr0/rollins/src
1336 :     val it = 0 : int
1337 :     - cd "../mzz";
1338 :     /usr0/rollins/mzz
1339 :     val it = 0 : int
1340 :     - mkdir "me";
1341 :     val it = 0 : int
1342 :     - ll();
1343 :     total 1
1344 :     drwxr-xr-x 2 rollins 512 Aug 20 12:26 me
1345 :     val it = 0 : int
1346 :     - pwd();
1347 :     /usr0/rollins/mzz
1348 :     val it = 0 : int
1349 :     - cd "..";
1350 :     /usr0/rollins
1351 :     val it = 0 : int
1352 :     - mkdir "me";
1353 :     val it = 0 : int
1354 :     - ll();
1355 :     total 9
1356 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1357 :     drwxr-xr-x 2 rollins 512 Aug 20 12:26 me
1358 :     drwxr-xr-x 2 rollins 512 Aug 20 12:18 mo.mipsl
1359 :     drwxr-xr-x 2 rollins 512 Aug 20 12:24 moon
1360 :     drwxr-xr-x 3 rollins 512 Aug 20 12:26 mzz
1361 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1362 :     drwxr-xr-x 2 rollins 512 Aug 20 12:17 tools
1363 :     drwxr-xr-x 2 rollins 512 Aug 20 12:25 tooth
1364 :     drwxr-xr-x 2 rollins 512 Aug 20 12:23 zed
1365 :     val it = 0 : int
1366 :     - cd "me";
1367 :     /usr0/rollins/me
1368 :     val it = 0 : int
1369 :     - cd "../tooth";
1370 :     /usr0/rollins/me
1371 :    
1372 :     uncaught exception NotDirectory
1373 :     - cd "..";
1374 :     /usr0/rollins
1375 :     val it = 0 : int
1376 :     - mkdir "teeth";
1377 :     val it = 0 : int
1378 :     - cd "teeth";
1379 :     /usr0/rollins/teeth
1380 :     val it = 0 : int
1381 :     - cd "../src";
1382 :     /usr0/rollins/src
1383 :     val it = 0 : int
1384 :     - cd "../teeth";
1385 :     /usr0/rollins/src
1386 :    
1387 :     uncaught exception NotDirectory
1388 :     - cd "..";
1389 :     /usr0/rollins
1390 :     val it = 0 : int
1391 :     - ll();
1392 :     total 10
1393 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1394 :     drwxr-xr-x 2 rollins 512 Aug 20 12:26 me
1395 :     drwxr-xr-x 2 rollins 512 Aug 20 12:18 mo.mipsl
1396 :     drwxr-xr-x 2 rollins 512 Aug 20 12:24 moon
1397 :     drwxr-xr-x 3 rollins 512 Aug 20 12:26 mzz
1398 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1399 :     drwxr-xr-x 2 rollins 512 Aug 20 12:27 teeth
1400 :     drwxr-xr-x 2 rollins 512 Aug 20 12:17 tools
1401 :     drwxr-xr-x 2 rollins 512 Aug 20 12:25 tooth
1402 :     drwxr-xr-x 2 rollins 512 Aug 20 12:23 zed
1403 :     val it = 0 : int
1404 :     - mkdir "tzz";
1405 :     val it = 0 : int
1406 :     - ll();
1407 :     total 11
1408 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1409 :     drwxr-xr-x 2 rollins 512 Aug 20 12:26 me
1410 :     drwxr-xr-x 2 rollins 512 Aug 20 12:18 mo.mipsl
1411 :     drwxr-xr-x 2 rollins 512 Aug 20 12:24 moon
1412 :     drwxr-xr-x 3 rollins 512 Aug 20 12:26 mzz
1413 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1414 :     drwxr-xr-x 2 rollins 512 Aug 20 12:27 teeth
1415 :     drwxr-xr-x 2 rollins 512 Aug 20 12:17 tools
1416 :     drwxr-xr-x 2 rollins 512 Aug 20 12:25 tooth
1417 :     drwxr-xr-x 2 rollins 512 Aug 20 12:27 tzz
1418 :     drwxr-xr-x 2 rollins 512 Aug 20 12:23 zed
1419 :     val it = 0 : int
1420 :     - cd "tzz";
1421 :     /usr0/rollins/tzz
1422 :     val it = 0 : int
1423 :     - cd "../src";
1424 :     /usr0/rollins/src
1425 :     val it = 0 : int
1426 :     - cd "../tzz";
1427 :     /usr0/rollins/tzz
1428 :     val it = 0 : int
1429 :     - cd "../teeth";
1430 :     /usr0/rollins/tzz
1431 :    
1432 :     uncaught exception NotDirectory
1433 :     - cd "..";
1434 :     /usr0/rollins
1435 :     val it = 0 : int
1436 :     - ll();
1437 :     total 11
1438 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 bin
1439 :     drwxr-xr-x 2 rollins 512 Aug 20 12:26 me
1440 :     drwxr-xr-x 2 rollins 512 Aug 20 12:18 mo.mipsl
1441 :     drwxr-xr-x 2 rollins 512 Aug 20 12:24 moon
1442 :     drwxr-xr-x 3 rollins 512 Aug 20 12:26 mzz
1443 :     drwxr-xr-x 2 rollins 512 Aug 20 12:16 src
1444 :     drwxr-xr-x 2 rollins 512 Aug 20 12:27 teeth
1445 :     drwxr-xr-x 2 rollins 512 Aug 20 12:17 tools
1446 :     drwxr-xr-x 2 rollins 512 Aug 20 12:25 tooth
1447 :     drwxr-xr-x 2 rollins 512 Aug 20 12:27 tzz
1448 :     drwxr-xr-x 2 rollins 512 Aug 20 12:23 zed
1449 :     val it = 0 : int
1450 :     -
1451 :     Comment: (Lal George)
1452 :     There is an operating system level 3 call that can be used to
1453 :     get the working directory.
1454 :     Unfortunately, we cannot use this because it does a malloc.
1455 :     So we have to build up the working directory pathname by
1456 :     interpreting inodes.
1457 :     It is my guess that this is what bombs out in the Andrew file
1458 :     system.
1459 :     ** This is probably another example of bug #651 (JHR, 10/6/92) **
1460 :     Status: fixed in 0.75
1461 :     ---------------------------------------------------------------------------
1462 :     Number: 422
1463 :     Title: overflow on int to real conversion
1464 :     Keywords:
1465 :     Submitter: Andrzej Filinski <andrzej@cs.cmu.edu>
1466 :     Date: 9/20/91
1467 :     Version: 0.73
1468 :     System: all
1469 :     Severity: major
1470 :     Problem: int->real conversion overflows on MININT
1471 :     Transcript: Standard ML of New Jersey, Version 0.73, 10 September 1991
1472 :     Arrays have changed; see doc/NEWS
1473 :     val it = () : unit
1474 :     - ~0x40000000;
1475 :     val it = ~1073741824 : int
1476 :     - real it;
1477 :    
1478 :     uncaught exception Overflow
1479 :     -
1480 :     Fix: In boot/perv.sml, move redundant check for MININT
1481 :     from Integer.mod to Real.real :-).
1482 :    
1483 :     Status: fixed in 0.74
1484 :     ---------------------------------------------------------------------------
1485 :     Number: 423
1486 :     Title: printing of structure signatures
1487 :     Keywords:
1488 :     Submitter: John Reppy
1489 :     Date: 10/1/91
1490 :     Version: 0.73
1491 :     Severity: minor
1492 :     Problem:
1493 :     At top level, some structure signatures are printed as identifiers,
1494 :     while others are printed in full.
1495 :     Transcript:
1496 :     Standard ML of New Jersey, Version 0.73, 10 September 1991
1497 :     Arrays have changed; see doc/NEWS
1498 :     val it = () : unit
1499 :     - structure I = IO;
1500 :     structure I : IO
1501 :     - structure V = Vector;
1502 :     structure V :
1503 :     sig
1504 :     eqtype 'a vector
1505 :     exception Size
1506 :     exception Subscript
1507 :     val length : 'a vector -> int
1508 :     val sub : 'a vector * int -> 'a
1509 :     val tabulate : int * (int -> 'a) -> 'a vector
1510 :     val vector : 'a list -> 'a vector
1511 :     val vector_n : int * 'a list -> 'a vector
1512 :     end
1513 :     -
1514 :     Comments: [Dave Tarditi]
1515 :     The reported behavior is intentional: the basic idea is that if we know
1516 :     the name of a structure's signature, we print the name of the signature
1517 :     instead of the whole signature.
1518 :    
1519 :     More formally, if S is structure which is bound to structure id SX,
1520 :     and S was the result of doing a signature match against signature T,
1521 :     which itself is bound to signature identifier TX, then when we print
1522 :     the signature for the structure bound to SX, we will print TX, provided
1523 :     that TX is still bound to the same signature.
1524 :    
1525 :     Thus we get the following results at the top-level:
1526 :    
1527 :     - structure S = IO;
1528 :     structure S : IO
1529 :     - structure T = S;
1530 :     structure T : IO
1531 :    
1532 :     but when we re-bind the signature identifier IO we get:
1533 :    
1534 :     - signature IO = sig end;
1535 :     signature IO =
1536 :     sig
1537 :     end
1538 :     - structure S = IO
1539 :     structure S =
1540 :     sig
1541 :     type instream
1542 :     ...
1543 :     end
1544 :    
1545 :     The problem is that the signature identifier VECTOR is not in
1546 :     the top-level environment. To fix this, change
1547 :     build/process.sml, lines 202-204 from:
1548 :    
1549 :     map Symbol.sigSymbol ["REF","LIST","ARRAY","BYTEARRAY","IO","BOOL",
1550 :     "ENVIRON", "COMPILE",
1551 :     "STRING","INTEGER","REAL","GENERAL"]
1552 :     to:
1553 :     map Symbol.sigSymbol ["REF","LIST","ARRAY","BYTEARRAY","IO","BOOL",
1554 :     "ENVIRON", "COMPILE"
1555 :     "STRING","INTEGER","REAL","GENERAL",
1556 :     "VECTOR"]
1557 :    
1558 :     Maybe we should add a flag to toggle this behavior, but I was hoping
1559 :     that we would an environment browsing structure to the compiler
1560 :     instead. It's a kludge to have to type "structure S = S" to see the
1561 :     signature of S.
1562 :    
1563 :     Status: not a bug (but a feature!)
1564 :     ---------------------------------------------------------------------------
1565 :     Number: 424
1566 :     Title: IO.execute on SPARC
1567 :     Keywords:
1568 :     Submitter: Emden Gansner
1569 :     Date: 10/1/91
1570 :     Version: 0.73
1571 :     System: SPARC, SunOS 4.1
1572 :     Severity: moderate
1573 :     Problem:
1574 :     "I just noticed that, starting with 0.71, the IO.execute function
1575 :     causes problems on the sparc, running SunOS4.1. This problem
1576 :     doesn't occur on 0.73 running on hunny."
1577 :     Transcript:
1578 :     t) /usr/addon/sml/bin/*69*
1579 :     Standard ML of New Jersey, Version 0.69, 3 April 1991
1580 :     val it = () : unit
1581 :     - IO.execute "/bin/date";
1582 :     val it = (-,-) : instream * outstream
1583 :     - t)
1584 :     t) sml
1585 :     Standard ML of New Jersey, Version 0.71, 23 July 1991
1586 :     val it = () : unit
1587 :     - IO.execute "/bin/date";
1588 :     /home/erg/bin/sml[7]: 6446 Bus error
1589 :     t) sml73
1590 :     Standard ML of New Jersey, Version 0.73, 10 September 1991
1591 :     val it = () : unit
1592 :     - IO.execute "/bin/date";
1593 :     Bus error
1594 :     t)
1595 :     Status: fixed in 0.74 (JHR)
1596 :     ---------------------------------------------------------------------------
1597 :     Number: 425
1598 :     Title: profiler flakiness
1599 :     Keywords:
1600 :     Submitter: Frank Pfenning
1601 :     Date: 10/2/91
1602 :     Version: 0.73
1603 :     Problem:
1604 :     I am currently in the process of eliminating obvious inefficiencies in an ML
1605 :     implementation of a logic programming language. While using the profiler, I
1606 :     noticed that it seemed to lead to inordinately large core images during the
1607 :     development (there is also a small overhead for the mere fact that we are
1608 :     profiling, but that is acceptable). My guess is the profiler keeps a
1609 :     (non-weak) pointer to code somehow, which prevents it from being garbage
1610 :     collected even if it is no longer accessible from the top-level. The fact
1611 :     that redefined functions show up twice or more often in the profiling
1612 :     statistics seem to confirm that, but I may be using it wrong, or there could
1613 :     be other reasons. I would be interested to hear what the
1614 :     developer/implementor of the profiler has to say about this. Thanks,
1615 :     Comment: (Andrew Appel)
1616 :     Yes, I think your analysis is correct.
1617 :     There's a profiler function that resets the profiler; perhaps that's
1618 :     what you want. But if you use it, you'd have to reload your entire
1619 :     source code.
1620 :     Status: fixed in 0.86
1621 :     ---------------------------------------------------------------------------
1622 :     Number: 426
1623 :     Title: type printing
1624 :     Keywords:
1625 :     Submitter: Andy Koenig (europa!ark)
1626 :     Date: 10/4/91
1627 :     Version: 0.73
1628 :     Severity: minor
1629 :     Problem:
1630 :     Spurious parenthesis around unit.
1631 :     Transcript:
1632 :     - (3,());
1633 :     val it = (3,()) : int * (unit)
1634 :     Status: fixed in 0.74
1635 :     ---------------------------------------------------------------------------
1636 :     Number: 427
1637 :     Title: Compiler bug: defineEqTycon/eqtyc
1638 :     Keywords:
1639 :     Submitter: John Reppy
1640 :     Date: 10/6/91
1641 :     Version: 0.73
1642 :     Severity: ?
1643 :     Problem:
1644 :     Compiler bug: defineEqTycon/eqtyc -- bad tycon
1645 :     Transcript:
1646 :     Standard ML of New Jersey, Version 0.73, 10 September 1991
1647 :     Arrays have changed; see doc/NEWS
1648 :     val it = () : unit
1649 :     - datatype 'a array = ARRAY of 'a ref VECTOR;
1650 :     std_in:2.38-2.43 Error: unbound type constructor VECTOR
1651 :     Error: Compiler bug: defineEqTycon/eqtyc -- bad tycon
1652 :     Comments:
1653 :     Obviously this code is incorrect, but I have a bigger example that
1654 :     only prints out the "bad tycon" message.
1655 :     Status: fixed in 0.74
1656 :     ---------------------------------------------------------------------------
1657 :     Number: 428
1658 :     Title: openStructureVar -- bad access value
1659 :     Keywords:
1660 :     Submitter: Benjamin.Pierce@cs.cmu.edu
1661 :     Date: 4/3/91
1662 :     Version: 0.67 (with SourceGroup)
1663 :     System: SunOS 4.1
1664 :     Severity: Major
1665 :     Problem: Compiler bug: EnvAccess.openStructureVar -- bad access value
1666 :     Code: see below
1667 :     Transcript:
1668 :    
1669 :     Standard ML of New Jersey, Version 0.67, 21 November 1990
1670 :     (Built on Sun Mar 17 11:37:30 EST 1991 with GnuTags and SourceGroup)
1671 :     val it = () : unit
1672 :     - use "bad.tmp";
1673 :     [opening bad.tmp]
1674 :     signature WR =
1675 :     sig
1676 :     type Wr
1677 :     val close : Wr -> unit
1678 :     val extract_str : Wr -> string
1679 :     val to_file : string -> Wr
1680 :     val to_fn : (string -> unit) -> (unit -> unit) -> Wr
1681 :     val to_nowhere : unit -> Wr
1682 :     val to_stdout : unit -> Wr
1683 :     val to_string : unit -> Wr
1684 :     val to_wrs : Wr list -> Wr
1685 :     val write_wr : Wr -> string -> unit
1686 :     end
1687 :     signature PP =
1688 :     sig
1689 :     structure Wr : sig...end
1690 :     type Pp
1691 :     val DEBUG : bool ref
1692 :     val break : Pp -> bool -> int -> unit
1693 :     val endb : Pp -> unit
1694 :     val expbreak : Pp -> bool -> string -> unit
1695 :     val pp_from_wr : Wr.Wr -> Pp
1696 :     val pwrite : Pp -> string -> unit
1697 :     val set_margin : Pp -> int -> unit
1698 :     val setb : Pp -> unit
1699 :     val wr_from_pp : Pp -> Wr.Wr
1700 :     end
1701 :     signature WRMGT =
1702 :     sig
1703 :     structure Pp : sig...end
1704 :     structure Wr : sig...end
1705 :     val get_current_wr : unit -> Wr.Wr
1706 :     val set_current_wr : Wr.Wr -> unit
1707 :     val stdpp : unit -> Pp.Pp
1708 :     val write : string -> unit
1709 :     end
1710 :     signature STRINGUTILS =
1711 :     sig
1712 :     end
1713 :     signature REGISTRY =
1714 :     sig
1715 :     type registeredtype
1716 :     val register : string -> (registeredtype -> unit) -> unit
1717 :     val registerflag : string -> registeredtype ref -> unit
1718 :     val set_all : registeredtype -> unit
1719 :     val set_flag : string -> registeredtype -> unit
1720 :     end
1721 :     signature LISTUTILS =
1722 :     sig
1723 :     val filter : ('a -> bool) -> 'a list -> 'a list
1724 :     val forall : ('a -> bool) -> 'a list -> bool
1725 :     val forsome : ('a -> bool) -> 'a list -> bool
1726 :     val mapappend : ('a -> 'b list) -> 'a list -> 'b list
1727 :     val mapfold : ('a -> 'b) -> ('b -> 'b -> 'b) -> 'b -> 'a list -> 'b
1728 :     val mapunit : ('b -> 'a) -> 'b list -> unit
1729 :     val mapunit_tuple : ('a -> unit) -> (unit -> unit) -> 'a list -> unit
1730 :     val memq : ('a -> 'a -> bool) -> 'a list -> 'a -> bool
1731 :     end
1732 :     signature ID =
1733 :     sig
1734 :     type T
1735 :     val == : T -> T -> bool
1736 :     val hashcode : T -> int
1737 :     val intern : string -> T
1738 :     val new : unit -> T
1739 :     val new_from : T -> T
1740 :     val tostr : T -> string
1741 :     end
1742 :     signature DEBUGUTILS =
1743 :     sig
1744 :     val wrap : bool ref -> string -> (unit -> 'a) -> (unit -> unit) -> ('a -> unit) -> 'a
1745 :     end
1746 :     signature GLOBALS =
1747 :     sig
1748 :     structure Id : sig...end
1749 :     structure Pp : sig...end
1750 :     structure Pp : sig...end
1751 :     structure Wr : sig...end
1752 :     structure Wr : sig...end
1753 :     structure WrMgt : sig...end
1754 :     type registeredtype
1755 :     val filter : ('a -> bool) -> 'a list -> 'a list
1756 :     val forall : ('a -> bool) -> 'a list -> bool
1757 :     val forsome : ('a -> bool) -> 'a list -> bool
1758 :     val get_current_wr : unit -> Wr.Wr
1759 :     val mapappend : ('a -> 'b list) -> 'a list -> 'b list
1760 :     val mapfold : ('a -> 'b) -> ('b -> 'b -> 'b) -> 'b -> 'a list -> 'b
1761 :     val mapunit : ('b -> 'a) -> 'b list -> unit
1762 :     val mapunit_tuple : ('a -> unit) -> (unit -> unit) -> 'a list -> unit
1763 :     val memq : ('a -> 'a -> bool) -> 'a list -> 'a -> bool
1764 :     val register : string -> (registeredtype -> unit) -> unit
1765 :     val registerflag : string -> registeredtype ref -> unit
1766 :     val set_all : registeredtype -> unit
1767 :     val set_current_wr : Wr.Wr -> unit
1768 :     val set_flag : string -> registeredtype -> unit
1769 :     val stdpp : unit -> Pp.Pp
1770 :     val wrap : bool ref -> string -> (unit -> 'a) -> (unit -> unit) -> ('a -> unit) -> 'a
1771 :     val write : string -> unit
1772 :     end
1773 :     Error: Compiler bug: EnvAccess.openStructureVar -- bad access value
1774 :     [closing bad.tmp]
1775 :     -
1776 :    
1777 :    
1778 :     --------------------------------------------------------------------------
1779 :     (* And here's the offending file ... *)
1780 :    
1781 :     signature WR = sig
1782 :    
1783 :     type Wr
1784 :    
1785 :     val to_stdout: unit -> Wr
1786 :     val to_file: string -> Wr
1787 :     val to_nowhere: unit -> Wr
1788 :     val to_wrs: Wr list -> Wr
1789 :     val to_fn: (string->unit) -> (unit->unit) -> Wr
1790 :     val to_string: unit -> Wr
1791 :     val extract_str: Wr -> string
1792 :    
1793 :     val close: Wr -> unit
1794 :    
1795 :     val write_wr: Wr -> string -> unit
1796 :    
1797 :     end;
1798 :     signature PP = sig
1799 :    
1800 :     structure Wr: WR
1801 :    
1802 :     type Pp
1803 :    
1804 :     val pp_from_wr: Wr.Wr -> Pp
1805 :     val wr_from_pp: Pp -> Wr.Wr;
1806 :    
1807 :     val pwrite : Pp -> string -> unit
1808 :     val setb: Pp -> unit
1809 :     val endb: Pp -> unit
1810 :     val break: Pp -> bool -> int -> unit
1811 :     val expbreak: Pp -> bool -> string -> unit
1812 :     val set_margin: Pp -> int -> unit
1813 :    
1814 :     val DEBUG: bool ref
1815 :    
1816 :     end;
1817 :    
1818 :     signature WRMGT = sig
1819 :    
1820 :     (* Maintains a notion of a current (prettyprinting) writer
1821 :     and its associated prettyprinter *)
1822 :    
1823 :     structure Wr: WR;
1824 :     structure Pp: PP;
1825 :     sharing Pp.Wr = Wr;
1826 :    
1827 :     val set_current_wr: Wr.Wr -> unit;
1828 :     val get_current_wr: unit -> Wr.Wr;
1829 :     val stdpp: unit -> Pp.Pp;
1830 :    
1831 :     val write: string -> unit;
1832 :    
1833 :     end;
1834 :    
1835 :     signature STRINGUTILS = sig
1836 :    
1837 :     end;
1838 :    
1839 :     signature REGISTRY = sig
1840 :    
1841 :     type registeredtype
1842 :    
1843 :     val register: string -> (registeredtype->unit) -> unit
1844 :     val registerflag: string -> (registeredtype ref) -> unit
1845 :    
1846 :     val set_flag: string -> registeredtype -> unit
1847 :     val set_all: registeredtype -> unit
1848 :    
1849 :     end;
1850 :    
1851 :     signature LISTUTILS = sig
1852 :    
1853 :     val memq: ('a -> 'a -> bool) -> 'a list -> 'a -> bool
1854 :    
1855 :     val mapappend: ('a -> 'b list) -> ('a list) -> ('b list)
1856 :     val mapunit: ('a -> 'b) -> ('a list) -> unit
1857 :     val mapunit_tuple: ('a -> unit) -> (unit -> unit) -> ('a list) -> unit
1858 :    
1859 :     val mapfold: ('a -> 'b) -> ('b -> 'b -> 'b) -> 'b -> ('a list) -> 'b
1860 :     val forall: ('a -> bool) -> ('a list) -> bool
1861 :     val forsome: ('a -> bool) -> ('a list) -> bool
1862 :    
1863 :     val filter: ('a -> bool) -> ('a list) -> ('a list)
1864 :    
1865 :     end;
1866 :    
1867 :     signature ID = sig
1868 :    
1869 :     type T
1870 :    
1871 :     val intern: string -> T
1872 :     val tostr: T -> string
1873 :    
1874 :     val hashcode: T -> int
1875 :     val new: unit -> T
1876 :     val new_from: T -> T
1877 :    
1878 :     val == : T -> T -> bool
1879 :    
1880 :     end;
1881 :    
1882 :    
1883 :     (* May eventually want to support these too:
1884 :    
1885 :     val lexlt : T -> T -> bool
1886 :     *)
1887 :    
1888 :     signature DEBUGUTILS = sig
1889 :    
1890 :     val wrap: (bool ref) -> string -> (unit -> 'a) -> (unit -> unit) -> ('a -> unit) -> 'a
1891 :    
1892 :     end;
1893 :    
1894 :     signature GLOBALS = sig
1895 :    
1896 :     structure Wr: WR
1897 :     structure Pp: PP
1898 :     structure WrMgt: WRMGT
1899 :     structure Id: ID
1900 :    
1901 :     sharing Pp.Wr = Wr
1902 :     sharing WrMgt.Pp = Pp
1903 :    
1904 :     include WRMGT
1905 :    
1906 :     include LISTUTILS
1907 :     include STRINGUTILS
1908 :     include DEBUGUTILS
1909 :     include REGISTRY
1910 :    
1911 :     sharing type registeredtype = bool
1912 :    
1913 :     end;
1914 :    
1915 :     signature TYPPVT = sig
1916 :    
1917 :     structure Globals: GLOBALS
1918 :     open Globals
1919 :    
1920 :     datatype pretyp =
1921 :     PRETVAR of Id.T
1922 :     | PREARROW of pretyp * pretyp
1923 :     | PREALL of Id.T * pretyp * pretyp
1924 :     | PREMEET of pretyp list
1925 :    
1926 :     datatype T =
1927 :     TVAR of unit * int
1928 :     | ARROW of unit * T * T
1929 :     | ALL of {name:Id.T} * T * T
1930 :     | MEET of unit * (T list)
1931 :    
1932 :     datatype tenvelt = BND of Id.T * T
1933 :     | ABB of Id.T * T
1934 :     | VBND of Id.T * T
1935 :    
1936 :     datatype tenv = TENV of tenvelt list
1937 :    
1938 :     val empty_tenv: tenv
1939 :     val extend_bound: tenv -> Id.T -> T -> tenv
1940 :     val push_bound: tenv -> Id.T -> T -> tenv
1941 :     val extend_abbrev: tenv -> Id.T -> T -> tenv
1942 :     val push_abbrev: tenv -> Id.T -> T -> tenv
1943 :     val extend_binding: tenv -> Id.T -> T -> tenv
1944 :     val push_binding: tenv -> Id.T -> T -> tenv
1945 :     val pop: tenv -> tenv
1946 :    
1947 :     val index: tenv -> Id.T -> int
1948 :     val lookup_name: tenv -> int -> Id.T
1949 :     val lookup_and_relocate_bound: tenv -> int -> T
1950 :     val lookup_and_relocate_binding: tenv -> int -> T
1951 :     val lookup_and_relocate: tenv -> int -> tenvelt
1952 :     val lookup: tenv -> int -> tenvelt
1953 :     val relocate: int -> T -> T
1954 :    
1955 :     exception UnknownId of string
1956 :     exception WrongKindOfId of tenv * int * string
1957 :     val debruijnify: tenv -> pretyp -> T
1958 :    
1959 :     val prt: Pp.Pp -> tenv -> T -> unit
1960 :     val prt_tenv: Pp.Pp -> tenv -> unit
1961 :    
1962 :     val NS: T
1963 :    
1964 :     end;
1965 :     Status: fixed in 0.71
1966 :     ---------------------------------------------------------------------------
1967 :     Number: 429
1968 :     Title: signature match fails
1969 :     Keywords:
1970 :     Submitter: Benjamin Pierce <Benjamin.Pierce@PROOF.ERGO.CS.CMU.EDU>
1971 :     Date: 4/4/91
1972 :     Version: 0.69
1973 :     Problem: signature spec not matched when it should be
1974 :     Transcript:
1975 :     Standard ML of New Jersey, Version 0.69, 3 April 1991
1976 :     val it = () : unit
1977 :     - use "bug.tmp";
1978 :     use "bug.tmp";
1979 :     [opening bug.tmp]
1980 :    
1981 :     [Major collection...
1982 :     [Increasing heap to 10011k]
1983 :     96% used (3502604/3627780), 7260 msec]
1984 :    
1985 :     [Increasing heap to 10431k]
1986 :     bug.tmp:1545.8-1775.3 Error: value type in structure doesn't match signature spec
1987 :     name: prt
1988 :     spec: Pp -> tenv -> T -> unit
1989 :     actual: ?.Pp -> tenv -> T -> unit
1990 :     bug.tmp:1545.8-1775.3 Error: value type in structure doesn't match signature spec
1991 :     name: prt_tenv
1992 :     spec: Pp -> tenv -> unit
1993 :     actual: ?.Pp -> tenv -> unit
1994 :     bug.tmp:1798.7-1802.44 Error: operator and operand don't agree (tycon mismatch)
1995 :     operator domain: ?.Pp
1996 :     operand: ?.Pp
1997 :     in expression:
1998 :     Typ.prt pp
1999 :     bug.tmp:1798.7-1820.56 Error: rules don't agree (tycon mismatch)
2000 :     expected: ?.Pp * 'Z * 'Y list * 'X * rhs_flag -> unit
2001 :     found: ?.Pp * tenv * lhsqueue list * 'W * 'V -> 'U
2002 :     rule:
2003 :     (pp,te,:: (ARROW_LHS <pat>,nil),t2,flag) => (<exp> <exp> te t1;# # t2 flag)
2004 :     bug.tmp:1807.7-1809.38 Error: operator and operand don't agree (tycon mismatch)
2005 :     operator domain: ?.Pp
2006 :     operand: ?.Pp
2007 :     in expression:
2008 :     Pp.pwrite pp
2009 :     bug.tmp:1798.7-1820.56 Error: rules don't agree (tycon mismatch)
2010 :     expected: ?.Pp * 'Z * 'Y list * 'X * rhs_flag -> unit
2011 :     found: ?.Pp * tenv * lhsqueue list * 'W * 'V -> 'U
2012 :     rule:
2013 :     (pp,te,:: (ARROW_LHS <pat>,X2),t2,flag) => (<exp> <exp> te t1;Pp.pwrite pp ",";# # t2 flag)
2014 :     bug.tmp:1811.7-1814.56 Error: operator and operand don't agree (tycon mismatch)
2015 :     operator domain: ?.Pp
2016 :     operand: ?.Pp
2017 :     in expression:
2018 :     Typ.prt pp
2019 :     bug.tmp:1811.7-1814.56 Error: operator and operand don't agree (tycon mismatch)
2020 :     operator domain: ?.Pp
2021 :     operand: ?.Pp
2022 :     in expression:
2023 :     describe_rest pp
2024 :     bug.tmp:1816.7-1820.56 Error: operator and operand don't agree (tycon mismatch)
2025 :     operator domain: ?.Pp
2026 :     operand: ?.Pp
2027 :     in expression:
2028 :     Typ.prt pp
2029 :     bug.tmp:1816.7-1820.56 Error: operator and operand don't agree (tycon mismatch)
2030 :     operator domain: ?.Pp
2031 :     operand: ?.Pp
2032 :     in expression:
2033 :     describe_rest pp
2034 :     bug.tmp:1797.1-1820.56 Error: pattern and expression in val rec dec don't agree (tycon mismatch)
2035 :     pattern: ?.Pp -> tenv -> lhsqueue list -> 'Z -> 'Y -> 'X
2036 :     expression: ?.Pp -> tenv -> lhsqueue list -> 'W -> rhs_flag -> unit
2037 :     in declaration:
2038 :     describe_rest = (fn arg => (fn <pat> => <exp>))
2039 :     bug.tmp:1823.3-1829.14 Error: operator and operand don't agree (tycon mismatch)
2040 :     operator domain: ?.Pp
2041 :     operand: ?.Pp
2042 :     in expression:
2043 :     Typ.prt pp
2044 :     bug.tmp:1823.3-1829.14 Error: operator and operand don't agree (tycon mismatch)
2045 :     operator domain: ?.Pp
2046 :     operand: ?.Pp
2047 :     in expression:
2048 :     describe_rest pp
2049 :     bug.tmp:1874.15-1874.54 Error: operator and operand don't agree (tycon mismatch)
2050 :     operator domain: ?.Pp
2051 :     operand: ?.Pp
2052 :     in expression:
2053 :     describe_problem (stdpp ())
2054 :     [closing bug.tmp]
2055 :    
2056 :    
2057 :     --------------------------------------------------------------------------
2058 :     (* and here's the offending file... Sorry it's a bit long *)
2059 :    
2060 :     signature WR = sig
2061 :    
2062 :     type Wr
2063 :    
2064 :     val to_stdout: unit -> Wr
2065 :     val to_file: string -> Wr
2066 :     val to_nowhere: unit -> Wr
2067 :     val to_wrs: Wr list -> Wr
2068 :     val to_fn: (string->unit) -> (unit->unit) -> Wr
2069 :     val to_string: unit -> Wr
2070 :     val extract_str: Wr -> string
2071 :    
2072 :     val close: Wr -> unit
2073 :    
2074 :     val write_wr: Wr -> string -> unit
2075 :    
2076 :     end
2077 :     signature PP = sig
2078 :    
2079 :     structure Wr: WR
2080 :    
2081 :     type Pp
2082 :    
2083 :     val pp_from_wr: Wr.Wr -> Pp
2084 :     val wr_from_pp: Pp -> Wr.Wr;
2085 :    
2086 :     val pwrite : Pp -> string -> unit
2087 :     val setb: Pp -> unit
2088 :     val endb: Pp -> unit
2089 :     val break: Pp -> bool -> int -> unit
2090 :     val expbreak: Pp -> bool -> string -> unit
2091 :     val set_margin: Pp -> int -> unit
2092 :    
2093 :     val DEBUG: bool ref
2094 :    
2095 :     end
2096 :     signature WRMGT = sig
2097 :    
2098 :     (* Maintains a notion of a current (prettyprinting) writer
2099 :     and its associated prettyprinter *)
2100 :    
2101 :     structure Wr: WR;
2102 :     structure Pp: PP;
2103 :     sharing Pp.Wr = Wr;
2104 :    
2105 :     val set_current_wr: Wr.Wr -> unit;
2106 :     val get_current_wr: unit -> Wr.Wr;
2107 :     val stdpp: unit -> Pp.Pp;
2108 :    
2109 :     val write: string -> unit;
2110 :    
2111 :     end
2112 :     signature STRINGUTILS = sig
2113 :    
2114 :     end
2115 :     signature REGISTRY = sig
2116 :    
2117 :     type registeredtype
2118 :    
2119 :     val register: string -> (registeredtype->unit) -> unit
2120 :     val registerflag: string -> (registeredtype ref) -> unit
2121 :    
2122 :     val set_flag: string -> registeredtype -> unit
2123 :     val set_all: registeredtype -> unit
2124 :    
2125 :     end
2126 :     signature LISTUTILS = sig
2127 :    
2128 :     val memq: ('a -> 'a -> bool) -> 'a list -> 'a -> bool
2129 :    
2130 :     val mapappend: ('a -> 'b list) -> ('a list) -> ('b list)
2131 :     val mapunit: ('a -> 'b) -> ('a list) -> unit
2132 :     val mapunit_tuple: ('a -> unit) -> (unit -> unit) -> ('a list) -> unit
2133 :    
2134 :     val mapfold: ('a -> 'b) -> ('b -> 'b -> 'b) -> 'b -> ('a list) -> 'b
2135 :     val forall: ('a -> bool) -> ('a list) -> bool
2136 :     val forsome: ('a -> bool) -> ('a list) -> bool
2137 :    
2138 :     val filter: ('a -> bool) -> ('a list) -> ('a list)
2139 :    
2140 :     end
2141 :     signature ID = sig
2142 :    
2143 :     type T
2144 :    
2145 :     val intern: string -> T
2146 :     val tostr: T -> string
2147 :    
2148 :     val hashcode: T -> int
2149 :     val new: unit -> T
2150 :     val new_from: T -> T
2151 :    
2152 :     val == : T -> T -> bool
2153 :    
2154 :     end
2155 :    
2156 :     (* May eventually want to support these too:
2157 :    
2158 :     val lexlt : T -> T -> bool
2159 :     *)
2160 :    
2161 :     signature DEBUGUTILS = sig
2162 :    
2163 :     val wrap: (bool ref) -> string -> (unit -> 'a) -> (unit -> unit) -> ('a -> unit) -> 'a
2164 :    
2165 :     end
2166 :     signature GLOBALS = sig
2167 :    
2168 :     structure Wr: WR
2169 :     structure Pp: PP
2170 :     structure WrMgt: WRMGT
2171 :     structure Id: ID
2172 :    
2173 :     sharing Pp.Wr = Wr
2174 :     sharing WrMgt.Pp = Pp
2175 :    
2176 :     include WRMGT
2177 :    
2178 :     include LISTUTILS
2179 :     include STRINGUTILS
2180 :     include DEBUGUTILS
2181 :     include REGISTRY
2182 :    
2183 :     sharing type registeredtype = bool
2184 :    
2185 :     exception CantHappen
2186 :    
2187 :     end
2188 :     signature TYPPVT = sig
2189 :    
2190 :     structure Globals: GLOBALS
2191 :     open Globals
2192 :    
2193 :     datatype pretyp =
2194 :     PRETVAR of Id.T
2195 :     | PREARROW of pretyp * pretyp
2196 :     | PREALL of Id.T * pretyp * pretyp
2197 :     | PREMEET of pretyp list
2198 :    
2199 :     datatype T =
2200 :     TVAR of unit * int
2201 :     | ARROW of unit * T * T
2202 :     | ALL of {name:Id.T} * T * T
2203 :     | MEET of unit * (T list)
2204 :    
2205 :     datatype tenvelt = BND of Id.T * T
2206 :     | ABB of Id.T * T
2207 :     | VBND of Id.T * T
2208 :    
2209 :     datatype tenv = TENV of tenvelt list
2210 :    
2211 :     val empty_tenv: tenv
2212 :     val push_bound: tenv -> Id.T -> T -> tenv
2213 :     val push_abbrev: tenv -> Id.T -> T -> tenv
2214 :     val push_binding: tenv -> Id.T -> T -> tenv
2215 :     val pop: tenv -> tenv
2216 :    
2217 :     val index: tenv -> Id.T -> int
2218 :     val lookup_name: tenv -> int -> Id.T
2219 :     val lookup_and_relocate_bound: tenv -> int -> T
2220 :     val lookup_and_relocate_binding: tenv -> int -> T
2221 :     val lookup_and_relocate: tenv -> int -> tenvelt
2222 :     val lookup: tenv -> int -> tenvelt
2223 :     val relocate: int -> T -> T
2224 :    
2225 :     (* Substitute the first arg for instances of var #0 in the second arg *)
2226 :     val tsubst_top: T -> T -> T
2227 :    
2228 :     exception UnknownId of string
2229 :     exception WrongKindOfId of tenv * int * string
2230 :     val debruijnify: tenv -> pretyp -> T
2231 :    
2232 :     val prt: Pp.Pp -> tenv -> T -> unit
2233 :     val prt_tenv: Pp.Pp -> tenv -> unit
2234 :    
2235 :     val NS: T
2236 :    
2237 :     end
2238 :    
2239 :     signature LEQ = sig
2240 :    
2241 :     structure Typ: TYPPVT
2242 :     structure Globals: GLOBALS
2243 :     sharing Globals = Typ.Globals
2244 :    
2245 :     val leq: Typ.tenv -> Typ.T -> Typ.T -> bool
2246 :    
2247 :     end
2248 :    
2249 :     signature LR_TABLE =
2250 :     sig
2251 :     datatype state = STATE of int
2252 :     datatype term = T of int
2253 :     datatype nonterm = NT of int
2254 :     datatype action = SHIFT of state
2255 :     | REDUCE of int
2256 :     | ACCEPT
2257 :     | ERROR
2258 :     type table
2259 :    
2260 :     val numStates : table -> int
2261 :     val describeActions : table -> state ->
2262 :     ((term * action) list) * action
2263 :     val describeGoto : table -> state -> (nonterm * state) list
2264 :     val action : table -> state * term -> action
2265 :     val goto : table -> state * nonterm -> state
2266 :     val initialState : table -> state
2267 :     exception Goto of state * nonterm
2268 :    
2269 :     val mkLrTable : {actions : (((term * action) list) * action) list,
2270 :     gotos : (nonterm * state) list list,
2271 :     numStates : int,
2272 :     initialState : state} -> table
2273 :     end
2274 :    
2275 :     signature TOKEN =
2276 :     sig
2277 :     structure LrTable : LR_TABLE
2278 :     datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
2279 :     val sameToken : ('a,'b) token * ('a,'b) token -> bool
2280 :     end
2281 :    
2282 :     signature PARSER_DATA =
2283 :     sig
2284 :     (* the type of line numbers *)
2285 :    
2286 :     type pos
2287 :    
2288 :     (* the type of semantic values *)
2289 :    
2290 :     type svalue
2291 :    
2292 :     (* the type of the user-supplied argument to the parser *)
2293 :     type arg
2294 :    
2295 :     (* the intended type of the result of the parser. This value is
2296 :     produced by applying extract from the structure Actions to the
2297 :     final semantic value resultiing from a parse.
2298 :     *)
2299 :    
2300 :     type result
2301 :    
2302 :     structure LrTable : LR_TABLE
2303 :     structure Token : TOKEN
2304 :     sharing Token.LrTable = LrTable
2305 :    
2306 :     (* structure Actions contains the functions which mantain the
2307 :     semantic values stack in the parser. Void is used to provide
2308 :     a default value for the semantic stack.
2309 :     *)
2310 :    
2311 :     structure Actions :
2312 :     sig
2313 :     val actions : int * pos *
2314 :     (LrTable.state * (svalue * pos * pos)) list * arg->
2315 :     LrTable.nonterm * (svalue * pos * pos) *
2316 :     ((LrTable.state *(svalue * pos * pos)) list)
2317 :     val void : svalue
2318 :     val extract : svalue -> result
2319 :     end
2320 :    
2321 :     (* structure EC contains information used to improve error
2322 :     recovery in an error-correcting parser *)
2323 :    
2324 :     structure EC :
2325 :     sig
2326 :     val is_keyword : LrTable.term -> bool
2327 :     val noShift : LrTable.term -> bool
2328 :     val preferred_subst : LrTable.term -> LrTable.term list
2329 :     val preferred_insert : LrTable.term -> bool
2330 :     val errtermvalue : LrTable.term -> svalue
2331 :     val showTerminal : LrTable.term -> string
2332 :     val terms: LrTable.term list
2333 :     end
2334 :    
2335 :     (* table is the LR table for the parser *)
2336 :    
2337 :     val table : LrTable.table
2338 :     end
2339 :    
2340 :     signature FMEET_TOKENS =
2341 :     sig
2342 :     type ('a,'b) token
2343 :     type svalue
2344 :     val T_PACK: ('a * 'a) ->(svalue,'a) token
2345 :     val T_END: ('a * 'a) ->(svalue,'a) token
2346 :     val T_OPEN: ('a * 'a) ->(svalue,'a) token
2347 :     val T_SOME: ('a * 'a) ->(svalue,'a) token
2348 :     val T_INSTALL: ('a * 'a) ->(svalue,'a) token
2349 :     val T_OBSERVE: ('a * 'a) ->(svalue,'a) token
2350 :     val T_FOR: ('a * 'a) ->(svalue,'a) token
2351 :     val T_OF: ('a * 'a) ->(svalue,'a) token
2352 :     val T_CASE: ('a * 'a) ->(svalue,'a) token
2353 :     val T_NS: ('a * 'a) ->(svalue,'a) token
2354 :     val T_IN: ('a * 'a) ->(svalue,'a) token
2355 :     val T_ALL: ('a * 'a) ->(svalue,'a) token
2356 :     val T_WITH: ('a * 'a) ->(svalue,'a) token
2357 :     val T_CHECK: ('a * 'a) ->(svalue,'a) token
2358 :     val T_DEBUG: ('a * 'a) ->(svalue,'a) token
2359 :     val T_RESET: ('a * 'a) ->(svalue,'a) token
2360 :     val T_SET: ('a * 'a) ->(svalue,'a) token
2361 :     val T_TYPE: ('a * 'a) ->(svalue,'a) token
2362 :     val T_USE: ('a * 'a) ->(svalue,'a) token
2363 :     val T_STR_CONST: ((string) * 'a * 'a) ->(svalue,'a) token
2364 :     val T_INT_CONST: ((string) * 'a * 'a) ->(svalue,'a) token
2365 :     val T_ID: ((string) * 'a * 'a) ->(svalue,'a) token
2366 :     val T_BIGLAMBDA: ('a * 'a) ->(svalue,'a) token
2367 :     val T_LAMBDA: ('a * 'a) ->(svalue,'a) token
2368 :     val T_INTER: ('a * 'a) ->(svalue,'a) token
2369 :     val T_RCURLY: ('a * 'a) ->(svalue,'a) token
2370 :     val T_LCURLY: ('a * 'a) ->(svalue,'a) token
2371 :     val T_RANGLE: ('a * 'a) ->(svalue,'a) token
2372 :     val T_LANGLE: ('a * 'a) ->(svalue,'a) token
2373 :     val T_RBRACK: ('a * 'a) ->(svalue,'a) token
2374 :     val T_LBRACK: ('a * 'a) ->(svalue,'a) token
2375 :     val T_RPAREN: ('a * 'a) ->(svalue,'a) token
2376 :     val T_LPAREN: ('a * 'a) ->(svalue,'a) token
2377 :     val T_DARROW: ('a * 'a) ->(svalue,'a) token
2378 :     val T_ARROW: ('a * 'a) ->(svalue,'a) token
2379 :     val T_AT: ('a * 'a) ->(svalue,'a) token
2380 :     val T_DOLLAR: ('a * 'a) ->(svalue,'a) token
2381 :     val T_DOUBLEEQ: ('a * 'a) ->(svalue,'a) token
2382 :     val T_EQ: ('a * 'a) ->(svalue,'a) token
2383 :     val T_APOST: ('a * 'a) ->(svalue,'a) token
2384 :     val T_COMMA: ('a * 'a) ->(svalue,'a) token
2385 :     val T_LEQ: ('a * 'a) ->(svalue,'a) token
2386 :     val T_SEMICOLON: ('a * 'a) ->(svalue,'a) token
2387 :     val T_COLON: ('a * 'a) ->(svalue,'a) token
2388 :     val T_DOT: ('a * 'a) ->(svalue,'a) token
2389 :     val T_EOF: ('a * 'a) ->(svalue,'a) token
2390 :     end
2391 :     signature FMEET_LRVALS =
2392 :     sig
2393 :     structure Tokens : FMEET_TOKENS
2394 :     structure ParserData:PARSER_DATA
2395 :     sharing type ParserData.Token.token = Tokens.token
2396 :     sharing type ParserData.svalue = Tokens.svalue
2397 :     end
2398 :     (* Externally visible aspects of the lexer and parser *)
2399 :    
2400 :     signature INTERFACE =
2401 :     sig
2402 :    
2403 :     type pos
2404 :     val line : pos ref
2405 :     val init_line : unit -> unit
2406 :     val next_line : unit -> unit
2407 :     val error : string * pos * pos -> unit
2408 :    
2409 :     end (* signature INTERFACE *)
2410 :    
2411 :     signature TYP = sig
2412 :    
2413 :     structure Globals: GLOBALS
2414 :     open Globals
2415 :    
2416 :     datatype pretyp =
2417 :     PRETVAR of Id.T
2418 :     | PREARROW of pretyp * pretyp
2419 :     | PREALL of Id.T * pretyp * pretyp
2420 :     | PREMEET of pretyp list
2421 :    
2422 :     type T
2423 :    
2424 :     type tenv
2425 :     val empty_tenv: tenv
2426 :     val push_bound: tenv -> Id.T -> T -> tenv
2427 :     val push_abbrev: tenv -> Id.T -> T -> tenv
2428 :     val push_binding: tenv -> Id.T -> T -> tenv
2429 :     val pop: tenv -> tenv
2430 :    
2431 :     exception UnknownId of string
2432 :     exception WrongKindOfId of tenv * int * string
2433 :     val debruijnify: tenv -> pretyp -> T
2434 :    
2435 :     val prt: Pp.Pp -> tenv -> T -> unit
2436 :     val prt_tenv: Pp.Pp -> tenv -> unit
2437 :    
2438 :     val NS: T
2439 :    
2440 :     end
2441 :    
2442 :     signature TRM = sig
2443 :    
2444 :     structure Globals: GLOBALS
2445 :     structure Typ: TYP
2446 :     sharing Typ.Globals = Globals
2447 :     open Globals
2448 :    
2449 :     datatype pretrm =
2450 :     PREVAR of Id.T
2451 :     | PREABS of Id.T * Typ.pretyp * pretrm
2452 :     | PREAPP of pretrm * pretrm
2453 :     | PRETABS of Id.T * Typ.pretyp * pretrm
2454 :     | PRETAPP of pretrm * Typ.pretyp
2455 :     | PREFOR of Id.T * (Typ.pretyp list) * pretrm
2456 :    
2457 :     type T
2458 :    
2459 :     exception UnknownId of string
2460 :     val debruijnify: Typ.tenv -> pretrm -> T
2461 :    
2462 :     val prt: Pp.Pp -> Typ.tenv -> T -> unit
2463 :    
2464 :     end
2465 :    
2466 :     signature PARSERES = sig
2467 :    
2468 :     structure Typ : TYP
2469 :     structure Trm : TRM
2470 :     structure Globals: GLOBALS
2471 :     sharing Typ.Globals = Globals
2472 :     sharing Trm.Typ = Typ
2473 :    
2474 :     datatype T =
2475 :     Leq of Typ.pretyp * Typ.pretyp
2476 :     | Type_Assumption of Globals.Id.T * Typ.pretyp
2477 :     | Type_Abbrev of Globals.Id.T * Typ.pretyp
2478 :     | Term_Def of Globals.Id.T * Trm.pretrm
2479 :     | Term_Assumption of Globals.Id.T * Typ.pretyp
2480 :     | Use of string
2481 :     | Set of string * string
2482 :     | Nothing
2483 :    
2484 :     end
2485 :     signature PARSE =
2486 :     sig
2487 :    
2488 :     structure ParseRes : PARSERES
2489 :    
2490 :     val file_parse: string -> ParseRes.T;
2491 :     val stream_parse: instream -> ParseRes.T;
2492 :     val top_parse: unit -> ParseRes.T;
2493 :    
2494 :     end (* signature PARSE *)
2495 :    
2496 :     signature STREAM =
2497 :     sig type 'xa stream
2498 :     val streamify : (unit -> '_a) -> '_a stream
2499 :     val cons : '_a * '_a stream -> '_a stream
2500 :     val get : '_a stream -> '_a * '_a stream
2501 :     end
2502 :    
2503 :     signature PARSER =
2504 :     sig
2505 :     structure Token : TOKEN
2506 :     structure Stream : STREAM
2507 :     exception ParseError
2508 :    
2509 :     type pos
2510 :     type result
2511 :     type arg
2512 :     type svalue
2513 :    
2514 :     val makeLexer : (int -> string) ->
2515 :     (svalue,pos) Token.token Stream.stream
2516 :    
2517 :     val parse : int * ((svalue,pos) Token.token Stream.stream) *
2518 :     (string * pos * pos -> unit) * arg ->
2519 :     result * (svalue,pos) Token.token Stream.stream
2520 :    
2521 :     val sameToken : (svalue,pos) Token.token * (svalue,pos) Token.token ->
2522 :     bool
2523 :     end
2524 :    
2525 :     functor Parse (structure Globals : GLOBALS
2526 :     structure ParseRes : PARSERES
2527 :     structure Interface : INTERFACE
2528 :     structure Parser : PARSER
2529 :     sharing type Parser.pos = Interface.pos
2530 :     sharing type Parser.result = ParseRes.T
2531 :     sharing type Parser.arg = unit
2532 :     structure Tokens : FMEET_TOKENS
2533 :     sharing type Tokens.token = Parser.Token.token
2534 :     sharing type Tokens.svalue = Parser.svalue
2535 :     ) : PARSE =
2536 :     struct
2537 :    
2538 :     structure ParseRes = ParseRes
2539 :     open Globals
2540 :    
2541 :     val parse = fn (lookahead,reader : int -> string) =>
2542 :     let val _ = Interface.init_line()
2543 :     val empty = !Interface.line
2544 :     val dummyEOF = Tokens.T_EOF(empty,empty)
2545 :     fun invoke lexer =
2546 :     Parser.parse(lookahead,lexer,Interface.error,())
2547 :     fun loop lexer =
2548 :     let val (result,lexer) = invoke lexer
2549 :     val (nextToken,lexer) = Parser.Stream.get lexer
2550 :     in if Parser.sameToken(nextToken,dummyEOF) then result
2551 :     else loop lexer
2552 :     end
2553 :     in loop (Parser.makeLexer reader)
2554 :     end
2555 :    
2556 :     fun string_reader s =
2557 :     let val next = ref s
2558 :     in fn _ => !next before next := ""
2559 :     end
2560 :    
2561 :     val string_parse = fn s => parse (0, string_reader s)
2562 :    
2563 :     val file_parse = fn name =>
2564 :     let val dev = open_in name
2565 :     in (parse (15,(fn i => input(dev,i)))) before close_in dev
2566 :     end
2567 :    
2568 :     fun prefix line len = substring(line,0,min(len,size line))
2569 :    
2570 :     fun echo_line line =
2571 :     if (line = "\n") orelse (line="")
2572 :     then write line
2573 :     else if prefix line 3 = "%% "
2574 :     then write (substring(line,3,size(line)-3))
2575 :     else if prefix line 2 = "%%"
2576 :     then write (substring(line,2,size(line)-2))
2577 :     else write ("> " ^ line)
2578 :    
2579 :     fun convert_tabs s =
2580 :     implode (map (fn "\t" => " " | s => s) (explode s));
2581 :    
2582 :     fun stream_parse dev =
2583 :     parse (15,(fn i =>
2584 :     let val line = convert_tabs(input_line(dev))
2585 :     val _ = echo_line line
2586 :     in line
2587 :     end))
2588 :    
2589 :     val top_parse = fn () => parse (0,
2590 :     let val not_first_flag = ref(false)
2591 :     in fn i => (( if (!not_first_flag)
2592 :     then (write "> "; flush_out std_out)
2593 :     else not_first_flag := true );
2594 :     input_line std_in)
2595 :     end)
2596 :    
2597 :     end (* functor Parse *)
2598 :    
2599 :     signature SYNTH = sig
2600 :    
2601 :     structure Globals: GLOBALS
2602 :     structure Trm: TRM
2603 :     structure Typ: TYP
2604 :     structure Leq: LEQ
2605 :     sharing Trm.Typ = Typ
2606 :     and Leq.Typ = Typ
2607 :     and Typ.Globals = Globals
2608 :     open Globals
2609 :    
2610 :     val synth: Typ.tenv -> Trm.T -> Typ.T
2611 :    
2612 :     end
2613 :    
2614 :     functor StrgHash() =
2615 :     struct
2616 :    
2617 :     val prime = 8388593 (* largest prime less than 2^23 *)
2618 :     val base = 128
2619 :    
2620 :     fun hashString(str: string) : int =
2621 :     let val l = size str
2622 :     in case l
2623 :     of 0 => 0
2624 :     | 1 => ord str
2625 :     | 2 => ordof(str,0) + base * ordof(str,1)
2626 :     | 3 => ordof(str,0) + base * (ordof(str,1) + base * ordof(str,2))
2627 :     | _ =>
2628 :     let fun loop (0,n) = n
2629 :     | loop (i,n) =
2630 :     let val i = i-1
2631 :     val n' = (base * n + ordof(str,i))
2632 :     in loop (i, (n' - prime * (n' quot prime)))
2633 :     end
2634 :     in loop (l,0)
2635 :     end
2636 :     end
2637 :    
2638 :     end (* structure StrgHash *)
2639 :     functor StringUtils() : STRINGUTILS = struct
2640 :    
2641 :     end
2642 :    
2643 :     signature LEXER =
2644 :     sig
2645 :     structure UserDeclarations :
2646 :     sig
2647 :     type ('a,'b) token
2648 :     type pos
2649 :     type svalue
2650 :     end
2651 :     val makeLexer : (int -> string) -> unit ->
2652 :     (UserDeclarations.svalue,UserDeclarations.pos) UserDeclarations.token
2653 :     end
2654 :    
2655 :     functor FMEETLexFun(structure Tokens: FMEET_TOKENS structure Interface: INTERFACE) : LEXER=
2656 :     struct
2657 :     structure UserDeclarations =
2658 :     struct
2659 :     structure Tokens = Tokens
2660 :     structure Interface = Interface
2661 :     open Interface
2662 :    
2663 :     type pos = Interface.pos
2664 :     type svalue = Tokens.svalue
2665 :     type ('a,'b) token = ('a,'b) Tokens.token
2666 :     type lexresult= (svalue,pos) token
2667 :    
2668 :     val eof = fn () => Tokens.T_EOF(!line,!line)
2669 :    
2670 :     val str_begin = ref(!line);
2671 :     val str_const = ref([]:string list);
2672 :    
2673 :     end (* end of user routines *)
2674 :     exception LexError (* raised if illegal leaf action tried *)
2675 :     structure Internal =
2676 :     struct
2677 :    
2678 :     datatype yyfinstate = N of int
2679 :     type statedata = {fin : yyfinstate list, trans: string}
2680 :     (* transition & final state table *)
2681 :     val tab = let
2682 :     val s0 =
2683 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2684 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2685 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2686 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2687 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2688 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2689 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2690 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2691 :     \\000"
2692 :     val s1 =
2693 :     "\007\007\007\007\007\007\007\007\007\097\099\007\007\007\007\007\
2694 :     \\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
2695 :     \\097\007\007\007\096\095\007\094\093\092\007\007\091\089\088\086\
2696 :     \\084\084\084\084\084\084\084\084\084\084\083\082\080\077\076\007\
2697 :     \\075\072\010\010\010\010\010\010\010\010\010\010\010\010\070\010\
2698 :     \\010\010\010\066\010\010\010\010\010\010\010\065\063\062\007\007\
2699 :     \\061\010\010\053\048\045\042\010\010\040\010\010\010\010\010\035\
2700 :     \\031\010\026\023\019\016\010\012\010\010\010\009\007\008\007\007\
2701 :     \\007"
2702 :     val s3 =
2703 :     "\100\100\100\100\100\100\100\100\100\100\101\100\100\100\100\100\
2704 :     \\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
2705 :     \\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
2706 :     \\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
2707 :     \\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
2708 :     \\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
2709 :     \\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
2710 :     \\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\100\
2711 :     \\100"
2712 :     val s5 =
2713 :     "\102\102\102\102\102\102\102\102\102\102\104\102\102\102\102\102\
2714 :     \\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
2715 :     \\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
2716 :     \\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
2717 :     \\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
2718 :     \\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
2719 :     \\103\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
2720 :     \\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\102\
2721 :     \\102"
2722 :     val s10 =
2723 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2724 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2725 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2726 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2727 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2728 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2729 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2730 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2731 :     \\000"
2732 :     val s12 =
2733 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2734 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2735 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2736 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2737 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2738 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2739 :     \\000\011\011\011\011\011\011\011\011\013\011\011\011\011\011\011\
2740 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2741 :     \\000"
2742 :     val s13 =
2743 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2744 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2745 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2746 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2747 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2748 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2749 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2750 :     \\011\011\011\011\014\011\011\011\011\011\011\000\000\000\000\000\
2751 :     \\000"
2752 :     val s14 =
2753 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2754 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2755 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2756 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2757 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2758 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2759 :     \\000\011\011\011\011\011\011\011\015\011\011\011\011\011\011\011\
2760 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2761 :     \\000"
2762 :     val s16 =
2763 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2764 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2765 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2766 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2767 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2768 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2769 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2770 :     \\011\011\011\017\011\011\011\011\011\011\011\000\000\000\000\000\
2771 :     \\000"
2772 :     val s17 =
2773 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2774 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2775 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2776 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2777 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2778 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2779 :     \\000\011\011\011\011\018\011\011\011\011\011\011\011\011\011\011\
2780 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2781 :     \\000"
2782 :     val s19 =
2783 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2784 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2785 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2786 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2787 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2788 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2789 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2790 :     \\011\011\011\011\011\011\011\011\011\020\011\000\000\000\000\000\
2791 :     \\000"
2792 :     val s20 =
2793 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2794 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2795 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2796 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2797 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2798 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2799 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2800 :     \\021\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2801 :     \\000"
2802 :     val s21 =
2803 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2804 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2805 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2806 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2807 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2808 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2809 :     \\000\011\011\011\011\022\011\011\011\011\011\011\011\011\011\011\
2810 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2811 :     \\000"
2812 :     val s23 =
2813 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2814 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2815 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2816 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2817 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2818 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2819 :     \\000\011\011\011\011\024\011\011\011\011\011\011\011\011\011\011\
2820 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2821 :     \\000"
2822 :     val s24 =
2823 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2824 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2825 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2826 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2827 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2828 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2829 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2830 :     \\011\011\011\011\025\011\011\011\011\011\011\000\000\000\000\000\
2831 :     \\000"
2832 :     val s26 =
2833 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2834 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2835 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2836 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2837 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2838 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2839 :     \\000\011\011\011\011\027\011\011\011\011\011\011\011\011\011\011\
2840 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2841 :     \\000"
2842 :     val s27 =
2843 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2844 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2845 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2846 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2847 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2848 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2849 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2850 :     \\011\011\011\028\011\011\011\011\011\011\011\000\000\000\000\000\
2851 :     \\000"
2852 :     val s28 =
2853 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2854 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2855 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2856 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2857 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2858 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2859 :     \\000\011\011\011\011\029\011\011\011\011\011\011\011\011\011\011\
2860 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2861 :     \\000"
2862 :     val s29 =
2863 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2864 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2865 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2866 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2867 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2868 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2869 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2870 :     \\011\011\011\011\030\011\011\011\011\011\011\000\000\000\000\000\
2871 :     \\000"
2872 :     val s31 =
2873 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2874 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2875 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2876 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2877 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2878 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2879 :     \\000\032\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2880 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2881 :     \\000"
2882 :     val s32 =
2883 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2884 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2885 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2886 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2887 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2888 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2889 :     \\000\011\011\033\011\011\011\011\011\011\011\011\011\011\011\011\
2890 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2891 :     \\000"
2892 :     val s33 =
2893 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2894 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2895 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2896 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2897 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2898 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2899 :     \\000\011\011\011\011\011\011\011\011\011\011\034\011\011\011\011\
2900 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2901 :     \\000"
2902 :     val s35 =
2903 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2904 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2905 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2906 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2907 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2908 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2909 :     \\000\011\011\011\011\011\039\011\011\011\011\011\011\011\011\011\
2910 :     \\036\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2911 :     \\000"
2912 :     val s36 =
2913 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2914 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2915 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2916 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2917 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2918 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2919 :     \\000\011\011\011\011\037\011\011\011\011\011\011\011\011\011\011\
2920 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2921 :     \\000"
2922 :     val s37 =
2923 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2924 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2925 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2926 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2927 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2928 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2929 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\038\011\
2930 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2931 :     \\000"
2932 :     val s40 =
2933 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2934 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2935 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2936 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2937 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2938 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2939 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\041\011\
2940 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2941 :     \\000"
2942 :     val s42 =
2943 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2944 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2945 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2946 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2947 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2948 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2949 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\043\
2950 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2951 :     \\000"
2952 :     val s43 =
2953 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2954 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2955 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2956 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2957 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2958 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2959 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2960 :     \\011\011\044\011\011\011\011\011\011\011\011\000\000\000\000\000\
2961 :     \\000"
2962 :     val s45 =
2963 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2964 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2965 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2966 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2967 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2968 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2969 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\046\011\
2970 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2971 :     \\000"
2972 :     val s46 =
2973 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2974 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2975 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2976 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2977 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2978 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2979 :     \\000\011\011\011\047\011\011\011\011\011\011\011\011\011\011\011\
2980 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2981 :     \\000"
2982 :     val s48 =
2983 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2984 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2985 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2986 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2987 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2988 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2989 :     \\000\011\011\011\011\049\011\011\011\011\011\011\011\011\011\011\
2990 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
2991 :     \\000"
2992 :     val s49 =
2993 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2994 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
2995 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
2996 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
2997 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
2998 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
2999 :     \\000\011\050\011\011\011\011\011\011\011\011\011\011\011\011\011\
3000 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3001 :     \\000"
3002 :     val s50 =
3003 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3004 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3005 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3006 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3007 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3008 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3009 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3010 :     \\011\011\011\011\011\051\011\011\011\011\011\000\000\000\000\000\
3011 :     \\000"
3012 :     val s51 =
3013 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3014 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3015 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3016 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3017 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3018 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3019 :     \\000\011\011\011\011\011\011\052\011\011\011\011\011\011\011\011\
3020 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3021 :     \\000"
3022 :     val s53 =
3023 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3024 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3025 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3026 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3027 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3028 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3029 :     \\000\058\011\011\011\011\011\011\054\011\011\011\011\011\011\011\
3030 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3031 :     \\000"
3032 :     val s54 =
3033 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3034 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3035 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3036 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3037 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3038 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3039 :     \\000\011\011\011\011\055\011\011\011\011\011\011\011\011\011\011\
3040 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3041 :     \\000"
3042 :     val s55 =
3043 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3044 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3045 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3046 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3047 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3048 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3049 :     \\000\011\011\056\011\011\011\011\011\011\011\011\011\011\011\011\
3050 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3051 :     \\000"
3052 :     val s56 =
3053 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3054 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3055 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3056 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3057 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3058 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3059 :     \\000\011\011\011\011\011\011\011\011\011\011\057\011\011\011\011\
3060 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3061 :     \\000"
3062 :     val s58 =
3063 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3064 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3065 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3066 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3067 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3068 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3069 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3070 :     \\011\011\011\059\011\011\011\011\011\011\011\000\000\000\000\000\
3071 :     \\000"
3072 :     val s59 =
3073 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3074 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3075 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3076 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3077 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3078 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3079 :     \\000\011\011\011\011\060\011\011\011\011\011\011\011\011\011\011\
3080 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3081 :     \\000"
3082 :     val s63 =
3083 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3084 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3085 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3086 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3087 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3088 :     \\000\000\000\000\000\000\000\000\000\000\000\000\064\000\000\000\
3089 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3090 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3091 :     \\000"
3092 :     val s66 =
3093 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3094 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3095 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3096 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3097 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3098 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3099 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\067\
3100 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3101 :     \\000"
3102 :     val s67 =
3103 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3104 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3105 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3106 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3107 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3108 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3109 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\068\011\011\
3110 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3111 :     \\000"
3112 :     val s68 =
3113 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3114 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3115 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3116 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3117 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3118 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3119 :     \\000\011\011\011\011\069\011\011\011\011\011\011\011\011\011\011\
3120 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3121 :     \\000"
3122 :     val s70 =
3123 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3124 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3125 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3126 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3127 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3128 :     \\011\011\011\071\011\011\011\011\011\011\011\000\000\000\000\011\
3129 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3130 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3131 :     \\000"
3132 :     val s72 =
3133 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3134 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3135 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3136 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3137 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3138 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3139 :     \\000\011\011\011\011\011\011\011\011\011\011\011\073\011\011\011\
3140 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3141 :     \\000"
3142 :     val s73 =
3143 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3144 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3145 :     \\000\000\000\000\000\000\000\011\000\000\000\000\000\000\000\000\
3146 :     \\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\000\
3147 :     \\000\011\011\011\011\011\011\011\011\011\011\011\011\011\011\011\
3148 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\011\
3149 :     \\000\011\011\011\011\011\011\011\011\011\011\011\074\011\011\011\
3150 :     \\011\011\011\011\011\011\011\011\011\011\011\000\000\000\000\000\
3151 :     \\000"
3152 :     val s77 =
3153 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3154 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3155 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3156 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\079\078\000\
3157 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3158 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3159 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3160 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3161 :     \\000"
3162 :     val s80 =
3163 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3164 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3165 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3166 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\081\000\000\
3167 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3168 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3169 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3170 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3171 :     \\000"
3172 :     val s84 =
3173 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3174 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3175 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3176 :     \\085\085\085\085\085\085\085\085\085\085\000\000\000\000\000\000\
3177 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3178 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3179 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3180 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3181 :     \\000"
3182 :     val s86 =
3183 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3184 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3185 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3186 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3187 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3188 :     \\000\000\000\000\000\000\000\000\000\000\000\000\087\000\000\000\
3189 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3190 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3191 :     \\000"
3192 :     val s89 =
3193 :     "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3194 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3195 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3196 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\090\000\
3197 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3198 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3199 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3200 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3201 :     \\000"
3202 :     val s97 =
3203 :     "\000\000\000\000\000\000\000\000\000\098\000\000\000\000\000\000\
3204 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3205 :     \\098\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3206 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3207 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3208 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3209 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3210 :     \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
3211 :     \\000"
3212 :     in arrayoflist
3213 :     [{fin = [], trans = s0},
3214 :     {fin = [(N 32)], trans = s1},
3215 :     {fin = [(N 32)], trans = s1},
3216 :     {fin = [], trans = s3},
3217 :     {fin = [], trans = s3},
3218 :     {fin = [], trans = s5},
3219 :     {fin = [], trans = s5},
3220 :     {fin = [(N 144)], trans = s0},
3221 :     {fin = [(N 80),(N 144)], trans = s0},
3222 :     {fin = [(N 78),(N 144)], trans = s0},
3223 :     {fin = [(N 137),(N 144)], trans = s10},
3224 :     {fin = [(N 137)], trans = s10},
3225 :     {fin = [(N 137),(N 144)], trans = s12},
3226 :     {fin = [(N 137)], trans = s13},
3227 :     {fin = [(N 137)], trans = s14},
3228 :     {fin = [(N 91),(N 137)], trans = s10},
3229 :     {fin = [(N 137),(N 144)], trans = s16},
3230 :     {fin = [(N 137)], trans = s17},
3231 :     {fin = [(N 3),(N 137)], trans = s10},
3232 :     {fin = [(N 137),(N 144)], trans = s19},
3233 :     {fin = [(N 137)], trans = s20},
3234 :     {fin = [(N 137)], trans = s21},
3235 :     {fin = [(N 8),(N 137)], trans = s10},
3236 :     {fin = [(N 137),(N 144)], trans = s23},
3237 :     {fin = [(N 137)], trans = s24},
3238 :     {fin = [(N 12),(N 137)], trans = s10},
3239 :     {fin = [(N 137),(N 144)], trans = s26},
3240 :     {fin = [(N 137)], trans = s27},
3241 :     {fin = [(N 137)], trans = s28},
3242 :     {fin = [(N 137)], trans = s29},
3243 :     {fin = [(N 18),(N 137)], trans = s10},
3244 :     {fin = [(N 137),(N 144)], trans = s31},
3245 :     {fin = [(N 137)], trans = s32},
3246 :     {fin = [(N 137)], trans = s33},
3247 :     {fin = [(N 122),(N 137)], trans = s10},
3248 :     {fin = [(N 137),(N 144)], trans = s35},
3249 :     {fin = [(N 137)], trans = s36},
3250 :     {fin = [(N 137)], trans = s37},
3251 :     {fin = [(N 117),(N 137)], trans = s10},
3252 :     {fin = [(N 99),(N 137)], trans = s10},
3253 :     {fin = [(N 137),(N 144)], trans = s40},
3254 :     {fin = [(N 129),(N 137)], trans = s10},
3255 :     {fin = [(N 137),(N 144)], trans = s42},
3256 :     {fin = [(N 137)], trans = s43},
3257 :     {fin = [(N 103),(N 137)], trans = s10},
3258 :     {fin = [(N 137),(N 144)], trans = s45},
3259 :     {fin = [(N 137)], trans = s46},
3260 :     {fin = [(N 126),(N 137)], trans = s10},
3261 :     {fin = [(N 137),(N 144)], trans = s48},
3262 :     {fin = [(N 137)], trans = s49},
3263 :     {fin = [(N 137)], trans = s50},
3264 :     {fin = [(N 137)], trans = s51},
3265 :     {fin = [(N 24),(N 137)], trans = s10},
3266 :     {fin = [(N 137),(N 144)], trans = s53},
3267 :     {fin = [(N 137)], trans = s54},
3268 :     {fin = [(N 137)], trans = s55},
3269 :     {fin = [(N 137)], trans = s56},
3270 :     {fin = [(N 30),(N 137)], trans = s10},
3271 :     {fin = [(N 137)], trans = s58},
3272 :     {fin = [(N 137)], trans = s59},
3273 :     {fin = [(N 96),(N 137)], trans = s10},
3274 :     {fin = [(N 142),(N 144)], trans = s0},
3275 :     {fin = [(N 72),(N 144)], trans = s0},
3276 :     {fin = [(N 134),(N 144)], trans = s63},
3277 :     {fin = [(N 132)], trans = s0},
3278 :     {fin = [(N 70),(N 144)], trans = s0},
3279 :     {fin = [(N 137),(N 144)], trans = s66},
3280 :     {fin = [(N 137)], trans = s67},
3281 :     {fin = [(N 137)], trans = s68},
3282 :     {fin = [(N 112),(N 137)], trans = s10},
3283 :     {fin = [(N 137),(N 144)], trans = s70},
3284 :     {fin = [(N 86),(N 137)], trans = s10},
3285 :     {fin = [(N 137),(N 144)], trans = s72},
3286 :     {fin = [(N 137)], trans = s73},
3287 :     {fin = [(N 107),(N 137)], trans = s10},
3288 :     {fin = [(N 42),(N 144)], trans = s0},
3289 :     {fin = [(N 76),(N 144)], trans = s0},
3290 :     {fin = [(N 52),(N 144)], trans = s77},
3291 :     {fin = [(N 61)], trans = s0},
3292 :     {fin = [(N 55)], trans = s0},
3293 :     {fin = [(N 74),(N 144)], trans = s80},
3294 :     {fin = [(N 58)], trans = s0},
3295 :     {fin = [(N 44),(N 144)], trans = s0},
3296 :     {fin = [(N 38),(N 144)], trans = s0},
3297 :     {fin = [(N 140),(N 144)], trans = s84},
3298 :     {fin = [(N 140)], trans = s84},
3299 :     {fin = [(N 144)], trans = s86},
3300 :     {fin = [(N 64)], trans = s0},
3301 :     {fin = [(N 46),(N 144)], trans = s0},
3302 :     {fin = [(N 144)], trans = s89},
3303 :     {fin = [(N 83)], trans = s0},
3304 :     {fin = [(N 48),(N 144)], trans = s0},
3305 :     {fin = [(N 68),(N 144)], trans = s0},
3306 :     {fin = [(N 66),(N 144)], trans = s0},
3307 :     {fin = [(N 50),(N 144)], trans = s0},
3308 :     {fin = [(N 36),(N 144)], trans = s0},
3309 :     {fin = [(N 40),(N 144)], trans = s0},
3310 :     {fin = [(N 32),(N 144)], trans = s97},
3311 :     {fin = [(N 32)], trans = s97},
3312 :     {fin = [(N 34)], trans = s0},
3313 :     {fin = [(N 148)], trans = s0},
3314 :     {fin = [(N 146)], trans = s0},
3315 :     {fin = [(N 154)], trans = s0},
3316 :     {fin = [(N 152),(N 154)], trans = s0},
3317 :     {fin = [(N 150)], trans = s0}]
3318 :     end
3319 :     structure StartStates =
3320 :     struct
3321 :     datatype yystartstate = STARTSTATE of int
3322 :    
3323 :     (* start state definitions *)
3324 :    
3325 :     val COMMENT = STARTSTATE 3;
3326 :     val INITIAL = STARTSTATE 1;
3327 :     val STRING = STARTSTATE 5;
3328 :    
3329 :     end
3330 :     type result = UserDeclarations.lexresult
3331 :     exception LexerError (* raised if illegal leaf action tried *)
3332 :     end
3333 :    
3334 :     fun makeLexer yyinput =
3335 :     let
3336 :     val yyb = ref "\n" (* buffer *)
3337 :     val yybl = ref 1 (*buffer length *)
3338 :     val yybufpos = ref 1 (* location of next character to use *)
3339 :     val yygone = ref 1 (* position in file of beginning of buffer *)
3340 :     val yydone = ref false (* eof found yet? *)
3341 :     val yybegin = ref 1 (*Current 'start state' for lexer *)
3342 :    
3343 :     val YYBEGIN = fn (Internal.StartStates.STARTSTATE x) =>
3344 :     yybegin := x
3345 :    
3346 :     fun lex () : Internal.result =
3347 :     let fun continue() = lex() in
3348 :     let fun scan (s,AcceptingLeaves : Internal.yyfinstate list list,l,i0) =
3349 :     let fun action (i,nil) = raise LexError
3350 :     | action (i,nil::l) = action (i-1,l)
3351 :     | action (i,(node::acts)::l) =
3352 :     case node of
3353 :     Internal.N yyk =>
3354 :     (let val yytext = substring(!yyb,i0,i-i0)
3355 :     val yypos = i0+ !yygone
3356 :     open UserDeclarations Internal.StartStates
3357 :     in (yybufpos := i; case yyk of
3358 :    
3359 :     (* Application actions *)
3360 :    
3361 :     103 => (Tokens.T_FOR(!line,!line))
3362 :     | 107 => (Tokens.T_ALL(!line,!line))
3363 :     | 112 => (Tokens.T_SOME(!line,!line))
3364 :     | 117 => (Tokens.T_OPEN(!line,!line))
3365 :     | 12 => (Tokens.T_SET(!line,!line))
3366 :     | 122 => (Tokens.T_PACK(!line,!line))
3367 :     | 126 => (Tokens.T_END (!line,!line))
3368 :     | 129 => (Tokens.T_IN(!line,!line))
3369 :     | 132 => (Tokens.T_BIGLAMBDA(!line,!line))
3370 :     | 134 => (Tokens.T_LAMBDA(!line,!line))
3371 :     | 137 => (Tokens.T_ID (yytext,!line,!line))
3372 :     | 140 => (Tokens.T_INT_CONST (yytext,!line,!line))
3373 :     | 142 => (str_begin:=(!line); str_const:=[]; YYBEGIN STRING; lex())
3374 :     | 144 => (error ("ignoring illegal character" ^ yytext,
3375 :     !line,!line); lex())
3376 :     | 146 => (next_line(); YYBEGIN INITIAL; lex())
3377 :     | 148 => (lex())
3378 :     | 150 => (next_line(); lex())
3379 :     | 152 => (YYBEGIN INITIAL;
3380 :     Tokens.T_STR_CONST(implode(rev(!str_const)),
3381 :     !str_begin,!line))
3382 :     | 154 => (str_const:=(yytext::(!str_const)); lex())
3383 :     | 18 => (Tokens.T_RESET(!line,!line))
3384 :     | 24 => (Tokens.T_DEBUG(!line,!line))
3385 :     | 3 => (Tokens.T_USE(!line,!line))
3386 :     | 30 => (Tokens.T_CHECK(!line,!line))
3387 :     | 32 => (lex())
3388 :     | 34 => (next_line(); lex())
3389 :     | 36 => (YYBEGIN COMMENT; lex())
3390 :     | 38 => (Tokens.T_COLON(!line,!line))
3391 :     | 40 => (Tokens.T_DOLLAR(!line,!line))
3392 :     | 42 => (Tokens.T_AT(!line,!line))
3393 :     | 44 => (Tokens.T_EOF(!line,!line))
3394 :     | 46 => (Tokens.T_DOT(!line,!line))
3395 :     | 48 => (Tokens.T_COMMA(!line,!line))
3396 :     | 50 => (Tokens.T_APOST(!line,!line))
3397 :     | 52 => (Tokens.T_EQ(!line,!line))
3398 :     | 55 => (Tokens.T_DOUBLEEQ(!line,!line))
3399 :     | 58 => (Tokens.T_LEQ(!line,!line))
3400 :     | 61 => (Tokens.T_DARROW(!line,!line))
3401 :     | 64 => (Tokens.T_INTER(!line,!line))
3402 :     | 66 => (Tokens.T_LPAREN(!line,!line))
3403 :     | 68 => (Tokens.T_RPAREN(!line,!line))
3404 :     | 70 => (Tokens.T_LBRACK(!line,!line))
3405 :     | 72 => (Tokens.T_RBRACK(!line,!line))
3406 :     | 74 => (Tokens.T_LANGLE(!line,!line))
3407 :     | 76 => (Tokens.T_RANGLE(!line,!line))
3408 :     | 78 => (Tokens.T_LCURLY(!line,!line))
3409 :     | 8 => (Tokens.T_TYPE(!line,!line))
3410 :     | 80 => (Tokens.T_RCURLY(!line,!line))
3411 :     | 83 => (Tokens.T_ARROW(!line,!line))
3412 :     | 86 => (Tokens.T_NS(!line,!line))
3413 :     | 91 => (Tokens.T_WITH(!line,!line))
3414 :     | 96 => (Tokens.T_CASE(!line,!line))
3415 :     | 99 => (Tokens.T_OF(!line,!line))
3416 :     | _ => raise Internal.LexerError
3417 :    
3418 :     ) end )
3419 :    
3420 :     val {fin,trans} = Internal.tab sub s
3421 :     val NewAcceptingLeaves = fin::AcceptingLeaves
3422 :     in if l = !yybl then
3423 :     if trans = #trans(Internal.tab sub 0)
3424 :     then action(l,NewAcceptingLeaves) else
3425 :     let val newchars= if !yydone then "" else yyinput 1024
3426 :     in if (size newchars)=0
3427 :     then (yydone := true;
3428 :     if (l=i0) then UserDeclarations.eof ()
3429 :     else action(l,NewAcceptingLeaves))
3430 :     else (if i0=l then yyb := newchars
3431 :     else yyb := substring(!yyb,i0,l-i0)^newchars;
3432 :     yygone := !yygone+i0;
3433 :     yybl := size (!yyb);
3434 :     scan (s,AcceptingLeaves,l-i0,0))
3435 :     end
3436 :     else let val NewChar = ordof(!yyb,l)
3437 :     val NewState = if NewChar<128 then ordof(trans,NewChar) else ordof(trans,128)
3438 :     in if NewState=0 then action(l,NewAcceptingLeaves)
3439 :     else scan(NewState,NewAcceptingLeaves,l+1,i0)
3440 :     end
3441 :     end
3442 :     in scan(!yybegin (* start *),nil,!yybufpos,!yybufpos)
3443 :     end
3444 :     end
3445 :     in lex
3446 :     end
3447 :     end
3448 :     functor Registry(
3449 :     type registeredtype
3450 :     ): REGISTRY = struct
3451 :    
3452 :     type registeredtype = registeredtype
3453 :    
3454 :     val registry = ref(nil: (string * (registeredtype->unit)) list)
3455 :    
3456 :     fun register name callback =
3457 :     registry := (name,callback)::(!registry)
3458 :    
3459 :     fun registerflag name flagref =
3460 :     registry := (name,(fn b => flagref := b))::(!registry)
3461 :    
3462 :     exception NotRegistered of string
3463 :    
3464 :     fun set_flag name v =
3465 :     let fun f [] = raise NotRegistered(name)
3466 :     | f ((n,callback)::tl) = if name=n
3467 :     then (callback v)
3468 :     else f tl
3469 :     in f (!registry)
3470 :     end
3471 :    
3472 :     fun set_all v =
3473 :     let fun f [] = ()
3474 :     | f ((n,callback)::tl) = (callback v; f tl)
3475 :     in f (!registry)
3476 :     end
3477 :    
3478 :     end
3479 :     functor Typ(
3480 :     structure Globals: GLOBALS
3481 :     ) : TYPPVT
3482 :     = struct
3483 :    
3484 :     structure Globals = Globals
3485 :     open Globals
3486 :     open Pp
3487 :    
3488 :     datatype pretyp =
3489 :     PRETVAR of Id.T
3490 :     | PREARROW of pretyp * pretyp
3491 :     | PREALL of Id.T * pretyp * pretyp
3492 :     | PREMEET of pretyp list
3493 :    
3494 :     datatype T =
3495 :     TVAR of unit * int
3496 :     | ARROW of unit * T * T
3497 :     | ALL of {name:Id.T} * T * T
3498 :     | MEET of unit * (T list)
3499 :    
3500 :     type idindex = int
3501 :    
3502 :     val NS = MEET ((),[])
3503 :    
3504 :     exception UnknownId of string
3505 :    
3506 :     datatype tenvelt = BND of Id.T * T
3507 :     | ABB of Id.T * T
3508 :     | VBND of Id.T * T
3509 :    
3510 :     datatype tenv = TENV of tenvelt list
3511 :    
3512 :     fun push_bound (TENV(te)) i t = TENV(BND(i,t)::te)
3513 :    
3514 :     fun push_abbrev (TENV(te)) i t = TENV(ABB(i,t)::te)
3515 :    
3516 :     fun push_binding (TENV(te)) i t = TENV(VBND(i,t)::te)
3517 :    
3518 :     val empty_tenv = TENV(nil)
3519 :    
3520 :     fun index (TENV(bvs)) i =
3521 :     let fun ind [] n =
3522 :     raise UnknownId(Id.tostr i)
3523 :     | ind (BND(i',_)::rest) n =
3524 :     if Id.== i i'
3525 :     then n
3526 :     else ind rest (n+1)
3527 :     | ind (VBND(i',_)::rest) n =
3528 :     if Id.== i i'
3529 :     then n
3530 :     else ind rest (n+1)
3531 :     | ind (ABB(i',_)::rest) n =
3532 :     if Id.== i i'
3533 :     then n
3534 :     else ind rest (n+1)
3535 :     in ind bvs 0
3536 :     end
3537 :    
3538 :     exception TypeVariableOutOfRange of int
3539 :    
3540 :     fun old_lookup_name (TENV(te)) i =
3541 :     (case (nth (te,i)) of
3542 :     BND(name,_) => name
3543 :     | VBND(name,_) => name
3544 :     | ABB(name,_) => name)
3545 :     handle Nth => Id.intern(("<BAD INDEX: " ^ (makestring i) ^ ">"))
3546 :    
3547 :     fun lookup_name (TENV(te)) i =
3548 :     let fun l [] _ _ = Id.intern(("<BAD INDEX: " ^ (makestring i) ^ ">"))
3549 :     | l (hd::tl) rest 0 =
3550 :     let val name = case hd of BND(n,_) => n | VBND(n,_) => n | ABB(n,_) => n
3551 :     in if memq Id.== rest name
3552 :     then Id.intern ((Id.tostr name) ^ "^" ^ (makestring i))
3553 :     else name
3554 :     end
3555 :     | l (hd::tl) rest j =
3556 :     let val name = case hd of BND(n,_) => n | VBND(n,_) => n | ABB(n,_) => n
3557 :     in l tl (name::rest) (j-1)
3558 :     end
3559 :     in l te [] i
3560 :     end
3561 :    
3562 :     exception WrongKindOfId of tenv * int * string
3563 :    
3564 :     fun lookup (TENV(te)) i =
3565 :     nth (te,i)
3566 :     handle Nth => raise TypeVariableOutOfRange(i)
3567 :    
3568 :     exception TriedToPopEmptyTEnv
3569 :     fun pop (TENV(hd::tl)) = TENV(tl)
3570 :     | pop _ = raise TriedToPopEmptyTEnv
3571 :    
3572 :     fun inner_relocate offset cutoff t =
3573 :     let fun r c (TVAR((),i)) = if i>=c
3574 :     then TVAR((),i + offset)
3575 :     else TVAR((),i)
3576 :     | r c (ARROW((),t1,t2)) = ARROW((), r c t1, r c t2)
3577 :     | r c (ALL({name=i},t1,t2)) = ALL({name=i}, r c t1, r (c+1) t2)
3578 :     | r c (MEET((),ts)) = MEET((), map (fn t => r c t) ts)
3579 :     in r cutoff t
3580 :     end
3581 :    
3582 :     fun relocate offset t = inner_relocate offset 0 t
3583 :    
3584 :     fun lookup_and_relocate (te) i =
3585 :     case lookup te i of
3586 :     BND(n,b) => BND(n, relocate (i+1) b)
3587 :     | VBND(n,b) => VBND(n, relocate (i+1) b)
3588 :     | ABB(n,b) => ABB(n, relocate (i+1) b)
3589 :    
3590 :     fun lookup_and_relocate_bound te i =
3591 :     case lookup_and_relocate te i of
3592 :     BND(_,b) => b
3593 :     | VBND(n,_) => raise WrongKindOfId(te,i,"tvar")
3594 :     | ABB(n,_) => raise WrongKindOfId(te,i,"tvar")
3595 :    
3596 :     fun lookup_and_relocate_binding te i =
3597 :     case lookup_and_relocate te i of
3598 :     BND(n,b) => raise WrongKindOfId(te,i,"var")
3599 :     | VBND(n,b) => b
3600 :     | ABB(n,b) => raise WrongKindOfId(te,i,"var")
3601 :    
3602 :     fun lookup_abbrev te i =
3603 :     case lookup_and_relocate te i of
3604 :     BND(n,_) => raise WrongKindOfId(te,i,"tabbrev")
3605 :     | VBND(n,b) => raise WrongKindOfId(te,i,"tabbrev")
3606 :     | ABB(n,b) => b
3607 :    
3608 :     fun debruijnify te (PRETVAR i) =
3609 :     TVAR((), index te i)
3610 :     | debruijnify te (PREARROW (pt1,pt2)) =
3611 :     ARROW((), debruijnify te pt1, debruijnify te pt2)
3612 :     | debruijnify te (PREALL (i,pt1,pt2)) =
3613 :     ALL({name=i}, debruijnify te pt1, debruijnify (push_bound te i NS) pt2)
3614 :     | debruijnify te (PREMEET pts) =
3615 :     MEET((), map (fn pt => debruijnify te pt) pts)
3616 :    
3617 :     fun tsubst_top targ tbody =
3618 :     let fun s i (t as TVAR(x,i')) = if i = i'
3619 :     then relocate i targ
3620 :     else if i < i'
3621 :     then TVAR(x,i'-1)
3622 :     else t
3623 :     | s i (ARROW(x,t1,t2)) = ARROW(x, s i t1, s i t2)
3624 :     | s i (ALL(x,t1,t2)) = ALL(x, s i t1, s (i+1) t2)
3625 :     | s i (MEET(x,ts)) = MEET(x, map (fn t => s i t) ts)
3626 :     in s 0 tbody
3627 :     end
3628 :    
3629 :     fun prt pp te t =
3630 :     let fun p te (TVAR(_,i)) =
3631 :     Pp.pwrite pp (Id.tostr (lookup_name te i))
3632 :     | p te (ARROW(_,t1,t2)) =
3633 :     (Pp.pwrite pp "(";
3634 :     p te t1;
3635 :     Pp.pwrite pp "->";
3636 :     p te t2;
3637 :     Pp.pwrite pp ")")
3638 :     | p te (ALL({name=i},t1,t2)) =
3639 :     (Pp.pwrite pp "(All ";
3640 :     Pp.pwrite pp (Id.tostr i);
3641 :     Pp.pwrite pp "<=";
3642 :     p te t1;
3643 :     Pp.pwrite pp ". ";
3644 :     p (push_bound te i t1) t2;
3645 :     Pp.pwrite pp ")")
3646 :     | p te (MEET(_,[])) =
3647 :     Pp.pwrite pp "NS"
3648 :     | p te (MEET(_,ts)) =
3649 :     (Pp.pwrite pp "/\\[";
3650 :     plist te ts;
3651 :     Pp.pwrite pp "]")
3652 :     and plist te [] =
3653 :     ()
3654 :     | plist te [t] =
3655 :     p te t
3656 :     | plist te (hd::tl) =
3657 :     (p te hd; pwrite pp ","; plist te tl)
3658 :     in p te t
3659 :     end
3660 :    
3661 :     val short_tenvs = ref(true);
3662 :     val _ = registerflag "shorttenvs" short_tenvs;
3663 :    
3664 :     fun prt_tenv pp (TENV(te')) =
3665 :     let fun p [] = ()
3666 :     | p [(BND(i,t))] =
3667 :     (Pp.pwrite pp (Id.tostr i);
3668 :     Pp.pwrite pp "<=";
3669 :     prt pp (TENV([])) t)
3670 :     | p ((BND(i,t))::tl) =
3671 :     (if (!short_tenvs)
3672 :     then pwrite pp "... "
3673 :     else p tl;
3674 :     Pp.pwrite pp ", ";
3675 :     Pp.break pp false 0;
3676 :     Pp.pwrite pp (Id.tostr i);
3677 :     Pp.pwrite pp "<=";
3678 :     prt pp (TENV(tl)) t)
3679 :     | p [(VBND(i,t))] =
3680 :     (Pp.pwrite pp (Id.tostr i);
3681 :     Pp.pwrite pp ":";
3682 :     prt pp (TENV([])) t)
3683 :     | p ((VBND(i,t))::tl) =
3684 :     (if (!short_tenvs)
3685 :     then pwrite pp "... "
3686 :     else p tl;
3687 :     Pp.pwrite pp ", ";
3688 :     Pp.break pp false 0;
3689 :     Pp.pwrite pp (Id.tostr i);
3690 :     Pp.pwrite pp ":";
3691 :     prt pp (TENV(tl)) t)
3692 :     | p [(ABB(i,t))] =
3693 :     (Pp.pwrite pp (Id.tostr i);
3694 :     Pp.pwrite pp "=";
3695 :     prt pp (TENV([])) t)
3696 :     | p ((ABB(i,t))::tl) =
3697 :     (if (!short_tenvs)
3698 :     then pwrite pp "... "
3699 :     else p tl;
3700 :     Pp.pwrite pp ", ";
3701 :     Pp.break pp false 0;
3702 :     Pp.pwrite pp (Id.tostr i);
3703 :     Pp.pwrite pp "=";
3704 :     prt pp (TENV(tl)) t)
3705 :     in Pp.pwrite pp "{";
3706 :     Pp.setb pp;
3707 :     p te';
3708 :     Pp.endb pp;
3709 :     Pp.pwrite pp "}"
3710 :     end
3711 :    
3712 :     end
3713 :     functor Leq(
3714 :     structure Typ: TYPPVT
3715 :     structure Globals: GLOBALS
3716 :     sharing Typ.Globals = Globals
3717 :     ) : LEQ = struct
3718 :    
3719 :     structure Typ = Typ
3720 :     structure Globals = Globals
3721 :     open Globals
3722 :     open Typ
3723 :    
3724 :     datatype lhsqueue =
3725 :     ARROW_LHS of Typ.T
3726 :     | ALL_LHS of Id.T * Typ.T
3727 :    
3728 :     datatype rhs_flag = EXPAND | FIX
3729 :    
3730 :     val DEBUG = ref(false)
3731 :     val _ = (registerflag "leq" DEBUG;
3732 :     registerflag "Leq" DEBUG)
3733 :    
3734 :     fun describe_rest pp te [] t flag =
3735 :     (Pp.pwrite pp "] -> ";
3736 :     Typ.prt pp te t;
3737 :     case flag of
3738 :     EXPAND => Pp.pwrite pp " (EXPAND)? "
3739 :     | FIX => Pp.pwrite pp " (FIX)? ")
3740 :     | describe_rest pp te [ARROW_LHS(t1)] t2 flag =
3741 :     (Typ.prt pp te t1;
3742 :     describe_rest pp te [] t2 flag)
3743 :     | describe_rest pp te ((ARROW_LHS(t1))::X2) t2 flag =
3744 :     (Typ.prt pp te t1;
3745 :     Pp.pwrite pp ",";
3746 :     describe_rest pp te X2 t2 flag)
3747 :     | describe_rest pp te [ALL_LHS(v,t1)] t2 flag =
3748 :     (Pp.pwrite pp (Id.tostr v);
3749 :     Pp.pwrite pp "<=";
3750 :     Typ.prt pp te t1;
3751 :     describe_rest pp (push_bound te v t1) [] t2 flag)
3752 :     | describe_rest pp te ((ALL_LHS(v,t1))::X2) t2 flag =
3753 :     (Pp.pwrite pp (Id.tostr v);
3754 :     Pp.pwrite pp "<=";
3755 :     Typ.prt pp te t1;
3756 :     Pp.pwrite pp ",";
3757 :     describe_rest pp (push_bound te v t1) X2 t2 flag)
3758 :    
3759 :     fun describe_problem pp te s X t flag =
3760 :     (Pp.setb pp;
3761 :     Typ.prt pp te s;
3762 :     Pp.break pp true ~3;
3763 :     Pp.pwrite pp " <= ";
3764 :     Pp.pwrite pp "[";
3765 :     describe_rest pp te X t flag;
3766 :     Pp.endb pp)
3767 :    
3768 :     fun bindings_in [] = 0
3769 :     | bindings_in (ARROW_LHS(_)::tl) = bindings_in tl
3770 :     | bindings_in (ALL_LHS(_)::tl) = 1 + (bindings_in tl)
3771 :    
3772 :     fun leqq' te s X (MEET(_,ts)) EXPAND =
3773 :     forall (fn t => leqq te s X t EXPAND) ts
3774 :     | leqq' te s X (ARROW(_,t1,t2)) EXPAND =
3775 :     leqq te s (X@[ARROW_LHS(t1)]) t2 EXPAND
3776 :     | leqq' te s X (ALL({name=i},t1,t2)) EXPAND =
3777 :     leqq te s (X@[ALL_LHS(i,t1)]) t2 EXPAND
3778 :     | leqq' te s X (t as TVAR(_,vt)) EXPAND =
3779 :     let val bx = bindings_in X
3780 :     in if vt < bx
3781 :     then leqq te s X t FIX
3782 :     else case Typ.lookup te (vt - bx) of
3783 :     BND(_,_) => leqq te s X t FIX
3784 :     | VBND(n,_) => raise Typ.WrongKindOfId(te, vt - bx,"tvar or tabbrev")
3785 :     | ABB(_,ab) => leqq te s X (Typ.relocate (vt + bx) ab) EXPAND
3786 :     end
3787 :     | leqq' te (MEET(_,ss)) X (t as (TVAR(_,vt))) FIX =
3788 :     forsome (fn s => leqq te s X t FIX) ss
3789 :     | leqq' te (ARROW(_,s1,s2)) (ARROW_LHS(t1)::X) (t as (TVAR(_,vt))) FIX =
3790 :     (leqq te t1 [] s1 EXPAND)
3791 :     andalso
3792 :     (leqq te s2 X t FIX)
3793 :     | leqq' te (ALL(_,s1,s2)) (ALL_LHS(i,t1)::X) (t as (TVAR(_,vt))) FIX =
3794 :     (leqq (push_bound te i t1) s2 X t FIX)
3795 :     andalso
3796 :     (leqq te t1 [] s1 EXPAND)
3797 :     | leqq' te (TVAR(_,vs)) X (t as (TVAR(_,vt))) FIX =
3798 :     (vs = vt andalso (null X))
3799 :     orelse
3800 :     (case lookup_and_relocate te vs of
3801 :     BND(_,bnd) => (leqq te bnd X t FIX)
3802 :     | VBND(n,ab) => raise Typ.WrongKindOfId(te,vs,"tvar or tabbrev")
3803 :     | ABB(_,ab) => (leqq te ab X t FIX))
3804 :     | leqq' te s X t flag =
3805 :     false
3806 :    
3807 :     and leqq te s X t flag =
3808 :     wrap DEBUG "leqq"
3809 :     (fn () =>
3810 :     leqq' te s X t flag)
3811 :     (fn () => describe_problem (stdpp()) te s X t flag)
3812 :     (fn b => write (if b then "Yes" else "No"))
3813 :    
3814 :     fun leq te s t = leqq te s [] t EXPAND
3815 :    
3816 :     end
3817 :    
3818 :     functor HashFun () = struct
3819 :    
3820 :     val version = 1.0
3821 :    
3822 :     type ('a,'b) table = ('a*'a->bool) * (('a*int*'b) list array) * int
3823 :    
3824 :     fun create (sample'key :'1a) (equality :'1a * '1a -> bool)
3825 :     table'size (sample'value :'1b) :('1a,'1b) table =
3826 :     let val mt = tl [(sample'key, 0, sample'value)]
3827 :     in (equality, array (table'size, mt), table'size)
3828 :     end
3829 :    
3830 :     val defaultSize = 97 (* a prime; or try primes 37, 997 *)
3831 :    
3832 :     fun defaultEqual ((x :string), (y :string)) :bool = (x = y)
3833 :    
3834 :     fun createDefault (sample'value :'1b) :(string,'1b) table =
3835 :     let val mt = tl [("", 0, sample'value)]
3836 :     in (defaultEqual, array (defaultSize, mt), defaultSize)
3837 :     end
3838 :    
3839 :     fun enter ((equal, table, table'size) :('a,'b) table) key hash value =
3840 :     let val place = hash mod table'size
3841 :     val bucket = table sub place
3842 :     fun put'in [] = [(key,hash,value)]
3843 :     | put'in ((k,h,v)::tail) =
3844 :     if (h = hash) andalso equal (k, key)
3845 :     then (key,hash,value)::tail
3846 :     else (k,h,v)::(put'in tail)
3847 :     in
3848 :     update (table, place, put'in bucket)
3849 :     end
3850 :    
3851 :     fun remove ((equal, table, table'size) :('a,'b) table) key hash =
3852 :     let val place = hash mod table'size
3853 :     val bucket = table sub place
3854 :     fun take'out [] = []
3855 :     | take'out ((k,h,v)::tail) =
3856 :     if (h = hash) andalso equal (k, key)
3857 :     then tail
3858 :     else (k,h,v)::(take'out tail)
3859 :     in
3860 :     update (table, place, take'out bucket)
3861 :     end
3862 :    
3863 :     fun lookup ((equal, table, table'size) :('a,'b) table) key hash =
3864 :     let val place = hash mod table'size
3865 :     val bucket = table sub place
3866 :     fun get'out [] = NONE
3867 :     | get'out ((k,h,v)::tail) =
3868 :     if (h = hash) andalso equal (k, key)
3869 :     then SOME v
3870 :     else get'out tail
3871 :     in
3872 :     get'out bucket
3873 :     end
3874 :    
3875 :     fun print ((_, table, table'size) :('a,'b) table)
3876 :     (print'key :'a -> unit) (print'value :'b -> unit) =
3877 :     let fun pr'bucket [] = ()
3878 :     | pr'bucket ((key,hash,value)::rest) =
3879 :     (print'key key; String.print ": ";
3880 :     Integer.print hash; String.print ": ";
3881 :     print'value value; String.print "\n"; pr'bucket rest)
3882 :     fun pr i =
3883 :     if i >= table'size then ()
3884 :     else
3885 :     case (table sub i) of
3886 :     [] => (pr (i+1))
3887 :     | (b as (h::t)) =>
3888 :     (String.print "["; Integer.print i; String.print "]\n";
3889 :     pr'bucket b; pr (i+1))
3890 :     in pr 0 end
3891 :    
3892 :     fun scan ((_, table, table'size) :('a,'b) table) operation =
3893 :     let fun map'bucket [] = ()
3894 :     | map'bucket ((key,hash,value)::rest) =
3895 :     (operation key hash value; map'bucket rest)
3896 :     fun iter i =
3897 :     if i >= table'size then ()
3898 :     else (map'bucket (table sub i); iter (i+1))
3899 :     in iter 0 end
3900 :    
3901 :     fun fold ((_, table, table'size) :('a, 'b) table)
3902 :     (operation :'a -> int -> 'b -> 'g -> 'g) (init :'g) :'g =
3903 :     let fun fold'bucket [] acc = acc
3904 :     | fold'bucket ((key,hash,value)::rest) acc =
3905 :     fold'bucket rest (operation key hash value acc)
3906 :     fun iter i acc =
3907 :     if i >= table'size then acc
3908 :     else iter (i+1) (fold'bucket (table sub i) acc)
3909 :     in iter 0 init end
3910 :    
3911 :     fun scanUpdate ((_, table, table'size) :('a,'b) table) operation =
3912 :     let fun map'bucket [] = []
3913 :     | map'bucket ((key,hash,value)::rest) =
3914 :     ((key,hash,operation key hash value)::(map'bucket rest))
3915 :     fun iter i =
3916 :     if i >= table'size then ()
3917 :     else (update (table, i, map'bucket (table sub i)); iter (i+1))
3918 :     in iter 0 end
3919 :    
3920 :     fun eliminate ((_, table, table'size) :('a,'b) table) predicate =
3921 :     let fun map'bucket [] = []
3922 :     | map'bucket ((key,hash,value)::rest) =
3923 :     if predicate key hash value then map'bucket rest
3924 :     else (key,hash,value)::(map'bucket rest)
3925 :     fun iter i =
3926 :     if i >= table'size then ()
3927 :     else (update (table, i, map'bucket (table sub i)); iter (i+1))
3928 :     in iter 0 end
3929 :    
3930 :     fun bucketLengths ((_, table, table'size) :('a,'b) table) (maxlen :int)
3931 :     :int array =
3932 :     let val count :int array = array (maxlen+1, 0)
3933 :     fun inc'sub x =
3934 :     let val y = min (x, maxlen) in
3935 :     update (count, y, (count sub y) + 1)
3936 :     end
3937 :     fun iter i =
3938 :     if i >= table'size then ()
3939 :     else (inc'sub (length (table sub i)); iter (i+1))
3940 :     in
3941 :     iter 0;
3942 :     count
3943 :     end
3944 :    
3945 :     end
3946 :    
3947 :     signature ORDSET =
3948 :     sig
3949 :     type set
3950 :     type elem
3951 :     exception Select_arb
3952 :     val app : (elem -> 'b) -> set -> unit
3953 :     and card: set -> int
3954 :     and closure: set * (elem -> set) -> set
3955 :     and difference: set * set -> set
3956 :     and elem_eq: (elem * elem -> bool)
3957 :     and elem_gt : (elem * elem -> bool)
3958 :     and empty: set
3959 :     and exists: (elem * set) -> bool
3960 :     and find : (elem * set) -> elem option
3961 :     and fold: ((elem * 'b) -> 'b) -> set -> 'b -> 'b
3962 :     and insert: (elem * set) -> set
3963 :     and is_empty: set -> bool
3964 :     and make_list: set -> elem list
3965 :     and make_set: (elem list -> set)
3966 :     and partition: (elem -> bool) -> (set -> set * set)
3967 :     and remove: (elem * set) -> set
3968 :     and revfold: ((elem * 'b) -> 'b) -> set -> 'b -> 'b
3969 :     and select_arb: set -> elem
3970 :     and set_eq: (set * set) -> bool
3971 :     and set_gt: (set * set) -> bool
3972 :     and singleton: (elem -> set)
3973 :     and union: set * set -> set
3974 :     end
3975 :    
3976 :     signature TABLE =
3977 :     sig
3978 :     type 'a table
3979 :     type key
3980 :     val size : 'a table -> int
3981 :     val empty: 'a table
3982 :     val exists: (key * 'a table) -> bool
3983 :     val find : (key * 'a table) -> 'a option
3984 :     val insert: ((key * 'a) * 'a table) -> 'a table
3985 :     val make_table : (key * 'a ) list -> 'a table
3986 :     val make_list : 'a table -> (key * 'a) list
3987 :     val fold : ((key * 'a) * 'b -> 'b) -> 'a table -> 'b -> 'b
3988 :     end
3989 :    
3990 :     signature HASH =
3991 :     sig
3992 :     type table
3993 :     type elem
3994 :    
3995 :     val size : table -> int
3996 :     val add : elem * table -> table
3997 :     val find : elem * table -> int option
3998 :     val exists : elem * table -> bool
3999 :     val empty : table
4000 :     end;
4001 :    
4002 :     functor ListOrdSet(B : sig type elem
4003 :     val gt : elem * elem -> bool
4004 :     val eq : elem * elem -> bool
4005 :     end ) : ORDSET =
4006 :    
4007 :     struct
4008 :     type elem = B.elem
4009 :     val elem_gt = B.gt
4010 :     val elem_eq = B.eq
4011 :    
4012 :     type set = elem list
4013 :     exception Select_arb
4014 :     val empty = nil
4015 :    
4016 :     val insert = fn (key,s) =>
4017 :     let fun f (l as (h::t)) =
4018 :     if elem_gt(key,h) then h::(f t)
4019 :     else if elem_eq(key,h) then key::t
4020 :     else key::l
4021 :     | f nil = [key]
4022 :     in f s
4023 :     end
4024 :    
4025 :     val select_arb = fn nil => raise Select_arb
4026 :     | a::b => a
4027 :    
4028 :     val exists = fn (key,s) =>
4029 :     let fun f (h::t) = if elem_gt(key,h) then f t
4030 :     else elem_eq(h,key)
4031 :     | f nil = false
4032 :     in f s
4033 :     end
4034 :    
4035 :     val find = fn (key,s) =>
4036 :     let fun f (h::t) = if elem_gt(key,h) then f t
4037 :     else if elem_eq(h,key) then SOME h
4038 :     else NONE
4039 :     | f nil = NONE
4040 :     in f s
4041 :     end
4042 :    
4043 :     val revfold = List.revfold
4044 :     val fold = List.fold
4045 :     val app = List.app
4046 :    
4047 :     fun set_eq(h::t,h'::t') =
4048 :     (case elem_eq(h,h')
4049 :     of true => set_eq(t,t')
4050 :     | a => a)
4051 :     | set_eq(nil,nil) = true
4052 :     | set_eq _ = false
4053 :    
4054 :     fun set_gt(h::t,h'::t') =
4055 :     (case elem_gt(h,h')
4056 :     of false => (case (elem_eq(h,h'))
4057 :     of true => set_gt(t,t')
4058 :     | a => a)
4059 :     | a => a)
4060 :     | set_gt(_::_,nil) = true
4061 :     | set_gt _ = false
4062 :    
4063 :     fun union(a as (h::t),b as (h'::t')) =
4064 :     if elem_gt(h',h) then h::union(t,b)
4065 :     else if elem_eq(h,h') then h::union(t,t')
4066 :     else h'::union(a,t')
4067 :     | union(nil,s) = s
4068 :     | union(s,nil) = s
4069 :    
4070 :     val make_list = fn s => s
4071 :    
4072 :     val is_empty = fn nil => true | _ => false
4073 :    
4074 :     val make_set = fn l => List.fold insert l nil
4075 :    
4076 :     val partition = fn f => fn s =>
4077 :     fold (fn (e,(yes,no)) =>
4078 :     if (f e) then (e::yes,no) else (e::no,yes)) s (nil,nil)
4079 :    
4080 :     val remove = fn (e,s) =>
4081 :     let fun f (l as (h::t)) = if elem_gt(h,e) then l
4082 :     else if elem_eq(h,e) then t
4083 :     else h::(f t)
4084 :     | f nil = nil
4085 :     in f s
4086 :     end
4087 :    
4088 :     (* difference: X-Y *)
4089 :    
4090 :     fun difference (nil,_) = nil
4091 :     | difference (r,nil) = r
4092 :     | difference (a as (h::t),b as (h'::t')) =
4093 :     if elem_gt (h',h) then h::difference(t,b)
4094 :     else if elem_eq(h',h) then difference(t,t')
4095 :     else difference(a,t')
4096 :    
4097 :     fun singleton X = [X]
4098 :    
4099 :     fun card(S) = fold (fn (a,count) => count+1) S 0
4100 :    
4101 :     local
4102 :     fun closure'(from, f, result) =
4103 :     if is_empty from then result
4104 :     else
4105 :     let val (more,result) =
4106 :     fold (fn (a,(more',result')) =>
4107 :     let val more = f a
4108 :     val new = difference(more,result)
4109 :     in (union(more',new),union(result',new))
4110 :     end) from
4111 :     (empty,result)
4112 :     in closure'(more,f,result)
4113 :     end
4114 :     in
4115 :     fun closure(start, f) = closure'(start, f, start)
4116 :     end
4117 :     end
4118 :    
4119 :     functor RbOrdSet (B : sig type elem
4120 :     val eq : (elem*elem) -> bool
4121 :     val gt : (elem*elem) -> bool
4122 :     end
4123 :     ) : ORDSET =
4124 :     struct
4125 :    
4126 :     type elem = B.elem
4127 :     val elem_gt = B.gt
4128 :     val elem_eq = B.eq
4129 :    
4130 :     datatype Color = RED | BLACK
4131 :    
4132 :     abstype set = EMPTY | TREE of (B.elem * Color * set * set)
4133 :     with exception Select_arb
4134 :     val empty = EMPTY
4135 :    
4136 :     fun insert(key,t) =
4137 :     let fun f EMPTY = TREE(key,RED,EMPTY,EMPTY)
4138 :     | f (TREE(k,BLACK,l,r)) =
4139 :     if elem_gt (key,k)
4140 :     then case f r
4141 :     of r as TREE(rk,RED, rl as TREE(rlk,RED,rll,rlr),rr) =>
4142 :     (case l
4143 :     of TREE(lk,RED,ll,lr) =>
4144 :     TREE(k,RED,TREE(lk,BLACK,ll,lr),
4145 :     TREE(rk,BLACK,rl,rr))
4146 :     | _ => TREE(rlk,BLACK,TREE(k,RED,l,rll),
4147 :     TREE(rk,RED,rlr,rr)))
4148 :     | r as TREE(rk,RED,rl, rr as TREE(rrk,RED,rrl,rrr)) =>
4149 :     (case l
4150 :     of TREE(lk,RED,ll,lr) =>
4151 :     TREE(k,RED,TREE(lk,BLACK,ll,lr),
4152 :     TREE(rk,BLACK,rl,rr))
4153 :     | _ => TREE(rk,BLACK,TREE(k,RED,l,rl),rr))
4154 :     | r => TREE(k,BLACK,l,r)
4155 :     else if elem_gt(k,key)
4156 :     then case f l
4157 :     of l as TREE(lk,RED,ll, lr as TREE(lrk,RED,lrl,lrr)) =>
4158 :     (case r
4159 :     of TREE(rk,RED,rl,rr) =>
4160 :     TREE(k,RED,TREE(lk,BLACK,ll,lr),
4161 :     TREE(rk,BLACK,rl,rr))
4162 :     | _ => TREE(lrk,BLACK,TREE(lk,RED,ll,lrl),
4163 :     TREE(k,RED,lrr,r)))
4164 :     | l as TREE(lk,RED, ll as TREE(llk,RED,lll,llr), lr) =>
4165 :     (case r
4166 :     of TREE(rk,RED,rl,rr) =>
4167 :     TREE(k,RED,TREE(lk,BLACK,ll,lr),
4168 :     TREE(rk,BLACK,rl,rr))
4169 :     | _ => TREE(lk,BLACK,ll,TREE(k,RED,lr,r)))
4170 :     | l => TREE(k,BLACK,l,r)
4171 :     else TREE(key,BLACK,l,r)
4172 :     | f (TREE(k,RED,l,r)) =
4173 :     if elem_gt(key,k) then TREE(k,RED,l, f r)
4174 :     else if elem_gt(k,key) then TREE(k,RED, f l, r)
4175 :     else TREE(key,RED,l,r)
4176 :     in case f t
4177 :     of TREE(k,RED, l as TREE(_,RED,_,_), r) => TREE(k,BLACK,l,r)
4178 :     | TREE(k,RED, l, r as TREE(_,RED,_,_)) => TREE(k,BLACK,l,r)
4179 :     | t => t
4180 :     end
4181 :    
4182 :     fun select_arb (TREE(k,_,l,r)) = k
4183 :     | select_arb EMPTY = raise Select_arb
4184 :    
4185 :     fun exists(key,t) =
4186 :     let fun look EMPTY = false
4187 :     | look (TREE(k,_,l,r)) =
4188 :     if elem_gt(k,key) then look l
4189 :     else if elem_gt(key,k) then look r
4190 :     else true
4191 :     in look t
4192 :     end
4193 :    
4194 :     fun find(key,t) =
4195 :     let fun look EMPTY = NONE
4196 :     | look (TREE(k,_,l,r)) =
4197 :     if elem_gt(k,key) then look l
4198 :     else if elem_gt(key,k) then look r
4199 :     else SOME k
4200 :     in look t
4201 :     end
4202 :    
4203 :     fun revfold f t start =
4204 :     let fun scan (EMPTY,value) = value
4205 :     | scan (TREE(k,_,l,r),value) = scan(r,f(k,scan(l,value)))
4206 :     in scan(t,start)
4207 :     end
4208 :    
4209 :     fun fold f t start =
4210 :     let fun scan(EMPTY,value) = value
4211 :     | scan(TREE(k,_,l,r),value) = scan(l,f(k,scan(r,value)))
4212 :     in scan(t,start)
4213 :     end
4214 :    
4215 :     fun app f t =
4216 :     let fun scan EMPTY = ()
4217 :     | scan(TREE(k,_,l,r)) = (scan l; f k; scan r)
4218 :     in scan t
4219 :     end
4220 :    
4221 :    
4222 :     fun set_eq (tree1 as (TREE _),tree2 as (TREE _)) =
4223 :     let datatype pos = L | R | M
4224 :     exception Done
4225 :     fun getvalue(stack as ((a,position)::b)) =
4226 :     (case a
4227 :     of (TREE(k,_,l,r)) =>
4228 :     (case position
4229 :     of L => getvalue ((l,L)::(a,M)::b)
4230 :     | M => (k,case r of EMPTY => b | _ => (a,R)::b)
4231 :     | R => getvalue ((r,L)::b)
4232 :     )
4233 :     | EMPTY => getvalue b
4234 :     )
4235 :     | getvalue(nil) = raise Done
4236 :     fun f (nil,nil) = true
4237 :     | f (s1 as (_ :: _),s2 as (_ :: _ )) =
4238 :     let val (v1,news1) = getvalue s1
4239 :     and (v2,news2) = getvalue s2
4240 :     in (elem_eq(v1,v2)) andalso f(news1,news2)
4241 :     end
4242 :     | f _ = false
4243 :     in f ((tree1,L)::nil,(tree2,L)::nil) handle Done => false
4244 :     end
4245 :     | set_eq (EMPTY,EMPTY) = true
4246 :     | set_eq _ = false
4247 :    
4248 :    
4249 :     fun set_gt (tree1,tree2) =
4250 :     let datatype pos = L | R | M
4251 :     exception Done
4252 :     fun getvalue(stack as ((a,position)::b)) =
4253 :     (case a
4254 :     of (TREE(k,_,l,r)) =>
4255 :     (case position
4256 :     of L => getvalue ((l,L)::(a,M)::b)
4257 :     | M => (k,case r of EMPTY => b | _ => (a,R)::b)
4258 :     | R => getvalue ((r,L)::b)
4259 :     )
4260 :     | EMPTY => getvalue b
4261 :     )
4262 :     | getvalue(nil) = raise Done
4263 :     fun f (nil,nil) = false
4264 :     | f (s1 as (_ :: _),s2 as (_ :: _ )) =
4265 :     let val (v1,news1) = getvalue s1
4266 :     and (v2,news2) = getvalue s2
4267 :     in (elem_gt(v1,v2)) orelse (elem_eq(v1,v2) andalso f(news1,news2))
4268 :     end
4269 :     | f (_,nil) = true
4270 :     | f (nil,_) = false
4271 :     in f ((tree1,L)::nil,(tree2,L)::nil) handle Done => false
4272 :     end
4273 :    
4274 :     fun is_empty S = (let val _ = select_arb S in false end
4275 :     handle Select_arb => true)
4276 :    
4277 :     fun make_list S = fold (op ::) S nil
4278 :    
4279 :     fun make_set l = List.fold insert l empty
4280 :    
4281 :     fun partition F S = fold (fn (a,(Yes,No)) =>
4282 :     if F(a) then (insert(a,Yes),No)
4283 :     else (Yes,insert(a,No)))
4284 :     S (empty,empty)
4285 :    
4286 :     fun remove(X, XSet) =
4287 :     let val (YSet, _) =
4288 :     partition (fn a => not (elem_eq (X, a))) XSet
4289 :     in YSet
4290 :     end
4291 :    
4292 :     fun difference(Xs, Ys) =
4293 :     fold (fn (p as (a,Xs')) =>
4294 :     if exists(a,Ys) then Xs' else insert p)
4295 :     Xs empty
4296 :    
4297 :     fun singleton X = insert(X,empty)
4298 :    
4299 :     fun card(S) = fold (fn (_,count) => count+1) S 0
4300 :    
4301 :     fun union(Xs,Ys)= fold insert Ys Xs
4302 :    
4303 :     local
4304 :     fun closure'(from, f, result) =
4305 :     if is_empty from then result
4306 :     else
4307 :     let val (more,result) =
4308 :     fold (fn (a,(more',result')) =>
4309 :     let val more = f a
4310 :     val new = difference(more,result)
4311 :     in (union(more',new),union(result',new))
4312 :     end) from
4313 :     (empty,result)
4314 :     in closure'(more,f,result)
4315 :     end
4316 :     in
4317 :     fun closure(start, f) = closure'(start, f, start)
4318 :     end
4319 :     end
4320 :     end
4321 :    
4322 :    
4323 :     functor Table (B : sig type key
4324 :     val gt : (key * key) -> bool
4325 :     end
4326 :     ) : TABLE =
4327 :     struct
4328 :    
4329 :     datatype Color = RED | BLACK
4330 :     type key = B.key
4331 :    
4332 :     abstype 'a table = EMPTY
4333 :     | TREE of ((B.key * 'a ) * Color * 'a table * 'a table)
4334 :     with
4335 :    
4336 :     val empty = EMPTY
4337 :    
4338 :     fun insert(elem as (key,data),t) =
4339 :     let val key_gt = fn (a,_) => B.gt(key,a)
4340 :     val key_lt = fn (a,_) => B.gt(a,key)
4341 :     fun f EMPTY = TREE(elem,RED,EMPTY,EMPTY)
4342 :     | f (TREE(k,BLACK,l,r)) =
4343 :     if key_gt k
4344 :     then case f r
4345 :     of r as TREE(rk,RED, rl as TREE(rlk,RED,rll,rlr),rr) =>
4346 :     (case l
4347 :     of TREE(lk,RED,ll,lr) =>
4348 :     TREE(k,RED,TREE(lk,BLACK,ll,lr),
4349 :     TREE(rk,BLACK,rl,rr))
4350 :     | _ => TREE(rlk,BLACK,TREE(k,RED,l,rll),
4351 :     TREE(rk,RED,rlr,rr)))
4352 :     | r as TREE(rk,RED,rl, rr as TREE(rrk,RED,rrl,rrr)) =>
4353 :     (case l
4354 :     of TREE(lk,RED,ll,lr) =>
4355 :     TREE(k,RED,TREE(lk,BLACK,ll,lr),
4356 :     TREE(rk,BLACK,rl,rr))
4357 :     | _ => TREE(rk,BLACK,TREE(k,RED,l,rl),rr))
4358 :     | r => TREE(k,BLACK,l,r)
4359 :     else if key_lt k
4360 :     then case f l
4361 :     of l as TREE(lk,RED,ll, lr as TREE(lrk,RED,lrl,lrr)) =>
4362 :     (case r
4363 :     of TREE(rk,RED,rl,rr) =>
4364 :     TREE(k,RED,TREE(lk,BLACK,ll,lr),
4365 :     TREE(rk,BLACK,rl,rr))
4366 :     | _ => TREE(lrk,BLACK,TREE(lk,RED,ll,lrl),
4367 :     TREE(k,RED,lrr,r)))
4368 :     | l as TREE(lk,RED, ll as TREE(llk,RED,lll,llr), lr) =>
4369 :     (case r
4370 :     of TREE(rk,RED,rl,rr) =>
4371 :     TREE(k,RED,TREE(lk,BLACK,ll,lr),
4372 :     TREE(rk,BLACK,rl,rr))
4373 :     | _ => TREE(lk,BLACK,ll,TREE(k,RED,lr,r)))
4374 :     | l => TREE(k,BLACK,l,r)
4375 :     else TREE(elem,BLACK,l,r)
4376 :     | f (TREE(k,RED,l,r)) =
4377 :     if key_gt k then TREE(k,RED,l, f r)
4378 :     else if key_lt k then TREE(k,RED, f l, r)
4379 :     else TREE(elem,RED,l,r)
4380 :     in case f t
4381 :     of TREE(k,RED, l as TREE(_,RED,_,_), r) => TREE(k,BLACK,l,r)
4382 :     | TREE(k,RED, l, r as TREE(_,RED,_,_)) => TREE(k,BLACK,l,r)
4383 :     | t => t
4384 :     end
4385 :    
4386 :     fun exists(key,t) =
4387 :     let fun look EMPTY = false
4388 :     | look (TREE((k,_),_,l,r)) =
4389 :     if B.gt(k,key) then look l
4390 :     else if B.gt(key,k) then look r
4391 :     else true
4392 :     in look t
4393 :     end
4394 :    
4395 :     fun find(key,t) =
4396 :     let fun look EMPTY = NONE
4397 :     | look (TREE((k,data),_,l,r)) =
4398 :     if B.gt(k,key) then look l
4399 :     else if B.gt(key,k) then look r
4400 :     else SOME data
4401 :     in look t
4402 :     end
4403 :    
4404 :     fun fold f t start =
4405 :     let fun scan(EMPTY,value) = value
4406 :     | scan(TREE(k,_,l,r),value) = scan(l,f(k,scan(r,value)))
4407 :     in scan(t,start)
4408 :     end
4409 :    
4410 :     fun make_table l = List.fold insert l empty
4411 :    
4412 :     fun size S = fold (fn (_,count) => count+1) S 0
4413 :    
4414 :     fun make_list table = fold (op ::) table nil
4415 :    
4416 :     end
4417 :     end;
4418 :    
4419 :     functor Hash(B : sig type elem
4420 :     val gt : elem * elem -> bool
4421 :     end) : HASH =
4422 :     struct
4423 :     type elem=B.elem
4424 :     structure HashTable = Table(type key=B.elem
4425 :     val gt = B.gt)
4426 :    
4427 :     type table = {count : int, table : int HashTable.table}
4428 :    
4429 :     val empty = {count=0,table=HashTable.empty}
4430 :     val size = fn {count,table} => count
4431 :     val add = fn (e,{count,table}) =>
4432 :     {count=count+1,table=HashTable.insert((e,count),table)}
4433 :     val find = fn (e,{table,count}) => HashTable.find(e,table)
4434 :     val exists = fn (e,{table,count}) => HashTable.exists(e,table)
4435 :     end;
4436 :    
4437 :     functor Interface () : INTERFACE =
4438 :     struct
4439 :    
4440 :     type pos = int
4441 :     val line = ref 0
4442 :     fun init_line () = (line := 0)
4443 :     fun next_line () = (line := !line + 1)
4444 :     fun error (errmsg,line:pos,_) =
4445 :     output (std_out, ("Line " ^ (makestring line) ^ ": " ^ errmsg ^ "\n"))
4446 :    
4447 :     end (* functor INTERFACE *)
4448 :     functor Globals(
4449 :     structure Wr: WR
4450 :     structure Pp: PP
4451 :     structure WrMgt: WRMGT
4452 :     structure ListUtils: LISTUTILS
4453 :     structure StringUtils: STRINGUTILS
4454 :     structure DebugUtils: DEBUGUTILS
4455 :     structure Id: ID
4456 :     structure Registry: REGISTRY
4457 :     sharing Pp.Wr = Wr
4458 :     and WrMgt.Pp = Pp
4459 :     and type Registry.registeredtype = bool
4460 :     ) : GLOBALS
4461 :     = struct
4462 :    
4463 :     structure Wr = Wr;
4464 :     open Wr;
4465 :    
4466 :     structure Pp = Pp;
4467 :     open Pp;
4468 :    
4469 :     structure WrMgt = WrMgt;
4470 :     open WrMgt;
4471 :    
4472 :     structure Id = Id;
4473 :    
4474 :     structure Registry = Registry
4475 :    
4476 :     open ListUtils
4477 :     open StringUtils
4478 :     open DebugUtils
4479 :     open Registry
4480 :    
4481 :     exception CantHappen
4482 :    
4483 :     end
4484 :    
4485 :     signature TRMPVT = sig
4486 :    
4487 :     structure Globals: GLOBALS
4488 :     structure Typ: TYPPVT
4489 :     sharing Typ.Globals = Globals
4490 :     open Globals
4491 :    
4492 :     datatype pretrm =
4493 :     PREVAR of Id.T
4494 :     | PREABS of Id.T * Typ.pretyp * pretrm
4495 :     | PREAPP of pretrm * pretrm
4496 :     | PRETABS of Id.T * Typ.pretyp * pretrm
4497 :     | PRETAPP of pretrm * Typ.pretyp
4498 :     | PREFOR of Id.T * (Typ.pretyp list) * pretrm
4499 :    
4500 :     datatype T =
4501 :     VAR of unit * int
4502 :     | ABS of {name:Id.T} * Typ.T * T
4503 :     | APP of unit * T * T
4504 :     | TABS of {name:Id.T} * Typ.T * T
4505 :     | TAPP of unit * T * Typ.T
4506 :     | FOR of {name:Id.T} * (Typ.T list) * T
4507 :    
4508 :     exception UnknownId of string
4509 :     val debruijnify: Typ.tenv -> pretrm -> T
4510 :    
4511 :     val prt: Pp.Pp -> Typ.tenv -> T -> unit
4512 :    
4513 :     end
4514 :    
4515 :     functor DebugUtils(
4516 :     structure WrMgt: WRMGT
4517 :     ) : DEBUGUTILS = struct
4518 :    
4519 :     open WrMgt
4520 :     open Pp;
4521 :    
4522 :     val level = ref(0);
4523 :    
4524 :     (* $$$ belongs in globals: *)
4525 :     fun unwind_protect f cleanup =
4526 :     (f())
4527 :     handle e => (cleanup(); raise e)
4528 :    
4529 :     fun do_wrap pp name f pbefore pafter =
4530 :     (pwrite pp "[";
4531 :     setb pp;
4532 :     pwrite pp (makestring (!level));
4533 :     pwrite pp "] ";
4534 :     pwrite pp name;
4535 :     pwrite pp "? ";
4536 :     pbefore();
4537 :     pwrite pp "\n";
4538 :     level := (!level) + 1;
4539 :     let val result = unwind_protect
4540 :     f
4541 :     (fn () => level := (!level) - 1)
4542 :     in
4543 :     level := (!level) - 1;
4544 :     break pp true ~3;
4545 :     pwrite pp " [";
4546 :     pwrite pp (makestring (!level));
4547 :     pwrite pp "] ";
4548 :     pwrite pp name;
4549 :     pwrite pp ": ";
4550 :     pafter(result);
4551 :     pwrite pp "\n";
4552 :     endb pp;
4553 :     result
4554 :     end
4555 :     )
4556 :    
4557 :     fun wrap DEBUG name f pbefore pafter =
4558 :     if (not (!DEBUG))
4559 :     then f()
4560 :     else do_wrap (stdpp()) name f pbefore pafter;
4561 :    
4562 :     end
4563 :     functor Trm(
4564 :     structure Globals: GLOBALS
4565 :     structure Typ: TYPPVT
4566 :     sharing Typ.Globals = Globals
4567 :     ) : TRMPVT
4568 :     = struct
4569 :    
4570 :     structure Globals = Globals
4571 :     structure Typ = Typ
4572 :     open Globals
4573 :     open Typ
4574 :     open Pp
4575 :    
4576 :     datatype pretrm =
4577 :     PREVAR of Id.T
4578 :     | PREABS of Id.T * pretyp * pretrm
4579 :     | PREAPP of pretrm * pretrm
4580 :     | PRETABS of Id.T * pretyp * pretrm
4581 :     | PRETAPP of pretrm * pretyp
4582 :     | PREFOR of Id.T * (pretyp list) * pretrm
4583 :    
4584 :     datatype T =
4585 :     VAR of unit * int
4586 :     | ABS of {name:Id.T} * Typ.T * T
4587 :     | APP of unit * T * T
4588 :     | TABS of {name:Id.T} * Typ.T * T
4589 :     | TAPP of unit * T * Typ.T
4590 :     | FOR of {name:Id.T} * (Typ.T list) * T
4591 :    
4592 :     fun debruijnify te (PREVAR i) =
4593 :     VAR((), index te i)
4594 :     | debruijnify te (PREABS(i,ptyp,ptrm)) =
4595 :     ABS({name=i}, Typ.debruijnify te ptyp,
4596 :     debruijnify (push_binding te i NS) ptrm)
4597 :     | debruijnify te (PREAPP(ptrm1,ptrm2)) =
4598 :     APP((), debruijnify te ptrm1, debruijnify te ptrm2)
4599 :     | debruijnify te (PRETABS(i,ptyp,ptrm)) =
4600 :     TABS({name=i}, Typ.debruijnify te ptyp,
4601 :     debruijnify (push_bound te i NS) ptrm)
4602 :     | debruijnify te (PRETAPP(ptrm,ptyp)) =
4603 :     TAPP((), debruijnify te ptrm, Typ.debruijnify te ptyp)
4604 :     | debruijnify te (PREFOR(i,ptyps,ptrm)) =
4605 :     FOR({name=i}, map (fn pt => Typ.debruijnify te pt) ptyps,
4606 :     debruijnify (push_bound te i NS) ptrm)
4607 :    
4608 :     fun prt pp te trm =
4609 :     let fun p te (VAR(_,i)) =
4610 :     Pp.pwrite pp (Id.tostr (lookup_name te i))
4611 :     | p te (ABS({name=i},t,body)) =
4612 :     (Pp.pwrite pp "(\\";
4613 :     Pp.pwrite pp (Id.tostr i);
4614 :     Pp.pwrite pp ":";
4615 :     Typ.prt pp te t;
4616 :     Pp.pwrite pp ". ";
4617 :     p (push_binding te i t) body;
4618 :     Pp.pwrite pp ")")