# HG changeset patch # User wenzelm # Date 1527364945 -7200 # Node ID 781a98696638cb04c35bd9dd5f52aeacf018b158 # Parent 0f513ae3db77c413355267f87e4fe04b553070c2 export sort algebra; diff -r 0f513ae3db77 -r 781a98696638 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sat May 26 21:24:07 2018 +0200 +++ b/src/Pure/Thy/export_theory.ML Sat May 26 22:02:25 2018 +0200 @@ -141,6 +141,24 @@ export_entities "classes" (fn name => fn () => export_class name) Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig))))); - in () end); + + (* sort algebra *) + + val {classrel, arities} = + Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents) + (#2 (#classes rep_tsig)); + + val encode_classrel = + let open XML.Encode + in list (pair string (list string)) end; + + val encode_arities = + let open XML.Encode Term_XML.Encode + in list (triple string (list sort) string) end; + + val _ = if null classrel then () else export_body thy "classrel" (encode_classrel classrel); + val _ = if null arities then () else export_body thy "arities" (encode_arities arities); + + in () end); end; diff -r 0f513ae3db77 -r 781a98696638 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Sat May 26 21:24:07 2018 +0200 +++ b/src/Pure/Thy/export_theory.scala Sat May 26 22:02:25 2018 +0200 @@ -31,6 +31,8 @@ facts: Boolean = true, classes: Boolean = true, typedefs: Boolean = true, + classrel: Boolean = true, + arities: Boolean = true, cache: Term.Cache = Term.make_cache()): Session = { val thys = @@ -64,7 +66,9 @@ axioms: List[Axiom], facts: List[Fact], classes: List[Class], - typedefs: List[Typedef]) + typedefs: List[Typedef], + classrel: List[Classrel], + arities: List[Arity]) { override def toString: String = name @@ -76,10 +80,13 @@ axioms.map(_.cache(cache)), facts.map(_.cache(cache)), classes.map(_.cache(cache)), - typedefs.map(_.cache(cache))) + typedefs.map(_.cache(cache)), + classrel.map(_.cache(cache)), + arities.map(_.cache(cache))) } - def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil) + def empty_theory(name: String): Theory = + Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil) def read_theory(db: SQL.Database, session_name: String, theory_name: String, types: Boolean = true, @@ -88,6 +95,8 @@ facts: Boolean = true, classes: Boolean = true, typedefs: Boolean = true, + classrel: Boolean = true, + arities: Boolean = true, cache: Option[Term.Cache] = None): Theory = { val parents = @@ -104,7 +113,9 @@ if (axioms) read_axioms(db, session_name, theory_name) else Nil, if (facts) read_facts(db, session_name, theory_name) else Nil, if (classes) read_classes(db, session_name, theory_name) else Nil, - if (typedefs) read_typedefs(db, session_name, theory_name) else Nil) + if (typedefs) read_typedefs(db, session_name, theory_name) else Nil, + if (classrel) read_classrel(db, session_name, theory_name) else Nil, + if (arities) read_arities(db, session_name, theory_name) else Nil) if (cache.isDefined) theory.cache(cache.get) else theory } @@ -281,6 +292,46 @@ }) + /* sort algebra */ + + sealed case class Classrel(class_name: String, super_names: List[String]) + { + def cache(cache: Term.Cache): Classrel = + Classrel(cache.string(class_name), super_names.map(cache.string(_))) + } + + def read_classrel(db: SQL.Database, session_name: String, theory_name: String): List[Classrel] = + read_export(db, session_name, theory_name, "classrel", + (body: XML.Body) => + { + val classrel = + { + import XML.Decode._ + list(pair(string, list(string)))(body) + } + for ((c, cs) <- classrel) yield Classrel(c, cs) + }) + + sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String) + { + def cache(cache: Term.Cache): Arity = + Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain)) + } + + def read_arities(db: SQL.Database, session_name: String, theory_name: String): List[Arity] = + read_export(db, session_name, theory_name, "arities", + (body: XML.Body) => + { + val arities = + { + import XML.Decode._ + import Term_XML.Decode._ + list(triple(string, list(sort), string))(body) + } + for ((a, b, c) <- arities) yield Arity(a, b, c) + }) + + /* HOL typedefs */ sealed case class Typedef(name: String, diff -r 0f513ae3db77 -r 781a98696638 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Sat May 26 21:24:07 2018 +0200 +++ b/src/Pure/sorts.ML Sat May 26 22:02:25 2018 +0200 @@ -43,6 +43,9 @@ val add_arities: Context.generic -> string * (class * sort list) list -> algebra -> algebra val empty_algebra: algebra val merge_algebra: Context.generic -> algebra * algebra -> algebra + val dest_algebra: algebra list -> algebra -> + {classrel: (class * class list) list, + arities: (string * sort list * class) list} val subalgebra: Context.generic -> (class -> bool) -> (class * string -> sort list option) -> algebra -> (sort -> sort) * algebra type class_error @@ -299,6 +302,26 @@ in make_algebra (classes', arities') end; +(* destruct *) + +fun dest_algebra parents (Algebra {classes, arities}) = + let + fun new_classrel rel = not (exists (fn algebra => class_less algebra rel) parents); + val classrel = + (classes, []) |-> Graph.fold (fn (c, (_, (_, ds))) => + (case filter (fn d => new_classrel (c, d)) (Graph.Keys.dest ds) of + [] => I + | ds' => cons (c, sort_strings ds'))) + |> sort_by #1; + + fun is_arity t ar algebra = member (op =) (Symtab.lookup_list (arities_of algebra) t) ar; + fun add_arity t (c, Ss) = not (exists (is_arity t (c, Ss)) parents) ? cons (t, Ss, c); + val arities = + (arities, []) |-> Symtab.fold (fn (t, ars) => fold_rev (add_arity t) (sort_by #1 ars)) + |> sort_by #1; + in {classrel = classrel, arities = arities} end; + + (* algebra projections *) (* FIXME potentially violates abstract type integrity *) fun subalgebra context P sargs (algebra as Algebra {classes, arities}) =