src/Pure/name.ML
author haftmann
Tue Apr 28 18:42:26 2009 +0200 (2009-04-28)
changeset 31013 69a476d6fea6
parent 30584 7e839627b9e7
child 31035 de0a20a030fd
permissions -rw-r--r--
Symbol.name_of and Name.desymbolize
wenzelm@20089
     1
(*  Title:      Pure/name.ML
wenzelm@20089
     2
    Author:     Makarius
wenzelm@20089
     3
haftmann@28965
     4
Names of basic logical entities (variables etc.).
wenzelm@20089
     5
*)
wenzelm@20089
     6
wenzelm@20089
     7
signature NAME =
wenzelm@20089
     8
sig
wenzelm@24849
     9
  val uu: string
wenzelm@24849
    10
  val aT: string
wenzelm@30584
    11
  val of_binding: binding -> string
wenzelm@20089
    12
  val bound: int -> string
wenzelm@20089
    13
  val is_bound: string -> bool
wenzelm@20089
    14
  val internal: string -> string
wenzelm@20089
    15
  val dest_internal: string -> string
wenzelm@20089
    16
  val skolem: string -> string
wenzelm@20089
    17
  val dest_skolem: string -> string
wenzelm@20089
    18
  val clean_index: string * int -> string * int
wenzelm@20089
    19
  val clean: string -> string
wenzelm@20089
    20
  type context
wenzelm@20089
    21
  val context: context
wenzelm@20158
    22
  val make_context: string list -> context
wenzelm@20089
    23
  val declare: string -> context -> context
wenzelm@20158
    24
  val is_declared: context -> string -> bool
wenzelm@20089
    25
  val invents: context -> string -> int -> string list
haftmann@20192
    26
  val names: context -> string -> 'a list -> (string * 'a) list
wenzelm@20089
    27
  val invent_list: string list -> string -> int -> string list
wenzelm@20089
    28
  val variants: string list -> context -> string list * context
wenzelm@20089
    29
  val variant_list: string list -> string list -> string list
wenzelm@20089
    30
  val variant: string list -> string -> string
haftmann@31013
    31
  val desymbolize: string -> string
wenzelm@20089
    32
end;
wenzelm@20089
    33
wenzelm@20089
    34
structure Name: NAME =
wenzelm@20089
    35
struct
wenzelm@20089
    36
wenzelm@24849
    37
(** common defaults **)
wenzelm@24849
    38
wenzelm@24849
    39
val uu = "uu";
wenzelm@24849
    40
val aT = "'a";
wenzelm@24849
    41
wenzelm@24849
    42
wenzelm@20089
    43
wenzelm@20089
    44
(** special variable names **)
wenzelm@20089
    45
wenzelm@30584
    46
(* checked binding *)
wenzelm@30584
    47
wenzelm@30584
    48
val of_binding = Long_Name.base_name o NameSpace.full_name NameSpace.default_naming;
wenzelm@30584
    49
wenzelm@30584
    50
wenzelm@20089
    51
(* encoded bounds *)
wenzelm@20089
    52
wenzelm@20089
    53
(*names for numbered variables --
wenzelm@20089
    54
  preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
wenzelm@20089
    55
wenzelm@20089
    56
val small_int = Vector.tabulate (1000, fn i =>
wenzelm@20089
    57
  let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
wenzelm@20089
    58
  in ":" ^ leading ^ string_of_int i end);
wenzelm@20089
    59
wenzelm@20089
    60
fun bound n =
wenzelm@20089
    61
  if n < 1000 then Vector.sub (small_int, n)
wenzelm@20089
    62
  else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
wenzelm@20089
    63
wenzelm@20089
    64
val is_bound = String.isPrefix ":";
wenzelm@20089
    65
wenzelm@20089
    66
wenzelm@20089
    67
(* internal names *)
wenzelm@20089
    68
wenzelm@20089
    69
val internal = suffix "_";
wenzelm@20089
    70
val dest_internal = unsuffix "_";
wenzelm@20089
    71
wenzelm@20089
    72
val skolem = suffix "__";
wenzelm@20089
    73
val dest_skolem = unsuffix "__";
wenzelm@20089
    74
wenzelm@20099
    75
fun clean_index (x, i) =
wenzelm@20099
    76
  (case try dest_internal x of
wenzelm@20099
    77
    NONE => (x, i)
wenzelm@20099
    78
  | SOME x' => clean_index (x', i + 1));
wenzelm@20089
    79
wenzelm@20089
    80
fun clean x = #1 (clean_index (x, 0));
wenzelm@20089
    81
wenzelm@20089
    82
wenzelm@20089
    83
wenzelm@20089
    84
(** generating fresh names **)
wenzelm@20089
    85
wenzelm@20089
    86
(* context *)
wenzelm@20089
    87
wenzelm@20089
    88
datatype context =
wenzelm@20089
    89
  Context of string option Symtab.table;    (*declared names with latest renaming*)
wenzelm@20089
    90
wenzelm@20099
    91
fun declare x (Context tab) =
wenzelm@20099
    92
  Context (Symtab.default (clean x, NONE) tab);
wenzelm@20099
    93
wenzelm@20099
    94
fun declare_renaming (x, x') (Context tab) =
wenzelm@20099
    95
  Context (Symtab.update (clean x, SOME (clean x')) tab);
wenzelm@20089
    96
wenzelm@20158
    97
fun is_declared (Context tab) = Symtab.defined tab;
wenzelm@20089
    98
fun declared (Context tab) = Symtab.lookup tab;
wenzelm@20089
    99
wenzelm@20121
   100
val context = Context Symtab.empty |> fold declare ["", "'"];
wenzelm@20089
   101
fun make_context used = fold declare used context;
wenzelm@20089
   102
wenzelm@20089
   103
wenzelm@20089
   104
(* invents *)
wenzelm@20089
   105
wenzelm@20089
   106
fun invents ctxt =
wenzelm@20089
   107
  let
wenzelm@20089
   108
    fun invs _ 0 = []
wenzelm@20089
   109
      | invs x n =
wenzelm@20089
   110
          let val x' = Symbol.bump_string x in
wenzelm@20158
   111
            if is_declared ctxt x then invs x' n
wenzelm@20089
   112
            else x :: invs x' (n - 1)
wenzelm@20089
   113
          end;
wenzelm@20099
   114
  in invs o clean end;
wenzelm@20089
   115
wenzelm@20198
   116
fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
wenzelm@20198
   117
wenzelm@20089
   118
val invent_list = invents o make_context;
wenzelm@20089
   119
wenzelm@20089
   120
wenzelm@20089
   121
(* variants *)
wenzelm@20089
   122
wenzelm@20089
   123
(*makes a variant of a name distinct from already used names in a
wenzelm@20089
   124
  context; preserves a suffix of underscores "_"*)
wenzelm@20089
   125
val variants = fold_map (fn name => fn ctxt =>
wenzelm@20089
   126
  let
wenzelm@20089
   127
    fun vary x =
wenzelm@20089
   128
      (case declared ctxt x of
wenzelm@20089
   129
        NONE => x
wenzelm@20089
   130
      | SOME x' => vary (Symbol.bump_string (the_default x x')));
wenzelm@20089
   131
wenzelm@20121
   132
    val (x, n) = clean_index (name, 0);
wenzelm@20089
   133
    val (x', ctxt') =
wenzelm@20158
   134
      if not (is_declared ctxt x) then (x, declare x ctxt)
wenzelm@20089
   135
      else
wenzelm@20089
   136
        let
wenzelm@20089
   137
          val x0 = Symbol.bump_init x;
wenzelm@20089
   138
          val x' = vary x0;
wenzelm@20089
   139
          val ctxt' = ctxt
wenzelm@21565
   140
            |> x0 <> x' ? declare_renaming (x0, x')
wenzelm@20089
   141
            |> declare x';
wenzelm@20089
   142
        in (x', ctxt') end;
wenzelm@20089
   143
  in (x' ^ replicate_string n "_", ctxt') end);
wenzelm@20089
   144
wenzelm@20089
   145
fun variant_list used names = #1 (make_context used |> variants names);
wenzelm@20089
   146
fun variant used = singleton (variant_list used);
wenzelm@20089
   147
haftmann@31013
   148
haftmann@31013
   149
(* names conforming to typical requirements of identifiers in the outside world *)
haftmann@31013
   150
haftmann@31013
   151
fun desymbolize "" = "x"
haftmann@31013
   152
  | desymbolize s =
haftmann@31013
   153
      let
haftmann@31013
   154
        val xs = Symbol.explode s;
haftmann@31013
   155
        val ys = if Symbol.is_ascii_letter (hd xs) then xs
haftmann@31013
   156
          else "x" :: xs;
haftmann@31013
   157
        fun is_valid x =
haftmann@31013
   158
          Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "'";
haftmann@31013
   159
        fun sep [] = []
haftmann@31013
   160
          | sep (xs as "_" :: _) = xs
haftmann@31013
   161
          | sep xs = "_" :: xs;
haftmann@31013
   162
        fun desymb x xs = if is_valid x
haftmann@31013
   163
            then x :: xs
haftmann@31013
   164
          else if Symbol.is_symbolic x
haftmann@31013
   165
            then "_" :: Symbol.name_of x :: sep xs 
haftmann@31013
   166
          else
haftmann@31013
   167
            sep xs
haftmann@31013
   168
      in implode (fold_rev desymb ys []) end;
haftmann@31013
   169
wenzelm@20089
   170
end;