# HG changeset patch
# User wenzelm
# Date 1321308056 -3600
# Node ID 12453fd8dcffc24fb98c2d5cc88ef184d30f82c5
# Parent  8b442f94d5d372a8bacfd8bc2299ebde582744d5
some support for partial evaluation of attributed facts;

diff -r 8b442f94d5d3 -r 12453fd8dcff src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Nov 14 20:25:22 2011 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Nov 14 23:00:56 2011 +0100
@@ -33,8 +33,11 @@
   val thm: thm context_parser
   val thms: thm list context_parser
   val multi_thm: thm list context_parser
+  val partial_evaluation: Proof.context ->
+    (binding * (thm list * Args.src list) list) list ->
+    (binding * (thm list * Args.src list) list) list
+  val internal: (morphism -> attribute) -> src
   val print_configs: Proof.context -> unit
-  val internal: (morphism -> attribute) -> src
   val config_bool: Binding.binding ->
     (Context.generic -> bool) -> bool Config.T * (theory -> theory)
   val config_int: Binding.binding ->
@@ -213,6 +216,48 @@
 
 
 
+(** partial evaluation **)
+
+local
+(* FIXME assignable, closure (!?) *)
+
+fun apply_att src (context, th) =
+  attribute_i (Context.theory_of context) src (context, th);
+
+fun eval src (th, (decls, context)) =
+  (case apply_att src (context, th) of
+    (NONE, SOME th') => (th', (decls, context))
+  | (opt_context', opt_th') =>
+      let
+        val context' = the_default context opt_context';
+        val th' = the_default th opt_th';
+        val decls' =
+          (case decls of
+            [] => [(th, [src])]
+          | (th2, srcs2) :: rest =>
+              if op = (pairself Thm.rep_thm (th, th2))  (* FIXME derivation!? *)
+              then ((th2, src :: srcs2) :: rest)
+              else (th, [src]) :: (th2, srcs2) :: rest);
+      in (th', (decls', context')) end);
+
+in
+
+fun partial_evaluation ctxt facts =
+  let
+    val (facts', (decls, _)) =
+      (facts, ([], Context.Proof ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn res =>
+        let
+          val (thss', res') =
+            (fact, res) |-> fold_map (fn (ths, atts) =>
+              fold_map (curry (fold eval (atts @ more_atts))) ths);
+        in (((b, []), [(flat thss', [])]), res') end);
+    val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
+  in decl_fact :: facts' end;
+
+end;
+
+
+
 (** basic attributes **)
 
 (* internal *)