// Written by Terence Tao. This work is licensed under a Creative Commons Attribution 4.0 International License: http://creativecommons.org/licenses/by/4.0/
/// Global variables
unlockedLaws = [];
exerciseButtons = [];
lastClickedButton = ""; // this will be updated to the last deduction button one clicked; prevents double clicking from doing anything
/////// CREATING AND UPDATING HTML ELEMENTS /////////////
function getElement(id) {
return document.getElementById(id);
}
// a standard box
// may be good practice to replace this with a box object that extends whatever object createlement is... but apparently one should not extend native elements
function newBox() {
var box = document.createElement("DIV");
box.className = "clickable";
box.style.float = "left";
box.style.margin = "5px";
box.style.padding = "0px 10px";
box.style.backgroundColor = "white";
box.style.cursor = "pointer";
return box;
}
// a standard heading
function newHeading(text) {
var header = document.createElement("H4");
header.innerHTML = text;
header.style.margin = "0px";
return header;
}
// a standard button
function newButton(text) {
var button = document.createElement("BUTTON");
button.innerHTML = text;
return button;
}
function createResetButton() {
var button = getElement("reset button");
button.onclick = function() {
if (confirm("Are you sure? This will erase all your progress!")) {
if (localStorage)
localStorage.clear();
location.reload();
}
};
return button;
}
// create the list of achievements
function createAchievementsBox() {
var box = getElement("achievement box");
box.appendChild(newHeading("Achievements"));
var list = document.createElement("UL");
list.id = "achievements";
// list.style.paddingLeft = "10px";
box.appendChild(list);
return box;
}
// record an achievement
function achieve(achievement) {
var log = getElement("achievements");
var node = document.createElement("LI");
var span = document.createElement("SPAN");
span.innerHTML = achievement;
node.appendChild(span);
log.insertBefore(node, log.firstChild);
}
// notifications, error messages, debugging tool
function createNotificationsBox() {
var box = getElement("notification box");
box.appendChild(newHeading("Notifications"));
var list = document.createElement("UL");
list.id = "notifications";
// list.style.paddingLeft = "10px";
box.appendChild(list);
return box;
}
function notify(msg) {
var log = getElement("notifications");
var node = document.createElement("LI");
var span = document.createElement("SPAN");
span.innerHTML = msg;
node.appendChild(span);
log.appendChild(node);
}
function debug(msg) {
notify(msg);
}
function error(msg) {
notify(msg);
}
// create the proof box
function createProofBox() {
// var box = newBox();
var box = getElement("proof box");
box.appendChild(newHeading("Proof"));
var list = document.createElement("OL");
list.id = "proof";
list.numlines = 0;
// list.style.paddingLeft = "10px";
box.appendChild(list);
return box;
}
// add a line to the proof
function appendToProof(line) {
var proof = getElement("proof");
var node = document.createElement("LI");
var span = document.createElement("SPAN");
span.innerHTML = line;
node.appendChild(span);
proof.appendChild(node);
proof.numlines++;
}
// create exercise window
function createExerciseBox() {
var text = getElement("exercise");
if (localStorage)
if (localStorage.length != 0)
text.innerHTML = "";
return text;
}
// add a given hypothesis to main environment
function given(context) {
addContext(context);
appendToProof(context.name() + ". [given]");
}
// clear out an element
function clearElement(id) {
getElement(id).innerHTML = '';
}
// convert a list of sentences, boxes, or contexts to a string
function listToString(list) {
if (list.length == 0) return "";
var i;
var str = "";
for (i = 0; i < list.length; i++) {
str += toContext(list[i]).name() + ", ";
}
str = str.substring(0, str.length - 2);
return str;
}
// create a deduction string
function deductionString(prefix, list, conclusion)
{
if (list.length == 0)
return "Deduce " + conclusion + ".";
else
return prefix + " " + listToString(list) + ": deduce " + conclusion + ".";
}
// New exercise in the exercise window
function setExercise(exerciseButton) {
// clear all existing elements
clearElement("root environment");
getElement("root environment").appendChild(newHeading("Root environment"));
clearElement("proof");
getElement("proof").numlines = 0;
clearElement("deductionDesc");
clearElement("deductions");
clearElement("formula window");
getElement("formula window").appendChild(newHeading("Formulas"));
var exerciseText = getElement("exercise");
var exerciseDesc = document.createElement("DIV");
exerciseDesc.id = "exercise desc";
var exercise = exerciseButton.exercise;
// Display exercise text
if (exercise.name == exercise.law.name)
exerciseDesc.innerHTML = "" + exercise.name + ": " + exercise.law.string;
else
exerciseDesc.innerHTML = "" + exercise.name + " (" + exercise.law.name + "): " + exercise.law.string;
exerciseText.innerHTML = "";
exerciseText.appendChild(exerciseDesc);
if (exercise.bestLength > 0) {
exerciseText.appendChild(document.createElement("BR"));
exerciseText.appendChild(document.createTextNode("Shortest known non-circular proof: " + exercise.bestLength + " lines."));
}
// Display exercise notes
if (exercise.notes != "") {
exerciseText.appendChild(document.createElement("BR"));
var notes = document.createElement("DIV");
notes.innerHTML = exercise.notes;
exerciseText.appendChild(notes);
}
// Load all given hypotheses
exercise.law.givens.forEach( function(item) {
if (item.type == "sentence in environment")
given(item);
});
exerciseText.exercise = exercise;
exerciseText.exerciseButton = exerciseButton;
// reveal the formula window, if this option is active
if (exercise.revealFormulaWindow) {
if (getElement("formula window").style.display == 'none') {
achieve("UNLOCKED formula window.");
getElement("formula window").style.display = 'block';
if (localStorage)
localStorage.setItem("formula window", "unlocked");
}
}
// Unlock any laws that were unlocked by the exercise
exercise.newLaws.forEach( function(item) {
if (!item.unlocked) {
unlock(item, "UNLOCKED");
}
});
// add each primitive to the formula window
var primitives = listPrimitives(exercise.law);
primitives.forEach( function(primitive) {
addContext(formulaContext(primitiveSentence(primitive)));
});
var color = 'yellow';
if (localStorage)
if (localStorage.getItem(exercise.name) == 'solved')
color = 'lightgreen';
exerciseDesc.style.backgroundColor = color;
getElement("proof box").style.backgroundColor = color;
}
// create the root environment window
function createRootEnvironment() {
var box = getElement("root environment");
box.style.margin = "5px";
box.style.padding = "0px 10px";
box.style.border = "1px solid black";
box.style.backgroundColor = "#eeeeee";
box.setAttribute('ondragover', "allowDrop(event)");
box.setAttribute('ondrop', "drop(event)");
box.type = "environment";
box.appendChild(newHeading("Root environment"));
return box;
}
// returns the subenvironment of env with sentence in it, or false otherwise
function findAssumption(env, sentence) {
var i;
for (i=0; i < env.children.length; i++)
{
var child = env.children[i];
if (child.type == "environment")
if (child.sentence.shortText == sentence.shortText) {
return child;
}
}
return false;
}
// inside an existing environment, add an assumption subenvironment
function makeAssumption(env, sentence) {
var box = findAssumption(env,sentence);
if (box != false) return box;
box = newBox();
box.id = uniqueId();
box.type = "environment";
env.appendChild(box);
box.appendChild(newHeading("Assume " + sentence.shortText));
box.sentence = sentence;
return box;
}
// when creating child environments, remember to set box.type to "environment" and box.sentence to the sentence being assumed.
// create formula window
function createFormulaWindow() {
var box = getElement("formula window");
box.style.margin = "5px";
box.style.padding = "0px 10px";
box.style.border = "1px solid black";
box.style.background = "#eeeeee";
box.setAttribute('ondragover', "allowDrop(event)");
box.setAttribute('ondrop', "drop(event)");
box.type = "formula window";
box.appendChild(newHeading("Formulas"));
box.style.display = 'none';
return box;
}
// if formula window unlocked in previous session, reveal it
function checkIfFormulaWindowUnlocked() {
if (localStorage)
if (localStorage.getItem("formula window") == "unlocked") {
achieve("UNLOCKED formula window.");
getElement("formula window").style.display = 'block';
}
}
// unique ID generator for creating new objects
function uniqueId() {
return 'id-' + Math.random().toString(36).substr(2, 16);
};
// create a new box with a sentence in it
function newSentenceBox(sentence) {
var box = newBox();
box.innerHTML = sentence.shortText;
box.setAttribute('draggable', true);
box.setAttribute('ondragstart', "drag(event)");
box.setAttribute('onclick', "clickBox(this)");
box.id = uniqueId();
box.type = "sentenceBox";
box.sentence = sentence;
return box;
};
// add a formula to the formula window, or a sentence in environment to the relevant environment
// convert a list of assumptions into an environment box
function getEnvironment(list) {
var env = getElement("root environment");
list.forEach( function(statement) {
env = makeAssumption(env, statement);
});
return env;
}
function addContext(context) {
if (context.type != "formula" & context.type != "sentence in environment") {
error("Cannot add this type of context: " + context.type);
return;
}
var box = newBox();
box.innerHTML = context.sentence.shortText;
box.setAttribute('draggable', true);
box.setAttribute('ondragstart', "drag(event)");
box.setAttribute('onclick', "clickBox(this)");
box.id = uniqueId();
box.sentence = context.sentence;
if (context.type == "formula")
{
box.type = "formulaBox";
getElement("formula window").appendChild(box);
} else {
var env = getEnvironment(context.environment);
box.type = "sentenceBox";
env.appendChild(box);
}
}
// make a deduction; check for victory condition
function deduce(conclusion, justification, law) {
// add conclusion to either a deduction environment or the formula window, as appropriate.
addContext(conclusion);
// creating a formula is not important enough to mention explicitly in the proof, nor should it trigger a victory condition.
if (conclusion.type == "formula") return;
var justificationSentences = justification.filter( function(context) { return (context.type == "sentence in environment"); });
appendToProof( deductionString("From", justificationSentences, conclusion.name()) + " [" + law.name + "]");
var exercise = getElement("exercise").exercise;
var exerciseButton = getElement("exercise").exerciseButton;
if (conclusion.name() == exercise.law.conclusion.name())
{
// hooray, you solved it!
if (!exerciseButton.solved) {
appendToProof('QED!');
unlock(exercise.law, "PROVED");
getElement("exercise desc").style.backgroundColor = 'lightgreen';
exerciseButton.style.backgroundColor = 'hsl(150,50%,50%)';
exerciseButton.style.color = 'white';
exerciseButton.style.cursor = 'pointer';
exerciseButton.solved = true;
getElement("proof box").style.backgroundColor = 'lightgreen';
if (localStorage)
localStorage.setItem(exercise.name, "solved");
exercise.newExercises.forEach( function(item) {
activateExerciseButton(item);
});
if (exercise.completionMsg != "")
alert(exercise.completionMsg);
// search through all exercise buttons to see if they are all solved
if (exerciseButtons.every( function(button) { return button.solved; } )) {
alert("Congratulations, you completed all the exercises! You are now a master of propositional logic!");
}
} else {
appendToProof('QED! (again)');
}
var len = getElement("proof").numlines;
if (localStorage) {
var oldlen = localStorage.getItem("lines " + exercise.name);
if (oldlen == undefined)
{
notify(exercise.name + " was proved in " + len + " lines.");
localStorage.setItem("lines " + exercise.name, len);
} else if (oldlen > len) {
notify(exercise.name + " was reproved in " + len + " lines. A new personal best!");
localStorage.setItem("lines " + exercise.name, len);
} else {
notify(exercise.name + " was reproved in " + len + " lines.");
}
}
else
notify(exercise.name + " was proved in " + len + " lines.");
if (len == exercise.bestLength)
notify("You matched the record for the shortest known proof!");
if (len < exercise.bestLength)
alert("You beat the record for the shortest known proof! If your proof was non-circular (that is, it did not use the current exercise, or any rules obtained subsequently to this exercise), please send it to me at tao@math.ucla.edu and I will update the record (with an acknowledgment) in the next version of the text.");
}
}
//// ExerciseButton ////
function createExerciseButtonBox() {
var box = document.createElement("DIV");
box.id = "exerciseButtonBox";
document.body.appendChild(box);
}
function createExerciseButton( exercise) {
var button = newButton(exercise.name);
button.exercise = exercise;
button.className = "clickable";
button.style.backgroundColor = 'hsl(0,10%,75%)';
button.style.color = 'white';
button.style.cursor = 'not-allowed';
button.enabled = false;
exercise.button = button;
getElement("exercise button box").appendChild(button);
}
function activateExerciseButton(exercise) {
var button = exercise.button;
if (button.enabled) return;
button.enabled = true;
button.style.backgroundColor = 'hsl(60,100%,75%)';
button.style.color = "black";
button.style.cursor = "pointer";
button.onclick = function() {
setExercise(this);
};
notify(exercise.name + " now available.")
button.solved = false;
exerciseButtons.push(button);
if (localStorage) {
localStorage.setItem(exercise.name, "unlocked");
var len = localStorage.getItem("lines " + exercise.name);
if (len != undefined) {
notify(exercise.name + " was proven in " + len + " lines.");
}
}
return button;
}
// create the box of available deductions
function createDeductionsBox() {
var box = getElement("deductions box");
box.style.margin = "5px";
box.style.padding = "0px 10px";
// box.style.border = "1px solid black";
box.appendChild(newHeading("Available deductions"));
var desc = document.createElement("DIV");
desc.id = "deductionDesc";
box.appendChild(desc);
var list = document.createElement("UL");
list.id = "deductions";
box.appendChild(list);
}
// list the assumptions used when searching for deductions
function from( assumptions )
{
var desc = getElement("deductionDesc");
if (assumptions.length == 1) {
desc.innerHTML = "From " + toContext(assumptions[0]).name() + ":";
}
if (assumptions.length == 2) {
desc.innerHTML = "From " + toContext(assumptions[0]).name() + ", " + toContext(assumptions[1]).name() + ":";
}
clearElement("deductions");
}
// add a line to available deductions
function appendToDeductions(conclusion, justification, law) {
var proof = getElement("deductions");
var node = document.createElement("LI");
var span = document.createElement("SPAN");
span.innerHTML = "" + law.name + ": ";
node.appendChild(span);
var button = newButton( conclusion.name());
button.conclusion = conclusion;
button.justification = justification;
button.onclick = function() {
if (this == lastClickedButton) return; // prevent double click from doing anything
lastClickedButton = this;
deduce(this.conclusion, this.justification, law);
};
node.appendChild(button);
proof.appendChild(node);
}
//// Sentence object
function Sentence() {
this.type = ""; // "primitive", "AND", "OR", "NOT", "IMPLIES", "IFF"
this.shortText = ""; // name of sentence when used standalone
this.longText = ""; // name of sentence when combined with other sentences
}
// create a primitive sentence
function primitiveSentence(primitive) {
sentence = new Sentence();
sentence.type = "primitive";
sentence.shortText = ""+primitive+"";
sentence.longText = sentence.shortText;
sentence.name = primitive;
return sentence;
}
// form the conjunction of two sentences
function AND( sentence1, sentence2) {
sentence = new Sentence();
sentence.type = "AND";
sentence.shortText = sentence1.longText + " AND " + sentence2.longText;
sentence.longText = "(" + sentence.shortText + ")";
sentence.arg1 = sentence1;
sentence.arg2 = sentence2;
return sentence;
}
// form the disjunction of two sentences
function OR( sentence1, sentence2) {
sentence = new Sentence();
sentence.type = "OR";
sentence.shortText = sentence1.longText + " OR " + sentence2.longText;
sentence.longText = "(" + sentence.shortText + ")";
sentence.arg1 = sentence1;
sentence.arg2 = sentence2;
return sentence;
}
// form the implication of two sentences
function IMPLIES( sentence1, sentence2) {
sentence = new Sentence();
sentence.type = "IMPLIES";
sentence.shortText = sentence1.longText + " IMPLIES " + sentence2.longText;
sentence.longText = "(" + sentence.shortText + ")";
sentence.arg1 = sentence1;
sentence.arg2 = sentence2;
return sentence;
}
// form the iff of two sentences
function IFF( sentence1, sentence2) {
sentence = new Sentence();
sentence.type = "IFF";
sentence.shortText = sentence1.longText + " IFF " + sentence2.longText;
sentence.longText = "(" + sentence.shortText + ")";
sentence.arg1 = sentence1;
sentence.arg2 = sentence2;
return sentence;
}
// form the negation of a sentence
function NOT( sentence1) {
sentence = new Sentence();
sentence.type = "NOT";
sentence.shortText = "NOT " + sentence1.longText;
sentence.longText = "(" + sentence.shortText + ")";
sentence.arg1 = sentence1;
return sentence;
}
// Law object
function Law(name, givens, conclusion) {
this.name = name; // name of law, e.g. "EXERCISE 1"
// givens is an array of given hypotheses (can be empty). I allow sentences as givens, so these need to be converted to contexts.
var givenslist = [];
givens.forEach( function(given) {
givenslist.push(toContext(given));
});
this.givens = givenslist;
this.conclusion = toContext(conclusion); // given conclusion
this.unlocked = false; // by default the law is not unlocked
this.string = deductionString("Given", givens, this.conclusion.name());
this.desc = ""+name+": " + this.string;
if (localStorage)
if (localStorage.getItem("law " + this.name) != null)
unlock(this, localStorage.getItem("law " + this.name));
}
// list the (names of) primitives occurring in a law
function listPrimitives(law) {
list = [];
law.givens.forEach( function(item) {
pushContext(list, toContext(item));
});
// most likely the line below is redundant, as any primitives in conclusion should have already appeared in one of the givens
pushContext(list, law.conclusion);
return list;
}
// push all the primitives from context onto list (removing duplicates)
function pushContext(list, context) {
if (context.type == "formula" || context.type == "sentence in environment") {
pushPrimitives(list, context.sentence);
}
if (context.type == "environment" || context.type == "sentence in environment")
{
context.environment.forEach( function(item) {
pushPrimitives(list, item);
});
}
}
// push all the primitives from sentence onto list (removing duplicates)
function pushPrimitives(list, sentence)
{
if (sentence.type == "primitive")
{
if (!list.includes(sentence.name)) {
list.push(sentence.name);
}
} else if (sentence.type == "NOT") {
pushPrimitives(list, sentence.arg1);
}
else {
pushPrimitives(list, sentence.arg1);
pushPrimitives(list, sentence.arg2);
}
}
// a tricky routine: tries to match arglist to the givens of a law and see what the primitives are, returning this data in an output object
function matchWithGivens( arglist, givens, primitives ) {
var output = new Object();
output.matches = true; // so far, no reason to doubt a match.
output.env = []; // by default, the output environment will be the root one.
primitives.forEach( function(primitive) {
output[primitive] = "";
});
// technically one needs to ensure that "matches" is never a primitive.
if (arglist.length != givens.length) {
output.matches = false;
return output;
}
// convert everything to contexts if not already done so (this step may be redundant)
var i;
for (i = 0; i < givens.length; i++) {
arglist[i] = toContext(arglist[i]);
givens[i] = toContext(givens[i]);
}
// check if all the givens are formulas
var allFormulas = true;
for (i = 0; i < givens.length; i++) {
if (givens[i].type != "formula") allFormulas = false;
}
if (!allFormulas)
{
var proposedYet = false;
var proposedEnv = [];
for (i = 0; i < givens.length; i++) {
if (givens[i].type != "formula") {
if (arglist[i].environment.length < givens[i].environment.length) {
// can't match if the template has more deeply nested assumptions than the arglist!
output.matches = false;
return output;
}
var candidateEnv = arglist[i].environment.slice( 0, arglist[i].environment.length - givens[i].environment.length);
if (proposedYet == false) {
proposedYet = true;
proposedEnv = candidateEnv;
}
else if (listToString(proposedEnv) != listToString(candidateEnv)) { // need to convert to string here as a proxy for passing by value rather than by reference
output.matches = false;
return output;
}
}
}
output.env = proposedEnv;
}
var i;
for (i = 0; i < givens.length; i++) {
matchWithGiven( arglist[i], givens[i], output)
if (!output.matches) return output;
}
return output;
}
// try to match a context with a template context and store the match in output
function matchWithGiven( context, template, output) {
if (!output.matches) return;
if (context.type != template.type) {
output.matches = false;
return;
}
if (template.type == "environment" || template.type == "sentence in environment") {
var i;
for (i = 0; i < template.environment.length; i++) {
matchWithGivenSentence( context.environment[i + output.env.length], template.environment[i], output);
if (!output.matches) return;
}
}
if (template.type == "formula" || template.type == "sentence in environment")
matchWithGivenSentence( context.sentence, template.sentence, output);
}
// try to match a sentence with a template sentence and store the match in output
function matchWithGivenSentence( sentence, template, output) {
if (!output.matches) return;
if (template.type == "primitive") {
if (sentence.shortText == output[template.name].shortText) {
// good, it matches what we've already fit to the template!
return;
}
if (output[template.name] == "") {
output[template.name] = sentence;
return;
}
output.matches = false;
return;
}
if (template.type != sentence.type) {
// debug("Type mismatch.");
output.matches = false;
return;
}
if (template.type == "NOT") {
matchWithGivenSentence( sentence.arg1, template.arg1, output);
} else {
matchWithGivenSentence( sentence.arg1, template.arg1, output);
matchWithGivenSentence( sentence.arg2, template.arg2, output);
}
}
// insert the values of the output object (previously obtained by matchWithGivens) to a template sentence
function subsSentence(template, output)
{
if (template.type == "primitive") {
return output[template.name];
}
if (template.type == "NOT") {
return NOT( subsSentence(template.arg1, output) );
}
if (template.type == "AND") {
return AND( subsSentence(template.arg1, output), subsSentence(template.arg2, output) );
}
if (template.type == "OR") {
return OR( subsSentence(template.arg1, output), subsSentence(template.arg2, output) );
}
if (template.type == "IMPLIES") {
return IMPLIES( subsSentence(template.arg1, output), subsSentence(template.arg2, output) );
}
if (template.type == "IFF") {
return IFF( subsSentence(template.arg1, output), subsSentence(template.arg2, output) );
}
}
// insert the values of the output object (previously obtained by matchWithGivens) to an environment; starts with the object ambient environment
function subsEnvironment(env, output) {
var list = output.env;
env.forEach( function(item) {
list.push( subsSentence(item, output));
});
return list;
}
// insert the values of the output object (previously obtained by matchWithGivens) to a template context
function subs(template, output)
{
if (template.type == "formula") {
return formulaContext(subsSentence(template.sentence, output));
}
if (template.type == "environment") {
return environmentContext(subsEnvironment(template.environment, output));;
}
if (template.type == "sentence in environment") {
return sentenceContext(subsSentence(template.sentence, output), subsEnvironment(template.environment, output));
}
error("Template type not recognised:" + template.type);
}
// unlock a law, make it available for use in future deductions
function unlock(law, text) {
law.unlocked = true;
unlockedLaws.push(law);
achieve("" + text + " " + law.desc);
if (localStorage)
localStorage.setItem("law " + law.name, text);
}
// Exercise object
function Exercise(exerciseName, lawName, givens, conclusion) {
this.name = exerciseName;
if (lawName == "")
lawName = exerciseName;
this.law = new Law(lawName,givens,conclusion);
this.newLaws = []; // an array of laws unlocked when exercise is attempted(can be empty)
this.newExercises = []; // an array of exercises unlocked when exercise is completed (empty by default)
this.hasButton = false; // whether a button for this exercise exists yet
this.completionMsg = ""; // message upon completion of exercise (default empty)
this.notes = ""; // notes to make when an exercise is set
this.revealFormulaWindow = false; // do we reveal the formula window when this exercise opens?
this.bestLength = 0; // the shortest length proof I know of (w/o cheating)
this.unlockedBy = function( prerequisite ) {
prerequisite.newExercises.push(this);
};
this.unlocks = function( law ) {
this.newLaws.push(law);
};
createExerciseButton(this);
if (localStorage) {
var str = localStorage.getItem(this.name);
if (str == "unlocked" || str == "solved") {
var button = activateExerciseButton(this);
if (str == "solved")
{
button.style.backgroundColor = 'hsl(150,50%,50%)';
button.style.color = "white";
button.solved = true;
localStorage.setItem(this.name, "solved");
}
}
}
}
// Context object
// perhaps the most complicated object in the code. A context is one of three things:
// A sentence inside an environment ("A [assuming B]";
// An environment ("[assuming A]", or "[Root environment]");
// A formula "Formula "A"" (a sentence without environment)
function Context() {
this.type = ""; // "sentence in environment", "environment", "formula"
this.sentence = new Sentence(); // sentence used (for sentence and formula types)
this.environment = []; // environment used (for sentence and environment types); an ordered list of sentences
this.name = function() {
if (this.type == "formula") {
return 'formula "' + this.sentence.shortText + '"';
}
if (this.type == "environment")
{
var env = this.environment;
if (env.length == 0) return "[root environment]";
return "[assuming " + listToString(env) + "]";
}
if (this.type == "sentence in environment")
{
var env = this.environment;
// debug("env length: " + env.length);
if (env.length == 0) return this.sentence.shortText;
return this.sentence.shortText + " [assuming " + listToString(env) + "]";;
}
error("Unknown context type!");
return "";
}
}
function formulaContext(sentence) {
formula = new Context();
formula.type = "formula";
formula.sentence = sentence;
return formula;
}
function sentenceContext(sentence, env) {
context = new Context();
context.type = "sentence in environment";
context.sentence = sentence;
context.environment = env;
return context;
}
function environmentContext(env) {
environment = new Context();
environment.type = "environment";
environment.environment = env;
return environment;
}
function rootEnvironmentContext() {
return environmentContext([]);
}
// create a new context from an existing context with an additional assumption. This assumption is put at the bottom of the assumption nesting, e.g. assuming("A assuming B", C) would give "A assuming B,C"
function assuming(context, assumption) {
// in case one is passed a sentence or box instead of a context
var newcontext = toContext(context);
// need a copy of newcontext.environment, otherwise push would modify the original environment.
var envclone = newcontext.environment.slice(0);
envclone.unshift(assumption);
return sentenceContext(newcontext.sentence, envclone);
}
// return the list of assumptions associated to an environment box
function listAssumptions(env) {
if (env.id == "root environment") {
return [];
} else {
var list = listAssumptions(env.parentElement).slice(0);
list.push( env.sentence );
return list;
}
}
// convert obj to context, where object is either a sentence, a context, or a box
function toContext(obj) {
if (obj instanceof Sentence) {
return sentenceContext(obj, []);
}
if (obj instanceof Context) {
return obj;
}
// only remaining possibility is that it is a sentencebox, formulabox or an environment
if (obj.type == "environment") {
return environmentContext(listAssumptions(obj));
}
if (obj.type == "sentenceBox") {
return sentenceContext(obj.sentence, listAssumptions(obj.parentElement));
}
if (obj.type == "formulaBox") {
return formulaContext(obj.sentence);
}
error("Unrecognised type: " + obj.type);
return new Context();
}
////////////////////// ACTIONS //////////////////
// ev.target is not always the box or environment that one wishes to manipulate due to the fact that one may have dropped onto a suboject. So one has to pop up until one has a valid object
function correctTarget(ev) {
var targ = ev.target;
while (targ.type != "environment" && targ.type != "sentenceBox" && targ.type != "formulaBox" && targ.type != "formula window")
targ = targ.parentElement;
return targ;
}
// click a sentence box
function clickBox(box) {
makeMatches([toContext(box)]);
}
function makeMatches(justification) {
from( justification );
var numMatches = 0;
unlockedLaws.forEach( function(law) {
var primitives = listPrimitives(law);
var output = matchWithGivens( justification, law.givens, primitives );
if (output.matches) {
appendToDeductions(subs(law.conclusion, output), justification, law);
numMatches++;
}
});
if (numMatches == 0) {
var proof = getElement("deductions");
var node = document.createElement("LI");
var span = document.createElement("SPAN");
span.innerHTML = "No available deductions can be formed from this selection.";
node.appendChild(span);
proof.appendChild(node);
}
}
// remember the ID of the object being dragged.
function drag(ev) {
ev.dataTransfer.setData("text", ev.target.id);
}
function allowDrop(ev) {
ev.preventDefault();
}
function drop(ev) {
ev.preventDefault();
// arg1 is the object that is being dragged.
var arg1 = getElement(ev.dataTransfer.getData("text"));
var arg2 = correctTarget(ev);
if (arg2.type == "formula window")
{
if (arg1.type == "sentenceBox") {
addContext(formulaContext(arg1.sentence));
return;
}
return;
}
makeMatches([toContext(arg1), toContext(arg2)]);
}