src/HOL/Tools/dseq.ML
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 33770 1ef05f838d51
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
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
berghofe@33770
     9
  type 'a seq = int * int * 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
berghofe@33770
    19
  val pull: 'a seq -> ('a * 'a Seq.seq) option
haftmann@25308
    20
  val hd: 'a seq -> 'a
berghofe@33770
    21
  val generator: (int -> 'a * 'b) -> 'a seq
haftmann@25308
    22
end;
haftmann@25308
    23
haftmann@25308
    24
structure DSeq : DSEQ =
haftmann@24625
    25
struct
haftmann@24625
    26
berghofe@33770
    27
type 'a seq = int * int * int -> 'a Seq.seq;
haftmann@25308
    28
berghofe@33770
    29
fun maps f s (0, _, _) = Seq.empty
berghofe@33770
    30
  | maps f s (i, j, k) = Seq.maps (fn a => f a (i, j, k)) (s (i - 1, j, k));
haftmann@24625
    31
berghofe@33770
    32
fun map f s p = Seq.map f (s p);
haftmann@24625
    33
berghofe@33770
    34
fun append s1 s2 p = Seq.append (s1 p) (s2 p);
haftmann@24625
    35
berghofe@33770
    36
fun interleave s1 s2 p = Seq.interleave (s1 p, s2 p);
haftmann@24625
    37
berghofe@33770
    38
fun single x _ = Seq.single x;
haftmann@24625
    39
berghofe@33770
    40
fun empty _ = Seq.empty;
haftmann@24625
    41
haftmann@24625
    42
fun guard b = if b then single () else empty;
haftmann@24625
    43
berghofe@33770
    44
fun of_list xs _ = Seq.of_list xs;
haftmann@24625
    45
berghofe@33770
    46
fun list_of s = Seq.list_of (s (~1, 0, 0));
berghofe@33770
    47
berghofe@33770
    48
fun pull s = Seq.pull (s (~1, 0, 0));
haftmann@24625
    49
berghofe@33770
    50
fun hd s = Seq.hd (s (~1, 0, 0));
haftmann@24625
    51
berghofe@33770
    52
fun generator g (i, 0, k) = Seq.empty
berghofe@33770
    53
  | generator g (i, j, k) =
berghofe@33770
    54
      Seq.make (fn () => SOME (fst (g k), generator g (i, j-1, k)));
haftmann@24625
    55
haftmann@24625
    56
end;
haftmann@24625
    57
haftmann@24625
    58
haftmann@24625
    59
(* combinators for code generated from inductive predicates *)
haftmann@24625
    60
haftmann@24625
    61
infix 5 :->;
haftmann@24625
    62
infix 3 ++;
haftmann@24625
    63
haftmann@24625
    64
fun s :-> f = DSeq.maps f s;
haftmann@24625
    65
haftmann@24625
    66
fun f ++ g = DSeq.append f g;
haftmann@24625
    67
haftmann@24625
    68
val ?? = DSeq.guard;
haftmann@24625
    69
haftmann@24625
    70
fun ??? f g = f o g;
haftmann@24625
    71
haftmann@24625
    72
fun ?! s = is_some (DSeq.pull s);
haftmann@24625
    73
haftmann@24625
    74
fun equal__1 x = DSeq.single x;
haftmann@24625
    75
haftmann@24625
    76
val equal__2 = equal__1;
haftmann@24625
    77
haftmann@24625
    78
fun equal__1_2 (x, y) = ?? (x = y);