src/Pure/name.ML
author haftmann
Fri Jul 21 14:45:25 2006 +0200 (2006-07-21)
changeset 20174 c057b3618963
parent 20158 b71f4f4c6b1e
child 20192 956cd30ef3be
permissions -rw-r--r--
added give_names and alphanum
wenzelm@20089
     1
(*  Title:      Pure/name.ML
wenzelm@20089
     2
    ID:         $Id$
wenzelm@20089
     3
    Author:     Makarius
wenzelm@20089
     4
wenzelm@20089
     5
Names of basic logical entities (variables etc.).
wenzelm@20089
     6
*)
wenzelm@20089
     7
wenzelm@20089
     8
signature NAME =
wenzelm@20089
     9
sig
wenzelm@20089
    10
  val bound: int -> string
wenzelm@20089
    11
  val is_bound: string -> bool
wenzelm@20089
    12
  val internal: string -> string
wenzelm@20089
    13
  val dest_internal: string -> string
wenzelm@20089
    14
  val skolem: string -> string
wenzelm@20089
    15
  val dest_skolem: string -> string
wenzelm@20089
    16
  val clean_index: string * int -> string * int
wenzelm@20089
    17
  val clean: string -> string
wenzelm@20089
    18
  type context
wenzelm@20089
    19
  val context: context
wenzelm@20158
    20
  val make_context: string list -> context
wenzelm@20089
    21
  val declare: string -> context -> context
wenzelm@20158
    22
  val is_declared: context -> string -> bool
wenzelm@20089
    23
  val invents: context -> string -> int -> string list
haftmann@20174
    24
  val give_names: context -> string -> 'a list -> (string * 'a) list
wenzelm@20089
    25
  val invent_list: string list -> string -> int -> string list
wenzelm@20089
    26
  val variants: string list -> context -> string list * context
wenzelm@20089
    27
  val variant_list: string list -> string list -> string list
wenzelm@20089
    28
  val variant: string list -> string -> string
haftmann@20174
    29
  val alphanum: string -> string
wenzelm@20089
    30
end;
wenzelm@20089
    31
wenzelm@20089
    32
structure Name: NAME =
wenzelm@20089
    33
struct
wenzelm@20089
    34
wenzelm@20089
    35
wenzelm@20089
    36
(** special variable names **)
wenzelm@20089
    37
wenzelm@20089
    38
(* encoded bounds *)
wenzelm@20089
    39
wenzelm@20089
    40
(*names for numbered variables --
wenzelm@20089
    41
  preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
wenzelm@20089
    42
wenzelm@20089
    43
val small_int = Vector.tabulate (1000, fn i =>
wenzelm@20089
    44
  let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
wenzelm@20089
    45
  in ":" ^ leading ^ string_of_int i end);
wenzelm@20089
    46
wenzelm@20089
    47
fun bound n =
wenzelm@20089
    48
  if n < 1000 then Vector.sub (small_int, n)
wenzelm@20089
    49
  else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
wenzelm@20089
    50
wenzelm@20089
    51
val is_bound = String.isPrefix ":";
wenzelm@20089
    52
wenzelm@20089
    53
wenzelm@20089
    54
(* internal names *)
wenzelm@20089
    55
wenzelm@20089
    56
val internal = suffix "_";
wenzelm@20089
    57
val dest_internal = unsuffix "_";
wenzelm@20089
    58
wenzelm@20089
    59
val skolem = suffix "__";
wenzelm@20089
    60
val dest_skolem = unsuffix "__";
wenzelm@20089
    61
wenzelm@20099
    62
fun clean_index (x, i) =
wenzelm@20099
    63
  (case try dest_internal x of
wenzelm@20099
    64
    NONE => (x, i)
wenzelm@20099
    65
  | SOME x' => clean_index (x', i + 1));
wenzelm@20089
    66
wenzelm@20089
    67
fun clean x = #1 (clean_index (x, 0));
wenzelm@20089
    68
wenzelm@20089
    69
wenzelm@20089
    70
wenzelm@20089
    71
(** generating fresh names **)
wenzelm@20089
    72
wenzelm@20089
    73
(* context *)
wenzelm@20089
    74
wenzelm@20089
    75
datatype context =
wenzelm@20089
    76
  Context of string option Symtab.table;    (*declared names with latest renaming*)
wenzelm@20089
    77
wenzelm@20099
    78
fun declare x (Context tab) =
wenzelm@20099
    79
  Context (Symtab.default (clean x, NONE) tab);
wenzelm@20099
    80
wenzelm@20099
    81
fun declare_renaming (x, x') (Context tab) =
wenzelm@20099
    82
  Context (Symtab.update (clean x, SOME (clean x')) tab);
wenzelm@20089
    83
wenzelm@20158
    84
fun is_declared (Context tab) = Symtab.defined tab;
wenzelm@20089
    85
fun declared (Context tab) = Symtab.lookup tab;
wenzelm@20089
    86
wenzelm@20121
    87
val context = Context Symtab.empty |> fold declare ["", "'"];
wenzelm@20089
    88
fun make_context used = fold declare used context;
wenzelm@20089
    89
wenzelm@20089
    90
wenzelm@20089
    91
(* invents *)
wenzelm@20089
    92
wenzelm@20089
    93
fun invents ctxt =
wenzelm@20089
    94
  let
wenzelm@20089
    95
    fun invs _ 0 = []
wenzelm@20089
    96
      | invs x n =
wenzelm@20089
    97
          let val x' = Symbol.bump_string x in
wenzelm@20158
    98
            if is_declared ctxt x then invs x' n
wenzelm@20089
    99
            else x :: invs x' (n - 1)
wenzelm@20089
   100
          end;
wenzelm@20099
   101
  in invs o clean end;
wenzelm@20089
   102
wenzelm@20089
   103
val invent_list = invents o make_context;
haftmann@20174
   104
fun give_names ctxt x xs = invents ctxt x (length xs) ~~ xs;
wenzelm@20089
   105
wenzelm@20089
   106
wenzelm@20089
   107
(* variants *)
wenzelm@20089
   108
wenzelm@20089
   109
(*makes a variant of a name distinct from already used names in a
wenzelm@20089
   110
  context; preserves a suffix of underscores "_"*)
wenzelm@20089
   111
val variants = fold_map (fn name => fn ctxt =>
wenzelm@20089
   112
  let
wenzelm@20089
   113
    fun vary x =
wenzelm@20089
   114
      (case declared ctxt x of
wenzelm@20089
   115
        NONE => x
wenzelm@20089
   116
      | SOME x' => vary (Symbol.bump_string (the_default x x')));
wenzelm@20089
   117
wenzelm@20121
   118
    val (x, n) = clean_index (name, 0);
wenzelm@20089
   119
    val (x', ctxt') =
wenzelm@20158
   120
      if not (is_declared ctxt x) then (x, declare x ctxt)
wenzelm@20089
   121
      else
wenzelm@20089
   122
        let
wenzelm@20089
   123
          val x0 = Symbol.bump_init x;
wenzelm@20089
   124
          val x' = vary x0;
wenzelm@20089
   125
          val ctxt' = ctxt
wenzelm@20089
   126
            |> K (x0 <> x') ? declare_renaming (x0, x')
wenzelm@20089
   127
            |> declare x';
wenzelm@20089
   128
        in (x', ctxt') end;
wenzelm@20089
   129
  in (x' ^ replicate_string n "_", ctxt') end);
wenzelm@20089
   130
wenzelm@20089
   131
fun variant_list used names = #1 (make_context used |> variants names);
wenzelm@20089
   132
fun variant used = singleton (variant_list used);
wenzelm@20089
   133
haftmann@20174
   134
haftmann@20174
   135
(*turning arbitrary names into alphanumerics*)
haftmann@20174
   136
haftmann@20174
   137
fun alphanum s =
haftmann@20174
   138
  let
haftmann@20174
   139
    fun replace_invalid c (last_inv, cs) =
haftmann@20174
   140
      if ((Char.isAlphaNum o the o Char.fromString) c orelse c = "'")
haftmann@20174
   141
        andalso not (NameSpace.separator = c)
haftmann@20174
   142
      then (false, if last_inv then c :: "_" :: cs else c :: cs)
haftmann@20174
   143
      else (true, cs);
haftmann@20174
   144
    fun prefix_num_empty [] = ["x"]
haftmann@20174
   145
      | prefix_num_empty (cs as c::_) =
haftmann@20174
   146
          if (Char.isDigit o the o Char.fromString) c
haftmann@20174
   147
          then "x" :: cs
haftmann@20174
   148
          else cs;
haftmann@20174
   149
    val (prefix, cs1) = case explode s of "'"::cs => ("'", cs) | cs => ("", cs);
haftmann@20174
   150
    val (_, cs2) = fold_rev replace_invalid cs1 (false, []);
haftmann@20174
   151
    val cs3 = prefix_num_empty cs2;
haftmann@20174
   152
  in implode (prefix :: cs3) end;
haftmann@20174
   153
wenzelm@20089
   154
end;