Algorithm implementation to convert propositional formula into conjunctive normal form in JavaScript?

I saw How to convert a propositional formula to conjunctive normal form (CNF)? but it doesn’t go into implementation details. So I was lucky to find this which shows the types:

abstract class Formula { }
class Variable extends Formula { String varname; }
class AndFormula extends Formula { Formula p; Formula q; }  // conjunction
class OrFormula extends Formula { Formula p; Formula q; }  // disjunction
class NotFormula extends Formula { Formula p; } // negation
class ImpliesFormula extends Formula { Formula p; Formula q; } // if-then
class EquivFormula extends Formula { Formula p; Formula q; }
class XorFormula extends Formula { Formula p; Formula q; }

Then it has this helpful (start of a) function CONVERT:

CONVERT(φ):   // returns a CNF formula equivalent to φ

// Any syntactically valid propositional formula φ must fall into
// exactly one of the following 7 cases (that is, it is an instanceof
// one of the 7 subclasses of Formula).

If φ is a variable, then:
  return φ.
  // this is a CNF formula consisting of 1 clause that contains 1 literal

If φ has the form P ^ Q, then:
  CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
  CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
  where all the Pi and Qi are disjunctions of literals.
  So return P1 ^ P2 ^ ... ^ Pm ^ Q1 ^ Q2 ^ ... ^ Qn.

If φ has the form P v Q, then:
  CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
  CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
  where all the Pi and Qi are dijunctions of literals.
  So we need a CNF formula equivalent to
      (P1 ^ P2 ^ ... ^ Pm) v (Q1 ^ Q2 ^ ... ^ Qn).
  So return (P1 v Q1) ^ (P1 v Q2) ^ ... ^ (P1 v Qn)
          ^ (P2 v Q1) ^ (P2 v Q2) ^ ... ^ (P2 v Qn)
            ...
          ^ (Pm v Q1) ^ (Pm v Q2) ^ ... ^ (Pm v Qn)

If φ has the form ~(...), then:
  If φ has the form ~A for some variable A, then return φ.
  If φ has the form ~(~P), then return CONVERT(P).           // double negation
  If φ has the form ~(P ^ Q), then return CONVERT(~P v ~Q).  // de Morgan's Law
  If φ has the form ~(P v Q), then return CONVERT(~P ^ ~Q).  // de Morgan's Law

If φ has the form P -> Q, then:
  Return CONVERT(~P v Q).   // equivalent

If φ has the form P <-> Q, then:
  Return CONVERT((P ^ Q) v (~P ^ ~Q)).

If φ has the form P xor Q, then:
  Return CONVERT((P ^ ~Q) v (~P ^ Q)).

I translated it to JavaScript below, but am stuck on the AND and OR bits. I want to make sure I get this correct too.

The description of my “data model” / data structure is here.

/*
 * Any syntactically valid propositional formula φ must fall into
 * exactly one of the following 7 cases (that is, it is an instanceof
 * one of the 7 subclasses of Formula).
 *
 * @see https://www.cs.jhu.edu/~jason/tutorials/convert-to-CNF.html
 */

function convert(formula) {
  switch (formula.type) {
    case 'variable': return formula
    case 'conjunction': return convertConjunction(formula)
    case 'disjunction': return convertDisjunction(formula)
    case 'negation': return convertNegation(formula)
    case 'conditional': return convertConditional(formula)
    case 'biconditional': return convertBiconditional(formula)
    case 'xor': return convertXOR(formula)
    default:
      throw new Error(`Unknown formula type ${formula.type}.`)
  }
}

function convertConjunction(formula) {
  // CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
  // CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
  // where all the Pi and Qi are disjunctions of literals.
  // So return P1 ^ P2 ^ ... ^ Pm ^ Q1 ^ Q2 ^ ... ^ Qn.
}

function convertDisjunction(formula) {
  // CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
  // CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
  // where all the Pi and Qi are dijunctions of literals.
  // So we need a CNF formula equivalent to
  //    (P1 ^ P2 ^ ... ^ Pm) v (Q1 ^ Q2 ^ ... ^ Qn).
  // So return (P1 v Q1) ^ (P1 v Q2) ^ ... ^ (P1 v Qn)
  //         ^ (P2 v Q1) ^ (P2 v Q2) ^ ... ^ (P2 v Qn)
  //           ...
  //         ^ (Pm v Q1) ^ (Pm v Q2) ^ ... ^ (Pm v Qn)
}

function convertNegation(formula) {
  // If φ has the form ~(...), then:
  //   If φ has the form ~A for some variable A, then return φ.
  //   If φ has the form ~(~P), then return CONVERT(P).           // double negation
  //   If φ has the form ~(P ^ Q), then return CONVERT(~P v ~Q).  // de Morgan's Law
  //   If φ has the form ~(P v Q), then return CONVERT(~P ^ ~Q).  // de Morgan's Law
}

function convertConditional(formula) {
  // Return CONVERT(~P v Q).   // equivalent
  return convert({
    type: 'disjunction',
    base: {
      type: 'negation',
      formula: formula.base,
    },
    head: formula.head
  })
}

function convertBiconditional(formula) {
  // Return CONVERT((P ^ Q) v (~P ^ ~Q)).
  return convert({
    type: 'disjunction',
    base: {
      type: 'conjunction',
      base: formula.base,
      head: formula.head,
    },
    head: {
      type: 'conjunction',
      base: {
        type: 'negation',
        formula: formula.base,
      },
      head: {
        type: 'negation',
        formula: formula.head,
      },
    }
  })
}

function convertXOR(formula) {
  // CONVERT((P ^ ~Q) v (~P ^ Q)).
  return convert({
    type: 'disjunction',
    base: {
      type: 'conjunction',
      base: formula.base,
      head: {
        type: 'negation',
        formula: formula.head,
      },
    },
    head: {
      type: 'conjunction',
      base: {
        type: 'negation',
        formula: formula.base,
      },
      head: formula.head,
    }
  })
}

I have the AND and OR as a pair. So if you write in math like this:

A ∧ B ∧ C ∧ D ∧ E

That would be more like this in code:

A ∧ (B ∧ (C ∧ (D ∧ E)))

But the problem is, we might have arbitrary trees of formulas:

(((A ∧ B) ∧ (C ∧ D)) ∧ (E ∧ F))

Same with the OR. So how would you implement these functions convertDisjunction and convertConjunction, so they can handle that sort of tree data structure?

So what I would do is this:

function convertConjunction(formula) {
  let convertedBase
  if (formula.base.type === 'conjunction') {
    convertedBase = convertConjunction(formula.base)
  }
  let convertedHead
  if (formula.head.type === 'conjunction') {
    convertedHead = convertConjunction(formula.head)
  }
  ???
  // CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
  // CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
  // where all the Pi and Qi are disjunctions of literals.
  // So return P1 ^ P2 ^ ... ^ Pm ^ Q1 ^ Q2 ^ ... ^ Qn.
}

I get lost right at the beginning.