src/Pure/name.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29006 abe0f11cfa4e
child 30584 7e839627b9e7
permissions -rw-r--r--
use long names for old-style fold combinators;
     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 aT: string
    11   val bound: int -> string
    12   val is_bound: string -> bool
    13   val internal: string -> string
    14   val dest_internal: string -> string
    15   val skolem: string -> string
    16   val dest_skolem: string -> string
    17   val clean_index: string * int -> string * int
    18   val clean: string -> string
    19   type context
    20   val context: context
    21   val make_context: string list -> context
    22   val declare: string -> context -> context
    23   val is_declared: context -> string -> bool
    24   val invents: context -> string -> int -> string list
    25   val names: context -> string -> 'a list -> (string * 'a) list
    26   val invent_list: string list -> string -> int -> string list
    27   val variants: string list -> context -> string list * context
    28   val variant_list: string list -> string list -> string list
    29   val variant: string list -> string -> string
    30 end;
    31 
    32 structure Name: NAME =
    33 struct
    34 
    35 (** common defaults **)
    36 
    37 val uu = "uu";
    38 val aT = "'a";
    39 
    40 
    41 
    42 (** special variable names **)
    43 
    44 (* encoded bounds *)
    45 
    46 (*names for numbered variables --
    47   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
    48 
    49 val small_int = Vector.tabulate (1000, fn i =>
    50   let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
    51   in ":" ^ leading ^ string_of_int i end);
    52 
    53 fun bound n =
    54   if n < 1000 then Vector.sub (small_int, n)
    55   else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
    56 
    57 val is_bound = String.isPrefix ":";
    58 
    59 
    60 (* internal names *)
    61 
    62 val internal = suffix "_";
    63 val dest_internal = unsuffix "_";
    64 
    65 val skolem = suffix "__";
    66 val dest_skolem = unsuffix "__";
    67 
    68 fun clean_index (x, i) =
    69   (case try dest_internal x of
    70     NONE => (x, i)
    71   | SOME x' => clean_index (x', i + 1));
    72 
    73 fun clean x = #1 (clean_index (x, 0));
    74 
    75 
    76 
    77 (** generating fresh names **)
    78 
    79 (* context *)
    80 
    81 datatype context =
    82   Context of string option Symtab.table;    (*declared names with latest renaming*)
    83 
    84 fun declare x (Context tab) =
    85   Context (Symtab.default (clean x, NONE) tab);
    86 
    87 fun declare_renaming (x, x') (Context tab) =
    88   Context (Symtab.update (clean x, SOME (clean x')) tab);
    89 
    90 fun is_declared (Context tab) = Symtab.defined tab;
    91 fun declared (Context tab) = Symtab.lookup tab;
    92 
    93 val context = Context Symtab.empty |> fold declare ["", "'"];
    94 fun make_context used = fold declare used context;
    95 
    96 
    97 (* invents *)
    98 
    99 fun invents ctxt =
   100   let
   101     fun invs _ 0 = []
   102       | invs x n =
   103           let val x' = Symbol.bump_string x in
   104             if is_declared ctxt x then invs x' n
   105             else x :: invs x' (n - 1)
   106           end;
   107   in invs o clean end;
   108 
   109 fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
   110 
   111 val invent_list = invents 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 val variants = fold_map (fn name => fn 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 |> variants names);
   139 fun variant used = singleton (variant_list used);
   140 
   141 end;