From 6fe52cac418bab53e5ba8d43330525cb57fddf15 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 14 Nov 2022 21:09:40 +0100 Subject: [PATCH] doc: explain some decisions in ElimDeadBranches --- src/Lean/Compiler/LCNF/ElimDeadBranches.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean index 14047efef1..160a574c77 100644 --- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean +++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean @@ -465,6 +465,12 @@ where return .top | .fvar _ args => args.forM handleFunArg + /- + Since free variables in `LetValue`s cannot be of the form + `let x := y` after a simplifier pass we know they are in fact a + partially applied function, we cannot know anything about the result + of a partially applied function. + -/ return .top | .erased => return .top @@ -573,6 +579,12 @@ open UnreachableBranches in def Decl.elimDeadBranches (decls : Array Decl) : CompilerM (Array Decl) := do let mut assignments := decls.map fun _ => {} let initialVal i := + /- + Non terminating functions are marked as unsafe, we don't want to run + any analysis on them since we cannot be sure they will ever return + the constructor that we inferred for them. For more information + refer to the docstring of `Decl.safe`. + -/ if decls[i]!.safe then .bot else .top let mut funVals := decls.size.fold (init := .empty) fun i p => p.push (initialVal i) let ctx := { decls }