|
| 1 | +# TypeScript Frontend for Strata |
| 2 | + |
| 3 | +This directory contains a manual TypeScript frontend for Strata that translates TypeScript programs to Strata's internal representation for analysis and verification. |
| 4 | + |
| 5 | +## Architecture Overview |
| 6 | + |
| 7 | +The TypeScript frontend consists of several key components that work together to parse, translate, and evaluate TypeScript code: |
| 8 | + |
| 9 | +### Core Files |
| 10 | + |
| 11 | +#### `js_ast.lean` - AST Node Definitions |
| 12 | +This file defines the **structure of TypeScript AST nodes** in Lean. Each TypeScript construct (variables, functions, expressions, etc.) has a corresponding Lean structure. |
| 13 | + |
| 14 | +**Key components:** |
| 15 | +- `BaseNode` - Common fields for all AST nodes (location, type info) |
| 16 | +- Type definitions: `TS_TSNumberKeyword`, `TS_TSBooleanKeyword`, `TS_TSStringKeyword` |
| 17 | +- Expression types: `TS_BinaryExpression`, `TS_CallExpression`, `TS_Identifier`, etc. |
| 18 | +- Statement types: `TS_VariableDeclaration`, `TS_FunctionDeclaration`, `TS_IfStatement`, etc. |
| 19 | +- Root types: `TS_Program`, `TS_File` |
| 20 | + |
| 21 | +**What students modify:** Add new `structure` definitions for unsupported TypeScript constructs, then add them to the appropriate `inductive` type. |
| 22 | + |
| 23 | +#### `TS_to_Strata.lean` - Translation Engine |
| 24 | +This file contains the **core translation logic** that converts TypeScript AST nodes into Strata's internal representation (CallHeap statements). |
| 25 | + |
| 26 | +**Key functions:** |
| 27 | +- `translate_expression` - Converts TypeScript expressions to Strata expressions |
| 28 | +- `translate_statement` - Converts TypeScript statements to Strata statements |
| 29 | +- `TS_type_to_HMonoTy` - Maps TypeScript types to Strata heap types |
| 30 | +- `extract_type_from_annotation` - Handles TypeScript type annotations |
| 31 | + |
| 32 | +**What students modify:** Add new translation cases for the AST nodes they added to `js_ast.lean`. |
| 33 | + |
| 34 | +#### `TSStrataStatement.lean` - Statement Wrappers |
| 35 | +This file provides **TypeScript-specific aliases** for Strata's generic CallHeap statements. It's mostly just type aliases to make the code more readable. |
| 36 | + |
| 37 | +**Contents:** |
| 38 | +```lean |
| 39 | +abbrev TSStrataStatement := CallHeapStrataStatement |
| 40 | +abbrev TSStrataExpression := CallHeapStrataExpression |
| 41 | +-- etc. |
| 42 | +``` |
| 43 | + |
| 44 | +**What students modify:** Usually nothing - this file rarely needs changes. |
| 45 | + |
| 46 | +#### `TSStrataEval.lean` - Evaluation Helpers |
| 47 | +Contains **utility functions** for evaluating TypeScript constructs within Strata's evaluation framework. |
| 48 | + |
| 49 | +**What students modify:** May need to add evaluation helpers for complex new constructs. |
| 50 | + |
| 51 | +#### `TSFunction.lean` - Function Utilities |
| 52 | +Contains **function-specific utilities** and helpers for handling TypeScript function declarations and calls. |
| 53 | + |
| 54 | +**What students modify:** May need updates when adding new function-related features. |
| 55 | + |
| 56 | +## Currently Supported Features |
| 57 | + |
| 58 | +### Data Types |
| 59 | +- `number` - Numeric literals and arithmetic |
| 60 | +- `string` - String literals |
| 61 | +- `boolean` - Boolean literals and logic |
| 62 | +- `null` - Null values |
| 63 | + |
| 64 | +### Expressions |
| 65 | +- **Binary expressions**: `+`, `-`, `*`, `/`, `%`, `==`, `!=`, `<`, `>`, `<=`, `>=` |
| 66 | +- **Logical expressions**: `&&`, `||` |
| 67 | +- **Unary expressions**: `-`, `!` |
| 68 | +- **Assignment expressions**: `=` |
| 69 | +- **Conditional expressions**: `condition ? true_val : false_val` |
| 70 | +- **Member expressions**: `obj[0]`, `obj[1]` (numeric keys only) |
| 71 | +- **Call expressions**: `func(arg1, arg2)` |
| 72 | + |
| 73 | +### Statements |
| 74 | +- **Variable declarations**: `let x: number = 5;` |
| 75 | +- **Function declarations**: `function name(params): returnType { ... }` |
| 76 | +- **If statements**: `if (condition) { ... } else { ... }` |
| 77 | +- **Return statements**: `return value;` |
| 78 | +- **Expression statements**: `x + 5;` |
| 79 | +- **Block statements**: `{ ... }` |
| 80 | + |
| 81 | +### Objects |
| 82 | +- Objects with **numeric keys only**: `{0: value1, 1: value2}` |
| 83 | +- Member access with numeric indices: `obj[0]` |
| 84 | + |
| 85 | +## Running Tests |
| 86 | + |
| 87 | +### Prerequisites |
| 88 | +```bash |
| 89 | +# Install Node.js dependencies |
| 90 | +npm install -g ts-node typescript |
| 91 | +npm install @babel/parser @babel/types @babel/traverse @babel/generator |
| 92 | + |
| 93 | +# Install Python dependencies |
| 94 | +pip install tqdm |
| 95 | + |
| 96 | +# Build Strata |
| 97 | +lake build StrataTypeScriptRunner |
| 98 | +``` |
| 99 | + |
| 100 | +### Running Conformance Tests |
| 101 | +```bash |
| 102 | +# Run all TypeScript tests |
| 103 | +cd conformance_testing |
| 104 | +python3 conformance_cli.py test ../StrataTest/Languages/TypeScript -l typescript -v |
| 105 | + |
| 106 | +# Run a specific test file |
| 107 | +python3 conformance_cli.py test ../StrataTest/Languages/TypeScript/test_variables.ts -l typescript -v |
| 108 | +``` |
| 109 | + |
| 110 | +### Test262 Test Suite |
| 111 | +This directory also contains modified tests from **Test262**, the official ECMAScript conformance test suite. Test262 is the standard test suite used to validate JavaScript engines and ensure they correctly implement the ECMAScript specification. |
| 112 | + |
| 113 | +**About Test262:** |
| 114 | +- Official test suite for JavaScript/ECMAScript compliance |
| 115 | +- Contains thousands of tests covering all language features |
| 116 | +- Used by browser vendors and JavaScript engine developers |
| 117 | +- Tests both positive cases (should work) and negative cases (should throw errors) |
| 118 | + |
| 119 | +**Modified Test262 Files:** |
| 120 | +The Test262 files in this directory have been adapted for the Strata TypeScript frontend. Note that many don't work yet because the test harness itself uses `assertThrows` statements, which require **function pointers** (passing functions as arguments) - a feature not yet supported in our frontend. |
| 121 | + |
| 122 | +**Using Test262 Tests:** |
| 123 | +Students can use these as reference implementations and test cases when adding new features. The tests show expected behavior for various JavaScript constructs and edge cases. Once function pointers are implemented, many more Test262 tests will become runnable. |
| 124 | + |
| 125 | +For more information about Test262, see: https://github.com/tc39/test262 |
| 126 | + |
| 127 | +### Understanding Test Results |
| 128 | +- **Pass**: Native TypeScript execution matches Strata evaluation |
| 129 | +- **Fail**: Mismatch between native and Strata results |
| 130 | +- **Failed files** are saved to `failures/` directory for debugging |
| 131 | + |
| 132 | +## Student Development Workflow |
| 133 | + |
| 134 | +### 1. Identify Missing Feature |
| 135 | +Run conformance tests to see what fails: |
| 136 | +```bash |
| 137 | +cd conformance_testing |
| 138 | +python3 conformance_cli.py test ../StrataTest/Languages/TypeScript -l typescript -v |
| 139 | +``` |
| 140 | + |
| 141 | +### 2. Add AST Definition |
| 142 | +Add the structure to `js_ast.lean`: |
| 143 | +```lean |
| 144 | +structure TS_YourNewConstruct extends BaseNode where |
| 145 | + field1 : Type1 |
| 146 | + field2 : Type2 |
| 147 | +deriving Repr, Lean.FromJson, Lean.ToJson |
| 148 | +``` |
| 149 | + |
| 150 | +### 3. Add to Inductive Type |
| 151 | +Add your construct to the appropriate inductive (TS_Expression or TS_Statement): |
| 152 | +```lean |
| 153 | +inductive TS_Statement where |
| 154 | + -- ... existing cases ... |
| 155 | + | TS_YourNewConstruct : TS_YourNewConstruct → TS_Statement |
| 156 | +``` |
| 157 | + |
| 158 | +### 4. Implement Translation |
| 159 | +Add translation logic in `TS_to_Strata.lean`: |
| 160 | +```lean |
| 161 | +def translate_your_construct (construct: TS_YourNewConstruct) (ctx: TranslationContext) : |
| 162 | + TranslationContext × List TSStrataStatement := |
| 163 | + -- Your implementation here |
| 164 | +``` |
| 165 | + |
| 166 | +### 5. Test and Debug |
| 167 | +```bash |
| 168 | +lake build StrataTypeScriptRunner |
| 169 | +python3 conformance_cli.py test ../StrataTest/Languages/TypeScript/your_test.ts -l typescript -v |
| 170 | +``` |
| 171 | + |
| 172 | +### 6. Iterate |
| 173 | +- **Parse errors** → Fix AST structure |
| 174 | +- **Translation errors** → Fix translation logic |
| 175 | +- **Wrong results** → Check semantic correctness |
| 176 | + |
| 177 | +## Common Error Messages |
| 178 | + |
| 179 | +### "no inductive constructor matched" |
| 180 | +- **Cause:** AST structure in `js_ast.lean` doesn't match what the parser generates |
| 181 | +- **Fix:** Check the AST structure and adjust your Lean definitions |
| 182 | + |
| 183 | +### "Native execution failed" |
| 184 | +- **Cause:** TypeScript code has syntax errors or uses unsupported features |
| 185 | +- **Fix:** Simplify the test case or check TypeScript syntax |
| 186 | + |
| 187 | +### "Value mismatches" |
| 188 | +- **Cause:** Translation logic doesn't match native TypeScript semantics |
| 189 | +- **Fix:** Debug the translation in `TS_to_Strata.lean` |
| 190 | + |
| 191 | +### "Failed to convert JSON to Node" |
| 192 | +- **Cause:** Field name or structure mismatch in AST definition |
| 193 | +- **Fix:** Check that your Lean structure matches the expected format |
| 194 | + |
| 195 | +## Debugging Tips |
| 196 | + |
| 197 | +1. **Start simple**: Begin with the most basic version of a feature |
| 198 | +2. **Test incrementally**: Get simple cases working before complex ones |
| 199 | +3. **Compare with working examples**: Look at existing test files that pass |
| 200 | +4. **Check the roadmap**: See `FEATURES_ROADMAP.md` for implementation priorities |
| 201 | + |
| 202 | +## Next Steps |
| 203 | + |
| 204 | +See `FEATURES_ROADMAP.md` for a comprehensive list of features to implement, organized by priority. Start with Priority 1 features like loops and arrays for maximum impact. |
| 205 | + |
| 206 | +This manual approach gives you complete control over how TypeScript constructs map to Strata's internal representation, making it perfect for educational purposes and incremental development. |
0 commit comments