Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: export to javascript using scala-js #4

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 24 additions & 0 deletions .github/workflows/scalajs.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
# Build JS files using https://www.scala-js.org/
name: ScalaJS
on:
push:
branches: [master, main]
pull_request:
branches: [master, main]
jobs:
build-scala-js:
runs-on: ubuntu-20.04
steps:
- name: Checkout
uses: actions/checkout@v1
- name: Setup Scala
uses: olafurpg/setup-scala@v10
with:
java-version: "[email protected]"
- name: Build and Test
run: sbt -v -Dfile.encoding=UTF-8 +fullLinkJS
- name: Upload Artifact
uses: actions/upload-artifact@v2
with:
name: scala-js
path: target/scala-2.13/scala-tptp-parser-opt/
4 changes: 4 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -28,3 +28,7 @@ bin/*
*.swp
*~
ext_config


# OSX
.DS_Store
13 changes: 13 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,19 @@ libraryDependencies += "io.github.leoprover" %% "scala-tptp-parser" % "1.3"
### Non-sbt-projects
In order to use the library with a non-sbt project, you can simply compile the library and use the class files as an unmanaged dependency/class path. The latest release JAR can also be downloaded from the Maven Central link above.

#### ScalaJS
This project supports very basic (and untested) export to JavaScript ESModule using [ScalaJS](https://www.scala-js.org/).

To compile an unoptimized version use `sbt fastLinkJS`, for an optimized version `sbt fullLinkJS`.

To use it in your code import the TPTPParser Object:

```javascript
import {TPTPParser} from "./main.js";

console.log(TPTPParser.annotatedTHF("thf(f, axiom, ![X:$i]: (p @ X))."));
```

## Usage
The parser object `TPTPParser` offers several methods for parsing TPTP problems, annotated formulas or simple formulas. The input is transformed into an
abstract syntax tree (AST) provided at `leo.datastructures.TPTP`. The ASTs are mostly case classes that can be further processed by pattern matching.
Expand Down
3 changes: 3 additions & 0 deletions build.sbt
Original file line number Diff line number Diff line change
Expand Up @@ -41,3 +41,6 @@ lazy val tptpParser = (project in file("."))

libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.5" % "test"
)
.enablePlugins(ScalaJSPlugin)

scalaJSLinkerConfig ~= { _.withModuleKind(ModuleKind.ESModule) }
3 changes: 2 additions & 1 deletion project/plugins.sbt
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
addSbtPlugin("com.geirsson" % "sbt-ci-release" % "1.5.7")
addSbtPlugin("com.geirsson" % "sbt-ci-release" % "1.5.7")
addSbtPlugin("org.scala-js" % "sbt-scalajs" % "1.5.1")
3 changes: 3 additions & 0 deletions src/main/scala/leo/modules/input/TPTPParser.scala
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ import leo.datastructures.TPTP.TCFAnnotated
import java.util.NoSuchElementException
import scala.annotation.tailrec
import scala.io.Source
import scala.scalajs.js.annotation.{JSExportAll, JSExportTopLevel}

/**
*
Expand Down Expand Up @@ -54,6 +55,8 @@ import scala.io.Source
* @note Limitations: Currently, FOOL logic (i.e., TFX) cannot be parsed.
* @since January 2021
*/
@JSExportTopLevel("TPTPParser")
@JSExportAll
object TPTPParser {
import datastructures.TPTP.{Problem, AnnotatedFormula, THFAnnotated, TFFAnnotated,
FOFAnnotated, CNFAnnotated, TPIAnnotated}
Expand Down