From 15335efae28cbfa1bc826682660ede203dc02475 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 18 Dec 2020 08:00:22 -0800 Subject: [PATCH] refactor: move `Format` to `Init` package We are going to use it to define `Repr` class. --- src/Init/Data.lean | 1 + src/Init/Data/Format.lean | 272 ++++++++++++++++++++ src/Lean/Data/Format.lean | 288 +++------------------- src/Lean/Data/Json/Printer.lean | 2 +- src/Lean/Data/Trie.lean | 2 +- src/Lean/Hygiene.lean | 2 +- src/Lean/Parser/Extra.lean | 2 +- src/Lean/PrettyPrinter/Formatter.lean | 4 +- src/Lean/PrettyPrinter/Parenthesizer.lean | 2 +- src/Lean/Syntax.lean | 2 +- tests/lean/Format.lean | 6 +- tests/lean/PPRoundtrip.lean | 4 +- tests/lean/Reformat.lean | 2 +- tests/lean/run/Reparen.lean | 2 +- 14 files changed, 319 insertions(+), 272 deletions(-) create mode 100644 src/Init/Data/Format.lean diff --git a/src/Init/Data.lean b/src/Init/Data.lean index cbde3a49c9..02fe948ce1 100644 --- a/src/Init/Data.lean +++ b/src/Init/Data.lean @@ -22,3 +22,4 @@ import Init.Data.ToString import Init.Data.Range import Init.Data.Hashable import Init.Data.OfScientific +import Init.Data.Format diff --git a/src/Init/Data/Format.lean b/src/Init/Data/Format.lean new file mode 100644 index 0000000000..62c508a09d --- /dev/null +++ b/src/Init/Data/Format.lean @@ -0,0 +1,272 @@ +/- +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Leonardo de Moura +-/ +prelude +import Init.Control.State +import Init.Data.Int.Basic +import Init.Data.ToString.Macro + +namespace Std + +inductive Format.FlattenBehavior where + | allOrNone + | fill + deriving Inhabited, BEq + +open Format + +inductive Format where + | nil : Format + | line : Format + | text : String → Format + | nest (indent : Int) : Format → Format + | append : Format → Format → Format + | group : Format → (behavior : FlattenBehavior := FlattenBehavior.allOrNone) → Format + deriving Inhabited + +namespace Format +def fill (f : Format) : Format := + group f (behavior := FlattenBehavior.fill) + +@[export lean_format_append] +protected def appendEx (a b : Format) : Format := + append a b + +@[export lean_format_group] +protected def groupEx : Format → Format := + group + +instance : Append Format := ⟨Format.append⟩ +instance : Coe String Format := ⟨text⟩ + +def join (xs : List Format) : Format := + xs.foldl (·++·) "" + +def isNil : Format → Bool + | nil => true + | _ => false + +private structure SpaceResult where + foundLine : Bool := false + foundFlattenedHardLine : Bool := false + space : Nat := 0 + deriving Inhabited + +@[inline] private def merge (w : Nat) (r₁ : SpaceResult) (r₂ : Nat → SpaceResult) : SpaceResult := + if r₁.space > w || r₁.foundLine then + r₁ + else + let r₂ := r₂ (w - r₁.space); + { r₂ with space := r₁.space + r₂.space } + +private def spaceUptoLine : Format → Bool → Nat → SpaceResult + | nil, flatten, w => {} + | line, flatten, w => if flatten then { space := 1 } else { foundLine := true } + | text s, flatten, w => + let p := s.posOf '\n'; + let off := s.offsetOfPos p; + { foundLine := p != s.bsize, foundFlattenedHardLine := flatten && p != s.bsize, space := off } + | append f₁ f₂, flatten, w => merge w (spaceUptoLine f₁ flatten w) (spaceUptoLine f₂ flatten) + | nest _ f, flatten, w => spaceUptoLine f flatten w + | group f _, _, w => spaceUptoLine f true w + +private structure WorkItem where + f : Format + indent : Int + +private structure WorkGroup where + flatten : Bool + flb : FlattenBehavior + items : List WorkItem + +private partial def spaceUptoLine' : List WorkGroup → Nat → SpaceResult + | [], w => {} + | { items := [], .. }::gs, w => spaceUptoLine' gs w + | g@{ items := i::is, .. }::gs, w => merge w (spaceUptoLine i.f g.flatten w) (spaceUptoLine' ({ g with items := is }::gs)) + +private structure State where + out : String := "" + column : Nat := 0 + +private def pushGroup (flb : FlattenBehavior) (items : List WorkItem) (gs : List WorkGroup) (w : Nat) : StateM State (List WorkGroup) := do + let k := (← get).column + -- Flatten group if it + the remainder (gs) fits in the remaining space. For `fill`, measure only up to the next (ungrouped) line break. + let g := { flatten := flb == FlattenBehavior.allOrNone, flb := flb, items := items : WorkGroup } + let r := spaceUptoLine' [g] (w-k) + let r' := merge (w-k) r (spaceUptoLine' gs); + -- Prevent flattening if any item contains a hard line break, except within `fill` if it is ungrouped (=> unflattened) + return { g with flatten := !r.foundFlattenedHardLine && r'.space <= w-k }::gs + +private def pushOutput (s : String) : StateM State Unit := + modify fun st => { st with out := st.out ++ s, column := st.column + s.length } + +private def pushNewline (indent : Nat) : StateM State Unit := + modify fun st => { st with out := st.out ++ "\n".pushn ' ' indent, column := indent } + +private partial def be (w : Nat) : List WorkGroup → StateM State Unit + | [] => pure () + | { items := [], .. }::gs => be w gs + | g@{ items := i::is, .. }::gs => do + let gs' (is' : List WorkItem) := { g with items := is' }::gs; + match i.f with + | nil => be w (gs' is) + | append f₁ f₂ => be w (gs' ({ i with f := f₁ }::{ i with f := f₂ }::is)) + | nest n f => be w (gs' ({ i with f := f, indent := i.indent + n }::is)) + | text s => + let p := s.posOf '\n' + if p == s.bsize then + pushOutput s + be w (gs' is) + else + pushOutput (s.extract 0 p) + pushNewline i.indent.toNat + let is := { i with f := s.extract (s.next p) s.bsize }::is + -- after a hard line break, re-evaluate whether to flatten the remaining group + pushGroup g.flb is gs w >>= be w + | line => + match g.flb with + | FlattenBehavior.allOrNone => + if g.flatten then + -- flatten line = text " " + pushOutput " " + be w (gs' is) + else + pushNewline i.indent.toNat + be w (gs' is) + | FlattenBehavior.fill => + let breakHere := do + pushNewline i.indent.toNat + -- make new `fill` group and recurse + pushGroup FlattenBehavior.fill is gs w >>= be w + -- if preceding fill item fit in a single line, try to fit next one too + if g.flatten then + let gs'@(g'::_) ← pushGroup FlattenBehavior.fill is gs (w - " ".length) + | unreachable! + if g'.flatten then + pushOutput " "; + be w gs' -- TODO: use `return` + else + breakHere + else + breakHere + | group f flb => + if g.flatten then + -- flatten (group f) = flatten f + be w (gs' ({ i with f := f }::is)) + else + pushGroup flb [{ i with f := f }] (gs' is) w >>= be w + +@[inline] def bracket (l : String) (f : Format) (r : String) : Format := + group (nest l.length $ l ++ f ++ r) + +@[inline] def paren (f : Format) : Format := + bracket "(" f ")" + +@[inline] def sbracket (f : Format) : Format := + bracket "[" f "]" + +def defIndent := 2 +def defUnicode := true +def defWidth := 120 + +@[export lean_format_pretty] +def pretty (f : Format) (w : Nat := defWidth) : String := + let (_, st) := be w [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent := 0 }] }] {}; + st.out + +end Format + +class ToFormat (α : Type u) where + format : α → Format + +export ToFormat (format) + +def fmt {α : Type u} [ToFormat α] : α → Format := format + +syntax:max "f!" interpolatedStr(term) : term + +macro_rules + | `(f! $interpStr) => do interpStr.expandInterpolatedStr (← `(Format)) (← `(fmt)) + +instance {α : Type u} [ToString α] : ToFormat α := ⟨text ∘ toString⟩ + +-- note: must take precendence over the above instance to avoid premature formatting +instance : ToFormat Format where + format f := f + +instance : ToFormat String where + format s := Format.text s + +def Format.joinSep {α : Type u} [ToFormat α] : List α → Format → Format + | [], sep => nil + | [a], sep => format a + | a::as, sep => format a ++ sep ++ joinSep as sep + +def Format.prefixJoin {α : Type u} [ToFormat α] (pre : Format) : List α → Format + | [] => nil + | a::as => pre ++ format a ++ prefixJoin pre as + +def Format.joinSuffix {α : Type u} [ToFormat α] : List α → Format → Format + | [], suffix => nil + | a::as, suffix => format a ++ suffix ++ joinSuffix as suffix + +def Format.joinArraySep {α : Type u} [ToFormat α] (as : Array α) (sep : Format) : Format := do + let mut r := nil + let mut i := 0 + for a in as do + if i > 0 then + r := r ++ sep ++ format a + else + r := r ++ format a + i := i + 1 + return r + +instance : ToFormat Nat where + format n := toString n + +instance : ToFormat UInt16 where + format n := toString n + +instance : ToFormat UInt32 where + format n := toString n + +instance : ToFormat UInt64 where + format n := toString n + +instance : ToFormat USize where + format n := toString n + +instance : ToString Format where + toString f := f.pretty + +end Std + +open Std +open Std.Format + +def List.format [ToFormat α] : List α → Format + | [] => "[]" + | xs => sbracket $ Format.joinSep xs ("," ++ line) + +instance [ToFormat α] : ToFormat (List α) where + format := List.format + +instance [ToFormat α] : ToFormat (Array α) where + format a := "#" ++ fmt a.toList + +def Option.format {α : Type u} [ToFormat α] : Option α → Format + | none => "none" + | some a => "some " ++ fmt a + +instance {α : Type u} [ToFormat α] : ToFormat (Option α) where + format + | none => "none" + | some a => "some " ++ fmt a + +instance {α : Type u} {β : Type v} [ToFormat α] [ToFormat β] : ToFormat (Prod α β) where + format := fun (a, b) => paren <| format a ++ "," ++ line ++ format b + +def String.toFormat (s : String) : Std.Format := + Std.Format.joinSep (s.splitOn "\n") Std.Format.line diff --git a/src/Lean/Data/Format.lean b/src/Lean/Data/Format.lean index 085411ad90..b0f6262634 100644 --- a/src/Lean/Data/Format.lean +++ b/src/Lean/Data/Format.lean @@ -6,170 +6,9 @@ Author: Leonardo de Moura import Lean.Data.Options universes u v -namespace Lean +namespace Std namespace Format - -inductive FlattenBehavior where - | allOrNone - | fill - deriving Inhabited, BEq - -end Format - -open Format - -inductive Format where - | nil : Format - | line : Format - | text : String → Format - | nest (indent : Int) : Format → Format - | append : Format → Format → Format - | group : Format → (behavior : FlattenBehavior := FlattenBehavior.allOrNone) → Format - deriving Inhabited - -namespace Format -def fill (f : Format) : Format := - group f (behavior := FlattenBehavior.fill) - -@[export lean_format_append] -protected def appendEx (a b : Format) : Format := - append a b - -@[export lean_format_group] -protected def groupEx : Format → Format := - group - -instance : Append Format := ⟨Format.append⟩ -instance : Coe String Format := ⟨text⟩ - -def join (xs : List Format) : Format := - xs.foldl (·++·) "" - -def isNil : Format → Bool - | nil => true - | _ => false - -private structure SpaceResult where - foundLine : Bool := false - foundFlattenedHardLine : Bool := false - space : Nat := 0 - deriving Inhabited - -@[inline] private def merge (w : Nat) (r₁ : SpaceResult) (r₂ : Nat → SpaceResult) : SpaceResult := - if r₁.space > w || r₁.foundLine then r₁ - else - let r₂ := r₂ (w - r₁.space); - { r₂ with space := r₁.space + r₂.space } - -private def spaceUptoLine : Format → Bool → Nat → SpaceResult - | nil, flatten, w => {} - | line, flatten, w => if flatten then { space := 1 } else { foundLine := true } - | text s, flatten, w => - let p := s.posOf '\n'; - let off := s.offsetOfPos p; - { foundLine := p != s.bsize, foundFlattenedHardLine := flatten && p != s.bsize, space := off } - | append f₁ f₂, flatten, w => merge w (spaceUptoLine f₁ flatten w) (spaceUptoLine f₂ flatten) - | nest _ f, flatten, w => spaceUptoLine f flatten w - | group f _, _, w => spaceUptoLine f true w - -private structure WorkItem where - f : Format - indent : Int - -private structure WorkGroup where - flatten : Bool - flb : FlattenBehavior - items : List WorkItem - -private partial def spaceUptoLine' : List WorkGroup → Nat → SpaceResult - | [], w => {} - | { items := [], .. }::gs, w => spaceUptoLine' gs w - | g@{ items := i::is, .. }::gs, w => merge w (spaceUptoLine i.f g.flatten w) (spaceUptoLine' ({ g with items := is }::gs)) - -private structure State where - out : String := "" - column : Nat := 0 - -private def pushGroup (flb : FlattenBehavior) (items : List WorkItem) (gs : List WorkGroup) (w : Nat) : StateM State (List WorkGroup) := do - let k := (← get).column - -- Flatten group if it + the remainder (gs) fits in the remaining space. For `fill`, measure only up to the next (ungrouped) line break. - let g := { flatten := flb == FlattenBehavior.allOrNone, flb := flb, items := items : WorkGroup } - let r := spaceUptoLine' [g] (w-k) - let r' := merge (w-k) r (spaceUptoLine' gs); - -- Prevent flattening if any item contains a hard line break, except within `fill` if it is ungrouped (=> unflattened) - return { g with flatten := !r.foundFlattenedHardLine && r'.space <= w-k }::gs - -private def pushOutput (s : String) : StateM State Unit := - modify fun st => { st with out := st.out ++ s, column := st.column + s.length } - -private def pushNewline (indent : Nat) : StateM State Unit := - modify fun st => { st with out := st.out ++ "\n".pushn ' ' indent, column := indent } - -private partial def be (w : Nat) : List WorkGroup → StateM State Unit - | [] => pure () - | { items := [], .. }::gs => be w gs - | g@{ items := i::is, .. }::gs => do - let gs' (is' : List WorkItem) := { g with items := is' }::gs; - match i.f with - | nil => be w (gs' is) - | append f₁ f₂ => be w (gs' ({ i with f := f₁ }::{ i with f := f₂ }::is)) - | nest n f => be w (gs' ({ i with f := f, indent := i.indent + n }::is)) - | text s => - let p := s.posOf '\n' - if p == s.bsize then - pushOutput s - be w (gs' is) - else - pushOutput (s.extract 0 p) - pushNewline i.indent.toNat - let is := { i with f := s.extract (s.next p) s.bsize }::is - -- after a hard line break, re-evaluate whether to flatten the remaining group - pushGroup g.flb is gs w >>= be w - | line => - match g.flb with - | FlattenBehavior.allOrNone => - if g.flatten then - -- flatten line = text " " - pushOutput " " - be w (gs' is) - else - pushNewline i.indent.toNat - be w (gs' is) - | FlattenBehavior.fill => - let breakHere := do - pushNewline i.indent.toNat - -- make new `fill` group and recurse - pushGroup FlattenBehavior.fill is gs w >>= be w - -- if preceding fill item fit in a single line, try to fit next one too - if g.flatten then - let gs'@(g'::_) ← pushGroup FlattenBehavior.fill is gs (w - " ".length) - | unreachable! - if g'.flatten then - pushOutput " "; - be w gs' -- TODO: use `return` - else - breakHere - else - breakHere - | group f flb => - if g.flatten then - -- flatten (group f) = flatten f - be w (gs' ({ i with f := f }::is)) - else - pushGroup flb [{ i with f := f }] (gs' is) w >>= be w - -@[inline] def bracket (l : String) (f : Format) (r : String) : Format := - group (nest l.length $ l ++ f ++ r) - -@[inline] def paren (f : Format) : Format := - bracket "(" f ")" - -@[inline] def sbracket (f : Format) : Format := - bracket "[" f "]" - -def defIndent := 2 -def defUnicode := true -def defWidth := 120 +open Lean def getWidth (o : Options) : Nat := o.get `format.width defWidth def getIndent (o : Options) : Nat := o.get `format.indent defIndent @@ -180,86 +19,10 @@ builtin_initialize registerOption `format.unicode { defValue := defUnicode, group := "format", descr := "unicode characters" } registerOption `format.width { defValue := defWidth, group := "format", descr := "line width" } -@[export lean_format_pretty] -def prettyAux (f : Format) (w : Nat := defWidth) : String := - let (_, st) := be w [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent := 0 }] }] {}; - st.out +def pretty' (f : Format) (o : Options := {}) : String := + pretty f (getWidth o) -def pretty (f : Format) (o : Options := {}) : String := - prettyAux f (getWidth o) - -end Format - -open Lean.Format - -class ToFormat (α : Type u) where - format : α → Format - -export Lean.ToFormat (format) - -def fmt {α : Type u} [ToFormat α] : α → Format := format - -syntax:max "f!" interpolatedStr(term) : term - -macro_rules - | `(f! $interpStr) => do interpStr.expandInterpolatedStr (← `(Format)) (← `(fmt)) - -instance {α : Type u} [ToString α] : ToFormat α := ⟨text ∘ toString⟩ - --- note: must take precendence over the above instance to avoid premature formatting -instance : ToFormat Format := ⟨id⟩ -instance : ToFormat String := ⟨Format.text⟩ - -def Format.joinSep {α : Type u} [ToFormat α] : List α → Format → Format - | [], sep => nil - | [a], sep => format a - | a::as, sep => format a ++ sep ++ joinSep as sep - -def Format.prefixJoin {α : Type u} [ToFormat α] (pre : Format) : List α → Format - | [] => nil - | a::as => pre ++ format a ++ prefixJoin pre as - -def Format.joinSuffix {α : Type u} [ToFormat α] : List α → Format → Format - | [], suffix => nil - | a::as, suffix => format a ++ suffix ++ joinSuffix as suffix - -def List.format {α : Type u} [ToFormat α] : List α → Format - | [] => "[]" - | xs => sbracket $ Format.joinSep xs ("," ++ line) - -instance {α : Type u} [ToFormat α] : ToFormat (List α) := ⟨List.format⟩ - -instance {α : Type u} [ToFormat α] : ToFormat (Array α) := ⟨fun a => "#" ++ fmt a.toList⟩ - -def Option.format {α : Type u} [ToFormat α] : Option α → Format - | none => "none" - | some a => "some " ++ fmt a - -instance {α : Type u} [ToFormat α] : ToFormat (Option α) := ⟨Option.format⟩ - -instance {α : Type u} {β : Type v} [ToFormat α] [ToFormat β] : ToFormat (Prod α β) := ⟨fun ⟨a, b⟩ => - paren $ format a ++ "," ++ line ++ format b -⟩ - -def Format.joinArraySep {α : Type u} [ToFormat α] (as : Array α) (sep : Format) : Format := do - let mut r := nil - let mut i := 0 - for a in as do - if i > 0 then - r := r ++ sep ++ format a - else - r := r ++ format a - i := i + 1 - return r - -instance : ToFormat Nat := ⟨fun n => toString n⟩ -instance : ToFormat UInt16 := ⟨fun n => toString n⟩ -instance : ToFormat UInt32 := ⟨fun n => toString n⟩ -instance : ToFormat UInt64 := ⟨fun n => toString n⟩ -instance : ToFormat USize := ⟨fun n => toString n⟩ -instance : ToFormat Name := ⟨fun n => n.toString⟩ - -protected def Format.repr : Format → Format +protected def repr : Format → Format | nil => "Format.nil" | line => "Format.line" | text s => paren $ "Format.text" ++ line ++ repr s @@ -268,23 +31,37 @@ protected def Format.repr : Format → Format | group f FlattenBehavior.allOrNone => paren $ "Format.group" ++ line ++ Format.repr f | group f FlattenBehavior.fill => paren $ "Format.fill" ++ line ++ Format.repr f -instance : ToString Format := ⟨Format.pretty⟩ +instance : Repr Format where + repr := Format.pretty ∘ Format.repr -instance : Repr Format := ⟨Format.pretty ∘ Format.repr⟩ +end Format +end Std -def formatDataValue : DataValue → Format - | DataValue.ofString v => format (repr v) - | DataValue.ofBool v => format v - | DataValue.ofName v => "`" ++ format v - | DataValue.ofNat v => format v - | DataValue.ofInt v => format v +namespace Lean +open Std -instance : ToFormat DataValue := ⟨formatDataValue⟩ +export Std + (Format ToFormat fmt Format.nest Format.nil Format.joinSep Format.line + Format.sbracket Format.bracket Format.group Format.pretty Format.fill Format.paren Format.join) +export Std.ToFormat (format) -def formatEntry : Name × DataValue → Format - | (n, v) => format n ++ " := " ++ format v +instance : ToFormat Name where + format n := n.toString -instance : ToFormat (Name × DataValue) := ⟨formatEntry⟩ +instance : ToFormat DataValue where + format + | DataValue.ofString v => format (repr v) + | DataValue.ofBool v => format v + | DataValue.ofName v => "`" ++ format v + | DataValue.ofNat v => format v + | DataValue.ofInt v => format v + +instance : ToFormat (Name × DataValue) where + format + | (n, v) => format n ++ " := " ++ format v + + +open Std.Format def formatKVMap (m : KVMap) : Format := sbracket (Format.joinSep m.entries ", ") @@ -292,6 +69,3 @@ def formatKVMap (m : KVMap) : Format := instance : ToFormat KVMap := ⟨formatKVMap⟩ end Lean - -def String.toFormat (s : String) : Lean.Format := - Lean.Format.joinSep (s.splitOn "\n") Lean.Format.line diff --git a/src/Lean/Data/Json/Printer.lean b/src/Lean/Data/Json/Printer.lean index c8c4244ad9..6ddfec24b7 100644 --- a/src/Lean/Data/Json/Printer.lean +++ b/src/Lean/Data/Json/Printer.lean @@ -65,7 +65,7 @@ partial def render : Json → Format end def pretty (j : Json) (lineWidth := 80) : String := - Format.prettyAux (render j) lineWidth + Format.pretty (render j) lineWidth partial def compress : Json → String | null => "null" diff --git a/src/Lean/Data/Trie.lean b/src/Lean/Data/Trie.lean index e3412dbb75..c95446cc78 100644 --- a/src/Lean/Data/Trie.lean +++ b/src/Lean/Data/Trie.lean @@ -82,7 +82,7 @@ partial def matchPrefix (s : String) (t : Trie α) (i : String.Pos) : String.Pos private partial def toStringAux {α : Type} : Trie α → List Format | Trie.Node val map => map.fold (fun Fs c t => - format (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) [] + format (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) [] instance {α : Type} : ToString (Trie α) := ⟨fun t => (flip Format.joinSep Format.line $ toStringAux t).pretty⟩ diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean index fda906df9d..fe398fd1ff 100644 --- a/src/Lean/Hygiene.lean +++ b/src/Lean/Hygiene.lean @@ -78,7 +78,7 @@ structure NameSanitizerState where private partial def mkFreshInaccessibleUserName (userName : Name) (idx : Nat) : StateM NameSanitizerState Name := do let s ← get - let userNameNew := mkInaccessibleUserName (Format.getUnicode s.options) (Name.mkNum userName idx) + let userNameNew := mkInaccessibleUserName (Std.Format.getUnicode s.options) (Name.mkNum userName idx) if s.nameStem2Idx.contains userNameNew then mkFreshInaccessibleUserName userName (idx+1) else do diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index 5653171506..aaf90b2f0f 100644 --- a/src/Lean/Parser/Extra.lean +++ b/src/Lean/Parser/Extra.lean @@ -88,7 +88,7 @@ open PrettyPrinter @[combinatorFormatter Lean.Parser.ppIndent] def ppIndent.formatter (p : Formatter) : Formatter := Formatter.indent p @[combinatorFormatter Lean.Parser.ppDedent] def ppDedent.formatter (p : Formatter) : Formatter := do let opts ← getOptions - Formatter.indent p (some ((0:Int) - Format.getIndent opts)) + Formatter.indent p (some ((0:Int) - Std.Format.getIndent opts)) end namespace Parser diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 9cda686758..38a853b5c6 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -135,7 +135,7 @@ def concat (x : FormatterM Unit) : FormatterM Unit := do def indent (x : Formatter) (indent : Option Int := none) : Formatter := do concat x let ctx ← read - let indent := indent.getD $ Format.getIndent ctx.options + let indent := indent.getD $ Std.Format.getIndent ctx.options modify fun st => { st with stack := st.stack.pop.push (Format.nest indent st.stack.back) } def group (x : Formatter) : Formatter := do @@ -293,7 +293,7 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do if ws.contains '\n' then do -- Indentation is automatically increased when entering a category, but comments should be aligned -- with the actual token, so dedent - indent (push s!"{ss'}\n") (some ((0:Int) - Format.getIndent (← getOptions))) + indent (push s!"{ss'}\n") (some ((0:Int) - Std.Format.getIndent (← getOptions))) else push s!"{ss'} " modify fun st => { st with leadWord := "" } diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 597380776a..192e487c5b 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -164,7 +164,7 @@ unsafe def mkCombinatorParenthesizerAttribute : IO ParserCompiler.CombinatorAttr namespace Parenthesizer open Lean.Core -open Lean.Format +open Std.Format def throwBacktrack {α} : ParenthesizerM α := throw $ Exception.internal backtrackExceptionId diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index 460076f4b1..822f724118 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -200,7 +200,7 @@ partial def reprint : Syntax → Option String else args.foldlM (fun r stx => do let s ← reprint stx; pure $ r ++ s) "" | _ => "" -open Lean.Format +open Std.Format private def formatInfo (showInfo : Bool) (info : SourceInfo) (f : Format) : Format := if showInfo then diff --git a/tests/lean/Format.lean b/tests/lean/Format.lean index e3367b06a2..b2bbe415ad 100644 --- a/tests/lean/Format.lean +++ b/tests/lean/Format.lean @@ -1,10 +1,10 @@ #lang lean4 -import Lean.Data.Format open Lean -open Lean.Format +open Std +open Std.Format def eval (w : Nat) (f : Format) : IO Unit := do -IO.println $ f.prettyAux w +IO.println $ f.pretty w -- hard line breaks should re-evaluate flattening behavior within group #eval eval 5 $ fill (text "a" ++ line ++ text "b\nlooooooooong" ++ line ++ text "c") ++ line ++ text "d" diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index 711ff0f83e..fa956ea21e 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -4,7 +4,7 @@ open Lean open Lean.Elab open Lean.Elab.Term open Lean.Elab.Command -open Lean.Format +open Std.Format open Std open Lean.PrettyPrinter open Lean.Meta @@ -15,7 +15,7 @@ let stx ← stx let e ← elabTermAndSynthesize stx none <* throwErrorIfErrors let stx' ← delab Name.anonymous [] e optionsPerPos let f' ← PrettyPrinter.ppTerm stx' -let s := f'.pretty opts +let s := f'.pretty' opts IO.println s let env ← getEnv match Parser.runParserCategory env `term s "" with diff --git a/tests/lean/Reformat.lean b/tests/lean/Reformat.lean index 4ffa5c1697..53f4310398 100644 --- a/tests/lean/Reformat.lean +++ b/tests/lean/Reformat.lean @@ -4,7 +4,7 @@ import Lean.PrettyPrinter open Lean open Lean.Elab open Lean.Elab.Term -open Lean.Format +open Std.Format open Std unsafe def main (args : List String) : IO Unit := do let (debug, f) : Bool × String := match args with diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean index c67e8b9666..18ba96d65e 100644 --- a/tests/lean/run/Reparen.lean +++ b/tests/lean/run/Reparen.lean @@ -2,7 +2,7 @@ import Lean.Parser open Lean -open Lean.Format +open Std.Format open Std def unparenAux (parens body : Syntax) : Syntax := match parens.getHeadInfo, body.getHeadInfo, body.getTailInfo, parens.getTailInfo with