From 702211db2a917e73f9568ace3b6e47b27b81ebdc Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Sat, 31 Jul 2021 07:20:20 -0700 Subject: [PATCH] feat: pp.analyze detect when struct-inst type needed --- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 2 +- .../Delaborator/TopDownAnalyze.lean | 54 +++++++++---------- tests/lean/236.lean.expected.out | 2 +- tests/lean/243.lean.expected.out | 4 +- tests/lean/415.lean.expected.out | 4 +- tests/lean/emptyc.lean.expected.out | 2 +- tests/lean/infoTree.lean.expected.out | 13 +++-- tests/lean/run/PPTopDownAnalyze.lean | 19 +++++-- tests/lean/structInstError.lean.expected.out | 2 +- 9 files changed, 54 insertions(+), 48 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index d2f49e9247..2df03f6f2d 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -184,7 +184,7 @@ def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o) def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o) def getPPStructureProjections (o : Options) : Bool := o.get pp.structureProjections.name (!getPPAll o) def getPPStructureInstances (o : Options) : Bool := o.get pp.structureInstances.name (!getPPAll o) -def getPPStructureInstanceType (o : Options) : Bool := o.get pp.structureInstanceTypes.name (getPPAll o || getPPAnalyze o) +def getPPStructureInstanceType (o : Options) : Bool := o.get pp.structureInstanceTypes.name (getPPAll o) def getPPUniverses (o : Options) : Bool := o.get pp.universes.name (getPPAll o) def getPPFullNames (o : Options) : Bool := o.get pp.fullNames.name (getPPAll o) def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPAll o) diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index eaa559472c..9992786920 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -191,17 +191,6 @@ def tryUnify (t s : Expr) : MetaM Unit := do trace[pp.analyze.tryUnify] "warning: isDefEq threw" pure () -structure BottomUpKind where - needsType : Bool - needsLevel : Bool - deriving Inhabited, Repr, BEq - -def BottomUpKind.safe : BottomUpKind := ⟨false, false⟩ -def BottomUpKind.unsafe : BottomUpKind := ⟨true, true⟩ - -def BottomUpKind.isSafe : BottomUpKind → Bool := (· == BottomUpKind.safe) -def BottomUpKind.isUnsafe : BottomUpKind → Bool := (· == BottomUpKind.unsafe) - partial def inspectOutParams (arg mvar : Expr) : MetaM Unit := do let argType ← inferType arg -- HAdd α α α let mvarType ← inferType mvar @@ -222,18 +211,18 @@ where inspectAux (fb.instantiate1 args[i]) (mb.instantiate1 mvars[i]) (i+1) args mvars | _, _ => return () -partial def okBottomUp? (e : Expr) (mvar? : Option Expr := none) (fuel : Nat := 10) : MetaM BottomUpKind := do +partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat := 10) : MetaM Bool := do -- Here we check if `e` can be safely elaborated without its expected type. -- These are incomplete (and possibly unsound) heuristics. -- TODO: do I need to snapshot the state before calling this? match fuel with - | 0 => BottomUpKind.unsafe + | 0 => false | fuel + 1 => - if e.isFVar || e.isNatLit || e.isStringLit then return BottomUpKind.safe - if getPPAnalyzeTrustOfNat (← getOptions) && e.isAppOfArity `OfNat.ofNat 3 then return BottomUpKind.safe - if getPPAnalyzeTrustOfScientific (← getOptions) && e.isAppOfArity `OfScientific.ofScientific 5 then return BottomUpKind.safe + if e.isFVar || e.isNatLit || e.isStringLit then return true + if getPPAnalyzeTrustOfNat (← getOptions) && e.isAppOfArity `OfNat.ofNat 3 then return true + if getPPAnalyzeTrustOfScientific (← getOptions) && e.isAppOfArity `OfScientific.ofScientific 5 then return true let f := e.getAppFn - if !f.isConst && !f.isFVar then return BottomUpKind.unsafe + if !f.isConst && !f.isFVar then return false let args := e.getAppArgs let fType ← replaceLPsWithVars (← inferType e.getAppFn) let ⟨mvars, bInfos, resultType⟩ ← forallMetaBoundedTelescope fType e.getAppArgs.size @@ -241,13 +230,11 @@ partial def okBottomUp? (e : Expr) (mvar? : Option Expr := none) (fuel : Nat := if bInfos[i] == BinderInfo.instImplicit then inspectOutParams args[i] mvars[i] else if bInfos[i] == BinderInfo.default then - match ← okBottomUp? args[i] mvars[i] fuel with - | ⟨false, false⟩ => tryUnify args[i] mvars[i] - | _ => pure () + if ← canBottomUp args[i] mvars[i] fuel then tryUnify args[i] mvars[i] if ← (isHBinOp e <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then tryUnify mvars[0] mvars[1] if mvar?.isSome then tryUnify resultType (← inferType mvar?.get!) let resultType ← instantiateMVars resultType - pure ⟨resultType.hasExprMVar, resultType.hasLevelMVar⟩ + return !resultType.hasMVar def isHigherOrder (type : Expr) : MetaM Bool := do withTransparency TransparencyMode.all do forallTelescopeReducing type fun xs b => xs.size > 0 && b.isSort @@ -334,11 +321,22 @@ partial def analyze (parentIsApp : Bool := false) : AnalyzeM Unit := do | Expr.bvar .. => pure () where analyzeApp := do - let needsType := !(← read).knowsType && !(← okBottomUp? (← getExpr)).isSafe withKnowing true true $ analyzeAppStaged (← getExpr).getAppFn (← getExpr).getAppArgs - if needsType then - annotateBool `pp.analysis.needsType - withType $ withKnowing true false $ analyze + + if !(← read).knowsType then + if !(← canBottomUp (← getExpr)) then + annotateBool `pp.analysis.needsType + withType $ withKnowing true false $ analyze + else + -- structure instances will "seem" bottomUp-okay but may not be when + -- pretty-printed as its fields. + match (← getExpr).isConstructorApp? (← getEnv) with + | none => pure () + | some s => + if isStructure (← getEnv) s.induct then + withType do + annotateBool `pp.structureInstanceTypes + withKnowing true false $ analyze analyzeAppStaged (f : Expr) (args : Array Expr) : AnalyzeM Unit := do let fType ← replaceLPsWithVars (← inferType f) @@ -356,14 +354,14 @@ where -- more complex ones. for i in [:args.size] do if bInfos[i] == BinderInfo.default then - if (← valUnknown mvars[i]) && (← okBottomUp? args[i]).isSafe then + if ← valUnknown mvars[i] <&&> canBottomUp args[i] then tryUnify args[i] mvars[i] bottomUps := bottomUps.set! i true -- Now, collect explicit arguments that can be elaborated with *incomplete* top-down info for i in [:args.size] do if !bottomUps[i] && bInfos[i] == BinderInfo.default then - if (← valUnknown mvars[i]) && (← okBottomUp? args[i] mvars[i]).isSafe then + if ← valUnknown mvars[i] <&&> canBottomUp args[i] mvars[i] then tryUnify args[i] mvars[i] bottomUps := bottomUps.set! i true @@ -460,7 +458,7 @@ where analyzeLet : AnalyzeM Unit := do let Expr.letE n t v body .. ← getExpr | unreachable! - if (← okBottomUp? v).needsType then + if !(← canBottomUp v) then annotateBool `pp.analysis.letVarType withLetVarType $ withKnowing true false analyze withLetValue $ withKnowing true true analyze diff --git a/tests/lean/236.lean.expected.out b/tests/lean/236.lean.expected.out index 4725b33322..226d08e3ac 100644 --- a/tests/lean/236.lean.expected.out +++ b/tests/lean/236.lean.expected.out @@ -1,3 +1,3 @@ -{ x := 10, b := true : Foo } : Foo +{ x := 10, b := true } : Foo Foo.mk (@OfNat.ofNat.{0} Nat 10 (instOfNatNat 10)) Bool.true : Foo { x := OfNat.ofNat 10, b := Bool.true : Foo } : Foo diff --git a/tests/lean/243.lean.expected.out b/tests/lean/243.lean.expected.out index 80d009511c..a036080057 100644 --- a/tests/lean/243.lean.expected.out +++ b/tests/lean/243.lean.expected.out @@ -1,5 +1,5 @@ 243.lean:2:3-2:14: error: application type mismatch - { fst := Bool, snd := true : Sigma fun α => α } + { fst := Bool, snd := true } argument true has type @@ -7,7 +7,7 @@ has type but is expected to have type Bool : Type 243.lean:13:3-13:8: error: application type mismatch - { fst := A, snd := A.a : Sigma fun α => α } + { fst := A, snd := A.a } argument A.a has type diff --git a/tests/lean/415.lean.expected.out b/tests/lean/415.lean.expected.out index 89268ecdeb..dd657ca7fb 100644 --- a/tests/lean/415.lean.expected.out +++ b/tests/lean/415.lean.expected.out @@ -1,4 +1,4 @@ Set.insert (Set.insert (Set.insert Set.empty 1) 2) 3 : Set Nat -fun x y => g { x := x, y := y : Point } : Nat → Nat → Nat +fun x y => g { x := x, y := y } : Nat → Nat → Nat fun x y => Set.insert (Set.insert Set.empty x) y : Nat → Nat → Set Nat -fun x y => { x := x, y := y : Point } : Nat → Nat → Point +fun x y => { x := x, y := y } : Nat → Nat → Point diff --git a/tests/lean/emptyc.lean.expected.out b/tests/lean/emptyc.lean.expected.out index 4ed6354e75..3a730562fc 100644 --- a/tests/lean/emptyc.lean.expected.out +++ b/tests/lean/emptyc.lean.expected.out @@ -1,4 +1,4 @@ emptyc.lean:19:0-19:2: error: ambiguous, possible interpretations ∅ - { x := 0 : A } + { x := 0 } diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index 365fb4cfe8..5ba46c68bb 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -297,26 +297,25 @@ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent [.] `B : some Sort.{?_uniq.1896} @ ⟨33, 19⟩-⟨33, 20⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ - { pair := ({ val := id : A }, { val := id : A }) : - B } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst - ({ val := id : A }, { val := id : A }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩ @ Lean.Elab.Term.expandParen + { pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst + ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩ @ Lean.Elab.Term.expandParen Macro expansion ({ val := id }, { val := id }) ===> Prod.mk✝ { val := id } { val := id } - ({ val := id : A }, { val := id : A }) : A × A @ ⟨34, 10⟩†-⟨34, 39⟩ @ Lean.Elab.Term.elabApp + ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩†-⟨34, 39⟩ @ Lean.Elab.Term.elabApp Prod.mk : {α β : Type} → α → β → α × β @ ⟨34, 10⟩†-⟨34, 40⟩† - { val := id : A } : A @ ⟨34, 11⟩-⟨34, 24⟩ @ Lean.Elab.Term.StructInst.elabStructInst + { val := id } : A @ ⟨34, 11⟩-⟨34, 24⟩ @ Lean.Elab.Term.StructInst.elabStructInst id : Nat → Nat @ ⟨34, 20⟩-⟨34, 22⟩ @ Lean.Elab.Term.elabIdent [.] `id : some Nat -> Nat @ ⟨34, 20⟩-⟨34, 22⟩ id : {α : Type} → α → α @ ⟨34, 20⟩-⟨34, 22⟩ val : Nat → Nat := id @ ⟨34, 13⟩-⟨34, 16⟩ - { val := id : A } : A @ ⟨34, 26⟩-⟨34, 39⟩ @ Lean.Elab.Term.StructInst.elabStructInst + { val := id } : A @ ⟨34, 26⟩-⟨34, 39⟩ @ Lean.Elab.Term.StructInst.elabStructInst id : Nat → Nat @ ⟨34, 35⟩-⟨34, 37⟩ @ Lean.Elab.Term.elabIdent [.] `id : some Nat -> Nat @ ⟨34, 35⟩-⟨34, 37⟩ id : {α : Type} → α → α @ ⟨34, 35⟩-⟨34, 37⟩ val : Nat → Nat := id @ ⟨34, 28⟩-⟨34, 31⟩ - pair : A × A := ({ val := id : A }, { val := id : A }) @ ⟨34, 2⟩-⟨34, 6⟩ + pair : A × A := ({ val := id }, { val := id }) @ ⟨34, 2⟩-⟨34, 6⟩ def Nat.xor : Nat → Nat → Nat := bitwise bne [Elab.info] command @ ⟨37, 0⟩-⟨38, 10⟩ @ Lean.Elab.Command.expandInCmd diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index c3b9d2c195..c164af7615 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -109,7 +109,7 @@ def fPolyInst {α : Type u} [Add α] : α → α → α := Add.add def fPolyNotInst {α : Type u} (inst : Add α) : α → α → α := Add.add #testDelab @fPolyNotInst Nat ⟨Nat.add⟩ - expecting fPolyNotInst { add := Nat.add : Add Nat } + expecting fPolyNotInst { add := Nat.add } #testDelab (fun (x : Nat) => x) Nat.zero expecting (fun (x : Nat) => x) Nat.zero @@ -131,17 +131,17 @@ instance : Foo Bool := ⟨true⟩ expecting Foo.foo #testDelab @Foo.foo Bool ⟨false⟩ - expecting Foo.foo (self := { foo := false : Foo Bool }) + expecting Foo.foo (self := { foo := false }) axiom wild {α : Type u} {f : α → Type v} {x : α} [_inst_1 : Foo (f x)] : Nat abbrev nat2bool : Nat → Type := fun _ => Bool #testDelab @wild Nat nat2bool Nat.zero ⟨false⟩ - expecting wild (f := nat2bool) (x := Nat.zero) (_inst_1 := { foo := false : Foo (nat2bool Nat.zero) }) + expecting wild (f := nat2bool) (x := Nat.zero) (_inst_1 := { foo := false }) #testDelab @wild Nat (fun (n : Nat) => Bool) Nat.zero ⟨false⟩ - expecting wild (f := fun n => Bool) (x := Nat.zero) (_inst_1 := { foo := false : Foo Bool }) + expecting wild (f := fun n => Bool) (x := Nat.zero) (_inst_1 := { foo := false }) #testDelab (fun {α : Type u} (x : α) => x : ∀ {α : Type u}, α → α) expecting fun {α} x => x @@ -188,7 +188,7 @@ set_option pp.analyze.trustSubst true in set_option pp.analyze.trustId true in #testDelab Sigma.mk (β := fun α => α) Bool true - expecting { fst := Bool, snd := true : Sigma fun α => α } + expecting { fst := Bool, snd := true } set_option pp.analyze.trustId false in #testDelab Sigma.mk (β := fun α => α) Bool true @@ -236,6 +236,15 @@ set_option pp.analyze.trustCoe true in #testDelab fun (xs : List Nat) => xs ≠ xs expecting fun xs => xs ≠ xs +structure S1 where x : Unit +structure S2 where x : Unit + +#testDelab { x := () : S1 } + expecting { x := () } + +#testDelab (fun (u : Unit) => { x := () : S2 }) () + expecting (fun (u : Unit) => { x := () : S2 }) () + #testDelabN Nat.brecOn #testDelabN Nat.below #testDelabN Nat.mod_lt diff --git a/tests/lean/structInstError.lean.expected.out b/tests/lean/structInstError.lean.expected.out index cf099f6ede..32fc54a551 100644 --- a/tests/lean/structInstError.lean.expected.out +++ b/tests/lean/structInstError.lean.expected.out @@ -1,2 +1,2 @@ structInstError.lean:5:7-5:29: error: invalid {...} notation, expected type is not known -{ x := 10, b := true : Foo } : Foo +{ x := 10, b := true } : Foo