src/Pure/General/name_space.ML
changeset 28941 128459bd72d2
parent 28923 0a981c596372
child 28965 1de908189869
equal deleted inserted replaced
28940:df0cb410be35 28941:128459bd72d2
     1 (*  Title:      Pure/General/name_space.ML
     1 (*  Title:      Pure/General/name_space.ML
     2     ID:         $Id$
       
     3     Author:     Markus Wenzel, TU Muenchen
     2     Author:     Markus Wenzel, TU Muenchen
     4 
     3 
     5 Generic name spaces with declared and hidden entries.  Unknown names
     4 Generic name spaces with declared and hidden entries.  Unknown names
     6 are considered global; no support for absolute addressing.
     5 are considered global; no support for absolute addressing.
     7 *)
     6 *)
     8 
     7 
     9 type bstring = string;    (*names to be bound*)
     8 type bstring = string;    (*names to be bound*)
    10 type xstring = string;    (*external names*)
     9 type xstring = string;    (*external names*)
    11 
    10 
    12 signature BASIC_NAME_SPACE =
       
    13 sig
       
    14   val long_names: bool ref
       
    15   val short_names: bool ref
       
    16   val unique_names: bool ref
       
    17 end;
       
    18 
       
    19 signature NAME_BINDING =
       
    20 sig
       
    21   type binding
       
    22   val binding_pos: string * Position.T -> binding
       
    23   val binding: string -> binding
       
    24   val no_binding: binding
       
    25   val dest_binding: binding -> (string * bool) list * string
       
    26   val is_nothing: binding -> bool
       
    27   val pos_of: binding -> Position.T
       
    28   val map_binding: ((string * bool) list * string -> (string * bool) list * string)
       
    29     -> binding -> binding
       
    30 end
       
    31 
       
    32 signature NAME_SPACE =
    11 signature NAME_SPACE =
    33 sig
    12 sig
    34   include BASIC_NAME_SPACE
    13   include BASIC_BINDING
    35   val hidden: string -> string
    14   val hidden: string -> string
    36   val is_hidden: string -> bool
    15   val is_hidden: string -> bool
    37   val separator: string                 (*single char*)
    16   val separator: string                 (*single char*)
    38   val is_qualified: string -> bool
    17   val is_qualified: string -> bool
    39   val implode: string list -> string
    18   val implode: string list -> string
    58   val default_naming: naming
    37   val default_naming: naming
    59   val add_path: string -> naming -> naming
    38   val add_path: string -> naming -> naming
    60   val no_base_names: naming -> naming
    39   val no_base_names: naming -> naming
    61   val qualified_names: naming -> naming
    40   val qualified_names: naming -> naming
    62   val sticky_prefix: string -> naming -> naming
    41   val sticky_prefix: string -> naming -> naming
    63   include NAME_BINDING
    42   val full_binding: naming -> Binding.T -> string
    64   val full_binding: naming -> binding -> string
    43   val declare_binding: naming -> Binding.T -> T -> string * T
    65   val declare_binding: naming -> binding -> T -> string * T
       
    66   type 'a table = T * 'a Symtab.table
    44   type 'a table = T * 'a Symtab.table
    67   val empty_table: 'a table
    45   val empty_table: 'a table
    68   val table_declare: naming -> binding * 'a
    46   val table_declare: naming -> Binding.T * 'a
    69     -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    47     -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    70   val table_declare_permissive: naming -> binding * 'a
    48   val table_declare_permissive: naming -> Binding.T * 'a
    71     -> 'a table -> string * 'a table
    49     -> 'a table -> string * 'a table
    72   val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
    50   val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
    73   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    51   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    74   val dest_table: 'a table -> (string * 'a) list
    52   val dest_table: 'a table -> (string * 'a) list
    75   val extern_table: 'a table -> (xstring * 'a) list
    53   val extern_table: 'a table -> (xstring * 'a) list
    76 end;
    54 end;
    77 
    55 
    78 structure NameSpace: NAME_SPACE =
    56 structure NameSpace: NAME_SPACE =
    79 struct
    57 struct
       
    58 
       
    59 open Basic_Binding;
       
    60 
    80 
    61 
    81 (** long identifiers **)
    62 (** long identifiers **)
    82 
    63 
    83 fun hidden name = "??." ^ name;
    64 fun hidden name = "??." ^ name;
    84 val is_hidden = String.isPrefix "??."
    65 val is_hidden = String.isPrefix "??."
   167 
   148 
   168 
   149 
   169 (* intern and extern *)
   150 (* intern and extern *)
   170 
   151 
   171 fun intern space xname = #1 (lookup space xname);
   152 fun intern space xname = #1 (lookup space xname);
   172 
       
   173 val long_names = ref false;
       
   174 val short_names = ref false;
       
   175 val unique_names = ref true;
       
   176 
   153 
   177 fun extern space name =
   154 fun extern space name =
   178   let
   155   let
   179     fun valid unique xname =
   156     fun valid unique xname =
   180       let val (name', uniq) = lookup space xname
   157       let val (name', uniq) = lookup space xname
   239         else (Library.merge (op =) (xnames1, xnames2), stamp ())));
   216         else (Library.merge (op =) (xnames1, xnames2), stamp ())));
   240   in NameSpace (tab', xtab') end;
   217   in NameSpace (tab', xtab') end;
   241 
   218 
   242 
   219 
   243 
   220 
   244 (** generic name bindings **)
       
   245 
       
   246 datatype binding = Binding of ((string * bool) list * string) * Position.T;
       
   247 
       
   248 fun binding_pos (name, pos) = Binding (([], name), pos);
       
   249 fun binding name = binding_pos (name, Position.none);
       
   250 val no_binding = binding "";
       
   251 
       
   252 fun pos_of (Binding (_, pos)) = pos;
       
   253 fun dest_binding (Binding (prefix_name, _)) = prefix_name;
       
   254 
       
   255 fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
       
   256 
       
   257 fun is_nothing (Binding ((_, name), _)) = name = "";
       
   258 
       
   259 
       
   260 
       
   261 (** naming contexts **)
   221 (** naming contexts **)
   262 
   222 
   263 (* datatype naming *)
   223 (* datatype naming *)
   264 
   224 
   265 datatype naming = Naming of
   225 datatype naming = Naming of
   319           orelse exists_string (fn s => s = "\"") name) andalso
   279           orelse exists_string (fn s => s = "\"") name) andalso
   320         error ("Bad name declaration " ^ quote name);
   280         error ("Bad name declaration " ^ quote name);
   321       val (accs, accs') = pairself (map implode_name) (accesses naming names);
   281       val (accs, accs') = pairself (map implode_name) (accesses naming names);
   322     in space |> fold (add_name name) accs |> put_accesses name accs' end;
   282     in space |> fold (add_name name) accs |> put_accesses name accs' end;
   323 
   283 
   324 fun declare_binding bnaming (Binding ((prefix, bname), _)) =
   284 fun declare_binding bnaming b =
   325   let
   285   let
       
   286     val (prefix, bname) = Binding.dest_binding b;
   326     val naming = apply_prefix prefix bnaming;
   287     val naming = apply_prefix prefix bnaming;
   327     val name = full naming bname;
   288     val name = full naming bname;
   328   in declare naming name #> pair name end;
   289   in declare naming name #> pair name end;
   329 
   290 
   330 
   291 
   341   in (name, (space', update (name, x) tab)) end;
   302   in (name, (space', update (name, x) tab)) end;
   342 
   303 
   343 fun table_declare naming = gen_table_declare Symtab.update_new naming;
   304 fun table_declare naming = gen_table_declare Symtab.update_new naming;
   344 fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
   305 fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
   345 
   306 
   346 fun full_binding naming (Binding ((prefix, bname), _)) =
   307 fun full_binding naming b =
   347   full (apply_prefix prefix naming) bname;
   308   let val (prefix, bname) = Binding.dest_binding b
       
   309   in full (apply_prefix prefix naming) bname end;
   348 
   310 
   349 fun extend_table naming bentries (space, tab) =
   311 fun extend_table naming bentries (space, tab) =
   350   let val entries = map (apfst (full naming)) bentries
   312   let val entries = map (apfst (full naming)) bentries
   351   in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
   313   in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
   352 
   314 
   364 (*final declarations of this structure!*)
   326 (*final declarations of this structure!*)
   365 val implode = implode_name;
   327 val implode = implode_name;
   366 val explode = explode_name;
   328 val explode = explode_name;
   367 
   329 
   368 end;
   330 end;
   369 
       
   370 structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
       
   371 open BasicNameSpace;