Process Shorthands

In order to make it convenient to enter large documents in putdown notation, it is convenient to use fromPutdown to enter some reserved content in the document that is preprocessed before evaluating the document.

The following are what we have for Shorthands. More might be added later.

• Scan for occurrences of the symbol <comma and mark its previous sibling's .continued attribute true. Then delete the <comma symbol.

• Scan for occurrences of the symbol given> and mark its next sibling as a given. If the next sibling has attribute .continued true then do the same for it's next sibling and iterate until a sibling is found that does not have that propoerty (or you run out of next siblings) Then delete the given> symbol.

• Scan a document looking for any of the following Shorthands and convert the next (>) or previous (<) sibling to the corresponding type in the asA column.

  Shorthand	mark asA
  'BIH>'	'BIH'
  'declare>'	'Declare'
  'rule>'	'Rule'
  'cases>'	'Cases'
  'subs>'	'Subs'
  'thm>'	'Theorem'
  '<thm'	'Theorem'
  'proof>'	'Proof'

• Scan for occurrences of the symbol rules>. Its next sibling should be an environment containing given Environments. Mark each child of the next sibling as a Rule and delete both the rules> symbol and the outer environment containing the newly marked Rules. This allows us to use an Environment to mark a lot of consecutive Rulesall at once and then ignore the wrapper Environment. For libraries this is cleaner than trying to mark every Rule withrule>` individually.

• Scan for occurrences of the symbol λ (or @ for backwards compatibility) and replace that with the symbol "LDE EFA" (which then will still print as '𝜆' but it's what is needed under the hood).

• Scan for occurrences of the symbols pairand triple, and replace them with the symbol "tuple".

• Scan for occurrences of the symbol then. They are intended to be a shorthand way to enter an If-then environment inline without using a shell. The 'then' should be between given siblings and one or more claim siblings in a continuation chain determined by commas. For example, If A,B,C then D,E,F will then be converted to the environment { :A :B :C D E F }. These cannot be nested. This is useful for both inserting If-then environments inline, and also for using them as the body of a declaration. Thus, for example you can say e.g. If A,B,C then D,E,F for some c or Let x be such that if A,B,C then D,E,F If you just want a conjunction you can also do D,E,F for some c or Let x be such that D,E,F

The Rule will then be replaced by the expanded version and the ≡ symbols removed, following the cyclic TFAE style of implications. For example, if the Rule has the form :{ a ≡ b c ≡ d } then it will be replaced by :{ {:a {b c}} {:{b c} d } {:d a} }.

• Scan for occurrences of the symbol ≡. They are intended to be a shorthand way to enter IFF rules (equivalences). The '≡' should be a child of a Rule environment, and should not be the first or last child. The Rule will then be replaced by the expanded version and the ≡ symbols removed, following the cyclic TFAE style of implications. For example, if the Rule has the form :{ a ≡ b c ≡ d } then it will be replaced by :{ {:a {b c}} {:{b c} d } {:d a} }.

• Scan for occurrences of the symbol ➤. If found it should be the first child of an Application whose second child is a symbol whose text is the text of the comment. Mark that Application with .ignore=true so it is ignored propositionally.

• Scan for occurrences of the symbol by and mark its previous sibling's .by attribute with the text of its next sibling, which must be a LurchSymbol. Then delete both the by and it's next sibling. Currently used by the Cases tool, the Substitution rule, the CAS tool, and the Arithmetic and Algebra tools.

• Scan for occurrences of the symbol ✔︎, ✗, and ⁉︎ and mark its previous sibling with .expectedResult 'valid', 'indeterminate', and 'invalid' respectively.

• Scan a document looking for the symbol <<, which we call a 'marker'. For every marker,

  • if the preceding sibling is an environment, attribute it as a BIH.

  • if the preceding sibling is a declaration, attribute it as a Declare,

  • in either case, finally, delete the marker.

Naturally we have to run this FIRST before anything else. These changes are made in-place - they don't return a copy of the document.

This does no error checking, so << has to be an outermost expression with a previous sibling and λ has to appear in some sensible location and so on.

Make both a normal and tracing peggy parser from the given string and capture and customize the error formatting, then return both parsers and the original parser (which throws errors but doesn't trace) in an array.