// src/utils/ast.js

// Function to create a new AST node
function Node(type, value, left, right) {
    return {
      type: type,
      value: value,
      left: left,
      right: right 
    };
}

const precedence = {
  'imply': 1,
  'or': 2,
  'and': 3,
  'not': 4,
  'symbol': 5,
  'true': 5,
  'false': 5
};

function astsToString(nodes){
    const leftList = nodes[0];
    const rightList = nodes[1];

    if (leftList.length > 0) {
        const leftFormulas = leftList.map(ast => astToString(ast)).join(",");
        const rightFormulas = rightList.map(ast => astToString(ast)).join(",");
        return `${leftFormulas}|-${rightFormulas}`;
    }

    const rightFormulas = rightList.map(ast => astToString(ast)).join(",");

    return `|-${rightFormulas}`;
}

function astToString(node, parentPrecedence = 0) {
  if (!node) return "";

  let currentPrecedence = precedence[node.type];

  let left = astToString(node.left, currentPrecedence);
  let right = astToString(node.right, currentPrecedence);

  let result;
  switch (node.type) {
      case 'not':
          result = `!${left}`;
          break;
      case 'and':
          result = `${left}&${right}`;
          break;
      case 'or':
          result = `${left}||${right}`;
          break;
      case 'imply':
          result = `${left}->${right}`;
          break;
      case 'symbol':
          result = node.value;
          break;
      case 'true':
          result = 'true';
          break;
      case 'false':
          result = 'false';
          break;
      default:
          throw new Error(`Unknown node type: ${node.type}`);
  }

  if (currentPrecedence < parentPrecedence) {
      result = `(${result})`;
  }

  return result;
}

// nodes are [[ast],[ast]]
function astsToLateX(nodes) {
    const leftList = nodes[0];
    const rightList = nodes[1];


    if (leftList.length > 0) {
        const leftFormulas = leftList.map(ast => astToLaTeX(ast)).join(", ");
        const rightFormulas = rightList.map(ast => astToLaTeX(ast)).join(", ");
        return `${leftFormulas} \\vdash ${rightFormulas}`;
    }

    const rightFormulas = rightList.map(ast => astToLaTeX(ast)).join(", ");

    return `\\vdash ${rightFormulas}`;
}

function astToLaTeX(node, parentPrecedence = 0) {
    if (!node) return "";

    let currentPrecedence = precedence[node.type];

    let left = astToLaTeX(node.left, currentPrecedence);
    let right = astToLaTeX(node.right, currentPrecedence);

    let result;
    switch (node.type) {
        case 'not':
            result = `\\neg ${left}`;
            break;
        case 'and':
            result = `${left} \\land ${right}`;
            break;
        case 'or':
            result = `${left} \\lor ${right}`;
            break;
        case 'imply':
            result = `${left} \\rightarrow ${right}`;
            break;
        case 'symbol':
            result = `\\mathit{${node.value}}`;
            break;
        case 'true':
            result = '\\top';
            break;
        case 'false':
            result = '\\bot';
            break;
        default:
            throw new Error(`Unknown node type: ${node.type}`);
    }

    if (currentPrecedence < parentPrecedence) {
        result = `(${result})`;
    }

    return result;
}


  
var ast = {};
ast.Not = Node.bind(null, 'not');
ast.And = Node.bind(null, 'and');
ast.Or = Node.bind(null, 'or');
ast.Imply = Node.bind(null, 'imply');
ast.Symbol = Node.bind(null, 'symbol');
ast.True = Node.bind(null, 'true');
ast.False = Node.bind(null, 'false');
ast.astToString = astToString;
ast.astToLaTeX = astToLaTeX;
ast.astsToLateX = astsToLateX;
ast.astsToString = astsToString;

module.exports = ast; // Export the AST module