# HG changeset patch
# User haftmann
# Date 1177060912 -7200
# Node ID 189efc4a9f541f4048b209edad0b3bc1a7efc9de
# Parent  474f92c32348eaa76451c1e7630890516e87833f
unfold attribute now also accepts HOL equations

diff -r 474f92c32348 -r 189efc4a9f54 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Apr 20 11:21:50 2007 +0200
+++ b/src/Pure/codegen.ML	Fri Apr 20 11:21:52 2007 +0200
@@ -201,6 +201,8 @@
 
 (* data kind 'Pure/codegen' *)
 
+structure CodeData = CodegenData;
+
 structure CodegenData = TheoryDataFun
 (struct
   val name = "Pure/codegen";
@@ -297,30 +299,6 @@
   end;
 
 
-(**** code attribute ****)
-
-fun add_attribute name att thy =
-  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
-    CodegenData.get thy
-  in (case AList.lookup (op =) attrs name of
-      NONE => CodegenData.put {tycodegens = tycodegens,
-        codegens = codegens, consts = consts, types = types,
-        attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs,
-        preprocs = preprocs, modules = modules,
-        test_params = test_params} thy
-    | SOME _ => error ("Code attribute " ^ name ^ " already declared"))
-  end;
-
-fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
-
-val code_attr =
-  Attrib.syntax (Scan.peek (fn context => foldr op || Scan.fail (map mk_parser
-    (#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 =
@@ -350,17 +328,57 @@
 
 fun add_unfold eqn =
   let
-    val names = term_consts (fst (Logic.dest_equals (prop_of eqn)));
+    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)
+        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
+  in (case AList.lookup (op =) attrs name of
+      NONE => CodegenData.put {tycodegens = tycodegens,
+        codegens = codegens, consts = consts, types = types,
+        attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs,
+        preprocs = preprocs, modules = modules,
+        test_params = test_params} thy
+    | SOME _ => error ("Code attribute " ^ name ^ " already declared"))
+  end;
+
+fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
+
+val code_attr =
+  Attrib.syntax (Scan.peek (fn context => foldr op || Scan.fail (map mk_parser
+    (#attrs (CodegenData.get (Context.theory_of context))))));
+
+val _ = Context.add_setup
+  (Attrib.add_attributes [("code", code_attr, "declare theorems for code generation")]);
+
+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 ****)