clarified signature;
authorwenzelm
Fri Apr 27 22:47:30 2012 +0200 (2012-04-27 ago)
changeset 4781543f677b3ae91
parent 47814 53668571d300
child 47816 cd0dfb06b0c8
clarified signature;
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/recdef.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/element.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_thms.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/choice_specification.ML	Fri Apr 27 21:47:47 2012 +0200
     1.2 +++ b/src/HOL/Tools/choice_specification.ML	Fri Apr 27 22:47:30 2012 +0200
     1.3 @@ -202,7 +202,7 @@
     1.4                               |> apfst undo_imps
     1.5                               |> apfst Drule.export_without_context
     1.6                               |-> Thm.theory_attributes
     1.7 -                                (map (Attrib.attribute thy)
     1.8 +                                (map (Attrib.attribute_cmd_global thy)
     1.9                                    (@{attributes [nitpick_choice_spec]} @ atts))
    1.10                               |> add_final
    1.11                               |> swap
     2.1 --- a/src/HOL/Tools/recdef.ML	Fri Apr 27 21:47:47 2012 +0200
     2.2 +++ b/src/HOL/Tools/recdef.ML	Fri Apr 27 22:47:30 2012 +0200
     2.3 @@ -220,7 +220,7 @@
     2.4        |> Sign.parent_path;
     2.5    in (thy, result) end;
     2.6  
     2.7 -val add_recdef = gen_add_recdef Tfl.define Attrib.attribute prepare_hints;
     2.8 +val add_recdef = gen_add_recdef Tfl.define Attrib.attribute_cmd_global prepare_hints;
     2.9  fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
    2.10  
    2.11  
     3.1 --- a/src/Pure/Isar/attrib.ML	Fri Apr 27 21:47:47 2012 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Fri Apr 27 22:47:30 2012 +0200
     3.3 @@ -15,8 +15,10 @@
     3.4    val intern_src: theory -> src -> src
     3.5    val pretty_attribs: Proof.context -> src list -> Pretty.T list
     3.6    val defined: theory -> string -> bool
     3.7 -  val attribute: theory -> src -> attribute
     3.8 -  val attribute_i: theory -> src -> attribute
     3.9 +  val attribute: Proof.context -> src -> attribute
    3.10 +  val attribute_global: theory -> src -> attribute
    3.11 +  val attribute_cmd: Proof.context -> src -> attribute
    3.12 +  val attribute_cmd_global: theory -> src -> attribute
    3.13    val map_specs: ('a list -> 'att list) ->
    3.14      (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
    3.15    val map_facts: ('a list -> 'att list) ->
    3.16 @@ -120,7 +122,7 @@
    3.17  
    3.18  val defined = Symtab.defined o #2 o Attributes.get;
    3.19  
    3.20 -fun attribute_i thy =
    3.21 +fun attribute_global thy =
    3.22    let
    3.23      val (space, tab) = Attributes.get thy;
    3.24      fun attr src =
    3.25 @@ -131,7 +133,11 @@
    3.26        end;
    3.27    in attr end;
    3.28  
    3.29 -fun attribute thy = attribute_i thy o intern_src thy;
    3.30 +val attribute = attribute_global o Proof_Context.theory_of;
    3.31 +val attribute_generic = attribute_global o Context.theory_of;
    3.32 +
    3.33 +fun attribute_cmd_global thy = attribute_global thy o intern_src thy;
    3.34 +val attribute_cmd = attribute_cmd_global o Proof_Context.theory_of;
    3.35  
    3.36  
    3.37  (* attributed declarations *)
    3.38 @@ -145,17 +151,17 @@
    3.39  (* fact expressions *)
    3.40  
    3.41  fun global_notes kind facts thy = thy |>
    3.42 -  Global_Theory.note_thmss kind (map_facts (map (attribute_i thy)) facts);
    3.43 +  Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
    3.44  
    3.45  fun local_notes kind facts ctxt = ctxt |>
    3.46 -  Proof_Context.note_thmss kind (map_facts (map (attribute_i (Proof_Context.theory_of ctxt))) facts);
    3.47 +  Proof_Context.note_thmss kind (map_facts (map (attribute ctxt)) facts);
    3.48  
    3.49  fun generic_notes kind facts context = context |>
    3.50    Context.mapping_result (global_notes kind facts) (local_notes kind facts);
    3.51  
    3.52  fun eval_thms ctxt srcs = ctxt
    3.53    |> Proof_Context.note_thmss ""
    3.54 -    (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
    3.55 +    (map_facts_refs (map (attribute_cmd ctxt)) (Proof_Context.get_fact ctxt)
    3.56        [((Binding.empty, []), srcs)])
    3.57    |> fst |> maps snd;
    3.58  
    3.59 @@ -203,7 +209,7 @@
    3.60    in
    3.61      Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
    3.62        let
    3.63 -        val atts = map (attribute_i thy) srcs;
    3.64 +        val atts = map (attribute_generic context) srcs;
    3.65          val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
    3.66        in (context', pick "" [th']) end)
    3.67      ||
    3.68 @@ -215,7 +221,7 @@
    3.69      -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
    3.70        let
    3.71          val ths = Facts.select thmref fact;
    3.72 -        val atts = map (attribute_i thy) srcs;
    3.73 +        val atts = map (attribute_generic context) srcs;
    3.74          val (ths', context') =
    3.75            fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
    3.76        in (context', pick name ths') end)
    3.77 @@ -240,7 +246,7 @@
    3.78  fun apply_att src (context, th) =
    3.79    let
    3.80      val src1 = Args.assignable src;
    3.81 -    val result = attribute_i (Context.theory_of context) src1 (context, th);
    3.82 +    val result = attribute_generic context src1 (context, th);
    3.83      val src2 = Args.closure src1;
    3.84    in (src2, result) end;
    3.85  
     4.1 --- a/src/Pure/Isar/element.ML	Fri Apr 27 21:47:47 2012 +0200
     4.2 +++ b/src/Pure/Isar/element.ML	Fri Apr 27 22:47:30 2012 +0200
     4.3 @@ -485,16 +485,14 @@
     4.4    | init (Constrains _) = I
     4.5    | init (Assumes asms) = Context.map_proof (fn ctxt =>
     4.6        let
     4.7 -        val asms' =
     4.8 -          Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) asms;
     4.9 +        val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
    4.10          val (_, ctxt') = ctxt
    4.11            |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
    4.12            |> Proof_Context.add_assms_i Assumption.assume_export asms';
    4.13        in ctxt' end)
    4.14    | init (Defines defs) = Context.map_proof (fn ctxt =>
    4.15        let
    4.16 -        val defs' =
    4.17 -          Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) defs;
    4.18 +        val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
    4.19          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
    4.20              let val ((c, _), t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
    4.21              in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Apr 27 21:47:47 2012 +0200
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 27 22:47:30 2012 +0200
     5.3 @@ -192,7 +192,8 @@
     5.4  fun add_defs ((unchecked, overloaded), args) thy =
     5.5    thy |>
     5.6      (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
     5.7 -      overloaded (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args)
     5.8 +      overloaded
     5.9 +      (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute_cmd_global thy) srcs)) args)
    5.10    |> snd;
    5.11  
    5.12  
     6.1 --- a/src/Pure/Isar/obtain.ML	Fri Apr 27 21:47:47 2012 +0200
     6.2 +++ b/src/Pure/Isar/obtain.ML	Fri Apr 27 22:47:30 2012 +0200
     6.3 @@ -126,7 +126,7 @@
     6.4      val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
     6.5      val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt;
     6.6      val asm_props = maps (map fst) proppss;
     6.7 -    val asms = map fst (Attrib.map_specs (map (prep_att thy)) raw_asms) ~~ proppss;
     6.8 +    val asms = map fst (Attrib.map_specs (map (prep_att ctxt)) raw_asms) ~~ proppss;
     6.9  
    6.10      (*obtain parms*)
    6.11      val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
    6.12 @@ -168,7 +168,7 @@
    6.13  in
    6.14  
    6.15  val obtain = gen_obtain (K I) Proof_Context.cert_vars Proof_Context.cert_propp;
    6.16 -val obtain_cmd = gen_obtain Attrib.attribute Proof_Context.read_vars Proof_Context.read_propp;
    6.17 +val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.read_propp;
    6.18  
    6.19  end;
    6.20  
     7.1 --- a/src/Pure/Isar/proof.ML	Fri Apr 27 21:47:47 2012 +0200
     7.2 +++ b/src/Pure/Isar/proof.ML	Fri Apr 27 22:47:30 2012 +0200
     7.3 @@ -83,7 +83,7 @@
     7.4    val apply: Method.text -> state -> state Seq.seq
     7.5    val apply_end: Method.text -> state -> state Seq.seq
     7.6    val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     7.7 -    (theory -> 'a -> attribute) ->
     7.8 +    (Proof.context -> 'a -> attribute) ->
     7.9      ('b list -> context -> (term list list * (context -> context)) * context) ->
    7.10      string -> Method.text option -> (thm list list -> state -> state) ->
    7.11      ((binding * 'a list) * 'b) list -> state -> state
    7.12 @@ -400,7 +400,8 @@
    7.13  fun no_goal_cases st = map (rpair NONE) (goals st);
    7.14  
    7.15  fun goal_cases st =
    7.16 -  Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
    7.17 +  Rule_Cases.make_common
    7.18 +    (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
    7.19  
    7.20  fun apply_method current_context meth state =
    7.21    let
    7.22 @@ -612,13 +613,13 @@
    7.23  fun gen_assume asm prep_att exp args state =
    7.24    state
    7.25    |> assert_forward
    7.26 -  |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (theory_of state))) args))
    7.27 +  |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (context_of state))) args))
    7.28    |> these_factss [] |> #2;
    7.29  
    7.30  in
    7.31  
    7.32  val assm = gen_assume Proof_Context.add_assms_i (K I);
    7.33 -val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute;
    7.34 +val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute_cmd;
    7.35  val assume = assm Assumption.assume_export;
    7.36  val assume_cmd = assm_cmd Assumption.assume_export;
    7.37  val presume = assm Assumption.presume_export;
    7.38 @@ -634,10 +635,8 @@
    7.39  fun gen_def prep_att prep_vars prep_binds args state =
    7.40    let
    7.41      val _ = assert_forward state;
    7.42 -    val thy = theory_of state;
    7.43 -
    7.44      val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
    7.45 -    val name_atts = map (apsnd (map (prep_att thy))) raw_name_atts;
    7.46 +    val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
    7.47    in
    7.48      state
    7.49      |> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars))
    7.50 @@ -651,7 +650,7 @@
    7.51  in
    7.52  
    7.53  val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind_i;
    7.54 -val def_cmd = gen_def Attrib.attribute Proof_Context.read_vars Proof_Context.match_bind;
    7.55 +val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind;
    7.56  
    7.57  end;
    7.58  
    7.59 @@ -683,10 +682,8 @@
    7.60  fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
    7.61    state
    7.62    |> assert_forward
    7.63 -  |> map_context_result (Proof_Context.note_thmss ""
    7.64 -    (Attrib.map_facts_refs
    7.65 -      (map (prep_atts (theory_of state)))
    7.66 -      (prep_fact (context_of state)) args))
    7.67 +  |> map_context_result (fn ctxt => ctxt |> Proof_Context.note_thmss ""
    7.68 +    (Attrib.map_facts_refs (map (prep_atts ctxt)) (prep_fact ctxt) args))
    7.69    |> these_factss (more_facts state)
    7.70    ||> opt_chain
    7.71    |> opt_result;
    7.72 @@ -694,13 +691,15 @@
    7.73  in
    7.74  
    7.75  val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
    7.76 -val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute Proof_Context.get_fact;
    7.77 +val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
    7.78  
    7.79  val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
    7.80 -val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
    7.81 +val from_thmss_cmd =
    7.82 +  gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
    7.83  
    7.84  val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
    7.85 -val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
    7.86 +val with_thmss_cmd =
    7.87 +  gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
    7.88  
    7.89  val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
    7.90  
    7.91 @@ -715,9 +714,8 @@
    7.92    state
    7.93    |> assert_backward
    7.94    |> map_context_result
    7.95 -    (Proof_Context.note_thmss ""
    7.96 -      (Attrib.map_facts_refs (map (prep_att (theory_of state))) (prep_fact (context_of state))
    7.97 -        (no_binding args)))
    7.98 +    (fn ctxt => ctxt |> Proof_Context.note_thmss ""
    7.99 +      (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
   7.100    |> (fn (named_facts, state') =>
   7.101      state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
   7.102        let
   7.103 @@ -732,9 +730,9 @@
   7.104  in
   7.105  
   7.106  val using = gen_using append_using (K (K I)) (K I) (K I);
   7.107 -val using_cmd = gen_using append_using (K (K I)) Attrib.attribute Proof_Context.get_fact;
   7.108 +val using_cmd = gen_using append_using (K (K I)) Attrib.attribute_cmd Proof_Context.get_fact;
   7.109  val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
   7.110 -val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute Proof_Context.get_fact;
   7.111 +val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact;
   7.112  
   7.113  end;
   7.114  
   7.115 @@ -748,7 +746,7 @@
   7.116  
   7.117  fun gen_invoke_case prep_att (name, xs, raw_atts) state =
   7.118    let
   7.119 -    val atts = map (prep_att (theory_of state)) raw_atts;
   7.120 +    val atts = map (prep_att (context_of state)) raw_atts;
   7.121      val (asms, state') = state |> map_context_result (fn ctxt =>
   7.122        ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
   7.123      val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
   7.124 @@ -762,7 +760,7 @@
   7.125  in
   7.126  
   7.127  val invoke_case = gen_invoke_case (K I);
   7.128 -val invoke_case_cmd = gen_invoke_case Attrib.attribute;
   7.129 +val invoke_case_cmd = gen_invoke_case Attrib.attribute_cmd;
   7.130  
   7.131  end;
   7.132  
   7.133 @@ -935,9 +933,8 @@
   7.134  
   7.135  fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state =
   7.136    let
   7.137 -    val thy = theory_of state;
   7.138      val ((names, attss), propp) =
   7.139 -      Attrib.map_specs (map (prep_att thy)) stmt |> split_list |>> split_list;
   7.140 +      Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
   7.141  
   7.142      fun after_qed' results =
   7.143        local_results ((names ~~ attss) ~~ results)
   7.144 @@ -1044,9 +1041,9 @@
   7.145  in
   7.146  
   7.147  val have = gen_have (K I) Proof_Context.bind_propp_i;
   7.148 -val have_cmd = gen_have Attrib.attribute Proof_Context.bind_propp;
   7.149 +val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp;
   7.150  val show = gen_show (K I) Proof_Context.bind_propp_i;
   7.151 -val show_cmd = gen_show Attrib.attribute Proof_Context.bind_propp;
   7.152 +val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp;
   7.153  
   7.154  end;
   7.155  
     8.1 --- a/src/Pure/ML/ml_antiquote.ML	Fri Apr 27 21:47:47 2012 +0200
     8.2 +++ b/src/Pure/ML/ml_antiquote.ML	Fri Apr 27 22:47:30 2012 +0200
     8.3 @@ -88,8 +88,7 @@
     8.4    macro (Binding.name "note")
     8.5      (Args.context :|-- (fn ctxt =>
     8.6        Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms
     8.7 -        >> (fn ((a, srcs), ths) =>
     8.8 -          ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
     8.9 +        >> (fn ((a, srcs), ths) => ((a, map (Attrib.attribute_cmd ctxt) srcs), [(ths, [])])))
    8.10        >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #>
    8.11  
    8.12    value (Binding.name "ctyp") (Args.typ >> (fn T =>
     9.1 --- a/src/Pure/ML/ml_thms.ML	Fri Apr 27 21:47:47 2012 +0200
     9.2 +++ b/src/Pure/ML/ml_thms.ML	Fri Apr 27 22:47:30 2012 +0200
     9.3 @@ -42,7 +42,7 @@
     9.4  
     9.5            val i = serial ();
     9.6            val srcs = map (Attrib.intern_src thy) raw_srcs;
     9.7 -          val _ = map (Attrib.attribute_i thy) srcs;
     9.8 +          val _ = map (Attrib.attribute background) srcs;
     9.9            val (a, background') = background
    9.10              |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
    9.11            val ml =
    10.1 --- a/src/ZF/Tools/ind_cases.ML	Fri Apr 27 21:47:47 2012 +0200
    10.2 +++ b/src/ZF/Tools/ind_cases.ML	Fri Apr 27 22:47:30 2012 +0200
    10.3 @@ -48,7 +48,7 @@
    10.4    let
    10.5      val ctxt = Proof_Context.init_global thy;
    10.6      val facts = args |> map (fn ((name, srcs), props) =>
    10.7 -      ((name, map (Attrib.attribute thy) srcs),
    10.8 +      ((name, map (Attrib.attribute_cmd_global thy) srcs),
    10.9          map (Thm.no_attributes o single o smart_cases ctxt) props));
   10.10    in thy |> Global_Theory.note_thmss "" facts |> snd end;
   10.11  
    11.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Apr 27 21:47:47 2012 +0200
    11.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Apr 27 22:47:30 2012 +0200
    11.3 @@ -558,7 +558,7 @@
    11.4      val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
    11.5        #> Syntax.check_terms ctxt;
    11.6  
    11.7 -    val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
    11.8 +    val intr_atts = map (map (Attrib.attribute_cmd_global thy) o snd) intr_srcs;
    11.9      val sintrs = map fst intr_srcs ~~ intr_atts;
   11.10      val rec_tms = read_terms srec_tms;
   11.11      val dom_sum = singleton read_terms sdom_sum;
    12.1 --- a/src/ZF/Tools/primrec_package.ML	Fri Apr 27 21:47:47 2012 +0200
    12.2 +++ b/src/ZF/Tools/primrec_package.ML	Fri Apr 27 22:47:30 2012 +0200
    12.3 @@ -189,7 +189,7 @@
    12.4  
    12.5  fun add_primrec args thy =
    12.6    add_primrec_i (map (fn ((name, s), srcs) =>
    12.7 -    ((name, Syntax.read_prop_global thy s), map (Attrib.attribute thy) srcs))
    12.8 +    ((name, Syntax.read_prop_global thy s), map (Attrib.attribute_cmd_global thy) srcs))
    12.9      args) thy;
   12.10  
   12.11