(*  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;