src/Pure/Thy/export_theory.ML
author wenzelm
Sun, 20 May 2018 15:37:16 +0200
changeset 68231 0004e7a9fa10
parent 68230 9bee37c2ac2b
child 68232 4b93573ac5b4
permissions -rw-r--r--
clarified encoding;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68154
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/export_theory.ML
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
     3
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
     4
Export foundational theory content.
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
     5
*)
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
     6
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
     7
signature EXPORT_THEORY =
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
     8
sig
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
     9
  val setup_presentation: (Thy_Info.presentation_context -> theory -> unit) -> unit
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    10
  val export_body: theory -> string -> XML.body -> unit
68154
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
    11
end;
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
    12
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
    13
structure Export_Theory: EXPORT_THEORY =
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
    14
struct
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
    15
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    16
(* general setup *)
68154
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
    17
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    18
fun setup_presentation f =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    19
  Theory.setup (Thy_Info.add_presentation (fn context => fn thy =>
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    20
    if Options.bool (#options context) "export_theory" then f context thy else ()));
68154
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
    21
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    22
fun export_body thy name body =
68230
9bee37c2ac2b more scalable;
wenzelm
parents: 68208
diff changeset
    23
  Export.export thy ("theory/" ^ name) (Buffer.chunks (YXML.buffer_body body Buffer.empty));
68165
a7a2174ac014 more exports;
wenzelm
parents: 68154
diff changeset
    24
68154
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
    25
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    26
(* presentation *)
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    27
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    28
val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    29
  let
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68201
diff changeset
    30
    (* parents *)
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68201
diff changeset
    31
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68201
diff changeset
    32
    val parents = Theory.parents_of thy;
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68201
diff changeset
    33
    val _ =
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68201
diff changeset
    34
      export_body thy "parents"
68231
0004e7a9fa10 clarified encoding;
wenzelm
parents: 68230
diff changeset
    35
        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68201
diff changeset
    36
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68201
diff changeset
    37
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    38
    (* entities *)
68154
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
    39
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    40
    fun entity_markup space name =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    41
      let
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    42
        val {serial, pos, ...} = Name_Space.the_entry space name;
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    43
        val props =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    44
          Markup.serial_properties serial @
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    45
          Position.offset_properties_of (adjust_pos pos);
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    46
      in (Markup.entityN, (Markup.nameN, name) :: props) end;
68154
42d63ea39161 some export of foundational theory content;
wenzelm
parents:
diff changeset
    47
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    48
    fun export_entities export_name export get_space decls =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    49
      let val elems =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    50
        let
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68201
diff changeset
    51
          val parent_spaces = map get_space parents;
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    52
          val space = get_space thy;
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    53
        in
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    54
          (decls, []) |-> fold (fn (name, decl) =>
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    55
            if exists (fn space => Name_Space.declared space name) parent_spaces then I
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    56
            else
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    57
              (case export name decl of
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    58
                NONE => I
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    59
              | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    60
          |> sort_by #1 |> map #2
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    61
        end;
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    62
      in if null elems then () else export_body thy export_name elems end;
68165
a7a2174ac014 more exports;
wenzelm
parents: 68154
diff changeset
    63
a7a2174ac014 more exports;
wenzelm
parents: 68154
diff changeset
    64
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    65
    (* types *)
68165
a7a2174ac014 more exports;
wenzelm
parents: 68154
diff changeset
    66
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    67
    val encode_type =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    68
      let open XML.Encode Term_XML.Encode
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    69
      in pair (list string) (option typ) end;
68165
a7a2174ac014 more exports;
wenzelm
parents: 68154
diff changeset
    70
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    71
    fun export_type (Type.LogicalType n) =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    72
          SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    73
      | export_type (Type.Abbreviation (args, U, false)) =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    74
          SOME (encode_type (args, SOME U))
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    75
      | export_type _ = NONE;
68165
a7a2174ac014 more exports;
wenzelm
parents: 68154
diff changeset
    76
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    77
    val _ =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    78
      export_entities "types" (K export_type) Sign.type_space
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    79
        (Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy))));
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    80
68173
7ed88a534bb6 more uniform types vs. consts;
wenzelm
parents: 68172
diff changeset
    81
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    82
    (* consts *)
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    83
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    84
    val encode_const =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    85
      let open XML.Encode Term_XML.Encode
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    86
      in triple (list string) typ (option term) end;
68165
a7a2174ac014 more exports;
wenzelm
parents: 68154
diff changeset
    87
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    88
    fun export_const c (T, abbrev) =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    89
      let
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    90
        val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    91
        val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    92
        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    93
      in SOME (encode_const (args, T', abbrev')) end;
68165
a7a2174ac014 more exports;
wenzelm
parents: 68154
diff changeset
    94
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    95
    val _ =
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    96
      export_entities "consts" export_const Sign.const_space
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    97
        (#constants (Consts.dest (Sign.consts_of thy)));
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
    98
68208
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
    99
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   100
    (* axioms *)
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   101
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   102
    val encode_axiom =
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   103
      let open XML.Encode Term_XML.Encode
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   104
      in triple (list (pair string sort)) (list (pair string typ)) term end;
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   105
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   106
    fun export_axiom prop =
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   107
      let
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   108
        val prop' = Logic.unvarify_global prop;
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   109
        val typargs = rev (Term.add_tfrees prop' []);
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   110
        val args = rev (Term.add_frees prop' []);
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   111
      in encode_axiom (typargs, args, prop') end;
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   112
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   113
    val _ =
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   114
      export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   115
        (Theory.axioms_of thy);
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   116
68201
dee993b88a7b misc tuning and clarification;
wenzelm
parents: 68199
diff changeset
   117
    in () end);
68165
a7a2174ac014 more exports;
wenzelm
parents: 68154
diff changeset
   118
a7a2174ac014 more exports;
wenzelm
parents: 68154
diff changeset
   119
end;