src/Pure/Thy/export_theory.ML
author wenzelm
Sat Aug 04 22:32:41 2018 +0200 (14 months ago)
changeset 68724 7fafadbf16c7
parent 68539 6740e3611a86
child 68725 367e60d9aa1b
permissions -rw-r--r--
export in foundational order;
wenzelm@68154
     1
(*  Title:      Pure/Thy/export_theory.ML
wenzelm@68154
     2
    Author:     Makarius
wenzelm@68154
     3
wenzelm@68154
     4
Export foundational theory content.
wenzelm@68154
     5
*)
wenzelm@68154
     6
wenzelm@68154
     7
signature EXPORT_THEORY =
wenzelm@68154
     8
sig
wenzelm@68201
     9
  val setup_presentation: (Thy_Info.presentation_context -> theory -> unit) -> unit
wenzelm@68201
    10
  val export_body: theory -> string -> XML.body -> unit
wenzelm@68154
    11
end;
wenzelm@68154
    12
wenzelm@68154
    13
structure Export_Theory: EXPORT_THEORY =
wenzelm@68154
    14
struct
wenzelm@68154
    15
wenzelm@68201
    16
(* general setup *)
wenzelm@68154
    17
wenzelm@68201
    18
fun setup_presentation f =
wenzelm@68201
    19
  Theory.setup (Thy_Info.add_presentation (fn context => fn thy =>
wenzelm@68201
    20
    if Options.bool (#options context) "export_theory" then f context thy else ()));
wenzelm@68154
    21
wenzelm@68201
    22
fun export_body thy name body =
wenzelm@68230
    23
  Export.export thy ("theory/" ^ name) (Buffer.chunks (YXML.buffer_body body Buffer.empty));
wenzelm@68165
    24
wenzelm@68154
    25
wenzelm@68201
    26
(* presentation *)
wenzelm@68201
    27
wenzelm@68201
    28
val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
wenzelm@68201
    29
  let
wenzelm@68264
    30
    val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
wenzelm@68264
    31
wenzelm@68264
    32
wenzelm@68206
    33
    (* parents *)
wenzelm@68206
    34
wenzelm@68206
    35
    val parents = Theory.parents_of thy;
wenzelm@68206
    36
    val _ =
wenzelm@68206
    37
      export_body thy "parents"
wenzelm@68231
    38
        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
wenzelm@68206
    39
wenzelm@68206
    40
wenzelm@68201
    41
    (* entities *)
wenzelm@68154
    42
wenzelm@68201
    43
    fun entity_markup space name =
wenzelm@68201
    44
      let
wenzelm@68201
    45
        val {serial, pos, ...} = Name_Space.the_entry space name;
wenzelm@68201
    46
        val props =
wenzelm@68201
    47
          Markup.serial_properties serial @
wenzelm@68201
    48
          Position.offset_properties_of (adjust_pos pos);
wenzelm@68201
    49
      in (Markup.entityN, (Markup.nameN, name) :: props) end;
wenzelm@68154
    50
wenzelm@68201
    51
    fun export_entities export_name export get_space decls =
wenzelm@68201
    52
      let val elems =
wenzelm@68201
    53
        let
wenzelm@68206
    54
          val parent_spaces = map get_space parents;
wenzelm@68201
    55
          val space = get_space thy;
wenzelm@68201
    56
        in
wenzelm@68201
    57
          (decls, []) |-> fold (fn (name, decl) =>
wenzelm@68201
    58
            if exists (fn space => Name_Space.declared space name) parent_spaces then I
wenzelm@68201
    59
            else
wenzelm@68201
    60
              (case export name decl of
wenzelm@68201
    61
                NONE => I
wenzelm@68724
    62
              | SOME body =>
wenzelm@68724
    63
                  cons (#serial (Name_Space.the_entry space name),
wenzelm@68724
    64
                    XML.Elem (entity_markup space name, body))))
wenzelm@68724
    65
          |> sort (int_ord o apply2 #1) |> map #2
wenzelm@68201
    66
        end;
wenzelm@68724
    67
wenzelm@68201
    68
      in if null elems then () else export_body thy export_name elems end;
wenzelm@68165
    69
wenzelm@68165
    70
wenzelm@68201
    71
    (* types *)
wenzelm@68165
    72
wenzelm@68201
    73
    val encode_type =
wenzelm@68201
    74
      let open XML.Encode Term_XML.Encode
wenzelm@68201
    75
      in pair (list string) (option typ) end;
wenzelm@68165
    76
wenzelm@68201
    77
    fun export_type (Type.LogicalType n) =
wenzelm@68201
    78
          SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
wenzelm@68201
    79
      | export_type (Type.Abbreviation (args, U, false)) =
wenzelm@68201
    80
          SOME (encode_type (args, SOME U))
wenzelm@68201
    81
      | export_type _ = NONE;
wenzelm@68165
    82
wenzelm@68201
    83
    val _ =
wenzelm@68201
    84
      export_entities "types" (K export_type) Sign.type_space
wenzelm@68264
    85
        (Name_Space.dest_table (#types rep_tsig));
wenzelm@68201
    86
wenzelm@68173
    87
wenzelm@68201
    88
    (* consts *)
wenzelm@68201
    89
wenzelm@68201
    90
    val encode_const =
wenzelm@68201
    91
      let open XML.Encode Term_XML.Encode
wenzelm@68201
    92
      in triple (list string) typ (option term) end;
wenzelm@68165
    93
wenzelm@68201
    94
    fun export_const c (T, abbrev) =
wenzelm@68201
    95
      let
wenzelm@68201
    96
        val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
wenzelm@68201
    97
        val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
wenzelm@68201
    98
        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
wenzelm@68201
    99
      in SOME (encode_const (args, T', abbrev')) end;
wenzelm@68165
   100
wenzelm@68201
   101
    val _ =
wenzelm@68201
   102
      export_entities "consts" export_const Sign.const_space
wenzelm@68201
   103
        (#constants (Consts.dest (Sign.consts_of thy)));
wenzelm@68201
   104
wenzelm@68208
   105
wenzelm@68232
   106
    (* axioms and facts *)
wenzelm@68208
   107
wenzelm@68539
   108
    val standard_prop_of =
wenzelm@68539
   109
      Thm.transfer thy #>
wenzelm@68539
   110
      Thm.check_hyps (Context.Theory thy) #>
wenzelm@68539
   111
      Drule.sort_constraint_intr_shyps #>
wenzelm@68539
   112
      Thm.full_prop_of;
wenzelm@68539
   113
wenzelm@68232
   114
    val encode_props =
wenzelm@68208
   115
      let open XML.Encode Term_XML.Encode
wenzelm@68232
   116
      in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
wenzelm@68208
   117
wenzelm@68232
   118
    fun export_props props =
wenzelm@68208
   119
      let
wenzelm@68232
   120
        val props' = map Logic.unvarify_global props;
wenzelm@68232
   121
        val typargs = rev (fold Term.add_tfrees props' []);
wenzelm@68232
   122
        val args = rev (fold Term.add_frees props' []);
wenzelm@68232
   123
      in encode_props (typargs, args, props') end;
wenzelm@68208
   124
wenzelm@68235
   125
    val export_axiom = export_props o single;
wenzelm@68539
   126
    val export_fact = export_props o Term_Subst.zero_var_indexes_list o map standard_prop_of;
wenzelm@68208
   127
wenzelm@68232
   128
    val _ =
wenzelm@68235
   129
      export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
wenzelm@68235
   130
        (Theory.axioms_of thy);
wenzelm@68235
   131
    val _ =
wenzelm@68235
   132
      export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of)
wenzelm@68232
   133
        (Facts.dest_static true [] (Global_Theory.facts_of thy));
wenzelm@68232
   134
wenzelm@68264
   135
wenzelm@68264
   136
    (* type classes *)
wenzelm@68264
   137
wenzelm@68264
   138
    val encode_class =
wenzelm@68264
   139
      let open XML.Encode Term_XML.Encode
wenzelm@68264
   140
      in pair (list (pair string typ)) (list term) end;
wenzelm@68264
   141
wenzelm@68264
   142
    fun export_class name =
wenzelm@68264
   143
      (case try (Axclass.get_info thy) name of
wenzelm@68264
   144
        NONE => ([], [])
wenzelm@68264
   145
      | SOME {params, axioms, ...} =>
wenzelm@68264
   146
          (params, map (Logic.unvarify_global o Thm.full_prop_of) axioms))
wenzelm@68264
   147
      |> encode_class |> SOME;
wenzelm@68264
   148
wenzelm@68264
   149
    val _ =
wenzelm@68264
   150
      export_entities "classes" (fn name => fn () => export_class name)
wenzelm@68264
   151
        Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))));
wenzelm@68264
   152
wenzelm@68295
   153
wenzelm@68295
   154
    (* sort algebra *)
wenzelm@68295
   155
wenzelm@68295
   156
    val {classrel, arities} =
wenzelm@68295
   157
      Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
wenzelm@68295
   158
        (#2 (#classes rep_tsig));
wenzelm@68295
   159
wenzelm@68295
   160
    val encode_classrel =
wenzelm@68295
   161
      let open XML.Encode
wenzelm@68295
   162
      in list (pair string (list string)) end;
wenzelm@68295
   163
wenzelm@68295
   164
    val encode_arities =
wenzelm@68295
   165
      let open XML.Encode Term_XML.Encode
wenzelm@68295
   166
      in list (triple string (list sort) string) end;
wenzelm@68295
   167
wenzelm@68295
   168
    val _ = if null classrel then () else export_body thy "classrel" (encode_classrel classrel);
wenzelm@68295
   169
    val _ = if null arities then () else export_body thy "arities" (encode_arities arities);
wenzelm@68295
   170
wenzelm@68295
   171
  in () end);
wenzelm@68165
   172
wenzelm@68165
   173
end;