--- a/src/HOL/Lazy_Sequence.thy Wed Apr 28 15:42:10 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy Wed Apr 28 16:56:18 2010 +0200
@@ -123,6 +123,13 @@
subsection {* Code setup *}
+code_reflect
+ datatypes lazy_sequence = Lazy_Sequence
+ functions "Lazy_Sequence.map" yield
+ module_name Lazy_Sequence
+
+(* FIXME formulate yieldn in the logic with type code_numeral *)
+
ML {*
signature LAZY_SEQUENCE =
sig
@@ -135,9 +142,9 @@
structure Lazy_Sequence : LAZY_SEQUENCE =
struct
-@{code_datatype lazy_sequence = Lazy_Sequence}
+open Lazy_Sequence;
-val yield = @{code yield}
+fun map f = mapa f;
fun anamorph f k x = (if k = 0 then ([], x)
else case f x
@@ -148,17 +155,9 @@
fun yieldn S = anamorph yield S;
-val map = @{code map}
-
end;
*}
-code_reserved Eval Lazy_Sequence
-
-code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence")
-
-code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
-
section {* With Hit Bound Value *}
text {* assuming in negative context *}
--- a/src/HOL/Predicate.thy Wed Apr 28 15:42:10 2010 +0200
+++ b/src/HOL/Predicate.thy Wed Apr 28 16:56:18 2010 +0200
@@ -880,6 +880,11 @@
code_abort not_unique
+code_reflect
+ datatypes pred = Seq and seq = Empty | Insert | Join
+ functions map
+ module_name Predicate
+
ML {*
signature PREDICATE =
sig
@@ -893,15 +898,17 @@
structure Predicate : PREDICATE =
struct
-@{code_datatype pred = Seq};
-@{code_datatype seq = Empty | Insert | Join};
+datatype pred = datatype Predicate.pred
+datatype seq = datatype Predicate.seq
+
+fun map f = Predicate.map f;
-fun yield (@{code 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
+fun yield (Seq f) = next (f ())
+and next Empty = NONE
+ | next (Insert (x, P)) = SOME (x, P)
+ | next (Join (P, xq)) = (case yield P
of NONE => next xq
- | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))));
+ | SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq))));
fun anamorph f k x = (if k = 0 then ([], x)
else case f x
@@ -912,19 +919,9 @@
fun yieldn P = anamorph yield P;
-fun map f = @{code map} f;
-
end;
*}
-code_reserved Eval Predicate
-
-code_type pred and seq
- (Eval "_/ Predicate.pred" and "_/ Predicate.seq")
-
-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