src/Pure/Thy/export_theory.ML
author wenzelm
Sun May 20 16:25:27 2018 +0200 (17 months ago)
changeset 68232 4b93573ac5b4
parent 68231 0004e7a9fa10
child 68235 a3bd410db5b2
permissions -rw-r--r--
export facts;
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@68206
    30
    (* parents *)
wenzelm@68206
    31
wenzelm@68206
    32
    val parents = Theory.parents_of thy;
wenzelm@68206
    33
    val _ =
wenzelm@68206
    34
      export_body thy "parents"
wenzelm@68231
    35
        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
wenzelm@68206
    36
wenzelm@68206
    37
wenzelm@68201
    38
    (* entities *)
wenzelm@68154
    39
wenzelm@68201
    40
    fun entity_markup space name =
wenzelm@68201
    41
      let
wenzelm@68201
    42
        val {serial, pos, ...} = Name_Space.the_entry space name;
wenzelm@68201
    43
        val props =
wenzelm@68201
    44
          Markup.serial_properties serial @
wenzelm@68201
    45
          Position.offset_properties_of (adjust_pos pos);
wenzelm@68201
    46
      in (Markup.entityN, (Markup.nameN, name) :: props) end;
wenzelm@68154
    47
wenzelm@68201
    48
    fun export_entities export_name export get_space decls =
wenzelm@68201
    49
      let val elems =
wenzelm@68201
    50
        let
wenzelm@68206
    51
          val parent_spaces = map get_space parents;
wenzelm@68201
    52
          val space = get_space thy;
wenzelm@68201
    53
        in
wenzelm@68201
    54
          (decls, []) |-> fold (fn (name, decl) =>
wenzelm@68201
    55
            if exists (fn space => Name_Space.declared space name) parent_spaces then I
wenzelm@68201
    56
            else
wenzelm@68201
    57
              (case export name decl of
wenzelm@68201
    58
                NONE => I
wenzelm@68201
    59
              | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
wenzelm@68201
    60
          |> sort_by #1 |> map #2
wenzelm@68201
    61
        end;
wenzelm@68201
    62
      in if null elems then () else export_body thy export_name elems end;
wenzelm@68165
    63
wenzelm@68165
    64
wenzelm@68201
    65
    (* types *)
wenzelm@68165
    66
wenzelm@68201
    67
    val encode_type =
wenzelm@68201
    68
      let open XML.Encode Term_XML.Encode
wenzelm@68201
    69
      in pair (list string) (option typ) end;
wenzelm@68165
    70
wenzelm@68201
    71
    fun export_type (Type.LogicalType n) =
wenzelm@68201
    72
          SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
wenzelm@68201
    73
      | export_type (Type.Abbreviation (args, U, false)) =
wenzelm@68201
    74
          SOME (encode_type (args, SOME U))
wenzelm@68201
    75
      | export_type _ = NONE;
wenzelm@68165
    76
wenzelm@68201
    77
    val _ =
wenzelm@68201
    78
      export_entities "types" (K export_type) Sign.type_space
wenzelm@68201
    79
        (Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy))));
wenzelm@68201
    80
wenzelm@68173
    81
wenzelm@68201
    82
    (* consts *)
wenzelm@68201
    83
wenzelm@68201
    84
    val encode_const =
wenzelm@68201
    85
      let open XML.Encode Term_XML.Encode
wenzelm@68201
    86
      in triple (list string) typ (option term) end;
wenzelm@68165
    87
wenzelm@68201
    88
    fun export_const c (T, abbrev) =
wenzelm@68201
    89
      let
wenzelm@68201
    90
        val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
wenzelm@68201
    91
        val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
wenzelm@68201
    92
        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
wenzelm@68201
    93
      in SOME (encode_const (args, T', abbrev')) end;
wenzelm@68165
    94
wenzelm@68201
    95
    val _ =
wenzelm@68201
    96
      export_entities "consts" export_const Sign.const_space
wenzelm@68201
    97
        (#constants (Consts.dest (Sign.consts_of thy)));
wenzelm@68201
    98
wenzelm@68208
    99
wenzelm@68232
   100
    (* axioms and facts *)
wenzelm@68208
   101
wenzelm@68232
   102
    val encode_props =
wenzelm@68208
   103
      let open XML.Encode Term_XML.Encode
wenzelm@68232
   104
      in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
wenzelm@68208
   105
wenzelm@68232
   106
    fun export_props props =
wenzelm@68208
   107
      let
wenzelm@68232
   108
        val props' = map Logic.unvarify_global props;
wenzelm@68232
   109
        val typargs = rev (fold Term.add_tfrees props' []);
wenzelm@68232
   110
        val args = rev (fold Term.add_frees props' []);
wenzelm@68232
   111
      in encode_props (typargs, args, props') end;
wenzelm@68208
   112
wenzelm@68208
   113
    val _ =
wenzelm@68232
   114
      export_entities "axioms" (K (SOME o export_props o single)) Theory.axiom_space
wenzelm@68208
   115
        (Theory.axioms_of thy);
wenzelm@68208
   116
wenzelm@68232
   117
    val _ =
wenzelm@68232
   118
      export_entities "facts" (K (SOME o export_props o map Thm.full_prop_of))
wenzelm@68232
   119
        (Facts.space_of o Global_Theory.facts_of)
wenzelm@68232
   120
        (Facts.dest_static true [] (Global_Theory.facts_of thy));
wenzelm@68232
   121
wenzelm@68201
   122
    in () end);
wenzelm@68165
   123
wenzelm@68165
   124
end;