# HG changeset patch # User berghofe # Date 1124979189 -7200 # Node ID e623e57b0f44be64497bbb11e7bf5cc30d83f45f # Parent 6642e0f96f44b6ed1d11b7fdab1706cf247c3ce1 Adapted to new code generator syntax. diff -r 6642e0f96f44 -r e623e57b0f44 src/HOL/Extraction/Higman.thy --- 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 diff -r 6642e0f96f44 -r e623e57b0f44 src/HOL/Extraction/Pigeonhole.thy --- 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 \ nat" ("{* (0::nat, 0::nat) *}") -generate_code +code_module PH +contains test = "\n. pigeonhole n (\m. m - 1)" test' = "\n. pigeonhole_slow n (\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 diff -r 6642e0f96f44 -r e623e57b0f44 src/HOL/Extraction/QuotRem.thy --- 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: "\n::nat. m = n \ m \ n" @@ -46,7 +45,8 @@ @{thm [display] division_correctness [no_vars]} *} -generate_code +code_module Div +contains test = "division 9 2" end diff -r 6642e0f96f44 -r e623e57b0f44 src/HOL/Lambda/WeakNorm.thy --- 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 \ '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); *} diff -r 6642e0f96f44 -r e623e57b0f44 src/HOL/MicroJava/BV/BVExample.thy --- 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 diff -r 6642e0f96f44 -r e623e57b0f44 src/HOL/MicroJava/J/JListExample.thy --- 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\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"); *} diff -r 6642e0f96f44 -r e623e57b0f44 src/HOL/MicroJava/JVM/JVMListExample.thy --- 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