src/HOL/Tools/dseq.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 28308 d4396a28fb29
child 31853 f079b174e56a
permissions -rw-r--r--
use long names for old-style fold combinators;
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
    ID:         $Id$
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
     4
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
     5
Sequences with recursion depth limit.
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
     6
*)
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
     7
25308
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
     8
signature DSEQ =
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
     9
sig
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    10
  type 'a seq = int -> 'a Seq.seq;
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    11
  val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    12
  val map: ('a -> 'b) -> 'a seq -> 'b seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    13
  val append: 'a seq -> 'a seq -> 'a seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    14
  val interleave: 'a seq -> 'a seq -> 'a seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    15
  val single: 'a -> 'a seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    16
  val empty: 'a seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    17
  val guard: bool -> unit seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    18
  val of_list: 'a list -> 'a seq
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    19
  val list_of: 'a seq -> 'a list
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    20
  val pull: 'a seq -> ('a * 'a seq) option
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    21
  val hd: 'a seq -> 'a
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
25308
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    27
type 'a seq = int -> 'a Seq.seq;
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    28
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    29
fun maps f s 0 = Seq.empty
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    30
  | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    31
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    32
fun map f s i = Seq.map f (s i);
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    33
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    34
fun append s1 s2 i = Seq.append (s1 i) (s2 i);
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    35
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    36
fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i);
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    37
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    38
fun single x i = Seq.single x;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    39
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    40
fun empty i = Seq.empty;
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
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    44
fun of_list xs i = Seq.of_list xs;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    45
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    46
fun list_of s = Seq.list_of (s ~1);
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    47
25308
fc01c83a466d added explicit signature
haftmann
parents: 24625
diff changeset
    48
fun pull s = Seq.pull (s ~1) |> (Option.map o apsnd) K; (*FIXME*)
24625
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    49
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    50
fun hd s = Seq.hd (s ~1);
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    51
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    52
end;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    53
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    54
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    55
(* combinators for code generated from inductive predicates *)
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    56
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    57
infix 5 :->;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    58
infix 3 ++;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    59
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    60
fun s :-> f = DSeq.maps f s;
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    61
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff changeset
    62
fun f ++ g = DSeq.append f g;
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
val ?? = DSeq.guard;
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 = f o 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
fun ?! s = is_some (DSeq.pull s);
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 equal__1 x = DSeq.single x;
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
val equal__2 = equal__1;
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_2 (x, y) = ?? (x = y);