# HG changeset patch
# User haftmann
# Date 1159822853 -7200
# Node ID 099877d83d2b5cdb72d527d2c8a0dca6e4ebab33
# Parent  9e40d815e00201cf317fb485647c020c6f375367
added example for code_gen

diff -r 9e40d815e002 -r 099877d83d2b src/HOL/Extraction/Higman.thy
--- 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
diff -r 9e40d815e002 -r 099877d83d2b src/HOL/Extraction/Pigeonhole.thy
--- 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