# HG changeset patch
# User haftmann
# Date 1238490274 -7200
# Node ID 461da7178275efbbd09a4f6cdc876c1c1142b7e1
# Parent  83642621425affbc5f5064f9dd55e9d34bf6786b# Parent  684720b0b9e69f9c5f9daa1f7c5f97431a17aa38
merged

diff -r 684720b0b9e6 -r 461da7178275 src/HOL/ex/Predicate_Compile.thy
--- a/src/HOL/ex/Predicate_Compile.thy	Mon Mar 30 23:12:13 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Tue Mar 31 11:04:34 2009 +0200
@@ -1,5 +1,5 @@
 theory Predicate_Compile
-imports Complex_Main Lattice_Syntax
+imports Complex_Main Code_Index Lattice_Syntax
 uses "predicate_compile.ML"
 begin
 
@@ -12,10 +12,27 @@
   | "next yield (Predicate.Join P xq) = (case yield P
    of None \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))"
 
-primrec pull :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option)
-  \<Rightarrow> nat \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a list \<times> 'a Predicate.pred" where
-    "pull yield 0 P = ([], \<bottom>)"
-  | "pull yield (Suc n) P = (case yield P
-      of None \<Rightarrow> ([], \<bottom>) | Some (x, Q) \<Rightarrow> let (xs, R) = pull yield n Q in (x # xs, R))"
+ML {*
+let
+  fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ())
+in
+  yield @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
+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))"
+
+ML {*
+let
+  fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ())
+  fun yieldn k = @{code pull} yield k
+in
+  yieldn 0 (*replace with number of elements to retrieve*)
+    @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
+end
+*}
 
 end
\ No newline at end of file