Mercurial > urweb
comparison src/expl_util.sml @ 162:06a98129b23f
Add datatype import constructor annotations; datatypes through explify
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 29 Jul 2008 12:30:04 -0400 |
parents | 7420fa18d657 |
children | 33d4a8eea484 |
comparison
equal
deleted
inserted
replaced
161:a5ae7b3e37a4 | 162:06a98129b23f |
---|---|
340 val kind = Kind.mapfold kind | 340 val kind = Kind.mapfold kind |
341 | 341 |
342 fun sgi ctx si acc = | 342 fun sgi ctx si acc = |
343 S.bindP (sgi' ctx si acc, sgn_item ctx) | 343 S.bindP (sgi' ctx si acc, sgn_item ctx) |
344 | 344 |
345 and sgi' ctx (si, loc) = | 345 and sgi' ctx (siAll as (si, loc)) = |
346 case si of | 346 case si of |
347 SgiConAbs (x, n, k) => | 347 SgiConAbs (x, n, k) => |
348 S.map2 (kind k, | 348 S.map2 (kind k, |
349 fn k' => | 349 fn k' => |
350 (SgiConAbs (x, n, k'), loc)) | 350 (SgiConAbs (x, n, k'), loc)) |
352 S.bind2 (kind k, | 352 S.bind2 (kind k, |
353 fn k' => | 353 fn k' => |
354 S.map2 (con ctx c, | 354 S.map2 (con ctx c, |
355 fn c' => | 355 fn c' => |
356 (SgiCon (x, n, k', c'), loc))) | 356 (SgiCon (x, n, k', c'), loc))) |
357 | SgiDatatype (x, n, xncs) => | |
358 S.map2 (ListUtil.mapfold (fn (x, n, c) => | |
359 case c of | |
360 NONE => S.return2 (x, n, c) | |
361 | SOME c => | |
362 S.map2 (con ctx c, | |
363 fn c' => (x, n, SOME c'))) xncs, | |
364 fn xncs' => | |
365 (SgiDatatype (x, n, xncs'), loc)) | |
366 | SgiDatatypeImp (x, n, m1, ms, s, xncs) => | |
367 S.map2 (ListUtil.mapfold (fn (x, n, c) => | |
368 case c of | |
369 NONE => S.return2 (x, n, c) | |
370 | SOME c => | |
371 S.map2 (con ctx c, | |
372 fn c' => (x, n, SOME c'))) xncs, | |
373 fn xncs' => | |
374 (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc)) | |
357 | SgiVal (x, n, c) => | 375 | SgiVal (x, n, c) => |
358 S.map2 (con ctx c, | 376 S.map2 (con ctx c, |
359 fn c' => | 377 fn c' => |
360 (SgiVal (x, n, c'), loc)) | 378 (SgiVal (x, n, c'), loc)) |
361 | SgiStr (x, n, s) => | 379 | SgiStr (x, n, s) => |
377 (case #1 si of | 395 (case #1 si of |
378 SgiConAbs (x, _, k) => | 396 SgiConAbs (x, _, k) => |
379 bind (ctx, NamedC (x, k)) | 397 bind (ctx, NamedC (x, k)) |
380 | SgiCon (x, _, k, _) => | 398 | SgiCon (x, _, k, _) => |
381 bind (ctx, NamedC (x, k)) | 399 bind (ctx, NamedC (x, k)) |
400 | SgiDatatype (x, n, xncs) => | |
401 bind (ctx, NamedC (x, (KType, loc))) | |
402 | SgiDatatypeImp (x, _, _, _, _, _) => | |
403 bind (ctx, NamedC (x, (KType, loc))) | |
382 | SgiVal _ => ctx | 404 | SgiVal _ => ctx |
383 | SgiStr (x, _, sgn) => | 405 | SgiStr (x, _, sgn) => |
384 bind (ctx, Str (x, sgn)) | 406 bind (ctx, Str (x, sgn)) |
385 | SgiSgn (x, _, sgn) => | 407 | SgiSgn (x, _, sgn) => |
386 bind (ctx, Sgn (x, sgn)), | 408 bind (ctx, Sgn (x, sgn)), |