src/Pure/Isar/generic_target.ML
author wenzelm
Tue, 03 Apr 2012 16:27:32 +0200
changeset 47292 1884d34e9aab
parent 47291 6a641856a0e9
child 47293 052cd5f1a591
permissions -rw-r--r--
export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 41228
diff changeset
     1
(*  Title:      Pure/Isar/generic_target.ML
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
     2
    Author:     Makarius
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
     4
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
     5
Common target infrastructure.
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
     6
*)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
     7
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
     8
signature GENERIC_TARGET =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
     9
sig
40782
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39557
diff changeset
    10
  val define: (((binding * typ) * mixfix) * (binding * term) ->
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39557
diff changeset
    11
      term list * term list -> local_theory -> (term * thm) * local_theory) ->
46992
eeea81b86b70 refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents: 46916
diff changeset
    12
    bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
40782
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39557
diff changeset
    13
    (term * (string * thm)) * local_theory
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
    14
  val notes:
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
    15
    (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
40782
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39557
diff changeset
    16
      (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39557
diff changeset
    17
    string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39557
diff changeset
    18
    (string * thm list) list * local_theory
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
    19
  val locale_notes: string -> string ->
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
    20
    (Attrib.binding * (thm list * Args.src list) list) list ->
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
    21
    (Attrib.binding * (thm list * Args.src list) list) list ->
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
    22
    local_theory -> local_theory
40782
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39557
diff changeset
    23
  val abbrev: (string * bool -> binding * mixfix -> term * term ->
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39557
diff changeset
    24
      term list -> local_theory -> local_theory) ->
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
    25
    string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
47081
5e70b457b704 uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents: 47080
diff changeset
    26
  val background_declaration: declaration -> local_theory -> local_theory
47280
wenzelm
parents: 47279
diff changeset
    27
  val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory
47282
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
    28
  val standard_declaration: (int -> bool) -> declaration -> local_theory -> local_theory
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
    29
  val generic_const: bool -> Syntax.mode -> (binding * mixfix) * term ->
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
    30
    Context.generic -> Context.generic
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
    31
  val const_declaration: (int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
    32
    local_theory -> local_theory
47284
0e65b6a016dc clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents: 47283
diff changeset
    33
  val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
0e65b6a016dc clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents: 47283
diff changeset
    34
    term list * term list -> local_theory -> (term * thm) * local_theory
40782
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39557
diff changeset
    35
  val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39557
diff changeset
    36
    term list * term list -> local_theory -> (term * thm) * local_theory
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
    37
  val theory_notes: string ->
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
    38
    (Attrib.binding * (thm list * Args.src list) list) list ->
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
    39
    (Attrib.binding * (thm list * Args.src list) list) list ->
40782
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39557
diff changeset
    40
    local_theory -> local_theory
47286
392c4cd97e5c more uniform theory_abbrev with const_declaration;
wenzelm
parents: 47285
diff changeset
    41
  val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term * term -> term list ->
392c4cd97e5c more uniform theory_abbrev with const_declaration;
wenzelm
parents: 47285
diff changeset
    42
    local_theory -> local_theory
47279
4bab649dedf0 clarified standard_declaration vs. theory_declaration;
wenzelm
parents: 47276
diff changeset
    43
  val theory_declaration: declaration -> local_theory -> local_theory
45353
wenzelm
parents: 45352
diff changeset
    44
end
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    45
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    46
structure Generic_Target: GENERIC_TARGET =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    47
struct
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    48
38341
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
    49
(** lifting primitive to target operations **)
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
    50
38312
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    51
(* mixfix syntax *)
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    52
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    53
fun check_mixfix ctxt (b, extra_tfrees) mx =
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    54
  if null extra_tfrees then mx
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    55
  else
38831
4933a3dfd745 more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents: 38757
diff changeset
    56
    (Context_Position.if_visible ctxt warning
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42375
diff changeset
    57
      ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
38312
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    58
        commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    59
        (if mx = NoSyn then ""
42287
d98eb048a2e4 discontinued special treatment of structure Mixfix;
wenzelm
parents: 41959
diff changeset
    60
         else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)));
38312
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    61
      NoSyn);
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    62
47291
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
    63
fun check_mixfix_global (b, no_params) mx =
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
    64
  if no_params orelse mx = NoSyn then mx
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
    65
  else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
    66
    Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
    67
38312
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    68
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    69
(* define *)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    70
46992
eeea81b86b70 refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents: 46916
diff changeset
    71
fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    72
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
    73
    val thy = Proof_Context.theory_of lthy;
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
    74
    val thy_ctxt = Proof_Context.init_global thy;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    75
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    76
    (*term and type parameters*)
47276
wenzelm
parents: 47272
diff changeset
    77
    val ((defs, _), rhs') = Thm.cterm_of thy rhs
wenzelm
parents: 47272
diff changeset
    78
      |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    79
47272
ca31cfa509b1 refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);
wenzelm
parents: 47250
diff changeset
    80
    val xs = Variable.add_fixed lthy rhs' [];
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    81
    val T = Term.fastype_of rhs;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    82
    val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    83
    val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
38312
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    84
    val mx' = check_mixfix lthy (b, extra_tfrees) mx;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    85
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    86
    val type_params = map (Logic.mk_type o TFree) extra_tfrees;
47272
ca31cfa509b1 refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);
wenzelm
parents: 47250
diff changeset
    87
    val term_params = map Free (sort (Variable.fixed_ord lthy o pairself #1) xs);
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    88
    val params = type_params @ term_params;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    89
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    90
    val U = map Term.fastype_of params ---> T;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    91
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    92
    (*foundation*)
45353
wenzelm
parents: 45352
diff changeset
    93
    val ((lhs', global_def), lthy2) = lthy
wenzelm
parents: 45352
diff changeset
    94
      |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params);
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    95
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    96
    (*local definition*)
38315
fa3f90cf6d9c basic renumbering
haftmann
parents: 38313
diff changeset
    97
    val ((lhs, local_def), lthy3) = lthy2
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    98
      |> Local_Defs.add_def ((b, NoSyn), lhs');
47240
wenzelm
parents: 47238
diff changeset
    99
wenzelm
parents: 47238
diff changeset
   100
    (*result*)
47238
289dcbdd5984 more direct Local_Defs.contract;
wenzelm
parents: 47081
diff changeset
   101
    val def =
47240
wenzelm
parents: 47238
diff changeset
   102
      Thm.transitive local_def global_def
wenzelm
parents: 47238
diff changeset
   103
      |> Local_Defs.contract defs
wenzelm
parents: 47238
diff changeset
   104
          (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs)));
38315
fa3f90cf6d9c basic renumbering
haftmann
parents: 38313
diff changeset
   105
    val ([(res_name, [res])], lthy4) = lthy3
47080
wenzelm
parents: 46992
diff changeset
   106
      |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
38315
fa3f90cf6d9c basic renumbering
haftmann
parents: 38313
diff changeset
   107
  in ((lhs, (res_name, res)), lthy4) end;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   108
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   109
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   110
(* notes *)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   111
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   112
local
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   113
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   114
fun import_export_proof ctxt (name, raw_th) =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   115
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
   116
    val thy = Proof_Context.theory_of ctxt;
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
   117
    val thy_ctxt = Proof_Context.init_global thy;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   118
    val certT = Thm.ctyp_of thy;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   119
    val cert = Thm.cterm_of thy;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   120
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   121
    (*export assumes/defines*)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   122
    val th = Goal.norm_result raw_th;
45407
a83574606719 more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
wenzelm
parents: 45390
diff changeset
   123
    val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
a83574606719 more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
wenzelm
parents: 45390
diff changeset
   124
    val asms' = map (Raw_Simplifier.rewrite_rule defs) asms;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   125
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   126
    (*export fixes*)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   127
    val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   128
    val frees = map Free (Thm.fold_terms Term.add_frees th' []);
45352
0b4038361a3a misc tuning;
wenzelm
parents: 45310
diff changeset
   129
    val (th'' :: vs) =
0b4038361a3a misc tuning;
wenzelm
parents: 45310
diff changeset
   130
      (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   131
      |> Variable.export ctxt thy_ctxt
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   132
      |> Drule.zero_var_indexes_list;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   133
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   134
    (*thm definition*)
45413
117ff038f8f7 disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;
wenzelm
parents: 45407
diff changeset
   135
    val result = Global_Theory.name_thm true true name th'';
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   136
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   137
    (*import fixes*)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   138
    val (tvars, vars) =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   139
      chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   140
      |>> map Logic.dest_type;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   141
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   142
    val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   143
    val inst = filter (is_Var o fst) (vars ~~ frees);
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   144
    val cinstT = map (pairself certT o apfst TVar) instT;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   145
    val cinst = map (pairself (cert o Term.map_types (Term_Subst.instantiateT instT))) inst;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   146
    val result' = Thm.instantiate (cinstT, cinst) result;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   147
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   148
    (*import assumes/defines*)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   149
    val result'' =
45407
a83574606719 more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
wenzelm
parents: 45390
diff changeset
   150
      (fold (curry op COMP) asms' result'
a83574606719 more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
wenzelm
parents: 45390
diff changeset
   151
        handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
47238
289dcbdd5984 more direct Local_Defs.contract;
wenzelm
parents: 47081
diff changeset
   152
      |> Local_Defs.contract defs (Thm.cprop_of th)
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   153
      |> Goal.norm_result
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38831
diff changeset
   154
      |> Global_Theory.name_thm false false name;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   155
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   156
  in (result'', result) end;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   157
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   158
fun standard_facts lthy ctxt =
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   159
  Element.transform_facts (Local_Theory.standard_morphism lthy ctxt);
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   160
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   161
in
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   162
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   163
fun notes target_notes kind facts lthy =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   164
  let
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   165
    val facts' = facts
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38831
diff changeset
   166
      |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   167
          (Local_Theory.full_name lthy (fst a))) bs))
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38831
diff changeset
   168
      |> Global_Theory.map_facts (import_export_proof lthy);
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38831
diff changeset
   169
    val local_facts = Global_Theory.map_facts #1 facts';
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38831
diff changeset
   170
    val global_facts = Global_Theory.map_facts #2 facts';
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   171
  in
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   172
    lthy
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   173
    |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
47249
c0481c3c2a6c added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents: 47246
diff changeset
   174
    |> Attrib.local_notes kind local_facts
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   175
  end;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   176
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   177
fun locale_notes locale kind global_facts local_facts =
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   178
  Local_Theory.background_theory
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   179
    (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   180
  (fn lthy => lthy |>
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   181
    Local_Theory.target (fn ctxt => ctxt |>
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   182
      Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   183
  (fn lthy => lthy |>
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   184
    Local_Theory.map_contexts (fn level => fn ctxt =>
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   185
      if level = 0 orelse level = Local_Theory.level lthy then ctxt
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   186
      else ctxt |> Attrib.local_notes kind (standard_facts lthy ctxt local_facts) |> snd));
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   187
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   188
end;
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   189
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   190
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   191
(* abbrev *)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   192
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   193
fun abbrev target_abbrev prmode ((b, mx), t) lthy =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   194
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
   195
    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   196
47292
1884d34e9aab export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
wenzelm
parents: 47291
diff changeset
   197
    val t' = Assumption.export_term lthy (Local_Theory.target_of lthy) t;
47290
ba9c8613ad9b more uniform abbrev vs. define;
wenzelm
parents: 47288
diff changeset
   198
    val xs = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy t' []));
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   199
    val u = fold_rev lambda xs t';
47290
ba9c8613ad9b more uniform abbrev vs. define;
wenzelm
parents: 47288
diff changeset
   200
    val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   201
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   202
    val extra_tfrees =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   203
      subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
38312
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
   204
    val mx' = check_mixfix lthy (b, extra_tfrees) mx;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   205
  in
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   206
    lthy
38312
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
   207
    |> target_abbrev prmode (b, mx') (global_rhs, t') xs
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
   208
    |> Proof_Context.add_abbrev Print_Mode.internal (b, t) |> snd
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   209
    |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   210
  end;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   211
38341
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   212
47081
5e70b457b704 uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents: 47080
diff changeset
   213
(* declaration *)
5e70b457b704 uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents: 47080
diff changeset
   214
5e70b457b704 uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents: 47080
diff changeset
   215
fun background_declaration decl lthy =
5e70b457b704 uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents: 47080
diff changeset
   216
  let
5e70b457b704 uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents: 47080
diff changeset
   217
    val theory_decl =
5e70b457b704 uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents: 47080
diff changeset
   218
      Local_Theory.standard_form lthy
5e70b457b704 uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents: 47080
diff changeset
   219
        (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
5e70b457b704 uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents: 47080
diff changeset
   220
  in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
5e70b457b704 uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents: 47080
diff changeset
   221
47246
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47245
diff changeset
   222
fun locale_declaration locale syntax decl lthy = lthy
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47245
diff changeset
   223
  |> Local_Theory.target (fn ctxt => ctxt |>
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47245
diff changeset
   224
    Locale.add_declaration locale syntax
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47245
diff changeset
   225
      (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47245
diff changeset
   226
47282
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   227
fun standard_declaration pred decl lthy =
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   228
  Local_Theory.map_contexts (fn level => fn ctxt =>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   229
    if pred level then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   230
    else ctxt) lthy;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   231
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   232
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   233
(* const declaration *)
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   234
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   235
fun generic_const same_shape prmode ((b, mx), t) context =
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   236
  let
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   237
    val const_alias =
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   238
      if same_shape then
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   239
        (case t of
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   240
          Const (c, T) =>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   241
            let
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   242
              val thy = Context.theory_of context;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   243
              val ctxt = Context.proof_of context;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   244
            in
47291
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   245
              (case Type_Infer_Context.const_type ctxt c of
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   246
                SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   247
              | NONE => NONE)
47282
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   248
            end
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   249
        | _ => NONE)
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   250
      else NONE;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   251
  in
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   252
    (case const_alias of
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   253
      SOME c =>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   254
        context
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   255
        |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c)
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   256
        |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)])
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   257
    | NONE =>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   258
        context
47288
b79bf8288b29 clarified generic_const vs. close_schematic_term;
wenzelm
parents: 47286
diff changeset
   259
        |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, Term.close_schematic_term t)
47282
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   260
        |-> (fn (const as Const (c, _), _) => same_shape ?
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   261
              (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   262
               Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   263
  end;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   264
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   265
fun const_declaration pred prmode ((b, mx), rhs) =
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   266
  standard_declaration pred (fn phi =>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   267
    let
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   268
      val b' = Morphism.binding phi b;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   269
      val rhs' = Morphism.term phi rhs;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   270
      val same_shape = Term.aconv_untyped (rhs, rhs');
47288
b79bf8288b29 clarified generic_const vs. close_schematic_term;
wenzelm
parents: 47286
diff changeset
   271
    in generic_const same_shape prmode ((b', mx), rhs') end);
47280
wenzelm
parents: 47279
diff changeset
   272
47081
5e70b457b704 uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents: 47080
diff changeset
   273
45352
0b4038361a3a misc tuning;
wenzelm
parents: 45310
diff changeset
   274
38341
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   275
(** primitive theory operations **)
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   276
47284
0e65b6a016dc clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents: 47283
diff changeset
   277
fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
38341
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   278
  let
47291
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   279
    val params = type_params @ term_params;
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   280
    val mx' = check_mixfix_global (b, null params) mx;
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   281
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   282
    val (const, lthy2) = lthy
47291
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   283
      |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx'));
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   284
    val lhs = Term.list_comb (const, params);
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   285
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   286
    val ((_, def), lthy3) = lthy2
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   287
      |> Local_Theory.background_theory_result
46916
e7ea35b41e2d Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents: 45413
diff changeset
   288
        (Thm.add_def lthy2 false false
e7ea35b41e2d Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents: 45413
diff changeset
   289
          (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
38341
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   290
  in ((lhs, def), lthy3) end;
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   291
47284
0e65b6a016dc clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents: 47283
diff changeset
   292
fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
0e65b6a016dc clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents: 47283
diff changeset
   293
  background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
47285
ca4cf5de366c avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents: 47284
diff changeset
   294
  #-> (fn (lhs, def) => fn lthy' => lthy' |>
ca4cf5de366c avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents: 47284
diff changeset
   295
        const_declaration (fn level => level <> Local_Theory.level lthy')
ca4cf5de366c avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents: 47284
diff changeset
   296
          Syntax.mode_default ((b, mx), lhs)
ca4cf5de366c avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents: 47284
diff changeset
   297
    |> pair (lhs, def));
47284
0e65b6a016dc clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents: 47283
diff changeset
   298
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   299
fun theory_notes kind global_facts local_facts =
47249
c0481c3c2a6c added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents: 47246
diff changeset
   300
  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   301
  (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   302
    if level = Local_Theory.level lthy then ctxt
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   303
    else
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   304
      ctxt |> Attrib.local_notes kind
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   305
        (Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd));
38341
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   306
47286
392c4cd97e5c more uniform theory_abbrev with const_declaration;
wenzelm
parents: 47285
diff changeset
   307
fun theory_abbrev prmode (b, mx) (t, _) xs =
392c4cd97e5c more uniform theory_abbrev with const_declaration;
wenzelm
parents: 47285
diff changeset
   308
  Local_Theory.background_theory_result
38757
2b3e054ae6fc renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents: 38341
diff changeset
   309
    (Sign.add_abbrev (#1 prmode) (b, t) #->
47291
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   310
      (fn (lhs, _) =>  (* FIXME type_params!? *)
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   311
        Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs))
47286
392c4cd97e5c more uniform theory_abbrev with const_declaration;
wenzelm
parents: 47285
diff changeset
   312
  #-> (fn lhs => fn lthy' => lthy' |>
392c4cd97e5c more uniform theory_abbrev with const_declaration;
wenzelm
parents: 47285
diff changeset
   313
        const_declaration (fn level => level <> Local_Theory.level lthy') prmode
392c4cd97e5c more uniform theory_abbrev with const_declaration;
wenzelm
parents: 47285
diff changeset
   314
          ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
38341
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   315
47279
4bab649dedf0 clarified standard_declaration vs. theory_declaration;
wenzelm
parents: 47276
diff changeset
   316
fun theory_declaration decl =
47282
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   317
  background_declaration decl #> standard_declaration (K true) decl;
47279
4bab649dedf0 clarified standard_declaration vs. theory_declaration;
wenzelm
parents: 47276
diff changeset
   318
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   319
end;