Skip to content

Commit

Permalink
Popcorn parser works, but is excruciatingly slow!
Browse files Browse the repository at this point in the history
  • Loading branch information
dominique-unruh committed Aug 22, 2016
1 parent 203f082 commit 6e589b2
Show file tree
Hide file tree
Showing 7 changed files with 155 additions and 171 deletions.

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion .idea/modules/proof-editor-build.iml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

8 changes: 4 additions & 4 deletions .idea/modules/proof-editor.iml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion project/Downloads.scala
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ object Downloads extends AutoPlugin {
lazy val installSymcompOpenmath = TaskKey[Unit]("Download Symcomp's openmath.jar")

lazy val enableDownloads = Seq(
installResources := recursiveFiles(installJQuery.value,installMathQuill.value),
installResources := recursiveFiles(/*installJQuery.value,*/installMathQuill.value),

installJars := {
installZ3Linux64.value
Expand Down
2 changes: 1 addition & 1 deletion sbt
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
export JAVA_HOME=/usr/java/jdk1.8.0_92
"$JAVA_HOME/bin/java" -jar /home/unruh/.IdeaIC2016.1/config/plugins/Scala/launcher/sbt-launch.jar "$@"
"$JAVA_HOME/bin/java" -jar /home/unruh/.IdeaIC2016.2/config/plugins/Scala/launcher/sbt-launch.jar "$@"
35 changes: 31 additions & 4 deletions src/cmathml/CMathML.scala
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package cmathml

import java.math.{BigInteger, MathContext}
import java.util.stream.Stream

import cmathml.CMathML._
import com.sun.org.apache.xerces.internal.util.XMLChar
Expand All @@ -9,6 +10,7 @@ import org.symcomp.openmath.{OMSymbol, _}
import _root_.z3.Z3
import com.sun.glass.events.KeyEvent
import misc.Utils.Typed
import org.antlr.v4.runtime.{ANTLRInputStream, BailErrorStrategy, CommonTokenStream}

import scala.collection.mutable
import scala.reflect.internal.JavaAccFlags
Expand Down Expand Up @@ -166,7 +168,20 @@ object CMathML {

private lazy val z3 = new Z3()

def fromPopcorn(str: String) = {

@Pure
def fromPopcorn(popcorn:String) : CMathML = {
val stream = new ANTLRInputStream(popcorn)
val lexer = new PopcornGrammarLexer(stream)
val tokens = new CommonTokenStream(lexer)
val parser = new PopcornGrammarParser(tokens)
parser.setErrorHandler(new BailErrorStrategy)
val tree = parser.expr_eof()
tree.cmathml
}

@deprecated("use fromPopcorn","Aug 21, 2016")
def fromPopcornSYMCOMP(str: String) = {
val om = OpenMathBase.parsePopcorn(str.trim)
fromSymcomp(om)
}
Expand Down Expand Up @@ -260,7 +275,7 @@ object CMathML {
def sum(x:CMathML, y:CMathML) : Apply = Apply(sum,x,y)
val product = CSymbol(cd,"product")
def product(x:CMathML, y:CMathML) : Apply = Apply(product,x,y)
val uminus = CSymbol(cd,"unary_minus")
val uminus = CSymbol(cd,"unary_minus") // TODO rename
def uminus(x:CMathML) : Apply = Apply(uminus,x)
}

Expand Down Expand Up @@ -807,6 +822,9 @@ final case class CError(attributes : Attributes, cd: String, name: String, args:
for (Typed(m:CMathML) <- args) m.freeVariables$(acc,hidden)
}
}
object CError {
def apply(cd: String, name: String, args: Any*) = new CError(NoAttr, cd, name, args :_*)
}

/** An addition to the Content MathML standard. Represents a missing node.
* Not valid Content MathML, cannot be exported to valid XML
Expand Down Expand Up @@ -865,6 +883,15 @@ final case class PathRev(path : List[Int]) extends AnyVal {

/** Various convenience methods to ease access to CMathML objects from Java */
object JavaHelpers {
@annotation.varargs
def apply(hd:CMathML, args:CMathML*) = Apply(hd,args:_*)
import scala.collection.JavaConverters._
@annotation.varargs def apply(cd:String, name:String, args:CMathML*) = Apply(CSymbol(cd,name), args:_*)
def apply(cd:String, name:String, args:Stream[CMathML]) = Apply(CSymbol(cd,name), args.iterator.asScala.toSeq :_*)
def apply(hd: CMathML, args:Stream[CMathML]) = Apply(hd, args.iterator.asScala.toSeq :_*)
def addAttributes(math: CMathML, attrs:Stream[org.antlr.v4.runtime.misc.Pair[CSymbol,CMathML]]) : CMathML = ???
def bind(hd:CMathML, vars:Stream[CILike], body:CMathML) = Bind(hd, vars.iterator.asScala.toSeq, body)
def error(hd:CSymbol, args:Stream[CMathML]) = CError(hd.cd,hd.name, args.iterator.asScala.toSeq)
def cn(i:String) = CN(i)
def ci(i:String) = CI(i)
def cs(i:String) = CS(i)
def csymbol(cd:String, name:String) = CSymbol(cd,name)
}
Loading

0 comments on commit 6e589b2

Please sign in to comment.