max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: disable attribute features that are not currently being used

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-08 15:44:29 -08:00
parent 680ac55506
commit fe09e99fef
2 changed files with 26 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/Init/Lean/Attributes.lean
View file

@ -27,6 +27,7 @@ structure AttributeImpl :=
(name : Name)
(descr : String)
(add (env : Environment) (decl : Name) (args : Syntax) (persistent : Bool) : IO Environment)
/-
(addScoped (env : Environment) (decl : Name) (args : Syntax) : IO Environment
:= throw (IO.userError ("attribute '" ++ toString name ++ "' does not support scopes")))
(erase (env : Environment) (decl : Name) (persistent : Bool) : IO Environment
@ -34,6 +35,7 @@ structure AttributeImpl :=
(activateScoped (env : Environment) (scope : Name) : IO Environment := pure env)
(pushScope (env : Environment) : IO Environment := pure env)
(popScope (env : Environment) : IO Environment := pure env)
-/
(applicationTime := AttributeApplicationTime.afterTypeChecking)
/- Auxiliary function for parsing attribute arguments -/
@ -44,17 +46,11 @@ def Syntax.hasArgs : Syntax → Bool
instance AttributeImpl.inhabited : Inhabited AttributeImpl :=
⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure env }⟩
def mkAttributeMapRef : IO (IO.Ref (HashMap Name AttributeImpl)) :=
def mkAttributeMapRef : IO (IO.Ref (PersistentHashMap Name AttributeImpl)) :=
IO.mkRef {}
@[init mkAttributeMapRef]
constant attributeMapRef : IO.Ref (HashMap Name AttributeImpl) := arbitrary _
def mkAttributeArrayRef : IO (IO.Ref (Array AttributeImpl)) :=
IO.mkRef #[]
@[init mkAttributeArrayRef]
constant attributeArrayRef : IO.Ref (Array AttributeImpl) := arbitrary _
constant attributeMapRef : IO.Ref (PersistentHashMap Name AttributeImpl) := arbitrary _
/- Low level attribute registration function. -/
def registerAttribute (attr : AttributeImpl) : IO Unit := do
@ -62,8 +58,7 @@ m ← attributeMapRef.get;
when (m.contains attr.name) $ throw (IO.userError ("invalid attribute declaration, '" ++ toString attr.name ++ "' has already been used"));
initializing ← IO.initializing;
unless initializing $ throw (IO.userError ("failed to register attribute, attributes can only be registered during initialization"));
attributeMapRef.modify (fun m => m.insert attr.name attr);
attributeArrayRef.modify (fun attrs => attrs.push attr)
attributeMapRef.modify (fun m => m.insert attr.name attr)
/- Return true iff `n` is the name of a registered attribute. -/
@[export lean_is_attribute]
@ -72,7 +67,7 @@ m ← attributeMapRef.get; pure (m.contains n)
/- Return the name of all registered attributes. -/
def getAttributeNames : IO (List Name) := do
m ← attributeMapRef.get; pure $ m.fold (fun r n _ => n::r) []
m ← attributeMapRef.get; pure $ m.foldl (fun r n _ => n::r) []
def getAttributeImpl (attrName : Name) : IO AttributeImpl := do
m ← attributeMapRef.get;
@ -97,6 +92,7 @@ def addAttribute (env : Environment) (decl : Name) (attrName : Name) (args : Syn
attr ← getAttributeImpl attrName;
attr.add env decl args persistent
/-
/- 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
@ -132,6 +128,7 @@ attr.activateScoped env scope
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. -/
@ -139,15 +136,17 @@ attrs.foldlM (fun env attr => attr.activateScoped env scope) env
def pushScope (env : Environment) (header : Name) (isNamespace : Bool) : IO Environment := do
let env := env.pushScopeCore header isNamespace;
let ns := env.getNamespace;
attrs ← attributeArrayRef.get;
attrs.foldlM (fun env attr => do env ← attr.pushScope env; if isNamespace then attr.activateScoped env ns else pure env) env
-- 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 := env.popScopeCore;
attrs ← attributeArrayRef.get;
attrs.foldlM (fun env attr => attr.popScope env) env
-- attrs ← attributeArrayRef.get;
-- attrs.foldlM (fun env attr => attr.popScope env) env
pure env
end Environment

22
src/frontends/lean/decl_attributes.cpp
View file

@ -24,8 +24,8 @@ namespace lean {
extern "C" object* lean_is_attribute(object* n, object* w);
extern "C" object* lean_attribute_application_time(object* n, object* w);
extern "C" object* lean_add_attribute(object* env, object* decl, object* attr, object* args, uint8 persistent, object *w);
extern "C" object* lean_add_scoped_attribute(object* env, object* decl, object* attr, object* args, object *w);
extern "C" object* lean_erase_attribute(object* env, object* decl, object* attr, uint8 persistent, object *w);
// extern "C" object* lean_add_scoped_attribute(object* env, object* decl, object* attr, object* args, object *w);
// extern "C" object* lean_erase_attribute(object* env, object* decl, object* attr, uint8 persistent, object *w);
bool is_new_attribute(name const & n) {
return get_io_scalar_result<bool>(lean_is_attribute(n.to_obj_arg(), io_mk_world()));
@ -33,12 +33,12 @@ bool is_new_attribute(name const & n) {
environment add_attribute(environment const & env, name const & decl, name const & attr, syntax const & args, bool persistent) {
return get_io_result<environment>(lean_add_attribute(env.to_obj_arg(), decl.to_obj_arg(), attr.to_obj_arg(), args.to_obj_arg(), persistent, io_mk_world()));
}
environment add_scoped_attribute(environment const & env, name const & decl, name const & attr, syntax const & args) {
return get_io_result<environment>(lean_add_scoped_attribute(env.to_obj_arg(), decl.to_obj_arg(), attr.to_obj_arg(), args.to_obj_arg(), io_mk_world()));
}
environment erase_attribute(environment const & env, name const & decl, name const & attr, bool persistent) {
return get_io_result<environment>(lean_erase_attribute(env.to_obj_arg(), decl.to_obj_arg(), attr.to_obj_arg(), persistent, io_mk_world()));
}
// environment add_scoped_attribute(environment const & env, name const & decl, name const & attr, syntax const & args) {
// return get_io_result<environment>(lean_add_scoped_attribute(env.to_obj_arg(), decl.to_obj_arg(), attr.to_obj_arg(), args.to_obj_arg(), io_mk_world()));
// }
// environment erase_attribute(environment const & env, name const & decl, name const & attr, bool persistent) {
// return get_io_result<environment>(lean_erase_attribute(env.to_obj_arg(), decl.to_obj_arg(), attr.to_obj_arg(), persistent, io_mk_world()));
// }
/*
inductive AttributeApplicationTime
| afterTypeChecking | afterCompilation | beforeElaboration
@ -216,9 +216,11 @@ environment decl_attributes::apply_new_entries(environment env, list<new_entry>
--i;
auto const & entry = new_entries[i];
if (entry.m_deleted) {
env = erase_attribute(env, d, entry.m_attr, m_persistent);
// env = erase_attribute(env, d, entry.m_attr, m_persistent);
throw exception("attribute erasure has not been implemented yet");
} else if (entry.m_scoped) {
env = add_scoped_attribute(env, d, entry.m_attr, entry.m_args);
// env = add_scoped_attribute(env, d, entry.m_attr, entry.m_args);
throw exception("scoped attributes have not been implemented yet");
} else {
env = add_attribute(env, d, entry.m_attr, entry.m_args, m_persistent);
}