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