misc tuning and clarification;
authorwenzelm
Thu May 17 14:01:13 2018 +0200 (4 days ago)
changeset 68201dee993b88a7b
parent 68200 5859c688102a
child 68202 a99180ad3441
misc tuning and clarification;
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu May 17 07:42:33 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Thu May 17 14:01:13 2018 +0200
     1.3 @@ -6,90 +6,88 @@
     1.4  
     1.5  signature EXPORT_THEORY =
     1.6  sig
     1.7 +  val setup_presentation: (Thy_Info.presentation_context -> theory -> unit) -> unit
     1.8 +  val export_body: theory -> string -> XML.body -> unit
     1.9  end;
    1.10  
    1.11  structure Export_Theory: EXPORT_THEORY =
    1.12  struct
    1.13  
    1.14 -(* name space entries *)
    1.15 +(* general setup *)
    1.16  
    1.17 -fun entity_markup adjust_pos space name =
    1.18 +fun setup_presentation f =
    1.19 +  Theory.setup (Thy_Info.add_presentation (fn context => fn thy =>
    1.20 +    if Options.bool (#options context) "export_theory" then f context thy else ()));
    1.21 +
    1.22 +fun export_body thy name body =
    1.23 +  Export.export thy ("theory/" ^ name) [YXML.string_of_body body];
    1.24 +
    1.25 +
    1.26 +(* presentation *)
    1.27 +
    1.28 +val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
    1.29    let
    1.30 -    val {serial, pos, ...} = Name_Space.the_entry space name;
    1.31 -    val props = Markup.serial_properties serial @ Position.offset_properties_of (adjust_pos pos);
    1.32 -  in (Markup.entityN, (Markup.nameN, name) :: props) end;
    1.33 +    (* entities *)
    1.34  
    1.35 -fun export_decls export_decl parents thy adjust_pos space decls =
    1.36 -  (decls, []) |-> fold (fn (name, decl) =>
    1.37 -    if exists (fn space => Name_Space.declared space name) parents then I
    1.38 -    else
    1.39 -      (case export_decl thy name decl of
    1.40 -        NONE => I
    1.41 -      | SOME body => cons (name, XML.Elem (entity_markup adjust_pos space name, body))))
    1.42 -  |> sort_by #1 |> map #2;
    1.43 +    fun entity_markup space name =
    1.44 +      let
    1.45 +        val {serial, pos, ...} = Name_Space.the_entry space name;
    1.46 +        val props =
    1.47 +          Markup.serial_properties serial @
    1.48 +          Position.offset_properties_of (adjust_pos pos);
    1.49 +      in (Markup.entityN, (Markup.nameN, name) :: props) end;
    1.50  
    1.51 +    fun export_entities export_name export get_space decls =
    1.52 +      let val elems =
    1.53 +        let
    1.54 +          val parent_spaces = map get_space (Theory.parents_of thy);
    1.55 +          val space = get_space thy;
    1.56 +        in
    1.57 +          (decls, []) |-> fold (fn (name, decl) =>
    1.58 +            if exists (fn space => Name_Space.declared space name) parent_spaces then I
    1.59 +            else
    1.60 +              (case export name decl of
    1.61 +                NONE => I
    1.62 +              | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
    1.63 +          |> sort_by #1 |> map #2
    1.64 +        end;
    1.65 +      in if null elems then () else export_body thy export_name elems end;
    1.66  
    1.67 -(* present *)
    1.68  
    1.69 -fun present get_space get_decls export name adjust_pos thy =
    1.70 -  if Options.default_bool "export_theory" then
    1.71 -    (case
    1.72 -      export (map get_space (Theory.parents_of thy)) thy adjust_pos (get_space thy) (get_decls thy)
    1.73 -     of
    1.74 -      [] => ()
    1.75 -    | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body])
    1.76 -  else ();
    1.77 +    (* types *)
    1.78  
    1.79 -fun present_decls get_space get_decls =
    1.80 -  present get_space get_decls o export_decls;
    1.81 +    val encode_type =
    1.82 +      let open XML.Encode Term_XML.Encode
    1.83 +      in pair (list string) (option typ) end;
    1.84  
    1.85 -val setup_presentation = Theory.setup o Thy_Info.add_presentation;
    1.86 +    fun export_type (Type.LogicalType n) =
    1.87 +          SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
    1.88 +      | export_type (Type.Abbreviation (args, U, false)) =
    1.89 +          SOME (encode_type (args, SOME U))
    1.90 +      | export_type _ = NONE;
    1.91  
    1.92 +    val _ =
    1.93 +      export_entities "types" (K export_type) Sign.type_space
    1.94 +        (Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy))));
    1.95  
    1.96 -(* types *)
    1.97  
    1.98 -local
    1.99 +    (* consts *)
   1.100  
   1.101 -val present_types =
   1.102 -  present_decls Sign.type_space (Name_Space.dest_table o #types o Type.rep_tsig o Sign.tsig_of);
   1.103 +    val encode_const =
   1.104 +      let open XML.Encode Term_XML.Encode
   1.105 +      in triple (list string) typ (option term) end;
   1.106  
   1.107 -val encode_type =
   1.108 -  let open XML.Encode Term_XML.Encode
   1.109 -  in pair (list string) (option typ) end;
   1.110 +    fun export_const c (T, abbrev) =
   1.111 +      let
   1.112 +        val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
   1.113 +        val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
   1.114 +        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
   1.115 +      in SOME (encode_const (args, T', abbrev')) end;
   1.116  
   1.117 -fun export_type (Type.LogicalType n) = SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
   1.118 -  | export_type (Type.Abbreviation (args, U, false)) = SOME (encode_type (args, SOME U))
   1.119 -  | export_type _ = NONE;
   1.120 +    val _ =
   1.121 +      export_entities "consts" export_const Sign.const_space
   1.122 +        (#constants (Consts.dest (Sign.consts_of thy)));
   1.123  
   1.124 -in
   1.125 -
   1.126 -val _ = setup_presentation (present_types (K (K export_type)) "types" o #adjust_pos);
   1.127 +    in () end);
   1.128  
   1.129  end;
   1.130 -
   1.131 -
   1.132 -(* consts *)
   1.133 -
   1.134 -local
   1.135 -
   1.136 -val present_consts =
   1.137 -  present_decls Sign.const_space (#constants o Consts.dest o Sign.consts_of);
   1.138 -
   1.139 -val encode_const =
   1.140 -  let open XML.Encode Term_XML.Encode
   1.141 -  in triple (list string) typ (option term) end;
   1.142 -
   1.143 -fun export_const thy c (T, abbrev) =
   1.144 -  let
   1.145 -    val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
   1.146 -    val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
   1.147 -    val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
   1.148 -  in SOME (encode_const (args, T', abbrev')) end;
   1.149 -
   1.150 -in
   1.151 -
   1.152 -val _ = setup_presentation (present_consts export_const "consts" o #adjust_pos);
   1.153 -
   1.154 -end;
   1.155 -
   1.156 -end;