canonical argument order for attribute application;
authorwenzelm
Sat Mar 03 21:43:59 2012 +0100 (2012-03-03)
changeset 467756287653e63ec
parent 46774 38f113b052b1
child 46776 8575cc482dfb
canonical argument order for attribute application;
src/HOL/Tools/choice_specification.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof_context.ML
src/Pure/global_theory.ML
src/Pure/more_thm.ML
     1.1 --- a/src/HOL/Tools/choice_specification.ML	Sat Mar 03 18:18:39 2012 +0100
     1.2 +++ b/src/HOL/Tools/choice_specification.ML	Sat Mar 03 21:43:59 2012 +0100
     1.3 @@ -185,20 +185,21 @@
     1.4                          fun undo_imps thm =
     1.5                              Thm.equal_elim (Thm.symmetric rew_imp) thm
     1.6  
     1.7 -                        fun add_final (arg as (thy, thm)) =
     1.8 +                        fun add_final (thm, thy) =
     1.9                              if name = ""
    1.10 -                            then arg |> Library.swap
    1.11 +                            then (thm, thy)
    1.12                              else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
    1.13                                    Global_Theory.store_thm (Binding.name name, thm) thy)
    1.14                      in
    1.15 -                        args |> apsnd (remove_alls frees)
    1.16 -                             |> apsnd undo_imps
    1.17 -                             |> apsnd Drule.export_without_context
    1.18 -                             |> Thm.theory_attributes
    1.19 +                        swap args
    1.20 +                             |> apfst (remove_alls frees)
    1.21 +                             |> apfst undo_imps
    1.22 +                             |> apfst Drule.export_without_context
    1.23 +                             |-> Thm.theory_attributes
    1.24                                  (map (Attrib.attribute thy)
    1.25                                    (@{attributes [nitpick_choice_spec]} @ atts))
    1.26                               |> add_final
    1.27 -                             |> Library.swap
    1.28 +                             |> swap
    1.29                      end
    1.30  
    1.31                  fun process_all [proc_arg] args =
     2.1 --- a/src/Pure/Isar/attrib.ML	Sat Mar 03 18:18:39 2012 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Sat Mar 03 21:43:59 2012 +0100
     2.3 @@ -191,8 +191,7 @@
     2.4      Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
     2.5        let
     2.6          val atts = map (attribute_i thy) srcs;
     2.7 -        val (context', th') =
     2.8 -          Library.apply (map Thm.apply_attribute atts) (context, Drule.dummy_thm);
     2.9 +        val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
    2.10        in (context', pick "" [th']) end)
    2.11      ||
    2.12      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    2.13 @@ -204,8 +203,8 @@
    2.14        let
    2.15          val ths = Facts.select thmref fact;
    2.16          val atts = map (attribute_i thy) srcs;
    2.17 -        val (context', ths') =
    2.18 -          Library.foldl_map (Library.apply (map Thm.apply_attribute atts)) (context, ths);
    2.19 +        val (ths', context') =
    2.20 +          fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
    2.21        in (context', pick name ths') end)
    2.22    end);
    2.23  
     3.1 --- a/src/Pure/Isar/method.ML	Sat Mar 03 18:18:39 2012 +0100
     3.2 +++ b/src/Pure/Isar/method.ML	Sat Mar 03 21:43:59 2012 +0100
     3.3 @@ -377,13 +377,12 @@
     3.4  local
     3.5  
     3.6  fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
     3.7 -fun app (f, att) (context, ths) =
     3.8 -  Library.foldl_map (Thm.apply_attribute att) (Context.map_proof f context, ths);
     3.9 +fun app (f, att) ths context = fold_map (Thm.apply_attribute att) ths (Context.map_proof f context);
    3.10  
    3.11  in
    3.12  
    3.13  fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|--
    3.14 -  (fn (m, ths) => Scan.succeed (app m (context, ths))));
    3.15 +  (fn (m, ths) => Scan.succeed (swap (app m ths context))));
    3.16  
    3.17  fun sections ss = Scan.repeat (section ss);
    3.18  
     4.1 --- a/src/Pure/Isar/proof_context.ML	Sat Mar 03 18:18:39 2012 +0100
     4.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Mar 03 21:43:59 2012 +0100
     4.3 @@ -894,13 +894,12 @@
     4.4  
     4.5  in
     4.6  
     4.7 -fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
     4.8 +fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt =>
     4.9    let
    4.10      val name = full_name ctxt b;
    4.11      val facts = Global_Theory.name_thmss false name raw_facts;
    4.12 -    fun app (th, attrs) x =
    4.13 -      swap (Library.foldl_map
    4.14 -        (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
    4.15 +    fun app (ths, atts) =
    4.16 +      fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
    4.17      val (res, ctxt') = fold_map app facts ctxt;
    4.18      val thms = Global_Theory.name_thms false false name (flat res);
    4.19      val Mode {stmt, ...} = get_mode ctxt;
     5.1 --- a/src/Pure/global_theory.ML	Sat Mar 03 18:18:39 2012 +0100
     5.2 +++ b/src/Pure/global_theory.ML	Sat Mar 03 21:43:59 2012 +0100
     5.3 @@ -80,7 +80,7 @@
     5.4  
     5.5  (* forked proofs *)
     5.6  
     5.7 -fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (add_proofs thms))) thy, thms);
     5.8 +fun register_proofs thms thy = (thms, Data.map (apsnd (pairself (add_proofs thms))) thy);
     5.9  
    5.10  val begin_recent_proofs = Data.map (apsnd (apfst (K empty_proofs)));
    5.11  val join_recent_proofs = force_proofs o #1 o #2 o Data.get;
    5.12 @@ -153,13 +153,12 @@
    5.13  
    5.14  fun enter_thms pre_name post_name app_att (b, thms) thy =
    5.15    if Binding.is_empty b
    5.16 -  then swap (register_proofs (app_att (thy, thms)))
    5.17 +  then app_att thms thy |-> register_proofs
    5.18    else
    5.19      let
    5.20        val naming = Sign.naming_of thy;
    5.21        val name = Name_Space.full_name naming b;
    5.22 -      val (thy', thms') =
    5.23 -        register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
    5.24 +      val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
    5.25        val thms'' = map (Thm.transfer thy') thms';
    5.26        val thy'' = thy'
    5.27          |> (Data.map o apfst)
    5.28 @@ -170,19 +169,18 @@
    5.29  (* store_thm(s) *)
    5.30  
    5.31  fun store_thms (b, thms) =
    5.32 -  enter_thms (name_thms true true) (name_thms false true) I (b, thms);
    5.33 +  enter_thms (name_thms true true) (name_thms false true) pair (b, thms);
    5.34  
    5.35  fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
    5.36  
    5.37  fun store_thm_open (b, th) =
    5.38 -  enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single;
    5.39 +  enter_thms (name_thms true false) (name_thms false false) pair (b, [th]) #>> the_single;
    5.40  
    5.41  
    5.42  (* add_thms(s) *)
    5.43  
    5.44  fun add_thms_atts pre_name ((b, thms), atts) =
    5.45 -  enter_thms pre_name (name_thms false true)
    5.46 -    (Library.foldl_map (Thm.theory_attributes atts)) (b, thms);
    5.47 +  enter_thms pre_name (name_thms false true) (fold_map (Thm.theory_attributes atts)) (b, thms);
    5.48  
    5.49  fun gen_add_thmss pre_name =
    5.50    fold_map (add_thms_atts pre_name);
    5.51 @@ -204,13 +202,14 @@
    5.52  
    5.53  (* note_thmss *)
    5.54  
    5.55 -fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
    5.56 +fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn thy =>
    5.57    let
    5.58      val name = Sign.full_name thy b;
    5.59 -    fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
    5.60 -    val (thms, thy') = thy |> enter_thms
    5.61 -      (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app)
    5.62 -      (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
    5.63 +    fun app (ths, atts) =
    5.64 +      fold_map (Thm.theory_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
    5.65 +    val (thms, thy') =
    5.66 +      enter_thms (name_thmss true) (name_thms false true) (apfst flat oo fold_map app)
    5.67 +        (b, facts) thy;
    5.68    in ((name, thms), thy') end);
    5.69  
    5.70  
     6.1 --- a/src/Pure/more_thm.ML	Sat Mar 03 18:18:39 2012 +0100
     6.2 +++ b/src/Pure/more_thm.ML	Sat Mar 03 21:43:59 2012 +0100
     6.3 @@ -73,10 +73,10 @@
     6.4    val rule_attribute: (Context.generic -> thm -> thm) -> attribute
     6.5    val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
     6.6    val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
     6.7 -  val apply_attribute: attribute -> Context.generic * thm -> Context.generic * thm
     6.8 +  val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic
     6.9    val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
    6.10 -  val theory_attributes: attribute list -> theory * thm -> theory * thm
    6.11 -  val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
    6.12 +  val theory_attributes: attribute list -> thm -> theory -> thm * theory
    6.13 +  val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
    6.14    val no_attributes: 'a -> 'a * 'b list
    6.15    val simple_fact: 'a -> ('a * 'b list) list
    6.16    val tag_rule: Properties.entry -> thm -> thm
    6.17 @@ -403,16 +403,16 @@
    6.18  fun declaration_attribute f (x, th) = (SOME (f th x), NONE);
    6.19  fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
    6.20  
    6.21 -fun apply_attribute (att: attribute) (x, th) =
    6.22 +fun apply_attribute (att: attribute) th x =
    6.23    let val (x', th') = att (x, th)
    6.24 -  in (the_default x x', the_default th th') end;
    6.25 +  in (the_default th th', the_default x x') end;
    6.26  
    6.27 -fun attribute_declaration att th x = #1 (apply_attribute att (x, th));
    6.28 +fun attribute_declaration att th x = #2 (apply_attribute att th x);
    6.29  
    6.30  fun apply_attributes mk dest =
    6.31    let
    6.32 -    fun app [] = I
    6.33 -      | app (att :: atts) = fn (x, th) => apply_attribute att (mk x, th) |>> dest |> app atts;
    6.34 +    fun app [] th x = (th, x)
    6.35 +      | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts;
    6.36    in app end;
    6.37  
    6.38  val theory_attributes = apply_attributes Context.Theory Context.the_theory;