10 "next yield Predicate.Empty = None" |
10 "next yield Predicate.Empty = None" |
11 | "next yield (Predicate.Insert x P) = Some (x, P)" |
11 | "next yield (Predicate.Insert x P) = Some (x, P)" |
12 | "next yield (Predicate.Join P xq) = (case yield P |
12 | "next yield (Predicate.Join P xq) = (case yield P |
13 of None \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))" |
13 of None \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))" |
14 |
14 |
15 ML {* |
|
16 let |
|
17 fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ()) |
|
18 in |
|
19 yield @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*) |
|
20 end |
|
21 *} |
|
22 |
|
23 fun anamorph :: "('b \<Rightarrow> ('a \<times> 'b) option) \<Rightarrow> index \<Rightarrow> 'b \<Rightarrow> 'a list \<times> 'b" where |
15 fun anamorph :: "('b \<Rightarrow> ('a \<times> 'b) option) \<Rightarrow> index \<Rightarrow> 'b \<Rightarrow> 'a list \<times> 'b" where |
24 "anamorph f k x = (if k = 0 then ([], x) |
16 "anamorph f k x = (if k = 0 then ([], x) |
25 else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow> let (vs, z) = anamorph f (k - 1) y in (v # vs, z))" |
17 else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow> let (vs, z) = anamorph f (k - 1) y in (v # vs, z))" |
26 |
18 |
27 ML {* |
19 ML {* |
28 let |
20 structure Predicate = |
29 fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ()) |
21 struct |
30 fun yieldn k = @{code anamorph} yield k |
22 |
31 in |
23 open Predicate; |
32 yieldn 0 (*replace with number of elements to retrieve*) |
24 |
33 @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*) |
25 fun yield (Predicate.Seq f) = @{code next} yield (f ()); |
34 end |
26 |
|
27 fun yieldn k = @{code anamorph} yield k; |
|
28 |
|
29 end; |
35 *} |
30 *} |
36 |
31 |
37 end |
32 end |