clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
authorwenzelm
Sat Jul 20 12:52:29 2019 +0200 (3 months ago)
changeset 703848ce08b154aa1
parent 70383 38ac2e714729
child 70385 68d2c533db9c
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
src/Pure/logic.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sat Jul 20 11:48:30 2019 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sat Jul 20 12:52:29 2019 +0200
     1.3 @@ -325,16 +325,24 @@
     1.4        Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
     1.5          (#2 (#classes rep_tsig));
     1.6  
     1.7 +    val encode_prop0 =
     1.8 +      encode_axiom Name.context o Logic.varify_global;
     1.9 +
    1.10      val encode_classrel =
    1.11        let open XML.Encode
    1.12 -      in list (pair string (list string)) end;
    1.13 +      in list (pair encode_prop0 (pair string string)) end;
    1.14  
    1.15      val encode_arities =
    1.16        let open XML.Encode Term_XML.Encode
    1.17 -      in list (triple string (list sort) string) end;
    1.18 +      in list (pair encode_prop0 (triple string (list sort) string)) end;
    1.19 +
    1.20 +    val export_classrel =
    1.21 +      maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel;
    1.22  
    1.23 -    val _ = if null classrel then () else export_body thy "classrel" (encode_classrel classrel);
    1.24 -    val _ = if null arities then () else export_body thy "arities" (encode_arities arities);
    1.25 +    val export_arities = map (`Logic.mk_arity) #> encode_arities;
    1.26 +
    1.27 +    val _ = if null classrel then () else export_body thy "classrel" (export_classrel classrel);
    1.28 +    val _ = if null arities then () else export_body thy "arities" (export_arities arities);
    1.29  
    1.30  
    1.31      (* locales *)
     2.1 --- a/src/Pure/Thy/export_theory.scala	Sat Jul 20 11:48:30 2019 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Sat Jul 20 12:52:29 2019 +0200
     2.3 @@ -440,10 +440,10 @@
     2.4  
     2.5    /* sort algebra */
     2.6  
     2.7 -  sealed case class Classrel(class_name: String, super_names: List[String])
     2.8 +  sealed case class Classrel(class1: String, class2: String, prop: Prop)
     2.9    {
    2.10      def cache(cache: Term.Cache): Classrel =
    2.11 -      Classrel(cache.string(class_name), super_names.map(cache.string(_)))
    2.12 +      Classrel(cache.string(class1), cache.string(class2), prop.cache(cache))
    2.13    }
    2.14  
    2.15    def read_classrel(provider: Export.Provider): List[Classrel] =
    2.16 @@ -452,15 +452,16 @@
    2.17      val classrel =
    2.18      {
    2.19        import XML.Decode._
    2.20 -      list(pair(string, list(string)))(body)
    2.21 +      list(pair(decode_prop, pair(string, string)))(body)
    2.22      }
    2.23 -    for ((c, cs) <- classrel) yield Classrel(c, cs)
    2.24 +    for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop)
    2.25    }
    2.26  
    2.27 -  sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String)
    2.28 +  sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String, prop: Prop)
    2.29    {
    2.30      def cache(cache: Term.Cache): Arity =
    2.31 -      Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain))
    2.32 +      Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain),
    2.33 +        prop.cache(cache))
    2.34    }
    2.35  
    2.36    def read_arities(provider: Export.Provider): List[Arity] =
    2.37 @@ -470,9 +471,9 @@
    2.38      {
    2.39        import XML.Decode._
    2.40        import Term_XML.Decode._
    2.41 -      list(triple(string, list(sort), string))(body)
    2.42 +      list(pair(decode_prop, triple(string, list(sort), string)))(body)
    2.43      }
    2.44 -    for ((a, b, c) <- arities) yield Arity(a, b, c)
    2.45 +    for ((prop, (a, b, c)) <- arities) yield Arity(a, b, c, prop)
    2.46    }
    2.47  
    2.48  
     3.1 --- a/src/Pure/logic.ML	Sat Jul 20 11:48:30 2019 +0200
     3.2 +++ b/src/Pure/logic.ML	Sat Jul 20 12:52:29 2019 +0200
     3.3 @@ -54,6 +54,7 @@
     3.4    val name_arities: arity -> string list
     3.5    val name_arity: string * sort list * class -> string
     3.6    val mk_arities: arity -> term list
     3.7 +  val mk_arity: string * sort list * class -> term
     3.8    val dest_arity: term -> string * sort list * class
     3.9    val unconstrainT: sort list -> term ->
    3.10      ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
    3.11 @@ -319,6 +320,8 @@
    3.12    let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss))
    3.13    in map (fn c => mk_of_class (T, c)) S end;
    3.14  
    3.15 +fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c]));
    3.16 +
    3.17  fun dest_arity tm =
    3.18    let
    3.19      fun err () = raise TERM ("dest_arity", [tm]);