import { eqType } from "../primitives/type.js";
import { isTypeVar } from "../primitives/typevars.js";
import { prettyT } from "../util/pretty.js";
import { indent, zip } from "../util/util.js";
import { compareStrings } from "../compare/primitives.js";
import { getHumanReadableName } from "../primitives/symbol.js";
import { occurring, substitute } from "./generics.js";

export const prettyS = (typevar, type) => {
  return `${getHumanReadableName(typevar)} ↦ ${prettyT(type)}`;
}
export const prettySS = (rUni) => '{'+[...rUni].map(([symbol,type]) => `${prettyS(symbol,type)}`).join(', ')+'}';

export class IncompabibleTypesError extends Error {
  constructor(typeA, typeB, nestedErr) {
    const msg = `\nIncompatible types: ${prettyT(typeA)} and ${prettyT(typeB)}`;
    if (nestedErr) {
      super(msg + indent(nestedErr.message, 2));
    }
    else {
      super(msg);
    }
  }
}

export class SubstitutionCycle extends Error {
  constructor(typevar, type) {
    super(`\nSubstitution cycle: ${getHumanReadableName(typevar)} ↦ ${prettyT(type)}`);
  }
}

// pure
export const subsitutionsEqual = (m1,m2) => {
  if (m1.size !== m2.size ) return false;
  for (const [key1,type1] of m1) {
    if (!eqType(m2.get(key1))(type1)) return false;
  }
  return true;
};

// pure
// Partial ordering between types
//  - deep-equal types are equal (e.g., Int == Int)
//  - non-typevars are smaller than typevars (e.g., Int < a)
//  - typevars with smaller letters are smaller (e.g., a < b)
//  - if the symbols match, and if an ordering exists between all the parameters, then we take the ordering of the first non-equal parameter (e.g., (a,Int) < (b,Int))
// returns: Ordering | undefined
const partialCompareTypes = (typeA, typeB) => {
  if (isTypeVar(typeA)) {
    if (isTypeVar(typeB)) {
      return compareStrings(typeA.symbol)(typeB.symbol);
    }
    if (!isTypeVar(typeB)) {
      return 1;
    }
  }
  if (isTypeVar(typeB)) {
    // console.log(typeB, 'is a typevar');
    return -1; // typeB is typevar, typeA is not
  }

  if (typeA.symbol === typeB.symbol) {
    let result = 0;
    for (const [paramA, paramB] of zip(typeA.params, typeB.params)) {
      const paramCmp = partialCompareTypes(paramA(typeA), paramB(typeB));
      if (paramCmp === undefined) return; // no ordering
      result ||= paramCmp;
    }
    return result;
  }
}

// pure
const checkCycle = (typevar, type) => {
  if (occurring(type).has(typevar)) {
    throw new SubstitutionCycle(typevar, type);
  }
}

// impure, modifies 'substitutions'
const addReduce = (substitutions, typevar, type) => {
  // console.log('add ', prettyS(typevar, type));
  substitutions.set(typevar, type);
}

// impure, modifies 'substitutions'
const attemptReduce = (substitutions, typevar, type) => {
  // assuming 'substitutions' is already reduced as much as possible,
  // substitute all typevars in our type with the existing substitutions
  const substType = substitute(type, substitutions);
  // Check for cycles. For instance, the substitution
  //    a ↦ [a]
  // is forbidden. Not sure if this is too strict, because on the other hand, we do support recursive types...
  checkCycle(typevar, substType);
  const overlappingType = substitutions.get(typevar);
  if (overlappingType) {
    const uni = unify(overlappingType, substType);
    for (const [typevar, type] of uni) {
      attemptReduce(substitutions, typevar, type);
    }
    const cmp = partialCompareTypes(substType, overlappingType);
    if (cmp === -1) {
      // our type "wins" (smaller than the existing type)
      addReduce(substitutions, typevar, substType);
    }
    else {
      // other type "wins" -> don't do anything
    }
  }
  else {
    // no overlap
    addReduce(substitutions, typevar, substType);
  }
}

// pure
export const mergeSubstitutionsN = (substs) => {
  return substs.reduce((acc, cur) => {
    return mergeSubstitutions2(acc, cur);
  }, new Map());
}

// pure
const mergeSubstitutions2 = (substA, substB) => {
  const result = new Map(substA);
  for (const [typevarB, typeB] of substB) {
    attemptReduce(result, typevarB, typeB);
  }
  return result;
}

// pure
export const unify = (typeA, typeB) => {
  try {
    if (isTypeVar(typeA)) {
      if (isTypeVar(typeB)) {
        const cmp = partialCompareTypes(typeA, typeB);
        if (cmp === -1) {
          // console.log(prettyT(typeA), 'is smaller than', prettyT(typeB));
          return new Map([[typeB.symbol, typeA]]);
        }
        if (cmp === 1) {
          // console.log(prettyT(typeB), 'is smaller than', prettyT(typeA));
          return new Map([[typeA.symbol, typeB]]);
        }
        return new Map(); // typevars are equal
      }
      // A is typevar, B is not
      checkCycle(typeA.symbol, typeB);
      return new Map([[typeA.symbol, typeB]]);
    }
    if (isTypeVar(typeB)) {
      // B is typevar, A is not
      checkCycle(typeB.symbol, typeA);
      return new Map([[typeB.symbol, typeA]]);
    }

    // A and B are not typevars
    if (typeA.symbol !== typeB.symbol) {
      throw new IncompabibleTypesError(typeA, typeB);
    }

    const subs = zip(typeA.params, typeB.params)
    .map(([getParamA, getParamB]) => {
      const paramA = getParamA(typeA);
      const paramB = getParamB(typeB);
      // console.log('request...');
      return unify(paramA, paramB);
    });
    return mergeSubstitutionsN(subs);
  }
  catch (e) {
    if (e instanceof SubstitutionCycle) {
      throw new IncompabibleTypesError(typeA, typeB, e);
    }
    if (e instanceof IncompabibleTypesError) {
      // nest errors to get a nice trace of what went wrong
      throw new IncompabibleTypesError(typeA, typeB, e);
    }
    throw e;
  }
};