# HG changeset patch # User bulwahn # Date 1319006234 -7200 # Node ID 4baa475a51e66a5cfcddc79bcb29c247b9850f27 # Parent 0e8e662013f919532b47a7d97415ab07ec0c537c removing invocations of the old code generator diff -r 0e8e662013f9 -r 4baa475a51e6 src/HOL/Library/Transitive_Closure_Table.thy --- a/src/HOL/Library/Transitive_Closure_Table.thy Tue Oct 18 15:40:59 2011 +0200 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Wed Oct 19 08:37:14 2011 +0200 @@ -201,22 +201,6 @@ | "test B A" | "test B C" -subsubsection {* Invoking with the (legacy) SML code generator *} - -text {* this test can be removed once the SML code generator is deactivated *} - -code_module Test -contains -test1 = "test\<^sup>*\<^sup>* A C" -test2 = "test\<^sup>*\<^sup>* C A" -test3 = "test\<^sup>*\<^sup>* A _" -test4 = "test\<^sup>*\<^sup>* _ C" - -ML "Test.test1" -ML "Test.test2" -ML "DSeq.list_of Test.test3" -ML "DSeq.list_of Test.test4" - subsubsection {* Invoking with the predicate compiler and the generic code generator *} code_pred test . diff -r 0e8e662013f9 -r 4baa475a51e6 src/HOL/Proofs/Extraction/Higman_Extraction.thy --- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy Tue Oct 18 15:40:59 2011 +0200 +++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy Wed Oct 19 08:37:14 2011 +0200 @@ -107,58 +107,4 @@ end; *} -text {* The same story with the legacy SML code generator, -this can be removed once the code generator is removed. *} - -code_module Higman -contains - higman = higman_idx - -ML {* -local open Higman 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 zero = 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 zero = [A,A] - | f1 (Suc zero) = [B] - | f1 (Suc (Suc zero)) = [A,B] - | f1 _ = []; - -fun f2 zero = [A,A] - | f2 (Suc zero) = [B] - | f2 (Suc (Suc zero)) = [B,A] - | f2 _ = []; - -val (i1, j1) = higman g1; -val (v1, w1) = (g1 i1, g1 j1); -val (i2, j2) = higman g2; -val (v2, w2) = (g2 i2, g2 j2); -val (i3, j3) = higman f1; -val (v3, w3) = (f1 i3, f1 j3); -val (i4, j4) = higman f2; -val (v4, w4) = (f2 i4, f2 j4); - -end; -*} - end diff -r 0e8e662013f9 -r 4baa475a51e6 src/HOL/Proofs/Extraction/Pigeonhole.thy --- a/src/HOL/Proofs/Extraction/Pigeonhole.thy Tue Oct 18 15:40:59 2011 +0200 +++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy Wed Oct 19 08:37:14 2011 +0200 @@ -252,28 +252,5 @@ ML "timeit (@{code test} 500)" ML "timeit @{code test''}" -text {* the same story with the legacy SML code generator. -this can be removed once the code generator is removed. -*} - -consts_code - "default :: nat" ("{* 0::nat *}") - "default :: nat \ nat" ("{* (0::nat, 0::nat) *}") - -code_module PH -contains - test = test - test' = test' - test'' = test'' - -ML "timeit (PH.test 10)" -ML "timeit (PH.test' 10)" -ML "timeit (PH.test 20)" -ML "timeit (PH.test' 20)" -ML "timeit (PH.test 25)" -ML "timeit (PH.test' 25)" -ML "timeit (PH.test 500)" -ML "timeit PH.test''" - end diff -r 0e8e662013f9 -r 4baa475a51e6 src/HOL/Proofs/Lambda/WeakNorm.thy --- a/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Oct 18 15:40:59 2011 +0200 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Wed Oct 19 08:37:14 2011 +0200 @@ -437,81 +437,4 @@ val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2); *} - -text {* -The same story again for the (legacy) SML code generator. -This can be removed once the SML code generator is removed. -*} - -consts_code - "default" ("(error \"default\")") - "default :: 'a \ 'b::default" ("(fn '_ => error \"default\")") - -code_module Norm -contains - test = "type_NF" - -ML {* -fun nat_of_int 0 = Norm.zero - | nat_of_int n = Norm.Suc (nat_of_int (n-1)); - -fun int_of_nat Norm.zero = 0 - | int_of_nat (Norm.Suc n) = 1 + int_of_nat n; - -fun dBtype_of_typ (Type ("fun", [T, U])) = - Norm.Fun (dBtype_of_typ T, dBtype_of_typ U) - | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of - ["'", 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) = 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])) (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 (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 - | _ => error "term_of_dB: function type expected" - end - | term_of_dB' _ _ = error "term_of_dB: term not in normal form"; - -fun typing_of_term Ts e (Bound i) = - Norm.Var (e, nat_of_int i, dBtype_of_typ (nth Ts i)) - | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of - 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 Norm.rtypingT_Abs (e, dBT, dB_of_term t, - dBtype_of_typ (fastype_of1 (T :: Ts, t)), - typing_of_term (T :: Ts) (Norm.shift e Norm.zero dBT) t) - end - | typing_of_term _ _ _ = error "typing_of_term: bad term"; - -fun dummyf _ = error "dummy"; -*} - -text {* -We now try out the extracted program @{text "type_NF"} on some example terms. -*} - -ML {* -val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"}; -val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1)); -val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1); - -val ct2 = @{cterm "%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, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2)); -val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2); -*} - end