src/Pure/Isar/interpretation.ML
author ballarin
Fri, 02 Mar 2018 14:19:25 +0100
changeset 67740 b6ce18784872
parent 67702 2d9918f5b33c
child 67777 2d3c1091527b
permissions -rw-r--r--
Proper rewrite morphisms in locale instances.
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*)
62680
646b84666a56 eliminated unused argument (see also 58110c1e02bc);
wenzelm
parents: 61890
diff changeset
    14
  val interpret: Expression.expression_i -> term rewrites -> Proof.state -> Proof.state
646b84666a56 eliminated unused argument (see also 58110c1e02bc);
wenzelm
parents: 61890
diff changeset
    15
  val interpret_cmd: Expression.expression -> string rewrites -> Proof.state -> Proof.state
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    16
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    17
  (*interpretation in local theories*)
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    18
  val interpretation: Expression.expression_i ->
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    19
    term rewrites -> local_theory -> Proof.state
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    20
  val interpretation_cmd: Expression.expression ->
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    21
    string rewrites -> local_theory -> Proof.state
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    22
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    23
  (*interpretation into global theories*)
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    24
  val global_interpretation: Expression.expression_i ->
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    25
    term defines -> term rewrites -> local_theory -> Proof.state
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    26
  val global_interpretation_cmd: Expression.expression ->
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    27
    string defines -> string rewrites -> local_theory -> Proof.state
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    28
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    29
  (*interpretation between locales*)
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    30
  val sublocale: Expression.expression_i ->
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    31
    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
    32
  val sublocale_cmd: Expression.expression ->
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    33
    string defines -> string rewrites -> local_theory -> Proof.state
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    34
  val global_sublocale: string -> Expression.expression_i ->
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    35
    term defines -> term rewrites -> theory -> Proof.state
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    36
  val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    37
    string defines -> string rewrites -> theory -> Proof.state
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    38
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    39
  (*mixed Isar interface*)
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    40
  val isar_interpretation: Expression.expression_i ->
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    41
    term rewrites -> local_theory -> Proof.state
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    42
  val isar_interpretation_cmd: Expression.expression ->
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    43
    string rewrites -> local_theory -> Proof.state
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    44
end;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    45
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    46
structure Interpretation : INTERPRETATION =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    47
struct
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    48
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    49
(** common interpretation machinery **)
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
type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
67740
b6ce18784872 Proper rewrite morphisms in locale instances.
ballarin
parents: 67702
diff changeset
    52
type 'a rewrites = 'a Expression.rewrites
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    53
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    54
(* reading of locale expressions with rewrite morphisms *)
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    55
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
    56
local
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    57
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
    58
fun augment_with_def prep_term ((name, atts), ((b, mx), raw_rhs)) lthy =
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    59
  let
61775
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    60
    val rhs = prep_term lthy raw_rhs;
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    61
    val lthy' = Variable.declare_term rhs lthy;
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    62
    val ((_, (_, def)), lthy'') =
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    63
      Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy';
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    64
  in (def, lthy'') end;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    65
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
    66
fun augment_with_defs _ [] _ ctxt = ([], ctxt)
61691
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    67
      (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
61775
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    68
  | augment_with_defs prep_term raw_defs deps lthy =
61691
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    69
      let
61775
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    70
        val (_, inner_lthy) =
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    71
          Local_Theory.open_target lthy
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    72
          ||> fold Locale.activate_declarations deps;
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    73
        val (inner_defs, inner_lthy') =
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
    74
          fold_map (augment_with_def prep_term) raw_defs inner_lthy;
61775
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    75
        val lthy' =
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    76
          inner_lthy'
61708
4de2380ae3ab explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents: 61698
diff changeset
    77
          |> 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
    78
        val def_eqns =
61775
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    79
          map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    80
      in (def_eqns, lthy') end;
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    81
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
    82
fun prep_eqns _ _ [] _ _ = ([], [])
61775
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    83
  | prep_eqns prep_props prep_attr raw_eqns deps ctxt =
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    84
      let
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
    85
        (* FIXME incompatibility, creating context for parsing rewrites equation may fail in
67740
b6ce18784872 Proper rewrite morphisms in locale instances.
ballarin
parents: 67702
diff changeset
    86
           presence of rewrites clause in expression *)
61775
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    87
        val ctxt' = fold Locale.activate_declarations deps ctxt;
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    88
        val eqns =
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    89
          (Variable.export_terms ctxt' ctxt o prep_props ctxt' o map snd) raw_eqns;
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    90
        val attrss = map (apsnd (map (prep_attr ctxt)) o fst) raw_eqns;
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    91
      in (eqns, attrss) end;
61691
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    92
61774
029162bc9793 prefer conventional read/check distinction over manual check
haftmann
parents: 61773
diff changeset
    93
fun prep_interpretation prep_expr prep_term prep_props prep_attr
61691
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    94
  expression raw_defs raw_eqns initial_ctxt =
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    95
  let
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
    96
    val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt;
61775
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    97
    val (def_eqns, def_ctxt) =
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    98
      augment_with_defs prep_term raw_defs deps expr_ctxt;
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    99
    val (eqns, attrss) = prep_eqns prep_props prep_attr raw_eqns deps def_ctxt;
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   100
    val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
61772
2f33f6cc964d formally correct context for export, which got screwed up in 87203a0f0041
haftmann
parents: 61771
diff changeset
   101
    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   102
  in (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   103
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   104
in
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   105
61698
c4a6edbfec49 make SML/NJ happy;
wenzelm
parents: 61691
diff changeset
   106
fun cert_interpretation expression =
61774
029162bc9793 prefer conventional read/check distinction over manual check
haftmann
parents: 61773
diff changeset
   107
  prep_interpretation Expression.cert_goal_expression Syntax.check_term
029162bc9793 prefer conventional read/check distinction over manual check
haftmann
parents: 61773
diff changeset
   108
    Syntax.check_props (K I) expression;
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   109
61698
c4a6edbfec49 make SML/NJ happy;
wenzelm
parents: 61691
diff changeset
   110
fun read_interpretation expression =
61774
029162bc9793 prefer conventional read/check distinction over manual check
haftmann
parents: 61773
diff changeset
   111
  prep_interpretation Expression.read_goal_expression Syntax.read_term
029162bc9793 prefer conventional read/check distinction over manual check
haftmann
parents: 61773
diff changeset
   112
    Syntax.read_props Attrib.check_src expression;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   113
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   114
end;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   115
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   116
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   117
(* interpretation machinery *)
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   118
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   119
local
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   120
63381
823660593928 tuned whitespace;
wenzelm
parents: 63380
diff changeset
   121
fun meta_rewrite eqns ctxt =
823660593928 tuned whitespace;
wenzelm
parents: 63380
diff changeset
   122
  (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   123
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   124
fun note_eqns_register pos note activate deps eqnss witss def_eqns thms attrss export export' ctxt =
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   125
  let
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   126
    val (thmss, thms') = split_last (unflat ((map o map) fst eqnss @ [attrss]) thms);
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   127
    val factss =
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   128
      map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) fst eqnss) thmss;
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   129
    val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt;
63381
823660593928 tuned whitespace;
wenzelm
parents: 63380
diff changeset
   130
    val facts =
823660593928 tuned whitespace;
wenzelm
parents: 63380
diff changeset
   131
      (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) ::
823660593928 tuned whitespace;
wenzelm
parents: 63380
diff changeset
   132
        map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])]))
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   133
          attrss thms';
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   134
    val (eqns', ctxt'') = ctxt'
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   135
      |> note Thm.theoremK facts
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   136
      |-> meta_rewrite;
63381
823660593928 tuned whitespace;
wenzelm
parents: 63380
diff changeset
   137
    val dep_morphs =
823660593928 tuned whitespace;
wenzelm
parents: 63380
diff changeset
   138
      map2 (fn (dep, morph) => fn wits =>
63382
4270da306442 clarified positions, e.g. for reports on literal facts;
wenzelm
parents: 63381
diff changeset
   139
        let val morph' = morph
4270da306442 clarified positions, e.g. for reports on literal facts;
wenzelm
parents: 63381
diff changeset
   140
          $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
4270da306442 clarified positions, e.g. for reports on literal facts;
wenzelm
parents: 63381
diff changeset
   141
          $> Morphism.binding_morphism "position" (Binding.set_pos pos)
4270da306442 clarified positions, e.g. for reports on literal facts;
wenzelm
parents: 63381
diff changeset
   142
        in (dep, morph') end) deps witss;
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   143
    fun activate' (dep_morph, eqns) ctxt =
63381
823660593928 tuned whitespace;
wenzelm
parents: 63380
diff changeset
   144
      activate dep_morph
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   145
        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')))
63381
823660593928 tuned whitespace;
wenzelm
parents: 63380
diff changeset
   146
        export ctxt;
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   147
  in ctxt'' |> fold activate' (dep_morphs ~~ eqnss') end;
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   148
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   149
in
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   150
63380
wenzelm
parents: 63379
diff changeset
   151
fun generic_interpretation prep_interpretation setup_proof note add_registration
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   152
    expression raw_defs raw_eqns initial_ctxt =
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   153
  let
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   154
    val (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   155
      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
63382
4270da306442 clarified positions, e.g. for reports on literal facts;
wenzelm
parents: 63381
diff changeset
   156
    val pos = Position.thread_data ();
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   157
    fun after_qed witss eqns =
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   158
      note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns attrss export export';
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
   159
  in setup_proof after_qed propss (flat (eq_propss @ [eqns])) goal_ctxt end;
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   160
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   161
end;
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   162
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   163
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   164
(** interfaces **)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   165
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   166
(* interpretation in proofs *)
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   167
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   168
local
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   169
62680
646b84666a56 eliminated unused argument (see also 58110c1e02bc);
wenzelm
parents: 61890
diff changeset
   170
fun gen_interpret prep_interpretation expression raw_eqns state =
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   171
  let
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   172
    val _ = Proof.assert_forward_or_chain state;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   173
    fun lift_after_qed after_qed witss eqns =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   174
      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   175
    fun setup_proof after_qed propss eqns goal_ctxt =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   176
      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
62680
646b84666a56 eliminated unused argument (see also 58110c1e02bc);
wenzelm
parents: 61890
diff changeset
   177
        propss eqns goal_ctxt state;
67702
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67450
diff changeset
   178
    fun add_registration reg mixin export ctxt = ctxt
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67450
diff changeset
   179
      |> Proof_Context.set_stmt false
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67450
diff changeset
   180
      |> Context.proof_map (Locale.add_registration reg mixin export)
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67450
diff changeset
   181
      |> Proof_Context.restore_stmt ctxt;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   182
  in
63379
wenzelm
parents: 63352
diff changeset
   183
    Proof.context_of state
wenzelm
parents: 63352
diff changeset
   184
    |> generic_interpretation prep_interpretation setup_proof
67702
2d9918f5b33c command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents: 67450
diff changeset
   185
      Attrib.local_notes add_registration expression [] raw_eqns
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   186
  end;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   187
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   188
in
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   189
63379
wenzelm
parents: 63352
diff changeset
   190
val interpret = gen_interpret cert_interpretation;
wenzelm
parents: 63352
diff changeset
   191
val interpret_cmd = gen_interpret read_interpretation;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   192
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   193
end;
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   194
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   195
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   196
(* interpretation in local theories *)
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   197
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   198
fun interpretation expression =
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   199
  generic_interpretation cert_interpretation Element.witness_proof_eqs
63380
wenzelm
parents: 63379
diff changeset
   200
    Local_Theory.notes_kind Locale.activate_fragment expression [];
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   201
63380
wenzelm
parents: 63379
diff changeset
   202
fun interpretation_cmd expression =
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   203
  generic_interpretation read_interpretation Element.witness_proof_eqs
63380
wenzelm
parents: 63379
diff changeset
   204
    Local_Theory.notes_kind Locale.activate_fragment expression [];
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   205
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   206
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   207
(* interpretation into global theories *)
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   208
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   209
fun global_interpretation expression =
63380
wenzelm
parents: 63379
diff changeset
   210
  generic_interpretation cert_interpretation Element.witness_proof_eqs
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   211
    Local_Theory.notes_kind Local_Theory.theory_registration expression;
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   212
63380
wenzelm
parents: 63379
diff changeset
   213
fun global_interpretation_cmd expression =
wenzelm
parents: 63379
diff changeset
   214
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm
parents: 63379
diff changeset
   215
    Local_Theory.notes_kind Local_Theory.theory_registration expression;
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   216
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   217
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   218
(* interpretation between locales *)
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   219
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   220
fun sublocale expression =
63380
wenzelm
parents: 63379
diff changeset
   221
  generic_interpretation cert_interpretation Element.witness_proof_eqs
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   222
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   223
63380
wenzelm
parents: 63379
diff changeset
   224
fun sublocale_cmd expression =
wenzelm
parents: 63379
diff changeset
   225
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm
parents: 63379
diff changeset
   226
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   227
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   228
local
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   229
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   230
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
   231
    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
   232
  let
66334
b210ae666a42 provide explicit variant initializers for regular named target vs. almost-named target
haftmann
parents: 63402
diff changeset
   233
    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   234
    fun setup_proof after_qed =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   235
      Element.witness_proof_eqs
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   236
        (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
   237
  in
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   238
    lthy |>
63380
wenzelm
parents: 63379
diff changeset
   239
      generic_interpretation prep_interpretation setup_proof
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   240
        Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs raw_eqns
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   241
  end;
61669
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
in
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   244
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   245
fun global_sublocale expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   246
  gen_global_sublocale (K I) cert_interpretation expression;
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   247
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   248
fun global_sublocale_cmd raw_expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   249
  gen_global_sublocale Locale.check read_interpretation raw_expression;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   250
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   251
end;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   252
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
(* mixed Isar interface *)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   255
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   256
local
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   257
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   258
fun register_or_activate lthy =
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   259
  if Named_Target.is_theory lthy
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   260
  then Local_Theory.theory_registration
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   261
  else Locale.activate_fragment;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   262
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   263
fun gen_isar_interpretation prep_interpretation expression raw_eqns lthy =
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   264
  generic_interpretation prep_interpretation Element.witness_proof_eqs
63380
wenzelm
parents: 63379
diff changeset
   265
    Local_Theory.notes_kind (register_or_activate lthy) expression [] raw_eqns lthy;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   266
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   267
in
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   268
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   269
fun isar_interpretation expression =
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   270
  gen_isar_interpretation cert_interpretation expression;
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   271
fun isar_interpretation_cmd raw_expression =
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   272
  gen_isar_interpretation read_interpretation raw_expression;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   273
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   274
end;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   275
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   276
end;