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

refactor: move to consistent naming for fvars in LCNF (#12611)

Browse source
This commit is contained in:
Henrik Böving 2026-02-20 13:36:45 +01:00 • committed by GitHub
parent 8702861945
commit de522117d7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
11 changed files with 50 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Compiler/IR/ToIR.lean
View file

@ -101,14 +101,14 @@ partial def lowerCode (c : LCNF.Code .impure) : M FnBody := do
let ret ← getFVarValue fvarId
return .ret ret
| .unreach .. => return .unreachable
| .sset var i offset y type k _ =>
| .sset fvarId i offset y type k _ =>
let .var y ← getFVarValue y | unreachable!
let .var var ← getFVarValue var | unreachable!
return .sset var i offset y (toIRType type) (← lowerCode k)
| .uset var i y k _ =>
let .var fvarId ← getFVarValue fvarId | unreachable!
return .sset fvarId i offset y (toIRType type) (← lowerCode k)
| .uset fvarId i y k _ =>
let .var y ← getFVarValue y | unreachable!
let .var var ← getFVarValue var | unreachable!
return .uset var i y (← lowerCode k)
let .var fvarId ← getFVarValue fvarId | unreachable!
return .uset fvarId i y (← lowerCode k)
| .inc fvarId n check persistent k _ =>
let .var var ← getFVarValue fvarId | unreachable!
return .inc var n check persistent (← lowerCode k)

8
src/Lean/Compiler/LCNF/AlphaEqv.lean
View file

@ -143,16 +143,16 @@ partial def eqv (code₁ code₂ : Code pu) : EqvM Bool := do
eqvFVar c₁.discr c₂.discr <&&>
eqvType c₁.resultType c₂.resultType <&&>
eqvAlts c₁.alts c₂.alts
| .sset var₁ i₁ offset₁ y₁ ty₁ k₁ _, .sset var₂ i₂ offset₂ y₂ ty₂ k₂ _ =>
| .sset fvarId₁ i₁ offset₁ y₁ ty₁ k₁ _, .sset fvarId₂ i₂ offset₂ y₂ ty₂ k₂ _ =>
pure (i₁ == i₂) <&&>
pure (offset₁ == offset₂) <&&>
eqvFVar var₁ var₂ <&&>
eqvFVar fvarId₁ fvarId₂ <&&>
eqvFVar y₁ y₂ <&&>
eqvType ty₁ ty₂ <&&>
eqv k₁ k₂
| .uset var₁ i₁ y₁ k₁ _, .uset var₂ i₂ y₂ k₂ _ =>
| .uset fvarId₁ i₁ y₁ k₁ _, .uset fvarId₂ i₂ y₂ k₂ _ =>
pure (i₁ == i₂) <&&>
eqvFVar var₁ var₂ <&&>
eqvFVar fvarId₁ fvarId₂ <&&>
eqvFVar y₁ y₂ <&&>
eqv k₁ k₂
| .inc fvarId₁ n₁ c₁ p₁ k₁ _, .inc fvarId₂ n₂ c₂ p₂ k₂ _ =>

23
src/Lean/Compiler/LCNF/Basic.lean
View file

@ -361,8 +361,8 @@ inductive Code (pu : Purity) where
| cases (cases : Cases pu)
| return (fvarId : FVarId)
| unreach (type : Expr)
| uset (var : FVarId) (i : Nat) (y : FVarId) (k : Code pu) (h : pu = .impure := by purity_tac)
| sset (var : FVarId) (i : Nat) (offset : Nat) (y : FVarId) (ty : Expr) (k : Code pu) (h : pu = .impure := by purity_tac)
| uset (fvarId : FVarId) (i : Nat) (y : FVarId) (k : Code pu) (h : pu = .impure := by purity_tac)
| sset (fvarId : FVarId) (i : Nat) (offset : Nat) (y : FVarId) (ty : Expr) (k : Code pu) (h : pu = .impure := by purity_tac)
| inc (fvarId : FVarId) (n : Nat) (check : Bool) (persistent : Bool) (k : Code pu) (h : pu = .impure := by purity_tac)
| dec (fvarId : FVarId) (n : Nat) (check : Bool) (persistent : Bool) (k : Code pu) (h : pu = .impure := by purity_tac)
deriving Inhabited
@ -440,8 +440,8 @@ inductive CodeDecl (pu : Purity) where
| let (decl : LetDecl pu)
| fun (decl : FunDecl pu) (h : pu = .pure := by purity_tac)
| jp (decl : FunDecl pu)
| uset (var : FVarId) (i : Nat) (y : FVarId) (h : pu = .impure := by purity_tac)
| sset (var : FVarId) (i : Nat) (offset : Nat) (y : FVarId) (ty : Expr) (h : pu = .impure := by purity_tac)
| uset (fvarId : FVarId) (i : Nat) (y : FVarId) (h : pu = .impure := by purity_tac)
| sset (fvarId : FVarId) (i : Nat) (offset : Nat) (y : FVarId) (ty : Expr) (h : pu = .impure := by purity_tac)
| inc (fvarId : FVarId) (n : Nat) (check : Bool) (persistent : Bool) (h : pu = .impure := by purity_tac)
| dec (fvarId : FVarId) (n : Nat) (check : Bool) (persistent : Bool) (h : pu = .impure := by purity_tac)
deriving Inhabited
@ -454,8 +454,8 @@ def Code.toCodeDecl! : Code pu → CodeDecl pu
| .let decl _ => .let decl
| .fun decl _ _ => .fun decl
| .jp decl _ => .jp decl
| .uset var i y _ _ => .uset var i y
| .sset var i offset ty y _ _ => .sset var i offset ty y
| .uset fvarId i y _ _ => .uset fvarId i y
| .sset fvarId i offset ty y _ _ => .sset fvarId i offset ty y
| .inc fvarId n check persistent _ _ => .inc fvarId n check persistent
| .dec fvarId n check persistent _ _ => .dec fvarId n check persistent
| _ => unreachable!
@ -469,8 +469,8 @@ where
| .let decl => go (i-1) (.let decl code)
| .fun decl _ => go (i-1) (.fun decl code)
| .jp decl => go (i-1) (.jp decl code)
| .uset var idx y _ => go (i-1) (.uset var idx y code)
| .sset var idx offset y ty _ => go (i-1) (.sset var idx offset y ty code)
| .uset fvarId idx y _ => go (i-1) (.uset fvarId idx y code)
| .sset fvarId idx offset y ty _ => go (i-1) (.sset fvarId idx offset y ty code)
| .inc fvarId n check persistent _ => go (i-1) (.inc fvarId n check persistent code)
| .dec fvarId n check persistent _ => go (i-1) (.dec fvarId n check persistent code)
else
@ -1078,8 +1078,8 @@ partial def Code.collectUsed (code : Code pu) (s : FVarIdHashSet := {}) : FVarId
| .return fvarId => s.insert fvarId
| .unreach type => collectType type s
| .jmp fvarId args => collectArgs args <| s.insert fvarId
| .sset var _ _ y _ k _ | .uset var _ y k _ =>
let s := s.insert var
| .sset fvarId _ _ y _ k _ | .uset fvarId _ y k _ =>
let s := s.insert fvarId
let s := s.insert y
k.collectUsed s
| .inc (fvarId := fvarId) (k := k) .. | .dec (fvarId := fvarId) (k := k) .. =>
@ -1093,7 +1093,8 @@ def CodeDecl.collectUsed (codeDecl : CodeDecl pu) (s : FVarIdHashSet := ∅) : F
match codeDecl with
| .let decl => collectLetValue decl.value <| collectType decl.type s
| .jp decl | .fun decl _ => decl.collectUsed s
| .sset (var := var) (y := y) .. | .uset (var := var) (y := y) .. => s.insert var |>.insert y
| .sset (fvarId := fvarId) (y := y) .. | .uset (fvarId := fvarId) (y := y) .. =>
s.insert fvarId |>.insert y
| .inc (fvarId := fvarId) .. | .dec (fvarId := fvarId) .. => s.insert fvarId
/--

5
src/Lean/Compiler/LCNF/DependsOn.lean
View file

@ -66,8 +66,9 @@ def CodeDecl.dependsOn (decl : CodeDecl pu) (s : FVarIdSet) : Bool :=
match decl with
| .let decl => decl.dependsOn s
| .jp decl | .fun decl _ => decl.dependsOn s
| .uset (var := var) (y := y) .. | .sset (var := var) (y := y) .. => s.contains var || s.contains y
| .inc (fvarId := fvarId) .. | .dec (fvarId := fvarId) .. => s.contains fvarId
| .uset (fvarId := fvarId) (y := y) .. | .sset (fvarId := fvarId) (y := y) .. =>
s.contains fvarId || s.contains y
| .inc (fvarId := fvarId) .. | .dec (fvarId := fvarId) .. => s.contains fvarId
/--
Return `true` is `c` depends on a free variable in `s`.

4
src/Lean/Compiler/LCNF/ElimDead.lean
View file

@ -95,9 +95,9 @@ partial def Code.elimDead (code : Code pu) : M (Code pu) := do
| .return fvarId => collectFVarM fvarId; return code
| .jmp fvarId args => collectFVarM fvarId; args.forM collectArgM; return code
| .unreach .. => return code
| .uset var _ y k _ | .sset var _ _ y _ k _ =>
| .uset fvarId _ y k _ | .sset fvarId _ _ y _ k _ =>
let k ← k.elimDead
if (← get).contains var then
if (← get).contains fvarId then
collectFVarM y
return code.updateCont! k
else

8
src/Lean/Compiler/LCNF/ExplicitBoxing.lean
View file

@ -274,14 +274,14 @@ partial def Code.explicitBoxing (code : Code .impure) : BoxM (Code .impure) := d
let decl ← decl.update (← getResultType) decl.params value
let k ← k.explicitBoxing
return code.updateFun! decl k
| .uset var i y k _ =>
| .uset fvarId i y k _ =>
let k ← k.explicitBoxing
castVarIfNeeded y ImpureType.usize fun y =>
return code.updateUset! var i y k
| .sset var i offset y ty k _ =>
return code.updateUset! fvarId i y k
| .sset fvarId i offset y ty k _ =>
let k ← k.explicitBoxing
castVarIfNeeded y ty fun y =>
return code.updateSset! var i offset y ty k
return code.updateSset! fvarId i offset y ty k
| .cases cs =>
let alts ← cs.alts.mapMonoM (·.mapCodeM (·.explicitBoxing))
castVarIfNeeded cs.discr (mkConst cs.typeName) fun discr =>

6
src/Lean/Compiler/LCNF/ExplicitRC.lean
View file

@ -638,10 +638,10 @@ partial def Code.explicitRc (code : Code .impure) : RcM (Code .impure) := do
addInc fvarId code
else
return code
| .uset (var := var) (k := k) .. | .sset (var := var) (k := k) .. =>
| .uset (fvarId := fvarId) (k := k) .. | .sset (fvarId := fvarId) (k := k) .. =>
let k ← k.explicitRc
-- We don't need to insert `var` since we only need to track live variables that are references at runtime
useVar var
-- We don't need to insert `fvarId` since we only need to track live variables that are references at runtime
useVar fvarId
return code.updateCont! k
| .unreach .. =>
setRetLiveVars

8
src/Lean/Compiler/LCNF/FVarUtil.lean
View file

@ -209,8 +209,8 @@ instance : TraverseFVar (CodeDecl pu) where
| .fun decl _ => return .fun (← mapFVarM f decl)
| .jp decl => return .jp (← mapFVarM f decl)
| .let decl => return .let (← mapFVarM f decl)
| .uset var i y _ => return .uset (← f var) i (← f y)
| .sset var i offset y ty _ => return .sset (← f var) i offset (← f y) (← mapFVarM f ty)
| .uset fvarId i y _ => return .uset (← f fvarId) i (← f y)
| .sset fvarId i offset y ty _ => return .sset (← f fvarId) i offset (← f y) (← mapFVarM f ty)
| .inc fvarId n check persistent _ => return .inc (← f fvarId) n check persistent
| .dec fvarId n check persistent _ => return .dec (← f fvarId) n check persistent
forFVarM f decl :=
@ -218,8 +218,8 @@ instance : TraverseFVar (CodeDecl pu) where
| .fun decl _ => forFVarM f decl
| .jp decl => forFVarM f decl
| .let decl => forFVarM f decl
| .uset var i y _ => do f var; f y
| .sset var i offset y ty _ => do f var; f y; forFVarM f ty
| .uset fvarId i y _ => do f fvarId; f y
| .sset fvarId i offset y ty _ => do f fvarId; f y; forFVarM f ty
| .inc (fvarId := fvarId) .. | .dec (fvarId := fvarId) .. => f fvarId
instance : TraverseFVar (Alt pu) where

12
src/Lean/Compiler/LCNF/Internalize.lean
View file

@ -180,16 +180,16 @@ partial def internalizeCodeDecl (decl : CodeDecl pu) : InternalizeM pu (CodeDecl
| .let decl => return .let (← internalizeLetDecl decl)
| .fun decl _ => return .fun (← internalizeFunDecl decl)
| .jp decl => return .jp (← internalizeFunDecl decl)
| .uset var i y _ =>
| .uset fvarId i y _ =>
-- Something weird should be happening if these become erased...
let .fvar var ← normFVar var | unreachable!
let .fvar fvarId ← normFVar fvarId | unreachable!
let .fvar y ← normFVar y | unreachable!
return .uset var i y
| .sset var i offset y ty _ =>
let .fvar var ← normFVar var | unreachable!
return .uset fvarId i y
| .sset fvarId i offset y ty _ =>
let .fvar fvarId ← normFVar fvarId | unreachable!
let .fvar y ← normFVar y | unreachable!
let ty ← normExpr ty
return .sset var i offset y ty
return .sset fvarId i offset y ty
| .inc fvarId n check offset _ =>
let .fvar fvarId ← normFVar fvarId | unreachable!
return .inc fvarId n check offset

4
src/Lean/Compiler/LCNF/LiveVars.lean
View file

@ -63,8 +63,8 @@ where
match c with
| .let decl k => (pure <| decl.dependsOn (← read).targetSet) <||> go k
| .jp decl k => go decl.value <||> (do markJpVisited decl.fvarId; go k)
| .uset var _ y k _ | .sset var _ _ y _ k _ =>
visitVar var <||> visitVar y <||> go k
| .uset fvarId _ y k _ | .sset fvarId _ _ y _ k _ =>
visitVar fvarId <||> visitVar y <||> go k
| .cases c => visitVar c.discr <||> c.alts.anyM (go ·.getCode)
| .jmp fvarId args =>
(pure <| args.any (·.dependsOn (← read).targetSet)) <||> do

8
src/Lean/Compiler/LCNF/PushProj.lean
View file

@ -133,10 +133,10 @@ where
| .jp decl k =>
let decl ← decl.updateValue (← decl.value.pushProj)
go k (decls.push (.jp decl))
| .uset var i y k _ =>
go k (decls.push (.uset var i y))
| .sset var i offset y ty k _ =>
go k (decls.push (.sset var i offset y ty))
| .uset fvarId i y k _ =>
go k (decls.push (.uset fvarId i y))
| .sset fvarId i offset y ty k _ =>
go k (decls.push (.sset fvarId i offset y ty))
| .inc fvarId n check persistent k _ =>
go k (decls.push (.inc fvarId n check persistent))
| .dec fvarId n check persistent k _ =>