From b98fa5641992c1d64ab18bc74f85d4b2f5d84101 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Oct 2020 13:24:46 -0700 Subject: [PATCH] chore: add workaround to control IR size @Kha the new dependent pattern matching compiler assumes the eager inlining at `csimp` will be fixed. Each alternative should produce a joinpoint, but `csimp` is currently inlining all of them. Without this workaround the .C file is 30K lines bigger. --- src/Std/Data/RBMap.lean | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/Std/Data/RBMap.lean b/src/Std/Data/RBMap.lean index d4b37e79df..5a40bee28b 100644 --- a/src/Std/Data/RBMap.lean +++ b/src/Std/Data/RBMap.lean @@ -109,12 +109,14 @@ else ins lt t k v end Insert -def balance₃ : RBNode α β → ∀ k, β k → RBNode α β → RBNode α β -| node red (node red a kx vx b) ky vy c, k, v, d => node red (node black a kx vx b) ky vy (node black c k v d) -| node red a kx vx (node red b ky vy c), k, v, d => node red (node black a kx vx b) ky vy (node black c k v d) -| a, k, v, node red b ky vy (node red c kz vz d) => node red (node black a k v b) ky vy (node black c kz vz d) -| a, k, v, node red (node red b ky vy c) kz vz d => node red (node black a k v b) ky vy (node black c kz vz d) -| l, k, v, r => node black l k v r +def balance₃ (a : RBNode α β) (k : α) (v : β k) (d : RBNode α β) : RBNode α β := +match a with +| node red (node red a kx vx b) ky vy c => node red (node black a kx vx b) ky vy (node black c k v d) +| node red a kx vx (node red b ky vy c) => node red (node black a kx vx b) ky vy (node black c k v d) +| a => match d with + | node red b ky vy (node red c kz vz d) => node red (node black a k v b) ky vy (node black c kz vz d) + | node red (node red b ky vy c) kz vz d => node red (node black a k v b) ky vy (node black c kz vz d) + | _ => node black a k v d def setRed : RBNode α β → RBNode α β | node _ a k v b => node red a k v b