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/LinearOperators.scala similarity index 92% rename from src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/NewStuff.scala rename to src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/LinearOperators.scala index 7e107bb4b..721472e84 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/LinearOperators.scala @@ -3,7 +3,6 @@ package info.kwarc.mmt.api.modules.diagrams import info.kwarc.mmt.api._ import info.kwarc.mmt.api.libraries.Lookup import info.kwarc.mmt.api.modules.{Module, ModuleOrLink, Theory, View} -import info.kwarc.mmt.api.notations.NotationContainer import info.kwarc.mmt.api.objects.{OMCOMP, OMIDENT, OMMOD, Term} import info.kwarc.mmt.api.symbols._ @@ -365,38 +364,3 @@ trait LinearOperators { def applyConstant(c: Constant, container: ModuleOrLink)(implicit interp: DiagramInterpreter): Unit } - -class NewPushout(m: Term, dom: MPath, cod: MPath) extends LinearOperators { - override val ops: LinearOperatorSpecs = resolve(List( - ("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 newC = new FinalConstant( - home = OMMOD(ops("P")(c.parent)), - name = ops("P")(c.name), - alias = c.alias.map(ops("P")(_)), - tpC = c.tpC.map(tr), - dfC = c.dfC.map(tr), - rl = c.rl, - notC = NotationContainer.empty(), - vs = c.vs - ) - newC.metadata.add(c.metadata.getAll : _*) // TODO: shall we translate meta data via tr(), too? - interp.add(newC) - // Declaration.translate method - - 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/modules/diagrams/PushoutOperator.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/PushoutOperator.scala index 7f5e90bd1..0dd8d5c8e 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/PushoutOperator.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/PushoutOperator.scala @@ -1,128 +1,42 @@ package info.kwarc.mmt.api.modules.diagrams -import info.kwarc.mmt.api._ -import info.kwarc.mmt.api.libraries.Library -import info.kwarc.mmt.api.modules.diagrams.oldstuff.{InwardsLinearConnector, LinearFunctor, LinearOperator} -import info.kwarc.mmt.api.objects._ -import info.kwarc.mmt.api.symbols.{Constant, Declaration} -import info.kwarc.mmt.api.uom.SimplificationUnit - -sealed case class PushoutNames(viewNames: MPath => Option[MPath], pushoutNames: MPath => Option[MPath]) -object PushoutNames { - val default: PushoutNames = PushoutNames(_ => None, _ => None) -} - -class PushoutFunctor(connection: DiagramConnection, names: PushoutNames = PushoutNames.default) extends LinearFunctor { - override def applyModulePath(mpath: MPath): MPath = names.pushoutNames(mpath).getOrElse(super.applyModulePath(mpath)) - override def applyModuleName(name: LocalName): LocalName = name.suffixLastSimple("_pushout") - - override val dom: Diagram = connection.dom - override val cod: Diagram = connection.cod - - override def applyDomainModule(m: MPath): MPath = connection.functor(m).toMPath - - // lazy due to cyclic instance creation with PushoutConnector - private lazy val connector = new PushoutConnector(connection, names) - - override def translateConstant(c: Constant)(implicit interp: DiagramInterpreter): List[Declaration] = { - val translationMor = connector.applyModuleExpression(expressionContext(c)) - - val su = SimplificationUnit( - Context(applyModuleExpression(expressionContext(c)).toMPath), - expandConDefs = true, - expandVarDefs = false, - fullRecursion = true - ) - - def translate(t: Term): Term = interp.ctrl.simplifier(interp.ctrl.library.ApplyMorphs(t, translationMor), su) - - val pushedc = Constant( - home = OMMOD(equiNamer(c.path).module), - name = equiNamer(c.path).name, - alias = c.alias, - tp = c.tp.map(translate), - df = c.df.map(translate), +import info.kwarc.mmt.api.{ComplexStep, LocalName, MPath} +import info.kwarc.mmt.api.modules.ModuleOrLink +import info.kwarc.mmt.api.notations.NotationContainer +import info.kwarc.mmt.api.objects.{OMMOD, Term} +import info.kwarc.mmt.api.symbols.{Constant, FinalConstant} + +class PushoutOperator(m: Term, dom: MPath, cod: MPath) extends LinearOperators { + override val ops: LinearOperatorSpecs = resolve(List( + ("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))) + + // todo: potentially use Constant.translate method + val newC = new FinalConstant( + home = OMMOD(ops("P")(c.parent)), + name = ops("P")(c.name), + alias = c.alias.map(ops("P")(_)), + tpC = c.tpC.map(tr), + dfC = c.dfC.map(tr), rl = c.rl, - not = c.notC.copy() // todo(diagops,pushout): probably need to tweak argument positions, no? + notC = NotationContainer.empty(), + vs = c.vs ) - pushedc.metadata.add(c.metadata.getAll : _*) - List(pushedc) - } -} - -class PushoutConnector(connection: DiagramConnection, names: PushoutNames = PushoutNames.default) extends InwardsLinearConnector { - override def applyModulePath(mpath: MPath): MPath = names.viewNames(mpath).getOrElse(super.applyModulePath(mpath)) - override def applyModuleName(name: LocalName): LocalName = name.suffixLastSimple("_pushout_view") - - override val out = new PushoutFunctor(connection, names) - - override def applyDomainModule(thy: MPath): MPath = connection.applyTheory(thy).toMPath - - override def translateConstant(c: Constant)(implicit interp: DiagramInterpreter): List[Declaration] = { - List(assgn(c.path, OMS(out.applyModulePath(c.path.module) ? c.name))) - } -} - -object GenericPushoutOperator extends ParametricLinearOperator { - override val head: GlobalName = Path.parseS("http://cds.omdoc.org/urtheories?DiagramOperators?generic_pushout") - - override def instantiate(parameters: List[Term])(implicit interp: DiagramInterpreter): Option[LinearOperator] = parameters match { - case List(mor) => - val (dom, cod) = inferMorphismDomains(mor).getOrElse(return None) - val connection = DiagramConnection.Singleton(dom, cod, mor) - Some((new PushoutFunctor(connection) :: new PushoutConnector(connection)).withFocus(0)) - - case _ => None - } - - /** - * Tries to infer a morphism's domain and codomain as MPaths - */ - private[diagrams] def inferMorphismDomains(mor: Term)(implicit interp: DiagramInterpreter): Option[(MPath, MPath)] = { - implicit val library: Library = interp.ctrl.library - Morph.domain(mor) zip Morph.codomain(mor) match { - case Some((OMMOD(dom), OMMOD(cod))) => Some((dom, cod)) - case _ => - interp.errorCont(InvalidObject( - mor, - s"Cannot infer atomic domain and codomain (i.e., MPaths) from morphism passed to ${getClass.getSimpleName}`" - )) - None - } - } -} - -object SimplePushoutOperator extends NamedOperator { - override val head: GlobalName = Path.parseS("http://cds.omdoc.org/urtheories?DiagramOperators?simple_pushout") - - final override def apply(invocation: Term)(implicit interp: DiagramInterpreter): Option[Term] = invocation match { - case OMA(OMS(`head`), List(inputDiagramTerm, mor, viewNamesTerm, pushoutNamesTerm)) => - implicit val library: Library = interp.ctrl.library - - val List(inputDiagram, viewNames, pushoutNames) = List(inputDiagramTerm, viewNamesTerm, pushoutNamesTerm).map( - interp(_).getOrElse(return None) - ) - - if (List(inputDiagram, viewNames, pushoutNames).exists(_.mt.nonEmpty)) { - interp.errorCont(InvalidObject( - invocation, - s"Diagrams passed to ${getClass.getSimpleName} must not possess any meta diagrams; they are inferred anyway." - )) - } - - val (dom, cod) = GenericPushoutOperator.inferMorphismDomains(mor).getOrElse(return None) - val connection = DiagramConnection.Singleton(dom, cod, mor) - val diagram = inputDiagram.copy(mt = Some(connection.dom)) - val names = PushoutNames( - viewNames = m => diagram.modules.zip(viewNames.modules).find(_._1 == m).map(_._2), - pushoutNames = m => diagram.modules.zip(pushoutNames.modules).find(_._1 == m).map(_._2), - ) - - (new PushoutFunctor(connection, names) :: new PushoutConnector(connection, names)) - .withFocus(0) - .applyDiagram(diagram) - .map(_.toTerm) - - case _ => None + newC.metadata.add(c.metadata.getAll : _*) // TODO: shall we translate meta data via tr(), too? + interp.add(newC) + + 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/modules/diagrams/oldstuff/PushoutOperator.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/PushoutOperator.scala new file mode 100644 index 000000000..07deb94b4 --- /dev/null +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/PushoutOperator.scala @@ -0,0 +1,128 @@ +package info.kwarc.mmt.api.modules.diagrams.oldstuff + +import info.kwarc.mmt.api._ +import info.kwarc.mmt.api.libraries.Library +import info.kwarc.mmt.api.modules.diagrams.oldstuff.{InwardsLinearConnector, LinearFunctor, LinearOperator} +import info.kwarc.mmt.api.objects._ +import info.kwarc.mmt.api.symbols.{Constant, Declaration} +import info.kwarc.mmt.api.uom.SimplificationUnit + +sealed case class PushoutNames(viewNames: MPath => Option[MPath], pushoutNames: MPath => Option[MPath]) +object PushoutNames { + val default: PushoutNames = PushoutNames(_ => None, _ => None) +} + +class PushoutFunctor(connection: DiagramConnection, names: PushoutNames = PushoutNames.default) extends LinearFunctor { + override def applyModulePath(mpath: MPath): MPath = names.pushoutNames(mpath).getOrElse(super.applyModulePath(mpath)) + override def applyModuleName(name: LocalName): LocalName = name.suffixLastSimple("_pushout") + + override val dom: Diagram = connection.dom + override val cod: Diagram = connection.cod + + override def applyDomainModule(m: MPath): MPath = connection.functor(m).toMPath + + // lazy due to cyclic instance creation with PushoutConnector + private lazy val connector = new PushoutConnector(connection, names) + + override def translateConstant(c: Constant)(implicit interp: DiagramInterpreter): List[Declaration] = { + val translationMor = connector.applyModuleExpression(expressionContext(c)) + + val su = SimplificationUnit( + Context(applyModuleExpression(expressionContext(c)).toMPath), + expandConDefs = true, + expandVarDefs = false, + fullRecursion = true + ) + + def translate(t: Term): Term = interp.ctrl.simplifier(interp.ctrl.library.ApplyMorphs(t, translationMor), su) + + val pushedc = Constant( + home = OMMOD(equiNamer(c.path).module), + name = equiNamer(c.path).name, + alias = c.alias, + tp = c.tp.map(translate), + df = c.df.map(translate), + rl = c.rl, + not = c.notC.copy() // todo(diagops,pushout): probably need to tweak argument positions, no? + ) + pushedc.metadata.add(c.metadata.getAll : _*) + List(pushedc) + } +} + +class PushoutConnector(connection: DiagramConnection, names: PushoutNames = PushoutNames.default) extends InwardsLinearConnector { + override def applyModulePath(mpath: MPath): MPath = names.viewNames(mpath).getOrElse(super.applyModulePath(mpath)) + override def applyModuleName(name: LocalName): LocalName = name.suffixLastSimple("_pushout_view") + + override val out = new PushoutFunctor(connection, names) + + override def applyDomainModule(thy: MPath): MPath = connection.applyTheory(thy).toMPath + + override def translateConstant(c: Constant)(implicit interp: DiagramInterpreter): List[Declaration] = { + List(assgn(c.path, OMS(out.applyModulePath(c.path.module) ? c.name))) + } +} + +object GenericPushoutOperator extends ParametricLinearOperator { + override val head: GlobalName = Path.parseS("http://cds.omdoc.org/urtheories?DiagramOperators?generic_pushout") + + override def instantiate(parameters: List[Term])(implicit interp: DiagramInterpreter): Option[LinearOperator] = parameters match { + case List(mor) => + val (dom, cod) = inferMorphismDomains(mor).getOrElse(return None) + val connection = DiagramConnection.Singleton(dom, cod, mor) + Some((new PushoutFunctor(connection) :: new PushoutConnector(connection)).withFocus(0)) + + case _ => None + } + + /** + * Tries to infer a morphism's domain and codomain as MPaths + */ + private[diagrams] def inferMorphismDomains(mor: Term)(implicit interp: DiagramInterpreter): Option[(MPath, MPath)] = { + implicit val library: Library = interp.ctrl.library + Morph.domain(mor) zip Morph.codomain(mor) match { + case Some((OMMOD(dom), OMMOD(cod))) => Some((dom, cod)) + case _ => + interp.errorCont(InvalidObject( + mor, + s"Cannot infer atomic domain and codomain (i.e., MPaths) from morphism passed to ${getClass.getSimpleName}`" + )) + None + } + } +} + +object SimplePushoutOperator extends NamedOperator { + override val head: GlobalName = Path.parseS("http://cds.omdoc.org/urtheories?DiagramOperators?simple_pushout") + + final override def apply(invocation: Term)(implicit interp: DiagramInterpreter): Option[Term] = invocation match { + case OMA(OMS(`head`), List(inputDiagramTerm, mor, viewNamesTerm, pushoutNamesTerm)) => + implicit val library: Library = interp.ctrl.library + + val List(inputDiagram, viewNames, pushoutNames) = List(inputDiagramTerm, viewNamesTerm, pushoutNamesTerm).map( + interp(_).getOrElse(return None) + ) + + if (List(inputDiagram, viewNames, pushoutNames).exists(_.mt.nonEmpty)) { + interp.errorCont(InvalidObject( + invocation, + s"Diagrams passed to ${getClass.getSimpleName} must not possess any meta diagrams; they are inferred anyway." + )) + } + + val (dom, cod) = GenericPushoutOperator.inferMorphismDomains(mor).getOrElse(return None) + val connection = DiagramConnection.Singleton(dom, cod, mor) + val diagram = inputDiagram.copy(mt = Some(connection.dom)) + val names = PushoutNames( + viewNames = m => diagram.modules.zip(viewNames.modules).find(_._1 == m).map(_._2), + pushoutNames = m => diagram.modules.zip(pushoutNames.modules).find(_._1 == m).map(_._2), + ) + + (new PushoutFunctor(connection, names) :: new PushoutConnector(connection, names)) + .withFocus(0) + .applyDiagram(diagram) + .map(_.toTerm) + + case _ => None + } +} diff --git a/src/test/DiagramOperatorTest.scala b/src/test/DiagramOperatorTest.scala index 586cf3a97..8d3f8b3ba 100644 --- a/src/test/DiagramOperatorTest.scala +++ b/src/test/DiagramOperatorTest.scala @@ -91,8 +91,6 @@ class Additive extends LinearOperators { } override def applyConstant(c: Constant, container: ModuleOrLink)(implicit interp: DiagramInterpreter): Unit = { - - // use Infix shorthand val modifications: Map[GlobalName, () => (TextNotation, List[LocalName])] = Map( Symbols.binaryOp -> (() => ( c.not.get.copy(fixity = Infix(Delim("+"), 0, 2, Some(true))),