import { parse } from '../parser/GeneratedParser.js';
import { DSL_PRELUDE } from './DSLPrelude.js';

const BUILTIN_TYPES = new Set(['string', 'number', 'boolean', 'timestamp', 'duration', 'object', 'any']);
const BUILTIN_CHALLENGES = new Set([
  'mfa',
  'webauthn',
  'login',
  'sms',
  'voice',
  'magic_link',
  'email_verified',
  'oauth_session'
]);

const DEFAULT_EVIDENCE_RETURN = 'boolean';
const DEFAULT_MEASURE_RETURN = 'any';

export function validateDslText(dslText, options = {}) {
  const preludeProgram = parsePrelude(options);
  let program;
  try {
    program = parse(dslText);
  } catch (error) {
    const syntaxError = formatPegError(error, dslText, options.source || 'input');
    return {
      success: false,
      program: null,
      errors: [formatValidationError(syntaxError)],
      warnings: [],
      errorDetails: [syntaxError]
    };
  }

  const errors = [];
  const warnings = [];

  const tables = buildSymbolTables(program, preludeProgram);
  validateDefinitions(program, tables, errors, warnings, dslText);
  validateFacts(program, tables, errors, warnings, dslText);
  validateSources(program, tables, errors, warnings, dslText);
  validateMeasures(program, tables, errors, warnings, dslText);
  validateEvidence(program, tables, errors, warnings, dslText);
  validateCrossKindRelationNames(program, errors, warnings, dslText);

  return {
    success: errors.length === 0,
    program,
    errors: errors.map(formatValidationError),
    warnings: warnings.map(formatValidationError),
    errorDetails: errors,
    warningDetails: warnings
  };
}

function buildSymbolTables(program, preludeProgram) {
  const definitions = new Map();
  const facts = new Map();
  const evidence = new Map();
  const measures = new Map();
  const sources = new Map();
  const builtins = {
    definitions: new Set(),
    facts: new Set(),
    evidence: new Set(),
    measures: new Set(),
    sources: new Set()
  };

  for (const def of preludeProgram?.definitions || []) {
    definitions.set(def.name, def);
    builtins.definitions.add(def.name);
  }
  for (const fact of preludeProgram?.facts || []) {
    facts.set(fact.name, fact);
    builtins.facts.add(fact.name);
  }
  for (const ev of preludeProgram?.evidence || []) {
    evidence.set(ev.name, ev);
    builtins.evidence.add(ev.name);
  }
  for (const measure of preludeProgram?.measures || []) {
    measures.set(measure.name, measure);
    builtins.measures.add(measure.name);
  }
  for (const source of preludeProgram?.sources || []) {
    sources.set(source.name, source);
    builtins.sources.add(source.name);
  }

  for (const def of program.definitions || []) {
    definitions.set(def.name, def);
  }
  for (const fact of program.facts || []) {
    facts.set(fact.name, fact);
  }
  for (const ev of program.evidence || []) {
    evidence.set(ev.name, ev);
  }
  for (const measure of program.measures || []) {
    measures.set(measure.name, measure);
  }
  for (const source of program.sources || []) {
    sources.set(source.name, source);
  }

  return { definitions, facts, evidence, measures, sources, builtins };
}

function validateDefinitions(program, tables, errors, warnings, source) {
  const seen = new Map();
  for (const def of program.definitions || []) {
    if (tables.builtins?.definitions?.has(def.name)) {
      errors.push(createError({
        message: `Type '${def.name}' is a built-in and cannot be redefined.`,
        rule: 'Built-in types are reserved and cannot be overridden.',
        fix: `Rename your type or remove the duplicate definition for '${def.name}'.`,
        location: findLocation(source, `definition ${def.name}`),
        context: formatContext(source, findLocation(source, def.name))
      }));
    }
    if (seen.has(def.name)) {
      errors.push(createError({
        message: `Duplicate type definition '${def.name}'.`,
        rule: 'Each type name must be unique within a program.',
        fix: 'Rename one of the type definitions to a unique name.',
        location: findLocation(source, `definition ${def.name}`),
        context: formatContext(source, findLocation(source, def.name))
      }));
    }
    seen.set(def.name, def);

    for (const field of def.fields || []) {
      if (!isTypeKnown(field.fieldType, tables)) {
        errors.push(createError({
          message: `Unknown field type '${field.fieldType}' in '${def.name}.${field.name}'.`,
          rule: 'Field types must be built-in or declared as a definition.',
          fix: `Add a type definition for '${field.fieldType}' or correct the field type.`,
          location: findLocation(source, field.fieldType),
          context: formatContext(source, findLocation(source, def.name))
        }));
      }
    }
  }
}

function validateFacts(program, tables, errors, warnings, source) {
  const seen = new Map();
  for (const fact of program.facts || []) {
    if (tables.builtins?.facts?.has(fact.name)) {
      errors.push(createError({
        message: `Fact '${fact.name}' is a built-in and cannot be redefined.`,
        rule: 'Built-in facts are reserved and cannot be overridden.',
        fix: `Rename your fact or remove the duplicate definition for '${fact.name}'.`,
        location: findLocation(source, `fact ${fact.name}`),
        context: formatContext(source, findLocation(source, fact.name))
      }));
    }
    if (seen.has(fact.name)) {
      errors.push(createError({
        message: `Duplicate fact definition '${fact.name}'.`,
        rule: 'Each fact name must be unique within a program.',
        fix: 'Rename one of the fact definitions to a unique name.',
        location: findLocation(source, `fact ${fact.name}`),
        context: formatContext(source, findLocation(source, fact.name))
      }));
    }
    seen.set(fact.name, fact);
    const arity = fact.params ? fact.params.length : 0;
    if (!fact.params || arity === 0) {
      warnings.push(createError({
        message: `Fact '${fact.name}' declares no parameters.`,
        rule: 'Facts should declare parameters to capture relation signatures.',
        fix: `Add parameters to '${fact.name}', e.g. (${fact.name}(user: User, doc: Document)).`,
        location: findLocation(source, `fact ${fact.name}`),
        context: formatContext(source, findLocation(source, fact.name))
      }));
    }

    const paramNames = new Set();
    for (const param of fact.params || []) {
      if (paramNames.has(param.name)) {
        errors.push(createError({
          message: `Duplicate parameter '${param.name}' in fact '${fact.name}'.`,
          rule: 'Each parameter name must be unique within a fact signature.',
          fix: 'Rename the parameter to a unique name.',
          location: findLocation(source, param.name),
          context: formatContext(source, findLocation(source, fact.name))
        }));
      }
      paramNames.add(param.name);

      if (!isTypeKnown(param.paramType, tables)) {
        errors.push(createError({
          message: `Unknown parameter type '${param.paramType}' in fact '${fact.name}'.`,
          rule: 'Parameter types must be built-in or declared as a definition.',
          fix: `Add a type definition for '${param.paramType}' or correct the parameter type.`,
          location: findLocation(source, param.paramType),
          context: formatContext(source, findLocation(source, fact.name))
        }));
      }
    }
  }
}

function validateSources(program, tables, errors, warnings, source) {
  for (const src of program.sources || []) {
    if (tables.builtins?.sources?.has(src.name)) {
      errors.push(createError({
        message: `Source '${src.name}' is a built-in and cannot be redefined.`,
        rule: 'Built-in sources are reserved and cannot be overridden.',
        fix: `Rename your source or remove the duplicate definition for '${src.name}'.`,
        location: findLocation(source, `source ${src.name}`),
        context: formatContext(source, findLocation(source, src.name))
      }));
    }

    const returnType = src.provides || null;
    if (returnType && !isTypeKnown(returnType, tables)) {
      errors.push(createError({
        message: `Unknown return type '${returnType}' for source '${src.name}'.`,
        rule: 'Source PROVIDES types must be built-in or declared as a definition.',
        fix: `Add a type definition for '${returnType}' or correct the PROVIDES clause.`,
        location: findLocation(source, returnType),
        context: formatContext(source, findLocation(source, src.name))
      }));
    }

    if (src.within && !isValidDuration(src.within)) {
      errors.push(createError({
        message: `Invalid duration '${src.within?.value || ''}' in within constraint for source '${src.name}'.`,
        rule: 'Within constraints must be duration literals (e.g. 10m, 5h, 1d).',
        fix: `Use a duration literal like '10m' in the within constraint for '${src.name}'.`,
        location: findLocation(source, 'within'),
        context: formatContext(source, findLocation(source, src.name))
      }));
    }

    const paramNames = new Set();
    for (const param of src.params || []) {
      if (paramNames.has(param.name)) {
        errors.push(createError({
          message: `Duplicate parameter '${param.name}' in source '${src.name}'.`,
          rule: 'Each parameter name must be unique within a source signature.',
          fix: 'Rename the parameter to a unique name.',
          location: findLocation(source, param.name),
          context: formatContext(source, findLocation(source, src.name))
        }));
      }
      paramNames.add(param.name);

      if (!isTypeKnown(param.paramType, tables)) {
        errors.push(createError({
          message: `Unknown parameter type '${param.paramType}' in source '${src.name}'.`,
          rule: 'Parameter types must be built-in or declared as a definition.',
          fix: `Add a type definition for '${param.paramType}' or correct the parameter type.`,
          location: findLocation(source, param.paramType),
          context: formatContext(source, findLocation(source, src.name))
        }));
      }
    }
  }
}

function isValidDuration(within) {
  if (!within || typeof within.value !== 'string') return false;
  return /^\d+(h|d|w|m)$/.test(within.value);
}

function validateMeasures(program, tables, errors, warnings, source) {
  for (const measure of program.measures || []) {
    if (tables.builtins?.measures?.has(measure.name)) {
      errors.push(createError({
        message: `Measure '${measure.name}' is a built-in and cannot be redefined.`,
        rule: 'Built-in measures are reserved and cannot be overridden.',
        fix: `Rename your measure or remove the duplicate definition for '${measure.name}'.`,
        location: findLocation(source, `measure ${measure.name}`),
        context: formatContext(source, findLocation(source, measure.name))
      }));
    }
    const returnType = measure.provides || DEFAULT_MEASURE_RETURN;
    if (returnType !== DEFAULT_MEASURE_RETURN && !isTypeKnown(returnType, tables)) {
      errors.push(createError({
        message: `Unknown return type '${returnType}' for measure '${measure.name}'.`,
        rule: 'Measure return types must be built-in or declared as a definition.',
        fix: `Add a type definition for '${returnType}' or correct the PROVIDES clause.`,
        location: findLocation(source, returnType),
        context: formatContext(source, findLocation(source, measure.name))
      }));
    }

    const paramScope = buildParamScope(measure.params, tables, errors, source, `measure ${measure.name}`);
    if (measure.body) {
      validateMeasureBody(measure.body, paramScope, tables, errors, warnings, source, measure);
    }
  }
}

function validateEvidence(program, tables, errors, warnings, source) {
  const seen = new Map();
  for (const ev of program.evidence || []) {
    if (tables.builtins?.evidence?.has(ev.name)) {
      errors.push(createError({
        message: `Evidence '${ev.name}' is a built-in and cannot be redefined.`,
        rule: 'Built-in evidence names are reserved and cannot be overridden.',
        fix: `Rename your evidence or remove the duplicate definition for '${ev.name}'.`,
        location: findLocation(source, `evidence ${ev.name}`),
        context: formatContext(source, findLocation(source, ev.name))
      }));
    }
    if (seen.has(ev.name)) {
      errors.push(createError({
        message: `Duplicate evidence definition '${ev.name}'.`,
        rule: 'Each evidence name must be unique within a program.',
        fix: 'Rename one of the evidence definitions to a unique name.',
        location: findLocation(source, `evidence ${ev.name}`),
        context: formatContext(source, findLocation(source, ev.name))
      }));
    }
    seen.set(ev.name, ev);
    const returnType = ev.provides || DEFAULT_EVIDENCE_RETURN;
    if (returnType !== DEFAULT_EVIDENCE_RETURN && !isTypeKnown(returnType, tables)) {
      errors.push(createError({
        message: `Unknown return type '${returnType}' for evidence '${ev.name}'.`,
        rule: 'Evidence return types must be built-in or declared as a definition.',
        fix: `Add a type definition for '${returnType}' or correct the PROVIDES clause.`,
        location: findLocation(source, returnType),
        context: formatContext(source, findLocation(source, ev.name))
      }));
    }

    const paramScope = buildParamScope(ev.params, tables, errors, source, `evidence ${ev.name}`);
    if (ev.body) {
      validateEvidenceBody(ev.body, paramScope, tables, errors, warnings, source, ev);
    }
  }
}

/**
 * Relation names must be unique across facts, sources, evidence, and measures.
 * A fact and an evidence sharing a name would silently overwrite each other's
 * relation config during generation (and read as a false cyclic reference).
 */
function validateCrossKindRelationNames(program, errors, warnings, source) {
  const seen = new Map();
  const kinds = [
    ['fact', program.facts],
    ['source', program.sources],
    ['evidence', program.evidence],
    ['measure', program.measures]
  ];
  for (const [kind, items] of kinds) {
    for (const item of items || []) {
      const prev = seen.get(item.name);
      if (prev) {
        errors.push(createError({
          message: `Name '${item.name}' is already used by a ${prev} declaration.`,
          rule: 'Relation names must be unique across facts, sources, evidence, and measures.',
          fix: `Rename the ${kind} or the ${prev} to a unique name.`,
          location: findLocation(source, `${kind} ${item.name}`),
          context: formatContext(source, findLocation(source, item.name))
        }));
      } else {
        seen.set(item.name, kind);
      }
    }
  }
}

function validateEvidenceBody(body, scope, tables, errors, warnings, source, parent) {
  for (const stmt of body.statements || []) {
    switch (stmt.type) {
      case 'DefeasibleLogic':
        validateBooleanExpression(stmt.condition, scope, tables, errors, warnings, source, parent);
        if (stmt.defeater) {
          validateBooleanExpression(stmt.defeater, scope, tables, errors, warnings, source, parent);
        }
        break;
      case 'Fusion':
        for (const expr of stmt.expressions || []) {
          validateBooleanExpression(expr, scope, tables, errors, warnings, source, parent);
        }
        break;
      case 'CollectionProcessing':
        validateCollectionProcessing(stmt, scope, tables, errors, warnings, source, parent);
        break;
      case 'PatternMatch':
        validatePatternMatch(stmt, scope, tables, errors, warnings, source, parent);
        break;
      default:
        validateBooleanExpression(stmt, scope, tables, errors, warnings, source, parent);
        break;
    }
  }
}

function validateMeasureBody(body, scope, tables, errors, warnings, source, measure) {
  for (const stmt of body.statements || []) {
    if (stmt.type === 'Fusion') {
      for (const expr of stmt.expressions || []) {
        inferExpressionType(expr, scope, tables, errors, warnings, source, measure);
      }
    } else if (stmt.type === 'Aggregation') {
      for (const expr of stmt.expressions || []) {
        inferExpressionType(expr, scope, tables, errors, warnings, source, measure);
      }
    } else {
      inferExpressionType(stmt, scope, tables, errors, warnings, source, measure);
    }
  }

  if (body.returnStatement && body.returnStatement.expression) {
    const returnType = measure.provides || DEFAULT_MEASURE_RETURN;
    const inferred = inferExpressionType(body.returnStatement.expression, scope, tables, errors, warnings, source, measure);
    if (returnType !== DEFAULT_MEASURE_RETURN && inferred && inferred.type) {
      if (!isAssignable(inferred.type, returnType)) {
        errors.push(createError({
          message: `Return type mismatch in measure '${measure.name}': expected '${returnType}', got '${inferred.type}'.`,
          rule: 'Measure return expressions must match the PROVIDES type.',
          fix: 'Update the return expression or adjust the PROVIDES type.',
          location: findLocation(source, measure.name),
          context: formatContext(source, findLocation(source, measure.name))
        }));
      }
    }
  }
}

function validateCollectionProcessing(stmt, scope, tables, errors, warnings, source, parent) {
  const measureType = inferExpressionType(stmt.measure, scope, tables, errors, warnings, source, parent);
  if (measureType && measureType.type && !measureType.isArray) {
    errors.push(createError({
      message: 'Collection processing requires a measure that returns an array.',
      rule: 'Use |var| only with measures that return array types.',
      fix: 'Change the measure to return an array (Type[]) or use a direct predicate instead.',
      location: findLocation(source, stmt.variable),
      context: formatContext(source, findLocation(source, stmt.variable))
    }));
  }

  const nextScope = new Map(scope);
  if (measureType && measureType.elementType) {
    nextScope.set(stmt.variable, { type: measureType.elementType, isArray: false });
  } else {
    nextScope.set(stmt.variable, { type: 'any', isArray: false });
  }
  validateEvidenceBody(stmt.body, nextScope, tables, errors, warnings, source, parent);
}

function validatePatternMatch(stmt, scope, tables, errors, warnings, source, parent) {
  const predicate = stmt.predicate;
  if (!predicate || !predicate.name) return;

  const signature = resolvePredicateSignature(predicate.name, tables);
  if (!signature) {
    errors.push(createError({
      message: `Unknown predicate '${predicate.name}'.`,
      rule: 'Predicates must reference defined facts, evidence, or measures.',
      fix: `Define '${predicate.name}' as a fact/evidence/measure or correct the name.`,
      location: findLocation(source, predicate.name),
      context: formatContext(source, findLocation(source, predicate.name))
    }));
    return;
  }

  const nextScope = new Map(scope);
  for (let i = 0; i < (predicate.args || []).length; i++) {
    const arg = predicate.args[i];
    const expected = signature.params[i];
    if (!expected) continue;
    if (arg && arg.type === 'Wildcard') {
      nextScope.set(arg.name, { type: expected.type, isArray: expected.isArray });
      continue;
    }
    const inferred = inferExpressionType(arg, scope, tables, errors, warnings, source, parent);
    if (inferred && inferred.type && expected.type) {
      if (!isAssignable(inferred.type, expected.type, inferred.isArray, expected.isArray)) {
        errors.push(createError({
          message: `Type mismatch for '${predicate.name}' argument ${i + 1}: expected '${formatType(expected)}', got '${formatType(inferred)}'.`,
          rule: 'Predicate arguments must match declared parameter types.',
          fix: 'Update the argument or adjust the predicate signature.',
          location: findLocation(source, predicate.name),
          context: formatContext(source, findLocation(source, predicate.name))
        }));
      }
    }
  }

  if (stmt.binding) {
    nextScope.set(stmt.binding, { type: 'relation', isArray: false, relation: predicate.name });
  }

  validateEvidenceBody(stmt.body, nextScope, tables, errors, warnings, source, parent);

  if (stmt.withClause) {
    validateBooleanExpression(stmt.withClause.condition, nextScope, tables, errors, warnings, source, parent);
  }
}

function validateBooleanExpression(expr, scope, tables, errors, warnings, source, parent) {
  const inferred = inferExpressionType(expr, scope, tables, errors, warnings, source, parent);
  if (!inferred || !inferred.type) return;
  // Challenge / injectable-source predicate calls are proof requirements,
  // not value expressions — they are valid evidence-body statements.
  if (inferred.type !== 'boolean' && inferred.type !== 'challenge_proof') {
    errors.push(createError({
      message: `Expected a boolean expression, got '${inferred.type}'.`,
      rule: 'Evidence statements must evaluate to boolean or possibilistic truth values.',
      fix: 'Use a predicate, comparison, or logical expression that returns boolean.',
      location: expr?.location || findLocation(source, inferred.name || ''),
      context: formatContext(source, expr?.location || findLocation(source, inferred.name || ''))
    }));
  }
}

function inferExpressionType(expr, scope, tables, errors, warnings, source, parent) {
  if (!expr) return null;

  switch (expr.type) {
    case 'Literal':
      return inferLiteralType(expr);
    case 'Variable':
      return resolveVariableType(expr, scope, errors, source);
    case 'PredicateCall':
      return resolvePredicateCallType(expr, scope, tables, errors, warnings, source, parent);
    case 'AttributeAccess':
      return resolveAttributeType(expr, scope, tables, errors, warnings, source, parent);
    case 'BindingAccess':
      return inferExpressionType(expr.expression, scope, tables, errors, warnings, source, parent);
    case 'UnaryExpression':
      return { type: 'boolean', isArray: false };
    case 'BinaryExpression':
      return resolveBinaryExpressionType(expr, scope, tables, errors, warnings, source, parent);
    default:
      return { type: 'any', isArray: false };
  }
}

function resolveBinaryExpressionType(expr, scope, tables, errors, warnings, source, parent) {
  const left = inferExpressionType(expr.left, scope, tables, errors, warnings, source, parent);
  let scopedForRight = scope;
  const guard = extractTypeGuard(expr.left, scope, tables, errors, warnings, source, parent);
  if (expr.operator === '&&' && guard) {
    scopedForRight = new Map(scope);
    scopedForRight.set(guard.targetPath, { type: guard.typeName, isArray: false });
  }
  const right = inferExpressionType(expr.right, scopedForRight, tables, errors, warnings, source, parent);
  const operator = expr.operator;

  if (operator === 'is') {
    const typeName = resolveTypeName(expr.right);
    if (!typeName || !isTypeKnown(typeName, tables)) {
      errors.push(createError({
        message: 'Type guard requires a known type name on the right-hand side.',
        rule: 'Use "value is TypeName" with a declared type.',
        fix: 'Ensure the right-hand side is a valid type name.',
        location: expr.location || findLocation(source, 'is'),
        context: formatContext(source, expr.location || findLocation(source, 'is'))
      }));
    }
    return { type: 'boolean', isArray: false };
  }

  if (['+', '-', '*', '/'].includes(operator)) {
    if (!isNumberType(left) || !isNumberType(right)) {
      errors.push(createError({
        message: `Arithmetic operator '${operator}' requires numeric operands.`,
        rule: 'Arithmetic expressions must use numbers.',
        fix: 'Cast or convert operands to numbers before applying arithmetic operators.',
        location: expr.location || findLocation(source, operator),
        context: formatContext(source, expr.location || findLocation(source, operator))
      }));
    }
    return { type: 'number', isArray: false };
  }

  if (['==', '!=', '>=', '<=', '>', '<', 'within'].includes(operator)) {
    if (operator === 'within') {
      if (!isTimestampType(left) || !isDurationType(right)) {
        errors.push(createError({
          message: 'Temporal comparisons require a timestamp on the left and duration on the right.',
          rule: 'Use "within" with timestamp values and duration literals.',
          fix: 'Ensure the left expression is a timestamp and the right is a duration (e.g., 1h).',
          location: expr.location || findLocation(source, 'within'),
          context: formatContext(source, expr.location || findLocation(source, 'within'))
        }));
      }
    } else if (!areComparableTypes(left, right)) {
      errors.push(createError({
        message: `Comparison '${operator}' uses incompatible types '${formatType(left)}' and '${formatType(right)}'.`,
        rule: 'Comparisons require compatible operand types.',
        fix: 'Align the types on both sides of the comparison.',
        location: expr.location || findLocation(source, operator),
        context: formatContext(source, expr.location || findLocation(source, operator))
      }));
    }
    return { type: 'boolean', isArray: false };
  }

  if (['&&', '||'].includes(operator)) {
    return { type: 'boolean', isArray: false };
  }

  return { type: 'any', isArray: false };
}

function resolvePredicateCallType(expr, scope, tables, errors, warnings, source, parent) {
  if (expr.name === 'is_type') {
    const guard = extractTypeGuard(expr, scope, tables, errors, warnings, source, parent);
    if (!guard) {
      errors.push(createError({
        message: 'is_type requires a value expression and a known type name.',
        rule: 'Type guards must be written as is_type(value, TypeName).',
        fix: 'Pass a value expression and a declared type name.',
        location: findLocation(source, expr.name),
        context: formatContext(source, findLocation(source, expr.name))
      }));
    }
    return { type: 'boolean', isArray: false };
  }

  if (expr.challenge) {
    if (!Array.isArray(expr.args) || expr.args.length === 0) {
      errors.push(createError({
        message: `Challenge predicate '${expr.name}' must specify a subject (e.g., !${expr.name}(user)).`,
        rule: 'Challenge predicates require an explicit subject bound to the current session or user.',
        fix: `Add an argument: !${expr.name}(user) or !${expr.name}(session).`,
        location: findLocation(source, expr.name),
        context: formatContext(source, findLocation(source, expr.name))
      }));
      return { type: 'any', isArray: false };
    }
    if (BUILTIN_CHALLENGES.has(expr.name)) {
      return { type: 'challenge_proof', isArray: false, challenge: true };
    }
    const ev = tables.evidence.get(expr.name);
    if (ev && ev.challenge) {
      return { type: 'challenge_proof', isArray: false, challenge: true };
    }
    if (ev && !ev.challenge) {
      errors.push(createError({
        message: `Evidence '${expr.name}' is not declared as a challenge evidence.`,
        rule: 'Only challenge evidence can be referenced with a ! prefix.',
        fix: `Declare '${expr.name}' as 'evidence !${expr.name}(...)' or remove the ! prefix.`,
        location: findLocation(source, expr.name),
        context: formatContext(source, findLocation(source, expr.name))
      }));
      return { type: 'any', isArray: false };
    }
    // Injectable sources and injectable facts are valid challenge-style
    // references (witness requirements), even though they are not evidence.
    const src = tables.sources.get(expr.name);
    if (src) {
      return { type: 'challenge_proof', isArray: false, challenge: true };
    }
    const injectableFact = tables.facts.get(expr.name);
    if (injectableFact && injectableFact.injectable) {
      return { type: 'challenge_proof', isArray: false, challenge: true };
    }
    errors.push(createError({
      message: `Unknown challenge predicate '${expr.name}'.`,
      rule: 'Challenge predicates must be predefined or declared as challenge evidence.',
      fix: `Define 'evidence !${expr.name}(...)' or use a predefined challenge predicate.`,
      location: findLocation(source, expr.name),
      context: formatContext(source, findLocation(source, expr.name))
    }));
    return { type: 'any', isArray: false };
  }

  const signature = resolvePredicateSignature(expr.name, tables);
  if (!signature) {
    errors.push(createError({
      message: `Unknown predicate '${expr.name}'.`,
      rule: 'Predicates must reference defined facts, evidence, or measures.',
      fix: `Define '${expr.name}' as a fact/evidence/measure or correct the name.`,
      location: findLocation(source, expr.name),
      context: formatContext(source, findLocation(source, expr.name))
    }));
    return { type: 'any', isArray: false };
  }

  const expectedCount = signature.params.length;
  const actualCount = expr.args ? expr.args.length : 0;
  if (expectedCount !== actualCount) {
    errors.push(createError({
      message: `Predicate '${expr.name}' expects ${expectedCount} arguments, got ${actualCount}.`,
      rule: 'Predicate calls must match the declared parameter count.',
      fix: 'Add or remove arguments to match the predicate signature.',
      location: findLocation(source, expr.name),
      context: formatContext(source, findLocation(source, expr.name))
    }));
  }

  for (let i = 0; i < Math.min(expectedCount, actualCount); i++) {
    const expected = signature.params[i];
    const arg = expr.args[i];
    if (arg && arg.type === 'Wildcard') {
      continue;
    }
    const inferred = inferExpressionType(arg, scope, tables, errors, warnings, source, parent);
    if (inferred && expected) {
      if (!isAssignable(inferred.type, expected.type, inferred.isArray, expected.isArray)) {
        errors.push(createError({
          message: `Type mismatch for '${expr.name}' argument ${i + 1}: expected '${formatType(expected)}', got '${formatType(inferred)}'.`,
          rule: 'Predicate arguments must match declared parameter types.',
          fix: 'Update the argument or adjust the predicate signature.',
          location: findLocation(source, expr.name),
          context: formatContext(source, findLocation(source, expr.name))
        }));
      }
    }
  }

  return signature.returnType;
}

function resolveAttributeType(expr, scope, tables, errors, warnings, source, parent) {
  const override = getScopeOverride(expr.object, scope);
  const objectType = override || inferExpressionType(expr.object, scope, tables, errors, warnings, source, parent);
  if (!objectType || !objectType.type) {
    return { type: 'any', isArray: false };
  }

  if (objectType.challenge) {
    const attr = expr.attribute;
    if (attr === 'issued_at' || attr === 'issuedAt' || attr === 'expires_at' || attr === 'expiresAt') {
      return { type: 'timestamp', isArray: false };
    }
    errors.push(createError({
      message: `Unknown challenge proof field '${attr}'.`,
      rule: 'Challenge proofs only expose issued_at and expires_at fields.',
      fix: `Use ${objectType.challenge ? 'issued_at' : 'expires_at'} on the challenge proof.`,
      location: expr.location || findLocation(source, attr),
      context: formatContext(source, expr.location || findLocation(source, attr))
    }));
    return { type: 'any', isArray: false };
  }

  if (objectType.type === 'relation') {
    warnings.push(createError({
      message: `Attribute access '${expr.attribute}' cannot be validated on relation bindings yet.`,
      rule: 'Relation attribute schemas are not declared in the current DSL grammar.',
      fix: 'Add a relation attribute schema once supported, or validate this in application code.',
      location: expr.location || findLocation(source, expr.attribute),
      context: formatContext(source, expr.location || findLocation(source, expr.attribute))
    }));
    return { type: 'any', isArray: false };
  }

  const def = tables.definitions.get(objectType.type);
  if (!def) {
    errors.push(createError({
      message: `Cannot access attribute '${expr.attribute}' on unknown type '${objectType.type}'.`,
      rule: 'Attribute access requires a typed node definition.',
      fix: `Define type '${objectType.type}' with the desired fields.`,
      location: expr.location || findLocation(source, expr.attribute),
      context: formatContext(source, expr.location || findLocation(source, expr.attribute))
    }));
    return { type: 'any', isArray: false };
  }

  const field = (def.fields || []).find(f => f.name === expr.attribute);
  if (!field) {
    errors.push(createError({
      message: `Unknown field '${expr.attribute}' on type '${def.name}'.`,
      rule: 'Attribute access must reference a declared field.',
      fix: `Add field '${expr.attribute}' to type '${def.name}' or correct the attribute name.`,
      location: expr.location || findLocation(source, expr.attribute),
      context: formatContext(source, expr.location || findLocation(source, expr.attribute))
    }));
    return { type: 'any', isArray: false };
  }

  return {
    type: field.fieldType,
    isArray: !!field.isArray
  };
}

function extractTypeGuard(expr, scope, tables, errors, warnings, source, parent) {
  if (expr && expr.type === 'BinaryExpression' && expr.operator === 'is') {
    const targetPath = getExpressionPath(expr.left);
    const typeName = resolveTypeName(expr.right);
    if (targetPath && typeName && isTypeKnown(typeName, tables)) {
      return { targetPath, typeName };
    }
    return null;
  }
  const guardExpr = expr && expr.type === 'PredicateCall' ? expr : null;
  if (!guardExpr || guardExpr.name !== 'is_type') return null;
  const args = guardExpr.args || [];
  if (args.length !== 2) return null;
  const target = args[0];
  const typeArg = args[1];
  const targetPath = getExpressionPath(target);
  if (!targetPath) return null;
  const typeName = resolveTypeName(typeArg);
  if (!typeName || !isTypeKnown(typeName, tables)) return null;
  return { targetPath, typeName };
}

function resolveTypeName(expr) {
  if (!expr) return null;
  if (expr.type === 'TypeName') return expr.name;
  if (expr.type === 'Variable') return expr.name;
  if (expr.type === 'Literal' && typeof expr.value === 'string') return expr.value;
  return null;
}

function getExpressionPath(expr) {
  if (!expr) return null;
  if (expr.type === 'Variable') return expr.name;
  if (expr.type === 'AttributeAccess') {
    const base = getExpressionPath(expr.object);
    if (!base || !expr.attribute) return null;
    return `${base}.${expr.attribute}`;
  }
  return null;
}

function getScopeOverride(expr, scope) {
  const path = getExpressionPath(expr);
  if (!path) return null;
  const entry = scope.get(path);
  if (!entry) return null;
  return { type: entry.type, isArray: entry.isArray || false };
}

function resolveVariableType(expr, scope, errors, source) {
  const entry = scope.get(expr.name);
  if (!entry) {
    if (isChallengePredicateName(expr.name)) {
      errors.push(createError({
        message: `Challenge predicate '${expr.name}' must be prefixed with '!'.`,
        rule: 'Challenge predicates are only valid as !<name> in Evidence DSL expressions.',
        fix: `Rewrite '${expr.name}' as '!${expr.name}'.`,
        location: findLocation(source, expr.name),
        context: formatContext(source, findLocation(source, expr.name))
      }));
      return { type: 'any', isArray: false, name: expr.name };
    }
    errors.push(createError({
      message: `Unknown variable '${expr.name}'.`,
      rule: 'Variables must be declared in the current scope or bound by a pattern.',
      fix: 'Add the variable to the parameter list or bind it with a wildcard/pattern.',
      location: findLocation(source, expr.name),
      context: formatContext(source, findLocation(source, expr.name))
    }));
    return { type: 'any', isArray: false, name: expr.name };
  }
  return { type: entry.type, isArray: entry.isArray || false, name: expr.name };
}

function isChallengePredicateName(name) {
  return BUILTIN_CHALLENGES.has(name);
}

function buildParamScope(params, tables, errors, source, contextLabel) {
  const scope = new Map();
  for (const param of params || []) {
    if (!isTypeKnown(param.paramType, tables)) {
      errors.push(createError({
        message: `Unknown parameter type '${param.paramType}' in ${contextLabel}.`,
        rule: 'Parameter types must be built-in or declared as a definition.',
        fix: `Add a type definition for '${param.paramType}' or correct the parameter type.`,
        location: findLocation(source, param.paramType),
        context: formatContext(source, findLocation(source, contextLabel))
      }));
    }
    scope.set(param.name, { type: param.paramType, isArray: !!param.isArray });
  }
  return scope;
}

function resolvePredicateSignature(name, tables) {
  if (tables.facts.has(name)) {
    const fact = tables.facts.get(name);
    return {
      params: (fact.params || []).map(param => ({
        type: param.paramType,
        isArray: !!param.isArray
      })),
      returnType: { type: 'boolean', isArray: false }
    };
  }
  if (tables.evidence.has(name)) {
    const ev = tables.evidence.get(name);
    return {
      params: (ev.params || []).map(param => ({
        type: param.paramType,
        isArray: !!param.isArray
      })),
      returnType: { type: ev.provides || DEFAULT_EVIDENCE_RETURN, isArray: false }
    };
  }
  if (tables.measures.has(name)) {
    const measure = tables.measures.get(name);
    const returnType = measure.provides || DEFAULT_MEASURE_RETURN;
    return {
      params: (measure.params || []).map(param => ({
        type: param.paramType,
        isArray: !!param.isArray
      })),
      returnType: { type: returnType, isArray: false }
    };
  }
  if (tables.sources.has(name)) {
    const source = tables.sources.get(name);
    return {
      params: (source.params || []).map(param => ({
        type: param.paramType,
        isArray: !!param.isArray
      })),
      returnType: { type: source.provides || 'boolean', isArray: false },
      injectable: !!source.injectable,
      within: source.within || null
    };
  }
  return null;
}

function inferLiteralType(expr) {
  if (typeof expr.value === 'boolean') return { type: 'boolean', isArray: false };
  if (typeof expr.value === 'number') return { type: 'number', isArray: false };
  if (expr.unit) return { type: 'duration', isArray: false };
  if (typeof expr.value === 'string') return { type: 'string', isArray: false };
  return { type: 'any', isArray: false };
}

function isTypeKnown(type, tables) {
  if (!type) return false;
  if (BUILTIN_TYPES.has(type)) return true;
  return tables.definitions.has(type);
}

function isAssignable(actualType, expectedType, actualIsArray = false, expectedIsArray = false) {
  if (!expectedType || expectedType === 'any') return true;
  if (actualType === 'any') return true;
  if (actualIsArray !== expectedIsArray) return false;
  return actualType === expectedType;
}

function areComparableTypes(left, right) {
  if (!left || !right) return true;
  if (left.type === 'any' || right.type === 'any') return true;
  if (left.isArray || right.isArray) return false;
  return left.type === right.type;
}

function isNumberType(entry) {
  if (!entry) return true;
  return entry.type === 'number' || entry.type === 'any';
}

function isTimestampType(entry) {
  if (!entry) return true;
  return entry.type === 'timestamp' || entry.type === 'any';
}

function isDurationType(entry) {
  if (!entry) return true;
  return entry.type === 'duration' || entry.type === 'any';
}

function formatType(entry) {
  if (!entry) return 'unknown';
  const base = entry.type || 'unknown';
  return entry.isArray ? `${base}[]` : base;
}

function createError({ message, rule, fix, location, context, severity = 'error' }) {
  return { message, rule, fix, location, context, severity };
}

function formatValidationError(error) {
  const parts = [];
  if (error.location && error.location.start) {
    parts.push(`[${error.location.start.line}:${error.location.start.column}]`);
  }
  parts.push(error.message);
  if (error.rule) parts.push(`Rule: ${error.rule}`);
  if (error.fix) parts.push(`Fix: ${error.fix}`);
  if (error.context) parts.push(`Context: ${error.context}`);
  return parts.join(' ');
}

function formatPegError(error, sourceText, sourceName) {
  const expected = (error.expected || []).map(exp => exp.description || exp.text || exp.type || String(exp));
  const found = error.found === null ? 'end of input' : String(error.found);
  const location = error.location || null;
  const expectedStr = expected.length > 3 ? `${expected.slice(0, 3).join(', ')}, ...` : expected.join(' or ');

  let message = `Syntax error: unexpected ${found}`;
  let fix = expectedStr ? `Expected ${expectedStr}.` : 'Check the DSL syntax.';
  let rule = 'Statements must follow the Evidence DSL grammar.';

  if (expected.includes('"}"') || expected.includes('}')) {
    message = 'Missing closing brace.';
    fix = 'Add a closing "}" to end the block.';
    rule = 'Blocks must be closed with "}".';
  } else if (expected.includes('")"') || expected.includes(')')) {
    message = 'Missing closing parenthesis.';
    fix = 'Add a closing ")" to end the parameter list.';
    rule = 'Parameter lists must be closed with ")".';
  } else if (expected.includes('":"') || expected.includes(':')) {
    message = 'Missing colon after identifier.';
    fix = 'Add ":" between a name and its type.';
    rule = 'Types must be declared using name: Type syntax.';
  }

  return createError({
    message,
    rule,
    fix,
    location,
    context: formatContext(sourceText, location),
    severity: 'error',
    expected: expectedStr,
    found,
    source: sourceName
  });
}

function parsePrelude(options = {}) {
  if (options.includePrelude === false) return null;
  try {
    return parse(DSL_PRELUDE);
  } catch (error) {
    return null;
  }
}

function formatContext(sourceText, location) {
  if (!sourceText) return null;
  if (!location || !location.start) return null;
  const lines = sourceText.split('\n');
  const line = lines[location.start.line - 1];
  if (!line) return null;
  const pointer = ' '.repeat(Math.max(0, location.start.column - 1)) + '^';
  return `${line.trimEnd()}\n${pointer}`;
}

function findLocation(sourceText, needle) {
  if (!sourceText || !needle) return null;
  const lines = sourceText.split('\n');
  for (let i = 0; i < lines.length; i++) {
    const col = lines[i].indexOf(needle);
    if (col !== -1) {
      return {
        start: { line: i + 1, column: col + 1 },
        end: { line: i + 1, column: col + needle.length }
      };
    }
  }
  return null;
}