more uniform types vs. consts;
authorwenzelm
Sun May 13 21:20:28 2018 +0200 (12 months ago)
changeset 681737ed88a534bb6
parent 68172 0f14cf9c632f
child 68174 7c4793e39dd5
more uniform types vs. consts;
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun May 13 20:24:33 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun May 13 21:20:28 2018 +0200
     1.3 @@ -20,11 +20,11 @@
     1.4      val props = Markup.serial_properties serial @ Position.offset_properties_of pos;
     1.5    in (Markup.entityN, (Markup.nameN, name) :: props) end;
     1.6  
     1.7 -fun export_decls export_decl parents space decls =
     1.8 +fun export_decls export_decl parents thy space decls =
     1.9    (decls, []) |-> fold (fn (name, decl) =>
    1.10      if exists (fn space => Name_Space.declared space name) parents then I
    1.11      else
    1.12 -      (case export_decl decl of
    1.13 +      (case export_decl thy name decl of
    1.14          NONE => I
    1.15        | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
    1.16    |> sort_by #1 |> map #2;
    1.17 @@ -34,7 +34,7 @@
    1.18  
    1.19  fun present get_space get_decls export name thy =
    1.20    if Options.default_bool "export_theory" then
    1.21 -    (case export (map get_space (Theory.parents_of thy)) (get_space thy) (get_decls thy) of
    1.22 +    (case export (map get_space (Theory.parents_of thy)) thy (get_space thy) (get_decls thy) of
    1.23        [] => ()
    1.24      | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body])
    1.25    else ();
    1.26 @@ -62,7 +62,7 @@
    1.27  
    1.28  in
    1.29  
    1.30 -val _ = setup_presentation (present_types export_type "types");
    1.31 +val _ = setup_presentation (present_types (K (K export_type)) "types");
    1.32  
    1.33  end;
    1.34  
    1.35 @@ -76,11 +76,18 @@
    1.36  
    1.37  val encode_const =
    1.38    let open XML.Encode Term_XML.Encode
    1.39 -  in pair typ (option term) end;
    1.40 +  in triple (list string) typ (option term) end;
    1.41 +
    1.42 +fun export_const thy c (T, abbrev) =
    1.43 +  let
    1.44 +    val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
    1.45 +    val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
    1.46 +    val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
    1.47 +  in SOME (encode_const (args, T', abbrev')) end;
    1.48  
    1.49  in
    1.50  
    1.51 -val _ = setup_presentation (present_consts (SOME o encode_const) "consts");
    1.52 +val _ = setup_presentation (present_consts export_const "consts");
    1.53  
    1.54  end;
    1.55  
     2.1 --- a/src/Pure/Thy/export_theory.scala	Sun May 13 20:24:33 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Sun May 13 21:20:28 2018 +0200
     2.3 @@ -34,9 +34,6 @@
     2.4    /* types */
     2.5  
     2.6    sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
     2.7 -  {
     2.8 -    def arity: Int = args.length
     2.9 -  }
    2.10  
    2.11    def decode_type(tree: XML.Tree): Type =
    2.12    {
    2.13 @@ -52,16 +49,17 @@
    2.14  
    2.15    /* consts */
    2.16  
    2.17 -  sealed case class Const(entity: Entity, typ: Term.Typ, abbrev: Option[Term.Term])
    2.18 +  sealed case class Const(
    2.19 +    entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
    2.20  
    2.21    def decode_const(tree: XML.Tree): Const =
    2.22    {
    2.23      val (entity, body) = decode_entity(tree)
    2.24 -    val (typ, abbrev) =
    2.25 +    val (args, typ, abbrev) =
    2.26      {
    2.27        import XML.Decode._
    2.28 -      pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
    2.29 +      triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
    2.30      }
    2.31 -    Const(entity, typ, abbrev)
    2.32 +    Const(entity, args, typ, abbrev)
    2.33    }
    2.34  }