From ea682830d1684df4bdcc2eeeeac84f05a0e10952 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 Apr 2022 07:45:46 -0700 Subject: [PATCH] refactor: change `addTermInfo` type --- src/Lean/Elab/App.lean | 14 +++++++------- src/Lean/Elab/Binders.lean | 6 +++--- src/Lean/Elab/Declaration.lean | 2 +- src/Lean/Elab/Inductive.lean | 6 +++--- src/Lean/Elab/LetRec.lean | 6 +++--- src/Lean/Elab/Match.lean | 3 +-- src/Lean/Elab/MutualDef.lean | 4 ++-- src/Lean/Elab/PreDefinition/Basic.lean | 4 ++-- src/Lean/Elab/PreDefinition/Main.lean | 2 +- src/Lean/Elab/Structure.lean | 6 +++--- src/Lean/Elab/Term.lean | 18 +++++++++++++----- 11 files changed, 39 insertions(+), 32 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 9150eb5442..d7b427c4cb 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -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 diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 3bbf647fd2..6d8e79cddf 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -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 diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 77ab3344b8..b95bfd70b6 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -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 diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index f5b7efc304..37ae5dd701 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -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 diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index 8669931858..dfa2763582 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/src/Lean/Elab/LetRec.lean @@ -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 diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 8cb27b6b17..1ff649285c 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -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" diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index c2a0145d5b..daa8b993e0 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -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 ·) diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index e4e05a76d9..200bebccd0 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -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 () diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index b0dde5d2de..6d2c1ee56c 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -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 diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 13c5b9b8b9..f7b5fa1c81 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -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) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 58c5d9536f..bed9b0c6dc 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -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"