import { inspect } from "node:util";
import { inspectType, makeTypeConstructor } from "../meta/type_constructor.js";
import { getSymbol } from "../primitives/type.js";
import { isTypeVar, TYPE_VARS, UNBOUND_SYMBOLS } from "../primitives/typevars.js";
import { symbolFunction } from "../structures/type_constructors.js";
import { prettyT } from '../util/pretty.js';
import { reduceUnification, unifyLL } from "./low_level.js";

// helper for creating generic types
//   for instance, the type:
//     a -> a -> Bool
//   is created by
//     makeGeneric(a => fnType(() => a)(() => fnType(() => a)(() => Bool)))
export const makeGeneric = callback => {
  // type variables to make available:
  const type = callback(...TYPE_VARS);
  return type;
};

const _occurring = stack => type => {
  if (isTypeVar(type)) {
    return new Set([getSymbol(type)]);
  }
  const tag = stack.length;
  const newStack = [...stack, tag];
  return new Set(type.params.flatMap(p => {
    const innerType = p(tag);
    if (newStack.includes(innerType)) {
      return []; // no endless recursion!
    }
    return [..._occurring(newStack)(innerType)]; 
  }));
};

// Get set of type variables in type.
export const occurring = _occurring([]);

export class UnifyError extends Error {}
export class NotAFunctionError extends Error {}

export const unify = (fType, aType) => {
  [fType, aType] = recomputeTypeVars([fType, aType]);
  const unification = unifyLL(fType, aType);
  const substitutions = reduceUnification(unification);
  const uType = substitute(fType, // or aType, doesn't matter here
    substitutions);
  return recomputeTypeVars([uType])[0];
};

export const substitute = (type, substitutions, stack=[]) => {
  // console.log('substitute...', {type, substitutions, stack});
  const found = substitutions.get(getSymbol(type));
  if (found) {
    return found;
  }
  return {
    symbol: getSymbol(type),
    params: type.params.map(getParam => parent => {
      const param = getParam(parent);
      if (stack.includes(param)) {
        // param points back up - that's ok - means we don't have to recurse
        return param;
      }
      return substitute(param, substitutions, [...stack, parent]);
    }),
    [inspect.custom]: inspectType,
  };
};

export const assignFn = (funType, paramType, skip=0) => {
  // Precondition
  if (getSymbol(funType) !== symbolFunction) {
    throw new NotAFunctionError(`${prettyT(funType)} is not a function type!`);
  }

  // Step 1: Very important: Function and parameter type may have overlapping type variables, so we recompute them to make them non-overlapping:
  const [funType1, paramType1] = recomputeTypeVars([funType, paramType]);

  // Step 2: Get input and output type of function
  const [inType1, outType1] = funType1.params.map(p => p(funType1));

  // Step 3: Unify parameter type with input type
  const unifInType1 = unifyLL(inType1, paramType1);

  // Step 4: Substitute typevars in output type
  const substInType1 = reduceUnification(unifInType1);
  const reducedOutType1 = substitute(outType1, substInType1);

  // Step 5: 'Normalize' output type
  const [outType] = recomputeTypeVars([reducedOutType1], skip);
  return outType;
}

// Ensures that no type variables overlap
export const recomputeTypeVars = (types, skip=0) => {
  return recomputeTypeVarsWithInverse(types, skip)[0];
};

export const recomputeTypeVarsWithInverse = (types, skip=0) => {
  let nextIdx = skip;
  const inverse = new Map();
  return [types.map(type => {
      const substitutions = new Map();
      const typeVars = occurring(type);
      for (const typeVar of typeVars) {
        const idx = nextIdx++;
        if (typeVar !== UNBOUND_SYMBOLS[idx]) {
          substitutions.set(typeVar, TYPE_VARS[idx]);
          inverse.set(UNBOUND_SYMBOLS[idx], typeVar);
        }
      }
      return substitute(type, substitutions);
    }), inverse];
}