--- 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 .
--- 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
--- 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 \<times> 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
--- 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 \<Rightarrow> '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