--- 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 *)