# HG changeset patch
# User bulwahn
# Date 1319006241 -7200
# Node ID ae8411edd939f2d3cf309dd1a11526f49a6a8214
# Parent  10c3597f92f0bd857a398cf1ad6d134a8f669852
removing old code generator setup for product types

diff -r 10c3597f92f0 -r ae8411edd939 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 19 08:37:20 2011 +0200
+++ b/src/HOL/Product_Type.thy	Wed Oct 19 08:37:21 2011 +0200
@@ -312,95 +312,6 @@
 code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   (Haskell infix 4 "==")
 
-types_code
-  "prod"     ("(_ */ _)")
-attach (term_of) {*
-fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
-*}
-attach (test) {*
-fun gen_prod aG aT bG bT i =
-  let
-    val (x, t) = aG i;
-    val (y, u) = bG i
-  in ((x, y), fn () => HOLogic.pair_const aT bT $ t () $ u ()) end;
-*}
-
-consts_code
-  "Pair"    ("(_,/ _)")
-
-setup {*
-let
-
-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 (@{const_name prod_case}, _) $ 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 =
-      strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
-
-fun let_codegen thy mode defs dep thyname brack t gr =
-  (case strip_comb t of
-    (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
-    let
-      fun dest_let (l as Const (@{const_name 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 (l, r) gr =
-        let
-          val (pl, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false l gr;
-          val (pr, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false r gr1;
-        in ((pl, pr), gr2) end
-    in case dest_let (t1 $ t2 $ t3) of
-        ([], _) => NONE
-      | (ps, u) =>
-          let
-            val (qs, gr1) = fold_map mk_code ps gr;
-            val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
-            val (pargs, gr3) = fold_map
-              (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
-          in
-            SOME (Codegen.mk_app brack
-              (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
-                  (separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
-                    [Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
-                       Pretty.brk 1, pr]]) qs))),
-                Pretty.brk 1, Codegen.str "in ", pu,
-                Pretty.brk 1, Codegen.str "end"])) pargs, gr3)
-          end
-    end
-  | _ => NONE);
-
-fun split_codegen thy mode defs dep thyname brack t gr = (case strip_comb t of
-    (t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
-      let
-        val ([p], u) = strip_abs_split 1 (t1 $ t2);
-        val (q, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false p gr;
-        val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
-        val (pargs, gr3) = fold_map
-          (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
-      in
-        SOME (Codegen.mk_app brack
-          (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
-            Pretty.brk 1, pu, Codegen.str ")"]) pargs, gr2)
-      end
-  | _ => NONE);
-
-in
-
-  Codegen.add_codegen "let_codegen" let_codegen
-  #> Codegen.add_codegen "split_codegen" split_codegen
-
-end
-*}
-
 
 subsubsection {* Fundamental operations and properties *}