src/Pure/Thy/export_theory.ML
author wenzelm
Sat May 26 22:02:25 2018 +0200 (17 months ago)
changeset 68295 781a98696638
parent 68264 bb9a3be6952a
child 68539 6740e3611a86
permissions -rw-r--r--
export sort algebra;
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@68201
    62
              | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
wenzelm@68201
    63
          |> sort_by #1 |> map #2
wenzelm@68201
    64
        end;
wenzelm@68201
    65
      in if null elems then () else export_body thy export_name elems end;
wenzelm@68165
    66
wenzelm@68165
    67
wenzelm@68201
    68
    (* types *)
wenzelm@68165
    69
wenzelm@68201
    70
    val encode_type =
wenzelm@68201
    71
      let open XML.Encode Term_XML.Encode
wenzelm@68201
    72
      in pair (list string) (option typ) end;
wenzelm@68165
    73
wenzelm@68201
    74
    fun export_type (Type.LogicalType n) =
wenzelm@68201
    75
          SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
wenzelm@68201
    76
      | export_type (Type.Abbreviation (args, U, false)) =
wenzelm@68201
    77
          SOME (encode_type (args, SOME U))
wenzelm@68201
    78
      | export_type _ = NONE;
wenzelm@68165
    79
wenzelm@68201
    80
    val _ =
wenzelm@68201
    81
      export_entities "types" (K export_type) Sign.type_space
wenzelm@68264
    82
        (Name_Space.dest_table (#types rep_tsig));
wenzelm@68201
    83
wenzelm@68173
    84
wenzelm@68201
    85
    (* consts *)
wenzelm@68201
    86
wenzelm@68201
    87
    val encode_const =
wenzelm@68201
    88
      let open XML.Encode Term_XML.Encode
wenzelm@68201
    89
      in triple (list string) typ (option term) end;
wenzelm@68165
    90
wenzelm@68201
    91
    fun export_const c (T, abbrev) =
wenzelm@68201
    92
      let
wenzelm@68201
    93
        val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
wenzelm@68201
    94
        val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
wenzelm@68201
    95
        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
wenzelm@68201
    96
      in SOME (encode_const (args, T', abbrev')) end;
wenzelm@68165
    97
wenzelm@68201
    98
    val _ =
wenzelm@68201
    99
      export_entities "consts" export_const Sign.const_space
wenzelm@68201
   100
        (#constants (Consts.dest (Sign.consts_of thy)));
wenzelm@68201
   101
wenzelm@68208
   102
wenzelm@68232
   103
    (* axioms and facts *)
wenzelm@68208
   104
wenzelm@68232
   105
    val encode_props =
wenzelm@68208
   106
      let open XML.Encode Term_XML.Encode
wenzelm@68232
   107
      in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
wenzelm@68208
   108
wenzelm@68232
   109
    fun export_props props =
wenzelm@68208
   110
      let
wenzelm@68232
   111
        val props' = map Logic.unvarify_global props;
wenzelm@68232
   112
        val typargs = rev (fold Term.add_tfrees props' []);
wenzelm@68232
   113
        val args = rev (fold Term.add_frees props' []);
wenzelm@68232
   114
      in encode_props (typargs, args, props') end;
wenzelm@68208
   115
wenzelm@68235
   116
    val export_axiom = export_props o single;
wenzelm@68235
   117
    val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of;
wenzelm@68208
   118
wenzelm@68232
   119
    val _ =
wenzelm@68235
   120
      export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
wenzelm@68235
   121
        (Theory.axioms_of thy);
wenzelm@68235
   122
    val _ =
wenzelm@68235
   123
      export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of)
wenzelm@68232
   124
        (Facts.dest_static true [] (Global_Theory.facts_of thy));
wenzelm@68232
   125
wenzelm@68264
   126
wenzelm@68264
   127
    (* type classes *)
wenzelm@68264
   128
wenzelm@68264
   129
    val encode_class =
wenzelm@68264
   130
      let open XML.Encode Term_XML.Encode
wenzelm@68264
   131
      in pair (list (pair string typ)) (list term) end;
wenzelm@68264
   132
wenzelm@68264
   133
    fun export_class name =
wenzelm@68264
   134
      (case try (Axclass.get_info thy) name of
wenzelm@68264
   135
        NONE => ([], [])
wenzelm@68264
   136
      | SOME {params, axioms, ...} =>
wenzelm@68264
   137
          (params, map (Logic.unvarify_global o Thm.full_prop_of) axioms))
wenzelm@68264
   138
      |> encode_class |> SOME;
wenzelm@68264
   139
wenzelm@68264
   140
    val _ =
wenzelm@68264
   141
      export_entities "classes" (fn name => fn () => export_class name)
wenzelm@68264
   142
        Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))));
wenzelm@68264
   143
wenzelm@68295
   144
wenzelm@68295
   145
    (* sort algebra *)
wenzelm@68295
   146
wenzelm@68295
   147
    val {classrel, arities} =
wenzelm@68295
   148
      Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
wenzelm@68295
   149
        (#2 (#classes rep_tsig));
wenzelm@68295
   150
wenzelm@68295
   151
    val encode_classrel =
wenzelm@68295
   152
      let open XML.Encode
wenzelm@68295
   153
      in list (pair string (list string)) end;
wenzelm@68295
   154
wenzelm@68295
   155
    val encode_arities =
wenzelm@68295
   156
      let open XML.Encode Term_XML.Encode
wenzelm@68295
   157
      in list (triple string (list sort) string) end;
wenzelm@68295
   158
wenzelm@68295
   159
    val _ = if null classrel then () else export_body thy "classrel" (encode_classrel classrel);
wenzelm@68295
   160
    val _ = if null arities then () else export_body thy "arities" (encode_arities arities);
wenzelm@68295
   161
wenzelm@68295
   162
  in () end);
wenzelm@68165
   163
wenzelm@68165
   164
end;