From 4772fb58497767fdf10db7e67c30de076d575c2f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 2 Feb 2021 13:38:47 +0100 Subject: [PATCH] =?UTF-8?q?feat:=20delaborator:=20use=20`=E2=88=80`=20if?= =?UTF-8?q?=20prop?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Lean/Parser/Term.lean | 5 ++-- .../PrettyPrinter/Delaborator/Builtins.lean | 24 +++++++++++++------ tests/lean/223.lean.expected.out | 2 +- tests/lean/PPRoundtrip.lean | 5 +++- tests/lean/PPRoundtrip.lean.expected.out | 8 +++++-- tests/lean/Reformat.lean.expected.out | 4 ++-- tests/lean/precissues.lean.expected.out | 2 +- tests/lean/sizeof.lean.expected.out | 4 ++-- 8 files changed, 36 insertions(+), 18 deletions(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 8bc5891eff..67a4534de0 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -97,7 +97,8 @@ def binderDefault := parser! " := " >> termParser def explicitBinder (requireType := false) := ppGroup $ parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")" def implicitBinder (requireType := false) := ppGroup $ parser! "{" >> many1 binderIdent >> binderType requireType >> "}" def instBinder := ppGroup $ parser! "[" >> optIdent >> termParser >> "]" -def bracketedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder +def bracketedBinder (requireType := false) := withAntiquot (mkAntiquot "bracketedBinder" none (anonymous := false)) <| + explicitBinder requireType <|> implicitBinder requireType <|> instBinder /- It is feasible to support dependent arrows such as `{α} → α → α` without sacrificing the quality of the error messages for the longer case. @@ -118,7 +119,7 @@ Note that we did not add a `explicitShortBinder` parser since `(α) → α → def simpleBinder := parser! many1 binderIdent >> optType @[builtinTermParser] -def «forall» := parser!:leadPrec unicodeSymbol "∀ " "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser +def «forall» := parser!:leadPrec unicodeSymbol "∀" "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser def matchAlt (rhsParser : Parser := termParser) : Parser := nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $ diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index d2da63054b..0f032a2dd6 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -108,7 +108,7 @@ def delabAppExplicit : Delab := do let fn ← getExpr let stx ← if fn.isConst then delabConst else delab let paramKinds ← liftM <| getParamKinds fn <|> pure #[] - let stx ← if paramKinds.any (fun k => match k with | ParamKind.explicit => false | _ => true) = true then `(@$stx) else pure stx + let stx ← if paramKinds.any (fun | ParamKind.explicit => false | _ => true) = true then `(@$stx) else pure stx pure (stx, #[])) (fun ⟨fnStx, argStxs⟩ => do let argStx ← delab @@ -350,21 +350,31 @@ def delabLam : Delab := def delabForall : Delab := delabBinders fun curNames stxBody => do let e ← getExpr + let prop ← try isProp e catch _ => false let stxT ← withBindingDomain delab - match e.binderInfo with + let group ← match e.binderInfo with | BinderInfo.default => -- heuristic: use non-dependent arrows only if possible for whole group to avoid -- noisy mix like `(α : Type) → Type → (γ : Type) → ...`. let dependent := curNames.any $ fun n => hasIdent n.getId stxBody -- NOTE: non-dependent arrows are available only for the default binder info - if dependent then do - `(($curNames* : $stxT) → $stxBody) + if dependent then + if prop && !(← getPPOption getPPBinderTypes) then + return ← `(∀ $curNames:ident*, $stxBody) + else + `(bracketedBinderF|($curNames* : $stxT)) else - curNames.foldrM (fun _ stxBody => `($stxT → $stxBody)) stxBody - | BinderInfo.implicit => `({$curNames* : $stxT} → $stxBody) + return ← curNames.foldrM (fun _ stxBody => `($stxT → $stxBody)) stxBody + | BinderInfo.implicit => `(bracketedBinderF|{$curNames* : $stxT}) -- here `curNames.size == 1` - | BinderInfo.instImplicit => `([$curNames.back : $stxT] → $stxBody) + | BinderInfo.instImplicit => `(bracketedBinderF|[$curNames.back : $stxT]) | _ => unreachable! + if prop then + match stxBody with + | `(∀ $groups*, $stxBody) => `(∀ $group $groups*, $stxBody) + | _ => `(∀ $group, $stxBody) + else + `($group:bracketedBinder → $stxBody) @[builtinDelab letE] def delabLetE : Delab := do diff --git a/tests/lean/223.lean.expected.out b/tests/lean/223.lean.expected.out index ce437bf1c9..9ba1868a58 100644 --- a/tests/lean/223.lean.expected.out +++ b/tests/lean/223.lean.expected.out @@ -2,7 +2,7 @@ def h.{u_1, u_2} : {α : Type u_1} → {β : Type u_2} → {f : α → β} → { fun {α : Type u_1} {β : Type u_2} {f : α → β} (x : β) (x_1 : Imf f x) => match x, x_1 with | .(f a), Imf.mk a => a -theorem ex.{u} : {α β : Sort u} → (h : α = β) → (a : α) → cast h a ≅ a := +theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a := fun (x x_1 : Sort u) (x_2 : x = x_1) (x_3 : x) => match x, x_1, x_2, x_3 with | α, .(α), Eq.refl α, a => HEq.refl a diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index 08741e8928..94ad4fefb7 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -73,9 +73,12 @@ end #eval checkM `((α β : Type) → α) -- group #eval checkM `((α β : Type) → Type) -- don't group #eval checkM `((α : Type) → (a : α) → α) -#eval checkM `((α : Type) → (a : α) → a = a) #eval checkM `({α : Type} → α) #eval checkM `({α : Type} → [ToString α] → α) +#eval checkM `(∀ x : Nat, x = x) +#eval checkM `(∀ {x : Nat} [ToString Nat], x = x) +set_option pp.binder_types false in +#eval checkM `(∀ x : Nat, x = x) -- TODO: hide `ofNat` #eval checkM `(0) diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out index 3f05f0aed0..69e92b16a5 100644 --- a/tests/lean/PPRoundtrip.lean.expected.out +++ b/tests/lean/PPRoundtrip.lean.expected.out @@ -31,13 +31,17 @@ fun {α : Type} (α β : Type) → α Type → Type → Type (α : Type) → α → α -(α : Type) → - (a : α) → a = a {α : Type} → α {α : Type} → [inst : ToString α] → α +∀ (x : Nat), x = x +∀ {x : Nat} + [inst : + ToString Nat], + x = x +∀ x, x = x 0 1 42 diff --git a/tests/lean/Reformat.lean.expected.out b/tests/lean/Reformat.lean.expected.out index d0311e65c3..bedffb287c 100644 --- a/tests/lean/Reformat.lean.expected.out +++ b/tests/lean/Reformat.lean.expected.out @@ -230,7 +230,7 @@ structure PLift(α : Sort u) : Type u := up :: (down : α) /- Bijection between α and PLift α -/ -theorem PLift.upDown {α : Sort u} : ∀ (b : PLift α), Eq (up (down b)) b +theorem PLift.upDown {α : Sort u} : ∀ (b : PLift α), Eq (up (down b)) b | up a => rfl theorem PLift.downUp {α : Sort u} (a : α) : Eq (down (up a)) a := @@ -249,7 +249,7 @@ structure ULift.{r, s}(α : Type s) : Type (max s r) := up :: (down : α) /- Bijection between α and ULift.{v} α -/ -theorem ULift.upDown {α : Type u} : ∀ (b : ULift.{v} α), Eq (up (down b)) b +theorem ULift.upDown {α : Type u} : ∀ (b : ULift.{v} α), Eq (up (down b)) b | up a => rfl theorem ULift.downUp {α : Type u} (a : α) : Eq (down (up.{v} a)) a := diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out index 1624278267..9b9a248659 100644 --- a/tests/lean/precissues.lean.expected.out +++ b/tests/lean/precissues.lean.expected.out @@ -21,6 +21,6 @@ p ∧ ¬q : Prop ¬p = q : Prop ¬p = q : Prop id ¬p : Prop -(a a : Nat) → a = a : Prop +∀ (a a : Nat), a = a : Prop id : ?m → ?m precissues.lean:41:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term diff --git a/tests/lean/sizeof.lean.expected.out b/tests/lean/sizeof.lean.expected.out index e83204c032..eaf831bfd4 100644 --- a/tests/lean/sizeof.lean.expected.out +++ b/tests/lean/sizeof.lean.expected.out @@ -7,5 +7,5 @@ 308 310 11 -InfTree.node.sizeOf_spec : {α : Type u_1} → - [inst : SizeOf α] → (children : Nat → InfTree α) → sizeOf (InfTree.node children) = 1 +InfTree.node.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (children : Nat → InfTree α), + sizeOf (InfTree.node children) = 1