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