1.1 --- a/src/HOL/ex/Predicate_Compile.thy	Sun Mar 29 19:48:35 2009 +0200
     1.2 +++ b/src/HOL/ex/Predicate_Compile.thy	Tue Mar 31 11:04:05 2009 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  theory Predicate_Compile
     1.5 -imports Complex_Main Lattice_Syntax
     1.6 +imports Complex_Main Code_Index Lattice_Syntax
     1.7  uses "predicate_compile.ML"
     1.8  begin
     1.9  
    1.10 @@ -12,10 +12,27 @@
    1.11    | "next yield (Predicate.Join P xq) = (case yield P
    1.12     of None \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))"
    1.13  
    1.14 -primrec pull :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option)
    1.15 -  \<Rightarrow> nat \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a list \<times> 'a Predicate.pred" where
    1.16 -    "pull yield 0 P = ([], \<bottom>)"
    1.17 -  | "pull yield (Suc n) P = (case yield P
    1.18 -      of None \<Rightarrow> ([], \<bottom>) | Some (x, Q) \<Rightarrow> let (xs, R) = pull yield n Q in (x # xs, R))"
    1.19 +ML {*
    1.20 +let
    1.21 +  fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ())
    1.22 +in
    1.23 +  yield @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
    1.24 +end
    1.25 +*}
    1.26 +
    1.27 +fun pull :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option)
    1.28 +  \<Rightarrow> index \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a list \<times> 'a Predicate.pred" where
    1.29 +  "pull yield k P = (if k = 0 then ([], \<bottom>)
    1.30 +    else case yield P of None \<Rightarrow> ([], \<bottom>) | Some (x, Q) \<Rightarrow> let (xs, R) = pull yield (k - 1) Q in (x # xs, R))"
    1.31 +
    1.32 +ML {*
    1.33 +let
    1.34 +  fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ())
    1.35 +  fun yieldn k = @{code pull} yield k
    1.36 +in
    1.37 +  yieldn 0 (*replace with number of elements to retrieve*)
    1.38 +    @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
    1.39 +end
    1.40 +*}
    1.41  
    1.42  end
    1.43 \ No newline at end of file