diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/DiagramInterpreter.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/DiagramInterpreter.scala
index 2bf66c298..9fcf6a5fc 100644
--- a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/DiagramInterpreter.scala
+++ b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/DiagramInterpreter.scala
@@ -165,6 +165,7 @@ object InstallDiagram {
   */
 class DiagramInterpreter(val ctrl: Controller, private val interpreterContext: Context, val errorCont: ErrorHandler) {
 
+  private val addedModules: mutable.LinkedHashSet[Module] = mutable.LinkedHashSet[Module]()
   private val transientPaths: mutable.ListBuffer[Path] = mutable.ListBuffer()
 
   // need mutable.LinkedHashMap as it guarantees to preserve insertion order (needed for commit())
@@ -185,8 +186,14 @@ class DiagramInterpreter(val ctrl: Controller, private val interpreterContext: C
 
   def endAdd(elem: ContainerElement[_]): Unit = {
     ctrl.endAdd(elem)
+    elem match {
+      case module: Module => addedModules += module
+      case _ => /* do nothing */
+    }
   }
 
+  def getAddedModules: List[Module] = addedModules.toList
+
   /**
     * [[add]] plus registering as a toplevel result
     */
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 a625db1fd..525559207 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,15 +1,13 @@
 package info.kwarc.mmt.api.modules.diagrams
 
-import info.kwarc.mmt.api.{ComplexStep, GeneratedFrom, ImplementationError, InvalidElement, LocalName, MPath, SimpleStep}
-import info.kwarc.mmt.api.frontend.Controller
+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.{Constant, Declaration, FinalConstant, Include, IncludeData, Structure}
+import info.kwarc.mmt.api.symbols._
 
-
-trait Blah {
+trait LinearOperators {
   val ops: LinearOperatorSpecs
 
   private val self = this
@@ -54,14 +52,22 @@ trait Blah {
     def applyDomain(m: MPath): MPath = metaFunctor(m).toMPath
   }
 
-  def suffixBy(str: String): MPath => MPath = m => {
+  private def transformModulePath(f: SimpleStep => SimpleStep): 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?
+      case x@SimpleStep(_) => f(x)
+      case ComplexStep(path) => ComplexStep(transformModulePath(f)(path)) // todo: is this correct for nested modules?
     })
     m.doc ? newName
   }
 
+  def prefixBy(str: String): MPath => MPath = transformModulePath {
+    case SimpleStep(name) => SimpleStep(str + name)
+  }
+
+  def suffixBy(str: String): MPath => MPath = transformModulePath {
+    case SimpleStep(name) => SimpleStep(name + str)
+  }
+
   object IdentityFunctorSpec {
     def apply(dom: Diagram): LinearFunctorSpec = new LinearFunctorSpec(None, dom, dom, DiagramFunctor.identity(dom), x => x)
   }
@@ -85,36 +91,56 @@ trait Blah {
   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 connectorTupleToSpec(x: (String, (LinearFunctorSpec, String), DiagramConnection, MPath => MPath)): UnresolvedLinearConnectorSpec =
+  implicit def connectorTupleToSpec1(x: (String, (LinearFunctorSpec, LinearFunctorSpec), DiagramConnection, MPath => MPath)): UnresolvedLinearConnectorSpec =
+    UnresolvedLinearConnectorSpec(Some(x._1), dom = Right(x._2._1), cod = Right(x._2._2), x._3, x._4)
+
+  implicit def connectorTupleToSpec2(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)
 
+  implicit def connectorTupleToSpec3(x: (String, (String, LinearFunctorSpec), DiagramConnection, MPath => MPath)): UnresolvedLinearConnectorSpec =
+    UnresolvedLinearConnectorSpec(Some(x._1), dom = Left(x._2._1), cod = Right(x._2._2), x._3, x._4)
+
+  implicit def connectorTupleToSpec4(x: (String, (String, String), DiagramConnection, MPath => MPath)): UnresolvedLinearConnectorSpec =
+    UnresolvedLinearConnectorSpec(Some(x._1), dom = Left(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 = {
+  trait ConstantRenamer {
+    def apply(n: LocalName)(implicit interp: DiagramInterpreter): LocalName
+  }
+
+  def getRenamer(opKey: String)(f: String => String): ConstantRenamer = {
     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))
-    })
+    new ConstantRenamer {
+      override def apply(n: LocalName)(implicit interp: DiagramInterpreter): LocalName = 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)
+  def getEquinamer(opKey: String): ConstantRenamer = 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.
+    * invariant: idempotent, i.e., when called more than once on the same view, always returns the same modules (i.e., the objects in the Java sense).
+    *
+    * @return (modules, alreadyProcessed) where modules are the either newly created (but yet empty) or existing mapped modules and alreadyProcessed indicates whether _any_ of the operators has already processed the input module
+    * @see [[beginView]]
     */
-  protected def beginTheory(thy: Theory)(implicit interp: DiagramInterpreter): List[ModuleOrLink] = {
-    ops.specs map {
+  protected def beginTheory(thy: Theory)(implicit interp: DiagramInterpreter): (List[ModuleOrLink], Boolean) = {
+    var alreadyProcessed = false
+    val modules = ops.specs map {
       case op@LinearFunctorSpec(_, dom, _, _, _) =>
         val newThyPath = op(thy.path)
 
         if (interp.ctrl.getAsO(classOf[Theory], newThyPath).nonEmpty) {
+          alreadyProcessed = true
           interp.ctrl.getTheory(newThyPath)
         } else {
           val newMeta = thy.meta.map {
@@ -143,6 +169,7 @@ trait Blah {
         val newMorPath = op(thy.path)
 
         if (interp.ctrl.getAsO(classOf[Module], newMorPath).nonEmpty) {
+          alreadyProcessed = true
           interp.ctrl.getModule(newMorPath)
         } else {
           val newMor = View(
@@ -157,13 +184,18 @@ trait Blah {
           newMor
         }
     }
+    (modules, alreadyProcessed)
   }
 
   /**
-    * invariant: idempotent, i.e., when called more than once on the same view, always returns the same existing result.
+    * invariant: idempotent, i.e., when called more than once on the same view, always returns the same modules (i.e., the objects in the Java sense).
+    *
+    * @return (modules, alreadyProcessed) where modules are the either newly created (but yet empty) or existing mapped modules and alreadyProcessed indicates whether _any_ of the operators has already processed the input module
+    * @see [[beginTheory]]
     */
-  protected def beginView(view: View)(implicit interp: DiagramInterpreter): List[View] = {
-    ops.specs flatMap {
+  protected def beginView(view: View)(implicit interp: DiagramInterpreter): (List[View], Boolean) = {
+    var alreadyProcessed = false
+    val modules = ops.specs flatMap {
       case op@LinearFunctorSpec(_, _, _, _, _) =>
         if (applyModule(interp.ctrl.getModule(view.from.toMPath)).isEmpty) {
           None
@@ -173,6 +205,7 @@ trait Blah {
           val newMorPath = op(view.path)
 
           if (interp.ctrl.getAsO(classOf[View], newMorPath).nonEmpty) {
+            alreadyProcessed = true
             Some(interp.ctrl.getAs(classOf[View], newMorPath))
           } else {
             val newMor = View(
@@ -192,6 +225,8 @@ trait Blah {
         //                            but the MMT system does not yet support native statements of morphism equality
         None
     }
+
+    (modules, alreadyProcessed)
   }
 
   /**
@@ -203,15 +238,18 @@ trait Blah {
     // related to inModule gets constructed)
     interp.ctrl.simplifier(m)
 
-    val addedModules = m match {
+    val (addedModules, alreadyProcessed) = m match {
       case thy: Theory =>
         beginTheory(thy)
       case v: View =>
         beginView(v)
     }
-    m.getDeclarations.foreach(d => applyDeclaration(d, m))
 
-    addedModules.foreach(interp.ctrl.endAdd)
+    if (!alreadyProcessed) {
+      m.getDeclarations.foreach(d => applyDeclaration(d, m))
+      // finish up modules (esp. handle includes that might have been added by the last line)
+      addedModules.foreach(interp.endAdd)
+    }
     addedModules
   }
 
@@ -318,26 +356,27 @@ trait Blah {
   }
 
   def applyStructure(s: Structure, container: ModuleOrLink): Unit = {
-    ???
+    // todo: implement
   }
 
   def applyConstant(c: Constant, container: ModuleOrLink)(implicit interp: DiagramInterpreter): Unit
 }
 
-class NewPushout(m: Term, dom: MPath, cod: MPath) extends Blah {
+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"))
   ))
 
+  private val equinamer = getEquinamer("P")
+
   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 = equinamer(c.name),
-      alias = c.alias map equinamer,
+      alias = c.alias.map(n => equinamer(n)),
       tpC = c.tpC.map(tr),
       dfC = c.dfC.map(tr),
       rl = c.rl,
diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/Operators.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/Operators.scala
index 481db6237..4141a7599 100644
--- a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/Operators.scala
+++ b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/Operators.scala
@@ -1,5 +1,6 @@
 package info.kwarc.mmt.api.modules.diagrams
 
+import info.kwarc.mmt.api.modules.diagrams.oldstuff.{Functor, InwardsLinearConnector, LinearConnector, LinearFunctor, LinearOperator, OutwardsLinearConnector}
 import info.kwarc.mmt.api.objects._
 import info.kwarc.mmt.api.{GlobalName, SyntaxDrivenRule}
 
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 0858822f8..7f5e90bd1 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
@@ -2,6 +2,7 @@ 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
diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/ZippingOperator.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/ZippingOperator.scala
index d17455707..70edd7743 100644
--- a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/ZippingOperator.scala
+++ b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/ZippingOperator.scala
@@ -2,6 +2,7 @@ package info.kwarc.mmt.api.modules.diagrams
 
 import info.kwarc.mmt.api.ContentPath
 import info.kwarc.mmt.api.libraries.Library
+import info.kwarc.mmt.api.modules.diagrams.oldstuff.LinearOperator
 import info.kwarc.mmt.api.symbols.{Constant, Declaration, IncludeData, Structure}
 
 /**
diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/LinearConnector.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/LinearConnector.scala
similarity index 98%
rename from src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/LinearConnector.scala
rename to src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/LinearConnector.scala
index 232d9aca7..e1f1bc286 100644
--- a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/LinearConnector.scala
+++ b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/LinearConnector.scala
@@ -1,4 +1,4 @@
-package info.kwarc.mmt.api.modules.diagrams
+package info.kwarc.mmt.api.modules.diagrams.oldstuff
 
 import info.kwarc.mmt.api.libraries.Lookup
 import info.kwarc.mmt.api.modules.{Theory, View}
@@ -6,6 +6,7 @@ import info.kwarc.mmt.api.notations.NotationContainer
 import info.kwarc.mmt.api.objects.{OMMOD, Term}
 import info.kwarc.mmt.api.symbols._
 import info.kwarc.mmt.api._
+import info.kwarc.mmt.api.modules.diagrams.{Diagram, DiagramInterpreter}
 
 /**
   * A natural transformation betweeen two [[LinearFunctor]]s `in` and `out` that linearly maps theories to views ("connections") and views not at all.
diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/LinearFunctor.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/LinearFunctor.scala
similarity index 99%
rename from src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/LinearFunctor.scala
rename to src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/LinearFunctor.scala
index ba28dd966..9bf030fd9 100644
--- a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/LinearFunctor.scala
+++ b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/LinearFunctor.scala
@@ -1,4 +1,4 @@
-package info.kwarc.mmt.api.modules.diagrams
+package info.kwarc.mmt.api.modules.diagrams.oldstuff
 
 import info.kwarc.mmt.api.libraries.Lookup
 import info.kwarc.mmt.api.modules.{AbstractTheory, Link, Module, Theory, View}
@@ -7,6 +7,7 @@ import info.kwarc.mmt.api.objects.{Context, OMCOMP, OMID, OMIDENT, OMMOD, OMS, O
 import info.kwarc.mmt.api.symbols._
 import info.kwarc.mmt.api._
 import info.kwarc.mmt.api.frontend.Controller
+import info.kwarc.mmt.api.modules.diagrams.{Diagram, DiagramInterpreter}
 
 /**
   * A functor that linearly maps theories to theories and views to views.
diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/ModuleOperator.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/ModuleOperator.scala
similarity index 99%
rename from src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/ModuleOperator.scala
rename to src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/ModuleOperator.scala
index 70b64b8c0..1a8921d4f 100644
--- a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/ModuleOperator.scala
+++ b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/ModuleOperator.scala
@@ -1,5 +1,6 @@
-package info.kwarc.mmt.api.modules.diagrams
+package info.kwarc.mmt.api.modules.diagrams.oldstuff
 
+import info.kwarc.mmt.api.modules.diagrams.{Diagram, DiagramInterpreter, UnaryOperator, ZippingOperator}
 import info.kwarc.mmt.api.{ContainerElement, ContentPath, GeneratedFrom, GlobalName, ImplementationError, InvalidElement, InvalidObject, LocalName, MPath}
 import info.kwarc.mmt.api.modules.{Module, ModuleOrLink}
 import info.kwarc.mmt.api.objects.{OMCOMP, OMID, OMIDENT, OMMOD, OMS, Term}
diff --git a/src/mmt-lf/src/info/kwarc/mmt/DropArgsFunctor.scala b/src/mmt-lf/src/info/kwarc/mmt/DropArgsFunctor.scala
index 660203d08..5c29b5c3f 100644
--- a/src/mmt-lf/src/info/kwarc/mmt/DropArgsFunctor.scala
+++ b/src/mmt-lf/src/info/kwarc/mmt/DropArgsFunctor.scala
@@ -5,6 +5,7 @@ import info.kwarc.mmt.api._
 import info.kwarc.mmt.api.libraries.Library
 import info.kwarc.mmt.api.metadata.{MetaData, MetaDatum}
 import info.kwarc.mmt.api.modules.diagrams._
+import info.kwarc.mmt.api.modules.diagrams.oldstuff.{InwardsLinearConnector, LinearFunctor, LinearOperator}
 import info.kwarc.mmt.api.notations.NotationContainer
 import info.kwarc.mmt.api.objects._
 import info.kwarc.mmt.api.symbols.{Constant, Declaration, TermContainer}
diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/comptrans/CompTransOperator.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/comptrans/CompTransOperator.scala
index f1d869ef1..aadb41e96 100644
--- a/src/mmt-lf/src/info/kwarc/mmt/lf/comptrans/CompTransOperator.scala
+++ b/src/mmt-lf/src/info/kwarc/mmt/lf/comptrans/CompTransOperator.scala
@@ -5,6 +5,7 @@ import info.kwarc.mmt.api._
 import info.kwarc.mmt.api.frontend.Controller
 import info.kwarc.mmt.api.libraries.Library
 import info.kwarc.mmt.api.modules.diagrams._
+import info.kwarc.mmt.api.modules.diagrams.oldstuff.{LinearFunctor, LinearOperator}
 import info.kwarc.mmt.api.notations.NotationContainer
 import info.kwarc.mmt.api.objects.{Context, OMA, OMMOD, OMS, Term}
 import info.kwarc.mmt.api.symbols.{Constant, Declaration, TermContainer}
diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/comptrans/LogrelOperator.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/comptrans/LogrelOperator.scala
index ac37d37ea..d75d94dc0 100644
--- a/src/mmt-lf/src/info/kwarc/mmt/lf/comptrans/LogrelOperator.scala
+++ b/src/mmt-lf/src/info/kwarc/mmt/lf/comptrans/LogrelOperator.scala
@@ -5,6 +5,7 @@ import info.kwarc.mmt.api._
 import info.kwarc.mmt.api.frontend.Controller
 import info.kwarc.mmt.api.libraries.Library
 import info.kwarc.mmt.api.modules.diagrams._
+import info.kwarc.mmt.api.modules.diagrams.oldstuff.{InwardsLinearConnector, LinearFunctor, LinearOperator, SystematicRenamer}
 import info.kwarc.mmt.api.notations.NotationContainer
 import info.kwarc.mmt.api.objects.{Context, OMMOD, OMS, Term}
 import info.kwarc.mmt.api.symbols.{Constant, Declaration, TermContainer}
diff --git a/src/mmt-odk/src/info/kwarc/mmt/odk/diagops/SubFunctor.scala b/src/mmt-odk/src/info/kwarc/mmt/odk/diagops/SubFunctor.scala
index fa71f9a8f..84d165f8f 100644
--- a/src/mmt-odk/src/info/kwarc/mmt/odk/diagops/SubFunctor.scala
+++ b/src/mmt-odk/src/info/kwarc/mmt/odk/diagops/SubFunctor.scala
@@ -3,6 +3,7 @@ package info.kwarc.mmt.odk.diagops
 import info.kwarc.mmt.api.checking.Solver
 import info.kwarc.mmt.api.frontend.Controller
 import info.kwarc.mmt.api.modules.diagrams._
+import info.kwarc.mmt.api.modules.diagrams.oldstuff.{Functor, InwardsLinearConnector, LinearFunctor, LinearOperator, SystematicRenamer}
 import info.kwarc.mmt.api.objects._
 import info.kwarc.mmt.api.symbols.{Constant, Declaration, TermContainer}
 import info.kwarc.mmt.api.{GlobalName, LocalName, MPath, Path}
diff --git a/src/test/DiagramOperatorTest.scala b/src/test/DiagramOperatorTest.scala
index 8d722fac5..603282ceb 100644
--- a/src/test/DiagramOperatorTest.scala
+++ b/src/test/DiagramOperatorTest.scala
@@ -1,8 +1,12 @@
-import info.kwarc.mmt.api.modules.diagrams.{NewPushout, DiagramInterpreter}
-import info.kwarc.mmt.api.objects.{Context, OMMOD}
+import info.kwarc.mmt.api.modules.ModuleOrLink
+import info.kwarc.mmt.api.modules.diagrams.{Diagram, DiagramConnection, DiagramFunctor, DiagramInterpreter, LinearOperators, NewPushout}
+import info.kwarc.mmt.api.notations.{Delim, Delimiter, Mixfix, NotationContainer, SimpArg, TextNotation}
+import info.kwarc.mmt.api.objects.{Context, OMID, OMIDENT, OMMOD, StatelessTraverser, Term, Traverser, UniformTranslator}
 import info.kwarc.mmt.api.presentation.{ConsoleWriter, MMTSyntaxPresenter, NotationBasedPresenter}
-import info.kwarc.mmt.api.{DPath, ErrorLogger, NamespaceMap, Path, presentation}
+import info.kwarc.mmt.api.symbols.{Constant, FinalConstant}
+import info.kwarc.mmt.api.{ComplexStep, DPath, ErrorLogger, GlobalName, LocalName, MPath, NamespaceMap, Path, presentation}
 import info.kwarc.mmt.api.utils.URI
+import info.kwarc.mmt.lf.Apply
 
 /**
   * Debugging links for diagram output:
@@ -27,17 +31,9 @@ trait DiagramOperatorHelper {
   *
   * @author Navid
   */
-object DiagramOperatorTest extends MagicTest("debug") with DiagramOperatorHelper {
+object DiagramPushoutTest extends MagicTest("debug") with DiagramOperatorHelper {
 
   override def run(): Unit = {
-    /*val x = Path.parseD("latin:/domain_theories/algebra/groups.omdoc", NamespaceMap.empty)
-    val rh = new presentation.StringBuilder
-    val p = new MMTSyntaxPresenter(new NotationBasedPresenter, presentGenerated = true, machineReadable = true)
-    p.init(controller)
-    p(controller.get(x), standalone = true)(rh)
-
-    println(rh.get)*/
-
     val magma = Path.parseM("latin:/algebraic?Magma")
     val opposite = Path.parseM("latin:/algebraic?OppositeMagma")
     val semigroup = Path.parseM("latin:/algebraic?Semigroup")
@@ -46,24 +42,139 @@ 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))
-    val modules = pushout.applyModule(controller.getModule(semigroup))(interp)
+    pushout.applyModule(controller.getModule(semigroup))(interp)
 
-    modules.foreach(m => {
+    interp.getAddedModules.foreach(m => {
       controller.presenter.apply(m)(ConsoleWriter)
     })
   }
 }
 
-/**
-  * Test for ITP 2021 paper by Florian and Navid.
-  */
-object ITP2021Test extends MagicTest("debug") with DiagramOperatorHelper {
+object DiagramAdditiveTest extends MagicTest("debug") with DiagramOperatorHelper {
 
   override def run(): Unit = {
-    val repl = new FastREPLExtension(FastREPL.shortcuts, Some("build MMT/LATIN2 mmt-omdoc itp2021/input.mmt"))
-    controller.extman.addExtension(repl)
+    val semigroup = Path.parseM("latin:/algebraic?Semigroup")
+
+    val additive = new Additive()
+    val interp = new DiagramInterpreter(controller, Context.empty, new ErrorLogger(controller.report))
+    additive.applyModule(controller.getModule(semigroup))(interp)
+
+    interp.getAddedModules.foreach(m => {
+      controller.presenter.apply(m)(ConsoleWriter)
+    })
+  }
+}
+
+class Additive extends LinearOperators {
+  private val Magma: MPath = Path.parseM("latin:/algebraic?Magma")
+  private val Set: MPath = Path.parseM("latin:/algebraic?Set")
+
+  private object Symbols {
+    val binaryOp: GlobalName = Magma ? "op"
+    val inverseOp: GlobalName = Path.parseM("latin:/algebraic?InverseOperator") ? "inv"
+    val unit: GlobalName = Path.parseM("latin:/algebraic?UnitElement") ? "unit"
+  }
+
+  override val ops: LinearOperatorSpecs = resolve(List(
+    ("A", Diagram.singleton(Set) -> Diagram.singleton(Set), DiagramFunctor.singleton(Set, Set), prefixBy("Additive")),
+    ("inA", Id(Set) -> "A", DiagramConnection.Singleton(Set, Set, OMIDENT(OMMOD(Set))), suffixBy("AsAdditive")),
+    ("outA", "A" -> Id(Set), DiagramConnection.Singleton(Set, Set, OMIDENT(OMMOD(Set))), suffixBy("AsMultiplicative"))
+  ))
 
-    repl.run()
-    sys.exit(0)
+  private val equinamer = getEquinamer("A")
+
+  override def applyConstant(c: Constant, container: ModuleOrLink)(implicit interp: DiagramInterpreter): Unit = {
+
+    val modifications: Map[GlobalName, () => (TextNotation, List[LocalName])] = Map(
+      Symbols.binaryOp -> (() => (
+        c.not.get.copy(fixity = Mixfix(List(SimpArg(1), Delim("+"), SimpArg(2)))),
+        List(LocalName("plus"))
+      )),
+      Symbols.inverseOp -> (() => (
+        c.not.get.copy(fixity = Mixfix(List(Delim("-", associatesToLeft = false), SimpArg(1)))),
+        List(LocalName("negate"))
+      )),
+      Symbols.unit -> (() => (
+        c.not.get.copy(fixity = Mixfix(List(Delim("0")))),
+        List(LocalName("zero"))
+      ))
+    )
+
+    def inTr(t: Term): Term = interp.ctrl.library.ApplyMorphs(t, OMMOD(ops("inA")(c.parent)))
+
+    val newC = new FinalConstant(
+      home = OMMOD(ops("A")(c.parent)),
+      name = equinamer(c.name),
+      alias = c.alias.map(n => equinamer(n)) ++ modifications.get(c.path).map(f => f()._2).getOrElse(Nil),
+      tpC = c.tpC map inTr,
+      dfC = c.dfC map inTr,
+      rl = c.rl,
+      notC = modifications.get(c.path).map(f => NotationContainer(f()._1)).getOrElse(c.notC),
+      vs = c.vs
+    )
+    interp.add(newC)
+
+    if (c.df.isEmpty) {
+      val inC = Constant(
+        home = OMMOD(ops("inA")(c.parent)),
+        name = LocalName(ComplexStep(c.parent) :: c.name),
+        alias = Nil,
+        tp = c.tpC.map(inTr).get,
+        df = Some(newC.toTerm),
+        rl = None
+      )
+      val outC = Constant(
+        home = OMMOD(ops("outA")(c.parent)),
+        name = LocalName(ComplexStep(newC.parent) :: equinamer(c.name)),
+        alias = Nil,
+        tp = c.tpC.get,
+        df = Some(c.toTerm),
+        rl = None
+      )
+      interp.add(inC)
+      interp.add(outC)
+    }
+  }
+}
+
+class FOL2SFOL extends LinearOperators {
+  private val FOL: MPath = Path.parseM("latin:/?FOL")
+  private val SFOL: MPath = Path.parseM("latin:/?SingleUniverseSFOL")
+
+  private val term: GlobalName = ???
+  private val tm: GlobalName = ???
+  private val designatedTp: GlobalName = SFOL ? "U"
+
+  override val ops: LinearOperatorSpecs = resolve(List(
+    ("F", Diagram.singleton(FOL) -> Diagram.singleton(SFOL), DiagramFunctor.singleton(FOL, SFOL), suffixBy("_SFOL"))
+  ))
+
+  private val equinamer = getEquinamer("P")
+
+  override def applyConstant(c: Constant, container: ModuleOrLink)(implicit interp: DiagramInterpreter): Unit = {
+    val trr = new StatelessTraverser {
+      override def traverse(t: Term)(implicit con: Context, state: State): Term = t match {
+        case OMID(`term`) => Apply(OMID(tm), OMID(designatedTp))
+        case t => Traverser.apply(this, t)
+      }
+    }
+
+    val tr = new UniformTranslator {
+      override def applyPlain(con: Context, tm: Term): Term = trr(tm, con)
+    }
+
+    val newC = new FinalConstant(
+      home = OMMOD(ops("F")(c.parent)),
+      name = equinamer(c.name),
+      alias = c.alias.map(n => equinamer(n)),
+      tpC = c.tpC.map(t => tr.applyType(Context(c.parent), t)),
+      dfC = c.dfC.map(t => tr.applyDef(Context(c.parent), t)),
+      rl = c.rl,
+      notC = NotationContainer.empty(),
+      vs = c.vs
+    )
+    newC.metadata.add(c.metadata.getAll : _*)
+
+    interp.add(newC)
   }
-}
\ No newline at end of file
+}