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

refactor: change addTermInfo type

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-08 07:45:46 -07:00
parent 74435013f4
commit ea682830d1
11 changed files with 39 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Lean/Elab/App.lean
View file

@ -721,7 +721,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
match lvalRes with
| LValResolution.projIdx structName idx =>
let f ← mkProjAndCheck structName idx f
addTermInfo lval.getRef f
let f ← addTermInfo lval.getRef f
loop f lvals
| LValResolution.projFn baseStructName structName fieldName =>
let f ← mkBaseProjections baseStructName structName f
@ -729,7 +729,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
if isPrivateNameFromImportedModule (← getEnv) info.projFn then
throwError "field '{fieldName}' from structure '{structName}' is private"
let projFn ← mkConst info.projFn
addTermInfo lval.getRef projFn
let projFn ← addTermInfo lval.getRef projFn
if lvals.isEmpty then
let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
@ -741,7 +741,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
| LValResolution.const baseStructName structName constName =>
let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
let projFn ← mkConst constName
addTermInfo lval.getRef projFn
let projFn ← addTermInfo lval.getRef projFn
if lvals.isEmpty then
let projFnType ← inferType projFn
let (args, namedArgs) ← addLValArg baseStructName constName f args namedArgs projFnType
@ -750,7 +750,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
let f ← elabAppArgs projFn #[] #[Arg.expr f] (expectedType? := none) (explicit := false) (ellipsis := false)
loop f lvals
| LValResolution.localRec baseName fullName fvar =>
addTermInfo lval.getRef fvar
let fvar ← addTermInfo lval.getRef fvar
if lvals.isEmpty then
let fvarType ← inferType fvar
let (args, namedArgs) ← addLValArg baseName fullName f args namedArgs fvarType
@ -760,7 +760,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
loop f lvals
| LValResolution.getOp fullName idx =>
let getOpFn ← mkConst fullName
addTermInfo lval.getRef getOpFn
let getOpFn ← addTermInfo lval.getRef getOpFn
if lvals.isEmpty then
let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
let namedArgs ← addNamedArg namedArgs { name := `idx, val := Arg.stx idx }
@ -811,7 +811,7 @@ private partial def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level)
funLVals.foldlM (init := acc) fun acc (f, fIdent, fields) => do
let lvals' := toLVals fields (first := true)
let s ← observing do
addTermInfo fIdent f expectedType?
let f ← addTermInfo fIdent f expectedType?
let e ← elabAppLVals f (lvals' ++ lvals) namedArgs args expectedType? explicit ellipsis
if overloaded then ensureHasType expectedType? e else pure e
return acc.push s
@ -874,7 +874,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
unless (← getEnv).contains idNew do
throwError "invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
let fConst ← mkConst idNew
addTermInfo f fConst
let fConst ← addTermInfo f fConst
let s ← observing do
let e ← elabAppLVals fConst lvals namedArgs args expectedType? explicit ellipsis
if overloaded then ensureHasType expectedType? e else pure e

6
src/Lean/Elab/Binders.lean
View file

@ -137,8 +137,8 @@ private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) := do
private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit :=
registerCustomErrorIfMVar type ref "failed to infer binder type"
def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit := do
addTermInfo (isBinder := true) stx fvar
def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit :=
addTermInfo' (isBinder := true) stx fvar
private def ensureAtomicBinderName (binderView : BinderView) : TermElabM Unit :=
let n := binderView.id.getId.eraseMacroScopes
@ -360,7 +360,7 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat
We do not believe this is an useful feature, and it would complicate the logic here.
-/
let lctx := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi
addTermInfo (lctx? := some lctx) (isBinder := true) binderView.id fvar
addTermInfo' (lctx? := some lctx) (isBinder := true) binderView.id fvar
let s ← withRef binderView.id <| propagateExpectedType fvar type s
let s := { s with lctx := lctx }
match (← isClass? type) with

2
src/Lean/Elab/Declaration.lean
View file

@ -96,7 +96,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
Term.ensureNoUnassignedMVars decl
addDecl decl
withSaveInfoContext do -- save new env
Term.addTermInfo declId (← mkConstWithLevelParams declName) (isBinder := true)
Term.addTermInfo' declId (← mkConstWithLevelParams declName) (isBinder := true)
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterTypeChecking
if isExtern (← getEnv) declName then
compileDecl decl

6
src/Lean/Elab/Inductive.lean
View file

@ -677,7 +677,7 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
let mut indTypesArray := #[]
for i in [:views.size] do
let indFVar := indFVars[i]
Term.addTermInfo (isBinder := true) views[i].declId indFVar
Term.addLocalVarInfo views[i].declId indFVar
let r := rs[i]
let type ← mkForallFVars params r.type
let ctors ← elabCtors indFVars indFVar params r
@ -708,9 +708,9 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
mkAuxConstructions views
withSaveInfoContext do -- save new env
for view in views do
Term.addTermInfo view.ref[1] (← mkConstWithLevelParams view.declName) (isBinder := true)
Term.addTermInfo' view.ref[1] (← mkConstWithLevelParams view.declName) (isBinder := true)
for ctor in view.ctors do
Term.addTermInfo ctor.ref[2] (← mkConstWithLevelParams ctor.declName) (isBinder := true)
Term.addTermInfo' ctor.ref[2] (← mkConstWithLevelParams ctor.declName) (isBinder := true)
-- We need to invoke `applyAttributes` because `class` is implemented as an attribute.
Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking

6
src/Lean/Elab/LetRec.lean
View file

@ -77,8 +77,8 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
forallBoundedTelescope view.type view.binderIds.size fun xs type => do
-- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
for i in [0:view.binderIds.size] do
addTermInfo (isBinder := true) view.binderIds[i] xs[i]
withDeclName view.declName do
addLocalVarInfo view.binderIds[i] xs[i]
withDeclName view.declName do
let value ← elabTermEnsuringType view.valStx type
mkLambdaFVars xs value
@ -108,7 +108,7 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
let view ← mkLetRecDeclView stx
withAuxLocalDecls view.decls fun fvars => do
for decl in view.decls, fvar in fvars do
addTermInfo (isBinder := true) decl.ref fvar
addLocalVarInfo decl.ref fvar
let values ← elabLetRecDeclValues view
let body ← elabTermEnsuringType view.body expectedType?
registerLetRecsToLift view.decls fvars values

3
src/Lean/Elab/Match.lean
View file

@ -62,8 +62,7 @@ private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do
| some e@(Expr.fvar fvarId _) =>
let localDecl ← getLocalDecl fvarId
if !isAuxDiscrName localDecl.userName then
addTermInfo discr e
return e -- it is not an auxiliary local created by `expandNonAtomicDiscrs?`
addTermInfo discr e -- it is not an auxiliary local created by `expandNonAtomicDiscrs?`
else
instantiateMVars localDecl.value
| _ => throwErrorAt discr "unexpected discriminant"

4
src/Lean/Elab/MutualDef.lean
View file

@ -202,7 +202,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array
-- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
for i in [0:header.binderIds.size] do
-- skip auto-bound prefix in `xs`
addTermInfo (isBinder := true) header.binderIds[i] xs[header.numParams - header.binderIds.size + i]
addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]
let val ← elabTermEnsuringType valStx type
mkLambdaFVars xs val
@ -730,7 +730,7 @@ where
let allUserLevelNames := getAllUserLevelNames headers
withFunLocalDecls headers fun funFVars => do
for view in views, funFVar in funFVars do
addTermInfo (isBinder := true) view.declId funFVar
addLocalVarInfo view.declId funFVar
let values ← elabFunValues headers
Term.synthesizeSyntheticMVarsNoPostponing
let values ← values.mapM (instantiateMVars ·)

4
src/Lean/Elab/PreDefinition/Basic.lean
View file

@ -115,7 +115,7 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (applyAttrAft
safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe }
addDecl decl
withSaveInfoContext do -- save new env
addTermInfo preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
if preDef.modifiers.isNoncomputable then
modifyEnv fun env => addNoncomputable env preDef.declName
@ -154,7 +154,7 @@ def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSaf
addDecl decl
withSaveInfoContext do -- save new env
for preDef in preDefs do
addTermInfo preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
applyAttributesOf preDefs AttributeApplicationTime.afterTypeChecking
unless (← compileDecl decl) do
return ()

2
src/Lean/Elab/PreDefinition/Main.lean
View file

@ -88,7 +88,7 @@ private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
}
addDecl decl
withSaveInfoContext do -- save new env
addTermInfo preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation

6
src/Lean/Elab/Structure.lean
View file

@ -826,13 +826,13 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
let decl ← Term.getFVarLocalDecl! info.fvar
pure (info.isSubobject && decl.binderInfo.isInstImplicit)
withSaveInfoContext do -- save new env
Term.addTermInfo view.ref[1] (← mkConstWithLevelParams view.declName) (isBinder := true)
Term.addLocalVarInfo view.ref[1] (← mkConstWithLevelParams view.declName)
if let some _ := view.ctor.ref[1].getPos? (originalOnly := true) then
Term.addTermInfo view.ctor.ref[1] (← mkConstWithLevelParams view.ctor.declName) (isBinder := true)
Term.addTermInfo' view.ctor.ref[1] (← mkConstWithLevelParams view.ctor.declName) (isBinder := true)
for field in view.fields do
-- may not exist if overriding inherited field
if (← getEnv).contains field.declName then
Term.addTermInfo field.ref (← mkConstWithLevelParams field.declName) (isBinder := true)
Term.addTermInfo' field.ref (← mkConstWithLevelParams field.declName) (isBinder := true)
Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
let projInstances := instParents.toList.map fun info => info.declName
projInstances.forM fun declName => addInstance declName AttributeKind.global (eval_prio default)

18
src/Lean/Elab/Term.lean
View file

@ -993,8 +993,17 @@ def mkTermInfo (elaborator : Name) (stx : Syntax) (e : Expr) (expectedType? : Op
let e := removeSaveInfoAnnotation e
return Sum.inl <| Info.ofTermInfo { elaborator, lctx := lctx?.getD (← getLCtx), expr := e, stx, expectedType?, isBinder }
def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator := Name.anonymous) (isBinder := false) : TermElabM Unit := do
def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator := Name.anonymous) (isBinder := false) : TermElabM Expr := do
-- TODO: do not save info when inPattern is true, and store `stx` in `Expr.mdata`
withInfoContext' (pure ()) (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder) |> discard
return e
def addTermInfo' (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator := Name.anonymous) (isBinder := false) : TermElabM Unit :=
discard <| addTermInfo stx e expectedType? lctx? elaborator isBinder
def withInfoContext' (stx : Syntax) (x : TermElabM Expr) (mkInfo : Expr → TermElabM (Sum Info MVarId)) : TermElabM Expr := do
-- TODO: do not save info when inPattern is true, and store `stx` in `Expr.mdata`
Elab.withInfoContext' x mkInfo
/-
Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or
@ -1005,7 +1014,7 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
| (elabFn::elabFns) =>
try
-- record elaborator in info tree, but only when not backtracking to other elaborators (outer `try`)
withInfoContext' (mkInfo := mkTermInfo elabFn.declName (expectedType? := expectedType?) stx)
withInfoContext' stx (mkInfo := mkTermInfo elabFn.declName (expectedType? := expectedType?) stx)
(try
elabFn.value stx expectedType?
catch ex => match ex with
@ -1190,7 +1199,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
match (← liftMacroM (expandMacroImpl? env stx)) with
| some (decl, stxNew?) =>
let stxNew ← liftMacroM <| liftExcept stxNew?
withInfoContext' (mkInfo := mkTermInfo decl (expectedType? := expectedType?) stx) <|
withInfoContext' stx (mkInfo := mkTermInfo decl (expectedType? := expectedType?) stx) <|
withMacroExpansion stx stxNew <|
withRef stxNew <|
elabTermAux expectedType? catchExPostpone implicitLambda stxNew
@ -1523,8 +1532,7 @@ def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (
match fs with
| [] => return none
| [f] =>
if withInfo then
addTermInfo stx f
let f ← if withInfo then addTermInfo stx f else pure f
return some f
| _ => throwError "ambiguous {kind}, use fully qualified name, possible interpretations {fs}"
| _ => throwError "identifier expected"