From 03699cd5ba7801bb94a37f5db5e47ce8bc68f3e6 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 17 Jul 2021 12:40:22 -0700 Subject: [PATCH] feat: uniformly split idents --- src/Lean/Elab/App.lean | 10 ++------ src/Lean/Elab/Term.lean | 25 ++----------------- src/Lean/Syntax.lean | 54 ++++++++++++++++++++++++++++++----------- 3 files changed, 44 insertions(+), 45 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 185c09ea54..00f5231d5b 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -785,15 +785,9 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra f.getArgs.foldlM (fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc) acc else let elabFieldName (e field : Syntax) := do - let newLVals := + let newLVals := field.identComponents.map fun comp => -- We use `none` in `suffix?` since `field` can't be part of a composite name - if field.getId.hasMacroScopes then - -- We assume that names with macro scopes have no meaningful syntax associated - field.getId.eraseMacroScopes.components.map fun n => - LVal.fieldName Syntax.missing (toString n) none e - else - field.identComponents.map fun comp => - LVal.fieldName comp (toString comp.getId) none e + LVal.fieldName comp (toString comp.getId) none e elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc let elabFieldIdx (e idxStx : Syntax) := do let idx := idxStx.isFieldIdx?.get! diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 0b48144ca3..24c41987e0 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1379,29 +1379,8 @@ def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : | Syntax.ident info rawStr n preresolved => 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 (· ≠ '.') - ({ restSstr with stopPos := restSstr.stopPos - (fieldSstr.bsize + 1) }, (field, fieldSstr) :: fs) - let mkIdentFromPos pos rawVal val := - let info := match info with - | SourceInfo.original .. => SourceInfo.original "".toSubstring pos "".toSubstring (pos + rawVal.bsize) - | _ => SourceInfo.synthetic pos (pos + rawVal.bsize) - Syntax.ident info rawVal val [] - let id := match c with - | Expr.const id _ _ => id - | Expr.fvar id _ => id - | _ => unreachable! - let id := mkIdentFromPos (ident.getPos?.getD 0) cSstr id - match info.getPos? with - | none => - return (c, id, fields.map fun (field, _) => mkIdentFrom ident (Name.mkSimple field)) - | some pos => - let mut pos := pos + cSstr.bsize + 1 - let mut newFields := #[] - for (field, fieldSstr) in fields do - newFields := newFields.push <| mkIdentFromPos pos fieldSstr (Name.mkSimple field) - pos := pos + fieldSstr.bsize + 1 - return (c, id, newFields.toList) + let ids := ident.identComponents (nFields? := fields.length) + return (c, ids.head!, ids.tail!) | _ => throwError "identifier expected" def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) := diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index c7075b008c..fd2712e2c8 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -173,22 +173,48 @@ partial def getTailWithPos : Syntax → Option Syntax | _ => none open SourceInfo in -/-- Splits an `ident` into its dot-separated components while preserving source info. -For example, `` `foo.bla.boo `` ↦ `` [`foo, `bla, `boo] ``. -/ -def identComponents : Syntax → List Syntax - | ident info rawStr val _ => - rawStr.splitOn "." |>.map fun ss => +/-- Split an `ident` into its dot-separated components while preserving source info. +Macro scopes are first erased. For example, `` `foo.bla.boo._@._hyg.4 `` ↦ `` [`foo, `bla, `boo] ``. +If `nFields` is set, we take that many fields from the end and keep the remaining components +as one name. For example, `` `foo.bla.boo `` with `(nFields := 1)` ↦ `` [`foo.bla, `boo] ``. -/ +def identComponents (stx : Syntax) (nFields? : Option Nat := none) : List Syntax := + match stx with + | ident (SourceInfo.original lead pos trail _) rawStr val _ => + let val := val.eraseMacroScopes + -- With original info, we assume that `rawStr` represents `val`. + let nameComps := nameComps val nFields? + let rawComps := rawStr.splitOn "." + let rawComps := + if let some nFields := nFields? then + let nPrefix := rawComps.length - nFields + let prefixSz := rawComps.take nPrefix |>.foldl (init := 0) fun acc (ss : Substring) => acc + ss.bsize + 1 + let prefixSz := prefixSz - 1 -- The last component has no dot + rawStr.extract 0 prefixSz :: rawComps.drop nPrefix + else + rawComps + assert! nameComps.length == rawComps.length + nameComps.zip rawComps |>.map fun (id, ss) => let off := ss.startPos - rawStr.startPos - let info := match info with - | original lead pos trail _ => - let lead := if off == 0 then lead else "".toSubstring - let trail := if ss.stopPos == rawStr.stopPos then trail else "".toSubstring - original lead (pos + off) trail (pos + off + ss.bsize) - | synthetic pos _ => - synthetic (pos + off) (pos + off + ss.bsize) - | SourceInfo.none => SourceInfo.none - ident info ss (Name.mkSimple ss.toString) [] + let lead := if off == 0 then lead else "".toSubstring + let trail := if ss.stopPos == rawStr.stopPos then trail else "".toSubstring + let info := original lead (pos + off) trail (pos + off + ss.bsize) + ident info ss id [] + | ident si _ val _ => + let val := val.eraseMacroScopes + /- With non-original info: + - `rawStr` can take all kinds of forms so we only use `val`. + - there is no source extent to offset, so we pass it as-is. -/ + nameComps val nFields? |>.map fun n => ident si n.toString.toSubstring n [] | _ => unreachable! + where + nameComps (n : Name) (nFields? : Option Nat) : List Name := + if let some nFields := nFields? then + let nameComps := n.components + let nPrefix := nameComps.length - nFields + let namePrefix := nameComps.take nPrefix |>.foldl (init := Name.anonymous) fun acc n => acc ++ n + namePrefix :: nameComps.drop nPrefix + else + n.components structure TopDown where firstChoiceOnly : Bool