// a pseudo-C++ description of the main classes appearing in the code


/////////////////// logical components of the code - mostly in logic.js

/// Global variables

Sentence sentences[];  // sentences[name] is a sentence/term attached to a name string; easier to populate this dynamically than to create a general string to sentence/term parser.
Law unlockedLaws[];  // all the unlocked laws
Law allLaws[];  // list of all Laws
var lawsByShortName = {}; // laws indexed by shortname



// a FreeVariable is a variable such as x, y, z that are not bound by quantifiers.

FreeVariable {
	string type;     // "free variable"
	string subtype;  // name of variable
	string name;     // name of variable
	string Name;     // name of variable in italics
}

// BoundVariable is a variable such as X, Y, Z that can be bound by quantifiers.

BoundVariable {
	string type;     // "bound variable"
	string subtype;  // name of variable
	string name;     // name of variable (in italics)
	string longName; // name of variable
}

// Operators are functions such as f(), g(,) or binary operations such as +, -, *, which take terms as input and return a term as output.

Operator {
	string type;     // "operator"
	string subtype;  // name of operator
	string text;	 // name of operator in italics
	int arity;       // number of arguments
	bool additionStyle;  // is it an op like +?
}

// A Term is an expression such as g(x,Y), alpha or X+z that can be constructed from free and bound variables, primitive terms, and operators.

Term {
	string type;	   // "term"
	string subtype;    // "free variable", "bound variable", "primitive", or "operator"
	string shortText;  // how term is displayed standalone
	strong longText;   // how term is displayed inside more complex expressions
	Operator operator; // the operator used (for "operator" subtype)
	Term argList[];    // arguments or variables used
}

// note: right now, a distinction is made between a term that consists of a free or bound variable, and the free or bound variable itself.  For instance, the term "x" is not the same as the free variable "x", the latter being the argList[0] of the former.  On reflection, though, there is not much point to this distinction, and one could reduce the number of data structures slightly by treating free and bound variables more like primitive terms (so that a term "x" now is the same as the free variable "x" and argList is now empty).  On the other hand there isn't much advantage to changing things either (a few lines of code might get a little simpler, but also a bunch of bugs might be introduced).


// A Predicate is a symbol such as P(), Q(,), or a relation such as =, >, which takes terms as input and return sentences as output.  The equality relation = requires special treatment.

Predicate {
	string type;	// "predicate"
	string subtype;	// name of predicate
	string text;	// name of predicate in italics
	string arity;	// number of arguments
	bool relationStyle; // is it a relation like =?
}

Predicate equality;  // the equality relation

// A logical connective such as AND, OR, NOT, etc. takes statements as input and returns a statement as output.

Connective {
	string name;  // name of connective
	int arity;
}

Connective ANDConnective, ORConnective, NOTConnective, IMPLIESConnective, IFFConnective, TRUEConnective, FALSEConnective;

// A sentence is an assertion which can be true or false in any given environment (for given choices of free variables).  For instance P(x) AND (NOT Q(x+y)) would be a sentence that would be well-formed in any environment containing x and y as free variables.

Sentence {
	string type;	//  "primitive", "connective", "quantifier"
	string subtype;	//  "AND", "OR", "NOT", "IMPLIES", "IFF", "TRUE", "FALSE" for connectives; "atomic" or "predicate" for primitives; "for all" or "there exists" for quantifiers
	string name // name of sentence when used standalone
	string longName; // name of sentence when combined with other sentences
	Sentence argList[];   // the list of arguments in this sentence (usually of length 0, 1, or 2)
	Predicate predicate; // predicate used ("predicate" subtype only)
	Connective connective; // connective used ("connective" subtype only)
}

// Sentences and terms have very similar structure, and some of the code treats them in a unified fashion.  If one were to redo the data structures one could consider unifying the two (this would also unify the concepts of a connective, operator, and predicate).


// A law is a rule of deduction that has sentence templates as input, and another sentence template as output.  (For instance, Modus ponens "Given A, A IMPLIES B: deduce B" is a law.) Some laws are too complex to be fully captured by these templates due to side conditions, and need to be handled separately.

Law {
	string shortName;  // id of law
	string name; // HTML name of law
	Context givens[]; // hypotheses
	Context conclusion; // conclusion
	Context givensTemplate[];  // hypothesis template (used for matching)
	Context conclusionTemplate; // conclusion template (used for matching)
	bool unlocked;  // is it available for use?
	string string; // name of law when invoked
	int index; // index in the list of laws
	Law clone; // in case one can add a root environment hypothesis
}

// The following are the list of special laws that are coded separately.  Originally they were placed in the QED file; now they are defined in logic.js.

Law universalIntroduction, universalIntroduction2, universalSpecification, universalSpecification2, existentialInstantiation, existentialInstantiation2, existentialIntroduction, existentialIntroduction2, indiscernability;


// an Assumption is what separates an environment from a subenvironment.  Examples include "Assume A", "Let x be arbitrary", and "Set x s.t. P(x)".

Assumption {
	string type // "assuming", "letting", "setting"
        Sentence sentence;   // the sentence being assumed (for "assuming" and "setting" types)
        FreeVariable variable;    // the free variable used (for "letting" and "setting types")
    	string name;   // name of assumption
}

// A Context is a sentence inside an environment (an ordered list of assumptions), a formula in the Formulas window, or a Term in the Terms window.  The main operation of the text is dragging one context onto another (or clicking on a context) to reveal potential deductions.

Context {
    string type; // "sentence in environment", "environment", "formula", "term context"
    Sentence sentence; // sentence used (for sentence, sentence-in-envrionment, and formula types)
    Assumption environment[];  // environment used (for sentence-in-environment and environment types)
    Term term;  // term used (For term context types)

    string name;  // name of context
}




///////////////////////////////////// GUI elements

// Global variables

Button exerciseButtons[];   // ordered list of activated exercise buttons
Exercise exerciseList[];  // list of all exercises (including those not yet unlocked)
Exercise exercisesByShortName[]; // list of exercises (including those not yet unlocked) indexed by shortname
Button lastClickedButton;   // this will be updated to the last deduction button one clicked; prevents double clicking from doing anything
bool revealTrueFalse;  // do we populate the formula window with true and false?
String sectionTitle;  // name of last section to be created
int numIndexedLaws;  // number of laws that have been properly assigned an index



// An Exercise, such as Exercise 4.1, asks the reader to establish some conclusion from given hypothesis.  It also may come with some supplementary text, unlock some laws or windows when beginning the exercise, and unlock some further exercises when completed.

Exercise {
	string shortName; // short name of exercise (without "EXERCISE ")
	string name;  // name of exercise
	Law law;      // the law the exercise seeks to prove
	Law newLaws[]; // the laws unlocked when starting exercise
	Exercise newExercises[]; // the exercises unlocked when completing exercise
	string notes; // the notes for the exercise, displayed on opening
	bool revealFormulaWindow;  // do we unlock the formula window?
	bool revealTermWindow;  // do we unlock the term window?
	bool revealTrueFalse;      // do we unlock TRUE and FALSE?
	bool revealBoundButton;  // do we unlock the new bound var button?
	int bestLength;  // the shortest known length of proof
	string proof;  // the shortest known proof of this exercise
	int personalBest; // personal best length of proof
	bool activated; // has this exercise been unlocked?
	Button button;  // the button created by this exercise

	function unlocks(law); // add law to the laws unlocked by this exercise
	function unlockedBy(exercise2);  // add this exercise to the exercises unlocked by exercise2
}


// the undo button is constructed by createUndoButton().

UndoButton extends button {
	bool canUndo;  //  whether undo is available
    	element deletionList[]; // list  of elements to be deleted on undo
        int numlines;  // what to rewind numlines back to
	bool hasCircularity; // what to rewind hasCircularity back to
}


// inside the proof box there is an ordered list containing the proof.

proof extends orderedList {
	int numlines;  // number of lines in the proof
	bool hasCircularity;  // does the proof use something at or after the exercise?
}

// the exercise Box lists the exercise

ExerciseBox extends box {
	Exercise exercise;  // the current exercise
	ExerciseButton exerciseButton;  // the current exercise button
}

// a droppable text field for receiving arguments for operators and predicates

ArgDroppable extends span {
	OperatorItem li;  the list element the field belongs to
	int i;  the index of the field (1 or 2)
}

// a line item containing an operator or predicate in the Operators and Predicates window

OperatorItem extends li {
	Operator operator; // the operator in question (can also be Predicate)
	Term args[];  // the argument list (default "").
	ArgDroppable fields[];  // the list of text fields
}

// the box for an environment
environmentBox extends box {
	Assumption assumption;  // the assumption for this box
	string type;  // "environment"
}

// the box for a sentence

sentenceBox extends box {
	Sentence sentence;  // the ambient sentence;
	string type;  // "sentenceBox"
}

formulaBox extends box {
	Sentence sentence;  // the ambient sentence;
	string type;  // "formulaBox"
}

termBox extends box {
	Term term;  // the ambient term;
	string type;  // "termBox"
}




exerciseButton extends button {
	Exercise exercise;  // the exercise associated to button
	bool solved;  // has the exercise been solved yet?
	bool enabled;  // is the button eabled yet?
	String sectionTitle; // what is the title of the section the button is in?
}