# 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 \<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
 
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 \<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