src/Pure/name.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (21 months ago)
changeset 66695 91500c024c7f
parent 56812 baef1c110f12
child 69137 90fce429e1bc
permissions -rw-r--r--
tuned;
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@43683
    10
  val uu_: string
wenzelm@24849
    11
  val aT: 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@55948
    16
  val is_internal: string -> bool
wenzelm@55949
    17
  val reject_internal: string * Position.T list -> unit
wenzelm@20089
    18
  val skolem: string -> string
wenzelm@20089
    19
  val dest_skolem: string -> string
wenzelm@55948
    20
  val is_skolem: string -> bool
wenzelm@55949
    21
  val reject_skolem: string * Position.T list -> unit
wenzelm@20089
    22
  val clean_index: string * int -> string * int
wenzelm@20089
    23
  val clean: string -> string
wenzelm@20089
    24
  type context
wenzelm@20089
    25
  val context: context
wenzelm@20158
    26
  val make_context: string list -> context
wenzelm@20089
    27
  val declare: string -> context -> context
wenzelm@20158
    28
  val is_declared: context -> string -> bool
wenzelm@43329
    29
  val invent: context -> string -> int -> string list
wenzelm@43329
    30
  val invent_names: context -> string -> 'a list -> (string * 'a) list
wenzelm@20089
    31
  val invent_list: string list -> string -> int -> string list
wenzelm@43326
    32
  val variant: string -> context -> string * context
wenzelm@20089
    33
  val variant_list: string list -> string list -> string list
haftmann@56812
    34
  val enforce_case: bool -> string -> string
haftmann@56811
    35
  val desymbolize: bool option -> string -> string
wenzelm@20089
    36
end;
wenzelm@20089
    37
wenzelm@20089
    38
structure Name: NAME =
wenzelm@20089
    39
struct
wenzelm@20089
    40
wenzelm@24849
    41
(** common defaults **)
wenzelm@24849
    42
wenzelm@24849
    43
val uu = "uu";
wenzelm@43683
    44
val uu_ = "uu_";
wenzelm@24849
    45
val aT = "'a";
wenzelm@24849
    46
wenzelm@24849
    47
wenzelm@20089
    48
wenzelm@20089
    49
(** special variable names **)
wenzelm@20089
    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@55949
    67
(* internal names -- NB: internal subsumes skolem *)
wenzelm@20089
    68
wenzelm@20089
    69
val internal = suffix "_";
wenzelm@20089
    70
val dest_internal = unsuffix "_";
wenzelm@55948
    71
val is_internal = String.isSuffix "_";
wenzelm@55949
    72
fun reject_internal (x, ps) =
wenzelm@55949
    73
  if is_internal x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
wenzelm@20089
    74
wenzelm@20089
    75
val skolem = suffix "__";
wenzelm@20089
    76
val dest_skolem = unsuffix "__";
wenzelm@55948
    77
val is_skolem = String.isSuffix "__";
wenzelm@55949
    78
fun reject_skolem (x, ps) =
wenzelm@55949
    79
  if is_skolem x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
wenzelm@20089
    80
wenzelm@20099
    81
fun clean_index (x, i) =
wenzelm@20099
    82
  (case try dest_internal x of
wenzelm@20099
    83
    NONE => (x, i)
wenzelm@20099
    84
  | SOME x' => clean_index (x', i + 1));
wenzelm@20089
    85
wenzelm@20089
    86
fun clean x = #1 (clean_index (x, 0));
wenzelm@20089
    87
wenzelm@20089
    88
wenzelm@20089
    89
wenzelm@20089
    90
(** generating fresh names **)
wenzelm@20089
    91
wenzelm@20089
    92
(* context *)
wenzelm@20089
    93
wenzelm@20089
    94
datatype context =
wenzelm@20089
    95
  Context of string option Symtab.table;    (*declared names with latest renaming*)
wenzelm@20089
    96
wenzelm@20099
    97
fun declare x (Context tab) =
wenzelm@20099
    98
  Context (Symtab.default (clean x, NONE) tab);
wenzelm@20099
    99
wenzelm@20099
   100
fun declare_renaming (x, x') (Context tab) =
wenzelm@20099
   101
  Context (Symtab.update (clean x, SOME (clean x')) tab);
wenzelm@20089
   102
wenzelm@20158
   103
fun is_declared (Context tab) = Symtab.defined tab;
wenzelm@20089
   104
fun declared (Context tab) = Symtab.lookup tab;
wenzelm@20089
   105
wenzelm@20121
   106
val context = Context Symtab.empty |> fold declare ["", "'"];
wenzelm@20089
   107
fun make_context used = fold declare used context;
wenzelm@20089
   108
wenzelm@20089
   109
wenzelm@43329
   110
(* invent names *)
wenzelm@20089
   111
wenzelm@43329
   112
fun invent ctxt =
wenzelm@20089
   113
  let
wenzelm@20089
   114
    fun invs _ 0 = []
wenzelm@20089
   115
      | invs x n =
wenzelm@43329
   116
          let val x' = Symbol.bump_string x
wenzelm@43329
   117
          in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end;
wenzelm@20099
   118
  in invs o clean end;
wenzelm@20089
   119
wenzelm@43329
   120
fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs;
wenzelm@20198
   121
wenzelm@43329
   122
val invent_list = invent o make_context;
wenzelm@20089
   123
wenzelm@20089
   124
wenzelm@20089
   125
(* variants *)
wenzelm@20089
   126
wenzelm@20089
   127
(*makes a variant of a name distinct from already used names in a
wenzelm@20089
   128
  context; preserves a suffix of underscores "_"*)
wenzelm@43326
   129
fun variant name ctxt =
wenzelm@20089
   130
  let
wenzelm@20089
   131
    fun vary x =
wenzelm@20089
   132
      (case declared ctxt x of
wenzelm@20089
   133
        NONE => x
wenzelm@20089
   134
      | SOME x' => vary (Symbol.bump_string (the_default x x')));
wenzelm@20089
   135
wenzelm@20121
   136
    val (x, n) = clean_index (name, 0);
wenzelm@20089
   137
    val (x', ctxt') =
wenzelm@20158
   138
      if not (is_declared ctxt x) then (x, declare x ctxt)
wenzelm@20089
   139
      else
wenzelm@20089
   140
        let
wenzelm@20089
   141
          val x0 = Symbol.bump_init x;
wenzelm@20089
   142
          val x' = vary x0;
wenzelm@20089
   143
          val ctxt' = ctxt
wenzelm@21565
   144
            |> x0 <> x' ? declare_renaming (x0, x')
wenzelm@20089
   145
            |> declare x';
wenzelm@20089
   146
        in (x', ctxt') end;
wenzelm@43326
   147
  in (x' ^ replicate_string n "_", ctxt') end;
wenzelm@20089
   148
wenzelm@43326
   149
fun variant_list used names = #1 (make_context used |> fold_map variant names);
wenzelm@20089
   150
haftmann@31013
   151
haftmann@31035
   152
(* names conforming to typical requirements of identifiers in the world outside *)
haftmann@31013
   153
haftmann@56812
   154
fun enforce_case' false cs = 
haftmann@56812
   155
      (if forall Symbol.is_ascii_upper cs then map else nth_map 0) Symbol.to_ascii_lower cs
haftmann@56812
   156
  | enforce_case' true cs = 
haftmann@56812
   157
      nth_map 0 Symbol.to_ascii_upper cs;
haftmann@56812
   158
haftmann@56812
   159
fun enforce_case upper = implode o enforce_case' upper o raw_explode;
haftmann@56812
   160
haftmann@56811
   161
fun desymbolize perhaps_upper "" =
haftmann@56811
   162
      if the_default false perhaps_upper then "X" else "x"
haftmann@56811
   163
  | desymbolize perhaps_upper s =
haftmann@31013
   164
      let
haftmann@31035
   165
        val xs as (x :: _) = Symbol.explode s;
wenzelm@33547
   166
        val ys =
wenzelm@33547
   167
          if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
haftmann@31013
   168
          else "x" :: xs;
haftmann@31013
   169
        fun is_valid x =
haftmann@34307
   170
          Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x;
haftmann@31013
   171
        fun sep [] = []
haftmann@31013
   172
          | sep (xs as "_" :: _) = xs
haftmann@31013
   173
          | sep xs = "_" :: xs;
haftmann@31035
   174
        fun desep ("_" :: xs) = xs
haftmann@31035
   175
          | desep xs = xs;
wenzelm@33547
   176
        fun desymb x xs =
wenzelm@33547
   177
          if is_valid x then x :: xs
haftmann@31013
   178
          else
wenzelm@33547
   179
            (case Symbol.decode x of
wenzelm@40627
   180
              Symbol.Sym name => "_" :: raw_explode name @ sep xs
wenzelm@33547
   181
            | _ => sep xs);
haftmann@56812
   182
        val upper_lower = Option.map enforce_case' perhaps_upper |> the_default I;
haftmann@31035
   183
      in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
haftmann@31013
   184
wenzelm@20089
   185
end;