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

refactor: move to Meta namespace

Browse source
This commit is contained in:
Leonardo de Moura 2021-10-06 19:05:37 -07:00
parent def7641926
commit c02b4f2675
3 changed files with 10 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/Inductive.lean
View file

@ -368,13 +368,13 @@ private def checkResultingUniverses (indTypes : List InductiveType) : TermElabM
private def collectUsed (indTypes : List InductiveType) : StateRefT CollectFVars.State MetaM Unit := do
indTypes.forM fun indType => do
Term.collectUsedFVars indType.type
Meta.collectUsedFVars indType.type
indType.ctors.forM fun ctor =>
Term.collectUsedFVars ctor.type
Meta.collectUsedFVars ctor.type
private def removeUnused (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (LocalContext × LocalInstances × Array Expr) := do
let (_, used) ← (collectUsed indTypes).run {}
Term.removeUnused vars used
Meta.removeUnused vars used
private def withUsed {α} (vars : Array Expr) (indTypes : List InductiveType) (k : Array Expr → TermElabM α) : TermElabM α := do
let (lctx, localInsts, vars) ← removeUnused vars indTypes

8
src/Lean/Elab/Structure.lean
View file

@ -588,18 +588,18 @@ private def getResultUniverse (type : Expr) : TermElabM Level := do
private def collectUsed (params : Array Expr) (fieldInfos : Array StructFieldInfo) : StateRefT CollectFVars.State MetaM Unit := do
params.forM fun p => do
let type ← inferType p
Term.collectUsedFVars type
Meta.collectUsedFVars type
fieldInfos.forM fun info => do
let fvarType ← inferType info.fvar
Term.collectUsedFVars fvarType
Meta.collectUsedFVars fvarType
match info.value? with
| none => pure ()
| some value => Term.collectUsedFVars value
| some value => Meta.collectUsedFVars value
private def removeUnused (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo)
: TermElabM (LocalContext × LocalInstances × Array Expr) := do
let (_, used) ← (collectUsed params fieldInfos).run {}
Term.removeUnused scopeVars used
Meta.removeUnused scopeVars used
private def withUsed {α} (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) (k : Array Expr → TermElabM α)
: TermElabM α := do

7
src/Lean/Meta/CollectFVars.lean
View file

@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
import Lean.Util.CollectFVars
import Lean.Elab.Term
namespace Lean.Elab.Term
namespace Lean.Meta
open Meta
def collectUsedFVars (e : Expr) : StateRefT CollectFVars.State MetaM Unit := do
@ -22,8 +22,7 @@ def removeUnused (vars : Array Expr) (used : CollectFVars.State) : MetaM (LocalC
let localInsts ← getLocalInstances
let lctx ← getLCtx
let (lctx, localInsts, newVars, _) ← vars.foldrM
(fun var (result : LocalContext × LocalInstances × Array Expr × CollectFVars.State) => do
let (lctx, localInsts, newVars, used) := result
(fun var (lctx, localInsts, newVars, used) => do
if used.fvarSet.contains var.fvarId! then
let varType ← inferType var
let (_, used) ← (collectUsedFVars varType).run used
@ -33,4 +32,4 @@ def removeUnused (vars : Array Expr) (used : CollectFVars.State) : MetaM (LocalC
(lctx, localInsts, #[], used)
pure (lctx, localInsts, newVars.reverse)
end Lean.Elab.Term
end Lean.Meta