src/Pure/name.ML
author wenzelm
Sat Oct 24 19:47:37 2009 +0200 (2009-10-24)
changeset 33095 bbd52d2f8696
parent 31035 de0a20a030fd
child 33547 edfc35dcfe31
permissions -rw-r--r--
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
     1 (*  Title:      Pure/name.ML
     2     Author:     Makarius
     3 
     4 Names of basic logical entities (variables etc.).
     5 *)
     6 
     7 signature NAME =
     8 sig
     9   val uu: string
    10   val aT: string
    11   val of_binding: binding -> string
    12   val bound: int -> string
    13   val is_bound: string -> bool
    14   val internal: string -> string
    15   val dest_internal: string -> string
    16   val skolem: string -> string
    17   val dest_skolem: string -> string
    18   val clean_index: string * int -> string * int
    19   val clean: string -> string
    20   type context
    21   val context: context
    22   val make_context: string list -> context
    23   val declare: string -> context -> context
    24   val is_declared: context -> string -> bool
    25   val invents: context -> string -> int -> string list
    26   val names: context -> string -> 'a list -> (string * 'a) list
    27   val invent_list: string list -> string -> int -> string list
    28   val variants: string list -> context -> string list * context
    29   val variant_list: string list -> string list -> string list
    30   val variant: string list -> string -> string
    31   val desymbolize: bool -> string -> string
    32 end;
    33 
    34 structure Name: NAME =
    35 struct
    36 
    37 (** common defaults **)
    38 
    39 val uu = "uu";
    40 val aT = "'a";
    41 
    42 
    43 
    44 (** special variable names **)
    45 
    46 (* checked binding *)
    47 
    48 val of_binding = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
    49 
    50 
    51 (* encoded bounds *)
    52 
    53 (*names for numbered variables --
    54   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
    55 
    56 val small_int = Vector.tabulate (1000, fn i =>
    57   let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
    58   in ":" ^ leading ^ string_of_int i end);
    59 
    60 fun bound n =
    61   if n < 1000 then Vector.sub (small_int, n)
    62   else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
    63 
    64 val is_bound = String.isPrefix ":";
    65 
    66 
    67 (* internal names *)
    68 
    69 val internal = suffix "_";
    70 val dest_internal = unsuffix "_";
    71 
    72 val skolem = suffix "__";
    73 val dest_skolem = unsuffix "__";
    74 
    75 fun clean_index (x, i) =
    76   (case try dest_internal x of
    77     NONE => (x, i)
    78   | SOME x' => clean_index (x', i + 1));
    79 
    80 fun clean x = #1 (clean_index (x, 0));
    81 
    82 
    83 
    84 (** generating fresh names **)
    85 
    86 (* context *)
    87 
    88 datatype context =
    89   Context of string option Symtab.table;    (*declared names with latest renaming*)
    90 
    91 fun declare x (Context tab) =
    92   Context (Symtab.default (clean x, NONE) tab);
    93 
    94 fun declare_renaming (x, x') (Context tab) =
    95   Context (Symtab.update (clean x, SOME (clean x')) tab);
    96 
    97 fun is_declared (Context tab) = Symtab.defined tab;
    98 fun declared (Context tab) = Symtab.lookup tab;
    99 
   100 val context = Context Symtab.empty |> fold declare ["", "'"];
   101 fun make_context used = fold declare used context;
   102 
   103 
   104 (* invents *)
   105 
   106 fun invents ctxt =
   107   let
   108     fun invs _ 0 = []
   109       | invs x n =
   110           let val x' = Symbol.bump_string x in
   111             if is_declared ctxt x then invs x' n
   112             else x :: invs x' (n - 1)
   113           end;
   114   in invs o clean end;
   115 
   116 fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
   117 
   118 val invent_list = invents o make_context;
   119 
   120 
   121 (* variants *)
   122 
   123 (*makes a variant of a name distinct from already used names in a
   124   context; preserves a suffix of underscores "_"*)
   125 val variants = fold_map (fn name => fn ctxt =>
   126   let
   127     fun vary x =
   128       (case declared ctxt x of
   129         NONE => x
   130       | SOME x' => vary (Symbol.bump_string (the_default x x')));
   131 
   132     val (x, n) = clean_index (name, 0);
   133     val (x', ctxt') =
   134       if not (is_declared ctxt x) then (x, declare x ctxt)
   135       else
   136         let
   137           val x0 = Symbol.bump_init x;
   138           val x' = vary x0;
   139           val ctxt' = ctxt
   140             |> x0 <> x' ? declare_renaming (x0, x')
   141             |> declare x';
   142         in (x', ctxt') end;
   143   in (x' ^ replicate_string n "_", ctxt') end);
   144 
   145 fun variant_list used names = #1 (make_context used |> variants names);
   146 fun variant used = singleton (variant_list used);
   147 
   148 
   149 (* names conforming to typical requirements of identifiers in the world outside *)
   150 
   151 fun desymbolize upper "" = if upper then "X" else "x"
   152   | desymbolize upper s =
   153       let
   154         val xs as (x :: _) = Symbol.explode s;
   155         val ys = if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
   156           else "x" :: xs;
   157         fun is_valid x =
   158           Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "'";
   159         fun sep [] = []
   160           | sep (xs as "_" :: _) = xs
   161           | sep xs = "_" :: xs;
   162         fun desep ("_" :: xs) = xs
   163           | desep xs = xs;
   164         fun desymb x xs = if is_valid x
   165             then x :: xs
   166           else if Symbol.is_symbolic x
   167             then "_" :: explode (Symbol.name_of x) @ sep xs
   168           else
   169             sep xs
   170         fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
   171           else (if forall Symbol.is_ascii_upper cs
   172             then map else nth_map 0) Symbol.to_ascii_lower cs;
   173       in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
   174 
   175 end;