comparison src/elab_print.sml @ 563:44958d74c43f

Initial conversion to arbitrary-kind classes
author Adam Chlipala <adamc@hcoop.net>
date Fri, 19 Dec 2008 10:03:31 -0500
parents 1bbcc3345d12
children 8998114760c1
comparison
equal deleted inserted replaced
562:6daa59a55c43 563:44958d74c43f
532 p_con env c1, 532 p_con env c1,
533 space, 533 space,
534 string "~", 534 string "~",
535 space, 535 space,
536 p_con env c2] 536 p_con env c2]
537 | SgiClassAbs (x, n) => box [string "class", 537 | SgiClassAbs (x, n, k) => box [string "class",
538 space, 538 space,
539 p_named x n] 539 p_named x n,
540 | SgiClass (x, n, c) => box [string "class", 540 space,
541 space, 541 string "::",
542 p_named x n, 542 space,
543 space, 543 p_kind k]
544 string "=", 544 | SgiClass (x, n, k, c) => box [string "class",
545 space, 545 space,
546 p_con env c] 546 p_named x n,
547 space,
548 string "::",
549 space,
550 p_kind k,
551 space,
552 string "=",
553 space,
554 p_con env c]
547 555
548 and p_sgn env (sgn, _) = 556 and p_sgn env (sgn, _) =
549 case sgn of 557 case sgn of
550 SgnConst sgis => box [string "sig", 558 SgnConst sgis => box [string "sig",
551 newline, 559 newline,
703 space, 711 space,
704 p_con env c] 712 p_con env c]
705 | DSequence (_, x, n) => box [string "sequence", 713 | DSequence (_, x, n) => box [string "sequence",
706 space, 714 space,
707 p_named x n] 715 p_named x n]
708 | DClass (x, n, c) => box [string "class", 716 | DClass (x, n, k, c) => box [string "class",
709 space, 717 space,
710 p_named x n, 718 p_named x n,
711 space, 719 space,
712 string "=", 720 string "::",
713 space, 721 space,
714 p_con env c] 722 p_kind k,
723 space,
724 string "=",
725 space,
726 p_con env c]
715 | DDatabase s => box [string "database", 727 | DDatabase s => box [string "database",
716 space, 728 space,
717 string s] 729 string s]
718 | DCookie (_, x, n, c) => box [string "cookie", 730 | DCookie (_, x, n, c) => box [string "cookie",
719 space, 731 space,