From 0de9a92d4c59eb2b11dfcbfd5abb39afaa4f42de Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 May 2019 06:04:18 -0700
Subject: [PATCH] feat(library/init/lean/compiler/ir/boxing): missing case

---
 library/init/lean/compiler/ir/boxing.lean  | 38 ++++++++++++----------
 library/init/lean/compiler/ir/default.lean |  1 +
 2 files changed, 22 insertions(+), 17 deletions(-)

diff --git a/library/init/lean/compiler/ir/boxing.lean b/library/init/lean/compiler/ir/boxing.lean
index 1cf1e7b02e..10bff0a765 100644
--- a/library/init/lean/compiler/ir/boxing.lean
+++ b/library/init/lean/compiler/ir/boxing.lean
@@ -27,6 +27,23 @@ Assumptions:
 -/
 local attribute [instance] monadInhabited
 
+/- Infer scrutinee type using `case` alternatives.
+   This can be done whenever `alts` does not contain an `Alt.default _` value. -/
+def getScrutineeType (alts : Array Alt) : IRType :=
+let isScalar :=
+   alts.size > 1 && -- Recall that we encode Unit and PUnit using `object`.
+   alts.all (λ alt, match alt with
+    | Alt.ctor c _  := c.isScalar
+    | Alt.default _ := false) in
+match isScalar with
+| false := IRType.object
+| true  :=
+  let n := alts.size in
+  if n < 256 then IRType.uint8
+  else if n < 65536 then IRType.uint16
+  else if n < 4294967296 then IRType.uint32
+  else IRType.object -- in practice this should be unreachable
+
 def eqvTypes (t₁ t₂ : IRType) : Bool :=
 (t₁.isScalar == t₂.isScalar) && (!t₁.isScalar || t₁ == t₂)
 
@@ -135,28 +152,15 @@ match e with
   decl ← getDecl f,
   castArgsIfNeeded ys decl.params $ λ ys,
   castResultIfNeeded x ty (Expr.fap f ys) decl.resultType b
+| Expr.pap f ys := do
+  decl ← getDecl f,
+  boxArgsIfNeeded ys $ λ ys, pure $ FnBody.vdecl x ty (Expr.pap f ys) b
 | Expr.ap f ys :=
   boxArgsIfNeeded ys $ λ ys,
   unboxResultIfNeeded x ty (Expr.ap f ys) b
-| _  :=
-   -- TODO(Leo)
+| other :=
   pure $ FnBody.vdecl x ty e b
 
-def getScrutineeType (alts : Array Alt) : IRType :=
-let isScalar :=
-   alts.size > 1 && -- Recall that we encode Unit and PUnit using `object`.
-   alts.all (λ alt, match alt with
-    | Alt.ctor c _  := c.isScalar
-    | Alt.default _ := false) in
-match isScalar with
-| false := IRType.object
-| true  :=
-  let n := alts.size in
-  if n < 256 then IRType.uint8
-  else if n < 65536 then IRType.uint16
-  else if n < 4294967296 then IRType.uint32
-  else IRType.object -- in practice this should be unreachable
-
 partial def visitFnBody : FnBody → M FnBody
 | (FnBody.vdecl x t v b)     := do
   b ← withVDecl x t v (visitFnBody b),
diff --git a/library/init/lean/compiler/ir/default.lean b/library/init/lean/compiler/ir/default.lean
index ac9263ec47..7127b959fe 100644
--- a/library/init/lean/compiler/ir/default.lean
+++ b/library/init/lean/compiler/ir/default.lean
@@ -12,6 +12,7 @@ import init.lean.compiler.ir.simpcase
 import init.lean.compiler.ir.resetreuse
 import init.lean.compiler.ir.normids
 import init.lean.compiler.ir.checker
+import init.lean.compiler.ir.boxing
 
 namespace Lean
 namespace IR