src/HOL/Tools/dseq.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 33770 1ef05f838d51
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28308
d4396a28fb29 fixed headers
haftmann
parents: 25308
diff changeset
     1
(*  Title:      HOL/Tools/dseq.ML
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
     3
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
     4
Sequences with recursion depth limit.
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
     5
*)
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
     6
25308
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
     7
signature DSEQ =
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
     8
sig
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
     9
  type 'a seq = int * int * int -> 'a Seq.seq;
25308
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    10
  val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    11
  val map: ('a -> 'b) -> 'a seq -> 'b seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    12
  val append: 'a seq -> 'a seq -> 'a seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    13
  val interleave: 'a seq -> 'a seq -> 'a seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    14
  val single: 'a -> 'a seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    15
  val empty: 'a seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    16
  val guard: bool -> unit seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    17
  val of_list: 'a list -> 'a seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    18
  val list_of: 'a seq -> 'a list
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    19
  val pull: 'a seq -> ('a * 'a Seq.seq) option
25308
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    20
  val hd: 'a seq -> 'a
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    21
  val generator: (int -> 'a * 'b) -> 'a seq
25308
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    22
end;
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    23
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    24
structure DSeq : DSEQ =
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    25
struct
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    26
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    27
type 'a seq = int * int * int -> 'a Seq.seq;
25308
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    28
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    29
fun maps f s (0, _, _) = Seq.empty
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    30
  | maps f s (i, j, k) = Seq.maps (fn a => f a (i, j, k)) (s (i - 1, j, k));
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    31
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    32
fun map f s p = Seq.map f (s p);
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    33
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    34
fun append s1 s2 p = Seq.append (s1 p) (s2 p);
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    35
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    36
fun interleave s1 s2 p = Seq.interleave (s1 p, s2 p);
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    37
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    38
fun single x _ = Seq.single x;
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    39
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    40
fun empty _ = Seq.empty;
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    41
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    42
fun guard b = if b then single () else empty;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    43
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    44
fun of_list xs _ = Seq.of_list xs;
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    45
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    46
fun list_of s = Seq.list_of (s (~1, 0, 0));
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    47
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    48
fun pull s = Seq.pull (s (~1, 0, 0));
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    49
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    50
fun hd s = Seq.hd (s (~1, 0, 0));
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    51
33770
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    52
fun generator g (i, 0, k) = Seq.empty
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    53
  | generator g (i, j, k) =
1ef05f838d51 Added infrastructure for embedding random data generators into code generated
berghofe
parents: 31853
diff changeset
    54
      Seq.make (fn () => SOME (fst (g k), generator g (i, j-1, k)));
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    55
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    56
end;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    57
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    58
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    59
(* combinators for code generated from inductive predicates *)
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    60
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    61
infix 5 :->;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    62
infix 3 ++;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    63
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    64
fun s :-> f = DSeq.maps f s;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    65
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    66
fun f ++ g = DSeq.append f g;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    67
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    68
val ?? = DSeq.guard;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    69
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    70
fun ??? f g = f o g;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    71
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    72
fun ?! s = is_some (DSeq.pull s);
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    73
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    74
fun equal__1 x = DSeq.single x;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    75
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    76
val equal__2 = equal__1;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    77
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    78
fun equal__1_2 (x, y) = ?? (x = y);