<commit_before>
/*
TODO:
- make it so that each instance has its own tactic set
*/

// CONFIGURATION
var nodeMinSpacing = 5;
var nodeStroke = 2;
var nodeHeight = 25;
var rectMargin = {top: 2, right: 8, bottom: 2, left: 8};
var scrollbarWidth = 0; // I could compute this if I cared enough
var nbChildrenToShow = 2;
var animationDuration = 420;

// OTHER GLOBALS
var i = 1; // unique identifier, should closure it to avoid drama
var maxNodesOnLine = Math.pow(nbChildrenToShow, 2);
var diagonal = d3.svg.diagonal();
var rootId = i++;
var animationRunning = false;

// GLOBALS TO BE INITIALIZED LATER
var tree, svg, canvas;
var smallestNodeWidth, width, height, curNode, rootNode;
var xFactor, yFactor;

var thms = [
'Theorem trivial : ∀c : comparison, True.',
'Theorem plus_O_n : ∀n : nat, 0 + n = n.',
'Theorem plus_1_l : ∀n : nat, 1 + n = S n.',
'Theorem mult_0_l : ∀n : nat, 0 * n = 0.',
'Theorem plus_id_example : ∀n m:nat, n = m → n + n = m + m.',
'Theorem plus_id_exercise : ∀n m o : nat, n = m → m = o → n + m = m + o.',
'Theorem mult_0_plus : ∀n m : nat, (0 + n) * m = n * m.',
'Theorem mult_S_1 : ∀n m : nat, m = S n → m * (1 + n) = m * m.',
'Theorem negb_involutive : ∀b : bool, negb (negb b) = b.',
'Theorem identity_fn_applied_twice : ∀(f : bool → bool), (∀(x : bool), f x = x) → ∀(b : bool), f (f b) = b.',
'Theorem andb_eq_orb : ∀(b c : bool), (andb b c = orb b c) → b = c.',
'Theorem andb_true_elim1 : ∀b c : bool, andb b c = true → b = true.',
'Theorem andb_true_elim2 : ∀b c : bool, andb b c = true → c = true.',
'Theorem plus_0_r : ∀n:nat, n + 0 = n.',
'Theorem minus_diag : ∀n, minus n n = 0.',
'Theorem mult_0_r : ∀n:nat, n * 0 = 0.',
'Theorem plus_n_Sm : ∀n m : nat, S (n + m) = n + (S m).',
'Theorem plus_comm : ∀n m : nat, n + m = m + n.',
'Theorem plus_assoc : ∀n m p : nat, n + (m + p) = (n + m) + p.',
'Theorem plus_rearrange : ∀n m p q : nat, (n + m) + (p + q) = (m + n) + (p + q).',
'Theorem plus_swap : ∀n m p : nat, n + (m + p) = m + (n + p).',
'Theorem mult_comm : ∀m n : nat, m * n = n * m.',
'Theorem andb_false_r : ∀b : bool, andb b false = false.',
'Theorem mult_1_l : ∀n:nat, 1 * n = n.',
'Theorem all3_spec : ∀b c : bool, orb (andb b c) (orb (negb b) (negb c)) = true.',
'Theorem mult_plus_distr_r : ∀n m p : nat, (n + m) * p = (n * p) + (m * p).',
'Theorem mult_assoc : ∀n m p : nat, n * (m * p) = (n * m) * p.',
];

function parseSVGTransform(a) {
    var b = {};
    for (var i in a = a.match(/(\w+\((\-?\d+\.?\d*,?)+\))+/g)) {
        var c = a[i].match(/[\w\.\-]+/g);
        b[c.shift()] = c;
    }
    return b;
}

function evenFloor(x) {
    var r = Math.floor(x);
    return (r % 2 === 0) ? r : r - 1;
}

function nodeWidth(d) {
    return smallestNodeWidth
        //* ((isCurNode(d) || isCurNodeParent(d)) ? nbChildrenToShow : 1)
    ;
}

function treeDepth(root) {
    return (
        root.visibleChildren
            ? 1 + _(root.visibleChildren).map(treeDepth).max()
            : 0
    );
}

function addTheorem(theorem) {
    var b = $('<button>', {
        text: theorem,
        click: function() { newTheorem(theorem); }
    });
    $('#buttons').append(b);
}

$(document).ready(function() {
    _(thms).each(addTheorem);

    smallestNodeWidth = evenFloor(
        ($(window).width()
         - scrollbarWidth
         - ((maxNodesOnLine - 1) * nodeMinSpacing)
        )
        / maxNodesOnLine
    );
    width =
        maxNodesOnLine * smallestNodeWidth
        + (maxNodesOnLine - 1) * nodeMinSpacing;
    // now that the buttons are here, we can compute the remaining height
    height = $(window).height() - ($('#tips').height() + $('#buttons').height());
    xFactor = width;
    yFactor = height;

    newTheorem(thms[17], hInit);
});

function newTheorem(theorem) {
    d3.select("svg").remove();

    tree = d3.layout.tree()
        .children(function(d) {
            if (d.solved) { return []; }
            if (isCurNode(d)) { return d.allChildren; }
            if (isCurNodeParent(d) && isTactic(d)) { return d.allChildren; }
            return d.visibleChildren;
        })
        .separation(function(n1, n2) {
            //if (isCurNode(n1) || isCurNode(n2)) { return nbChildrenToShow; }
            return 1;
        })
    ;

    svg = d3.select("body")
        .on("keydown", function() {
            if (animationRunning) { return; }
            //console.log(d3.event);
            switch (d3.event.keyIdentifier) {
            case "Left": shiftLeft(curNode); break;
            case "Right": shiftRight(curNode); break;
            case "Up":
                if(hasParent(curNode)) {
                    click(curNode.parent);
                }
                break;
            case "Down":
                if (isTactic(curNode)) {
                    var dest = _(curNode.visibleChildren).find(function(n) {
                        return !(n.solved);
                    });
                    if (dest) { click(dest); }
                } else {
                    if (curNode.visibleChildren[0]) { click(curNode.visibleChildren[0]); }
                }
                break;
            case "U+0031": case "U+0041":
                if (curNode.visibleChildren[0]) { click(curNode.visibleChildren[0]); }
                break;
            case "U+0032": case "U+0042":
                if (curNode.visibleChildren[1]) { click(curNode.visibleChildren[1]); }
                break;
            case "U+0033": case "U+0043":
                if (curNode.visibleChildren[2]) { click(curNode.visibleChildren[2]); }
                break;
            default: return;
            }
            // Prevent arrows from scrolling the webpage
            d3.event.preventDefault();
        })<commit_msg>fixed keyboard navigation for Firefox<commit_after>
/*
TODO:
- make it so that each instance has its own tactic set
*/

// CONFIGURATION
var nodeMinSpacing = 5;
var nodeStroke = 2;
var nodeHeight = 25;
var rectMargin = {top: 2, right: 8, bottom: 2, left: 8};
var scrollbarWidth = 0; // I could compute this if I cared enough
var nbChildrenToShow = 2;
var animationDuration = 420;

// OTHER GLOBALS
var i = 1; // unique identifier, should closure it to avoid drama
var maxNodesOnLine = Math.pow(nbChildrenToShow, 2);
var diagonal = d3.svg.diagonal();
var rootId = i++;
var animationRunning = false;

// GLOBALS TO BE INITIALIZED LATER
var tree, svg, canvas;
var smallestNodeWidth, width, height, curNode, rootNode;
var xFactor, yFactor;

var thms = [
'Theorem trivial : ∀c : comparison, True.',
'Theorem plus_O_n : ∀n : nat, 0 + n = n.',
'Theorem plus_1_l : ∀n : nat, 1 + n = S n.',
'Theorem mult_0_l : ∀n : nat, 0 * n = 0.',
'Theorem plus_id_example : ∀n m:nat, n = m → n + n = m + m.',
'Theorem plus_id_exercise : ∀n m o : nat, n = m → m = o → n + m = m + o.',
'Theorem mult_0_plus : ∀n m : nat, (0 + n) * m = n * m.',
'Theorem mult_S_1 : ∀n m : nat, m = S n → m * (1 + n) = m * m.',
'Theorem negb_involutive : ∀b : bool, negb (negb b) = b.',
'Theorem identity_fn_applied_twice : ∀(f : bool → bool), (∀(x : bool), f x = x) → ∀(b : bool), f (f b) = b.',
'Theorem andb_eq_orb : ∀(b c : bool), (andb b c = orb b c) → b = c.',
'Theorem andb_true_elim1 : ∀b c : bool, andb b c = true → b = true.',
'Theorem andb_true_elim2 : ∀b c : bool, andb b c = true → c = true.',
'Theorem plus_0_r : ∀n:nat, n + 0 = n.',
'Theorem minus_diag : ∀n, minus n n = 0.',
'Theorem mult_0_r : ∀n:nat, n * 0 = 0.',
'Theorem plus_n_Sm : ∀n m : nat, S (n + m) = n + (S m).',
'Theorem plus_comm : ∀n m : nat, n + m = m + n.',
'Theorem plus_assoc : ∀n m p : nat, n + (m + p) = (n + m) + p.',
'Theorem plus_rearrange : ∀n m p q : nat, (n + m) + (p + q) = (m + n) + (p + q).',
'Theorem plus_swap : ∀n m p : nat, n + (m + p) = m + (n + p).',
'Theorem mult_comm : ∀m n : nat, m * n = n * m.',
'Theorem andb_false_r : ∀b : bool, andb b false = false.',
'Theorem mult_1_l : ∀n:nat, 1 * n = n.',
'Theorem all3_spec : ∀b c : bool, orb (andb b c) (orb (negb b) (negb c)) = true.',
'Theorem mult_plus_distr_r : ∀n m p : nat, (n + m) * p = (n * p) + (m * p).',
'Theorem mult_assoc : ∀n m p : nat, n * (m * p) = (n * m) * p.',
];

function parseSVGTransform(a) {
    var b = {};
    for (var i in a = a.match(/(\w+\((\-?\d+\.?\d*,?)+\))+/g)) {
        var c = a[i].match(/[\w\.\-]+/g);
        b[c.shift()] = c;
    }
    return b;
}

function evenFloor(x) {
    var r = Math.floor(x);
    return (r % 2 === 0) ? r : r - 1;
}

function nodeWidth(d) {
    return smallestNodeWidth
        //* ((isCurNode(d) || isCurNodeParent(d)) ? nbChildrenToShow : 1)
    ;
}

function treeDepth(root) {
    return (
        root.visibleChildren
            ? 1 + _(root.visibleChildren).map(treeDepth).max()
            : 0
    );
}

function addTheorem(theorem) {
    var b = $('<button>', {
        text: theorem,
        click: function() { newTheorem(theorem); }
    });
    $('#buttons').append(b);
}

$(document).ready(function() {
    _(thms).each(addTheorem);

    smallestNodeWidth = evenFloor(
        ($(window).width()
         - scrollbarWidth
         - ((maxNodesOnLine - 1) * nodeMinSpacing)
        )
        / maxNodesOnLine
    );
    width =
        maxNodesOnLine * smallestNodeWidth
        + (maxNodesOnLine - 1) * nodeMinSpacing;
    // now that the buttons are here, we can compute the remaining height
    height = $(window).height() - ($('#tips').height() + $('#buttons').height());
    xFactor = width;
    yFactor = height;

    newTheorem(thms[17], hInit);
});

function newTheorem(theorem) {
    d3.select("svg").remove();

    tree = d3.layout.tree()
        .children(function(d) {
            if (d.solved) { return []; }
            if (isCurNode(d)) { return d.allChildren; }
            if (isCurNodeParent(d) && isTactic(d)) { return d.allChildren; }
            return d.visibleChildren;
        })
        .separation(function(n1, n2) {
            //if (isCurNode(n1) || isCurNode(n2)) { return nbChildrenToShow; }
            return 1;
        })
    ;

    svg = d3.select("body")
        .on("keydown", function() {
            if (animationRunning) { return; }
            //console.log(d3.event);
            var event = null;
            if (d3.event.hasOwnProperty('keyIdentifier')) { // Chrome
                event = d3.event.keyIdentifier;
            } else if ('key' in d3.event) { // Firefox
                event = d3.event.key;
            }
            console.log('Event:', event);
            switch (event) {
            case "Left": shiftLeft(curNode); break;
            case "Right": shiftRight(curNode); break;
            case "Up":
                if(hasParent(curNode)) {
                    click(curNode.parent);
                }
                break;
            case "Down":
                if (isTactic(curNode)) {
                    var dest = _(curNode.visibleChildren).find(function(n) {
                        return !(n.solved);
                    });
                    if (dest) { click(dest); }
                } else {
                    if (curNode.visibleChildren[0]) { click(curNode.visibleChildren[0]); }
                }
                break;
            case "U+0031": case "U+0041":
                if (curNode.visibleChildren[0]) { click(curNode.visibleChildren[0]); }
                break;
            case "U+0032": case "U+0042":
                if (curNode.visibleChildren[1]) { click(curNode.visibleChildren[1]); }
                break;
            case "U+0033": case "U+0043":
                if (curNode.visibleChildren[2]) { click(curNode.visibleChildren[2]); }
                break;
            default: return;
            }
            // Prevent arrows from scrolling the webpage
            d3.event.preventDefault();
        })
{'fraction_non_alphanumeric': 0.16732350925291295, 'fraction_numerical': 0.01567854694996573, 'mean_word_length': 2.0897300158814187, 'pattern_counts': {'":': 20, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '53793', 'n_tokens_mistral': 4408, 'n_tokens_neox': 4072, 'n_words': 1170}