# HG changeset patch
# User haftmann
# Date 1272546041 -7200
# Node ID f8df589ca2a59e592790e8450d450ac9296abd55
# Parent  fdfc3725409086703c6668544c08ff2178fb0518
dropped unnecessary ML code

diff -r fdfc37254090 -r f8df589ca2a5 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Thu Apr 29 15:00:41 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Thu Apr 29 15:00:41 2010 +0200
@@ -123,41 +123,18 @@
 
 subsection {* Code setup *}
 
-code_reflect
-  datatypes lazy_sequence = Lazy_Sequence
-  functions map yield
-  module_name Lazy_Sequence
-
-(* FIXME formulate yieldn in the logic with type code_numeral -- get rid of mapa confusion *)
-
-ML {*
-signature LAZY_SEQUENCE =
-sig
-  datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
-  val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
-  val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
-  val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
-  val mapa : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
-end;
+fun anamorph :: "('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> code_numeral \<Rightarrow> 'a \<Rightarrow> 'b list \<times> 'a" 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))"
 
-structure Lazy_Sequence : LAZY_SEQUENCE =
-struct
-
-open Lazy_Sequence;
-
-fun map f = mapa f;
+definition yieldn :: "code_numeral \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a list \<times> 'a lazy_sequence" where
+  "yieldn = anamorph yield"
 
-fun anamorph f k x = (if k = 0 then ([], x)
-  else case f x
-   of NONE => ([], x)
-    | SOME (v, y) => let
-        val (vs, z) = anamorph f (k - 1) y
-      in (v :: vs, z) end);
-
-fun yieldn S = anamorph yield S;
-
-end;
-*}
+code_reflect Lazy_Sequence
+  datatypes lazy_sequence = Lazy_Sequence
+  functions map yield yieldn
 
 section {* With Hit Bound Value *}
 text {* assuming in negative context *}
diff -r fdfc37254090 -r f8df589ca2a5 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Apr 29 15:00:41 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Apr 29 15:00:41 2010 +0200
@@ -3232,14 +3232,14 @@
                 (Code_Eval.eval NONE
                   ("Predicate_Compile_Core.new_random_dseq_stats_eval_ref", new_random_dseq_stats_eval_ref)
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
-                    |> Lazy_Sequence.map (apfst proc))
+                    |> Lazy_Sequence.mapa (apfst proc))
                     thy t' [] nrandom size seed depth))))
             else rpair NONE
               (fst (Lazy_Sequence.yieldn k
                 (Code_Eval.eval NONE
                   ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
-                    |> Lazy_Sequence.map proc)
+                    |> Lazy_Sequence.mapa proc)
                     thy t' [] nrandom size seed depth)))
           end
       | _ =>
diff -r fdfc37254090 -r f8df589ca2a5 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Apr 29 15:00:41 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Apr 29 15:00:41 2010 +0200
@@ -267,7 +267,7 @@
               Code_Eval.eval (SOME target)
                 ("Predicate_Compile_Quickcheck.new_test_ref", new_test_ref)
                 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
-                  g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
+                  g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
                   thy4 qc_term []
           in
             fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield