src/Pure/name.ML
changeset 20089 d757ebadb0a2
child 20099 bc3f9cb33645
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/name.ML	Tue Jul 11 12:17:17 2006 +0200
     1.3 @@ -0,0 +1,127 @@
     1.4 +(*  Title:      Pure/name.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Names of basic logical entities (variables etc.).
     1.9 +*)
    1.10 +
    1.11 +signature NAME =
    1.12 +sig
    1.13 +  val bound: int -> string
    1.14 +  val is_bound: string -> bool
    1.15 +  val internal: string -> string
    1.16 +  val dest_internal: string -> string
    1.17 +  val skolem: string -> string
    1.18 +  val dest_skolem: string -> string
    1.19 +  val clean_index: string * int -> string * int
    1.20 +  val clean: string -> string
    1.21 +  type context
    1.22 +  val context: context
    1.23 +  val make_context: string list -> context
    1.24 +  val declare: string -> context -> context
    1.25 +  val invents: context -> string -> int -> string list
    1.26 +  val invent_list: string list -> string -> int -> string list
    1.27 +  val variants: string list -> context -> string list * context
    1.28 +  val variant_list: string list -> string list -> string list
    1.29 +  val variant: string list -> string -> string
    1.30 +end;
    1.31 +
    1.32 +structure Name: NAME =
    1.33 +struct
    1.34 +
    1.35 +
    1.36 +(** special variable names **)
    1.37 +
    1.38 +(* encoded bounds *)
    1.39 +
    1.40 +(*names for numbered variables --
    1.41 +  preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
    1.42 +
    1.43 +val small_int = Vector.tabulate (1000, fn i =>
    1.44 +  let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
    1.45 +  in ":" ^ leading ^ string_of_int i end);
    1.46 +
    1.47 +fun bound n =
    1.48 +  if n < 1000 then Vector.sub (small_int, n)
    1.49 +  else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
    1.50 +
    1.51 +val is_bound = String.isPrefix ":";
    1.52 +
    1.53 +
    1.54 +(* internal names *)
    1.55 +
    1.56 +val internal = suffix "_";
    1.57 +val dest_internal = unsuffix "_";
    1.58 +
    1.59 +val skolem = suffix "__";
    1.60 +val dest_skolem = unsuffix "__";
    1.61 +
    1.62 +fun clean_index ("", i) = ("u", i + 1)
    1.63 +  | clean_index (x, i) =
    1.64 +      (case try dest_internal x of
    1.65 +        NONE => (x, i)
    1.66 +      | SOME x' => clean_index (x', i + 1));
    1.67 +
    1.68 +fun clean x = #1 (clean_index (x, 0));
    1.69 +
    1.70 +
    1.71 +
    1.72 +(** generating fresh names **)
    1.73 +
    1.74 +(* context *)
    1.75 +
    1.76 +datatype context =
    1.77 +  Context of string option Symtab.table;    (*declared names with latest renaming*)
    1.78 +
    1.79 +fun declare x (Context tab) = Context (Symtab.default (x, NONE) tab);
    1.80 +fun declare_renaming (x, x') (Context tab) = Context (Symtab.update (x, SOME x') tab);
    1.81 +
    1.82 +fun declared (Context tab) = Symtab.lookup tab;
    1.83 +
    1.84 +val context = Context Symtab.empty;
    1.85 +fun make_context used = fold declare used context;
    1.86 +
    1.87 +
    1.88 +(* invents *)
    1.89 +
    1.90 +fun invents ctxt =
    1.91 +  let
    1.92 +    fun invs _ 0 = []
    1.93 +      | invs x n =
    1.94 +          let val x' = Symbol.bump_string x in
    1.95 +            if is_some (declared ctxt x) then invs x' n
    1.96 +            else x :: invs x' (n - 1)
    1.97 +          end;
    1.98 +  in invs end;
    1.99 +
   1.100 +val invent_list = invents o make_context;
   1.101 +
   1.102 +
   1.103 +(* variants *)
   1.104 +
   1.105 +(*makes a variant of a name distinct from already used names in a
   1.106 +  context; preserves a suffix of underscores "_"*)
   1.107 +val variants = fold_map (fn name => fn ctxt =>
   1.108 +  let
   1.109 +    fun vary x =
   1.110 +      (case declared ctxt x of
   1.111 +        NONE => x
   1.112 +      | SOME x' => vary (Symbol.bump_string (the_default x x')));
   1.113 +
   1.114 +    val (x, n) = clean_index (name, 0);
   1.115 +    val (x', ctxt') =
   1.116 +      if is_none (declared ctxt x) then (x, declare x ctxt)
   1.117 +      else
   1.118 +        let
   1.119 +          val x0 = Symbol.bump_init x;
   1.120 +          val x' = vary x0;
   1.121 +          val ctxt' = ctxt
   1.122 +            |> K (x0 <> x') ? declare_renaming (x0, x')
   1.123 +            |> declare x';
   1.124 +        in (x', ctxt') end;
   1.125 +  in (x' ^ replicate_string n "_", ctxt') end);
   1.126 +
   1.127 +fun variant_list used names = #1 (make_context used |> variants names);
   1.128 +fun variant used = singleton (variant_list used);
   1.129 +
   1.130 +end;