src/Pure/General/name_space.ML

tuned signature;

(*  Title:      Pure/General/name_space.ML
    Author:     Markus Wenzel, TU Muenchen

Generic name spaces with declared and hidden entries.  Unknown names
are considered global; no support for absolute addressing.
*)

type xstring = string;    (*external names*)

signature NAME_SPACE =
sig
  val hidden: string -> string
  val is_hidden: string -> bool
  type T
  val empty: string -> T
  val kind_of: T -> string
  val defined_entry: T -> string -> bool
  val the_entry: T -> string ->
    {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
  val entry_ord: T -> string * string -> order
  val markup: T -> string -> Markup.T
  val is_concealed: T -> string -> bool
  val intern: T -> xstring -> string
  val names_long_raw: Config.raw
  val names_long: bool Config.T
  val names_short_raw: Config.raw
  val names_short: bool Config.T
  val names_unique_raw: Config.raw
  val names_unique: bool Config.T
  val extern: Proof.context -> T -> string -> xstring
  val extern_ord: Proof.context -> T -> string * string -> order
  val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
  val pretty: Proof.context -> T -> string -> Pretty.T
  val hide: bool -> string -> T -> T
  val merge: T * T -> T
  type naming
  val conceal: naming -> naming
  val get_group: naming -> serial option
  val set_group: serial option -> naming -> naming
  val set_theory_name: string -> naming -> naming
  val new_group: naming -> naming
  val reset_group: naming -> naming
  val add_path: string -> naming -> naming
  val root_path: naming -> naming
  val parent_path: naming -> naming
  val mandatory_path: string -> naming -> naming
  val qualified_path: bool -> binding -> naming -> naming
  val default_naming: naming
  val local_naming: naming
  val transform_binding: naming -> binding -> binding
  val full_name: naming -> binding -> string
  val base_name: binding -> string
  val alias: naming -> binding -> string -> T -> T
  val naming_of: Context.generic -> naming
  val map_naming: (naming -> naming) -> Context.generic -> Context.generic
  val declare: Context.generic -> bool -> binding -> T -> string * T
  type 'a table = T * 'a Symtab.table
  val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
  val get: 'a table -> string -> 'a
  val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
  val empty_table: string -> 'a table
  val merge_tables: 'a table * 'a table -> 'a table
  val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
    'a table * 'a table -> 'a table
  val dest_table: Proof.context -> 'a table -> (string * 'a) list
  val extern_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
end;

structure Name_Space: NAME_SPACE =
struct


(** name spaces **)

(* hidden entries *)

fun hidden name = "??." ^ name;
val is_hidden = String.isPrefix "??.";


(* datatype entry *)

type entry =
 {concealed: bool,
  group: serial option,
  theory_name: string,
  pos: Position.T,
  id: serial};

fun entry_markup def kind (name, {pos, id, ...}: entry) =
  Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);

fun print_entry_ref kind (name, entry) =
  quote (Markup.markup (entry_markup false kind (name, entry)) name);

fun err_dup kind entry1 entry2 pos =
  error ("Duplicate " ^ kind ^ " declaration " ^
    print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos);

fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name;


(* datatype T *)

datatype T =
  Name_Space of
   {kind: string,
    internals: (string list * string list) Symtab.table,  (*visible, hidden*)
    entries: (xstring list * entry) Symtab.table};        (*externals, entry*)

fun make_name_space (kind, internals, entries) =
  Name_Space {kind = kind, internals = internals, entries = entries};

fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
  make_name_space (f (kind, internals, entries));

fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
  (kind, Symtab.map_default (xname, ([], [])) f internals, entries));


fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty);

fun kind_of (Name_Space {kind, ...}) = kind;

fun defined_entry (Name_Space {entries, ...}) = Symtab.defined entries;

fun the_entry (Name_Space {kind, entries, ...}) name =
  (case Symtab.lookup entries name of
    NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
  | SOME (_, entry) => entry);

fun entry_ord space = int_ord o pairself (#id o the_entry space);

fun markup (Name_Space {kind, entries, ...}) name =
  (case Symtab.lookup entries name of
    NONE => Markup.intensify
  | SOME (_, entry) => entry_markup false kind (name, entry));

fun is_concealed space name = #concealed (the_entry space name);


(* name accesses *)

fun lookup (Name_Space {internals, ...}) xname =
  (case Symtab.lookup internals xname of
    NONE => (xname, true)
  | SOME ([], []) => (xname, true)
  | SOME ([name], _) => (name, true)