Add system declarations to the top of the document. These are reserved symbols that the user is not allowed to use. Currently they are 'LDE EFA' and '➤'.

Assign Proper Names

Rename any non-constant free symbol declared by a declaration by appending a #, followed by a canonical form of the body if it has one.

For bodies that have a binding we want to use the alpha-equivalent canonical form.

Common helper used by both replaceBindings and renameBindings to walk a tree and assign canonical bound variable names.

Interpret

This takes a raw user's document as an LC environment and preprocesses it in preparation for validation. It does the following:

• addSystemDeclarations(doc)
• processShorthands(doc)
• moveDeclaresToTop(doc)
• processTheorems(doc)
• processDeclarationBodies(doc)
• processLetEnvironments(doc)
• processBindings(doc)
• processRules(doc)
• assignProperNames(doc)
• markDeclaredSymbols(doc) When it is finished it marks the document as interpreted.

Mark Declared Symbols

Mark explicitly declared symbols s, throughout an LC by setting s.constant=true. Symbols consisting of a string of digits, decimals, and repeating decimals like 1.23[456] are automatically marked as constants.

Move Declare declarations to the top of the document.

Rename Bindings for Alpha Equivalence

Make all bindings canonical by assigning ProperNames x₀, x₁, ... to the bound variables in order.

Process Declaration Bodies

Append a copy of the bodies of all declarations immediately after its Declaration.

Process Let Environments

Get the Let's. If they don't start an environment, wrap them to make a valid Let-environment. We make this restriction, so that a Let-env is a type of LC that can be used as a rule premise and can only be satisfied by another Let-env. We don't upgrade that to a subclass for now.

TODO: consider upgrading let-envs to a subclass of environment

Process Rules

Check all of Rules to ensure they are the right type of LC. Convert them into formulas. If they have metavariables, mark them .ignore so they have no prop form. If they don't mark them as an Inst. Replace and rename their bound variables to y₀, y₁, ... to avoid classes with user variables with the same name.

Process the user's theorems

If a user specifies that a claim Environment is a Theorem, he is declaring that he wants to use it as a Rule after that (if we enable the option to allow users to enter Theorems... otherwise just let them enter them as ordinary claim environments like proofs that aren't marked asA Theorem but can be formatted as such).

But we want to mark his theorem as valid or invalid just like any other proof in addition to using it as a Rule. To accomplish this, we make an invisible copy of the Theorem immediately following the theorem, make that a formula, and label it as a Rule for future use. This does not have to be done if the Theorem has no metavariables as a Rule because it would be redundant. When a Rule copy of the user's Theorem is inserted it does not have to be marked as a given since it has no prop form, but its instantiations do. We flag the inserted Rule version of the Theorem as .userThm to distinguish it from ordinary Rules.

This has to be done after processing Shorthands and moving Declares to the top so the user's theorems are in the scope of declared constants in the library, which then prevents them from being metavariables.

If LurchOptions.swapTheoremProofPairs is true, and a Proof is the next sibling of the Theorem, swap the two of them first before inserting the .userThm Rule. This prevents the Theorem from being used in its own proof, which is done correctly if you don't swap them but is counterintuitive because mathematicians don't usually expect it to follow the rules of accessibilty in that situation.

Remove trailing givens

Remove any givens at the end of an environment because they have no propositional value.

(currently not used because of EquationsRule type rules where they won't be instantiated if they have just a claim as a constant. TODO: fix this correctly)

Rename bound variables for alpha equivalence (scope-aware)

This assigns canonical names x₀, x₁, etc. as the ProperName attribute of variables lexically bound in BindingExpressions. It avoids renaming variables that are free or outside the scope of any binding. This allows alpha equivalent expression to have the same propositional form.

Replace bound variables in formulas

This turns all bound variables in formulas to a canonical form like y₀, y₁, ... that cannot be entered by the user. Applying this to formulas before instantiating prevents variable capture.

Split Multiple Conclusion Environments

Find all given environments in the document which have more than one conclusion and split them into multiple propositionally equivalent environments with one conclusion each.