# HG changeset patch # User wenzelm # Date 1330807439 -3600 # Node ID 6287653e63ece84221ccd4f64e9fad7283fb771b # Parent 38f113b052b1c91473d22c7e2a5af958a91c1f14 canonical argument order for attribute application; diff -r 38f113b052b1 -r 6287653e63ec src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Sat Mar 03 18:18:39 2012 +0100 +++ b/src/HOL/Tools/choice_specification.ML Sat Mar 03 21:43:59 2012 +0100 @@ -185,20 +185,21 @@ fun undo_imps thm = Thm.equal_elim (Thm.symmetric rew_imp) thm - fun add_final (arg as (thy, thm)) = + fun add_final (thm, thy) = if name = "" - then arg |> Library.swap + then (thm, thy) else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm); Global_Theory.store_thm (Binding.name name, thm) thy) in - args |> apsnd (remove_alls frees) - |> apsnd undo_imps - |> apsnd Drule.export_without_context - |> Thm.theory_attributes + swap args + |> apfst (remove_alls frees) + |> apfst undo_imps + |> apfst Drule.export_without_context + |-> Thm.theory_attributes (map (Attrib.attribute thy) (@{attributes [nitpick_choice_spec]} @ atts)) |> add_final - |> Library.swap + |> swap end fun process_all [proc_arg] args = diff -r 38f113b052b1 -r 6287653e63ec src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sat Mar 03 18:18:39 2012 +0100 +++ b/src/Pure/Isar/attrib.ML Sat Mar 03 21:43:59 2012 +0100 @@ -191,8 +191,7 @@ Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs => let val atts = map (attribute_i thy) srcs; - val (context', th') = - Library.apply (map Thm.apply_attribute atts) (context, Drule.dummy_thm); + val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context); in (context', pick "" [th']) end) || (Scan.ahead Args.alt_name -- Args.named_fact get_fact @@ -204,8 +203,8 @@ let val ths = Facts.select thmref fact; val atts = map (attribute_i thy) srcs; - val (context', ths') = - Library.foldl_map (Library.apply (map Thm.apply_attribute atts)) (context, ths); + val (ths', context') = + fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context; in (context', pick name ths') end) end); diff -r 38f113b052b1 -r 6287653e63ec src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sat Mar 03 18:18:39 2012 +0100 +++ b/src/Pure/Isar/method.ML Sat Mar 03 21:43:59 2012 +0100 @@ -377,13 +377,12 @@ local fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat; -fun app (f, att) (context, ths) = - Library.foldl_map (Thm.apply_attribute att) (Context.map_proof f context, ths); +fun app (f, att) ths context = fold_map (Thm.apply_attribute att) ths (Context.map_proof f context); in fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|-- - (fn (m, ths) => Scan.succeed (app m (context, ths)))); + (fn (m, ths) => Scan.succeed (swap (app m ths context)))); fun sections ss = Scan.repeat (section ss); diff -r 38f113b052b1 -r 6287653e63ec src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Mar 03 18:18:39 2012 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Mar 03 21:43:59 2012 +0100 @@ -894,13 +894,12 @@ in -fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt => +fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt => let val name = full_name ctxt b; val facts = Global_Theory.name_thmss false name raw_facts; - fun app (th, attrs) x = - swap (Library.foldl_map - (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th)); + fun app (ths, atts) = + fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; val (res, ctxt') = fold_map app facts ctxt; val thms = Global_Theory.name_thms false false name (flat res); val Mode {stmt, ...} = get_mode ctxt; diff -r 38f113b052b1 -r 6287653e63ec src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Sat Mar 03 18:18:39 2012 +0100 +++ b/src/Pure/global_theory.ML Sat Mar 03 21:43:59 2012 +0100 @@ -80,7 +80,7 @@ (* forked proofs *) -fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (add_proofs thms))) thy, thms); +fun register_proofs thms thy = (thms, Data.map (apsnd (pairself (add_proofs thms))) thy); val begin_recent_proofs = Data.map (apsnd (apfst (K empty_proofs))); val join_recent_proofs = force_proofs o #1 o #2 o Data.get; @@ -153,13 +153,12 @@ fun enter_thms pre_name post_name app_att (b, thms) thy = if Binding.is_empty b - then swap (register_proofs (app_att (thy, thms))) + then app_att thms thy |-> register_proofs else let val naming = Sign.naming_of thy; val name = Name_Space.full_name naming b; - val (thy', thms') = - register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms))); + val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs; val thms'' = map (Thm.transfer thy') thms'; val thy'' = thy' |> (Data.map o apfst) @@ -170,19 +169,18 @@ (* store_thm(s) *) fun store_thms (b, thms) = - enter_thms (name_thms true true) (name_thms false true) I (b, thms); + enter_thms (name_thms true true) (name_thms false true) pair (b, thms); fun store_thm (b, th) = store_thms (b, [th]) #>> the_single; fun store_thm_open (b, th) = - enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single; + enter_thms (name_thms true false) (name_thms false false) pair (b, [th]) #>> the_single; (* add_thms(s) *) fun add_thms_atts pre_name ((b, thms), atts) = - enter_thms pre_name (name_thms false true) - (Library.foldl_map (Thm.theory_attributes atts)) (b, thms); + enter_thms pre_name (name_thms false true) (fold_map (Thm.theory_attributes atts)) (b, thms); fun gen_add_thmss pre_name = fold_map (add_thms_atts pre_name); @@ -204,13 +202,14 @@ (* note_thmss *) -fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy => +fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn thy => let val name = Sign.full_name thy b; - fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths); - val (thms, thy') = thy |> enter_thms - (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app) - (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts); + fun app (ths, atts) = + fold_map (Thm.theory_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; + val (thms, thy') = + enter_thms (name_thmss true) (name_thms false true) (apfst flat oo fold_map app) + (b, facts) thy; in ((name, thms), thy') end); diff -r 38f113b052b1 -r 6287653e63ec src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sat Mar 03 18:18:39 2012 +0100 +++ b/src/Pure/more_thm.ML Sat Mar 03 21:43:59 2012 +0100 @@ -73,10 +73,10 @@ val rule_attribute: (Context.generic -> thm -> thm) -> attribute val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute - val apply_attribute: attribute -> Context.generic * thm -> Context.generic * thm + val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic - val theory_attributes: attribute list -> theory * thm -> theory * thm - val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm + val theory_attributes: attribute list -> thm -> theory -> thm * theory + val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context val no_attributes: 'a -> 'a * 'b list val simple_fact: 'a -> ('a * 'b list) list val tag_rule: Properties.entry -> thm -> thm @@ -403,16 +403,16 @@ fun declaration_attribute f (x, th) = (SOME (f th x), NONE); fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end; -fun apply_attribute (att: attribute) (x, th) = +fun apply_attribute (att: attribute) th x = let val (x', th') = att (x, th) - in (the_default x x', the_default th th') end; + in (the_default th th', the_default x x') end; -fun attribute_declaration att th x = #1 (apply_attribute att (x, th)); +fun attribute_declaration att th x = #2 (apply_attribute att th x); fun apply_attributes mk dest = let - fun app [] = I - | app (att :: atts) = fn (x, th) => apply_attribute att (mk x, th) |>> dest |> app atts; + fun app [] th x = (th, x) + | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts; in app end; val theory_attributes = apply_attributes Context.Theory Context.the_theory;