src/Pure/Isar/generic_target.ML
author nipkow
Fri, 21 Jun 2013 09:00:26 +0200
changeset 52402 c2f30ba4bb98
parent 52230 1105b3b5aa77
child 54742 7a86358a3c0b
permissions -rw-r--r--
tuned
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
52153
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
    44
  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
    45
    local_theory -> local_theory
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
    46
  val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
    47
    local_theory -> local_theory
45353
wenzelm
parents: 45352
diff changeset
    48
end
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    49
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    50
structure Generic_Target: GENERIC_TARGET =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    51
struct
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    52
38341
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
    53
(** lifting primitive to target operations **)
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
    54
38312
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    55
(* mixfix syntax *)
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    56
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    57
fun check_mixfix ctxt (b, extra_tfrees) mx =
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    58
  if null extra_tfrees then mx
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    59
  else
38831
4933a3dfd745 more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents: 38757
diff changeset
    60
    (Context_Position.if_visible ctxt warning
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42375
diff changeset
    61
      ("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
    62
        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
    63
        (if mx = NoSyn then ""
42287
d98eb048a2e4 discontinued special treatment of structure Mixfix;
wenzelm
parents: 41959
diff changeset
    64
         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
    65
      NoSyn);
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    66
47291
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
    67
fun check_mixfix_global (b, no_params) mx =
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
    68
  if no_params orelse mx = NoSyn then mx
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
    69
  else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
    70
    Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
    71
38312
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
    72
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    73
(* define *)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    74
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
    75
fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    76
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
    77
    val thy = Proof_Context.theory_of lthy;
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
    78
    val thy_ctxt = Proof_Context.init_global thy;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    79
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    80
    (*term and type parameters*)
47276
wenzelm
parents: 47272
diff changeset
    81
    val ((defs, _), rhs') = Thm.cterm_of thy rhs
wenzelm
parents: 47272
diff changeset
    82
      |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    83
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
    84
    val xs = Variable.add_fixed lthy rhs' [];
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    85
    val T = Term.fastype_of rhs;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    86
    val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    87
    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
    88
    val mx' = check_mixfix lthy (b, extra_tfrees) mx;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    89
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    90
    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
    91
    val term_params = map Free (sort (Variable.fixed_ord lthy o pairself #1) xs);
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    92
    val params = type_params @ term_params;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    93
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    94
    val U = map Term.fastype_of params ---> T;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    95
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    96
    (*foundation*)
45353
wenzelm
parents: 45352
diff changeset
    97
    val ((lhs', global_def), lthy2) = lthy
wenzelm
parents: 45352
diff changeset
    98
      |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params);
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
    99
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   100
    (*local definition*)
38315
fa3f90cf6d9c basic renumbering
haftmann
parents: 38313
diff changeset
   101
    val ((lhs, local_def), lthy3) = lthy2
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   102
      |> Local_Defs.add_def ((b, NoSyn), lhs');
47240
wenzelm
parents: 47238
diff changeset
   103
wenzelm
parents: 47238
diff changeset
   104
    (*result*)
47238
289dcbdd5984 more direct Local_Defs.contract;
wenzelm
parents: 47081
diff changeset
   105
    val def =
47240
wenzelm
parents: 47238
diff changeset
   106
      Thm.transitive local_def global_def
wenzelm
parents: 47238
diff changeset
   107
      |> Local_Defs.contract defs
wenzelm
parents: 47238
diff changeset
   108
          (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs)));
38315
fa3f90cf6d9c basic renumbering
haftmann
parents: 38313
diff changeset
   109
    val ([(res_name, [res])], lthy4) = lthy3
47080
wenzelm
parents: 46992
diff changeset
   110
      |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
38315
fa3f90cf6d9c basic renumbering
haftmann
parents: 38313
diff changeset
   111
  in ((lhs, (res_name, res)), lthy4) end;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   112
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   113
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   114
(* notes *)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   115
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   116
local
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   117
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   118
fun import_export_proof ctxt (name, raw_th) =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   119
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
   120
    val thy = Proof_Context.theory_of ctxt;
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
   121
    val thy_ctxt = Proof_Context.init_global thy;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   122
    val certT = Thm.ctyp_of thy;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   123
    val cert = Thm.cterm_of thy;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   124
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   125
    (*export assumes/defines*)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   126
    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
   127
    val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
52230
1105b3b5aa77 standardized aliases;
wenzelm
parents: 52153
diff changeset
   128
    val asms' = map (rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   129
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   130
    (*export fixes*)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   131
    val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   132
    val frees = map Free (Thm.fold_terms Term.add_frees th' []);
45352
0b4038361a3a misc tuning;
wenzelm
parents: 45310
diff changeset
   133
    val (th'' :: vs) =
0b4038361a3a misc tuning;
wenzelm
parents: 45310
diff changeset
   134
      (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   135
      |> Variable.export ctxt thy_ctxt
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   136
      |> Drule.zero_var_indexes_list;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   137
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   138
    (*thm definition*)
45413
117ff038f8f7 disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;
wenzelm
parents: 45407
diff changeset
   139
    val result = Global_Theory.name_thm true true name th'';
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   140
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   141
    (*import fixes*)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   142
    val (tvars, vars) =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   143
      chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   144
      |>> map Logic.dest_type;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   145
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   146
    val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   147
    val inst = filter (is_Var o fst) (vars ~~ frees);
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   148
    val cinstT = map (pairself certT o apfst TVar) instT;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   149
    val cinst = map (pairself (cert o Term.map_types (Term_Subst.instantiateT instT))) inst;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   150
    val result' = Thm.instantiate (cinstT, cinst) result;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   151
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   152
    (*import assumes/defines*)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   153
    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
   154
      (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
   155
        handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
47238
289dcbdd5984 more direct Local_Defs.contract;
wenzelm
parents: 47081
diff changeset
   156
      |> Local_Defs.contract defs (Thm.cprop_of th)
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   157
      |> 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
   158
      |> Global_Theory.name_thm false false name;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   159
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   160
  in (result'', result) end;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   161
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   162
fun standard_facts lthy ctxt =
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   163
  Element.transform_facts (Local_Theory.standard_morphism lthy ctxt);
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   164
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   165
in
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   166
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   167
fun notes target_notes kind facts lthy =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   168
  let
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   169
    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
   170
      |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   171
          (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
   172
      |> 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
   173
    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
   174
    val global_facts = Global_Theory.map_facts #2 facts';
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   175
  in
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   176
    lthy
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   177
    |> 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
   178
    |> Attrib.local_notes kind local_facts
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   179
  end;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   180
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   181
fun locale_notes locale kind global_facts local_facts =
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   182
  Local_Theory.background_theory
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   183
    (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
   184
  (fn lthy => lthy |>
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   185
    Local_Theory.target (fn ctxt => ctxt |>
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   186
      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
   187
  (fn lthy => lthy |>
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   188
    Local_Theory.map_contexts (fn level => fn ctxt =>
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   189
      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
   190
      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
   191
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   192
end;
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   193
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   194
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   195
(* abbrev *)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   196
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   197
fun abbrev target_abbrev prmode ((b, mx), t) lthy =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   198
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
   199
    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   200
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
   201
    val t' = Assumption.export_term lthy (Local_Theory.target_of lthy) t;
47290
ba9c8613ad9b more uniform abbrev vs. define;
wenzelm
parents: 47288
diff changeset
   202
    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
   203
    val u = fold_rev lambda xs t';
47290
ba9c8613ad9b more uniform abbrev vs. define;
wenzelm
parents: 47288
diff changeset
   204
    val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   205
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   206
    val extra_tfrees =
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   207
      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
   208
    val mx' = check_mixfix lthy (b, extra_tfrees) mx;
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   209
  in
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   210
    lthy
38312
9dd57db3c0f2 moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents: 38311
diff changeset
   211
    |> target_abbrev prmode (b, mx') (global_rhs, t') xs
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
   212
    |> Proof_Context.add_abbrev Print_Mode.internal (b, t) |> snd
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   213
    |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   214
  end;
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   215
38341
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   216
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
   217
(* 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
   218
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
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
   220
  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
   221
    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
   222
      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
   223
        (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
   224
  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
   225
47246
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47245
diff changeset
   226
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
   227
  |> Local_Theory.target (fn ctxt => ctxt |>
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47245
diff changeset
   228
    Locale.add_declaration locale syntax
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47245
diff changeset
   229
      (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
   230
47282
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   231
fun standard_declaration pred decl lthy =
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   232
  Local_Theory.map_contexts (fn level => fn ctxt =>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   233
    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
   234
    else ctxt) lthy;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   235
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   236
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   237
(* const declaration *)
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   238
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   239
fun generic_const same_shape prmode ((b, mx), t) context =
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   240
  let
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   241
    val const_alias =
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   242
      if same_shape then
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   243
        (case t of
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   244
          Const (c, T) =>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   245
            let
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   246
              val thy = Context.theory_of context;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   247
              val ctxt = Context.proof_of context;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   248
            in
47291
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   249
              (case Type_Infer_Context.const_type ctxt c of
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   250
                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
   251
              | NONE => NONE)
47282
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   252
            end
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   253
        | _ => NONE)
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   254
      else NONE;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   255
  in
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   256
    (case const_alias of
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   257
      SOME c =>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   258
        context
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   259
        |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c)
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   260
        |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)])
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   261
    | NONE =>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   262
        context
47288
b79bf8288b29 clarified generic_const vs. close_schematic_term;
wenzelm
parents: 47286
diff changeset
   263
        |> 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
   264
        |-> (fn (const as Const (c, _), _) => same_shape ?
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   265
              (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   266
               Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   267
  end;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   268
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   269
fun const_declaration pred prmode ((b, mx), rhs) =
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   270
  standard_declaration pred (fn phi =>
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   271
    let
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   272
      val b' = Morphism.binding phi b;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   273
      val rhs' = Morphism.term phi rhs;
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   274
      val same_shape = Term.aconv_untyped (rhs, rhs');
47288
b79bf8288b29 clarified generic_const vs. close_schematic_term;
wenzelm
parents: 47286
diff changeset
   275
    in generic_const same_shape prmode ((b', mx), rhs') end);
47280
wenzelm
parents: 47279
diff changeset
   276
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
   277
52153
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
   278
(* registrations and dependencies *)
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
   279
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
   280
val theory_registration =
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
   281
  Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
   282
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
   283
fun locale_dependency locale dep_morph mixin export =
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
   284
  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
   285
  #> Local_Theory.activate_nonbrittle dep_morph mixin export;
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
   286
f5773a46cf05 more specific structure for registration into theory and dependency onto locale
haftmann
parents: 47313
diff changeset
   287
45352
0b4038361a3a misc tuning;
wenzelm
parents: 45310
diff changeset
   288
38341
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   289
(** primitive theory operations **)
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   290
47284
0e65b6a016dc clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents: 47283
diff changeset
   291
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
   292
  let
47291
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   293
    val params = type_params @ term_params;
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   294
    val mx' = check_mixfix_global (b, null params) mx;
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   295
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   296
    val (const, lthy2) = lthy
47291
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   297
      |> 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
   298
    val lhs = Term.list_comb (const, params);
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   299
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   300
    val ((_, def), lthy3) = lthy2
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   301
      |> 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
   302
        (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
   303
          (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
   304
  in ((lhs, def), lthy3) end;
72dba5bd5f63 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents: 38315
diff changeset
   305
47284
0e65b6a016dc clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents: 47283
diff changeset
   306
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
   307
  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
   308
  #-> (fn (lhs, def) => fn lthy' => lthy' |>
ca4cf5de366c avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents: 47284
diff changeset
   309
        const_declaration (fn level => level <> Local_Theory.level lthy')
ca4cf5de366c avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents: 47284
diff changeset
   310
          Syntax.mode_default ((b, mx), lhs)
ca4cf5de366c avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents: 47284
diff changeset
   311
    |> pair (lhs, def));
47284
0e65b6a016dc clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents: 47283
diff changeset
   312
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   313
fun theory_notes kind global_facts local_facts =
47249
c0481c3c2a6c added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents: 47246
diff changeset
   314
  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
   315
  (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
   316
    if level = Local_Theory.level lthy then ctxt
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   317
    else
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   318
      ctxt |> Attrib.local_notes kind
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47249
diff changeset
   319
        (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
   320
47286
392c4cd97e5c more uniform theory_abbrev with const_declaration;
wenzelm
parents: 47285
diff changeset
   321
fun theory_abbrev prmode (b, mx) (t, _) xs =
392c4cd97e5c more uniform theory_abbrev with const_declaration;
wenzelm
parents: 47285
diff changeset
   322
  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
   323
    (Sign.add_abbrev (#1 prmode) (b, t) #->
47291
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   324
      (fn (lhs, _) =>  (* FIXME type_params!? *)
6a641856a0e9 better drop background syntax if entity depends on parameters;
wenzelm
parents: 47290
diff changeset
   325
        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
   326
  #-> (fn lhs => fn lthy' => lthy' |>
392c4cd97e5c more uniform theory_abbrev with const_declaration;
wenzelm
parents: 47285
diff changeset
   327
        const_declaration (fn level => level <> Local_Theory.level lthy') prmode
47293
052cd5f1a591 another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);
wenzelm
parents: 47292
diff changeset
   328
          ((b, if null xs then NoSyn else 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
   329
47279
4bab649dedf0 clarified standard_declaration vs. theory_declaration;
wenzelm
parents: 47276
diff changeset
   330
fun theory_declaration decl =
47282
57d486231c92 more general standard_declaration;
wenzelm
parents: 47280
diff changeset
   331
  background_declaration decl #> standard_declaration (K true) decl;
47279
4bab649dedf0 clarified standard_declaration vs. theory_declaration;
wenzelm
parents: 47276
diff changeset
   332
38309
9bd4e568c58c added generic_target.ML
haftmann
parents:
diff changeset
   333
end;