# HG changeset patch # User haftmann # Date 1227189325 -3600 # Node ID f53abb0733ee70a8894f9c6191ca575f1bb68b7d # Parent b1d46059d502ec1f20fe76d5ee1b8230dcd5c056 using name bindings diff -r b1d46059d502 -r f53abb0733ee src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu Nov 20 14:51:40 2008 +0100 +++ b/src/Pure/Isar/class.ML Thu Nov 20 14:55:25 2008 +0100 @@ -513,7 +513,7 @@ val ty' = Term.fastype_of rhs'; in thy' - |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs'') |> snd + |> Sign.add_abbrev (#1 prmode) pos (Name.binding c, map_types Type.strip_sorts rhs'') |> snd |> Sign.add_const_constraint (c', SOME ty') |> Sign.notation true prmode [(Const (c', ty'), mx)] |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE)) diff -r b1d46059d502 -r f53abb0733ee src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Nov 20 14:51:40 2008 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Nov 20 14:55:25 2008 +0100 @@ -26,6 +26,7 @@ val name_decl: (string * 'a -> Proof.context -> 'b * Proof.context) -> Name.binding * 'a -> Proof.context -> (string * 'b) * Proof.context val full_name: Proof.context -> bstring -> string + val full_binding: Proof.context -> Name.binding -> string val consts_of: Proof.context -> Consts.T val const_syntax_name: Proof.context -> string -> string val the_const_constraint: Proof.context -> string -> typ @@ -136,7 +137,7 @@ Context.generic -> Context.generic val add_const_constraint: string * typ option -> Proof.context -> Proof.context val add_abbrev: string -> Properties.T -> - bstring * term -> Proof.context -> (term * term) * Proof.context + Name.binding * term -> Proof.context -> (term * term) * Proof.context val revert_abbrev: string -> string -> Proof.context -> Proof.context val verbose: bool ref val setmp_verbose: ('a -> 'b) -> 'a -> 'b @@ -248,19 +249,20 @@ val naming_of = #naming o rep_context; -fun name_decl decl (binding, x) ctxt = +fun name_decl decl (b, x) ctxt = let val naming = naming_of ctxt; - val (naming', name) = Name.namify naming binding; + val (naming', name) = Name.namify naming b; in ctxt |> map_naming (K naming') - |> decl (Name.name_of binding, x) + |> decl (Name.name_of b, x) |>> pair name ||> map_naming (K naming) end; val full_name = NameSpace.full o naming_of; +val full_binding = NameSpace.full_binding o naming_of; val syntax_of = #syntax o rep_context; val syn_of = LocalSyntax.syn_of o syntax_of; @@ -977,15 +979,14 @@ local -fun update_thms _ (bname, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt bname)) - | update_thms do_props (bname, SOME ths) ctxt = ctxt |> map_facts - (Facts.add_local do_props (naming_of ctxt) (full_name ctxt bname, ths)); +fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_binding ctxt b)) + | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts + (Facts.add_local do_props (naming_of ctxt) (full_binding ctxt b, ths)); -fun gen_note_thmss get k = fold_map (fn ((binding, more_attrs), raw_facts) => fn ctxt => +fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt => let - val bname = Name.name_of binding; - val pos = Name.pos_of binding; - val name = full_name ctxt bname; + val pos = Name.pos_of b; + val name = full_binding ctxt b; val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos; val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts); @@ -994,7 +995,7 @@ val (res, ctxt') = fold_map app facts ctxt; val thms = PureThy.name_thms false false pos name (flat res); val Mode {stmt, ...} = get_mode ctxt; - in ((name, thms), ctxt' |> update_thms stmt (bname, SOME thms)) end); + in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end); in @@ -1004,7 +1005,7 @@ fun put_thms do_props thms ctxt = ctxt |> map_naming (K local_naming) |> ContextPosition.set_visible false - |> update_thms do_props thms + |> update_thms do_props (apfst Name.binding thms) |> ContextPosition.restore_visible ctxt |> restore_naming ctxt; @@ -1023,9 +1024,9 @@ local fun prep_vars prep_typ internal = - fold_map (fn (raw_binding, raw_T, raw_mx) => fn ctxt => + fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt => let - val raw_x = Name.name_of raw_binding; + val raw_x = Name.name_of raw_b; val (x, mx) = Syntax.const_mixfix raw_x raw_mx; val _ = Syntax.is_identifier (no_skolem internal x) orelse error ("Illegal variable name: " ^ quote x); @@ -1034,7 +1035,7 @@ if internal then T else Type.no_tvars T handle TYPE (msg, _, _) => error msg; val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T; - val var = (Name.map_name (K x) raw_binding, opt_T, mx); + val var = (Name.map_name (K x) raw_b, opt_T, mx); in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end); in @@ -1105,13 +1106,13 @@ in cert_term ctxt (Const (c, T)); T end; in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end; -fun add_abbrev mode tags (c, raw_t) ctxt = +fun add_abbrev mode tags (b, raw_t) ctxt = let val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t - handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c); + handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b)); val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; val ((lhs, rhs), consts') = consts_of ctxt - |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (c, t); + |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t); in ctxt |> (map_consts o apfst) (K consts') @@ -1140,8 +1141,8 @@ ctxt' |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars) |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix); - val _ = (vars ~~ xs') |> List.app (fn ((binding, _, _), x') => - ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of binding)); + val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') => + ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of b)); in (xs', ctxt'') end; in diff -r b1d46059d502 -r f53abb0733ee src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Thu Nov 20 14:51:40 2008 +0100 +++ b/src/Pure/Isar/theory_target.ML Thu Nov 20 14:55:25 2008 +0100 @@ -1,5 +1,6 @@ (* Title: Pure/Isar/theory_target.ML ID: $Id$ + ID: $Id$ Author: Makarius Common theory/locale/class/instantiation/overloading targets. @@ -192,18 +193,18 @@ else if not is_class then (NoSyn, mx, NoSyn) else (mx, NoSyn, NoSyn); -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi = +fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((b, mx), rhs) phi = let - val c' = Morphism.name phi c; + val b' = Morphism.name phi b; val rhs' = Morphism.term phi rhs; - val name' = Name.name_with_prefix c'; - val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs')); - val arg = (name', Term.close_schematic_term rhs'); + val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs')); + val arg = (b', Term.close_schematic_term rhs'); val similar_body = Type.similar_types (rhs, rhs'); (* FIXME workaround based on educated guess *) - val class_global = Name.name_of c = Name.name_of c' - andalso not (null (Name.prefix_of c')) - andalso (fst o snd o split_last) (Name.prefix_of c') = Class.class_prefix target; + val (prefix', _) = Name.dest_binding b'; + val class_global = Name.name_of b = Name.name_of b' + andalso not (null prefix') + andalso (fst o snd o split_last) prefix' = Class.class_prefix target; in not (is_class andalso (similar_body orelse class_global)) ? (Context.mapping_result @@ -267,7 +268,7 @@ in lthy |> (if is_locale then - LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (c, global_rhs)) + LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (b, global_rhs)) #-> (fn (lhs, _) => let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #> @@ -275,9 +276,9 @@ end) else LocalTheory.theory - (Sign.add_abbrev (#1 prmode) tags (c, global_rhs) #-> (fn (lhs, _) => + (Sign.add_abbrev (#1 prmode) tags (b, global_rhs) #-> (fn (lhs, _) => Sign.notation true prmode [(lhs, mx3)]))) - |> ProofContext.add_abbrev PrintMode.internal tags (c, t) |> snd + |> ProofContext.add_abbrev PrintMode.internal tags (b, t) |> snd |> LocalDefs.fixed_abbrev ((b, NoSyn), t) end; diff -r b1d46059d502 -r f53abb0733ee src/Pure/consts.ML --- a/src/Pure/consts.ML Thu Nov 20 14:51:40 2008 +0100 +++ b/src/Pure/consts.ML Thu Nov 20 14:55:25 2008 +0100 @@ -30,10 +30,10 @@ val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*) val typargs: T -> string * typ -> typ list val instance: T -> string * typ list -> typ - val declare: bool -> NameSpace.naming -> Properties.T -> (bstring * typ) -> T -> T + val declare: bool -> NameSpace.naming -> Properties.T -> (Name.binding * typ) -> T -> T val constrain: string * typ option -> T -> T val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T -> - bstring * term -> T -> (term * term) * T + Name.binding * term -> T -> (term * term) * T val revert_abbrev: string -> string -> T -> T val hide: bool -> string -> T -> T val empty: T @@ -211,7 +211,7 @@ fun err_dup_const c = error ("Duplicate declaration of constant " ^ quote c); -fun extend_decls naming decl tab = NameSpace.extend_table naming [decl] tab +fun extend_decls naming decl tab = NameSpace.table_declare naming decl tab handle Symtab.DUP c => err_dup_const c; @@ -223,11 +223,11 @@ (* declarations *) -fun declare authentic naming tags (c, declT) = map_consts (fn (decls, constraints, rev_abbrevs) => +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 (c, ((decl, NONE), serial ())); + val (_, decls') = decls |> extend_decls naming (b, ((decl, NONE), serial ())); in (decls', constraints, rev_abbrevs) end); @@ -262,7 +262,7 @@ in -fun abbreviate pp tsig naming mode tags (c, raw_rhs) consts = +fun abbreviate pp tsig naming mode tags (b, raw_rhs) consts = let val cert_term = certify pp tsig false consts; val expand_term = certify pp tsig true consts; @@ -273,7 +273,7 @@ |> cert_term; val normal_rhs = expand_term rhs; val T = Term.fastype_of rhs; - val lhs = Const (NameSpace.full naming c, T); + val lhs = Const (NameSpace.full_binding naming b, T); fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^ Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs))); @@ -285,8 +285,8 @@ val tags' = tags |> Position.default_properties (Position.thread_data ()); 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 (c, ((decl, SOME abbr), serial ())); + val (_, decls') = decls + |> extend_decls naming (b, ((decl, SOME abbr), serial ())); val rev_abbrevs' = rev_abbrevs |> fold (curry Symtab.cons_list mode) (rev_abbrev lhs rhs); in (decls', constraints, rev_abbrevs') end) diff -r b1d46059d502 -r f53abb0733ee src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Nov 20 14:51:40 2008 +0100 +++ b/src/Pure/pure_thy.ML Thu Nov 20 14:55:25 2008 +0100 @@ -143,35 +143,36 @@ fun enter_proofs (thy, thms) = (FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms); -fun enter_thms _ _ app_att ("", thms) thy = swap (enter_proofs (app_att (thy, thms))) - | enter_thms pre_name post_name app_att (bname, thms) thy = - let - val naming = Sign.naming_of thy; - val name = NameSpace.full naming bname; - val (thy', thms') = - enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms))); - val thms'' = map (Thm.transfer thy') thms'; - val thy'' = thy' |> FactsData.map (apfst (Facts.add_global naming (name, thms''))); - in (thms'', thy'') end; +fun enter_thms pre_name post_name app_att (b, thms) thy = + if Name.is_nothing b + then swap (enter_proofs (app_att (thy, thms))) + else let + val naming = Sign.naming_of thy; + val name = NameSpace.full_binding naming b; + val (thy', thms') = + enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms))); + val thms'' = map (Thm.transfer thy') thms'; + val thy'' = thy' |> FactsData.map (apfst (Facts.add_global naming (name, thms''))); + in (thms'', thy'') end; (* store_thm(s) *) -val store_thms = - enter_thms (name_thms true true Position.none) (name_thms false true Position.none) I; +fun store_thms (bname, thms) = enter_thms (name_thms true true Position.none) + (name_thms false true Position.none) I (Name.binding bname, thms); -fun store_thm (name, th) = store_thms (name, [th]) #>> the_single; +fun store_thm (bname, th) = store_thms (bname, [th]) #>> the_single; -fun store_thm_open (name, th) = +fun store_thm_open (bname, th) = enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I - (name, [th]) #>> the_single; + (Name.binding bname, [th]) #>> the_single; (* add_thms(s) *) fun add_thms_atts pre_name ((bname, thms), atts) = enter_thms pre_name (name_thms false true Position.none) - (foldl_map (Thm.theory_attributes atts)) (bname, thms); + (foldl_map (Thm.theory_attributes atts)) (Name.binding bname, thms); fun gen_add_thmss pre_name = fold_map (add_thms_atts pre_name); @@ -195,17 +196,16 @@ local -fun gen_note_thmss tag = fold_map (fn ((binding, more_atts), ths_atts) => fn thy => +fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy => let - val bname = Name.name_of binding; - val pos = Name.pos_of binding; - val name = Sign.full_name thy bname; + val pos = Name.pos_of b; + val name = Sign.full_binding thy b; val _ = Position.report (Markup.fact_decl name) pos; fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths); val (thms, thy') = thy |> enter_thms (name_thmss true pos) (name_thms false true pos) (apsnd flat o foldl_map app) - (bname, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts); + (b, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts); in ((name, thms), thy') end); in diff -r b1d46059d502 -r f53abb0733ee src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Nov 20 14:51:40 2008 +0100 +++ b/src/Pure/sign.ML Thu Nov 20 14:55:25 2008 +0100 @@ -18,6 +18,7 @@ val name_decl: (string * 'a -> theory -> 'b * theory) -> Name.binding * 'a -> theory -> (string * 'b) * theory val full_name: theory -> bstring -> string + val full_binding: theory -> Name.binding -> string val full_name_path: theory -> string -> bstring -> string val declare_name: theory -> string -> NameSpace.T -> NameSpace.T val syn_of: theory -> Syntax.syntax @@ -93,10 +94,10 @@ val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory + val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory val add_consts: (bstring * string * mixfix) list -> theory -> theory val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory - val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory - val add_abbrev: string -> Properties.T -> bstring * term -> theory -> (term * term) * theory + val add_abbrev: string -> Properties.T -> Name.binding * term -> theory -> (term * term) * theory val revert_abbrev: string -> string -> theory -> theory val add_const_constraint: string * typ option -> theory -> theory val primitive_class: string * class list -> theory -> theory @@ -190,20 +191,21 @@ val naming_of = #naming o rep_sg; val base_name = NameSpace.base; -fun name_decl decl (binding, x) thy = +fun name_decl decl (b, x) thy = let val naming = naming_of thy; - val (naming', name) = Name.namify naming binding; + val (naming', name) = Name.namify naming b; in thy |> map_naming (K naming') - |> decl (Name.name_of binding, x) + |> decl (Name.name_of b, x) |>> pair name ||> map_naming (K naming) end; val namify = Name.namify o naming_of; val full_name = NameSpace.full o naming_of; +val full_binding = NameSpace.full_binding o naming_of; fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy)); val declare_name = NameSpace.declare o naming_of; @@ -520,15 +522,16 @@ let val ctxt = ProofContext.init thy; val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt; - fun prep (raw_c, raw_T, raw_mx) = + fun prep (raw_b, raw_T, raw_mx) = let - val (c, mx) = Syntax.const_mixfix raw_c raw_mx; - val full_c = full_name thy c; - val c' = if authentic then Syntax.constN ^ full_c else c; + val (mx_name, mx) = Syntax.const_mixfix (Name.name_of raw_b) raw_mx; + val b = Name.map_name (K mx_name) raw_b; + val c = full_binding thy b; + val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b; val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg => - cat_error msg ("in declaration of constant " ^ quote c); + cat_error msg ("in declaration of constant " ^ quote (Name.display b)); val T' = Logic.varifyT T; - in ((c, T'), (c', T', mx), Const (full_c, T)) end; + in ((b, T'), (c_syn, T', mx), Const (c, T)) end; val args = map prep raw_args; val tags' = tags |> Properties.put (Markup.theory_nameN, Context.theory_name thy); in @@ -538,18 +541,19 @@ |> pair (map #3 args) end; +fun bindify (name, T, mx) = (Name.binding name, T, mx); + in -val add_consts = snd oo gen_add_consts Syntax.parse_typ false []; -val add_consts_i = snd oo gen_add_consts (K I) false []; +fun add_consts args = snd o gen_add_consts Syntax.parse_typ false [] (map bindify args); +fun add_consts_i args = snd o gen_add_consts (K I) false [] (map bindify args); fun declare_const tags ((b, T), mx) thy = let - val c = Name.name_of b; val pos = Name.pos_of b; val tags' = Position.default_properties pos tags; - val ([const as Const (full_c, _)], thy') = gen_add_consts (K I) true tags' [(c, T, mx)] thy; - val _ = Position.report (Markup.const_decl full_c) pos; + val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy; + val _ = Position.report (Markup.const_decl c) pos; in (const, thy') end; end; @@ -557,14 +561,14 @@ (* abbreviations *) -fun add_abbrev mode tags (c, raw_t) thy = +fun add_abbrev mode tags (b, raw_t) thy = let val pp = Syntax.pp_global thy; val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy; val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg) - handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c); + handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b)); val (res, consts') = consts_of thy - |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (c, t); + |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t); in (res, thy |> map_consts (K consts')) end; fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);