# HG changeset patch # User haftmann # Date 1228156876 -3600 # Node ID 128459bd72d22f3356e360f6301eb49069ec25db # Parent df0cb410be355c3342b967b0b9c750f4814bef2c new Binding module diff -r df0cb410be35 -r 128459bd72d2 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/HOL/Tools/inductive_package.ML Mon Dec 01 19:41:16 2008 +0100 @@ -638,8 +638,8 @@ (* add definiton of recursive predicates to theory *) val rec_name = - if Name.is_nothing alt_name then - Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn)) + if Binding.is_nothing alt_name then + Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn)) else alt_name; val ((rec_const, (_, fp_def)), ctxt') = ctxt |> diff -r df0cb410be35 -r 128459bd72d2 src/HOL/Tools/inductive_set_package.ML --- a/src/HOL/Tools/inductive_set_package.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/HOL/Tools/inductive_set_package.ML Mon Dec 01 19:41:16 2008 +0100 @@ -499,8 +499,8 @@ (* convert theorems to set notation *) val rec_name = - if Name.is_nothing alt_name then - Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn)) + if Binding.is_nothing alt_name then + Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn)) else alt_name; val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn; (* FIXME *) val (intr_names, intr_atts) = split_list (map fst intros); diff -r df0cb410be35 -r 128459bd72d2 src/Pure/General/ROOT.ML --- a/src/Pure/General/ROOT.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/General/ROOT.ML Mon Dec 01 19:41:16 2008 +0100 @@ -27,6 +27,7 @@ use "ord_list.ML"; use "balanced_tree.ML"; use "graph.ML"; +use "binding.ML"; use "name_space.ML"; use "lazy.ML"; use "path.ML"; diff -r df0cb410be35 -r 128459bd72d2 src/Pure/General/binding.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/binding.ML Mon Dec 01 19:41:16 2008 +0100 @@ -0,0 +1,75 @@ +(* Title: Pure/General/binding.ML + Author: Florian Haftmann, TU Muenchen + +Structured name bindings. +*) + +signature BASIC_BINDING = +sig + val long_names: bool ref + val short_names: bool ref + val unique_names: bool ref +end; + +signature BINDING = +sig + include BASIC_BINDING + type T + val binding_pos: string * Position.T -> T + val binding: string -> T + val no_binding: T + val dest_binding: T -> (string * bool) list * string + val is_nothing: T -> bool + val pos_of: T -> Position.T + + val map_binding: ((string * bool) list * string -> (string * bool) list * string) + -> T -> T + val add_prefix: bool -> string -> T -> T + val map_prefix: ((string * bool) list -> T -> T) -> T -> T + val display: T -> string +end + +structure Binding : BINDING = +struct + +(** global flags **) + +val long_names = ref false; +val short_names = ref false; +val unique_names = ref true; + + +(** binding representation **) + +datatype T = Binding of ((string * bool) list * string) * Position.T; + (* (prefix components (with mandatory flag), base name, position) *) + +fun binding_pos (name, pos) = Binding (([], name), pos); +fun binding name = binding_pos (name, Position.none); +val no_binding = binding ""; + +fun pos_of (Binding (_, pos)) = pos; +fun dest_binding (Binding (prefix_name, _)) = prefix_name; + +fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos); + +fun is_nothing (Binding ((_, name), _)) = name = ""; + +fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix" + else (map_binding o apfst) (cons (prfx, sticky)) b; + +fun map_prefix f (Binding ((prefix, name), pos)) = + f prefix (binding_pos (name, pos)); + +fun display (Binding ((prefix, name), _)) = + let + fun mk_prefix (prfx, true) = prfx + | mk_prefix (prfx, false) = enclose "(" ")" prfx + in if not (! long_names) orelse null prefix orelse name = "" then name + else space_implode "." (map mk_prefix prefix) ^ ":" ^ name + end; + +end; + +structure Basic_Binding : BASIC_BINDING = Binding; +open Basic_Binding; diff -r df0cb410be35 -r 128459bd72d2 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/General/name_space.ML Mon Dec 01 19:41:16 2008 +0100 @@ -1,5 +1,4 @@ (* Title: Pure/General/name_space.ML - ID: $Id$ Author: Markus Wenzel, TU Muenchen Generic name spaces with declared and hidden entries. Unknown names @@ -9,29 +8,9 @@ type bstring = string; (*names to be bound*) type xstring = string; (*external names*) -signature BASIC_NAME_SPACE = -sig - val long_names: bool ref - val short_names: bool ref - val unique_names: bool ref -end; - -signature NAME_BINDING = -sig - type binding - val binding_pos: string * Position.T -> binding - val binding: string -> binding - val no_binding: binding - val dest_binding: binding -> (string * bool) list * string - val is_nothing: binding -> bool - val pos_of: binding -> Position.T - val map_binding: ((string * bool) list * string -> (string * bool) list * string) - -> binding -> binding -end - signature NAME_SPACE = sig - include BASIC_NAME_SPACE + include BASIC_BINDING val hidden: string -> string val is_hidden: string -> bool val separator: string (*single char*) @@ -60,14 +39,13 @@ val no_base_names: naming -> naming val qualified_names: naming -> naming val sticky_prefix: string -> naming -> naming - include NAME_BINDING - val full_binding: naming -> binding -> string - val declare_binding: naming -> binding -> T -> string * T + val full_binding: naming -> Binding.T -> string + val declare_binding: naming -> Binding.T -> T -> string * T type 'a table = T * 'a Symtab.table val empty_table: 'a table - val table_declare: naming -> binding * 'a + val table_declare: naming -> Binding.T * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*) - val table_declare_permissive: naming -> binding * 'a + val table_declare_permissive: naming -> Binding.T * 'a -> 'a table -> string * 'a table val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table @@ -78,6 +56,9 @@ structure NameSpace: NAME_SPACE = struct +open Basic_Binding; + + (** long identifiers **) fun hidden name = "??." ^ name; @@ -170,10 +151,6 @@ fun intern space xname = #1 (lookup space xname); -val long_names = ref false; -val short_names = ref false; -val unique_names = ref true; - fun extern space name = let fun valid unique xname = @@ -241,23 +218,6 @@ -(** generic name bindings **) - -datatype binding = Binding of ((string * bool) list * string) * Position.T; - -fun binding_pos (name, pos) = Binding (([], name), pos); -fun binding name = binding_pos (name, Position.none); -val no_binding = binding ""; - -fun pos_of (Binding (_, pos)) = pos; -fun dest_binding (Binding (prefix_name, _)) = prefix_name; - -fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos); - -fun is_nothing (Binding ((_, name), _)) = name = ""; - - - (** naming contexts **) (* datatype naming *) @@ -321,8 +281,9 @@ val (accs, accs') = pairself (map implode_name) (accesses naming names); in space |> fold (add_name name) accs |> put_accesses name accs' end; -fun declare_binding bnaming (Binding ((prefix, bname), _)) = +fun declare_binding bnaming b = let + val (prefix, bname) = Binding.dest_binding b; val naming = apply_prefix prefix bnaming; val name = full naming bname; in declare naming name #> pair name end; @@ -343,8 +304,9 @@ fun table_declare naming = gen_table_declare Symtab.update_new naming; fun table_declare_permissive naming = gen_table_declare Symtab.update naming; -fun full_binding naming (Binding ((prefix, bname), _)) = - full (apply_prefix prefix naming) bname; +fun full_binding naming b = + let val (prefix, bname) = Binding.dest_binding b + in full (apply_prefix prefix naming) bname end; fun extend_table naming bentries (space, tab) = let val entries = map (apfst (full naming)) bentries @@ -366,6 +328,3 @@ val explode = explode_name; end; - -structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace; -open BasicNameSpace; diff -r df0cb410be35 -r 128459bd72d2 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/Isar/args.ML Mon Dec 01 19:41:16 2008 +0100 @@ -171,7 +171,7 @@ val name_source_position = named >> T.source_position_of; val name = named >> T.content_of; -val binding = P.position name >> Name.binding_pos; +val binding = P.position name >> Binding.binding_pos; val alt_name = alt_string >> T.content_of; val symbol = symbolic >> T.content_of; val liberal_name = symbol || name; diff -r df0cb410be35 -r 128459bd72d2 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/Isar/class.ML Mon Dec 01 19:41:16 2008 +0100 @@ -78,7 +78,7 @@ val class_prefix = Logic.const_of_class o Sign.base_name; fun class_name_morphism class = - Name.map_prefix (K (Name.add_prefix false (class_prefix class))); + Binding.map_prefix (K (Binding.add_prefix false (class_prefix class))); fun activate_class_morphism thy class inst morphism = Locale.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst; diff -r df0cb410be35 -r 128459bd72d2 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/Isar/locale.ML Mon Dec 01 19:41:16 2008 +0100 @@ -947,8 +947,8 @@ val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params; val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps]; val (lprfx, pprfx) = param_prefix name params; - val add_prefices = pprfx <> "" ? Name.add_prefix false pprfx - #> Name.add_prefix false lprfx; + val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx + #> Binding.add_prefix false lprfx; val elem_morphism = Element.rename_morphism ren $> Morphism.name_morphism add_prefices $> @@ -1634,10 +1634,10 @@ fun name_morph phi_name (lprfx, pprfx) b = b - |> (if not (Name.is_nothing b) andalso pprfx <> "" - then Name.add_prefix false pprfx else I) - |> (if not (Name.is_nothing b) - then Name.add_prefix false lprfx else I) + |> (if not (Binding.is_nothing b) andalso pprfx <> "" + then Binding.add_prefix false pprfx else I) + |> (if not (Binding.is_nothing b) + then Binding.add_prefix false lprfx else I) |> phi_name; fun inst_morph thy phi_name param_prfx insts prems eqns export = @@ -2442,11 +2442,11 @@ end; fun standard_name_morph interp_prfx b = - if Name.is_nothing b then b - else Name.map_prefix (fn ((lprfx, _) :: pprfx) => - fold (Name.add_prefix false o fst) pprfx - #> interp_prfx <> "" ? Name.add_prefix true interp_prfx - #> Name.add_prefix false lprfx + if Binding.is_nothing b then b + else Binding.map_prefix (fn ((lprfx, _) :: pprfx) => + fold (Binding.add_prefix false o fst) pprfx + #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx + #> Binding.add_prefix false lprfx ) b; in diff -r df0cb410be35 -r 128459bd72d2 src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/Isar/outer_parse.ML Mon Dec 01 19:41:16 2008 +0100 @@ -228,7 +228,7 @@ (* names and text *) val name = group "name declaration" (short_ident || sym_ident || string || number); -val binding = position name >> Name.binding_pos; +val binding = position name >> Binding.binding_pos; val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number); val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim); val path = group "file name/path specification" name >> Path.explode; diff -r df0cb410be35 -r 128459bd72d2 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/Isar/proof_context.ML Mon Dec 01 19:41:16 2008 +0100 @@ -971,7 +971,7 @@ fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt => let - val pos = Name.pos_of b; + val pos = Binding.pos_of b; val name = full_binding ctxt b; val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos; @@ -1128,7 +1128,7 @@ |> 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 ((b, _, _), x') => - ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of b)); + ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b)); in (xs', ctxt'') end; in diff -r df0cb410be35 -r 128459bd72d2 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/Isar/specification.ML Mon Dec 01 19:41:16 2008 +0100 @@ -190,7 +190,7 @@ val y = Name.name_of b; val _ = x = y orelse error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ - Position.str_of (Name.pos_of b)); + Position.str_of (Binding.pos_of b)); in (b, mx) end); val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK (var, ((Name.map_name (suffix "_raw") name, []), rhs)); @@ -223,7 +223,7 @@ val y = Name.name_of b; val _ = x = y orelse error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^ - Position.str_of (Name.pos_of b)); + Position.str_of (Binding.pos_of b)); in (b, mx) end); val lthy' = lthy |> ProofContext.set_syntax_mode mode (* FIXME ?!? *) @@ -348,7 +348,7 @@ lthy |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results') |> (fn (res, lthy') => - if Name.is_nothing name andalso null atts then + if Binding.is_nothing name andalso null atts then (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy') else let diff -r df0cb410be35 -r 128459bd72d2 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/Isar/theory_target.ML Mon Dec 01 19:41:16 2008 +0100 @@ -201,7 +201,7 @@ val arg = (b', Term.close_schematic_term rhs'); val similar_body = Type.similar_types (rhs, rhs'); (* FIXME workaround based on educated guess *) - val (prefix', _) = Name.dest_binding b'; + val (prefix', _) = Binding.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; diff -r df0cb410be35 -r 128459bd72d2 src/Pure/facts.ML --- a/src/Pure/facts.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/facts.ML Mon Dec 01 19:41:16 2008 +0100 @@ -192,7 +192,7 @@ fun add permissive do_props naming (b, ths) (Facts {facts, props}) = let - val (name, facts') = if Name.is_nothing b then ("", facts) + val (name, facts') = if Binding.is_nothing b then ("", facts) else let val (space, tab) = facts; val (name, space') = NameSpace.declare_binding naming b space; diff -r df0cb410be35 -r 128459bd72d2 src/Pure/name.ML --- a/src/Pure/name.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/name.ML Mon Dec 01 19:41:16 2008 +0100 @@ -29,20 +29,16 @@ val variant_list: string list -> string list -> string list val variant: string list -> string -> string - include NAME_BINDING - val add_prefix: bool -> string -> binding -> binding - val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding - val name_of: binding -> string (*FIMXE legacy*) - val map_name: (string -> string) -> binding -> binding (*FIMXE legacy*) - val qualified: string -> binding -> binding (*FIMXE legacy*) - val display: binding -> string + include BINDING + type binding = Binding.T + val name_of: Binding.T -> string (*FIMXE legacy*) + val map_name: (string -> string) -> Binding.T -> Binding.T (*FIMXE legacy*) + val qualified: string -> Binding.T -> Binding.T (*FIMXE legacy*) end; structure Name: NAME = struct -open NameSpace; - (** common defaults **) val uu = "uu"; @@ -152,27 +148,13 @@ (** generic name bindings **) -fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix" - else (map_binding o apfst) (cons (prfx, sticky)) b; +open Binding; + +type binding = Binding.T; val prefix_of = fst o dest_binding; val name_of = snd o dest_binding; val map_name = map_binding o apsnd; val qualified = map_name o NameSpace.qualified; -fun map_prefix f b = - let - val (prefix, name) = dest_binding b; - val pos = pos_of b; - in f prefix (binding_pos (name, pos)) end; - -fun display b = - let - val (prefix, name) = dest_binding b - fun mk_prefix (prfx, true) = prfx - | mk_prefix (prfx, false) = enclose "(" ")" prfx - in if not (! NameSpace.long_names) orelse null prefix orelse name = "" then name - else NameSpace.implode (map mk_prefix prefix) ^ ":" ^ name - end; - end; diff -r df0cb410be35 -r 128459bd72d2 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/pure_thy.ML Mon Dec 01 19:41:16 2008 +0100 @@ -144,7 +144,7 @@ (FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms); fun enter_thms pre_name post_name app_att (b, thms) thy = - if Name.is_nothing b + if Binding.is_nothing b then swap (enter_proofs (app_att (thy, thms))) else let val naming = Sign.naming_of thy; @@ -198,7 +198,7 @@ fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy => let - val pos = Name.pos_of b; + val pos = Binding.pos_of b; val name = Sign.full_binding thy b; val _ = Position.report (Markup.fact_decl name) pos; diff -r df0cb410be35 -r 128459bd72d2 src/Pure/sign.ML --- a/src/Pure/sign.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/sign.ML Mon Dec 01 19:41:16 2008 +0100 @@ -535,7 +535,7 @@ fun declare_const tags ((b, T), mx) thy = let - val pos = Name.pos_of b; + val pos = Binding.pos_of b; val tags' = Position.default_properties pos tags; 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;