src/Pure/name.ML
author wenzelm
Tue Jul 11 23:00:36 2006 +0200 (2006-07-11)
changeset 20099 bc3f9cb33645
parent 20089 d757ebadb0a2
child 20104 f8e7c71926e4
permissions -rw-r--r--
clean: no special treatment of empty name;
declare, invent: clean arguments;
     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 bound: int -> string
    11   val is_bound: string -> bool
    12   val internal: string -> string
    13   val dest_internal: string -> string
    14   val skolem: string -> string
    15   val dest_skolem: string -> string
    16   val clean_index: string * int -> string * int
    17   val clean: string -> string
    18   type context
    19   val context: context
    20   val make_context: string list -> context
    21   val declare: string -> context -> context
    22   val invents: context -> string -> int -> string list
    23   val invent_list: string list -> string -> int -> string list
    24   val variants: string list -> context -> string list * context
    25   val variant_list: string list -> string list -> string list
    26   val variant: string list -> string -> string
    27 end;
    28 
    29 structure Name: NAME =
    30 struct
    31 
    32 
    33 (** special variable names **)
    34 
    35 (* encoded bounds *)
    36 
    37 (*names for numbered variables --
    38   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
    39 
    40 val small_int = Vector.tabulate (1000, fn i =>
    41   let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
    42   in ":" ^ leading ^ string_of_int i end);
    43 
    44 fun bound n =
    45   if n < 1000 then Vector.sub (small_int, n)
    46   else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
    47 
    48 val is_bound = String.isPrefix ":";
    49 
    50 
    51 (* internal names *)
    52 
    53 val internal = suffix "_";
    54 val dest_internal = unsuffix "_";
    55 
    56 val skolem = suffix "__";
    57 val dest_skolem = unsuffix "__";
    58 
    59 fun clean_index (x, i) =
    60   (case try dest_internal x of
    61     NONE => (x, i)
    62   | SOME x' => clean_index (x', i + 1));
    63 
    64 fun clean x = #1 (clean_index (x, 0));
    65 
    66 
    67 
    68 (** generating fresh names **)
    69 
    70 (* context *)
    71 
    72 datatype context =
    73   Context of string option Symtab.table;    (*declared names with latest renaming*)
    74 
    75 fun declare x (Context tab) =
    76   Context (Symtab.default (clean x, NONE) tab);
    77 
    78 fun declare_renaming (x, x') (Context tab) =
    79   Context (Symtab.update (clean x, SOME (clean x')) tab);
    80 
    81 fun declared (Context tab) = Symtab.lookup tab;
    82 
    83 val context = Context Symtab.empty;
    84 fun make_context used = fold declare used context;
    85 
    86 
    87 (* invents *)
    88 
    89 fun invents ctxt =
    90   let
    91     fun invs _ 0 = []
    92       | invs x n =
    93           let val x' = Symbol.bump_string x in
    94             if is_some (declared ctxt x) then invs x' n
    95             else x :: invs x' (n - 1)
    96           end;
    97   in invs o clean end;
    98 
    99 val invent_list = invents o make_context;
   100 
   101 
   102 (* variants *)
   103 
   104 (*makes a variant of a name distinct from already used names in a
   105   context; preserves a suffix of underscores "_"*)
   106 val variants = fold_map (fn name => fn ctxt =>
   107   let
   108     fun vary x =
   109       (case declared ctxt x of
   110         NONE => x
   111       | SOME x' => vary (Symbol.bump_string (the_default x x')));
   112 
   113     val (x, n) = clean_index (name, 0);
   114     val (x', ctxt') =
   115       if is_none (declared ctxt x) then (x, declare x ctxt)
   116       else
   117         let
   118           val x0 = Symbol.bump_init x;
   119           val x' = vary x0;
   120           val ctxt' = ctxt
   121             |> K (x0 <> x') ? declare_renaming (x0, x')
   122             |> declare x';
   123         in (x', ctxt') end;
   124   in (x' ^ replicate_string n "_", ctxt') end);
   125 
   126 fun variant_list used names = #1 (make_context used |> variants names);
   127 fun variant used = singleton (variant_list used);
   128 
   129 end;