retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
authorwenzelm
Wed Nov 16 23:09:46 2011 +0100 (2011-11-16)
changeset 45527d2b3d16b673a
parent 45526 20a82863d5ef
child 45531 528bad46f29e
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Nov 16 21:16:36 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Nov 16 23:09:46 2011 +0100
     1.3 @@ -229,13 +229,16 @@
     1.4      val src2 = Args.closure src1;
     1.5    in (src2, result) end;
     1.6  
     1.7 -fun eval src (th, (decls, context)) =
     1.8 -  (case apply_att src (context, th) of
     1.9 -    (_, (NONE, SOME th')) => (th', (decls, context))
    1.10 -  | (src', (opt_context', opt_th')) =>
    1.11 +fun err msg src =
    1.12 +  let val ((name, _), pos) = Args.dest_src src
    1.13 +  in error (msg ^ " " ^ quote name ^ Position.str_of pos) end;
    1.14 +
    1.15 +fun eval src ((th, dyn), (decls, context)) =
    1.16 +  (case (apply_att src (context, th), dyn) of
    1.17 +    ((_, (NONE, SOME th')), NONE) => ((th', NONE), (decls, context))
    1.18 +  | ((_, (NONE, SOME _)), SOME _) => err "Mixed dynamic attribute followed by static rule" src
    1.19 +  | ((src', (SOME context', NONE)), NONE) =>
    1.20        let
    1.21 -        val context' = the_default context opt_context';
    1.22 -        val th' = the_default th opt_th';
    1.23          val decls' =
    1.24            (case decls of
    1.25              [] => [(th, [src'])]
    1.26 @@ -243,7 +246,16 @@
    1.27                if strict_thm_eq (th, th2)
    1.28                then ((th2, src' :: srcs2) :: rest)
    1.29                else (th, [src']) :: (th2, srcs2) :: rest);
    1.30 -      in (th', (decls', context')) end);
    1.31 +      in ((th, NONE), (decls', context')) end
    1.32 +  | ((src', (opt_context', opt_th')), _) =>
    1.33 +      let
    1.34 +        val context' = the_default context opt_context';
    1.35 +        val th' = the_default th opt_th';
    1.36 +        val dyn' =
    1.37 +          (case dyn of
    1.38 +            NONE => SOME (th, [src'])
    1.39 +          | SOME (dyn_th, srcs) => SOME (dyn_th, src' :: srcs));
    1.40 +      in ((th', dyn'), (decls, context')) end);
    1.41  
    1.42  in
    1.43  
    1.44 @@ -252,11 +264,18 @@
    1.45      val (facts', (decls, _)) =
    1.46        (facts, ([], Context.Proof ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn res =>
    1.47          let
    1.48 -          val (ths', res') =
    1.49 -            (fact, res) |-> fold_map (fn (ths, atts) =>
    1.50 -              fold_map (curry (fold eval (atts @ more_atts))) ths)
    1.51 +          val (fact', res') =
    1.52 +            (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
    1.53 +              (ths, res1) |-> fold_map (fn th => fn res2 =>
    1.54 +                let
    1.55 +                  val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
    1.56 +                  val th_atts' =
    1.57 +                    (case dyn' of
    1.58 +                      NONE => ([th'], [])
    1.59 +                    | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
    1.60 +                in (th_atts', res3) end))
    1.61              |>> flat;
    1.62 -        in (((b, []), [(ths', [])]), res') end);
    1.63 +        in (((b, []), fact'), res') end);
    1.64      val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
    1.65    in decl_fact :: facts' end;
    1.66