comparison src/expl_util.sml @ 460:d34834af4512

Cookies through explify
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 10:43:48 -0500
parents 787d4931fb07
children ae03d09043c1
comparison
equal deleted inserted replaced
459:f542bc3133dc 460:d34834af4512
430 (SgiStr (x, n, s'), loc)) 430 (SgiStr (x, n, s'), loc))
431 | SgiSgn (x, n, s) => 431 | SgiSgn (x, n, s) =>
432 S.map2 (sg ctx s, 432 S.map2 (sg ctx s,
433 fn s' => 433 fn s' =>
434 (SgiSgn (x, n, s'), loc)) 434 (SgiSgn (x, n, s'), loc))
435 | SgiTable (tn, x, n, c) =>
436 S.map2 (con ctx c,
437 fn c' =>
438 (SgiTable (tn, x, n, c'), loc))
439 | SgiSequence _ => S.return2 siAll
440 435
441 and sg ctx s acc = 436 and sg ctx s acc =
442 S.bindP (sg' ctx s acc, sgn ctx) 437 S.bindP (sg' ctx s acc, sgn ctx)
443 438
444 and sg' ctx (sAll as (s, loc)) = 439 and sg' ctx (sAll as (s, loc)) =
456 bind (ctx, NamedC (x, (KType, loc))) 451 bind (ctx, NamedC (x, (KType, loc)))
457 | SgiVal _ => ctx 452 | SgiVal _ => ctx
458 | SgiStr (x, _, sgn) => 453 | SgiStr (x, _, sgn) =>
459 bind (ctx, Str (x, sgn)) 454 bind (ctx, Str (x, sgn))
460 | SgiSgn (x, _, sgn) => 455 | SgiSgn (x, _, sgn) =>
461 bind (ctx, Sgn (x, sgn)) 456 bind (ctx, Sgn (x, sgn)),
462 | SgiTable _ => ctx
463 | SgiSequence _ => ctx,
464 sgi ctx si)) ctx sgis, 457 sgi ctx si)) ctx sgis,
465 fn sgis' => 458 fn sgis' =>
466 (SgnConst sgis', loc)) 459 (SgnConst sgis', loc))
467 460
468 | SgnVar _ => S.return2 sAll 461 | SgnVar _ => S.return2 sAll