src/HOL/Tools/dseq.ML
author haftmann
Wed Dec 08 13:34:50 2010 +0100 (2010-12-08)
changeset 41075 4bed56dc95fb
parent 33770 1ef05f838d51
permissions -rw-r--r--
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
     1 (*  Title:      HOL/Tools/dseq.ML
     2     Author:     Stefan Berghofer, TU Muenchen
     3 
     4 Sequences with recursion depth limit.
     5 *)
     6 
     7 signature DSEQ =
     8 sig
     9   type 'a seq = int * int * int -> 'a Seq.seq;
    10   val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
    11   val map: ('a -> 'b) -> 'a seq -> 'b seq
    12   val append: 'a seq -> 'a seq -> 'a seq
    13   val interleave: 'a seq -> 'a seq -> 'a seq
    14   val single: 'a -> 'a seq
    15   val empty: 'a seq
    16   val guard: bool -> unit seq
    17   val of_list: 'a list -> 'a seq
    18   val list_of: 'a seq -> 'a list
    19   val pull: 'a seq -> ('a * 'a Seq.seq) option
    20   val hd: 'a seq -> 'a
    21   val generator: (int -> 'a * 'b) -> 'a seq
    22 end;
    23 
    24 structure DSeq : DSEQ =
    25 struct
    26 
    27 type 'a seq = int * int * int -> 'a Seq.seq;
    28 
    29 fun maps f s (0, _, _) = Seq.empty
    30   | maps f s (i, j, k) = Seq.maps (fn a => f a (i, j, k)) (s (i - 1, j, k));
    31 
    32 fun map f s p = Seq.map f (s p);
    33 
    34 fun append s1 s2 p = Seq.append (s1 p) (s2 p);
    35 
    36 fun interleave s1 s2 p = Seq.interleave (s1 p, s2 p);
    37 
    38 fun single x _ = Seq.single x;
    39 
    40 fun empty _ = Seq.empty;
    41 
    42 fun guard b = if b then single () else empty;
    43 
    44 fun of_list xs _ = Seq.of_list xs;
    45 
    46 fun list_of s = Seq.list_of (s (~1, 0, 0));
    47 
    48 fun pull s = Seq.pull (s (~1, 0, 0));
    49 
    50 fun hd s = Seq.hd (s (~1, 0, 0));
    51 
    52 fun generator g (i, 0, k) = Seq.empty
    53   | generator g (i, j, k) =
    54       Seq.make (fn () => SOME (fst (g k), generator g (i, j-1, k)));
    55 
    56 end;
    57 
    58 
    59 (* combinators for code generated from inductive predicates *)
    60 
    61 infix 5 :->;
    62 infix 3 ++;
    63 
    64 fun s :-> f = DSeq.maps f s;
    65 
    66 fun f ++ g = DSeq.append f g;
    67 
    68 val ?? = DSeq.guard;
    69 
    70 fun ??? f g = f o g;
    71 
    72 fun ?! s = is_some (DSeq.pull s);
    73 
    74 fun equal__1 x = DSeq.single x;
    75 
    76 val equal__2 = equal__1;
    77 
    78 fun equal__1_2 (x, y) = ?? (x = y);