# HG changeset patch
# User haftmann
# Date 1190093798 -7200
# Node ID 0398a5e802d33c6f99428bc0face9c454ebbb11a
# Parent  b8383b1bbae39cd73725d67bf7ef7f241bdcd400
separated code for inductive sequences from inductive_codegen.ML

diff -r b8383b1bbae3 -r 0398a5e802d3 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Sep 18 07:36:15 2007 +0200
+++ b/src/HOL/Inductive.thy	Tue Sep 18 07:36:38 2007 +0200
@@ -11,6 +11,7 @@
   ("Tools/inductive_package.ML")
   ("Tools/inductive_set_package.ML")
   ("Tools/inductive_realizer.ML")
+  "Tools/dseq.ML"
   ("Tools/inductive_codegen.ML")
   ("Tools/datatype_aux.ML")
   ("Tools/datatype_prop.ML")
diff -r b8383b1bbae3 -r 0398a5e802d3 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Sep 18 07:36:15 2007 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 18 07:36:38 2007 +0200
@@ -112,7 +112,8 @@
   Tools/datatype_case.ML Tools/datatype_codegen.ML			\
   Tools/datatype_hooks.ML Tools/datatype_package.ML			\
   Tools/datatype_prop.ML Tools/datatype_realizer.ML			\
-  Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML	\
+  Tools/datatype_rep_proofs.ML Tools/dseq.ML	\
+  Tools/function_package/auto_term.ML	\
   Tools/function_package/context_tree.ML				\
   Tools/function_package/fundef_common.ML				\
   Tools/function_package/fundef_core.ML					\
diff -r b8383b1bbae3 -r 0398a5e802d3 src/HOL/Tools/dseq.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/dseq.ML	Tue Sep 18 07:36:38 2007 +0200
@@ -0,0 +1,56 @@
+(*  Title:      HOL/Tools/DSeq.ML
+    ID:         $Id$
+    Author:     Stefan Berghofer, TU Muenchen
+
+Sequences with recursion depth limit.
+*)
+
+structure DSeq =
+struct
+
+fun maps f s 0 = Seq.empty
+  | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
+
+fun map f s i = Seq.map f (s i);
+
+fun append s1 s2 i = Seq.append (s1 i) (s2 i);
+
+fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i);
+
+fun single x i = Seq.single x;
+
+fun empty i = Seq.empty;
+
+fun guard b = if b then single () else empty;
+
+fun of_list xs i = Seq.of_list xs;
+
+fun list_of s = Seq.list_of (s ~1);
+
+fun pull s = Seq.pull (s ~1);
+
+fun hd s = Seq.hd (s ~1);
+
+end;
+
+
+(* combinators for code generated from inductive predicates *)
+
+infix 5 :->;
+infix 3 ++;
+
+fun s :-> f = DSeq.maps f s;
+
+fun f ++ g = DSeq.append f g;
+
+val ?? = DSeq.guard;
+
+fun ??? f g = f o g;
+
+fun ?! s = is_some (DSeq.pull s);
+
+fun equal__1 x = DSeq.single x;
+
+val equal__2 = equal__1;
+
+fun equal__1_2 (x, y) = ?? (x = y);
diff -r b8383b1bbae3 -r 0398a5e802d3 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Tue Sep 18 07:36:15 2007 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Sep 18 07:36:38 2007 +0200
@@ -698,54 +698,3 @@
     Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
 
 end;
-
-
-(**** sequences with recursion depth limit ****)
-
-structure DSeq =
-struct
-
-fun maps f s 0 = Seq.empty
-  | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
-
-fun map f s i = Seq.map f (s i);
-
-fun append s1 s2 i = Seq.append (s1 i) (s2 i);
-
-fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i);
-
-fun single x i = Seq.single x;
-
-fun empty i = Seq.empty;
-
-fun of_list xs i = Seq.of_list xs;
-
-fun list_of s = Seq.list_of (s ~1);
-
-fun pull s = Seq.pull (s ~1);
-
-fun hd s = Seq.hd (s ~1);
-
-end;
-
-
-(**** combinators for code generated from inductive predicates ****)
-
-infix 5 :->;
-infix 3 ++;
-
-fun s :-> f = DSeq.maps f s;
-
-fun s1 ++ s2 = DSeq.append s1 s2;
-
-fun ?? b = if b then DSeq.single () else DSeq.empty;
-
-fun ??? f g = f o g;
-
-fun ?! s = is_some (DSeq.pull s);
-
-fun equal__1 x = DSeq.single x;
-
-val equal__2 = equal__1;
-
-fun equal__1_2 (x, y) = ?? (x = y);