Exploring the Ohmjs parser

quint/package.json

@@ -69,22 +69,24 @@
     "yargs": "^17.2.1"
   },
   "scripts": {
-    "compile": "genversion -e src/version.ts && tsc && copyfiles -u 1 ./src/reflection.proto ./src/builtin.qnt ./dist/src/",
+    "compile": "genversion -e src/version.ts && tsc && copyfiles -u 1 ./src/reflection.proto ./src/builtin.qnt src/generated/quint.ohm-bundle.* ./dist/src/",
     "prepare": "rm -rf ./dist && npm run compile && chmod +x ./dist/src/cli.js",
     "test": "mocha --reporter-option maxDiffSize=0 -r ts-node/register test/*.test.ts test/**/*.test.ts",
     "coverage": "nyc npm run test",
     "integration": "txm cli-tests.md && txm io-cli-tests.md",
     "apalache-integration": "txm apalache-tests.md",
     "apalache-dist": "txm apalache-dist-tests.md",
-    "generate": "npm run antlr && npm run compile && npm link && npm run api-docs && npm run update-fixtures",
+    "generate": "npm run antlr && npm run ohmjs && npm run compile && npm link && npm run api-docs && npm run update-fixtures",
     "antlr": "antlr4ts -visitor ./src/generated/Quint.g4 && antlr4ts -visitor ./src/generated/Effect.g4",
+    "ohmjs": "npx ohm generateBundles --withTypes src/generated/quint.ohm",
     "api-docs": "quint docs ./src/builtin.qnt > ../doc/builtin.md",
     "update-fixtures": "./scripts/update-fixtures.sh",
     "format-check": "npx prettier --check '**/*.ts' && npx eslint '**/*.ts'",
     "format": "npx prettier --write '**/*.ts' && npx eslint --fix '**/*.ts'",
     "debug": "npx ts-node ./src/cli.ts"
   },
   "devDependencies": {
+    "@ohm-js/cli": "^2.0.0",
     "@types/chai": "^4.2.18",
     "@types/json-bigint": "^1.0.1",
     "@types/lodash.isequal": "^4.5.6",

quint/scripts/parse-ohmjs.js

@@ -0,0 +1,23 @@
+#!/usr/bin/env node
+
+// A test script to make sure that our Ohmjs grammar conforms to the Antlr4
+// grammar. Since we do not allow the user to parse files via Ohmjs directly,
+// we have this script, for debugging purposes.
+
+const fs = require('fs')
+const quint = require('../src/generated/quint.ohm-bundle.js')
+const filename = process.argv[2]
+if (!filename) {
+  console.error('Expected an input file as my first argument')
+  process.exit(1)
+}
+
+const text = fs.readFileSync(filename, 'utf-8')
+const m = quint.match(text)
+if (m.failed()) {
+  console.error(m.message)
+  process.exit(2)
+} else {
+  // nothing to report
+  process.exit(0)
+}

quint/src/ErrorMessage.ts

@@ -23,10 +23,22 @@ export interface ErrorMessage {
   locs: Loc[]
 }
 
+/**
+ * A single-point position in a file.
+ */
+export interface Pos {
+  line: number
+  col: number
+  index: number
+}
+
+/**
+ * An interval in a file.
+ */
 export interface Loc {
   source: string
-  start: { line: number; col: number; index: number }
-  end?: { line: number; col: number; index: number }
+  start: Pos
+  end?: Pos
 }
 
 /**

quint/src/generated/.gitattributes

@@ -2,3 +2,4 @@
 *.tokens linguist-generated
 *.ts linguist-generated
 *.jar linguist-generated
+*.ohm-bundle.* linguist-generated