author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 33770  1ef05f838d51 
permissions  rwrr 
28308  1 
(* Title: HOL/Tools/dseq.ML 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

2 
Author: Stefan Berghofer, TU Muenchen 
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

3 

0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

4 
Sequences with recursion depth limit. 
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

5 
*) 
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

6 

25308  7 
signature DSEQ = 
8 
sig 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

9 
type 'a seq = int * int * int > 'a Seq.seq; 
25308  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 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

19 
val pull: 'a seq > ('a * 'a Seq.seq) option 
25308  20 
val hd: 'a seq > 'a 
33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

21 
val generator: (int > 'a * 'b) > 'a seq 
25308  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 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

27 
type 'a seq = int * int * int > 'a Seq.seq; 
25308  28 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

29 
fun maps f s (0, _, _) = Seq.empty 
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

30 
 maps f s (i, j, k) = Seq.maps (fn a => f a (i, j, k)) (s (i  1, j, k)); 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

31 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

32 
fun map f s p = Seq.map f (s p); 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

33 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

34 
fun append s1 s2 p = Seq.append (s1 p) (s2 p); 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

35 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

36 
fun interleave s1 s2 p = Seq.interleave (s1 p, s2 p); 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

37 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

38 
fun single x _ = Seq.single x; 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

39 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

40 
fun empty _ = Seq.empty; 
24625
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 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

44 
fun of_list xs _ = Seq.of_list xs; 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

45 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

46 
fun list_of s = Seq.list_of (s (~1, 0, 0)); 
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

47 

1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

48 
fun pull s = Seq.pull (s (~1, 0, 0)); 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

49 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

50 
fun hd s = Seq.hd (s (~1, 0, 0)); 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

51 

33770
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

52 
fun generator g (i, 0, k) = Seq.empty 
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

53 
 generator g (i, j, k) = 
1ef05f838d51
Added infrastructure for embedding random data generators into code generated
berghofe
parents:
31853
diff
changeset

54 
Seq.make (fn () => SOME (fst (g k), generator g (i, j1, k))); 
24625
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

55 

0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

56 
end; 
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

57 

0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

58 

0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

59 
(* combinators for code generated from inductive predicates *) 
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

60 

0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

61 
infix 5 :>; 
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

62 
infix 3 ++; 
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 
fun s :> f = DSeq.maps f s; 
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 = DSeq.append f 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 
val ?? = DSeq.guard; 
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 ??? f g = f o g; 
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 
fun ?! s = is_some (DSeq.pull s); 
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 x = DSeq.single x; 
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

75 

0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

76 
val equal__2 = equal__1; 
0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

77 

0398a5e802d3
separated code for inductive sequences from inductive_codegen.ML
haftmann
parents:
diff
changeset

78 
fun equal__1_2 (x, y) = ?? (x = y); 