From 413db56b89459d7328cee7abd669f9b99e7f4b37 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 7 Aug 2022 07:31:11 -0700 Subject: [PATCH] refactor: simplify `runTermElabM` and `liftTermElabM` --- src/Lean/Elab/BuiltinCommand.lean | 12 +++--- src/Lean/Elab/Command.lean | 18 ++++---- src/Lean/Elab/Declaration.lean | 57 +++++++++++++------------- src/Lean/Elab/DefView.lean | 2 +- src/Lean/Elab/Deriving/BEq.lean | 4 +- src/Lean/Elab/Deriving/Basic.lean | 2 +- src/Lean/Elab/Deriving/DecEq.lean | 6 +-- src/Lean/Elab/Deriving/FromToJson.lean | 8 ++-- src/Lean/Elab/Deriving/Hashable.lean | 2 +- src/Lean/Elab/Deriving/Inhabited.lean | 2 +- src/Lean/Elab/Deriving/Ord.lean | 2 +- src/Lean/Elab/Deriving/Repr.lean | 2 +- src/Lean/Elab/Deriving/SizeOf.lean | 2 +- src/Lean/Elab/GenInjective.lean | 2 +- src/Lean/Elab/Inductive.lean | 6 +-- src/Lean/Elab/MutualDef.lean | 2 +- src/Lean/Elab/Structure.lean | 4 +- src/Lean/Elab/Syntax.lean | 6 +-- src/Lean/Server/Rpc/Deriving.lean | 6 +-- src/Lean/Server/Snapshots.lean | 4 +- src/Lean/Widget/UserWidget.lean | 2 +- src/lake | 2 +- tests/lean/445.lean | 2 +- tests/lean/resolveGlobalName.lean | 2 +- tests/lean/run/PPTopDownAnalyze.lean | 4 +- tests/lean/run/matchEqs.lean | 2 +- tests/lean/run/matchEqsBug.lean | 2 +- 27 files changed, 81 insertions(+), 84 deletions(-) diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index f69c130c8c..330dab678a 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -217,7 +217,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin @[builtinCommandElab «variable»] def elabVariable : CommandElab | `(variable $binders*) => do -- Try to elaborate `binders` for sanity checking - runTermElabM none fun _ => Term.withAutoBoundImplicit <| + runTermElabM fun _ => Term.withAutoBoundImplicit <| Term.elabBinders binders fun _ => pure () for binder in binders do let binders ← replaceBinderAnnotation binder @@ -230,7 +230,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin open Meta def elabCheckCore (ignoreStuckTC : Bool) : CommandElab - | `(#check%$tk $term) => withoutModifyingEnv $ runTermElabM (some `_check) fun _ => do + | `(#check%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_check do let e ← Term.elabTerm term none Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := ignoreStuckTC) let (e, _) ← Term.levelMVarToParam (← instantiateMVars e) @@ -242,7 +242,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab @[builtinCommandElab Lean.Parser.Command.check] def elabCheck : CommandElab := elabCheckCore (ignoreStuckTC := true) @[builtinCommandElab Lean.Parser.Command.reduce] def elabReduce : CommandElab - | `(#reduce%$tk $term) => withoutModifyingEnv <| runTermElabM (some `_check) fun _ => do + | `(#reduce%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do let e ← Term.elabTerm term none Term.synthesizeSyntheticMVarsNoPostponing let (e, _) ← Term.levelMVarToParam (← instantiateMVars e) @@ -344,7 +344,7 @@ unsafe def elabEvalUnsafe : CommandElab -- Evaluate using term using `MetaEval` class. let elabMetaEval : CommandElabM Unit := do -- act? is `some act` if elaborated `term` has type `CommandElabM α` - let act? ← runTermElabM (some declName) fun _ => do + let act? ← runTermElabM fun _ => Term.withDeclName declName do let e ← elabEvalTerm let eType ← instantiateMVars (← inferType e) if eType.isAppOfArity ``CommandElabM 1 then @@ -366,7 +366,7 @@ unsafe def elabEvalUnsafe : CommandElab let some act := act? | return () act -- Evaluate using term using `Eval` class. - let elabEval : CommandElabM Unit := runTermElabM (some declName) fun _ => do + let elabEval : CommandElabM Unit := runTermElabM fun _ => Term.withDeclName declName do -- fall back to non-meta eval if MetaEval hasn't been defined yet -- modify e to `runEval e` let e ← mkRunEval (← elabEvalTerm) @@ -388,7 +388,7 @@ opaque elabEval : CommandElab @[builtinCommandElab «synth»] def elabSynth : CommandElab := fun stx => do let term := stx[1] - withoutModifyingEnv <| runTermElabM `_synth_cmd fun _ => do + withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_synth_cmd do let inst ← Term.elabTerm term none Term.synthesizeSyntheticMVarsNoPostponing let inst ← instantiateMVars inst diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index d275729341..81b3672517 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -343,20 +343,18 @@ def getBracketedBinderIds : Syntax → Array Name | `(bracketedBinder|[$_]) => #[Name.anonymous] | _ => #[] -private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name) : Term.Context := Id.run do +private def mkTermContext (ctx : Context) (s : State) : Term.Context := Id.run do let scope := s.scopes.head! let mut sectionVars := {} for id in scope.varDecls.concatMap getBracketedBinderIds, uid in scope.varUIds do sectionVars := sectionVars.insert id uid { macroStack := ctx.macroStack - declName? := declName? sectionVars := sectionVars isNoncomputableSection := scope.isNoncomputable tacticCache? := ctx.tacticCache? } /-- Lift the `TermElabM` monadic action `x` into a `CommandElabM` monadic action. -You can optionally set the current declaration name for `x` using the parameter `declName?`. Note that `x` is executed with an empty message log. Thus, `x` cannot modify/view messages produced by previous commands. @@ -375,11 +373,11 @@ def printExpr (e : Expr) : MetaM Unit := do IO.println s!"{← ppExpr e} : {← ppExpr (← inferType e)}" #eval - liftTermElabM none do + liftTermElabM do printExpr (mkConst ``Nat) ``` -/ -def liftTermElabM (declName? : Option Name) (x : TermElabM α) : CommandElabM α := do +def liftTermElabM (x : TermElabM α) : CommandElabM α := do let ctx ← read let s ← get let heartbeats ← IO.getNumHeartbeats @@ -388,7 +386,7 @@ def liftTermElabM (declName? : Option Name) (x : TermElabM α) : CommandElabM α -- We execute `x` with an empty message log. Thus, `x` cannot modify/view messages produced by previous commands. -- This is useful for implementing `runTermElabM` where we use `Term.resetMessageLog` let x : TermElabM _ := withSaveInfoContext x - let x : MetaM _ := (observing x).run (mkTermContext ctx s declName?) { levelNames := scope.levelNames } + let x : MetaM _ := (observing x).run (mkTermContext ctx s) { levelNames := scope.levelNames } let x : CoreM _ := x.run mkMetaContext {} let x : EIO _ _ := x.run (mkCoreContext ctx s heartbeats) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope, infoState.enabled := s.infoState.enabled } let (((ea, _), _), coreS) ← liftEIO x @@ -410,8 +408,6 @@ corresponding to all active scoped variables declared using the `variable` comma This method is similar to `liftTermElabM`, but it elaborates all scoped variables declared using the `variable` command. -You can optionally set the current declaration name for `elabFn xs` using the parameter `declName?`. - Example: ``` import Lean @@ -422,14 +418,14 @@ variable {α : Type u} {f : α → α} variable (n : Nat) #eval - runTermElabM none fun xs => do + runTermElabM fun xs => do for x in xs do IO.println s!"{← ppExpr x} : {← ppExpr (← inferType x)}" ``` -/ -def runTermElabM (declName? : Option Name) (elabFn : Array Expr → TermElabM α) : CommandElabM α := do +def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do let scope ← getScope - liftTermElabM declName? <| + liftTermElabM <| Term.withAutoBoundImplicit <| Term.elabBinders scope.varDecls fun xs => do -- We need to synthesize postponed terms because this is a checkpoint for the auto-bound implicit feature diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index b46320c87b..aeef19c154 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -104,34 +104,35 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do let scopeLevelNames ← getLevelNames let ⟨_, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers addDeclarationRanges declName stx - runTermElabM declName fun vars => Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do - Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration - let type ← Term.elabType typeStx - Term.synthesizeSyntheticMVarsNoPostponing - let type ← instantiateMVars type - let type ← mkForallFVars xs type - let type ← mkForallFVars vars type (usedOnly := true) - let (type, _) ← Term.levelMVarToParam type - let usedParams := collectLevelParams {} type |>.params - match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with - | Except.error msg => throwErrorAt stx msg - | Except.ok levelParams => + runTermElabM fun vars => + Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do + Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration + let type ← Term.elabType typeStx + Term.synthesizeSyntheticMVarsNoPostponing let type ← instantiateMVars type - let decl := Declaration.axiomDecl { - name := declName, - levelParams := levelParams, - type := type, - isUnsafe := modifiers.isUnsafe - } - trace[Elab.axiom] "{declName} : {type}" - Term.ensureNoUnassignedMVars decl - addDecl decl - withSaveInfoContext do -- save new env - Term.addTermInfo' declId (← mkConstWithLevelParams declName) (isBinder := true) - Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterTypeChecking - if isExtern (← getEnv) declName then - compileDecl decl - Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation + let type ← mkForallFVars xs type + let type ← mkForallFVars vars type (usedOnly := true) + let (type, _) ← Term.levelMVarToParam type + let usedParams := collectLevelParams {} type |>.params + match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with + | Except.error msg => throwErrorAt stx msg + | Except.ok levelParams => + let type ← instantiateMVars type + let decl := Declaration.axiomDecl { + name := declName, + levelParams := levelParams, + type := type, + isUnsafe := modifiers.isUnsafe + } + trace[Elab.axiom] "{declName} : {type}" + Term.ensureNoUnassignedMVars decl + addDecl decl + withSaveInfoContext do -- save new env + Term.addTermInfo' declId (← mkConstWithLevelParams declName) (isBinder := true) + Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterTypeChecking + if isExtern (← getEnv) declName then + compileDecl decl + Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation /- leading_parser "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor @@ -366,7 +367,7 @@ def elabMutual : CommandElab := fun stx => do attrInsts := attrInsts.push attrKindStx let attrs ← elabAttrs attrInsts let idents := stx[4].getArgs - for ident in idents do withRef ident <| liftTermElabM none do + for ident in idents do withRef ident <| liftTermElabM do let declName ← resolveGlobalConstNoOverloadWithInfo ident Term.applyAttributes declName attrs for attrName in toErase do diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index a4a0fd67eb..a6570d5717 100644 --- a/src/Lean/Elab/DefView.lean +++ b/src/Lean/Elab/DefView.lean @@ -83,7 +83,7 @@ def mkFreshInstanceName : CommandElabM Name := do def mkInstanceName (binders : Array Syntax) (type : Syntax) : CommandElabM Name := do let savedState ← get try - let result ← runTermElabM `inst fun _ => Term.withAutoBoundImplicit <| Term.elabBinders binders fun _ => Term.withoutErrToSorry do + let result ← runTermElabM fun _ => Term.withAutoBoundImplicit <| Term.elabBinders binders fun _ => Term.withoutErrToSorry do let type ← instantiateMVars (← Term.elabType type) let ref ← IO.mkRef "" Meta.forEachExpr type fun e => do diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index c810a7a09c..a3963f056b 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/src/Lean/Elab/Deriving/BEq.lean @@ -111,11 +111,11 @@ open Command def mkBEqInstanceHandler (declNames : Array Name) : CommandElabM Bool := do if declNames.size == 1 && (← isEnumType declNames[0]!) then - let cmds ← liftTermElabM none <| mkBEqEnumCmd declNames[0]! + let cmds ← liftTermElabM <| mkBEqEnumCmd declNames[0]! cmds.forM elabCommand return true else if (← declNames.allM isInductive) && declNames.size > 0 then - let cmds ← liftTermElabM none <| mkBEqInstanceCmds declNames + let cmds ← liftTermElabM <| mkBEqInstanceCmds declNames cmds.forM elabCommand return true else diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean index 431054587e..e3b35b6e66 100644 --- a/src/Lean/Elab/Deriving/Basic.lean +++ b/src/Lean/Elab/Deriving/Basic.lean @@ -43,7 +43,7 @@ def applyDerivingHandlers (className : Name) (typeNames : Array Name) (args? : O | none => defaultHandler className typeNames private def tryApplyDefHandler (className : Name) (declName : Name) : CommandElabM Bool := - liftTermElabM none do + liftTermElabM do Term.processDefDeriving className declName @[builtinCommandElab «deriving»] def elabDeriving : CommandElab diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index cb20007938..9e655ccddf 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -103,7 +103,7 @@ def mkDecEq (declName : Name) : CommandElabM Bool := do if indVal.isNested then return false -- nested inductive types are not supported yet else - let cmds ← liftTermElabM none <| mkDecEqCmds indVal + let cmds ← liftTermElabM <| mkDecEqCmds indVal cmds.forM elabCommand return true @@ -157,8 +157,8 @@ def mkEnumOfNatThm (declName : Name) : MetaM Unit := do } def mkDecEqEnum (declName : Name) : CommandElabM Unit := do - liftTermElabM none <| mkEnumOfNat declName - liftTermElabM none <| mkEnumOfNatThm declName + liftTermElabM <| mkEnumOfNat declName + liftTermElabM <| mkEnumOfNatThm declName let ofNatIdent := mkIdent (Name.mkStr declName "ofNat") let auxThmIdent := mkIdent (Name.mkStr declName "ofNat_toCtorIdx") let cmd ← `( diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean index 5bab186dc6..a6f0ad4b30 100644 --- a/src/Lean/Elab/Deriving/FromToJson.lean +++ b/src/Lean/Elab/Deriving/FromToJson.lean @@ -22,7 +22,7 @@ def mkJsonField (n : Name) : Bool × Term := def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do if declNames.size == 1 then if isStructure (← getEnv) declNames[0]! then - let cmds ← liftTermElabM none <| do + let cmds ← liftTermElabM do let ctx ← mkContext "toJson" declNames[0]! let header ← mkHeader ``ToJson 1 ctx.typeInfos[0]! let fields := getStructureFieldsFlattened (← getEnv) declNames[0]! (includeSubobjectFields := false) @@ -37,7 +37,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do return true else let indVal ← getConstInfoInduct declNames[0]! - let cmds ← liftTermElabM none <| do + let cmds ← liftTermElabM do let ctx ← mkContext "toJson" declNames[0]! let toJsonFuncId := mkIdent ctx.auxFunNames[0]! -- Return syntax to JSONify `id`, either via `ToJson` or recursively @@ -104,7 +104,7 @@ where def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do if declNames.size == 1 then if isStructure (← getEnv) declNames[0]! then - let cmds ← liftTermElabM none <| do + let cmds ← liftTermElabM do let ctx ← mkContext "fromJson" declNames[0]! let header ← mkHeader ``FromJson 0 ctx.typeInfos[0]! let fields := getStructureFieldsFlattened (← getEnv) declNames[0]! (includeSubobjectFields := false) @@ -119,7 +119,7 @@ def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do return true else let indVal ← getConstInfoInduct declNames[0]! - let cmds ← liftTermElabM none <| do + let cmds ← liftTermElabM do let ctx ← mkContext "fromJson" declNames[0]! let header ← mkHeader ``FromJson 0 ctx.typeInfos[0]! let fromJsonFuncId := mkIdent ctx.auxFunNames[0]! diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean index 299ed6cc97..b1b5787297 100644 --- a/src/Lean/Elab/Deriving/Hashable.lean +++ b/src/Lean/Elab/Deriving/Hashable.lean @@ -80,7 +80,7 @@ private def mkHashableInstanceCmds (declNames : Array Name) : TermElabM (Array S def mkHashableHandler (declNames : Array Name) : CommandElabM Bool := do if (← declNames.allM isInductive) && declNames.size > 0 then - let cmds ← liftTermElabM none <| mkHashableInstanceCmds declNames + let cmds ← liftTermElabM <| mkHashableInstanceCmds declNames cmds.forM elabCommand return true else diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index 60e31667a3..0fefc397fd 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -16,7 +16,7 @@ private def implicitBinderF := Parser.Term.implicitBinder private def instBinderF := Parser.Term.instBinder private def mkInhabitedInstanceUsing (inductiveTypeName : Name) (ctorName : Name) (addHypotheses : Bool) : CommandElabM Bool := do - match (← liftTermElabM none mkInstanceCmd?) with + match (← liftTermElabM mkInstanceCmd?) with | some cmd => elabCommand cmd return true diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean index a6cb31617a..a59c371009 100644 --- a/src/Lean/Elab/Deriving/Ord.lean +++ b/src/Lean/Elab/Deriving/Ord.lean @@ -96,7 +96,7 @@ open Command def mkOrdInstanceHandler (declNames : Array Name) : CommandElabM Bool := do if (← declNames.allM isInductive) && declNames.size > 0 then - let cmds ← liftTermElabM none <| mkOrdInstanceCmds declNames + let cmds ← liftTermElabM <| mkOrdInstanceCmds declNames cmds.forM elabCommand return true else diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean index ca219fbb8c..c14736f007 100644 --- a/src/Lean/Elab/Deriving/Repr.lean +++ b/src/Lean/Elab/Deriving/Repr.lean @@ -116,7 +116,7 @@ open Command def mkReprInstanceHandler (declNames : Array Name) : CommandElabM Bool := do if (← declNames.allM isInductive) && declNames.size > 0 then - let cmds ← liftTermElabM none <| mkReprInstanceCmds declNames + let cmds ← liftTermElabM <| mkReprInstanceCmds declNames cmds.forM elabCommand return true else diff --git a/src/Lean/Elab/Deriving/SizeOf.lean b/src/Lean/Elab/Deriving/SizeOf.lean index 0ab6fd59e0..0d904db525 100644 --- a/src/Lean/Elab/Deriving/SizeOf.lean +++ b/src/Lean/Elab/Deriving/SizeOf.lean @@ -17,7 +17,7 @@ open Command def mkSizeOfHandler (declNames : Array Name) : CommandElabM Bool := do if (← declNames.allM isInductive) && declNames.size > 0 then - liftTermElabM none <| Meta.mkSizeOfInstances declNames[0]! + liftTermElabM <| Meta.mkSizeOfInstances declNames[0]! return true else return false diff --git a/src/Lean/Elab/GenInjective.lean b/src/Lean/Elab/GenInjective.lean index 4ed70fed2d..808b49df3e 100644 --- a/src/Lean/Elab/GenInjective.lean +++ b/src/Lean/Elab/GenInjective.lean @@ -10,7 +10,7 @@ namespace Lean.Elab.Command @[builtinCommandElab genInjectiveTheorems] def elabGenInjectiveTheorems : CommandElab := fun stx => do let declName ← resolveGlobalConstNoOverload stx[1] - liftTermElabM none do + liftTermElabM do Meta.mkInjectiveTheorems declName end Lean.Elab.Command diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index b2443cdd44..eecaa6c147 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -831,13 +831,13 @@ private def applyComputedFields (indViews : Array InductiveView) : CommandElabM |>.setBool `elaboratingComputedFields true}) <| elabCommand <| ← `(mutual $computedFieldDefs* end) - liftTermElabM indViews[0]!.declName do + liftTermElabM do Term.withDeclName indViews[0]!.declName do ComputedFields.setComputedFields computedFields def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do let view0 := views[0]! let ref := view0.ref - runTermElabM view0.declName fun vars => withRef ref do + runTermElabM fun vars => Term.withDeclName view0.declName do withRef ref do mkInductiveDecl vars views mkSizeOfInstances view0.declName Lean.Meta.IndPredBelow.mkBelow view0.declName @@ -845,7 +845,7 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do mkInjectiveTheorems view.declName applyComputedFields views -- NOTE: any generated code before this line is invalid applyDerivingHandlers views - runTermElabM view0.declName fun _ => withRef ref do + runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do for view in views do Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 2051f75906..b6b4dfb3bd 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -873,7 +873,7 @@ def elabMutualDef (ds : Array Syntax) (hints : TerminationHints) : CommandElabM if ds.size > 1 && modifiers.isNonrec then throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block" mkDefView modifiers d[1] - runTermElabM none fun vars => Term.elabMutualDef vars views hints + runTermElabM fun vars => Term.elabMutualDef vars views hints end Command end Lean.Elab diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index fb1f111741..c596526903 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -876,7 +876,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := let derivingClassViews ← getOptDerivingClasses stx[6] let type ← if optType.isNone then `(Sort _) else pure optType[0][1] let declName ← - runTermElabM none fun scopeVars => do + runTermElabM fun scopeVars => do let scopeLevelNames ← Term.getLevelNames let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers Term.withAutoBoundImplicitForbiddenPred (fun n => name == n) do @@ -908,7 +908,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := mkInjectiveTheorems declName return declName derivingClassViews.forM fun view => view.applyHandlers #[declName] - runTermElabM declName fun _ => + runTermElabM fun _ => Term.withDeclName declName do Term.applyAttributesAt declName modifiers.attrs .afterCompilation builtin_initialize registerTraceClass `Elab.structure diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 343c10332e..caa5c1f925 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -346,7 +346,7 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do let cat := catStx.getId.eraseMacroScopes unless (Parser.isParserCategory (← getEnv) cat) do throwErrorAt catStx "unknown category '{cat}'" - liftTermElabM none <| Term.addCategoryInfo catStx cat + liftTermElabM <| Term.addCategoryInfo catStx cat let syntaxParser := mkNullNode ps -- If the user did not provide an explicit precedence, we assign `maxPrec` to atom-like syntax and `leadPrec` otherwise. let precDefault := if isAtomLikeSyntax syntaxParser then Parser.maxPrec else Parser.leadPrec @@ -359,7 +359,7 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do let prio ← liftMacroM <| evalOptPrio prio? let stxNodeKind := (← getCurrNamespace) ++ name let catParserId := mkIdentFrom stx (cat.appendAfter "Parser") - let (val, lhsPrec?) ← runTermElabM none fun _ => Term.toParserDescr syntaxParser cat + let (val, lhsPrec?) ← runTermElabM fun _ => Term.toParserDescr syntaxParser cat let declName := mkIdentFrom stx name let attrInstance ← `(attrInstance| $attrKind:attrKind $catParserId:ident $(quote prio):num) let attrInstances := attrInstances.getD { elemsAndSeps := #[] } @@ -376,7 +376,7 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do @[builtinCommandElab «syntaxAbbrev»] def elabSyntaxAbbrev : CommandElab := fun stx => do let `($[$doc?:docComment]? syntax $declName:ident := $[$ps:stx]*) ← pure stx | throwUnsupportedSyntax -- TODO: nonatomic names - let (val, _) ← runTermElabM none fun _ => Term.toParserDescr (mkNullNode ps) Name.anonymous + let (val, _) ← runTermElabM fun _ => Term.toParserDescr (mkNullNode ps) Name.anonymous let stxNodeKind := (← getCurrNamespace) ++ declName.getId let stx' ← `($[$doc?:docComment]? def $declName:ident : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val) withMacroExpansion stx stx' <| elabCommand stx' diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean index 50f0611173..6f31fc90c9 100644 --- a/src/Lean/Server/Rpc/Deriving.lean +++ b/src/Lean/Server/Rpc/Deriving.lean @@ -198,7 +198,7 @@ private def deriveInstance (typeName : Name) : CommandElabM Bool := do if indVal.numIndices ≠ 0 then throwError "indexed inductive families are not supported" - let (paramBinders, packetParamBinders, encInstBinders) ← liftTermElabM none do + let (paramBinders, packetParamBinders, encInstBinders) ← liftTermElabM do -- introduce fvars for all the parameters forallTelescopeReducing indVal.type fun params _ => do let mut paramBinders := #[] -- input parameters @@ -219,7 +219,7 @@ private def deriveInstance (typeName : Name) : CommandElabM Bool := do return (paramBinders, packetParamBinders, encInstBinders) - elabCommand <| ← liftTermElabM none do + elabCommand <| ← liftTermElabM do Term.elabBinders (paramBinders ++ packetParamBinders ++ encInstBinders) fun locals => do let params := locals[:paramBinders.size] if isStructure (← getEnv) typeName then @@ -234,7 +234,7 @@ private unsafe def dispatchDeriveInstanceUnsafe (declNames : Array Name) (args? return false let args ← if let some args := args? then - liftTermElabM none do + liftTermElabM do let argsT := mkConst ``DerivingParams let args ← elabTerm args argsT evalExpr' DerivingParams ``DerivingParams args diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index b157bd426a..dc1fdd4403 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/src/Lean/Server/Snapshots.lean @@ -80,7 +80,7 @@ def runCommandElabM (snap : Snapshot) (meta : DocumentMeta) (c : CommandElabM α fileMap := meta.text, tacticCache? := snap.tacticCache, } - c.run ctx |>.run' snap.cmdState + c.run ctx |>.run' snap.cmdState /-- Run a `CoreM` computation using the data in the given snapshot.-/ def runCoreM (snap : Snapshot) (meta : DocumentMeta) (c : CoreM α) : EIO Exception α := @@ -88,7 +88,7 @@ def runCoreM (snap : Snapshot) (meta : DocumentMeta) (c : CoreM α) : EIO Except /-- Run a `TermElabM` computation using the data in the given snapshot.-/ def runTermElabM (snap : Snapshot) (meta : DocumentMeta) (c : TermElabM α) : EIO Exception α := - snap.runCommandElabM meta <| Command.liftTermElabM none c + snap.runCommandElabM meta <| Command.liftTermElabM c end Snapshot diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index 6a193cbb84..707a797de3 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -187,7 +187,7 @@ open Elab Command in /-- Use this to place a widget. Useful for debugging widgets. -/ @[commandElab widgetCmd] def elabWidgetCmd : CommandElab := fun | stx@`(#widget $id:ident $props) => do - let props : Json ← runTermElabM none (fun _ => evalJson props) + let props : Json ← runTermElabM fun _ => evalJson props saveWidgetInfo id.getId props stx | _ => throwUnsupportedSyntax diff --git a/src/lake b/src/lake index b899c0abac..6cfb4e3fd7 160000 --- a/src/lake +++ b/src/lake @@ -1 +1 @@ -Subproject commit b899c0abac7d6c7ad69c06cd5b7964ac5684d3f0 +Subproject commit 6cfb4e3fd7ff700ace8c2cfdb85056d59f321920 diff --git a/tests/lean/445.lean b/tests/lean/445.lean index 3f19bcb976..a5c19831aa 100644 --- a/tests/lean/445.lean +++ b/tests/lean/445.lean @@ -69,7 +69,7 @@ open Lean.Meta open Lean.Elab open Lean.Elab.Command elab "unfold " e:term : command => - runTermElabM none fun xs => do + runTermElabM fun xs => do let e ← instantiateMVars (← Term.withSynthesize <| Term.elabTerm e none) match (← unfoldDefinition? e) with | some e => logInfo m!"{e}" diff --git a/tests/lean/resolveGlobalName.lean b/tests/lean/resolveGlobalName.lean index d91f7844ca..267d9531f6 100644 --- a/tests/lean/resolveGlobalName.lean +++ b/tests/lean/resolveGlobalName.lean @@ -17,7 +17,7 @@ open Lean.Elab.Command syntax (name := resolveKind) "#resolve " ident : command @[commandElab resolveKind] def elabResolve : CommandElab := -fun stx => liftTermElabM none do +fun stx => liftTermElabM do let cs ← resolveGlobalName $ stx.getIdAt 1; Lean.logInfo $ toString cs; pure () diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 04adbc85ac..668e7b39f9 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -41,7 +41,7 @@ def checkDelab (e : Expr) (tgt? : Option Term) (name? : Option Name := none) : T syntax (name := testDelabTD) "#testDelab " term " expecting " term : command @[commandElab testDelabTD] def elabTestDelabTD : CommandElab - | `(#testDelab $stx:term expecting $tgt:term) => liftTermElabM `delabTD do + | `(#testDelab $stx:term expecting $tgt:term) => liftTermElabM do withDeclName `delabTD do let e ← elabTerm stx none let ⟨e, _⟩ ← levelMVarToParam e let e ← instantiateMVars e @@ -51,7 +51,7 @@ syntax (name := testDelabTD) "#testDelab " term " expecting " term : command syntax (name := testDelabTDN) "#testDelabN " ident : command @[commandElab testDelabTDN] def elabTestDelabTDN : CommandElab - | `(#testDelabN $name:ident) => liftTermElabM `delabTD do + | `(#testDelabN $name:ident) => liftTermElabM do withDeclName `delabTD do let name := name.getId let [name] ← resolveGlobalConst (mkIdent name) | throwError "cannot resolve name" let some cInfo := (← getEnv).find? name | throwError "no decl for name" diff --git a/tests/lean/run/matchEqs.lean b/tests/lean/run/matchEqs.lean index 2f63824204..f51dfa0403 100644 --- a/tests/lean/run/matchEqs.lean +++ b/tests/lean/run/matchEqs.lean @@ -6,7 +6,7 @@ open Lean.Elab.Command @[commandElab test] def elabTest : CommandElab := fun stx => do let id ← resolveGlobalConstNoOverloadWithInfo stx[1] - liftTermElabM none do + liftTermElabM do IO.println (repr (← Lean.Meta.Match.getEquationsFor id)) return () diff --git a/tests/lean/run/matchEqsBug.lean b/tests/lean/run/matchEqsBug.lean index b2aa92495b..e69b414c2d 100644 --- a/tests/lean/run/matchEqsBug.lean +++ b/tests/lean/run/matchEqsBug.lean @@ -6,7 +6,7 @@ open Lean.Elab.Command @[commandElab test] def elabTest : CommandElab := fun stx => do let id ← resolveGlobalConstNoOverloadWithInfo stx[1] - liftTermElabM none do + liftTermElabM do IO.println (repr (← Lean.Meta.Match.getEquationsFor id)) return ()