src/Pure/codegen.ML

   {size = size, iterations = iterations,
    default_type = SOME (Sign.read_typ thy s)};
 
 (* data kind 'Pure/codegen' *)
 
+structure CodeData = CodegenData;
+
 structure CodegenData = TheoryDataFun
 (struct
   val name = "Pure/codegen";
   type T =
     {codegens : (string * term codegen) list,

         test_params = test_params} thy
     | SOME _ => error ("Code generator " ^ name ^ " already declared"))
   end;
 
 
+(**** preprocessors ****)
+
+fun add_preprocessor p thy =
+  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
+    CodegenData.get thy
+  in CodegenData.put {tycodegens = tycodegens,
+    codegens = codegens, consts = consts, types = types,
+    attrs = attrs, preprocs = (stamp (), p) :: preprocs,
+    modules = modules, test_params = test_params} thy
+  end;
+
+fun preprocess thy =
+  let val {preprocs, ...} = CodegenData.get thy
+  in fold (fn (_, f) => f thy) preprocs end;
+
+fun preprocess_term thy t =
+  let
+    val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
+    (* fake definition *)
+    val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
+      (Logic.mk_equals (x, t));
+    fun err () = error "preprocess_term: bad preprocessor"
+  in case map prop_of (preprocess thy [eq]) of
+      [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
+    | _ => err ()
+  end;
+
+fun add_unfold eqn =
+  let
+    val thy = Thm.theory_of_thm eqn;
+    val ctxt = ProofContext.init thy;
+    val eqn' = LocalDefs.meta_rewrite_rule ctxt eqn;
+    val names = term_consts (fst (Logic.dest_equals (prop_of eqn')));
+    fun prep thy = map (fn th =>
+      let val prop = prop_of th
+      in
+        if forall (fn name => exists_Const (equal name o fst) prop) names
+        then rewrite_rule [eqn'] (Thm.transfer thy th)
+        else th
+      end)
+  in add_preprocessor prep end;
+
+
 (**** code attribute ****)
 
 fun add_attribute name att thy =
   let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
     CodegenData.get thy

     (#attrs (CodegenData.get (Context.theory_of context))))));
 
 val _ = Context.add_setup
   (Attrib.add_attributes [("code", code_attr, "declare theorems for code generation")]);
 
-
-(**** preprocessors ****)
-
-fun add_preprocessor p thy =
-  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
-    CodegenData.get thy
-  in CodegenData.put {tycodegens = tycodegens,
-    codegens = codegens, consts = consts, types = types,
-    attrs = attrs, preprocs = (stamp (), p) :: preprocs,
-    modules = modules, test_params = test_params} thy
-  end;
-
-fun preprocess thy =
-  let val {preprocs, ...} = CodegenData.get thy
-  in fold (fn (_, f) => f thy) preprocs end;
-
-fun preprocess_term thy t =
-  let
-    val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
-    (* fake definition *)
-    val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
-      (Logic.mk_equals (x, t));
-    fun err () = error "preprocess_term: bad preprocessor"
-  in case map prop_of (preprocess thy [eq]) of
-      [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
-    | _ => err ()
-  end;
-
-fun add_unfold eqn =
-  let
-    val names = term_consts (fst (Logic.dest_equals (prop_of eqn)));
-    fun prep thy = map (fn th =>
-      let val prop = prop_of th
-      in
-        if forall (fn name => exists_Const (equal name o fst) prop) names
-        then rewrite_rule [eqn] (Thm.transfer thy th)
-        else th
-      end)
-  in add_preprocessor prep end;
-
+local
+  fun add_simple_attribute (name, f) =
+    (add_attribute name o (Scan.succeed o Thm.declaration_attribute))
+      (fn th => Context.mapping (f th) I);
+in
+  val _ = map (Context.add_setup o add_simple_attribute) [
+    ("func", CodeData.add_func true),
+    ("nofunc", CodeData.del_func),
+    ("unfold", (fn thm => add_unfold thm #> CodeData.add_inline thm)),
+    ("inline", CodeData.add_inline),
+    ("noinline", CodeData.del_inline)
+  ]
+end; (*local*)
 
 
 (**** associate constants with target language code ****)
 
 fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) =>