From 552ca3bb11698b02c332ce04b022c157082359e3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 May 2018 12:56:55 -0700
Subject: [PATCH] feat(library/init/lean/ir): allow `uint32` in `case`
 instruction

---
 library/init/lean/ir/extract_cpp.lean | 18 ++++++++++++------
 library/init/lean/ir/type_check.lean  |  2 +-
 2 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean
index 3f545b9317..55af467604 100644
--- a/library/init/lean/ir/extract_cpp.lean
+++ b/library/init/lean/ir/extract_cpp.lean
@@ -98,12 +98,18 @@ def emit_cases : list blockid → nat → extract_m unit
 
 def emit_case : var → list blockid → extract_m unit
 | x [b]     := emit "goto " >> emit_blockid b >> emit_eos
-| x [b₁,b₂] :=
-  do env ← read,
-     if env.ctx.find x = some type.bool
-     then emit "if (" >> emit_var x >> emit ") goto " >> emit_blockid b₂ >> emit "; else goto " >> emit_blockid b₁ >> emit_eos
-     else emit "if (" >> emit_tag x >> emit " == 0) goto " >> emit_blockid b₁ >> emit "; else goto " >> emit_blockid b₂ >> emit_eos
-| x bs      := emit "switch (" >> emit_tag x >> emit ") {" >> emit_cases bs 0 >> emit "}" >> emit_line
+| x [b₁,b₂] := do
+     env ← read,
+     (match env.ctx.find x with
+      | some type.bool   := emit "if (" >> emit_var x >> emit ") goto " >> emit_blockid b₂ >> emit "; else goto " >> emit_blockid b₁
+      | some type.uint32 := emit "if (" >> emit_var x >> emit " == 0) goto " >> emit_blockid b₁ >> emit "; else goto " >> emit_blockid b₂
+      | _                := emit "if (" >> emit_tag x >> emit " == 0) goto " >> emit_blockid b₁ >> emit "; else goto " >> emit_blockid b₂),
+     emit_eos
+| x bs      :=  do
+    env ← read,
+    emit "switch ",
+    paren (if env.ctx.find x = some type.uint32 then emit_var x else emit_tag x),
+    emit " {" >> emit_line >> emit_cases bs 0 >> emit "}" >> emit_line
 
 def emit_terminator (term : terminator) : extract_m unit :=
 term.decorate_error $
diff --git a/library/init/lean/ir/type_check.lean b/library/init/lean/ir/type_check.lean
index b76f613b5c..bcc77a3992 100644
--- a/library/init/lean/ir/type_check.lean
+++ b/library/init/lean/ir/type_check.lean
@@ -210,7 +210,7 @@ def terminator.check (term : terminator) : type_checker_m unit :=
 term.decorate_error $
 match term with
 | (terminator.ret ys)   := do (_, rs) ← read, check_result_types ys rs
-| (terminator.case x _) := do t ← get_type x, unless (t = type.object || t = type.bool) $ throw "variable must be an object or bool"
+| (terminator.case x _) := do t ← get_type x, unless (t = type.object || t = type.bool || t = type.uint32) $ throw "variable must be an object, uint32 or bool"
 | (terminator.jmp _)    := return ()
 
 def block.check (b : block) : type_checker_m unit :=