feat: add Expr.inferImplicit

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"]

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