Additional operations for structure String, following Isabelle/ML conventions.
NB: Isabelle normally works with Symbol.symbol, which is represented as a small string fragment. Raw type char is rarely useful.
*)
signatureSTRING = sig
include STRING val nth: string -> int -> char valexists: (char -> bool) -> string -> bool val forall: (char -> bool) -> string -> bool val member: string -> char -> bool val fold: (char -> 'a -> 'a) -> string -> 'a -> 'a val fold_rev: (char -> 'a -> 'a) -> string -> 'a -> 'a end;
structureString: STRING = struct
openString;
fun nth str i = sub (str, i);
funexists pred str = let val n = size str; fun ex i = Int.< (i, n) andalso (pred (nth str i) orelse ex (i + 1)); in ex 0 end;
fun forall pred = not o exists (not o pred);
fun member str c = exists (fn c' => c = c') str;
fun fold f str x0 = let val n = size str; fun iter (x, i) = if Int.< (i, n) then iter (f (nth str i) x, i + 1) else x; in iter (x0, 0) end;
fun fold_rev f str x0 = let val n = size str; fun iter (x, i) = if Int.>= (i, 0) then iter (f (nth str i) x, i - 1) else x; in iter (x0, n - 1) end;
end;
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
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.
