|
| 1 | +/- |
| 2 | +Copyright (c) 2024 Damiano Testa. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Damiano Testa |
| 5 | +-/ |
| 6 | + |
| 7 | +import Lean.Elab.Command |
| 8 | +import Mathlib.Init |
| 9 | + |
| 10 | +/-! |
| 11 | +# The "ppRoundtrip" linter |
| 12 | +
|
| 13 | +The "ppRoundtrip" linter emits a warning when the syntax of a command differs substantially |
| 14 | +from the pretty-printed version of itself. |
| 15 | +-/ |
| 16 | +open Lean Elab Command |
| 17 | + |
| 18 | +namespace Mathlib.Linter |
| 19 | + |
| 20 | +/-- |
| 21 | +The "ppRoundtrip" linter emits a warning when the syntax of a command differs substantially |
| 22 | +from the pretty-printed version of itself. |
| 23 | +
|
| 24 | +The linter makes an effort to start the highlighting at the first difference. |
| 25 | +However, it may not always be successful. |
| 26 | +It also prints both the source code and the "expected code" in a 5-character radius from |
| 27 | +the first difference. |
| 28 | +-/ |
| 29 | +register_option linter.ppRoundtrip : Bool := { |
| 30 | + defValue := false |
| 31 | + descr := "enable the ppRoundtrip linter" |
| 32 | +} |
| 33 | + |
| 34 | +/-- `polishPP s` takes as input a `String` `s`, assuming that it is the output of |
| 35 | +pretty-printing a lean command. |
| 36 | +The main intent is to convert `s` to a reasonable candidate for a desirable source code format. |
| 37 | +The function first replaces consecutive whitespace sequences into a single space (` `), in an |
| 38 | +attempt to side-step line-break differences. |
| 39 | +After that, it applies some pre-emptive changes: |
| 40 | +* doc-module beginnings tend to have some whitespace following them, so we add a space back in; |
| 41 | +* name quotations such as ``` ``Nat``` get pretty-printed as ``` `` Nat```, so we remove a space |
| 42 | + after double back-ticks, but take care of adding one more for triple (or more) back-ticks; |
| 43 | +* `notation3` is not followed by a pretty-printer space, so we add it here (#15515). |
| 44 | +-/ |
| 45 | +def polishPP (s : String) : String := |
| 46 | + let s := s.split (·.isWhitespace) |
| 47 | + (" ".intercalate (s.filter (!·.isEmpty))) |
| 48 | + |>.replace "/-!" "/-! " |
| 49 | + |>.replace "``` " "``` " -- avoid losing an existing space after the triple back-ticks |
| 50 | + -- as a consequence of the following replacement |
| 51 | + |>.replace "`` " "``" -- weird pp ```#eval ``«Nat»``` pretty-prints as ```#eval `` «Nat»``` |
| 52 | + |>.replace "notation3(" "notation3 (" |
| 53 | + |>.replace "notation3\"" "notation3 \"" |
| 54 | + |
| 55 | +/-- `polishSource s` is similar to `polishPP s`, but expects the input to be actual source code. |
| 56 | +For this reason, `polishSource s` performs more conservative changes: |
| 57 | +it only replace all whitespace starting from a linebreak (`\n`) with a single whitespace. -/ |
| 58 | +def polishSource (s : String) : String × Array Nat := |
| 59 | + let split := s.split (· == '\n') |
| 60 | + let preWS := split.foldl (init := #[]) fun p q => |
| 61 | + let txt := q.trimLeft.length |
| 62 | + (p.push (q.length - txt)).push txt |
| 63 | + let preWS := preWS.eraseIdx 0 |
| 64 | + let s := (split.map .trimLeft).filter (· != "") |
| 65 | + (" ".intercalate (s.filter (!·.isEmpty)), preWS) |
| 66 | + |
| 67 | +/-- `posToShiftedPos lths diff` takes as input an array `lths` of natural numbers, |
| 68 | +and one further natural number `diff`. |
| 69 | +It adds up the elements of `lths` occupying the odd positions, as long as the sum of the |
| 70 | +elements in the even positions does not exceed `diff`. |
| 71 | +It returns the sum of the accumulated odds and `diff`. |
| 72 | +This is useful to figure out the difference between the output of `polishSource s` and `s` itself. |
| 73 | +It plays a role similar to the `fileMap`. -/ |
| 74 | +def posToShiftedPos (lths : Array Nat) (diff : Nat) : Nat := Id.run do |
| 75 | + let mut (ws, noWS) := (diff, 0) |
| 76 | + for con in [:lths.size / 2] do |
| 77 | + let curr := lths[2 * con]! |
| 78 | + if noWS + curr < diff then |
| 79 | + noWS := noWS + curr |
| 80 | + ws := ws + lths[2 * con + 1]! |
| 81 | + else |
| 82 | + break |
| 83 | + return ws |
| 84 | + |
| 85 | +/-- `zoomString str centre offset` returns the substring of `str` consisting of the `offset` |
| 86 | +characters around the `centre`th character. -/ |
| 87 | +def zoomString (str : String) (centre offset : Nat) : Substring := |
| 88 | + { str := str, startPos := ⟨centre - offset⟩, stopPos := ⟨centre + offset⟩ } |
| 89 | + |
| 90 | +/-- `capSourceInfo s p` "shortens" all end-position information in the `SourceInfo` `s` to be |
| 91 | +at most `p`, trimming down also the relevant substrings. -/ |
| 92 | +def capSourceInfo (s : SourceInfo) (p : Nat) : SourceInfo := |
| 93 | + match s with |
| 94 | + | .original leading pos trailing endPos => |
| 95 | + .original leading pos {trailing with stopPos := ⟨min endPos.1 p⟩} ⟨min endPos.1 p⟩ |
| 96 | + | .synthetic pos endPos canonical => |
| 97 | + .synthetic pos ⟨min endPos.1 p⟩ canonical |
| 98 | + | .none => s |
| 99 | + |
| 100 | +/-- `capSyntax stx p` applies `capSourceInfo · s` to all `SourceInfo`s in all |
| 101 | +`node`s, `atom`s and `ident`s contained in `stx`. |
| 102 | +
|
| 103 | +This is used to trim away all "fluff" that follows a command: comments and whitespace after |
| 104 | +a command get removed with `capSyntax stx stx.getTailPos?.get!`. |
| 105 | +-/ |
| 106 | +partial |
| 107 | +def capSyntax (stx : Syntax) (p : Nat) : Syntax := |
| 108 | + match stx with |
| 109 | + | .node si k args => .node (capSourceInfo si p) k (args.map (capSyntax · p)) |
| 110 | + | .atom si val => .atom (capSourceInfo si p) (val.take p) |
| 111 | + | .ident si r v pr => .ident (capSourceInfo si p) { r with stopPos := ⟨min r.stopPos.1 p⟩ } v pr |
| 112 | + | s => s |
| 113 | + |
| 114 | +namespace PPRoundtrip |
| 115 | + |
| 116 | +@[inherit_doc Mathlib.Linter.linter.ppRoundtrip] |
| 117 | +def ppRoundtrip : Linter where run := withSetOptionIn fun stx ↦ do |
| 118 | + unless Linter.getLinterValue linter.ppRoundtrip (← getOptions) do |
| 119 | + return |
| 120 | + if (← MonadState.get).messages.hasErrors then |
| 121 | + return |
| 122 | + let stx := capSyntax stx (stx.getTailPos?.getD default).1 |
| 123 | + let origSubstring := stx.getSubstring?.getD default |
| 124 | + let (real, lths) := polishSource origSubstring.toString |
| 125 | + let fmt ← (liftCoreM do PrettyPrinter.ppCategory `command stx <|> (do |
| 126 | + Linter.logLint linter.ppRoundtrip stx |
| 127 | + m!"The ppRoundtrip linter had some parsing issues: \ |
| 128 | + feel free to silence it with `set_option linter.ppRoundtrip false in` \ |
| 129 | + and report this error!" |
| 130 | + return real)) |
| 131 | + let st := polishPP fmt.pretty |
| 132 | + if st != real then |
| 133 | + let diff := real.firstDiffPos st |
| 134 | + let pos := posToShiftedPos lths diff.1 + origSubstring.startPos.1 |
| 135 | + let f := origSubstring.str.drop (pos) |
| 136 | + let extraLth := (f.takeWhile (· != st.get diff)).length |
| 137 | + let srcCtxt := zoomString real diff.1 5 |
| 138 | + let ppCtxt := zoomString st diff.1 5 |
| 139 | + Linter.logLint linter.ppRoundtrip (.ofRange ⟨⟨pos⟩, ⟨pos + extraLth + 1⟩⟩) |
| 140 | + m!"source context\n'{srcCtxt}'\n'{ppCtxt}'\npretty-printed context" |
| 141 | + |
| 142 | +initialize addLinter ppRoundtrip |
| 143 | + |
| 144 | +end Mathlib.Linter.PPRoundtrip |
0 commit comments