From d2ff2de4f632d64730da7f0db8385074d072d3bd Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Wed, 28 Jul 2021 16:29:17 -0700 Subject: [PATCH] feat: add @ to consts/locals with pi {..} type --- .../PrettyPrinter/Delaborator/Builtins.lean | 33 ++++++---- .../Delaborator/TopDownAnalyze.lean | 61 +++++++++++-------- tests/lean/run/PPTopDownAnalyze.lean | 10 ++- 3 files changed, 60 insertions(+), 44 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index ed3a5618af..d042a474f1 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -14,15 +14,18 @@ open Lean.Meta open Lean.Parser.Term open SubExpr +def maybeAddExplicit (ident : Syntax) : DelabM Syntax := do + if ← getPPOption getPPAnalysisNeedsExplicit then `(@$ident:ident) else ident + @[builtinDelab fvar] def delabFVar : Delab := do let Expr.fvar id _ ← getExpr | unreachable! try let l ← getLocalDecl id - pure $ mkIdent l.userName + maybeAddExplicit (mkIdent l.userName) catch _ => -- loose free variable, use internal name - pure $ mkIdent id + maybeAddExplicit $ mkIdent id -- loose bound variable, use pseudo syntax @[builtinDelab bvar] @@ -113,17 +116,21 @@ def delabConst : Delab := do c := (privateToUserName? c).getD c let ppUnivs ← getPPOption getPPUniverses - if ls.isEmpty || !ppUnivs then - if (← getLCtx).usesUserName c then - -- `c` is also a local declaration - if c == c₀ && !(← read).inPattern then - -- `c` is the fully qualified named. So, we append the `_root_` prefix - c := `_root_ ++ c - else - c := c₀ - return mkIdent c - else - `($(mkIdent c).{$[$(ls.toArray.map quote)],*}) + + let stx ← + if ls.isEmpty || !ppUnivs then + if (← getLCtx).usesUserName c then + -- `c` is also a local declaration + if c == c₀ && !(← read).inPattern then + -- `c` is the fully qualified named. So, we append the `_root_` prefix + c := `_root_ ++ c + else + c := c₀ + return mkIdent c + else + `($(mkIdent c).{$[$(ls.toArray.map quote)],*}) + + maybeAddExplicit stx inductive ParamKind where | explicit diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index c50f608326..6c516dbd52 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -67,11 +67,12 @@ def getPPAnalyzeTrustSubst (o : Options) : Bool := o.get pp.ana def getPPAnalyzeTrustOfNat (o : Options) : Bool := o.get pp.analyze.trustOfNat.name pp.analyze.trustOfNat.defValue def getPPAnalyzeTrustKnownFOType2TypeHOFuns (o : Options) : Bool := o.get pp.analyze.trustKnownFOType2TypeHOFuns.name pp.analyze.trustKnownFOType2TypeHOFuns.defValue -def getPPAnalysisSkip (o : Options) : Bool := o.get `pp.analysis.skip false -def getPPAnalysisHole (o : Options) : Bool := o.get `pp.analysis.hole false -def getPPAnalysisNamedArg (o : Options) : Bool := o.get `pp.analysis.namedArg false -def getPPAnalysisLetVarType (o : Options) : Bool := o.get `pp.analysis.letVarType true -def getPPAnalysisNeedsType (o : Options) : Bool := o.get `pp.analysis.needsType false +def getPPAnalysisSkip (o : Options) : Bool := o.get `pp.analysis.skip false +def getPPAnalysisHole (o : Options) : Bool := o.get `pp.analysis.hole false +def getPPAnalysisNamedArg (o : Options) : Bool := o.get `pp.analysis.namedArg false +def getPPAnalysisLetVarType (o : Options) : Bool := o.get `pp.analysis.letVarType true +def getPPAnalysisNeedsType (o : Options) : Bool := o.get `pp.analysis.needsType false +def getPPAnalysisNeedsExplicit (o : Options) : Bool := o.get `pp.analysis.needsExplicit false namespace PrettyPrinter.Delaborator @@ -197,9 +198,10 @@ def isSubstLike (e : Expr) : Bool := open SubExpr structure Context where - knowsType : Bool - knowsLevel : Bool -- only constants look at this - inBottomUp : Bool := false + knowsType : Bool + knowsLevel : Bool -- only constants look at this + inBottomUp : Bool := false + parentIsApp : Bool := false deriving Inhabited, Repr structure State where @@ -227,22 +229,23 @@ def annotateName (n : Name) (v : Name) : AnalyzeM Unit := do let opts := (← get).annotations.findD pos {} |>.setName n v modify fun s => { s with annotations := s.annotations.insert pos opts } -partial def analyze : AnalyzeM Unit := do +partial def analyze (parentIsApp : Bool := false) : AnalyzeM Unit := do checkMaxHeartbeats "Delaborator.topDownAnalyze" trace[pp.analyze] "{(← read).knowsType}.{(← read).knowsLevel} {← getExpr}" - match (← getExpr) with - | Expr.app .. => analyzeApp - | Expr.forallE .. => analyzePi - | Expr.lam .. => analyzeLam - | Expr.const .. => analyzeConst - | Expr.sort .. => analyzeSort - | Expr.proj .. => analyzeProj - | Expr.fvar .. => analyzeFVar - | Expr.mdata .. => analyzeMData - | Expr.letE .. => analyzeLet - | Expr.lit .. => pure () - | Expr.mvar .. => pure () - | Expr.bvar .. => unreachable! + withReader (fun ctx => { ctx with parentIsApp := parentIsApp }) do + match (← getExpr) with + | Expr.app .. => analyzeApp + | Expr.forallE .. => analyzePi + | Expr.lam .. => analyzeLam + | Expr.const .. => analyzeConst + | Expr.sort .. => analyzeSort + | Expr.proj .. => analyzeProj + | Expr.fvar .. => analyzeFVar + | Expr.mdata .. => analyzeMData + | Expr.letE .. => analyzeLet + | Expr.lit .. => pure () + | Expr.mvar .. => pure () + | Expr.bvar .. => unreachable! where analyzeApp := do withKnowing true true $ analyzeAppStaged (← getExpr).getAppFn (← getExpr).getAppArgs @@ -283,7 +286,7 @@ where higherOrders := higherOrders.set! i true -- Now, if this is the first staging, analyze the n-ary function without expected type - if !f.isApp then withKnowing false !(← instantiateMVars fType).hasLevelMVar $ withNaryFn analyze + if !f.isApp then withKnowing false !(← instantiateMVars fType).hasLevelMVar $ withNaryFn (analyze (parentIsApp := true)) let disableNamedImplicits : Bool := getPPAnalyzeTrustSubst (← getOptions) && isSubstLike (← getExpr) @@ -316,11 +319,19 @@ where if not rest.isEmpty then analyzeAppStaged (mkAppN f args) rest + maybeAddExplicit : AnalyzeM Unit := do + -- See `MonadLift.noConfusion for an example where this is necessary. + if !(← read).parentIsApp then + let type ← inferType (← getExpr) + if type.isForall && type.bindingInfo! == BinderInfo.implicit then + annotateBool `pp.analysis.needsExplicit true + analyzeConst : AnalyzeM Unit := do - -- TODO: currently, the analyzer never uses @, + -- TODO: currently, the analyzer never uses @ for applications, -- even though named arguments do not work for inaccessible names let Expr.const n ls .. ← getExpr | unreachable! annotateBool `pp.universes (!(← read).knowsLevel && !ls.isEmpty) + maybeAddExplicit analyzePi : AnalyzeM Unit := do annotateBool `pp.binderTypes true @@ -342,7 +353,7 @@ where analyzeSort : AnalyzeM Unit := pure () analyzeProj : AnalyzeM Unit := withProj analyze - analyzeFVar : AnalyzeM Unit := pure () + analyzeFVar : AnalyzeM Unit := maybeAddExplicit analyzeMData : AnalyzeM Unit := withMDataExpr analyze valUnknown (e : Expr) : AnalyzeM Bool := do diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 6f6dc78010..339fce4036 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -223,6 +223,10 @@ def fooReadGetModify : ReaderT Unit (StateT Unit IO) Unit := do #testDelabN Lean.Syntax.getOptionalIdent? #testDelabN Lean.Meta.ppExpr #testDelabN Eq.mprProp +#testDelabN MonadLift.noConfusion +#testDelabN MonadLift.noConfusionType +#testDelabN MonadExcept.noConfusion +#testDelabN MonadFinally.noConfusion -- TODO: this test is broken because of the inability to solve structural max constraints -- (See https://github.com/leanprover/lean4/issues/590) @@ -234,11 +238,5 @@ def fooReadGetModify : ReaderT Unit (StateT Unit IO) Unit := do -- #testDelabN Std.ShareCommon.ObjectMap.find? -- #testDelabN Std.ShareCommon.ObjectMap.insert --- TODO: these all fail currently because of implicit lambdas --- #testDelabN MonadLift.noConfusion --- #testDelabN MonadLift.noConfusionType --- #testDelabN MonadExcept.noConfusion --- #testDelabN MonadFinally.noConfusion - -- TODO: these fail because we are not disable named patterns when not using `match` syntax -- #testDelabN Lean.Elab.InfoTree.goalsAt?.match_1