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