--- a/NEWS Sat May 26 22:11:55 2018 +0100
+++ b/NEWS Sat May 26 22:12:18 2018 +0100
@@ -372,8 +372,8 @@
$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
"isabelle jedit -s" or "isabelle build -s").
-* The command-line tool retrieves theory exports from the session build
-database.
+* The command-line tool "export" and 'export_files' in session ROOT
+entries retrieve theory exports from the session build database.
* The command-line tools "isabelle server" and "isabelle client" provide
access to the Isabelle Server: it supports responsive session management
--- a/src/Doc/System/Sessions.thy Sat May 26 22:11:55 2018 +0100
+++ b/src/Doc/System/Sessions.thy Sat May 26 22:12:18 2018 +0100
@@ -54,7 +54,7 @@
@{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline>
(@{syntax system_name} '+')? description? options? \<newline>
- (sessions?) (theories*) (document_files*)
+ (sessions?) (theories*) (document_files*) \<newline> (export_files*)
;
groups: '(' (@{syntax name} +) ')'
;
@@ -75,6 +75,8 @@
theory_entry: @{syntax system_name} ('(' @'global' ')')?
;
document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
+ ;
+ export_files: @'export_files' ('(' dir ')')? (@{syntax name}+)
\<close>}
\<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
@@ -138,12 +140,14 @@
directory to the document output directory, before formal document
processing is started (see also \secref{sec:tool-document}). The local path
structure of the \<open>files\<close> is preserved, which allows to reconstruct the
- original directory hierarchy of \<open>base_dir\<close>.
+ original directory hierarchy of \<open>base_dir\<close>. The default \<open>base_dir\<close> is
+ \<^verbatim>\<open>document\<close> within the session root directory.
- \<^descr> \isakeyword{document_files}~\<open>files\<close> abbreviates
- \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\
- document sources are taken from the base directory \<^verbatim>\<open>document\<close> within the
- session root directory.
+ \<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) patterns\<close> writes
+ theory exports to the file-system: the \<open>target_dir\<close> specification is
+ relative to the session root directory; its default is \<^verbatim>\<open>export\<close>. Exports
+ are selected via \<open>patterns\<close> as in @{tool_ref export}
+ (\secref{sec:tool-export}).
\<close>
@@ -562,7 +566,7 @@
-x PATTERN extract files matching pattern (e.g. "*:**" for all)
List or export theory exports for SESSION: named blobs produced by
- isabelle build. Option -l or -x is required.
+ isabelle build. Option -l or -x is required; option -x may be repeated.
The PATTERN language resembles glob patterns in the shell, with ? and *
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
@@ -583,7 +587,8 @@
pattern. Note that wild cards ``\<^verbatim>\<open>?\<close>'' and ``\<^verbatim>\<open>*\<close>'' do not match the
separators ``\<^verbatim>\<open>:\<close>'' and ``\<^verbatim>\<open>/\<close>''; the wild card \<^verbatim>\<open>**\<close> matches over directory
name hierarchies separated by ``\<^verbatim>\<open>/\<close>''. Thus the pattern ``\<^verbatim>\<open>*:**\<close>'' matches
- \<^emph>\<open>all\<close> theory exports.
+ \<^emph>\<open>all\<close> theory exports. Multiple options \<^verbatim>\<open>-x\<close> refer to the union of all
+ specified patterns.
Option \<^verbatim>\<open>-D\<close> specifies an alternative base directory for option \<^verbatim>\<open>-x\<close>: the
default is \<^verbatim>\<open>export\<close> within the current directory. Each theory creates its
--- a/src/Pure/General/position.scala Sat May 26 22:11:55 2018 +0100
+++ b/src/Pure/General/position.scala Sat May 26 22:12:18 2018 +0100
@@ -144,7 +144,7 @@
case (None, Some(name)) => "file " + quote(name)
case _ => ""
}
- val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else " " + s0
+ val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else s0
Markup(Markup.POSITION, pos).markup(s)
}
}
--- a/src/Pure/PIDE/session.scala Sat May 26 22:11:55 2018 +0100
+++ b/src/Pure/PIDE/session.scala Sat May 26 22:12:18 2018 +0100
@@ -386,9 +386,8 @@
prover.get.define_command(command)
}
}
- change.doc_edits foreach {
- case (_, edit) =>
- edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
+ for { (_, edit) <- change.doc_edits } {
+ edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) })
}
val assignment = global_state.value.the_assignment(change.previous).check_finished
--- a/src/Pure/Sessions.thy Sat May 26 22:11:55 2018 +0100
+++ b/src/Pure/Sessions.thy Sat May 26 22:12:18 2018 +0100
@@ -7,7 +7,8 @@
theory Sessions
imports Pure
keywords "session" :: thy_decl
- and "description" "options" "sessions" "theories" "document_files" :: quasi_command
+ and "description" "options" "sessions" "theories"
+ "document_files" "export_files" :: quasi_command
and "global"
begin
--- a/src/Pure/Thy/export.scala Sat May 26 22:11:55 2018 +0100
+++ b/src/Pure/Thy/export.scala Sat May 26 22:12:18 2018 +0100
@@ -153,12 +153,10 @@
/* database consumer thread */
- def consumer(db: SQL.Database): Consumer = new Consumer(db)
+ def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache)
- class Consumer private[Export](db: SQL.Database)
+ class Consumer private[Export](db: SQL.Database, cache: XZ.Cache)
{
- val xz_cache = XZ.make_cache()
-
private val export_errors = Synchronized[List[String]](Nil)
private val consumer =
@@ -176,7 +174,7 @@
})
def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
- consumer.send(make_entry(session_name, args, body, cache = xz_cache))
+ consumer.send(make_entry(session_name, args, body, cache = cache))
def shutdown(close: Boolean = false): List[String] =
{
@@ -187,6 +185,52 @@
}
+ /* export to file-system */
+
+ def export_files(
+ store: Sessions.Store,
+ session_name: String,
+ export_dir: Path,
+ progress: Progress = No_Progress,
+ export_list: Boolean = false,
+ export_patterns: List[String] = Nil,
+ export_prefix: String = "")
+ {
+ using(store.open_database(session_name))(db =>
+ {
+ db.transaction {
+ val export_names = read_theory_exports(db, session_name)
+
+ // list
+ if (export_list) {
+ (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
+ sorted.foreach(progress.echo(_))
+ }
+
+ // export
+ if (export_patterns.nonEmpty) {
+ val exports =
+ (for {
+ export_pattern <- export_patterns.iterator
+ matcher = make_matcher(export_pattern)
+ (theory_name, name) <- export_names if matcher(theory_name, name)
+ } yield (theory_name, name)).toSet
+ for {
+ (theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1)
+ name <- group.map(_._2).sorted
+ entry <- read_entry(db, session_name, theory_name, name)
+ } {
+ val path = export_dir + Path.basic(theory_name) + Path.explode(name)
+ progress.echo(export_prefix + "export " + path)
+ Isabelle_System.mkdirs(path.dir)
+ Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
+ }
+ }
+ }
+ })
+ }
+
+
/* Isabelle tool wrapper */
val default_export_dir = Path.explode("export")
@@ -201,7 +245,7 @@
var no_build = false
var options = Options.init()
var system_mode = false
- var export_pattern = ""
+ var export_patterns: List[String] = Nil
val getopts = Getopts("""
Usage: isabelle export [OPTIONS] SESSION
@@ -216,7 +260,7 @@
-x PATTERN extract files matching pattern (e.g. "*:**" for all)
List or export theory exports for SESSION: named blobs produced by
- isabelle build. Option -l or -x is required.
+ isabelle build. Option -l or -x is required; option -x may be repeated.
The PATTERN language resembles glob patterns in the shell, with ? and *
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
@@ -228,12 +272,12 @@
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
"s" -> (_ => system_mode = true),
- "x:" -> (arg => export_pattern = arg))
+ "x:" -> (arg => export_patterns ::= arg))
val more_args = getopts(args)
val session_name =
more_args match {
- case List(session_name) if export_list || export_pattern != "" => session_name
+ case List(session_name) if export_list || export_patterns.nonEmpty => session_name
case _ => getopts.usage()
}
@@ -256,37 +300,10 @@
}
- /* database */
+ /* export files */
val store = Sessions.store(options, system_mode)
-
- using(store.open_database(session_name))(db =>
- {
- db.transaction {
- val export_names = read_theory_exports(db, session_name)
-
- // list
- if (export_list) {
- (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
- sorted.foreach(Output.writeln(_, stdout = true))
- }
-
- // export
- if (export_pattern != "") {
- val xz_cache = XZ.make_cache()
-
- val matcher = make_matcher(export_pattern)
- for {
- (theory_name, name) <- export_names if matcher(theory_name, name)
- entry <- read_entry(db, session_name, theory_name, name)
- } {
- val path = export_dir + Path.basic(theory_name) + Path.explode(name)
- progress.echo("exporting " + path)
- Isabelle_System.mkdirs(path.dir)
- Bytes.write(path, entry.uncompressed(cache = xz_cache))
- }
- }
- }
- })
+ export_files(store, session_name, export_dir, progress = progress,
+ export_list = export_list, export_patterns = export_patterns)
})
}
--- a/src/Pure/Thy/export_theory.ML Sat May 26 22:11:55 2018 +0100
+++ b/src/Pure/Thy/export_theory.ML Sat May 26 22:12:18 2018 +0100
@@ -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;
--- a/src/Pure/Thy/export_theory.scala Sat May 26 22:11:55 2018 +0100
+++ b/src/Pure/Thy/export_theory.scala Sat May 26 22:12:18 2018 +0100
@@ -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,
--- a/src/Pure/Thy/sessions.ML Sat May 26 22:11:55 2018 +0100
+++ b/src/Pure/Thy/sessions.ML Sat May 26 22:12:18 2018 +0100
@@ -27,15 +27,18 @@
val theories =
Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry);
+val in_path =
+ Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.position Parse.path --| Parse.$$$ ")");
+
val document_files =
Parse.$$$ "document_files" |--
- Parse.!!!
- (Scan.optional
- (Parse.$$$ "(" |--
- Parse.!!! (Parse.$$$ "in" |-- Parse.position Parse.path --| Parse.$$$ ")"))
- ("document", Position.none)
+ Parse.!!! (Scan.optional in_path ("document", Position.none)
-- Scan.repeat1 (Parse.position Parse.path));
+val export_files =
+ Parse.$$$ "export_files" |--
+ Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.name);
+
in
val command_parser =
@@ -49,9 +52,10 @@
Scan.optional (Parse.$$$ "sessions" |--
Parse.!!! (Scan.repeat1 (Parse.position Parse.session_name))) [] --
Scan.repeat theories --
- Scan.repeat document_files))
+ Scan.repeat document_files --
+ Scan.repeat export_files))
>> (fn (((session, _), dir),
- ((((((parent, descr), options), sessions), theories), document_files))) =>
+ (((((((parent, descr), options), sessions), theories), document_files), export_files))) =>
Toplevel.keep (fn state =>
let
val ctxt = Toplevel.context_of state;
@@ -89,6 +93,10 @@
val dir = Resources.check_dir ctxt session_dir doc_dir;
val _ = List.app (ignore o Resources.check_file ctxt dir) doc_files;
in () end);
+
+ val _ =
+ export_files |> List.app (fn (export_dir, _) =>
+ ignore (Resources.check_path ctxt session_dir export_dir));
in () end));
end;
--- a/src/Pure/Thy/sessions.scala Sat May 26 22:11:55 2018 +0100
+++ b/src/Pure/Thy/sessions.scala Sat May 26 22:12:18 2018 +0100
@@ -428,7 +428,8 @@
options = Nil,
imports = info.deps,
theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))),
- document_files = Nil))))
+ document_files = Nil,
+ export_files = Nil))))
}
}
else (session, Nil)
@@ -469,6 +470,7 @@
theories: List[(Options, List[(String, Position.T)])],
global_theories: List[String],
document_files: List[(Path, Path)],
+ export_files: List[(Path, List[String])],
meta_digest: SHA1.Digest)
{
def deps: List[String] = parent.toList ::: imports
@@ -520,13 +522,16 @@
val document_files =
entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
+ val export_files =
+ entry.export_files.map({ case (dir, pats) => (Path.explode(dir), pats) })
+
val meta_digest =
SHA1.digest((name, chapter, entry.parent, entry.options, entry.imports,
- entry.theories_no_position, conditions, entry.document_files).toString)
+ entry.theories_no_position, conditions, entry.document_files, entry.export_files).toString)
Info(name, chapter, dir_selected, entry.pos, entry.groups,
dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
- entry.imports, theories, global_theories, document_files, meta_digest)
+ entry.imports, theories, global_theories, document_files, export_files, meta_digest)
}
catch {
case ERROR(msg) =>
@@ -703,6 +708,7 @@
private val THEORIES = "theories"
private val GLOBAL = "global"
private val DOCUMENT_FILES = "document_files"
+ private val EXPORT_FILES = "export_files"
val root_syntax =
Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
@@ -712,7 +718,8 @@
(OPTIONS, Keyword.QUASI_COMMAND) +
(SESSIONS, Keyword.QUASI_COMMAND) +
(THEORIES, Keyword.QUASI_COMMAND) +
- (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
+ (DOCUMENT_FILES, Keyword.QUASI_COMMAND) +
+ (EXPORT_FILES, Keyword.QUASI_COMMAND)
abstract class Entry
sealed case class Chapter(name: String) extends Entry
@@ -726,7 +733,8 @@
options: List[Options.Spec],
imports: List[String],
theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
- document_files: List[(String, String)]) extends Entry
+ document_files: List[(String, String)],
+ export_files: List[(String, List[String])]) extends Entry
{
def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
@@ -759,11 +767,15 @@
((options | success(Nil)) ~ rep1(theory_entry)) ^^
{ case _ ~ (x ~ y) => (x, y) }
+ val in_path = $$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^ { case _ ~ (_ ~ x ~ _) => x }
+
val document_files =
$$$(DOCUMENT_FILES) ~!
- (($$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^
- { case _ ~ (_ ~ x ~ _) => x } | success("document")) ~
- rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
+ ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
+
+ val export_files =
+ $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ rep1(name)) ^^
+ { case _ ~ (x ~ y) => (x, y) }
command(SESSION) ~!
(position(session_name) ~
@@ -775,9 +787,10 @@
(($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
(($$$(SESSIONS) ~! rep1(session_name) ^^ { case _ ~ x => x }) | success(Nil)) ~
rep(theories) ~
- (rep(document_files) ^^ (x => x.flatten))))) ^^
- { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
- Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
+ (rep(document_files) ^^ (x => x.flatten)) ~
+ (rep(export_files))))) ^^
+ { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j))) =>
+ Session_Entry(pos, a, b, c, d, e, f, g, h, i, j) }
}
def parse_root(path: Path): List[Entry] =
@@ -1079,8 +1092,8 @@
/* SQL database content */
- val xml_cache = XML.make_cache()
- val xz_cache = XZ.make_cache()
+ val xml_cache: XML.Cache = XML.make_cache()
+ val xz_cache: XZ.Cache = XZ.make_cache()
def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
db.using_statement(Session_Info.table.select(List(column),
--- a/src/Pure/Tools/build.scala Sat May 26 22:11:55 2018 +0100
+++ b/src/Pure/Tools/build.scala Sat May 26 22:12:18 2018 +0100
@@ -189,7 +189,8 @@
isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
private val export_tmp_dir = Isabelle_System.tmp_dir("export")
- private val export_consumer = Export.consumer(store.open_database(name, output = true))
+ private val export_consumer =
+ Export.consumer(store.open_database(name, output = true), cache = store.xz_cache)
private val future_result: Future[Process_Result] =
Future.thread("build") {
@@ -321,8 +322,15 @@
Isabelle_System.rm_tree(export_tmp_dir)
- if (result1.ok)
+ if (result1.ok) {
+ for ((dir, pats) <- info.export_files) {
+ Export.export_files(store, name, info.dir + dir,
+ progress = if (verbose) progress else No_Progress,
+ export_patterns = pats,
+ export_prefix = name + ": ")
+ }
Present.finish(progress, store.browser_info, graph_file, info, name)
+ }
graph_file.delete
--- a/src/Pure/sorts.ML Sat May 26 22:11:55 2018 +0100
+++ b/src/Pure/sorts.ML Sat May 26 22:12:18 2018 +0100
@@ -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}) =