From adf40096fc23140d443c3fb3e63251e9abec2178 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Mar 2020 14:16:20 -0700
Subject: [PATCH] feat: compute `ReducibilityHints`

---
 src/Init/Lean/Elab/Declaration.lean |  2 +-
 src/Init/Lean/Elab/Definition.lean  | 20 ++++++++++++++------
 src/Init/Lean/Util/FoldConsts.lean  | 11 +++++++++++
 3 files changed, 26 insertions(+), 7 deletions(-)

diff --git a/src/Init/Lean/Elab/Declaration.lean b/src/Init/Lean/Elab/Declaration.lean
index abf85a2bc7..52ef36fab7 100644
--- a/src/Init/Lean/Elab/Declaration.lean
+++ b/src/Init/Lean/Elab/Declaration.lean
@@ -33,7 +33,7 @@ let (binders, type) := expandOptDeclSig (stx.getArg 2);
 let modifiers       := modifiers.addAttribute { name := `inline };
 let modifiers       := modifiers.addAttribute { name := `reducible };
 elabDefLike {
-  ref := stx, kind := DefKind.def, modifiers := modifiers,
+  ref := stx, kind := DefKind.abbrev, modifiers := modifiers,
   declId := stx.getArg 1, binders := binders, type? := type, val := stx.getArg 3
 }
 
diff --git a/src/Init/Lean/Elab/Definition.lean b/src/Init/Lean/Elab/Definition.lean
index 1332d6b3a5..111a4b1ab9 100644
--- a/src/Init/Lean/Elab/Definition.lean
+++ b/src/Init/Lean/Elab/Definition.lean
@@ -4,26 +4,28 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
+import Init.ShareCommon
 import Init.Lean.Util.CollectLevelParams
+import Init.Lean.Util.FoldConsts
 import Init.Lean.Util.CollectFVars
 import Init.Lean.Elab.DeclModifiers
 import Init.Lean.Elab.Binders
-import Init.ShareCommon
 
 namespace Lean
 namespace Elab
 namespace Command
 
 inductive DefKind
-| «def» | «theorem» | «example» | «opaque»
+| «def» | «theorem» | «example» | «opaque» | «abbrev»
 
 def DefKind.isTheorem : DefKind → Bool
 | DefKind.theorem => true
 | _               => false
 
-def DefKind.isDefOrOpaque : DefKind → Bool
+def DefKind.isDefOrAbbrevOrOpaque : DefKind → Bool
 | DefKind.def    => true
 | DefKind.opaque => true
+| DefKind.abbrev => true
 | _              => false
 
 def DefKind.isExample : DefKind → Bool
@@ -90,7 +92,7 @@ Term.synthesizeSyntheticMVars false;
 type    ← Term.instantiateMVars ref type;
 val     ← Term.instantiateMVars view.val val;
 if view.kind.isExample then pure none
-else withUsedWhen ref vars xs val type view.kind.isDefOrOpaque $ fun vars => do
+else withUsedWhen ref vars xs val type view.kind.isDefOrAbbrevOrOpaque $ fun vars => do
   type ← Term.mkForall ref xs type;
   type ← Term.mkForall ref vars type;
   val  ← Term.mkLambda ref xs val;
@@ -116,10 +118,16 @@ else withUsedWhen ref vars xs val type view.kind.isDefOrOpaque $ fun vars => do
     pure $ some $ Declaration.thmDecl { name := declName, lparams := levelParams, type := type, value := Task.pure val }
   | DefKind.opaque  =>
     pure $ some $ Declaration.opaqueDecl { name := declName, lparams := levelParams, type := type, value := val, isUnsafe := view.modifiers.isUnsafe }
-  | DefKind.def =>
+  | DefKind.abbrev =>
     pure $ some $ Declaration.defnDecl {
       name := declName, lparams := levelParams, type := type, value := val,
-      hints := ReducibilityHints.regular 0, -- TODO
+      hints := ReducibilityHints.abbrev,
+      isUnsafe := view.modifiers.isUnsafe }
+  | DefKind.def => do
+    env ← Term.getEnv;
+    pure $ some $ Declaration.defnDecl {
+      name := declName, lparams := levelParams, type := type, value := val,
+      hints := ReducibilityHints.regular (getMaxHeight env val + 1),
       isUnsafe := view.modifiers.isUnsafe }
   | _ => unreachable!
 
diff --git a/src/Init/Lean/Util/FoldConsts.lean b/src/Init/Lean/Util/FoldConsts.lean
index 94a281f9ba..d45a9fbf3a 100644
--- a/src/Init/Lean/Util/FoldConsts.lean
+++ b/src/Init/Lean/Util/FoldConsts.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Control.Option
 import Init.Lean.Expr
+import Init.Lean.Environment
 
 namespace Lean
 namespace Expr
@@ -60,4 +61,14 @@ end FoldConstsImpl
 constant foldConsts {α : Type} (e : Expr) (init : α) (f : Name → α → α) : α := init
 
 end Expr
+
+def getMaxHeight (env : Environment) (e : Expr) : UInt32 :=
+e.foldConsts 0 $ fun constName max =>
+  match env.find? constName with
+  | ConstantInfo.defnInfo val =>
+    match val.hints with
+    | ReducibilityHints.regular h => if h > max then h else max
+    | _                           => max
+  | _ => max
+
 end Lean