Skip to content

Commit

Permalink
diagops [skip ci]
Browse files Browse the repository at this point in the history
  • Loading branch information
@ComFreek
ComFreek committed Apr 26, 2024
1 parent 5486762 commit a04b009
Show file tree
Hide file tree
Showing 3 changed files with 67 additions and 61 deletions.
59 changes: 30 additions & 29 deletions src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/NewStuff.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ trait LinearOperators {

abstract class LinearOperatorSpec(val key: Option[String], val renamer: MPath => MPath) {
def apply(m: MPath): MPath = renamer(m)
def apply(n: LocalName)(implicit interp: DiagramInterpreter): LocalName
}
sealed trait UnresolvedLinearOperatorSpec {
val key: Option[String]
Expand All @@ -49,6 +50,8 @@ trait LinearOperators {
override val renamer: MPath => MPath)
extends LinearOperatorSpec(key, renamer) with UnresolvedLinearOperatorSpec {

private lazy val equinamer = getEquinamer(this)
override def apply(n: LocalName)(implicit interp: DiagramInterpreter): LocalName = equinamer(n)
def applyDomain(m: MPath): MPath = metaFunctor(m).toMPath
}

Expand All @@ -69,13 +72,15 @@ trait LinearOperators {
}

object IdentityFunctorSpec {
def apply(dom: Diagram): LinearFunctorSpec = new LinearFunctorSpec(None, dom, dom, DiagramFunctor.identity(dom), x => x)
def apply(dom: Diagram): LinearFunctorSpec = LinearFunctorSpec(None, dom, dom, DiagramFunctor.identity(dom), x => x)
}
case class LinearConnectorSpec(override val key: Option[String],
dom: LinearFunctorSpec,
cod: LinearFunctorSpec,
metaConnector: DiagramConnection,
override val renamer: MPath => MPath) extends LinearOperatorSpec(key, renamer) {
override def apply(n: LocalName)(implicit interp: DiagramInterpreter): LocalName = ???

// 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)
}
Expand Down Expand Up @@ -109,19 +114,18 @@ trait LinearOperators {
def apply(n: LocalName)(implicit interp: DiagramInterpreter): LocalName
}

def getRenamer(opKey: String)(f: String => String): ConstantRenamer = {
val op = ops(opKey).asInstanceOf[LinearFunctorSpec]

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 getRenamer(opKey: String)(f: String => String): ConstantRenamer = getRenamer(ops(opKey).asInstanceOf[LinearFunctorSpec])(f)
def getRenamer(op: LinearFunctorSpec)(f: String => String): ConstantRenamer = 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(op: LinearFunctorSpec): ConstantRenamer = getRenamer(op)(x => x)
def getEquinamer(opKey: String): ConstantRenamer = getRenamer(opKey)(x => x)

/** DSL END **/
Expand Down Expand Up @@ -368,15 +372,13 @@ class NewPushout(m: Term, dom: MPath, cod: MPath) extends LinearOperators {
("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 newC = new FinalConstant(
home = OMMOD(ops("P")(c.parent)),
name = equinamer(c.name),
alias = c.alias.map(n => equinamer(n)),
name = ops("P")(c.name),
alias = c.alias.map(ops("P")(_)),
tpC = c.tpC.map(tr),
dfC = c.dfC.map(tr),
rl = c.rl,
Expand All @@ -385,17 +387,16 @@ class NewPushout(m: Term, dom: MPath, cod: MPath) extends LinearOperators {
)
newC.metadata.add(c.metadata.getAll : _*) // TODO: shall we translate meta data via tr(), too?
interp.add(newC)

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)
}
// 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)
}
}
10 changes: 5 additions & 5 deletions src/mmt-api/src/main/info/kwarc/mmt/api/notations/NotationExtension.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -217,7 +217,7 @@ abstract class SimpleFixity extends Fixity {
}

/** delimiter after a certain argument */
case class PrePostfix(delim: Delimiter, leftArgs: Int, expl: Int, rightArgsBracketed: Boolean = false, impl: Int = 0) extends SimpleFixity {
case class PrePostfix(override val delim: Delimiter, leftArgs: Int, override val expl: Int, rightArgsBracketed: Boolean = false, override val impl: Int = 0) extends SimpleFixity {
lazy val markers = if (expl != 0) {
val leftArgMarkers = (impl until impl+leftArgs).map(i=>SimpArg(i+1)).toList
val rightArgsMarkers = (impl+leftArgs until impl+expl).map(i=>SimpArg(i+1)).toList
Expand All @@ -229,7 +229,7 @@ case class PrePostfix(delim: Delimiter, leftArgs: Int, expl: Int, rightArgsBrack
}

/** delimiter followed by the (explicit) arguments */
case class Prefix(delim: Delimiter, impl: Int, expl: Int) extends SimpleFixity {
case class Prefix(override val delim: Delimiter, override val impl: Int, override val expl: Int) extends SimpleFixity {
lazy val markers = if (expl != 0) argsWithOp(0) else argsWithOp(0) ::: implArgs
def asString = ("prefix", simpleArgs)
def addInitialImplicits(n: Int) = copy(impl = impl+n)
Expand All @@ -239,7 +239,7 @@ case class Prefix(delim: Delimiter, impl: Int, expl: Int) extends SimpleFixity {
*
* @param assoc None/Some(true)/Some(false) for none, left, right; currently ignored
*/
case class Infix(delim: Delimiter, impl: Int, expl: Int, assoc: Option[Boolean]) extends SimpleFixity {
case class Infix(override val delim: Delimiter, override val impl: Int, override val expl: Int, assoc: Option[Boolean]) extends SimpleFixity {
lazy val markers = assoc match {
case Some(true) => argsWithOp(1)
case None => argsWithOp(1)
Expand All @@ -257,7 +257,7 @@ case class Infix(delim: Delimiter, impl: Int, expl: Int, assoc: Option[Boolean])
}

/** delimiter after the (explicit) arguments */
case class Postfix(delim: Delimiter, impl: Int, expl: Int) extends SimpleFixity {
case class Postfix(override val delim: Delimiter, override val impl: Int, override val expl: Int) extends SimpleFixity {
lazy val markers = argsWithOp(expl)
def asString = ("postfix", simpleArgs)
def addInitialImplicits(n: Int) = copy(impl = impl+n)
Expand All @@ -269,7 +269,7 @@ case class Postfix(delim: Delimiter, impl: Int, expl: Int) extends SimpleFixity
*
* assumes arguments are one variable and one scope; expl must be 1
*/
case class Bindfix(delim: Delimiter, impl: Int, expl: Int, assoc: Boolean) extends SimpleFixity {
case class Bindfix(override val delim: Delimiter, override val impl: Int, override val expl: Int, assoc: Boolean) extends SimpleFixity {
def markers = List(delim, Var(impl+1, true, None), Delim("."), SimpArg(impl+2))
def asString = {
val assocString = if (assoc) "-assoc" else ""
Expand Down
59 changes: 32 additions & 27 deletions src/test/DiagramOperatorTest.scala
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
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.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}
Expand Down Expand Up @@ -66,9 +66,16 @@ object DiagramAdditiveTest extends MagicTest("debug") with DiagramOperatorHelper
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(
Expand All @@ -83,17 +90,16 @@ class Additive extends LinearOperators {
val unit: GlobalName = Path.parseS("latin:/algebraic?UnitElement?unit")
}

private val equinamer = getEquinamer("A")

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 = Mixfix(List(SimpArg(1), Delim("+"), SimpArg(2)))),
c.not.get.copy(fixity = Infix(Delim("+"), 0, 2, Some(true))),
List(LocalName("plus"))
)),
Symbols.inverseOp -> (() => (
c.not.get.copy(fixity = Mixfix(List(Delim("-", associatesToLeft = false), SimpArg(1)))),
c.not.get.copy(fixity = Prefix(Delim("-"), 0, 1)),
List(LocalName("negate"))
)),
Symbols.unit -> (() => (
Expand All @@ -106,8 +112,8 @@ class Additive extends LinearOperators {

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),
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,
Expand All @@ -116,26 +122,25 @@ class Additive extends LinearOperators {
)
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)
}
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)
}
}

Expand Down

0 comments on commit a04b009

Please sign in to comment.