From 8da79fdfbef419cfc9d098e7833c7f9a8c8301ab Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 11 Oct 2024 07:55:26 +0200 Subject: [PATCH] fix: improved tracing and fix anonymous ctors --- .../SubVerso/Highlighting/Code.lean | 58 +++++++++++++++++-- .../SubVerso/Highlighting/Highlighted.lean | 2 + 2 files changed, 56 insertions(+), 4 deletions(-) diff --git a/src/highlighting/SubVerso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean index 000088a..a284529 100644 --- a/src/highlighting/SubVerso/Highlighting/Code.lean +++ b/src/highlighting/SubVerso/Highlighting/Code.lean @@ -25,6 +25,7 @@ partial def Token.Kind.priority : Token.Kind → Nat | .var .. => 2 | .str .. => 3 | .const .. => 5 + | .anonCtor .. => 6 | .option .. => 4 | .sort => 4 | .keyword _ _ _ => 3 @@ -220,6 +221,20 @@ def identKind [Monad m] [MonadLiftT IO m] [MonadFileMap m] [MonadEnv m] [MonadMC pure kind +def anonCtorKind [Monad m] [MonadLiftT IO m] [MonadFileMap m] [MonadEnv m] [MonadMCtx m] + (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (trees : PersistentArray InfoTree) (stx : Syntax) + : m (Option Token.Kind) := do + let mut kind : Token.Kind := .unknown + for t in trees do + for (ci, info) in infoForSyntax t stx do + if let some seen ← infoKind ids ci info then + if seen.priority > kind.priority then kind := seen + else continue + return match kind with + | .const n sig doc? => some <| .anonCtor n sig doc? + | .anonCtor .. => some kind + | _ => none + def infoExists [Monad m] [MonadLiftT IO m] (trees : PersistentArray InfoTree) (stx : Syntax) : m Bool := do for t in trees do for _ in infoForSyntax t stx do @@ -710,6 +725,7 @@ partial def highlight' tactics := false match stx with | `($e.%$tk$field:ident) => + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Highlighting projection {e} {tk} {field}") do highlight' ids trees e tactics if let some ⟨pos, endPos⟩ := tk.getRange? then emitToken tk.getHeadInfo <| .mk .unknown <| (← getFileMap).source.extract pos endPos @@ -724,26 +740,40 @@ partial def highlight' -- identifier (e.g. in `have`) and the user didn't write it. pure () | stx@(.ident i _ x _) => + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Identifier {x}") do match x.eraseMacroScopes with | .str (.str _ _) _ => match stx.identComponents (nFields? := some 1) with | [y, field] => + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Perhaps a field? {y} {field}") do if (← infoExists trees field) then + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Yes, a field!") do highlight' ids trees y tactics emitToken' <| fakeToken .unknown "." highlight' ids trees field tactics else - emitToken i ⟨← identKind ids trees ⟨stx⟩, x.toString⟩ - | _ => emitToken i ⟨← identKind ids trees ⟨stx⟩, x.toString⟩ - | _ => emitToken i ⟨← identKind ids trees ⟨stx⟩, x.toString⟩ + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Not a field.") do + let k ← identKind ids trees ⟨stx⟩ + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Identifier token for {stx} is {repr k}") do + emitToken i ⟨k, x.toString⟩ + | _ => + let k ← identKind ids trees ⟨stx⟩ + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Identifier token for {stx} is {repr k}") do + emitToken i ⟨k, x.toString⟩ + | _ => + let k ← identKind ids trees ⟨stx⟩ + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Identifier token for {stx} is {repr k}") do + emitToken i ⟨k, x.toString⟩ | stx@(.atom i x) => + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Keyword while looking at {lookingAt}") do let docs ← match lookingAt with | none => pure none | some (n, _) => findDocString? (← getEnv) n let name := lookingAt.map (·.1) let occ := lookingAt.map fun (n, pos) => s!"{n}-{pos}" if let .sort ← identKind ids trees ⟨stx⟩ then - emitToken i ⟨.sort, x⟩ + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Sort") do + emitToken i ⟨.sort, x⟩ return else emitToken i <| (⟨ ·, x⟩) <| @@ -759,17 +789,20 @@ partial def highlight' else .unknown | _ => .unknown | .node _ `str #[.atom i string] => + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"String") do if let some s := Syntax.decodeStrLit string then emitToken i ⟨.str s, string⟩ else emitToken i ⟨.unknown, string⟩ | .node _ ``Lean.Parser.Command.docComment #[.atom i1 opener, .atom i2 body] => + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Doc comment") do if let .original leading pos ws _ := i1 then if let .original ws' _ trailing endPos := i2 then emitToken (.original leading pos trailing endPos) ⟨.docComment, opener ++ ws.toString ++ ws'.toString ++ body⟩ return emitString' (opener ++ " " ++ body ++ "\n") | .node _ ``Lean.Parser.Term.dotIdent #[dot@(.atom i _), name@(.ident i' _ x _)] => + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Dotted identifier") do match i, i' with | .original leading pos _ _, .original _ _ trailing endPos => let info := .original leading pos trailing endPos @@ -777,7 +810,23 @@ partial def highlight' | _, _ => highlight' ids trees dot tactics highlight' ids trees name tactics + | .node info k@``Lean.Parser.Term.anonymousCtor #[opener@(.atom oi l), children@(.node _ _ contents), closer@(.atom ci r)] => + if let some tk ← anonCtorKind ids trees stx then + emitToken oi ⟨tk, l⟩ + for child in contents do + match child with + | .atom commaInfo "," => + emitToken commaInfo ⟨tk, ","⟩ + | _ => + highlight' ids trees child tactics + emitToken ci ⟨tk, r⟩ + else + let pos := stx.getPos? + highlight' ids trees opener tactics (lookingAt := pos.map (k, ·)) + highlight' ids trees children tactics (lookingAt := pos.map (k, ·)) + highlight' ids trees closer tactics (lookingAt := pos.map (k, ·)) | .node _ `choice alts => + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Choice node with {alts.size} alternatives") do -- Arbitrarily select one of the alternatives found by the parser. Otherwise, quotations of -- let-bindings with antiquotations as the bound variable leads to doubled bound variables, -- because the parser emits a choice node in the quotation. And it's never correct to show @@ -785,6 +834,7 @@ partial def highlight' if h : alts.size > 0 then highlight' ids trees alts[0] tactics | stx@(.node _ k children) => + withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Other node, kind {k}, with {children.size} children") do let pos := stx.getPos? for child in children do highlight' ids trees child tactics (lookingAt := pos.map (k, ·)) diff --git a/src/highlighting/SubVerso/Highlighting/Highlighted.lean b/src/highlighting/SubVerso/Highlighting/Highlighted.lean index 58616db..a6ecbcd 100644 --- a/src/highlighting/SubVerso/Highlighting/Highlighted.lean +++ b/src/highlighting/SubVerso/Highlighting/Highlighted.lean @@ -42,6 +42,7 @@ inductive Token.Kind where | /-- `occurrence` is a unique identifier that unites the various keyword tokens from a given production -/ keyword (name : Option Name) (occurrence : Option String) (docs : Option String) | const (name : Name) (signature : String) (docs : Option String) + | anonCtor (name : Name) (signature : String) (docs : Option String) | var (name : FVarId) (type : String) | str (string : String) | option (name : Name) (declName : Name) (docs : Option String) @@ -56,6 +57,7 @@ instance : Quote Token.Kind where quote | .keyword n occ docs => mkCApp ``keyword #[quote n, quote occ, quote docs] | .const n sig docs => mkCApp ``const #[quote n, quote sig, quote docs] + | .anonCtor n sig docs => mkCApp ``anonCtor #[quote n, quote sig, quote docs] | .option n d docs => mkCApp ``option #[quote n, quote d, quote docs] | .var (.mk n) type => mkCApp ``var #[mkCApp ``FVarId.mk #[quote n], quote type] | .str s => mkCApp ``str #[quote s]