new tsig components;
authorwenzelm
Wed Sep 29 13:50:26 1999 +0200 (1999-09-29)
changeset 76354c1d2eb68db8
parent 7634 c326808da921
child 7636 102a4b6b83a6
new tsig components;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Wed Sep 29 13:49:49 1999 +0200
     1.2 +++ b/src/Pure/display.ML	Wed Sep 29 13:50:26 1999 +0200
     1.3 @@ -178,6 +178,13 @@
     1.4      fun pretty_ty (t, n) = Pretty.block
     1.5        [Pretty.str t, Pretty.spc 1, Pretty.str (string_of_int n)];
     1.6  
     1.7 +    fun pretty_log_types ts = Pretty.block
     1.8 +      (Pretty.breaks (Pretty.str "logical types:" :: map Pretty.str ts));
     1.9 +
    1.10 +    fun pretty_witness None = Pretty.str "universal non-emptiness witness: --"
    1.11 +      | pretty_witness (Some (T, S)) = Pretty.block
    1.12 +          [Pretty.str "universal non-emptiness witness:", Pretty.brk 1, prt_typ T, Pretty.brk 1, prt_sort S];
    1.13 +
    1.14      fun pretty_abbr (t, (vs, rhs)) = Pretty.block
    1.15        [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
    1.16          Pretty.str " =", Pretty.brk 1, prt_typ rhs];
    1.17 @@ -189,7 +196,7 @@
    1.18  
    1.19      val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg;
    1.20      val spaces' = Library.sort_wrt fst spaces;
    1.21 -    val {classes, classrel, default, tycons = type_tab, abbrs, arities} =
    1.22 +    val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} =
    1.23        Type.rep_tsig tsig;
    1.24      val tycons = Sign.cond_extern_table sg Sign.typeK type_tab;
    1.25      val consts = Sign.cond_extern_table sg Sign.constK const_tab;
    1.26 @@ -201,6 +208,8 @@
    1.27      Pretty.writeln (pretty_classes classes);
    1.28      Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)));
    1.29      Pretty.writeln (pretty_default default);
    1.30 +    Pretty.writeln (pretty_log_types log_types);
    1.31 +    Pretty.writeln (pretty_witness univ_witness);
    1.32      Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons));
    1.33      Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)));
    1.34      Pretty.writeln (Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))));