# HG changeset patch # User wenzelm # Date 1256404803 -7200 # Node ID c859019d3ac57d05d3992a9f0cc2fe34a935b803 # Parent d23e75d4f7daf8013a56edb781114c4b9e22057b eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; diff -r d23e75d4f7da -r c859019d3ac5 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sat Oct 24 19:04:57 2009 +0200 +++ b/src/Pure/Isar/attrib.ML Sat Oct 24 19:20:03 2009 +0200 @@ -67,27 +67,25 @@ structure Attributes = TheoryDataFun ( - type T = (((src -> attribute) * string) * stamp) NameSpace.table; + type T = ((src -> attribute) * string) NameSpace.table; val empty = NameSpace.empty_table; val copy = I; val extend = I; - fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup => - error ("Attempt to merge different versions of attribute " ^ quote dup); + fun merge _ tables : T = NameSpace.merge_tables tables; ); fun print_attributes thy = let val attribs = Attributes.get thy; - fun prt_attr (name, ((_, comment), _)) = Pretty.block + fun prt_attr (name, (_, comment)) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; in [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))] |> Pretty.chunks |> Pretty.writeln end; -fun add_attribute name att comment thy = thy |> Attributes.map (fn atts => - #2 (NameSpace.define (Sign.naming_of thy) (name, ((att, comment), stamp ())) atts) - handle Symtab.DUP dup => error ("Duplicate declaration of attribute " ^ quote dup)); +fun add_attribute name att comment thy = thy + |> Attributes.map (#2 o NameSpace.define true (Sign.naming_of thy) (name, (att, comment))); (* name space *) @@ -117,7 +115,7 @@ let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup attrs name of NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos) - | SOME ((att, _), _) => (Position.report (Markup.attribute name) pos; att src)) + | SOME (att, _) => (Position.report (Markup.attribute name) pos; att src)) end; in attr end; diff -r d23e75d4f7da -r c859019d3ac5 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sat Oct 24 19:04:57 2009 +0200 +++ b/src/Pure/Isar/locale.ML Sat Oct 24 19:20:03 2009 +0200 @@ -143,7 +143,7 @@ | NONE => error ("Unknown locale " ^ quote name)); fun register_locale binding parameters spec intros axioms decls notes dependencies thy = - thy |> Locales.map (NameSpace.define (Sign.naming_of thy) + thy |> Locales.map (NameSpace.define true (Sign.naming_of thy) (binding, mk_locale ((parameters, spec, intros, axioms), ((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes), diff -r d23e75d4f7da -r c859019d3ac5 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sat Oct 24 19:04:57 2009 +0200 +++ b/src/Pure/Isar/method.ML Sat Oct 24 19:20:03 2009 +0200 @@ -322,27 +322,25 @@ structure Methods = TheoryDataFun ( - type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table; + type T = ((src -> Proof.context -> method) * string) NameSpace.table; val empty = NameSpace.empty_table; val copy = I; val extend = I; - fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup => - error ("Attempt to merge different versions of method " ^ quote dup); + fun merge _ tables : T = NameSpace.merge_tables tables; ); fun print_methods thy = let val meths = Methods.get thy; - fun prt_meth (name, ((_, comment), _)) = Pretty.block + fun prt_meth (name, (_, comment)) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; in [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))] |> Pretty.chunks |> Pretty.writeln end; -fun add_method name meth comment thy = thy |> Methods.map (fn meths => - #2 (NameSpace.define (Sign.naming_of thy) (name, ((meth, comment), stamp ())) meths) - handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup)); +fun add_method name meth comment thy = thy + |> Methods.map (#2 o NameSpace.define true (Sign.naming_of thy) (name, (meth, comment))); (* get methods *) @@ -357,7 +355,7 @@ let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup meths name of NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos) - | SOME ((mth, _), _) => (Position.report (Markup.method name) pos; mth src)) + | SOME (mth, _) => (Position.report (Markup.method name) pos; mth src)) end; in meth end; diff -r d23e75d4f7da -r c859019d3ac5 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Sat Oct 24 19:04:57 2009 +0200 +++ b/src/Pure/codegen.ML Sat Oct 24 19:20:03 2009 +0200 @@ -337,15 +337,16 @@ val tc = Sign.intern_type thy s; in case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of - SOME ((Type.LogicalType i, _), _) => + SOME (Type.LogicalType i, _) => if num_args_of (fst syn) > i then error ("More arguments than corresponding type constructor " ^ s) - else (case AList.lookup (op =) types tc of - NONE => CodegenData.put {codegens = codegens, - tycodegens = tycodegens, consts = consts, - types = (tc, syn) :: types, - preprocs = preprocs, modules = modules} thy - | SOME _ => error ("Type " ^ tc ^ " already associated with code")) + else + (case AList.lookup (op =) types tc of + NONE => CodegenData.put {codegens = codegens, + tycodegens = tycodegens, consts = consts, + types = (tc, syn) :: types, + preprocs = preprocs, modules = modules} thy + | SOME _ => error ("Type " ^ tc ^ " already associated with code")) | _ => error ("Not a type constructor: " ^ s) end; diff -r d23e75d4f7da -r c859019d3ac5 src/Pure/consts.ML --- a/src/Pure/consts.ML Sat Oct 24 19:04:57 2009 +0200 +++ b/src/Pure/consts.ML Sat Oct 24 19:20:03 2009 +0200 @@ -50,7 +50,7 @@ type abbrev = {rhs: term, normal_rhs: term, force_expand: bool}; datatype T = Consts of - {decls: ((decl * abbrev option) * serial) NameSpace.table, + {decls: (decl * abbrev option) NameSpace.table, constraints: typ Symtab.table, rev_abbrevs: (term * term) Item_Net.T Symtab.table}; @@ -84,7 +84,7 @@ fun dest (Consts {decls = (space, decls), constraints, ...}) = {constants = (space, - Symtab.fold (fn (c, (({T, ...}, abbr), _)) => + Symtab.fold (fn (c, ({T, ...}, abbr)) => Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty), constraints = (space, constraints)}; @@ -93,7 +93,7 @@ fun the_const (Consts {decls = (_, tab), ...}) c = (case Symtab.lookup tab c of - SOME (decl, _) => decl + SOME decl => decl | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], [])); fun the_type consts c = @@ -221,13 +221,6 @@ (** build consts **) -fun err_dup_const c = - error ("Duplicate declaration of constant " ^ quote c); - -fun extend_decls naming decl tab = NameSpace.define naming decl tab - handle Symtab.DUP c => err_dup_const c; - - (* name space *) fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) => @@ -236,12 +229,13 @@ (* declarations *) -fun declare authentic naming tags (b, declT) = map_consts (fn (decls, constraints, rev_abbrevs) => - let - val tags' = tags |> Position.default_properties (Position.thread_data ()); - val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic}; - val (_, decls') = decls |> extend_decls naming (b, ((decl, NONE), serial ())); - in (decls', constraints, rev_abbrevs) end); +fun declare authentic naming tags (b, declT) = + map_consts (fn (decls, constraints, rev_abbrevs) => + let + val tags' = tags |> Position.default_properties (Position.thread_data ()); + val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic}; + val (_, decls') = decls |> NameSpace.define true naming (b, (decl, NONE)); + in (decls', constraints, rev_abbrevs) end); (* constraints *) @@ -278,7 +272,7 @@ val force_expand = mode = PrintMode.internal; val _ = Term.exists_subterm Term.is_Var raw_rhs andalso - error ("Illegal schematic variables on rhs of abbreviation: " ^ Binding.str_of b); + error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b)); val rhs = raw_rhs |> Term.map_types (Type.cert_typ tsig) @@ -294,7 +288,7 @@ val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true}; val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand}; val (_, decls') = decls - |> extend_decls naming (b, ((decl, SOME abbr), serial ())); + |> NameSpace.define true naming (b, (decl, SOME abbr)); val rev_abbrevs' = rev_abbrevs |> insert_abbrevs mode (rev_abbrev lhs rhs); in (decls', constraints, rev_abbrevs') end) @@ -319,8 +313,7 @@ (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1}, Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) = let - val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2) - handle Symtab.DUP c => err_dup_const c; + val decls' = NameSpace.merge_tables (decls1, decls2); val constraints' = Symtab.join (K fst) (constraints1, constraints2); val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2); in make_consts (decls', constraints', rev_abbrevs') end; diff -r d23e75d4f7da -r c859019d3ac5 src/Pure/display.ML --- a/src/Pure/display.ML Sat Oct 24 19:04:57 2009 +0200 +++ b/src/Pure/display.ML Sat Oct 24 19:20:03 2009 +0200 @@ -146,14 +146,14 @@ [Pretty.str "default sort:", Pretty.brk 1, prt_sort S]; val tfrees = map (fn v => TFree (v, [])); - fun pretty_type syn (t, ((Type.LogicalType n, _), _)) = + fun pretty_type syn (t, (Type.LogicalType n, _)) = if syn then NONE else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n)))) - | pretty_type syn (t, ((Type.Abbreviation (vs, U, syn'), _), _)) = + | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) = if syn <> syn' then NONE else SOME (Pretty.block [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U]) - | pretty_type syn (t, ((Type.Nonterminal, _), _)) = + | pretty_type syn (t, (Type.Nonterminal, _)) = if not syn then NONE else SOME (prt_typ (Type (t, []))); diff -r d23e75d4f7da -r c859019d3ac5 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Oct 24 19:04:57 2009 +0200 +++ b/src/Pure/simplifier.ML Sat Oct 24 19:20:03 2009 +0200 @@ -143,9 +143,6 @@ (** named simprocs **) -fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name); - - (* data *) structure Simprocs = GenericDataFun @@ -153,8 +150,7 @@ type T = simproc NameSpace.table; val empty = NameSpace.empty_table; val extend = I; - fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs - handle Symtab.DUP dup => err_dup_simproc dup; + fun merge _ simprocs = NameSpace.merge_tables simprocs; ); @@ -201,9 +197,7 @@ val b' = Morphism.binding phi b; val simproc' = morph_simproc phi simproc; in - Simprocs.map (fn simprocs => - NameSpace.define naming (b', simproc') simprocs |> snd - handle Symtab.DUP dup => err_dup_simproc dup) + Simprocs.map (#2 o NameSpace.define true naming (b', simproc')) #> map_ss (fn ss => ss addsimprocs [simproc']) end) end; diff -r d23e75d4f7da -r c859019d3ac5 src/Pure/theory.ML --- a/src/Pure/theory.ML Sat Oct 24 19:04:57 2009 +0200 +++ b/src/Pure/theory.ML Sat Oct 24 19:20:03 2009 +0200 @@ -86,8 +86,6 @@ fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers}; -fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup); - structure ThyData = TheoryDataFun ( type T = thy; @@ -166,7 +164,7 @@ fun read_axm thy (b, str) = cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg => - cat_error msg ("The error(s) above occurred in axiom: " ^ quote (Binding.str_of b)); + cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b)); (* add_axioms(_i) *) @@ -176,8 +174,7 @@ fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms => let val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms; - val axioms' = fold (snd oo NameSpace.define (Sign.naming_of thy)) axms axioms - handle Symtab.DUP dup => err_dup_axm dup; + val axioms' = fold (#2 oo NameSpace.define true (Sign.naming_of thy)) axms axioms; in axioms' end); in diff -r d23e75d4f7da -r c859019d3ac5 src/Pure/thm.ML --- a/src/Pure/thm.ML Sat Oct 24 19:04:57 2009 +0200 +++ b/src/Pure/thm.ML Sat Oct 24 19:20:03 2009 +0200 @@ -1724,16 +1724,13 @@ (* authentic derivation names *) -fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup); - structure Oracles = TheoryDataFun ( - type T = serial NameSpace.table; + type T = unit NameSpace.table; val empty = NameSpace.empty_table; val copy = I; val extend = I; - fun merge _ oracles : T = NameSpace.merge_tables (op =) oracles - handle Symtab.DUP dup => err_dup_ora dup; + fun merge _ oracles : T = NameSpace.merge_tables oracles; ); val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get; @@ -1741,8 +1738,7 @@ fun add_oracle (b, oracle) thy = let val naming = Sign.naming_of thy; - val (name, tab') = NameSpace.define naming (b, serial ()) (Oracles.get thy) - handle Symtab.DUP _ => err_dup_ora (Binding.str_of b); + val (name, tab') = NameSpace.define true naming (b, ()) (Oracles.get thy); val thy' = Oracles.put tab' thy; in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;