/**
* Abstract Syntax Tree (AST) node definitions for the Constraint Specification DSL
*
* This module defines all AST node types used to represent parsed CSDL programs.
* The AST supports visitor pattern for traversal and analysis.
*/
// ============================================================================
// AST Node Base Types
// ============================================================================
export interface ASTNodeBase {
type: string;
location?: SourceLocation;
}
export interface SourceLocation {
line: number;
column: number;
length?: number;
}
// ============================================================================
// Program Structure
// ============================================================================
export interface ProgramNode extends ASTNodeBase {
type: 'Program';
declarations: DeclarationNode[];
constraints: ConstraintNode[];
}
// ============================================================================
// Declarations
// ============================================================================
export type DeclarationNode =
| VarDeclNode
| ConstDeclNode
| FunctionDeclNode
| ConstraintTypeDeclNode;
export interface VarDeclNode extends ASTNodeBase {
type: 'VarDecl';
names: string[];
varType: TypeNode;
initializer?: ExprNode;
whereClause?: ExprNode; // For constrained variables: var x: Int where x > 0
}
export interface ConstDeclNode extends ASTNodeBase {
type: 'ConstDecl';
name: string;
constType: TypeNode;
value: ExprNode;
}
export interface FunctionDeclNode extends ASTNodeBase {
type: 'FunctionDecl';
name: string;
params: Array<{ name: string; paramType: TypeNode }>;
returnType: TypeNode;
body: ExprNode;
isRecursive?: boolean;
}
export interface ConstraintTypeDeclNode extends ASTNodeBase {
type: 'ConstraintTypeDecl';
name: string;
params: Array<{ name: string; paramType: TypeNode }>;
constraints: ExprNode[];
}
// ============================================================================
// Constraints
// ============================================================================
export type ConstraintNode =
| AssertNode
| SoftConstraintNode
| CheckSatNode
| OptimizeNode
| ExprNode;
export interface AssertNode extends ASTNodeBase {
type: 'Assert';
name?: string;
expr: ExprNode;
}
export interface SoftConstraintNode extends ASTNodeBase {
type: 'SoftConstraint';
name?: string;
expr: ExprNode;
weight: number;
}
export interface CheckSatNode extends ASTNodeBase {
type: 'CheckSat';
expr: ExprNode;
}
export interface OptimizeNode extends ASTNodeBase {
type: 'Optimize';
direction: 'minimize' | 'maximize';
name?: string;
expr: ExprNode;
}
// ============================================================================
// Expressions
// ============================================================================
export type ExprNode =
| LiteralNode
| VariableNode
| BinaryExprNode
| UnaryExprNode
| CallExprNode
| IndexExprNode
| IfExprNode
| QuantifiedExprNode
| ArrayLiteralNode
| SetLiteralNode
| TupleLiteralNode
| ArrayComprehensionNode
| SetComprehensionNode
| LambdaExprNode
| MemberAccessNode;
export interface LiteralNode extends ASTNodeBase {
type: 'Literal';
valueType: 'number' | 'string' | 'boolean';
value: number | string | boolean;
inferredType?: 'Int' | 'Real' | 'Bool' | 'String';
}
export interface VariableNode extends ASTNodeBase {
type: 'Variable';
name: string;
}
export interface BinaryExprNode extends ASTNodeBase {
type: 'BinaryExpr';
operator: BinaryOperator;
left: ExprNode;
right: ExprNode;
}
export type BinaryOperator =
// Arithmetic
| 'add' | 'subtract' | 'multiply' | 'divide' | 'div' | 'mod' | 'power'
// Comparison
| 'eq' | 'ne' | 'lt' | 'le' | 'gt' | 'ge'
// Logical
| 'and' | 'or' | 'implies' | 'iff' | 'xor'
// Bitwise
| 'bitAnd' | 'bitOr' | 'bitXor' | 'lshift' | 'rshift' | 'arshift'
// Set/Array
| 'in' | 'contains' | 'union' | 'intersect' | 'diff'
// String
| 'concat' | 'startsWith' | 'endsWith' | 'matches';
export interface UnaryExprNode extends ASTNodeBase {
type: 'UnaryExpr';
operator: UnaryOperator;
operand: ExprNode;
}
export type UnaryOperator = 'negate' | 'not' | 'bitNot';
export interface CallExprNode extends ASTNodeBase {
type: 'CallExpr';
callee: string;
args: ExprNode[];
}
export interface IndexExprNode extends ASTNodeBase {
type: 'IndexExpr';
array: ExprNode;
index: ExprNode;
}
export interface IfExprNode extends ASTNodeBase {
type: 'IfExpr';
condition: ExprNode;
thenBranch: ExprNode;
elseBranch: ExprNode;
}
export interface QuantifiedExprNode extends ASTNodeBase {
type: 'QuantifiedExpr';
quantifier: 'forall' | 'exists';
variable: string;
domain: DomainNode;
body: ExprNode;
}
export interface ArrayLiteralNode extends ASTNodeBase {
type: 'ArrayLiteral';
elements: ExprNode[];
}
export interface SetLiteralNode extends ASTNodeBase {
type: 'SetLiteral';
elements: ExprNode[];
}
export interface TupleLiteralNode extends ASTNodeBase {
type: 'TupleLiteral';
elements: ExprNode[];
}
export interface ArrayComprehensionNode extends ASTNodeBase {
type: 'ArrayComprehension';
element: ExprNode;
variable: string;
domain: DomainNode;
condition?: ExprNode;
}
export interface SetComprehensionNode extends ASTNodeBase {
type: 'SetComprehension';
element: ExprNode;
variable: string;
domain: DomainNode;
condition?: ExprNode;
}
export interface LambdaExprNode extends ASTNodeBase {
type: 'LambdaExpr';
param: string;
body: ExprNode;
}
export interface MemberAccessNode extends ASTNodeBase {
type: 'MemberAccess';
object: ExprNode;
member: string;
}
// ============================================================================
// Domain Specifications
// ============================================================================
export type DomainNode =
| RangeDomainNode
| SetDomainNode
| VariableDomainNode;
export interface RangeDomainNode {
type: 'Range';
start: ExprNode;
end: ExprNode;
exclusive: boolean;
}
export interface SetDomainNode {
type: 'Set';
elements: ExprNode[];
}
export interface VariableDomainNode {
type: 'Variable';
name: string;
}
// ============================================================================
// Type System
// ============================================================================
export interface TypeNode extends ASTNodeBase {
type: 'Type';
name: TypeName;
params?: TypeNode[];
size?: number; // For BitVec[n]
}
export type TypeName =
| 'Int'
| 'Real'
| 'Bool'
| 'String'
| 'BitVec'
| 'Array'
| 'Tuple'
| 'Set'
| 'Map'
| string; // User-defined types
// ============================================================================
// Visitor Pattern Support
// ============================================================================
export interface ASTVisitor<T> {
// Program
visitProgram(node: ProgramNode): T;
// Declarations
visitVarDecl(node: VarDeclNode): T;
visitConstDecl(node: ConstDeclNode): T;
visitFunctionDecl(node: FunctionDeclNode): T;
visitConstraintTypeDecl(node: ConstraintTypeDeclNode): T;
// Constraints
visitAssert(node: AssertNode): T;
visitSoftConstraint(node: SoftConstraintNode): T;
visitCheckSat(node: CheckSatNode): T;
visitOptimize(node: OptimizeNode): T;
// Expressions
visitLiteral(node: LiteralNode): T;
visitVariable(node: VariableNode): T;
visitBinaryExpr(node: BinaryExprNode): T;
visitUnaryExpr(node: UnaryExprNode): T;
visitCallExpr(node: CallExprNode): T;
visitIndexExpr(node: IndexExprNode): T;
visitIfExpr(node: IfExprNode): T;
visitQuantifiedExpr(node: QuantifiedExprNode): T;
visitArrayLiteral(node: ArrayLiteralNode): T;
visitSetLiteral(node: SetLiteralNode): T;
visitTupleLiteral(node: TupleLiteralNode): T;
visitArrayComprehension(node: ArrayComprehensionNode): T;
visitSetComprehension(node: SetComprehensionNode): T;
visitLambdaExpr(node: LambdaExprNode): T;
visitMemberAccess(node: MemberAccessNode): T;
// Types
visitType(node: TypeNode): T;
}
// ============================================================================
// AST Utility Functions
// ============================================================================
export function isExprNode(node: ASTNodeBase): node is ExprNode {
return [
'Literal', 'Variable', 'BinaryExpr', 'UnaryExpr', 'CallExpr',
'IndexExpr', 'IfExpr', 'QuantifiedExpr', 'ArrayLiteral', 'SetLiteral',
'TupleLiteral', 'ArrayComprehension', 'SetComprehension', 'LambdaExpr',
'MemberAccess'
].includes(node.type);
}
export function isDeclarationNode(node: ASTNodeBase): node is DeclarationNode {
return ['VarDecl', 'ConstDecl', 'FunctionDecl', 'ConstraintTypeDecl'].includes(node.type);
}
export function isConstraintNode(node: ASTNodeBase): node is ConstraintNode {
return ['Assert', 'SoftConstraint', 'CheckSat', 'Optimize'].includes(node.type) || isExprNode(node);
}
/**
* Create a source location object
*/
export function createLocation(line: number, column: number, length?: number): SourceLocation {
return { line, column, length };
}
/**
* Pretty-print AST for debugging
*/
export function astToString(node: ASTNodeBase, indent: number = 0): string {
const spaces = ' '.repeat(indent);
const lines: string[] = [];
lines.push(`${spaces}${node.type}`);
for (const [key, value] of Object.entries(node)) {
if (key === 'type' || key === 'location') continue;
if (Array.isArray(value)) {
lines.push(`${spaces} ${key}:`);
for (const item of value) {
if (typeof item === 'object' && item !== null && 'type' in item) {
lines.push(astToString(item as ASTNodeBase, indent + 2));
} else {
lines.push(`${spaces} ${JSON.stringify(item)}`);
}
}
} else if (typeof value === 'object' && value !== null && 'type' in value) {
lines.push(`${spaces} ${key}:`);
lines.push(astToString(value as ASTNodeBase, indent + 2));
} else {
lines.push(`${spaces} ${key}: ${JSON.stringify(value)}`);
}
}
return lines.join('\n');
}
