src/Pure/Isar/attrib.ML
changeset 45493 12453fd8dcff
parent 45491 3c9aff74fb58
child 45526 20a82863d5ef
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Nov 14 20:25:22 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Nov 14 23:00:56 2011 +0100
     1.3 @@ -33,8 +33,11 @@
     1.4    val thm: thm context_parser
     1.5    val thms: thm list context_parser
     1.6    val multi_thm: thm list context_parser
     1.7 +  val partial_evaluation: Proof.context ->
     1.8 +    (binding * (thm list * Args.src list) list) list ->
     1.9 +    (binding * (thm list * Args.src list) list) list
    1.10 +  val internal: (morphism -> attribute) -> src
    1.11    val print_configs: Proof.context -> unit
    1.12 -  val internal: (morphism -> attribute) -> src
    1.13    val config_bool: Binding.binding ->
    1.14      (Context.generic -> bool) -> bool Config.T * (theory -> theory)
    1.15    val config_int: Binding.binding ->
    1.16 @@ -213,6 +216,48 @@
    1.17  
    1.18  
    1.19  
    1.20 +(** partial evaluation **)
    1.21 +
    1.22 +local
    1.23 +(* FIXME assignable, closure (!?) *)
    1.24 +
    1.25 +fun apply_att src (context, th) =
    1.26 +  attribute_i (Context.theory_of context) src (context, th);
    1.27 +
    1.28 +fun eval src (th, (decls, context)) =
    1.29 +  (case apply_att src (context, th) of
    1.30 +    (NONE, SOME th') => (th', (decls, context))
    1.31 +  | (opt_context', opt_th') =>
    1.32 +      let
    1.33 +        val context' = the_default context opt_context';
    1.34 +        val th' = the_default th opt_th';
    1.35 +        val decls' =
    1.36 +          (case decls of
    1.37 +            [] => [(th, [src])]
    1.38 +          | (th2, srcs2) :: rest =>
    1.39 +              if op = (pairself Thm.rep_thm (th, th2))  (* FIXME derivation!? *)
    1.40 +              then ((th2, src :: srcs2) :: rest)
    1.41 +              else (th, [src]) :: (th2, srcs2) :: rest);
    1.42 +      in (th', (decls', context')) end);
    1.43 +
    1.44 +in
    1.45 +
    1.46 +fun partial_evaluation ctxt facts =
    1.47 +  let
    1.48 +    val (facts', (decls, _)) =
    1.49 +      (facts, ([], Context.Proof ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn res =>
    1.50 +        let
    1.51 +          val (thss', res') =
    1.52 +            (fact, res) |-> fold_map (fn (ths, atts) =>
    1.53 +              fold_map (curry (fold eval (atts @ more_atts))) ths);
    1.54 +        in (((b, []), [(flat thss', [])]), res') end);
    1.55 +    val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
    1.56 +  in decl_fact :: facts' end;
    1.57 +
    1.58 +end;
    1.59 +
    1.60 +
    1.61 +
    1.62  (** basic attributes **)
    1.63  
    1.64  (* internal *)