chore: remove support for Lean3 scopes
This commit is contained in:
Leonardo de Moura
parent
e1c3c55027
commit
deb283a415
3 changed files with 0 additions and 205 deletions
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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}'"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue