diff --git a/src/Lean/Compiler/LCNF/Simp/Used.lean b/src/Lean/Compiler/LCNF/Simp/Used.lean index c23230de47..7a25688fd0 100644 --- a/src/Lean/Compiler/LCNF/Simp/Used.lean +++ b/src/Lean/Compiler/LCNF/Simp/Used.lean @@ -5,9 +5,6 @@ Authors: Leonardo de Moura -/ import Lean.Compiler.LCNF.Simp.SimpM -set_option warningAsError false -#exit - namespace Lean.Compiler.LCNF namespace Simp @@ -19,18 +16,37 @@ def markUsedFVar (fvarId : FVarId) : SimpM Unit := modify fun s => { s with used := s.used.insert fvarId } /-- -Mark all free variables occurring in `e` as used. +Mark all free variables occurring in `type` as used. This is information is used to eliminate dead local declarations. -/ -def markUsedExpr (e : Expr) : SimpM Unit := - modify fun s => { s with used := collectLocalDecls s.used e } +def markUsedType (type : Expr) : SimpM Unit := + modify fun s => { s with used := collectLocalDeclsType s.used type } + +/-- +Mark all free variables occurring in `arg` as used. +-/ +def markUsedArg (arg : Arg) : SimpM Unit := + match arg with + | .fvar fvarId => markUsedFVar fvarId + | .type type => markUsedType type + | .erased => return () + +/-- +Mark all free variables occurring in `e` as used. +-/ +def markUsedLetExpr (e : LetExpr) : SimpM Unit := do + match e with + | .value .. | .erased => return () + | .proj _ _ fvarId => markUsedFVar fvarId + | .const _ _ args => args.forM markUsedArg + | .fvar fvarId args => markUsedFVar fvarId; args.forM markUsedArg /-- Mark all free variables occurring on the right-hand side of the given let declaration as used. This is information is used to eliminate dead local declarations. -/ def markUsedLetDecl (letDecl : LetDecl) : SimpM Unit := - markUsedExpr letDecl.value + markUsedLetExpr letDecl.value mutual /-- @@ -42,7 +58,7 @@ partial def markUsedCode (code : Code) : SimpM Unit := do | .jp decl k | .fun decl k => markUsedFunDecl decl; markUsedCode k | .return fvarId => markUsedFVar fvarId | .unreach .. => return () - | .jmp fvarId args => markUsedFVar fvarId; args.forM markUsedExpr + | .jmp fvarId args => markUsedFVar fvarId; args.forM markUsedArg | .cases c => markUsedFVar c.discr; c.alts.forM fun alt => markUsedCode alt.getCode /--