mm-calc.user.js

// ==UserScript==
// @name     mm-calc
// @description  Make `metamath /html' proofs look more like calculations.  (License: public domain; initial author: Marnix Klooster <[email protected]>.)
// @version  3
// @grant    none
// @include  /^https?://.*\.metamath\.org(:\d+)?/[^/]*/[^/]*.html(#.*)?$/
// @require  https://code.jquery.com/jquery-3.3.1.slim.min.js
// ==/UserScript==

// Mark all proof-like tables with class 'proof'
$(function() {
    $('table:has(> tbody > tr > th:contains("Step"))').addClass("proof");
});


// Collapsing proofs parts
jQuery.prototype.calcant = function() {
    var selector = $('#nonexistingwhatever');
    var proofStep = $(this);
    var a = proofStep.attr('data-calcants');
    if (a) {
        $.each(JSON.parse(a), function(i, calcAnt) {
            selector = selector.add(proofStep.parents().find("tr[data-step=" + String(calcAnt) + "]"));
        });
    }
    return $(selector);
}

jQuery.prototype.collapse = function() {
    $(this).each(function() {
        $(this).addClass('collapsed');
        $(this).calcant().collapse();
    });
}

jQuery.prototype.expand = function() {
    $(this).each(function() {
        $(this).removeClass('collapsed');
        $(this).filter(":not(.ant-collapsed)").calcant().expand();
    });
}



// Highlighting antecedents

jQuery.prototype.ant = function() {
    var selector = $('#nonexistingwhatever');
    var proofStep = $(this);
    var calcAnts = proofStep.attr('data-calcants');
    if (calcAnts) {
        $.each(JSON.parse(calcAnts), function(i, ant) {
            selector = selector.add(proofStep.parents().find("tr[data-step=" + String(ant) + "]"));
        });
    }
    return $(selector);
}

function hant(elt) {
    elt.toggleClass('hstmt');
    elt.ant().toggleClass('hant');
};

$(function() {
    $('.proof tr td').wrapInner('<div />');
    $('.proof tr').mouseenter(function() {
        hant($(this));
    });
    $('.proof tr').mouseleave(function() {
        hant($(this));
    });
});



// calculate new indentations and remove old, set attributes data-indent, data-ant, and data-calcants on <tr>
$(function() {
    $('.proof').each(function() {
        proofTable = $(this);

        // a stack containing the proof steps
        var stepStack = [];

        function removeCalcAntsOf(proofTable, stepNumber) {
                var proofStep = proofTable.find('tr[data-step="' + String(stepNumber) + '"]');
                var result = JSON.parse(proofStep.attr('data-calcants'));
                proofStep.attr('data-calcants', JSON.stringify([]));
                return result;
            }
            // for every row (i.e., proof step): process it
        proofTable.find('> tbody > tr').each(function() {
            if ($(this).find('td').length == 0) return;

            // extract level and step number, remove indentation
            var stepNumber = Number($(this).find('td:first').text());
            $(this).attr('data-step', String(stepNumber));
            var levelSpan = $(this).find('td:last span.i');
            var level = Number(levelSpan.text().replace(/^(\. )*/, ''));
            $(this).attr('data-level', String(level));

            // perform proof step (pop and push), store Metamath antecedents step numbers
            var ants = [];
            while (stepStack.length > 0 && stepStack[0].level > level) {
                ants.unshift(stepStack[0].stepNumber);
                stepStack.shift();
            }
            stepStack.unshift({
                level: level,
                stepNumber: stepNumber
            });
            $(this).attr('data-ants', JSON.stringify(ants));

            // the 'indent' is the number of steps left on the stack (minus 1)
            var indent = String(stepStack.length - 1);
            $(this).attr('data-indent', indent);

            // calculate 'calculational antecedents' (TODO: explain better)
            var calcAnts = ants;
            if (ants.length > 0) {
                calcAnts = [ants[0]].concat(removeCalcAntsOf(proofTable, ants[0]), ants.slice(1));
            }
            $(this).attr('data-calcants', JSON.stringify(calcAnts));
        });

        // change indent to data-indent
        proofTable.find('> tbody > tr').each(function() {
            if ($(this).find('td').length == 0) return;
            //var stepNumber = $(this).attr('data-step');
            //console.log('stepNumber: ' + JSON.stringify(stepNumber));
            var levelSpan = $(this).find('td:last span.i');
            var levelString = $(this).attr('data-level');
            var indent = Number($(this).attr('data-indent'));
            levelSpan.parents().css('padding-left', String(indent * 4) + 'ex');
            levelSpan.text(levelString);
        });

        // styling: hide 'collapsed' and to show 'tree icons' for data-calcants!='[]'
        // (inspired by Thierry's http://metamath.tirix.org/hant.css)
        $('head').append("<style> \
  .collapsed td { display:none; } \
  .collapsed td { border-width: 0px; padding: 0px; transition: all .5s ease; } \
  tr[data-calcants] > td:first-child { text-align: right; } \
  \
  tr[data-ants='[]'] > td { padding-top: 1ex; } \
  tr[data-calcants]:not([data-calcants='[]']).ant-collapsed > td { padding-top: 1ex; } \
  tr[data-calcants]:not([data-calcants='[]']) > td { padding-bottom: 1ex; } \
  \
  tr[data-calcants='[]'] > td:first-child:before { content: ''; } \
  tr[data-calcants]:not([data-calcants='[]']).ant-collapsed > td:first-child > div:first-child:before { content: '> '; } \
  tr[data-calcants]:not([data-calcants='[]']):not(ant-collapsed) > td:first-child > div:first-child:before { content: '^ '; } \
  tr.hant { background-color: #D0F0FF !important; } \
  tr.hstmt { background-color: #C0D0FF !important; } \
      </style>");

        // make 'tree icons' clickable, and initially collapsed
        proofTable.find('> tbody > tr[data-calcants]:not([data-calcants="[]"])').each(function() {
            if ($(this).find('td').length == 0) return;

            function onClickTreeIcon() {
                if ($(this).hasClass('ant-collapsed')) $(this).calcant().expand();
                else $(this).calcant().collapse();
                $(this).toggleClass('ant-collapsed');
            }
            $(this).click(onClickTreeIcon);
            onClickTreeIcon.call(this);
        });

        // expand only top level initially
        proofTable.find('> tbody > tr[data-calcants]:not([data-calcants="[]"]):last').each(function() {
            $(this).trigger('click');
        });
    });
});

mm-calc2.user.js

// ==UserScript==
// @name     mm-calc2
// @description  Replace `metamath /html' proof tables by calculations.  (License: public domain; initial author: Marnix Klooster <[email protected]>.)
// @version  10
// @grant    none
// @run-at   document-start
// @include  /^https?://.*\.metamath\.org(:\d+)?/[^/]*/[^/]*.html(#.*)?$/
// @include  /^https?://metamath\.tirix\.org(:\d+)?/[^/]*.html(#.*)?$/
// @require  https://code.jquery.com/jquery-3.5.1.slim.min.js
// ==/UserScript==

/*
TODO:

- Move referredStepNumbers to separate calculations at the bottom.

- Some kind of 'tabs' to switch between the different views?

- Button to interactively move a subproof to the 'spine position'?
  That way the user can correct incorrect guesses by guessMainSubproof() below.

*/

$(function() {
	// mark all proof-like tables with class 'proofTable'
	$('table:has(> tbody > tr > th:contains("Step"))').addClass("proofTable");

  $('.proofTable').each(function() {
    var proofTable = $(this);
		var proofTableBody = proofTable.find('> tbody');

    // parse table into proof tree
    var stepsByNumber = {};
    var referredStepNumbers = [];

    var subproofStack = [];
    proofTableBody.find('> tr:not(:has(th))').each(function() {
      var stepRow = $(this);

      var stepNumber = Number(stepRow.find('> td:nth-child(1)').text());
      var substepNumbers = stepRow.find('> td:nth-child(2)').text().trim().split(/\s*,\s*/).filter(s => s !== '').map(Number);
      var refHTML = stepRow.find('> td:nth-child(3)').html();
      var lastColumn = stepRow.find('> td:nth-child(4)');
      var expressionHTML = lastColumn.find('> span.math, > span:has(> svg)').html();
      var expressionText = lastColumn.find('> span.math, > span:has(> svg)').text();

      var level = Number(lastColumn.find('> span.i').text().replace(/(\. )*/, ''));
      var step = {number:stepNumber, refHTML:refHTML, expressionHTML:expressionHTML, expressionText:expressionText, substepNumbers:substepNumbers};
      ///console.log(JSON.stringify(step, null, 2));
      stepsByNumber[stepNumber] = step;

      // perform proof step (pop and push), store Metamath antecedents/subproofs
      ///console.log('expected step numbers: ' + JSON.stringify(substepNumbers));
      var j = substepNumbers.length - 1;
      var stepSubproofs = [];
      while (true) {
        var substepNumberOnStack = subproofStack.length == 0 || subproofStack[0].level <= level ? null : subproofStack[0].subproof.step.number;
        while (0 <= j) {
          var substepNumber = substepNumbers[j--];
          if (substepNumberOnStack === substepNumber) break;
          ///console.log("In step " + step.number.toString() + " skipping substep " + JSON.stringify(stepsByNumber[substepNumber]));
          var r = substepNumber.toString();
          if (stepsByNumber[substepNumber].substepNumbers.length == 0) {
            r = stepsByNumber[substepNumber].refHTML;
          } else {
            referredStepNumbers.push(substepNumber);
          }
          var e = stepsByNumber[substepNumber].expressionHTML;
          var et = stepsByNumber[substepNumber].expressionText;
          stepSubproofs.unshift({step:{number:substepNumber, refHTML:r, expressionHTML:e, expressionText:et, substepNumbers:[]}, subproofs:[]});
        }
        if (substepNumberOnStack === null) break;
        stepSubproofs.unshift(subproofStack[0].subproof);
        subproofStack.shift();
      }
      subproofStack.unshift({level:level, subproof:{step:step, subproofs:stepSubproofs}});
    });
    // we assume that subproofStack.length == 1 at this point

    var proof = subproofStack[0].subproof;
    ///console.log(JSON.stringify(proof, null, 2));
    ///console.log(JSON.stringify(referredStepNumbers));

    // add the calculation next to the table
    var calculation = renderCalculation(proof, referredStepNumbers, 'ROOT');
    calculation.prepend(proofTable.find('> caption').clone());
 		insertCalculation(proofTable, calculation);
  });
  console.log('Success rendering calculations!');
});

$(function() {
  $('head').append("<style> \
    .calc { border-left:1px solid #FFA500; border-top:1px solid #FFA500; border-bottom:1px solid #FFA500; padding-right: 2ex;} \
    .calcOp { text-align: right; } \
    .calc .calc, .calcHint { margin-left: 2ex; } \
    .calcSmallStep { opacity: 0.3; } \
	");
  console.log('Success inserting styles!');
});

function guessMainSubproof(c, referredStepNumbers) {
  // determine which subproof is part of the 'spine': roughly the one 'most like the conclusion'.
  // the measure is the length of the 'longest common subsequence',
  // or rather, the difference in length of the non-common parts.
  var subproofNr = null;
  var minIsTrivial = false;
  var minDiffLengthDiff = 9999999;
  var i;
  for (i = 0; i < c.subproofs.length; i++) {
    if (referredStepNumbers.includes(c.subproofs[i].step.number)) {
      // assume a 'shared' step is auxiliary?? if so, here we should continue;
    }

    var subproofText = c.subproofs[i].step.expressionText;
    var conclusionText = c.step.expressionText;
    var l = mostly_longest_common_subsequence_length(subproofText, conclusionText);
    // see https://math.stackexchange.com/q/495137/11994 for the following comparison function
    var diffLengthDiff = Math.log2((subproofText.length - l + 1) / (conclusionText.length - l + 1));
    var subproofIsTrivial = (c.subproofs[i].subproofs.length == 0);
    console.log(JSON.stringify([c.step.number, c.subproofs[i].step.number, l, conclusionText.length - l, subproofText.length - l, diffLengthDiff, subproofIsTrivial]));

    if (Math.abs(Math.abs(minDiffLengthDiff) - Math.abs(diffLengthDiff)) <= 0.2 && !subproofIsTrivial && !minIsTrivial) {
      // if multiple non-trivial subproofs have similar diffLengthDiff, choose neither.
      subproofNr = null;
    } else if (Math.abs(diffLengthDiff) < Math.abs(minDiffLengthDiff)) {
      subproofNr = i;
    }
    if (Math.abs(diffLengthDiff) < Math.abs(minDiffLengthDiff)) {
      minDiffLengthDiff = diffLengthDiff;
      minIsTrivial = subproofIsTrivial;
    }
  }
  var stepDescription = (subproofNr === null ? "none" : c.subproofs[subproofNr].step.number.toString());
  console.log("(done, chosen "+stepDescription+" for " + c.step.refHTML + ")");
  var stepIsSmall = c.subproofs.length == 1 && minDiffLengthDiff <= 2; // here be magic
  return {subproofNr: subproofNr, stepIsSmall: stepIsSmall};
}

function renderCalculation(proof, referredStepNumbers, parentCalcId) {

  // build up a table from the bottom up, looping over the 'spine'
  var table = []
  var calcId = proof.step.number.toString();
  var c = proof;
  var nextStepIsSmall = false;
  while (c.subproofs.length >= 1) {
    // the result expression of the current proof
    var l = referredStepNumbers.includes(c.step.number) ? $('<span>').append('('+c.step.number.toString()+')') : null;
    table.push({rightClass:'calcExpression' + (nextStepIsSmall ? ' calcSmallStep' : ''), leftHTML:l, rightHTML:c.step.expressionHTML});

    // determine which subproof is part of the 'spine' (can be null!)
    var guess = guessMainSubproof(c, referredStepNumbers);
    var subproofNr = guess.subproofNr;
    nextStepIsSmall = guess.stepIsSmall;

    // calculate and show the hint
    var refHTMLs = [];
    var nrSubcalcs = 0;
    var i;
    for (i = c.subproofs.length-1; i >= 0; i--) {
      if (i == subproofNr) continue;
      var subproof = c.subproofs[i];
      if (subproof.subproofs.length == 0 ) {
        refHTMLs.push(subproof.step.refHTML);
        // we don't render the single-step proof's expressionHTML, assuming it is obvious
      } else {
        nrSubcalcs += 1;
      }
    }
    table.push({rightClass:'calcHint' + (nextStepIsSmall ? ' calcSmallStep' : ''),
                leftHTML:$('<div>').addClass('calcOp').addClass(nextStepIsSmall ? 'calcSmallStep' : '').append($('<span style="font-family: XITSMath-Regular">').text('⇐')),
                rightHTML:renderHint(c.step.refHTML, refHTMLs, nrSubcalcs)});

    // add all other subproofs (recursively), indented
    if (c.subproofs.length > 1) {
      table.push({rightClass:'calcSpacer', leftHTML:null, rightHTML:null});
      var i;
      for (i = c.subproofs.length-1; i >= 0; i--) {
        if (i == subproofNr) continue;
        var subproof = c.subproofs[i];
        if (subproof.subproofs.length != 0 ) {
          table.push({rightClass:'calcSubproof', leftHTML:null, rightHTML:renderCalculation(subproof, referredStepNumbers, calcId)});
      		table.push({rightClass:'calcSpacer', leftHTML:null, rightHTML:null});
        }
      }
    }

    // ...and on to the next proof on the 'spine', higher in the calculation
    if (subproofNr === null) {
      c = null;
      break;
    }
    c = c.subproofs[subproofNr];
  }
  if (c !== null) {
	  table.push({rightClass:(nextStepIsSmall ? 'calcSmallStep' : ''), leftHTML:$('<span>').append('(').append(c.step.refHTML).append(')'), rightHTML:c.step.expressionHTML});
  } else {
	  table.push({leftHTML:null, rightHTML:'TRUE'});
  }
  if (parentCalcId != 'ROOT') {
    table.push({leftHTML:$('<button class="calcExpander">').text('...'), rightHTML:null});
  }

  // render the table to HTML
  var result = $('<table/>').addClass('calc');
  $.each(table, function(i,r) {
    result.append($('<tr/>')
      .append($('<td/>').html(r.leftHTML))
      .append($('<td/>').addClass(r.rightClass).html(r.rightHTML)));
  });
  return result;
}

function renderHint(refHTML, refHTMLs, nrSubcalcs) {
  var result = $('<span/>').addClass('calcHint').append('“using '); //TOOD replace spaces by CSS
  var htmls = refHTMLs.slice();
  if (nrSubcalcs == 1) { htmls.push('subproof'); }
  else if (nrSubcalcs > 1) { htmls.push('subproofs'); }
  htmls.push(refHTML);
  if (htmls.length > 0) {
    result.append(renderSeq(htmls));
  }
  result.append('”');
  return result;
}

function renderSeq(htmls) {
  if (htmls.length == 0) {
    return null;
  } else if (htmls.length == 1) {
    return htmls[0];
  } else if (htmls.length == 2) {
    return $('<span/>').append(htmls[0]).append(' and ').append(htmls[1]);
  } else {
    var result = $('<span/>');
    $.each(htmls.slice(0,-1), function(i, html) {
      result.append(html).append(', ');
    });
    result.append('and ').append(htmls.slice(-1));
    return result;
  }
}

function insertCalculation(proofTable, calculation) {
  // TODO: allow to switch between the table and the calculation
  proofTable.before(calculation);
}

// currently not used, but it is a possible alternative
// for mostly_longest_common_subsequence_length()
function number_of_common_characters(x,y) {
    var yy = y.split(''); // convert y to array of characters
    var result = x.length;
    var i;
    for (i = 0; i < x.length; i++) {
        var p = yy.indexOf(x[i]);
        if (p == -1) {
            result -= 1;
        } else {
            yy[p] = null;
        }
    }
    return result;
}

// copied (and slightly modified) from lcs_greedy()
// from https://rosettacode.org/wiki/Longest_common_subsequence#Greedy_Algorithm
function mostly_longest_common_subsequence_length(x,y){
  var p1, i, idx,
      symbols = {},
      r = 0,
      p = 0,
      l = 0,
      m = x.length,
      n = y.length;

  p1 = popsym(0);

  for (i = 0; i < m; i++) {
    p = (r === p) ? p1 : popsym(i);
    p1 = popsym(i + 1);
    if (p > p1) {
      i += 1;
      idx = p1;
    } else {
      idx = p;
    }

    if (idx === n) {
      p = popsym(i);
    } else {
      r = idx;
      l += 1;
    }
  }
  return l;

  function popsym(index) {
    var s = x[index],
        pos = symbols[s] + 1;

    pos = y.indexOf(s, ((pos > r) ? pos : r));
    if (pos === -1) { pos = n; }
    symbols[s] = pos;
    return pos;
  }
}

$(function () {
  $('.calcExpander').on('click', function (e) {
    e.stopPropagation();
    $(this).parent().parent().parent().find('tr').not(':first').not(':last').toggle();
  });
  $('.calcExpander').each(function(){ $(this).click(); });
});