From e48cc8901ecce29e44b2bb20c591947cfec0ad1d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Mar 2022 08:40:57 -0700 Subject: [PATCH] fix: add new `addAutoBoundImplicits` that avoids the hack at `addAutoBoundImplicitsOld` --- src/Lean/Elab/Inductive.lean | 20 +++--- src/Lean/Elab/Term.lean | 68 +++++++++++++++++++ .../fixedIndicesToParams.lean.expected.out | 12 ++-- tests/lean/interactive/autoBoundIssue.lean | 18 +++++ .../autoBoundIssue.lean.expected.out | 12 ++++ 5 files changed, 114 insertions(+), 16 deletions(-) create mode 100644 tests/lean/interactive/autoBoundIssue.lean create mode 100644 tests/lean/interactive/autoBoundIssue.lean.expected.out diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index bb421f8299..f6bd0bf91e 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -76,7 +76,7 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : let u ← mkFreshLevelMVar let type := mkSort u Term.synthesizeSyntheticMVarsNoPostponing - Term.addAutoBoundImplicitsOld params fun params => do + Term.addAutoBoundImplicits' params type fun params type => do pure <| acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view } | some typeStx => let (type, numImplicitIndices) ← Term.withAutoBoundImplicit do @@ -84,9 +84,9 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : unless (← isTypeFormerType type) do throwErrorAt typeStx "invalid inductive type, resultant type is not a sort" Term.synthesizeSyntheticMVarsNoPostponing - Term.addAutoBoundImplicitsOld #[] fun indices => - return (← mkForallFVars indices type, indices.size) - Term.addAutoBoundImplicitsOld params fun params => do + let indices ← Term.addAutoBoundImplicits #[] + return (← mkForallFVars indices type, indices.size) + Term.addAutoBoundImplicits' params type fun params type => do pure <| acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view } elabHeaderAux views (i+1) acc else @@ -219,12 +219,12 @@ private def elabCtors (indFVars : Array Expr) (indFVar : Expr) (params : Array E k type elabCtorType fun type => do Term.synthesizeSyntheticMVarsNoPostponing - Term.addAutoBoundImplicitsOld ctorParams fun ctorParams => do - let type ← mkForallFVars ctorParams type - Term.mvarsToParams type fun extraCtorParams type => do - let type ← mkForallFVars extraCtorParams type - let type ← mkForallFVars params type - return { name := ctorView.declName, type } + let ctorParams ← Term.addAutoBoundImplicits ctorParams + let type ← mkForallFVars ctorParams type + let extraCtorParams ← Term.collectUnassignedMVars type + let type ← mkForallFVars extraCtorParams type + let type ← mkForallFVars params type + return { name := ctorView.declName, type } where checkParamOccs (ctorType : Expr) : MetaM Expr := let visit (e : Expr) : MetaM TransformStep := do diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index d546212edd..2f68017219 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1391,6 +1391,74 @@ where | auto :: todo => mvarsToParamsCore (← inferType auto) (init := autos) (fun autos => go todo (autos.push auto)) +/-- + Collect unassigned metavariables in `type` that are not already in `init`. +-/ +partial def collectUnassignedMVars (type : Expr) (init : Array Expr := #[]) : TermElabM (Array Expr) := do + let mvarIds ← getMVars type + if mvarIds.isEmpty then + return init + else + go mvarIds.toList init +where + go (mvarIds : List MVarId) (result : Array Expr) : TermElabM (Array Expr) := do + match mvarIds with + | [] => return result + | mvarId :: mvarIds => do + if (← isExprMVarAssigned mvarId) then + go mvarIds result + else + let mvarType := (← getMVarDecl mvarId).type + let mvarIdsNew ← getMVars mvarType + if mvarIdsNew.isEmpty then + let mvar := mkMVar mvarId + if result.contains mvar then + go mvarIds result + else + go mvarIds (result.push (mkMVar mvarId)) + else + go (mvarIdsNew.toList ++ mvarId :: mvarIds) result + +/-- + Return `autoBoundImplicits ++ xs` + This methoid throws an error if a variable in `autoBoundImplicits` depends on some `x` in `xs`. + The `autoBoundImplicits` may contain free variables created by the auto-implicit feature, and unassigned free variables. + It avoids the hack used at `autoBoundImplicitsOld`. + + Remark: we cannot simply replace every occurrence of `addAutoBoundImplicitsOld` with this one because a particular + use-case may not be able to handle the metavariables in the array being given to `k`. +-/ +def addAutoBoundImplicits (xs : Array Expr) : TermElabM (Array Expr) := do + let autos := (← read).autoBoundImplicits + go autos.toList #[] +where + go (todo : List Expr) (autos : Array Expr) : TermElabM (Array Expr) := do + match todo with + | [] => + for auto in autos do + if auto.isFVar then + let localDecl ← getLocalDecl auto.fvarId! + for x in xs do + if (← getMCtx).localDeclDependsOn localDecl x.fvarId! then + throwError "invalid auto implicit argument '{auto}', it depends on explicitly provided argument '{x}'" + return autos ++ xs + | auto :: todo => + let autos ← collectUnassignedMVars (← inferType auto) autos + go todo (autos.push auto) + +/-- + Similar to `autoBoundImplicits`, but immediately if the resulting array of expressions contains metavariables, + it immediately use `mkForallFVars` + `forallBoundedTelescope` to convert them into free variables. + The type `type` is modified during the process if type depends on `xs`. + We use this method to simplify the conversion of code using `autoBoundImplicitsOld` to `autoBoundImplicits` +-/ +def addAutoBoundImplicits' (xs : Array Expr) (type : Expr) (k : Array Expr → Expr → TermElabM α) : TermElabM α := do + let xs ← addAutoBoundImplicits xs + if xs.all (·.isFVar) then + k xs type + else + forallBoundedTelescope (← mkForallFVars xs type) xs.size fun xs type => k xs type + def mkAuxName (suffix : Name) : TermElabM Name := do match (← read).declName? with | none => throwError "auxiliary declaration cannot be created when declaration name is not available" diff --git a/tests/lean/fixedIndicesToParams.lean.expected.out b/tests/lean/fixedIndicesToParams.lean.expected.out index 83bb9b06ec..147958af6b 100644 --- a/tests/lean/fixedIndicesToParams.lean.expected.out +++ b/tests/lean/fixedIndicesToParams.lean.expected.out @@ -1,15 +1,15 @@ inductive sublist.{u_1} : {α : Type u_1} → List α → List α → Prop number of parameters: 1 constructors: -sublist.slnil : ∀ {a : Type u_1}, sublist [] [] -sublist.cons : ∀ {a : Type u_1} (l₁ l₂ : List a) (a_1 : a), sublist l₁ l₂ → sublist l₁ (a_1 :: l₂) -sublist.cons2 : ∀ {a : Type u_1} (l₁ l₂ : List a) (a_1 : a), sublist l₁ l₂ → sublist (a_1 :: l₁) (a_1 :: l₂) +sublist.slnil : ∀ {x : Type u_1}, sublist [] [] +sublist.cons : ∀ {x : Type u_1} (l₁ l₂ : List x) (a : x), sublist l₁ l₂ → sublist l₁ (a :: l₂) +sublist.cons2 : ∀ {x : Type u_1} (l₁ l₂ : List x) (a : x), sublist l₁ l₂ → sublist (a :: l₁) (a :: l₂) inductive Foo.{u_1} : {α : Type u_1} → List α → Type u_1 number of parameters: 1 constructors: -Foo.mk₁ : {a : Type u_1} → Foo [] +Foo.mk₁ : {x : Type u_1} → Foo [] Foo.mk₂ : {α : Type u_1} → {as : List α} → (a : α) → Foo as → Foo (a :: as) -inductive Bla.{u_1} : {a : Type u_1} → {as : List a} → Foo as → Type +inductive Bla.{u_1} : {x : Type u_1} → {as : List x} → Foo as → Type number of parameters: 1 constructors: -Bla.mk₁ : {a : Type u_1} → Bla Foo.mk₁ +Bla.mk₁ : {x : Type u_1} → Bla Foo.mk₁ diff --git a/tests/lean/interactive/autoBoundIssue.lean b/tests/lean/interactive/autoBoundIssue.lean new file mode 100644 index 0000000000..693374fccd --- /dev/null +++ b/tests/lean/interactive/autoBoundIssue.lean @@ -0,0 +1,18 @@ +inductive Vector (α : Type u) : Nat → Type u + | nil : Vector α 0 + | cons : α → Vector α n → Vector α (n+1) + +infix:67 " :: " => Vector.cons + +inductive Ty where + | int + | bool + | fn (a r : Ty) + +inductive HasType : Fin n → Vector Ty n → Ty → Type where + | stop : HasType 0 (ty :: ctx) ty + | pop : HasType k ctx ty → HasType k.succ (u :: ctx) ty + --^ $/lean/plainTermGoal + +inductive Foo : HasType k ctx ty → Prop + --^ $/lean/plainTermGoal diff --git a/tests/lean/interactive/autoBoundIssue.lean.expected.out b/tests/lean/interactive/autoBoundIssue.lean.expected.out new file mode 100644 index 0000000000..4a6aff0e46 --- /dev/null +++ b/tests/lean/interactive/autoBoundIssue.lean.expected.out @@ -0,0 +1,12 @@ +{"textDocument": {"uri": "file://autoBoundIssue.lean"}, + "position": {"line": 13, "character": 21}} +{"range": + {"start": {"line": 13, "character": 21}, "end": {"line": 13, "character": 24}}, + "goal": + "HasType : {n : Nat} → Fin n → Vector Ty n → Ty → Type\nk : Fin ?m\nctx : Vector Ty ?m\nty u : Ty\n⊢ Vector Ty ?m"} +{"textDocument": {"uri": "file://autoBoundIssue.lean"}, + "position": {"line": 16, "character": 26}} +{"range": + {"start": {"line": 16, "character": 26}, "end": {"line": 16, "character": 29}}, + "goal": + "k : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"}