|
1 |
|
2 (* Author: Lukas Bulwahn, TU Muenchen *) |
|
3 |
|
4 header {* Depth-Limited Sequences with failure element *} |
|
5 |
|
6 theory Limited_Sequence |
|
7 imports Lazy_Sequence |
|
8 begin |
|
9 |
|
10 subsection {* Depth-Limited Sequence *} |
|
11 |
|
12 type_synonym 'a dseq = "code_numeral \<Rightarrow> bool \<Rightarrow> 'a lazy_sequence option" |
|
13 |
|
14 definition empty :: "'a dseq" |
|
15 where |
|
16 "empty = (\<lambda>_ _. Some Lazy_Sequence.empty)" |
|
17 |
|
18 definition single :: "'a \<Rightarrow> 'a dseq" |
|
19 where |
|
20 "single x = (\<lambda>_ _. Some (Lazy_Sequence.single x))" |
|
21 |
|
22 definition eval :: "'a dseq \<Rightarrow> code_numeral \<Rightarrow> bool \<Rightarrow> 'a lazy_sequence option" |
|
23 where |
|
24 [simp]: "eval f i pol = f i pol" |
|
25 |
|
26 definition yield :: "'a dseq \<Rightarrow> code_numeral \<Rightarrow> bool \<Rightarrow> ('a \<times> 'a dseq) option" |
|
27 where |
|
28 "yield f i pol = (case eval f i pol of |
|
29 None \<Rightarrow> None |
|
30 | Some s \<Rightarrow> (Option.map \<circ> apsnd) (\<lambda>r _ _. Some r) (Lazy_Sequence.yield s))" |
|
31 |
|
32 definition map_seq :: "('a \<Rightarrow> 'b dseq) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b dseq" |
|
33 where |
|
34 "map_seq f xq i pol = Option.map Lazy_Sequence.flat |
|
35 (Lazy_Sequence.those (Lazy_Sequence.map (\<lambda>x. f x i pol) xq))" |
|
36 |
|
37 lemma map_seq_code [code]: |
|
38 "map_seq f xq i pol = (case Lazy_Sequence.yield xq of |
|
39 None \<Rightarrow> Some Lazy_Sequence.empty |
|
40 | Some (x, xq') \<Rightarrow> (case eval (f x) i pol of |
|
41 None \<Rightarrow> None |
|
42 | Some yq \<Rightarrow> (case map_seq f xq' i pol of |
|
43 None \<Rightarrow> None |
|
44 | Some zq \<Rightarrow> Some (Lazy_Sequence.append yq zq))))" |
|
45 by (cases xq) |
|
46 (auto simp add: map_seq_def Lazy_Sequence.those_def lazy_sequence_eq_iff split: list.splits option.splits) |
|
47 |
|
48 definition bind :: "'a dseq \<Rightarrow> ('a \<Rightarrow> 'b dseq) \<Rightarrow> 'b dseq" |
|
49 where |
|
50 "bind x f = (\<lambda>i pol. |
|
51 if i = 0 then |
|
52 (if pol then Some Lazy_Sequence.empty else None) |
|
53 else |
|
54 (case x (i - 1) pol of |
|
55 None \<Rightarrow> None |
|
56 | Some xq \<Rightarrow> map_seq f xq i pol))" |
|
57 |
|
58 definition union :: "'a dseq \<Rightarrow> 'a dseq \<Rightarrow> 'a dseq" |
|
59 where |
|
60 "union x y = (\<lambda>i pol. case (x i pol, y i pol) of |
|
61 (Some xq, Some yq) \<Rightarrow> Some (Lazy_Sequence.append xq yq) |
|
62 | _ \<Rightarrow> None)" |
|
63 |
|
64 definition if_seq :: "bool \<Rightarrow> unit dseq" |
|
65 where |
|
66 "if_seq b = (if b then single () else empty)" |
|
67 |
|
68 definition not_seq :: "unit dseq \<Rightarrow> unit dseq" |
|
69 where |
|
70 "not_seq x = (\<lambda>i pol. case x i (\<not> pol) of |
|
71 None \<Rightarrow> Some Lazy_Sequence.empty |
|
72 | Some xq \<Rightarrow> (case Lazy_Sequence.yield xq of |
|
73 None \<Rightarrow> Some (Lazy_Sequence.single ()) |
|
74 | Some _ \<Rightarrow> Some (Lazy_Sequence.empty)))" |
|
75 |
|
76 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dseq \<Rightarrow> 'b dseq" |
|
77 where |
|
78 "map f g = (\<lambda>i pol. case g i pol of |
|
79 None \<Rightarrow> None |
|
80 | Some xq \<Rightarrow> Some (Lazy_Sequence.map f xq))" |
|
81 |
|
82 |
|
83 subsection {* Positive Depth-Limited Sequence *} |
|
84 |
|
85 type_synonym 'a pos_dseq = "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence" |
|
86 |
|
87 definition pos_empty :: "'a pos_dseq" |
|
88 where |
|
89 "pos_empty = (\<lambda>i. Lazy_Sequence.empty)" |
|
90 |
|
91 definition pos_single :: "'a \<Rightarrow> 'a pos_dseq" |
|
92 where |
|
93 "pos_single x = (\<lambda>i. Lazy_Sequence.single x)" |
|
94 |
|
95 definition pos_bind :: "'a pos_dseq \<Rightarrow> ('a \<Rightarrow> 'b pos_dseq) \<Rightarrow> 'b pos_dseq" |
|
96 where |
|
97 "pos_bind x f = (\<lambda>i. Lazy_Sequence.bind (x i) (\<lambda>a. f a i))" |
|
98 |
|
99 definition pos_decr_bind :: "'a pos_dseq \<Rightarrow> ('a \<Rightarrow> 'b pos_dseq) \<Rightarrow> 'b pos_dseq" |
|
100 where |
|
101 "pos_decr_bind x f = (\<lambda>i. |
|
102 if i = 0 then |
|
103 Lazy_Sequence.empty |
|
104 else |
|
105 Lazy_Sequence.bind (x (i - 1)) (\<lambda>a. f a i))" |
|
106 |
|
107 definition pos_union :: "'a pos_dseq \<Rightarrow> 'a pos_dseq \<Rightarrow> 'a pos_dseq" |
|
108 where |
|
109 "pos_union xq yq = (\<lambda>i. Lazy_Sequence.append (xq i) (yq i))" |
|
110 |
|
111 definition pos_if_seq :: "bool \<Rightarrow> unit pos_dseq" |
|
112 where |
|
113 "pos_if_seq b = (if b then pos_single () else pos_empty)" |
|
114 |
|
115 definition pos_iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a pos_dseq" |
|
116 where |
|
117 "pos_iterate_upto f n m = (\<lambda>i. Lazy_Sequence.iterate_upto f n m)" |
|
118 |
|
119 definition pos_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pos_dseq \<Rightarrow> 'b pos_dseq" |
|
120 where |
|
121 "pos_map f xq = (\<lambda>i. Lazy_Sequence.map f (xq i))" |
|
122 |
|
123 |
|
124 subsection {* Negative Depth-Limited Sequence *} |
|
125 |
|
126 type_synonym 'a neg_dseq = "code_numeral \<Rightarrow> 'a Lazy_Sequence.hit_bound_lazy_sequence" |
|
127 |
|
128 definition neg_empty :: "'a neg_dseq" |
|
129 where |
|
130 "neg_empty = (\<lambda>i. Lazy_Sequence.empty)" |
|
131 |
|
132 definition neg_single :: "'a \<Rightarrow> 'a neg_dseq" |
|
133 where |
|
134 "neg_single x = (\<lambda>i. Lazy_Sequence.hb_single x)" |
|
135 |
|
136 definition neg_bind :: "'a neg_dseq \<Rightarrow> ('a \<Rightarrow> 'b neg_dseq) \<Rightarrow> 'b neg_dseq" |
|
137 where |
|
138 "neg_bind x f = (\<lambda>i. hb_bind (x i) (\<lambda>a. f a i))" |
|
139 |
|
140 definition neg_decr_bind :: "'a neg_dseq \<Rightarrow> ('a \<Rightarrow> 'b neg_dseq) \<Rightarrow> 'b neg_dseq" |
|
141 where |
|
142 "neg_decr_bind x f = (\<lambda>i. |
|
143 if i = 0 then |
|
144 Lazy_Sequence.hit_bound |
|
145 else |
|
146 hb_bind (x (i - 1)) (\<lambda>a. f a i))" |
|
147 |
|
148 definition neg_union :: "'a neg_dseq \<Rightarrow> 'a neg_dseq \<Rightarrow> 'a neg_dseq" |
|
149 where |
|
150 "neg_union x y = (\<lambda>i. Lazy_Sequence.append (x i) (y i))" |
|
151 |
|
152 definition neg_if_seq :: "bool \<Rightarrow> unit neg_dseq" |
|
153 where |
|
154 "neg_if_seq b = (if b then neg_single () else neg_empty)" |
|
155 |
|
156 definition neg_iterate_upto |
|
157 where |
|
158 "neg_iterate_upto f n m = (\<lambda>i. Lazy_Sequence.iterate_upto (\<lambda>i. Some (f i)) n m)" |
|
159 |
|
160 definition neg_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a neg_dseq \<Rightarrow> 'b neg_dseq" |
|
161 where |
|
162 "neg_map f xq = (\<lambda>i. Lazy_Sequence.hb_map f (xq i))" |
|
163 |
|
164 |
|
165 subsection {* Negation *} |
|
166 |
|
167 definition pos_not_seq :: "unit neg_dseq \<Rightarrow> unit pos_dseq" |
|
168 where |
|
169 "pos_not_seq xq = (\<lambda>i. Lazy_Sequence.hb_not_seq (xq (3 * i)))" |
|
170 |
|
171 definition neg_not_seq :: "unit pos_dseq \<Rightarrow> unit neg_dseq" |
|
172 where |
|
173 "neg_not_seq x = (\<lambda>i. case Lazy_Sequence.yield (x i) of |
|
174 None => Lazy_Sequence.hb_single () |
|
175 | Some ((), xq) => Lazy_Sequence.empty)" |
|
176 |
|
177 |
|
178 ML {* |
|
179 signature LIMITED_SEQUENCE = |
|
180 sig |
|
181 type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option |
|
182 val map : ('a -> 'b) -> 'a dseq -> 'b dseq |
|
183 val yield : 'a dseq -> int -> bool -> ('a * 'a dseq) option |
|
184 val yieldn : int -> 'a dseq -> int -> bool -> 'a list * 'a dseq |
|
185 end; |
|
186 |
|
187 structure Limited_Sequence : LIMITED_SEQUENCE = |
|
188 struct |
|
189 |
|
190 type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option |
|
191 |
|
192 fun map f = @{code Limited_Sequence.map} f; |
|
193 |
|
194 fun yield f = @{code Limited_Sequence.yield} f; |
|
195 |
|
196 fun yieldn n f i pol = (case f i pol of |
|
197 NONE => ([], fn _ => fn _ => NONE) |
|
198 | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn _ => fn _ => SOME s') end); |
|
199 |
|
200 end; |
|
201 *} |
|
202 |
|
203 code_reserved Eval Limited_Sequence |
|
204 |
|
205 |
|
206 hide_const (open) yield empty single eval map_seq bind union if_seq not_seq map |
|
207 pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map |
|
208 neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map |
|
209 |
|
210 hide_fact (open) yield_def empty_def single_def eval_def map_seq_def bind_def union_def |
|
211 if_seq_def not_seq_def map_def |
|
212 pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def |
|
213 neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def |
|
214 |
|
215 end |
|
216 |