diagops: add polymorphify [skip ci]

src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/oldstuff/PushoutOperator.scala

@@ -2,6 +2,7 @@ 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.{Diagram, DiagramConnection, DiagramInterpreter, NamedOperator, ParametricLinearOperator}
 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}

src/mmt-api/src/main/info/kwarc/mmt/api/notations/NotationContainer.scala

@@ -155,6 +155,7 @@ class NotationContainer extends ComponentContainer {
      ).flatten
    }
 
+  def map(f: TextNotation => TextNotation): NotationContainer = copy().mapInPlace(f)
   def mapInPlace(f: TextNotation => TextNotation): this.type = collectInPlace(x => Some(f(x)))
 
   def collectInPlace(f: TextNotation => Option[TextNotation]): this.type = {

src/mmt-api/src/main/info/kwarc/mmt/api/notations/NotationExtension.scala

@@ -48,15 +48,16 @@ abstract class Fixity {
 case class Mixfix(markers: List[Marker]) extends Fixity {
    def asString: (String, String) = ("mixfix", markers.mkString(" "))
    def addInitialImplicits(n: Int): Mixfix = {
-     val markersM = markers.map {
+     def shift(m: Marker): Marker = m match {
        case d: Delimiter => d
        case a: Arg => a * {_ + n}
        case a: ImplicitArg => a * {_ + n}
        case v: Var => v.copy(number = v.number + 1)
+       case f: FractionMarker => f.copy(above = f.above map shift)
        // TODO other cases
        case other => throw ImplementationError("undefined case of marker " + other.toString)
      }
-     Mixfix(markersM)
+     Mixfix(markers map shift)
    }
 
   /**

src/mmt-api/src/main/info/kwarc/mmt/api/objects/Traverse.scala

@@ -9,16 +9,16 @@ import info.kwarc.mmt.api.objects.Conversions._
   *
   * During the traversal, a value of type [[State]] may be used to carry along state.
   *
-  * To implement a traverser, subclass and overwrite [[traverse()]].
+  * To implement a traverser, subclass and overwrite [[traverse]].
   * Delegate cases you do not wish to handle to `Traverser(this, t)` from the companion
   * object.
-  * In a sense, `Traverser(this, t)` works as if [[traverse()]] were extended homomorphically
-  * to `t`. Namely, if `t` is complex (say on [[OMBINDC]]), then [[traverse()]] is called
+  * In a sense, `Traverser(this, t)` works as if [[traverse]] were extended homomorphically
+  * to `t`. Namely, if `t` is complex (say on [[OMBINDC]]), then [[traverse]] is called
   * on all children and the result reassembled to the same kind of term `t` was before
   * (e.g. again [[OMBINDC]]).
   * If `t` is simple (say on [[OMID]]), is is returned as-is.
   *
-  * Hence, therer are two options for doing recursion within [[traverse()]]:
+  * Hence, therer are two options for doing recursion within [[traverse]]:
   *
   * - call `Traverser(this, t)`: do this only if you determined you do not wish to handle `t`, but
   *   possibly its children.

src/test/DiagramOperatorTest.scala

@@ -1,12 +1,9 @@
-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, Infix, Mixfix, NotationContainer, Prefix, 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.symbols.{Constant, FinalConstant}
-import info.kwarc.mmt.api.{ComplexStep, DPath, ErrorLogger, GlobalName, LocalName, MPath, NamespaceMap, Path, presentation}
+import diagops.{AdditiveOperator, PolymorphifySFOL}
+import info.kwarc.mmt.api._
+import info.kwarc.mmt.api.modules.diagrams._
+import info.kwarc.mmt.api.objects._
+import info.kwarc.mmt.api.presentation.ConsoleWriter
 import info.kwarc.mmt.api.utils.URI
-import info.kwarc.mmt.lf.Apply
 
 /**
   * Debugging links for diagram output:
@@ -43,7 +40,7 @@ object DiagramPushoutTest extends MagicTest("debug") with DiagramOperatorHelper
     //              Apparently, without this forced build, not all includes are visible?
     controller.handleLine("build MMT/LATIN2 mmt-omdoc domain_theories/algebra/magmas.mmt")
 
-    val pushout = new NewPushout(OMMOD(opposite), magma, magma)
+    val pushout = new PushoutOperator(OMMOD(opposite), magma, magma)
 
     val interp = new DiagramInterpreter(controller, Context.empty, new ErrorLogger(controller.report))
     pushout.applyModule(controller.getModule(semigroup))(interp)
@@ -55,131 +52,29 @@ object DiagramPushoutTest extends MagicTest("debug") with DiagramOperatorHelper
 }
 
 object DiagramAdditiveTest extends MagicTest("debug") with DiagramOperatorHelper {
-
   override def run(): Unit = {
     val semigroup = Path.parseM("latin:/algebraic?Semigroup")
 
-    val additive = new Additive()
+    val additive = new AdditiveOperator()
     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)
     })
-
-    /*
-      
-
-
-     */
   }
 }
 
-// todo: potentially generalize to general notation-changing ops
-class Additive extends LinearOperators {
-  private val Set: MPath = Path.parseM("latin:/algebraic?Set")
-  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"))
-  ))
-
-  private object Symbols {
-    val binaryOp: GlobalName = Path.parseS("latin:/algebraic?Magma?op")
-    val inverseOp: GlobalName = Path.parseS("latin:/algebraic?InverseOperator?inv")
-    val unit: GlobalName = Path.parseS("latin:/algebraic?UnitElement?unit")
-  }
-
-  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 = Infix(Delim("+"), 0, 2, Some(true))),
-        List(LocalName("plus"))
-      )),
-      Symbols.inverseOp -> (() => (
-        c.not.get.copy(fixity = Prefix(Delim("-"), 0, 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 = ops("A")(c.name),
-      alias = c.alias.map(ops("A")(_)) ++ 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)
-
-    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) :: ops("A")(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)
-    }
+object PolymorphifyTest extends MagicTest("debug") with DiagramOperatorHelper {
+  override def run(): Unit = {
+    val magma = Path.parseM("latin:/algebraic?Magma")
 
-    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 : _*)
+    val op = new PolymorphifySFOL
+    val interp = new DiagramInterpreter(controller, Context.empty, new ErrorLogger(controller.report))
+    op.applyModule(controller.getModule(magma))(interp)
 
-    interp.add(newC)
+    interp.getAddedModules.foreach(m => {
+      controller.presenter.apply(m)(ConsoleWriter)
+    })
   }
 }