src/Pure/Isar/interpretation.ML
author haftmann
Sat Nov 14 08:45:52 2015 +0100 (2015-11-14 ago)
changeset 61670 301e0b4ecd45
parent 61669 27ca6147e3b3
child 61672 87203a0f0041
permissions -rw-r--r--
coalesce permanent_interpretation.ML with interpretation.ML
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@61669
    10
  val interpret: Expression.expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
haftmann@61669
    11
  val interpret_cmd: Expression.expression -> (Attrib.binding * string) list ->
haftmann@61669
    12
    bool -> Proof.state -> Proof.state
haftmann@61670
    13
  val ephemeral_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
haftmann@61670
    14
    local_theory -> Proof.state
haftmann@61670
    15
  val permanent_interpretation: Expression.expression_i ->
haftmann@61670
    16
    (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
haftmann@61670
    17
    local_theory -> Proof.state
haftmann@61670
    18
  val permanent_interpretation_cmd: Expression.expression ->
haftmann@61670
    19
    (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
haftmann@61670
    20
    local_theory -> Proof.state
haftmann@61670
    21
haftmann@61669
    22
  val interpretation: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
haftmann@61669
    23
  val interpretation_cmd: Expression.expression -> (Attrib.binding * string) list ->
haftmann@61669
    24
    local_theory -> Proof.state
haftmann@61669
    25
  val sublocale: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
haftmann@61669
    26
  val sublocale_cmd: Expression.expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
haftmann@61669
    27
  val sublocale_global: string -> Expression.expression_i ->
haftmann@61669
    28
    (Attrib.binding * term) list -> theory -> Proof.state
haftmann@61669
    29
  val sublocale_global_cmd: xstring * Position.T -> Expression.expression ->
haftmann@61669
    30
    (Attrib.binding * string) list -> theory -> Proof.state
haftmann@61669
    31
end;
haftmann@61669
    32
haftmann@61669
    33
structure Interpretation : INTERPRETATION =
haftmann@61669
    34
struct
haftmann@61669
    35
haftmann@61669
    36
local
haftmann@61669
    37
haftmann@61670
    38
(** reading **)
haftmann@61670
    39
haftmann@61670
    40
(* without mixin definitions *)
haftmann@61669
    41
haftmann@61669
    42
fun prep_with_extended_syntax prep_prop deps ctxt props =
haftmann@61669
    43
  let
haftmann@61669
    44
    val deps_ctxt = fold Locale.activate_declarations deps ctxt;
haftmann@61669
    45
  in
haftmann@61669
    46
    map (prep_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
haftmann@61669
    47
      |> Variable.export_terms deps_ctxt ctxt
haftmann@61669
    48
  end;
haftmann@61669
    49
haftmann@61669
    50
fun prep_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt =
haftmann@61669
    51
  let
haftmann@61669
    52
    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
haftmann@61669
    53
    val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
haftmann@61669
    54
    val attrss = map (apsnd (map (prep_attr initial_ctxt)) o fst) raw_eqns;
haftmann@61669
    55
    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
haftmann@61669
    56
    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
haftmann@61669
    57
  in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
haftmann@61669
    58
haftmann@61669
    59
val cert_interpretation =
haftmann@61669
    60
  prep_interpretation Expression.cert_goal_expression (K I) (K I);
haftmann@61669
    61
haftmann@61669
    62
val read_interpretation =
haftmann@61669
    63
  prep_interpretation Expression.read_goal_expression Syntax.parse_prop Attrib.check_src;
haftmann@61669
    64
haftmann@61669
    65
haftmann@61670
    66
(* with mixin definitions *)
haftmann@61670
    67
haftmann@61670
    68
fun prep_interpretation_with_defs prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
haftmann@61670
    69
  let
haftmann@61670
    70
    (*reading*)
haftmann@61670
    71
    val ((propss, deps, export), expr_ctxt1) = prep_expr expression initial_ctxt;
haftmann@61670
    72
    val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt1;
haftmann@61670
    73
    val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
haftmann@61670
    74
    val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
haftmann@61670
    75
    val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
haftmann@61670
    76
haftmann@61670
    77
    (*defining*)
haftmann@61670
    78
    val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
haftmann@61670
    79
      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
haftmann@61670
    80
    val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt1;
haftmann@61670
    81
    val expr_ctxt2 = Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) expr_ctxt1;
haftmann@61670
    82
    val def_eqns = defs
haftmann@61670
    83
      |> map (Thm.symmetric o
haftmann@61670
    84
        Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt2) o snd o snd);
haftmann@61670
    85
haftmann@61670
    86
    (*setting up*)
haftmann@61670
    87
    val attrss = map (apsnd (map (prep_attr expr_ctxt2)) o fst) raw_eqns;
haftmann@61670
    88
    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt2;
haftmann@61670
    89
    val export' = Variable.export_morphism goal_ctxt expr_ctxt2;
haftmann@61670
    90
  in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
haftmann@61670
    91
haftmann@61670
    92
val cert_interpretation_with_defs =
haftmann@61670
    93
  prep_interpretation_with_defs Expression.cert_goal_expression (K I) (K I) (K I);
haftmann@61670
    94
haftmann@61670
    95
val read_interpretation_with_defs =
haftmann@61670
    96
  prep_interpretation_with_defs Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
haftmann@61670
    97
haftmann@61670
    98
haftmann@61670
    99
(** generic interpretation machinery **)
haftmann@61670
   100
haftmann@61670
   101
(* without mixin definitions *)
haftmann@61670
   102
haftmann@61670
   103
local
haftmann@61669
   104
haftmann@61669
   105
fun meta_rewrite ctxt eqns =
haftmann@61669
   106
  map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
haftmann@61669
   107
haftmann@61669
   108
fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
haftmann@61669
   109
  let
haftmann@61669
   110
    val facts = map2 (fn attrs => fn eqn =>
haftmann@61669
   111
      (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
haftmann@61669
   112
    val (eqns', ctxt') = ctxt
haftmann@61669
   113
      |> note Thm.theoremK facts
haftmann@61669
   114
      |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
haftmann@61669
   115
    val dep_morphs =
haftmann@61669
   116
      map2 (fn (dep, morph) => fn wits =>
haftmann@61669
   117
          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)))
haftmann@61669
   118
        deps witss;
haftmann@61669
   119
    fun activate' dep_morph ctxt =
haftmann@61669
   120
      activate dep_morph
haftmann@61669
   121
        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns'))
haftmann@61669
   122
        export ctxt;
haftmann@61669
   123
  in
haftmann@61669
   124
    ctxt'
haftmann@61669
   125
    |> fold activate' dep_morphs
haftmann@61669
   126
  end;
haftmann@61669
   127
haftmann@61670
   128
in
haftmann@61670
   129
haftmann@61669
   130
fun generic_interpretation prep_interpretation setup_proof note activate
haftmann@61669
   131
    expression raw_eqns initial_ctxt =
haftmann@61669
   132
  let
haftmann@61669
   133
    val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) =
haftmann@61669
   134
      prep_interpretation expression raw_eqns initial_ctxt;
haftmann@61669
   135
    fun after_qed witss eqns =
haftmann@61669
   136
      note_eqns_register note activate deps witss eqns attrss export export';
haftmann@61669
   137
  in setup_proof after_qed propss eqns goal_ctxt end;
haftmann@61669
   138
haftmann@61670
   139
end;
haftmann@61669
   140
haftmann@61670
   141
haftmann@61670
   142
(* without mixin definitions *)
haftmann@61670
   143
haftmann@61670
   144
local
haftmann@61670
   145
haftmann@61670
   146
fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
haftmann@61670
   147
haftmann@61670
   148
fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
haftmann@61670
   149
  let
haftmann@61670
   150
    val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
haftmann@61670
   151
      :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
haftmann@61670
   152
    val (eqns', ctxt') = ctxt
haftmann@61670
   153
      |> note Thm.theoremK facts
haftmann@61670
   154
      |-> meta_rewrite;
haftmann@61670
   155
    val dep_morphs = map2 (fn (dep, morph) => fn wits =>
haftmann@61670
   156
      (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
haftmann@61670
   157
    fun activate' dep_morph ctxt = activate dep_morph
haftmann@61670
   158
      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
haftmann@61670
   159
  in
haftmann@61670
   160
    ctxt'
haftmann@61670
   161
    |> fold activate' dep_morphs
haftmann@61670
   162
  end;
haftmann@61670
   163
haftmann@61670
   164
in
haftmann@61670
   165
haftmann@61670
   166
fun generic_interpretation_with_defs prep_interpretation setup_proof note add_registration
haftmann@61670
   167
    expression raw_defs raw_eqns initial_ctxt =
haftmann@61670
   168
  let
haftmann@61670
   169
    val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
haftmann@61670
   170
      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
haftmann@61670
   171
    fun after_qed witss eqns =
haftmann@61670
   172
      note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
haftmann@61670
   173
  in setup_proof after_qed propss eqns goal_ctxt end;
haftmann@61670
   174
haftmann@61670
   175
end;
haftmann@61670
   176
haftmann@61670
   177
haftmann@61670
   178
(** first dimension: proof vs. local theory **)
haftmann@61670
   179
haftmann@61670
   180
(* proof *)
haftmann@61669
   181
haftmann@61669
   182
fun gen_interpret prep_interpretation expression raw_eqns int state =
haftmann@61669
   183
  let
haftmann@61669
   184
    val _ = Proof.assert_forward_or_chain state;
haftmann@61669
   185
    val ctxt = Proof.context_of state;
haftmann@61669
   186
    fun lift_after_qed after_qed witss eqns =
haftmann@61669
   187
      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
haftmann@61669
   188
    fun setup_proof after_qed propss eqns goal_ctxt =
haftmann@61669
   189
      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
haftmann@61669
   190
        propss eqns goal_ctxt int state;
haftmann@61669
   191
  in
haftmann@61669
   192
    generic_interpretation prep_interpretation setup_proof
haftmann@61669
   193
      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
haftmann@61669
   194
  end;
haftmann@61669
   195
haftmann@61670
   196
haftmann@61670
   197
(* local theory *)
haftmann@61670
   198
haftmann@61669
   199
fun gen_local_theory_interpretation prep_interpretation activate expression raw_eqns lthy =
haftmann@61669
   200
  generic_interpretation prep_interpretation Element.witness_proof_eqs
haftmann@61669
   201
    Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy;
haftmann@61669
   202
haftmann@61669
   203
haftmann@61670
   204
(* local theory with mixin definitions *)
haftmann@61670
   205
haftmann@61670
   206
fun gen_interpretation_with_defs prep_interpretation expression raw_defs raw_eqns =
haftmann@61670
   207
  Local_Theory.assert_bottom true
haftmann@61670
   208
  #> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
haftmann@61670
   209
    Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
haftmann@61670
   210
haftmann@61670
   211
haftmann@61670
   212
(** second dimension: relation to underlying target **)
haftmann@61669
   213
haftmann@61669
   214
fun subscribe_or_activate lthy =
haftmann@61669
   215
  if Named_Target.is_theory lthy
haftmann@61669
   216
  then Local_Theory.subscription
haftmann@61669
   217
  else Locale.activate_fragment;
haftmann@61669
   218
haftmann@61669
   219
fun subscribe_locale_only lthy =
haftmann@61669
   220
  let
haftmann@61669
   221
    val _ =
haftmann@61669
   222
      if Named_Target.is_theory lthy
haftmann@61669
   223
      then error "Not possible on level of global theory"
haftmann@61669
   224
      else ();
haftmann@61669
   225
  in Local_Theory.subscription end;
haftmann@61669
   226
haftmann@61669
   227
haftmann@61670
   228
(** special case: global sublocale command **)
haftmann@61669
   229
haftmann@61669
   230
fun gen_sublocale_global prep_loc prep_interpretation
haftmann@61669
   231
    raw_locale expression raw_eqns thy =
haftmann@61669
   232
  let
haftmann@61669
   233
    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
haftmann@61669
   234
    fun setup_proof after_qed =
haftmann@61669
   235
      Element.witness_proof_eqs
haftmann@61669
   236
        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
haftmann@61669
   237
  in
haftmann@61669
   238
    lthy |>
haftmann@61669
   239
      generic_interpretation prep_interpretation setup_proof
haftmann@61669
   240
        Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns
haftmann@61669
   241
  end;
haftmann@61669
   242
haftmann@61669
   243
in
haftmann@61669
   244
haftmann@61669
   245
haftmann@61670
   246
(** interfaces **)
haftmann@61669
   247
haftmann@61669
   248
fun interpret x = gen_interpret cert_interpretation x;
haftmann@61669
   249
fun interpret_cmd x = gen_interpret read_interpretation x;
haftmann@61669
   250
haftmann@61669
   251
fun ephemeral_interpretation x =
haftmann@61669
   252
  gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
haftmann@61669
   253
haftmann@61670
   254
fun permanent_interpretation x = gen_interpretation_with_defs cert_interpretation_with_defs x;
haftmann@61670
   255
fun permanent_interpretation_cmd x = gen_interpretation_with_defs read_interpretation_with_defs x;
haftmann@61670
   256
haftmann@61669
   257
fun interpretation x =
haftmann@61669
   258
  gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
haftmann@61669
   259
fun interpretation_cmd x =
haftmann@61669
   260
  gen_local_theory_interpretation read_interpretation subscribe_or_activate x;
haftmann@61669
   261
haftmann@61669
   262
fun sublocale x =
haftmann@61669
   263
  gen_local_theory_interpretation cert_interpretation subscribe_locale_only x;
haftmann@61669
   264
fun sublocale_cmd x =
haftmann@61669
   265
  gen_local_theory_interpretation read_interpretation subscribe_locale_only x;
haftmann@61669
   266
haftmann@61669
   267
fun sublocale_global x = gen_sublocale_global (K I) cert_interpretation x;
haftmann@61669
   268
fun sublocale_global_cmd x = gen_sublocale_global Locale.check read_interpretation x;
haftmann@61669
   269
haftmann@61669
   270
end;
haftmann@61669
   271
haftmann@61669
   272
end;