Mercurial > urweb

comparison src/expl_print.sml @ 806:0e554bfd6d6a

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