src/Pure/name.ML
author wenzelm
Mon Mar 10 15:04:01 2014 +0100 (2014-03-10)
changeset 56026 893fe12639bc
parent 55949 4766342e8376
child 56811 b66639331db5
permissions -rw-r--r--
tuned signature -- prefer Name_Space.get with its builtin error;
     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 uu_: string
    11   val aT: string
    12   val bound: int -> string
    13   val is_bound: string -> bool
    14   val internal: string -> string
    15   val dest_internal: string -> string
    16   val is_internal: string -> bool
    17   val reject_internal: string * Position.T list -> unit
    18   val skolem: string -> string
    19   val dest_skolem: string -> string
    20   val is_skolem: string -> bool
    21   val reject_skolem: string * Position.T list -> unit
    22   val clean_index: string * int -> string * int
    23   val clean: string -> string
    24   type context
    25   val context: context
    26   val make_context: string list -> context
    27   val declare: string -> context -> context
    28   val is_declared: context -> string -> bool
    29   val invent: context -> string -> int -> string list
    30   val invent_names: context -> string -> 'a list -> (string * 'a) list
    31   val invent_list: string list -> string -> int -> string list
    32   val variant: string -> context -> string * context
    33   val variant_list: string list -> string list -> string list
    34   val desymbolize: bool -> string -> string
    35 end;
    36 
    37 structure Name: NAME =
    38 struct
    39 
    40 (** common defaults **)
    41 
    42 val uu = "uu";
    43 val uu_ = "uu_";
    44 val aT = "'a";
    45 
    46 
    47 
    48 (** special variable names **)
    49 
    50 (* encoded bounds *)
    51 
    52 (*names for numbered variables --
    53   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
    54 
    55 val small_int = Vector.tabulate (1000, fn i =>
    56   let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
    57   in ":" ^ leading ^ string_of_int i end);
    58 
    59 fun bound n =
    60   if n < 1000 then Vector.sub (small_int, n)
    61   else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
    62 
    63 val is_bound = String.isPrefix ":";
    64 
    65 
    66 (* internal names -- NB: internal subsumes skolem *)
    67 
    68 val internal = suffix "_";
    69 val dest_internal = unsuffix "_";
    70 val is_internal = String.isSuffix "_";
    71 fun reject_internal (x, ps) =
    72   if is_internal x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
    73 
    74 val skolem = suffix "__";
    75 val dest_skolem = unsuffix "__";
    76 val is_skolem = String.isSuffix "__";
    77 fun reject_skolem (x, ps) =
    78   if is_skolem x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
    79 
    80 fun clean_index (x, i) =
    81   (case try dest_internal x of
    82     NONE => (x, i)
    83   | SOME x' => clean_index (x', i + 1));
    84 
    85 fun clean x = #1 (clean_index (x, 0));
    86 
    87 
    88 
    89 (** generating fresh names **)
    90 
    91 (* context *)
    92 
    93 datatype context =
    94   Context of string option Symtab.table;    (*declared names with latest renaming*)
    95 
    96 fun declare x (Context tab) =
    97   Context (Symtab.default (clean x, NONE) tab);
    98 
    99 fun declare_renaming (x, x') (Context tab) =
   100   Context (Symtab.update (clean x, SOME (clean x')) tab);
   101 
   102 fun is_declared (Context tab) = Symtab.defined tab;
   103 fun declared (Context tab) = Symtab.lookup tab;
   104 
   105 val context = Context Symtab.empty |> fold declare ["", "'"];
   106 fun make_context used = fold declare used context;
   107 
   108 
   109 (* invent names *)
   110 
   111 fun invent ctxt =
   112   let
   113     fun invs _ 0 = []
   114       | invs x n =
   115           let val x' = Symbol.bump_string x
   116           in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end;
   117   in invs o clean end;
   118 
   119 fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs;
   120 
   121 val invent_list = invent o make_context;
   122 
   123 
   124 (* variants *)
   125 
   126 (*makes a variant of a name distinct from already used names in a
   127   context; preserves a suffix of underscores "_"*)
   128 fun variant name ctxt =
   129   let
   130     fun vary x =
   131       (case declared ctxt x of
   132         NONE => x
   133       | SOME x' => vary (Symbol.bump_string (the_default x x')));
   134 
   135     val (x, n) = clean_index (name, 0);
   136     val (x', ctxt') =
   137       if not (is_declared ctxt x) then (x, declare x ctxt)
   138       else
   139         let
   140           val x0 = Symbol.bump_init x;
   141           val x' = vary x0;
   142           val ctxt' = ctxt
   143             |> x0 <> x' ? declare_renaming (x0, x')
   144             |> declare x';
   145         in (x', ctxt') end;
   146   in (x' ^ replicate_string n "_", ctxt') end;
   147 
   148 fun variant_list used names = #1 (make_context used |> fold_map variant names);
   149 
   150 
   151 (* names conforming to typical requirements of identifiers in the world outside *)
   152 
   153 fun desymbolize upper "" = if upper then "X" else "x"
   154   | desymbolize upper s =
   155       let
   156         val xs as (x :: _) = Symbol.explode s;
   157         val ys =
   158           if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
   159           else "x" :: xs;
   160         fun is_valid x =
   161           Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x;
   162         fun sep [] = []
   163           | sep (xs as "_" :: _) = xs
   164           | sep xs = "_" :: xs;
   165         fun desep ("_" :: xs) = xs
   166           | desep xs = xs;
   167         fun desymb x xs =
   168           if is_valid x then x :: xs
   169           else
   170             (case Symbol.decode x of
   171               Symbol.Sym name => "_" :: raw_explode name @ sep xs
   172             | _ => sep xs);
   173         fun upper_lower cs =
   174           if upper then nth_map 0 Symbol.to_ascii_upper cs
   175           else
   176             (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
   177               Symbol.to_ascii_lower cs;
   178       in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
   179 
   180 end;