diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean index b07d4a697d..d860361909 100644 --- a/src/Lean/Class.lean +++ b/src/Lean/Class.lean @@ -69,7 +69,7 @@ def isOutParam (e : Expr) : Bool := private partial def checkOutParam : Nat → Array FVarId → Expr → Except String Bool | i, outParams, Expr.forallE _ d b _ => if isOutParam d then - let fvarId := Name.mkNum `_fvar outParams.size + let fvarId := { name := Name.mkNum `_fvar outParams.size } let outParams := outParams.push fvarId let fvar := mkFVar fvarId let b := b.instantiate1 fvar diff --git a/src/Lean/Compiler/Util.lean b/src/Lean/Compiler/Util.lean index 6e193ee79f..c522e95f69 100644 --- a/src/Lean/Compiler/Util.lean +++ b/src/Lean/Compiler/Util.lean @@ -31,12 +31,12 @@ instance : AndThen Visitor where @[inline] def skip : Visitor := id -@[inline] def visitFVar (x y : Name) : Visitor +@[inline] def visitFVar (x y : FVarId) : Visitor | d@{result := false, ..} => d | {found := false, result := true} => {found := x == y, result := true} | {found := true, result := true} => {found := true, result := x != y} -def visit (x : Name) : Expr → Visitor +def visit (x : FVarId) : Expr → Visitor | Expr.fvar y _ => visitFVar y x | Expr.app f a _ => visit x a >> visit x f | Expr.lam _ d b _ => visit x d >> visit x b @@ -51,7 +51,7 @@ end atMostOnce open atMostOnce (visit) in /-- Return true iff the free variable with id `x` occurs at most once in `e` -/ @[export lean_at_most_once] -def atMostOnce (e : Expr) (x : Name) : Bool := +def atMostOnce (e : Expr) (x : FVarId) : Bool := let {result := result, ..} := visit x e {found := false, result := true} result diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index 3cd3ae4bf7..99f0edc1d5 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -10,7 +10,7 @@ open Command open Meta private abbrev IndexSet := Std.RBTree Nat compare -private abbrev LocalInst2Index := NameMap Nat +private abbrev LocalInst2Index := FVarIdMap Nat private def implicitBinderF := Parser.Term.implicitBinder private def instBinderF := Parser.Term.instBinder diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean index 00d9e99665..57f1752881 100644 --- a/src/Lean/Elab/InfoTree.lean +++ b/src/Lean/Elab/InfoTree.lean @@ -243,7 +243,7 @@ def Info.updateContext? : Option ContextInfo → Info → Option ContextInfo partial def InfoTree.format (tree : InfoTree) (ctx? : Option ContextInfo := none) : IO Format := do match tree with | ofJson j => return toString j - | hole id => return toString id + | hole id => return toString id.name | context i t => format t i | node i cs => match ctx? with | none => return "" diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean index 50f64259a3..77215415f0 100644 --- a/src/Lean/Elab/Level.lean +++ b/src/Lean/Elab/Level.lean @@ -38,7 +38,7 @@ instance : MonadNameGenerator LevelElabM where setNGen ngen := modify fun s => { s with ngen := ngen } def mkFreshLevelMVar : LevelElabM Level := do - let mvarId ← mkFreshId + let mvarId ← mkFreshMVarId modify fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId } return mkLevelMVar mvarId diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 4b0600b32e..75423a6085 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -406,7 +406,7 @@ def finalizePatternDecls (patternVarDecls : Array PatternVarDecl) : TermElabM (A decls := decls.push decl | PatternVarDecl.anonymousVar mvarId fvarId => let e ← instantiateMVars (mkMVar mvarId); - trace[Elab.match] "finalizePatternDecls: mvarId: {mvarId} := {e}, fvar: {mkFVar fvarId}" + trace[Elab.match] "finalizePatternDecls: mvarId: {mvarId.name} := {e}, fvar: {mkFVar fvarId}" match e with | Expr.mvar newMVarId _ => /- Metavariable was not assigned, or assigned to another metavariable. So, @@ -425,9 +425,9 @@ open Meta.Match (Pattern Pattern.var Pattern.inaccessible Pattern.ctor Pattern.a namespace ToDepElimPattern structure State where - found : NameSet := {} + found : FVarIdSet := {} localDecls : Array LocalDecl - newLocals : NameSet := {} + newLocals : FVarIdSet := {} abbrev M := StateRefT State TermElabM @@ -448,7 +448,7 @@ private def mkLocalDeclFor (mvar : Expr) : M Pattern := do match (← getExprMVarAssignment? mvarId) with | some val => return Pattern.inaccessible val | none => - let fvarId ← mkFreshId + let fvarId ← mkFreshFVarId let type ← inferType mvar /- HACK: `fvarId` is not in the scope of `mvarId` If this generates problems in the future, we should update the metavariable declarations. -/ @@ -857,7 +857,7 @@ private def expandNonAtomicDiscrs? (matchStx : Syntax) : TermElabM (Option Synta else -- We use `foundFVars` to make sure the discriminants are distinct variables. -- See: code for computing "matchType" at `elabMatchTypeAndDiscrs` - let rec loop (discrs : List Syntax) (discrsNew : Array Syntax) (foundFVars : NameSet) := do + let rec loop (discrs : List Syntax) (discrsNew : Array Syntax) (foundFVars : FVarIdSet) := do match discrs with | [] => let discrs := Syntax.mkSep discrsNew (mkAtomFrom matchStx ", "); diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index d4f857d384..a6e7e96d8c 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -266,7 +266,7 @@ private def checkLetRecsToLiftTypes (funVars : Array Expr) (letRecsToLift : List namespace MutualClosure /- A mapping from FVarId to Set of FVarIds. -/ -abbrev UsedFVarsMap := NameMap NameSet +abbrev UsedFVarsMap := FVarIdMap FVarIdSet /- Create the `UsedFVarsMap` mapping that takes the variable id for the mutually recursive functions being defined to the set of @@ -369,7 +369,7 @@ private def getUsedFVarsMap : M UsedFVarsMap := do pure (← get).usedFVarsMap private def modifyUsedFVars (f : UsedFVarsMap → UsedFVarsMap) : M Unit := modify fun s => { s with usedFVarsMap := f s.usedFVarsMap } -- merge s₂ into s₁ -private def merge (s₁ s₂ : NameSet) : M NameSet := +private def merge (s₁ s₂ : FVarIdSet) : M FVarIdSet := s₂.foldM (init := s₁) fun s₁ k => do if s₁.contains k then pure s₁ @@ -408,7 +408,7 @@ def run (letRecFVarIds : List FVarId) (usedFVarsMap : UsedFVarsMap) : UsedFVarsM end FixPoint -abbrev FreeVarMap := NameMap (Array FVarId) +abbrev FreeVarMap := FVarIdMap (Array FVarId) private def mkFreeVarMap (mctx : MetavarContext) (sectionVars : Array Expr) (mainFVarIds : Array FVarId) @@ -524,7 +524,7 @@ private def mkLetRecClosures (letRecsToLift : List LetRecToLift) (freeVarMap : F letRecsToLift.mapM fun toLift => mkLetRecClosureFor toLift (freeVarMap.find? toLift.fvarId).get! /- Mapping from FVarId of mutually recursive functions being defined to "closure" expression. -/ -abbrev Replacement := NameMap Expr +abbrev Replacement := FVarIdMap Expr def insertReplacementForMainFns (r : Replacement) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainFVars : Array Expr) : Replacement := mainFVars.size.fold (init := r) fun i r => diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 8e576dedc6..68fbcec777 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -18,7 +18,7 @@ inductive PatternVar where instance : ToString PatternVar := ⟨fun | PatternVar.localVar x => toString x - | PatternVar.anonymousVar mvarId => s!"?m{mvarId}"⟩ + | PatternVar.anonymousVar mvarId => s!"?m{mvarId.name}"⟩ /-- Create an auxiliary Syntax node wrapping a fresh metavariable id. @@ -30,7 +30,7 @@ private def mkMVarSyntax : TermElabM Syntax := do /-- Given a syntax node constructed using `mkMVarSyntax`, return its MVarId -/ def getMVarSyntaxMVarId (stx : Syntax) : MVarId := - stx[0].getKind + { name := stx[0].getKind } /- Patterns define new local variables. diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 9d2f7ad252..589d8cd55a 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -181,7 +181,7 @@ private def sortFVarIds (fvarIds : Array FVarId) : TacticM (Array FVarId) := | some d₁, some d₂ => d₁.index > d₂.index | some _, none => false | none, some _ => true - | none, none => Name.quickLt fvarId₁ fvarId₂ + | none, none => Name.quickLt fvarId₁.name fvarId₂.name @[builtinTactic Lean.Parser.Tactic.clear] def evalClear : Tactic := fun stx => match stx with diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 0dad59368b..e8e431d50f 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -376,7 +376,7 @@ private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do appendGoals result.others.toList where checkTargets (targets : Array Expr) : MetaM Unit := do - let mut foundFVars : NameSet := {} + let mut foundFVars : FVarIdSet := {} for target in targets do unless target.isFVar do throwError "index in target's type is not a variable (consider using the `cases` tactic instead){indentExpr target}" diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 71f6ce7213..5976314565 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -121,7 +121,7 @@ where else Term.elabCDotFunctionAlias? simpArgTerm -abbrev FVarIdToLemmaId := NameMap Name +abbrev FVarIdToLemmaId := FVarIdMap Name -- TODO: move? private def getPropHyps : MetaM (Array FVarId) := do diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 624ae3ee98..69cdf35a55 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -483,7 +483,7 @@ def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) (extraMsg? : Op let s ← get let hasOtherErrors := s.messages.hasErrors let mut hasNewErrors := false - let mut alreadyVisited : NameSet := {} + let mut alreadyVisited : MVarIdSet := {} for mvarErrorInfo in s.mvarErrorInfos do let mvarId := mvarErrorInfo.mvarId unless alreadyVisited.contains mvarId do diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index ff34fcd682..1239b26418 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -157,8 +157,27 @@ def Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8) open Expr -abbrev MVarId := Name -abbrev FVarId := Name +structure FVarId where + name : Name + deriving Inhabited, BEq, Hashable + +instance : Repr FVarId where + reprPrec n p := reprPrec n.name p + +def FVarIdSet := Std.RBTree FVarId (Name.quickCmp ·.name ·.name) + deriving Inhabited, EmptyCollection + +instance : ForIn m FVarIdSet FVarId := inferInstanceAs (ForIn _ (Std.RBTree ..) ..) + +def FVarIdHashSet := Std.HashSet FVarId + deriving Inhabited, EmptyCollection + +def FVarIdMap (α : Type) := Std.RBMap FVarId α (Name.quickCmp ·.name ·.name) + +instance : EmptyCollection (FVarIdMap α) := inferInstanceAs (EmptyCollection (Std.RBMap ..)) + +instance : Inhabited (FVarIdMap α) where + default := {} /- We use the `E` suffix (short for `Expr`) to avoid collision with keywords. We considered using «...», but it is too inconvenient to use. -/ @@ -1077,10 +1096,10 @@ def isLHSGoal? (e : Expr) : Option Expr := none def mkFreshFVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m FVarId := - mkFreshId + return { name := (← mkFreshId) } -def mkFreshMVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m FVarId := - mkFreshId +def mkFreshMVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m MVarId := + return { name := (← mkFreshId) } def mkNot (p : Expr) : Expr := mkApp (mkConst ``Not) p def mkOr (p q : Expr) : Expr := mkApp2 (mkConst ``Or) p q diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index 31aea81a6e..3fad358994 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -50,13 +50,32 @@ def Level.mkData (h : UInt64) (depth : Nat) (hasMVar hasParam : Bool) : Level.Da open Level +structure MVarId where + name : Name + deriving Inhabited, BEq, Hashable + +instance : Repr MVarId where + reprPrec n p := reprPrec n.name p + +def MVarIdSet := Std.RBTree MVarId (Name.quickCmp ·.name ·.name) + deriving Inhabited, EmptyCollection + +instance : ForIn m MVarIdSet MVarId := inferInstanceAs (ForIn _ (Std.RBTree ..) ..) + +def MVarIdMap (α : Type) := Std.RBMap MVarId α (Name.quickCmp ·.name ·.name) + +instance : EmptyCollection (MVarIdMap α) := inferInstanceAs (EmptyCollection (Std.RBMap ..)) + +instance : Inhabited (MVarIdMap α) where + default := {} + inductive Level where | zero : Data → Level | succ : Level → Data → Level | max : Level → Level → Data → Level | imax : Level → Level → Data → Level | param : Name → Data → Level - | mvar : Name → Data → Level + | mvar : MVarId → Data → Level deriving Inhabited namespace Level @@ -93,7 +112,7 @@ end Level def levelZero := Level.zero $ mkData 2221 0 false false -def mkLevelMVar (mvarId : Name) := +def mkLevelMVar (mvarId : MVarId) := Level.mvar mvarId $ mkData (mixHash 2237 $ hash mvarId) 0 true false def mkLevelParam (name : Name) := @@ -116,7 +135,7 @@ def levelOne := mkLevelSucc levelZero @[export lean_level_mk_zero] def mkLevelZeroEx : Unit → Level := fun _ => levelZero @[export lean_level_mk_succ] def mkLevelSuccEx : Level → Level := mkLevelSucc -@[export lean_level_mk_mvar] def mkLevelMVarEx : Name → Level := mkLevelMVar +@[export lean_level_mk_mvar] def mkLevelMVarEx : MVarId → Level := mkLevelMVar @[export lean_level_mk_param] def mkLevelParamEx : Name → Level := mkLevelParam @[export lean_level_mk_max] def mkLevelMaxEx : Level → Level → Level := mkLevelMax @[export lean_level_mk_imax] def mkLevelIMaxEx : Level → Level → Level := mkLevelIMax @@ -152,7 +171,7 @@ def isMVar : Level → Bool | mvar .. => true | _ => false -def mvarId! : Level → Name +def mvarId! : Level → MVarId | mvar mvarId _ => mvarId | _ => panic! "metavariable expected" @@ -231,7 +250,7 @@ partial def normLtAux : Level → Nat → Level → Nat → Bool else if l₁₁ != l₂₁ then normLtAux l₁₁ 0 l₂₁ 0 else normLtAux l₁₂ 0 l₂₂ 0 | param n₁ _, k₁, param n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂ -- use Name.lt because it is lexicographical - | mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.quickLt n₁ n₂ -- metavariables are temporary, the actual order doesn't matter + | mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.quickLt n₁.name n₂.name -- metavariables are temporary, the actual order doesn't matter | l₁, k₁, l₂, k₂ => if l₁ == l₂ then k₁ < k₂ else ctorToNat l₁ < ctorToNat l₂ /-- @@ -386,7 +405,7 @@ def toResult : Level → Result | imax l₁ l₂ _ => Result.imax (toResult l₁) (toResult l₂) | param n _ => Result.leaf n | mvar n _ => - let n := n.replacePrefix `_uniq (Name.mkSimple "?u"); + let n := n.name.replacePrefix `_uniq (Name.mkSimple "?u"); Result.leaf n private def parenIfFalse : Format → Bool → Format @@ -531,7 +550,7 @@ abbrev LevelSet := HashSet Level abbrev PersistentLevelSet := PHashSet Level abbrev PLevelSet := PersistentLevelSet -def Level.collectMVars (u : Level) (s : NameSet := {}) : NameSet := +def Level.collectMVars (u : Level) (s : MVarIdSet := {}) : MVarIdSet := match u with | succ v _ => collectMVars v s | max u v _ => collectMVars u (collectMVars v s) diff --git a/src/Lean/Meta/AbstractMVars.lean b/src/Lean/Meta/AbstractMVars.lean index 48d050b2b7..6813105b78 100644 --- a/src/Lean/Meta/AbstractMVars.lean +++ b/src/Lean/Meta/AbstractMVars.lean @@ -24,8 +24,8 @@ structure State where nextParamIdx : Nat := 0 paramNames : Array Name := #[] fvars : Array Expr := #[] - lmap : HashMap Name Level := {} - emap : HashMap Name Expr := {} + lmap : HashMap MVarId Level := {} + emap : HashMap MVarId Expr := {} abbrev M := StateM State @@ -35,6 +35,9 @@ def mkFreshId : M Name := do modify fun s => { s with ngen := s.ngen.next } pure fresh +def mkFreshFVarId : M FVarId := + return { name := (← mkFreshId) } + private partial def abstractLevelMVars (u : Level) : M Level := do if !u.hasMVar then return u @@ -91,7 +94,7 @@ partial def abstractExprMVars (e : Expr) : M Expr := do return e | none => let type ← abstractExprMVars decl.type - let fvarId ← mkFreshId + let fvarId ← mkFreshFVarId let fvar := mkFVar fvarId; let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter s.fvars.size else decl.userName modify fun s => { diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index e0328612df..59b42c5d28 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -157,7 +157,7 @@ structure State where mctx : MetavarContext := {} cache : Cache := {} /- When `trackZeta == true`, then any let-decl free variable that is zeta expansion performed by `MetaM` is stored in `zetaFVarIds`. -/ - zetaFVarIds : NameSet := {} + zetaFVarIds : FVarIdSet := {} postponed : PersistentArray PostponedEntry := {} deriving Inhabited @@ -264,7 +264,7 @@ def setMCtx (mctx : MetavarContext) : MetaM Unit := def resetZetaFVarIds : MetaM Unit := modify fun s => { s with zetaFVarIds := {} } -def getZetaFVarIds : MetaM NameSet := +def getZetaFVarIds : MetaM FVarIdSet := return (← get).zetaFVarIds def getPostponed : MetaM (PersistentArray PostponedEntry) := @@ -302,10 +302,10 @@ def mkFreshExprMVarAt (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (kind : MetavarKind := MetavarKind.natural) (userName : Name := Name.anonymous) (numScopeArgs : Nat := 0) : MetaM Expr := do - mkFreshExprMVarAtCore (← mkFreshId) lctx localInsts type kind userName numScopeArgs + mkFreshExprMVarAtCore (← mkFreshMVarId) lctx localInsts type kind userName numScopeArgs def mkFreshLevelMVar : MetaM Level := do - let mvarId ← mkFreshId + let mvarId ← mkFreshMVarId modifyMCtx fun mctx => mctx.addLevelMVarDecl mvarId; return mkLevelMVar mvarId @@ -365,7 +365,7 @@ def shouldReduceReducibleOnly : MetaM Bool := def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do match (← getMCtx).findDecl? mvarId with | some d => pure d - | none => throwError "unknown metavariable '?{mvarId}'" + | none => throwError "unknown metavariable '?{mvarId.name}'" def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit := modifyMCtx fun mctx => mctx.setMVarKind mvarId kind @@ -387,7 +387,7 @@ def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do def getLevelMVarDepth (mvarId : MVarId) : MetaM Nat := do match (← getMCtx).findLevelDepth? mvarId with | some depth => return depth - | _ => throwError "unknown universe metavariable '?{mvarId}'" + | _ => throwError "unknown universe metavariable '?{mvarId.name}'" def isReadOnlyLevelMVar (mvarId : MVarId) : MetaM Bool := do if (← getConfig).ignoreLevelMVarDepth then @@ -684,7 +684,7 @@ mutual | Expr.forallE n d b c => if fvarsSizeLtMaxFVars fvars maxFVars? then let d := d.instantiateRevRange j fvars.size fvars - let fvarId ← mkFreshId + let fvarId ← mkFreshFVarId let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo let fvar := mkFVar fvarId let fvars := fvars.push fvar @@ -785,14 +785,14 @@ where match consumeLet, e with | _, Expr.lam n d b c => let d := d.instantiateRevRange j fvars.size fvars - let fvarId ← mkFreshId + let fvarId ← mkFreshFVarId let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo let fvar := mkFVar fvarId process consumeLet lctx (fvars.push fvar) j b | true, Expr.letE n t v b _ => do let t := t.instantiateRevRange j fvars.size fvars let v := v.instantiateRevRange j fvars.size fvars - let fvarId ← mkFreshId + let fvarId ← mkFreshFVarId let lctx := lctx.mkLetDecl fvarId n t v let fvar := mkFVar fvarId process true lctx (fvars.push fvar) j b @@ -884,7 +884,7 @@ private def withNewFVar (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM | some c => withNewLocalInstance c fvar <| k fvar private def withLocalDeclImp (n : Name) (bi : BinderInfo) (type : Expr) (k : Expr → MetaM α) : MetaM α := do - let fvarId ← mkFreshId + let fvarId ← mkFreshFVarId let ctx ← read let lctx := ctx.lctx.mkLocalDecl fvarId n type bi let fvar := mkFVar fvarId @@ -924,7 +924,7 @@ def withNewBinderInfos (bs : Array (FVarId × BinderInfo)) (k : n α) : n α := mapMetaM (fun k => withNewBinderInfosImp bs k) k private def withLetDeclImp (n : Name) (type : Expr) (val : Expr) (k : Expr → MetaM α) : MetaM α := do - let fvarId ← mkFreshId + let fvarId ← mkFreshFVarId let ctx ← read let lctx := ctx.lctx.mkLetDecl fvarId n type val let fvar := mkFVar fvarId diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index 2f1ff9180e..d17d5dff16 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -60,7 +60,7 @@ def Key.ctorIdx : Key → Nat def Key.lt : Key → Key → Bool | Key.lit v₁, Key.lit v₂ => v₁ < v₂ - | Key.fvar n₁ a₁, Key.fvar n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂) + | Key.fvar n₁ a₁, Key.fvar n₂ a₂ => Name.quickLt n₁.name n₂.name || (n₁ == n₂ && a₁ < a₂) | Key.const n₁ a₁, Key.const n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂) | Key.proj s₁ i₁, Key.proj s₂ i₂ => Name.quickLt s₁ s₂ || (s₁ == s₂ && i₁ < i₂) | k₁, k₂ => k₁.ctorIdx < k₂.ctorIdx @@ -75,7 +75,7 @@ def Key.format : Key → Format | Key.lit (Literal.strVal v) => repr v | Key.const k _ => Std.format k | Key.proj s i => Std.format s ++ "." ++ Std.format i - | Key.fvar k _ => Std.format k + | Key.fvar k _ => Std.format k.name | Key.arrow => "→" instance : ToFormat Key := ⟨Key.format⟩ @@ -109,7 +109,7 @@ instance [ToFormat α] : ToFormat (DiscrTree α) := ⟨format⟩ /- The discrimination tree ignores implicit arguments and proofs. We use the following auxiliary id as a "mark". -/ -private def tmpMVarId : MVarId := `_discr_tree_tmp +private def tmpMVarId : MVarId := { name := `_discr_tree_tmp } private def tmpStar := mkMVar tmpMVarId instance : Inhabited (DiscrTree α) where diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 43f5557e43..f24df7da89 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -211,7 +211,7 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr) let process (n : Name) (d₁ d₂ b₁ b₂ : Expr) : MetaM Bool := do let d₁ := d₁.instantiateRev fvars let d₂ := d₂.instantiateRev fvars - let fvarId ← mkFreshId + let fvarId ← mkFreshFVarId let lctx := lctx.mkLocalDecl fvarId n d₁ let fvars := fvars.push (mkFVar fvarId) isDefEqBindingAux lctx fvars b₁ b₂ (ds₂.push d₂) @@ -303,8 +303,8 @@ where /- Traverse `e` and stores in the state `NameHashSet` any let-declaration with index greater than `(← read)`. The context `Nat` is the position of `xs[0]` in the local context. -/ - collectLetDeclsFrom (e : Expr) : ReaderT Nat (StateRefT NameHashSet MetaM) Unit := do - let rec visit (e : Expr) : MonadCacheT Expr Unit (ReaderT Nat (StateRefT NameHashSet MetaM)) Unit := + collectLetDeclsFrom (e : Expr) : ReaderT Nat (StateRefT FVarIdHashSet MetaM) Unit := do + let rec visit (e : Expr) : MonadCacheT Expr Unit (ReaderT Nat (StateRefT FVarIdHashSet MetaM)) Unit := checkCache e fun _ => do match e with | Expr.forallE _ d b _ => visit d; visit b @@ -326,7 +326,7 @@ where or equal to the position of `xs.back` in the local context. The `Nat` context `(← read)` is the position of `xs[0]` in the local context. -/ - collectLetDepsAux : Nat → ReaderT Nat (StateRefT NameHashSet MetaM) Unit + collectLetDepsAux : Nat → ReaderT Nat (StateRefT FVarIdHashSet MetaM) Unit | 0 => return () | i+1 => do if i+1 == (← read) then @@ -343,7 +343,7 @@ where collectLetDepsAux i /- Computes the set `ys`. It is a set of `FVarId`s, -/ - collectLetDeps : MetaM NameHashSet := do + collectLetDeps : MetaM FVarIdHashSet := do let lctx ← getLCtx let start := lctx.getFVar! xs[0] |>.index let stop := lctx.getFVar! xs.back |>.index diff --git a/src/Lean/Meta/GeneralizeVars.lean b/src/Lean/Meta/GeneralizeVars.lean index b5ca3481ff..22091d3ce2 100644 --- a/src/Lean/Meta/GeneralizeVars.lean +++ b/src/Lean/Meta/GeneralizeVars.lean @@ -11,7 +11,7 @@ namespace Lean.Meta /-- Add to `forbidden` all a set of `FVarId`s containing `targets` and all variables they depend on. -/ -partial def mkGeneralizationForbiddenSet (targets : Array Expr) (forbidden : NameSet := {}) : MetaM NameSet := do +partial def mkGeneralizationForbiddenSet (targets : Array Expr) (forbidden : FVarIdSet := {}) : MetaM FVarIdSet := do let mut s := { fvarSet := forbidden } let mut todo := #[] for target in targets do @@ -21,7 +21,7 @@ partial def mkGeneralizationForbiddenSet (targets : Array Expr) (forbidden : Nam s := collectFVars s (← instantiateMVars (← inferType target)) loop todo.toList s.fvarSet where - visit (fvarId : FVarId) (todo : List FVarId) (s : NameSet) : MetaM (List FVarId × NameSet) := do + visit (fvarId : FVarId) (todo : List FVarId) (s : FVarIdSet) : MetaM (List FVarId × FVarIdSet) := do let localDecl ← getLocalDecl fvarId let mut s' := collectFVars {} (← instantiateMVars localDecl.type) if let some val := localDecl.value? then @@ -34,7 +34,7 @@ where s := s.insert fvarId return (todo, s) - loop (todo : List FVarId) (s : NameSet) : MetaM NameSet := do + loop (todo : List FVarId) (s : FVarIdSet) : MetaM FVarIdSet := do match todo with | [] => return s | fvarId::todo => @@ -54,9 +54,9 @@ where Remark: we *not* collect instance implicit arguments nor auxiliary declarations for compiling recursive declarations. -/ -def getFVarSetToGeneralize (targets : Array Expr) (forbidden : NameSet) : MetaM NameSet := do - let mut s : NameSet := targets.foldl (init := {}) fun s target => if target.isFVar then s.insert target.fvarId! else s - let mut r : NameSet := {} +def getFVarSetToGeneralize (targets : Array Expr) (forbidden : FVarIdSet) : MetaM FVarIdSet := do + let mut s : FVarIdSet := targets.foldl (init := {}) fun s target => if target.isFVar then s.insert target.fvarId! else s + let mut r : FVarIdSet := {} for localDecl in (← getLCtx) do unless forbidden.contains localDecl.fvarId do unless localDecl.isAuxDecl || localDecl.binderInfo.isInstImplicit do @@ -65,12 +65,12 @@ def getFVarSetToGeneralize (targets : Array Expr) (forbidden : NameSet) : MetaM s := s.insert localDecl.fvarId return r -def sortFVars (fvars : NameSet) : MetaM (Array FVarId) := do +def sortFVars (fvars : FVarIdSet) : MetaM (Array FVarId) := do let fvarIds := fvars.fold (init := #[]) fun s fvarId => s.push fvarId let lctx ← getLCtx return fvarIds.qsort fun x y => (lctx.get! x).index < (lctx.get! y).index -def getFVarsToGeneralize (targets : Array Expr) (forbidden : NameSet := {}) : MetaM (Array FVarId) := do +def getFVarsToGeneralize (targets : Array Expr) (forbidden : FVarIdSet := {}) : MetaM (Array FVarId) := do let forbidden ← mkGeneralizationForbiddenSet targets forbidden let s ← getFVarSetToGeneralize targets forbidden sortFVars s diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 823a5d32f7..75b98fa751 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -152,12 +152,12 @@ private def inferLambdaType (e : Expr) : MetaM Expr := @[inline] private def withLocalDecl' {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α := savingCache do - let fvarId ← mkFreshId + let fvarId ← mkFreshFVarId withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do x (mkFVar fvarId) def throwUnknownMVar {α} (mvarId : MVarId) : MetaM α := - throwError "unknown metavariable '?{mvarId}'" + throwError "unknown metavariable '?{mvarId.name}'" private def inferMVarType (mvarId : MVarId) : MetaM Expr := do match (← getMCtx).findDecl? mvarId with diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean index f6d5739c89..3ff67584b1 100644 --- a/src/Lean/Meta/Match/CaseValues.lean +++ b/src/Lean/Meta/Match/CaseValues.lean @@ -46,7 +46,7 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa let clearH := false let (thenSubst, thenMVarId) ← substCore thenMVarId thenH symm subst clearH withMVarContext thenMVarId do - trace[Meta] "subst domain: {thenSubst.domain}" + trace[Meta] "subst domain: {thenSubst.domain.map (·.name)}" let thenH := (thenSubst.get thenH).fvarId! trace[Meta] "searching for decl" let decl ← getLocalDecl thenH diff --git a/src/Lean/Meta/Match/MVarRenaming.lean b/src/Lean/Meta/Match/MVarRenaming.lean index d2617d8334..cada805d9d 100644 --- a/src/Lean/Meta/Match/MVarRenaming.lean +++ b/src/Lean/Meta/Match/MVarRenaming.lean @@ -9,7 +9,7 @@ namespace Lean.Meta /- A mapping from MVarId to MVarId -/ structure MVarRenaming where - map : NameMap MVarId := {} + map : MVarIdMap MVarId := {} def MVarRenaming.isEmpty (s : MVarRenaming) : Bool := s.map.isEmpty diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index a77da5f1b5..795c78d493 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -197,13 +197,13 @@ private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (al proveSubgoal mvarId instantiateMVars proof where - mkMap : NameMap Expr := do + mkMap : FVarIdMap Expr := do let mut m := {} for alt in alts, altNew in altsNew do m := m.insert alt.fvarId! altNew return m - convertTemplate (m : NameMap Expr) : StateRefT (Array MVarId) MetaM Expr := + convertTemplate (m : FVarIdMap Expr) : StateRefT (Array MVarId) MetaM Expr := transform template fun e => do match e.getAppFn with | Expr.fvar fvarId .. => diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean index 0a1276c700..34de76d95f 100644 --- a/src/Lean/Meta/PPGoal.lean +++ b/src/Lean/Meta/PPGoal.lean @@ -29,8 +29,8 @@ def withPPInaccessibleNames [MonadControlT MetaM m] [Monad m] (x : m α) (flag : namespace ToHide structure State where - hiddenInaccessibleProp : NameSet := {} -- FVarIds of Propostions with inaccessible names but containing only visible names. We show only their types - hiddenInaccessible : NameSet := {} -- FVarIds with inaccessible names, but not in hiddenInaccessibleProp + hiddenInaccessibleProp : FVarIdSet := {} -- FVarIds of Propostions with inaccessible names but containing only visible names. We show only their types + hiddenInaccessible : FVarIdSet := {} -- FVarIds with inaccessible names, but not in hiddenInaccessibleProp modified : Bool := false structure Context where @@ -125,7 +125,7 @@ The `goalTarget` counts as a forward dependency. We say a name is visible if it is a free variable with FVarId not in `hiddenInaccessible` nor `hiddenInaccessibleProp` -/ -def collect (goalTarget : Expr) : MetaM (NameSet × NameSet) := do +def collect (goalTarget : Expr) : MetaM (FVarIdSet × FVarIdSet) := do if pp.inaccessibleNames.get (← getOptions) then /- Don't hide inaccessible names when `pp.inaccessibleNames` is set to true. -/ return ({}, {}) diff --git a/src/Lean/Meta/SortLocalDecls.lean b/src/Lean/Meta/SortLocalDecls.lean index df39bf5ede..f51ce34e25 100644 --- a/src/Lean/Meta/SortLocalDecls.lean +++ b/src/Lean/Meta/SortLocalDecls.lean @@ -28,12 +28,12 @@ mutual | Expr.app f a _ => visitExpr f; visitExpr a | Expr.mdata _ b _ => visitExpr b | Expr.mvar _ _ => let v ← instantiateMVars e; unless v.isMVar do visitExpr v - | Expr.fvar fvarId _ => if let some localDecl := (← read).localDecls.find? fvarId then visitLocalDecl localDecl + | Expr.fvar fvarId _ => if let some localDecl := (← read).localDecls.find? fvarId.name then visitLocalDecl localDecl | _ => return () partial def visitLocalDecl (localDecl : LocalDecl) : M Unit := do - unless (← get).visited.contains localDecl.fvarId do - modify fun s => { s with visited := s.visited.insert localDecl.fvarId } + unless (← get).visited.contains localDecl.fvarId.name do + modify fun s => { s with visited := s.visited.insert localDecl.fvarId.name } visitExpr localDecl.type if let some val := localDecl.value? then visitExpr val @@ -45,6 +45,6 @@ end SortLocalDecls open SortLocalDecls in def sortLocalDecls (localDecls : Array LocalDecl) : MetaM (Array LocalDecl) := let aux : M (Array LocalDecl) := do localDecls.forM visitLocalDecl; return (← get).result - aux.run { localDecls := localDecls.foldl (init := {}) fun s d => s.insert d.fvarId d } |>.run' {} + aux.run { localDecls := localDecls.foldl (init := {}) fun s d => s.insert d.fvarId.name d } |>.run' {} -end Lean.Meta \ No newline at end of file +end Lean.Meta diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 788d630804..03675e0a9d 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -131,7 +131,7 @@ partial def normExpr (e : Expr) : M Expr := do match s.emap.find? mvarId with | some e' => pure e' | none => do - let e' := mkFVar $ Name.mkNum `_tc s.nextIdx + let e' := mkFVar { name := Name.mkNum `_tc s.nextIdx } modify fun s => { s with nextIdx := s.nextIdx + 1, emap := s.emap.insert mvarId e' } pure e' | _ => pure e diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean index 097e64b33a..5bebf7fa1a 100644 --- a/src/Lean/Meta/Tactic/Intro.lean +++ b/src/Lean/Meta/Tactic/Intro.lean @@ -28,7 +28,7 @@ namespace Lean.Meta let type := type.instantiateRevRange j fvars.size fvars let type := type.headBeta let val := val.instantiateRevRange j fvars.size fvars - let fvarId ← mkFreshId + let fvarId ← mkFreshFVarId let (n, s) ← mkName lctx n true s let lctx := lctx.mkLetDecl fvarId n type val let fvar := mkFVar fvarId @@ -37,7 +37,7 @@ namespace Lean.Meta | (i+1), lctx, fvars, j, s, Expr.forallE n type body c => do let type := type.instantiateRevRange j fvars.size fvars let type := type.headBeta - let fvarId ← mkFreshId + let fvarId ← mkFreshFVarId let (n, s) ← mkName lctx n c.binderInfo.isExplicit s let lctx := lctx.mkLocalDecl fvarId n type c.binderInfo let fvar := mkFVar fvarId diff --git a/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean b/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean index f0227a76f5..a758a8abbe 100644 --- a/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean +++ b/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean @@ -52,7 +52,7 @@ def mkCongrLemma (declName : Name) (prio : Nat) : MetaM CongrLemma := withReduci lhs.withApp fun lhsFn lhsArgs => rhs.withApp fun rhsFn rhsArgs => do unless lhsFn.isConst && rhsFn.isConst && lhsFn.constName! == rhsFn.constName! && lhsArgs.size == rhsArgs.size do throwError "invalid 'congr' theorem, equality left/right-hand sides must be applications of the same function{indentExpr type}" - let mut foundMVars : NameSet := {} + let mut foundMVars : MVarIdSet := {} for lhsArg in lhsArgs do unless lhsArg.isSort do unless lhsArg.isMVar do @@ -98,7 +98,7 @@ def mkCongrLemma (declName : Name) (prio : Nat) : MetaM CongrLemma := withReduci } where /-- Return `true` if `t` contains a metavariable that is not in `mvarSet` -/ - onlyMVarsAt (t : Expr) (mvarSet : NameSet) : Bool := + onlyMVarsAt (t : Expr) (mvarSet : MVarIdSet) : Bool := Option.isNone <| t.find? fun e => e.isMVar && !mvarSet.contains e.mvarId! def addCongrLemma (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index ecea795600..b3020ea64b 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -430,7 +430,7 @@ def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (disc else return some (fvarId, mvarId) -abbrev FVarIdToLemmaId := NameMap Name +abbrev FVarIdToLemmaId := FVarIdMap Name def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (fvarIdToLemmaId : FVarIdToLemmaId := {}) : MetaM (Option (Array FVarId × MVarId)) := do withMVarContext mvarId do diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean index 2e6690862a..2e7b6f3256 100644 --- a/src/Lean/Meta/Tactic/Subst.lean +++ b/src/Lean/Meta/Tactic/Subst.lean @@ -28,7 +28,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : match a with | Expr.fvar aFVarId _ => do let aFVarIdOriginal := aFVarId - trace[Meta.Tactic.subst] "substituting {a} (id: {aFVarId}) with {b}" + trace[Meta.Tactic.subst] "substituting {a} (id: {aFVarId.name}) with {b}" let mctx ← getMCtx if mctx.exprDependsOn b aFVarId then throwTacticEx `subst mvarId m!"'{a}' occurs at{indentExpr b}" @@ -37,7 +37,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : trace[Meta.Tactic.subst] "after revert {MessageData.ofGoal mvarId}" let (twoVars, mvarId) ← introNP mvarId 2 trace[Meta.Tactic.subst] "after intro2 {MessageData.ofGoal mvarId}" - trace[Meta.Tactic.subst] "reverted variables {vars}" + trace[Meta.Tactic.subst] "reverted variables {vars.map (·.name)}" let aFVarId := twoVars[0] let a := mkFVar aFVarId let hFVarId := twoVars[1] diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index d830b38019..a2d880e5f0 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/src/Lean/Meta/Tactic/Util.lean @@ -59,7 +59,7 @@ def headBetaMVarType (mvarId : MVarId) : MetaM Unit := do /-- Collect nondependent hypotheses that are propositions. -/ def getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) := withMVarContext mvarId do - let mut candidates : NameHashSet := {} + let mut candidates : FVarIdHashSet := {} for localDecl in (← getLCtx) do unless localDecl.isAuxDecl do candidates ← removeDeps localDecl.type candidates @@ -78,9 +78,9 @@ def getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) := result := result.push localDecl.fvarId return result where - removeDeps (e : Expr) (candidates : NameHashSet) : MetaM NameHashSet := do + removeDeps (e : Expr) (candidates : FVarIdHashSet) : MetaM FVarIdHashSet := do let e ← instantiateMVars e - let visit : StateRefT NameHashSet MetaM NameHashSet := do + let visit : StateRefT FVarIdHashSet MetaM FVarIdHashSet := do e.forEach fun | Expr.fvar fvarId _ => modify fun s => s.erase fvarId | _ => pure () diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index ec285b2d26..2f7ecc85c0 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -906,7 +906,7 @@ mutual let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x -- Remark: we must reset the before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs` let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type - let newMVarId := (← get).ngen.curr + let newMVarId := { name := (← get).ngen.curr } let newMVar := mkMVar newMVarId let result := mkMVarApp mvarLCtx newMVar toRevert newMVarKind let numScopeArgs := mvarDecl.numScopeArgs + result.getAppNumArgs diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index a25cc1c739..e36cd2a4f8 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -29,7 +29,7 @@ try maybeAddBlockImplicit (mkIdent l.userName) catch _ => -- loose free variable, use internal name - maybeAddBlockImplicit $ mkIdent id + maybeAddBlockImplicit $ mkIdent id.name -- loose bound variable, use pseudo syntax @[builtinDelab bvar] @@ -43,7 +43,7 @@ def delabMVar : Delab := do let mvarDecl ← getMVarDecl n let n := match mvarDecl.userName with - | Name.anonymous => n.replacePrefix `_uniq `m + | Name.anonymous => n.name.replacePrefix `_uniq `m | n => n `(?$(mkIdent n)) diff --git a/src/Lean/Util/CollectFVars.lean b/src/Lean/Util/CollectFVars.lean index ab0f438df6..296d1fd927 100644 --- a/src/Lean/Util/CollectFVars.lean +++ b/src/Lean/Util/CollectFVars.lean @@ -9,7 +9,7 @@ namespace Lean.CollectFVars structure State where visitedExpr : ExprSet := {} - fvarSet : NameSet := {} + fvarSet : FVarIdSet := {} deriving Inhabited abbrev Visitor := State → State diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean index 97947156dc..527f6595f6 100644 --- a/src/Lean/Widget/InteractiveGoal.lean +++ b/src/Lean/Widget/InteractiveGoal.lean @@ -68,7 +68,7 @@ open Meta in /-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do let some mvarDecl ← (← getMCtx).findDecl? mvarId - | throwError "unknown goal {mvarId}" + | throwError "unknown goal {mvarId.name}" let ppAuxDecls := pp.auxDecls.get (← getOptions) let lctx := mvarDecl.lctx let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }