src/HOL/Tools/dseq.ML
author wenzelm
Thu Mar 27 14:41:09 2008 +0100 (2008-03-27)
changeset 26424 a6cad32a27b0
parent 25308 fc01c83a466d
child 28308 d4396a28fb29
permissions -rw-r--r--
eliminated theory ProtoPure;
haftmann@24625
     1
(*  Title:      HOL/Tools/DSeq.ML
haftmann@24625
     2
    ID:         $Id$
haftmann@24625
     3
    Author:     Stefan Berghofer, TU Muenchen
haftmann@24625
     4
haftmann@24625
     5
Sequences with recursion depth limit.
haftmann@24625
     6
*)
haftmann@24625
     7
haftmann@25308
     8
signature DSEQ =
haftmann@25308
     9
sig
haftmann@25308
    10
  type 'a seq = int -> 'a Seq.seq;
haftmann@25308
    11
  val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
haftmann@25308
    12
  val map: ('a -> 'b) -> 'a seq -> 'b seq
haftmann@25308
    13
  val append: 'a seq -> 'a seq -> 'a seq
haftmann@25308
    14
  val interleave: 'a seq -> 'a seq -> 'a seq
haftmann@25308
    15
  val single: 'a -> 'a seq
haftmann@25308
    16
  val empty: 'a seq
haftmann@25308
    17
  val guard: bool -> unit seq
haftmann@25308
    18
  val of_list: 'a list -> 'a seq
haftmann@25308
    19
  val list_of: 'a seq -> 'a list
haftmann@25308
    20
  val pull: 'a seq -> ('a * 'a seq) option
haftmann@25308
    21
  val hd: 'a seq -> 'a
haftmann@25308
    22
end;
haftmann@25308
    23
haftmann@25308
    24
structure DSeq : DSEQ =
haftmann@24625
    25
struct
haftmann@24625
    26
haftmann@25308
    27
type 'a seq = int -> 'a Seq.seq;
haftmann@25308
    28
haftmann@24625
    29
fun maps f s 0 = Seq.empty
haftmann@24625
    30
  | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
haftmann@24625
    31
haftmann@24625
    32
fun map f s i = Seq.map f (s i);
haftmann@24625
    33
haftmann@24625
    34
fun append s1 s2 i = Seq.append (s1 i) (s2 i);
haftmann@24625
    35
haftmann@24625
    36
fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i);
haftmann@24625
    37
haftmann@24625
    38
fun single x i = Seq.single x;
haftmann@24625
    39
haftmann@24625
    40
fun empty i = Seq.empty;
haftmann@24625
    41
haftmann@24625
    42
fun guard b = if b then single () else empty;
haftmann@24625
    43
haftmann@24625
    44
fun of_list xs i = Seq.of_list xs;
haftmann@24625
    45
haftmann@24625
    46
fun list_of s = Seq.list_of (s ~1);
haftmann@24625
    47
haftmann@25308
    48
fun pull s = Seq.pull (s ~1) |> (Option.map o apsnd) K; (*FIXME*)
haftmann@24625
    49
haftmann@24625
    50
fun hd s = Seq.hd (s ~1);
haftmann@24625
    51
haftmann@24625
    52
end;
haftmann@24625
    53
haftmann@24625
    54
haftmann@24625
    55
(* combinators for code generated from inductive predicates *)
haftmann@24625
    56
haftmann@24625
    57
infix 5 :->;
haftmann@24625
    58
infix 3 ++;
haftmann@24625
    59
haftmann@24625
    60
fun s :-> f = DSeq.maps f s;
haftmann@24625
    61
haftmann@24625
    62
fun f ++ g = DSeq.append f g;
haftmann@24625
    63
haftmann@24625
    64
val ?? = DSeq.guard;
haftmann@24625
    65
haftmann@24625
    66
fun ??? f g = f o g;
haftmann@24625
    67
haftmann@24625
    68
fun ?! s = is_some (DSeq.pull s);
haftmann@24625
    69
haftmann@24625
    70
fun equal__1 x = DSeq.single x;
haftmann@24625
    71
haftmann@24625
    72
val equal__2 = equal__1;
haftmann@24625
    73
haftmann@24625
    74
fun equal__1_2 (x, y) = ?? (x = y);