From 7026337b6edf6577aaabfeaded699ccd4ef2cce6 Mon Sep 17 00:00:00 2001 From: ComFreek Date: Sat, 13 Apr 2024 17:28:36 +0200 Subject: [PATCH] diag-ops [skip ci] --- .../mmt/api/modules/diagrams/Diagram.scala | 10 +- .../mmt/api/modules/diagrams/NewStuff.scala | 292 +++++++++++------- .../api/presentation/MMTSyntaxPresenter.scala | 3 +- src/test/DiagramOperatorTest.scala | 4 +- 4 files changed, 190 insertions(+), 119 deletions(-) diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/Diagram.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/Diagram.scala index 38f5feb2c..0cf302ec4 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/Diagram.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/Diagram.scala @@ -194,10 +194,14 @@ object DiagramConnection { object Singleton { def apply(domTheory: MPath, codTheory: MPath, mor: Term): DiagramConnection = { - DiagramConnection( + new DiagramConnection( DiagramFunctor(Diagram(List(domTheory)), Diagram(List(codTheory)), Map(domTheory -> OMMOD(codTheory))), - Map(domTheory -> mor) - ) + Map(domTheory -> mor)) { + override def applyTheory(thy: MPath): Term = thy match { + case `domTheory` => mor + case _ => OMCOMP(OMIDENT(OMMOD(thy)), mor) // i.e., mor domain-restricted to thy + } + } } def unapply(connection: DiagramConnection): Option[(MPath, MPath, Term)] = connection match { diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/NewStuff.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/NewStuff.scala index d6083a5d7..a625db1fd 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/NewStuff.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/NewStuff.scala @@ -1,6 +1,6 @@ package info.kwarc.mmt.api.modules.diagrams -import info.kwarc.mmt.api.{ComplexStep, GeneratedFrom, ImplementationError, InvalidElement, LocalName, MPath} +import info.kwarc.mmt.api.{ComplexStep, GeneratedFrom, ImplementationError, InvalidElement, LocalName, MPath, SimpleStep} import info.kwarc.mmt.api.frontend.Controller import info.kwarc.mmt.api.libraries.Lookup import info.kwarc.mmt.api.modules.{Module, ModuleOrLink, Theory, View} @@ -23,123 +23,181 @@ trait Blah { s"operator spec with unknown key.")) } - abstract class LinearOperatorSpec(val key: Option[String]) { - def apply(m: MPath): MPath + abstract class LinearOperatorSpec(val key: Option[String], val renamer: MPath => MPath) { + def apply(m: MPath): MPath = renamer(m) } sealed trait UnresolvedLinearOperatorSpec { val key: Option[String] + val renamer: MPath => MPath } def resolve(u: List[UnresolvedLinearOperatorSpec]): LinearOperatorSpecs = { LinearOperatorSpecs(u.map { - case op@LinearFunctorSpec(_, _, _, _) => op - case UnresolvedLinearConnectorSpec(key, dom, cod, metaConnector) => + case op@LinearFunctorSpec(_, _, _, _, _) => op + case UnresolvedLinearConnectorSpec(key, dom, cod, metaConnector, renamer) => def resolve_(x: Either[String, LinearFunctorSpec]): LinearFunctorSpec = x match { case Left(searchKey) => u.find(_.key.contains(searchKey)).get.asInstanceOf[LinearFunctorSpec] case Right(givenOp) => givenOp } - LinearConnectorSpec(key, resolve_(dom), resolve_(cod), metaConnector) + LinearConnectorSpec(key, resolve_(dom), resolve_(cod), metaConnector, renamer) }) } - case class LinearFunctorSpec(override val key: Option[String], dom: Diagram, cod: Diagram, metaFunctor: DiagramFunctor) extends LinearOperatorSpec(key) with UnresolvedLinearOperatorSpec { + case class LinearFunctorSpec(override val key: Option[String], + dom: Diagram, + cod: Diagram, + metaFunctor: DiagramFunctor, + override val renamer: MPath => MPath) + extends LinearOperatorSpec(key, renamer) with UnresolvedLinearOperatorSpec { + def applyDomain(m: MPath): MPath = metaFunctor(m).toMPath + } - override def apply(m: MPath): MPath = m.doc ? m.name.suffixLastSimple(key.get) + def suffixBy(str: String): MPath => MPath = m => { + val newName = LocalName(m.name.steps.map { + case SimpleStep(x) => SimpleStep(x + str) + case ComplexStep(path) => ComplexStep(suffixBy(str)(path)) // todo: is this correct for nested modules? + }) + m.doc ? newName } + object IdentityFunctorSpec { - def apply(dom: Diagram): LinearFunctorSpec = new LinearFunctorSpec(None, dom, dom, DiagramFunctor.identity(dom)) { - override def apply(m: MPath): MPath = m - } + def apply(dom: Diagram): LinearFunctorSpec = new LinearFunctorSpec(None, dom, dom, DiagramFunctor.identity(dom), x => x) } - case class LinearConnectorSpec(override val key: Option[String], dom: LinearFunctorSpec, cod: LinearFunctorSpec, metaConnector: DiagramConnection) extends LinearOperatorSpec(key) { + case class LinearConnectorSpec(override val key: Option[String], + dom: LinearFunctorSpec, + cod: LinearFunctorSpec, + metaConnector: DiagramConnection, + override val renamer: MPath => MPath) extends LinearOperatorSpec(key, renamer) { // this needs to return a Term (instead of a mere MPath) to allow for constructs of the form OMIDENT(thy) def applyDomain(m: MPath): Term = metaConnector.applyTheory(m) - - override def apply(m: MPath): MPath = m.doc ? m.name.suffixLastSimple(key.get) } - case class UnresolvedLinearConnectorSpec(override val key: Option[String], dom: Either[String, LinearFunctorSpec], cod: Either[String, LinearFunctorSpec], metaConnector: DiagramConnection) extends UnresolvedLinearOperatorSpec + case class UnresolvedLinearConnectorSpec(override val key: Option[String], + dom: Either[String, LinearFunctorSpec], + cod: Either[String, LinearFunctorSpec], + metaConnector: DiagramConnection, + override val renamer: MPath => MPath) extends UnresolvedLinearOperatorSpec + + /** DSL BEGIN **/ - implicit def any2ArrowAssoc(x: (String, (Diagram, Diagram), DiagramFunctor)): LinearFunctorSpec = - LinearFunctorSpec(Some(x._1), x._2._1, x._2._2, x._3) + implicit def functorTupleToSpec(x: (String, (Diagram, Diagram), DiagramFunctor, MPath => MPath)): LinearFunctorSpec = + LinearFunctorSpec(Some(x._1), x._2._1, x._2._2, x._3, x._4) - implicit def anyasd(x: (String, (LinearFunctorSpec, String), DiagramConnection)): UnresolvedLinearConnectorSpec = - UnresolvedLinearConnectorSpec(Some(x._1), dom = Right(x._2._1), cod = Left(x._2._2), x._3) + implicit def connectorTupleToSpec(x: (String, (LinearFunctorSpec, String), DiagramConnection, MPath => MPath)): UnresolvedLinearConnectorSpec = + UnresolvedLinearConnectorSpec(Some(x._1), dom = Right(x._2._1), cod = Left(x._2._2), x._3, x._4) def Id(m: MPath): LinearFunctorSpec = IdentityFunctorSpec(Diagram.singleton(m)) + def getRenamer(opKey: String)(f: String => String)(implicit interp: DiagramInterpreter): LocalName => LocalName = { + val op = ops(opKey).asInstanceOf[LinearFunctorSpec] + + n => LocalName(n.steps map { + case SimpleStep(x) => SimpleStep(f(x)) + case ComplexStep(m) if op.dom.hasImplicitFrom(m)(interp.ctrl.library) => + ComplexStep(op.applyDomain(m)) + case ComplexStep(m) => + ComplexStep(op(m)) + }) + } + def getEquinamer(opKey: String)(implicit interp: DiagramInterpreter): LocalName => LocalName = getRenamer(opKey)(x => x) + + /** DSL END **/ + /** + * invariant: idempotent, i.e., when called more than once on the same theory, always returns the same existing result. + */ protected def beginTheory(thy: Theory)(implicit interp: DiagramInterpreter): List[ModuleOrLink] = { ops.specs map { - case op@LinearFunctorSpec(_, dom, cod, _) => + case op@LinearFunctorSpec(_, dom, _, _, _) => val newThyPath = op(thy.path) - val newMeta = thy.meta.map { - case mt if op.dom.hasImplicitFrom(mt)(interp.ctrl.library) => // meta theory is subsumed by functor's domain - op.applyDomain(mt) - - case mt => // otherwise, recurse into meta theory - if (applyModule(interp.ctrl.getModule(mt)).isEmpty) { - interp.errorCont(InvalidElement(thy, s"Theory had meta theory `$mt` for which there " + - s"was no implicit morphism into `$dom`. Recursing into meta theory as usual " + - s"failed, too; reasons are probably logged above. Keeping meta theory as-is.")) - mt - } else { - op(mt) - } - } - val newThy = Theory.empty(newThyPath.doc, newThyPath.name, newMeta) - newThy.setOrigin(GeneratedFrom(thy.path, this, None)) - interp.add(newThy) + if (interp.ctrl.getAsO(classOf[Theory], newThyPath).nonEmpty) { + interp.ctrl.getTheory(newThyPath) + } else { + val newMeta = thy.meta.map { + case mt if op.dom.hasImplicitFrom(mt)(interp.ctrl.library) => // meta theory is subsumed by functor's domain + op.applyDomain(mt) + + case mt => // otherwise, recurse into meta theory + if (applyModule(interp.ctrl.getModule(mt)).isEmpty) { + interp.errorCont(InvalidElement(thy, s"Theory had meta theory `$mt` for which there " + + s"was no implicit morphism into `$dom`. Recursing into meta theory as usual " + + s"failed, too; reasons are probably logged above. Keeping meta theory as-is.")) + mt + } else { + op(mt) + } + } + + val newThy = Theory.empty(newThyPath.doc, newThyPath.name, newMeta) + newThy.setOrigin(GeneratedFrom(thy.path, this, None)) + interp.add(newThy) - newThy + newThy + } - case op@LinearConnectorSpec(_, dom, cod, _) => + case op@LinearConnectorSpec(_, dom, cod, _, _) => val newMorPath = op(thy.path) - val newMor = View( - newMorPath.doc, newMorPath.name, - from = OMMOD(dom(thy.path)), - to = OMMOD(cod(thy.path)), - isImplicit = false - ) - newMor.setOrigin(GeneratedFrom(thy.path, this, None)) - interp.add(newMor) + if (interp.ctrl.getAsO(classOf[Module], newMorPath).nonEmpty) { + interp.ctrl.getModule(newMorPath) + } else { + val newMor = View( + newMorPath.doc, newMorPath.name, + from = OMMOD(dom(thy.path)), + to = OMMOD(cod(thy.path)), + isImplicit = false + ) + newMor.setOrigin(GeneratedFrom(thy.path, this, None)) + interp.add(newMor) - newMor + newMor + } } } + /** + * invariant: idempotent, i.e., when called more than once on the same view, always returns the same existing result. + */ protected def beginView(view: View)(implicit interp: DiagramInterpreter): List[View] = { ops.specs flatMap { - case op@LinearFunctorSpec(_, dom, cod, _) => + case op@LinearFunctorSpec(_, _, _, _, _) => if (applyModule(interp.ctrl.getModule(view.from.toMPath)).isEmpty) { None } else if (applyModule(interp.ctrl.getModule(view.to.toMPath)).isEmpty) { None } else { val newMorPath = op(view.path) - val newMor = View( - newMorPath.doc, newMorPath.name, - OMMOD(op(view.from.toMPath)), OMMOD(op(view.to.toMPath)), - view.isImplicit - ) - newMor.setOrigin(GeneratedFrom(view.path, this, None)) - interp.add(newMor) - Some(newMor) + if (interp.ctrl.getAsO(classOf[View], newMorPath).nonEmpty) { + Some(interp.ctrl.getAs(classOf[View], newMorPath)) + } else { + val newMor = View( + newMorPath.doc, newMorPath.name, + OMMOD(op(view.from.toMPath)), OMMOD(op(view.to.toMPath)), + view.isImplicit + ) + + newMor.setOrigin(GeneratedFrom(view.path, this, None)) + interp.add(newMor) + Some(newMor) + } } - case LinearConnectorSpec(_, _, _, _) => + case LinearConnectorSpec(_, _, _, _, _) => // todo(diagop-mor-equality): theoretically, we could output morphism equality // but the MMT system does not yet support native statements of morphism equality None } } + /** + * Applies the operators to a module. + * This method is idempotent, calling it more than once will result in returning of the existing result. + */ final def applyModule(m: Module)(implicit interp: DiagramInterpreter): List[ModuleOrLink] = { // force elaboration on input module (among other things, this makes sure the implicit graph // related to inModule gets constructed) @@ -172,18 +230,26 @@ trait Blah { val ctrl = interp.ctrl implicit val library: Lookup = ctrl.library + // general behavior: + // ignore includes that go above the domain operator's meta diagram + // e.g., if we have a linear functor op: {LF} -> {S}, i.e., on the singleton diagram containing the LF theory + // to the singleton diagram containing some theory S, then when op processes theories like + // T = {include LF, include Lambda, ...}, it will simply ignore `include Lambda` and do nothing on that + // particular declaration. + ops.specs foreach { - case op@LinearFunctorSpec(_, dom, _, _) => + case op@LinearFunctorSpec(_, dom, _, _, _) => if (include.args.nonEmpty) throw new NotImplementedError("Parametric includes not supported by linear diagram operators yet") - def handleFrom(from: MPath): Term = { - if (dom.hasImplicitFrom(from)) OMMOD(op.applyDomain(from)) - else { - // recurse into include's domain module + def handleFrom(from: MPath): Option[Term] = { + if (dom.hasImplicitFrom(from)) { + op.metaFunctor.functor.get(from) // in case of None: will lead to current include being ignored below + } + else { // recurse into include's domain module applyModule(ctrl.getModule(from)) // todo(diagop-state): inheritState(container.modulePath, from) - OMMOD(op(from)) + Some(OMMOD(op(from))) } } @@ -193,48 +259,44 @@ trait Blah { case _ => ??? } - val newFrom = handleFrom(include.from) - val newDf = include.df.map(handleDf) - - val s = Structure( - home = OMMOD(op(container.modulePath)), - name = LocalName(newFrom.toMPath), - from = newFrom, - df = newDf, - isImplicit = if (container.isInstanceOf[Theory]) true else false, // theory includes are always implicit - isTotal = include.total - ) - s.setOrigin(GeneratedFrom(structure.path, this, None)) - - // TODO hack to prevent: "add error: a declaration for the name [...] already exists [...]" - // when refactoring the whole framework, we should fix this anyway in the course of doing so - if (ctrl.getO(s.path).isEmpty) { - interp.add(s) - interp.endAdd(s) - } + handleFrom(include.from).foreach(newFrom => { + val newDf = include.df.map(handleDf) - case op@LinearConnectorSpec(_, dom, _, _) => + val s = Structure( + home = OMMOD(op(container.modulePath)), + name = LocalName(newFrom.toMPath), + from = newFrom, + df = newDf, + isImplicit = if (container.isInstanceOf[Theory]) true else false, // theory includes are always implicit + isTotal = include.total + ) + s.setOrigin(GeneratedFrom(structure.path, this, None)) + + // TODO hack to prevent: "add error: a declaration for the name [...] already exists [...]" + // when refactoring the whole framework, we should fix this anyway in the course of doing so + if (ctrl.getO(s.path).isEmpty) { + interp.add(s) + interp.endAdd(s) + } + }) + + case op@LinearConnectorSpec(_, dom, _, _, _) => if (include.df.nonEmpty) { // todo(diagop-mor-equality): theoretically, we could output morphism equality // but the MMT system does not yet support native statements of morphism equality } else if (include.args.nonEmpty) { throw new NotImplementedError("Parametric includes not supported by linear diagram operators yet") } else { - val newData: Option[(MPath, Term)] = include.from match { - case from if dom.dom.hasImplicitFrom(from) => // assumed invariant dom.dom == cod.dom - // only create the actually necessary includes - // TODO hacky work around here, see discussion at https://mattermost.kwarc.info/kwarc/pl/opp88dhc57g4zmhyfzr7gyqixr - // if (library.hasImplicit(op.dom.applyDomain(from), dom(container.path.toMPath))) { - // None - //} else { - Some((dom.applyDomain(from), op.applyDomain(from))) - // } - - case from => - // recurse into include domain - applyModule(ctrl.getModule(from)) - // todo(diagop-state): inheritState(container.path, m.path) - Some((dom(from), OMMOD(op(from)))) + val from = include.from + val newData: Option[(MPath, Term)] = if (dom.dom.hasImplicitFrom(from)) { // assumed invariant dom.dom == cod.dom + dom.metaFunctor.functor.get(from).map(newFrom => { + (newFrom.toMPath, op.applyDomain(from)) + }) // in case of None: will lead to current include being ignored below + } else { + // recurse into include domain + applyModule(ctrl.getModule(from)) + // todo(diagop-state): inheritState(container.path, m.path) + Some((dom(from), OMMOD(op(from)))) } newData match { @@ -264,17 +326,18 @@ trait Blah { class NewPushout(m: Term, dom: MPath, cod: MPath) extends Blah { override val ops: LinearOperatorSpecs = resolve(List( - ("P", Diagram.singleton(dom) -> Diagram.singleton(cod), DiagramFunctor.singleton(dom, cod)), - ("in", Id(dom) -> "P", DiagramConnection.Singleton(dom, cod, m)) + ("P", Diagram.singleton(dom) -> Diagram.singleton(cod), DiagramFunctor.singleton(dom, cod), suffixBy("_Pushout")), + ("in", Id(dom) -> "P", DiagramConnection.Singleton(dom, cod, m), suffixBy("_Projection")) )) def applyConstant(c: Constant, container: ModuleOrLink)(implicit interp: DiagramInterpreter): Unit = { def tr(t: Term): Term = interp.ctrl.library.ApplyMorphs(t, OMMOD(ops("in")(c.parent))) + val equinamer = getEquinamer("P") val newC = new FinalConstant( home = OMMOD(ops("P")(c.parent)), - name = c.name, - alias = c.alias, + name = equinamer(c.name), + alias = c.alias map equinamer, tpC = c.tpC.map(tr), dfC = c.dfC.map(tr), rl = c.rl, @@ -282,17 +345,18 @@ class NewPushout(m: Term, dom: MPath, cod: MPath) extends Blah { vs = c.vs ) newC.metadata.add(c.metadata.getAll : _*) - - val cAssignment = Constant( - home = OMMOD(ops("in")(c.parent)), - name = LocalName(ComplexStep(c.parent) :: c.name), - alias = Nil, - tp = c.tpC.map(tr).get, - df = Some(newC.toTerm), - rl = None - ) - interp.add(newC) - interp.add(cAssignment) + + if (c.df.isEmpty) { + val cAssignment = Constant( + home = OMMOD(ops("in")(c.parent)), + name = LocalName(ComplexStep(c.parent) :: c.name), + alias = Nil, + tp = c.tpC.map(tr).get, + df = Some(newC.toTerm), + rl = None + ) + interp.add(cAssignment) + } } } diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/presentation/MMTSyntaxPresenter.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/presentation/MMTSyntaxPresenter.scala index aa09dcc48..a25b7fc92 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/presentation/MMTSyntaxPresenter.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/presentation/MMTSyntaxPresenter.scala @@ -398,9 +398,10 @@ class MMTSyntaxPresenter( doURI(OMMOD(from), rh, needsHand = true) // TODO args ignored df.foreach(definiensTerm => { - rh(" " + getObjDelim) + rh(" " + getObjDelim + " = ") objectPresenter(definiensTerm, Some(s.path $ DefComponent))(rh) }) + rh("\n") // actual structure, not just trivial include case _ => diff --git a/src/test/DiagramOperatorTest.scala b/src/test/DiagramOperatorTest.scala index 035ee4b02..8d722fac5 100644 --- a/src/test/DiagramOperatorTest.scala +++ b/src/test/DiagramOperatorTest.scala @@ -46,7 +46,9 @@ object DiagramOperatorTest extends MagicTest("debug") with DiagramOperatorHelper val pushout = new NewPushout(OMMOD(opposite), magma, magma) val interp = new DiagramInterpreter(controller, Context.empty, new ErrorLogger(controller.report)) - pushout.applyModule(controller.getModule(semigroup))(interp).foreach(m => { + val modules = pushout.applyModule(controller.getModule(semigroup))(interp) + + modules.foreach(m => { controller.presenter.apply(m)(ConsoleWriter) }) }