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 symbol declared by a declaration with body by appending the putdown form of their body. Rename any symbol in the scope of a Let-without body by appending a tick mark.

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

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`. The document containing the target must be specified to fetch the Declares.

TODO: Maybe upgrade to just compute doc from target.root()

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.

Rename bound variables for alpha equivalence

We also need alpha equivalent statements to have the same propositional form. This assigns canonical names x₀ , x₁ , etc. as the ProperName attribute of bound variables, and that is what .prop uses to make the propositional form.

Replace bound variables in formulas

Matching checks if a match would violate variable capture, but Formula.instantiate does not. So we need to turn all bound variables in formulas to a canonical form e.g. y₀, y₁, ... that cannot be entered by the user. Applying this to formulas before instantiating fixes that.

TODO:

• When making this permanent, just upgrade Formula.instantiate to respect ProperNames so we can delete this routine and just use the previous one instead.
• Also enforce the requirement that user's can't enter any of y₀, y₁, ... .
• We might want to keep the user's original bound formula variable names somewhere for feedback purposes, but the canonical ones aren't that bad for now.