Quelle seq.ML Sprache: SML

(*  Title:      Pure/General/seq.ML
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Author:     Markus Wenzel, TU Munich

Unbounded sequences implemented by closures.  RECOMPUTES if sequence
is re-inspected.  Memoing, using polymorphic refs, was found to be
slower!  (More GCs)
*)

signature SEQ =
sig
  type 'a seq
  val make: (unit -> ('a * 'a seq) option) -> 'a seq
  val pull: 'a seq -> ('a * 'a seq) option
  val empty: 'a seq
  val cons: 'a -> 'a seq -> 'a seq
  val single: 'a -> 'a seq
  val try: ('a -> 'b) -> 'a -> 'b seq
  val hd: 'a seq -> 'a
  val tl: 'a seq -> 'a seq
  val chop: int -> 'a seq -> 'a list * 'a seq
  val take: int -> 'a seq -> 'a seq
  val list_of: 'a seq -> 'a list
  val of_list: 'a list -> 'a seq
  val append: 'a seq -> 'a seq -> 'a seq
  val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
  val interleave: 'a seq * 'a seq -> 'a seq
  val filter: ('a -> bool) -> 'a seq -> 'a seq
  val flat: 'a seq seq -> 'a seq
  val map: ('a -> 'b) -> 'a seq -> 'b seq
  val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
  val map_filter: ('a -> 'b option) -> 'a seq -> 'b seq
  val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq
  val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq
  val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq
  val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
  val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
  datatype 'a result = Result of 'a | Error of unit -> string
  val make_results: 'a seq -> 'a result seq
  val filter_results: 'a result seq -> 'a seq
  val maps_results: ('a -> 'b result seq) -> 'a result seq -> 'b result seq
  val maps_result: ('a -> 'b seq) -> 'a result seq -> 'b result seq
  val map_result: ('a -> 'b) -> 'a result seq -> 'b result seq
  val first_result: string -> 'a result seq -> 'a * 'a seq
  val the_result: string -> 'a result seq -> 'a
  val succeed: 'a -> 'a seq
  val fail: 'a -> 'b seq
  val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
  val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
  val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
  val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
  val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
  val TRY: ('a -> 'a seq) -> 'a -> 'a seq
  val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
  val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
  val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
  val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
end;

structure Seq: SEQ =
struct

(** lazy sequences **)

datatype 'a seq = Seq of unit -> ('a * 'a seq) option;

(*the abstraction for making a sequence*)
val make = Seq;

(*return next sequence element as NONE or SOME (x, xq)*)
fun pull (Seq f) = f ();

(*the empty sequence*)
val empty = Seq (fn () => NONE);

(*prefix an element to the sequence -- use cons (x, xq) only if
  evaluation of xq need not be delayed, otherwise use
  make (fn () => SOME (x, xq))*)
fun cons x xq = make (fn () => SOME (x, xq));

fun single x = cons x empty;

(*head and tail -- beware of calling the sequence function twice!!*)
fun hd xq = #1 (the (pull xq))
and tl xq = #2 (the (pull xq));

(*partial function as procedure*)
fun try f x =
  (case Basics.try f x of
    SOME y => single y
  | NONE => empty);

(*the list of the first n elements, paired with rest of sequence;
  if length of list is less than n, then sequence had less than n elements*)
fun chop n xq =
  if n <= (0 : int) then ([], xq)
  else
    (case pull xq of
      NONE => ([], xq)
    | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1) xq'));

(*truncate the sequence after n elements*)
fun take n xq =
  if n <= (0 : int) then empty
  else make (fn () =>
    (Option.map o apsnd) (take (n - 1)) (pull xq));

(*conversion from sequence to list*)
fun list_of xq =
  (case pull xq of
    NONE => []
  | SOME (x, xq') => x :: list_of xq');

(*conversion from list to sequence*)
fun of_list xs = fold_rev cons xs empty;

(*sequence append: put the elements of xq in front of those of yq*)
fun append xq yq =
  let
    fun copy s =
      make (fn () =>
        (case pull s of
          NONE => pull yq
        | SOME (x, s') => SOME (x, copy s')))
  in copy xq end;

(*map over a sequence xq, append the sequence yq*)
fun mapp f xq yq =
  let
    fun copy s =
      make (fn () =>
        (case pull s of
          NONE => pull yq
        | SOME (x, s') => SOME (f x, copy s')))
  in copy xq end;

(*interleave elements of xq with those of yq -- fairer than append*)
fun interleave (xq, yq) =
  make (fn () =>
    (case pull xq of
      NONE => pull yq
    | SOME (x, xq') => SOME (x, interleave (yq, xq'))));

(*filter sequence by predicate*)
fun filter pred xq =
  let
    fun copy s =
      make (fn () =>
        (case pull s of
          NONE => NONE
        | SOME (x, s') => if pred x then SOME (x, copy s') else pull (copy s')));
  in copy xq end;

(*flatten a sequence of sequences to a single sequence*)
fun flat xqq =
  make (fn () =>
    (case pull xqq of
      NONE => NONE
    | SOME (xq, xqq') => pull (append xq (flat xqq'))));

(*map the function f over the sequence, making a new sequence*)
fun map f xq =
  make (fn () =>
    (case pull xq of
      NONE => NONE
    | SOME (x, xq') => SOME (f x, map f xq')));

fun maps f xq =
  make (fn () =>
    (case pull xq of
      NONE => NONE
    | SOME (x, xq') => pull (append (f x) (maps f xq'))));

fun map_filter f = maps (fn x => (case f x of NONE => empty | SOME y => single y));

fun lift f xq y = map (fn x => f x y) xq;
fun lifts f xq y = maps (fn x => f x y) xq;

fun singleton f x = f [x] |> map (fn [y] => y | _ => raise List.Empty);

(*print a sequence, up to "count" elements*)
fun print print_elem count =
  let
    fun prnt (k: int) xq =
      if k > count then ()
      else
        (case pull xq of
          NONE => ()
        | SOME (x, xq') => (print_elem k x; writeln ""; prnt (k + 1) xq'));
  in prnt 1 end;

(*accumulating a function over a sequence; this is lazy*)
fun it_right f (xq, yq) =
  let
    fun its s =
      make (fn () =>
        (case pull s of
          NONE => pull yq
        | SOME (a, s') => pull (f (a, its s'))))
  in its xq end;

(* embedded errors *)

datatype 'a result = Result of 'a | Error of unit -> string;

fun make_results xq = map Result xq;
fun filter_results xq = map_filter (fn Result x => SOME x | Error _ => NONE) xq;

fun maps_results f xq =
  make (fn () =>
    (case pull xq of
      NONE => NONE
    | SOME (Result x, xq') => pull (append (f x) (maps_results f xq'))
    | SOME (Error msg, xq') => SOME (Error msg, maps_results f xq')));

fun maps_result f = maps_results (map Result o f);
fun map_result f = maps_result (single o f);

(*first result or first error within sequence*)
fun first_result default_msg seq =
  let
    fun result opt_msg xq =
      (case (opt_msg, pull xq) of
        (_, SOME (Result x, xq')) => (x, filter_results xq')
      | (SOME _, SOME (Error _, xq')) => result opt_msg xq'
      | (NONE, SOME (Error msg, xq')) => result (SOME msg) xq'
      | (SOME msg, NONE) => error (msg ())
      | (NONE, NONE) => error (if default_msg = "" then "Empty result sequence" else default_msg));
  in result NONE seq end;

fun the_result default_msg seq = #1 (first_result default_msg seq);

(** sequence functions **)      (*cf. Pure/tactical.ML*)

fun succeed x = single x;
fun fail _ = empty;

fun op THEN (f, g) x = maps g (f x);

fun op ORELSE (f, g) x =
  (case pull (f x) of
    NONE => g x
  | some => make (fn () => some));

fun op APPEND (f, g) x =
  append (f x) (make (fn () => pull (g x)));

fun EVERY fs = fold_rev (curry op THEN) fs succeed;
fun FIRST fs = fold_rev (curry op ORELSE) fs fail;

fun TRY f = ORELSE (f, succeed);

fun REPEAT f =
  let
    fun rep qs x =
      (case pull (f x) of
        NONE => SOME (x, make (fn () => repq qs))
      | SOME (x', q) => rep (q :: qs) x')
    and repq [] = NONE
      | repq (q :: qs) =
          (case pull q of
            NONE => repq qs
          | SOME (x, q) => rep (q :: qs) x);
  in fn x => make (fn () => rep [] x) end;

fun REPEAT1 f = THEN (f, REPEAT f);

fun INTERVAL f (i: int) j x =
  if i > j then single x
  else op THEN (f j, INTERVAL f i (j - 1)) x;

fun DETERM f x =
  (case pull (f x) of
    NONE => empty
  | SOME (x', _) => cons x' empty);

end;

quality95%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

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.