(*  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_default: bool Unsynchronized.ref

   val names_long_raw: Config.raw

   val names_long: bool Config.T

   val names_short_default: bool Unsynchronized.ref

   val names_short_raw: Config.raw

   val names_short: bool Config.T

   val names_unique_default: bool Unsynchronized.ref

   val names_unique_raw: Config.raw

   val names_unique: bool Config.T

   val extern: Proof.context -> T -> string -> xstring

   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 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 -> (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) (Isabelle_Markup.entity kind name);

 fun print_entry def kind (name, entry) =

   quote (Markup.markup (entry_markup def kind (name, entry)) name);

 fun err_dup kind entry1 entry2 =

   error ("Duplicate " ^ kind ^ " declaration " ^

     print_entry true kind entry1 ^ " vs. " ^ print_entry true kind entry2);

 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 => Isabelle_Markup.hilite

   | 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)

   | SOME (name :: _, _) => (name, false)

   | SOME ([], name' :: _) => (hidden name', true));

 fun get_accesses (Name_Space {entries, ...}) name =

   (case Symtab.lookup entries name of

     NONE => [name]

   | SOME (externals, _) => externals);

 fun valid_accesses (Name_Space {internals, ...}) name =

   Symtab.fold (fn (xname, (names, _)) =>

     if not (null names) andalso hd names = name then cons xname else I) internals [];

 (* intern and extern *)

 fun intern space xname = #1 (lookup space xname);

 val names_long_default = Unsynchronized.ref false;

 val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default));

 val names_long = Config.bool names_long_raw;

 val names_short_default = Unsynchronized.ref false;

 val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default));

 val names_short = Config.bool names_short_raw;

 val names_unique_default = Unsynchronized.ref true;

 val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default));

 val names_unique = Config.bool names_unique_raw;

 fun extern ctxt space name =

   let

     val names_long = Config.get ctxt names_long;

     val names_short = Config.get ctxt names_short;

     val names_unique = Config.get ctxt names_unique;

     fun valid require_unique xname =

       let val (name', is_unique) = lookup space xname

       in name = name' andalso (not require_unique orelse is_unique) end;

     fun ext [] = if valid false name then name else hidden name

       | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;

   in

     if names_long then name

     else if names_short then Long_Name.base_name name

     else ext (get_accesses space name)

   end;

 (* modify internals *)

 val del_name = map_internals o apfst o remove (op =);

 fun del_name_extra name =

   map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));

 val add_name = map_internals o apfst o update (op =);

 val add_name' = map_internals o apsnd o update (op =);

 (* hide *)

 fun hide fully name space =

   if not (Long_Name.is_qualified name) then

     error ("Attempt to hide global name " ^ quote name)

   else if is_hidden name then

     error ("Attempt to hide hidden name " ^ quote name)

   else

     let val names = valid_accesses space name in

       space

       |> add_name' name name

       |> fold (del_name name)

         (if fully then names else inter (op =) [Long_Name.base_name name] names)

       |> fold (del_name_extra name) (get_accesses space name)

     end;

 (* merge *)

 fun merge

   (Name_Space {kind = kind1, internals = internals1, entries = entries1},

     Name_Space {kind = kind2, internals = internals2, entries = entries2}) =

   let

     val kind' =

       if kind1 = kind2 then kind1

       else error ("Attempt to merge different kinds of name spaces " ^

         quote kind1 ^ " vs. " ^ quote kind2);

     val internals' = (internals1, internals2) |> Symtab.join

       (K (fn ((names1, names1'), (names2, names2')) =>

         if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')

         then raise Symtab.SAME

         else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));

     val entries' = (entries1, entries2) |> Symtab.join

       (fn name => fn ((_, entry1), (_, entry2)) =>

         if #id entry1 = #id entry2 then raise Symtab.SAME

         else err_dup kind' (name, entry1) (name, entry2));

   in make_name_space (kind', internals', entries') end;

 (** naming context **)

 (* datatype naming *)

 datatype naming = Naming of

  {conceal: bool,

   group: serial option,

   theory_name: string,

   path: (string * bool) list};

 fun make_naming (conceal, group, theory_name, path) =

   Naming {conceal = conceal, group = group, theory_name = theory_name, path = path};

 fun map_naming f (Naming {conceal, group, theory_name, path}) =

   make_naming (f (conceal, group, theory_name, path));

 fun map_path f = map_naming (fn (conceal, group, theory_name, path) =>

   (conceal, group, theory_name, f path));

 val conceal = map_naming (fn (_, group, theory_name, path) =>

   (true, group, theory_name, path));

 fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>

   (conceal, group, theory_name, path));

 fun get_group (Naming {group, ...}) = group;

 fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>

   (conceal, group, theory_name, path));

 fun new_group naming = set_group (SOME (serial ())) naming;

 val reset_group = set_group NONE;

 fun add_path elems = map_path (fn path => path @ [(elems, false)]);

 val root_path = map_path (fn _ => []);

 val parent_path = map_path (perhaps (try (#1 o split_last)));

 fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);

 fun qualified_path mandatory binding = map_path (fn path =>

   path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));

 val default_naming = make_naming (false, NONE, "", []);

 val local_naming = default_naming |> add_path "local";

 (* full name *)

 fun err_bad binding = error (Binding.bad binding);

 fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal

   | transform_binding _ = I;

 fun name_spec (naming as Naming {path, ...}) raw_binding =

   let

     val binding = transform_binding naming raw_binding;

     val (concealed, prefix, name) = Binding.dest binding;

     val _ = Long_Name.is_qualified name andalso err_bad binding;

     val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);

     val spec2 = if name = "" then [] else [(name, true)];

     val spec = spec1 @ spec2;

     val _ =

       exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec

       andalso err_bad binding;

   in (concealed, if null spec2 then [] else spec) end;

 fun full_name naming =

   name_spec naming #> #2 #> map #1 #> Long_Name.implode;

 (* accesses *)

 fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;

 fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs

 and mandatory_prefixes1 [] = []

   | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)

   | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);

 fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));

 fun accesses naming binding =

   let

     val spec = #2 (name_spec naming binding);

     val sfxs = mandatory_suffixes spec;

     val pfxs = mandatory_prefixes spec;

   in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;

 (* alias *)

 fun alias naming binding name space =

   let

     val (accs, accs') = accesses naming binding;

     val space' = space

       |> fold (add_name name) accs

       |> map_name_space (fn (kind, internals, entries) =>

         let

           val _ = Symtab.defined entries name orelse error (undefined kind name);

           val entries' = entries

             |> Symtab.map_entry name (fn (externals, entry) =>

               (Library.merge (op =) (externals, accs'), entry))

         in (kind, internals, entries') end);

   in space' end;

 (** context naming **)

 structure Data_Args =

 struct

   type T = naming;

   val empty = default_naming;

   fun extend _ = default_naming;

   fun merge _ = default_naming;

   fun init _ = local_naming;

 end;

 structure Global_Naming = Theory_Data(Data_Args);

 structure Local_Naming = Proof_Data(Data_Args);

 fun naming_of (Context.Theory thy) = Global_Naming.get thy

   | naming_of (Context.Proof ctxt) = Local_Naming.get ctxt;

 fun map_naming f (Context.Theory thy) = Context.Theory (Global_Naming.map f thy)

   | map_naming f (Context.Proof ctxt) = Context.Proof (Local_Naming.map f ctxt);

 (** entry definition **)

 (* declaration *)

 fun new_entry strict (name, (externals, entry)) =

   map_name_space (fn (kind, internals, entries) =>

     let

       val entries' =

         (if strict then Symtab.update_new else Symtab.update) (name, (externals, entry)) entries

           handle Symtab.DUP dup =>

             err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);

     in (kind, internals, entries') end);

 fun declare context strict binding space =

   let

     val naming = naming_of context;

     val Naming {group, theory_name, ...} = naming;

     val (concealed, spec) = name_spec naming binding;

     val (accs, accs') = accesses naming binding;

     val name = Long_Name.implode (map fst spec);

     val _ = name = "" andalso err_bad binding;

     val pos = Position.default (Binding.pos_of binding);

     val entry =

      {concealed = concealed,

       group = group,

       theory_name = theory_name,

       pos = pos,

       id = serial ()};

     val space' = space

       |> fold (add_name name) accs

       |> new_entry strict (name, (accs', entry));

     val _ =

       Context_Position.report_generic context pos

         (entry_markup true (kind_of space) (name, entry));

   in (name, space') end;

 (* definition in symbol table *)

 type 'a table = T * 'a Symtab.table;

 fun check context (space, tab) (xname, pos) =

   let val name = intern space xname in

     (case Symtab.lookup tab name of

       SOME x => (Context_Position.report_generic context pos (markup space name); (name, x))

     | NONE => error (undefined (kind_of space) name ^ Position.str_of pos))

   end;

 fun get (space, tab) name =

   (case Symtab.lookup tab name of

     SOME x => x

   | NONE => error (undefined (kind_of space) name));

 fun define context strict (binding, x) (space, tab) =

   let val (name, space') = declare context strict binding space

   in (name, (space', Symtab.update (name, x) tab)) end;

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

 fun merge_tables ((space1, tab1), (space2, tab2)) =

   (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));

 fun join_tables f ((space1, tab1), (space2, tab2)) =

   (merge (space1, space2), Symtab.join f (tab1, tab2));

 fun ext_table ctxt (space, tab) =

   Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []

   |> Library.sort_wrt (#2 o #1);

 fun dest_table ctxt tab = map (apfst #1) (ext_table ctxt tab);

 fun extern_table ctxt tab = map (apfst #2) (ext_table ctxt tab);

 end;