From deb283a415392913152b07fa130590f95221eba6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Oct 2020 08:20:05 -0700 Subject: [PATCH] chore: remove support for Lean3 scopes --- src/Lean/Attributes.lean | 74 ------------------------- src/Lean/Elab/Util.lean | 14 ----- src/Lean/Scopes.lean | 117 --------------------------------------- 3 files changed, 205 deletions(-) delete mode 100644 src/Lean/Scopes.lean diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 24c24127d2..063990fa0a 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -3,7 +3,6 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ -import Lean.Scopes import Lean.Syntax import Lean.CoreM import Lean.ResolveName @@ -178,84 +177,11 @@ def registerAttributeOfBuilder (env : Environment) (builderId : Name) (args : Li else pure $ attributeExtension.addEntry env (AttributeExtensionOLeanEntry.builder builderId args, attrImpl) -namespace Environment - -/- Add attribute `attr` to declaration `decl` with arguments `args`. If `persistent == true`, then attribute is saved on .olean file. - It throws an error when - - `attr` is not the name of an attribute registered in the system. - - `attr` does not support `persistent == false`. - - `args` is not valid for `attr`. - - TODO: delete after we remove old frontend. -/ -@[export lean_add_attribute] -def addAttributeOld (env : Environment) (decl : Name) (attrName : Name) (args : Syntax := Syntax.missing) (persistent := true) : IO Environment := do - let attr ← IO.ofExcept $ getAttributeImpl env attrName - let (_, s) ← ((attr.add decl args persistent).run { currNamespace := Name.anonymous, openDecls := [] }).toIO {} { env := env } - pure s.env - -/- -/- Add a scoped attribute `attr` to declaration `decl` with arguments `args` and scope `decl.getPrefix`. - Scoped attributes are always persistent. - It returns `Except.error` when - - `attr` is not the name of an attribute registered in the system. - - `attr` does not support scoped attributes. - - `args` is not valid for `attr`. - - Remark: the attribute will not be activated if `decl` is not inside the current namespace `env.getNamespace`. -/ -@[export lean_add_scoped_attribute] -def addScopedAttribute (env : Environment) (decl : Name) (attrName : Name) (args : Syntax := Syntax.missing) : IO Environment := do -attr ← getAttributeImpl attrName; -attr.addScoped env decl args - -/- Remove attribute `attr` from declaration `decl`. The effect is the current scope. - It returns `Except.error` when - - `attr` is not the name of an attribute registered in the system. - - `attr` does not support erasure. - - `args` is not valid for `attr`. -/ -@[export lean_erase_attribute] -def eraseAttribute (env : Environment) (decl : Name) (attrName : Name) (persistent := true) : IO Environment := do -attr ← getAttributeImpl attrName; -attr.erase env decl persistent - -/- Activate the scoped attribute `attr` for all declarations in scope `scope`. - We use this function to implement the command `open foo`. -/ -@[export lean_activate_scoped_attribute] -def activateScopedAttribute (env : Environment) (attrName : Name) (scope : Name) : IO Environment := do -attr ← getAttributeImpl attrName; -attr.activateScoped env scope - -/- Activate all scoped attributes at `scope` -/ -@[export lean_activate_scoped_attributes] -def activateScopedAttributes (env : Environment) (scope : Name) : IO Environment := do -attrs ← attributeArrayRef.get; -attrs.foldlM (fun env attr => attr.activateScoped env scope) env --/ - -/- We use this function to implement commands `namespace foo` and `section foo`. - It activates scoped attributes in the new resulting namespace. -/ -@[export lean_push_scope] -def pushScope (env : Environment) (header : Name) (isNamespace : Bool) : IO Environment := do - let env := Lean.TODELETE.pushScopeCore env header isNamespace - -- attrs ← attributeArrayRef.get; - -- attrs.foldlM (fun env attr => do env ← attr.pushScope env; if isNamespace then attr.activateScoped env ns else pure env) env - pure env - -/- We use this function to implement commands `end foo` for closing namespaces and sections. -/ -@[export lean_pop_scope] -def popScope (env : Environment) : IO Environment := do - let env := Lean.TODELETE.popScopeCore env - -- attrs ← attributeArrayRef.get; - -- attrs.foldlM (fun env attr => attr.popScope env) env - pure env - -end Environment - def addAttribute (decl : Name) (attrName : Name) (args : Syntax) (persistent : Bool := true) : AttrM Unit := do let env ← getEnv let attr ← ofExcept $ getAttributeImpl env attrName attr.add decl args persistent - /-- Tag attributes are simple and efficient. They are useful for marking declarations in the modules where they were defined. diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean index 1f74f7203d..9059d0de11 100644 --- a/src/Lean/Elab/Util.lean +++ b/src/Lean/Elab/Util.lean @@ -62,18 +62,6 @@ def checkSyntaxNodeKind (k : Name) : AttrM Name := do if Parser.isValidSyntaxNodeKind (← getEnv) k then pure k else throwError "failed" -namespace OldFrontend -- TODO: delete - -private def checkSyntaxNodeKindAtNamespacesAux (k : Name) : List Name → AttrM Name - | [] => throwError "failed" - | n::ns => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux k ns - -def checkSyntaxNodeKindAtNamespaces (k : Name) : AttrM Name := do - let env ← getEnv - checkSyntaxNodeKindAtNamespacesAux k (Lean.TODELETE.getNamespaces env) - -end OldFrontend - def checkSyntaxNodeKindAtNamespacesAux (k : Name) : Name → AttrM Name | n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux k p | _ => throwError "failed" @@ -89,8 +77,6 @@ def syntaxNodeKindOfAttrParam (defaultParserNamespace : Name) (arg : Syntax) : A <|> checkSyntaxNodeKindAtNamespaces k <|> - OldFrontend.checkSyntaxNodeKindAtNamespaces k -- TODO: delete the following old frontend support code - <|> checkSyntaxNodeKind (defaultParserNamespace ++ k) <|> throwError! "invalid syntax node kind '{k}'" diff --git a/src/Lean/Scopes.lean b/src/Lean/Scopes.lean deleted file mode 100644 index 9adffd6f63..0000000000 --- a/src/Lean/Scopes.lean +++ /dev/null @@ -1,117 +0,0 @@ -/- -Copyright (c) 2019 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -import Lean.Environment - -namespace Lean -namespace TODELETE - -/- Scope management - -TODO: delete after we delete parser implemented in C++. -We have decided to store scope information at ElabState --/ - -structure ScopeManagerState := -(allNamespaces : NameSet := {}) -/- Stack of namespaces for each each open namespace and section -/ -(namespaces : List Name := []) -/- Stack of namespace/section headers -/ -(headers : List Name := []) -(isNamespace : List Bool := []) - -namespace ScopeManagerState - -instance : Inhabited ScopeManagerState := ⟨{}⟩ - -def saveNamespace (s : ScopeManagerState) (n : Name) : ScopeManagerState := -{ s with allNamespaces := s.allNamespaces.insert n } - -end ScopeManagerState - -def regScopeManagerExtension : IO (SimplePersistentEnvExtension Name ScopeManagerState) := -registerSimplePersistentEnvExtension { - name := `scopes, - addImportedFn := fun as => mkStateFromImportedEntries ScopeManagerState.saveNamespace {} as, - addEntryFn := fun s n => { s with allNamespaces := s.allNamespaces.insert n }, -} - -@[builtinInit regScopeManagerExtension] -constant scopeManagerExt : SimplePersistentEnvExtension Name ScopeManagerState := arbitrary _ - -@[export lean_get_namespaces] -def getNamespaces (env : Environment) : List Name := -(scopeManagerExt.getState env).namespaces - -def getNamespaceSet (env : Environment) : NameSet := -(scopeManagerExt.getState env).allNamespaces - -@[export lean_is_namespace] -def isNamespace (env : Environment) (n : Name) : Bool := -(getNamespaceSet env).contains n - -@[export lean_in_section] -def inSection (env : Environment) : Bool := -match (scopeManagerExt.getState env).isNamespace with -| (b::_) => !b -| _ => false - -@[export lean_has_open_scopes] -def hasOpenScopes (env : Environment) : Bool := -!(getNamespaces env).isEmpty - -@[export lean_get_namespace] -def getNamespace (env : Environment) : Name := -match getNamespaces env with -| (n::_) => n -| _ => Name.anonymous - -@[export lean_get_scope_header] -def getScopeHeader (env : Environment) : Name := -match (scopeManagerExt.getState env).headers with -| (n::_) => n -| _ => Name.anonymous - -@[export lean_to_valid_namespace] -def toValidNamespace (env : Environment) (n : Name) : Option Name := -let s := scopeManagerExt.getState env; -if s.allNamespaces.contains n then some n -else s.namespaces.foldl - (fun r ns => match r with - | some _ => r - | none => - let c := ns ++ n; - if s.allNamespaces.contains c then some c else none) - none - -def registerNamespaceAux (env : Environment) (n : Name) : Environment := -if (getNamespaceSet env).contains n then env else scopeManagerExt.addEntry env n - -@[export lean_register_namespace] -def registerNamespace : Environment → Name → Environment -| env, n@(Name.str p _ _) => registerNamespace (registerNamespaceAux env n) p -| env, _ => env - -def pushScopeCore (env : Environment) (header : Name) (isNamespace : Bool) : Environment := -let ns := getNamespace env; -let newNs := if isNamespace then ns ++ header else ns; -let env := registerNamespaceAux env newNs; -let env := scopeManagerExt.modifyState env $ fun s => - { s with - headers := header :: s.headers, - namespaces := newNs :: s.namespaces, - isNamespace := isNamespace :: s.isNamespace }; -env - -def popScopeCore (env : Environment) : Environment := -if (getNamespaces env).isEmpty then env -else scopeManagerExt.modifyState env $ fun s => - { s with - headers := s.headers.tail!, - namespaces := s.namespaces.tail!, - isNamespace := s.isNamespace.tail! } - -end TODELETE -end Lean