--- a/etc/settings Tue Mar 31 12:59:16 2009 +0200
+++ b/etc/settings Tue Mar 31 12:59:31 2009 +0200
@@ -94,7 +94,7 @@
# Specifically for the HOL image
HOL_USEDIR_OPTIONS=""
-#HOL_USEDIR_OPTIONS="-p 2"
+#HOL_USEDIR_OPTIONS="-p 2 -Q false"
#Source file identification (default: full name + date stamp)
ISABELLE_FILE_IDENT=""
--- a/src/HOL/ex/Predicate_Compile.thy Tue Mar 31 12:59:16 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy Tue Mar 31 12:59:31 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,26 @@
| "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 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 anamorph} 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