refactor: use computed fields for Name
This commit is contained in:
Gabriel Ebner
Leonardo de Moura
parent
3176943750
commit
eba400543d
42 changed files with 236 additions and 226 deletions
|
|
@ -99,16 +99,16 @@ namespace Name
|
|||
|
||||
def getRoot : Name → Name
|
||||
| anonymous => anonymous
|
||||
| n@(str anonymous _ _) => n
|
||||
| n@(num anonymous _ _) => n
|
||||
| str n _ _ => getRoot n
|
||||
| num n _ _ => getRoot n
|
||||
| n@(str anonymous _) => n
|
||||
| n@(num anonymous _) => n
|
||||
| str n _ => getRoot n
|
||||
| num n _ => getRoot n
|
||||
|
||||
@[export lean_is_inaccessible_user_name]
|
||||
def isInaccessibleUserName : Name → Bool
|
||||
| Name.str _ s _ => s.contains '✝' || s == "_inaccessible"
|
||||
| Name.num p _ _ => isInaccessibleUserName p
|
||||
| _ => false
|
||||
| Name.str _ s => s.contains '✝' || s == "_inaccessible"
|
||||
| Name.num p _ => isInaccessibleUserName p
|
||||
| _ => false
|
||||
|
||||
def escapePart (s : String) : Option String :=
|
||||
if s.length > 0 && isIdFirst (s.get 0) && (s.toSubstring.drop 1).all isIdRest then s
|
||||
|
|
@ -118,11 +118,11 @@ def escapePart (s : String) : Option String :=
|
|||
-- NOTE: does not roundtrip even with `escape = true` if name is anonymous or contains numeric part or `idEndEscape`
|
||||
variable (sep : String) (escape : Bool)
|
||||
def toStringWithSep : Name → String
|
||||
| anonymous => "[anonymous]"
|
||||
| str anonymous s _ => maybeEscape s
|
||||
| num anonymous v _ => toString v
|
||||
| str n s _ => toStringWithSep n ++ sep ++ maybeEscape s
|
||||
| num n v _ => toStringWithSep n ++ sep ++ Nat.repr v
|
||||
| anonymous => "[anonymous]"
|
||||
| str anonymous s => maybeEscape s
|
||||
| num anonymous v => toString v
|
||||
| str n s => toStringWithSep n ++ sep ++ maybeEscape s
|
||||
| num n v => toStringWithSep n ++ sep ++ Nat.repr v
|
||||
where
|
||||
maybeEscape s := if escape then escapePart s |>.getD s else s
|
||||
|
||||
|
|
@ -131,7 +131,7 @@ protected def toString (n : Name) (escape := true) : String :=
|
|||
toStringWithSep "." (escape && !n.isInaccessibleUserName && !n.hasMacroScopes && !maybePseudoSyntax) n
|
||||
where
|
||||
maybePseudoSyntax :=
|
||||
if let Name.str _ s _ := n.getRoot then
|
||||
if let .str _ s := n.getRoot then
|
||||
-- could be pseudo-syntax for loose bvar or universe mvar, output as is
|
||||
"#".isPrefixOf s || "?".isPrefixOf s
|
||||
else
|
||||
|
|
@ -148,8 +148,8 @@ private def hasNum : Name → Bool
|
|||
protected def reprPrec (n : Name) (prec : Nat) : Std.Format :=
|
||||
match n with
|
||||
| anonymous => Std.Format.text "Lean.Name.anonymous"
|
||||
| num p i _ => Repr.addAppParen ("Lean.Name.mkNum " ++ Name.reprPrec p max_prec ++ " " ++ repr i) prec
|
||||
| str p s _ =>
|
||||
| num p i => Repr.addAppParen ("Lean.Name.mkNum " ++ Name.reprPrec p max_prec ++ " " ++ repr i) prec
|
||||
| str p s =>
|
||||
if p.hasNum then
|
||||
Repr.addAppParen ("Lean.Name.mkStr " ++ Name.reprPrec p max_prec ++ " " ++ repr s) prec
|
||||
else
|
||||
|
|
@ -161,23 +161,23 @@ instance : Repr Name where
|
|||
deriving instance Repr for Syntax
|
||||
|
||||
def capitalize : Name → Name
|
||||
| Name.str p s _ => Name.mkStr p s.capitalize
|
||||
| n => n
|
||||
| .str p s => .str p s.capitalize
|
||||
| n => n
|
||||
|
||||
def replacePrefix : Name → Name → Name → Name
|
||||
| anonymous, anonymous, newP => newP
|
||||
| anonymous, _, _ => anonymous
|
||||
| n@(str p s _), queryP, newP => if n == queryP then newP else Name.mkStr (p.replacePrefix queryP newP) s
|
||||
| n@(num p s _), queryP, newP => if n == queryP then newP else Name.mkNum (p.replacePrefix queryP newP) s
|
||||
| anonymous, anonymous, newP => newP
|
||||
| anonymous, _, _ => anonymous
|
||||
| n@(str p s), queryP, newP => if n == queryP then newP else Name.mkStr (p.replacePrefix queryP newP) s
|
||||
| n@(num p s), queryP, newP => if n == queryP then newP else Name.mkNum (p.replacePrefix queryP newP) s
|
||||
|
||||
/--
|
||||
`eraseSuffix? n s` return `n'` if `n` is of the form `n == n' ++ s`.
|
||||
-/
|
||||
def eraseSuffix? : Name → Name → Option Name
|
||||
| n, anonymous => some n
|
||||
| str p s _, str p' s' _ => if s == s' then eraseSuffix? p p' else none
|
||||
| num p s _, num p' s' _ => if s == s' then eraseSuffix? p p' else none
|
||||
| _, _ => none
|
||||
| n, anonymous => some n
|
||||
| str p s, str p' s' => if s == s' then eraseSuffix? p p' else none
|
||||
| num p s, num p' s' => if s == s' then eraseSuffix? p p' else none
|
||||
| _, _ => none
|
||||
|
||||
/-- Remove macros scopes, apply `f`, and put them back -/
|
||||
@[inline] def modifyBase (n : Name) (f : Name → Name) : Name :=
|
||||
|
|
@ -190,21 +190,32 @@ def eraseSuffix? : Name → Name → Option Name
|
|||
@[export lean_name_append_after]
|
||||
def appendAfter (n : Name) (suffix : String) : Name :=
|
||||
n.modifyBase fun
|
||||
| str p s _ => Name.mkStr p (s ++ suffix)
|
||||
| n => Name.mkStr n suffix
|
||||
| str p s => Name.mkStr p (s ++ suffix)
|
||||
| n => Name.mkStr n suffix
|
||||
|
||||
@[export lean_name_append_index_after]
|
||||
def appendIndexAfter (n : Name) (idx : Nat) : Name :=
|
||||
n.modifyBase fun
|
||||
| str p s _ => Name.mkStr p (s ++ "_" ++ toString idx)
|
||||
| n => Name.mkStr n ("_" ++ toString idx)
|
||||
| str p s => Name.mkStr p (s ++ "_" ++ toString idx)
|
||||
| n => Name.mkStr n ("_" ++ toString idx)
|
||||
|
||||
@[export lean_name_append_before]
|
||||
def appendBefore (n : Name) (pre : String) : Name :=
|
||||
n.modifyBase fun
|
||||
| anonymous => Name.mkStr anonymous pre
|
||||
| str p s _ => Name.mkStr p (pre ++ s)
|
||||
| num p n _ => Name.mkNum (Name.mkStr p pre) n
|
||||
| str p s => Name.mkStr p (pre ++ s)
|
||||
| num p n => Name.mkNum (Name.mkStr p pre) n
|
||||
|
||||
protected theorem beq_iff_eq {m n : Name} : m == n ↔ m = n := by
|
||||
show m.beq n ↔ _
|
||||
induction m generalizing n <;> cases n <;> simp_all [Name.beq, And.comm]
|
||||
|
||||
instance : LawfulBEq Name where
|
||||
eq_of_beq := Name.beq_iff_eq.1
|
||||
rfl := Name.beq_iff_eq.2 rfl
|
||||
|
||||
instance : DecidableEq Name :=
|
||||
fun a b => if h : a == b then .isTrue (by simp_all) else .isFalse (by simp_all)
|
||||
|
||||
end Name
|
||||
|
||||
|
|
@ -920,15 +931,15 @@ instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[qu
|
|||
-- in contrast to `Name.toString`, we can, and want to be, precise here
|
||||
private def getEscapedNameParts? (acc : List String) : Name → Option (List String)
|
||||
| Name.anonymous => if acc.isEmpty then none else some acc
|
||||
| Name.str n s _ => do
|
||||
| Name.str n s => do
|
||||
let s ← Name.escapePart s
|
||||
getEscapedNameParts? (s::acc) n
|
||||
| Name.num _ _ _ => none
|
||||
| Name.num _ _ => none
|
||||
|
||||
def quoteNameMk : Name → Term
|
||||
| Name.anonymous => mkCIdent ``Name.anonymous
|
||||
| Name.str n s _ => Syntax.mkCApp ``Name.mkStr #[quoteNameMk n, quote s]
|
||||
| Name.num n i _ => Syntax.mkCApp ``Name.mkNum #[quoteNameMk n, quote i]
|
||||
| Name.str n s => Syntax.mkCApp ``Name.mkStr #[quoteNameMk n, quote s]
|
||||
| Name.num n i => Syntax.mkCApp ``Name.mkNum #[quoteNameMk n, quote i]
|
||||
|
||||
instance : Quote Name `term where
|
||||
quote n := match getEscapedNameParts? [] n with
|
||||
|
|
|
|||
|
|
@ -1747,47 +1747,47 @@ namespace Lean
|
|||
/- Hierarchical names -/
|
||||
inductive Name where
|
||||
| anonymous : Name
|
||||
| str : Name → String → UInt64 → Name
|
||||
| num : Name → Nat → UInt64 → Name
|
||||
| str : Name → String → Name
|
||||
| num : Name → Nat → Name
|
||||
with
|
||||
@[computedField] hash : Name → UInt64
|
||||
| .anonymous => .ofNatCore 1723 (by decide)
|
||||
| .str p s => mixHash p.hash s.hash
|
||||
| .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide)))
|
||||
|
||||
instance : Inhabited Name where
|
||||
default := Name.anonymous
|
||||
|
||||
protected def Name.hash : Name → UInt64
|
||||
| Name.anonymous => UInt64.ofNatCore 1723 (by decide)
|
||||
| Name.str _ _ h => h
|
||||
| Name.num _ _ h => h
|
||||
|
||||
instance : Hashable Name where
|
||||
hash := Name.hash
|
||||
|
||||
namespace Name
|
||||
|
||||
@[export lean_name_mk_string]
|
||||
def mkStr (p : Name) (s : String) : Name :=
|
||||
Name.str p s (mixHash (hash p) (hash s))
|
||||
abbrev mkStr (p : Name) (s : String) : Name :=
|
||||
Name.str p s
|
||||
|
||||
@[export lean_name_mk_numeral]
|
||||
def mkNum (p : Name) (v : Nat) : Name :=
|
||||
Name.num p v (mixHash (hash p) (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide))))
|
||||
abbrev mkNum (p : Name) (v : Nat) : Name :=
|
||||
Name.num p v
|
||||
|
||||
def mkSimple (s : String) : Name :=
|
||||
abbrev mkSimple (s : String) : Name :=
|
||||
mkStr Name.anonymous s
|
||||
|
||||
@[extern "lean_name_eq"]
|
||||
protected def beq : (@& Name) → (@& Name) → Bool
|
||||
| anonymous, anonymous => true
|
||||
| str p₁ s₁ _, str p₂ s₂ _ => and (BEq.beq s₁ s₂) (Name.beq p₁ p₂)
|
||||
| num p₁ n₁ _, num p₂ n₂ _ => and (BEq.beq n₁ n₂) (Name.beq p₁ p₂)
|
||||
| _, _ => false
|
||||
| anonymous, anonymous => true
|
||||
| str p₁ s₁, str p₂ s₂ => and (BEq.beq s₁ s₂) (Name.beq p₁ p₂)
|
||||
| num p₁ n₁, num p₂ n₂ => and (BEq.beq n₁ n₂) (Name.beq p₁ p₂)
|
||||
| _, _ => false
|
||||
|
||||
instance : BEq Name where
|
||||
beq := Name.beq
|
||||
|
||||
protected def append : Name → Name → Name
|
||||
| n, anonymous => n
|
||||
| n, str p s _ => Name.mkStr (Name.append n p) s
|
||||
| n, num p d _ => Name.mkNum (Name.append n p) d
|
||||
| n, str p s => Name.mkStr (Name.append n p) s
|
||||
| n, num p d => Name.mkNum (Name.append n p) d
|
||||
|
||||
instance : Append Name where
|
||||
append := Name.append
|
||||
|
|
@ -2143,16 +2143,16 @@ The delimiter `_hyg` is used just to improve the `hasMacroScopes` performance.
|
|||
-/
|
||||
|
||||
def Name.hasMacroScopes : Name → Bool
|
||||
| str _ s _ => beq s "_hyg"
|
||||
| num p _ _ => hasMacroScopes p
|
||||
| _ => false
|
||||
| str _ s => beq s "_hyg"
|
||||
| num p _ => hasMacroScopes p
|
||||
| _ => false
|
||||
|
||||
private def eraseMacroScopesAux : Name → Name
|
||||
| Name.str p s _ => match beq s "_@" with
|
||||
| .str p s => match beq s "_@" with
|
||||
| true => p
|
||||
| false => eraseMacroScopesAux p
|
||||
| Name.num p _ _ => eraseMacroScopesAux p
|
||||
| Name.anonymous => Name.anonymous
|
||||
| .num p _ => eraseMacroScopesAux p
|
||||
| .anonymous => Name.anonymous
|
||||
|
||||
@[export lean_erase_macro_scopes]
|
||||
def Name.eraseMacroScopes (n : Name) : Name :=
|
||||
|
|
@ -2161,8 +2161,8 @@ def Name.eraseMacroScopes (n : Name) : Name :=
|
|||
| false => n
|
||||
|
||||
private def simpMacroScopesAux : Name → Name
|
||||
| Name.num p i _ => Name.mkNum (simpMacroScopesAux p) i
|
||||
| n => eraseMacroScopesAux n
|
||||
| .num p i => Name.mkNum (simpMacroScopesAux p) i
|
||||
| n => eraseMacroScopesAux n
|
||||
|
||||
/- Helper function we use to create binder names that do not need to be unique. -/
|
||||
@[export lean_simp_macro_scopes]
|
||||
|
|
@ -2188,30 +2188,30 @@ def MacroScopesView.review (view : MacroScopesView) : Name :=
|
|||
view.scopes.foldl Name.mkNum base
|
||||
|
||||
private def assembleParts : List Name → Name → Name
|
||||
| List.nil, acc => acc
|
||||
| List.cons (Name.str _ s _) ps, acc => assembleParts ps (Name.mkStr acc s)
|
||||
| List.cons (Name.num _ n _) ps, acc => assembleParts ps (Name.mkNum acc n)
|
||||
| _, _ => panic "Error: unreachable @ assembleParts"
|
||||
| .nil, acc => acc
|
||||
| .cons (.str _ s) ps, acc => assembleParts ps (Name.mkStr acc s)
|
||||
| .cons (.num _ n) ps, acc => assembleParts ps (Name.mkNum acc n)
|
||||
| _, _ => panic "Error: unreachable @ assembleParts"
|
||||
|
||||
private def extractImported (scps : List MacroScope) (mainModule : Name) : Name → List Name → MacroScopesView
|
||||
| n@(Name.str p str _), parts =>
|
||||
| n@(Name.str p str), parts =>
|
||||
match beq str "_@" with
|
||||
| true => { name := p, mainModule := mainModule, imported := assembleParts parts Name.anonymous, scopes := scps }
|
||||
| false => extractImported scps mainModule p (List.cons n parts)
|
||||
| n@(Name.num p _ _), parts => extractImported scps mainModule p (List.cons n parts)
|
||||
| n@(Name.num p _), parts => extractImported scps mainModule p (List.cons n parts)
|
||||
| _, _ => panic "Error: unreachable @ extractImported"
|
||||
|
||||
private def extractMainModule (scps : List MacroScope) : Name → List Name → MacroScopesView
|
||||
| n@(Name.str p str _), parts =>
|
||||
| n@(Name.str p str), parts =>
|
||||
match beq str "_@" with
|
||||
| true => { name := p, mainModule := assembleParts parts Name.anonymous, imported := Name.anonymous, scopes := scps }
|
||||
| false => extractMainModule scps p (List.cons n parts)
|
||||
| n@(Name.num _ _ _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
|
||||
| n@(Name.num _ _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
|
||||
| _, _ => panic "Error: unreachable @ extractMainModule"
|
||||
|
||||
private def extractMacroScopesAux : Name → List MacroScope → MacroScopesView
|
||||
| Name.num p scp _, acc => extractMacroScopesAux p (List.cons scp acc)
|
||||
| Name.str p _ _, acc => extractMainModule acc p List.nil -- str must be "_hyg"
|
||||
| Name.num p scp, acc => extractMacroScopesAux p (List.cons scp acc)
|
||||
| Name.str p _ , acc => extractMainModule acc p List.nil -- str must be "_hyg"
|
||||
| _, _ => panic "Error: unreachable @ extractMacroScopesAux"
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -66,17 +66,17 @@ namespace Lean
|
|||
an opaque function for computing the hashcode field. -/
|
||||
protected noncomputable def Name.sizeOf : Name → Nat
|
||||
| anonymous => 1
|
||||
| str p s _ => 1 + Name.sizeOf p + sizeOf s
|
||||
| num p n _ => 1 + Name.sizeOf p + sizeOf n
|
||||
| str p s => 1 + Name.sizeOf p + sizeOf s
|
||||
| num p n => 1 + Name.sizeOf p + sizeOf n
|
||||
|
||||
noncomputable instance : SizeOf Name where
|
||||
sizeOf n := n.sizeOf
|
||||
|
||||
@[simp] theorem Name.anonymous.sizeOf_spec : sizeOf anonymous = 1 :=
|
||||
rfl
|
||||
@[simp] theorem Name.str.sizeOf_spec (p : Name) (s : String) (h : UInt64) : sizeOf (str p s h) = 1 + sizeOf p + sizeOf s :=
|
||||
@[simp] theorem Name.str.sizeOf_spec (p : Name) (s : String) : sizeOf (str p s) = 1 + sizeOf p + sizeOf s :=
|
||||
rfl
|
||||
@[simp] theorem Name.num.sizeOf_spec (p : Name) (n : Nat) (h : UInt64) : sizeOf (num p n h) = 1 + sizeOf p + sizeOf n :=
|
||||
@[simp] theorem Name.num.sizeOf_spec (p : Name) (n : Nat) : sizeOf (num p n) = 1 + sizeOf p + sizeOf n :=
|
||||
rfl
|
||||
|
||||
deriving instance SizeOf for Syntax
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
|
|||
|
||||
def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : Name) : Bool :=
|
||||
match declName with
|
||||
| Name.str _ s _ => s == suffix && isAuxRecursor env declName
|
||||
| .str _ s => s == suffix && isAuxRecursor env declName
|
||||
| _ => false
|
||||
|
||||
def isCasesOnRecursor (env : Environment) (declName : Name) : Bool :=
|
||||
|
|
|
|||
|
|
@ -12,9 +12,9 @@ private def isValidCppId (id : String) : Bool :=
|
|||
first.isAlpha && (id.toSubstring.drop 1).all (fun c => c.isAlpha || c.isDigit || c == '_')
|
||||
|
||||
private def isValidCppName : Name → Bool
|
||||
| Name.str Name.anonymous s _ => isValidCppId s
|
||||
| Name.str p s _ => isValidCppId s && isValidCppName p
|
||||
| _ => false
|
||||
| .str .anonymous s => isValidCppId s
|
||||
| .str p s => isValidCppId s && isValidCppName p
|
||||
| _ => false
|
||||
|
||||
builtin_initialize exportAttr : ParametricAttribute Name ←
|
||||
registerParametricAttribute {
|
||||
|
|
|
|||
|
|
@ -32,9 +32,8 @@ open Std (AssocList)
|
|||
def mkBoxedName (n : Name) : Name :=
|
||||
Name.mkStr n "_boxed"
|
||||
|
||||
def isBoxedName : Name → Bool
|
||||
| Name.str _ "_boxed" _ => true
|
||||
| _ => false
|
||||
def isBoxedName (name : Name) : Bool :=
|
||||
name matches .str _ "_boxed"
|
||||
|
||||
abbrev N := StateM Nat
|
||||
|
||||
|
|
|
|||
|
|
@ -72,9 +72,9 @@ def toCName (n : Name) : M String := do
|
|||
let env ← getEnv;
|
||||
-- TODO: we should support simple export names only
|
||||
match getExportNameFor env n with
|
||||
| some (Name.str Name.anonymous s _) => pure s
|
||||
| some _ => throwInvalidExportName n
|
||||
| none => if n == `main then pure leanMainFn else pure n.mangle
|
||||
| some (.str .anonymous s) => pure s
|
||||
| some _ => throwInvalidExportName n
|
||||
| none => if n == `main then pure leanMainFn else pure n.mangle
|
||||
|
||||
def emitCName (n : Name) : M Unit :=
|
||||
toCName n >>= emit
|
||||
|
|
@ -83,9 +83,9 @@ def toCInitName (n : Name) : M String := do
|
|||
let env ← getEnv;
|
||||
-- TODO: we should support simple export names only
|
||||
match getExportNameFor env n with
|
||||
| some (Name.str Name.anonymous s _) => return "_init_" ++ s
|
||||
| some _ => throwInvalidExportName n
|
||||
| none => pure ("_init_" ++ n.mangle)
|
||||
| some (.str .anonymous s) => return "_init_" ++ s
|
||||
| some _ => throwInvalidExportName n
|
||||
| none => pure ("_init_" ++ n.mangle)
|
||||
|
||||
def emitCInitName (n : Name) : M Unit :=
|
||||
toCInitName n >>= emit
|
||||
|
|
|
|||
|
|
@ -48,12 +48,12 @@ namespace Lean
|
|||
|
||||
private def Name.mangleAux : Name → String
|
||||
| Name.anonymous => ""
|
||||
| Name.str p s _ =>
|
||||
| Name.str p s =>
|
||||
let m := String.mangle s
|
||||
match p with
|
||||
| Name.anonymous => m
|
||||
| p => mangleAux p ++ "_" ++ m
|
||||
| Name.num p n _ => mangleAux p ++ "_" ++ toString n ++ "_"
|
||||
| Name.num p n => mangleAux p ++ "_" ++ toString n ++ "_"
|
||||
|
||||
@[export lean_name_mangle]
|
||||
def Name.mangle (n : Name) (pre : String := "l_") : String :=
|
||||
|
|
|
|||
|
|
@ -65,9 +65,9 @@ def mkEagerLambdaLiftingName (n : Name) (idx : Nat) : Name :=
|
|||
|
||||
@[export lean_is_eager_lambda_lifting_name]
|
||||
def isEagerLambdaLiftingName : Name → Bool
|
||||
| Name.str p s _ => "_elambda".isPrefixOf s || isEagerLambdaLiftingName p
|
||||
| Name.num p _ _ => isEagerLambdaLiftingName p
|
||||
| _ => false
|
||||
| .str p s => "_elambda".isPrefixOf s || isEagerLambdaLiftingName p
|
||||
| .num p _ => isEagerLambdaLiftingName p
|
||||
| _ => false
|
||||
|
||||
/-- Return the name of new definitions in the a given declaration.
|
||||
Here we consider only declarations we generate code for.
|
||||
|
|
@ -97,7 +97,7 @@ def mkUnsafeRecName (declName : Name) : Name :=
|
|||
/-- Return `some _` if the given name was created using `mkUnsafeRecName` -/
|
||||
@[export lean_is_unsafe_rec_name]
|
||||
def isUnsafeRecName? : Name → Option Name
|
||||
| Name.str n "_unsafe_rec" _ => some n
|
||||
| .str n "_unsafe_rec" => some n
|
||||
| _ => none
|
||||
|
||||
end Compiler
|
||||
|
|
|
|||
|
|
@ -18,58 +18,58 @@ namespace Name
|
|||
|
||||
def getPrefix : Name → Name
|
||||
| anonymous => anonymous
|
||||
| str p _ _ => p
|
||||
| num p _ _ => p
|
||||
| str p _ => p
|
||||
| num p _ => p
|
||||
|
||||
def getString! : Name → String
|
||||
| str _ s _ => s
|
||||
| _ => unreachable!
|
||||
| str _ s => s
|
||||
| _ => unreachable!
|
||||
|
||||
def getNumParts : Name → Nat
|
||||
| anonymous => 0
|
||||
| str p _ _ => getNumParts p + 1
|
||||
| num p _ _ => getNumParts p + 1
|
||||
| str p _ => getNumParts p + 1
|
||||
| num p _ => getNumParts p + 1
|
||||
|
||||
def updatePrefix : Name → Name → Name
|
||||
| anonymous, _ => anonymous
|
||||
| str _ s _, newP => Name.mkStr newP s
|
||||
| num _ s _, newP => Name.mkNum newP s
|
||||
| str _ s, newP => Name.mkStr newP s
|
||||
| num _ s, newP => Name.mkNum newP s
|
||||
|
||||
def components' : Name → List Name
|
||||
| anonymous => []
|
||||
| str n s _ => Name.mkStr anonymous s :: components' n
|
||||
| num n v _ => Name.mkNum anonymous v :: components' n
|
||||
| str n s => Name.mkStr anonymous s :: components' n
|
||||
| num n v => Name.mkNum anonymous v :: components' n
|
||||
|
||||
def components (n : Name) : List Name :=
|
||||
n.components'.reverse
|
||||
|
||||
def eqStr : Name → String → Bool
|
||||
| str anonymous s _, s' => s == s'
|
||||
| str anonymous s, s' => s == s'
|
||||
| _, _ => false
|
||||
|
||||
def isPrefixOf : Name → Name → Bool
|
||||
| p, anonymous => p == anonymous
|
||||
| p, n@(num p' _ _) => p == n || isPrefixOf p p'
|
||||
| p, n@(str p' _ _) => p == n || isPrefixOf p p'
|
||||
| p, anonymous => p == anonymous
|
||||
| p, n@(num p' _) => p == n || isPrefixOf p p'
|
||||
| p, n@(str p' _) => p == n || isPrefixOf p p'
|
||||
|
||||
|
||||
def isSuffixOf : Name → Name → Bool
|
||||
| anonymous, _ => true
|
||||
| str p₁ s₁ _, str p₂ s₂ _ => s₁ == s₂ && isSuffixOf p₁ p₂
|
||||
| num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && isSuffixOf p₁ p₂
|
||||
| _, _ => false
|
||||
| anonymous, _ => true
|
||||
| str p₁ s₁, str p₂ s₂ => s₁ == s₂ && isSuffixOf p₁ p₂
|
||||
| num p₁ n₁, num p₂ n₂ => n₁ == n₂ && isSuffixOf p₁ p₂
|
||||
| _, _ => false
|
||||
|
||||
def cmp : Name → Name → Ordering
|
||||
| anonymous, anonymous => Ordering.eq
|
||||
| anonymous, _ => Ordering.lt
|
||||
| _, anonymous => Ordering.gt
|
||||
| num p₁ i₁ _, num p₂ i₂ _ =>
|
||||
| anonymous, anonymous => Ordering.eq
|
||||
| anonymous, _ => Ordering.lt
|
||||
| _, anonymous => Ordering.gt
|
||||
| num p₁ i₁, num p₂ i₂ =>
|
||||
match cmp p₁ p₂ with
|
||||
| Ordering.eq => compare i₁ i₂
|
||||
| ord => ord
|
||||
| num _ _ _, str _ _ _ => Ordering.lt
|
||||
| str _ _ _, num _ _ _ => Ordering.gt
|
||||
| str p₁ n₁ _, str p₂ n₂ _ =>
|
||||
| num _ _, str _ _ => Ordering.lt
|
||||
| str _ _, num _ _ => Ordering.gt
|
||||
| str p₁ n₁, str p₂ n₂ =>
|
||||
match cmp p₁ p₂ with
|
||||
| Ordering.eq => compare n₁ n₂
|
||||
| ord => ord
|
||||
|
|
@ -78,16 +78,16 @@ def lt (x y : Name) : Bool :=
|
|||
cmp x y == Ordering.lt
|
||||
|
||||
def quickCmpAux : Name → Name → Ordering
|
||||
| anonymous, anonymous => Ordering.eq
|
||||
| anonymous, _ => Ordering.lt
|
||||
| _, anonymous => Ordering.gt
|
||||
| num n v _, num n' v' _ =>
|
||||
| anonymous, anonymous => Ordering.eq
|
||||
| anonymous, _ => Ordering.lt
|
||||
| _, anonymous => Ordering.gt
|
||||
| num n v, num n' v' =>
|
||||
match compare v v' with
|
||||
| Ordering.eq => n.quickCmpAux n'
|
||||
| ord => ord
|
||||
| num _ _ _, str _ _ _ => Ordering.lt
|
||||
| str _ _ _, num _ _ _ => Ordering.gt
|
||||
| str n s _, str n' s' _ =>
|
||||
| num _ _, str _ _ => Ordering.lt
|
||||
| str _ _, num _ _ => Ordering.gt
|
||||
| str n s, str n' s' =>
|
||||
match compare s s' with
|
||||
| Ordering.eq => n.quickCmpAux n'
|
||||
| ord => ord
|
||||
|
|
@ -110,15 +110,15 @@ def quickLt (n₁ n₂ : Name) : Bool :=
|
|||
/- The frontend does not allow user declarations to start with `_` in any of its parts.
|
||||
We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
|
||||
def isInternal : Name → Bool
|
||||
| str p s _ => s.get 0 == '_' || isInternal p
|
||||
| num p _ _ => isInternal p
|
||||
| _ => false
|
||||
| str p s => s.get 0 == '_' || isInternal p
|
||||
| num p _ => isInternal p
|
||||
| _ => false
|
||||
|
||||
def isAtomic : Name → Bool
|
||||
| anonymous => true
|
||||
| str anonymous _ _ => true
|
||||
| num anonymous _ _ => true
|
||||
| _ => false
|
||||
| anonymous => true
|
||||
| str anonymous _ => true
|
||||
| num anonymous _ => true
|
||||
| _ => false
|
||||
|
||||
def isAnonymous : Name → Bool
|
||||
| anonymous => true
|
||||
|
|
|
|||
|
|
@ -34,8 +34,8 @@ private def toKey (n : Name) : List NamePart :=
|
|||
loop n []
|
||||
where
|
||||
loop
|
||||
| Name.str p s _, parts => loop p (NamePart.str s :: parts)
|
||||
| Name.num p n _, parts => loop p (NamePart.num n :: parts)
|
||||
| Name.str p s, parts => loop p (NamePart.str s :: parts)
|
||||
| Name.num p n, parts => loop p (NamePart.num n :: parts)
|
||||
| Name.anonymous, parts => parts
|
||||
|
||||
def NameTrie.insert (t : NameTrie β) (n : Name) (b : β) : NameTrie β :=
|
||||
|
|
|
|||
|
|
@ -49,7 +49,7 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
|
|||
let attrName ← if attr.getKind == ``Parser.Attr.simple then
|
||||
pure attr[0].getId.eraseMacroScopes
|
||||
else match attr.getKind with
|
||||
| Name.str _ s _ => pure <| Name.mkSimple s
|
||||
| .str _ s => pure <| Name.mkSimple s
|
||||
| _ => throwErrorAt attr "unknown attribute"
|
||||
unless isAttribute (← getEnv) attrName do
|
||||
throwError "unknown attribute [{attrName}]"
|
||||
|
|
|
|||
|
|
@ -39,12 +39,12 @@ Therefore, we do consider identifier with macro scopes anymore.
|
|||
|
||||
def isValidAutoBoundImplicitName (n : Name) (relaxed : Bool) : Bool :=
|
||||
match n with
|
||||
| Name.str Name.anonymous s _ => s.length > 0 && (relaxed || ((isGreek s.front || s.front.isLower) && isValidAutoBoundSuffix s))
|
||||
| .str .anonymous s => s.length > 0 && (relaxed || ((isGreek s.front || s.front.isLower) && isValidAutoBoundSuffix s))
|
||||
| _ => false
|
||||
|
||||
def isValidAutoBoundLevelName (n : Name) (relaxed : Bool) : Bool :=
|
||||
match n with
|
||||
| Name.str Name.anonymous s _ => s.length > 0 && (relaxed || (s.front.isLower && isValidAutoBoundSuffix s))
|
||||
| .str .anonymous s => s.length > 0 && (relaxed || (s.front.isLower && isValidAutoBoundSuffix s))
|
||||
| _ => false
|
||||
|
||||
end Lean.Elab
|
||||
|
|
|
|||
|
|
@ -30,8 +30,8 @@ private def addScope (isNewNamespace : Bool) (isNoncomputable : Bool) (header :
|
|||
activateScoped newNamespace
|
||||
|
||||
private def addScopes (isNewNamespace : Bool) (isNoncomputable : Bool) : Name → CommandElabM Unit
|
||||
| Name.anonymous => pure ()
|
||||
| Name.str p header _ => do
|
||||
| .anonymous => pure ()
|
||||
| .str p header => do
|
||||
addScopes isNewNamespace isNoncomputable p
|
||||
let currNamespace ← getCurrNamespace
|
||||
addScope isNewNamespace isNoncomputable header (if isNewNamespace then Name.mkStr currNamespace header else currNamespace)
|
||||
|
|
@ -55,9 +55,9 @@ private def checkAnonymousScope : List Scope → Bool
|
|||
| _ => false
|
||||
|
||||
private def checkEndHeader : Name → List Scope → Bool
|
||||
| Name.anonymous, _ => true
|
||||
| Name.str p s _, { header := h, .. } :: scopes => h == s && checkEndHeader p scopes
|
||||
| _, _ => false
|
||||
| .anonymous, _ => true
|
||||
| .str p s, { header := h, .. } :: scopes => h == s && checkEndHeader p scopes
|
||||
| _, _ => false
|
||||
|
||||
@[builtinCommandElab «namespace»] def elabNamespace : CommandElab := fun stx =>
|
||||
match stx with
|
||||
|
|
|
|||
|
|
@ -99,7 +99,7 @@ private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) :
|
|||
let (some declName) ← getDeclName?
|
||||
| throwError "invalid `leading_parser` macro, it must be used in definitions"
|
||||
match extractMacroScopes declName with
|
||||
| { name := Name.str _ s _, .. } =>
|
||||
| { name := .str _ s, .. } =>
|
||||
let kind := quote declName
|
||||
let s := quote s
|
||||
``(withAntiquot (mkAntiquot $s $kind $(quote withAnonymousAntiquot)) (leadingNode $kind $prec $e))
|
||||
|
|
|
|||
|
|
@ -171,7 +171,7 @@ def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name)
|
|||
throwError "atomic identifier expected '{shortName}'"
|
||||
let declName := if isRootName then { view with name := name.replacePrefix `_root_ Name.anonymous }.review else currNamespace ++ shortName
|
||||
if isRootName then
|
||||
let .str p s _ := name | throwError "invalid declaration name '{name}'"
|
||||
let .str p s := name | throwError "invalid declaration name '{name}'"
|
||||
shortName := Name.mkSimple s
|
||||
currNamespace := p.replacePrefix `_root_ Name.anonymous
|
||||
checkIfShadowingStructureField declName
|
||||
|
|
@ -179,7 +179,7 @@ def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name)
|
|||
match modifiers.visibility with
|
||||
| Visibility.protected =>
|
||||
match currNamespace with
|
||||
| Name.str _ s _ => pure (declName, Name.mkSimple s ++ shortName)
|
||||
| .str _ s => pure (declName, Name.mkSimple s ++ shortName)
|
||||
| _ => throwError "protected declarations must be in a namespace"
|
||||
| _ => pure (declName, shortName)
|
||||
|
||||
|
|
|
|||
|
|
@ -58,8 +58,8 @@ def mkFreshInstanceName (env : Environment) (nextIdx : Nat) : Name :=
|
|||
|
||||
def isFreshInstanceName (name : Name) : Bool :=
|
||||
match name with
|
||||
| Name.str _ s _ => "_instance".isPrefixOf s
|
||||
| _ => false
|
||||
| .str _ s => "_instance".isPrefixOf s
|
||||
| _ => false
|
||||
|
||||
/--
|
||||
Sort the given list of `usedParams` using the following order:
|
||||
|
|
|
|||
|
|
@ -17,12 +17,12 @@ open TSyntax.Compat
|
|||
|
||||
private def ensureValidNamespace (name : Name) : MacroM Unit := do
|
||||
match name with
|
||||
| Name.str p s _ =>
|
||||
| .str p s =>
|
||||
if s == "_root_" then
|
||||
Macro.throwError s!"invalid namespace '{name}', '_root_' is a reserved namespace"
|
||||
ensureValidNamespace p
|
||||
| Name.num _ .. => Macro.throwError s!"invalid namespace '{name}', it must not contain numeric parts"
|
||||
| Name.anonymous => return ()
|
||||
| .num .. => Macro.throwError s!"invalid namespace '{name}', it must not contain numeric parts"
|
||||
| .anonymous => return ()
|
||||
|
||||
/-- Auxiliary function for `expandDeclNamespace?` -/
|
||||
private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × Syntax)) := do
|
||||
|
|
@ -32,8 +32,8 @@ private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × S
|
|||
return none
|
||||
let scpView := extractMacroScopes id
|
||||
match scpView.name with
|
||||
| Name.str Name.anonymous _ _ => return none
|
||||
| Name.str pre s _ =>
|
||||
| .str .anonymous _ => return none
|
||||
| .str pre s =>
|
||||
ensureValidNamespace pre
|
||||
let nameNew := { scpView with name := Name.mkSimple s }.review
|
||||
-- preserve "original" info, if any, so that hover etc. on the namespaced
|
||||
|
|
|
|||
|
|
@ -91,7 +91,7 @@ def mkInstanceName (binders : Array Syntax) (type : Syntax) : CommandElabM Name
|
|||
else if e.isSort then ref.modify (· ++ "Sort")
|
||||
else if e.isConst then
|
||||
match e.constName!.eraseMacroScopes with
|
||||
| Name.str _ str _ =>
|
||||
| .str _ str =>
|
||||
if str.front.isLower then
|
||||
ref.modify (· ++ str.capitalize)
|
||||
else
|
||||
|
|
|
|||
|
|
@ -73,8 +73,8 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
|
|||
let mut auxFunNames := #[]
|
||||
for typeName in indVal.all do
|
||||
match typeName.eraseMacroScopes with
|
||||
| Name.str _ t _ => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t)
|
||||
| _ => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn)
|
||||
| .str _ t => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t)
|
||||
| _ => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn)
|
||||
trace[Elab.Deriving.beq] "{auxFunNames}"
|
||||
let usePartial := indVal.isNested || typeInfos.size > 1
|
||||
return {
|
||||
|
|
|
|||
|
|
@ -60,7 +60,7 @@ def resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name
|
|||
-- decode macro scopes from name before recursion
|
||||
let extractionResult := extractMacroScopes id
|
||||
let rec loop : Name → List String → List (Name × List String)
|
||||
| id@(Name.str p s _), projs =>
|
||||
| id@(.str p s), projs =>
|
||||
-- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
|
||||
let id := { extractionResult with name := id }.review
|
||||
match sectionVars.find? id with
|
||||
|
|
@ -179,7 +179,7 @@ def getQuotKind (stx : Syntax) : TermElabM SyntaxNodeKind := do
|
|||
| ``Parser.Term.attr.quot => pure `attr
|
||||
| ``Parser.Term.prio.quot => pure `prio
|
||||
| ``Parser.Term.doElem.quot => pure `doElem
|
||||
| Name.str kind "quot" _ => return kind
|
||||
| .str kind "quot" => return kind
|
||||
| ``dynamicQuot =>
|
||||
match (← resolveGlobalConst stx[1]) with
|
||||
| [parser] => pure parser
|
||||
|
|
|
|||
|
|
@ -425,8 +425,8 @@ private def expandParentFields (s : Struct) : TermElabM Struct := do
|
|||
else match getPathToBaseStructure? env baseStructName s.structName with
|
||||
| some path =>
|
||||
let path := path.map fun funName => match funName with
|
||||
| .str _ s _ => .fieldName ref (Name.mkSimple s)
|
||||
| _ => unreachable!
|
||||
| .str _ s => .fieldName ref (Name.mkSimple s)
|
||||
| _ => unreachable!
|
||||
return { field with lhs := path ++ field.lhs }
|
||||
| _ => throwErrorAt ref "failed to access field '{fieldName}' in parent structure"
|
||||
| _ => return field
|
||||
|
|
|
|||
|
|
@ -240,7 +240,7 @@ open Lean.Parser.Term hiding macroArg
|
|||
open Lean.Parser.Command
|
||||
|
||||
private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
|
||||
if let Name.str _ suffix _ := catName then
|
||||
if let .str _ suffix := catName then
|
||||
let quotSymbol := "`(" ++ suffix ++ "|"
|
||||
let name := catName ++ `quot
|
||||
let cmd ← `(
|
||||
|
|
@ -297,7 +297,7 @@ where
|
|||
|
||||
appendCatName (str : String) :=
|
||||
match catName with
|
||||
| Name.str _ s _ => s ++ str
|
||||
| .str _ s => s ++ str
|
||||
| _ => str
|
||||
|
||||
/- We assume a new syntax can be treated as an atom when it starts and ends with a token.
|
||||
|
|
|
|||
|
|
@ -1650,7 +1650,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
|
|||
match findLocalDecl? givenNameView (skipAuxDecl := not projs.isEmpty) with
|
||||
| some decl => some (decl.toExpr, projs)
|
||||
| none => match n with
|
||||
| .str pre s _ => loop pre (s::projs)
|
||||
| .str pre s => loop pre (s::projs)
|
||||
| _ => none
|
||||
return loop view.name []
|
||||
|
||||
|
|
|
|||
|
|
@ -75,8 +75,8 @@ def checkSyntaxNodeKind [Monad m] [MonadEnv m] [MonadError m] (k : Name) : m Nam
|
|||
else throwError "failed"
|
||||
|
||||
def checkSyntaxNodeKindAtNamespaces [Monad m] [MonadEnv m] [MonadError m] (k : Name) : Name → m Name
|
||||
| n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces k p
|
||||
| Name.anonymous => checkSyntaxNodeKind k
|
||||
| n@(.str p _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces k p
|
||||
| .anonymous => checkSyntaxNodeKind k
|
||||
| _ => throwError "failed"
|
||||
|
||||
def checkSyntaxNodeKindAtCurrentNamespaces (k : Name) : AttrM Name := do
|
||||
|
|
|
|||
|
|
@ -695,13 +695,13 @@ def getNamespaceSet (env : Environment) : NameSSet :=
|
|||
namespacesExt.getState env
|
||||
|
||||
private def isNamespaceName : Name → Bool
|
||||
| Name.str Name.anonymous _ _ => true
|
||||
| Name.str p _ _ => isNamespaceName p
|
||||
| _ => false
|
||||
| .str .anonymous _ => true
|
||||
| .str p _ => isNamespaceName p
|
||||
| _ => false
|
||||
|
||||
private def registerNamePrefixes : Environment → Name → Environment
|
||||
| env, Name.str p _ _ => if isNamespaceName p then registerNamePrefixes (registerNamespace env p) p else env
|
||||
| env, _ => env
|
||||
| env, .str p _ => if isNamespaceName p then registerNamePrefixes (registerNamespace env p) p else env
|
||||
| env, _ => env
|
||||
|
||||
@[export lean_environment_add]
|
||||
def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
|
||||
|
|
|
|||
|
|
@ -51,11 +51,11 @@ private def mkInaccessibleUserNameAux (unicode : Bool) (name : Name) (idx : Nat)
|
|||
name ++ Name.mkNum "_inaccessible" idx
|
||||
|
||||
private def mkInaccessibleUserName (unicode : Bool) : Name → Name
|
||||
| Name.num p@(Name.str _ _ _) idx _ =>
|
||||
| .num p@(.str ..) idx =>
|
||||
mkInaccessibleUserNameAux unicode p idx
|
||||
| Name.num Name.anonymous idx _ =>
|
||||
| .num .anonymous idx =>
|
||||
mkInaccessibleUserNameAux unicode Name.anonymous idx
|
||||
| Name.num p idx _ =>
|
||||
| .num p idx =>
|
||||
if unicode then
|
||||
(mkInaccessibleUserName unicode p).appendAfter ("⁻" ++ idx.toSuperscriptString)
|
||||
else
|
||||
|
|
|
|||
|
|
@ -130,7 +130,7 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
|
|||
| nCtx, ctx, tagged t d =>
|
||||
/- Messages starting a trace context have their tags postfixed with `_traceCtx` so that
|
||||
we can detect them later. Here, we do so in order to print the trace context class. -/
|
||||
if let Name.str cls "_traceCtx" _ := t then do
|
||||
if let .str cls "_traceCtx" := t then do
|
||||
let d₁ ← formatAux nCtx ctx d
|
||||
return f!"[{cls}] {d₁}"
|
||||
else
|
||||
|
|
|
|||
|
|
@ -95,7 +95,7 @@ private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat)
|
|||
let env ← getEnv
|
||||
if !isAuxRecursor env declName then pure none
|
||||
else match declName with
|
||||
| Name.str p s _ =>
|
||||
| .str p s =>
|
||||
if s != recOnSuffix && s != casesOnSuffix && s != brecOnSuffix then
|
||||
pure none
|
||||
else do
|
||||
|
|
|
|||
|
|
@ -44,11 +44,11 @@ private partial def evalName (e : Expr) : MetaM Name := do
|
|||
let Expr.const c _ _ ← pure e.getAppFn | throwFailedToEval e
|
||||
let nargs := e.getAppNumArgs
|
||||
if c == ``Lean.Name.anonymous && nargs == 0 then pure Name.anonymous
|
||||
else if c == ``Lean.Name.str && nargs == 3 then do
|
||||
else if c == ``Lean.Name.str && nargs == 2 then do
|
||||
let n ← evalName $ e.getArg! 0
|
||||
let s ← reduceEval $ e.getArg! 1
|
||||
pure $ Name.mkStr n s
|
||||
else if c == ``Lean.Name.num && nargs == 3 then do
|
||||
else if c == ``Lean.Name.num && nargs == 2 then do
|
||||
let n ← evalName $ e.getArg! 0
|
||||
let u ← reduceEval $ e.getArg! 1
|
||||
pure $ Name.mkNum n u
|
||||
|
|
|
|||
|
|
@ -34,17 +34,17 @@ def mkPrivateName (env : Environment) (n : Name) : Name :=
|
|||
Name.mkNum (privateHeader ++ env.mainModule) 0 ++ n
|
||||
|
||||
def isPrivateName : Name → Bool
|
||||
| n@(Name.str p _ _) => n == privateHeader || isPrivateName p
|
||||
| Name.num p _ _ => isPrivateName p
|
||||
| _ => false
|
||||
| n@(.str p _) => n == privateHeader || isPrivateName p
|
||||
| .num p _ => isPrivateName p
|
||||
| _ => false
|
||||
|
||||
@[export lean_is_private_name]
|
||||
def isPrivateNameExport (n : Name) : Bool :=
|
||||
isPrivateName n
|
||||
|
||||
private def privateToUserNameAux : Name → Name
|
||||
| Name.str p s _ => Name.mkStr (privateToUserNameAux p) s
|
||||
| _ => Name.anonymous
|
||||
| .str p s => Name.mkStr (privateToUserNameAux p) s
|
||||
| _ => Name.anonymous
|
||||
|
||||
@[export lean_private_to_user_name]
|
||||
def privateToUserName? (n : Name) : Option Name :=
|
||||
|
|
@ -57,8 +57,8 @@ def isPrivateNameFromImportedModule (env : Environment) (n : Name) : Bool :=
|
|||
| _ => false
|
||||
|
||||
private def privatePrefixAux : Name → Name
|
||||
| Name.str p _ _ => privatePrefixAux p
|
||||
| n => n
|
||||
| .str p _ => privatePrefixAux p
|
||||
| n => n
|
||||
|
||||
@[export lean_private_prefix]
|
||||
def privatePrefix? (n : Name) : Option Name :=
|
||||
|
|
|
|||
|
|
@ -656,7 +656,7 @@ def delabProj : Delab := do
|
|||
@[builtinDelab app]
|
||||
def delabProjectionApp : Delab := whenPPOption getPPStructureProjections $ do
|
||||
let e@(Expr.app fn _ _) ← getExpr | failure
|
||||
let Expr.const c@(Name.str _ f _) _ _ ← pure fn.getAppFn | failure
|
||||
let .const c@(.str _ f) _ _ ← pure fn.getAppFn | failure
|
||||
let env ← getEnv
|
||||
let some info ← pure $ env.getProjectionFnInfo? c | failure
|
||||
-- can't use with classes since the instance parameter is implicit
|
||||
|
|
@ -768,18 +768,18 @@ def delabDo : Delab := whenPPOption getPPNotation do
|
|||
`(do $items:doSeqItem*)
|
||||
|
||||
def reifyName : Expr → DelabM Name
|
||||
| Expr.const ``Lean.Name.anonymous .. => return Name.anonymous
|
||||
| Expr.app (Expr.app (Expr.const ``Lean.Name.mkStr ..) n _) (Expr.lit (Literal.strVal s) _) _ => return (← reifyName n).mkStr s
|
||||
| Expr.app (Expr.app (Expr.const ``Lean.Name.mkNum ..) n _) (Expr.lit (Literal.natVal i) _) _ => return (← reifyName n).mkNum i
|
||||
| .const ``Lean.Name.anonymous .. => return Name.anonymous
|
||||
| .app (.app (.const ``Lean.Name.str ..) n _) (.lit (.strVal s) _) _ => return (← reifyName n).mkStr s
|
||||
| .app (.app (.const ``Lean.Name.num ..) n _) (.lit (.natVal i) _) _ => return (← reifyName n).mkNum i
|
||||
| _ => failure
|
||||
|
||||
@[builtinDelab app.Lean.Name.mkStr]
|
||||
@[builtinDelab app.Lean.Name.str]
|
||||
def delabNameMkStr : Delab := whenPPOption getPPNotation do
|
||||
let n ← reifyName (← getExpr)
|
||||
-- not guaranteed to be a syntactically valid name, but usually more helpful than the explicit version
|
||||
return mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{n}"]
|
||||
|
||||
@[builtinDelab app.Lean.Name.mkNum]
|
||||
@[builtinDelab app.Lean.Name.num]
|
||||
def delabNameMkNum : Delab := delabNameMkStr
|
||||
|
||||
end Lean.PrettyPrinter.Delaborator
|
||||
|
|
|
|||
|
|
@ -71,7 +71,7 @@ private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : L
|
|||
|
||||
/- Check surrounding namespaces -/
|
||||
private def resolveUsingNamespace (env : Environment) (id : Name) : Name → List Name
|
||||
| ns@(Name.str p _ _) =>
|
||||
| ns@(.str p _) =>
|
||||
match resolveQualifiedName env ns id with
|
||||
| [] => resolveUsingNamespace env id p
|
||||
| resolvedIds => resolvedIds
|
||||
|
|
@ -118,7 +118,7 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
|
|||
let extractionResult := extractMacroScopes id
|
||||
let rec loop (id : Name) (projs : List String) : List (Name × List String) :=
|
||||
match id with
|
||||
| Name.str p s _ =>
|
||||
| .str p s =>
|
||||
-- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
|
||||
let id := { extractionResult with name := id }.review
|
||||
match resolveUsingNamespace env id ns with
|
||||
|
|
@ -141,9 +141,9 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
|
|||
/- Namespace resolution -/
|
||||
|
||||
def resolveNamespaceUsingScope? (env : Environment) (n : Name) : Name → Option Name
|
||||
| Name.anonymous => if env.isNamespace n then some n else none
|
||||
| ns@(Name.str p _ _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope? env n p
|
||||
| _ => unreachable!
|
||||
| .anonymous => if env.isNamespace n then some n else none
|
||||
| ns@(.str p _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope? env n p
|
||||
| _ => unreachable!
|
||||
|
||||
def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDecl → List Name
|
||||
| [] => []
|
||||
|
|
|
|||
|
|
@ -124,7 +124,7 @@ private def runM (ctx : ContextInfo) (lctx : LocalContext) (x : M Unit) : IO (Op
|
|||
|
||||
private def matchAtomic (id : Name) (declName : Name) : Option Float :=
|
||||
match id, declName with
|
||||
| Name.str Name.anonymous s₁ _, Name.str Name.anonymous s₂ _ => fuzzyMatchScoreWithThreshold? s₁ s₂
|
||||
| .str .anonymous s₁, .str .anonymous s₂ => fuzzyMatchScoreWithThreshold? s₁ s₂
|
||||
| _, _ => none
|
||||
|
||||
private def normPrivateName (declName : Name) : MetaM Name := do
|
||||
|
|
@ -157,7 +157,7 @@ private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName :
|
|||
return none
|
||||
else if !danglingDot then
|
||||
match id, declName with
|
||||
| Name.str p₁ s₁ _, Name.str p₂ s₂ _ =>
|
||||
| .str p₁ s₁, .str p₂ s₂ =>
|
||||
if p₁ == p₂ then
|
||||
return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (s₂, ·)
|
||||
else
|
||||
|
|
@ -175,7 +175,7 @@ private partial def truncate (id : Name) (newLen : Nat) : Name :=
|
|||
match id with
|
||||
| Name.anonymous => (id, 0)
|
||||
| Name.num .. => unreachable!
|
||||
| Name.str p s _ =>
|
||||
| .str p s =>
|
||||
let (p', len) := go p
|
||||
if len + 1 >= newLen then
|
||||
(p', len)
|
||||
|
|
@ -200,7 +200,7 @@ def matchNamespace (ns : Name) (nsFragment : Name) (danglingDot : Bool) : Option
|
|||
none
|
||||
else
|
||||
match ns, nsFragment with
|
||||
| Name.str p₁ s₁ _, Name.str p₂ s₂ _ =>
|
||||
| .str p₁ s₁, .str p₂ s₂ =>
|
||||
if p₁ == p₂ then fuzzyMatchScoreWithThreshold? s₂ s₁ else none
|
||||
| _, _ => none
|
||||
|
||||
|
|
@ -304,7 +304,7 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverI
|
|||
| _ => return ()
|
||||
searchAlias ctx.currNamespace
|
||||
-- Search keywords
|
||||
if let Name.str Name.anonymous s _ := id then
|
||||
if let .str .anonymous s := id then
|
||||
let keywords := Parser.getTokenTable env
|
||||
for keyword in keywords.findPrefix s do
|
||||
addKeywordCompletionItem keyword
|
||||
|
|
|
|||
|
|
@ -367,7 +367,7 @@ namespace Syntax
|
|||
|
||||
-- quotation node kinds are formed from a unique quotation name plus "quot"
|
||||
def isQuot : Syntax → Bool
|
||||
| Syntax.node _ (Name.str _ "quot" _) _ => true
|
||||
| Syntax.node _ (Name.str _ "quot") _ => true
|
||||
| Syntax.node _ `Lean.Parser.Term.dynamicQuot _ => true
|
||||
| _ => false
|
||||
|
||||
|
|
@ -380,8 +380,8 @@ def getQuotContent (stx : Syntax) : Syntax :=
|
|||
|
||||
-- antiquotation node kinds are formed from the original node kind (if any) plus "antiquot"
|
||||
def isAntiquot : Syntax → Bool
|
||||
| Syntax.node _ (Name.str _ "antiquot" _) _ => true
|
||||
| _ => false
|
||||
| .node _ (.str _ "antiquot") _ => true
|
||||
| _ => false
|
||||
|
||||
def isAntiquots (stx : Syntax) : Bool :=
|
||||
stx.isAntiquot || (stx.isOfKind choiceKind && stx.getNumArgs > 0 && stx.getArgs.all isAntiquot)
|
||||
|
|
@ -425,9 +425,9 @@ def getAntiquotTerm (stx : Syntax) : Syntax :=
|
|||
|
||||
/-- Return kind of parser expected at this antiquotation, and whether it is a "pseudo" kind (see `mkAntiquot`). -/
|
||||
def antiquotKind? : Syntax → Option (SyntaxNodeKind × Bool)
|
||||
| Syntax.node _ (Name.str (Name.str k "pseudo" _) "antiquot" _) _ => (k, true)
|
||||
| Syntax.node _ (Name.str k "antiquot" _) _ => (k, false)
|
||||
| _ => none
|
||||
| .node _ (.str (.str k "pseudo") "antiquot") _ => (k, true)
|
||||
| .node _ (.str k "antiquot") _ => (k, false)
|
||||
| _ => none
|
||||
|
||||
def antiquotKinds (stx : Syntax) : List (SyntaxNodeKind × Bool) :=
|
||||
if stx.isOfKind choiceKind then
|
||||
|
|
@ -439,7 +439,7 @@ def antiquotKinds (stx : Syntax) : List (SyntaxNodeKind × Bool) :=
|
|||
|
||||
-- An "antiquotation splice" is something like `$[...]?` or `$[...]*`.
|
||||
def antiquotSpliceKind? : Syntax → Option SyntaxNodeKind
|
||||
| Syntax.node _ (Name.str k "antiquot_scope" _) _ => some k
|
||||
| .node _ (.str k "antiquot_scope") _ => some k
|
||||
| _ => none
|
||||
|
||||
def isAntiquotSplice (stx : Syntax) : Bool :=
|
||||
|
|
@ -461,7 +461,7 @@ def mkAntiquotSpliceNode (kind : SyntaxNodeKind) (contents : Array Syntax) (suff
|
|||
|
||||
-- `$x,*` etc.
|
||||
def antiquotSuffixSplice? : Syntax → Option SyntaxNodeKind
|
||||
| Syntax.node _ (Name.str k "antiquot_suffix_splice" _) _ => some k
|
||||
| .node _ (.str k "antiquot_suffix_splice") _ => some k
|
||||
| _ => none
|
||||
|
||||
def isAntiquotSuffixSplice (stx : Syntax) : Bool :=
|
||||
|
|
|
|||
|
|
@ -20,9 +20,9 @@ def modToFilePath (base : FilePath) (mod : Name) (ext : String) : FilePath :=
|
|||
go mod |>.withExtension ext
|
||||
where
|
||||
go : Name → FilePath
|
||||
| Name.str p h _ => go p / h
|
||||
| Name.str p h => go p / h
|
||||
| Name.anonymous => base
|
||||
| Name.num _ _ _ => panic! "ill-formed import"
|
||||
| Name.num _ _ => panic! "ill-formed import"
|
||||
|
||||
/-- A `.olean' search path. -/
|
||||
abbrev SearchPath := System.SearchPath
|
||||
|
|
|
|||
|
|
@ -54,8 +54,8 @@ def resetTraceState {m} [MonadTrace m] : m Unit :=
|
|||
modifyTraceState (fun _ => {})
|
||||
|
||||
private def checkTraceOptionAux (opts : Options) : Name → Bool
|
||||
| n@(Name.str p _ _) => opts.getBool n || (!opts.contains n && checkTraceOptionAux opts p)
|
||||
| _ => false
|
||||
| n@(.str p _) => opts.getBool n || (!opts.contains n && checkTraceOptionAux opts p)
|
||||
| _ => false
|
||||
|
||||
def checkTraceOption (opts : Options) (cls : Name) : Bool :=
|
||||
if opts.isEmpty then false
|
||||
|
|
|
|||
|
|
@ -106,7 +106,7 @@ where
|
|||
| _, ctx, withNamingContext nCtx d => go nCtx ctx d
|
||||
| nCtx, ctx, tagged t d => do
|
||||
-- We postfix trace contexts with `_traceCtx` in order to detect them in messages.
|
||||
if let Name.str cls "_traceCtx" _ := t then
|
||||
if let .str cls "_traceCtx" := t then
|
||||
-- When interactive trace exploration is possible, we hide traces which can otherwise
|
||||
-- take significant resources to pretty-print.
|
||||
if hasWidgets then
|
||||
|
|
|
|||
2
src/lake
2
src/lake
|
|
@ -1 +1 @@
|
|||
Subproject commit 35cc869b018e41a0dbaf74ed07c8ec9cf1ee4ac3
|
||||
Subproject commit 0d6e16a3ad6b0e190b1d557df86fc627d4597c29
|
||||
|
|
@ -1,8 +1,8 @@
|
|||
Lean.Name.mkStr Lean.Name.anonymous "foo" : Lean.Name
|
||||
Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo") "bla" : Lean.Name
|
||||
Lean.Name.mkStr Lean.Name.anonymous "foo bla" : Lean.Name
|
||||
Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo bla") "hello world" : Lean.Name
|
||||
Lean.Name.mkStr (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo bla") "boo") "hello world" : Lean.Name
|
||||
Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo") "hello" : Lean.Name
|
||||
Lean.Name.mkStr Lean.Name.anonymous "hello" : Lean.Name
|
||||
Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "hello") "world !!!" : Lean.Name
|
||||
Lean.Name.str Lean.Name.anonymous "foo" : Lean.Name
|
||||
Lean.Name.str (Lean.Name.str Lean.Name.anonymous "foo") "bla" : Lean.Name
|
||||
Lean.Name.str Lean.Name.anonymous "foo bla" : Lean.Name
|
||||
Lean.Name.str (Lean.Name.str Lean.Name.anonymous "foo bla") "hello world" : Lean.Name
|
||||
Lean.Name.str (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "foo bla") "boo") "hello world" : Lean.Name
|
||||
Lean.Name.str (Lean.Name.str Lean.Name.anonymous "foo") "hello" : Lean.Name
|
||||
Lean.Name.str Lean.Name.anonymous "hello" : Lean.Name
|
||||
Lean.Name.str (Lean.Name.str Lean.Name.anonymous "hello") "world !!!" : Lean.Name
|
||||
|
|
|
|||
|
|
@ -55,9 +55,9 @@ def exportName (n : Name) : ExportM Nat := do
|
|||
match (← get).names.map.find? n with
|
||||
| some i => pure i
|
||||
| none => match n with
|
||||
| Name.anonymous => pure 0
|
||||
| Name.num p a _ => let i ← alloc n; IO.println s!"{i} #NI {← exportName p} {a}"; pure i
|
||||
| Name.str p s _ => let i ← alloc n; IO.println s!"{i} #NS {← exportName p} {s}"; pure i
|
||||
| .anonymous => pure 0
|
||||
| .num p a => let i ← alloc n; IO.println s!"{i} #NI {← exportName p} {a}"; pure i
|
||||
| .str p s => let i ← alloc n; IO.println s!"{i} #NS {← exportName p} {s}"; pure i
|
||||
|
||||
attribute [simp] exportName
|
||||
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ open Lean.Meta
|
|||
def shouldIgnore (declName : Name) : Bool :=
|
||||
declName.isInternal
|
||||
|| match declName with
|
||||
| Name.str _ s _ => "match_".isPrefixOf s || "proof_".isPrefixOf s || "eq_".isPrefixOf s
|
||||
| .str _ s => "match_".isPrefixOf s || "proof_".isPrefixOf s || "eq_".isPrefixOf s
|
||||
| _ => true
|
||||
|
||||
-- Print declarations that have the given prefix.
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue