src/Pure/Isar/interpretation.ML
author wenzelm
Mon Jul 04 20:33:47 2016 +0200 (2016-07-04 ago)
changeset 63383 4270da306442
parent 63382 823660593928
child 63402 f199837304d7
permissions -rw-r--r--
clarified positions, e.g. for reports on literal facts;
haftmann@61669
     1
(*  Title:      Pure/Isar/interpretation.ML
haftmann@61669
     2
    Author:     Clemens Ballarin, TU Muenchen
haftmann@61670
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@61669
     4
haftmann@61669
     5
Locale interpretation.
haftmann@61669
     6
*)
haftmann@61669
     7
haftmann@61669
     8
signature INTERPRETATION =
haftmann@61669
     9
sig
haftmann@61673
    10
  type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
haftmann@61673
    11
  type 'a rewrites = (Attrib.binding * 'a) list
haftmann@61673
    12
haftmann@61673
    13
  (*interpretation in proofs*)
wenzelm@62680
    14
  val interpret: Expression.expression_i -> term rewrites -> Proof.state -> Proof.state
wenzelm@62680
    15
  val interpret_cmd: Expression.expression -> string rewrites -> Proof.state -> Proof.state
haftmann@61673
    16
haftmann@61858
    17
  (*interpretation in local theories*)
haftmann@61858
    18
  val interpretation: Expression.expression_i ->
haftmann@61858
    19
    term rewrites -> local_theory -> Proof.state
haftmann@61858
    20
  val interpretation_cmd: Expression.expression ->
haftmann@61858
    21
    string rewrites -> local_theory -> Proof.state
haftmann@61858
    22
haftmann@61858
    23
  (*interpretation into global theories*)
haftmann@61673
    24
  val global_interpretation: Expression.expression_i ->
haftmann@61858
    25
    term defines -> term rewrites -> local_theory -> Proof.state
haftmann@61858
    26
  val global_interpretation_cmd: Expression.expression ->
haftmann@61858
    27
    string defines -> string rewrites -> local_theory -> Proof.state
haftmann@61858
    28
haftmann@61858
    29
  (*interpretation between locales*)
haftmann@61673
    30
  val sublocale: Expression.expression_i ->
haftmann@61673
    31
    term defines -> term rewrites -> local_theory -> Proof.state
haftmann@61673
    32
  val sublocale_cmd: Expression.expression ->
haftmann@61673
    33
    string defines -> string rewrites -> local_theory -> Proof.state
haftmann@61858
    34
  val global_sublocale: string -> Expression.expression_i ->
haftmann@61858
    35
    term defines -> term rewrites -> theory -> Proof.state
haftmann@61858
    36
  val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
haftmann@61858
    37
    string defines -> string rewrites -> theory -> Proof.state
haftmann@61673
    38
haftmann@61673
    39
  (*mixed Isar interface*)
haftmann@61858
    40
  val isar_interpretation: Expression.expression_i ->
haftmann@61858
    41
    term rewrites -> local_theory -> Proof.state
haftmann@61858
    42
  val isar_interpretation_cmd: Expression.expression ->
haftmann@61858
    43
    string rewrites -> local_theory -> Proof.state
haftmann@61669
    44
end;
haftmann@61669
    45
haftmann@61669
    46
structure Interpretation : INTERPRETATION =
haftmann@61669
    47
struct
haftmann@61669
    48
haftmann@61673
    49
(** common interpretation machinery **)
haftmann@61673
    50
haftmann@61673
    51
type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
haftmann@61673
    52
type 'a rewrites = (Attrib.binding * 'a) list
haftmann@61673
    53
haftmann@61673
    54
(* reading of locale expressions with rewrite morphisms *)
haftmann@61670
    55
haftmann@61672
    56
local
haftmann@61669
    57
haftmann@61775
    58
fun augment_with_def prep_term deps ((name, atts), ((b, mx), raw_rhs)) lthy =
haftmann@61670
    59
  let
haftmann@61775
    60
    val rhs = prep_term lthy raw_rhs;
haftmann@61775
    61
    val lthy' = Variable.declare_term rhs lthy;
haftmann@61775
    62
    val ((_, (_, def)), lthy'') =
haftmann@61775
    63
      Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy';
haftmann@61775
    64
  in (def, lthy'') end;
haftmann@61669
    65
haftmann@61775
    66
fun augment_with_defs prep_term [] deps ctxt = ([], ctxt)
haftmann@61691
    67
      (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
haftmann@61775
    68
  | augment_with_defs prep_term raw_defs deps lthy =
haftmann@61691
    69
      let
haftmann@61775
    70
        val (_, inner_lthy) =
haftmann@61775
    71
          Local_Theory.open_target lthy
haftmann@61775
    72
          ||> fold Locale.activate_declarations deps;
haftmann@61775
    73
        val (inner_defs, inner_lthy') =
haftmann@61775
    74
          fold_map (augment_with_def prep_term deps) raw_defs inner_lthy;
haftmann@61775
    75
        val lthy' =
haftmann@61775
    76
          inner_lthy'
haftmann@61708
    77
          |> Local_Theory.close_target;
haftmann@61708
    78
        val def_eqns =
haftmann@61775
    79
          map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs
haftmann@61775
    80
      in (def_eqns, lthy') end;
haftmann@61775
    81
haftmann@61775
    82
fun prep_eqns prep_props prep_attr [] deps ctxt = ([], [])
haftmann@61775
    83
  | prep_eqns prep_props prep_attr raw_eqns deps ctxt =
haftmann@61775
    84
      let
haftmann@61775
    85
        val ctxt' = fold Locale.activate_declarations deps ctxt;
haftmann@61775
    86
        val eqns =
haftmann@61775
    87
          (Variable.export_terms ctxt' ctxt o prep_props ctxt' o map snd) raw_eqns;
haftmann@61775
    88
        val attrss = map (apsnd (map (prep_attr ctxt)) o fst) raw_eqns;
haftmann@61775
    89
      in (eqns, attrss) end;
haftmann@61691
    90
haftmann@61774
    91
fun prep_interpretation prep_expr prep_term prep_props prep_attr
haftmann@61691
    92
  expression raw_defs raw_eqns initial_ctxt =
haftmann@61691
    93
  let
haftmann@61691
    94
    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
haftmann@61775
    95
    val (def_eqns, def_ctxt) =
haftmann@61775
    96
      augment_with_defs prep_term raw_defs deps expr_ctxt;
haftmann@61775
    97
    val (eqns, attrss) = prep_eqns prep_props prep_attr raw_eqns deps def_ctxt;
haftmann@61672
    98
    val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
haftmann@61772
    99
    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
haftmann@61672
   100
  in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
haftmann@61669
   101
haftmann@61670
   102
in
haftmann@61670
   103
wenzelm@61698
   104
fun cert_interpretation expression =
haftmann@61774
   105
  prep_interpretation Expression.cert_goal_expression Syntax.check_term
haftmann@61774
   106
    Syntax.check_props (K I) expression;
haftmann@61672
   107
wenzelm@61698
   108
fun read_interpretation expression =
haftmann@61774
   109
  prep_interpretation Expression.read_goal_expression Syntax.read_term
haftmann@61774
   110
    Syntax.read_props Attrib.check_src expression;
haftmann@61669
   111
haftmann@61670
   112
end;
haftmann@61669
   113
haftmann@61670
   114
haftmann@61673
   115
(* interpretation machinery *)
haftmann@61670
   116
haftmann@61670
   117
local
haftmann@61670
   118
wenzelm@63382
   119
fun meta_rewrite eqns ctxt =
wenzelm@63382
   120
  (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
haftmann@61670
   121
wenzelm@63383
   122
fun note_eqns_register pos note activate deps witss def_eqns eqns attrss export export' ctxt =
haftmann@61670
   123
  let
wenzelm@63382
   124
    val facts =
wenzelm@63382
   125
      (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) ::
wenzelm@63382
   126
        map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])]))
wenzelm@63382
   127
          attrss eqns;
haftmann@61670
   128
    val (eqns', ctxt') = ctxt
haftmann@61670
   129
      |> note Thm.theoremK facts
haftmann@61670
   130
      |-> meta_rewrite;
wenzelm@63382
   131
    val dep_morphs =
wenzelm@63382
   132
      map2 (fn (dep, morph) => fn wits =>
wenzelm@63383
   133
        let val morph' = morph
wenzelm@63383
   134
          $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
wenzelm@63383
   135
          $> Morphism.binding_morphism "position" (Binding.set_pos pos)
wenzelm@63383
   136
        in (dep, morph') end) deps witss;
wenzelm@63382
   137
    fun activate' dep_morph ctxt =
wenzelm@63382
   138
      activate dep_morph
wenzelm@63382
   139
        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns'))
wenzelm@63382
   140
        export ctxt;
wenzelm@63382
   141
  in ctxt' |> fold activate' dep_morphs end;
haftmann@61670
   142
haftmann@61670
   143
in
haftmann@61670
   144
wenzelm@63381
   145
fun generic_interpretation prep_interpretation setup_proof note add_registration
haftmann@61670
   146
    expression raw_defs raw_eqns initial_ctxt =
haftmann@61670
   147
  let
haftmann@61670
   148
    val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
haftmann@61670
   149
      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
wenzelm@63383
   150
    val pos = Position.thread_data ();
haftmann@61670
   151
    fun after_qed witss eqns =
wenzelm@63383
   152
      note_eqns_register pos note add_registration deps witss def_eqns eqns attrss export export';
haftmann@61670
   153
  in setup_proof after_qed propss eqns goal_ctxt end;
haftmann@61670
   154
haftmann@61670
   155
end;
haftmann@61670
   156
haftmann@61670
   157
haftmann@61673
   158
(** interfaces **)
haftmann@61673
   159
haftmann@61673
   160
(* interpretation in proofs *)
haftmann@61670
   161
haftmann@61672
   162
local
haftmann@61672
   163
wenzelm@62680
   164
fun gen_interpret prep_interpretation expression raw_eqns state =
haftmann@61669
   165
  let
haftmann@61669
   166
    val _ = Proof.assert_forward_or_chain state;
haftmann@61669
   167
    fun lift_after_qed after_qed witss eqns =
haftmann@61669
   168
      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
haftmann@61669
   169
    fun setup_proof after_qed propss eqns goal_ctxt =
haftmann@61669
   170
      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
wenzelm@62680
   171
        propss eqns goal_ctxt state;
haftmann@61669
   172
  in
wenzelm@63380
   173
    Proof.context_of state
wenzelm@63380
   174
    |> generic_interpretation prep_interpretation setup_proof
wenzelm@63381
   175
      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression [] raw_eqns
haftmann@61669
   176
  end;
haftmann@61669
   177
haftmann@61673
   178
in
haftmann@61670
   179
wenzelm@63380
   180
val interpret = gen_interpret cert_interpretation;
wenzelm@63380
   181
val interpret_cmd = gen_interpret read_interpretation;
haftmann@61669
   182
haftmann@61673
   183
end;
haftmann@61670
   184
haftmann@61670
   185
haftmann@61858
   186
(* interpretation in local theories *)
haftmann@61858
   187
haftmann@61858
   188
fun interpretation expression =
haftmann@61858
   189
  generic_interpretation cert_interpretation Element.witness_proof_eqs
wenzelm@63381
   190
    Local_Theory.notes_kind Locale.activate_fragment expression [];
haftmann@61858
   191
wenzelm@63381
   192
fun interpretation_cmd expression =
haftmann@61858
   193
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm@63381
   194
    Local_Theory.notes_kind Locale.activate_fragment expression [];
haftmann@61858
   195
haftmann@61858
   196
haftmann@61858
   197
(* interpretation into global theories *)
haftmann@61858
   198
haftmann@61858
   199
fun global_interpretation expression =
wenzelm@63381
   200
  generic_interpretation cert_interpretation Element.witness_proof_eqs
haftmann@61858
   201
    Local_Theory.notes_kind Local_Theory.theory_registration expression;
haftmann@61858
   202
wenzelm@63381
   203
fun global_interpretation_cmd expression =
wenzelm@63381
   204
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm@63381
   205
    Local_Theory.notes_kind Local_Theory.theory_registration expression;
haftmann@61858
   206
haftmann@61858
   207
haftmann@61858
   208
(* interpretation between locales *)
haftmann@61858
   209
haftmann@61858
   210
fun sublocale expression =
wenzelm@63381
   211
  generic_interpretation cert_interpretation Element.witness_proof_eqs
haftmann@61858
   212
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
haftmann@61858
   213
wenzelm@63381
   214
fun sublocale_cmd expression =
wenzelm@63381
   215
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm@63381
   216
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
haftmann@61673
   217
haftmann@61673
   218
local
haftmann@61669
   219
haftmann@61673
   220
fun gen_global_sublocale prep_loc prep_interpretation
haftmann@61673
   221
    raw_locale expression raw_defs raw_eqns thy =
haftmann@61673
   222
  let
haftmann@61673
   223
    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
haftmann@61673
   224
    fun setup_proof after_qed =
haftmann@61673
   225
      Element.witness_proof_eqs
haftmann@61673
   226
        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
haftmann@61673
   227
  in
haftmann@61673
   228
    lthy |>
wenzelm@63381
   229
      generic_interpretation prep_interpretation setup_proof
haftmann@61858
   230
        Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs raw_eqns
haftmann@61673
   231
  end;
haftmann@61669
   232
haftmann@61673
   233
in
haftmann@61669
   234
haftmann@61673
   235
fun global_sublocale expression =
haftmann@61673
   236
  gen_global_sublocale (K I) cert_interpretation expression;
haftmann@61858
   237
haftmann@61673
   238
fun global_sublocale_cmd raw_expression =
haftmann@61673
   239
  gen_global_sublocale Locale.check read_interpretation raw_expression;
haftmann@61669
   240
haftmann@61673
   241
end;
haftmann@61673
   242
haftmann@61673
   243
haftmann@61673
   244
(* mixed Isar interface *)
haftmann@61673
   245
haftmann@61673
   246
local
haftmann@61670
   247
haftmann@61858
   248
fun register_or_activate lthy =
haftmann@61673
   249
  if Named_Target.is_theory lthy
haftmann@61858
   250
  then Local_Theory.theory_registration
haftmann@61673
   251
  else Locale.activate_fragment;
haftmann@61669
   252
haftmann@61858
   253
fun gen_isar_interpretation prep_interpretation expression raw_eqns lthy =
haftmann@61673
   254
  generic_interpretation prep_interpretation Element.witness_proof_eqs
wenzelm@63381
   255
    Local_Theory.notes_kind (register_or_activate lthy) expression [] raw_eqns lthy;
haftmann@61669
   256
haftmann@61673
   257
in
haftmann@61673
   258
haftmann@61858
   259
fun isar_interpretation expression =
haftmann@61858
   260
  gen_isar_interpretation cert_interpretation expression;
haftmann@61858
   261
fun isar_interpretation_cmd raw_expression =
haftmann@61858
   262
  gen_isar_interpretation read_interpretation raw_expression;
haftmann@61669
   263
haftmann@61669
   264
end;
haftmann@61669
   265
haftmann@61669
   266
end;