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