From c524bcf2d3d4c5b3fff144a5e2c38c327100c5ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Dec 2020 07:23:07 -0800 Subject: [PATCH] feat: improve universe level pretty printer --- src/Lean/Hygiene.lean | 4 +- src/Lean/Level.lean | 83 ++++++++++++------- src/Lean/Parser/Level.lean | 4 +- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 19 ----- .../PrettyPrinter/Delaborator/Builtins.lean | 4 +- src/Lean/Util/PPExt.lean | 1 + tests/lean/PPRoundtrip.lean | 6 +- tests/lean/PPRoundtrip.lean.expected.out | 2 - .../autoBoundImplicits2.lean.expected.out | 4 +- tests/lean/evalWithMVar.lean.expected.out | 4 +- tests/lean/pplevel.lean | 9 ++ tests/lean/pplevel.lean.expected.out | 6 ++ tests/lean/rewrite.lean.expected.out | 4 +- .../sanitizeMacroScopes.lean.expected.out | 4 +- tests/lean/structAutoBound.lean.expected.out | 4 +- tests/lean/univInference.lean.expected.out | 8 +- 16 files changed, 93 insertions(+), 73 deletions(-) create mode 100644 tests/lean/pplevel.lean create mode 100644 tests/lean/pplevel.lean.expected.out diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean index f419127ad5..e526295cec 100644 --- a/src/Lean/Hygiene.lean +++ b/src/Lean/Hygiene.lean @@ -3,7 +3,9 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ -import Lean.Syntax +import Lean.Data.Name +import Lean.Data.Options +import Lean.Data.Format namespace Lean /- Remark: `MonadQuotation` class is part of the `Init` package and loaded by default since it is used in the builtin command `macro`. -/ diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index d384b7282a..40bfcadef5 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -7,11 +7,12 @@ import Std.Data.HashMap import Std.Data.HashSet import Std.Data.PersistentHashMap import Std.Data.PersistentHashSet +import Lean.Hygiene import Lean.Data.Name import Lean.Data.Format def Nat.imax (n m : Nat) : Nat := -if m = 0 then 0 else Nat.max n m + if m = 0 then 0 else Nat.max n m namespace Lean @@ -356,10 +357,10 @@ def dec : Level → Option Level | imax l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂ -/- Level to Format -/ -namespace LevelToFormat +/- Level to Format/Syntax -/ +namespace PP inductive Result where - | leaf : Format → Result + | leaf : Name → Result | num : Nat → Result | offset : Result → Nat → Result | maxNode : List Result → Result @@ -378,41 +379,63 @@ def Result.imax : Result → Result → Result | f, Result.imaxNode Fs => Result.imaxNode (f::Fs) | f₁, f₂ => Result.imaxNode [f₁, f₂] -def parenIfFalse : Format → Bool → Format - | f, true => f - | f, false => f.paren - -@[specialize] private def formatLst (fmt : Result → Format) : List Result → Format - | [] => Format.nil - | r::rs => Format.line ++ fmt r ++ formatLst fmt rs - -partial def Result.format : Result → Bool → Format - | Result.leaf f, _ => f - | Result.num k, _ => toString k - | Result.offset f 0, r => format f r - | Result.offset f (k+1), r => - let f' := format f false; - parenIfFalse (f' ++ "+" ++ fmt (k+1)) r - | Result.maxNode fs, r => parenIfFalse (Format.group $ "max" ++ formatLst (fun r => format r false) fs) r - | Result.imaxNode fs, r => parenIfFalse (Format.group $ "imax" ++ formatLst (fun r => format r false) fs) r - def toResult : Level → Result | zero _ => Result.num 0 | succ l _ => Result.succ (toResult l) | max l₁ l₂ _ => Result.max (toResult l₁) (toResult l₂) | imax l₁ l₂ _ => Result.imax (toResult l₁) (toResult l₂) - | param n _ => Result.leaf (fmt n) + | param n _ => Result.leaf n | mvar n _ => - let n := n.replacePrefix `_uniq `u; - Result.leaf ("?" ++ fmt n) + let n := n.replacePrefix `_uniq (Name.mkSimple "?u"); + Result.leaf n -end LevelToFormat +private def parenIfFalse : Format → Bool → Format + | f, true => f + | f, false => f.paren -protected def format (l : Level) : Format := - (LevelToFormat.toResult l).format true +mutual + private partial def Result.formatLst : List Result → Format + | [] => Format.nil + | r::rs => Format.line ++ format r false ++ formatLst rs -instance : ToFormat Level := ⟨Level.format⟩ -instance : ToString Level := ⟨Format.pretty ∘ Level.format⟩ + partial def Result.format : Result → Bool → Format + | Result.leaf n, _ => fmt n + | Result.num k, _ => toString k + | Result.offset f 0, r => format f r + | Result.offset f (k+1), r => + let f' := format f false; + parenIfFalse (f' ++ "+" ++ fmt (k+1)) r + | Result.maxNode fs, r => parenIfFalse (Format.group $ "max" ++ formatLst fs) r + | Result.imaxNode fs, r => parenIfFalse (Format.group $ "imax" ++ formatLst fs) r +end + +protected partial def Result.quote (r : Result) (prec : Nat) : Syntax := + let addParen (s : Syntax) := + if prec > 0 then Unhygienic.run `(level| ( $s )) else s + match r with + | Result.leaf n => Unhygienic.run `(level| $(mkIdent n):ident) + | Result.num k => Unhygienic.run `(level| $(quote k):numLit) + | Result.offset r 0 => Result.quote r prec + | Result.offset r (k+1) => addParen <| Unhygienic.run `(level| $(Result.quote r 65) + $(quote (k+1)):numLit) + | Result.maxNode rs => addParen <| Unhygienic.run `(level| max $(rs.toArray.map (Result.quote · maxPrec!))*) + | Result.imaxNode rs => addParen <| Unhygienic.run `(level| imax $(rs.toArray.map (Result.quote · maxPrec!))*) + +end PP + +protected def format (u : Level) : Format := + (PP.toResult u).format true + +instance : ToFormat Level where + format u := Level.format u + +instance : ToString Level where + toString u := Format.pretty (Level.format u) + +protected def quote (u : Level) (prec : Nat := 0) : Syntax := + (PP.toResult u).quote prec + +instance : Quote Level where + quote u := Level.quote u end Level diff --git a/src/Lean/Parser/Level.lean b/src/Lean/Parser/Level.lean index 98a0687fc1..0528d9bf82 100644 --- a/src/Lean/Parser/Level.lean +++ b/src/Lean/Parser/Level.lean @@ -17,8 +17,8 @@ builtin_initialize namespace Level @[builtinLevelParser] def paren := parser! "(" >> levelParser >> ")" -@[builtinLevelParser] def max := parser! nonReservedSymbol "max " true >> many1 (levelParser maxPrec) -@[builtinLevelParser] def imax := parser! nonReservedSymbol "imax " true >> many1 (levelParser maxPrec) +@[builtinLevelParser] def max := parser! nonReservedSymbol "max" true >> many1 (ppSpace >> levelParser maxPrec) +@[builtinLevelParser] def imax := parser! nonReservedSymbol "imax" true >> many1 (ppSpace >> levelParser maxPrec) @[builtinLevelParser] def hole := parser! "_" @[builtinLevelParser] def num := checkPrec maxPrec >> numLit @[builtinLevelParser] def ident := checkPrec maxPrec >> Parser.ident diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index d63b01595e..decdf33574 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -32,25 +32,6 @@ import Lean.Meta.Match import Lean.Elab.Term namespace Lean --- TODO: move, maybe -namespace Level -protected partial def quote : Level → Syntax - | zero _ => Unhygienic.run `(level|0) - | l@(succ _ _) => match l.toNat with - | some n => Unhygienic.run `(level|$(quote n):numLit) - | none => Unhygienic.run `(level|$(Level.quote l.getLevelOffset) + $(quote l.getOffset):numLit) - | max l1 l2 _ => match Level.quote l2 with - | `(level|max $ls*) => Unhygienic.run `(level|max $(Level.quote l1) $ls*) - | l2 => Unhygienic.run `(level|max $(Level.quote l1) $l2) - | imax l1 l2 _ => match Level.quote l2 with - | `(level|imax $ls*) => Unhygienic.run `(level|imax $(Level.quote l1) $ls*) - | l2 => Unhygienic.run `(level|imax $(Level.quote l1) $l2) - | param n _ => Unhygienic.run `(level|$(mkIdent n):ident) - -- HACK: approximation - | mvar n _ => Unhygienic.run `(level|_) - -instance : Quote Level := ⟨Level.quote⟩ -end Level def getPPBinderTypes (o : Options) : Bool := o.get `pp.binder_types true def getPPCoercions (o : Options) : Bool := o.get `pp.coercions true diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 62265e4263..86cc09e092 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -40,8 +40,8 @@ def delabSort : Delab := do | Level.zero _ => `(Prop) | Level.succ (Level.zero _) _ => `(Type) | _ => match l.dec with - | some l' => `(Type $(quote l')) - | none => `(Sort $(quote l)) + | some l' => `(Type $(Level.quote l' maxPrec!)) + | none => `(Sort $(Level.quote l maxPrec!)) -- find shorter names for constants, in reverse to Lean.Elab.ResolveName diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean index a0485942fd..e95fe8b800 100644 --- a/src/Lean/Util/PPExt.lean +++ b/src/Lean/Util/PPExt.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ import Lean.Environment +import Lean.Syntax import Lean.MetavarContext import Lean.Data.OpenDecl diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index fa956ea21e..08741e8928 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -34,9 +34,9 @@ set_option format.width 20 #eval checkM `(Type) #eval checkM `(Type 0) #eval checkM `(Type 1) --- can't add a new universe variable inside a term... -#eval checkM `(Type _) -#eval checkM `(Type (_ + 2)) +-- TODO: we need support for parsing `?u` to roundtrip the terms containing universe metavariables. Just pretty printing them as `_` is bad for error and trace messages +-- #eval checkM `(Type _) +-- #eval checkM `(Type (_ + 2)) #eval checkM `(Nat) #eval checkM `(List Nat) diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out index fb74e5547e..3f05f0aed0 100644 --- a/tests/lean/PPRoundtrip.lean.expected.out +++ b/tests/lean/PPRoundtrip.lean.expected.out @@ -2,8 +2,6 @@ Prop Type Type Type 1 -Type _ -Type (_ + 2) Nat List Nat id Nat diff --git a/tests/lean/autoBoundImplicits2.lean.expected.out b/tests/lean/autoBoundImplicits2.lean.expected.out index b22837e74a..3b85382896 100644 --- a/tests/lean/autoBoundImplicits2.lean.expected.out +++ b/tests/lean/autoBoundImplicits2.lean.expected.out @@ -3,10 +3,10 @@ g1 : ?m → ?m autoBoundImplicits2.lean:30:17: error: unknown universe level 'u' autoBoundImplicits2.lean:30:37: error: type expected failed to synthesize instance - CoeSort (sorryAx (Sort _)) ?m + CoeSort (sorryAx (Sort ?u)) ?m autoBoundImplicits2.lean:33:17: error: unknown universe level 'β' autoBoundImplicits2.lean:33:90: error: type expected failed to synthesize instance - CoeSort (sorryAx (Sort _)) ?m + CoeSort (sorryAx (Sort ?u)) ?m def h1.{u} : {m : Type u → Type u} → {α : Type u} → m α → m α := fun {m : Type u → Type u} {α : Type u} (a : m α) => a diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out index 6f6693eabb..3c0639418e 100644 --- a/tests/lean/evalWithMVar.lean.expected.out +++ b/tests/lean/evalWithMVar.lean.expected.out @@ -2,10 +2,10 @@ Sum.someRight c : Option Nat evalWithMVar.lean:13:6: error: don't know how to synthesize implicit argument @Sum.someRight ?m Nat c context: -⊢ Type _ +⊢ Type ?u evalWithMVar.lean:13:20: error: don't know how to synthesize implicit argument @c ?m context: -⊢ Type _ +⊢ Type ?u Sum.someRight c : Option Nat Sum.someRight c : Option Nat diff --git a/tests/lean/pplevel.lean b/tests/lean/pplevel.lean new file mode 100644 index 0000000000..a8d165927d --- /dev/null +++ b/tests/lean/pplevel.lean @@ -0,0 +1,9 @@ +universes u v w + +set_option pp.universes true +#check Type (max u v w) +#check Type u +#check @id.{max u v w} +#check Monad.{max u v, w+1} +#check Type (max (u+1) w (v+2)) +#check Type _ diff --git a/tests/lean/pplevel.lean.expected.out b/tests/lean/pplevel.lean.expected.out new file mode 100644 index 0000000000..cc9abba3ea --- /dev/null +++ b/tests/lean/pplevel.lean.expected.out @@ -0,0 +1,6 @@ +Type (max u v w) : Type ((max u v w) + 1) +Type u : Type (u + 1) +id.{max u v w} : {α : Sort (max u v w)} → α → α +Monad.{max u v, w + 1} : (Type (max u v) → Type (w + 1)) → Type (max (w + 1) ((max u v) + 1)) +Type (max (u + 1) w (v + 2)) : Type ((max (u + 1) w (v + 2)) + 1) +Type u_1 : Type (u_1 + 1) diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out index a8d53ef3a2..a66a463908 100644 --- a/tests/lean/rewrite.lean.expected.out +++ b/tests/lean/rewrite.lean.expected.out @@ -1,9 +1,9 @@ -α : Type _ +α : Type ?u as bs : List α ⊢ as ++ bs ++ bs = as ++ (bs ++ bs) rewrite.lean:12:20: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression List.reverse (List.reverse ?m) -α : Type _ +α : Type ?u as bs : List α ⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs) x y z : Nat diff --git a/tests/lean/sanitizeMacroScopes.lean.expected.out b/tests/lean/sanitizeMacroScopes.lean.expected.out index 0ccf9f7d84..a4a5799bc8 100644 --- a/tests/lean/sanitizeMacroScopes.lean.expected.out +++ b/tests/lean/sanitizeMacroScopes.lean.expected.out @@ -1,13 +1,13 @@ fun (x : ?m) (x_1 : ?m x) => x : (x : ?m) → ?m x → ?m [Elab.step] expected type: , term fun x => m x -[Elab.step] expected type: Sort _, term +[Elab.step] expected type: Sort ?u, term _ [Elab.step] expected type: , term m x [Elab.step] expected type: , term fun x✝ => x - [Elab.step] expected type: Sort _, term + [Elab.step] expected type: Sort ?u, term _ [Elab.step] expected type: , term x diff --git a/tests/lean/structAutoBound.lean.expected.out b/tests/lean/structAutoBound.lean.expected.out index 41413518b7..e3e148a212 100644 --- a/tests/lean/structAutoBound.lean.expected.out +++ b/tests/lean/structAutoBound.lean.expected.out @@ -1,8 +1,8 @@ -inductive Foo.{v, u_1} : {α : Sort u_1} → (α → Type v) → Sort max u_1(v + 1) +inductive Foo.{v, u_1} : {α : Sort u_1} → (α → Type v) → Sort (max u_1 (v + 1)) constructors: Foo.mk : {α : Sort u_1} → {β : α → Type v} → (a : α) → β a → Foo β structAutoBound.lean:9:15: error: a universe level named 'u' has already been declared -inductive Boo.{u, v} : Type u → Type v → Type max u v +inductive Boo.{u, v} : Type u → Type v → Type (max u v) constructors: Boo.mk : {α : Type u} → {β : Type v} → α → β → Boo α β structAutoBound.lean:18:0: error: unused universe parameter 'w' diff --git a/tests/lean/univInference.lean.expected.out b/tests/lean/univInference.lean.expected.out index 5a8da652c1..18162bc9dc 100644 --- a/tests/lean/univInference.lean.expected.out +++ b/tests/lean/univInference.lean.expected.out @@ -1,9 +1,9 @@ univInference.lean:26:0: error: failed to compute resulting universe level of inductive datatype, provide universe explicitly -S6 : Sort max w₂ w₁ → Type w₂ → Sort max w₁(w₂ + 1) +S6 : Sort (max w₁ w₂) → Type w₂ → Sort (max w₁ (w₂ + 1)) univInference.lean:46:0: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u' - max v u + max u v univInference.lean:65:0: error: failed to compute resulting universe level of inductive datatype, provide universe explicitly univInference.lean:74:0: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u' - max v u + max u v univInference.lean:82:0: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u' - max v u + max u v