chore(lean/typeclass): distinguish 'TmpMVar' from 'MVar'

library/init/lean/typeclass/context.lean

@@ -86,7 +86,7 @@ partial def eFind (f : Expr → Bool) : Expr → Bool
 def eOccursIn (t₀ : Expr) (e : Expr) : Bool :=
 eFind (λ t => t == t₀) e
 
-def eHasEMVar (e : Expr) : Bool :=
+def eHasETmpMVar (e : Expr) : Bool :=
 eFind eIsMeta e
 
 -- Levels
@@ -135,7 +135,7 @@ partial def uFind (f : Level → Bool) : Level → Bool
 def uOccursIn (l₀ : Level) (l : Level) : Bool :=
 uFind (λ l => l == l₀) l
 
-def uHasMVar (l : Level) : Bool :=
+def uHasTmpMVar (l : Level) : Bool :=
 uFind uIsMeta l
 
 partial def uUnify : Level → Level → EState String Context Unit
@@ -175,9 +175,9 @@ partial def uInstantiate (ctx : Context) : Level → Level
 
 -- Expressions and Levels
 
-def eHasMVar (e : Expr) : Bool :=
+def eHasTmpMVar (e : Expr) : Bool :=
 if e.hasMVar
-then eFind (λ t => eIsMeta t || (t.isConst && t.constLevels.any uHasMVar)) e
+then eFind (λ t => eIsMeta t || (t.isConst && t.constLevels.any uHasTmpMVar)) e
 else false
 
 partial def slowWhnfApp : Expr → List Expr → Expr

library/init/lean/typeclass/synth.lean

@@ -60,7 +60,7 @@ structure TableEntry : Type :=
 structure TCState : Type :=
 (env            : Environment)
 (finalAnswer    : Option TypedExpr                  := none)
-(mainMVar       : Expr                              := default _)
+(mainTmpMVar       : Expr                              := default _)
 (generatorStack : Array GeneratorNode               := Array.empty)
 (consumerStack  : Array ConsumerNode                := Array.empty)
 (resumeQueue    : Queue (ConsumerNode × TypedExpr)  := {})
@@ -106,14 +106,14 @@ do let mvarType := ctx.eInfer mvar;
        .. ϕ
      }
 
-partial def introduceMVars (lctx : LocalContext) (locals : Array Expr) : Context → Expr → Expr → Array Expr → Context × Expr × Expr × Array Expr
+partial def introduceTmpMVars (lctx : LocalContext) (locals : Array Expr) : Context → Expr → Expr → Array Expr → Context × Expr × Expr × Array Expr
 | ctx, instVal, Expr.pi _ info domain body, mvars => do
   let ⟨mvar, ctx⟩ := (Context.eNewMeta $ lctx.mkForall locals domain).run ctx;
   let arg := mkApp mvar locals.toList; -- TODO(dselsam): rm toList
   let instVal := Expr.app instVal arg;
   let instType := body.instantiate1 arg;
   let mvars := if info.isInstImplicit then mvars.push mvar else mvars;
-  introduceMVars ctx instVal instType mvars
+  introduceTmpMVars ctx instVal instType mvars
 
 | ctx, instVal, instType, mvars => (ctx, instVal, instType, mvars)
 
@@ -130,13 +130,13 @@ def tryResolve (ctx : Context) (futureAnswer : TypedExpr) (instTE : TypedExpr) :
 do let ⟨mvar, mvarType⟩ := futureAnswer;
    let ⟨instVal, instType⟩ := instTE;
    let ⟨lctx, mvarType, locals⟩ := introduceLocals 0 {} Array.empty mvarType;
-   let ⟨ctx, instVal, instType, newMVars⟩ := introduceMVars lctx locals ctx instVal instType Array.empty;
+   let ⟨ctx, instVal, instType, newTmpMVars⟩ := introduceTmpMVars lctx locals ctx instVal instType Array.empty;
    match (Context.eUnify mvarType instType *> Context.eUnify mvar (lctx.mkLambda locals instVal)).run ctx with
    | EState.Result.error msg   _ => pure none
-   | EState.Result.ok    _   ctx => pure $ some $ (ctx, newMVars.toList) -- TODO(dselsam): rm toList
+   | EState.Result.ok    _   ctx => pure $ some $ (ctx, newTmpMVars.toList) -- TODO(dselsam): rm toList
 
-def newConsumerNode (node : Node) (ctx : Context) (newMVars : List Expr) : TCMethod Unit :=
-let cNode : ConsumerNode := { remainingSubgoals := newMVars, ctx := ctx, .. node };
+def newConsumerNode (node : Node) (ctx : Context) (newTmpMVars : List Expr) : TCMethod Unit :=
+let cNode : ConsumerNode := { remainingSubgoals := newTmpMVars, ctx := ctx, .. node };
 modify $ λ ϕ => { consumerStack := ϕ.consumerStack.push cNode, .. ϕ }
 
 def resume : TCMethod Unit :=
@@ -152,7 +152,7 @@ do ((cNode, answer), resumeQueue) ← get >>= λ ϕ =>
      modify $ λ ϕ => { resumeQueue := resumeQueue, .. ϕ };
      match result with
      | none => pure ()
-     | some (ctx, newMVars) => newConsumerNode cNode.toNode ctx (newMVars ++ rest)
+     | some (ctx, newTmpMVars) => newConsumerNode cNode.toNode ctx (newTmpMVars ++ rest)
 
 def wakeUp (answer : TypedExpr) : Waiter → TCMethod Unit
 | Waiter.root               => modify $ λ ϕ => { finalAnswer := some answer .. ϕ }
@@ -176,7 +176,7 @@ do cNode ← get >>= λ ϕ => pure ϕ.consumerStack.back;
        val := cNode.ctx.eInstantiate cNode.futureAnswer.val,
        type := cNode.ctx.eInstantiate cNode.futureAnswer.type
      };
-     when (Context.eHasMVar answer.val || Context.eHasMVar answer.type) $
+     when (Context.eHasTmpMVar answer.val || Context.eHasTmpMVar answer.type) $
        throw $ "answer " ++ toString answer ++ " not fully instantiated";
      modify $ λ ϕ => { consumerStack := ϕ.consumerStack.pop .. ϕ };
      newAnswer cNode.anormSubgoal answer
@@ -227,7 +227,7 @@ do gNode ← get >>= λ ϕ => pure ϕ.generatorStack.back;
      modify $ λ ϕ => { generatorStack := nextGeneratorStack, .. ϕ };
      match result with
      | none => pure ()
-     | some (ctx, newMVars) => newConsumerNode gNode.toNode ctx newMVars
+     | some (ctx, newTmpMVars) => newConsumerNode gNode.toNode ctx newTmpMVars
 
 def step : TCMethod Unit :=
 do ϕ ← get;
@@ -248,7 +248,7 @@ partial def synthCoreFueled (ctx₀ : Context) (goalType : Expr) : Nat → TCMet
 def synthCore (ctx₀ : Context) (goalType : Expr) (fuel : Nat) : TCMethod TypedExpr :=
 do let ⟨mvar, ctx⟩ := (Context.eNewMeta goalType).run ctx₀;
    newSubgoal Waiter.root ctx mvar;
-   modify $ λ ϕ => { mainMVar := mvar .. ϕ };
+   modify $ λ ϕ => { mainTmpMVar := mvar .. ϕ };
    synthCoreFueled ctx₀ goalType fuel
 
 def collectUReplacements : List Level → Context → Array (Level × Level) → Array Level
@@ -304,7 +304,7 @@ do env ← get >>= λ ϕ => pure ϕ.env;
    | EState.Result.error msg _ => throw $ "outParams do not match: " ++ toString goalType₀ ++ " ≠ " ++ toString instType
    | EState.Result.ok _ ctx => do
      let instVal : Expr := ctx.eInstantiate instVal;
-     when (Context.eHasMVar instVal) $ throw "synthesized instance has mvar";
+     when (Context.eHasTmpMVar instVal) $ throw "synthesized instance has mvar";
      pure instVal
 
 end TypeClass