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

feat: pp.analyze detect when struct-inst type needed

Browse source
This commit is contained in:
Daniel Selsam 2021-07-31 07:20:20 -07:00 • committed by Sebastian Ullrich
parent e0897ae78c
commit 702211db2a
9 changed files with 54 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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

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

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

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

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

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

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

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

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

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

@ -1,4 +1,4 @@
emptyc.lean:19:0-19:2: error: ambiguous, possible interpretations
∅
{ x := 0 : A }
{ x := 0 }

13
tests/lean/infoTree.lean.expected.out
View file

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

19
tests/lean/run/PPTopDownAnalyze.lean
View file

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

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

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