Added call to Codegen.preprocess.
authorberghofe
Tue Oct 26 16:26:53 2004 +0200 (2004-10-26)
changeset 1525719dcdea98649
parent 15256 9237f388fbb1
child 15258 b93efa469f92
Added call to Codegen.preprocess.
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/recfun_codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Oct 26 16:25:41 2004 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Oct 26 16:26:53 2004 +0200
     1.3 @@ -72,12 +72,12 @@
     1.4    in case Symtab.lookup (intros, s) of
     1.5        None => (case InductivePackage.get_inductive thy s of
     1.6          None => None
     1.7 -      | Some ({names, ...}, {intrs, ...}) => Some (names, intrs))
     1.8 +      | Some ({names, ...}, {intrs, ...}) => Some (names, preprocess thy intrs))
     1.9      | Some _ =>
    1.10          let val Some names = find_first
    1.11            (fn xs => s mem xs) (Graph.strong_conn graph)
    1.12 -        in Some (names,
    1.13 -          flat (map (fn s => the (Symtab.lookup (intros, s))) names))
    1.14 +        in Some (names, preprocess thy
    1.15 +          (flat (map (fn s => the (Symtab.lookup (intros, s))) names)))
    1.16          end
    1.17    end;
    1.18  
    1.19 @@ -692,7 +692,7 @@
    1.20          None => list_of_indset thy gr dep brack t
    1.21        | Some eqns =>
    1.22            let
    1.23 -            val gr' = mk_fun thy s eqns dep gr
    1.24 +            val gr' = mk_fun thy s (preprocess thy eqns) dep gr
    1.25              val (gr'', ps) = foldl_map (invoke_codegen thy dep true) (gr', ts);
    1.26            in Some (gr'', mk_app brack (Pretty.str (mk_const_id
    1.27              (sign_of thy) s)) ps)
     2.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Oct 26 16:25:41 2004 +0200
     2.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Oct 26 16:26:53 2004 +0200
     2.3 @@ -62,8 +62,8 @@
     2.4  fun get_equations thy (s, T) =
     2.5    (case Symtab.lookup (CodegenData.get thy, s) of
     2.6       None => []
     2.7 -   | Some thms => filter (fn thm => is_instance thy T
     2.8 -       (snd (const_of (prop_of thm)))) thms);
     2.9 +   | Some thms => preprocess thy (filter (fn thm => is_instance thy T
    2.10 +       (snd (const_of (prop_of thm)))) thms));
    2.11  
    2.12  fun mk_poly_id thy (s, T) = mk_const_id (sign_of thy) s ^
    2.13    (case get_defn thy s T of
    2.14 @@ -133,9 +133,10 @@
    2.15    end;
    2.16  
    2.17  fun recfun_codegen thy gr dep brack t = (case strip_comb t of
    2.18 -    (Const p, ts) => (case get_equations thy p of
    2.19 -       [] => None
    2.20 -     | eqns =>
    2.21 +    (Const (p as (s, T)), ts) => (case (get_equations thy p, get_assoc_code thy s T) of
    2.22 +       ([], _) => None
    2.23 +     | (_, Some _) => None
    2.24 +     | (eqns, None) =>
    2.25          let val (gr', ps) = foldl_map (invoke_codegen thy dep true) (gr, ts)
    2.26          in
    2.27            Some (add_rec_funs thy gr' dep (map prop_of eqns),