From 3de97ddc2740eaf5b971a2cb535451d57c8bd67c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Oct 2020 14:04:28 -0700 Subject: [PATCH] feat: run linters in the new frontend --- src/Lean.lean | 1 - src/Lean/Elab/Command.lean | 31 ++++- src/Lean/Elab/DefView.lean | 170 ++++++++++++------------- src/Lean/Linter.lean | 27 ---- src/frontends/lean/definition_cmds.cpp | 9 -- tests/plugin/SnakeLinter.lean | 21 +-- 6 files changed, 126 insertions(+), 133 deletions(-) delete mode 100644 src/Lean/Linter.lean diff --git a/src/Lean.lean b/src/Lean.lean index 653156c4a6..73a7944d92 100644 --- a/src/Lean.lean +++ b/src/Lean.lean @@ -17,7 +17,6 @@ import Lean.Class import Lean.LocalContext import Lean.MetavarContext import Lean.AuxRecursor -import Lean.Linter import Lean.Meta import Lean.Util import Lean.Eval diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index bdcc04970a..5f6fb451a5 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -54,6 +54,15 @@ structure Context := abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε abbrev CommandElabM := CommandElabCoreM Exception abbrev CommandElab := Syntax → CommandElabM Unit +abbrev Linter := Syntax → CommandElabM Unit + +/- Linters should be loadable as plugins, so store in a global IO ref instead of an attribute managed by the + environment (which only contains `import`ed objects). -/ +builtin_initialize lintersRef : IO.Ref (Array Linter) ← IO.mkRef #[] + +def addLinter (l : Linter) : IO Unit := do +let ls ← lintersRef.get +lintersRef.set (ls.push l) instance : MonadEnv CommandElabM := { getEnv := do pure (← get).env, @@ -137,6 +146,18 @@ instance : MonadLog CommandElabM := { modify fun s => { s with messages := s.messages.add msg } } +def runLinters (stx : Syntax) : CommandElabM Unit := do + let linters ← lintersRef.get + unless linters.isEmpty do + for linter in linters do + let savedState ← get + try + linter stx + catch ex => + logException ex + finally + modify fun s => { savedState with messages := s.messages } + protected def getCurrMacroScope : CommandElabM Nat := do pure (← read).currMacroScope protected def getMainModule : CommandElabM Name := do pure (← getEnv).mainModule @@ -194,7 +215,9 @@ instance : MonadRecDepth CommandElabM := { builtin_initialize registerTraceClass `Elab.command partial def elabCommand : Syntax → CommandElabM Unit - | stx => withLogging $ withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with + | stx => withLogging $ withRef stx $ withIncRecDepth $ withFreshMacroScope do + runLinters stx + match stx with | Syntax.node k args => if k == nullKind then -- list of commands => elaborate in order @@ -618,4 +641,8 @@ def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM Expand let currLevelNames ← getLevelNames Lean.Elab.expandDeclId currNamespace currLevelNames declId modifiers -end Lean.Elab.Command +end Elab.Command + +export Elab.Command (Linter addLinter) + +end Lean diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index 468e94381a..c08755e3bc 100644 --- a/src/Lean/Elab/DefView.lean +++ b/src/Lean/Elab/DefView.lean @@ -15,121 +15,121 @@ import Lean.Elab.DeclUtil namespace Lean.Elab inductive DefKind -| «def» | «theorem» | «example» | «opaque» | «abbrev» + | «def» | «theorem» | «example» | «opaque» | «abbrev» def DefKind.isTheorem : DefKind → Bool -| «theorem» => true -| _ => false + | «theorem» => true + | _ => false def DefKind.isDefOrAbbrevOrOpaque : DefKind → Bool -| «def» => true -| «opaque» => true -| «abbrev» => true -| _ => false + | «def» => true + | «opaque» => true + | «abbrev» => true + | _ => false def DefKind.isExample : DefKind → Bool -| «example» => true -| _ => false + | «example» => true + | _ => false structure DefView := -(kind : DefKind) -(ref : Syntax) -(modifiers : Modifiers) -(declId : Syntax) -(binders : Syntax) -(type? : Option Syntax) -(value : Syntax) + (kind : DefKind) + (ref : Syntax) + (modifiers : Modifiers) + (declId : Syntax) + (binders : Syntax) + (type? : Option Syntax) + (value : Syntax) namespace Command open Meta def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView := --- parser! "abbrev " >> declId >> optDeclSig >> declVal -let (binders, type) := expandOptDeclSig (stx.getArg 2) -let modifiers := modifiers.addAttribute { name := `inline } -let modifiers := modifiers.addAttribute { name := `reducible } -{ ref := stx, kind := DefKind.abbrev, modifiers := modifiers, - declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 } + -- parser! "abbrev " >> declId >> optDeclSig >> declVal + let (binders, type) := expandOptDeclSig (stx.getArg 2) + let modifiers := modifiers.addAttribute { name := `inline } + let modifiers := modifiers.addAttribute { name := `reducible } + { ref := stx, kind := DefKind.abbrev, modifiers := modifiers, + declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 } def mkDefViewOfDef (modifiers : Modifiers) (stx : Syntax) : DefView := --- parser! "def " >> declId >> optDeclSig >> declVal -let (binders, type) := expandOptDeclSig (stx.getArg 2) -{ ref := stx, kind := DefKind.def, modifiers := modifiers, - declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 } + -- parser! "def " >> declId >> optDeclSig >> declVal + let (binders, type) := expandOptDeclSig (stx.getArg 2) + { ref := stx, kind := DefKind.def, modifiers := modifiers, + declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 } def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView := --- parser! "theorem " >> declId >> declSig >> declVal -let (binders, type) := expandDeclSig (stx.getArg 2) -{ ref := stx, kind := DefKind.theorem, modifiers := modifiers, - declId := stx.getArg 1, binders := binders, type? := some type, value := stx.getArg 3 } + -- parser! "theorem " >> declId >> declSig >> declVal + let (binders, type) := expandDeclSig (stx.getArg 2) + { ref := stx, kind := DefKind.theorem, modifiers := modifiers, + declId := stx.getArg 1, binders := binders, type? := some type, value := stx.getArg 3 } def mkFreshInstanceName : CommandElabM Name := do -let s ← get -let idx := s.nextInstIdx -modify fun s => { s with nextInstIdx := s.nextInstIdx + 1 } -return Lean.Elab.mkFreshInstanceName s.env idx + let s ← get + let idx := s.nextInstIdx + modify fun s => { s with nextInstIdx := s.nextInstIdx + 1 } + return Lean.Elab.mkFreshInstanceName s.env idx def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do --- parser! "constant " >> declId >> declSig >> optional declValSimple -let (binders, type) := expandDeclSig (stx.getArg 2) -let val ← match (stx.getArg 3).getOptional? with - | some val => pure val - | none => - let val ← `(arbitrary _) - pure $ Syntax.node `Lean.Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ] -return { - ref := stx, kind := DefKind.opaque, modifiers := modifiers, - declId := stx.getArg 1, binders := binders, type? := some type, value := val -} + -- parser! "constant " >> declId >> declSig >> optional declValSimple + let (binders, type) := expandDeclSig (stx.getArg 2) + let val ← match (stx.getArg 3).getOptional? with + | some val => pure val + | none => + let val ← `(arbitrary _) + pure $ Syntax.node `Lean.Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ] + return { + ref := stx, kind := DefKind.opaque, modifiers := modifiers, + declId := stx.getArg 1, binders := binders, type? := some type, value := val + } def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do --- parser! "instance " >> optional declId >> declSig >> declVal -let (binders, type) := expandDeclSig (stx.getArg 2) -let modifiers := modifiers.addAttribute { name := `instance } -let declId ← match (stx.getArg 1).getOptional? with - | some declId => pure declId - | none => - let id ← mkFreshInstanceName - pure $ Syntax.node `Lean.Parser.Command.declId #[mkIdentFrom stx id, mkNullNode] -return { - ref := stx, kind := DefKind.def, modifiers := modifiers, - declId := declId, binders := binders, type? := type, value := stx.getArg 3 -} + -- parser! "instance " >> optional declId >> declSig >> declVal + let (binders, type) := expandDeclSig (stx.getArg 2) + let modifiers := modifiers.addAttribute { name := `instance } + let declId ← match (stx.getArg 1).getOptional? with + | some declId => pure declId + | none => + let id ← mkFreshInstanceName + pure $ Syntax.node `Lean.Parser.Command.declId #[mkIdentFrom stx id, mkNullNode] + return { + ref := stx, kind := DefKind.def, modifiers := modifiers, + declId := declId, binders := binders, type? := type, value := stx.getArg 3 + } def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView := --- parser! "example " >> declSig >> declVal -let (binders, type) := expandDeclSig (stx.getArg 1) -let id := mkIdentFrom stx `_example -let declId := Syntax.node `Lean.Parser.Command.declId #[id, mkNullNode] -{ ref := stx, kind := DefKind.example, modifiers := modifiers, - declId := declId, binders := binders, type? := some type, value := stx.getArg 2 } + -- parser! "example " >> declSig >> declVal + let (binders, type) := expandDeclSig (stx.getArg 1) + let id := mkIdentFrom stx `_example + let declId := Syntax.node `Lean.Parser.Command.declId #[id, mkNullNode] + { ref := stx, kind := DefKind.example, modifiers := modifiers, + declId := declId, binders := binders, type? := some type, value := stx.getArg 2 } def isDefLike (stx : Syntax) : Bool := -let declKind := stx.getKind -declKind == `Lean.Parser.Command.«abbrev» || -declKind == `Lean.Parser.Command.«def» || -declKind == `Lean.Parser.Command.«theorem» || -declKind == `Lean.Parser.Command.«constant» || -declKind == `Lean.Parser.Command.«instance» || -declKind == `Lean.Parser.Command.«example» + let declKind := stx.getKind + declKind == `Lean.Parser.Command.«abbrev» || + declKind == `Lean.Parser.Command.«def» || + declKind == `Lean.Parser.Command.«theorem» || + declKind == `Lean.Parser.Command.«constant» || + declKind == `Lean.Parser.Command.«instance» || + declKind == `Lean.Parser.Command.«example» def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := -let declKind := stx.getKind -if declKind == `Lean.Parser.Command.«abbrev» then - pure $ mkDefViewOfAbbrev modifiers stx -else if declKind == `Lean.Parser.Command.«def» then - pure $ mkDefViewOfDef modifiers stx -else if declKind == `Lean.Parser.Command.«theorem» then - pure $ mkDefViewOfTheorem modifiers stx -else if declKind == `Lean.Parser.Command.«constant» then - mkDefViewOfConstant modifiers stx -else if declKind == `Lean.Parser.Command.«instance» then - mkDefViewOfInstance modifiers stx -else if declKind == `Lean.Parser.Command.«example» then - pure $ mkDefViewOfExample modifiers stx -else - throwError "unexpected kind of definition" + let declKind := stx.getKind + if declKind == `Lean.Parser.Command.«abbrev» then + pure $ mkDefViewOfAbbrev modifiers stx + else if declKind == `Lean.Parser.Command.«def» then + pure $ mkDefViewOfDef modifiers stx + else if declKind == `Lean.Parser.Command.«theorem» then + pure $ mkDefViewOfTheorem modifiers stx + else if declKind == `Lean.Parser.Command.«constant» then + mkDefViewOfConstant modifiers stx + else if declKind == `Lean.Parser.Command.«instance» then + mkDefViewOfInstance modifiers stx + else if declKind == `Lean.Parser.Command.«example» then + pure $ mkDefViewOfExample modifiers stx + else + throwError "unexpected kind of definition" builtin_initialize registerTraceClass `Elab.definition diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean deleted file mode 100644 index fd9d339c9c..0000000000 --- a/src/Lean/Linter.lean +++ /dev/null @@ -1,27 +0,0 @@ -#lang lean4 -/- -Copyright (c) 2019 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Sebastian Ullrich --/ -import Lean.Attributes -import Lean.Syntax -import Lean.Message - -namespace Lean - -def Linter := Environment → Name → Syntax → IO MessageLog - -def mkLintersRef : IO (IO.Ref (Array Linter)) := -IO.mkRef #[] - -/- Linters should be loadable as plugins, so store in a global IO ref instead of an attribute managed by the - environment (which only contains `import`ed objects). -/ -@[builtinInit mkLintersRef, export lean_linters_ref] -constant lintersRef : IO.Ref (Array Linter) - -def addLinter (l : Linter) : IO Unit := do -let ls ← lintersRef.get -lintersRef.set (ls.push l) - -end Lean diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index ab536218b5..bf19a11526 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -475,15 +475,6 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m } new_env = meta.m_attrs.apply_after_comp(new_env, c_real_name); - // temporary code that should soon be removed together with the whole C++ frontend - object_ref r(st_ref_get(lean_linters_ref, io_mk_world())); - lean_assert(io_result_is_ok(r.raw())); - array_ref linters(io_result_get_value(r.raw()), true); - for (object * const & linter : linters) { - object * r2 = apply_4(linter, new_env.to_obj_arg(), local_name_p(fn).to_obj_arg(), lean_box(0) /* Syntax.missing */, io_mk_world()); - consume_io_result(r2); - } - return new_env; }; diff --git a/tests/plugin/SnakeLinter.lean b/tests/plugin/SnakeLinter.lean index 6be20fad34..0cd958d8ae 100644 --- a/tests/plugin/SnakeLinter.lean +++ b/tests/plugin/SnakeLinter.lean @@ -1,15 +1,18 @@ +#lang lean4 import Lean open Lean - def oh_no : Nat := 0 -def snakeLinter : Linter := -fun env n stx => - -- TODO(Sebastian): return actual message with position from syntax tree - if n.toString.contains '_' then throw $ IO.userError "SNAKES!!" - else pure MessageLog.empty +def snakeLinter : Linter := fun stx => do + if stx.getKind == `Lean.Parser.Command.declaration then + let decl := stx[1] + if decl.getKind == `Lean.Parser.Command.def then + let declId := decl[1] + withRef declId do + let declName := declId[0].getId + if declName.eraseMacroScopes.toString.contains '_' then + -- TODO(Sebastian): return actual message with position from syntax tree + throwError "SNAKES!!" -@[init] -def registerSnakeLinter : IO Unit := -addLinter snakeLinter +initialize addLinter snakeLinter