src/Tools/Code/code_preproc.ML
author haftmann
Thu Dec 29 10:47:54 2011 +0100 (2011-12-29)
changeset 46026 83caa4f4bd56
parent 45230 1b08942bb86f
child 46497 89ccf66aa73d
permissions -rw-r--r--
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
     1 (*  Title:      Tools/Code/code_preproc.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Preprocessing code equations into a well-sorted system
     5 in a graph with explicit dependencies.
     6 *)
     7 
     8 signature CODE_PREPROC =
     9 sig
    10   val map_pre: (simpset -> simpset) -> theory -> theory
    11   val map_post: (simpset -> simpset) -> theory -> theory
    12   val add_unfold: thm -> theory -> theory
    13   val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
    14   val del_functrans: string -> theory -> theory
    15   val simple_functrans: (theory -> thm list -> thm list option)
    16     -> theory -> (thm * bool) list -> (thm * bool) list option
    17   val preprocess_functrans: theory -> (thm * bool) list -> (thm * bool) list
    18   val print_codeproc: theory -> unit
    19 
    20   type code_algebra
    21   type code_graph
    22   val cert: code_graph -> string -> Code.cert
    23   val sortargs: code_graph -> string -> sort list
    24   val all: code_graph -> string list
    25   val pretty: theory -> code_graph -> Pretty.T
    26   val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
    27   val dynamic_conv: theory
    28     -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
    29   val dynamic_value: theory -> ((term -> term) -> 'a -> 'a)
    30     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
    31   val static_conv: theory -> string list
    32     -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
    33   val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
    34     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
    35 
    36   val setup: theory -> theory
    37 end
    38 
    39 structure Code_Preproc : CODE_PREPROC =
    40 struct
    41 
    42 (** preprocessor administration **)
    43 
    44 (* theory data *)
    45 
    46 datatype thmproc = Thmproc of {
    47   pre: simpset,
    48   post: simpset,
    49   functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
    50 };
    51 
    52 fun make_thmproc ((pre, post), functrans) =
    53   Thmproc { pre = pre, post = post, functrans = functrans };
    54 fun map_thmproc f (Thmproc { pre, post, functrans }) =
    55   make_thmproc (f ((pre, post), functrans));
    56 fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 },
    57   Thmproc { pre = pre2, post = post2, functrans = functrans2 }) =
    58     let
    59       val pre = Simplifier.merge_ss (pre1, pre2);
    60       val post = Simplifier.merge_ss (post1, post2);
    61       val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2)
    62         handle AList.DUP => error ("Duplicate function transformer");
    63     in make_thmproc ((pre, post), functrans) end;
    64 
    65 structure Code_Preproc_Data = Theory_Data
    66 (
    67   type T = thmproc;
    68   val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
    69   val extend = I;
    70   val merge = merge_thmproc;
    71 );
    72 
    73 fun the_thmproc thy = case Code_Preproc_Data.get thy
    74  of Thmproc x => x;
    75 
    76 fun delete_force msg key xs =
    77   if AList.defined (op =) xs key then AList.delete (op =) key xs
    78   else error ("No such " ^ msg ^ ": " ^ quote key);
    79 
    80 val map_data = Code_Preproc_Data.map o map_thmproc;
    81 
    82 val map_pre_post = map_data o apfst;
    83 val map_pre = map_pre_post o apfst;
    84 val map_post = map_pre_post o apsnd;
    85 
    86 val add_unfold = map_pre o Simplifier.add_simp;
    87 val del_unfold = map_pre o Simplifier.del_simp;
    88 val add_post = map_post o Simplifier.add_simp;
    89 val del_post = map_post o Simplifier.del_simp;
    90 
    91 fun add_code_abbrev raw_thm thy =
    92   let
    93     val thm = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy) raw_thm;
    94     val thm_sym = Thm.symmetric thm;
    95   in
    96     thy |> map_pre_post (fn (pre, post) =>
    97       (pre |> Simplifier.add_simp thm_sym, post |> Simplifier.add_simp thm))
    98   end;
    99 
   100 fun add_functrans (name, f) = (map_data o apsnd)
   101   (AList.update (op =) (name, (serial (), f)));
   102 
   103 fun del_functrans name = (map_data o apsnd)
   104   (delete_force "function transformer" name);
   105 
   106 
   107 (* post- and preprocessing *)
   108 
   109 fun no_variables_conv conv ct =
   110   let
   111     val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
   112     val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t)
   113       | t as Var _ => insert (op aconvc) (cert t)
   114       | _ => I) (Thm.term_of ct) [];
   115     fun apply_beta var thm = Thm.combination thm (Thm.reflexive var)
   116       |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
   117       |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
   118   in
   119     ct
   120     |> fold_rev Thm.cabs all_vars
   121     |> conv
   122     |> fold apply_beta all_vars
   123   end;
   124 
   125 fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
   126 
   127 fun eqn_conv conv ct =
   128   let
   129     fun lhs_conv ct = if can Thm.dest_comb ct
   130       then Conv.combination_conv lhs_conv conv ct
   131       else Conv.all_conv ct;
   132   in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end;
   133 
   134 val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
   135 
   136 fun term_of_conv thy conv =
   137   Thm.cterm_of thy
   138   #> conv
   139   #> Thm.prop_of
   140   #> Logic.dest_equals
   141   #> snd;
   142 
   143 fun term_of_conv_resubst thy conv t =
   144   let
   145     val all_vars = fold_aterms (fn t as Free _ => insert (op aconv) t
   146       | t as Var _ => insert (op aconv) t
   147       | _ => I) t [];
   148     val resubst = curry (Term.betapplys o swap) all_vars;
   149   in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
   150 
   151 
   152 fun preprocess_functrans thy = 
   153   let
   154     val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
   155       o the_thmproc) thy;
   156   in perhaps (perhaps_loop (perhaps_apply functrans)) end;
   157 
   158 fun preprocess thy =
   159   let
   160     val ctxt = Proof_Context.init_global thy;
   161     val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   162   in
   163     preprocess_functrans thy
   164     #> (map o apfst) (singleton (Variable.trade (K (map (rewrite_eqn pre))) ctxt)) 
   165   end;
   166 
   167 fun preprocess_conv thy =
   168   let
   169     val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   170   in
   171     Simplifier.rewrite pre
   172     #> trans_conv_rule (AxClass.unoverload_conv thy)
   173   end;
   174 
   175 fun preprocess_term thy = term_of_conv_resubst thy (preprocess_conv thy);
   176 
   177 fun postprocess_conv thy =
   178   let
   179     val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
   180   in
   181     AxClass.overload_conv thy
   182     #> trans_conv_rule (Simplifier.rewrite post)
   183   end;
   184 
   185 fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
   186 
   187 fun print_codeproc thy =
   188   let
   189     val ctxt = Proof_Context.init_global thy;
   190     val pre = (#pre o the_thmproc) thy;
   191     val post = (#post o the_thmproc) thy;
   192     val functrans = (map fst o #functrans o the_thmproc) thy;
   193   in
   194     (Pretty.writeln o Pretty.chunks) [
   195       Pretty.block [
   196         Pretty.str "preprocessing simpset:",
   197         Pretty.fbrk,
   198         Simplifier.pretty_ss ctxt pre
   199       ],
   200       Pretty.block [
   201         Pretty.str "postprocessing simpset:",
   202         Pretty.fbrk,
   203         Simplifier.pretty_ss ctxt post
   204       ],
   205       Pretty.block (
   206         Pretty.str "function transformers:"
   207         :: Pretty.fbrk
   208         :: (Pretty.fbreaks o map Pretty.str) functrans
   209       )
   210     ]
   211   end;
   212 
   213 fun simple_functrans f thy eqns = case f thy (map fst eqns)
   214  of SOME thms' => SOME (map (rpair (forall snd eqns)) thms')
   215   | NONE => NONE;
   216 
   217 
   218 (** sort algebra and code equation graph types **)
   219 
   220 type code_algebra = (sort -> sort) * Sorts.algebra;
   221 type code_graph = ((string * sort) list * Code.cert) Graph.T;
   222 
   223 fun get_node eqngr const = Graph.get_node eqngr const
   224   handle Graph.UNDEF _ => error ("No such constant in code equation graph: " ^ quote const);
   225 
   226 fun cert eqngr = snd o get_node eqngr;
   227 fun sortargs eqngr = map snd o fst o get_node eqngr;
   228 fun all eqngr = Graph.keys eqngr;
   229 
   230 fun pretty thy eqngr =
   231   AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
   232   |> (map o apfst) (Code.string_of_const thy)
   233   |> sort (string_ord o pairself fst)
   234   |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
   235   |> Pretty.chunks;
   236 
   237 
   238 (** the Waisenhaus algorithm **)
   239 
   240 (* auxiliary *)
   241 
   242 fun is_proper_class thy = can (AxClass.get_info thy);
   243 
   244 fun complete_proper_sort thy =
   245   Sign.complete_sort thy #> filter (is_proper_class thy);
   246 
   247 fun inst_params thy tyco =
   248   map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
   249     o maps (#params o AxClass.get_info thy);
   250 
   251 
   252 (* data structures *)
   253 
   254 datatype const = Fun of string | Inst of class * string;
   255 
   256 fun const_ord (Fun c1, Fun c2) = fast_string_ord (c1, c2)
   257   | const_ord (Inst class_tyco1, Inst class_tyco2) =
   258       prod_ord fast_string_ord fast_string_ord (class_tyco1, class_tyco2)
   259   | const_ord (Fun _, Inst _) = LESS
   260   | const_ord (Inst _, Fun _) = GREATER;
   261 
   262 type var = const * int;
   263 
   264 structure Vargraph =
   265   Graph(type key = var val ord = prod_ord const_ord int_ord);
   266 
   267 datatype styp = Tyco of string * styp list | Var of var | Free;
   268 
   269 fun styp_of c_lhs (Type (tyco, tys)) = Tyco (tyco, map (styp_of c_lhs) tys)
   270   | styp_of c_lhs (TFree (v, _)) = case c_lhs
   271      of SOME (c, lhs) => Var (Fun c, find_index (fn (v', _) => v = v') lhs)
   272       | NONE => Free;
   273 
   274 type vardeps_data = ((string * styp list) list * class list) Vargraph.T
   275   * (((string * sort) list * Code.cert) Symtab.table
   276     * (class * string) list);
   277 
   278 val empty_vardeps_data : vardeps_data =
   279   (Vargraph.empty, (Symtab.empty, []));
   280 
   281 
   282 (* retrieving equations and instances from the background context *)
   283 
   284 fun obtain_eqns thy eqngr c =
   285   case try (Graph.get_node eqngr) c
   286    of SOME (lhs, cert) => ((lhs, []), cert)
   287     | NONE => let
   288         val cert = Code.get_cert thy (preprocess thy) c;
   289         val (lhs, rhss) = Code.typargs_deps_of_cert thy cert;
   290       in ((lhs, rhss), cert) end;
   291 
   292 fun obtain_instance thy arities (inst as (class, tyco)) =
   293   case AList.lookup (op =) arities inst
   294    of SOME classess => (classess, ([], []))
   295     | NONE => let
   296         val all_classes = complete_proper_sort thy [class];
   297         val super_classes = remove (op =) class all_classes;
   298         val classess = map (complete_proper_sort thy)
   299           (Sign.arity_sorts thy tyco [class]);
   300         val inst_params = inst_params thy tyco all_classes;
   301       in (classess, (super_classes, inst_params)) end;
   302 
   303 
   304 (* computing instantiations *)
   305 
   306 fun add_classes thy arities eqngr c_k new_classes vardeps_data =
   307   let
   308     val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
   309     val diff_classes = new_classes |> subtract (op =) old_classes;
   310   in if null diff_classes then vardeps_data
   311   else let
   312     val c_ks = Vargraph.immediate_succs (fst vardeps_data) c_k |> insert (op =) c_k;
   313   in
   314     vardeps_data
   315     |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
   316     |> fold (fn styp => fold (ensure_typmatch_inst thy arities eqngr styp) new_classes) styps
   317     |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
   318   end end
   319 and add_styp thy arities eqngr c_k new_tyco_styps vardeps_data =
   320   let
   321     val (old_tyco_stypss, classes) = Vargraph.get_node (fst vardeps_data) c_k;
   322   in if member (op =) old_tyco_stypss new_tyco_styps then vardeps_data
   323   else
   324     vardeps_data
   325     |> (apfst o Vargraph.map_node c_k o apfst) (cons new_tyco_styps)
   326     |> fold (ensure_typmatch_inst thy arities eqngr new_tyco_styps) classes
   327   end
   328 and add_dep thy arities eqngr c_k c_k' vardeps_data =
   329   let
   330     val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k;
   331   in
   332     vardeps_data
   333     |> add_classes thy arities eqngr c_k' classes
   334     |> apfst (Vargraph.add_edge (c_k, c_k'))
   335   end
   336 and ensure_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
   337   if can (Sign.arity_sorts thy tyco) [class]
   338   then vardeps_data
   339     |> ensure_inst thy arities eqngr (class, tyco)
   340     |> fold_index (fn (k, styp) =>
   341          ensure_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
   342   else vardeps_data (*permissive!*)
   343 and ensure_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
   344   if member (op =) insts inst then vardeps_data
   345   else let
   346     val (classess, (super_classes, inst_params)) =
   347       obtain_instance thy arities inst;
   348   in
   349     vardeps_data
   350     |> (apsnd o apsnd) (insert (op =) inst)
   351     |> fold_index (fn (k, _) =>
   352          apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess
   353     |> fold (fn super_class => ensure_inst thy arities eqngr (super_class, tyco)) super_classes
   354     |> fold (ensure_fun thy arities eqngr) inst_params
   355     |> fold_index (fn (k, classes) =>
   356          add_classes thy arities eqngr (Inst (class, tyco), k) classes
   357          #> fold (fn super_class =>
   358              add_dep thy arities eqngr (Inst (super_class, tyco), k)
   359              (Inst (class, tyco), k)) super_classes
   360          #> fold (fn inst_param =>
   361              add_dep thy arities eqngr (Fun inst_param, k)
   362              (Inst (class, tyco), k)
   363              ) inst_params
   364          ) classess
   365   end
   366 and ensure_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
   367       vardeps_data
   368       |> add_styp thy arities eqngr c_k tyco_styps
   369   | ensure_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
   370       vardeps_data
   371       |> add_dep thy arities eqngr c_k c_k'
   372   | ensure_typmatch thy arities eqngr Free c_k vardeps_data =
   373       vardeps_data
   374 and ensure_rhs thy arities eqngr (c', styps) vardeps_data =
   375   vardeps_data
   376   |> ensure_fun thy arities eqngr c'
   377   |> fold_index (fn (k, styp) =>
   378        ensure_typmatch thy arities eqngr styp (Fun c', k)) styps
   379 and ensure_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) =
   380   if Symtab.defined eqntab c then vardeps_data
   381   else let
   382     val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
   383     val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
   384   in
   385     vardeps_data
   386     |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
   387     |> fold_index (fn (k, _) =>
   388          apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs
   389     |> fold_index (fn (k, (_, sort)) =>
   390          add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
   391     |> fold (ensure_rhs thy arities eqngr) rhss'
   392   end;
   393 
   394 
   395 (* applying instantiations *)
   396 
   397 fun dicts_of thy (proj_sort, algebra) (T, sort) =
   398   let
   399     fun class_relation (x, _) _ = x;
   400     fun type_constructor (tyco, _) xs class =
   401       inst_params thy tyco (Sorts.complete_sort algebra [class])
   402         @ (maps o maps) fst xs;
   403     fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
   404   in
   405     flat (Sorts.of_sort_derivation algebra
   406       { class_relation = K class_relation, type_constructor = type_constructor,
   407         type_variable = type_variable } (T, proj_sort sort)
   408        handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
   409   end;
   410 
   411 fun add_arity thy vardeps (class, tyco) =
   412   AList.default (op =) ((class, tyco),
   413     map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
   414       (Sign.arity_number thy tyco));
   415 
   416 fun add_cert thy vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) =
   417   if can (Graph.get_node eqngr) c then (rhss, eqngr)
   418   else let
   419     val lhs = map_index (fn (k, (v, _)) =>
   420       (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
   421     val cert = Code.constrain_cert thy (map (Sign.minimize_sort thy o snd) lhs) proto_cert;
   422     val (vs, rhss') = Code.typargs_deps_of_cert thy cert;
   423     val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
   424   in (map (pair c) rhss' @ rhss, eqngr') end;
   425 
   426 fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
   427   let
   428     val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
   429       insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
   430     val (vardeps, (eqntab, insts)) = empty_vardeps_data
   431       |> fold (ensure_fun thy arities eqngr) cs
   432       |> fold (ensure_rhs thy arities eqngr) cs_rhss;
   433     val arities' = fold (add_arity thy vardeps) insts arities;
   434     val algebra = Sorts.subalgebra (Syntax.init_pretty_global thy) (is_proper_class thy)
   435       (AList.lookup (op =) arities') (Sign.classes_of thy);
   436     val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
   437     fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
   438       (rhs ~~ sortargs eqngr' c);
   439     val eqngr'' = fold (fn (c, rhs) => fold
   440       (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
   441   in (algebra, (arities', eqngr'')) end;
   442 
   443 
   444 (** store for preprocessed arities and code equations **)
   445 
   446 structure Wellsorted = Code_Data
   447 (
   448   type T = ((string * class) * sort list) list * code_graph;
   449   val empty = ([], Graph.empty);
   450 );
   451 
   452 
   453 (** retrieval and evaluation interfaces **)
   454 
   455 fun obtain ignore_cache thy consts ts = apsnd snd
   456   (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy) (extend_arities_eqngr thy consts ts));
   457 
   458 fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
   459 
   460 fun dynamic_conv thy conv = no_variables_conv (fn ct =>
   461   let
   462     val thm1 = preprocess_conv thy ct;
   463     val ct' = Thm.rhs_of thm1;
   464     val (vs', t') = dest_cterm ct';
   465     val consts = fold_aterms
   466       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
   467     val (algebra', eqngr') = obtain false thy consts [t'];
   468     val thm2 = conv algebra' eqngr' vs' t' ct';
   469     val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
   470   in
   471     Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
   472       error ("could not construct evaluation proof:\n"
   473       ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
   474   end);
   475 
   476 fun dynamic_value thy postproc evaluator t =
   477   let
   478     val (resubst, t') = preprocess_term thy t;
   479     val vs' = Term.add_tfrees t' [];
   480     val consts = fold_aterms
   481       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
   482     val (algebra', eqngr') = obtain false thy consts [t'];
   483   in
   484     t'
   485     |> evaluator algebra' eqngr' vs'
   486     |> postproc (postprocess_term thy o resubst)
   487   end;
   488 
   489 fun static_conv thy consts conv =
   490   let
   491     val (algebra, eqngr) = obtain true thy consts [];
   492     val conv' = conv algebra eqngr;
   493   in
   494     no_variables_conv ((preprocess_conv thy)
   495       then_conv (fn ct => uncurry conv' (dest_cterm ct) ct)
   496       then_conv (postprocess_conv thy))
   497   end;
   498 
   499 fun static_value thy postproc consts evaluator =
   500   let
   501     val (algebra, eqngr) = obtain true thy consts [];
   502     val evaluator' = evaluator algebra eqngr;
   503   in 
   504     preprocess_term thy
   505     #-> (fn resubst => fn t => t
   506       |> evaluator' (Term.add_tfrees t [])
   507       |> postproc (postprocess_term thy o resubst))
   508   end;
   509 
   510 
   511 (** setup **)
   512 
   513 val setup = 
   514   let
   515     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   516     fun add_del_attribute_parser add del =
   517       Attrib.add_del (mk_attribute add) (mk_attribute del);
   518   in
   519     Attrib.setup @{binding code_unfold} (add_del_attribute_parser add_unfold del_unfold)
   520         "preprocessing equations for code generator"
   521     #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
   522         "postprocessing equations for code generator"
   523     #> Attrib.setup @{binding code_abbrev} (Scan.succeed (mk_attribute add_code_abbrev))
   524         "post- and preprocessing equations for code generator"
   525   end;
   526 
   527 val _ =
   528   Outer_Syntax.improper_command "print_codeproc" "print code preprocessor setup"
   529   Keyword.diag (Scan.succeed
   530       (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
   531         (print_codeproc o Toplevel.theory_of)));
   532 
   533 end; (*struct*)