unison/pretty.u

unique[ecf75311027ef922e3e50d358b1d7bc93c84035e] type Width
    -- | The number of columns.
  = SingleLine Nat 
    -- | The number of columns in the first, last, and longest lines.
  | MultiLine Nat Nat Nat

Width.empty = SingleLine 0
Width.append = cases
  SingleLine c, SingleLine c2 -> SingleLine (c + c2)
  SingleLine c, MultiLine fc lc mc -> 
    fc' = c + fc
    MultiLine fc' lc (max fc' mc)
  MultiLine fc lc mc, SingleLine c ->
    lc' = lc + c
    MultiLine fc lc' (max lc' mc)
  MultiLine fc lc mc, MultiLine fc2 lc2 mc2 ->
    MultiLine fc lc2 (max mc (max mc2 (lc + fc2)))

Width.maxColumn : Width -> Nat
Width.maxColumn = cases
  SingleLine c -> c
  MultiLine _ _ c -> c

Width.toNat : Width -> Nat
Width.toNat = cases
  SingleLine c -> c
  MultiLine _ c _ -> c

Width.fromChar : Char -> Width
Width.fromChar = cases
  ?\n -> MultiLine 0 0 0
  _ -> SingleLine 1

Width.snocChar : Width -> Char -> Width
Width.snocChar w ch = match ch with
  ?\n -> append w (fromChar ch) 
  _ -> match w with 
    SingleLine c -> SingleLine (c + 1)
    MultiLine fc lc mc ->
      lc' = lc + 1
      MultiLine fc lc' (max lc' mc)

Width.fromText : Text -> Width
Width.fromText txt = 
  foldLeft snocChar empty (Text.toCharList txt) 

-- Surgically modify the given width to pretend it has not exceeded availableWidth.
Width.forceFit : Nat -> Width -> Width
Width.forceFit availableWidth = cases
  SingleLine c -> SingleLine (min c (drop availableWidth 1))
  MultiLine fc lc mc -> MultiLine fc lc (min mc (drop availableWidth 1))

Width.fits : Nat -> Width -> Width -> Boolean
Width.fits availableWidth w1 w2 = 
  toNat (append w1 w2) <= availableWidth

Width.forceFits : Nat -> Width -> Width -> Boolean
Width.forceFits availableWidth w1 w2 = 
  toNat (append (forceFit availableWidth w1) w2) <= availableWidth

unique[d7b2ced8c08b2c6e54050d1f5acedef3395f293d] type Pretty.Annotated w txt
  = Empty
    -- | A group adds a level of breaking. Layout tries not to break a group
    -- unless needed to fit in available width. Breaking is done "outside in".
    --
    --   (a | b) <> (c | d) will try (a <> c), then (b <> d)
    --
    --   (a | b) <> group (c | d) will try (a <> c), then (b <> c), then (b <> d)
  | Group w (Pretty.Annotated w txt)
  | Lit w txt
  | Wrap w [Pretty.Annotated w txt]
  | OrElse w (Pretty.Annotated w txt) (Pretty.Annotated w txt)
  | Append w [Pretty.Annotated w txt]

type Pretty txt = Pretty (Pretty.Annotated () txt)

Pretty.get = cases Pretty p -> p

Pretty.annotate : (txt -> Width) -> Pretty txt -> Pretty.Annotated Width txt 
Pretty.annotate w p =
  go = cases
    Empty -> Empty
    Group _ p -> 
      p' = go p
      Group (preferredWidth p') p'
    Lit _ txt -> Lit (w txt) txt
    Wrap _ ps -> 
      ps' = List.map go ps
      preferred = foldLeft (acc p -> append acc (preferredWidth p)) empty ps'
      Wrap preferred ps' 
    OrElse _ p1 p2 -> 
      p1' = go p1
      p2' = go p2
      OrElse (append (preferredWidth p1') (preferredWidth p2')) p1' p2'
    Append _ ps ->
      ps' = List.map go ps
      preferred = foldLeft (acc p -> append acc (preferredWidth p)) empty ps'
      Append preferred ps' 

  go (Pretty.get p)

Pretty.preferredWidth : Pretty.Annotated Width s -> Width
Pretty.preferredWidth = cases
  Empty -> Width.empty
  Group w _ -> w
  Lit w _ -> w
  Wrap w _ -> w
  OrElse w _ _ -> w
  Append w _ -> w

List.for! : [a] -> (a ->{g} ()) ->{g} ()
List.for! as f = match as with 
  [] -> ()
  a +: as -> f a
             for! as f

Pretty.layout : (txt -> Width) -> Nat -> Pretty txt ->{Stream txt} ()
Pretty.layout width available p = layout' available (annotate width p)

Pretty.layout' : Nat -> Pretty.Annotated Width txt ->{Stream txt} ()
Pretty.layout' availableWidth p =
  -- `go currentWidth rem`, where `currentWidth` is the width of
  -- elements to the left of the current position, and the list is
  -- elements we need to append. Elements wrapped in Left in this 
  -- list are scheduled to be "broken"; elements wrapped in Right
  -- we will attempt to fit inline, and break only if necessary.
  go : Width 
    -> [Either (Pretty.Annotated Width txt) (Pretty.Annotated Width txt)] 
    -> {Stream txt} ()
  go = cases
    _, [] -> ()
    cur, p +: rest -> match p with
      Right p -> -- `p` might fit, let's try it!
        if forceFits availableWidth cur (preferredWidth p) then 
          flow p
          go (append cur (preferredWidth p)) rest
        else 
          go cur (Left p +: rest) -- nope, switch to breaking mode
      Left p -> match p with -- `p` requires breaking
        Empty -> go cur rest
        Append _ ps -> go cur (List.map Left ps ++ rest)
        Group _ p -> go cur (Right p +: rest)
        -- Note: literals can't be broken further so they're
        -- added to output unconditionally
        Lit preferred l -> emit l; go (append cur preferred) rest
        OrElse _ _ p -> go cur (Right p +: rest)
        Wrap _ ps -> go cur (List.map Right ps ++ rest)

  flow p = match p with
    Append _ ps -> for! ps flow
    Empty -> ()
    Group _ p -> flow p
    Lit _ s -> emit s
    OrElse _ p _ -> flow p
    Wrap _ ps -> for! ps flow

  go Width.empty [Right p]