adapted tsig/sg interface;
authorwenzelm
Fri May 21 21:28:14 2004 +0200 (2004-05-21)
changeset 14794751d5af6d91e
parent 14793 32d94d1e4842
child 14795 b702848de41f
adapted tsig/sg interface;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Fri May 21 21:28:01 2004 +0200
     1.2 +++ b/src/Pure/display.ML	Fri May 21 21:28:14 2004 +0200
     1.3 @@ -186,26 +186,24 @@
     1.4      fun prt_typ_no_tvars ty = Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)));
     1.5      fun prt_term t = Pretty.quote (Sign.pretty_term sg t);
     1.6  
     1.7 -    fun pretty_classes cs = Pretty.block
     1.8 -      (Pretty.breaks (Pretty.str "classes:" :: map prt_cls cs));
     1.9 -
    1.10 -    fun pretty_classrel (c, cs) = Pretty.block
    1.11 -      (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 ::
    1.12 -        Pretty.commas (map prt_cls cs));
    1.13 +    fun pretty_classrel (c, []) = prt_cls c
    1.14 +      | pretty_classrel (c, cs) = Pretty.block
    1.15 +          (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 ::
    1.16 +            Pretty.commas (map prt_cls cs));
    1.17  
    1.18      fun pretty_default S = Pretty.block
    1.19 -      [Pretty.str "default:", Pretty.brk 1, prt_sort S];
    1.20 +      [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
    1.21  
    1.22      fun pretty_ty (t, n) = Pretty.block
    1.23        [Pretty.str t, Pretty.brk 1, Pretty.str (string_of_int n)];
    1.24  
    1.25 -    fun pretty_log_types ts = Pretty.block
    1.26 -      (Pretty.breaks (Pretty.str "logical types:" :: map Pretty.str ts));
    1.27 -
    1.28      fun pretty_witness None = Pretty.str "universal non-emptiness witness: --"
    1.29        | pretty_witness (Some (T, S)) = Pretty.block
    1.30 -          [Pretty.str "universal non-emptiness witness:", Pretty.brk 1, prt_typ_no_tvars T,
    1.31 -            Pretty.brk 1, prt_sort S];
    1.32 +          [Pretty.str "universal non-emptiness witness:", Pretty.brk 1,
    1.33 +            prt_typ_no_tvars T, Pretty.str " ::", Pretty.brk 1, prt_sort S];
    1.34 +
    1.35 +    fun pretty_nonterminals ts = Pretty.block
    1.36 +      (Pretty.breaks (Pretty.str "syntactic types:" :: map Pretty.str ts));
    1.37  
    1.38      fun pretty_abbr (t, (vs, rhs)) = Pretty.block
    1.39        [prt_typ_no_tvars (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
    1.40 @@ -218,20 +216,23 @@
    1.41           (if null tys then [Pretty.str "<all instances>"]
    1.42  	  else Pretty.commas (map prt_typ_no_tvars tys)));
    1.43  
    1.44 -    fun pretty_const (c, ty) = Pretty.block
    1.45 +    fun pretty_const (c, (ty, _)) = Pretty.block
    1.46        [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    1.47  
    1.48      fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
    1.49  
    1.50  
    1.51 -    val {self = _, tsig, const_tab, path, spaces, data} = Sign.rep_sg sg;
    1.52 +    val {self = _, tsig, consts, path, spaces, data} = Sign.rep_sg sg;
    1.53      val {axioms, oracles, ...} = Theory.rep_theory thy;
    1.54      val spaces' = Library.sort_wrt fst spaces;
    1.55 -    val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} =
    1.56 -      Type.rep_tsig tsig;
    1.57 -    val finals = Symtab.dest (#final_consts (rep_theory thy));
    1.58 -    val tycons = Sign.cond_extern_table sg Sign.typeK type_tab;
    1.59 -    val consts = Sign.cond_extern_table sg Sign.constK const_tab;
    1.60 +    val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
    1.61 +    val tdecls = Symtab.dest types |>
    1.62 +      map (fn (t, (decl, _)) => (Sign.cond_extern sg Sign.typeK t, decl));
    1.63 +    val tycons = mapfilter (fn (t, Type.LogicalType n) => Some (t, n) | _ => None) tdecls;
    1.64 +    val abbrs = mapfilter (fn (t, Type.Abbreviation u) => Some (t, u) | _ => None) tdecls;
    1.65 +    val nonterminals = mapfilter (fn (t, Type.Nonterminal) => Some t | _ => None) tdecls;
    1.66 +    val finals = Symtab.dest (#final_consts (Theory.rep_theory thy));
    1.67 +    val cnsts = Sign.cond_extern_table sg Sign.constK consts;
    1.68      val axms = Sign.cond_extern_table sg Theory.axiomK axioms;
    1.69      val oras = Sign.cond_extern_table sg Theory.oracleK oracles;
    1.70    in
    1.71 @@ -239,15 +240,14 @@
    1.72        Pretty.strs ("data:" :: Sign.data_kinds data),
    1.73        Pretty.strs ["name prefix:", NameSpace.pack (if_none path ["-"])],
    1.74        Pretty.big_list "name spaces:" (map pretty_name_space spaces'),
    1.75 -      pretty_classes classes,
    1.76 -      Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)),
    1.77 +      Pretty.big_list "classes:" (map pretty_classrel (Graph.dest classes)),
    1.78        pretty_default default,
    1.79 -      pretty_log_types log_types,
    1.80 -      pretty_witness univ_witness,
    1.81 -      Pretty.big_list "type constructors:" (map pretty_ty tycons),
    1.82 -      Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)),
    1.83 +      pretty_witness witness,
    1.84 +      Pretty.big_list "logical type constructors:" (map pretty_ty tycons),
    1.85 +      Pretty.big_list "type abbreviations:" (map pretty_abbr abbrs),
    1.86 +      pretty_nonterminals nonterminals,
    1.87        Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))),
    1.88 -      Pretty.big_list "consts:" (map pretty_const consts),
    1.89 +      Pretty.big_list "consts:" (map pretty_const cnsts),
    1.90        Pretty.big_list "finals:" (map pretty_final finals),
    1.91        Pretty.big_list "axioms:" (map prt_axm axms),
    1.92        Pretty.strs ("oracles:" :: (map #1 oras))]