refer to name spaces values instead of names;
authorwenzelm
Sat Jun 11 22:15:48 2005 +0200 (2005-06-11)
changeset 16364dc9f7066d80a
parent 16363 c686a606dfba
child 16365 838c65dad23a
refer to name spaces values instead of names;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOLCF/holcf_logic.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/display.ML
src/ZF/Tools/induct_tacs.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Jun 11 22:15:47 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Jun 11 22:15:48 2005 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4  
     1.5    fun print sg tab =
     1.6      Pretty.writeln (Pretty.strs ("datatypes:" ::
     1.7 -      map #1 (Sign.extern_table sg Sign.typeK tab)));
     1.8 +      map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
     1.9  end;
    1.10  
    1.11  structure DatatypesData = TheoryDataFun(DatatypesArgs);
    1.12 @@ -466,7 +466,7 @@
    1.13          (loose_bnos (strip_abs_body t))
    1.14        end;
    1.15      val cases = map (fn ((cname, dts), t) =>
    1.16 -      (Sign.extern sg Sign.constK cname,
    1.17 +      (Sign.extern_const sg cname,
    1.18         strip_abs (length dts) t, is_dependent (length dts) t))
    1.19        (constrs ~~ fs);
    1.20      fun count_cases (cs, (_, _, true)) = cs
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Jun 11 22:15:47 2005 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Jun 11 22:15:48 2005 +0200
     2.3 @@ -101,7 +101,8 @@
     2.4      (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
     2.5  
     2.6    fun print sg (tab, monos) =
     2.7 -    [Pretty.strs ("(co)inductives:" :: map #1 (Sign.extern_table sg Sign.constK tab)),
     2.8 +    [Pretty.strs ("(co)inductives:" ::
     2.9 +      map #1 (NameSpace.extern_table (Sign.const_space sg, tab))),
    2.10       Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
    2.11      |> Pretty.chunks |> Pretty.writeln;
    2.12  end;
     3.1 --- a/src/HOL/Tools/recdef_package.ML	Sat Jun 11 22:15:47 2005 +0200
     3.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat Jun 11 22:15:48 2005 +0200
     3.3 @@ -120,8 +120,8 @@
     3.4            Drule.merge_rules (wfs1, wfs2)));
     3.5  
     3.6    fun print sg (tab, hints) =
     3.7 -   (Pretty.strs ("recdefs:" :: map #1 (Sign.extern_table sg Sign.constK tab)) ::
     3.8 -     pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
     3.9 +    (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space sg, tab))) ::
    3.10 +      pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
    3.11  end;
    3.12  
    3.13  structure GlobalRecdefData = TheoryDataFun(GlobalRecdefArgs);
     4.1 --- a/src/HOL/Tools/record_package.ML	Sat Jun 11 22:15:47 2005 +0200
     4.2 +++ b/src/HOL/Tools/record_package.ML	Sat Jun 11 22:15:48 2005 +0200
     4.3 @@ -287,7 +287,7 @@
     4.4              [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
     4.5  
     4.6        fun pretty_field (c, T) = Pretty.block
     4.7 -        [Pretty.str (Sign.extern sg Sign.constK c), Pretty.str " ::",
     4.8 +        [Pretty.str (Sign.extern_const sg c), Pretty.str " ::",
     4.9            Pretty.brk 1, Pretty.quote (prt_typ T)];
    4.10  
    4.11        fun pretty_record (name, {args, parent, fields, ...}: record_info) =
    4.12 @@ -670,7 +670,7 @@
    4.13                       SOME flds 
    4.14                       => (let
    4.15                            val (f::fs) = but_last (map fst flds);
    4.16 -                          val flds' = Sign.extern sg Sign.constK f::map NameSpace.base fs; 
    4.17 +                          val flds' = Sign.extern_const sg f :: map NameSpace.base fs; 
    4.18                            val (args',more) = split_last args; 
    4.19                           in (flds'~~args')@field_lst more end
    4.20                           handle UnequalLengths => [("",t)])
    4.21 @@ -775,7 +775,7 @@
    4.22                             SOME (_,alphas) 
    4.23                             => (let
    4.24                                  val (f::fs) = but_last flds;
    4.25 -                                val flds' = apfst (Sign.extern sg Sign.constK) f
    4.26 +                                val flds' = apfst (Sign.extern_const sg) f
    4.27                                              ::map (apfst NameSpace.base) fs; 
    4.28                                  val (args',more) = split_last args; 
    4.29                                  val alphavars = map Type.varifyT (but_last alphas); 
     5.1 --- a/src/HOLCF/holcf_logic.ML	Sat Jun 11 22:15:47 2005 +0200
     5.2 +++ b/src/HOLCF/holcf_logic.ML	Sat Jun 11 22:15:48 2005 +0200
     5.3 @@ -47,7 +47,7 @@
     5.4  
     5.5  (*cfun, ssum, sprod, u, tr, one *)
     5.6  
     5.7 -local val intern = Sign.intern_tycon HOLCF_sg;
     5.8 +local val intern = Sign.intern_type HOLCF_sg;
     5.9  in
    5.10  val cfun_arrow = intern "->";
    5.11  val op   ->>  = mk_btyp cfun_arrow;
     6.1 --- a/src/Pure/axclass.ML	Sat Jun 11 22:15:47 2005 +0200
     6.2 +++ b/src/Pure/axclass.ML	Sat Jun 11 22:15:48 2005 +0200
     6.3 @@ -131,12 +131,9 @@
     6.4  
     6.5    fun print sg tab =
     6.6      let
     6.7 -      val ext_class = Sign.extern sg Sign.classK;
     6.8 -      val ext_thm = PureThy.extern_thm_sg sg;
     6.9 -
    6.10        fun pretty_class c cs = Pretty.block
    6.11 -        (Pretty.str (ext_class c) :: Pretty.str " <" :: Pretty.brk 1 ::
    6.12 -          Pretty.breaks (map (Pretty.str o ext_class) cs));
    6.13 +        (Pretty.str (Sign.extern_class sg c) :: Pretty.str " <" :: Pretty.brk 1 ::
    6.14 +          Pretty.breaks (map (Pretty.str o Sign.extern_class sg) cs));
    6.15  
    6.16        fun pretty_thms name thms = Pretty.big_list (name ^ ":")
    6.17          (map (Display.pretty_thm_sg sg) thms);
    6.18 @@ -282,7 +279,7 @@
    6.19  fun prep_arity prep_tycon prep_sort prep sg (t, Ss, x) =
    6.20    test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep sg x);
    6.21  
    6.22 -val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
    6.23 +val read_arity = prep_arity Sign.intern_type Sign.read_sort Sign.read_sort;
    6.24  val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
    6.25  
    6.26  
     7.1 --- a/src/Pure/codegen.ML	Sat Jun 11 22:15:47 2005 +0200
     7.2 +++ b/src/Pure/codegen.ML	Sat Jun 11 22:15:48 2005 +0200
     7.3 @@ -300,7 +300,7 @@
     7.4    let
     7.5      val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
     7.6        CodegenData.get thy;
     7.7 -    val tc = Sign.intern_tycon (sign_of thy) s
     7.8 +    val tc = Sign.intern_type (sign_of thy) s
     7.9    in
    7.10      (case assoc (types, tc) of
    7.11         NONE => CodegenData.put {codegens = codegens,
    7.12 @@ -342,11 +342,11 @@
    7.13    end;
    7.14  
    7.15  fun mk_const_id sg s =
    7.16 -  let val s' = mk_id (Sign.extern sg Sign.constK s)
    7.17 +  let val s' = mk_id (Sign.extern_const sg s)
    7.18    in if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' end;
    7.19  
    7.20  fun mk_type_id sg s =
    7.21 -  let val s' = mk_id (Sign.extern sg Sign.typeK s)
    7.22 +  let val s' = mk_id (Sign.extern_type sg s)
    7.23    in if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' end;
    7.24  
    7.25  fun rename_terms ts =
     8.1 --- a/src/Pure/display.ML	Sat Jun 11 22:15:47 2005 +0200
     8.2 +++ b/src/Pure/display.ML	Sat Jun 11 22:15:48 2005 +0200
     8.3 @@ -199,14 +199,14 @@
     8.4              prt_typ_no_tvars T, Pretty.str " ::", Pretty.brk 1, prt_sort S];
     8.5  
     8.6      val tfrees = map (fn v => TFree (v, []));
     8.7 -    fun pretty_type syn (t, Type.LogicalType n) =
     8.8 +    fun pretty_type syn (t, (Type.LogicalType n, _)) =
     8.9            if syn then NONE
    8.10            else SOME (prt_typ (Type (t, tfrees (Term.invent_names [] "'a" n))))
    8.11 -      | pretty_type syn (t, Type.Abbreviation (vs, U, syn')) =
    8.12 +      | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
    8.13            if syn <> syn' then NONE
    8.14            else SOME (Pretty.block
    8.15              [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
    8.16 -      | pretty_type syn (t, Type.Nonterminal) =
    8.17 +      | pretty_type syn (t, (Type.Nonterminal, _)) =
    8.18            if not syn then NONE
    8.19            else SOME (prt_typ (Type (t, [])));
    8.20  
    8.21 @@ -224,20 +224,20 @@
    8.22  
    8.23  
    8.24      val {sign = _, defs, axioms, oracles, parents = _, ancestors = _} = Theory.rep_theory thy;
    8.25 -    val {self = _, tsig, consts, naming, spaces = _, data} = Sign.rep_sg sg;
    8.26 +    val {self = _, tsig, consts, naming, data} = Sign.rep_sg sg;
    8.27      val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
    8.28  
    8.29 -    val tdecls = Symtab.dest types |> map (fn (t, (d, _)) =>
    8.30 -      (Sign.extern sg Sign.typeK t, (t, d))) |> Library.sort_wrt #1 |> map #2;
    8.31 -    val cnsts = Sign.extern_table sg Sign.constK consts;
    8.32 -    val finals = Sign.extern_table sg Sign.constK (Defs.finals defs);
    8.33 +    val clsses = NameSpace.extern_table (apsnd (Symtab.make o Graph.dest) classes);
    8.34 +    val tdecls = NameSpace.extern_table types;
    8.35 +    val cnsts = NameSpace.extern_table consts;
    8.36 +    val finals = NameSpace.extern_table (#1 consts, Defs.finals defs);
    8.37      val axms = NameSpace.extern_table axioms;
    8.38      val oras = NameSpace.extern_table oracles;
    8.39    in
    8.40      [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
    8.41        Pretty.strs ("data:" :: Sign.data_kinds data),
    8.42        Pretty.strs ["name prefix:", NameSpace.path_of naming],
    8.43 -      Pretty.big_list "classes:" (map pretty_classrel (Graph.dest classes)),
    8.44 +      Pretty.big_list "classes:" (map pretty_classrel clsses),
    8.45        pretty_default default,
    8.46        pretty_witness witness,
    8.47        Pretty.big_list "syntactic types:" (List.mapPartial (pretty_type true) tdecls),
     9.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat Jun 11 22:15:47 2005 +0200
     9.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sat Jun 11 22:15:48 2005 +0200
     9.3 @@ -42,7 +42,7 @@
     9.4  
     9.5    fun print sg tab =
     9.6      Pretty.writeln (Pretty.strs ("datatypes:" ::
     9.7 -      map #1 (Sign.extern_table sg Sign.typeK tab)));
     9.8 +      map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
     9.9    end;
    9.10  
    9.11  structure DatatypesData = TheoryDataFun(DatatypesArgs);