comparison src/expl_util.sml @ 246:3aa010e97db9

Explify tables
author Adam Chlipala <adamc@hcoop.net>
date Sun, 31 Aug 2008 08:46:22 -0400
parents 0343557355fc
children e976b187d73a
comparison
equal deleted inserted replaced
245:1e24a3e6d614 246:3aa010e97db9
410 (SgiStr (x, n, s'), loc)) 410 (SgiStr (x, n, s'), loc))
411 | SgiSgn (x, n, s) => 411 | SgiSgn (x, n, s) =>
412 S.map2 (sg ctx s, 412 S.map2 (sg ctx s,
413 fn s' => 413 fn s' =>
414 (SgiSgn (x, n, s'), loc)) 414 (SgiSgn (x, n, s'), loc))
415 | SgiTable (tn, x, n, c) =>
416 S.map2 (con ctx c,
417 fn c' =>
418 (SgiTable (tn, x, n, c'), loc))
415 419
416 and sg ctx s acc = 420 and sg ctx s acc =
417 S.bindP (sg' ctx s acc, sgn ctx) 421 S.bindP (sg' ctx s acc, sgn ctx)
418 422
419 and sg' ctx (sAll as (s, loc)) = 423 and sg' ctx (sAll as (s, loc)) =
431 bind (ctx, NamedC (x, (KType, loc))) 435 bind (ctx, NamedC (x, (KType, loc)))
432 | SgiVal _ => ctx 436 | SgiVal _ => ctx
433 | SgiStr (x, _, sgn) => 437 | SgiStr (x, _, sgn) =>
434 bind (ctx, Str (x, sgn)) 438 bind (ctx, Str (x, sgn))
435 | SgiSgn (x, _, sgn) => 439 | SgiSgn (x, _, sgn) =>
436 bind (ctx, Sgn (x, sgn)), 440 bind (ctx, Sgn (x, sgn))
441 | SgiTable _ => ctx,
437 sgi ctx si)) ctx sgis, 442 sgi ctx si)) ctx sgis,
438 fn sgis' => 443 fn sgis' =>
439 (SgnConst sgis', loc)) 444 (SgnConst sgis', loc))
440 445
441 | SgnVar _ => S.return2 sAll 446 | SgnVar _ => S.return2 sAll