src/Pure/name.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24849 193a10e6bf90
child 28075 a45ce1bae4e0
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      Pure/name.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Names of basic logical entities (variables etc.).
     6 *)
     7 
     8 signature NAME =
     9 sig
    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 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 end;
    32 
    33 structure Name: NAME =
    34 struct
    35 
    36 (** common defaults **)
    37 
    38 val uu = "uu";
    39 val aT = "'a";
    40 
    41 
    42 
    43 (** special variable names **)
    44 
    45 (* encoded bounds *)
    46 
    47 (*names for numbered variables --
    48   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
    49 
    50 val small_int = Vector.tabulate (1000, fn i =>
    51   let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
    52   in ":" ^ leading ^ string_of_int i end);
    53 
    54 fun bound n =
    55   if n < 1000 then Vector.sub (small_int, n)
    56   else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
    57 
    58 val is_bound = String.isPrefix ":";
    59 
    60 
    61 (* internal names *)
    62 
    63 val internal = suffix "_";
    64 val dest_internal = unsuffix "_";
    65 
    66 val skolem = suffix "__";
    67 val dest_skolem = unsuffix "__";
    68 
    69 fun clean_index (x, i) =
    70   (case try dest_internal x of
    71     NONE => (x, i)
    72   | SOME x' => clean_index (x', i + 1));
    73 
    74 fun clean x = #1 (clean_index (x, 0));
    75 
    76 
    77 
    78 (** generating fresh names **)
    79 
    80 (* context *)
    81 
    82 datatype context =
    83   Context of string option Symtab.table;    (*declared names with latest renaming*)
    84 
    85 fun declare x (Context tab) =
    86   Context (Symtab.default (clean x, NONE) tab);
    87 
    88 fun declare_renaming (x, x') (Context tab) =
    89   Context (Symtab.update (clean x, SOME (clean x')) tab);
    90 
    91 fun is_declared (Context tab) = Symtab.defined tab;
    92 fun declared (Context tab) = Symtab.lookup tab;
    93 
    94 val context = Context Symtab.empty |> fold declare ["", "'"];
    95 fun make_context used = fold declare used context;
    96 
    97 
    98 (* invents *)
    99 
   100 fun invents ctxt =
   101   let
   102     fun invs _ 0 = []
   103       | invs x n =
   104           let val x' = Symbol.bump_string x in
   105             if is_declared ctxt x then invs x' n
   106             else x :: invs x' (n - 1)
   107           end;
   108   in invs o clean end;
   109 
   110 fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
   111 
   112 val invent_list = invents o make_context;
   113 
   114 
   115 (* variants *)
   116 
   117 (*makes a variant of a name distinct from already used names in a
   118   context; preserves a suffix of underscores "_"*)
   119 val variants = fold_map (fn name => fn ctxt =>
   120   let
   121     fun vary x =
   122       (case declared ctxt x of
   123         NONE => x
   124       | SOME x' => vary (Symbol.bump_string (the_default x x')));
   125 
   126     val (x, n) = clean_index (name, 0);
   127     val (x', ctxt') =
   128       if not (is_declared ctxt x) then (x, declare x ctxt)
   129       else
   130         let
   131           val x0 = Symbol.bump_init x;
   132           val x' = vary x0;
   133           val ctxt' = ctxt
   134             |> x0 <> x' ? declare_renaming (x0, x')
   135             |> declare x';
   136         in (x', ctxt') end;
   137   in (x' ^ replicate_string n "_", ctxt') end);
   138 
   139 fun variant_list used names = #1 (make_context used |> variants names);
   140 fun variant used = singleton (variant_list used);
   141 
   142 end;