Adapted to new code generator syntax.
--- a/src/HOL/Extraction/Higman.thy Thu Aug 25 16:10:16 2005 +0200
+++ b/src/HOL/Extraction/Higman.thy Thu Aug 25 16:13:09 2005 +0200
@@ -290,10 +290,13 @@
@{thm [display] prop3_def [no_vars]}
*}
-generate_code
+code_module Higman
+contains
test = good_prefix
ML {*
+local open Higman in
+
val a = 16807.0;
val m = 2147483647.0;
@@ -309,27 +312,29 @@
apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
end;
-fun f s id0 = mk_word s 0
+fun f s id_0 = mk_word s 0
| f s (Suc n) = f (fst (mk_word s 0)) n;
val g1 = snd o (f 20000.0);
val g2 = snd o (f 50000.0);
-fun f1 id0 = [A,A]
- | f1 (Suc id0) = [B]
- | f1 (Suc (Suc id0)) = [A,B]
+fun f1 id_0 = [A,A]
+ | f1 (Suc id_0) = [B]
+ | f1 (Suc (Suc id_0)) = [A,B]
| f1 _ = [];
-fun f2 id0 = [A,A]
- | f2 (Suc id0) = [B]
- | f2 (Suc (Suc id0)) = [B,A]
+fun f2 id_0 = [A,A]
+ | f2 (Suc id_0) = [B]
+ | f2 (Suc (Suc id_0)) = [B,A]
| f2 _ = [];
val xs1 = test g1;
val xs2 = test g2;
val xs3 = test f1;
val xs4 = test f2;
+
+end;
*}
end
--- a/src/HOL/Extraction/Pigeonhole.thy Thu Aug 25 16:10:16 2005 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy Thu Aug 25 16:13:09 2005 +0200
@@ -285,19 +285,20 @@
consts_code
arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
-generate_code
+code_module PH
+contains
test = "\<lambda>n. pigeonhole n (\<lambda>m. m - 1)"
test' = "\<lambda>n. pigeonhole_slow n (\<lambda>m. m - 1)"
sel = "op !"
-ML "timeit (fn () => test 10)"
-ML "timeit (fn () => test' 10)"
-ML "timeit (fn () => test 20)"
-ML "timeit (fn () => test' 20)"
-ML "timeit (fn () => test 25)"
-ML "timeit (fn () => test' 25)"
-ML "timeit (fn () => test 500)"
+ML "timeit (fn () => PH.test 10)"
+ML "timeit (fn () => PH.test' 10)"
+ML "timeit (fn () => PH.test 20)"
+ML "timeit (fn () => PH.test' 20)"
+ML "timeit (fn () => PH.test 25)"
+ML "timeit (fn () => PH.test' 25)"
+ML "timeit (fn () => PH.test 500)"
-ML "pigeonhole 8 (sel [0,1,2,3,4,5,6,3,7,8])"
+ML "PH.pigeonhole 8 (PH.sel [0,1,2,3,4,5,6,3,7,8])"
end
--- a/src/HOL/Extraction/QuotRem.thy Thu Aug 25 16:10:16 2005 +0200
+++ b/src/HOL/Extraction/QuotRem.thy Thu Aug 25 16:13:09 2005 +0200
@@ -6,7 +6,6 @@
header {* Quotient and remainder *}
theory QuotRem imports Main begin
-
text {* Derivation of quotient and remainder using program extraction. *}
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
@@ -46,7 +45,8 @@
@{thm [display] division_correctness [no_vars]}
*}
-generate_code
+code_module Div
+contains
test = "division 9 2"
end
--- a/src/HOL/Lambda/WeakNorm.thy Thu Aug 25 16:10:16 2005 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Thu Aug 25 16:13:09 2005 +0200
@@ -524,7 +524,8 @@
arbitrary :: "'a" ("(error \"arbitrary\")")
arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
-generate_code
+code_module Norm
+contains
test = "type_NF"
text {*
@@ -535,29 +536,29 @@
*}
ML {*
-fun nat_of_int 0 = id_0
- | nat_of_int n = Suc (nat_of_int (n-1));
+fun nat_of_int 0 = Norm.id_0
+ | nat_of_int n = Norm.Suc (nat_of_int (n-1));
-fun int_of_nat id_0 = 0
- | int_of_nat (Suc n) = 1 + int_of_nat n;
+fun int_of_nat Norm.id_0 = 0
+ | int_of_nat (Norm.Suc n) = 1 + int_of_nat n;
fun dBtype_of_typ (Type ("fun", [T, U])) =
- Fun (dBtype_of_typ T, dBtype_of_typ U)
+ Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
| dBtype_of_typ (TFree (s, _)) = (case explode s of
- ["'", a] => Atom (nat_of_int (ord a - 97))
+ ["'", a] => Norm.Atom (nat_of_int (ord a - 97))
| _ => error "dBtype_of_typ: variable name")
| dBtype_of_typ _ = error "dBtype_of_typ: bad type";
-fun dB_of_term (Bound i) = dB_Var (nat_of_int i)
- | dB_of_term (t $ u) = dB_App (dB_of_term t, dB_of_term u)
- | dB_of_term (Abs (_, _, t)) = dB_Abs (dB_of_term t)
+fun dB_of_term (Bound i) = Norm.dB_Var (nat_of_int i)
+ | dB_of_term (t $ u) = Norm.App (dB_of_term t, dB_of_term u)
+ | dB_of_term (Abs (_, _, t)) = Norm.Abs (dB_of_term t)
| dB_of_term _ = error "dB_of_term: bad term";
-fun term_of_dB Ts (Type ("fun", [T, U])) (dB_Abs dBt) =
+fun term_of_dB Ts (Type ("fun", [T, U])) (Norm.Abs dBt) =
Abs ("x", T, term_of_dB (T :: Ts) U dBt)
| term_of_dB Ts _ dBt = term_of_dB' Ts dBt
-and term_of_dB' Ts (dB_Var n) = Bound (int_of_nat n)
- | term_of_dB' Ts (dB_App (dBt, dBu)) =
+and term_of_dB' Ts (Norm.dB_Var n) = Bound (int_of_nat n)
+ | term_of_dB' Ts (Norm.App (dBt, dBu)) =
let val t = term_of_dB' Ts dBt
in case fastype_of1 (Ts, t) of
Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
@@ -566,17 +567,17 @@
| term_of_dB' _ _ = error "term_of_dB: term not in normal form";
fun typing_of_term Ts e (Bound i) =
- rtypingT_Var (e, nat_of_int i, dBtype_of_typ (List.nth (Ts, i)))
+ Norm.Var (e, nat_of_int i, dBtype_of_typ (List.nth (Ts, i)))
| typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
- Type ("fun", [T, U]) => rtypingT_App (e, dB_of_term t,
+ Type ("fun", [T, U]) => Norm.rtypingT_App (e, dB_of_term t,
dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
typing_of_term Ts e t, typing_of_term Ts e u)
| _ => error "typing_of_term: function type expected")
| typing_of_term Ts e (Abs (s, T, t)) =
let val dBT = dBtype_of_typ T
- in rtypingT_Abs (e, dBT, dB_of_term t,
+ in Norm.rtypingT_Abs (e, dBT, dB_of_term t,
dBtype_of_typ (fastype_of1 (T :: Ts, t)),
- typing_of_term (T :: Ts) (shift e id_0 dBT) t)
+ typing_of_term (T :: Ts) (Norm.shift e Norm.id_0 dBT) t)
end
| typing_of_term _ _ _ = error "typing_of_term: bad term";
@@ -592,12 +593,12 @@
fun rd s = read_cterm sg (s, TypeInfer.logicT);
val ct1 = rd "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))";
-val (dB1, _) = type_NF (typing_of_term [] dummyf (term_of ct1));
+val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
val ct1' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct1)) dB1);
val ct2 = rd
"%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))";
-val (dB2, _) = type_NF (typing_of_term [] dummyf (term_of ct2));
+val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
val ct2' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct2)) dB2);
*}
--- a/src/HOL/MicroJava/BV/BVExample.thy Thu Aug 25 16:10:16 2005 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Thu Aug 25 16:13:09 2005 +0200
@@ -475,12 +475,13 @@
lemmas [code ind] = rtrancl_refl converse_rtrancl_into_rtrancl
-generate_code
+code_module BV
+contains
test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
[(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
-ML test1
-ML test2
+ML BV.test1
+ML BV.test2
end
--- a/src/HOL/MicroJava/J/JListExample.thy Thu Aug 25 16:10:16 2005 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Thu Aug 25 16:13:09 2005 +0200
@@ -87,7 +87,8 @@
"l3_nam" ("\"l3\"")
"l4_nam" ("\"l4\"")
-generate_code
+code_module J
+contains
test = "example_prg\<turnstile>Norm (empty, empty)
-(Expr (l1_name::=NewC list_name);;
Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));;
@@ -108,19 +109,19 @@
ML {*
-val SOME ((_, (heap, locs)), _) = Seq.pull test;
-locs l1_name;
-locs l2_name;
-locs l3_name;
-locs l4_name;
-snd (the (heap (Loc 0))) (val_name, "list");
-snd (the (heap (Loc 0))) (next_name, "list");
-snd (the (heap (Loc 1))) (val_name, "list");
-snd (the (heap (Loc 1))) (next_name, "list");
-snd (the (heap (Loc 2))) (val_name, "list");
-snd (the (heap (Loc 2))) (next_name, "list");
-snd (the (heap (Loc 3))) (val_name, "list");
-snd (the (heap (Loc 3))) (next_name, "list");
+val SOME ((_, (heap, locs)), _) = Seq.pull J.test;
+locs J.l1_name;
+locs J.l2_name;
+locs J.l3_name;
+locs J.l4_name;
+snd (J.the (heap (J.Loc 0))) (J.val_name, "list");
+snd (J.the (heap (J.Loc 0))) (J.next_name, "list");
+snd (J.the (heap (J.Loc 1))) (J.val_name, "list");
+snd (J.the (heap (J.Loc 1))) (J.next_name, "list");
+snd (J.the (heap (J.Loc 2))) (J.val_name, "list");
+snd (J.the (heap (J.Loc 2))) (J.next_name, "list");
+snd (J.the (heap (J.Loc 3))) (J.val_name, "list");
+snd (J.the (heap (J.Loc 3))) (J.next_name, "list");
*}
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Thu Aug 25 16:10:16 2005 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Thu Aug 25 16:13:09 2005 +0200
@@ -114,62 +114,63 @@
subsection {* Single step execution *}
-generate_code
+code_module JVM
+contains
test = "exec (E, start_state E test_name makelist_name)"
-ML {* test *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
-ML {* exec (E, the it) *}
+ML {* JVM.test *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
end