src/Pure/Isar/theory_target.ML
author wenzelm
Sun Nov 26 18:07:31 2006 +0100 (2006-11-26)
changeset 21533 bada5ac1216a
parent 21498 6382c3a1e7cf
child 21570 f20f9304ab48
permissions -rw-r--r--
simplified consts: no auxiliary params, sane mixfix syntax;
declarations: proper morphisms;
added target_morphism/name;
wenzelm@20894
     1
(*  Title:      Pure/Isar/theory_target.ML
wenzelm@20894
     2
    ID:         $Id$
wenzelm@20894
     3
    Author:     Makarius
wenzelm@20894
     4
wenzelm@20894
     5
Common theory targets.
wenzelm@20894
     6
*)
wenzelm@20894
     7
wenzelm@20894
     8
signature THEORY_TARGET =
wenzelm@20894
     9
sig
wenzelm@21006
    10
  val peek: local_theory -> string option
wenzelm@20962
    11
  val begin: bstring -> Proof.context -> local_theory
wenzelm@20894
    12
  val init: xstring option -> theory -> local_theory
wenzelm@20894
    13
  val init_i: string option -> theory -> local_theory
wenzelm@20894
    14
end;
wenzelm@20894
    15
wenzelm@20894
    16
structure TheoryTarget: THEORY_TARGET =
wenzelm@20894
    17
struct
wenzelm@20894
    18
wenzelm@20894
    19
(** locale targets **)
wenzelm@20894
    20
wenzelm@21006
    21
(* context data *)
wenzelm@21006
    22
wenzelm@21006
    23
structure Data = ProofDataFun
wenzelm@21006
    24
(
wenzelm@21006
    25
  val name = "Isar/theory_target";
wenzelm@21006
    26
  type T = string option;
wenzelm@21006
    27
  fun init _ = NONE;
wenzelm@21006
    28
  fun print _ _ = ();
wenzelm@21006
    29
);
wenzelm@21006
    30
wenzelm@21006
    31
val _ = Context.add_setup Data.init;
wenzelm@21006
    32
val peek = Data.get;
wenzelm@21006
    33
wenzelm@21006
    34
wenzelm@20894
    35
(* pretty *)
wenzelm@20894
    36
wenzelm@20894
    37
fun pretty loc ctxt =
wenzelm@20894
    38
  let
wenzelm@20894
    39
    val thy = ProofContext.theory_of ctxt;
wenzelm@20894
    40
    val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
wenzelm@20894
    41
    val assumes = map (fn A => (("", []), [(A, [])])) (Assumption.assms_of ctxt);
wenzelm@20894
    42
    val elems =
wenzelm@20894
    43
      (if null fixes then [] else [Element.Fixes fixes]) @
wenzelm@20894
    44
      (if null assumes then [] else [Element.Assumes assumes]);
wenzelm@20894
    45
  in
wenzelm@20984
    46
    if loc = "" then
wenzelm@20984
    47
      [Pretty.block
wenzelm@20984
    48
        [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
wenzelm@20984
    49
          Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]]
wenzelm@20984
    50
    else if null elems then [Pretty.str ("locale " ^ Locale.extern thy loc)]
wenzelm@20984
    51
    else
wenzelm@20984
    52
      [Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =")
wenzelm@20984
    53
        (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
wenzelm@20894
    54
  end;
wenzelm@20894
    55
wenzelm@20894
    56
wenzelm@20894
    57
(* consts *)
wenzelm@20894
    58
wenzelm@20894
    59
fun consts loc depends decls lthy =
wenzelm@20894
    60
  let
wenzelm@21533
    61
    val is_loc = loc <> "";
wenzelm@21533
    62
    val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
wenzelm@20894
    63
wenzelm@20894
    64
    fun const ((c, T), mx) thy =
wenzelm@20894
    65
      let
wenzelm@20894
    66
        val U = map #2 xs ---> T;
wenzelm@21533
    67
        val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
wenzelm@21533
    68
        val thy' = Sign.add_consts_authentic [(c, U, Syntax.unlocalize_mixfix is_loc mx)] thy;
wenzelm@21533
    69
      in (((c, mx), t), thy') end;
wenzelm@20894
    70
wenzelm@21533
    71
    val (abbrs, lthy') = lthy |> LocalTheory.theory_result (fold_map const decls);
wenzelm@21533
    72
    val defs = abbrs |> map (fn (x, t) => (x, (("", []), t)));
wenzelm@20894
    73
  in
wenzelm@20894
    74
    lthy'
wenzelm@21533
    75
    |> K is_loc ? LocalTheory.abbrevs Syntax.default_mode abbrs
wenzelm@21533
    76
    |> LocalDefs.add_defs defs |>> map (apsnd snd)
wenzelm@20894
    77
  end;
wenzelm@20894
    78
wenzelm@20894
    79
wenzelm@20894
    80
(* axioms *)
wenzelm@20894
    81
wenzelm@20894
    82
local
wenzelm@20894
    83
wenzelm@20894
    84
fun add_axiom hyps (name, prop) thy =
wenzelm@20894
    85
  let
wenzelm@20894
    86
    val name' = if name = "" then "axiom_" ^ serial_string () else name;
wenzelm@20894
    87
    val prop' = Logic.list_implies (hyps, prop);
wenzelm@20894
    88
    val thy' = thy |> Theory.add_axioms_i [(name', prop')];
wenzelm@20894
    89
    val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
wenzelm@20894
    90
    val prems = map (Thm.assume o Thm.cterm_of thy') hyps;
wenzelm@20894
    91
  in (Drule.implies_elim_list axm prems, thy') end;
wenzelm@20894
    92
wenzelm@20894
    93
in
wenzelm@20894
    94
wenzelm@21433
    95
fun axioms kind specs lthy =
wenzelm@20915
    96
  let
wenzelm@20915
    97
    val hyps = Assumption.assms_of lthy;
wenzelm@20915
    98
    fun axiom ((name, atts), props) thy = thy
wenzelm@20915
    99
      |> fold_map (add_axiom hyps) (PureThy.name_multi name props)
wenzelm@20915
   100
      |-> (fn ths => pair ((name, atts), [(ths, [])]));
wenzelm@20915
   101
  in
wenzelm@20915
   102
    lthy
wenzelm@20984
   103
    |> fold (fold Variable.declare_term o snd) specs
wenzelm@20915
   104
    |> LocalTheory.theory_result (fold_map axiom specs)
wenzelm@21433
   105
    |-> LocalTheory.notes kind
wenzelm@20915
   106
  end;
wenzelm@20894
   107
wenzelm@20894
   108
end;
wenzelm@20894
   109
wenzelm@20894
   110
wenzelm@20894
   111
(* defs *)
wenzelm@20894
   112
wenzelm@20894
   113
local
wenzelm@20894
   114
wenzelm@20894
   115
fun add_def (name, prop) =
wenzelm@20894
   116
  Theory.add_defs_i false false [(name, prop)] #>
wenzelm@20894
   117
  (fn thy => (Drule.unvarify (Thm.get_axiom_i thy (Sign.full_name thy name)), thy));
wenzelm@20894
   118
wenzelm@20894
   119
fun expand_defs lthy =
wenzelm@20894
   120
  Drule.term_rule (ProofContext.theory_of lthy)
wenzelm@20894
   121
    (Assumption.export false lthy (LocalTheory.target_of lthy));
wenzelm@20894
   122
wenzelm@21533
   123
infix also;
wenzelm@21533
   124
fun eq1 also eq2 = Thm.transitive eq1 eq2;
wenzelm@21533
   125
wenzelm@20894
   126
in
wenzelm@20894
   127
wenzelm@21433
   128
fun defs kind args lthy =
wenzelm@20894
   129
  let
wenzelm@21533
   130
    fun def ((c, mx), ((name, atts), rhs)) lthy1 =
wenzelm@20894
   131
      let
wenzelm@21533
   132
        val name' = Thm.def_name_optional c name;
wenzelm@20894
   133
        val T = Term.fastype_of rhs;
wenzelm@21533
   134
wenzelm@20894
   135
        val rhs' = expand_defs lthy1 rhs;
wenzelm@20894
   136
        val depends = member (op =) (Term.add_frees rhs' []);
wenzelm@20894
   137
        val defined = filter_out depends (Term.add_frees rhs []);
wenzelm@20894
   138
wenzelm@21533
   139
        val ([(lhs, local_def)], lthy2) = lthy1
wenzelm@21533
   140
          |> LocalTheory.consts depends [((c, T), mx)];
wenzelm@21533
   141
        val lhs' = #2 (Logic.dest_equals (Thm.prop_of local_def));
wenzelm@21533
   142
wenzelm@20894
   143
        val rhs_conv = rhs
wenzelm@20894
   144
          |> Thm.cterm_of (ProofContext.theory_of lthy1)
wenzelm@20894
   145
          |> Tactic.rewrite true (map_filter (LocalDefs.find_def lthy1 o #1) defined);
wenzelm@20894
   146
wenzelm@20894
   147
        val (global_def, lthy3) = lthy2
wenzelm@20894
   148
          |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs')));
wenzelm@20894
   149
wenzelm@21533
   150
        val eq =
wenzelm@21533
   151
          local_def                      (*c == loc.c xs*)
wenzelm@21533
   152
          also global_def                (*... == rhs'*)
wenzelm@21533
   153
          also Thm.symmetric rhs_conv;   (*... == rhs*)
wenzelm@20894
   154
      in ((lhs, ((name', atts), [([eq], [])])), lthy3) end;
wenzelm@20894
   155
wenzelm@20894
   156
    val ((lhss, facts), lthy') = lthy |> fold_map def args |>> split_list;
wenzelm@21433
   157
    val (res, lthy'') = lthy' |> LocalTheory.notes kind facts;
wenzelm@20894
   158
  in (lhss ~~ map (apsnd the_single) res, lthy'') end;
wenzelm@20894
   159
wenzelm@20894
   160
end;
wenzelm@20894
   161
wenzelm@20894
   162
wenzelm@20894
   163
(* notes *)
wenzelm@20894
   164
wenzelm@21433
   165
fun context_notes kind facts lthy =
wenzelm@20894
   166
  let
wenzelm@20894
   167
    val facts' = facts
wenzelm@20894
   168
      |> Element.export_standard_facts lthy lthy
wenzelm@20894
   169
      |> Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of lthy));
wenzelm@20894
   170
  in
wenzelm@20894
   171
    lthy
wenzelm@21433
   172
    |> ProofContext.set_stmt true
wenzelm@20894
   173
    |> ProofContext.qualified_names
wenzelm@21433
   174
    |> ProofContext.note_thmss_i kind facts'
wenzelm@20894
   175
    ||> ProofContext.restore_naming lthy
wenzelm@21433
   176
    ||> ProofContext.restore_stmt lthy
wenzelm@20894
   177
  end;
wenzelm@20894
   178
wenzelm@21433
   179
fun theory_notes keep_atts kind facts lthy = lthy |> LocalTheory.theory (fn thy =>
wenzelm@20894
   180
  let
wenzelm@20894
   181
    val facts' = facts
wenzelm@20894
   182
      |> Element.export_standard_facts lthy (ProofContext.init thy)
wenzelm@20915
   183
      |> Attrib.map_facts (if keep_atts then Attrib.attribute_i thy else K I);
wenzelm@20894
   184
  in
wenzelm@20894
   185
    thy
wenzelm@20894
   186
    |> Sign.qualified_names
wenzelm@21433
   187
    |> PureThy.note_thmss_i kind facts' |> #2
wenzelm@20894
   188
    |> Sign.restore_naming thy
wenzelm@20894
   189
  end);
wenzelm@20894
   190
wenzelm@21433
   191
fun locale_notes loc kind facts lthy = lthy |> LocalTheory.target (fn ctxt =>
wenzelm@21433
   192
  #2 (Locale.add_thmss loc kind (Element.export_standard_facts lthy ctxt facts) ctxt));
wenzelm@20894
   193
wenzelm@21433
   194
fun notes "" kind facts = theory_notes true kind facts #> context_notes kind facts
wenzelm@21433
   195
  | notes loc kind facts = theory_notes false kind facts #>
wenzelm@21433
   196
      locale_notes loc kind facts #> context_notes kind facts;
wenzelm@20894
   197
wenzelm@20894
   198
wenzelm@21533
   199
(* target declarations *)
wenzelm@20894
   200
wenzelm@21533
   201
fun decl _ "" f =
wenzelm@21533
   202
      LocalTheory.theory (Context.theory_map (f Morphism.identity)) #>
wenzelm@21533
   203
      LocalTheory.target (Context.proof_map (f Morphism.identity))
wenzelm@21533
   204
  | decl add loc f =
wenzelm@21533
   205
      LocalTheory.target (add loc (Context.proof_map o f));
wenzelm@20894
   206
wenzelm@21498
   207
val type_syntax = decl Locale.add_type_syntax;
wenzelm@21498
   208
val term_syntax = decl Locale.add_term_syntax;
wenzelm@21498
   209
val declaration = decl Locale.add_declaration;
wenzelm@20894
   210
wenzelm@21533
   211
fun target_morphism loc lthy =
wenzelm@21533
   212
  ProofContext.export_standard_morphism lthy (LocalTheory.target_of lthy) $>
wenzelm@21533
   213
  Morphism.name_morphism (NameSpace.qualified loc);
wenzelm@21533
   214
wenzelm@21533
   215
fun target_name "" lthy = Sign.full_name (ProofContext.theory_of lthy)
wenzelm@21533
   216
  | target_name _ lthy = ProofContext.full_name (LocalTheory.target_of lthy);
wenzelm@21533
   217
wenzelm@20894
   218
wenzelm@20894
   219
(* init and exit *)
wenzelm@20894
   220
wenzelm@21293
   221
fun begin loc =
wenzelm@21293
   222
  Data.put (if loc = "" then NONE else SOME loc) #>
wenzelm@21533
   223
  LocalTheory.init (NameSpace.base loc)
wenzelm@21293
   224
   {pretty = pretty loc,
wenzelm@21293
   225
    consts = consts loc,
wenzelm@21293
   226
    axioms = axioms,
wenzelm@21293
   227
    defs = defs,
wenzelm@21293
   228
    notes = notes loc,
wenzelm@21498
   229
    type_syntax = type_syntax loc,
wenzelm@21293
   230
    term_syntax = term_syntax loc,
wenzelm@21293
   231
    declaration = declaration loc,
wenzelm@21533
   232
    target_morphism = target_morphism loc,
wenzelm@21533
   233
    target_name = target_name loc,
wenzelm@21293
   234
    reinit = fn _ => begin loc o (if loc = "" then ProofContext.init else Locale.init loc),
wenzelm@21533
   235
    exit = LocalTheory.target_of};
wenzelm@20894
   236
wenzelm@20962
   237
fun init_i NONE thy = begin "" (ProofContext.init thy)
wenzelm@20962
   238
  | init_i (SOME loc) thy = begin loc (Locale.init loc thy);
wenzelm@20894
   239
wenzelm@21276
   240
fun init (SOME "-") thy = init_i NONE thy
wenzelm@21276
   241
  | init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
wenzelm@20894
   242
wenzelm@20894
   243
end;