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