Quelle long_name.ML Sprache: SML

(*  Title:      Pure/General/long_name.ML
    Author:     Makarius

Long names.
*)

signature LONG_NAME =
sig
  val separator: string
  val append: string -> string -> string
  val qualify: string -> string -> string
  val is_qualified: string -> bool
  val qualifier: string -> string
  val base_name: string -> string
  val map_base_name: (string -> string) -> string -> string
  val count: string -> int
  val hidden: string -> string
  val is_hidden: string -> bool
  val dest_hidden: string -> string option
  val localN: string
  val dest_local: string -> string option
  val implode: string list -> string
  val explode: string -> string list
  type chunks
  val count_chunks: chunks -> int
  val size_chunks: chunks -> int
  val empty_chunks: chunks
  val is_empty_chunks: chunks -> bool
  val base_chunks: string -> chunks
  val suppress_chunks: int -> bool list -> string -> chunks
  val make_chunks: string -> chunks
  val explode_chunks: chunks -> string list
  val implode_chunks: chunks -> string
  val compare_chunks: chunks ord
  val eq_chunks: chunks * chunks -> bool
  structure Chunks: CHANGE_TABLE
end;

structure Long_Name: LONG_NAME =
struct

(* long names separated by "." *)

val separator = ".";
val separator_char = String.nth separator 0;

fun append name1 "" = name1
  | append "" name2 = name2
  | append name1 name2 = name1 ^ separator ^ name2;

fun qualify qual name =
  if qual = "" orelse name = "" then name
  else qual ^ separator ^ name;

fun last_separator name =
  let fun last i = if i < 0 orelse String.nth name i = separator_char then i else last (i - 1)
  in last (size name - 1) end;

fun is_qualified name = last_separator name >= 0;

fun qualifier name =
  let val i = last_separator name
  in if i < 0 then "" else String.substring (name, 0, i) end;

fun base_name name =
  let
    val i = last_separator name;
    val j = i + 1;
  in if i < 0 then name else String.substring (name, j, size name - j) end;

fun map_base_name f name =
  if name = "" then ""
  else qualify (qualifier name) (f (base_name name));

fun count "" = 0
  | count name = String.fold (fn c => c = separator_char ? Integer.add 1) name 1;

val hidden_prefix = "??.";
val hidden = prefix hidden_prefix;
val is_hidden = String.isPrefix hidden_prefix;
val dest_hidden = try (unprefix hidden_prefix);

val localN = "local";
val dest_local = try (unprefix "local.");

val implode = space_implode separator;
val explode = space_explode separator;

(* compact representation of chunks *)

local

fun failure string msg =
  raise Fail ("Malformed qualified name " ^ quote string ^ ":\n " ^ msg);

val range_limit = 32768;

val _ =
  if ML_Heap.sizeof1 (range_limit * (range_limit - 1)) = 0 then ()
  else raise Fail ("Bad Long_Name.range_limit for ML platform " ^ ML_System.platform);

fun range string index len =
  if len < range_limit then index * range_limit + len
  else failure string ("chunk length beyond " ^ string_of_int range_limit);

fun range_index r = r div range_limit;
fun range_length r = r mod range_limit;
fun range_string s r = String.substring (s, range_index r, range_length r);

in

abstype chunks = Chunks of {range0: int, ranges: int list (*reverse*), string: string}
with

val empty_chunks = Chunks {range0 = 0, ranges = [], string = ""};

fun is_empty_chunks (Chunks {range0, ranges, ...}) =
  range0 = 0 andalso null ranges;

fun count_chunks (chunks as Chunks {ranges, ...}) =
  if is_empty_chunks chunks then 0
  else length ranges + 1;

fun size_chunks (chunks as Chunks {range0, ranges, ...}) =
  if is_empty_chunks chunks then 0
  else fold (fn r => fn n => n + range_length r + 1) ranges (range_length range0);

fun base_chunks name =
  let
    val i = last_separator name;
    val j = i + 1;
  in
    if i < 0 then empty_chunks
    else Chunks {range0 = range name j (size name - j), ranges = [], string = name}
  end;

fun suppress_chunks suppress1 suppress2 string =
  let
    val n = size string;

    fun suppr_chunks suppr1 suppr2 i j rs =
      let
        val string_end = i >= n;
        val chunk_end = string_end orelse String.nth string i = separator_char;

        val suppr =
          if suppr1 > 0 then true
          else if suppr1 < 0 then false
          else if null suppr2 then false
          else hd suppr2;
        val suppr1' =
          if chunk_end andalso suppr1 > 0 then suppr1 - 1
          else if chunk_end andalso suppr1 < 0 then suppr1 + 1
          else suppr1;
        val suppr2' =
          if chunk_end andalso suppr1 = 0 andalso not (null suppr2)
          then tl suppr2 else suppr2;

        val i' = i + 1;
        val j' = if chunk_end then i' else j;
        val rs' = if chunk_end andalso not suppr then range string j (i - j) :: rs else rs;
      in
        if not string_end then suppr_chunks suppr1' suppr2' i' j' rs'
        else if not (suppr1' = 0 andalso null suppr2') then
          failure string ("cannot suppress chunks beyond " ^ string_of_int (length rs'))
        else
          (case rs' of
            [] => empty_chunks
          | r0 :: rest => Chunks {range0 = r0, ranges = rest, string = string})
      end;
  in suppr_chunks suppress1 suppress2 0 0 [] end;

val make_chunks = suppress_chunks 0 [];

fun explode_chunks (chunks as Chunks {range0, ranges, string}) =
  if is_empty_chunks chunks then []
  else fold (cons o range_string string) ranges [range_string string range0];

fun implode_chunks (chunks as Chunks {range0, ranges, string}) =
  if size_chunks chunks = size string then string
  else if null ranges then range_string string range0
  else implode (explode_chunks chunks);

val compare_chunks = pointer_eq_ord (fn (chunks1, chunks2) =>
  let
    val Chunks {range0 = range01, ranges = ranges1, string = string1} = chunks1;
    val Chunks {range0 = range02, ranges = ranges2, string = string2} = chunks2;
    val count1 = count_chunks chunks1;
    val count2 = count_chunks chunks2;

    val range_length_ord = int_ord o apply2 range_length;
    fun range_substring_ord arg =
      let
        val (i, j) = apply2 range_index arg;
        val (m, n) = apply2 range_length arg;

        fun substring_ord k =
          if k < n then
            (case Char.compare (String.nth string1 (i + k), String.nth string2 (j + k)) of
              EQUAL => substring_ord (k + 1)
            | ord => ord)
          else EQUAL;
      in (case int_ord (m, n) of EQUAL => substring_ord 0 | ord => ord) end;
  in
    if count1 = 0 andalso count2 = 0 then EQUAL
    else
      (case int_ord (count1, count2) of
        EQUAL =>
          (case range_length_ord (range01, range02) of
            EQUAL =>
              (case dict_ord range_length_ord (ranges1, ranges2) of
                EQUAL =>
                  (case range_substring_ord (range01, range02) of
                    EQUAL => dict_ord range_substring_ord (ranges1, ranges2)
                  | ord => ord)
              | ord => ord)
          | ord => ord)
      | ord => ord)
  end);

val eq_chunks = is_equal o compare_chunks;

end;

end;

structure Chunks = Change_Table(type key = chunks val ord = compare_chunks);

end;

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.