src/Pure/name.ML
author blanchet
Fri, 20 Dec 2013 20:36:38 +0100
changeset 54838 16511f84913c
parent 43683 b5d1873449fb
child 55948 bb21b380f65d
permissions -rw-r--r--
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/name.ML
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
     3
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28941
diff changeset
     4
Names of basic logical entities (variables etc.).
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
     5
*)
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
     6
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
     7
signature NAME =
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
     8
sig
24849
193a10e6bf90 added uu, aT;
wenzelm
parents: 21565
diff changeset
     9
  val uu: string
43683
b5d1873449fb tuned errors;
wenzelm
parents: 43329
diff changeset
    10
  val uu_: string
24849
193a10e6bf90 added uu, aT;
wenzelm
parents: 21565
diff changeset
    11
  val aT: string
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    12
  val bound: int -> string
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    13
  val is_bound: string -> bool
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    14
  val internal: string -> string
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    15
  val dest_internal: string -> string
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    16
  val skolem: string -> string
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    17
  val dest_skolem: string -> string
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    18
  val clean_index: string * int -> string * int
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    19
  val clean: string -> string
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    20
  type context
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    21
  val context: context
20158
b71f4f4c6b1e export make_context, is_declared;
wenzelm
parents: 20121
diff changeset
    22
  val make_context: string list -> context
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    23
  val declare: string -> context -> context
20158
b71f4f4c6b1e export make_context, is_declared;
wenzelm
parents: 20121
diff changeset
    24
  val is_declared: context -> string -> bool
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
    25
  val invent: context -> string -> int -> string list
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
    26
  val invent_names: context -> string -> 'a list -> (string * 'a) list
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    27
  val invent_list: string list -> string -> int -> string list
43326
47cf4bc789aa simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents: 43324
diff changeset
    28
  val variant: string -> context -> string * context
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    29
  val variant_list: string list -> string list -> string list
31035
de0a20a030fd desymbolization with case selection
haftmann
parents: 31013
diff changeset
    30
  val desymbolize: bool -> string -> string
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    31
end;
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    32
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    33
structure Name: NAME =
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    34
struct
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    35
24849
193a10e6bf90 added uu, aT;
wenzelm
parents: 21565
diff changeset
    36
(** common defaults **)
193a10e6bf90 added uu, aT;
wenzelm
parents: 21565
diff changeset
    37
193a10e6bf90 added uu, aT;
wenzelm
parents: 21565
diff changeset
    38
val uu = "uu";
43683
b5d1873449fb tuned errors;
wenzelm
parents: 43329
diff changeset
    39
val uu_ = "uu_";
24849
193a10e6bf90 added uu, aT;
wenzelm
parents: 21565
diff changeset
    40
val aT = "'a";
193a10e6bf90 added uu, aT;
wenzelm
parents: 21565
diff changeset
    41
193a10e6bf90 added uu, aT;
wenzelm
parents: 21565
diff changeset
    42
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    43
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    44
(** special variable names **)
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    45
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    46
(* encoded bounds *)
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    47
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    48
(*names for numbered variables --
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    49
  preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    50
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    51
val small_int = Vector.tabulate (1000, fn i =>
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    52
  let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    53
  in ":" ^ leading ^ string_of_int i end);
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    54
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    55
fun bound n =
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    56
  if n < 1000 then Vector.sub (small_int, n)
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    57
  else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    58
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    59
val is_bound = String.isPrefix ":";
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    60
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    61
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    62
(* internal names *)
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    63
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    64
val internal = suffix "_";
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    65
val dest_internal = unsuffix "_";
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    66
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    67
val skolem = suffix "__";
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    68
val dest_skolem = unsuffix "__";
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    69
20099
bc3f9cb33645 clean: no special treatment of empty name;
wenzelm
parents: 20089
diff changeset
    70
fun clean_index (x, i) =
bc3f9cb33645 clean: no special treatment of empty name;
wenzelm
parents: 20089
diff changeset
    71
  (case try dest_internal x of
bc3f9cb33645 clean: no special treatment of empty name;
wenzelm
parents: 20089
diff changeset
    72
    NONE => (x, i)
bc3f9cb33645 clean: no special treatment of empty name;
wenzelm
parents: 20089
diff changeset
    73
  | SOME x' => clean_index (x', i + 1));
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    74
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    75
fun clean x = #1 (clean_index (x, 0));
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    76
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    77
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    78
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    79
(** generating fresh names **)
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    80
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    81
(* context *)
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    82
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    83
datatype context =
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    84
  Context of string option Symtab.table;    (*declared names with latest renaming*)
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    85
20099
bc3f9cb33645 clean: no special treatment of empty name;
wenzelm
parents: 20089
diff changeset
    86
fun declare x (Context tab) =
bc3f9cb33645 clean: no special treatment of empty name;
wenzelm
parents: 20089
diff changeset
    87
  Context (Symtab.default (clean x, NONE) tab);
bc3f9cb33645 clean: no special treatment of empty name;
wenzelm
parents: 20089
diff changeset
    88
bc3f9cb33645 clean: no special treatment of empty name;
wenzelm
parents: 20089
diff changeset
    89
fun declare_renaming (x, x') (Context tab) =
bc3f9cb33645 clean: no special treatment of empty name;
wenzelm
parents: 20089
diff changeset
    90
  Context (Symtab.update (clean x, SOME (clean x')) tab);
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    91
20158
b71f4f4c6b1e export make_context, is_declared;
wenzelm
parents: 20121
diff changeset
    92
fun is_declared (Context tab) = Symtab.defined tab;
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    93
fun declared (Context tab) = Symtab.lookup tab;
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    94
20121
848fc1a1d355 do not export make_context;
wenzelm
parents: 20104
diff changeset
    95
val context = Context Symtab.empty |> fold declare ["", "'"];
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    96
fun make_context used = fold declare used context;
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    97
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
    98
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
    99
(* invent names *)
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   100
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   101
fun invent ctxt =
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   102
  let
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   103
    fun invs _ 0 = []
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   104
      | invs x n =
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   105
          let val x' = Symbol.bump_string x
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   106
          in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end;
20099
bc3f9cb33645 clean: no special treatment of empty name;
wenzelm
parents: 20089
diff changeset
   107
  in invs o clean end;
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   108
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   109
fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs;
20198
wenzelm
parents: 20192
diff changeset
   110
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   111
val invent_list = invent o make_context;
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   112
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   113
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   114
(* variants *)
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   115
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   116
(*makes a variant of a name distinct from already used names in a
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   117
  context; preserves a suffix of underscores "_"*)
43326
47cf4bc789aa simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents: 43324
diff changeset
   118
fun variant name ctxt =
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   119
  let
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   120
    fun vary x =
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   121
      (case declared ctxt x of
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   122
        NONE => x
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   123
      | SOME x' => vary (Symbol.bump_string (the_default x x')));
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   124
20121
848fc1a1d355 do not export make_context;
wenzelm
parents: 20104
diff changeset
   125
    val (x, n) = clean_index (name, 0);
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   126
    val (x', ctxt') =
20158
b71f4f4c6b1e export make_context, is_declared;
wenzelm
parents: 20121
diff changeset
   127
      if not (is_declared ctxt x) then (x, declare x ctxt)
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   128
      else
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   129
        let
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   130
          val x0 = Symbol.bump_init x;
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   131
          val x' = vary x0;
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   132
          val ctxt' = ctxt
21565
bd28361f4c5b simplified '?' operator;
wenzelm
parents: 20198
diff changeset
   133
            |> x0 <> x' ? declare_renaming (x0, x')
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   134
            |> declare x';
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   135
        in (x', ctxt') end;
43326
47cf4bc789aa simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents: 43324
diff changeset
   136
  in (x' ^ replicate_string n "_", ctxt') end;
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   137
43326
47cf4bc789aa simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents: 43324
diff changeset
   138
fun variant_list used names = #1 (make_context used |> fold_map variant names);
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   139
31013
69a476d6fea6 Symbol.name_of and Name.desymbolize
haftmann
parents: 30584
diff changeset
   140
31035
de0a20a030fd desymbolization with case selection
haftmann
parents: 31013
diff changeset
   141
(* names conforming to typical requirements of identifiers in the world outside *)
31013
69a476d6fea6 Symbol.name_of and Name.desymbolize
haftmann
parents: 30584
diff changeset
   142
31035
de0a20a030fd desymbolization with case selection
haftmann
parents: 31013
diff changeset
   143
fun desymbolize upper "" = if upper then "X" else "x"
de0a20a030fd desymbolization with case selection
haftmann
parents: 31013
diff changeset
   144
  | desymbolize upper s =
31013
69a476d6fea6 Symbol.name_of and Name.desymbolize
haftmann
parents: 30584
diff changeset
   145
      let
31035
de0a20a030fd desymbolization with case selection
haftmann
parents: 31013
diff changeset
   146
        val xs as (x :: _) = Symbol.explode s;
33547
edfc35dcfe31 desymbolize: use Symbol.decode directly;
wenzelm
parents: 33095
diff changeset
   147
        val ys =
edfc35dcfe31 desymbolize: use Symbol.decode directly;
wenzelm
parents: 33095
diff changeset
   148
          if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
31013
69a476d6fea6 Symbol.name_of and Name.desymbolize
haftmann
parents: 30584
diff changeset
   149
          else "x" :: xs;
69a476d6fea6 Symbol.name_of and Name.desymbolize
haftmann
parents: 30584
diff changeset
   150
        fun is_valid x =
34307
9074aa7d06e0 single quote is not a valid letter any more
haftmann
parents: 33547
diff changeset
   151
          Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x;
31013
69a476d6fea6 Symbol.name_of and Name.desymbolize
haftmann
parents: 30584
diff changeset
   152
        fun sep [] = []
69a476d6fea6 Symbol.name_of and Name.desymbolize
haftmann
parents: 30584
diff changeset
   153
          | sep (xs as "_" :: _) = xs
69a476d6fea6 Symbol.name_of and Name.desymbolize
haftmann
parents: 30584
diff changeset
   154
          | sep xs = "_" :: xs;
31035
de0a20a030fd desymbolization with case selection
haftmann
parents: 31013
diff changeset
   155
        fun desep ("_" :: xs) = xs
de0a20a030fd desymbolization with case selection
haftmann
parents: 31013
diff changeset
   156
          | desep xs = xs;
33547
edfc35dcfe31 desymbolize: use Symbol.decode directly;
wenzelm
parents: 33095
diff changeset
   157
        fun desymb x xs =
edfc35dcfe31 desymbolize: use Symbol.decode directly;
wenzelm
parents: 33095
diff changeset
   158
          if is_valid x then x :: xs
31013
69a476d6fea6 Symbol.name_of and Name.desymbolize
haftmann
parents: 30584
diff changeset
   159
          else
33547
edfc35dcfe31 desymbolize: use Symbol.decode directly;
wenzelm
parents: 33095
diff changeset
   160
            (case Symbol.decode x of
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 34307
diff changeset
   161
              Symbol.Sym name => "_" :: raw_explode name @ sep xs
33547
edfc35dcfe31 desymbolize: use Symbol.decode directly;
wenzelm
parents: 33095
diff changeset
   162
            | _ => sep xs);
edfc35dcfe31 desymbolize: use Symbol.decode directly;
wenzelm
parents: 33095
diff changeset
   163
        fun upper_lower cs =
edfc35dcfe31 desymbolize: use Symbol.decode directly;
wenzelm
parents: 33095
diff changeset
   164
          if upper then nth_map 0 Symbol.to_ascii_upper cs
edfc35dcfe31 desymbolize: use Symbol.decode directly;
wenzelm
parents: 33095
diff changeset
   165
          else
edfc35dcfe31 desymbolize: use Symbol.decode directly;
wenzelm
parents: 33095
diff changeset
   166
            (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
edfc35dcfe31 desymbolize: use Symbol.decode directly;
wenzelm
parents: 33095
diff changeset
   167
              Symbol.to_ascii_lower cs;
31035
de0a20a030fd desymbolization with case selection
haftmann
parents: 31013
diff changeset
   168
      in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
31013
69a476d6fea6 Symbol.name_of and Name.desymbolize
haftmann
parents: 30584
diff changeset
   169
20089
d757ebadb0a2 Names of basic logical entities (variables etc.).
wenzelm
parents:
diff changeset
   170
end;