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

refactor: replaceFVarIdAtLocalDecl => LocalDecl.replaceFVarId

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-03 10:32:45 -07:00
parent b4ad6fc289
commit cbd022e4eb
4 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -528,8 +528,8 @@ private partial def mkClosureForAux (toProcess : Array FVarId) : StateRefT Closu
newLetDecls := s.newLetDecls.push <| LocalDecl.ldecl default fvarId userName type val false,
/- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of fvarId
at `newLocalDecls` and `localDecls` -/
newLocalDecls := s.newLocalDecls.map (replaceFVarIdAtLocalDecl fvarId val)
localDecls := s.localDecls.map (replaceFVarIdAtLocalDecl fvarId val)
newLocalDecls := s.newLocalDecls.map (·.replaceFVarId fvarId val)
localDecls := s.localDecls.map (·.replaceFVarId fvarId val)
}
mkClosureForAux (pushNewVars toProcess (collectFVars (collectFVars {} type) val))

2
src/Lean/LocalContext.lean
View file

@ -423,7 +423,7 @@ export MonadLCtx (getLCtx)
instance [MonadLift m n] [MonadLCtx m] : MonadLCtx n where
getLCtx := liftM (getLCtx : m _)
def replaceFVarIdAtLocalDecl (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl :=
def LocalDecl.replaceFVarId (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl :=
if d.fvarId == fvarId then d
else match d with
| .cdecl idx id n type bi => .cdecl idx id n (type.replaceFVarId fvarId e) bi

2
src/Lean/Meta/Closure.lean
View file

@ -279,7 +279,7 @@ partial def process : ClosureM Unit := do
modify fun s => { s with newLetDecls := s.newLetDecls.push <| LocalDecl.ldecl default newFVarId userName type val false }
/- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of newFVarId
at `newLocalDecls` -/
modify fun s => { s with newLocalDecls := s.newLocalDecls.map (replaceFVarIdAtLocalDecl newFVarId val) }
modify fun s => { s with newLocalDecls := s.newLocalDecls.map (·.replaceFVarId newFVarId val) }
process
@[inline] def mkBinding (isLambda : Bool) (decls : Array LocalDecl) (b : Expr) : Expr :=

5
src/Lean/Meta/Match/Basic.lean
View file

@ -152,10 +152,11 @@ def applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt :=
def replaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : Alt :=
{ alt with
patterns := alt.patterns.map fun p => p.replaceFVarId fvarId v,
rhs := alt.rhs.replaceFVarId fvarId v
fvarDecls :=
let decls := alt.fvarDecls.filter fun d => d.fvarId != fvarId
decls.map $ replaceFVarIdAtLocalDecl fvarId v,
rhs := alt.rhs.replaceFVarId fvarId v }
decls.map (·.replaceFVarId fvarId v)
}
/--
Similar to `checkAndReplaceFVarId`, but ensures type of `v` is definitionally equal to type of `fvarId`.