Mercurial > urweb

comparison src/elab_print.sml @ 805:e2780d2f4afc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mutual datatypes through Elaborate
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:14:17 -0400
parents 8688e01ae469
children 7f871c03e3a1
comparison
equal deleted inserted replaced
804:10fe57e4a8c2 805:e2780d2f4afc
484 let 484 let
485 val k = (KType, ErrorMsg.dummySpan) 485 val k = (KType, ErrorMsg.dummySpan)
486 val env = E.pushCNamedAs env x n k NONE 486 val env = E.pushCNamedAs env x n k NONE
487 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs 487 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
488 in 488 in
489 box [string "datatype", 489 box [string x,
490 space,
491 string x,
492 p_list_sep (box []) (fn x => box [space, string x]) xs, 490 p_list_sep (box []) (fn x => box [space, string x]) xs,
493 space, 491 space,
494 string "=", 492 string "=",
495 space, 493 space,
496 p_list_sep (box [space, string "|", space]) 494 p_list_sep (box [space, string "|", space])
505 string "__", 503 string "__",
506 string (Int.toString n)] 504 string (Int.toString n)]
507 else 505 else
508 string x 506 string x
509 507
510 fun p_sgn_item env (sgi, _) = 508 fun p_sgn_item env (sgiAll as (sgi, _)) =
511 case sgi of 509 case sgi of
512 SgiConAbs (x, n, k) => box [string "con", 510 SgiConAbs (x, n, k) => box [string "con",
513 space, 511 space,
514 p_named x n, 512 p_named x n,
515 space, 513 space,
525 p_kind env k, 523 p_kind env k,
526 space, 524 space,
527 string "=", 525 string "=",
528 space, 526 space,
529 p_con env c] 527 p_con env c]
530 | SgiDatatype x => p_datatype env x 528 | SgiDatatype x => box [string "datatype",
529 space,
530 p_list_sep (box [space, string "and", space]) (p_datatype (E.sgiBinds env sgiAll)) x]
531 | SgiDatatypeImp (x, _, m1, ms, x', _, _) => 531 | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
532 let 532 let
533 val m1x = #1 (E.lookupStrNamed env m1) 533 val m1x = #1 (E.lookupStrNamed env m1)
534 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 534 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
535 in 535 in
667 p_kind env k, 667 p_kind env k,
668 space, 668 space,
669 string "=", 669 string "=",
670 space, 670 space,
671 p_con env c] 671 p_con env c]
672 | DDatatype x => p_datatype env x 672 | DDatatype x => box [string "datatype",
673 space,
674 p_list_sep (box [space, string "and", space]) (p_datatype (E.declBinds env dAll)) x]
673 | DDatatypeImp (x, _, m1, ms, x', _, _) => 675 | DDatatypeImp (x, _, m1, ms, x', _, _) =>
674 let 676 let
675 val m1x = #1 (E.lookupStrNamed env m1) 677 val m1x = #1 (E.lookupStrNamed env m1)
676 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 678 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
677 in 679 in