Skip to content
GitLab
Commit 9a44e756 authored by Dennis Müller's avatar Dennis Müller
Browse files

update

parent 095abbdd
Expand all Hide whitespace changes
Inline Side-by-side
build.sbt
View file @ 9a44e756
......@@ -10,7 +10,7 @@ resolvers += "Sonatype Releases" at "https://oss.sonatype.org/content/repositori
lazy val core = project.settings(
name := "Core"
).dependsOn(mmt,latex,stex,ml)
).dependsOn(mmt,latex,stex)
/*
lazy val mmtutil = project.settings(
name := "mmtutil",
......@@ -30,7 +30,7 @@ lazy val stex = project.settings(
name := "sTeX",
libraryDependencies ++= Seq(dependencies.os)
).dependsOn(latex)
/*
lazy val ml = project.settings(
name := "ML",
libraryDependencies ++= Seq(
......@@ -38,20 +38,22 @@ lazy val ml = project.settings(
)
).dependsOn(mmt) // TODO replace by mmt for final
*/
lazy val mmt = project.settings(
name := "MMT",
Compile / unmanagedJars ++= Seq(baseDirectory.value / "lib" / "mmt.jar")
)
lazy val dependencies = new {
val scalaxml = "org.scala-lang.modules" %% "scala-xml" % "1.2.0"
val scalacompiler = "org.scala-lang" % "scala-compiler" % "2.12.8"
val scalaparser = "org.scala-lang.modules" %% "scala-parser-combinators" % "1.1.2"
val tensorflow = "org.platanios" %% "tensorflow" % "0.4.1"
val tensorflow_cpu = tensorflow classifier "linux-cpu-x86_64"
val tensorflow_gpu = tensorflow classifier "linux-gpu-x86_64"
val xz = "org.tukaani" % "xz" % "1.8"
// val scalaxml = "org.scala-lang.modules" %% "scala-xml" % "1.2.0"
// val scalacompiler = "org.scala-lang" % "scala-compiler" % "2.12.8"
// val scalaparser = "org.scala-lang.modules" %% "scala-parser-combinators" % "1.1.2"
// val tensorflow = "org.platanios" %% "tensorflow" % "0.4.1"
// val tensorflow_cpu = tensorflow classifier "linux-cpu-x86_64"
// val tensorflow_gpu = tensorflow classifier "linux-gpu-x86_64"
// val xz = "org.tukaani" % "xz" % "1.8"
//val akka = "com.typesafe.akka" %% "akka-actor" % "2.6.4"
val os = "com.lihaoyi" %% "os-lib" % "0.2.7"
}
\ No newline at end of file
core/src/test/scala/Test.scala
View file @ 9a44e756
package com.jazzpirate
// import breeze.linalg.DenseVector
import com.jazzpirate.glove.TFGloVe
//import com.jazzpirate.glove.TFGloVe
import com.jazzpirate.latex.bindings.Commands
import com.jazzpirate.latex.{Expand, FileParser, LaTeXParser, LaTeXProcessor, Normalize, ParseError, Remove, StringParser}
import com.jazzpirate.latex.commands.{CommandObject, Environment, EnvironmentObject}
......@@ -10,12 +10,12 @@ import com.jazzpirate.ml.Labeller
import com.jazzpirate.mmt.{Generator, MitM, MyMMT, Textbook}
import com.jazzpirate.stex.bindings.StexCommands
import com.jazzpirate.stex.{CheckSTeX, DesTeXify, Notations, STeX, StexChecker, SymdefMacro, Symdefs, Tokenizer, Verbalizer, bindings}
import com.jazzpirate.tensorflow.Matrix
//import com.jazzpirate.tensorflow.Matrix
import info.kwarc.mmt.api.objects.{Context, Obj, VarDecl}
import info.kwarc.mmt.api.utils.{JSONArray, JSONInt, JSONObject, JSONString}
import info.kwarc.mmt.api.utils.time.Time
import org.platanios.tensorflow.api.core.Shape
import org.platanios.tensorflow.api.tensors.Tensor
//import org.platanios.tensorflow.api.core.Shape
//import org.platanios.tensorflow.api.tensors.Tensor
import scala.collection.mutable
......@@ -985,7 +985,7 @@ object Test {
println("\nDONE ----------------------------------------------------------\n")
}
/*
def tensortest: Unit = {
import com.jazzpirate.tensorflow._
// println(TensorFlow.currentCallbackRegistryPointer)
......@@ -1005,6 +1005,8 @@ object Test {
println(v1.asTensor.tensorDot(v2.asTensor,1).summarize())
}
*/
def parsesymdefs = { /*
val macros = StexChecker.collect(mmt.archivepath / "smglom",true)
......
deploy/ML.jar LFS
View file @ 9a44e756
No preview for this file type
deploy/example.sh
View file @ 9a44e756
java -jar ML.jar -tex example.tex -mathhub mathhub -eval_latex -alignments mathhub/Alignments -typecheck
java -jar ML.jar -tex example.tex -mathhub mathhub -eval_latex -alignments mathhub/Alignments -stex stex.tex -typecheck
deploy/stex.tex 0 → 100644
View file @ 9a44e756
$x$
$A$
$\inset xA$
\[\foral{A,B}{\biimpl{\eq{A,B}}{\foral x{\biimpl{\inset xA}{\inset xB}}}}\]
$P$
$\setst x{\nappa Px}$
$P$
\[\foral y{\biimpl{\inset y{\setst x{\nappa Px}}}{\nappa Py}}\]
$\setdots{a,b,c}$
$\setst x{\disj[or]{\eq{x,a},\eq{x,b},\eq{x,c},\ldots}}$
\[\eq{\NaturalNumbers,\setdots{0,1,2,3}}\]
\[\eq{\IntegerNumbers,\dotssetdots{-2,-1,0,1,2}}\]
\[\eq{\RationalNumbers,\setst{\fraction ab}{\conj[and]{\inset a\IntegerNumbers,\inset b\NaturalNumbers, \natmorethan b0}}}\]
$A$
$B$
$\sseteq AB$
$A$
$B$
\[\biimpl{\sseteq AB}{\foral{\inset xA}{\inset xB}}\]
$B$
$A$
$\superseteq BA$
$\notequal AB$
$A$
$B$
$B$
$A$
$A$
$\defeq{\powerset{A}}{\setst{x}{\sseteq xA}}$
$A$
$B$
\[\defeq{\union{A,B}}{\setst{x}{\disj[or]{\inset xA, \inset xB}}}\]
$A$
$B$
\[\defeq{\intersect{A,B}}{\setst{x}{\conj[and]{\inset xA, \inset xB}}}\]
$A$
$B$
\[\defeq{\setdiff AB}{\setst{\inset xA}{\ninset xB}}\]
$A$
$B$
\[\defeq{\cart{A,B}}{\setst{\tup{x,y}}{\conj[and]{\inset xA, \inset xB}}}\]
$A$
$A$
\[\inset{\card[bars]{A}}{\NaturalNumbers}\]
$X$
$Y$
\[\eq{\card[bars]{\cart{X,Y}},\nattimes{\card[bars]{X},\card[bars]{Y}}}\]
\[\eq{\card[bars]{\union{X,Y}},\natplus{\card[bars]{X},\natminus{\card[bars]{Y},\card[bars]{\intersect{X,Y}}}}}\]
$\foral[forall]{\natmethan n1}{\eq{\natplus{1,2,\ldots,n},\natdiv[frac]{\nattimes[invisible]{n,\natplus{n,1}}}2}}$
$\eq{n,5}$
$\eq{\natplus{1,2,3,4,5},\natdiv[slash]{\nattimes[cdot]{5,6}}2}$
$\nappa An$
$n$
$\nappa A1$
$\eq{1,\natdiv[frac]{\nattimes{1,\natplus{1,1}}}2}$
$\imply[verben]{\nappa An}{\nappa A{\natplus{n,1}}}$
$\eq{\natplus{1,2,\ldots,n},\natdiv[frac]{\nattimes[invisible]{n,\natplus{n,1}}}2}$
\[\eq{\natplus{1,2,\ldots,n,\natplus{n,1}},\natplus{\natdiv[frac]{\nattimes{n,\natplus{n,1}}}2,\natdiv[frac]{\nattimes{2,\natplus{n,1}}}2},\natdiv[frac]{\nattimes{\natplus{n,2},\natplus{n,1}}}2}\]
\[\eqFN\natdiv[frac]{\nattimes{\natplus{n,1},\natplus{n,1,1}}}2\]
$\nappa An$
$n$
$\natplus{n,1}$
\[\eq{\natplus{1,2,\ldots,n},\natplus{\natplus{1,n},\natplus{2,\natminus{n,1}},\ldots}}\]
$\eq{\natplus{1,2,\ldots,n},\natdiv[frac]{\nattimes[invisible]{n,\natplus{n,1}}}2}$
$\natdiv[slash] n2$
$\natplus{n,1}$
$n$
$\livar a1$
$\ldots$
$\livar an$
\[\defeq{\Sumfromto{i}1n{\livar ai}}{\natplus{\livar{a}{1},\livar{a}{2},\ldots,\livar{a}{n}}}\]
\[\foral[forall]{\natmethan n1}{\eq{\Sumfromto i1ni,\natdiv[frac]{\nattimes[invisible]{n,\natplus{n,1}}}2}}\]
$\livar a1$
$\ldots$
$\livar an$
\[\defeq{\Prodfromto{i}1n{\livar ai}}{\nattimes[cdot]{\livar{a}{1},\livar{a}{2},\ldots,\livar{a}{n}}}\]
$\Sumfromto i1ni$
$\factorial n$
$n$
\[\defeq{\factorial n}{\Prodfromto{i}1ni}\]
$\inset n\NaturalNumbers$
$\natlessthan kn$
$\livar ai$
$\eq{\Sumfromto i1n{\livar ai},\natplus{\Sumfromto i1k{\livar ai},\Sumfromto i{\natplus{k,1}}n{\livar ai}}}$
$\eq{k,n}$
$0$
$\eq{\Prodfromto i1n{\livar ai},\nattimes[cdot]{\Prodfromto i1n{\livar ai},\Prodfromto i{\natplus{n,1}}n{\livar ai}}}$
$1$
\[\defeq{\Sumfromto ikn{\livar ai}}0\]
$i$
\[\defeq{\Prodfromto ikn{\livar ai}}1\]
$i$
$\eq{\factorial0,1}$
$n$
$\factorial n$
$\eq{\factorial 3,6}$
$n$
$\natminus{n,1}$
$\factorial n$
$n$
$\natlessthan kn$
$\natdiv[frac]{\factorial n}{\factorial{(\natminus{n,k})}}$
$k$
$\natdiv[frac]{\factorial n}{\nattimes[cdot]{\factorial k,\factorial{\natminus{n,k}}}}$
$k$
$\eq{\natdiv[frac]{\factorial 4}{\factorial{(\natminus{4,2})}},12}$
$\eq{\natdiv[frac]{\factorial 4}{\nattimes[cdot]{\factorial 2,\factorial{\natminus{4,2}}}},6}$
$\factorial n$
$n$
$k$
$n$
$n$
$\natminus{n,k}$
$\natminus{n,k}$
$\natdiv[frac]{\factorial n}{\factorial{(\natminus{n,k})}}$
$k$
$\factorial k$
$\natdiv[frac]{\factorial n}{\nattimes{\factorial k,\factorial{\natminus{n,k}}}}$
$\natlessthan kn$
$\binomcoeff nk$
\[ \defeq{\binomcoeff nk}{\natdiv[frac]{\factorial n}{\nattimes{\factorial k,\factorial{\natminus{n,k}}}}} \]
\[\eq{\binomcoeff nk,\natdiv[frac]{\factorial n}{\nattimes{\factorial k}{\factorial{(\natminus{n,k})}}},\Prodfromto j0{\natminus{k,1}}{\natdiv[frac]{\natminus{n,j}}{\natminus{k,j}}},\binomcoeff n{\natminus{n,k}}}\]
\[\eq{\natplus{\binomcoeff n{\natminus{k,1}},\binomcoeff nk},\binomcoeff{\natplus{n,1}}k}\]
$n$
$m$
\[ \defeq{\natpower nm}{\Prodfromto i1mn} \]
$\eq{\natpower n0,1}$
$n$
$\foralS{n}{\NaturalNumbers}{\foralS{a,b}{\IntegerNumbers}{\eq{{\intpower{\intplus{a,b}}{n}},{\Sumfromto{k}{0}{n}{\inttimes{\binomcoeff nk,\intpower ak,\intpower b{\natminus{n,k}}}}}}}}$
$\eq{n,2}$
\[\eq{\intpower{\intplus{a,b}}2,\Sumfromto k02{\inttimes{\binomcoeff 2k,\intpower ak,\intpower b{\natminus{2,k}}}},\intplus{\intpower a2,\inttimes{2,a,b},\intpower b2}}\]
$\eq{n,0}$
$0$
$n$
\[\eq{\intpower{\intplus{a,b}}n,\Sumfromto k0n{\inttimes{\binomcoeff nk,\intpower ak,\intpower b{\natminus{n,k}}}}}\]
\[\eq{\intpower{\intplus{a,b}}{\natplus{n,1}},\inttimes{\intplus{a,b},\intpower{\intplus{a,b}}n},\inttimes{\intplus{a,b},\Sumfromto k0n{\inttimes{\binomcoeff nk,\intpower ak,\intpower b{\natminus{n,k}}}}}}\]
\[\intplus{\Sumfromto k0n{\inttimes{\binomcoeff nk,\intpower a{\intplus{k,1}},\intpower b{\natminus{n,k}}}},\Sumfromto k0n{\inttimes{\binomcoeff nk,\intpower ak,\intpower b{\natplus{\natminus{n,k},1}}}}}\]
$\eq{i,\natminus{k,1}}$
\[\intplus{\Sumfromto i1{\natplus{n,1}}{\inttimes{\binomcoeff n{\natminus{i,1}},\intpower ai,\intpower b{\natplus{\natminus{n,i},1}}}},\Sumfromto k0n{\inttimes{\binomcoeff nk,\intpower ak,\intpower b{\natplus{\natminus{n,k},1}}}}}\]
$k$
\[\intplus{\inttimes{\intpower a{\natplus{n,1}},\intpower b0},\Sumfromto k1n{\inttimes{\binomcoeff n{\natminus{k,1}},\intpower ak,\intpower b{\natplus{\natminus{n,k},1}}}},\Sumfromto k1n{\inttimes{\binomcoeff nk,\intpower ak,\intpower b{\natplus{\natminus{n,k},1}}}},\inttimes{\intpower a0,\intpower b{\natplus{n,1}}}}\]
\[\intplus{\inttimes{\intpower a{\natplus{n,1}},\intpower b0},\Sumfromto k1n{\inttimes{\binomcoeff {\natplus{n,1}}k,\intpower ak,\intpower b{\natplus{\natminus{n,k},1}}}},\inttimes{\intpower a0,\intpower b{\natplus{n,1}}}}\]
\[\Sumfromto k0{\natplus{n,1}}{\inttimes{\binomcoeff {\natplus{n,1}}k,\intpower ak,\intpower b{\natminus{\natplus{n,1},k}}}}\]
$\magmaset$
$\magmaOp$
$\unitalunit$
$\magmaOp$
$\unitalunit$
\[ \foral{a,b,c}{\eq{\magmaop{\magmaop ab}c,\magmaop a{\magmaop bc}}} \]
\[ \foral{a}{\eq{\magmaop a\unitalunit,\magmaop \unitalunit a,\unitalunit}} \]
$\minset{a,b}\magmaset$
\[\eq{\magmaop ab,\magmaop ba}\]
$\inset g\magmaset$
$\inset h\magmaset$
$g$
$\eq{\magmaop gh,\unitalunit}$
$g$
$\eq{\magmaop hg,\unitalunit}$
$\inset g\magmaset$
$\groupinv g$
\[\eq{\magmaop g{\groupinv g},\magmaop{\groupinv g}g,\unitalunit}\]
\ No newline at end of file
deploy/test.log
View file @ 9a44e756
This diff is collapsed.
stex/src/main/scala/com/jazzpirate/stex/Main.scala
View file @ 9a44e756
......@@ -69,8 +69,7 @@ object Translator {
}
}
def typecheck(mmt : MMT, ltx : LatexObject, macros : List[SymdefMacro], index : Int): (Term, Option[Term], Option[Term]) = {
print("\rTypecheck: Collecting symdefs... ")
private def getTerm(mmt : MMT, ltx: LatexObject, index : Int, is_eval : Boolean) : Term = {
val files = ltx.flatten.collect {
case co : CommandObject if co.command.isInstanceOf[SymdefMacro] =>
val sdm = co.command.asInstanceOf[SymdefMacro]
......@@ -82,9 +81,10 @@ object Translator {
assert(fn.endsWith(".tex"))
"\\gimport[" + a.id + "]{" + fn.dropRight(4) + "}"
}
val header = pre.replace("<root>",mmt.archivepath.toString).replace("<id>","temp" + index) + resolved.mkString("\n") + "\n\n" +
val name = if (is_eval) "temp" + index + "b" else "temp" + index
val header = pre.replace("<root>",mmt.archivepath.toString).replace("<id>",name) + resolved.mkString("\n") + "\n\n" +
Latex.print(ltx) + "\n\n\\end{module}\n\n\\end{document}"
val filename = ("temp" + index + ".tex")
val filename = (name + ".tex")
File.write(mmt.controller.backend.getArchive("stexify/temp").get.root / "source" / filename,header)
print("\rTypecheck: Calling latexml... ")
mmt.hl("build stexify/temp latexml " + filename)
......@@ -95,19 +95,32 @@ object Translator {
print("\rTypecheck: getting term...")
val consts = mmt.controller.getAs(classOf[Theory], path ? ("temp" + index)).getConstants
val consts = mmt.controller.getAs(classOf[Theory], path ? name).getConstants
if (consts.length != 1) {
print("")
}
val term = consts.head.df match {
consts.head.df match {
case Some(tm) => extractTerm(tm)
case _ =>
???
}
}
def typecheck(mmt : MMT, ltx : LatexObject, stx : Option[LatexObject], index : Int): (Term, Option[Term], Option[Term], Option[Term]) = {
print("\rTypecheck: Collecting symdefs... ")
val term = getTerm(mmt, ltx, index, false)
var stex_term = stx.flatMap(lo => Try(getTerm(mmt,lo, index, true)).toOption match {
case r@Some(_) =>
r
case _ =>
println("\rTypecheck: Parsing sTeX failed ")
None
})
term match {
case OMV(_) =>
return (term,Some(term),Some(OMS(Typed.kind)))
return (term,Some(term),Some(OMS(Typed.kind)),stex_term)
case _ =>
}
......@@ -123,13 +136,13 @@ object Translator {
val inferred = result.flatMap{ resI =>
Try {
var paths: List[GlobalName] = Nil
var pathsI: List[GlobalName] = Nil
val trav = new StatelessTraverser {
var inner = false
override def traverse(t: Term)(implicit con: Context, state: State): Term = t match {
case OMS(p) =>
inner = true
paths ::= p
pathsI ::= p
t
case Lambda(_,_,bd) if !inner =>
traverse(bd)
......@@ -139,7 +152,11 @@ object Translator {
}
}
val res = trav(resI, ())
val paths = pathsI
result = Some(res)
Try {
stex_term = stex_term.map(trav(_,()))
}
/*
paths.foreach {p =>
println(p)
......@@ -181,7 +198,7 @@ object Translator {
}.toOption
}.flatten//.toOption }
(term,result,inferred)
(term,result,inferred,stex_term)
}
class Client {
......@@ -269,6 +286,12 @@ object Translator {
println("File " + fs + " doesn't exist")
sys.exit()
}
case "-stex" :: fs :: tail =>
if (File(fs).exists()) parseOption(map ++ Map('stex -> File(File(fs).getAbsoluteFile)), tail)
else {
println("File " + fs + " doesn't exist")
sys.exit()
}
case "-eval_latex" :: tail =>
parseOption(map ++ Map('eval_latex -> true), tail)
case "-typecheck" :: tail =>
......@@ -309,6 +332,13 @@ object Translator {
None
}
var stexs = map.get('stex) match {
case Some(f : File) =>
println("File for stex-comparison provided. Parsing")
File.read(f).split('\n').toList
case _ => Nil
}
// Collect all sTeX-Macros ---------------------------------------------------------------------------------------
......@@ -381,11 +411,20 @@ object Translator {
}
map.get('typecheck) match {
case Some(true) =>
eval_map('parsed) = 0
eval_map('omdoc) = 0
eval_map('translated) = 0
eval_map('inferred) = 0
case _ =>
}
map.get('stex) match {
case Some(_) =>
eval_map('provided_stex) = 0
map.get('typecheck) match {
case Some(true) =>
eval_map('stex_as_omdoc) = 0
case _ =>
}
}
case _ =>
}
......@@ -409,7 +448,7 @@ object Translator {
eval_map('islatex) += 1
if (eval_map.isDefinedAt('stexcheck) && w) eval_map('stexcheck) += 1
(Latex.print(r),w)
}.getOrElse((Console.RED + Console.BOLD + st + Console.RESET,false))
}.getOrElse(("$" + Console.RED + Console.BOLD + st.drop(1).dropRight(1) + Console.RESET + "$",false))
}
assert(p.maths.length == nrets.length)
p.maths.indices.foreach {m =>
......@@ -436,14 +475,40 @@ object Translator {
}.getOrElse{println("Error parsing return!")}
case _ =>
}
var stex : Option[LatexObject] = None
map.get('stex) match {
case Some(_) =>
Try {
var st = stexs.head
stexs = stexs.tail
if (st.startsWith("\\[") || st.startsWith("$$") || st.startsWith("\\("))
st = "$" + st.drop(2).dropRight(2) + "$"
val st_obj = Latex.normalize(proc.expand(proc.parse(st),Normalize.cleanups) :: Nil).head
stex = Some(st_obj)
val st_orig = Latex.print(st_obj)
val ret = Latex.print(Latex.normalize(proc.expand(proc.parse(rets(m)),Normalize.cleanups) :: Nil))
println("Provided sTeX : " + st_orig)
val w = (st_orig == ret)
if (w) eval_map('provided_stex) += 1
println("Matches : " + w)
print("")
}.getOrElse{println("Error parsing sTeX")}
case _ =>
}
map.get('typecheck) match {
case Some(true) =>
Try {
val tm = Latex.normalize(proc.parse(rets(m)) :: Nil).head
val (parsed,transO,inferredO) = typecheck(immt,tm,macros,eval_map('total))
val (parsed,transO,inferredO,stexO) = typecheck(immt,tm,stex,eval_map('total))
print("\r ")
println("\rParsed : " + parsed.toStr(true))
eval_map('parsed) += 1
stexO.foreach {t =>
println("\rParsed orig sTeX : " + t.toStr(true))
val w = parsed.toStr(false) == t.toStr(false)
println("\rMatches : " + w)
if (w) eval_map('stex_as_omdoc) += 1
}
eval_map('omdoc) += 1
transO match {
case Some(trtm) =>
println("Translated : " + trtm.toStr(true))
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment