# HG changeset patch
# User haftmann
# Date 1240420159 -7200
# Node ID 458e55fd0a338a13b27639f9fcffbee13090d6d2
# Parent  d8a30cdae862b9d7d76e39eadd63b8e1ba8244ad
fixed compilation of predicate types in ML environment

diff -r d8a30cdae862 -r 458e55fd0a33 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Tue Apr 21 15:48:02 2009 +0200
+++ b/src/HOL/Predicate.thy	Wed Apr 22 19:09:19 2009 +0200
@@ -622,19 +622,38 @@
   "pred_rec f P = f (eval P)"
   by (cases P) simp
 
-export_code Seq in Eval module_name Predicate
+text {* for evaluation of predicate enumerations *}
 
 ML {*
 signature PREDICATE =
 sig
   datatype 'a pred = Seq of (unit -> 'a seq)
   and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
+  val yield: 'a pred -> ('a * 'a pred) option
+  val yieldn: int -> 'a pred -> 'a list * 'a pred
 end;
 
 structure Predicate : PREDICATE =
 struct
 
-open Predicate;
+@{code_datatype pred = Seq};
+@{code_datatype seq = Empty | Insert | Join};
+
+fun yield (Seq f) = next (f ())
+and next @{code Empty} = NONE
+  | next (@{code Insert} (x, P)) = SOME (x, P)
+  | next (@{code Join} (P, xq)) = (case yield P
+     of NONE => next xq
+      | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))))
+
+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 P = anamorph yield P;
 
 end;
 *}
@@ -647,6 +666,7 @@
 code_const Seq and Empty and Insert and Join
   (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
 
+
 no_notation
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65) and