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
     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 -> '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) option
    20   val hd: 'a seq -> 'a
    21 end;
    22 
    23 structure DSeq : DSEQ =
    24 struct
    25 
    26 type 'a seq = int -> 'a Seq.seq;
    27 
    28 fun maps f s 0 = Seq.empty
    29   | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
    30 
    31 fun map f s i = Seq.map f (s i);
    32 
    33 fun append s1 s2 i = Seq.append (s1 i) (s2 i);
    34 
    35 fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i);
    36 
    37 fun single x i = Seq.single x;
    38 
    39 fun empty i = Seq.empty;
    40 
    41 fun guard b = if b then single () else empty;
    42 
    43 fun of_list xs i = Seq.of_list xs;
    44 
    45 fun list_of s = Seq.list_of (s ~1);
    46 
    47 fun pull s = Seq.pull (s ~1) |> (Option.map o apsnd) K; (*FIXME*)
    48 
    49 fun hd s = Seq.hd (s ~1);
    50 
    51 end;
    52 
    53 
    54 (* combinators for code generated from inductive predicates *)
    55 
    56 infix 5 :->;
    57 infix 3 ++;
    58 
    59 fun s :-> f = DSeq.maps f s;
    60 
    61 fun f ++ g = DSeq.append f g;
    62 
    63 val ?? = DSeq.guard;
    64 
    65 fun ??? f g = f o g;
    66 
    67 fun ?! s = is_some (DSeq.pull s);
    68 
    69 fun equal__1 x = DSeq.single x;
    70 
    71 val equal__2 = equal__1;
    72 
    73 fun equal__1_2 (x, y) = ?? (x = y);