src/Pure/Isar/interpretation.ML
author haftmann
Wed, 02 Dec 2015 19:14:55 +0100
changeset 61771 acc532690ee1
parent 61708 4de2380ae3ab
child 61772 2f33f6cc964d
permissions -rw-r--r--
tuned whitespace
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     1
(*  Title:      Pure/Isar/interpretation.ML
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     2
    Author:     Clemens Ballarin, TU Muenchen
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     4
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     5
Locale interpretation.
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     6
*)
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     7
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     8
signature INTERPRETATION =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     9
sig
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    10
  type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    11
  type 'a rewrites = (Attrib.binding * 'a) list
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    12
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    13
  (*interpretation in proofs*)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    14
  val interpret: Expression.expression_i -> term rewrites -> bool -> Proof.state -> Proof.state
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    15
  val interpret_cmd: Expression.expression -> string rewrites -> bool -> Proof.state -> Proof.state
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    16
61771
acc532690ee1 tuned whitespace
haftmann
parents: 61708
diff changeset
    17
  (*algebraic view*)
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    18
  val global_interpretation: Expression.expression_i ->
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    19
    term defines -> term rewrites -> theory -> Proof.state
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    20
  val global_sublocale: string -> Expression.expression_i ->
61676
872b2ee75359 tuned whitespace
haftmann
parents: 61673
diff changeset
    21
    term defines -> term rewrites -> theory -> Proof.state
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    22
  val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    23
    string defines -> string rewrites -> theory -> Proof.state
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    24
  val sublocale: Expression.expression_i ->
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    25
    term defines -> term rewrites -> local_theory -> Proof.state
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    26
  val sublocale_cmd: Expression.expression ->
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    27
    string defines -> string rewrites -> local_theory -> Proof.state
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    28
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    29
  (*local-theory-based view*)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    30
  val ephemeral_interpretation: Expression.expression_i ->
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    31
    term rewrites -> local_theory -> Proof.state
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    32
  val permanent_interpretation: Expression.expression_i ->
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    33
    term defines -> term rewrites -> local_theory -> Proof.state
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    34
  val permanent_interpretation_cmd: Expression.expression ->
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    35
    string defines -> string rewrites -> local_theory -> Proof.state
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    36
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    37
  (*mixed Isar interface*)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    38
  val interpretation: Expression.expression_i -> term rewrites -> local_theory -> Proof.state
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    39
  val interpretation_cmd: Expression.expression -> string rewrites ->
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    40
    local_theory -> Proof.state
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    41
end;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    42
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    43
structure Interpretation : INTERPRETATION =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    44
struct
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    45
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    46
(** common interpretation machinery **)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    47
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    48
type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    49
type 'a rewrites = (Attrib.binding * 'a) list
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    50
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    51
(* reading of locale expressions with rewrite morphisms *)
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    52
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
    53
local
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    54
61691
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    55
fun prep_mixins prep_term prep_prop expr_ctxt deps_ctxt raw_defs raw_eqns =
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    56
  let
61684
048ba34613bb formally correct context for export
haftmann
parents: 61676
diff changeset
    57
    val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt expr_ctxt;
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    58
    val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    59
    val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    60
      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
61691
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    61
    val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    62
  in (pre_defs, eqns) end;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    63
61691
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    64
fun define_mixins [] expr_ctxt = ([], expr_ctxt)
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    65
      (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    66
  | define_mixins pre_defs expr_lthy =
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    67
      let
61708
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    68
        val ((_, defs), inner_def_lthy) =
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    69
          expr_lthy
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    70
          |> Local_Theory.open_target
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    71
          ||>> fold_map Local_Theory.define pre_defs
61691
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    72
        val def_lthy =
61708
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    73
          inner_def_lthy
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    74
          |> Local_Theory.close_target;
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    75
        val def_eqns =
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    76
          defs
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    77
          |> map (Thm.symmetric o snd o snd)
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    78
          |> Proof_Context.export inner_def_lthy def_lthy;
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    79
      in (def_eqns, Proof_Context.transfer (Proof_Context.theory_of def_lthy) expr_lthy) end;
61691
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    80
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    81
fun prep_interpretation prep_expr prep_term prep_prop prep_attr
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    82
  expression raw_defs raw_eqns initial_ctxt =
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    83
  let
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    84
    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    85
    val (pre_defs, eqns) =
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    86
      prep_mixins prep_term prep_prop expr_ctxt
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    87
        (fold Locale.activate_declarations deps expr_ctxt) raw_defs raw_eqns;
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    88
    val (def_eqns, def_ctxt) = define_mixins pre_defs expr_ctxt;
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
    89
    val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns;
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
    90
    val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
    91
    val export' = Variable.export_morphism goal_ctxt def_ctxt;
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
    92
  in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    93
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    94
in
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    95
61698
c4a6edbfec49 make SML/NJ happy;
wenzelm
parents: 61691
diff changeset
    96
fun cert_interpretation expression =
c4a6edbfec49 make SML/NJ happy;
wenzelm
parents: 61691
diff changeset
    97
  prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I) expression;
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
    98
61698
c4a6edbfec49 make SML/NJ happy;
wenzelm
parents: 61691
diff changeset
    99
fun read_interpretation expression =
c4a6edbfec49 make SML/NJ happy;
wenzelm
parents: 61691
diff changeset
   100
  prep_interpretation Expression.read_goal_expression Syntax.parse_term
c4a6edbfec49 make SML/NJ happy;
wenzelm
parents: 61691
diff changeset
   101
    Syntax.parse_prop Attrib.check_src expression;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   102
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   103
end;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   104
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   105
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   106
(* interpretation machinery *)
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   107
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   108
local
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   109
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   110
fun meta_rewrite eqns ctxt =
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   111
  (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   112
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   113
fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   114
  let
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   115
    val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   116
      :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   117
    val (eqns', ctxt') = ctxt
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   118
      |> note Thm.theoremK facts
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   119
      |-> meta_rewrite;
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   120
    val dep_morphs = map2 (fn (dep, morph) => fn wits =>
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   121
      (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   122
    fun activate' dep_morph ctxt = activate dep_morph
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   123
      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   124
  in
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   125
    ctxt'
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   126
    |> fold activate' dep_morphs
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   127
  end;
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   128
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   129
in
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   130
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   131
fun generic_interpretation_with_defs prep_interpretation setup_proof note add_registration
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   132
    expression raw_defs raw_eqns initial_ctxt =
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   133
  let
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   134
    val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   135
      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   136
    fun after_qed witss eqns =
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   137
      note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   138
  in setup_proof after_qed propss eqns goal_ctxt end;
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   139
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   140
fun generic_interpretation prep_interpretation setup_proof note add_registration expression =
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   141
  generic_interpretation_with_defs prep_interpretation setup_proof note add_registration expression [];
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   142
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   143
end;
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   144
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   145
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   146
(** interfaces **)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   147
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   148
(* interpretation in proofs *)
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   149
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   150
local
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   151
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   152
fun gen_interpret prep_interpretation expression raw_eqns int state =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   153
  let
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   154
    val _ = Proof.assert_forward_or_chain state;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   155
    val ctxt = Proof.context_of state;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   156
    fun lift_after_qed after_qed witss eqns =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   157
      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   158
    fun setup_proof after_qed propss eqns goal_ctxt =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   159
      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   160
        propss eqns goal_ctxt int state;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   161
  in
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   162
    generic_interpretation prep_interpretation setup_proof
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   163
      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   164
  end;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   165
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   166
in
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   167
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   168
fun interpret expression = gen_interpret cert_interpretation expression;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   169
fun interpret_cmd raw_expression = gen_interpret read_interpretation raw_expression;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   170
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   171
end;
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   172
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   173
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   174
(* algebraic-view *)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   175
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   176
local
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   177
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   178
fun gen_global_interpretation prep_interpretation expression
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   179
    raw_defs raw_eqns thy = 
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   180
  let
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   181
    val lthy = Named_Target.theory_init thy;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   182
    fun setup_proof after_qed =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   183
      Element.witness_proof_eqs
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   184
        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   185
  in
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   186
    lthy |>
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   187
      generic_interpretation_with_defs prep_interpretation setup_proof
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   188
        Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   189
  end;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   190
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   191
fun gen_global_sublocale prep_loc prep_interpretation
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   192
    raw_locale expression raw_defs raw_eqns thy =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   193
  let
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   194
    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   195
    fun setup_proof after_qed =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   196
      Element.witness_proof_eqs
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   197
        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   198
  in
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   199
    lthy |>
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   200
      generic_interpretation_with_defs prep_interpretation setup_proof
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   201
        Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   202
  end;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   203
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   204
fun subscribe_locale_only lthy =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   205
  let
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   206
    val _ =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   207
      if Named_Target.is_theory lthy
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   208
      then error "Not possible on level of global theory"
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   209
      else ();
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   210
  in Local_Theory.subscription end;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   211
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   212
fun gen_sublocale prep_interpretation expression raw_defs raw_eqns lthy =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   213
  generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   214
    Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_defs raw_eqns lthy;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   215
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   216
in
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   217
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   218
fun global_interpretation expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   219
  gen_global_interpretation cert_interpretation expression;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   220
fun global_sublocale expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   221
  gen_global_sublocale (K I) cert_interpretation expression;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   222
fun global_sublocale_cmd raw_expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   223
  gen_global_sublocale Locale.check read_interpretation raw_expression;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   224
fun sublocale expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   225
  gen_sublocale cert_interpretation expression;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   226
fun sublocale_cmd raw_expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   227
  gen_sublocale read_interpretation raw_expression;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   228
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   229
end;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   230
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   231
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   232
(* local-theory-based view *)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   233
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   234
local
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   235
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   236
fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   237
  Local_Theory.assert_bottom true
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   238
  #> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   239
    Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   240
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   241
in
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   242
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   243
fun ephemeral_interpretation expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   244
  generic_interpretation cert_interpretation Element.witness_proof_eqs
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   245
    Local_Theory.notes_kind Locale.activate_fragment expression;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   246
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   247
fun permanent_interpretation expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   248
  gen_permanent_interpretation cert_interpretation expression;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   249
fun permanent_interpretation_cmd raw_expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   250
  gen_permanent_interpretation read_interpretation raw_expression;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   251
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   252
end;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   253
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   254
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   255
(* mixed Isar interface *)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   256
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   257
local
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   258
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   259
fun subscribe_or_activate lthy =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   260
  if Named_Target.is_theory lthy
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   261
  then Local_Theory.subscription
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   262
  else Locale.activate_fragment;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   263
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   264
fun gen_local_theory_interpretation prep_interpretation expression raw_eqns lthy =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   265
  generic_interpretation prep_interpretation Element.witness_proof_eqs
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   266
    Local_Theory.notes_kind (subscribe_or_activate lthy) expression raw_eqns lthy;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   267
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   268
in
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   269
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   270
fun interpretation expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   271
  gen_local_theory_interpretation cert_interpretation expression;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   272
fun interpretation_cmd raw_expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   273
  gen_local_theory_interpretation read_interpretation raw_expression;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   274
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   275
end;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   276
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   277
end;