some export of foundational theory content;
authorwenzelm
Fri May 11 22:59:00 2018 +0200 (12 months ago)
changeset 6815442d63ea39161
parent 68153 e469d529e6da
child 68155 8b50f29a1992
some export of foundational theory content;
etc/options
src/Pure/ROOT.ML
src/Pure/Thy/export_theory.ML
     1.1 --- a/etc/options	Fri May 11 22:40:02 2018 +0200
     1.2 +++ b/etc/options	Fri May 11 22:59:00 2018 +0200
     1.3 @@ -247,6 +247,11 @@
     1.4    -- "maximum number of messages to keep SSH server connection alive"
     1.5  
     1.6  
     1.7 +section "Theory export"
     1.8 +
     1.9 +option export_theory : bool = false
    1.10 +
    1.11 +
    1.12  section "Build Log Database"
    1.13  
    1.14  option build_log_database_user : string = ""
     2.1 --- a/src/Pure/ROOT.ML	Fri May 11 22:40:02 2018 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Fri May 11 22:59:00 2018 +0200
     2.3 @@ -303,6 +303,7 @@
     2.4  ML_file "Thy/export.ML";
     2.5  ML_file "Thy/present.ML";
     2.6  ML_file "Thy/thy_info.ML";
     2.7 +ML_file "Thy/export_theory.ML";
     2.8  ML_file "Thy/sessions.ML";
     2.9  ML_file "PIDE/session.ML";
    2.10  ML_file "PIDE/protocol_message.ML";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Thy/export_theory.ML	Fri May 11 22:59:00 2018 +0200
     3.3 @@ -0,0 +1,61 @@
     3.4 +(*  Title:      Pure/Thy/export_theory.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Export foundational theory content.
     3.8 +*)
     3.9 +
    3.10 +signature EXPORT_THEORY =
    3.11 +sig
    3.12 +  val export_table_diff: ('a -> XML.tree list option) ->
    3.13 +    'a Name_Space.table list -> 'a Name_Space.table -> XML.tree list
    3.14 +end;
    3.15 +
    3.16 +structure Export_Theory: EXPORT_THEORY =
    3.17 +struct
    3.18 +
    3.19 +(* export namespace table *)
    3.20 +
    3.21 +fun export_table_diff export_decl prev_tables table =
    3.22 +  (table, []) |-> Name_Space.fold_table (fn (name, decl) =>
    3.23 +    if exists (fn prev => Name_Space.defined prev name) prev_tables then I
    3.24 +    else
    3.25 +      (case export_decl decl of
    3.26 +        NONE => I
    3.27 +      | SOME body =>
    3.28 +          let val markup = Name_Space.markup_def (Name_Space.space_of_table table) name
    3.29 +          in cons (name, XML.Elem (markup, body)) end))
    3.30 +  |> sort_by #1 |> map #2;
    3.31 +
    3.32 +
    3.33 +(* present *)
    3.34 +
    3.35 +fun present get export name thy =
    3.36 +  if Options.default_bool "export_theory" then
    3.37 +    (case export (map get (Theory.parents_of thy)) (get thy) of
    3.38 +      [] => ()
    3.39 +    | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body])
    3.40 +  else ();
    3.41 +
    3.42 +
    3.43 +(* types *)
    3.44 +
    3.45 +val present_types = present (#types o Type.rep_tsig o Sign.tsig_of) o export_table_diff;
    3.46 +
    3.47 +fun export_logical_type (Type.LogicalType n) = SOME (XML.Encode.int n)
    3.48 +  | export_logical_type _ = NONE;
    3.49 +
    3.50 +fun export_abbreviation (Type.Abbreviation (vs, U, _)) =
    3.51 +      let open XML.Encode Term_XML.Encode
    3.52 +      in SOME (pair (list string) typ (vs, U)) end
    3.53 +  | export_abbreviation _ = NONE;
    3.54 +
    3.55 +fun export_nonterminal Type.Nonterminal = SOME []
    3.56 +  | export_nonterminal _ = NONE;
    3.57 +
    3.58 +val _ =
    3.59 +  Theory.setup
    3.60 +    (Thy_Info.add_presentation (present_types export_logical_type "types") #>
    3.61 +     Thy_Info.add_presentation (present_types export_abbreviation "type_synonyms") #>
    3.62 +     Thy_Info.add_presentation (present_types export_nonterminal "nonterminals"));
    3.63 +
    3.64 +end;