From b09fb4348d9b4bf6fedb38378b2d338fcd094549 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Nov 2019 13:27:57 -0800 Subject: [PATCH] chore: rename `Name` constructors --- library/Init/Lean/Compiler/ConstFolding.lean | 6 +- library/Init/Lean/Compiler/ExportAttr.lean | 6 +- library/Init/Lean/Compiler/IR/Boxing.lean | 4 +- library/Init/Lean/Compiler/IR/EmitC.lean | 6 +- library/Init/Lean/Compiler/NameMangling.lean | 6 +- library/Init/Lean/Compiler/Util.lean | 8 +- library/Init/Lean/Elaborator/Command.lean | 12 +- library/Init/Lean/Elaborator/ResolveName.lean | 4 +- library/Init/Lean/Environment.lean | 10 +- library/Init/Lean/Modifiers.lean | 18 +-- library/Init/Lean/Name.lean | 153 ++++++++---------- library/Init/Lean/NameGenerator.lean | 4 +- library/Init/Lean/Parser/Parser.lean | 10 +- library/Init/Lean/Path.lean | 10 +- library/Init/Lean/Scopes.lean | 4 +- library/Init/Lean/ToExpr.lean | 6 +- library/Init/Lean/Trace.lean | 4 +- library/Init/Lean/TypeClass/Context.lean | 24 +-- library/Init/Lean/TypeClass/Synth.lean | 2 +- library/Init/Lean/WHNF.lean | 2 +- src/frontends/lean/parser.cpp | 3 +- src/library/constants.cpp | 16 +- src/library/constants.h | 4 +- src/library/constants.txt | 4 +- src/library/util.cpp | 4 +- 25 files changed, 158 insertions(+), 172 deletions(-) diff --git a/library/Init/Lean/Compiler/ConstFolding.lean b/library/Init/Lean/Compiler/ConstFolding.lean index a65a95d4ec..fbce3f1957 100644 --- a/library/Init/Lean/Compiler/ConstFolding.lean +++ b/library/Init/Lean/Compiler/ConstFolding.lean @@ -17,13 +17,13 @@ def BinFoldFn := Bool → Expr → Expr → Option Expr def UnFoldFn := Bool → Expr → Option Expr def mkUIntTypeName (nbytes : Nat) : Name := -mkSimpleName ("UInt" ++ toString nbytes) +mkNameSimple ("UInt" ++ toString nbytes) structure NumScalarTypeInfo := (nbits : Nat) (id : Name := mkUIntTypeName nbits) -(ofNatFn : Name := Name.mkString id "ofNat") -(toNatFn : Name := Name.mkString id "toNat") +(ofNatFn : Name := mkNameStr id "ofNat") +(toNatFn : Name := mkNameStr id "toNat") (size : Nat := 2^nbits) def numScalarTypes : List NumScalarTypeInfo := diff --git a/library/Init/Lean/Compiler/ExportAttr.lean b/library/Init/Lean/Compiler/ExportAttr.lean index d3428cd375..3a9de4cc66 100644 --- a/library/Init/Lean/Compiler/ExportAttr.lean +++ b/library/Init/Lean/Compiler/ExportAttr.lean @@ -13,9 +13,9 @@ let first := id.get 0; first.isAlpha && (id.toSubstring.drop 1).all (fun c => c.isAlpha || c.isDigit || c == '_') private def isValidCppName : Name → Bool -| Name.mkString Name.anonymous s => isValidCppId s -| Name.mkString p s => isValidCppId s && isValidCppName p -| _ => false +| Name.str Name.anonymous s => isValidCppId s +| Name.str p s => isValidCppId s && isValidCppName p +| _ => false def mkExportAttr : IO (ParametricAttribute Name) := registerParametricAttribute `export "name to be used by code generators" $ fun _ _ stx => diff --git a/library/Init/Lean/Compiler/IR/Boxing.lean b/library/Init/Lean/Compiler/IR/Boxing.lean index a8cecc4e7d..29e81fa013 100644 --- a/library/Init/Lean/Compiler/IR/Boxing.lean +++ b/library/Init/Lean/Compiler/IR/Boxing.lean @@ -35,10 +35,10 @@ Assumptions: -/ def mkBoxedName (n : Name) : Name := -Name.mkString n "_boxed" +mkNameStr n "_boxed" def isBoxedName : Name → Bool -| Name.mkString _ "_boxed" => true +| Name.str _ "_boxed" => true | _ => false abbrev N := StateM Nat diff --git a/library/Init/Lean/Compiler/IR/EmitC.lean b/library/Init/Lean/Compiler/IR/EmitC.lean index 19f04d26dd..2e71a7ee53 100644 --- a/library/Init/Lean/Compiler/IR/EmitC.lean +++ b/library/Init/Lean/Compiler/IR/EmitC.lean @@ -76,7 +76,7 @@ def toCName (n : Name) : M String := do env ← getEnv; -- TODO: we should support simple export names only match getExportNameFor env n with - | some (Name.mkString Name.anonymous s) => pure s + | some (Name.str Name.anonymous s) => pure s | some _ => throwInvalidExportName n | none => if n == `main then pure leanMainFn else pure n.mangle @@ -87,7 +87,7 @@ def toCInitName (n : Name) : M String := do env ← getEnv; -- TODO: we should support simple export names only match getExportNameFor env n with - | some (Name.mkString Name.anonymous s) => pure $ "_init_" ++ s + | some (Name.str Name.anonymous s) => pure $ "_init_" ++ s | some _ => throwInvalidExportName n | none => pure ("_init_" ++ n.mangle) @@ -119,7 +119,7 @@ do cppBaseName ← toCName decl.name; emitFnDeclAux decl cppBaseName addExternForConsts def emitExternDeclAux (decl : Decl) (cNameStr : String) : M Unit := -do let cName := mkSimpleName cNameStr; +do let cName := mkNameSimple cNameStr; env ← getEnv; let extC := isExternC env decl.name; emitFnDeclAux decl cNameStr (!extC) diff --git a/library/Init/Lean/Compiler/NameMangling.lean b/library/Init/Lean/Compiler/NameMangling.lean index 8258a345d6..b9c70235ef 100644 --- a/library/Init/Lean/Compiler/NameMangling.lean +++ b/library/Init/Lean/Compiler/NameMangling.lean @@ -36,13 +36,13 @@ def String.mangle (s : String) : String := String.mangleAux s.length s.mkIterator "" private def Name.mangleAux : Name → String -| Name.anonymous => "" -| Name.mkString p s => +| Name.anonymous => "" +| Name.str p s => let m := String.mangle s; match p with | Name.anonymous => m | _ => Name.mangleAux p ++ "_" ++ m -| Name.mkNumeral p n => Name.mangleAux p ++ "_" ++ toString n ++ "_" +| Name.num p n => Name.mangleAux p ++ "_" ++ toString n ++ "_" @[export lean_name_mangle] def Name.mangle (n : Name) (pre : String := "l_") : String := diff --git a/library/Init/Lean/Compiler/Util.lean b/library/Init/Lean/Compiler/Util.lean index 83bb90857e..3a81e6fd86 100644 --- a/library/Init/Lean/Compiler/Util.lean +++ b/library/Init/Lean/Compiler/Util.lean @@ -59,13 +59,13 @@ result @[export lean_mk_eager_lambda_lifting_name] def mkEagerLambdaLiftingName (n : Name) (idx : Nat) : Name := -Name.mkString n ("_elambda_" ++ toString idx) +mkNameStr n ("_elambda_" ++ toString idx) @[export lean_is_eager_lambda_lifting_name] def isEagerLambdaLiftingName : Name → Bool -| Name.mkString p s => "_elambda".isPrefixOf s || isEagerLambdaLiftingName p -| Name.mkNumeral p _ => isEagerLambdaLiftingName p -| _ => false +| Name.str p s => "_elambda".isPrefixOf s || isEagerLambdaLiftingName p +| Name.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. diff --git a/library/Init/Lean/Elaborator/Command.lean b/library/Init/Lean/Elaborator/Command.lean index d55139ecae..1e2cb9fd13 100644 --- a/library/Init/Lean/Elaborator/Command.lean +++ b/library/Init/Lean/Elaborator/Command.lean @@ -13,11 +13,11 @@ namespace Lean namespace Elab private def addScopes (cmd : String) (updateNamespace : Bool) : Name → List ElabScope → List ElabScope -| Name.anonymous, scopes => scopes -| Name.mkString p h, scopes => +| Name.anonymous, scopes => scopes +| Name.str p h, scopes => let scopes := addScopes p scopes; let ns := scopes.head!.ns; - let ns := if updateNamespace then Name.mkString ns h else ns; + let ns := if updateNamespace then mkNameStr ns h else ns; { cmd := cmd, header := h, ns := ns } :: scopes | _, _ => [] -- unreachable @@ -46,9 +46,9 @@ private def checkAnonymousScope : List ElabScope → Bool | _ => false private def checkEndHeader : Name → List ElabScope → Bool -| Name.anonymous, _ => true -| Name.mkString p s, { header := h, .. } :: scopes => h.eqStr s && checkEndHeader p scopes -| _, _ => false +| Name.anonymous, _ => true +| Name.str p s, { header := h, .. } :: scopes => h.eqStr s && checkEndHeader p scopes +| _, _ => false @[builtinCommandElab «end»] def elabEnd : CommandElab := fun n => do diff --git a/library/Init/Lean/Elaborator/ResolveName.lean b/library/Init/Lean/Elaborator/ResolveName.lean index 724458d84c..e89d091667 100644 --- a/library/Init/Lean/Elaborator/ResolveName.lean +++ b/library/Init/Lean/Elaborator/ResolveName.lean @@ -20,7 +20,7 @@ else resolvedIds /- Check surrounding namespaces -/ private def resolveUsingNamespace (env : Environment) (id : Name) : Name → List Name -| ns@(Name.mkString p _) => +| ns@(Name.str p _) => match resolveQualifiedName env ns id with | [] => resolveUsingNamespace p | resolvedIds => resolvedIds @@ -46,7 +46,7 @@ private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl → resolveOpenDecls openDecls resolvedIds private def resolveNameAux (env : Environment) (ns : Name) (openDecls : List OpenDecl) : Name → Nat → List (Nat × Name) -| id@(Name.mkString p _), projSize => +| id@(Name.str p _), projSize => match resolveUsingNamespace env id ns with | resolvedIds@(_ :: _) => resolvedIds.eraseDups.map $ fun id => (projSize, id) | [] => diff --git a/library/Init/Lean/Environment.lean b/library/Init/Lean/Environment.lean index 80221fbdaa..4eb3394747 100644 --- a/library/Init/Lean/Environment.lean +++ b/library/Init/Lean/Environment.lean @@ -534,13 +534,13 @@ namespacesExt.getState env namespace Environment private def isNamespaceName : Name → Bool -| Name.mkString Name.anonymous _ => true -| Name.mkString p _ => isNamespaceName p -| _ => false +| Name.str Name.anonymous _ => true +| Name.str p _ => isNamespaceName p +| _ => false private def registerNamePrefixes : Environment → Name → Environment -| env, Name.mkString p _ => if isNamespaceName p then registerNamePrefixes (registerNamespace env p) p else env -| env, _ => env +| env, Name.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 := diff --git a/library/Init/Lean/Modifiers.lean b/library/Init/Lean/Modifiers.lean index 8738efcbc8..a0db08d859 100644 --- a/library/Init/Lean/Modifiers.lean +++ b/library/Init/Lean/Modifiers.lean @@ -36,7 +36,7 @@ constant privateExt : EnvExtension Nat := arbitrary _ where `` comes from the environment extension `privateExt`. We assume that `n` is a valid user name and does not contain - `Name.mkNumeral` constructors. Thus, we can easily convert from + `Name.num` constructors. Thus, we can easily convert from private internal name to user given name. -/ @@ -45,7 +45,7 @@ def privateHeader : Name := `_private @[export lean_mk_private_prefix] def mkPrivatePrefix (env : Environment) : Environment × Name := let idx := privateExt.getState env; -let p := Name.mkNumeral (privateHeader ++ env.mainModule) idx; +let p := mkNameNum (privateHeader ++ env.mainModule) idx; let env := privateExt.setState env (idx+1); (env, p) @@ -55,17 +55,17 @@ let (env, p) := mkPrivatePrefix env; (env, p ++ n) def isPrivateName : Name → Bool -| n@(Name.mkString p _) => n == privateHeader || isPrivateName p -| Name.mkNumeral p _ => isPrivateName p -| _ => false +| n@(Name.str p _) => n == privateHeader || isPrivateName p +| Name.num p _ => isPrivateName p +| _ => false @[export lean_is_private_name] def isPrivateNameExport (n : Name) : Bool := isPrivateName n private def privateToUserNameAux : Name → Name -| Name.mkString p s => Name.mkString (privateToUserNameAux p) s -| _ => Name.anonymous +| Name.str p s => mkNameStr (privateToUserNameAux p) s +| _ => Name.anonymous @[export lean_private_to_user_name] def privateToUserName (n : Name) : Option Name := @@ -73,8 +73,8 @@ if isPrivateName n then privateToUserNameAux n else none private def privatePrefixAux : Name → Name -| Name.mkString p _ => privatePrefixAux p -| n => n +| Name.str p _ => privatePrefixAux p +| n => n @[export lean_private_prefix] def privatePrefix (n : Name) : Option Name := diff --git a/library/Init/Lean/Name.lean b/library/Init/Lean/Name.lean index f872640561..e0f8603944 100644 --- a/library/Init/Lean/Name.lean +++ b/library/Init/Lean/Name.lean @@ -15,26 +15,28 @@ namespace Lean inductive Name | anonymous : Name -| mkString : Name → String → Name -| mkNumeral : Name → Nat → Name +| str : Name → String → Name +| num : Name → Nat → Name -attribute [extern "lean_name_mk_string"] Name.mkString -attribute [extern "lean_name_mk_numeral"] Name.mkNumeral +attribute [extern "lean_name_mk_string"] Name.str +attribute [extern "lean_name_mk_numeral"] Name.num + +@[matchPattern] abbrev Name.mkString := Name.str instance : Inhabited Name := ⟨Name.anonymous⟩ -def mkStrName (p : Name) (s : String) : Name := -Name.mkString p s +def mkNameStr (p : Name) (s : String) : Name := +Name.str p s -def mkNumName (p : Name) (v : Nat) : Name := -Name.mkNumeral p v +def mkNameNum (p : Name) (v : Nat) : Name := +Name.num p v -def mkSimpleName (s : String) : Name := -mkStrName Name.anonymous s +def mkNameSimple (s : String) : Name := +mkNameStr Name.anonymous s instance stringToName : HasCoe String Name := -⟨mkSimpleName⟩ +⟨mkNameSimple⟩ namespace Name @[extern "lean_name_hash_usize"] @@ -44,84 +46,74 @@ instance : Hashable Name := ⟨Name.hash⟩ def getPrefix : Name → Name -| anonymous => anonymous -| mkString p s => p -| mkNumeral p s => p +| anonymous => anonymous +| str p s => p +| num p s => p def getNumParts : Name → Nat -| anonymous => 0 -| mkString p _ => getNumParts p + 1 -| mkNumeral p _ => getNumParts p + 1 +| anonymous => 0 +| str p _ => getNumParts p + 1 +| num p _ => getNumParts p + 1 def updatePrefix : Name → Name → Name -| anonymous, newP => anonymous -| mkString p s, newP => mkString newP s -| mkNumeral p s, newP => mkNumeral newP s +| anonymous, newP => anonymous +| str p s, newP => mkNameStr newP s +| num p s, newP => mkNameNum newP s def components' : Name → List Name -| anonymous => [] -| mkString n s => mkString anonymous s :: components' n -| mkNumeral n v => mkNumeral anonymous v :: components' n +| anonymous => [] +| str n s => mkNameStr anonymous s :: components' n +| num n v => mkNameNum anonymous v :: components' n def components (n : Name) : List Name := n.components'.reverse protected def beq : Name → Name → Bool -| anonymous, anonymous => true -| mkString p₁ s₁, mkString p₂ s₂ => s₁ == s₂ && beq p₁ p₂ -| mkNumeral p₁ n₁, mkNumeral p₂ n₂ => n₁ == n₂ && beq p₁ p₂ -| _, _ => false +| anonymous, anonymous => true +| str p₁ s₁, str p₂ s₂ => s₁ == s₂ && beq p₁ p₂ +| num p₁ n₁, num p₂ n₂ => n₁ == n₂ && beq p₁ p₂ +| _, _ => false instance : HasBeq Name := ⟨Name.beq⟩ def eqStr : Name → String → Bool -| mkString Name.anonymous s, s' => s == s' -| _, _ => false +| str anonymous s, s' => s == s' +| _, _ => false protected def append : Name → Name → Name | n, anonymous => n -| n, mkString p s => - mkString (append n p) s -| n, mkNumeral p d => - mkNumeral (append n p) d +| n, str p s => mkNameStr (append n p) s +| n, num p d => mkNameNum (append n p) d instance : HasAppend Name := ⟨Name.append⟩ def replacePrefix : Name → Name → Name → Name -| anonymous, anonymous, newP => newP -| anonymous, _, _ => anonymous -| n@(mkString p s), queryP, newP => - if n == queryP then - newP - else - mkString (p.replacePrefix queryP newP) s -| n@(mkNumeral p s), queryP, newP => - if n == queryP then - newP - else - mkNumeral (p.replacePrefix queryP newP) s +| anonymous, anonymous, newP => newP +| anonymous, _, _ => anonymous +| n@(str p s), queryP, newP => if n == queryP then newP else mkNameStr (p.replacePrefix queryP newP) s +| n@(num p s), queryP, newP => if n == queryP then newP else mkNameNum (p.replacePrefix queryP newP) s def isPrefixOf : Name → Name → Bool -| p, anonymous => p == anonymous -| p, n@(mkNumeral p' _) => p == n || isPrefixOf p p' -| p, n@(mkString 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 lt : Name → Name → Bool -| anonymous, anonymous => false -| anonymous, _ => true -| mkNumeral p₁ i₁, mkNumeral p₂ i₂ => lt p₁ p₂ || (p₁ == p₂ && i₁ < i₂) -| mkNumeral _ _, mkString _ _ => true -| mkString p₁ n₁, mkString p₂ n₂ => lt p₁ p₂ || (p₁ == p₂ && n₁ < n₂) -| _, _ => false +| anonymous, anonymous => false +| anonymous, _ => true +| num p₁ i₁, num p₂ i₂ => lt p₁ p₂ || (p₁ == p₂ && i₁ < i₂) +| num _ _, str _ _ => true +| str p₁ n₁, str p₂ n₂ => lt p₁ p₂ || (p₁ == p₂ && n₁ < n₂) +| _, _ => false def quickLtAux : Name → Name → Bool -| anonymous, anonymous => false -| anonymous, _ => true -| mkNumeral n v, mkNumeral n' v' => v < v' || (v = v' && n.quickLtAux n') -| mkNumeral _ _, mkString _ _ => true -| mkString n s, mkString n' s' => s < s' || (s = s' && n.quickLtAux n') -| _, _ => false +| anonymous, anonymous => false +| anonymous, _ => true +| num n v, num n' v' => v < v' || (v = v' && n.quickLtAux n') +| num _ _, str _ _ => true +| str n s, str n' s' => s < s' || (s = s' && n.quickLtAux n') +| _, _ => false def quickLt (n₁ n₂ : Name) : Bool := if n₁.hash < n₂.hash then true @@ -136,11 +128,11 @@ else quickLtAux n₁ n₂ inferInstanceAs (DecidableRel (fun a b => Name.quickLt a b = true)) def toStringWithSep (sep : String) : Name → String -| anonymous => "[anonymous]" -| mkString anonymous s => s -| mkNumeral anonymous v => toString v -| mkString n s => toStringWithSep n ++ sep ++ s -| mkNumeral n v => toStringWithSep n ++ sep ++ repr v +| anonymous => "[anonymous]" +| str anonymous s => s +| num anonymous v => toString v +| str n s => toStringWithSep n ++ sep ++ s +| num n v => toStringWithSep n ++ sep ++ repr v protected def toString : Name → String := toStringWithSep "." @@ -149,25 +141,25 @@ instance : HasToString Name := ⟨Name.toString⟩ def appendAfter : Name → String → Name -| mkString p s, suffix => mkString p (s ++ suffix) -| n, suffix => mkString n suffix +| str p s, suffix => mkNameStr p (s ++ suffix) +| n, suffix => mkNameStr n suffix def appendIndexAfter : Name → Nat → Name -| mkString p s, idx => mkString p (s ++ "_" ++ toString idx) -| n, idx => mkString n ("_" ++ toString idx) +| str p s, idx => mkNameStr p (s ++ "_" ++ toString idx) +| n, idx => mkNameStr n ("_" ++ toString idx) /- 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 -| mkString p s => s.get 0 == '_' || isInternal p -| mkNumeral p _ => isInternal p -| _ => false +| str p s => s.get 0 == '_' || isInternal p +| num p _ => isInternal p +| _ => false def isAtomic : Name → Bool -| anonymous => true -| mkString anonymous _ => true -| mkNumeral anonymous _ => true -| _ => false +| anonymous => true +| str anonymous _ => true +| num anonymous _ => true +| _ => false end Name @@ -205,17 +197,10 @@ def insert (s : NameSet) (n : Name) := RBTree.insert s n def contains (s : NameSet) (n : Name) : Bool := RBMap.contains s n end NameSet - -def mkNameStr (p : Name) (s : String) : Name := -Name.mkString p s - -def mkNameNum (p : Name) (v : Nat) : Name := -Name.mkNumeral p v - end Lean open Lean def String.toName (s : String) : Name := let ps := s.splitOn "."; -ps.foldl (fun n p => Name.mkString n p.trim) Name.anonymous +ps.foldl (fun n p => mkNameStr n p.trim) Name.anonymous diff --git a/library/Init/Lean/NameGenerator.lean b/library/Init/Lean/NameGenerator.lean index b1f4ef82de..555f19661a 100644 --- a/library/Init/Lean/NameGenerator.lean +++ b/library/Init/Lean/NameGenerator.lean @@ -17,13 +17,13 @@ namespace NameGenerator instance : Inhabited NameGenerator := ⟨{}⟩ @[inline] def curr (g : NameGenerator) : Name := -Name.mkNumeral g.namePrefix g.idx +mkNameNum g.namePrefix g.idx @[inline] def next (g : NameGenerator) : NameGenerator := { idx := g.idx + 1, .. g } @[inline] def mkChild (g : NameGenerator) : NameGenerator × NameGenerator := -({ namePrefix := Name.mkNumeral g.namePrefix g.idx, idx := 1 }, +({ namePrefix := mkNameNum g.namePrefix g.idx, idx := 1 }, { idx := g.idx + 1, .. g }) end NameGenerator diff --git a/library/Init/Lean/Parser/Parser.lean b/library/Init/Lean/Parser/Parser.lean index c4f1ae0532..a3e5a6efe5 100644 --- a/library/Init/Lean/Parser/Parser.lean +++ b/library/Init/Lean/Parser/Parser.lean @@ -772,7 +772,7 @@ partial def identFnAux (startPos : Nat) (tk : Option TokenConfig) : Name → Bas let s := satisfyFn isIdEndEscape "missing end of escaped identifier" c s; if s.hasError then s else - let r := Name.mkString r (input.extract startPart stopPart); + let r := mkNameStr r (input.extract startPart stopPart); if isIdCont input s then let s := s.next input s.pos; identFnAux r c s @@ -782,7 +782,7 @@ partial def identFnAux (startPos : Nat) (tk : Option TokenConfig) : Name → Bas let startPart := i; let s := takeWhileFn isIdRest c (s.next input i); let stopPart := s.pos; - let r := Name.mkString r (input.extract startPart stopPart); + let r := mkNameStr r (input.extract startPart stopPart); if isIdCont input s then let s := s.next input s.pos; identFnAux r c s @@ -1273,7 +1273,7 @@ let find (n : Name) : ParserState × List α := | some as => (s, as) | _ => (s, []); match stx with -| some (Syntax.atom _ sym) => find (mkSimpleName sym) +| some (Syntax.atom _ sym) => find (mkNameSimple sym) | some (Syntax.ident _ _ _ _) => find `ident | some (Syntax.node k _) => find k | _ => (s, []) @@ -1420,7 +1420,7 @@ do tables ← tablesRef.get; updateTokens p.info declName; updateSyntaxNodeKinds p.info; let addTokens (tks : List TokenConfig) : IO Unit := - let tks := tks.map $ fun tk => mkSimpleName tk.val; + let tks := tks.map $ fun tk => mkNameSimple tk.val; tablesRef.set $ tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { leadingTable := tables.leadingTable.insert tk p, .. tables }) tables; match p.info.firstTokens with | FirstTokens.tokens tks => addTokens tks @@ -1433,7 +1433,7 @@ do tables ← tablesRef.get; updateTokens p.info declName; updateSyntaxNodeKinds p.info; let addTokens (tks : List TokenConfig) : IO Unit := - let tks := tks.map $ fun tk => mkSimpleName tk.val; + let tks := tks.map $ fun tk => mkNameSimple tk.val; tablesRef.set $ tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { trailingTable := tables.trailingTable.insert tk p, .. tables }) tables; match p.info.firstTokens with | FirstTokens.tokens tks => addTokens tks diff --git a/library/Init/Lean/Path.lean b/library/Init/Lean/Path.lean index 33a1f1b82d..8c0cd2c09f 100644 --- a/library/Init/Lean/Path.lean +++ b/library/Init/Lean/Path.lean @@ -75,10 +75,10 @@ do let fname := System.FilePath.normalizePath fname; | other => pure other def modNameToFileName : Name → String -| Name.mkString Name.anonymous h => h -| Name.mkString p h => modNameToFileName p ++ pathSep ++ h -| Name.anonymous => "" -| Name.mkNumeral p _ => modNameToFileName p +| Name.str Name.anonymous h => h +| Name.str p h => modNameToFileName p ++ pathSep ++ h +| Name.anonymous => "" +| Name.num p _ => modNameToFileName p def addRel (baseDir : String) : Nat → String | 0 => baseDir @@ -117,7 +117,7 @@ do path ← findAtSearchPath fname; let modNameStr := fnameSuffix.extract 0 extPos; let extStr := fnameSuffix.extract (extPos + 1) fnameSuffix.bsize; let parts := modNameStr.splitOn pathSep; - let modName := parts.foldl Name.mkString Name.anonymous; + let modName := parts.foldl mkNameStr Name.anonymous; fname' ← findLeanFile modName extStr; unless (fname == fname') $ throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, module name '" ++ toString modName ++ "' resolves to '" ++ fname' ++ "'")); pure modName diff --git a/library/Init/Lean/Scopes.lean b/library/Init/Lean/Scopes.lean index 9c67595bd5..21aa40a4cb 100644 --- a/library/Init/Lean/Scopes.lean +++ b/library/Init/Lean/Scopes.lean @@ -93,8 +93,8 @@ if env.getNamespaceSet.contains n then env else scopeManagerExt.addEntry env n @[export lean_register_namespace] def registerNamespace : Environment → Name → Environment -| env, n@(Name.mkString p _) => registerNamespace (registerNamespaceAux env n) p -| env, _ => env +| env, n@(Name.str p _) => registerNamespace (registerNamespaceAux env n) p +| env, _ => env def pushScopeCore (env : Environment) (header : Name) (isNamespace : Bool) : Environment := let ns := env.getNamespace; diff --git a/library/Init/Lean/ToExpr.lean b/library/Init/Lean/ToExpr.lean index 347da75a77..3c2e95023e 100644 --- a/library/Init/Lean/ToExpr.lean +++ b/library/Init/Lean/ToExpr.lean @@ -21,9 +21,9 @@ instance natToExpr : ToExpr Nat := ⟨mkNatLit⟩ instance strToExpr : ToExpr String := ⟨mkStrLit⟩ def nameToExprAux : Name → Expr -| Name.anonymous => mkConst `Lean.Name.anonymous -| Name.mkString p s => mkCAppB `Lean.Name.mkString (nameToExprAux p) (toExpr s) -| Name.mkNumeral p n => mkCAppB `Lean.Name.mkNumeral (nameToExprAux p) (toExpr n) +| Name.anonymous => mkConst `Lean.Name.anonymous +| Name.str p s => mkCAppB `Lean.mkNameStr (nameToExprAux p) (toExpr s) +| Name.num p n => mkCAppB `Lean.mkNameNum (nameToExprAux p) (toExpr n) instance nameToExpr : ToExpr Name := ⟨nameToExprAux⟩ diff --git a/library/Init/Lean/Trace.lean b/library/Init/Lean/Trace.lean index fb32a21b07..eb71293607 100644 --- a/library/Init/Lean/Trace.lean +++ b/library/Init/Lean/Trace.lean @@ -106,8 +106,8 @@ namespace SimpleMonadTracerAdapter variables {m : Type → Type} [Monad m] [SimpleMonadTracerAdapter m] private def checkTraceOptionAux (opts : Options) : Name → Bool -| n@(Name.mkString p _) => opts.getBool n || (!opts.contains n && checkTraceOptionAux p) -| _ => false +| n@(Name.str p _) => opts.getBool n || (!opts.contains n && checkTraceOptionAux p) +| _ => false private def checkTraceOption (optName : Name) : m Bool := do opts ← getOptions; diff --git a/library/Init/Lean/TypeClass/Context.lean b/library/Init/Lean/TypeClass/Context.lean index 50361c0226..b1f3c2b2db 100644 --- a/library/Init/Lean/TypeClass/Context.lean +++ b/library/Init/Lean/TypeClass/Context.lean @@ -31,15 +31,15 @@ abbrev ContextFn : Type → Type := EStateM ContextFail Context namespace Context def metaPrefix : Name := -mkSimpleName "_tc_meta" +`_tc_meta def alphaMetaPrefix : Name := -mkSimpleName "_tc_alpha" +`_tc_alpha -- Expressions def eMetaIdx : Expr → Option Nat -| Expr.mvar (Name.mkNumeral n idx) _ => guard (n == metaPrefix) *> pure idx +| Expr.mvar (Name.num n idx) _ => guard (n == metaPrefix) *> pure idx | _ => none def eIsMeta (e : Expr) : Bool := (eMetaIdx e).toBool @@ -48,7 +48,7 @@ def eNewMeta (type : Expr) : StateM Context Expr := do ctx ← get; let idx := ctx.eTypes.size; set { eTypes := ctx.eTypes.push type, eVals := ctx.eVals.push none, .. ctx }; - pure $ mkMVar (mkNumName metaPrefix idx) + pure $ mkMVar (mkNameNum metaPrefix idx) def eLookupIdx (idx : Nat) : StateM Context (Option Expr) := do ctx ← get; pure $ ctx.eVals.get! idx @@ -97,7 +97,7 @@ eFind eIsMeta e -- Levels def uMetaIdx : Level → Option Nat -| Level.mvar (Name.mkNumeral n idx) _ => guard (n == metaPrefix) *> pure idx +| Level.mvar (Name.num n idx) _ => guard (n == metaPrefix) *> pure idx | _ => none def uIsMeta (l : Level) : Bool := (uMetaIdx l).toBool @@ -106,7 +106,7 @@ def uNewMeta : StateM Context Level := do ctx ← get; let idx := ctx.uVals.size; set { uVals := ctx.uVals.push none, .. ctx }; - pure $ mkLevelMVar (mkNumName metaPrefix idx) + pure $ mkLevelMVar (mkNameNum metaPrefix idx) def uLookupIdx (idx : Nat) : StateM Context (Option Level) := do ctx ← get; pure $ ctx.uVals.get! idx @@ -312,15 +312,15 @@ partial def eMetaNormalizeCore {α : Type} (fs : MetaNormFuncs α) : Expr → St def αNorm (e : Expr) : Expr := let fs : MetaNormFuncs Unit := { uNewMeta := λ idx => do { - l ← get >>= λ ϕ => pure $ mkLevelMVar (mkNumName alphaMetaPrefix ϕ.uRenameMap.size); + l ← get >>= λ ϕ => pure $ mkLevelMVar (mkNameNum alphaMetaPrefix ϕ.uRenameMap.size); modify $ λ ϕ => { uRenameMap := ϕ.uRenameMap.insert idx ϕ.uRenameMap.size .. ϕ }; pure l }, - uMkMeta := λ idx => pure $ mkLevelMVar (mkNumName alphaMetaPrefix idx), + uMkMeta := λ idx => pure $ mkLevelMVar (mkNameNum alphaMetaPrefix idx), eNewMeta := λ idx => do { - e ← get >>= λ ϕ => pure $ mkMVar (mkNumName alphaMetaPrefix ϕ.eRenameMap.size); + e ← get >>= λ ϕ => pure $ mkMVar (mkNameNum alphaMetaPrefix ϕ.eRenameMap.size); modify $ λ ϕ => { eRenameMap := ϕ.eRenameMap.insert idx ϕ.eRenameMap.size .. ϕ }; pure e }, - eMkMeta := λ idx => pure $ mkMVar (mkNumName alphaMetaPrefix idx) + eMkMeta := λ idx => pure $ mkMVar (mkNameNum alphaMetaPrefix idx) }; (eMetaNormalizeCore fs e).run' { ctx := () } @@ -333,7 +333,7 @@ let fs : MetaNormFuncs (Context × Context) := { | some newIdx => modify $ λ ϕ => { ctx := (oldCtx, newCtx), uRenameMap := ϕ.uRenameMap.insert idx newIdx, .. ϕ } | none => panic "unreachable"; pure l }, - uMkMeta := λ idx => pure $ mkLevelMVar (mkNumName metaPrefix idx), + uMkMeta := λ idx => pure $ mkLevelMVar (mkNameNum metaPrefix idx), eNewMeta := λ idx => do { (oldCtx, newCtx) ← get >>= λ ϕ => pure ϕ.ctx; (e, newCtx) ← pure $ StateT.run (Context.eNewMeta $ oldCtx.eTypes.get! idx) newCtx; @@ -341,7 +341,7 @@ let fs : MetaNormFuncs (Context × Context) := { | some newIdx => modify $ λ ϕ => { ctx := (oldCtx, newCtx), eRenameMap := ϕ.eRenameMap.insert idx newIdx, .. ϕ } | none => panic "unreachable"; pure e }, - eMkMeta := λ idx => pure $ mkMVar (mkNumName metaPrefix idx) + eMkMeta := λ idx => pure $ mkMVar (mkNameNum metaPrefix idx) }; match (do newType ← eMetaNormalizeCore fs type; newVal ← eMetaNormalizeCore fs val; pure (newVal, newType)).run { ctx := (oldCtx, newCtx) } with | ((newVal, newType), ϕ) => (newVal, newType, ϕ.ctx.2) diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean index 2ca519e214..0c5afd35cd 100644 --- a/library/Init/Lean/TypeClass/Synth.lean +++ b/library/Init/Lean/TypeClass/Synth.lean @@ -140,7 +140,7 @@ partial def introduceMVars (lctx : LocalContext) (locals : Array Expr) : Context partial def introduceLocals : Nat → LocalContext → Array Expr → Expr → LocalContext × Expr × Array Expr | nextIdx, lctx, ls, Expr.forallE name domain body c => let info := c.binderInfo; - let idxName : Name := mkNumName (mkSimpleName "_tmp") nextIdx; + let idxName : Name := mkNameNum `_tmp nextIdx; let lctx := lctx.mkLocalDecl idxName name domain info; let l : Expr := mkFVar idxName; introduceLocals (nextIdx + 1) lctx (ls.push l) (body.instantiate1 l) diff --git a/library/Init/Lean/WHNF.lean b/library/Init/Lean/WHNF.lean index 926ae8bcc2..cb77522eff 100644 --- a/library/Init/Lean/WHNF.lean +++ b/library/Init/Lean/WHNF.lean @@ -15,7 +15,7 @@ namespace Lean def smartUnfoldingSuffix := "_sunfold" @[inline] def mkSmartUnfoldingNameFor (n : Name) : Name := -Name.mkString n smartUnfoldingSuffix +mkNameStr n smartUnfoldingSuffix /- =========================== Helper functions diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 33b5d97ae9..82d7d090c4 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1527,7 +1527,8 @@ struct to_pattern_fn { buffer args; get_app_args(e, args); args[0] = fix_quoted_name(args[0]); - return mk_app(mk_constant(get_lean_name_mk_string_name()), args); +// return mk_app(mk_constant(get_lean_name_str_name()), args); + return mk_app(mk_constant(name{"Lean", "Name", "mkString"}), args); } expr fix_quoted_names(expr const & e) { diff --git a/src/library/constants.cpp b/src/library/constants.cpp index a526c40d2c..5b508477bd 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -116,8 +116,8 @@ name const * g_monad = nullptr; name const * g_monad_fail = nullptr; name const * g_lean_name = nullptr; name const * g_lean_name_anonymous = nullptr; -name const * g_lean_name_mk_numeral = nullptr; -name const * g_lean_name_mk_string = nullptr; +name const * g_lean_name_num = nullptr; +name const * g_lean_name_str = nullptr; name const * g_lean_mk_name_num = nullptr; name const * g_lean_mk_name_str = nullptr; name const * g_lean_parser_leading_node = nullptr; @@ -305,8 +305,8 @@ void initialize_constants() { g_monad_fail = new name{"MonadFail"}; g_lean_name = new name{"Lean", "Name"}; g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"}; - g_lean_name_mk_numeral = new name{"Lean", "Name", "mkNumeral"}; - g_lean_name_mk_string = new name{"Lean", "Name", "mkString"}; + g_lean_name_num = new name{"Lean", "Name", "num"}; + g_lean_name_str = new name{"Lean", "Name", "str"}; g_lean_mk_name_num = new name{"Lean", "mkNameNum"}; g_lean_mk_name_str = new name{"Lean", "mkNameStr"}; g_lean_parser_leading_node = new name{"Lean", "Parser", "leadingNode"}; @@ -495,8 +495,8 @@ void finalize_constants() { delete g_monad_fail; delete g_lean_name; delete g_lean_name_anonymous; - delete g_lean_name_mk_numeral; - delete g_lean_name_mk_string; + delete g_lean_name_num; + delete g_lean_name_str; delete g_lean_mk_name_num; delete g_lean_mk_name_str; delete g_lean_parser_leading_node; @@ -684,8 +684,8 @@ name const & get_monad_name() { return *g_monad; } name const & get_monad_fail_name() { return *g_monad_fail; } name const & get_lean_name_name() { return *g_lean_name; } name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; } -name const & get_lean_name_mk_numeral_name() { return *g_lean_name_mk_numeral; } -name const & get_lean_name_mk_string_name() { return *g_lean_name_mk_string; } +name const & get_lean_name_num_name() { return *g_lean_name_num; } +name const & get_lean_name_str_name() { return *g_lean_name_str; } name const & get_lean_mk_name_num_name() { return *g_lean_mk_name_num; } name const & get_lean_mk_name_str_name() { return *g_lean_mk_name_str; } name const & get_lean_parser_leading_node_name() { return *g_lean_parser_leading_node; } diff --git a/src/library/constants.h b/src/library/constants.h index 73d5934b65..329194664d 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -118,8 +118,8 @@ name const & get_monad_name(); name const & get_monad_fail_name(); name const & get_lean_name_name(); name const & get_lean_name_anonymous_name(); -name const & get_lean_name_mk_numeral_name(); -name const & get_lean_name_mk_string_name(); +name const & get_lean_name_num_name(); +name const & get_lean_name_str_name(); name const & get_lean_mk_name_num_name(); name const & get_lean_mk_name_str_name(); name const & get_lean_parser_leading_node_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 66f7a6e47f..f51defdb79 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -111,8 +111,8 @@ Monad MonadFail Lean.Name Lean.Name.anonymous -Lean.Name.mkNumeral -Lean.Name.mkString +Lean.Name.num +Lean.Name.str Lean.mkNameNum Lean.mkNameStr Lean.Parser.leadingNode diff --git a/src/library/util.cpp b/src/library/util.cpp index 07a60fe78b..cd64296fe4 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -1009,12 +1009,12 @@ optional is_unsafe_rec_name(name const & n) { optional name_lit_to_name(expr const & name_lit) { if (is_constant(name_lit, get_lean_name_anonymous_name())) return optional(name()); - if (is_app_of(name_lit, get_lean_name_mk_string_name(), 2)) { + if (is_app_of(name_lit, get_lean_name_str_name(), 2)) { if (auto p = name_lit_to_name(app_arg(app_fn(name_lit)))) if (auto str = to_string(app_arg(name_lit))) return optional(name(*p, str->c_str())); } - if (is_app_of(name_lit, get_lean_name_mk_numeral_name(), 2)) { + if (is_app_of(name_lit, get_lean_name_num_name(), 2)) { if (auto p = name_lit_to_name(app_arg(app_fn(name_lit)))) if (auto n = to_num(app_arg(name_lit))) return optional(name(*p, n->get_unsigned_int()));