Mercurial > urweb
comparison src/expl_print.sml @ 806:0e554bfd6d6a
Mutual datatypes through Corify
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 16 May 2009 15:22:05 -0400 |
parents | 6271f0e3c272 |
children | b2311dfb3158 |
comparison
equal
deleted
inserted
replaced
805:e2780d2f4afc | 806:0e554bfd6d6a |
---|---|
458 let | 458 let |
459 val k = (KType, ErrorMsg.dummySpan) | 459 val k = (KType, ErrorMsg.dummySpan) |
460 val env = E.pushCNamed env x n k NONE | 460 val env = E.pushCNamed env x n k NONE |
461 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs | 461 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs |
462 in | 462 in |
463 box [string "datatype", | 463 box [string x, |
464 space, | |
465 string x, | |
466 p_list_sep (box []) (fn x => box [space, string x]) xs, | 464 p_list_sep (box []) (fn x => box [space, string x]) xs, |
467 space, | 465 space, |
468 string "=", | 466 string "=", |
469 space, | 467 space, |
470 p_list_sep (box [space, string "|", space]) | 468 p_list_sep (box [space, string "|", space]) |
473 | (x, n, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n)) | 471 | (x, n, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n)) |
474 else string x, space, string "of", space, p_con env t]) | 472 else string x, space, string "of", space, p_con env t]) |
475 cons] | 473 cons] |
476 end | 474 end |
477 | 475 |
478 fun p_sgn_item env (sgi, _) = | 476 fun p_sgn_item env (sgiAll as (sgi, _)) = |
479 case sgi of | 477 case sgi of |
480 SgiConAbs (x, n, k) => box [string "con", | 478 SgiConAbs (x, n, k) => box [string "con", |
481 space, | 479 space, |
482 p_named x n, | 480 p_named x n, |
483 space, | 481 space, |
493 p_kind env k, | 491 p_kind env k, |
494 space, | 492 space, |
495 string "=", | 493 string "=", |
496 space, | 494 space, |
497 p_con env c] | 495 p_con env c] |
498 | SgiDatatype x => p_datatype env x | 496 | SgiDatatype x => box [string "datatype", |
497 space, | |
498 p_list_sep (box [space, string "and", space]) (p_datatype (E.sgiBinds env sgiAll)) x] | |
499 | SgiDatatypeImp (x, _, m1, ms, x', _, _) => | 499 | SgiDatatypeImp (x, _, m1, ms, x', _, _) => |
500 let | 500 let |
501 val m1x = #1 (E.lookupStrNamed env m1) | 501 val m1x = #1 (E.lookupStrNamed env m1) |
502 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 | 502 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 |
503 in | 503 in |
607 p_kind env k, | 607 p_kind env k, |
608 space, | 608 space, |
609 string "=", | 609 string "=", |
610 space, | 610 space, |
611 p_con env c] | 611 p_con env c] |
612 | DDatatype x => p_datatype env x | 612 | DDatatype x => box [string "datatype", |
613 space, | |
614 p_list_sep (box [space, string "and", space]) (p_datatype (E.declBinds env dAll)) x] | |
613 | DDatatypeImp (x, _, m1, ms, x', _, _) => | 615 | DDatatypeImp (x, _, m1, ms, x', _, _) => |
614 let | 616 let |
615 val m1x = #1 (E.lookupStrNamed env m1) | 617 val m1x = #1 (E.lookupStrNamed env m1) |
616 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 | 618 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 |
617 in | 619 in |