#!/usr/bin/env node
import yargs from 'yargs';
import { hideBin } from 'yargs/helpers';
import { parseSpeckFile } from './parser.js';
import { generateProvenanceGraph } from './generators/provenance.js';
import { generateCycloneDX } from './generators/cyclonedx.js';
import { generateSPDX } from './generators/spdx.js';
import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js';
import { generateZ3, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js';
import { generateRust } from './generators/rust.js';
import fs from 'fs';
import path from 'path';
async function main() {
    // Guard: check that dist is not stale before compiling
    const checkScript = path.join(path.dirname(new URL(import.meta.url).pathname), '..', 'check-dist.sh');
    if (fs.existsSync(checkScript)) {
        try {
            const { execSync } = await import('child_process');
            execSync(`bash "${checkScript}"`, { stdio: 'inherit' });
        }
        catch {
            console.error('\n❌ Cannot compile with stale dist. Rebuild first.');
            process.exit(1);
        }
    }
    const argv = await yargs(hideBin(process.argv))
        .command('$0 <file>', 'Compile a SpeckDL specification', (yargsCmd) => {
        return yargsCmd
            .positional('file', {
            describe: 'SpeckDL file to compile',
            type: 'string',
            demandOption: true,
        })
            .option('output-dir', {
            alias: 'o',
            describe: 'Output directory for compiled artifacts',
            type: 'string',
            default: './out',
        })
            .option('target', {
            alias: 't',
            describe: 'Compilation target',
            type: 'string',
            choices: ['typescript', 'z3', 'rust', 'all'],
            default: 'typescript',
        })
            .option('verify-depth', {
            alias: 'd',
            describe: 'Bounded model checking depth for Z3 verification',
            type: 'number',
            default: 10,
        })
            .option('bom-format', {
            alias: 'b',
            describe: 'BOM output format',
            type: 'string',
            choices: ['cdx', 'spdx', 'both'],
            default: 'both',
        });
    })
        .help()
        .argv;
    const file = argv.file;
    const options = {
        outputDir: argv.outputDir,
        bomFormat: argv.bomFormat,
        target: argv.target,
        verifyDepth: argv.verifyDepth,
    };
    console.log(`Compiling ${file}...`);
    // Parse the Speck file
    const ast = parseSpeckFile(file);
    const speckCount = ast.specks.length;
    const memberCount = ast.specks.reduce((sum, s) => sum + s.members.length, 0);
    console.log(`AST parsed successfully: ${speckCount} speck(s), ${memberCount} member(s)`);
    // Ensure output directory exists
    if (!fs.existsSync(options.outputDir)) {
        fs.mkdirSync(options.outputDir, { recursive: true });
    }
    // Read raw source for invariant/next parsing that the AST parser doesn't handle yet
    const rawSource = fs.readFileSync(file, 'utf-8');
    // Generate Rust state machine if target is rust or all
    if (options.target === 'rust' || options.target === 'all') {
        console.log('\nGenerating Rust state machine...');
        generateRust(ast, options.outputDir);
    }
    // Always generate provenance (it's the core output) if not z3-only or rust-only
    if (options.target !== 'z3' && options.target !== 'rust') {
        console.log('\nGenerating provenance graph (PROV-O JSON-LD)...');
        generateProvenanceGraph(ast, options.outputDir);
    }
    // Generate Z3 SMT-LIB2 if target is z3 or all
    if (options.target === 'z3' || options.target === 'all') {
        console.log('\nGenerating Z3 SMT-LIB2...');
        // Parse invariants from raw source for Z3 backend
        for (const speck of ast.specks) {
            const invariants = parseInvariantsFromSource(rawSource, speck.name);
            const nextNode = parseNextFromSource(rawSource, speck.name);
            // Attach parsed data to the AST for the generator
            speck._invariants = invariants;
            speck._next = nextNode;
        }
        const z3Options = { verifyDepth: options.verifyDepth };
        generateZ3(ast, options.outputDir, z3Options);
    }
    // Generate TypeScript state machine if not z3-only or rust-only
    if (options.target !== 'z3' && options.target !== 'rust') {
        console.log('\nGenerating TypeScript state machine...');
        generateTypeScriptStateMachine(ast, options.outputDir);
        // Generate BOM based on format selection
        if (options.bomFormat === 'cdx' || options.bomFormat === 'both') {
            console.log('\nGenerating CycloneDX BOM...');
            generateCycloneDX(ast, options.outputDir);
        }
        if (options.bomFormat === 'spdx' || options.bomFormat === 'both') {
            console.log('\nGenerating SPDX BOM...');
            generateSPDX(ast, options.outputDir);
        }
    }
    console.log(`\nCompilation complete. Output: ${options.outputDir}/`);
}
main().catch((err) => {
    console.error('Compilation failed:', err);
    process.exit(1);
});
//# sourceMappingURL=index.js.map