lean-language-javascript

Port of https://hackage.haskell.org/package/language-javascript

JavaScript and TypeScript in Lean 4: a lexer and parser, several syntax trees, a minifier, and printers which reproduce, character for character, what the prettier code formatter writes.

Install

In lakefile.toml

[[require]]
name = "LanguageJavascript"
git = "https://github.com/srghma/lean-language-javascript.git"
subdir = "lib"
rev = "main"

The libraries

Library	What is in it
LanguageJavascriptCommon	The only library the other four share. Everything here is independent of any syntax tree: Types (the refined leaves — a non-empty string or list, a number literal, a regular expression literal, the source form of a string literal), Common (the leaf types the trees agree on: the operators, the declaration keywords, name as alias, the import attributes, the JSX names), Unicode (the identifier character tables), RegExpEngine, Doc (the document algebra prettier lays out), Options (prettier's options record), StringLit (reading and writing the text of a literal), PrinterCommon (the parts of a printer that do not look at a tree) and JSXLayout (the layout of a JSX element from documents alone). The *Spec modules here are proofs about the literals of Types.
LanguageJavascript	The full tree. Token/SrcLocation/Lexer (the tokens and where they come from), AST (the tree), Parser (recursive descent, one function per production), Printer, Minify and ShowStripped; MinifySpec and TokenTextSpec are proofs about those modules rather than tests.
LanguageJavascriptMini	The small JavaScript tree the printer walks. AST and ASTOps (the tree and its smart constructors), Printer/PrinterSupport (the printer) and JSX.
LanguageJavascriptMiniTsAST	The same for TypeScript: AST, ASTEq, ASTOps, JSX and Printer/PrinterSupport.
LanguageJavascriptBrujin	A scope safe tree, where a variable is an index into the scope its type records, together with Strengthen (removing a binding) and Optimizer.
LanguageJavascriptConversions	The only library which may name two trees. MiniOfFull/MiniToFull (the small JavaScript tree read from, and written back as, the full tree), MiniElab and BrujinElab (the js! and jsb! syntax, which read a source text while Lean elaborates), MiniImportAttrSpec (a proof which needs the parser), BrujinOfMini/BrujinToMini (the scope safe tree read from, and written back as, the small one) and MiniTsOfJS (a JavaScript tree read as a TypeScript one).

How the libraries may depend on each other

A module of one tree's library never imports a module of another tree's library. What two trees share lives in LanguageJavascriptCommon, and that library depends on no tree.

A conversion names two trees by its very nature, so no conversion lives in a tree's library either: they are all in LanguageJavascriptConversions, which sits above the four and which nothing below it imports. The layering is therefore LanguageJavascriptCommon → each tree → LanguageJavascriptConversions.

The JavaScript and TypeScript printers share LanguageJavascriptCommon.PrinterCommon (operator text and precedence, argument lists, blocks, declarations, rendering) and LanguageJavascriptCommon.JSXLayout (the layout of a JSX element). In each printer, PrinterSupport holds the tests a layout decision is made by and Printer the mutually recursive walk of the tree.

The tests

LanguageJavascriptTests holds the suite, one module per subject, with the helpers used by more than one of them in Support (the name a source is given as a test, the printed form of a parse result), Mini/Support and Brujin/Support (reading a source into the deterministic and the scope safe tree, and the round trips they are checked by). MiniAstAndTsAstPrinterPrettierParityTests holds the corpus and the random program generators the prettier comparison scripts use.

Building and testing

lake build          # the shared library, the four trees and the conversions
lake test           # the test suite (also: lake exe tests)

The other executables are bench and unibench (timings of the parser and of the Unicode tables), dump/dumpts/dumpjsts (print the corpus), fuzz/fuzzts/fuzztsgen (print random programs) and scratch/scratchts (print the samples of the Scratch modules).

Ideas for further work

PROPOSALS.md collects concrete proposals for the library — coverage gaps (comments and blank lines, a TypeScript parser), properties worth proving, measured performance and build-time findings, and tooling — each with the evidence behind it and a sketch of how to carry it out.

Checking against prettier

The scripts/ directory compares the printers with prettier itself. They need node and an installed prettier; PRETTIER may point at the module, for example PRETTIER=/path/to/node_modules/prettier/index.mjs.

sh scripts/check.sh            # JavaScript: the corpus and random programs
sh scripts/check-ts.sh         # TypeScript: the corpus, the JavaScript corpus read
                               # as TypeScript, and random programs
sh scripts/check-options.sh    # the same under options other than prettier's default
sh scripts/sweep-ts.sh         # a wider sweep; see also scripts/sweep-options*.sh

Each script takes an optional sample count and seed. scripts/format.mjs formats one file with prettier, and scripts/diff-prettier*.mjs show the samples the printer and prettier disagree on.