src/Pure/Thy/export_theory.ML
author wenzelm
Fri May 11 22:59:00 2018 +0200 (17 months ago)
changeset 68154 42d63ea39161
child 68165 a7a2174ac014
permissions -rw-r--r--
some export of foundational theory content;
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@68154
     9
  val export_table_diff: ('a -> XML.tree list option) ->
wenzelm@68154
    10
    'a Name_Space.table list -> 'a Name_Space.table -> XML.tree list
wenzelm@68154
    11
end;
wenzelm@68154
    12
wenzelm@68154
    13
structure Export_Theory: EXPORT_THEORY =
wenzelm@68154
    14
struct
wenzelm@68154
    15
wenzelm@68154
    16
(* export namespace table *)
wenzelm@68154
    17
wenzelm@68154
    18
fun export_table_diff export_decl prev_tables table =
wenzelm@68154
    19
  (table, []) |-> Name_Space.fold_table (fn (name, decl) =>
wenzelm@68154
    20
    if exists (fn prev => Name_Space.defined prev name) prev_tables then I
wenzelm@68154
    21
    else
wenzelm@68154
    22
      (case export_decl decl of
wenzelm@68154
    23
        NONE => I
wenzelm@68154
    24
      | SOME body =>
wenzelm@68154
    25
          let val markup = Name_Space.markup_def (Name_Space.space_of_table table) name
wenzelm@68154
    26
          in cons (name, XML.Elem (markup, body)) end))
wenzelm@68154
    27
  |> sort_by #1 |> map #2;
wenzelm@68154
    28
wenzelm@68154
    29
wenzelm@68154
    30
(* present *)
wenzelm@68154
    31
wenzelm@68154
    32
fun present get export name thy =
wenzelm@68154
    33
  if Options.default_bool "export_theory" then
wenzelm@68154
    34
    (case export (map get (Theory.parents_of thy)) (get thy) of
wenzelm@68154
    35
      [] => ()
wenzelm@68154
    36
    | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body])
wenzelm@68154
    37
  else ();
wenzelm@68154
    38
wenzelm@68154
    39
wenzelm@68154
    40
(* types *)
wenzelm@68154
    41
wenzelm@68154
    42
val present_types = present (#types o Type.rep_tsig o Sign.tsig_of) o export_table_diff;
wenzelm@68154
    43
wenzelm@68154
    44
fun export_logical_type (Type.LogicalType n) = SOME (XML.Encode.int n)
wenzelm@68154
    45
  | export_logical_type _ = NONE;
wenzelm@68154
    46
wenzelm@68154
    47
fun export_abbreviation (Type.Abbreviation (vs, U, _)) =
wenzelm@68154
    48
      let open XML.Encode Term_XML.Encode
wenzelm@68154
    49
      in SOME (pair (list string) typ (vs, U)) end
wenzelm@68154
    50
  | export_abbreviation _ = NONE;
wenzelm@68154
    51
wenzelm@68154
    52
fun export_nonterminal Type.Nonterminal = SOME []
wenzelm@68154
    53
  | export_nonterminal _ = NONE;
wenzelm@68154
    54
wenzelm@68154
    55
val _ =
wenzelm@68154
    56
  Theory.setup
wenzelm@68154
    57
    (Thy_Info.add_presentation (present_types export_logical_type "types") #>
wenzelm@68154
    58
     Thy_Info.add_presentation (present_types export_abbreviation "type_synonyms") #>
wenzelm@68154
    59
     Thy_Info.add_presentation (present_types export_nonterminal "nonterminals"));
wenzelm@68154
    60
wenzelm@68154
    61
end;