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