SyntaxGen - Lean 4 Syntax Generator

Quick Start

SyntaxGen produces unelaborated syntax trees from grammar definitions, useful for generating ML training data and property-based testing.

Installation

Add to your lakefile.lean:

require SyntaxGen from git "https://github.com/alok/SyntaxGen"@"main"

Basic Usage

import SyntaxGen

-- Generate examples for built-in categories
#syntaxgen term 5
#syntaxgen tactic 10

-- Weighted generation (more realistic)
#syntaxgen_weighted term 10

-- Export to JSON Lines for ML training
#syntaxgen_export term 1000 to "training.jsonl"

-- Round-trip testing
#syntaxgen_roundtrip term 50

Features

ML Training Export

Export to JSON Lines or CSV with metadata (complexity, seed) for reproducible ML datasets.

Weighted Generation

Probability-weighted sampling produces more realistic examples with simpler terms appearing more frequently.

Round-Trip Testing

Verify parser correctness with generate → format → parse cycle testing.

Syntax Shrinking

Minimize counterexamples for property-based testing with multiple shrinking strategies.

Template System

Define generators for custom syntax using a simple template DSL.

Deterministic

Reproducible generation with seed-based random number generation.

Commands Reference

Core Generation

Command	Description
`#syntaxgen <cat> [n]`	Generate n examples from category
`#syntaxgen_weighted <cat> [n]`	Weighted generation (realistic)
`#syntaxgen_pretty <cat> [n]`	Pretty-printed output

ML Export

Command	Description
`#syntaxgen_export <cat> [n] to "path"`	Export to file (.jsonl, .csv)
`#syntaxgen_batch [cats] [n] to "path"`	Batch export multiple categories
`#syntaxgen_jsonl <cat> [n]`	Preview JSON Lines output
`#syntaxgen_stats <cat> [n]`	Show generation statistics

Testing

Command	Description
`#syntaxgen_roundtrip <cat> [n]`	Test generate → format → parse
`#syntaxgen_roundtrip_verbose <cat> [n]`	Verbose round-trip output
`#syntaxgen_shrink <cat> [seed]`	Show shrink tree

Templates

Command	Description
`#gen_template <name> [n]`	Generate from template
`syntax_gen <pattern> : <cat> as <name>`	Register custom generator

Modules

Module	Description
`Basic`	Core generator monad and built-in category generators
`Weighted`	Probability-weighted generation for realistic examples
`Pretty`	Enhanced pretty-printing with smart spacing
`Export`	JSON/CSV export for ML training datasets
`RoundTrip`	Parse round-trip testing
`Shrink`	Syntax shrinking for property testing
`Auto`	Automatic generator registration from patterns
`Macro`	Template-based generation

Examples

Custom List Comprehension

import SyntaxGen

-- Define syntax
syntax "[" term "|" term " in " term (" if " term)? "]" : term

-- Macro rules
macro_rules
  | `([ $expr | $item in $items if $pred ]) =>
      `(List.map (fun $item => $expr) (List.filter (fun $item => $pred) $items))
  | `([ $expr | $item in $items ]) =>
      `(List.map (fun $item => $expr) $items)

-- Use template generator
#gen_template listComp 5

JSON Export Format

{"text": "fun x => x + 1", "category": "term", "complexity": 5, "seed": 42}

Plausible Integration

SyntaxGen is designed to integrate with Plausible for property-based testing:

Shrinkable Syntax via the Shrink module
Round-trip tests for parser verification
Deterministic generation for reproducibility