From e53435979ff8226e895dcde94ca72c47790e35c8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Mar 2022 09:23:43 -0700 Subject: [PATCH] fix: remove hacky `addAutoBoundImplicitsOld` --- src/Lean/Elab/Command.lean | 3 +- src/Lean/Elab/Term.lean | 80 ------------------- tests/lean/interactive/autoBoundIssue.lean | 5 ++ .../autoBoundIssue.lean.expected.out | 6 ++ 4 files changed, 13 insertions(+), 81 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index f39b980d16..7ebb70e26e 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -395,7 +395,8 @@ def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandEla -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command. -- So, we use `Term.resetMessageLog`. Term.resetMessageLog - Term.addAutoBoundImplicitsOld xs fun xs => + let someType := mkSort levelZero + Term.addAutoBoundImplicits' xs someType fun xs _ => Term.withoutAutoBoundImplicit <| elabFn xs @[inline] def catchExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit := fun ctx ref => diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 6403fa00b9..781aa9c63a 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1311,86 +1311,6 @@ partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do def withoutAutoBoundImplicit (k : TermElabM α) : TermElabM α := do withReader (fun ctx => { ctx with autoBoundImplicit := false, autoBoundImplicits := {} }) k -private def mvarsToParamsCore (type : Expr) (init : Array Expr) (k : Array Expr → TermElabM α) : TermElabM α := do - let mvarIds ← getMVars type - if mvarIds.isEmpty then - k init - else - let hugeFuel := 10000000 - go hugeFuel mvarIds.toList init -where - go (fuel : Nat) (mvarIds : List MVarId) (params : Array Expr) : TermElabM α := - match fuel with - | 0 => throwError "too many parameters" - | fuel+1 => - match mvarIds with - | [] => k params - | mvarId :: mvarIds => do - if (← isExprMVarAssigned mvarId) then - go fuel mvarIds params - else - let mvarType := (← getMVarDecl mvarId).type - let mvarIdsNew ← getMVars mvarType - if mvarIdsNew.isEmpty then - withLocalDecl (← mkFreshUserName `a) BinderInfo.implicit mvarType fun newParam => do - /- - HACK: The following assingment is a bit hackish since `newParam` is not in the scope - of the metavariable. We claim this ok because we fully instantiate thes metavariables before executing the - continuation `k`. - Remark: yes, the resulting term is correct, but the `InfoTree` remains littered with invalid terms. - This must be fixed in the future. Otherwise, users will fin `_uniq.????` unknown free variables in the `InfoView`. - -/ - assignExprMVar mvarId newParam - go fuel mvarIds (params.push newParam) - else - go fuel (mvarIdsNew.toList ++ mvarId :: mvarIds) params - -/-- - Helper function for converting metavariables occurring in `type` into new parameters. --/ -def mvarsToParams (type : Expr) (k : Array Expr → Expr → TermElabM α) (init : Array Expr := #[]) : TermElabM α := - mvarsToParamsCore type init fun newParams => do - if newParams.isEmpty then - k newParams type - else - -- If new parameters were created for metavariables, we fully instantiate all metavariables in the current - -- local context befor invoking `k`. See hack above. - let (lctx, mctx) := (← getMCtx).instantiateLCtxMVars (← getLCtx) - setMCtx mctx - withLCtx lctx (← getLocalInstances) (k newParams (← instantiateMVars type)) - -/-- - Return `k (autoBoundImplicits ++ xs)` - This methoid throws an error if a variable in `autoBoundImplicits` depends on some `x` in `xs`. - - Remark: this method corrupts the `InfoTree` when metavariables are converted into fresh free variables. - See "HACK" comment `mvarsToParamsCore.go`. --/ -def addAutoBoundImplicitsOld (xs : Array Expr) (k : Array Expr → TermElabM α) : TermElabM α := do - let autos := (← read).autoBoundImplicits - go autos.toList #[] -where - go (todo : List Expr) (autos : Array Expr) : TermElabM α := do - match todo with - | [] => - for auto in autos do - let localDecl ← getLocalDecl auto.fvarId! - trace[Meta.debug] "auto bound implicit: {localDecl.userName} : {localDecl.type}" - 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}'" - if autos.size != (← read).autoBoundImplicits.size then - -- If new auto locals were created for metavariables, we fully instantiate all metavariables in the current - -- local context befor invoking `k`. See hack above. - let (lctx, mctx) := (← getMCtx).instantiateLCtxMVars (← getLCtx) - setMCtx mctx - withLCtx lctx (← getLocalInstances) do - k (autos ++ xs) - else - k (autos ++ xs) - | 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`. -/ diff --git a/tests/lean/interactive/autoBoundIssue.lean b/tests/lean/interactive/autoBoundIssue.lean index 63a24b4fe3..a2d2377324 100644 --- a/tests/lean/interactive/autoBoundIssue.lean +++ b/tests/lean/interactive/autoBoundIssue.lean @@ -26,3 +26,8 @@ structure Ex where --^ $/lean/plainTermGoal boo : HasType k ctx ty → Prop := fun _ => True --^ $/lean/plainTermGoal + +variable (x : HasType k ctx ty) + --^ $/lean/plainTermGoal + +#check x diff --git a/tests/lean/interactive/autoBoundIssue.lean.expected.out b/tests/lean/interactive/autoBoundIssue.lean.expected.out index 8ec9984994..74097d2644 100644 --- a/tests/lean/interactive/autoBoundIssue.lean.expected.out +++ b/tests/lean/interactive/autoBoundIssue.lean.expected.out @@ -28,3 +28,9 @@ {"start": {"line": 26, "character": 18}, "end": {"line": 26, "character": 21}}, "goal": "aux : {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty : Ty} → HasType k ctx ty\nk : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"} +{"textDocument": {"uri": "file://autoBoundIssue.lean"}, + "position": {"line": 29, "character": 24}} +{"range": + {"start": {"line": 29, "character": 24}, "end": {"line": 29, "character": 27}}, + "goal": + "k : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"}