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