Mercurial > urweb
comparison src/expl_util.sml @ 191:aa54250f58ac
Parametrized datatypes through explify
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 08 Aug 2008 10:28:32 -0400 |
parents | 8e9f97508f0d |
children | ab86aa858e6c |
comparison
equal
deleted
inserted
replaced
190:3eb53c957d10 | 191:aa54250f58ac |
---|---|
371 S.bind2 (kind k, | 371 S.bind2 (kind k, |
372 fn k' => | 372 fn k' => |
373 S.map2 (con ctx c, | 373 S.map2 (con ctx c, |
374 fn c' => | 374 fn c' => |
375 (SgiCon (x, n, k', c'), loc))) | 375 (SgiCon (x, n, k', c'), loc))) |
376 | SgiDatatype (x, n, xncs) => | 376 | SgiDatatype (x, n, xs, xncs) => |
377 S.map2 (ListUtil.mapfold (fn (x, n, c) => | 377 S.map2 (ListUtil.mapfold (fn (x, n, c) => |
378 case c of | 378 case c of |
379 NONE => S.return2 (x, n, c) | 379 NONE => S.return2 (x, n, c) |
380 | SOME c => | 380 | SOME c => |
381 S.map2 (con ctx c, | 381 S.map2 (con ctx c, |
382 fn c' => (x, n, SOME c'))) xncs, | 382 fn c' => (x, n, SOME c'))) xncs, |
383 fn xncs' => | 383 fn xncs' => |
384 (SgiDatatype (x, n, xncs'), loc)) | 384 (SgiDatatype (x, n, xs, xncs'), loc)) |
385 | SgiDatatypeImp (x, n, m1, ms, s, xncs) => | 385 | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) => |
386 S.map2 (ListUtil.mapfold (fn (x, n, c) => | 386 S.map2 (ListUtil.mapfold (fn (x, n, c) => |
387 case c of | 387 case c of |
388 NONE => S.return2 (x, n, c) | 388 NONE => S.return2 (x, n, c) |
389 | SOME c => | 389 | SOME c => |
390 S.map2 (con ctx c, | 390 S.map2 (con ctx c, |
391 fn c' => (x, n, SOME c'))) xncs, | 391 fn c' => (x, n, SOME c'))) xncs, |
392 fn xncs' => | 392 fn xncs' => |
393 (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc)) | 393 (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc)) |
394 | SgiVal (x, n, c) => | 394 | SgiVal (x, n, c) => |
395 S.map2 (con ctx c, | 395 S.map2 (con ctx c, |
396 fn c' => | 396 fn c' => |
397 (SgiVal (x, n, c'), loc)) | 397 (SgiVal (x, n, c'), loc)) |
398 | SgiStr (x, n, s) => | 398 | SgiStr (x, n, s) => |
414 (case #1 si of | 414 (case #1 si of |
415 SgiConAbs (x, _, k) => | 415 SgiConAbs (x, _, k) => |
416 bind (ctx, NamedC (x, k)) | 416 bind (ctx, NamedC (x, k)) |
417 | SgiCon (x, _, k, _) => | 417 | SgiCon (x, _, k, _) => |
418 bind (ctx, NamedC (x, k)) | 418 bind (ctx, NamedC (x, k)) |
419 | SgiDatatype (x, n, xncs) => | 419 | SgiDatatype (x, n, _, xncs) => |
420 bind (ctx, NamedC (x, (KType, loc))) | 420 bind (ctx, NamedC (x, (KType, loc))) |
421 | SgiDatatypeImp (x, _, _, _, _, _) => | 421 | SgiDatatypeImp (x, _, _, _, _, _, _) => |
422 bind (ctx, NamedC (x, (KType, loc))) | 422 bind (ctx, NamedC (x, (KType, loc))) |
423 | SgiVal _ => ctx | 423 | SgiVal _ => ctx |
424 | SgiStr (x, _, sgn) => | 424 | SgiStr (x, _, sgn) => |
425 bind (ctx, Str (x, sgn)) | 425 bind (ctx, Str (x, sgn)) |
426 | SgiSgn (x, _, sgn) => | 426 | SgiSgn (x, _, sgn) => |