/**
* Parser for the Constraint Specification DSL
*
* Implements a recursive descent parser that transforms tokens into an AST.
* Uses precedence climbing for expression parsing.
*/
import { Token, TokenType } from './constraintLexer.js';
import {
ProgramNode,
DeclarationNode,
ConstraintNode,
ExprNode,
VarDeclNode,
ConstDeclNode,
FunctionDeclNode,
ConstraintTypeDeclNode,
AssertNode,
SoftConstraintNode,
CheckSatNode,
OptimizeNode,
LiteralNode,
VariableNode,
BinaryExprNode,
BinaryOperator,
UnaryExprNode,
UnaryOperator,
CallExprNode,
IndexExprNode,
IfExprNode,
QuantifiedExprNode,
ArrayLiteralNode,
SetLiteralNode,
TupleLiteralNode,
ArrayComprehensionNode,
SetComprehensionNode,
LambdaExprNode,
MemberAccessNode,
DomainNode,
TypeNode,
createLocation,
} from './constraintAST.js';
// ============================================================================
// Parser Class
// ============================================================================
export class Parser {
private tokens: Token[];
private current: number = 0;
constructor(tokens: Token[]) {
// Filter out comments but keep all other tokens
this.tokens = tokens.filter(t => t.type !== TokenType.COMMENT);
}
/**
* Parse the token stream into an AST
*/
public parse(): ProgramNode {
const declarations: DeclarationNode[] = [];
const constraints: ConstraintNode[] = [];
while (!this.isAtEnd()) {
if (this.isDeclaration()) {
declarations.push(this.parseDeclaration());
} else {
constraints.push(this.parseConstraint());
}
}
return {
type: 'Program',
declarations,
constraints,
location: createLocation(1, 1),
};
}
// ==========================================================================
// Declaration Parsing
// ==========================================================================
private isDeclaration(): boolean {
return this.check(TokenType.VAR) ||
this.check(TokenType.CONST) ||
this.check(TokenType.FUNCTION) ||
this.check(TokenType.CONSTRAINT_TYPE);
}
private parseDeclaration(): DeclarationNode {
const token = this.peek();
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', token);
}
private parseVarDecl(): VarDeclNode {
const startToken = this.previous();
const names: string[] = [];
// Parse variable names
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();
}
let whereClause: ExprNode | undefined;
if (this.match(TokenType.WHERE)) {
whereClause = this.parseExpression();
}
return {
type: 'VarDecl',
names,
varType,
initializer,
whereClause,
location: createLocation(startToken.line, startToken.column),
};
}
private parseConstDecl(): ConstDeclNode {
const startToken = this.previous();
const name = this.consume(TokenType.IDENTIFIER, 'Expected constant name').value;
this.consume(TokenType.COLON, "Expected ':' after constant name");
const constType = this.parseType();
this.consume(TokenType.ASSIGN, "Expected '=' after constant type");
const value = this.parseExpression();
return {
type: 'ConstDecl',
name,
constType,
value,
location: createLocation(startToken.line, startToken.column),
};
}
private parseFunctionDecl(): FunctionDeclNode {
const startToken = this.previous();
const name = this.consume(TokenType.IDENTIFIER, 'Expected function name').value;
this.consume(TokenType.LPAREN, "Expected '(' after function name");
const params: Array<{ name: string; paramType: TypeNode }> = [];
if (!this.check(TokenType.RPAREN)) {
do {
const paramName = this.consume(TokenType.IDENTIFIER, 'Expected parameter name').value;
this.consume(TokenType.COLON, "Expected ':' after parameter name");
const paramType = this.parseType();
params.push({ name: paramName, paramType });
} while (this.match(TokenType.COMMA));
}
this.consume(TokenType.RPAREN, "Expected ')' after parameters");
this.consume(TokenType.ARROW, "Expected '->' before return type");
const returnType = this.parseType();
this.consume(TokenType.COLON, "Expected ':' before function body");
const body = this.parseExpression();
return {
type: 'FunctionDecl',
name,
params,
returnType,
body,
location: createLocation(startToken.line, startToken.column),
};
}
private parseConstraintTypeDecl(): ConstraintTypeDeclNode {
const startToken = this.previous();
const name = this.consume(TokenType.IDENTIFIER, 'Expected constraint type name').value;
this.consume(TokenType.LPAREN, "Expected '(' after constraint type name");
const params: Array<{ name: string; paramType: TypeNode }> = [];
if (!this.check(TokenType.RPAREN)) {
do {
const paramName = this.consume(TokenType.IDENTIFIER, 'Expected parameter name').value;
this.consume(TokenType.COLON, "Expected ':' after parameter name");
const paramType = this.parseType();
params.push({ name: paramName, paramType });
} while (this.match(TokenType.COMMA));
}
this.consume(TokenType.RPAREN, "Expected ')' after parameters");
this.consume(TokenType.COLON, "Expected ':' before constraint body");
const constraints: ExprNode[] = [];
// Parse constraints until next declaration or EOF
while (!this.isAtEnd() && !this.isDeclaration()) {
constraints.push(this.parseExpression());
}
return {
type: 'ConstraintTypeDecl',
name,
params,
constraints,
location: createLocation(startToken.line, startToken.column),
};
}
// ==========================================================================
// Constraint Parsing
// ==========================================================================
private parseConstraint(): ConstraintNode {
// Named constraints: assert/soft/check_sat/minimize/maximize
if (this.match(TokenType.ASSERT)) {
return this.parseAssert();
}
if (this.match(TokenType.SOFT)) {
return this.parseSoftConstraint();
}
if (this.match(TokenType.CHECK_SAT)) {
return this.parseCheckSat();
}
if (this.match(TokenType.MINIMIZE) || this.match(TokenType.MAXIMIZE)) {
return this.parseOptimize();
}
// Default: expression constraint
return this.parseExpression();
}
private parseAssert(): AssertNode {
const startToken = this.previous();
let name: string | undefined;
// Optional name: assert name: expr or assert: expr
if (this.check(TokenType.IDENTIFIER)) {
const saved = this.current;
const identifier = this.advance().value;
if (this.match(TokenType.COLON)) {
name = identifier;
} else {
// Not a name, backtrack
this.current = saved;
}
}
if (!name && this.check(TokenType.COLON)) {
this.advance(); // Consume unnamed colon
}
const expr = this.parseExpression();
return {
type: 'Assert',
name,
expr,
location: createLocation(startToken.line, startToken.column),
};
}
private parseSoftConstraint(): SoftConstraintNode {
const startToken = this.previous();
let name: string | undefined;
// Optional name
if (this.check(TokenType.IDENTIFIER)) {
const saved = this.current;
const identifier = this.advance().value;
if (this.match(TokenType.COLON)) {
name = identifier;
} else {
this.current = saved;
}
}
if (!name && this.check(TokenType.COLON)) {
this.advance();
}
const expr = this.parseExpression();
let weight = 1;
if (this.match(TokenType.WEIGHT)) {
const weightToken = this.consume(TokenType.NUMBER, 'Expected weight value');
weight = parseFloat(weightToken.value);
}
return {
type: 'SoftConstraint',
name,
expr,
weight,
location: createLocation(startToken.line, startToken.column),
};
}
private parseCheckSat(): CheckSatNode {
const startToken = this.previous();
let expr: ExprNode;
if (this.check(TokenType.COLON)) {
this.advance();
expr = this.parseExpression();
} else {
// check_sat without expression means check all assertions
expr = {
type: 'Literal',
valueType: 'boolean',
value: true,
location: createLocation(startToken.line, startToken.column),
};
}
return {
type: 'CheckSat',
expr,
location: createLocation(startToken.line, startToken.column),
};
}
private parseOptimize(): OptimizeNode {
const directionToken = this.previous();
const direction = directionToken.type === TokenType.MINIMIZE ? 'minimize' : 'maximize';
let name: string | undefined;
// Optional name
if (this.check(TokenType.IDENTIFIER)) {
const saved = this.current;
const identifier = this.advance().value;
if (this.match(TokenType.COLON)) {
name = identifier;
} else {
this.current = saved;
}
}
if (!name && this.check(TokenType.COLON)) {
this.advance();
}
const expr = this.parseExpression();
return {
type: 'Optimize',
direction,
name,
expr,
location: createLocation(directionToken.line, directionToken.column),
};
}
// ==========================================================================
// Expression Parsing (Precedence Climbing)
// ==========================================================================
private parseExpression(): ExprNode {
return this.parseIffExpression();
}
private parseIffExpression(): ExprNode {
let expr = this.parseImpliesExpression();
while (this.match(TokenType.IFF)) {
const opToken = this.previous();
const right = this.parseImpliesExpression();
expr = {
type: 'BinaryExpr',
operator: 'iff',
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseImpliesExpression(): ExprNode {
let expr = this.parseOrExpression();
while (this.match(TokenType.IMPLIES)) {
const opToken = this.previous();
const right = this.parseOrExpression();
expr = {
type: 'BinaryExpr',
operator: 'implies',
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseOrExpression(): ExprNode {
let expr = this.parseXorExpression();
while (this.match(TokenType.OR)) {
const opToken = this.previous();
const right = this.parseXorExpression();
expr = {
type: 'BinaryExpr',
operator: 'or',
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseXorExpression(): ExprNode {
let expr = this.parseAndExpression();
while (this.match(TokenType.XOR)) {
const opToken = this.previous();
const right = this.parseAndExpression();
expr = {
type: 'BinaryExpr',
operator: 'xor',
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseAndExpression(): ExprNode {
let expr = this.parseComparisonExpression();
while (this.match(TokenType.AND)) {
const opToken = this.previous();
const right = this.parseComparisonExpression();
expr = {
type: 'BinaryExpr',
operator: 'and',
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseComparisonExpression(): ExprNode {
let expr = this.parseInExpression();
if (this.match(TokenType.EQ, TokenType.NE, TokenType.LT, TokenType.LE, TokenType.GT, TokenType.GE)) {
const opToken = this.previous();
const operator = this.tokenTypeToOperator(opToken.type);
const right = this.parseInExpression();
return {
type: 'BinaryExpr',
operator,
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseInExpression(): ExprNode {
let expr = this.parseBitwiseOrExpression();
if (this.match(TokenType.IN)) {
const opToken = this.previous();
const right = this.parseBitwiseOrExpression();
expr = {
type: 'BinaryExpr',
operator: 'in',
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
} else if (this.match(TokenType.CONTAINS)) {
const opToken = this.previous();
const right = this.parseBitwiseOrExpression();
expr = {
type: 'BinaryExpr',
operator: 'contains',
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseBitwiseOrExpression(): ExprNode {
let expr = this.parseBitwiseXorExpression();
while (this.check(TokenType.BIT_OR) && !this.check(TokenType.PIPE)) {
this.advance();
const opToken = this.previous();
const right = this.parseBitwiseXorExpression();
expr = {
type: 'BinaryExpr',
operator: 'bitOr',
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseBitwiseXorExpression(): ExprNode {
let expr = this.parseBitwiseAndExpression();
while (this.match(TokenType.BIT_XOR)) {
const opToken = this.previous();
const right = this.parseBitwiseAndExpression();
expr = {
type: 'BinaryExpr',
operator: 'bitXor',
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseBitwiseAndExpression(): ExprNode {
let expr = this.parseShiftExpression();
while (this.match(TokenType.BIT_AND)) {
const opToken = this.previous();
const right = this.parseShiftExpression();
expr = {
type: 'BinaryExpr',
operator: 'bitAnd',
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseShiftExpression(): ExprNode {
let expr = this.parseAdditiveExpression();
while (this.match(TokenType.LSHIFT, TokenType.RSHIFT, TokenType.ARSHIFT)) {
const opToken = this.previous();
const operator = opToken.type === TokenType.LSHIFT ? 'lshift' :
opToken.type === TokenType.RSHIFT ? 'rshift' : 'arshift';
const right = this.parseAdditiveExpression();
expr = {
type: 'BinaryExpr',
operator,
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseAdditiveExpression(): ExprNode {
let expr = this.parseMultiplicativeExpression();
while (this.match(TokenType.PLUS, TokenType.MINUS)) {
const opToken = this.previous();
const operator = opToken.type === TokenType.PLUS ? 'add' : 'subtract';
const right = this.parseMultiplicativeExpression();
expr = {
type: 'BinaryExpr',
operator,
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseMultiplicativeExpression(): ExprNode {
let expr = this.parsePowerExpression();
while (this.match(TokenType.STAR, TokenType.SLASH, TokenType.DIV, TokenType.PERCENT)) {
const opToken = this.previous();
const operator = opToken.type === TokenType.STAR ? 'multiply' :
opToken.type === TokenType.SLASH ? 'divide' :
opToken.type === TokenType.DIV ? 'div' : 'mod';
const right = this.parsePowerExpression();
expr = {
type: 'BinaryExpr',
operator,
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parsePowerExpression(): ExprNode {
let expr = this.parseUnaryExpression();
if (this.match(TokenType.POWER)) {
const opToken = this.previous();
const right = this.parsePowerExpression(); // Right associative
expr = {
type: 'BinaryExpr',
operator: 'power',
left: expr,
right,
location: createLocation(opToken.line, opToken.column),
};
}
return expr;
}
private parseUnaryExpression(): ExprNode {
if (this.match(TokenType.NOT)) {
const opToken = this.previous();
const operand = this.parseUnaryExpression();
return {
type: 'UnaryExpr',
operator: 'not',
operand,
location: createLocation(opToken.line, opToken.column),
};
}
if (this.match(TokenType.MINUS)) {
const opToken = this.previous();
const operand = this.parseUnaryExpression();
return {
type: 'UnaryExpr',
operator: 'negate',
operand,
location: createLocation(opToken.line, opToken.column),
};
}
if (this.match(TokenType.BIT_NOT)) {
const opToken = this.previous();
const operand = this.parseUnaryExpression();
return {
type: 'UnaryExpr',
operator: 'bitNot',
operand,
location: createLocation(opToken.line, opToken.column),
};
}
// Unary plus is a no-op
if (this.match(TokenType.PLUS)) {
return this.parseUnaryExpression();
}
return this.parsePostfixExpression();
}
private parsePostfixExpression(): ExprNode {
let expr = this.parsePrimaryExpression();
while (true) {
if (this.match(TokenType.LPAREN)) {
// Function call
expr = this.parseCallExpr(expr);
} else if (this.match(TokenType.LBRACKET)) {
// Array indexing or slice
expr = this.parseIndexExpr(expr);
} else if (this.match(TokenType.DOT)) {
// Member access
expr = this.parseMemberAccess(expr);
} else {
break;
}
}
return expr;
}
private parseCallExpr(callee: ExprNode): CallExprNode {
const startToken = this.previous();
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 (callee.type !== 'Variable') {
throw this.error('Can only call named functions', this.previous());
}
return {
type: 'CallExpr',
callee: callee.name,
args,
location: createLocation(startToken.line, startToken.column),
};
}
private parseIndexExpr(array: ExprNode): IndexExprNode {
const startToken = this.previous();
const index = this.parseExpression();
this.consume(TokenType.RBRACKET, "Expected ']' after index");
return {
type: 'IndexExpr',
array,
index,
location: createLocation(startToken.line, startToken.column),
};
}
private parseMemberAccess(object: ExprNode): MemberAccessNode {
const startToken = this.previous();
const member = this.consume(TokenType.IDENTIFIER, 'Expected member name').value;
return {
type: 'MemberAccess',
object,
member,
location: createLocation(startToken.line, startToken.column),
};
}
private parsePrimaryExpression(): ExprNode {
const token = this.peek();
const location = createLocation(token.line, token.column);
// Literals
if (this.match(TokenType.NUMBER)) {
const value = parseFloat(this.previous().value);
return {
type: 'Literal',
valueType: 'number',
value,
location,
};
}
if (this.match(TokenType.STRING_LITERAL)) {
const value = this.previous().value;
return {
type: 'Literal',
valueType: 'string',
value,
location,
};
}
if (this.match(TokenType.TRUE, TokenType.FALSE)) {
const value = this.previous().type === TokenType.TRUE;
return {
type: 'Literal',
valueType: 'boolean',
value,
location,
};
}
// Identifiers (variables)
if (this.match(TokenType.IDENTIFIER)) {
const name = this.previous().value;
return {
type: 'Variable',
name,
location,
};
}
// Quantified expressions
if (this.match(TokenType.FORALL, TokenType.EXISTS)) {
return this.parseQuantifiedExpr();
}
// If expressions
if (this.match(TokenType.IF)) {
return this.parseIfExpr();
}
// Lambda expressions
if (this.match(TokenType.LAMBDA)) {
return this.parseLambdaExpr();
}
// Parenthesized expressions
if (this.match(TokenType.LPAREN)) {
const expr = this.parseExpression();
this.consume(TokenType.RPAREN, "Expected ')' after expression");
return expr;
}
// Array literals
if (this.match(TokenType.LBRACKET)) {
return this.parseArrayLiteral();
}
// Set literals
if (this.match(TokenType.LBRACE)) {
return this.parseSetLiteral();
}
throw this.error('Expected expression', token);
}
private parseQuantifiedExpr(): QuantifiedExprNode {
const quantToken = this.previous();
const startToken = quantToken;
const quantifier = quantToken.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,
location: createLocation(startToken.line, startToken.column),
};
}
private parseIfExpr(): IfExprNode {
const startToken = this.previous();
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,
location: createLocation(startToken.line, startToken.column),
};
}
private parseLambdaExpr(): LambdaExprNode {
const startToken = this.previous();
const param = this.consume(TokenType.IDENTIFIER, 'Expected parameter name').value;
this.consume(TokenType.COLON, "Expected ':' after lambda parameter");
const body = this.parseExpression();
return {
type: 'LambdaExpr',
param,
body,
location: createLocation(startToken.line, startToken.column),
};
}
private parseArrayLiteral(): ArrayLiteralNode | ArrayComprehensionNode {
const startToken = this.previous();
const elements: ExprNode[] = [];
if (this.check(TokenType.RBRACKET)) {
this.advance();
return {
type: 'ArrayLiteral',
elements: [],
location: createLocation(startToken.line, startToken.column),
};
}
// Try to parse as comprehension
const saved = this.current;
try {
const element = this.parseExpression();
if (this.match(TokenType.FOR)) {
// Array comprehension
const variable = this.consume(TokenType.IDENTIFIER, 'Expected variable name').value;
this.consume(TokenType.IN, "Expected 'in' after variable");
const domain = this.parseDomain();
let condition: ExprNode | undefined;
if (this.match(TokenType.IF)) {
condition = this.parseExpression();
}
this.consume(TokenType.RBRACKET, "Expected ']' after array comprehension");
return {
type: 'ArrayComprehension',
element,
variable,
domain,
condition,
location: createLocation(startToken.line, startToken.column),
};
} else {
// Regular array literal
elements.push(element);
while (this.match(TokenType.COMMA)) {
elements.push(this.parseExpression());
}
this.consume(TokenType.RBRACKET, "Expected ']' after array elements");
return {
type: 'ArrayLiteral',
elements,
location: createLocation(startToken.line, startToken.column),
};
}
} catch (e) {
// Backtrack and try regular array literal
this.current = saved;
do {
elements.push(this.parseExpression());
} while (this.match(TokenType.COMMA));
this.consume(TokenType.RBRACKET, "Expected ']' after array elements");
return {
type: 'ArrayLiteral',
elements,
location: createLocation(startToken.line, startToken.column),
};
}
}
private parseSetLiteral(): SetLiteralNode | SetComprehensionNode {
const startToken = this.previous();
const elements: ExprNode[] = [];
if (this.check(TokenType.RBRACE)) {
this.advance();
return {
type: 'SetLiteral',
elements: [],
location: createLocation(startToken.line, startToken.column),
};
}
// Try to parse as comprehension
const saved = this.current;
try {
const element = this.parseExpression();
if (this.match(TokenType.FOR)) {
// Set comprehension
const variable = this.consume(TokenType.IDENTIFIER, 'Expected variable name').value;
this.consume(TokenType.IN, "Expected 'in' after variable");
const domain = this.parseDomain();
let condition: ExprNode | undefined;
if (this.match(TokenType.IF)) {
condition = this.parseExpression();
}
this.consume(TokenType.RBRACE, "Expected '}' after set comprehension");
return {
type: 'SetComprehension',
element,
variable,
domain,
condition,
location: createLocation(startToken.line, startToken.column),
};
} else {
// Regular set literal
elements.push(element);
while (this.match(TokenType.COMMA)) {
elements.push(this.parseExpression());
}
this.consume(TokenType.RBRACE, "Expected '}' after set elements");
return {
type: 'SetLiteral',
elements,
location: createLocation(startToken.line, startToken.column),
};
}
} catch (e) {
// Backtrack and try regular set literal
this.current = saved;
do {
elements.push(this.parseExpression());
} while (this.match(TokenType.COMMA));
this.consume(TokenType.RBRACE, "Expected '}' after set elements");
return {
type: 'SetLiteral',
elements,
location: createLocation(startToken.line, startToken.column),
};
}
}
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 };
}
// Variable or set domain
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', this.previous());
}
// ==========================================================================
// Type Parsing
// ==========================================================================
private parseType(): TypeNode {
const token = this.peek();
const location = createLocation(token.line, token.column);
if (this.match(TokenType.INT)) {
return { type: 'Type', name: 'Int', location };
}
if (this.match(TokenType.REAL)) {
return { type: 'Type', name: 'Real', location };
}
if (this.match(TokenType.BOOL)) {
return { type: 'Type', name: 'Bool', location };
}
if (this.match(TokenType.STRING)) {
return { type: 'Type', name: 'String', location };
}
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, location };
}
if (this.match(TokenType.ARRAY, TokenType.TUPLE, TokenType.SET, TokenType.MAP)) {
const typeName = this.previous().value as any;
this.consume(TokenType.LBRACKET, `Expected '[' after ${typeName}`);
const params: TypeNode[] = [];
do {
params.push(this.parseType());
} while (this.match(TokenType.COMMA));
this.consume(TokenType.RBRACKET, `Expected ']' after ${typeName} type parameters`);
return { type: 'Type', name: typeName, params, location };
}
// User-defined types
if (this.match(TokenType.IDENTIFIER)) {
const name = this.previous().value;
return { type: 'Type', name, location };
}
throw this.error('Expected type', token);
}
// ==========================================================================
// Helper Methods
// ==========================================================================
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}`, this.peek());
}
}
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, this.peek());
}
private error(message: string, token: Token): Error {
return new Error(
`Parse error at line ${token.line}, column ${token.column}: ${message}\n` +
` Token: ${token.type} "${token.value}"`
);
}
}
// ============================================================================
// Utility Functions
// ============================================================================
/**
* Parse CSDL source code into an AST
*/
export function parse(tokens: Token[]): ProgramNode {
const parser = new Parser(tokens);
return parser.parse();
}
