src/HOL/Product_Type.thy
changeset 45205 2825ce94fd4d
parent 45204 5e4a1270c000
parent 45176 df4cbfc5ca4f
child 45607 16b4f5774621
     1.1 --- a/src/HOL/Product_Type.thy	Tue Oct 18 15:19:06 2011 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Oct 19 17:45:25 2011 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  imports Typedef Inductive Fun
     1.5  uses
     1.6    ("Tools/split_rule.ML")
     1.7 -  ("Tools/inductive_codegen.ML")
     1.8    ("Tools/inductive_set.ML")
     1.9  begin
    1.10  
    1.11 @@ -312,95 +311,6 @@
    1.12  code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.13    (Haskell infix 4 "==")
    1.14  
    1.15 -types_code
    1.16 -  "prod"     ("(_ */ _)")
    1.17 -attach (term_of) {*
    1.18 -fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
    1.19 -*}
    1.20 -attach (test) {*
    1.21 -fun gen_prod aG aT bG bT i =
    1.22 -  let
    1.23 -    val (x, t) = aG i;
    1.24 -    val (y, u) = bG i
    1.25 -  in ((x, y), fn () => HOLogic.pair_const aT bT $ t () $ u ()) end;
    1.26 -*}
    1.27 -
    1.28 -consts_code
    1.29 -  "Pair"    ("(_,/ _)")
    1.30 -
    1.31 -setup {*
    1.32 -let
    1.33 -
    1.34 -fun strip_abs_split 0 t = ([], t)
    1.35 -  | strip_abs_split i (Abs (s, T, t)) =
    1.36 -      let
    1.37 -        val s' = Codegen.new_name t s;
    1.38 -        val v = Free (s', T)
    1.39 -      in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
    1.40 -  | strip_abs_split i (u as Const (@{const_name prod_case}, _) $ t) =
    1.41 -      (case strip_abs_split (i+1) t of
    1.42 -        (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
    1.43 -      | _ => ([], u))
    1.44 -  | strip_abs_split i t =
    1.45 -      strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
    1.46 -
    1.47 -fun let_codegen thy mode defs dep thyname brack t gr =
    1.48 -  (case strip_comb t of
    1.49 -    (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
    1.50 -    let
    1.51 -      fun dest_let (l as Const (@{const_name Let}, _) $ t $ u) =
    1.52 -          (case strip_abs_split 1 u of
    1.53 -             ([p], u') => apfst (cons (p, t)) (dest_let u')
    1.54 -           | _ => ([], l))
    1.55 -        | dest_let t = ([], t);
    1.56 -      fun mk_code (l, r) gr =
    1.57 -        let
    1.58 -          val (pl, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false l gr;
    1.59 -          val (pr, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false r gr1;
    1.60 -        in ((pl, pr), gr2) end
    1.61 -    in case dest_let (t1 $ t2 $ t3) of
    1.62 -        ([], _) => NONE
    1.63 -      | (ps, u) =>
    1.64 -          let
    1.65 -            val (qs, gr1) = fold_map mk_code ps gr;
    1.66 -            val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
    1.67 -            val (pargs, gr3) = fold_map
    1.68 -              (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
    1.69 -          in
    1.70 -            SOME (Codegen.mk_app brack
    1.71 -              (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
    1.72 -                  (separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
    1.73 -                    [Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
    1.74 -                       Pretty.brk 1, pr]]) qs))),
    1.75 -                Pretty.brk 1, Codegen.str "in ", pu,
    1.76 -                Pretty.brk 1, Codegen.str "end"])) pargs, gr3)
    1.77 -          end
    1.78 -    end
    1.79 -  | _ => NONE);
    1.80 -
    1.81 -fun split_codegen thy mode defs dep thyname brack t gr = (case strip_comb t of
    1.82 -    (t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
    1.83 -      let
    1.84 -        val ([p], u) = strip_abs_split 1 (t1 $ t2);
    1.85 -        val (q, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false p gr;
    1.86 -        val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
    1.87 -        val (pargs, gr3) = fold_map
    1.88 -          (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
    1.89 -      in
    1.90 -        SOME (Codegen.mk_app brack
    1.91 -          (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
    1.92 -            Pretty.brk 1, pu, Codegen.str ")"]) pargs, gr2)
    1.93 -      end
    1.94 -  | _ => NONE);
    1.95 -
    1.96 -in
    1.97 -
    1.98 -  Codegen.add_codegen "let_codegen" let_codegen
    1.99 -  #> Codegen.add_codegen "split_codegen" split_codegen
   1.100 -
   1.101 -end
   1.102 -*}
   1.103 -
   1.104  
   1.105  subsubsection {* Fundamental operations and properties *}
   1.106  
   1.107 @@ -1203,9 +1113,6 @@
   1.108  
   1.109  subsection {* Inductively defined sets *}
   1.110  
   1.111 -use "Tools/inductive_codegen.ML"
   1.112 -setup Inductive_Codegen.setup
   1.113 -
   1.114  use "Tools/inductive_set.ML"
   1.115  setup Inductive_Set.setup
   1.116