Init.Data.Format.Basic

/-- Determines how groups should have linebreaks inserted when the
text would overfill its remaining space.

- `allOrNone` will make a linebreak on every `Format.line` in the group or none of them.
  ```
  [1,
   2,
   3]
  ```
- `fill` will only make linebreaks on as few `Format.line`s as possible:
  ```
  [1, 2,
   3]
  ```
-/
inductive Format.FlattenBehavior where
  | allOrNone
  | fill
  deriving Inhabited, BEq

Inhabited, BEq

BEq

/-- A string with pretty-printing information for rendering in a column-width-aware way.

The pretty-printing algorithm is based on Wadler's paper
[_A Prettier Printer_](https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf). -/
inductive Format where
  /-- The empty format. -/
  | nil                 : Format
  /-- A position where a newline may be inserted
  if the current group does not fit within the allotted column width. -/
  | line                : Format
  /-- `align` tells the formatter to pad with spaces to the current indent,
  or else add a newline if we are already at or past the indent. For example:
  ```
  nest 2 <| "." ++ align ++ "a" ++ line ++ "b"
  ```
  results in:
  ```
  . a
    b
  ```
  If `force` is true, then it will pad to the indent even if it is in a flattened group.
  -/
  | align (force : Bool) : Format
  /-- A node containing a plain string. -/
  | text                : String → Format
  /-- `nest n f` tells the formatter that `f` is nested inside something with length `n`
  so that it is pretty-printed with the correct indentation on a line break.
  For example, we can define a formatter for list `l : List Format` as:

  ```
  let f := join <| l.intersperse <| ", " ++ Format.line
  group (nest 1 <| "[" ++ f ++ "]")
  ```

  This will be written all on one line, but if the text is too large,
  the formatter will put in linebreaks after the commas and indent later lines by 1.
  -/
  | nest (indent : Int) : Format → Format
  /-- Concatenation of two Formats. -/
  | append              : Format → Format → Format
  /-- Creates a new flattening group for the given inner format.  -/
  | group               : Format → (behavior : FlattenBehavior := FlattenBehavior.allOrNone) → Format
  /-- Used for associating auxiliary information (e.g. `Expr`s) with `Format` objects. -/
  | tag                 : Nat → Format → Format
  deriving Inhabited

Inhabited

/-- Check whether the given format contains no characters. -/
def isEmpty : Format → Bool
  | nil          => true
  | line         => false
  | align _      => true
  | text msg     => msg == ""
  | nest _ f     => f.isEmpty
  | append f₁ f₂ => f₁.isEmpty && f₂.isEmpty
  | group f _    => f.isEmpty
  | tag _ f      => f.isEmpty

/-- Alias for a group with `FlattenBehavior` set to `fill`. -/
def fill (f : Format) : Format :=
  group f (behavior := FlattenBehavior.fill)

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

Inhabited

/-- A monad in which we can pretty-print `Format` objects. -/
class MonadPrettyFormat (m : Type → Type) where
  pushOutput (s : String)    : m Unit
  pushNewline (indent : Nat) : m Unit
  currColumn                 : m Nat
  /-- Start a scope tagged with `n`. -/
  startTag                   : Nat → m Unit
  /-- Exit the scope of `n`-many opened tags. -/
  endTags                    : Nat → m Unit

/-- Create a format `l ++ f ++ r` with a flatten group.
FlattenBehaviour is `allOrNone`; for `fill` use `bracketFill`. -/
@[inline] def bracket (l : String) (f : Format) (r : String) : Format :=
  group (nest l.length $ l ++ f ++ r)

/-- Creates the format `"(" ++ f ++ ")"` with a flattening group.-/
@[inline] def paren (f : Format) : Format :=
  bracket "(" f ")"

/-- Creates the format `"[" ++ f ++ "]"` with a flattening group.-/
@[inline] def sbracket (f : Format) : Format :=
  bracket "[" f "]"

/-- Same as `bracket` except uses the `fill` flattening behaviour. -/
@[inline] def bracketFill (l : String) (f : Format) (r : String) : Format :=
  fill (nest l.length $ l ++ f ++ r)

/-- Default indentation. -/
def defIndent  := 2

def defUnicode := true

/-- Default width of the targeted output pane. -/
def defWidth   := 120

/-- Nest with the default indentation amount.-/
def nestD (f : Format) : Format :=
  nest defIndent f

/-- Insert a newline and then `f`, all nested by the default indent amount. -/
def indentD (f : Format) : Format :=
  nestD (Format.line ++ f)

instance : MonadPrettyFormat (StateM State) where
  -- We avoid a structure instance update, and write these functions using pattern matching because of issue #316
  pushOutput s       := modify fun ⟨out, col⟩ => ⟨out ++ s, col + s.length⟩
  pushNewline indent := modify fun ⟨out, _⟩ => ⟨out ++ "\n".pushn ' ' indent, indent⟩
  currColumn         := return (← get).column
  startTag _         := return ()
  endTags _          := return ()

/-- Class for converting a given type α to a `Format` object for pretty-printing.
See also `Repr`, which also outputs a `Format` object. -/
class ToFormat (α : Type u) where
  format : α → Format

instance : ToFormat Format where
  format f := f

instance : ToFormat String where
  format s := Format.text s

/-- Intersperse the given list (each item printed with `format`) with the given `sep` format. -/
def Format.joinSep {α : Type u} [ToFormat α] : List α → Format → Format
  | [],    _   => nil
  | [a],   _   => format a
  | a::as, sep => as.foldl (· ++ sep ++ format ·) (format a)

/-- Format each item in `items` and prepend prefix `pre`. -/
def Format.prefixJoin {α : Type u} [ToFormat α] (pre : Format) : List α → Format
  | []    => nil
  | a::as => as.foldl (· ++ pre ++ format ·) (pre ++ format a)

/-- Format each item in `items` and append `suffix`. -/
def Format.joinSuffix {α : Type u} [ToFormat α] : List α → Format → Format
  | [],    _      => nil
  | a::as, suffix => as.foldl (· ++ format · ++ suffix) (format a ++ suffix)