src/HOL/Product_Type.thy
changeset 45175 ae8411edd939
parent 44921 58eef4843641
child 45176 df4cbfc5ca4f
     1.1 --- a/src/HOL/Product_Type.thy	Wed Oct 19 08:37:20 2011 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Oct 19 08:37:21 2011 +0200
     1.3 @@ -312,95 +312,6 @@
     1.4  code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
     1.5    (Haskell infix 4 "==")
     1.6  
     1.7 -types_code
     1.8 -  "prod"     ("(_ */ _)")
     1.9 -attach (term_of) {*
    1.10 -fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
    1.11 -*}
    1.12 -attach (test) {*
    1.13 -fun gen_prod aG aT bG bT i =
    1.14 -  let
    1.15 -    val (x, t) = aG i;
    1.16 -    val (y, u) = bG i
    1.17 -  in ((x, y), fn () => HOLogic.pair_const aT bT $ t () $ u ()) end;
    1.18 -*}
    1.19 -
    1.20 -consts_code
    1.21 -  "Pair"    ("(_,/ _)")
    1.22 -
    1.23 -setup {*
    1.24 -let
    1.25 -
    1.26 -fun strip_abs_split 0 t = ([], t)
    1.27 -  | strip_abs_split i (Abs (s, T, t)) =
    1.28 -      let
    1.29 -        val s' = Codegen.new_name t s;
    1.30 -        val v = Free (s', T)
    1.31 -      in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
    1.32 -  | strip_abs_split i (u as Const (@{const_name prod_case}, _) $ t) =
    1.33 -      (case strip_abs_split (i+1) t of
    1.34 -        (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
    1.35 -      | _ => ([], u))
    1.36 -  | strip_abs_split i t =
    1.37 -      strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
    1.38 -
    1.39 -fun let_codegen thy mode defs dep thyname brack t gr =
    1.40 -  (case strip_comb t of
    1.41 -    (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
    1.42 -    let
    1.43 -      fun dest_let (l as Const (@{const_name Let}, _) $ t $ u) =
    1.44 -          (case strip_abs_split 1 u of
    1.45 -             ([p], u') => apfst (cons (p, t)) (dest_let u')
    1.46 -           | _ => ([], l))
    1.47 -        | dest_let t = ([], t);
    1.48 -      fun mk_code (l, r) gr =
    1.49 -        let
    1.50 -          val (pl, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false l gr;
    1.51 -          val (pr, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false r gr1;
    1.52 -        in ((pl, pr), gr2) end
    1.53 -    in case dest_let (t1 $ t2 $ t3) of
    1.54 -        ([], _) => NONE
    1.55 -      | (ps, u) =>
    1.56 -          let
    1.57 -            val (qs, gr1) = fold_map mk_code ps gr;
    1.58 -            val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
    1.59 -            val (pargs, gr3) = fold_map
    1.60 -              (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
    1.61 -          in
    1.62 -            SOME (Codegen.mk_app brack
    1.63 -              (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
    1.64 -                  (separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
    1.65 -                    [Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
    1.66 -                       Pretty.brk 1, pr]]) qs))),
    1.67 -                Pretty.brk 1, Codegen.str "in ", pu,
    1.68 -                Pretty.brk 1, Codegen.str "end"])) pargs, gr3)
    1.69 -          end
    1.70 -    end
    1.71 -  | _ => NONE);
    1.72 -
    1.73 -fun split_codegen thy mode defs dep thyname brack t gr = (case strip_comb t of
    1.74 -    (t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
    1.75 -      let
    1.76 -        val ([p], u) = strip_abs_split 1 (t1 $ t2);
    1.77 -        val (q, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false p gr;
    1.78 -        val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
    1.79 -        val (pargs, gr3) = fold_map
    1.80 -          (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
    1.81 -      in
    1.82 -        SOME (Codegen.mk_app brack
    1.83 -          (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
    1.84 -            Pretty.brk 1, pu, Codegen.str ")"]) pargs, gr2)
    1.85 -      end
    1.86 -  | _ => NONE);
    1.87 -
    1.88 -in
    1.89 -
    1.90 -  Codegen.add_codegen "let_codegen" let_codegen
    1.91 -  #> Codegen.add_codegen "split_codegen" split_codegen
    1.92 -
    1.93 -end
    1.94 -*}
    1.95 -
    1.96  
    1.97  subsubsection {* Fundamental operations and properties *}
    1.98