src/Pure/name.ML
author wenzelm
Tue Jul 11 12:17:17 2006 +0200 (2006-07-11)
changeset 20089 d757ebadb0a2
child 20099 bc3f9cb33645
permissions -rw-r--r--
Names of basic logical entities (variables etc.).
     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 ("", i) = ("u", i + 1)
    60   | clean_index (x, i) =
    61       (case try dest_internal x of
    62         NONE => (x, i)
    63       | SOME x' => clean_index (x', i + 1));
    64 
    65 fun clean x = #1 (clean_index (x, 0));
    66 
    67 
    68 
    69 (** generating fresh names **)
    70 
    71 (* context *)
    72 
    73 datatype context =
    74   Context of string option Symtab.table;    (*declared names with latest renaming*)
    75 
    76 fun declare x (Context tab) = Context (Symtab.default (x, NONE) tab);
    77 fun declare_renaming (x, x') (Context tab) = Context (Symtab.update (x, SOME x') tab);
    78 
    79 fun declared (Context tab) = Symtab.lookup tab;
    80 
    81 val context = Context Symtab.empty;
    82 fun make_context used = fold declare used context;
    83 
    84 
    85 (* invents *)
    86 
    87 fun invents ctxt =
    88   let
    89     fun invs _ 0 = []
    90       | invs x n =
    91           let val x' = Symbol.bump_string x in
    92             if is_some (declared ctxt x) then invs x' n
    93             else x :: invs x' (n - 1)
    94           end;
    95   in invs end;
    96 
    97 val invent_list = invents o make_context;
    98 
    99 
   100 (* variants *)
   101 
   102 (*makes a variant of a name distinct from already used names in a
   103   context; preserves a suffix of underscores "_"*)
   104 val variants = fold_map (fn name => fn ctxt =>
   105   let
   106     fun vary x =
   107       (case declared ctxt x of
   108         NONE => x
   109       | SOME x' => vary (Symbol.bump_string (the_default x x')));
   110 
   111     val (x, n) = clean_index (name, 0);
   112     val (x', ctxt') =
   113       if is_none (declared ctxt x) then (x, declare x ctxt)
   114       else
   115         let
   116           val x0 = Symbol.bump_init x;
   117           val x' = vary x0;
   118           val ctxt' = ctxt
   119             |> K (x0 <> x') ? declare_renaming (x0, x')
   120             |> declare x';
   121         in (x', ctxt') end;
   122   in (x' ^ replicate_string n "_", ctxt') end);
   123 
   124 fun variant_list used names = #1 (make_context used |> variants names);
   125 fun variant used = singleton (variant_list used);
   126 
   127 end;