source-layout

#!/usr/bin/env node
import fs from 'node:fs';
import { execFileSync } from 'node:child_process';

if (process.argv.length !== 2) {
  console.error('usage: tools/source-layout');
  process.exit(2);
}

const files = [...new Set(execFileSync('git',
  ['ls-files', '--cached', '--others', '--exclude-standard'], { encoding: 'utf8' })
  .trim().split('\n'))].filter(f => fs.existsSync(f));
const active = files.filter(f => f.endsWith('.lean') && !/^(paper|data)\//.test(f));
const internal = /^(LeanExe|Verified|Examples|Library|Demos|TestSupport)(\.|$)/;
const modulePath = m => (m.startsWith('TestSupport') ? 'tests/' : '') +
  m.replaceAll('.', '/') + '.lean';
const imports = new Map();
const errors = [];
for (const file of active) {
  const source = fs.readFileSync(file, 'utf8');
  if (/(?<![\w.])\.(Library|Examples|Demos)\./.test(source)) {
    errors.push(`${file}: qualified anonymous constructor`);
  }
  const compiler = file.startsWith('LeanExe/') ||
    (file.startsWith('Verified/') && !file.startsWith('Verified/Examples/'));
  if (compiler && /^(?:open|def|abbrev|theorem|namespace) [^\n]*\b(?:Library|Demos|Examples|TestSupport)\./m.test(source)) {
    errors.push(`${file}: compiler declaration refers to application code`);
  }
  const names = [...source.matchAll(/^import ([\w.]+)/gm)]
    .map(m => m[1]).filter(m => internal.test(m));
  imports.set(file, names.map(modulePath));
  for (const name of names) {
    if (!fs.existsSync(modulePath(name))) errors.push(`${file}: missing import ${name}`);
    if (compiler && /^(Library|Demos|Examples|TestSupport)(\.|$)/.test(name)) {
      errors.push(`${file}: compiler imports ${name}`);
    }
    if (file.startsWith('Library/') && /^(Examples|Demos|TestSupport|Verified\.Examples)(\.|$)/.test(name)) {
      errors.push(`${file}: library imports ${name}`);
    }
  }
}

const visited = new Set();
const pending = new Set();
function visit(file) {
  if (pending.has(file)) { errors.push(`${file}: import cycle`); return; }
  if (visited.has(file)) return;
  pending.add(file);
  for (const dependency of imports.get(file) ?? []) visit(dependency);
  pending.delete(file);
  visited.add(file);
}
for (const file of active) visit(file);

const programs = active.filter(f => f.startsWith('Library/') && f.endsWith('/Program.lean'));
for (const program of programs) {
  const seen = new Set();
  function check(file) {
    if (seen.has(file)) return;
    seen.add(file);
    if (/^Verified\//.test(file)) {
      errors.push(`${program}: native import reaches ${file}`);
      return;
    }
    for (const dependency of imports.get(file) ?? []) check(dependency);
  }
  check(program);
  if (!imports.get('Library/Native.lean')?.includes(program)) {
    errors.push(`${program}: missing from Library.Native`);
  }
}

const verifiedNames = new Set();
let modules = 0;
const registry = 'tests/verified/modules.txt';
for (const line of fs.readFileSync(registry, 'utf8').trim().split('\n')) {
  const [module, constant, name, extra] = line.split(':');
  if (!module || !constant || !name || extra || !fs.existsSync(modulePath(module))) {
    errors.push(`${registry}: invalid entry ${line}`);
  }
  if (verifiedNames.has(name)) errors.push(`${registry}: duplicate output ${name}`);
  verifiedNames.add(name);
  modules++;
}
for (const line of fs.readFileSync('tests/verified/library-cases.txt', 'utf8').trim().split('\n')) {
  const [source, sourceExport, target, targetExport, extra] = line.split('|');
  if (!verifiedNames.has(source) || !verifiedNames.has(target) ||
      !sourceExport || !targetExport || extra) errors.push(`Invalid library case mapping: ${line}`);
}
for (const line of fs.readFileSync('tests/verified/numerics.txt', 'utf8').trim().split('\n')) {
  const [name, theorem, file, extra] = line.split(':');
  if (!verifiedNames.has(name) || !theorem || !fs.existsSync(modulePath(theorem)) ||
      !file || !fs.existsSync(file) || extra) errors.push(`Invalid numerical entry: ${line}`);
}
if (errors.length) {
  for (const error of errors) console.error(error);
  process.exitCode = 1;
} else {
  console.log(`Layout: ${active.length} Lean files, ${programs.length} native programs, ${modules} registered modules`);
}