# HG changeset patch
# User haftmann
# Date 1238490696 -7200
# Node ID 7d02340f095d27d2acdca51b1f33ebfa26e1a70c
# Parent  461da7178275efbbd09a4f6cdc876c1c1142b7e1
generalized pull to anamorph

diff -r 461da7178275 -r 7d02340f095d src/HOL/ex/Predicate_Compile.thy
--- a/src/HOL/ex/Predicate_Compile.thy	Tue Mar 31 11:04:34 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Tue Mar 31 11:11:36 2009 +0200
@@ -20,15 +20,14 @@
 end
 *}
 
-fun pull :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option)
-  \<Rightarrow> index \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a list \<times> 'a Predicate.pred" where
-  "pull yield k P = (if k = 0 then ([], \<bottom>)
-    else case yield P of None \<Rightarrow> ([], \<bottom>) | Some (x, Q) \<Rightarrow> let (xs, R) = pull yield (k - 1) Q in (x # xs, R))"
+fun anamorph :: "('b \<Rightarrow> ('a \<times> 'b) option) \<Rightarrow> index \<Rightarrow> 'b \<Rightarrow> 'a list \<times> 'b" where
+  "anamorph f k x = (if k = 0 then ([], x)
+    else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow> let (vs, z) = anamorph f (k - 1) y in (v # vs, z))"
 
 ML {*
 let
   fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ())
-  fun yieldn k = @{code pull} yield k
+  fun yieldn k = @{code anamorph} yield k
 in
   yieldn 0 (*replace with number of elements to retrieve*)
     @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)