From 825538ebe226311fea584cba2c1bc71261dd2240 Mon Sep 17 00:00:00 2001 From: watcha473 Date: Tue, 12 Nov 2024 23:18:34 +0100 Subject: [PATCH 1/4] Init ModuleGeneratingPresenter for exporting theories to sTeX, extension: mmt-stex Signed-off-by: watcha473 --- .../mmt/latex/CompilingLatexPresenter.scala | 137 ++++++++++++++++++ src/mmt-api/resources/mmtrc | 1 + 2 files changed, 138 insertions(+) diff --git a/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala b/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala index 51720b046..85698a947 100644 --- a/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala +++ b/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala @@ -221,6 +221,143 @@ class MacroGeneratingPresenter extends Presenter(new MacroUsingPresenter) { */ } +/** + * compiles MMT to sTeX by producing + * a tex-file for each theory + * containing a symdef definition for each constant + */ +class ModuleGeneratingPresenter extends Presenter(new MacroUsingPresenter) { + def key = "mmt-stex" + + override val outExt = "tex" + + def apply(structuralElement : StructuralElement, standalone: Boolean = false)(implicit rh : RenderingHandler): Unit = { + structuralElement match { + case theory: Theory => doTheory(theory, standalone) + case declaration: Declaration => doDeclaration(declaration) + case _ => + } + } + + private def doTheory(theory: Theory, standalone: Boolean)(implicit rh : RenderingHandler): Unit = { + controller.simplifier(theory) + if (standalone) { + rh << s"% generated by MMT from theory ${theory.path}\n" + rh << s"\\documentclass{sTeX}\n" + rh << s"\\begin{document}\n" + } + rh << s" \\begin{smodule}{${theory.name.toString}}\n" + theory.meta foreach { mPath => + doDeclaration(PlainInclude(mPath, theory.path)) + } + theory.getDeclarationsElaborated.foreach { + declaration => doDeclaration(declaration) + } + rh << s" \\end{smodule}\n" + if (standalone) { + rh << s"\\end{document}\n" + } + } + + private def doDeclaration(declaration: Declaration)(implicit rh : RenderingHandler): Unit = { + declaration match { + case constant: Constant => doConstant(constant) + case i @ Include(id) => + // skip redundant includes + if (i.isGenerated) + return + // ignore includes of theories written in scala + if (id.from.doc.uri.scheme contains "scala") + return + val archive = controller.backend.findOwningArchive(id.from).getOrElse { + logError("cannot find archive holding " + id.from + " (ignoring)") + return + } + val pLAbs = archive / outDim / "content" / archives.Archive.MMTPathToContentPath(id.from.mainModule).stripExtension + val pLRel = archive.root.up.up.relativize(pLAbs) + val pL = pLRel.segments.mkString("/") + + val archivePath = archive.archString + val stexImportmodule = s" \\importmodule[${archivePath}]{${pL}}" + rh << s"${stexImportmodule}\n" + case _ => + } + } + + private def doConstant(constant: Constant)(implicit rh : RenderingHandler): Unit = { + val notation = constant.notC.getPresentDefault + var numArgs = notation match { + case None => 0 + case Some(tn) => + tn.arity.length + } + var notationBody = notation match { + case None => Common.translateDelim(constant.name.toString) + case Some(tn) => + // if an InferenceMarker occurs, the generated macro expects an additional argument for the inferred type + val doMarkers = new DoMarkers(constant.path, numArgs+1) + val tnS = doMarkers.doMarkers(tn.presentationMarkers) + if (doMarkers.infMarkerUsed) + numArgs += 1 + tnS + } + + var stexArgs = if (numArgs == 0) "" else s",args=${numArgs.toString}" + + // Handle seqArgs + if (notationBody.contains("SeqArg")){ + notationBody = notationBody.replace("SeqArg", "") + notationBody = "\\argsep{#1} " + notationBody + stexArgs = ",args=a" + } + + val stexSymdef = s" \\symdef{${constant.name}}[name=${constant.name}${stexArgs}]{${notationBody}}" + rh << stexSymdef + "\n" + } + + /** helper class to encapsulate the state of doMarkers */ + private class DoMarkers(p: GlobalName, infMarkerPos: Int) { + var infMarkerUsed: Boolean = false + /** convert notation markers into the body of a \newcommand */ + def doMarkers(ms: List[Marker]): String = { + val msS = ms.map { + case a: Arg => "#" + a.number.abs + case a: ImplicitArg => s"{\\prop}" + case s: SeqArg => "SeqArg" + case d: Delimiter => doDelim(d) + case Var(n, _, Some(sep), _) => "\\mmt@fold{" + doDelim(sep) + "}{" + "#" + n + "}" + case Var(n, _, None, _) => "#" + n + case GroupMarker(elements) => "{" + doMarkers(elements) + "}" + case ScriptMarker(main, sup, sub, over, under) => + var res = doM(main) + over.foreach {s => res = s"\\overset{${doM(s)}}{$res}"} + under.foreach {s => res = s"\\underset{${doM(s)}}{$res}"} + sup.foreach {s => res = s"{$res}^{${doM(s)}}"} + sub.foreach {s => res = s"{$res}_{${doM(s)}}"} + res + case FractionMarker(above, below, line) => + val aboveL = doMarkers(above) + val belowL = doMarkers(below) + val command = if (line) "frac" else "Frac" + s"\\$command{$aboveL}{$belowL}" + case InferenceMarker => + infMarkerUsed = true + "#" + infMarkerPos + case m => + logError("unexpected notation marker: " + m) + "ERROR" + } + msS.mkString(" ") + } + private def doM(m: Marker) = doMarkers(List(m)) + + private def doDelim(d: Delimiter) = { + val dL = Common.translateDelim(d.expand(p, Nil).text) + dL + } + } +} + /** * convert a term into a LaTeX expression (using lots of \ { and }) * diff --git a/src/mmt-api/resources/mmtrc b/src/mmt-api/resources/mmtrc index b1f642a2e..ee467182f 100644 --- a/src/mmt-api/resources/mmtrc +++ b/src/mmt-api/resources/mmtrc @@ -4,6 +4,7 @@ lf-scala info.kwarc.mmt.lf.ScalaExporter tptp-twelf info.kwarc.mmt.tptp.TPTPImporter scala-bin info.kwarc.mmt.api.archives.ScalaCompiler mmt-sty info.kwarc.mmt.latex.MacroGeneratingPresenter +mmt-stex info.kwarc.mmt.latex.ModuleGeneratingPresenter mmttex info.kwarc.mmt.latex.MMTTeXActionParser mws info.kwarc.mmt.api.archives.MWSHarvestExporter planetary info.kwarc.mmt.planetary.PlanetaryPresenter From a566f444f5eb1d437af12226f16c0684cb5ef88b Mon Sep 17 00:00:00 2001 From: watcha473 Date: Thu, 14 Nov 2024 13:19:29 +0100 Subject: [PATCH 2/4] Add handling of documents --- .../mmt/latex/CompilingLatexPresenter.scala | 52 +++++++++++++++++-- 1 file changed, 49 insertions(+), 3 deletions(-) diff --git a/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala b/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala index 85698a947..668aa9ee1 100644 --- a/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala +++ b/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala @@ -6,6 +6,7 @@ import frontend._ import symbols._ import modules._ import documents._ +import info.kwarc.mmt.api.opaque.{ObjFragment, OpaqueText, ScopeFragment, StringFragment} import objects._ import presentation._ import notations._ @@ -98,7 +99,7 @@ import Common._ * It is to be distinguished from visualizing presenters that turn MMT/X into LaTeX/MMT/X, e.g., by generating LaTeX that represent MMT source code. * A preliminary such presenter exists in commented-out code. */ -class MacroGeneratingPresenter extends Presenter(new MacroUsingPresenter) { +class MacroGeneratingPresenter extends Presenter(new MacroUsingPresenter) { def key = "mmt-sty" override val outExt = "sty" @@ -235,6 +236,7 @@ class ModuleGeneratingPresenter extends Presenter(new MacroUsingPresenter) { structuralElement match { case theory: Theory => doTheory(theory, standalone) case declaration: Declaration => doDeclaration(declaration) + case document: Document => doDocument(document, standalone) case _ => } } @@ -278,8 +280,7 @@ class ModuleGeneratingPresenter extends Presenter(new MacroUsingPresenter) { val pL = pLRel.segments.mkString("/") val archivePath = archive.archString - val stexImportmodule = s" \\importmodule[${archivePath}]{${pL}}" - rh << s"${stexImportmodule}\n" + rh << s" \\importmodule[${archivePath}]{${pL}}\n" case _ => } } @@ -315,6 +316,51 @@ class ModuleGeneratingPresenter extends Presenter(new MacroUsingPresenter) { rh << stexSymdef + "\n" } + private def doDocument(document: Document, standalone: Boolean)(implicit rh : RenderingHandler): Unit = { + + if (standalone) { + // exclude file-extension + rh << "% generated by MMT from document " + document.path + "\n" + rh << "begin{document}\n" + rh << s"\\documentclass{sTeX}\n" + } + document.getDeclarations foreach { + // Sections? + case nestedDocument: Document => doDocument(nestedDocument, standalone = false) + // Handle namespaces? + case mRef: MRef => controller.globalLookup.get(mRef.target) match { + case theory: Theory => doDocument(theory.asDocument, standalone = false) + case view: View => doDocument(view.asDocument, standalone = false) + } + case sRef: SRef => controller.globalLookup.get(sRef.target) match { + case declaration: Declaration => doDeclaration(declaration) + case _ => + } + case opaqueText: OpaqueText => doOpaque(opaqueText) + case _ => + } + if (standalone) { + rh << "\\end{document}\n" + } + } + + private def doOpaque(opaqueText: OpaqueText)(implicit rh: RenderingHandler): Unit = { + // All lines except the first are indented, needs clear formatting + opaqueText.text match { + case stringFragment: StringFragment => { + rh << stringFragment.value + "\n" + } + // case ObjFragment(o) => doObj(o) + case objectFragment: ObjFragment => { + rh << objectFragment.toString + } + // case ScopeFragment(body) => body.map(doOpaque).mkString() + case scopeFragment: ScopeFragment => { + rh << scopeFragment.toString + } + } + } + /** helper class to encapsulate the state of doMarkers */ private class DoMarkers(p: GlobalName, infMarkerPos: Int) { var infMarkerUsed: Boolean = false From 4d1f58cbddc2fc548dee7423e143de3892b9e444 Mon Sep 17 00:00:00 2001 From: watcha473 Date: Tue, 4 Feb 2025 14:03:03 +0100 Subject: [PATCH 3/4] The basic structure of the exporter with occasional latex errors which will be fixed in the next commit. --- .../mmt/latex/CompilingLatexPresenter.scala | 254 +++++++++++------- .../resources/unicode/unicode-ascii-map | 3 + .../kwarc/mmt/api/archives/BuildTarget.scala | 6 +- 3 files changed, 168 insertions(+), 95 deletions(-) diff --git a/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala b/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala index 668aa9ee1..ef26e5e0f 100644 --- a/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala +++ b/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala @@ -6,12 +6,15 @@ import frontend._ import symbols._ import modules._ import documents._ +import info.kwarc.mmt.api.objects.Obj.{getConstants, parseTerm} import info.kwarc.mmt.api.opaque.{ObjFragment, OpaqueText, ScopeFragment, StringFragment} import objects._ import presentation._ import notations._ import parser._ +import scala.collection.immutable.Queue + /** helper functions for latex presenter */ object Common { @@ -232,10 +235,12 @@ class ModuleGeneratingPresenter extends Presenter(new MacroUsingPresenter) { override val outExt = "tex" + private val mathclassMap = UnicodeMap.readMap("unicode/latex-mathclass-map") + def apply(structuralElement : StructuralElement, standalone: Boolean = false)(implicit rh : RenderingHandler): Unit = { structuralElement match { case theory: Theory => doTheory(theory, standalone) - case declaration: Declaration => doDeclaration(declaration) + case declaration: Declaration => doDeclaration(declaration, standalone) case document: Document => doDocument(document, standalone) case _ => } @@ -245,96 +250,199 @@ class ModuleGeneratingPresenter extends Presenter(new MacroUsingPresenter) { controller.simplifier(theory) if (standalone) { rh << s"% generated by MMT from theory ${theory.path}\n" - rh << s"\\documentclass{sTeX}\n" + rh << s"\\documentclass{article}\n" + rh << s"\\usepackage{stex}\n" + // Testing this package for use with special math symbols + rh << s"\\libinput{preamble}\n" rh << s"\\begin{document}\n" } - rh << s" \\begin{smodule}{${theory.name.toString}}\n" + rh << s"\\begin{smodule}{${theory.name.toString}}\n" theory.meta foreach { mPath => - doDeclaration(PlainInclude(mPath, theory.path)) + doDeclaration(PlainInclude(mPath, theory.path), standalone) } theory.getDeclarationsElaborated.foreach { - declaration => doDeclaration(declaration) + declaration => doDeclaration(declaration, standalone) } - rh << s" \\end{smodule}\n" + rh << s"\\end{smodule}\n" if (standalone) { rh << s"\\end{document}\n" } } - private def doDeclaration(declaration: Declaration)(implicit rh : RenderingHandler): Unit = { + private def doDeclaration(declaration: Declaration, standalone: Boolean)(implicit rh : RenderingHandler): Unit = { declaration match { - case constant: Constant => doConstant(constant) - case i @ Include(id) => + case constant: Constant => doConstant(constant, standalone) + case i @ Include(id) if standalone => // skip redundant includes if (i.isGenerated) return // ignore includes of theories written in scala if (id.from.doc.uri.scheme contains "scala") return - val archive = controller.backend.findOwningArchive(id.from).getOrElse { - logError("cannot find archive holding " + id.from + " (ignoring)") - return - } - val pLAbs = archive / outDim / "content" / archives.Archive.MMTPathToContentPath(id.from.mainModule).stripExtension - val pLRel = archive.root.up.up.relativize(pLAbs) - val pL = pLRel.segments.mkString("/") - - val archivePath = archive.archString - rh << s" \\importmodule[${archivePath}]{${pL}}\n" + val importString = buildIncludeString(id.from, standalone) + rh << importString case _ => } } - private def doConstant(constant: Constant)(implicit rh : RenderingHandler): Unit = { - val notation = constant.notC.getPresentDefault - var numArgs = notation match { - case None => 0 - case Some(tn) => - tn.arity.length + private def buildIncludeString(mPath: MPath, standalone: Boolean): String = { + val archive = controller.backend.findOwningArchive(mPath).getOrElse { + logError("cannot find archive holding " + mPath + " (ignoring)") + return "Could not build the Include String" + } + val pLAbs = archive / outDim / "content" / archives.Archive.MMTPathToContentPath(mPath.mainModule).stripExtension + val pLRel = archive.root.up.up.relativize(pLAbs) + val pL = pLRel.segments.mkString("/") + + // Testing in MathHub-dir, importmodule-string has to be changed accordingly ($-escapes causes errors in path recognition) + val archivePath = archive.archString + val filePath = pL.replaceFirst(archivePath, "").replaceFirst("/", "") + val moduleName = pL.slice(pL.lastIndexOf("/") + 1, pL.length).replace("$", "") + val modulePath = filePath.slice(0, filePath.lastIndexOf("/")) + s"?$moduleName" + if (standalone) { + println(s"\\importmodule[$archivePath]{$modulePath}") + s"\\importmodule[$archivePath]{$modulePath}\n" } - var notationBody = notation match { - case None => Common.translateDelim(constant.name.toString) - case Some(tn) => - // if an InferenceMarker occurs, the generated macro expects an additional argument for the inferred type - val doMarkers = new DoMarkers(constant.path, numArgs+1) - val tnS = doMarkers.doMarkers(tn.presentationMarkers) - if (doMarkers.infMarkerUsed) - numArgs += 1 - tnS + else { + println(s"\\usemodule[$archivePath]{$modulePath}") + s"\\usemodule[$archivePath]{$modulePath}\n" } + } - var stexArgs = if (numArgs == 0) "" else s",args=${numArgs.toString}" + private def doConstant(constant: Constant, standalone: Boolean)(implicit rh : RenderingHandler): Unit = { + val constantName = constant.name.toString + // Handle alias(es)? + // val constantAlias = constant.alias + var symdef = s"\\symdef{$constantName}[name=$constantName" + val notation = constant.notC.getParseDefault + notation match { + case None => symdef = symdef + s"]{$constantName}" + case Some(textNotation: TextNotation) => + val numArgs = textNotation.arity.length + // possible args: i, a, b, B. Need proper handling + val args = numArgs match { + case 0 => "]" + case n if n > 0 => s",args=$n]" + } + // assoc not important for now, focus on notation only + // possible assoc: pre, bin, binl, binr, conj. Need proper handling + // val assoc = if (numArgs > 1) ",assoc=bin" else ",assoc=pre" + // precedence not important for now, focus on notation only + // precedence in sTeX is handled differently, need to convert + // val prec = s",prec=${textNotation.precedence.toString}" + val stexNotation = doNotation(textNotation, constant.path) - // Handle seqArgs - if (notationBody.contains("SeqArg")){ - notationBody = notationBody.replace("SeqArg", "") - notationBody = "\\argsep{#1} " + notationBody - stexArgs = ",args=a" + symdef = symdef + args + stexNotation + } + if (standalone) { + rh << s"$symdef\n" + } + else { + rh << s"Let $constantName be a constant such that...\n" + } + } + + // ToDo: symbol "brackets" in mmt?mmt seems not right + private def doNotation(textNotation: TextNotation, constantGlobalName: GlobalName): String = { + println(s"Constant: $constantGlobalName") + println(s"Notation: $textNotation") + + var notation = "{" + + val markers = textNotation.presentationMarkers + + markers.foreach { + case argument: Arg => + notation = notation + s"#${argument.number} " + case simpSeqArg: SimpSeqArg => + println(s"DEBUG: $textNotation") + println(s" SimpSeqArg: $simpSeqArg") + case implicitArg: ImplicitArg => + println(s"DEBUG: $textNotation") + println(s" ImplicitArg: $implicitArg") + case labelSeqArg: LabelSeqArg => + println(s"DEBUG: $textNotation") + println(s" LabelSeqArg: $labelSeqArg") + case scriptMarker: ScriptMarker => + println(s"DEBUG: $textNotation") + println(s" ScriptMarker: $scriptMarker") + case fractionMarker: FractionMarker => + println(s"DEBUG: $textNotation") + println(s" FractionMarker: $fractionMarker") + case delimiter: Delimiter => + val translatedDelimiter = doDelimiter(delimiter, constantGlobalName) + notation = notation + translatedDelimiter + case variable: Var => + notation = notation + s"${variable.toString} " } - val stexSymdef = s" \\symdef{${constant.name}}[name=${constant.name}${stexArgs}]{${notationBody}}" - rh << stexSymdef + "\n" + notation + "}" + } + + private def doDelimiter(delimiter: Delimiter, constantGlobalName: GlobalName): String = { + val translatedDelimiter = Common.translateDelim(delimiter.expand(constantGlobalName, Nil).text) + val delimWithClassWrapper = decideDelimiterClass(translatedDelimiter) + delimWithClassWrapper } + private def decideDelimiterClass(delimiterString: String): String = { + val trimmedDelimiter = delimiterString.trim() + var wrappedDelimiter = catchUnknownMacros(trimmedDelimiter) + + var debugFoundClass = false + mathclassMap.foreach { symbolClassPair => + if (symbolClassPair._1 == wrappedDelimiter) { + wrappedDelimiter = s" ${symbolClassPair._2}{\\maincomp{$wrappedDelimiter}} " + debugFoundClass = true + } + } + if (!debugFoundClass) { + println(s"No class found for delimiter, add to mathclassMap: $wrappedDelimiter") + } + + wrappedDelimiter + } + + // Some macros from unicode-latex-map do not get recognized, convert to a accepted equivalent + private def catchUnknownMacros(delimiter: String): String = { + delimiter match { + case "\\der" => "\\rightassert" + case "\\rA" => "\\rightarrow" + case "\\lrA" => "\\leftrightarrow" + case "\\lbracket" => "\\lbrack" + case "\\rbracket" => "\\rbrack" + case "\\{" => "\\lbrace" + case "\\}" => "\\rbrace" + case _ => delimiter + } + } + + // Exclude directories from getting handled like documents private def doDocument(document: Document, standalone: Boolean)(implicit rh : RenderingHandler): Unit = { if (standalone) { - // exclude file-extension - rh << "% generated by MMT from document " + document.path + "\n" - rh << "begin{document}\n" - rh << s"\\documentclass{sTeX}\n" + rh << s"% generated by MMT from document ${document.path}\n" + rh << s"\\documentclass{article}\n" + rh << s"\\usepackage{stex}\n" + // Testing this package for use with special math symbols + rh << s"\\libinput{preamble}\n" + rh << "\\begin{document}\n" } document.getDeclarations foreach { // Sections? case nestedDocument: Document => doDocument(nestedDocument, standalone = false) // Handle namespaces? case mRef: MRef => controller.globalLookup.get(mRef.target) match { - case theory: Theory => doDocument(theory.asDocument, standalone = false) + case theory: Theory => + val importString = buildIncludeString(mRef.target, standalone = false) + rh << importString + rh << s"Theory: ${theory.name}\n" + doDocument(theory.asDocument, standalone = false) case view: View => doDocument(view.asDocument, standalone = false) } case sRef: SRef => controller.globalLookup.get(sRef.target) match { - case declaration: Declaration => doDeclaration(declaration) - case _ => + case declaration: Declaration => doDeclaration(declaration, standalone = false) + case _ => } case opaqueText: OpaqueText => doOpaque(opaqueText) case _ => @@ -348,58 +456,16 @@ class ModuleGeneratingPresenter extends Presenter(new MacroUsingPresenter) { // All lines except the first are indented, needs clear formatting opaqueText.text match { case stringFragment: StringFragment => { - rh << stringFragment.value + "\n" + rh << s"${stringFragment.value}\n" } // case ObjFragment(o) => doObj(o) case objectFragment: ObjFragment => { - rh << objectFragment.toString + rh << s"${objectFragment.toString}\n" } // case ScopeFragment(body) => body.map(doOpaque).mkString() case scopeFragment: ScopeFragment => { - rh << scopeFragment.toString - } - } - } - - /** helper class to encapsulate the state of doMarkers */ - private class DoMarkers(p: GlobalName, infMarkerPos: Int) { - var infMarkerUsed: Boolean = false - /** convert notation markers into the body of a \newcommand */ - def doMarkers(ms: List[Marker]): String = { - val msS = ms.map { - case a: Arg => "#" + a.number.abs - case a: ImplicitArg => s"{\\prop}" - case s: SeqArg => "SeqArg" - case d: Delimiter => doDelim(d) - case Var(n, _, Some(sep), _) => "\\mmt@fold{" + doDelim(sep) + "}{" + "#" + n + "}" - case Var(n, _, None, _) => "#" + n - case GroupMarker(elements) => "{" + doMarkers(elements) + "}" - case ScriptMarker(main, sup, sub, over, under) => - var res = doM(main) - over.foreach {s => res = s"\\overset{${doM(s)}}{$res}"} - under.foreach {s => res = s"\\underset{${doM(s)}}{$res}"} - sup.foreach {s => res = s"{$res}^{${doM(s)}}"} - sub.foreach {s => res = s"{$res}_{${doM(s)}}"} - res - case FractionMarker(above, below, line) => - val aboveL = doMarkers(above) - val belowL = doMarkers(below) - val command = if (line) "frac" else "Frac" - s"\\$command{$aboveL}{$belowL}" - case InferenceMarker => - infMarkerUsed = true - "#" + infMarkerPos - case m => - logError("unexpected notation marker: " + m) - "ERROR" + rh << s"${scopeFragment.toString}\n" } - msS.mkString(" ") - } - private def doM(m: Marker) = doMarkers(List(m)) - - private def doDelim(d: Delimiter) = { - val dL = Common.translateDelim(d.expand(p, Nil).text) - dL } } } diff --git a/src/mmt-api/resources/unicode/unicode-ascii-map b/src/mmt-api/resources/unicode/unicode-ascii-map index 9197d9328..7547c1f69 100644 --- a/src/mmt-api/resources/unicode/unicode-ascii-map +++ b/src/mmt-api/resources/unicode/unicode-ascii-map @@ -7,8 +7,11 @@ <=>|⇔ // long arrows -->|⟶ +--->|⟶ <--|⟵ +<---|⟶ <-->|⟷ +<--->|⟷ ==>|⟹ <==|⟸ <==>|⟺ diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/archives/BuildTarget.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/archives/BuildTarget.scala index 08f642d6b..addbff970 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/archives/BuildTarget.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/archives/BuildTarget.scala @@ -297,7 +297,11 @@ abstract class TraversingBuildTarget extends BuildTarget { children: Option[List[BuildTask]],eCOpt: Option[ErrorHandler]): BuildTask = { val ew = makeHandler(a,inPath,children.isDefined) val errorCont = MultipleErrorHandler(new ErrorContainer :: ew :: eCOpt.toList, report) - val outFile = if (children.isDefined) getFolderOutFile(a,inPath) else getOutFile(a,inPath) + + // Change outFile to path without $ + val segmentsForInPathForStex = inPath.map(segment => segment.replace("$", "")) + val inPathForStex = new FilePath(segmentsForInPathForStex) + val outFile = if (children.isDefined) getFolderOutFile(a,inPathForStex) else getOutFile(a,inPathForStex) new BuildTask(key,a,inFile,children,inPath,outFile,errorCont) } From cf8bc8e8bd60810bfb14f78c1bdaae273d0e01b7 Mon Sep 17 00:00:00 2001 From: watcha473 Date: Sun, 17 Aug 2025 04:33:55 +0200 Subject: [PATCH 4/4] init mmt-stex --- .../mmt/latex/CompilingLatexPresenter.scala | 568 +++++++++++++----- .../resources/unicode/latex-mathclass-map | 117 ++++ .../resources/unicode/unicode-latex-map | 142 ++--- .../kwarc/mmt/api/archives/BuildTarget.scala | 6 +- 4 files changed, 589 insertions(+), 244 deletions(-) create mode 100644 src/mmt-api/resources/unicode/latex-mathclass-map diff --git a/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala b/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala index ef26e5e0f..bec905799 100644 --- a/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala +++ b/src/latex-mmt/src/info/kwarc/mmt/latex/CompilingLatexPresenter.scala @@ -2,21 +2,22 @@ package info.kwarc.mmt.latex import info.kwarc.mmt.api._ import utils._ -import frontend._ import symbols._ import modules._ import documents._ import info.kwarc.mmt.api.objects.Obj.{getConstants, parseTerm} -import info.kwarc.mmt.api.opaque.{ObjFragment, OpaqueText, ScopeFragment, StringFragment} +import info.kwarc.mmt.api.opaque.{ObjFragment, OpaqueText, ScopeFragment, StringFragment, TextFragment} import objects._ import presentation._ import notations._ import parser._ -import scala.collection.immutable.Queue +import java.nio.file._ +import java.nio.file.attribute.BasicFileAttributes +import scala.sys.process.Process -/** helper functions for latex presenter */ +/** helper functions for latex/stex presenter */ object Common { def doConstantName(p: GlobalName) = { val mod = doLocalName(p.module.name) @@ -28,6 +29,15 @@ object Common { case ComplexStep(p) => doLocalName(p.name) }.mkString("@") + def doSymbolName(p: GlobalName) = { + "\\" + "MMT" + Common.translateName(escapeToCamelCase(p.name.dropComplex.toString)) + } + + def escapeToCamelCase(name: String): String = { + val nameParts = name.split("[_/]") + nameParts.head + nameParts.tail.map(_.capitalize).mkString + } + /** translate each character in s according to by */ private def translate(s: String, by: Char => Option[String]): String = s.map {c => by(c).getOrElse(c.toString)}.mkString("") @@ -36,16 +46,22 @@ object Common { /** translates a string making up an MMT name into a latex name */ def translateName(s: String) = translate(s, c => utils.listmap(commandEscapes, c) orElse rawUnicodeMap.get(c)) - + + /** translates a unicode-containing string into a LaTeX-acceptable version (used for translating OpaqueText) */ + def translateOpaqueStringFragment(s: String): String = translate(s, c => if (allowedOpaqueChars.contains(c.toString)) Option(c.toString) else macroUnicodeMapForOpaqueStringFragment(c)) + /** escapes of characters within latex commands */ private val commandEscapes = "\\_-1234567890".toList zip List("B", "U", "M", "One", "Two", "Three", "Four", "Five", "Six", "Seven", "Eight", "Nine", "Zero") /** escapes of characters within latex delimiters */ private val delimEscapes = '\\' -> "\\backslash " :: '~' -> "\\sim " :: ' ' -> "\\;" :: "$#%&{}_^".toList.map(c => (c, "\\" + c)) + /** Elements in OpaqueText that should NOT be translated */ + private val allowedOpaqueChars = List("{", "}", "[", "]", "(", ")") /** maintains a map of unicode-latex replacements, populated on initialization from the resource as jEdit abbreviations - * later maps overwrite earlier ones; so make sure the resource always contain the non-standard commands (e.g., \ra) before their latex analogs + * later maps overwrite earlier ones; so make sure the resource always contain the non-standard commands (e.g., \ra) before their latex analogs */ private val rawUnicodeMap = new scala.collection.mutable.HashMap[Char,String]() private def macroUnicodeMap(c: Char): Option[String] = rawUnicodeMap.get(c).map(x => "\\" + x + " ") + private def macroUnicodeMapForOpaqueStringFragment(c: Char): Option[String] = rawUnicodeMap.get(c).map(x => "$\\" + x + "$ ") private val inverseUnicodeMap = new scala.collection.mutable.HashMap[String,String] /** this is not used by default; users can add it as a rule if they have difficulties typing Unicode characters in LaTeX */ object LatexToUnicodeConverter extends LexerExtension { @@ -72,7 +88,7 @@ object Common { fillMap(basicmap) } init - + private def fillMap(map: List[(String,String)]): Unit = { map.foreach {case (c,r) => // command starts with j @@ -95,9 +111,9 @@ import Common._ * compiles MMT to LaTeX by producing * * a sty-file for each theory * * containing a macro definition for each constant - * + * * type and definiens are ignored, only notations are used - * + * * This is 'compiling' in the sense that MMT/X is turned into LaTeX/X. * It is to be distinguished from visualizing presenters that turn MMT/X into LaTeX/MMT/X, e.g., by generating LaTeX that represent MMT source code. * A preliminary such presenter exists in commented-out code. @@ -106,7 +122,7 @@ class MacroGeneratingPresenter extends Presenter(new MacroUsingPresenter) { def key = "mmt-sty" override val outExt = "sty" - + def apply(e : StructuralElement, standalone: Boolean = false)(implicit rh : RenderingHandler): Unit = { e match { case t: Theory => doTheory(t) @@ -117,7 +133,6 @@ class MacroGeneratingPresenter extends Presenter(new MacroUsingPresenter) { private def doTheory(dt: Theory)(implicit rh : RenderingHandler): Unit = { controller.simplifier(dt) - rh << "% generated by MMT from theory " + dt.path + "\n" dt.meta foreach {m => doDeclaration(PlainInclude(m, dt.path)) } @@ -133,7 +148,7 @@ class MacroGeneratingPresenter extends Presenter(new MacroUsingPresenter) { // skip redundant includes if (i.isGenerated) return - // ignore includes of theories written in scala + // ignore includes of theories written in scala if (id.from.doc.uri.scheme contains "scala") return val arch = controller.backend.findOwningArchive(id.from).getOrElse { @@ -147,7 +162,7 @@ class MacroGeneratingPresenter extends Presenter(new MacroUsingPresenter) { case _ => } } - + private def doConstant(c: Constant)(implicit rh : RenderingHandler): Unit = { val not = c.notC.getPresentDefault var numArgs = not match { @@ -171,7 +186,7 @@ class MacroGeneratingPresenter extends Presenter(new MacroUsingPresenter) { /** helper class to encapsulate the state of doMarkers */ private class DoMarkers(p: GlobalName, infMarkerPos: Int) { - var infMarkerUsed: Boolean = false + var infMarkerUsed: Boolean = false /** convert notation markers into the body of a \newcommand */ def doMarkers(ms: List[Marker]): String = { val msS = ms.map { @@ -204,13 +219,13 @@ class MacroGeneratingPresenter extends Presenter(new MacroUsingPresenter) { msS.mkString("") } private def doM(m: Marker) = doMarkers(List(m)) - + private def doDelim(d: Delimiter) = { val dL = Common.translateDelim(d.expand(p, Nil).text) s"\\mmt@symref{${p.toPath}}{$dL}" } } - + /* private def requirePackage(p: MPath, bf: BuildTask): String = { controller.backend.findOwningArchive(p) match { @@ -226,18 +241,22 @@ class MacroGeneratingPresenter extends Presenter(new MacroUsingPresenter) { } /** - * compiles MMT to sTeX by producing - * a tex-file for each theory - * containing a symdef definition for each constant + * Converts MMT to sTeX by producing + * a smodule for each theory + * containing a symdef definition for each constant. + * Additionally, every MMT Document gets an informal version + * realized in a sTeX file as well. + * By using the OpaqueText String escape, LaTex can be embedded + * in the MMT Document and gets passed through to the sTeX file. */ -class ModuleGeneratingPresenter extends Presenter(new MacroUsingPresenter) { +class ModuleGeneratingPresenter extends Presenter(new SymbolUsingPresenter) { def key = "mmt-stex" override val outExt = "tex" private val mathclassMap = UnicodeMap.readMap("unicode/latex-mathclass-map") - def apply(structuralElement : StructuralElement, standalone: Boolean = false)(implicit rh : RenderingHandler): Unit = { + def apply(structuralElement: StructuralElement, standalone: Boolean = false)(implicit rh: RenderingHandler): Unit = { structuralElement match { case theory: Theory => doTheory(theory, standalone) case declaration: Declaration => doDeclaration(declaration, standalone) @@ -246,30 +265,32 @@ class ModuleGeneratingPresenter extends Presenter(new MacroUsingPresenter) { } } - private def doTheory(theory: Theory, standalone: Boolean)(implicit rh : RenderingHandler): Unit = { + private def doTheory(theory: Theory, standalone: Boolean)(implicit rh: RenderingHandler): Unit = { controller.simplifier(theory) if (standalone) { - rh << s"% generated by MMT from theory ${theory.path}\n" - rh << s"\\documentclass{article}\n" - rh << s"\\usepackage{stex}\n" - // Testing this package for use with special math symbols - rh << s"\\libinput{preamble}\n" - rh << s"\\begin{document}\n" - } - rh << s"\\begin{smodule}{${theory.name.toString}}\n" + rh << "\\documentclass[12pt]{article}" + "\n" + rh << "\\usepackage{stex}" + "\n" + rh << "\\libinput{mmt-stex}" + "\n" + rh << "\\begin{document}" + "\n" + rh << "\n" + } + rh << s"\\begin{smodule}{${theory.name.toString}}" + "\n" theory.meta foreach { mPath => doDeclaration(PlainInclude(mPath, theory.path), standalone) } - theory.getDeclarationsElaborated.foreach { - declaration => doDeclaration(declaration, standalone) + theory.getDeclarationsElaborated.foreach { declaration => + doDeclaration(declaration, standalone) } - rh << s"\\end{smodule}\n" + rh << "\\end{smodule}" + "\n" if (standalone) { - rh << s"\\end{document}\n" + rh << "\n" + rh << "\\end{document}" + rh << "\n" + rh << s"% Generated with mmt-stex from ${theory.parent.toString.replace("_", "\\_").replace(".omdoc", ".mmt")}" + "\n" } } - private def doDeclaration(declaration: Declaration, standalone: Boolean)(implicit rh : RenderingHandler): Unit = { + private def doDeclaration(declaration: Declaration, standalone: Boolean)(implicit rh: RenderingHandler): Unit = { declaration match { case constant: Constant => doConstant(constant, standalone) case i @ Include(id) if standalone => @@ -279,127 +300,165 @@ class ModuleGeneratingPresenter extends Presenter(new MacroUsingPresenter) { // ignore includes of theories written in scala if (id.from.doc.uri.scheme contains "scala") return - val importString = buildIncludeString(id.from, standalone) - rh << importString + rh << doInclude(id.from, standalone) + "\n" case _ => } } - private def buildIncludeString(mPath: MPath, standalone: Boolean): String = { + private def doInclude(mPath: MPath, standalone: Boolean): String = { val archive = controller.backend.findOwningArchive(mPath).getOrElse { - logError("cannot find archive holding " + mPath + " (ignoring)") - return "Could not build the Include String" - } + logError("cannot find archive holding " + mPath + " (ignoring)") + return "Could not build the Include String" + } + val archiveId = archive.archString + val moduleName = mPath.name.toString val pLAbs = archive / outDim / "content" / archives.Archive.MMTPathToContentPath(mPath.mainModule).stripExtension val pLRel = archive.root.up.up.relativize(pLAbs) - val pL = pLRel.segments.mkString("/") + val pL = pLRel.segments.dropWhile(_ != "mmt-stex").mkString("/") + val modulePath = pL.slice(0, pL.lastIndexOf("/")) + "?" + moduleName + if (standalone){ + s"\\importmodule[$archiveId]{$modulePath}" + } + else { + s"\\usemodule[$archiveId]{$modulePath}" + } + } + + private def doConstant(constant: Constant, standalone: Boolean)(implicit rh: RenderingHandler): Unit = { + val constantName = constant.name.dropComplex.toString + val macroName = Common.translateName(Common.escapeToCamelCase(constantName)) + + var symdef = s"\\symdef{MMT$macroName}[name=$macroName" + val (args, argsList, argsInOrderAsProvided) = doArgs(constant) - // Testing in MathHub-dir, importmodule-string has to be changed accordingly ($-escapes causes errors in path recognition) - val archivePath = archive.archString - val filePath = pL.replaceFirst(archivePath, "").replaceFirst("/", "") - val moduleName = pL.slice(pL.lastIndexOf("/") + 1, pL.length).replace("$", "") - val modulePath = filePath.slice(0, filePath.lastIndexOf("/")) + s"?$moduleName" + if (argsList.isEmpty) { + symdef += s"]{$macroName}" + } + else { + val precedence = doPrecedence(constant) + val notation = doNotation(constant, argsInOrderAsProvided) + + symdef += s"$args$precedence]{$notation}" + } if (standalone) { - println(s"\\importmodule[$archivePath]{$modulePath}") - s"\\importmodule[$archivePath]{$modulePath}\n" + rh << symdef + "\n" } else { - println(s"\\usemodule[$archivePath]{$modulePath}") - s"\\usemodule[$archivePath]{$modulePath}\n" + rh << convertToInformal(constant, macroName, argsList) + "\\\\" + "\n" } } - private def doConstant(constant: Constant, standalone: Boolean)(implicit rh : RenderingHandler): Unit = { - val constantName = constant.name.toString - // Handle alias(es)? - // val constantAlias = constant.alias - var symdef = s"\\symdef{$constantName}[name=$constantName" + private def doArgs(constant: Constant): (String, List[String], List[Int]) = { val notation = constant.notC.getParseDefault notation match { - case None => symdef = symdef + s"]{$constantName}" + case None => ("", List(), List()) case Some(textNotation: TextNotation) => - val numArgs = textNotation.arity.length - // possible args: i, a, b, B. Need proper handling - val args = numArgs match { - case 0 => "]" - case n if n > 0 => s",args=$n]" + var markers = textNotation.presentationMarkers + if (markers.exists(marker => marker.isInstanceOf[ScriptMarker])) { + markers = textNotation.parsingMarkers } - // assoc not important for now, focus on notation only - // possible assoc: pre, bin, binl, binr, conj. Need proper handling - // val assoc = if (numArgs > 1) ",assoc=bin" else ",assoc=pre" - // precedence not important for now, focus on notation only - // precedence in sTeX is handled differently, need to convert - // val prec = s",prec=${textNotation.precedence.toString}" - val stexNotation = doNotation(textNotation, constant.path) - - symdef = symdef + args + stexNotation - } - if (standalone) { - rh << s"$symdef\n" - } - else { - rh << s"Let $constantName be a constant such that...\n" - } + val argNums = markers.collect { + case arg: Arg => arg.number + case seqArg: SeqArg => seqArg.number + case variable: Var => variable.number + } + if (argNums.isEmpty) return ("", List(), List()) + val argsSorted = argNums.distinct.sorted + val rankMapping = argsSorted.zipWithIndex.map { case (value, index) => value -> (index + 1) }.toMap + val argsInOrderAsProvided = argNums.map(rankMapping) + val argsPos = markers.collect { + case _: Arg => "i" + case _: SeqArg => "a" + case variable: Var => if (variable.isSequence) "B" else "b" + } + val zippedPosAndNumArgs = argsInOrderAsProvided.zip(argsPos) + val zippedSorted = zippedPosAndNumArgs.sortBy(_._1) + val argsPosSortedList = zippedSorted.map(_._2) + val argsPosSortedString = ",args=" + argsPosSortedList.mkString("") + (argsPosSortedString, argsPosSortedList, argsInOrderAsProvided) + } } - // ToDo: symbol "brackets" in mmt?mmt seems not right - private def doNotation(textNotation: TextNotation, constantGlobalName: GlobalName): String = { - println(s"Constant: $constantGlobalName") - println(s"Notation: $textNotation") - - var notation = "{" - - val markers = textNotation.presentationMarkers - - markers.foreach { - case argument: Arg => - notation = notation + s"#${argument.number} " - case simpSeqArg: SimpSeqArg => - println(s"DEBUG: $textNotation") - println(s" SimpSeqArg: $simpSeqArg") - case implicitArg: ImplicitArg => - println(s"DEBUG: $textNotation") - println(s" ImplicitArg: $implicitArg") - case labelSeqArg: LabelSeqArg => - println(s"DEBUG: $textNotation") - println(s" LabelSeqArg: $labelSeqArg") - case scriptMarker: ScriptMarker => - println(s"DEBUG: $textNotation") - println(s" ScriptMarker: $scriptMarker") - case fractionMarker: FractionMarker => - println(s"DEBUG: $textNotation") - println(s" FractionMarker: $fractionMarker") - case delimiter: Delimiter => - val translatedDelimiter = doDelimiter(delimiter, constantGlobalName) - notation = notation + translatedDelimiter - case variable: Var => - notation = notation + s"${variable.toString} " - } - - notation + "}" - } - - private def doDelimiter(delimiter: Delimiter, constantGlobalName: GlobalName): String = { - val translatedDelimiter = Common.translateDelim(delimiter.expand(constantGlobalName, Nil).text) - val delimWithClassWrapper = decideDelimiterClass(translatedDelimiter) - delimWithClassWrapper + // MMT: has a higher precedence (and thus a higher binding strength) + // stex: The lower a precedence, the stronger a notation binds its arguments + // If symbol takes no args -> no prec (NOT prec=0 !!!) + private def doPrecedence(constant: Constant): String = { + val notation = constant.notC.getParseDefault + notation match { + case None => "" + case Some(textNotation: TextNotation) => + val prec = textNotation.precedence.toString.toInt + val stexPrec = -prec + s",prec=${stexPrec.toString}" + } } - private def decideDelimiterClass(delimiterString: String): String = { - val trimmedDelimiter = delimiterString.trim() - var wrappedDelimiter = catchUnknownMacros(trimmedDelimiter) + private def doNotation(constant: Constant, argsInOrderAsProvided: List[Int]): String = { + val notation = constant.notC.getParseDefault + notation match { + case None => "" + case Some(textNotation: TextNotation) => + var markers = textNotation.presentationMarkers + if (markers.exists(marker => marker.isInstanceOf[ScriptMarker])) { + markers = textNotation.parsingMarkers + } + + val numDelimiter = markers.count(marker => marker.isInstanceOf[Delimiter]) + val useMainCompIdentifier = if (numDelimiter > 1) false else true + + var argCounter = 0 + markers.map { + case _: Arg => + val argNum = argsInOrderAsProvided(argCounter) + argCounter += 1 + s"#$argNum " + case seqArg: SeqArg => + val argNum = argsInOrderAsProvided(argCounter) + argCounter += 1 + val seqDelimiter = doDelimiter(seqArg.sep, constant.path, useMainCompIdentifier) + s"\\argsep{#$argNum}{$seqDelimiter} " + case delimiter: Delimiter => + val translatedDelimiter = doDelimiter(delimiter, constant.path, useMainCompIdentifier) + translatedDelimiter + case variable: Var => + val argNum = argsInOrderAsProvided(argCounter) + argCounter += 1 + variable.sep match { + case Some(delimiter) => + val variableSeqDelimiter = doDelimiter(delimiter, constant.path, useMainCompIdentifier) + s"\\argsep{#$argNum}{$variableSeqDelimiter} " + case None => + s"#$argNum " + } + case _ => + }.mkString + } + } + + private def doDelimiter(delimiter: Delimiter, constantGlobalName: GlobalName, useMainCompIdentifier: Boolean): String = { + val translatedDelimiter = Common.translateDelim(delimiter.expand(constantGlobalName, Nil).text) + var wrappedDelimiter = catchUnknownMacros(translatedDelimiter.trim) - var debugFoundClass = false + var hasMathClass = false mathclassMap.foreach { symbolClassPair => if (symbolClassPair._1 == wrappedDelimiter) { - wrappedDelimiter = s" ${symbolClassPair._2}{\\maincomp{$wrappedDelimiter}} " - debugFoundClass = true + if (useMainCompIdentifier) { + wrappedDelimiter = s" ${symbolClassPair._2}{\\maincomp{$wrappedDelimiter}} " + } + else { + wrappedDelimiter = s" ${symbolClassPair._2}{\\comp{$wrappedDelimiter}} " + } + hasMathClass = true } } - if (!debugFoundClass) { - println(s"No class found for delimiter, add to mathclassMap: $wrappedDelimiter") + if (!hasMathClass) { + if (useMainCompIdentifier) { + wrappedDelimiter = s" \\mathord{\\maincomp{$wrappedDelimiter}} " + } + else { + wrappedDelimiter = s" \\mathord{\\comp{$wrappedDelimiter}} " + } } - wrappedDelimiter } @@ -413,60 +472,253 @@ class ModuleGeneratingPresenter extends Presenter(new MacroUsingPresenter) { case "\\rbracket" => "\\rbrack" case "\\{" => "\\lbrace" case "\\}" => "\\rbrace" + case "↯" => "contra" case _ => delimiter } } - // Exclude directories from getting handled like documents - private def doDocument(document: Document, standalone: Boolean)(implicit rh : RenderingHandler): Unit = { + private def convertToInformal(constant: Constant, constantName: String, argsList: List[String]): String = { + val numArgs = argsList.length + if (numArgs == 0) { + // Check if constant has a type defined + val constAnalyzedTerm = constant.tpC.getAnalyzedIfFullyChecked + constAnalyzedTerm match { + case Some(_) => + val constType = getConstants(constAnalyzedTerm.get).last.name.toString + if (constType == "type") + s"The symbol \\textbf{$constantName} represents a \\textcolor{violet}{$constType}. \\\\" + "\n" + s"Notation: $$\\MMT$constantName$$. \\\\" + "\n" + else + s"The constant \\textbf{$constantName} has the type: \\textcolor{violet}{$constType}. \\\\" + "\n" + s"Notation: $$\\MMT$constantName$$. \\\\" + "\n" + case None => + s"The constant \\textbf{$constantName} has the Notation: $$\\MMT$constantName$$. \\\\" + "\n" + } + } + else { + val notationArgs = ('a' to 'z').slice(0, numArgs) + val argsElaborated = argsList.zipWithIndex.map { + case ("i", index) => s"\\textit{${notationArgs(index)}} is a simple Argument. \\\\" + case ("a", index) => s"\\textit{${notationArgs(index)}} is an Argument Sequence. \\\\" + case ("b", index) => s"\\textit{${notationArgs(index)}} is an Argument bound by the constant. \\\\" + case ("B", index) => s"\\textit{${notationArgs(index)}} is an Argument Sequence bound by the constant. \\\\" + }.mkString("\n") + + s""" + |Let \\textbf{$constantName} be a constant with Arguments: \\textit{${notationArgs.mkString(", ")}} \n + |such that: $$\\MMT$constantName${notationArgs.map(c => s"{$c}").mkString}$$. \n + |$argsElaborated + |""".stripMargin + } + } + private def doDocument(document: Document, standalone: Boolean)(implicit rh: RenderingHandler): Unit = { if (standalone) { - rh << s"% generated by MMT from document ${document.path}\n" - rh << s"\\documentclass{article}\n" - rh << s"\\usepackage{stex}\n" - // Testing this package for use with special math symbols - rh << s"\\libinput{preamble}\n" - rh << "\\begin{document}\n" + rh << "\\documentclass[12pt]{article}" + "\n" + rh << "\\usepackage{stex}" + "\n" + rh << "\\libinput{mmt-stex}" + "\n" + rh << "\\begin{document}" + "\n" + rh << "\n" } document.getDeclarations foreach { - // Sections? - case nestedDocument: Document => doDocument(nestedDocument, standalone = false) - // Handle namespaces? + case nestedDocument: Document => + if (nestedDocument.level == SectionLevel || nestedDocument.level == SectionInModuleLevel){ + doSection(nestedDocument) + } + doDocument(nestedDocument, standalone = false) + case dRef: DRef => controller.globalLookup.get(dRef.target) match { + case document: Document => + doDocument(document, standalone = false) + case _ => + } case mRef: MRef => controller.globalLookup.get(mRef.target) match { case theory: Theory => - val importString = buildIncludeString(mRef.target, standalone = false) - rh << importString - rh << s"Theory: ${theory.name}\n" + rh << doInclude(mRef.target, standalone = false) + "\n" + rh << s"\\begin{theorysection}{${theory.name}}" + "\n" doDocument(theory.asDocument, standalone = false) + rh << "\\end{theorysection}" + "\n" case view: View => doDocument(view.asDocument, standalone = false) + case _ => } case sRef: SRef => controller.globalLookup.get(sRef.target) match { case declaration: Declaration => doDeclaration(declaration, standalone = false) case _ => - } - case opaqueText: OpaqueText => doOpaque(opaqueText) + } + case opaqueText: OpaqueText => doOpaque(opaqueText.text) case _ => } if (standalone) { - rh << "\\end{document}\n" + rh << s"\\MMTsTeXfootnote{${document.path.toString.replace("_", "\\_").replace(".omdoc", ".mmt")}}" + "\n" + rh << "\n" + rh << "\\end{document}" + "\n" } } - private def doOpaque(opaqueText: OpaqueText)(implicit rh: RenderingHandler): Unit = { - // All lines except the first are indented, needs clear formatting - opaqueText.text match { - case stringFragment: StringFragment => { - rh << s"${stringFragment.value}\n" - } - // case ObjFragment(o) => doObj(o) - case objectFragment: ObjFragment => { - rh << s"${objectFragment.toString}\n" - } - // case ScopeFragment(body) => body.map(doOpaque).mkString() - case scopeFragment: ScopeFragment => { - rh << s"${scopeFragment.toString}\n" + private def doSection(section: Document)(implicit rh: RenderingHandler): Unit = { + val sectionLabel = section.name.toString + val sectionTitle = NarrativeMetadata.title.get(section).getOrElse(sectionLabel) + rh << s"\\section*{$sectionTitle} \\label{$sectionLabel}" + "\n" + } + + private def doOpaque(textFragment: TextFragment)(implicit rh: RenderingHandler): Unit = { + textFragment match { + case stringFragment: StringFragment => doStringFragment(stringFragment, doNotEscape = false, newlineAfter = true) + case objFragment: ObjFragment => doObjFragment(objFragment) + case scopeFragment: ScopeFragment => doScopeFragment(scopeFragment) + } + } + + private def doStringFragment(stringFragment: StringFragment, doNotEscape: Boolean, newlineAfter: Boolean)(implicit rh: RenderingHandler): Unit = { + val fragmentValue = if (doNotEscape) { + stringFragment.value + } else { + stringFragment.value.replace("_", "\\_") + } + val resultString = Common.translateOpaqueStringFragment(fragmentValue) + if (newlineAfter) rh << resultString + "\n" else rh << resultString + } + + private def doObjFragment(objFragment: ObjFragment)(implicit rh: RenderingHandler): Unit = { + val objAnalyzed = objFragment.tc.getAnalyzedIfFullyChecked.get + objAnalyzed match { + case term: Term => + apply(term, None) + case _ => + } + } + + private def doScopeFragment(scopeFragment: ScopeFragment)(implicit rh: RenderingHandler): Unit = { + val doNotEscape = scopeFragment.body.head match { + case StringFragment(value) => value.startsWith("\\begin{lstlisting}") + case _ => false + } + + scopeFragment.body.foreach { + case stringFragment: StringFragment => doStringFragment(stringFragment, doNotEscape, newlineAfter = false) + case objFragment: ObjFragment => doObjFragment(objFragment) + case scopeFragment: ScopeFragment => doScopeFragment(scopeFragment) + } + + rh << "\n" + } +} + +/** + * convert a term into expressions processable by sTeX + * + * Used for [[ModuleGeneratingPresenter]] + */ +class SymbolUsingPresenter extends ObjectPresenter { + def apply(o: Obj, origin: Option[CPath])(implicit rh : RenderingHandler): Unit = { + val con = origin match { + case Some(CPath(p: ContentPath,_)) => Context(p.module) + case _ => Context.empty + } + rh << "$" + doObj(o)(con) + "$" + } + + private def removeImplicit(arity: Arity, termArgs: List[Term]): (List[ArgumentComponent], List[Term]) = { + val implArgs = arity.flatImplicitArguments(arity.length) + if (implArgs.isEmpty) { + return (arity.arguments, termArgs) + } + val indexedArgs = arity.arguments.zipWithIndex + val argsToKeep = indexedArgs.collect { + case (arg, index) if !implArgs.contains(arg) => index + } + val arityArgsWithoutImpl = argsToKeep.map(arity.arguments) + val termArgsWithoutImpl = argsToKeep.map(termArgs) + (arityArgsWithoutImpl, termArgsWithoutImpl) + } + + /** translates an MMT name into a sTeX symbol name + * some subtleties of complex steps are still ignored, but the resulting names should be unique in most cases + */ + private def doObj(obj: Obj)(implicit context: Context): String = { + val objS = obj match { + case OMS(p) => doSymbolName(p) + case OMV(n) => n.toPath + case t @ ComplexTerm(_, _, _, _) => + val tS = controller.pragmatic.makePragmatic(t)(p => Presenter.getNotations(controller, p, true)) match { + case None => + val ComplexTerm(p, subs, con, args) = t + Presenter.getNotations(controller, p, true).headOption match { + case Some(not) => + doComplexWithNotation(t, p, subs, con, args, not) + case None => + doComplexDefault(p, subs, con, args) + } + case Some(tP) => + val PragmaticTerm(p, subs, con, args, not, _) = tP + doComplexWithNotation(t, p, subs, con, args, not) + } + tS + case l: OMLITTrait => + l.toString + case o: OML => + doObj(o.vd) + case VarDecl(n, _, tp, df, _) => + val nL = n.toPath + val (tpLatex,tpInfText) = tp match { + case None => ("","") + case Some(t) => + val tL = doObj(t) + val inferred = parser.SourceRef.get(t).isEmpty + val tT = if (inferred) controller.presenter.asString(t) else "" + (tL,tT) + } + val dfL = df match { + case None => "" + case Some(t) => doObj(t) + } + // if the type was inferred, we add its text rendering as an optional argument (e.g., to display as a tooltip) + nL + case s: Sub => + doObj(VarDecl(s.name, df = s.target)) + case t => + logError("unexportable: " + t) + "\\MMTHelpererror{unknown object}" + } + objS + } + + private def doComplexWithNotation(strict: Term, p: GlobalName, subs: Substitution, con: Context, args: List[Term], not: TextNotation) + (implicit context: Context): String = { + val arity = not.arity + val (arityArgsWithoutImpl, termArgsWithoutImpl) = removeImplicit(arity, args) + val arityCopyWithoutImpl = Arity(not.arity.subargs, not.arity.variables, arityArgsWithoutImpl) + val subsG = arityCopyWithoutImpl.groupArgs(subs.map(_.target), true) + val conG = arityCopyWithoutImpl.groupVars(con) + val argsG = arityCopyWithoutImpl.groupArgs(termArgsWithoutImpl, false) + var res = doSymbolName(p) + def append(l: Seq[String]): Unit = { + res += l.mkString("{",",","}") + } + subsG.foreach {a => + val aS = a map doObj + append(aS) + } + var extCon = context + conG.foreach {c => + val cS = c.variables map {vd => + val r = doObj(vd)(extCon) + extCon ++= vd + r } + append(cS) + } + argsG.foreach {a => + val aS = a map {x => + doObj(x)(extCon)} + append(aS) } + res + } + private def doComplexDefault(p: GlobalName, subs: Substitution, con: Context, args: List[Term])(implicit context: Context): String = { + val name = doSymbolName(p) + val subsS = (subs map doObj).mkString(",") + val conS = (con mapVarDecls {case (vdCon,vd) => doObj(vd)(context++vdCon)}).mkString(",") + val argsCon = context ++ con + val argsS = (args map {a => doObj(a)(argsCon)}).mkString(",") + s"\\MMTHelpercomplex{$name}{$subsS}{$conS}{$argsS}" } } diff --git a/src/mmt-api/resources/unicode/latex-mathclass-map b/src/mmt-api/resources/unicode/latex-mathclass-map new file mode 100644 index 000000000..0d2ad00cc --- /dev/null +++ b/src/mmt-api/resources/unicode/latex-mathclass-map @@ -0,0 +1,117 @@ +// Binary operator ++|\mathbin +-|\mathbin +*|\mathbin +/|\mathbin +\cdot|\mathbin +\times|\mathbin +\div|\mathbin +\cup|\mathbin +\cap|\mathbin +\setminus|\mathbin +\uplus|\mathbin +\vee|\mathbin +\wedge|\mathbin +\oplus|\mathbin +\otimes|\mathbin +\odot|\mathbin +\circ|\mathbin +\ast|\mathbin +\star|\mathbin +\bullet|\mathbin +\diamond|\mathbin +\boxplus|\mathbin +\boxtimes|\mathbin +\bigcirc|\mathbin +// Binary relation +=|\mathrel +:=|\mathrel +<|\mathrel +>|\mathrel +\leq|\mathrel +\geq|\mathrel +\neq|\mathrel +\sim|\mathrel +\simeq|\mathrel +\approx|\mathrel +\cong|\mathrel +\equiv|\mathrel +\propto|\mathrel +\subset|\mathrel +\supset|\mathrel +\subseteq|\mathrel +\supseteq|\mathrel +\in|\mathrel +\notin|\mathrel +\parallel|\mathrel +\perp|\mathrel +\doteq|\mathrel +\models|\mathrel +\mid|\mathrel +\rightarrow|\mathrel +\Rightarrow|\mathrel +\longrightarrow|\mathrel +\leftarrow|\mathrel +\Leftarrow|\mathrel +\longleftarrow|\mathrel +\leftrightarrow|\mathrel +\longleftrightarrow|\mathrel +\lolli|\mathrel +\gg|\mathrel +\ll|\mathrel +// Punctuation +.|\mathpunct +,|\mathpunct +;|\mathpunct +:|\mathpunct +\ldotp|\mathpunct +\cdotp|\mathpunct +\colon|\mathpunct +// Large operator +\sum|\mathop +\prod|\mathop +\int|\mathop +\iint|\mathop +\iiint|\mathop +\lim|\mathop +\sup|\mathop +\inf|\mathop +\max|\mathop +\min|\mathop +\bigcup|\mathop +\bigcap|\mathop +\bigwedge|\mathop +\bigvee|\mathop +\coprod|\mathop +\bigsqcup|\mathop +\bigotimes|\mathop +\bigoplus|\mathop +\bigodot|\mathop +\oint|\mathop +\vdash|\mathop +\neg|\mathop +\forall|\mathop +\exists|\mathop +\lambda|\mathop +// Opening +(|\mathopen +[|\mathopen +\{|\mathopen +\langle|\mathopen +\lfloor|\mathopen +\lceil|\mathopen +\ulcorner|\mathopen +\llcorner|\mathopen +\lbracket|mathopen +\lparen|\mathopen +// Closing +)|\mathclose +]|\mathclose +\}|\mathclose +\rangle|\mathclose +\rfloor|\mathclose +\rceil|\mathclose +\urcorner|\mathclose +\lrcorner|\mathclose +\rbracket|\mathclose +\rparen|\mathclose diff --git a/src/mmt-api/resources/unicode/unicode-latex-map b/src/mmt-api/resources/unicode/unicode-latex-map index 34011cb67..a7b619bbe 100644 --- a/src/mmt-api/resources/unicode/unicode-latex-map +++ b/src/mmt-api/resources/unicode/unicode-latex-map @@ -1,23 +1,10 @@ -jMD|❚ -jDD|❙ -jOD|❘ +// To stay consistant and avoid conversion errors, the symbols which are not available in basic latex are restricted to the amssymb and amsmath packages +jvert|❚ +jvert|❙ +jvert|❘ jsharp|♯ jflat|♭ jnatural|♮ -jra|→ -jla|← -jlra|↔ -jrA|⇒ -jlA|⇐ -jlrA|⇔ -jraa|⟶ -jlaa|⟵ -jlraa|⟷ -jrAA|⟹ -jlAA|⟸ -jlrAA|⟺ -jhra|↪ -jhla|↩ jrightarrow|→ jleftarrow|← jleftrightarrow|↔ @@ -32,50 +19,41 @@ jlongleftrightarrow|⟷ jLongrightarrow|⟹ jLongleftarrow|⟸ jLongleftrightarrow|⟺ -jbla|↦ -jblA|⤇ -jblaa|⟼ -jblAA|⤇ -jbra|↤ -jbrA|⤆ -jbraa|⟻ -jbrAA|⤆ -jls|⇝ -jlss|⟿ -jrs|⇜ -jrss|⬳ -jmapsto|↦ -jMapsto|⤇ +jrightarrowtail|↦ +jrightarrowtail|↣ +jLongrightarrow|⤇ +jlongmapsto|⟼ +jleftarrowtail|↤ +jleftarrowtail|↢ +jleftarrowtail|⟻ +jrightsquigarrow|⟿ +jleftsquigarrow|⇜ +jleftsquigarrow|⬳ jlongmapsto|⟼ -jLongmapsto|⤇ -jmapsfrom|↤ -jMapsfrom|⤆ -jlongmapsfrom|⟻ -jLongmapsfrom|⤆ jrightsquigarrow|⇝ -jlongrightsquigarrow|⟿ +jrightsquigarrow|⟿ jleftsquigarrow|⇜ -jlongleftsquigarrow|⬳ -jlolli|⊸ -jrewrites|⟿ +jleftsquigarrow|⬳ +jmultimap|⊸ +jleftsquigarrow|⟿ juparrow|↑ jdownarrow|↓ jupdownarrow|↕ jUparrow|⇑ jDownarrow|⇓ jUpdownarrow|⇕ -jupfish|⥾ -jdownfish|⥿ -jleftfish|⥼ -jrightfish|⥽ -jhollowup|⇧ -jhollowdown|⇩ -jhollowleft|⇦ -jhollowright|⇨ -jcontra|↯ -jcheck|✓ +jupharpoonright|⥾ +jdownharpoonleft|⥿ +jleftharpoondown|⥼ +jrightharpoonup|⥽ +jUparrow|⇧ +jDownarrow|⇩ +jLeftarrow|⇦ +jRightarrow|⇨ +jbot|↯ +jcheckmark|✓ jast|∗ -jstar|★ +jbigstar|★ jcdot|⋅ jcirc|∘ jbullet|∙ @@ -83,11 +61,11 @@ jtimes|× jbigtimes|⨯ jpm|± jmp|∓ -jdivide|÷ -jdiv|∕ -jbackdiv|⧵ -jbigdiv|⧸ -jbigbackdiv|⧹ +jdiv|÷ +jslash|∕ +jbackslash|⧵ +jslash|⧸ +jbackslash|⧹ jwedge|∧ jvee|∨ jcap|∩ @@ -98,21 +76,21 @@ joplus|⊕ jominus|⊖ jotimes|⊗ joslash|⊘ -jodiv|⨸ -joast|⊛ -jocirc|⊚ +jdiv|⨸ +jcircledast|⊛ +jcircledcirc|⊚ jodot|⊙ -joequal|⊜ -jo0|⓪ -jo1|① -jo2|② -jo3|③ -jo4|④ -jo5|⑤ -jo6|⑥ -jo7|⑦ -jo8|⑧ -jo9|⑨ +jeqcirc|⊜ +0|⓪ +1|① +2|② +3|③ +4|④ +5|⑤ +6|⑥ +7|⑦ +8|⑧ +9|⑨ juplus|⊎ judot|⊍ jcapdot|⩀ @@ -130,11 +108,11 @@ jbigoplus|⨁ jbigotimes|⨂ jbiguplus|⨄ jbiguminus|⩁ -jbigudot|⨃ +jbigcupdot|⨃ jbigubar|⩂ jsubset|⊂ jsupset|⊃ -jsq|⊆ +jsubseteq|⊆ jsubseteq|⊆ jsupseteq|⊇ jnsubset|⊄ @@ -208,10 +186,10 @@ jtriangleright|▷ jtriangleleft|◁ jblacktriangleright|▶ jblacktriangleleft|◀ -jsmblksquare|▪ -jsmwhtsquare|▫ -jder|⊦ -jrightassert|⊦ +jblacksquare|▪ +jsquare|▫ +jvdash|⊦ +jvdash|⊦ jvdash|⊢ jdashv|⊣ jVdash|⊩ @@ -271,8 +249,8 @@ jcolon|∶ jzcolon|⦂ jcoloneq|≔ jeqcolon|≕ -jlparen|( -jrparen|) +(|( +)|) jllparen|⸨ jrrparen|⸩ jlwparen|⦅ @@ -289,8 +267,8 @@ jrbangle|⦉ jlbangle|⦊ jlhangle|❮ jrhangle|❯ -jlbracket|[ -jrbracket|] +jlbrack|[ +jrbrack|] jllbracket|⟦ jrrbracket|⟧ jlmbracket|⁅ @@ -359,7 +337,8 @@ jepsilon|ϵ jvarepsilon|ε jzeta|ζ jeta|η -jtheta|ϑ +jtheta|θ +jvartheta|ϑ jiota|ι jkappa|κ jlambda|λ @@ -370,6 +349,7 @@ jomikron|ο jpi|π jrho|ρ jsigma|σ +jvarsigma|ς jtau|τ jupsilon|υ jphi|ϕ diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/archives/BuildTarget.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/archives/BuildTarget.scala index addbff970..08f642d6b 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/archives/BuildTarget.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/archives/BuildTarget.scala @@ -297,11 +297,7 @@ abstract class TraversingBuildTarget extends BuildTarget { children: Option[List[BuildTask]],eCOpt: Option[ErrorHandler]): BuildTask = { val ew = makeHandler(a,inPath,children.isDefined) val errorCont = MultipleErrorHandler(new ErrorContainer :: ew :: eCOpt.toList, report) - - // Change outFile to path without $ - val segmentsForInPathForStex = inPath.map(segment => segment.replace("$", "")) - val inPathForStex = new FilePath(segmentsForInPathForStex) - val outFile = if (children.isDefined) getFolderOutFile(a,inPathForStex) else getOutFile(a,inPathForStex) + val outFile = if (children.isDefined) getFolderOutFile(a,inPath) else getOutFile(a,inPath) new BuildTask(key,a,inFile,children,inPath,outFile,errorCont) }