# CSDL Parser and Translator Design
## Architecture Overview
The CSDL parser follows a multi-stage pipeline architecture:
```
┌─────────────┐ ┌──────────┐ ┌────────────┐ ┌─────────────┐ ┌─────────────┐
│ Source │────▶│ Lexer │────▶│ Parser │────▶│ Type │────▶│ Z3 │
│ Code │ │(Tokenize)│ │(Build AST) │ │ Checker │ │ Translator │
└─────────────┘ └──────────┘ └────────────┘ └─────────────┘ └─────────────┘
│ │ │
▼ ▼ ▼
┌────────────┐ ┌─────────────┐ ┌─────────────┐
│ Symbol │ │ Typed │ │ Z3 Python │
│ Table │ │ AST │ │ API │
└────────────┘ └─────────────┘ └─────────────┘
```
## Stage 1: Lexical Analysis (Tokenizer)
### Token Types
```typescript
export enum TokenType {
// Keywords
VAR = 'VAR',
CONST = 'CONST',
FUNCTION = 'FUNCTION',
CONSTRAINT_TYPE = 'CONSTRAINT_TYPE',
IF = 'IF',
THEN = 'THEN',
ELSE = 'ELSE',
FORALL = 'FORALL',
EXISTS = 'EXISTS',
IN = 'IN',
ASSERT = 'ASSERT',
SOFT = 'SOFT',
CHECK_SAT = 'CHECK_SAT',
MINIMIZE = 'MINIMIZE',
MAXIMIZE = 'MAXIMIZE',
WEIGHT = 'WEIGHT',
// Type keywords
INT = 'INT',
REAL = 'REAL',
BOOL = 'BOOL',
STRING = 'STRING',
BITVEC = 'BITVEC',
ARRAY = 'ARRAY',
TUPLE = 'TUPLE',
SET = 'SET',
// Literals
NUMBER = 'NUMBER',
STRING_LITERAL = 'STRING_LITERAL',
TRUE = 'TRUE',
FALSE = 'FALSE',
// Identifiers
IDENTIFIER = 'IDENTIFIER',
// Operators
PLUS = 'PLUS', // +
MINUS = 'MINUS', // -
STAR = 'STAR', // *
SLASH = 'SLASH', // /
DIV = 'DIV', // div
PERCENT = 'PERCENT', // %
POWER = 'POWER', // **
// Comparison
EQ = 'EQ', // ==
NE = 'NE', // !=
LT = 'LT', // <
LE = 'LE', // <=
GT = 'GT', // >
GE = 'GE', // >=
// Logical
AND = 'AND', // and, &&
OR = 'OR', // or, ||
NOT = 'NOT', // not, !
IMPLIES = 'IMPLIES', // =>, implies
IFF = 'IFF', // <=>, iff
XOR = 'XOR', // xor
// Bitwise
BIT_AND = 'BIT_AND', // &
BIT_OR = 'BIT_OR', // |
BIT_XOR = 'BIT_XOR', // ^
BIT_NOT = 'BIT_NOT', // ~
LSHIFT = 'LSHIFT', // <<
RSHIFT = 'RSHIFT', // >>
ARSHIFT = 'ARSHIFT', // >>>
// Delimiters
LPAREN = 'LPAREN', // (
RPAREN = 'RPAREN', // )
LBRACKET = 'LBRACKET', // [
RBRACKET = 'RBRACKET', // ]
LBRACE = 'LBRACE', // {
RBRACE = 'RBRACE', // }
// Punctuation
COMMA = 'COMMA', // ,
COLON = 'COLON', // :
SEMICOLON = 'SEMICOLON', // ;
DOT = 'DOT', // .
DOTDOT = 'DOTDOT', // ..
DOTDOTLT = 'DOTDOTLT', // ..<
ARROW = 'ARROW', // ->
ASSIGN = 'ASSIGN', // =
// Special
COMMENT = 'COMMENT',
NEWLINE = 'NEWLINE',
EOF = 'EOF',
}
export interface Token {
type: TokenType;
value: string;
line: number;
column: number;
}
```
### Lexer Implementation
```typescript
export class Lexer {
private source: string;
private position: number = 0;
private line: number = 1;
private column: number = 1;
constructor(source: string) {
this.source = source;
}
/**
* Get the next token from the source
*/
public nextToken(): Token {
this.skipWhitespace();
if (this.isAtEnd()) {
return this.makeToken(TokenType.EOF, '');
}
const char = this.peek();
// Comments
if (char === '#') {
return this.scanComment();
}
// String literals
if (char === '"' || char === "'") {
return this.scanString();
}
// Numbers
if (this.isDigit(char)) {
return this.scanNumber();
}
// Identifiers and keywords
if (this.isAlpha(char) || char === '_') {
return this.scanIdentifier();
}
// Operators and punctuation
return this.scanOperator();
}
/**
* Tokenize the entire source
*/
public tokenize(): Token[] {
const tokens: Token[] = [];
let token: Token;
do {
token = this.nextToken();
tokens.push(token);
} while (token.type !== TokenType.EOF);
return tokens;
}
private scanComment(): Token {
const start = this.position;
this.advance(); // Skip #
while (!this.isAtEnd() && this.peek() !== '\n') {
this.advance();
}
const value = this.source.substring(start, this.position);
return this.makeToken(TokenType.COMMENT, value);
}
private scanString(): Token {
const quote = this.advance();
const start = this.position;
while (!this.isAtEnd() && this.peek() !== quote) {
if (this.peek() === '\\') {
this.advance(); // Skip escape character
}
this.advance();
}
if (this.isAtEnd()) {
throw new Error(`Unterminated string at line ${this.line}, column ${this.column}`);
}
const value = this.source.substring(start, this.position);
this.advance(); // Closing quote
return this.makeToken(TokenType.STRING_LITERAL, value);
}
private scanNumber(): Token {
const start = this.position;
while (this.isDigit(this.peek())) {
this.advance();
}
// Check for decimal point
if (this.peek() === '.' && this.isDigit(this.peekNext())) {
this.advance(); // Consume '.'
while (this.isDigit(this.peek())) {
this.advance();
}
}
// Check for scientific notation
if (this.peek() === 'e' || this.peek() === 'E') {
this.advance();
if (this.peek() === '+' || this.peek() === '-') {
this.advance();
}
while (this.isDigit(this.peek())) {
this.advance();
}
}
const value = this.source.substring(start, this.position);
return this.makeToken(TokenType.NUMBER, value);
}
private scanIdentifier(): Token {
const start = this.position;
while (this.isAlphaNumeric(this.peek())) {
this.advance();
}
const value = this.source.substring(start, this.position);
const type = this.getKeywordType(value);
return this.makeToken(type, value);
}
private scanOperator(): Token {
const char = this.advance();
switch (char) {
case '+': return this.makeToken(TokenType.PLUS, '+');
case '-':
if (this.match('>')) {
return this.makeToken(TokenType.ARROW, '->');
}
return this.makeToken(TokenType.MINUS, '-');
case '*':
if (this.match('*')) {
return this.makeToken(TokenType.POWER, '**');
}
return this.makeToken(TokenType.STAR, '*');
case '/': return this.makeToken(TokenType.SLASH, '/');
case '%': return this.makeToken(TokenType.PERCENT, '%');
case '=':
if (this.match('=')) {
return this.makeToken(TokenType.EQ, '==');
}
if (this.match('>')) {
return this.makeToken(TokenType.IMPLIES, '=>');
}
return this.makeToken(TokenType.ASSIGN, '=');
case '!':
if (this.match('=')) {
return this.makeToken(TokenType.NE, '!=');
}
return this.makeToken(TokenType.NOT, '!');
case '<':
if (this.match('=')) {
if (this.match('>')) {
return this.makeToken(TokenType.IFF, '<=>');
}
return this.makeToken(TokenType.LE, '<=');
}
if (this.match('<')) {
return this.makeToken(TokenType.LSHIFT, '<<');
}
return this.makeToken(TokenType.LT, '<');
case '>':
if (this.match('=')) {
return this.makeToken(TokenType.GE, '>=');
}
if (this.match('>')) {
if (this.match('>')) {
return this.makeToken(TokenType.ARSHIFT, '>>>');
}
return this.makeToken(TokenType.RSHIFT, '>>');
}
return this.makeToken(TokenType.GT, '>');
case '&':
if (this.match('&')) {
return this.makeToken(TokenType.AND, '&&');
}
return this.makeToken(TokenType.BIT_AND, '&');
case '|':
if (this.match('|')) {
return this.makeToken(TokenType.OR, '||');
}
return this.makeToken(TokenType.BIT_OR, '|');
case '^': return this.makeToken(TokenType.BIT_XOR, '^');
case '~': return this.makeToken(TokenType.BIT_NOT, '~');
case '(': return this.makeToken(TokenType.LPAREN, '(');
case ')': return this.makeToken(TokenType.RPAREN, ')');
case '[': return this.makeToken(TokenType.LBRACKET, '[');
case ']': return this.makeToken(TokenType.RBRACKET, ']');
case '{': return this.makeToken(TokenType.LBRACE, '{');
case '}': return this.makeToken(TokenType.RBRACE, '}');
case ',': return this.makeToken(TokenType.COMMA, ',');
case ':': return this.makeToken(TokenType.COLON, ':');
case ';': return this.makeToken(TokenType.SEMICOLON, ';');
case '.':
if (this.match('.')) {
if (this.match('<')) {
return this.makeToken(TokenType.DOTDOTLT, '..<');
}
return this.makeToken(TokenType.DOTDOT, '..');
}
return this.makeToken(TokenType.DOT, '.');
default:
throw new Error(`Unexpected character '${char}' at line ${this.line}, column ${this.column}`);
}
}
private getKeywordType(value: string): TokenType {
const keywords: { [key: string]: TokenType } = {
'var': TokenType.VAR,
'const': TokenType.CONST,
'function': TokenType.FUNCTION,
'constraint_type': TokenType.CONSTRAINT_TYPE,
'if': TokenType.IF,
'then': TokenType.THEN,
'else': TokenType.ELSE,
'forall': TokenType.FORALL,
'exists': TokenType.EXISTS,
'in': TokenType.IN,
'assert': TokenType.ASSERT,
'soft': TokenType.SOFT,
'check_sat': TokenType.CHECK_SAT,
'minimize': TokenType.MINIMIZE,
'maximize': TokenType.MAXIMIZE,
'weight': TokenType.WEIGHT,
'Int': TokenType.INT,
'Real': TokenType.REAL,
'Bool': TokenType.BOOL,
'String': TokenType.STRING,
'BitVec': TokenType.BITVEC,
'Array': TokenType.ARRAY,
'Tuple': TokenType.TUPLE,
'Set': TokenType.SET,
'true': TokenType.TRUE,
'false': TokenType.FALSE,
'and': TokenType.AND,
'or': TokenType.OR,
'not': TokenType.NOT,
'implies': TokenType.IMPLIES,
'iff': TokenType.IFF,
'xor': TokenType.XOR,
'div': TokenType.DIV,
};
return keywords[value] || TokenType.IDENTIFIER;
}
private skipWhitespace(): void {
while (!this.isAtEnd()) {
const char = this.peek();
if (char === ' ' || char === '\t' || char === '\r') {
this.advance();
} else if (char === '\n') {
this.line++;
this.column = 0;
this.advance();
} else {
break;
}
}
}
private advance(): string {
const char = this.source[this.position];
this.position++;
this.column++;
return char;
}
private match(expected: string): boolean {
if (this.isAtEnd() || this.peek() !== expected) {
return false;
}
this.advance();
return true;
}
private peek(): string {
if (this.isAtEnd()) return '\0';
return this.source[this.position];
}
private peekNext(): string {
if (this.position + 1 >= this.source.length) return '\0';
return this.source[this.position + 1];
}
private isAtEnd(): boolean {
return this.position >= this.source.length;
}
private isDigit(char: string): boolean {
return char >= '0' && char <= '9';
}
private isAlpha(char: string): boolean {
return (char >= 'a' && char <= 'z') ||
(char >= 'A' && char <= 'Z') ||
char === '_';
}
private isAlphaNumeric(char: string): boolean {
return this.isAlpha(char) || this.isDigit(char);
}
private makeToken(type: TokenType, value: string): Token {
return {
type,
value,
line: this.line,
column: this.column - value.length,
};
}
}
```
## Stage 2: Syntactic Analysis (Parser)
### AST Node Types
```typescript
export type ASTNode =
| ProgramNode
| VarDeclNode
| ConstDeclNode
| FunctionDeclNode
| ConstraintTypeDeclNode
| AssertNode
| SoftConstraintNode
| CheckSatNode
| OptimizeNode
| ExprNode;
export interface ProgramNode {
type: 'Program';
declarations: (VarDeclNode | ConstDeclNode | FunctionDeclNode | ConstraintTypeDeclNode)[];
constraints: (AssertNode | SoftConstraintNode | CheckSatNode | OptimizeNode | ExprNode)[];
}
export interface VarDeclNode {
type: 'VarDecl';
names: string[];
varType: TypeNode;
initializer?: ExprNode;
}
export interface ConstDeclNode {
type: 'ConstDecl';
name: string;
constType: TypeNode;
value: ExprNode;
}
export interface FunctionDeclNode {
type: 'FunctionDecl';
name: string;
params: Array<{ name: string; paramType: TypeNode }>;
returnType: TypeNode;
body: ExprNode;
}
export interface ConstraintTypeDeclNode {
type: 'ConstraintTypeDecl';
name: string;
params: Array<{ name: string; paramType: TypeNode }>;
constraints: ExprNode[];
}
export interface AssertNode {
type: 'Assert';
name?: string;
expr: ExprNode;
}
export interface SoftConstraintNode {
type: 'SoftConstraint';
name?: string;
expr: ExprNode;
weight: number;
}
export interface CheckSatNode {
type: 'CheckSat';
expr: ExprNode;
}
export interface OptimizeNode {
type: 'Optimize';
direction: 'minimize' | 'maximize';
name?: string;
expr: ExprNode;
}
export type ExprNode =
| LiteralNode
| VariableNode
| BinaryExprNode
| UnaryExprNode
| CallExprNode
| IndexExprNode
| IfExprNode
| QuantifiedExprNode
| ArrayLiteralNode
| SetLiteralNode
| TupleLiteralNode;
export interface LiteralNode {
type: 'Literal';
valueType: 'number' | 'string' | 'boolean';
value: number | string | boolean;
}
export interface VariableNode {
type: 'Variable';
name: string;
}
export interface BinaryExprNode {
type: 'BinaryExpr';
operator: BinaryOperator;
left: ExprNode;
right: ExprNode;
}
export type BinaryOperator =
| 'add' | 'subtract' | 'multiply' | 'divide' | 'div' | 'mod' | 'power'
| 'eq' | 'ne' | 'lt' | 'le' | 'gt' | 'ge'
| 'and' | 'or' | 'implies' | 'iff' | 'xor'
| 'bitAnd' | 'bitOr' | 'bitXor' | 'lshift' | 'rshift' | 'arshift';
export interface UnaryExprNode {
type: 'UnaryExpr';
operator: UnaryOperator;
operand: ExprNode;
}
export type UnaryOperator = 'negate' | 'not' | 'bitNot';
export interface CallExprNode {
type: 'CallExpr';
callee: string;
args: ExprNode[];
}
export interface IndexExprNode {
type: 'IndexExpr';
array: ExprNode;
index: ExprNode;
}
export interface IfExprNode {
type: 'IfExpr';
condition: ExprNode;
thenBranch: ExprNode;
elseBranch: ExprNode;
}
export interface QuantifiedExprNode {
type: 'QuantifiedExpr';
quantifier: 'forall' | 'exists';
variable: string;
domain: DomainNode;
body: ExprNode;
}
export type DomainNode =
| { type: 'Range'; start: ExprNode; end: ExprNode; exclusive: boolean }
| { type: 'Set'; elements: ExprNode[] }
| { type: 'Variable'; name: string };
export interface ArrayLiteralNode {
type: 'ArrayLiteral';
elements: ExprNode[];
}
export interface SetLiteralNode {
type: 'SetLiteral';
elements: ExprNode[];
}
export interface TupleLiteralNode {
type: 'TupleLiteral';
elements: ExprNode[];
}
export interface TypeNode {
type: 'Type';
name: 'Int' | 'Real' | 'Bool' | 'String' | 'BitVec' | 'Array' | 'Tuple' | 'Set' | string;
params?: TypeNode[];
size?: number; // For BitVec[n]
}
```
### Parser Implementation
```typescript
export class Parser {
private tokens: Token[];
private current: number = 0;
constructor(tokens: Token[]) {
this.tokens = tokens.filter(t => t.type !== TokenType.COMMENT);
}
/**
* Parse the token stream into an AST
*/
public parse(): ProgramNode {
const declarations: any[] = [];
const constraints: any[] = [];
while (!this.isAtEnd()) {
if (this.check(TokenType.VAR) || this.check(TokenType.CONST) ||
this.check(TokenType.FUNCTION) || this.check(TokenType.CONSTRAINT_TYPE)) {
declarations.push(this.parseDeclaration());
} else {
constraints.push(this.parseConstraint());
}
}
return {
type: 'Program',
declarations,
constraints,
};
}
private parseDeclaration(): ASTNode {
if (this.match(TokenType.VAR)) {
return this.parseVarDecl();
}
if (this.match(TokenType.CONST)) {
return this.parseConstDecl();
}
if (this.match(TokenType.FUNCTION)) {
return this.parseFunctionDecl();
}
if (this.match(TokenType.CONSTRAINT_TYPE)) {
return this.parseConstraintTypeDecl();
}
throw this.error('Expected declaration');
}
private parseVarDecl(): VarDeclNode {
const names: string[] = [];
names.push(this.consume(TokenType.IDENTIFIER, 'Expected variable name').value);
while (this.match(TokenType.COMMA)) {
names.push(this.consume(TokenType.IDENTIFIER, 'Expected variable name').value);
}
this.consume(TokenType.COLON, "Expected ':' after variable name(s)");
const varType = this.parseType();
let initializer: ExprNode | undefined;
if (this.match(TokenType.ASSIGN)) {
initializer = this.parseExpression();
}
return {
type: 'VarDecl',
names,
varType,
initializer,
};
}
private parseConstraint(): ASTNode {
if (this.match(TokenType.ASSERT)) {
let name: string | undefined;
if (this.check(TokenType.COLON)) {
this.advance();
name = this.consume(TokenType.IDENTIFIER, 'Expected constraint name').value;
this.consume(TokenType.COLON, "Expected ':' after constraint name");
}
const expr = this.parseExpression();
return { type: 'Assert', name, expr };
}
if (this.match(TokenType.SOFT)) {
let name: string | undefined;
if (this.check(TokenType.COLON)) {
this.advance();
name = this.consume(TokenType.IDENTIFIER, 'Expected constraint name').value;
this.consume(TokenType.COLON, "Expected ':' after constraint name");
}
const expr = this.parseExpression();
let weight = 1;
if (this.match(TokenType.WEIGHT)) {
weight = parseFloat(this.consume(TokenType.NUMBER, 'Expected weight value').value);
}
return { type: 'SoftConstraint', name, expr, weight };
}
if (this.match(TokenType.CHECK_SAT)) {
this.consume(TokenType.COLON, "Expected ':' after check_sat");
const expr = this.parseExpression();
return { type: 'CheckSat', expr };
}
if (this.match(TokenType.MINIMIZE) || this.match(TokenType.MAXIMIZE)) {
const direction = this.previous().type === TokenType.MINIMIZE ? 'minimize' : 'maximize';
let name: string | undefined;
if (this.check(TokenType.COLON)) {
this.advance();
if (this.check(TokenType.IDENTIFIER) && this.peek().type === TokenType.COLON) {
name = this.advance().value;
this.advance();
}
} else {
this.consume(TokenType.COLON, "Expected ':' after optimization directive");
}
const expr = this.parseExpression();
return { type: 'Optimize', direction, name, expr };
}
// Default: just an expression constraint
return this.parseExpression();
}
private parseExpression(): ExprNode {
return this.parseIffExpression();
}
private parseIffExpression(): ExprNode {
let expr = this.parseImpliesExpression();
while (this.match(TokenType.IFF)) {
const operator = 'iff';
const right = this.parseImpliesExpression();
expr = { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parseImpliesExpression(): ExprNode {
let expr = this.parseOrExpression();
while (this.match(TokenType.IMPLIES)) {
const operator = 'implies';
const right = this.parseOrExpression();
expr = { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parseOrExpression(): ExprNode {
let expr = this.parseXorExpression();
while (this.match(TokenType.OR)) {
const operator = 'or';
const right = this.parseXorExpression();
expr = { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parseXorExpression(): ExprNode {
let expr = this.parseAndExpression();
while (this.match(TokenType.XOR)) {
const operator = 'xor';
const right = this.parseAndExpression();
expr = { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parseAndExpression(): ExprNode {
let expr = this.parseComparisonExpression();
while (this.match(TokenType.AND)) {
const operator = 'and';
const right = this.parseComparisonExpression();
expr = { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parseComparisonExpression(): ExprNode {
let expr = this.parseBitwiseOrExpression();
if (this.match(TokenType.EQ, TokenType.NE, TokenType.LT, TokenType.LE, TokenType.GT, TokenType.GE)) {
const tokenType = this.previous().type;
const operator = this.tokenTypeToOperator(tokenType);
const right = this.parseBitwiseOrExpression();
return { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parseBitwiseOrExpression(): ExprNode {
let expr = this.parseBitwiseXorExpression();
while (this.match(TokenType.BIT_OR)) {
const operator = 'bitOr';
const right = this.parseBitwiseXorExpression();
expr = { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parseBitwiseXorExpression(): ExprNode {
let expr = this.parseBitwiseAndExpression();
while (this.match(TokenType.BIT_XOR)) {
const operator = 'bitXor';
const right = this.parseBitwiseAndExpression();
expr = { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parseBitwiseAndExpression(): ExprNode {
let expr = this.parseShiftExpression();
while (this.match(TokenType.BIT_AND)) {
const operator = 'bitAnd';
const right = this.parseShiftExpression();
expr = { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parseShiftExpression(): ExprNode {
let expr = this.parseAdditiveExpression();
while (this.match(TokenType.LSHIFT, TokenType.RSHIFT, TokenType.ARSHIFT)) {
const tokenType = this.previous().type;
const operator = tokenType === TokenType.LSHIFT ? 'lshift' :
tokenType === TokenType.RSHIFT ? 'rshift' : 'arshift';
const right = this.parseAdditiveExpression();
expr = { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parseAdditiveExpression(): ExprNode {
let expr = this.parseMultiplicativeExpression();
while (this.match(TokenType.PLUS, TokenType.MINUS)) {
const operator = this.previous().type === TokenType.PLUS ? 'add' : 'subtract';
const right = this.parseMultiplicativeExpression();
expr = { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parseMultiplicativeExpression(): ExprNode {
let expr = this.parsePowerExpression();
while (this.match(TokenType.STAR, TokenType.SLASH, TokenType.DIV, TokenType.PERCENT)) {
const tokenType = this.previous().type;
const operator = tokenType === TokenType.STAR ? 'multiply' :
tokenType === TokenType.SLASH ? 'divide' :
tokenType === TokenType.DIV ? 'div' : 'mod';
const right = this.parsePowerExpression();
expr = { type: 'BinaryExpr', operator, left: expr, right };
}
return expr;
}
private parsePowerExpression(): ExprNode {
let expr = this.parseUnaryExpression();
if (this.match(TokenType.POWER)) {
const right = this.parsePowerExpression(); // Right associative
expr = { type: 'BinaryExpr', operator: 'power', left: expr, right };
}
return expr;
}
private parseUnaryExpression(): ExprNode {
if (this.match(TokenType.NOT)) {
const operand = this.parseUnaryExpression();
return { type: 'UnaryExpr', operator: 'not', operand };
}
if (this.match(TokenType.MINUS)) {
const operand = this.parseUnaryExpression();
return { type: 'UnaryExpr', operator: 'negate', operand };
}
if (this.match(TokenType.BIT_NOT)) {
const operand = this.parseUnaryExpression();
return { type: 'UnaryExpr', operator: 'bitNot', operand };
}
return this.parsePostfixExpression();
}
private parsePostfixExpression(): ExprNode {
let expr = this.parsePrimaryExpression();
while (true) {
if (this.match(TokenType.LPAREN)) {
// Function call
const args: ExprNode[] = [];
if (!this.check(TokenType.RPAREN)) {
do {
args.push(this.parseExpression());
} while (this.match(TokenType.COMMA));
}
this.consume(TokenType.RPAREN, "Expected ')' after arguments");
if (expr.type !== 'Variable') {
throw this.error('Can only call named functions');
}
expr = { type: 'CallExpr', callee: expr.name, args };
} else if (this.match(TokenType.LBRACKET)) {
// Array indexing
const index = this.parseExpression();
this.consume(TokenType.RBRACKET, "Expected ']' after index");
expr = { type: 'IndexExpr', array: expr, index };
} else {
break;
}
}
return expr;
}
private parsePrimaryExpression(): ExprNode {
// Literals
if (this.match(TokenType.NUMBER)) {
const value = parseFloat(this.previous().value);
return { type: 'Literal', valueType: 'number', value };
}
if (this.match(TokenType.STRING_LITERAL)) {
const value = this.previous().value;
return { type: 'Literal', valueType: 'string', value };
}
if (this.match(TokenType.TRUE, TokenType.FALSE)) {
const value = this.previous().type === TokenType.TRUE;
return { type: 'Literal', valueType: 'boolean', value };
}
// Variables and function calls
if (this.match(TokenType.IDENTIFIER)) {
const name = this.previous().value;
return { type: 'Variable', name };
}
// Quantified expressions
if (this.match(TokenType.FORALL, TokenType.EXISTS)) {
const quantifier = this.previous().type === TokenType.FORALL ? 'forall' : 'exists';
const variable = this.consume(TokenType.IDENTIFIER, 'Expected variable name').value;
this.consume(TokenType.IN, "Expected 'in' after variable");
const domain = this.parseDomain();
this.consume(TokenType.COLON, "Expected ':' before quantified body");
const body = this.parseExpression();
return { type: 'QuantifiedExpr', quantifier, variable, domain, body };
}
// If expression
if (this.match(TokenType.IF)) {
const condition = this.parseExpression();
this.consume(TokenType.THEN, "Expected 'then' after if condition");
const thenBranch = this.parseExpression();
this.consume(TokenType.ELSE, "Expected 'else' after then branch");
const elseBranch = this.parseExpression();
return { type: 'IfExpr', condition, thenBranch, elseBranch };
}
// Parenthesized expression
if (this.match(TokenType.LPAREN)) {
const expr = this.parseExpression();
this.consume(TokenType.RPAREN, "Expected ')' after expression");
return expr;
}
// Array literal
if (this.match(TokenType.LBRACKET)) {
const elements: ExprNode[] = [];
if (!this.check(TokenType.RBRACKET)) {
do {
elements.push(this.parseExpression());
} while (this.match(TokenType.COMMA));
}
this.consume(TokenType.RBRACKET, "Expected ']' after array elements");
return { type: 'ArrayLiteral', elements };
}
// Set literal
if (this.match(TokenType.LBRACE)) {
const elements: ExprNode[] = [];
if (!this.check(TokenType.RBRACE)) {
do {
elements.push(this.parseExpression());
} while (this.match(TokenType.COMMA));
}
this.consume(TokenType.RBRACE, "Expected '}' after set elements");
return { type: 'SetLiteral', elements };
}
throw this.error('Expected expression');
}
private parseDomain(): DomainNode {
const start = this.parseExpression();
if (this.match(TokenType.DOTDOT)) {
const end = this.parseExpression();
return { type: 'Range', start, end, exclusive: false };
}
if (this.match(TokenType.DOTDOTLT)) {
const end = this.parseExpression();
return { type: 'Range', start, end, exclusive: true };
}
// Array or set
if (start.type === 'Variable') {
return { type: 'Variable', name: start.name };
}
if (start.type === 'ArrayLiteral' || start.type === 'SetLiteral') {
return { type: 'Set', elements: start.elements };
}
throw this.error('Expected range or set in domain');
}
private parseType(): TypeNode {
if (this.match(TokenType.INT)) {
return { type: 'Type', name: 'Int' };
}
if (this.match(TokenType.REAL)) {
return { type: 'Type', name: 'Real' };
}
if (this.match(TokenType.BOOL)) {
return { type: 'Type', name: 'Bool' };
}
if (this.match(TokenType.STRING)) {
return { type: 'Type', name: 'String' };
}
if (this.match(TokenType.BITVEC)) {
this.consume(TokenType.LBRACKET, "Expected '[' after BitVec");
const size = parseInt(this.consume(TokenType.NUMBER, 'Expected bit width').value);
this.consume(TokenType.RBRACKET, "Expected ']' after bit width");
return { type: 'Type', name: 'BitVec', size };
}
if (this.match(TokenType.ARRAY, TokenType.TUPLE, TokenType.SET)) {
const name = this.previous().value as any;
this.consume(TokenType.LBRACKET, `Expected '[' after ${name}`);
const params: TypeNode[] = [];
do {
params.push(this.parseType());
} while (this.match(TokenType.COMMA));
this.consume(TokenType.RBRACKET, `Expected ']' after ${name} type parameters`);
return { type: 'Type', name, params };
}
// User-defined types
if (this.match(TokenType.IDENTIFIER)) {
return { type: 'Type', name: this.previous().value };
}
throw this.error('Expected type');
}
private tokenTypeToOperator(tokenType: TokenType): BinaryOperator {
switch (tokenType) {
case TokenType.EQ: return 'eq';
case TokenType.NE: return 'ne';
case TokenType.LT: return 'lt';
case TokenType.LE: return 'le';
case TokenType.GT: return 'gt';
case TokenType.GE: return 'ge';
default: throw this.error(`Unexpected token type: ${tokenType}`);
}
}
private match(...types: TokenType[]): boolean {
for (const type of types) {
if (this.check(type)) {
this.advance();
return true;
}
}
return false;
}
private check(type: TokenType): boolean {
if (this.isAtEnd()) return false;
return this.peek().type === type;
}
private advance(): Token {
if (!this.isAtEnd()) this.current++;
return this.previous();
}
private isAtEnd(): boolean {
return this.peek().type === TokenType.EOF;
}
private peek(): Token {
return this.tokens[this.current];
}
private previous(): Token {
return this.tokens[this.current - 1];
}
private consume(type: TokenType, message: string): Token {
if (this.check(type)) return this.advance();
throw this.error(message);
}
private error(message: string): Error {
const token = this.peek();
return new Error(`Parse error at line ${token.line}, column ${token.column}: ${message}`);
}
}
```
## Stage 3: Type Checking
The type checker validates the AST and annotates it with type information. This is covered in the next document section...
(Continued in next file due to length)
