/
CompilingLatexPresenter.scala
336 lines (315 loc) · 12.4 KB
/
CompilingLatexPresenter.scala
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
package info.kwarc.mmt.latex
import info.kwarc.mmt.api._
import utils._
import frontend._
import symbols._
import modules._
import documents._
import objects._
import presentation._
import notations._
import parser._
/** helper functions for latex presenter */
object Common {
def doConstantName(p: GlobalName) = {
val mod = doLocalName(p.module.name)
val name = doLocalName(p.name)
"\\" + mod + "@@" + name
}
private def doLocalName(l: LocalName): String = l.steps.map {
case SimpleStep(n) => Common.translateName(n)
case ComplexStep(p) => doLocalName(p.name)
}.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("")
/** translates a unicode-containing string into the latex equivalent */
def translateDelim(s: String) = translate(s, c => utils.listmap(delimEscapes,c) orElse macroUnicodeMap(c))
/** 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))
/** 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))
/** 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
*/
private val rawUnicodeMap = new scala.collection.mutable.HashMap[Char,String]()
private def macroUnicodeMap(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 {
def apply(s: String, i: Int, firstPosition: SourcePosition): Option[Token] = {
if (s(i) != '\\') return None
var j = i+1
val l = s.length
while (j < l && s(j).isLetter) {j+=1}
val commandName = s.substring(i+1,j)
val command = "\\" + commandName
val wsBefore = i == 0 || TokenList.isWhitespace(s(i-1))
val t = inverseUnicodeMap.get(commandName) match {
case Some(unicode) =>
Token(unicode, firstPosition, wsBefore, Some(command))
case None =>
Token(command, firstPosition, wsBefore)
}
Some(t)
}
def trigger = Some("\\")
}
private def init: Unit = {
val basicmap = UnicodeMap.readMap("unicode/unicode-latex-map")
fillMap(basicmap)
}
init
private def fillMap(map: List[(String,String)]): Unit = {
map.foreach {case (c,r) =>
// command starts with j
val command = c.substring(1)
if (r.length == 1) {
val char = r(0)
rawUnicodeMap(char) = command
inverseUnicodeMap(command) = r
} else {
// better to ignore this because they can be useful in other contexts
// throw GeneralError(s"expected single character in symbol map: $c|$r")
}
}
}
}
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.
*/
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)
case d: Declaration => doDeclaration(d)
case _ =>
}
}
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))
}
dt.getDeclarationsElaborated.foreach {
case d => doDeclaration(d)
}
}
private def doDeclaration(d: Declaration)(implicit rh : RenderingHandler): Unit = {
d match {
case c: Constant => doConstant(c)
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 arch = controller.backend.findOwningArchive(id.from).getOrElse {
logError("cannot find archive holding " + id.from + " (ignoring)")
return
}
val pLAbs = arch / outDim / "content" / archives.Archive.MMTPathToContentPath(id.from.mainModule).stripExtension
val pLRel = arch.root.up.up.relativize(pLAbs)
val pL = pLRel.segments.mkString("/")
rh << "\\RequireMMTPackage{" + pL + "}\n"
case _ =>
}
}
private def doConstant(c: Constant)(implicit rh : RenderingHandler): Unit = {
val not = c.notC.getPresentDefault
var numArgs = not match {
case None => 0
case Some(tn) =>
tn.arity.length
}
val notBody = not match {
case None => Common.translateDelim(c.name.toString)
case Some(tn) =>
// if an InferenceMarker occurs, the generated macro expects an additional argument for the inferred type
val dm = new DoMarkers(c.path, numArgs+1)
val tnS = dm.doMarkers(tn.presentationMarkers)
if (dm.infMarkerUsed)
numArgs += 1
tnS
}
val numArgsS = if (numArgs == 0) "" else "[" + numArgs.toString + "]"
rh << s"\\newcommand{${doConstantName(c.path)}}$numArgsS{$notBody}\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"\\mmt@implicit{#${a.number.abs}}"
case s: SeqArg => "\\mmt@fold{" + doDelim(s.sep) + "}{" + "#" + s.number.abs + "}"
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)
s"\\mmt@symref{${p.toPath}}{$dL}"
}
}
/*
private def requirePackage(p: MPath, bf: BuildTask): String = {
controller.backend.findOwningArchive(p) match {
case None => "% skipping import of unknown module " + p.toPath
case Some(a) =>
val conP = Archive.MMTPathToContentPath(p)
val sty = (a / outDim / conP).stripExtension
val relSty = utils.FileURI(bf.outFile).relativize(utils.FileURI(sty)).pathAsString
s"\\RequirePackage{\\currfiledir $relSty}"
}
}
*/
}
/**
* convert a term into a LaTeX expression (using lots of \ { and })
*
* the LaTeX is relative to the macros generated by [[MacroGeneratingPresenter]]
*/
class MacroUsingPresenter 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)
}
/** translates an MMT name into a LaTeX 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) => doConstantName(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)
}
"\\mmt@group{" + tS + "}"
case l: OMLITTrait =>
"\\mmt@lit{" + 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)
s"{\\mmt@vardecl[$tpInfText]{$nL}{$tpLatex}{$dfL}}"
case s: Sub =>
doObj(VarDecl(s.name, df = s.target))
case t =>
logError("unexportable: " + t)
"\\mmt@error{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 subsG = arity.groupArgs(subs.map(_.target), true)
val conG = arity.groupVars(con)
val argsG = arity.groupArgs(args, false)
var res = doConstantName(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)
}
// add the inferred type as a final argument
if (not.markers exists {m => m.atomicDescendants contains InferenceMarker}) {
val strictI = checking.Solver.infer(controller, context, strict, None) match {
case Some(tp) =>
doObj(tp)
case None =>
"\\mmt@error{type inference failed}"
}
res += "{" + strictI + "}"
}
res
}
private def doComplexDefault(p: GlobalName, subs: Substitution, con: Context, args: List[Term])(implicit context: Context): String = {
val name = doConstantName(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"\\mmt@complex{$name}{$subsS}{$conS}{$argsS}"
}
}