From b555307f0699c92affb7ab77f6edabd05e65ec5c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Oct 2020 16:29:32 -0700 Subject: [PATCH] chore: move to new frontend --- src/Lean/Data/Format.lean | 330 +++++++++++++------------- src/Lean/PrettyPrinter/Backtrack.lean | 4 +- tests/lean/Format.lean | 1 + 3 files changed, 164 insertions(+), 171 deletions(-) diff --git a/src/Lean/Data/Format.lean b/src/Lean/Data/Format.lean index 43c9ab9d6a..8af700b40f 100644 --- a/src/Lean/Data/Format.lean +++ b/src/Lean/Data/Format.lean @@ -1,3 +1,4 @@ +#lang lean4 /- Copyright (c) 2018 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -7,42 +8,43 @@ import Lean.Data.Options universes u v namespace Lean - namespace Format + inductive FlattenBehavior -| allOrNone -| fill + | allOrNone + | fill namespace FlattenBehavior -instance hasBeq : HasBeq FlattenBehavior := -⟨fun b₁ b₂ => match b₁, b₂ with +instance : HasBeq FlattenBehavior := ⟨fun b₁ b₂ => + match b₁, b₂ with | allOrNone, allOrNone => true | fill, fill => true | _, _ => false⟩ end FlattenBehavior + end Format open Format inductive Format -| nil : Format -| line : Format -| text : String → Format -| nest (indent : Int) : Format → Format -| append : Format → Format → Format -| group : Format → optParam FlattenBehavior FlattenBehavior.allOrNone → Format + | nil : Format + | line : Format + | text : String → Format + | nest (indent : Int) : Format → Format + | append : Format → Format → Format + | group : Format → (behavior : FlattenBehavior := FlattenBehavior.allOrNone) → Format namespace Format def fill (f : Format) : Format := -group f FlattenBehavior.fill + group f (behavior := FlattenBehavior.fill) @[export lean_format_append] protected def appendEx (a b : Format) : Format := -append a b + append a b @[export lean_format_group] protected def groupEx : Format → Format := -group + group instance : HasAppend Format := ⟨Format.append⟩ instance : HasCoe String Format := ⟨text⟩ @@ -50,131 +52,130 @@ instance : Coe String Format := ⟨text⟩ instance : Inhabited Format := ⟨nil⟩ def join (xs : List Format) : Format := -xs.foldl HasAppend.append "" + xs.foldl HasAppend.append "" def isNil : Format → Bool -| nil => true -| _ => false + | nil => true + | _ => false private structure SpaceResult := -(foundLine := false) -(foundFlattenedHardLine := false) -(space := 0) + (foundLine : Bool := false) + (foundFlattenedHardLine : Bool := false) + (space : Nat := 0) -instance SpaceResult.inhabited : Inhabited SpaceResult := -⟨{}⟩ +instance SpaceResult.inhabited : Inhabited SpaceResult := ⟨{}⟩ @[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 } + 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 + | 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 := -(f : Format) -(indent : Int) + (f : Format) + (indent : Int) private structure WorkGroup := -(flatten : Bool) -(flb : FlattenBehavior) -(items : List WorkItem) + (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)) + | [], 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 := -(out : String := "") -(column : Nat := 0) + (out : String := "") + (column : Nat := 0) private def pushGroup (flb : FlattenBehavior) (items : List WorkItem) (gs : List WorkGroup) (w : Nat) : StateM State (List WorkGroup) := do -k ← State.column <$> get; --- 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 : WorkGroup := { flatten := flb == FlattenBehavior.allOrNone, flb := flb, items := items }; -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) -pure $ { g with flatten := !r.foundFlattenedHardLine && r'.space <= w-k }::gs + 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 } + 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 } + 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 gs -| g@{ items := i::is, .. }::gs => - let gs' (is' : List WorkItem) := { g with items := is' }::gs; - match i.f with - | nil => be (gs' is) - | append f₁ f₂ => be (gs' ({ i with f := f₁ }::{ i with f := f₂ }::is)) - | nest n f => be (gs' ({ i with f := f, indent := i.indent + n }::is)) - | text s => - let p := s.posOf '\n'; - if p == s.bsize then do - pushOutput s; - be (gs' is) - else do - 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 - | line => do - match g.flb with - | FlattenBehavior.allOrNone => - if g.flatten then do - -- flatten line = text " " - pushOutput " "; - be (gs' is) - else do - pushNewline i.indent.toNat; - be (gs' is) - | FlattenBehavior.fill => do - let breakHere := do { - pushNewline i.indent.toNat; - -- make new `fill` group and recurse - pushGroup FlattenBehavior.fill is gs w >>= be - }; - -- if preceding fill item fit in a single line, try to fit next one too - if g.flatten then do - gs'@(g'::_) ← pushGroup FlattenBehavior.fill is gs (w - " ".length) - | unreachable!; - if g'.flatten then do - pushOutput " "; - be gs' -- TODO: use `return` + | [] => 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 - breakHere - | group f flb => if g.flatten then - -- flatten (group f) = flatten f - be (gs' ({ i with f := f }::is)) - else - pushGroup flb [{ i with f := f }] (gs' is) w >>= be + 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) + group (nest l.length $ l ++ f ++ r) @[inline] def paren (f : Format) : Format := -bracket "(" f ")" + bracket "(" f ")" @[inline] def sbracket (f : Format) : Format := -bracket "[" f "]" + bracket "[" f "]" def defIndent := 2 def defUnicode := true @@ -184,119 +185,110 @@ def getWidth (o : Options) : Nat := o.get `format.width defWidth def getIndent (o : Options) : Nat := o.get `format.indent defIndent def getUnicode (o : Options) : Bool := o.get `format.unicode defUnicode -@[builtinInit] def indentOption : IO Unit := -registerOption `format.indent { defValue := defIndent, group := "format", descr := "indentation" } -@[builtinInit] def unicodeOption : IO Unit := -registerOption `format.unicode { defValue := defUnicode, group := "format", descr := "unicode characters" } -@[builtinInit] def widthOption : IO Unit := -registerOption `format.width { defValue := defWidth, group := "format", descr := "line width" } +builtin_initialize + registerOption `format.indent { defValue := defIndent, group := "format", descr := "indentation" } + 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 + let (_, st) := be w [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent := 0 }] }] {}; + st.out def pretty (f : Format) (o : Options := {}) : String := -prettyAux f (getWidth o) + prettyAux f (getWidth o) end Format open Lean.Format class HasFormat (α : Type u) := -(format : α → Format) + (format : α → Format) export Lean.HasFormat (format) -def fmt {α : Type u} [HasFormat α] : α → Format := -format +def fmt {α : Type u} [HasFormat α] : α → Format := format -instance toStringToFormat {α : Type u} [HasToString α] : HasFormat α := -⟨text ∘ toString⟩ +instance {α : Type u} [HasToString α] : HasFormat α := ⟨text ∘ toString⟩ -- note: must take precendence over the above instance to avoid premature formatting -instance formatHasFormat : HasFormat Format := -⟨id⟩ - -instance stringHasFormat : HasFormat String := ⟨Format.text⟩ +instance : HasFormat Format := ⟨id⟩ +instance : HasFormat String := ⟨Format.text⟩ def Format.joinSep {α : Type u} [HasFormat α] : List α → Format → Format -| [], sep => nil -| [a], sep => format a -| a::as, sep => format a ++ sep ++ Format.joinSep as sep + | [], sep => nil + | [a], sep => format a + | a::as, sep => format a ++ sep ++ joinSep as sep def Format.prefixJoin {α : Type u} [HasFormat α] (pre : Format) : List α → Format -| [] => nil -| a::as => pre ++ format a ++ Format.prefixJoin as + | [] => nil + | a::as => pre ++ format a ++ prefixJoin pre as def Format.joinSuffix {α : Type u} [HasFormat α] : List α → Format → Format -| [], suffix => nil -| a::as, suffix => format a ++ suffix ++ Format.joinSuffix as suffix + | [], suffix => nil + | a::as, suffix => format a ++ suffix ++ joinSuffix as suffix def List.format {α : Type u} [HasFormat α] : List α → Format -| [] => "[]" -| xs => sbracket $ Format.joinSep xs ("," ++ line) + | [] => "[]" + | xs => sbracket $ Format.joinSep xs ("," ++ line) -instance listHasFormat {α : Type u} [HasFormat α] : HasFormat (List α) := -⟨List.format⟩ +instance {α : Type u} [HasFormat α] : HasFormat (List α) := ⟨List.format⟩ -instance arrayHasFormat {α : Type u} [HasFormat α] : HasFormat (Array α) := -⟨fun a => "#" ++ fmt a.toList⟩ +instance {α : Type u} [HasFormat α] : HasFormat (Array α) := ⟨fun a => "#" ++ fmt a.toList⟩ def Option.format {α : Type u} [HasFormat α] : Option α → Format -| none => "none" -| some a => "some " ++ fmt a + | none => "none" + | some a => "some " ++ fmt a -instance optionHasFormat {α : Type u} [HasFormat α] : HasFormat (Option α) := -⟨Option.format⟩ +instance {α : Type u} [HasFormat α] : HasFormat (Option α) := ⟨Option.format⟩ -instance prodHasFormat {α : Type u} {β : Type v} [HasFormat α] [HasFormat β] : HasFormat (Prod α β) := -⟨fun ⟨a, b⟩ => paren $ format a ++ "," ++ line ++ format b⟩ +instance {α : Type u} {β : Type v} [HasFormat α] [HasFormat β] : HasFormat (Prod α β) := ⟨fun ⟨a, b⟩ => + paren $ format a ++ "," ++ line ++ format b +⟩ def Format.joinArraySep {α : Type u} [HasFormat α] (a : Array α) (sep : Format) : Format := -a.iterate nil (fun i a r => if i.val > 0 then r ++ sep ++ format a else r ++ format a) + a.iterate nil (fun i a r => if i.val > 0 then r ++ sep ++ format a else r ++ format a) -instance natHasFormat : HasFormat Nat := ⟨fun n => toString n⟩ -instance uint16HasFormat : HasFormat UInt16 := ⟨fun n => toString n⟩ -instance uint32HasFormat : HasFormat UInt32 := ⟨fun n => toString n⟩ -instance uint64HasFormat : HasFormat UInt64 := ⟨fun n => toString n⟩ -instance usizeHasFormat : HasFormat USize := ⟨fun n => toString n⟩ -instance nameHasFormat : HasFormat Name := ⟨fun n => n.toString⟩ +instance : HasFormat Nat := ⟨fun n => toString n⟩ +instance : HasFormat UInt16 := ⟨fun n => toString n⟩ +instance : HasFormat UInt32 := ⟨fun n => toString n⟩ +instance : HasFormat UInt64 := ⟨fun n => toString n⟩ +instance : HasFormat USize := ⟨fun n => toString n⟩ +instance : HasFormat Name := ⟨fun n => n.toString⟩ protected def Format.repr : Format → Format -| nil => "Format.nil" -| line => "Format.line" -| text s => paren $ "Format.text" ++ line ++ repr s -| nest n f => paren $ "Format.nest" ++ line ++ repr n ++ line ++ Format.repr f -| append f₁ f₂ => paren $ "Format.append " ++ line ++ Format.repr f₁ ++ line ++ Format.repr f₂ -| group f FlattenBehavior.allOrNone => paren $ "Format.group" ++ line ++ Format.repr f -| group f FlattenBehavior.fill => paren $ "Format.fill" ++ line ++ Format.repr f + | nil => "Format.nil" + | line => "Format.line" + | text s => paren $ "Format.text" ++ line ++ repr s + | nest n f => paren $ "Format.nest" ++ line ++ repr n ++ line ++ Format.repr f + | append f₁ f₂ => paren $ "Format.append " ++ line ++ Format.repr f₁ ++ line ++ Format.repr f₂ + | group f FlattenBehavior.allOrNone => paren $ "Format.group" ++ line ++ Format.repr f + | group f FlattenBehavior.fill => paren $ "Format.fill" ++ line ++ Format.repr f - -instance formatHasToString : HasToString Format := ⟨Format.pretty⟩ +instance : HasToString Format := ⟨Format.pretty⟩ instance : HasRepr Format := ⟨Format.pretty ∘ Format.repr⟩ 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 + | 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 dataValueHasFormat : HasFormat DataValue := ⟨formatDataValue⟩ +instance : HasFormat DataValue := ⟨formatDataValue⟩ def formatEntry : Name × DataValue → Format -| (n, v) => format n ++ " := " ++ format v + | (n, v) => format n ++ " := " ++ format v -instance entryHasFormat : HasFormat (Name × DataValue) := ⟨formatEntry⟩ +instance : HasFormat (Name × DataValue) := ⟨formatEntry⟩ def formatKVMap (m : KVMap) : Format := -sbracket (Format.joinSep m.entries ", ") + sbracket (Format.joinSep m.entries ", ") -instance kvMapHasFormat : HasFormat KVMap := ⟨formatKVMap⟩ +instance : HasFormat KVMap := ⟨formatKVMap⟩ end Lean def String.toFormat (s : String) : Lean.Format := -Lean.Format.joinSep (s.splitOn "\n") Lean.Format.line + Lean.Format.joinSep (s.splitOn "\n") Lean.Format.line diff --git a/src/Lean/PrettyPrinter/Backtrack.lean b/src/Lean/PrettyPrinter/Backtrack.lean index 42c2cc7366..2c58f1591f 100644 --- a/src/Lean/PrettyPrinter/Backtrack.lean +++ b/src/Lean/PrettyPrinter/Backtrack.lean @@ -1,3 +1,4 @@ +#lang lean4 /- Copyright (c) 2020 Sebastian Ullrich. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -10,8 +11,7 @@ namespace PrettyPrinter /- Auxiliary internal exception for backtracking the pretty printer. See `orelse.parenthesizer` for example -/ -def registerBacktrackId : IO InternalExceptionId := registerInternalExceptionId `backtrackFormatter -@[builtinInit registerBacktrackId] constant backtrackExceptionId : InternalExceptionId := arbitrary _ +builtin_initialize backtrackExceptionId : InternalExceptionId ← registerInternalExceptionId `backtrackFormatter end PrettyPrinter end Lean diff --git a/tests/lean/Format.lean b/tests/lean/Format.lean index 79ab9d35c2..e3367b06a2 100644 --- a/tests/lean/Format.lean +++ b/tests/lean/Format.lean @@ -1,3 +1,4 @@ +#lang lean4 import Lean.Data.Format open Lean open Lean.Format