From c8ab63ea757a520a85528abb36341a46428bf7e3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 10 Aug 2020 09:41:34 -0700
Subject: [PATCH] feat: mark auxiliary eliminators as `[inline]`

---
 src/Lean/Compiler/InlineAttrs.lean     |  3 +++
 src/Lean/Meta/Basic.lean               | 12 ++++++++++++
 src/Lean/Meta/EqnCompiler/DepElim.lean |  1 +
 3 files changed, 16 insertions(+)

diff --git a/src/Lean/Compiler/InlineAttrs.lean b/src/Lean/Compiler/InlineAttrs.lean
index 8dd299d53e..d0f57d6f48 100644
--- a/src/Lean/Compiler/InlineAttrs.lean
+++ b/src/Lean/Compiler/InlineAttrs.lean
@@ -62,5 +62,8 @@ hasInlineAttrAux env InlineAttributeKind.noinline n
 def hasMacroInlineAttribute (env : Environment) (n : Name) : Bool :=
 hasInlineAttrAux env InlineAttributeKind.macroInline n
 
+def setInlineAttribute (env : Environment) (declName : Name) (kind : InlineAttributeKind) : Except String Environment :=
+inlineAttrs.setValue env declName kind
+
 end Compiler
 end Lean
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 3d20c84d73..dd65be1e99 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -10,6 +10,7 @@ import Lean.ReducibilityAttrs
 import Lean.Util.Trace
 import Lean.Util.RecDepth
 import Lean.Util.Closure
+import Lean.Compiler.InlineAttrs
 import Lean.Meta.Exception
 import Lean.Meta.DiscrTreeTypes
 import Lean.Eval
@@ -259,6 +260,11 @@ ctx ← read;
 s ← get;
 throw (Exception.other ref (MessageData.withContext { env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts } msg))
 
+@[inline] def ofExcept {α ε} [HasToString ε] (x : Except ε α) : MetaM α :=
+match x with
+| Except.ok a    => pure a
+| Except.error e => throwOther (toString e)
+
 def throwBug {α} (b : Bug) : MetaM α :=
 throwEx $ Exception.bug b
 
@@ -860,6 +866,12 @@ type ← inferType value;
 let type := type.headBeta;
 mkAuxDefinition name type value
 
+def setInlineAttribute (declName : Name) (kind := Compiler.InlineAttributeKind.inline): MetaM Unit := do
+env ← getEnv;
+match Compiler.setInlineAttribute env declName kind with
+| Except.ok env    => setEnv env
+| Except.error msg => throwOther msg
+
 private partial def instantiateForallAux (ps : Array Expr) : Nat → Expr → MetaM Expr
 | i, e =>
   if h : i < ps.size then do
diff --git a/src/Lean/Meta/EqnCompiler/DepElim.lean b/src/Lean/Meta/EqnCompiler/DepElim.lean
index f79ab56d77..f15a14f27a 100644
--- a/src/Lean/Meta/EqnCompiler/DepElim.lean
+++ b/src/Lean/Meta/EqnCompiler/DepElim.lean
@@ -732,6 +732,7 @@ generalizeTelescope majors.toArray `_d fun majors => do
     val  ← mkLambda args mvar;
     trace! `Meta.EqnCompiler.matchDebug ("eliminator value: " ++ val ++ "\ntype: " ++ type);
     elim ← mkAuxDefinition elimName type val;
+    setInlineAttribute elimName;
     trace! `Meta.EqnCompiler.matchDebug ("eliminator: " ++ elim);
     let unusedAltIdxs : List Nat := lhss.length.fold
       (fun i r => if s.used.contains i then r else i::r)