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

feat: new pp.analyze.knowsType option

Browse source
This commit is contained in:
Daniel Selsam 2021-07-31 08:04:12 -07:00 • committed by Sebastian Ullrich
parent 7576b1dad1
commit 3fa992c684
2 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
View file

@ -88,6 +88,12 @@ register_builtin_option pp.analyze.omitMax : Bool := {
descr := "(pretty printer analyzer) omit universe `max` annotations (these constraints can actually hurt)"
}
register_builtin_option pp.analyze.knowsType : Bool := {
defValue := true
group := "pp.analyze"
descr := "(pretty printer analyzer) assume the type of the original expression is known"
}
def getPPAnalyze (o : Options) : Bool := o.get pp.analyze.name pp.analyze.defValue
def getPPAnalyzeCheckInstances (o : Options) : Bool := o.get pp.analyze.checkInstances.name pp.analyze.checkInstances.defValue
def getPPAnalyzeTypeAscriptions (o : Options) : Bool := o.get pp.analyze.typeAscriptions.name pp.analyze.typeAscriptions.defValue
@ -98,6 +104,7 @@ def getPPAnalyzeTrustId (o : Options) : Bool := o.get pp.ana
def getPPAnalyzeTrustCoe (o : Options) : Bool := o.get pp.analyze.trustCoe.name pp.analyze.trustCoe.defValue
def getPPAnalyzeTrustKnownFOType2TypeHOFuns (o : Options) : Bool := o.get pp.analyze.trustKnownFOType2TypeHOFuns.name pp.analyze.trustKnownFOType2TypeHOFuns.defValue
def getPPAnalyzeOmitMax (o : Options) : Bool := o.get pp.analyze.omitMax.name pp.analyze.omitMax.defValue
def getPPAnalyzeKnowsType (o : Options) : Bool := o.get pp.analyze.knowsType.name pp.analyze.knowsType.defValue
def getPPAnalysisSkip (o : Options) : Bool := o.get `pp.analysis.skip false
def getPPAnalysisHole (o : Options) : Bool := o.get `pp.analysis.hole false
@ -488,7 +495,8 @@ def topDownAnalyze (e : Expr) : MetaM OptionsPerPos := do
withReader (fun ctx => { ctx with config := Lean.Elab.Term.setElabConfig ctx.config }) do
let ϕ : AnalyzeM OptionsPerPos := do analyze; (← get).annotations
try
ϕ { knowsType := true, knowsLevel := true } (mkRoot e) |>.run' {}
let knowsType := getPPAnalyzeKnowsType (← getOptions)
ϕ { knowsType := knowsType, knowsLevel := knowsType } (mkRoot e) |>.run' {}
catch ex =>
trace[pp.analyze.error] "failed"
pure {}

3
tests/lean/PPRoundtrip.lean
View file

@ -59,6 +59,9 @@ end
-- specify the expected type of `a` in a way that is not erased by the delaborator
def typeAs.{u} (α : Type u) (a : α) := ()
set_option pp.analyze.knowsType false in
#eval checkM `(fun (a : Nat) => a)
#eval checkM `(fun (a : Nat) => a)
#eval checkM `(fun (a b : Nat) => a)
#eval checkM `(fun (a : Nat) (b : Bool) => a)