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