Mercurial > urweb

comparison src/expl_util.sml @ 162:06a98129b23f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)),