The foundation of Parinfer relies on a few somewhat formalized definitions and
properties:
We wish to define properties that each Parinfer mode should exhibit.
With the following definitions:
- $I$ = (Indent Mode) function accepting code text and returning new text.
- $P$ = (Paren Mode) function accepting code text and returning new text.
- $R$ = (Reader) function accepting code text and returning its AST data.
The following should be true:
The actual operations performed by the modes rely on a formal definition
of what it means for Lisp code to be “correctly formatted”. We establish an
invariant— something that must be true for every line of code. From that,
Parinfer corrects indentation or parens simply by choosing correct values for
$i_n$ or $p_n$ (defined later) to satisfy this invariant:
The following is a concise reference (not a guide) to establishing this
invariant that Parinfer’s modes rely on.
We wish to define necessary conditions for determining if a given file of Lisp
code is “correctly formatted”.
We start with a clarification that we only consider non-empty lines (i.e. lines
that have at least one non-whitespace, non-comment token). Thus, all following
references to line number $n$ will refer to the $n$th non-empty line.
To proceed, we define the following:
- $t_n$ = (tokens) index of non-whitespace, non-comment tokens at line $n$
- $i_n$ = (indentation) x-position of $t_n[0]$
- $p_n$ = (parens) number of close-parens at the end of $t_n$
- $s_n$ = (stack) index of x-positions of all open-parens unclosed before $t_n[-p_n]$
Next, we define a function which determines if a line’s indentation is valid:
where:
Finally, we define that a file of Lisp code is “correctly formatted” if:
- for every line $n > 0$:
- and for the last line $N$
These rules are necessary and sufficient for determining when indentation is
what we consider “unambiguous”, but they are not sufficient in determining if
code is “pretty”. For example:
Formal descriptions of the actual operations performed by the modes are
pending, but informal ones follow in their respective sections below.
