diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean index 2231c439a7..a76c9bf235 100644 --- a/src/Init/Control/EState.lean +++ b/src/Init/Control/EState.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura prelude import Init.Control.State import Init.Control.Except +import Init.Data.ToString.Basic universes u v namespace EStateM diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 39da8e96a6..53dba7e209 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -6,27 +6,11 @@ Authors: Jared Roesch, Sebastian Ullrich The Except monad transformer. -/ prelude -import Init.Data.ToString.Basic import Init.Control.Basic import Init.Control.Id universes u v w u' -section -variables {ε : Type u} {α : Type v} - -protected def Except.toString [ToString ε] [ToString α] : Except ε α → String - | Except.error e => "(error " ++ toString e ++ ")" - | Except.ok a => "(ok " ++ toString a ++ ")" - -protected def Except.repr [Repr ε] [Repr α] : Except ε α → String - | Except.error e => "(error " ++ repr e ++ ")" - | Except.ok a => "(ok " ++ repr a ++ ")" - -instance [ToString ε] [ToString α] : ToString (Except ε α) := ⟨Except.toString⟩ -instance [Repr ε] [Repr α] : Repr (Except ε α) := ⟨Except.repr⟩ -end - namespace Except variables {ε : Type u} @@ -135,7 +119,7 @@ variables {ε : Type u} {m : Type v → Type w} /-- Alternative orelse operator that allows to select which exception should be used. The default is to use the first exception since the standard `orelse` uses the second. -/ @[inline] def orelse' [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx := true) : m α := - tryCatch t₁ fun e₁ => tryCatch t₂ fun e₂ => throw (if useFirstEx then e₁ else e₂) + tryCatch t₁ fun e₁ => tryCatch t₂ fun e₂ => throw (if useFirstEx = true then e₁ else e₂) end MonadExcept diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean index 091b302a39..38a58762fe 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude +import Init.Data.Option.Basic import Init.Control.Basic import Init.Control.Except diff --git a/src/Init/Data/Format.lean b/src/Init/Data/Format.lean index 62c508a09d..7f56a4d18a 100644 --- a/src/Init/Data/Format.lean +++ b/src/Init/Data/Format.lean @@ -4,269 +4,6 @@ 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 +import Init.Data.Format.Basic +import Init.Data.Format.Macro +import Init.Data.Format.Instances diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean index 7722d0de09..daaefb883c 100644 --- a/src/Init/Data/ToString/Basic.lean +++ b/src/Init/Data/ToString/Basic.lean @@ -9,10 +9,11 @@ import Init.Data.UInt import Init.Data.Nat.Div import Init.Data.Repr import Init.Data.Int.Basic +import Init.Data.Format.Basic import Init.Control.Id open Sum Subtype Nat -universes u v +open Std class ToString (α : Type u) where toString : α → String @@ -94,6 +95,9 @@ instance : ToString UInt64 := instance : ToString USize := ⟨fun n => toString n.toNat⟩ +instance : ToString Format where + toString f := f.pretty + def addParenHeuristic (s : String) : String := if "(".isPrefixOf s || "[".isPrefixOf s || "{".isPrefixOf s || "#[".isPrefixOf s then s else if !s.any Char.isWhitespace then s @@ -133,3 +137,18 @@ def String.toInt! (s : String) : Int := match s.toInt? with | some v => v | none => panic "Int expected" + +section +variables {ε : Type u} {α : Type v} + +protected def Except.toString [ToString ε] [ToString α] : Except ε α → String + | Except.error e => "(error " ++ toString e ++ ")" + | Except.ok a => "(ok " ++ toString a ++ ")" + +protected def Except.repr [Repr ε] [Repr α] : Except ε α → String + | Except.error e => "(error " ++ repr e ++ ")" + | Except.ok a => "(ok " ++ repr a ++ ")" + +instance [ToString ε] [ToString α] : ToString (Except ε α) := ⟨Except.toString⟩ +instance [Repr ε] [Repr α] : Repr (Except ε α) := ⟨Except.repr⟩ +end