separated code for inductive sequences from inductive_codegen.ML
authorhaftmann
Tue Sep 18 07:36:38 2007 +0200 (2007-09-18)
changeset 246250398a5e802d3
parent 24624 b8383b1bbae3
child 24626 85eceef2edc7
separated code for inductive sequences from inductive_codegen.ML
src/HOL/Inductive.thy
src/HOL/IsaMakefile
src/HOL/Tools/dseq.ML
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Inductive.thy	Tue Sep 18 07:36:15 2007 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Sep 18 07:36:38 2007 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    ("Tools/inductive_package.ML")
     1.5    ("Tools/inductive_set_package.ML")
     1.6    ("Tools/inductive_realizer.ML")
     1.7 +  "Tools/dseq.ML"
     1.8    ("Tools/inductive_codegen.ML")
     1.9    ("Tools/datatype_aux.ML")
    1.10    ("Tools/datatype_prop.ML")
     2.1 --- a/src/HOL/IsaMakefile	Tue Sep 18 07:36:15 2007 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Sep 18 07:36:38 2007 +0200
     2.3 @@ -112,7 +112,8 @@
     2.4    Tools/datatype_case.ML Tools/datatype_codegen.ML			\
     2.5    Tools/datatype_hooks.ML Tools/datatype_package.ML			\
     2.6    Tools/datatype_prop.ML Tools/datatype_realizer.ML			\
     2.7 -  Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML	\
     2.8 +  Tools/datatype_rep_proofs.ML Tools/dseq.ML	\
     2.9 +  Tools/function_package/auto_term.ML	\
    2.10    Tools/function_package/context_tree.ML				\
    2.11    Tools/function_package/fundef_common.ML				\
    2.12    Tools/function_package/fundef_core.ML					\
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/dseq.ML	Tue Sep 18 07:36:38 2007 +0200
     3.3 @@ -0,0 +1,56 @@
     3.4 +(*  Title:      HOL/Tools/DSeq.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Stefan Berghofer, TU Muenchen
     3.7 +
     3.8 +Sequences with recursion depth limit.
     3.9 +*)
    3.10 +
    3.11 +structure DSeq =
    3.12 +struct
    3.13 +
    3.14 +fun maps f s 0 = Seq.empty
    3.15 +  | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
    3.16 +
    3.17 +fun map f s i = Seq.map f (s i);
    3.18 +
    3.19 +fun append s1 s2 i = Seq.append (s1 i) (s2 i);
    3.20 +
    3.21 +fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i);
    3.22 +
    3.23 +fun single x i = Seq.single x;
    3.24 +
    3.25 +fun empty i = Seq.empty;
    3.26 +
    3.27 +fun guard b = if b then single () else empty;
    3.28 +
    3.29 +fun of_list xs i = Seq.of_list xs;
    3.30 +
    3.31 +fun list_of s = Seq.list_of (s ~1);
    3.32 +
    3.33 +fun pull s = Seq.pull (s ~1);
    3.34 +
    3.35 +fun hd s = Seq.hd (s ~1);
    3.36 +
    3.37 +end;
    3.38 +
    3.39 +
    3.40 +(* combinators for code generated from inductive predicates *)
    3.41 +
    3.42 +infix 5 :->;
    3.43 +infix 3 ++;
    3.44 +
    3.45 +fun s :-> f = DSeq.maps f s;
    3.46 +
    3.47 +fun f ++ g = DSeq.append f g;
    3.48 +
    3.49 +val ?? = DSeq.guard;
    3.50 +
    3.51 +fun ??? f g = f o g;
    3.52 +
    3.53 +fun ?! s = is_some (DSeq.pull s);
    3.54 +
    3.55 +fun equal__1 x = DSeq.single x;
    3.56 +
    3.57 +val equal__2 = equal__1;
    3.58 +
    3.59 +fun equal__1_2 (x, y) = ?? (x = y);
     4.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Sep 18 07:36:15 2007 +0200
     4.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Sep 18 07:36:38 2007 +0200
     4.3 @@ -698,54 +698,3 @@
     4.4      Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
     4.5  
     4.6  end;
     4.7 -
     4.8 -
     4.9 -(**** sequences with recursion depth limit ****)
    4.10 -
    4.11 -structure DSeq =
    4.12 -struct
    4.13 -
    4.14 -fun maps f s 0 = Seq.empty
    4.15 -  | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
    4.16 -
    4.17 -fun map f s i = Seq.map f (s i);
    4.18 -
    4.19 -fun append s1 s2 i = Seq.append (s1 i) (s2 i);
    4.20 -
    4.21 -fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i);
    4.22 -
    4.23 -fun single x i = Seq.single x;
    4.24 -
    4.25 -fun empty i = Seq.empty;
    4.26 -
    4.27 -fun of_list xs i = Seq.of_list xs;
    4.28 -
    4.29 -fun list_of s = Seq.list_of (s ~1);
    4.30 -
    4.31 -fun pull s = Seq.pull (s ~1);
    4.32 -
    4.33 -fun hd s = Seq.hd (s ~1);
    4.34 -
    4.35 -end;
    4.36 -
    4.37 -
    4.38 -(**** combinators for code generated from inductive predicates ****)
    4.39 -
    4.40 -infix 5 :->;
    4.41 -infix 3 ++;
    4.42 -
    4.43 -fun s :-> f = DSeq.maps f s;
    4.44 -
    4.45 -fun s1 ++ s2 = DSeq.append s1 s2;
    4.46 -
    4.47 -fun ?? b = if b then DSeq.single () else DSeq.empty;
    4.48 -
    4.49 -fun ??? f g = f o g;
    4.50 -
    4.51 -fun ?! s = is_some (DSeq.pull s);
    4.52 -
    4.53 -fun equal__1 x = DSeq.single x;
    4.54 -
    4.55 -val equal__2 = equal__1;
    4.56 -
    4.57 -fun equal__1_2 (x, y) = ?? (x = y);