eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
authorwenzelm
Sat Oct 24 19:20:03 2009 +0200 (2009-10-24 ago)
changeset 33092c859019d3ac5
parent 33091 d23e75d4f7da
child 33093 d010f61d3702
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
src/Pure/Isar/attrib.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/codegen.ML
src/Pure/consts.ML
src/Pure/display.ML
src/Pure/simplifier.ML
src/Pure/theory.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Oct 24 19:04:57 2009 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Oct 24 19:20:03 2009 +0200
     1.3 @@ -67,27 +67,25 @@
     1.4  
     1.5  structure Attributes = TheoryDataFun
     1.6  (
     1.7 -  type T = (((src -> attribute) * string) * stamp) NameSpace.table;
     1.8 +  type T = ((src -> attribute) * string) NameSpace.table;
     1.9    val empty = NameSpace.empty_table;
    1.10    val copy = I;
    1.11    val extend = I;
    1.12 -  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
    1.13 -    error ("Attempt to merge different versions of attribute " ^ quote dup);
    1.14 +  fun merge _ tables : T = NameSpace.merge_tables tables;
    1.15  );
    1.16  
    1.17  fun print_attributes thy =
    1.18    let
    1.19      val attribs = Attributes.get thy;
    1.20 -    fun prt_attr (name, ((_, comment), _)) = Pretty.block
    1.21 +    fun prt_attr (name, (_, comment)) = Pretty.block
    1.22        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.23    in
    1.24      [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
    1.25      |> Pretty.chunks |> Pretty.writeln
    1.26    end;
    1.27  
    1.28 -fun add_attribute name att comment thy = thy |> Attributes.map (fn atts =>
    1.29 -  #2 (NameSpace.define (Sign.naming_of thy) (name, ((att, comment), stamp ())) atts)
    1.30 -    handle Symtab.DUP dup => error ("Duplicate declaration of attribute " ^ quote dup));
    1.31 +fun add_attribute name att comment thy = thy
    1.32 +  |> Attributes.map (#2 o NameSpace.define true (Sign.naming_of thy) (name, (att, comment)));
    1.33  
    1.34  
    1.35  (* name space *)
    1.36 @@ -117,7 +115,7 @@
    1.37        let val ((name, _), pos) = Args.dest_src src in
    1.38          (case Symtab.lookup attrs name of
    1.39            NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
    1.40 -        | SOME ((att, _), _) => (Position.report (Markup.attribute name) pos; att src))
    1.41 +        | SOME (att, _) => (Position.report (Markup.attribute name) pos; att src))
    1.42        end;
    1.43    in attr end;
    1.44  
     2.1 --- a/src/Pure/Isar/locale.ML	Sat Oct 24 19:04:57 2009 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Sat Oct 24 19:20:03 2009 +0200
     2.3 @@ -143,7 +143,7 @@
     2.4    | NONE => error ("Unknown locale " ^ quote name));
     2.5  
     2.6  fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
     2.7 -  thy |> Locales.map (NameSpace.define (Sign.naming_of thy)
     2.8 +  thy |> Locales.map (NameSpace.define true (Sign.naming_of thy)
     2.9      (binding,
    2.10        mk_locale ((parameters, spec, intros, axioms),
    2.11          ((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes),
     3.1 --- a/src/Pure/Isar/method.ML	Sat Oct 24 19:04:57 2009 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Sat Oct 24 19:20:03 2009 +0200
     3.3 @@ -322,27 +322,25 @@
     3.4  
     3.5  structure Methods = TheoryDataFun
     3.6  (
     3.7 -  type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
     3.8 +  type T = ((src -> Proof.context -> method) * string) NameSpace.table;
     3.9    val empty = NameSpace.empty_table;
    3.10    val copy = I;
    3.11    val extend = I;
    3.12 -  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
    3.13 -    error ("Attempt to merge different versions of method " ^ quote dup);
    3.14 +  fun merge _ tables : T = NameSpace.merge_tables tables;
    3.15  );
    3.16  
    3.17  fun print_methods thy =
    3.18    let
    3.19      val meths = Methods.get thy;
    3.20 -    fun prt_meth (name, ((_, comment), _)) = Pretty.block
    3.21 +    fun prt_meth (name, (_, comment)) = Pretty.block
    3.22        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    3.23    in
    3.24      [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
    3.25      |> Pretty.chunks |> Pretty.writeln
    3.26    end;
    3.27  
    3.28 -fun add_method name meth comment thy = thy |> Methods.map (fn meths =>
    3.29 -  #2 (NameSpace.define (Sign.naming_of thy) (name, ((meth, comment), stamp ())) meths)
    3.30 -    handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup));
    3.31 +fun add_method name meth comment thy = thy
    3.32 +  |> Methods.map (#2 o NameSpace.define true (Sign.naming_of thy) (name, (meth, comment)));
    3.33  
    3.34  
    3.35  (* get methods *)
    3.36 @@ -357,7 +355,7 @@
    3.37        let val ((name, _), pos) = Args.dest_src src in
    3.38          (case Symtab.lookup meths name of
    3.39            NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
    3.40 -        | SOME ((mth, _), _) => (Position.report (Markup.method name) pos; mth src))
    3.41 +        | SOME (mth, _) => (Position.report (Markup.method name) pos; mth src))
    3.42        end;
    3.43    in meth end;
    3.44  
     4.1 --- a/src/Pure/codegen.ML	Sat Oct 24 19:04:57 2009 +0200
     4.2 +++ b/src/Pure/codegen.ML	Sat Oct 24 19:20:03 2009 +0200
     4.3 @@ -337,15 +337,16 @@
     4.4      val tc = Sign.intern_type thy s;
     4.5    in
     4.6      case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
     4.7 -      SOME ((Type.LogicalType i, _), _) =>
     4.8 +      SOME (Type.LogicalType i, _) =>
     4.9          if num_args_of (fst syn) > i then
    4.10            error ("More arguments than corresponding type constructor " ^ s)
    4.11 -        else (case AList.lookup (op =) types tc of
    4.12 -          NONE => CodegenData.put {codegens = codegens,
    4.13 -            tycodegens = tycodegens, consts = consts,
    4.14 -            types = (tc, syn) :: types,
    4.15 -            preprocs = preprocs, modules = modules} thy
    4.16 -        | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
    4.17 +        else
    4.18 +          (case AList.lookup (op =) types tc of
    4.19 +            NONE => CodegenData.put {codegens = codegens,
    4.20 +              tycodegens = tycodegens, consts = consts,
    4.21 +              types = (tc, syn) :: types,
    4.22 +              preprocs = preprocs, modules = modules} thy
    4.23 +          | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
    4.24      | _ => error ("Not a type constructor: " ^ s)
    4.25    end;
    4.26  
     5.1 --- a/src/Pure/consts.ML	Sat Oct 24 19:04:57 2009 +0200
     5.2 +++ b/src/Pure/consts.ML	Sat Oct 24 19:20:03 2009 +0200
     5.3 @@ -50,7 +50,7 @@
     5.4  type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
     5.5  
     5.6  datatype T = Consts of
     5.7 - {decls: ((decl * abbrev option) * serial) NameSpace.table,
     5.8 + {decls: (decl * abbrev option) NameSpace.table,
     5.9    constraints: typ Symtab.table,
    5.10    rev_abbrevs: (term * term) Item_Net.T Symtab.table};
    5.11  
    5.12 @@ -84,7 +84,7 @@
    5.13  
    5.14  fun dest (Consts {decls = (space, decls), constraints, ...}) =
    5.15   {constants = (space,
    5.16 -    Symtab.fold (fn (c, (({T, ...}, abbr), _)) =>
    5.17 +    Symtab.fold (fn (c, ({T, ...}, abbr)) =>
    5.18        Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty),
    5.19    constraints = (space, constraints)};
    5.20  
    5.21 @@ -93,7 +93,7 @@
    5.22  
    5.23  fun the_const (Consts {decls = (_, tab), ...}) c =
    5.24    (case Symtab.lookup tab c of
    5.25 -    SOME (decl, _) => decl
    5.26 +    SOME decl => decl
    5.27    | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], []));
    5.28  
    5.29  fun the_type consts c =
    5.30 @@ -221,13 +221,6 @@
    5.31  
    5.32  (** build consts **)
    5.33  
    5.34 -fun err_dup_const c =
    5.35 -  error ("Duplicate declaration of constant " ^ quote c);
    5.36 -
    5.37 -fun extend_decls naming decl tab = NameSpace.define naming decl tab
    5.38 -  handle Symtab.DUP c => err_dup_const c;
    5.39 -
    5.40 -
    5.41  (* name space *)
    5.42  
    5.43  fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) =>
    5.44 @@ -236,12 +229,13 @@
    5.45  
    5.46  (* declarations *)
    5.47  
    5.48 -fun declare authentic naming tags (b, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
    5.49 -  let
    5.50 -    val tags' = tags |> Position.default_properties (Position.thread_data ());
    5.51 -    val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
    5.52 -    val (_, decls') = decls |> extend_decls naming (b, ((decl, NONE), serial ()));
    5.53 -  in (decls', constraints, rev_abbrevs) end);
    5.54 +fun declare authentic naming tags (b, declT) =
    5.55 +  map_consts (fn (decls, constraints, rev_abbrevs) =>
    5.56 +    let
    5.57 +      val tags' = tags |> Position.default_properties (Position.thread_data ());
    5.58 +      val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
    5.59 +      val (_, decls') = decls |> NameSpace.define true naming (b, (decl, NONE));
    5.60 +    in (decls', constraints, rev_abbrevs) end);
    5.61  
    5.62  
    5.63  (* constraints *)
    5.64 @@ -278,7 +272,7 @@
    5.65      val force_expand = mode = PrintMode.internal;
    5.66  
    5.67      val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
    5.68 -      error ("Illegal schematic variables on rhs of abbreviation: " ^ Binding.str_of b);
    5.69 +      error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));
    5.70  
    5.71      val rhs = raw_rhs
    5.72        |> Term.map_types (Type.cert_typ tsig)
    5.73 @@ -294,7 +288,7 @@
    5.74          val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
    5.75          val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
    5.76          val (_, decls') = decls
    5.77 -          |> extend_decls naming (b, ((decl, SOME abbr), serial ()));
    5.78 +          |> NameSpace.define true naming (b, (decl, SOME abbr));
    5.79          val rev_abbrevs' = rev_abbrevs
    5.80            |> insert_abbrevs mode (rev_abbrev lhs rhs);
    5.81        in (decls', constraints, rev_abbrevs') end)
    5.82 @@ -319,8 +313,7 @@
    5.83     (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
    5.84      Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
    5.85    let
    5.86 -    val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
    5.87 -      handle Symtab.DUP c => err_dup_const c;
    5.88 +    val decls' = NameSpace.merge_tables (decls1, decls2);
    5.89      val constraints' = Symtab.join (K fst) (constraints1, constraints2);
    5.90      val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
    5.91    in make_consts (decls', constraints', rev_abbrevs') end;
     6.1 --- a/src/Pure/display.ML	Sat Oct 24 19:04:57 2009 +0200
     6.2 +++ b/src/Pure/display.ML	Sat Oct 24 19:20:03 2009 +0200
     6.3 @@ -146,14 +146,14 @@
     6.4        [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
     6.5  
     6.6      val tfrees = map (fn v => TFree (v, []));
     6.7 -    fun pretty_type syn (t, ((Type.LogicalType n, _), _)) =
     6.8 +    fun pretty_type syn (t, (Type.LogicalType n, _)) =
     6.9            if syn then NONE
    6.10            else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
    6.11 -      | pretty_type syn (t, ((Type.Abbreviation (vs, U, syn'), _), _)) =
    6.12 +      | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
    6.13            if syn <> syn' then NONE
    6.14            else SOME (Pretty.block
    6.15              [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
    6.16 -      | pretty_type syn (t, ((Type.Nonterminal, _), _)) =
    6.17 +      | pretty_type syn (t, (Type.Nonterminal, _)) =
    6.18            if not syn then NONE
    6.19            else SOME (prt_typ (Type (t, [])));
    6.20  
     7.1 --- a/src/Pure/simplifier.ML	Sat Oct 24 19:04:57 2009 +0200
     7.2 +++ b/src/Pure/simplifier.ML	Sat Oct 24 19:20:03 2009 +0200
     7.3 @@ -143,9 +143,6 @@
     7.4  
     7.5  (** named simprocs **)
     7.6  
     7.7 -fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name);
     7.8 -
     7.9 -
    7.10  (* data *)
    7.11  
    7.12  structure Simprocs = GenericDataFun
    7.13 @@ -153,8 +150,7 @@
    7.14    type T = simproc NameSpace.table;
    7.15    val empty = NameSpace.empty_table;
    7.16    val extend = I;
    7.17 -  fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
    7.18 -    handle Symtab.DUP dup => err_dup_simproc dup;
    7.19 +  fun merge _ simprocs = NameSpace.merge_tables simprocs;
    7.20  );
    7.21  
    7.22  
    7.23 @@ -201,9 +197,7 @@
    7.24          val b' = Morphism.binding phi b;
    7.25          val simproc' = morph_simproc phi simproc;
    7.26        in
    7.27 -        Simprocs.map (fn simprocs =>
    7.28 -          NameSpace.define naming (b', simproc') simprocs |> snd
    7.29 -            handle Symtab.DUP dup => err_dup_simproc dup)
    7.30 +        Simprocs.map (#2 o NameSpace.define true naming (b', simproc'))
    7.31          #> map_ss (fn ss => ss addsimprocs [simproc'])
    7.32        end)
    7.33    end;
     8.1 --- a/src/Pure/theory.ML	Sat Oct 24 19:04:57 2009 +0200
     8.2 +++ b/src/Pure/theory.ML	Sat Oct 24 19:20:03 2009 +0200
     8.3 @@ -86,8 +86,6 @@
     8.4  
     8.5  fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
     8.6  
     8.7 -fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
     8.8 -
     8.9  structure ThyData = TheoryDataFun
    8.10  (
    8.11    type T = thy;
    8.12 @@ -166,7 +164,7 @@
    8.13  
    8.14  fun read_axm thy (b, str) =
    8.15    cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
    8.16 -    cat_error msg ("The error(s) above occurred in axiom: " ^ quote (Binding.str_of b));
    8.17 +    cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
    8.18  
    8.19  
    8.20  (* add_axioms(_i) *)
    8.21 @@ -176,8 +174,7 @@
    8.22  fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
    8.23    let
    8.24      val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
    8.25 -    val axioms' = fold (snd oo NameSpace.define (Sign.naming_of thy)) axms axioms
    8.26 -      handle Symtab.DUP dup => err_dup_axm dup;
    8.27 +    val axioms' = fold (#2 oo NameSpace.define true (Sign.naming_of thy)) axms axioms;
    8.28    in axioms' end);
    8.29  
    8.30  in
     9.1 --- a/src/Pure/thm.ML	Sat Oct 24 19:04:57 2009 +0200
     9.2 +++ b/src/Pure/thm.ML	Sat Oct 24 19:20:03 2009 +0200
     9.3 @@ -1724,16 +1724,13 @@
     9.4  
     9.5  (* authentic derivation names *)
     9.6  
     9.7 -fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
     9.8 -
     9.9  structure Oracles = TheoryDataFun
    9.10  (
    9.11 -  type T = serial NameSpace.table;
    9.12 +  type T = unit NameSpace.table;
    9.13    val empty = NameSpace.empty_table;
    9.14    val copy = I;
    9.15    val extend = I;
    9.16 -  fun merge _ oracles : T = NameSpace.merge_tables (op =) oracles
    9.17 -    handle Symtab.DUP dup => err_dup_ora dup;
    9.18 +  fun merge _ oracles : T = NameSpace.merge_tables oracles;
    9.19  );
    9.20  
    9.21  val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
    9.22 @@ -1741,8 +1738,7 @@
    9.23  fun add_oracle (b, oracle) thy =
    9.24    let
    9.25      val naming = Sign.naming_of thy;
    9.26 -    val (name, tab') = NameSpace.define naming (b, serial ()) (Oracles.get thy)
    9.27 -      handle Symtab.DUP _ => err_dup_ora (Binding.str_of b);
    9.28 +    val (name, tab') = NameSpace.define true naming (b, ()) (Oracles.get thy);
    9.29      val thy' = Oracles.put tab' thy;
    9.30    in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
    9.31