author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 28308  d4396a28fb29 
child 31853  f079b174e56a 
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 
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); 