max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: improve universe level pretty printer

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-21 07:23:07 -08:00
parent 83ae3b7aaa
commit c524bcf2d3
16 changed files with 93 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Hygiene.lean
View file

@ -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`. -/

83
src/Lean/Level.lean
View file

@ -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

4
src/Lean/Parser/Level.lean
View file

@ -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

19
src/Lean/PrettyPrinter/Delaborator/Basic.lean
View file

@ -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

4
src/Lean/PrettyPrinter/Delaborator/Builtins.lean
View file

@ -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

1
src/Lean/Util/PPExt.lean
View file

@ -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

6
tests/lean/PPRoundtrip.lean
View file

@ -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)

2
tests/lean/PPRoundtrip.lean.expected.out
View file

@ -2,8 +2,6 @@ Prop
Type
Type
Type 1
Type _
Type (_ + 2)
Nat
List Nat
id Nat

4
tests/lean/autoBoundImplicits2.lean.expected.out
View file

@ -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

4
tests/lean/evalWithMVar.lean.expected.out
View file

@ -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

9
tests/lean/pplevel.lean Normal file
View file

@ -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 _

6
tests/lean/pplevel.lean.expected.out Normal file
View file

@ -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)

4
tests/lean/rewrite.lean.expected.out
View file

@ -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

4
tests/lean/sanitizeMacroScopes.lean.expected.out
View file

@ -1,13 +1,13 @@
fun (x : ?m) (x_1 : ?m x) => x : (x : ?m) → ?m x → ?m
[Elab.step] expected type: <not-available>, term
fun x => m x
[Elab.step] expected type: Sort _, term
[Elab.step] expected type: Sort ?u, term
_
[Elab.step] expected type: <not-available>, term
m x
[Elab.step] expected type: <not-available>, term
fun x✝ => x
[Elab.step] expected type: Sort _, term
[Elab.step] expected type: Sort ?u, term
_
[Elab.step] expected type: <not-available>, term
x

4
tests/lean/structAutoBound.lean.expected.out
View file

@ -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'

8
tests/lean/univInference.lean.expected.out
View file

@ -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