From 18fce4f4552d1eb97c8d94efdf0a7fcfdc5e0017 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 Jul 2020 08:22:32 -0700
Subject: [PATCH] feat: add `Expr.inferImplicit`

---
 src/Lean/Expr.lean        | 26 ++++++++++++++++++++++++++
 tests/lean/run/meta2.lean | 32 ++++++++++++++++++++++++++++++++
 2 files changed, 58 insertions(+)

diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 9a010c7f43..d8420da3d9 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -551,6 +551,11 @@ def bindingBody! : Expr → Expr
 | lam _ _ b _     => b
 | _               => panic! "binding expected"
 
+def bindingInfo! : Expr → BinderInfo
+| forallE _ _ _ c => c.binderInfo
+| lam _ _ _ c     => c.binderInfo
+| _               => panic! "binding expected"
+
 def letName! : Expr → Name
 | letE n _ _ _ _ => n
 | _              => panic! "let expression expected"
@@ -565,6 +570,11 @@ e.looseBVarRange > 0
 @[extern "lean_expr_has_loose_bvar"]
 constant hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool := arbitrary _
 
+/-- Return true if `e` contains the loose bound variable `bvarIdx` in an explicit parameter, or in the range if `tryRange == true`. -/
+def hasLooseBVarInExplicitDomain : Expr → Nat → Bool → Bool
+| Expr.forallE _ d b c, bvarIdx, tryRange => (c.binderInfo.isExplicit && hasLooseBVar d bvarIdx) || hasLooseBVarInExplicitDomain b (bvarIdx+1) tryRange
+| e, bvarIdx, tryRange                    => tryRange && hasLooseBVar e bvarIdx
+
 /--
   Lower the loose bound variables `>= s` in `e` by `d`.
   That is, a loose bound variable `bvar i`.
@@ -579,6 +589,22 @@ constant lowerLooseBVars (e : @& Expr) (s d : @& Nat) : Expr := arbitrary _
 @[extern "lean_expr_lift_loose_bvars"]
 constant liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr := arbitrary _
 
+/--
+  `inferImplicit e numParams considerRange` updates the first `numParams` parameter binder annotations of the `e` forall type.
+  It marks any parameter with an explicit binder annotation if there is another explicit arguments that depends on it or
+  the resulting type if `considerRange == true`.
+
+  Remark: we use this function to infer the bind annotations of inductive datatype constructors, and structure projections.
+  When the `{}` annotation is used in these commands, we set `considerRange == false`.
+-/
+def inferImplicit : Expr → Nat → Bool → Expr
+| Expr.forallE n d b c, i+1, considerRange =>
+  let b       := inferImplicit b i considerRange;
+  let newInfo := if c.binderInfo.isExplicit && hasLooseBVarInExplicitDomain b 0 considerRange then BinderInfo.implicit else c.binderInfo;
+  mkForall n newInfo d b
+| e, 0, _ => e
+| e, _, _ => e
+
 /-- Instantiate the loose bound variables in `e` using `subst`.
     That is, a loose `Expr.bvar i` is replaced with `subst[i]`. -/
 @[extern "lean_expr_instantiate"]
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index a8193e163b..4c20baabc2 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -649,3 +649,35 @@ withLocalDecl `β type BinderInfo.default $ fun β => do
   pure ()
 
 #eval tst39
+
+
+def tst40 : MetaM Unit := do
+print "----- tst40 -----";
+withLocalDecl `α type BinderInfo.default $ fun α =>
+withLocalDecl `β type BinderInfo.default $ fun β =>
+withLocalDecl `a α    BinderInfo.default $ fun a =>
+withLocalDecl `b β    BinderInfo.default $ fun b =>
+do
+  p ← mkProd α β;
+  t1 ← mkForall #[α, β] p;
+  t2 ← mkForall #[α, β, a, b] p;
+  print t1;
+  print $ toString $ t1.bindingBody!.hasLooseBVarInExplicitDomain 0 false;
+  print $ toString $ t1.bindingBody!.hasLooseBVarInExplicitDomain 0 true;
+  print $ toString $ t2.bindingBody!.hasLooseBVarInExplicitDomain 0 false;
+  print $ t1.inferImplicit 2 false;
+  check $ pure $ ((t1.inferImplicit 2 false).bindingInfo! == BinderInfo.default);
+  check $ pure $ ((t1.inferImplicit 2 false).bindingBody!.bindingInfo! == BinderInfo.default);
+  print $ t1.inferImplicit 2 true;
+  check $ pure $ ((t1.inferImplicit 2 true).bindingInfo! == BinderInfo.implicit);
+  check $ pure $ ((t1.inferImplicit 2 true).bindingBody!.bindingInfo! == BinderInfo.implicit);
+  print t2;
+  print $ t2.inferImplicit 2 false;
+  check $ pure $ ((t2.inferImplicit 2 false).bindingInfo! == BinderInfo.implicit);
+  check $ pure $ ((t2.inferImplicit 2 false).bindingBody!.bindingInfo! == BinderInfo.implicit);
+  print $ t2.inferImplicit 1 false;
+  check $ pure $ ((t2.inferImplicit 1 false).bindingInfo! == BinderInfo.implicit);
+  check $ pure $ ((t2.inferImplicit 1 false).bindingBody!.bindingInfo! == BinderInfo.default);
+  pure ()
+
+#eval tst40