wenzelm@20089: (*  Title:      Pure/name.ML
wenzelm@20089:     Author:     Makarius
wenzelm@20089: 
haftmann@28965: Names of basic logical entities (variables etc.).
wenzelm@20089: *)
wenzelm@20089: 
wenzelm@20089: signature NAME =
wenzelm@20089: sig
wenzelm@24849:   val uu: string
wenzelm@24849:   val aT: string
wenzelm@20089:   val bound: int -> string
wenzelm@20089:   val is_bound: string -> bool
wenzelm@20089:   val internal: string -> string
wenzelm@20089:   val dest_internal: string -> string
wenzelm@20089:   val skolem: string -> string
wenzelm@20089:   val dest_skolem: string -> string
wenzelm@20089:   val clean_index: string * int -> string * int
wenzelm@20089:   val clean: string -> string
wenzelm@20089:   type context
wenzelm@20089:   val context: context
wenzelm@20158:   val make_context: string list -> context
wenzelm@20089:   val declare: string -> context -> context
wenzelm@20158:   val is_declared: context -> string -> bool
wenzelm@20089:   val invents: context -> string -> int -> string list
haftmann@20192:   val names: context -> string -> 'a list -> (string * 'a) list
wenzelm@20089:   val invent_list: string list -> string -> int -> string list
wenzelm@20089:   val variants: string list -> context -> string list * context
wenzelm@20089:   val variant_list: string list -> string list -> string list
wenzelm@20089:   val variant: string list -> string -> string
wenzelm@20089: end;
wenzelm@20089: 
wenzelm@20089: structure Name: NAME =
wenzelm@20089: struct
wenzelm@20089: 
wenzelm@24849: (** common defaults **)
wenzelm@24849: 
wenzelm@24849: val uu = "uu";
wenzelm@24849: val aT = "'a";
wenzelm@24849: 
wenzelm@24849: 
wenzelm@20089: 
wenzelm@20089: (** special variable names **)
wenzelm@20089: 
wenzelm@20089: (* encoded bounds *)
wenzelm@20089: 
wenzelm@20089: (*names for numbered variables --
wenzelm@20089:   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
wenzelm@20089: 
wenzelm@20089: val small_int = Vector.tabulate (1000, fn i =>
wenzelm@20089:   let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
wenzelm@20089:   in ":" ^ leading ^ string_of_int i end);
wenzelm@20089: 
wenzelm@20089: fun bound n =
wenzelm@20089:   if n < 1000 then Vector.sub (small_int, n)
wenzelm@20089:   else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
wenzelm@20089: 
wenzelm@20089: val is_bound = String.isPrefix ":";
wenzelm@20089: 
wenzelm@20089: 
wenzelm@20089: (* internal names *)
wenzelm@20089: 
wenzelm@20089: val internal = suffix "_";
wenzelm@20089: val dest_internal = unsuffix "_";
wenzelm@20089: 
wenzelm@20089: val skolem = suffix "__";
wenzelm@20089: val dest_skolem = unsuffix "__";
wenzelm@20089: 
wenzelm@20099: fun clean_index (x, i) =
wenzelm@20099:   (case try dest_internal x of
wenzelm@20099:     NONE => (x, i)
wenzelm@20099:   | SOME x' => clean_index (x', i + 1));
wenzelm@20089: 
wenzelm@20089: fun clean x = #1 (clean_index (x, 0));
wenzelm@20089: 
wenzelm@20089: 
wenzelm@20089: 
wenzelm@20089: (** generating fresh names **)
wenzelm@20089: 
wenzelm@20089: (* context *)
wenzelm@20089: 
wenzelm@20089: datatype context =
wenzelm@20089:   Context of string option Symtab.table;    (*declared names with latest renaming*)
wenzelm@20089: 
wenzelm@20099: fun declare x (Context tab) =
wenzelm@20099:   Context (Symtab.default (clean x, NONE) tab);
wenzelm@20099: 
wenzelm@20099: fun declare_renaming (x, x') (Context tab) =
wenzelm@20099:   Context (Symtab.update (clean x, SOME (clean x')) tab);
wenzelm@20089: 
wenzelm@20158: fun is_declared (Context tab) = Symtab.defined tab;
wenzelm@20089: fun declared (Context tab) = Symtab.lookup tab;
wenzelm@20089: 
wenzelm@20121: val context = Context Symtab.empty |> fold declare ["", "'"];
wenzelm@20089: fun make_context used = fold declare used context;
wenzelm@20089: 
wenzelm@20089: 
wenzelm@20089: (* invents *)
wenzelm@20089: 
wenzelm@20089: fun invents ctxt =
wenzelm@20089:   let
wenzelm@20089:     fun invs _ 0 = []
wenzelm@20089:       | invs x n =
wenzelm@20089:           let val x' = Symbol.bump_string x in
wenzelm@20158:             if is_declared ctxt x then invs x' n
wenzelm@20089:             else x :: invs x' (n - 1)
wenzelm@20089:           end;
wenzelm@20099:   in invs o clean end;
wenzelm@20089: 
wenzelm@20198: fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
wenzelm@20198: 
wenzelm@20089: val invent_list = invents o make_context;
wenzelm@20089: 
wenzelm@20089: 
wenzelm@20089: (* variants *)
wenzelm@20089: 
wenzelm@20089: (*makes a variant of a name distinct from already used names in a
wenzelm@20089:   context; preserves a suffix of underscores "_"*)
wenzelm@20089: val variants = fold_map (fn name => fn ctxt =>
wenzelm@20089:   let
wenzelm@20089:     fun vary x =
wenzelm@20089:       (case declared ctxt x of
wenzelm@20089:         NONE => x
wenzelm@20089:       | SOME x' => vary (Symbol.bump_string (the_default x x')));
wenzelm@20089: 
wenzelm@20121:     val (x, n) = clean_index (name, 0);
wenzelm@20089:     val (x', ctxt') =
wenzelm@20158:       if not (is_declared ctxt x) then (x, declare x ctxt)
wenzelm@20089:       else
wenzelm@20089:         let
wenzelm@20089:           val x0 = Symbol.bump_init x;
wenzelm@20089:           val x' = vary x0;
wenzelm@20089:           val ctxt' = ctxt
wenzelm@21565:             |> x0 <> x' ? declare_renaming (x0, x')
wenzelm@20089:             |> declare x';
wenzelm@20089:         in (x', ctxt') end;
wenzelm@20089:   in (x' ^ replicate_string n "_", ctxt') end);
wenzelm@20089: 
wenzelm@20089: fun variant_list used names = #1 (make_context used |> variants names);
wenzelm@20089: fun variant used = singleton (variant_list used);
wenzelm@20089: 
wenzelm@20089: end;