Lean4
/-- Scan the two input strings `L` and `M`, assuming `M` is the pretty-printed version of `L`.
This almost means that `L` and `M` only differ in whitespace.
While scanning the two strings, accumulate any discrepancies --- with some heuristics to avoid
flagging some line-breaking changes.
(The pretty-printer does not always produce desirably formatted code.)
-/
partial def parallelScanAux (as : Array FormatError) (L M : String) : Array FormatError :=
if M.trim.isEmpty then as
else
-- We try as hard as possible to scan the strings one character at a time.
-- However, single line comments introduced with `--` pretty-print differently than `/--`.
-- So, we first look ahead for `/--`: the linter will later ignore doc-strings, so it does not
-- matter too much what we do here and we simply drop `/--` from the original string and the
-- pretty-printed one, before continuing.
-- Next, if we already dealt with `/--`, finding a `--` means that this is a single line comment
-- (or possibly a comment embedded in a doc-string, which is ok, since we eventually discard
-- doc-strings). In this case, we drop everything until the following line break in the
-- original syntax, and for the same amount of characters in the pretty-printed one, since the
-- pretty-printer *erases* the line break at the end of a single line comment.
if L.take 3 == "/--" && M.take 3 == "/--" then parallelScanAux as (L.drop 3) (M.drop 3)
else
if L.take 2 == "--" then
let newL := L.dropWhile (· != '\n')
let diff := L.length - newL.length
let newM := M.dropWhile (· != '-') |>.drop diff
parallelScanAux as newL.trimLeft newM.trimLeft
else
if L.take 2 == "-/" then
let newL := L.drop 2 |>.trimLeft
let newM := M.drop 2 |>.trimLeft
parallelScanAux as newL newM
else
let ls := L.drop 1
let ms := M.drop 1
match L.get 0, M.get 0 with
| ' ', m =>
if m.isWhitespace then parallelScanAux as ls ms.trimLeft
else parallelScanAux (pushFormatError as (mkFormatError L M "extra space")) ls M
| '\n', m =>
if m.isWhitespace then parallelScanAux as ls.trimLeft ms.trimLeft
else parallelScanAux (pushFormatError as (mkFormatError L M "remove line break")) ls.trimLeft M
| l, m => -- `l` is not whitespace
if l == m then parallelScanAux as ls ms
else
if m.isWhitespace then
parallelScanAux (pushFormatError as (mkFormatError L M "missing space")) L ms.trimLeft
else
-- If this code is reached, then `L` and `M` differ by something other than whitespace.
-- This should not happen in practice.
pushFormatError as (mkFormatError ls ms "Oh no! (Unreachable?)")
