# HG changeset patch
# User haftmann
# Date 1140112779 -3600
# Node ID 47532d00e0c8a4cd6f5dd65d7a36e11d0025709d
# Parent  085b5badb8de40bd14cb85a0e889edf901f5e1d1
removed silly stuff

diff -r 085b5badb8de -r 47532d00e0c8 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Thu Feb 16 18:39:48 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy	Thu Feb 16 18:59:39 2006 +0100
@@ -1,76 +1,3 @@
-ML {*
-
-fun strip_abs_split 0 t = ([], t)
-  | strip_abs_split i (Abs (s, T, t)) =
-      let
-        val s' = Codegen.new_name t s;
-        val v = Free (s', T)
-      in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
-  | strip_abs_split i (u as Const ("split", _) $ t) = (case strip_abs_split (i+1) t of
-        (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
-      | _ => ([], u))
-  | strip_abs_split i t = ([], t);
-
-fun let_codegen thy defs gr dep thyname brack t = (case strip_comb t of
-    (t1 as Const ("Let", _), t2 :: t3 :: ts) =>
-    let
-      fun dest_let (l as Const ("Let", _) $ t $ u) =
-          (case strip_abs_split 1 u of
-             ([p], u') => apfst (cons (p, t)) (dest_let u')
-           | _ => ([], l))
-        | dest_let t = ([], t);
-      fun mk_code (gr, (l, r)) =
-        let
-          val (gr1, pl) = Codegen.invoke_codegen thy defs dep thyname false (gr, l);
-          val (gr2, pr) = Codegen.invoke_codegen thy defs dep thyname false (gr1, r);
-        in (gr2, (pl, pr)) end
-    in case dest_let (t1 $ t2 $ t3) of
-        ([], _) => NONE
-      | (ps, u) =>
-          let
-            val (gr1, qs) = foldl_map mk_code (gr, ps);
-            val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
-            val (gr3, pargs) = foldl_map
-              (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
-          in
-            SOME (gr3, Codegen.mk_app brack
-              (Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
-                  (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
-                    [Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
-                       Pretty.brk 1, pr]]) qs))),
-                Pretty.brk 1, Pretty.str "in ", pu,
-                Pretty.brk 1, Pretty.str "end"])) pargs)
-          end
-    end
-  | _ => NONE);
-
-fun split_codegen thy defs gr dep thyname brack t = (case strip_comb t of
-    (t1 as Const ("split", _), t2 :: ts) =>
-      (case strip_abs_split 1 (t1 $ t2) of
-         ([p], u) =>
-           let
-             val (gr1, q) = Codegen.invoke_codegen thy defs dep thyname false (gr, p);
-             val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
-             val (gr3, pargs) = foldl_map
-               (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
-           in
-             SOME (gr2, Codegen.mk_app brack
-               (Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>",
-                 Pretty.brk 1, pu, Pretty.str ")"]) pargs)
-           end
-       | _ => NONE)
-  | _ => NONE);
-
-val prod_codegen_setup =
-  Codegen.add_codegen "let_codegen" let_codegen #>
-  Codegen.add_codegen "split_codegen" split_codegen #>
-  CodegenPackage.add_appconst
-    ("Let", ((2, 2), CodegenPackage.appgen_let strip_abs_split)) #>
-  CodegenPackage.add_appconst
-    ("split", ((1, 1), CodegenPackage.appgen_split strip_abs_split));
-
-*}
-
 (*  Title:      HOL/Library/ExecutableRat.thy
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen