feat: add generalizeTelescope

src/Init/Lean/Meta.lean

@@ -20,3 +20,4 @@ import Init.Lean.Meta.Tactic
 import Init.Lean.Meta.Message
 import Init.Lean.Meta.KAbstract
 import Init.Lean.Meta.RecursorInfo
+import Init.Lean.Meta.GeneralizeTelescope

src/Init/Lean/Meta/Exception.lean

@@ -37,6 +37,7 @@ inductive Exception
 | appBuilder           (op : Name) (msg : String) (args : Array Expr) (ctx : ExceptionContext)
 | synthInstance        (inst : Expr) (ctx : ExceptionContext)
 | tactic               (tacticName : Name) (mvarId : MVarId) (msg : MessageData) (ctx : ExceptionContext)
+| generalizeTelescope  (es : Array Expr) (ctx : ExceptionContext)
 | kernel               (ex : KernelException) (opts : Options)
 | bug                  (b : Bug) (ctx : ExceptionContext)
 | other                (msg : String)
@@ -65,6 +66,7 @@ def toStr : Exception → String
 | appBuilder _ _ _ _            => "application builder failure"
 | synthInstance _ _             => "type class instance synthesis failed"
 | tactic tacName _ _ _          => "tactic '" ++ toString tacName ++ "' failed"
+| generalizeTelescope _ _       => "generalize telescope"
 | kernel _ _                    => "kernel exception"
 | bug _ _                       => "bug"
 | other s                       => s
@@ -95,6 +97,7 @@ def toTraceMessageData : Exception → MessageData
 | appBuilder op msg args ctx      => mkCtx ctx $ `appBuilder ++ " " ++ op ++ " " ++ args ++ " " ++ msg
 | synthInstance inst ctx          => mkCtx ctx $ `synthInstance ++ " " ++ inst
 | tactic tacName mvarId msg ctx   => mkCtx ctx $ `tacticFailure ++ " " ++ tacName ++ " " ++ msg
+| generalizeTelescope es ctx      => mkCtx ctx $ `generalizeTelescope ++ " " ++ es
 | kernel ex opts                  => ex.toMessageData opts
 | bug _ _                         => "internal bug" -- TODO improve
 | other s                         => s

src/Init/Lean/Meta/GeneralizeTelescope.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta.KAbstract
+
+namespace Lean
+namespace Meta
+namespace GeneralizeTelescope
+
+structure Entry :=
+(expr     : Expr)
+(type     : Expr)
+(modified : Bool)
+
+partial def updateTypes (e newE : Expr) : Array Entry → Nat → MetaM (Array Entry)
+| entries, i =>
+  if h : i < entries.size then
+    let entry := entries.get ⟨i, h⟩;
+    match entry with
+    | ⟨_, type, _⟩ => do
+      typeAbst ← kabstract type e;
+      if typeAbst.hasLooseBVars then do
+        let typeNew := typeAbst.instantiate1 newE;
+        unlessM (isTypeCorrect typeNew) $
+          throwEx $ Exception.generalizeTelescope (entries.map Entry.expr);
+        let entries := entries.set ⟨i, h⟩ { type := typeNew, modified := true, .. entry };
+        updateTypes entries (i+1)
+      else
+        updateTypes entries (i+1)
+  else
+    pure entries
+
+partial def generalizeTelescopeAux {α} (prefixForNewVars : Name) (k : Array FVarId → MetaM α) : Array Entry → Nat → Nat → Array FVarId → MetaM α
+| es, i, nextVarIdx, fvarIds =>
+  if h : i < es.size then
+    let replace (e : Expr) (type : Expr) : MetaM α := do {
+      let userName := prefixForNewVars.appendIndexAfter nextVarIdx;
+      withLocalDecl userName type BinderInfo.default $ fun x => do
+        es ← updateTypes e x es (i+1);
+        generalizeTelescopeAux es (i+1) (nextVarIdx+1) (fvarIds.push x.fvarId!)
+    };
+    match es.get ⟨i, h⟩ with
+    | ⟨e@(Expr.fvar fvarId _), type, false⟩ => do
+      localDecl ← getLocalDecl fvarId;
+      match localDecl with
+      | LocalDecl.cdecl _ _ _ _ _ => generalizeTelescopeAux es (i+1) nextVarIdx (fvarIds.push fvarId)
+      | LocalDecl.ldecl _ _ _ _ _ => replace e type
+    | ⟨e, type, _⟩ => replace e type
+  else
+    k fvarIds
+
+end GeneralizeTelescope
+
+open GeneralizeTelescope
+
+/--
+  Given expressions `es := #[e_1, e_2, ..., e_n]`, execute `k` with the
+  free variables `(x_1 : A_1) (x_2 : A_2 [x_1]) ... (x_n : A_n [x_1, ... x_{n-1}])`.
+  Moreover,
+  - type of `e_1` is definitionally equal to `A_1`,
+  - type of `e_2` is definitionally equal to `A_2[e_1]`.
+  - ...
+  - type of `e_n` is definitionally equal to `A_n[e_1, ..., e_{n-1}]`.
+
+  This method tries to avoid the creation of new free variables. For example, if `e_i` is a
+  free variable `x_i` and it is not a let-declaration variable, and its type does not depend on
+  previous `e_j`s, the method will just use `x_i`.
+
+  The telescope `x_1 ... x_n` can be used to create lambda and forall abstractions.
+  Moreover, for any type correct lambda abstraction `f` constructed using `mkForall #[x_1, ..., x_n] ...`,
+  The application `f e_1 ... e_n` is also type correct.
+
+  The parameter `prefixForNewVars` is used to create new user facing names for the (new) variables `x_i`.
+
+  The `kabstract` method is used to "locate" and abstract forward dependencies.
+  That is, an occurrence of `e_i` in the of `e_j` for `j > i`.
+
+  The method checks whether the abstract types `A_i` are type correct. Here is an example
+  where `generalizeTelescope` fails to create the telescope `x_1 ... x_n`.
+  Assume the local context contains `(n : Nat := 10) (xs : Vec Nat n) (ys : Vec Nat 10) (h : xs = ys)`.
+  Then, assume we invoke `generalizeTelescope` with `es := #[10, xs, ys, h]` and `prefixForNewVars := aux`.
+  A type error is detected when processing `h`'s type. At this point, the method had successfully produced
+  ```
+    (aux_1 : Nat) (xs : Vec Nat n) (aux_2 : Vec Nat aux_1)
+  ```
+  and the type for the new variable abstracting `h` is `xs = aux_2` which is not type correct. -/
+def generalizeTelescope {α} (es : Array Expr) (prefixForNewVars : Name) (k : Array FVarId → MetaM α) : MetaM α := do
+es ← es.mapM $ fun e => do {
+  type ← inferType e;
+  type ← instantiateMVars type;
+  pure { Entry . expr := e, type := type, modified := false }
+};
+generalizeTelescopeAux prefixForNewVars k es 0 1 #[]
+
+end Meta
+end Lean

src/Init/Lean/Meta/Message.lean

@@ -75,6 +75,7 @@ def toMessageData : Exception → MessageData
 | appBuilder op msg args ctx      => mkCtx ctx $ "application builder failure " ++ op ++ " " ++ args ++ " " ++ msg
 | synthInstance inst ctx          => mkCtx ctx $ "failed to synthesize" ++ indentExpr inst
 | tactic tacName mvarId msg ctx   => mkCtx ctx $ "tactic '" ++ tacName ++ "' failed, " ++ msg ++ Format.line ++ MessageData.ofGoal mvarId
+| generalizeTelescope es ctx      => mkCtx ctx $ "failed to create telescope generalizing " ++ es
 | kernel ex opts                  => ex.toMessageData opts
 | bug _ _                         => "internal bug" -- TODO improve
 | other s                         => s