--- a/src/HOL/Extraction/Higman.thy Mon Oct 02 23:00:52 2006 +0200
+++ b/src/HOL/Extraction/Higman.thy Mon Oct 02 23:00:53 2006 +0200
@@ -294,9 +294,6 @@
contains
test = good_prefix
-declare barT.recs(2) [where ?fun = ?func, code func]
-code_gen good_prefix (SML -)
-
ML {*
local open Higman in
@@ -340,4 +337,52 @@
end;
*}
+code_gen good_prefix (SML -)
+
+ML {*
+local
+ open ROOT.Higman
+ open ROOT.IntDef
+in
+
+val a = 16807.0;
+val m = 2147483647.0;
+
+fun nextRand seed =
+ let val t = a*seed
+ in t - m * real (Real.floor(t/m)) end;
+
+fun mk_word seed l =
+ let
+ val r = nextRand seed;
+ val i = Real.round (r / m * 10.0);
+ in if i > 7 andalso l > 2 then (r, []) else
+ apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
+ end;
+
+fun f s id_0 = mk_word s 0
+ | f s (Succ_nat n) = f (fst (mk_word s 0)) n;
+
+val g1 = snd o (f 20000.0);
+
+val g2 = snd o (f 50000.0);
+
+fun f1 id_0 = [A,A]
+ | f1 (Succ_nat id_0) = [B]
+ | f1 (Succ_nat (Succ_nat id_0)) = [A,B]
+ | f1 _ = [];
+
+fun f2 id_0 = [A,A]
+ | f2 (Succ_nat id_0) = [B]
+ | f2 (Succ_nat (Succ_nat id_0)) = [B,A]
+ | f2 _ = [];
+
+val xs1 = good_prefix g1;
+val xs2 = good_prefix g2;
+val xs3 = good_prefix f1;
+val xs4 = good_prefix f2;
+
+end;
+*}
+
end
--- a/src/HOL/Extraction/Pigeonhole.thy Mon Oct 02 23:00:52 2006 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy Mon Oct 02 23:00:53 2006 +0200
@@ -285,9 +285,6 @@
consts_code
arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
-code_const "arbitrary \<Colon> nat \<times> nat"
- (SML "{* (0\<Colon>nat, 0\<Colon>nat) *}")
-
code_module PH
contains
test = "\<lambda>n. pigeonhole n (\<lambda>m. m - 1)"
@@ -304,4 +301,32 @@
ML "PH.pigeonhole 8 (PH.sel [0,1,2,3,4,5,6,3,7,8])"
+definition
+ arbitrary_nat :: "nat \<times> nat"
+ "arbitrary_nat = arbitrary"
+
+lemma [code func]:
+ "arbitrary_nat = arbitrary_nat" ..
+
+declare arbitrary_nat_def [symmetric, code inline]
+
+code_const arbitrary_nat
+ (SML "{* (0\<Colon>nat, 0\<Colon>nat) *}")
+
+definition
+ "test n = pigeonhole n (\<lambda>m. m - 1)"
+ "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
+
+code_gen test test' "op !" (SML -)
+
+ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
+ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
+ML "timeit (fn () => ROOT.Pigeonhole.test 20)"
+ML "timeit (fn () => ROOT.Pigeonhole.test' 20)"
+ML "timeit (fn () => ROOT.Pigeonhole.test 25)"
+ML "timeit (fn () => ROOT.Pigeonhole.test' 25)"
+ML "timeit (fn () => ROOT.Pigeonhole.test 500)"
+
+ML "ROOT.Pigeonhole.pigeonhole 8 (ROOT.List.nth [0,1,2,3,4,5,6,3,7,8])"
+
end