From ac35b543bfa0421a964a683cb648c1bdfceb2003 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 3 Apr 2021 11:16:31 -0700 Subject: [PATCH] feat: add addional `CompletionInfo` --- src/Lean/Elab/App.lean | 2 +- src/Lean/Elab/Command.lean | 9 ++++++-- src/Lean/Elab/InfoTree.lean | 13 +++++++++--- src/Lean/Elab/SetOption.lean | 11 +++++++--- src/Lean/Elab/Tactic/Basic.lean | 3 ++- src/Lean/Elab/Term.lean | 37 +++++++++++++++++++-------------- 6 files changed, 49 insertions(+), 26 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index dda04a2849..29983087c0 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -774,7 +774,7 @@ false, no elaboration function executed by `x` will reset it to private partial def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level) (lvals : List LVal) (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool) (acc : Array (TermElabResult Expr)) : TermElabM (Array (TermElabResult Expr)) := do - let funLVals ← withRef fIdent <| resolveName' fIdent fExplicitUnivs + let funLVals ← withRef fIdent <| resolveName' fIdent fExplicitUnivs expectedType? let overloaded := overloaded || funLVals.length > 1 -- Set `errToSorry` to `false` if `funLVals` > 1. See comment above about the interaction between `errToSorry` and `observing`. withReader (fun ctx => { ctx with errToSorry := funLVals.length == 1 && ctx.errToSorry }) do diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 3af862f9ab..07173b00b4 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -415,8 +415,13 @@ private def popScopes (numScopes : Nat) : CommandElabM Unit := popScopes n throwError "invalid 'end', insufficient scopes" match header? with - | none => unless checkAnonymousScope scopes do throwError "invalid 'end', name is missing" - | some header => unless checkEndHeader header scopes do throwError "invalid 'end', name mismatch" + | none => + unless checkAnonymousScope scopes do + throwError "invalid 'end', name is missing" + | some header => + unless checkEndHeader header scopes do + addCompletionInfo <| CompletionInfo.endSection stx (scopes.map fun scope => scope.header) + throwError "invalid 'end', name mismatch" @[inline] def withNamespace {α} (ns : Name) (elabFn : CommandElabM α) : CommandElabM α := do addNamespace ns diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean index 16c825a940..925edaf271 100644 --- a/src/Lean/Elab/InfoTree.lean +++ b/src/Lean/Elab/InfoTree.lean @@ -40,15 +40,19 @@ structure CommandInfo where inductive CompletionInfo where | dot (termInfo : TermInfo) (field? : Option Syntax) (expectedType? : Option Expr) | id (stx : Syntax) (expectedType? : Option Expr) + | namespaceId (stx : Syntax) | option (stx : Syntax) - | endSection (stx : Syntax) + | endSection (stx : Syntax) (scopeNames : List String) + | tactic (stx : Syntax) (goals : List MVarId) -- TODO `import` def CompletionInfo.stx : CompletionInfo → Syntax | dot i .. => i.stx | id stx .. => stx + | namespaceId stx => stx | option stx => stx - | endSection stx => stx + | endSection stx .. => stx + | tactic stx .. => stx structure FieldInfo where name : Name @@ -112,7 +116,7 @@ class MonadInfoTree (m : Type → Type) where export MonadInfoTree (getInfoState modifyInfoState) -instance (m n) [MonadLift m n] [MonadInfoTree m] : MonadInfoTree n where +instance [MonadLift m n] [MonadInfoTree m] : MonadInfoTree n where getInfoState := liftM (getInfoState : m _) modifyInfoState f := liftM (modifyInfoState f : m _) @@ -224,6 +228,9 @@ def pushInfoLeaf (t : Info) : m Unit := do if (← getInfoState).enabled then pushInfoTree <| InfoTree.node (children := {}) t +def addCompletionInfo (info : CompletionInfo) : m Unit := do + pushInfoLeaf <| Info.ofCompletionInfo info + def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (id := stx.getId) : m Name := do let n ← resolveGlobalConstNoOverload id if (← getInfoState).enabled then diff --git a/src/Lean/Elab/SetOption.lean b/src/Lean/Elab/SetOption.lean index 62f59f5645..1cc3c4089a 100644 --- a/src/Lean/Elab/SetOption.lean +++ b/src/Lean/Elab/SetOption.lean @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.Elab.Log - +import Lean.Elab.InfoTree namespace Lean.Elab variable [Monad m] [MonadOptions m] [MonadExceptOf Exception m] [MonadRef m] -variable [AddErrorMessageContext m] [MonadLiftT (EIO Exception) m] +variable [AddErrorMessageContext m] [MonadLiftT (EIO Exception) m] [MonadInfoTree m] def elabSetOption (id : Syntax) (val : Syntax) : m Options := do let optionName := id.getId.eraseMacroScopes @@ -24,7 +24,12 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do | _ => throwError "unexpected set_option value {val}" where setOption (optionName : Name) (val : DataValue) : m Options := do - let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error (← getRef) ex.toString) (getOptionDecl optionName) + let decl ← + try + IO.toEIO (fun (ex : IO.Error) => Exception.error (← getRef) ex.toString) (getOptionDecl optionName) + catch ex => + addCompletionInfo <| CompletionInfo.option id + throw ex unless decl.defValue.sameCtor val do throwError "type mismatch at set_option" return (← getOptions).insert optionName val diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 4d00dac831..58ce8929e2 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -435,7 +435,8 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit := @[builtinTactic skip] def evalSkip : Tactic := fun stx => pure () -@[builtinTactic unknown] def evalUnknown : Tactic := fun stx => pure () +@[builtinTactic unknown] def evalUnknown : Tactic := fun stx => do + addCompletionInfo <| CompletionInfo.tactic stx (← getGoals) @[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx => do let tactic := stx[1] diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index b493302f91..f2a7f4c0f7 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1076,7 +1076,7 @@ def mkTermInfo (stx : Syntax) (e : Expr) : TermElabM (Sum Info MVarId) := do /-- Store in the `InfoTree` that `e` is a "dot"-completion target. -/ def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr) (field? : Option Syntax := none) : TermElabM Unit := do - pushInfoLeaf <| Info.ofCompletionInfo <| CompletionInfo.dot { expr := e, stx := stx, lctx := (← getLCtx) } (field? := field?) (expectedType? := expectedType?) + addCompletionInfo <| CompletionInfo.dot { expr := e, stx := stx, lctx := (← getLCtx) } (field? := field?) (expectedType? := expectedType?) /-- Main function for elaborating terms. @@ -1335,18 +1335,23 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels : let const ← mkConst constName explicitLevels return (const, projs) :: result -def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do - if let some (e, projs) ← resolveLocalName n then - unless explicitLevels.isEmpty do - throwError "invalid use of explicit universe parameters, '{e}' is a local" - return [(e, projs)] - -- check for section variable capture by a quotation - if let some (e, projs) := preresolved.findSome? fun (n, projs) => (← read).sectionFVars.find? n |>.map (·, projs) then - return [(e, projs)] -- section variables should shadow global decls - if preresolved.isEmpty then - process (← resolveGlobalName n) - else - process preresolved +def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) (expectedType? : Option Expr := none): TermElabM (List (Expr × List String)) := do + try + if let some (e, projs) ← resolveLocalName n then + unless explicitLevels.isEmpty do + throwError "invalid use of explicit universe parameters, '{e}' is a local" + return [(e, projs)] + -- check for section variable capture by a quotation + if let some (e, projs) := preresolved.findSome? fun (n, projs) => (← read).sectionFVars.find? n |>.map (·, projs) then + return [(e, projs)] -- section variables should shadow global decls + if preresolved.isEmpty then + process (← resolveGlobalName n) + else + process preresolved + catch ex => + if preresolved.isEmpty && explicitLevels.isEmpty then + addCompletionInfo <| CompletionInfo.id stx expectedType? + throw ex where process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do if candidates.isEmpty then if (← read).autoBoundImplicit && isValidAutoBoundImplicitName n then @@ -1359,10 +1364,10 @@ where process (candidates : List (Name × List String)) : TermElabM (List (Expr Similar to `resolveName`, but creates identifiers for the main part and each projection with position information derived from `ident`. Example: Assume resolveName `v.head.bla.boo` produces `(v.head, ["bla", "boo"])`, then this method produces `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. -/ -def resolveName' (ident : Syntax) (explicitLevels : List Level) : TermElabM (List (Expr × Syntax × List Syntax)) := do +def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × Syntax × List Syntax)) := do match ident with | Syntax.ident info rawStr n preresolved => - let r ← resolveName n preresolved explicitLevels + let r ← resolveName ident n preresolved explicitLevels expectedType? r.mapM fun (c, fields) => do let (cSstr, fields) := fields.foldr (init := (rawStr, [])) fun field (restSstr, fs) => let fieldSstr := restSstr.takeRightWhile (· ≠ '.') @@ -1392,7 +1397,7 @@ def resolveName' (ident : Syntax) (explicitLevels : List Level) : TermElabM (Lis def resolveId? (stx : Syntax) (kind := "term") : TermElabM (Option Expr) := match stx with | Syntax.ident _ _ val preresolved => do - let rs ← try resolveName val preresolved [] catch _ => pure [] + let rs ← try resolveName stx val preresolved [] catch _ => pure [] let rs := rs.filter fun ⟨f, projs⟩ => projs.isEmpty let fs := rs.map fun (f, _) => f match fs with