author | wenzelm |
Sat, 21 Mar 2009 20:38:49 +0100 | |
changeset 30633 | cc18ae3c1c7f |
parent 28308 | d4396a28fb29 |
child 31853 | f079b174e56a |
permissions | -rw-r--r-- |
28308 | 1 |
(* Title: HOL/Tools/dseq.ML |
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
2 |
ID: $Id$ |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
3 |
Author: Stefan Berghofer, TU Muenchen |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
4 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
5 |
Sequences with recursion depth limit. |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
6 |
*) |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
7 |
|
25308 | 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 = |
|
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
25 |
struct |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
26 |
|
25308 | 27 |
type 'a seq = int -> 'a Seq.seq; |
28 |
||
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
29 |
fun maps f s 0 = Seq.empty |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
30 |
| maps f s i = Seq.maps (fn a => f a i) (s (i - 1)); |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
31 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
32 |
fun map f s i = Seq.map f (s i); |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
33 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
34 |
fun append s1 s2 i = Seq.append (s1 i) (s2 i); |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
35 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
36 |
fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i); |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
37 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
38 |
fun single x i = Seq.single x; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
39 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
40 |
fun empty i = Seq.empty; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
41 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
42 |
fun guard b = if b then single () else empty; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
43 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
44 |
fun of_list xs i = Seq.of_list xs; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
45 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
46 |
fun list_of s = Seq.list_of (s ~1); |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
47 |
|
25308 | 48 |
fun pull s = Seq.pull (s ~1) |> (Option.map o apsnd) K; (*FIXME*) |
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
49 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
50 |
fun hd s = Seq.hd (s ~1); |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
51 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
52 |
end; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
53 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
54 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
55 |
(* combinators for code generated from inductive predicates *) |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
56 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
57 |
infix 5 :->; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
58 |
infix 3 ++; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
59 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
60 |
fun s :-> f = DSeq.maps f s; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
61 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
62 |
fun f ++ g = DSeq.append f g; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
63 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
64 |
val ?? = DSeq.guard; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
65 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
66 |
fun ??? f g = f o g; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
67 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
68 |
fun ?! s = is_some (DSeq.pull s); |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
69 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
70 |
fun equal__1 x = DSeq.single x; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
71 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
72 |
val equal__2 = equal__1; |
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
73 |
|
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset
|
74 |
fun equal__1_2 (x, y) = ?? (x = y); |