From 77311592666d71dd5e29c900fed9fe0d7b61f0d4 Mon Sep 17 00:00:00 2001 From: ComFreek Date: Fri, 26 Apr 2024 19:16:36 +0200 Subject: [PATCH] diagops: add polymorphify [skip ci] --- .../diagrams/oldstuff/PushoutOperator.scala | 1 + .../mmt/api/notations/NotationContainer.scala | 1 + .../mmt/api/notations/NotationExtension.scala | 5 +- .../info/kwarc/mmt/api/objects/Traverse.scala | 8 +- src/test/DiagramOperatorTest.scala | 137 ++---------------- 5 files changed, 25 insertions(+), 127 deletions(-) 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 index 07deb94b4c..20d6d4f062 100644 --- 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 @@ -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} diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/notations/NotationContainer.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/notations/NotationContainer.scala index 28ece1b3be..2c9dbcbe8b 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/notations/NotationContainer.scala +++ b/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 = { diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/notations/NotationExtension.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/notations/NotationExtension.scala index 640ed69601..7b6987cbb6 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/notations/NotationExtension.scala +++ b/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) } /** diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/objects/Traverse.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/objects/Traverse.scala index 9b40fc6584..0e5cdb75ba 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/objects/Traverse.scala +++ b/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. diff --git a/src/test/DiagramOperatorTest.scala b/src/test/DiagramOperatorTest.scala index 8d3f8b3bac..5087243173 100644 --- a/src/test/DiagramOperatorTest.scala +++ b/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) + }) } }