New code generator for let and split.
authorberghofe
Fri Dec 10 16:48:01 2004 +0100 (2004-12-10)
changeset 15394a2c34e6ca4f8
parent 15393 2e6a9146caca
child 15395 b93cdbac8f46
New code generator for let and split.
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Fri Dec 10 16:47:15 2004 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Dec 10 16:48:01 2004 +0100
     1.3 @@ -742,4 +742,86 @@
     1.4  use "Tools/split_rule.ML"
     1.5  setup SplitRule.setup
     1.6  
     1.7 +
     1.8 +subsection {* Code generator setup *}
     1.9 +
    1.10 +types_code
    1.11 +  "*"     ("(_ */ _)")
    1.12 +
    1.13 +consts_code
    1.14 +  "Pair"    ("(_,/ _)")
    1.15 +  "fst"     ("fst")
    1.16 +  "snd"     ("snd")
    1.17 +
    1.18 +ML {*
    1.19 +fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
    1.20 +
    1.21 +fun gen_id_42 aG bG i = (aG i, bG i);
    1.22 +
    1.23 +local
    1.24 +
    1.25 +fun strip_abs 0 t = ([], t)
    1.26 +  | strip_abs i (Abs (s, T, t)) =
    1.27 +    let
    1.28 +      val s' = Codegen.new_name t s;
    1.29 +      val v = Free (s', T)
    1.30 +    in apfst (cons v) (strip_abs (i-1) (subst_bound (v, t))) end
    1.31 +  | strip_abs i (u as Const ("split", _) $ t) = (case strip_abs (i+1) t of
    1.32 +        (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
    1.33 +      | _ => ([], u))
    1.34 +  | strip_abs i t = ([], t);
    1.35 +
    1.36 +fun let_codegen thy gr dep brack (t as Const ("Let", _) $ _ $ _) =
    1.37 +    let
    1.38 +      fun dest_let (l as Const ("Let", _) $ t $ u) =
    1.39 +          (case strip_abs 1 u of
    1.40 +             ([p], u') => apfst (cons (p, t)) (dest_let u')
    1.41 +           | _ => ([], l))
    1.42 +        | dest_let t = ([], t);
    1.43 +      fun mk_code (gr, (l, r)) =
    1.44 +        let
    1.45 +          val (gr1, pl) = Codegen.invoke_codegen thy dep false (gr, l);
    1.46 +          val (gr2, pr) = Codegen.invoke_codegen thy dep false (gr1, r);
    1.47 +        in (gr2, (pl, pr)) end
    1.48 +    in case dest_let t of
    1.49 +        ([], _) => None
    1.50 +      | (ps, u) =>
    1.51 +          let
    1.52 +            val (gr1, qs) = foldl_map mk_code (gr, ps);
    1.53 +            val (gr2, pu) = Codegen.invoke_codegen thy dep false (gr1, u)
    1.54 +          in
    1.55 +            Some (gr2, Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, flat
    1.56 +                (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
    1.57 +                  [Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
    1.58 +                     Pretty.brk 1, pr]]) qs))),
    1.59 +              Pretty.brk 1, Pretty.str "in ", pu,
    1.60 +              Pretty.brk 1, Pretty.str "end"]))
    1.61 +          end
    1.62 +    end
    1.63 +  | let_codegen thy gr dep brack t = None;
    1.64 +
    1.65 +fun split_codegen thy gr dep brack (t as Const ("split", _) $ _) =
    1.66 +    (case strip_abs 1 t of
    1.67 +       ([p], u) =>
    1.68 +         let
    1.69 +           val (gr1, q) = Codegen.invoke_codegen thy dep false (gr, p);
    1.70 +           val (gr2, pu) = Codegen.invoke_codegen thy dep false (gr1, u)
    1.71 +         in
    1.72 +           Some (gr2, Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>",
    1.73 +             Pretty.brk 1, pu, Pretty.str ")"])
    1.74 +         end
    1.75 +     | _ => None)
    1.76 +  | split_codegen thy gr dep brack t = None;
    1.77 +
    1.78 +in
    1.79 +
    1.80 +val prod_codegen_setup =
    1.81 +  [Codegen.add_codegen "let_codegen" let_codegen,
    1.82 +   Codegen.add_codegen "split_codegen" split_codegen];
    1.83 +
    1.84 +end;
    1.85 +*}
    1.86 +
    1.87 +setup prod_codegen_setup
    1.88 +
    1.89  end