feat(library/init/lean): add protected extension

library/init/lean/default.lean

@@ -8,3 +8,4 @@ import init.lean.compiler
 import init.lean.frontend
 import init.lean.extern
 import init.lean.environment
+import init.lean.modifiers

library/init/lean/environment.lean

@@ -158,18 +158,20 @@ structure PersistentEnvExtension (α : Type) (σ : Type) extends EnvExtension (P
 (someVal    : α)
 (addEntryFn : Bool → σ → α → σ)
 (toArrayFn  : List α → Array α)
+(lazy       : Bool)
 
 /- Opaque persistent environment extension entry. It is essentially a C `void *`
    TODO: mark opaque -/
 @[derive Inhabited]
 def EnvExtensionEntry := NonScalar
 
-instance PersistentEnvExtensionState.inhabited : Inhabited (PersistentEnvExtensionState EnvExtensionEntry EnvExtensionState) :=
+instance PersistentEnvExtensionState.inhabited {α σ} [Inhabited α] [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
 ⟨{importedEntries := Array.empty, importedState := Thunk.pure (default _) }⟩
 
-instance PersistentEnvExtension.inhabited : Inhabited (PersistentEnvExtension EnvExtensionEntry EnvExtensionState) :=
+instance PersistentEnvExtension.inhabited {α σ} [Inhabited α] [Inhabited σ] : Inhabited (PersistentEnvExtension α σ) :=
 ⟨{ toEnvExtension := { idx := 0, initial := default _ },
-   name := default _, someVal := default _, addEntryFn := λ _ s _, s, toArrayFn := λ es, es.toArray }⟩
+   name  := default _, someVal := default _, addEntryFn := λ _ s _, s, toArrayFn := λ es, es.toArray,
+   lazy  := true }⟩
 
 namespace PersistentEnvExtension
 
@@ -205,7 +207,7 @@ IO.mkRef Array.empty
 @[init mkPersistentEnvExtensionsRef]
 private constant persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionState)) := default _
 
-unsafe def registerPersistentEnvExtensionUnsafe {α σ : Type} (name : Name) (initState : σ) (someVal : α) (addEntryFn : Bool → σ → α → σ) (toArrayFn : List α → Array α) : IO (PersistentEnvExtension α σ) :=
+unsafe def registerPersistentEnvExtensionUnsafe {α σ : Type} (name : Name) (initState : σ) (someVal : α) (addEntryFn : Bool → σ → α → σ) (toArrayFn : List α → Array α := λ as, as.toArray) (lazy := true) : IO (PersistentEnvExtension α σ) :=
 do
 let s : PersistentEnvExtensionState α σ := {
   importedEntries := Array.empty,
@@ -220,13 +222,14 @@ let pExt : PersistentEnvExtension α σ := {
   name           := name,
   someVal        := someVal,
   addEntryFn     := addEntryFn,
-  toArrayFn      := toArrayFn
+  toArrayFn      := toArrayFn,
+  lazy           := lazy
 },
 persistentEnvExtensionsRef.modify (λ pExts, pExts.push (unsafeCast pExt)),
 pure pExt
 
 @[implementedBy registerPersistentEnvExtensionUnsafe]
-constant registerPersistentEnvExtension {α σ : Type} (name : Name) (initState : σ) (someVal : α) (addEntryFn : Bool → σ → α → σ) (toArrayFn : List α → Array α) : IO (PersistentEnvExtension α σ) := default _
+constant registerPersistentEnvExtension {α σ : Type} (name : Name) (initState : σ) (someVal : α) (addEntryFn : Bool → σ → α → σ) (toArrayFn : List α → Array α := λ as, as.toArray) (lazy := true) : IO (PersistentEnvExtension α σ) := default _
 
 /- API for creating extensions in C++.
    This API will eventually be deleted. -/
@@ -363,9 +366,10 @@ do
 pExtDescrs ← persistentEnvExtensionsRef.get,
 pure $ pExtDescrs.iterate env $ λ _ extDescr env,
   extDescr.toEnvExtension.modifyState env $ λ s,
-    { importedState := mkImportedStateThunk s.importedEntries extDescr.initial.importedState.get extDescr.addEntryFn,
-      entries := [],
-      state   := none,
+    let importedState : Thunk EnvExtensionState := mkImportedStateThunk s.importedEntries extDescr.initial.importedState.get extDescr.addEntryFn in
+    { importedState := importedState,
+      entries       := [],
+      state         := if extDescr.lazy then none else some importedState.get,
       .. s }
 
 @[export lean.import_modules_core]

library/init/lean/modifiers.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.lean.environment
+
+namespace Lean
+
+def mkProtectedExtension : IO (PersistentEnvExtension Name NameSet) :=
+registerPersistentEnvExtension `protected {} Name.anonymous (λ _ s n, s.insert n) (λ ns, ns.toArray) false
+
+@[init mkProtectedExtension]
+constant protectedExt : PersistentEnvExtension Name NameSet := default _
+
+@[export lean.add_protected_core]
+def addProtected (env : Environment) (n : Name) : Environment :=
+protectedExt.addEntry env n
+
+@[export lean.is_protected_core]
+def isProtected (env : Environment) (n : Name) : Bool :=
+(protectedExt.getState env).contains n
+
+end Lean

src/stage0/CMakeLists.txt

@@ -1 +1 @@
-add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/environment.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/stringliteral.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/smap.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
+add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/environment.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/stringliteral.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/smap.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)

src/stage0/init/lean/default.cpp

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.default
-// Imports: init.lean.compiler.default init.lean.frontend init.lean.extern init.lean.environment
+// Imports: init.lean.compiler.default init.lean.frontend init.lean.extern init.lean.environment init.lean.modifiers
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -18,6 +18,7 @@ obj* initialize_init_lean_compiler_default(obj*);
 obj* initialize_init_lean_frontend(obj*);
 obj* initialize_init_lean_extern(obj*);
 obj* initialize_init_lean_environment(obj*);
+obj* initialize_init_lean_modifiers(obj*);
 static bool _G_initialized = false;
 obj* initialize_init_lean_default(obj* w) {
  if (_G_initialized) return w;
@@ -31,5 +32,7 @@ w = initialize_init_lean_extern(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_environment(w);
 if (io_result_is_error(w)) return w;
+w = initialize_init_lean_modifiers(w);
+if (io_result_is_error(w)) return w;
 return w;
 }

src/stage0/init/lean/modifiers.cpp

@@ -0,0 +1,190 @@
+// Lean compiler output
+// Module: init.lean.modifiers
+// Imports: init.lean.environment
+#include "runtime/object.h"
+#include "runtime/apply.h"
+typedef lean::object obj;    typedef lean::usize  usize;
+typedef lean::uint8  uint8;  typedef lean::uint16 uint16;
+typedef lean::uint32 uint32; typedef lean::uint64 uint64;
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+extern obj* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__2;
+namespace lean {
+obj* add_protected_core(obj*, obj*);
+}
+obj* l_List_toArrayAux___main___rarg(obj*, obj*);
+obj* l_Lean_mkProtectedExtension___lambda__1(uint8, obj*, obj*);
+obj* l_List_redLength___main___rarg(obj*);
+obj* l_Lean_isProtected___boxed(obj*, obj*);
+obj* l_Lean_mkProtectedExtension___closed__2;
+obj* l_Lean_protectedExt___elambda__1(obj*);
+uint8 l_Lean_NameSet_contains(obj*, obj*);
+obj* l_RBNode_insert___at_Lean_NameSet_insert___spec__1(obj*, obj*, obj*);
+obj* l_Lean_PersistentEnvExtension_getState___rarg(obj*, obj*);
+obj* l_Lean_mkProtectedExtension___closed__1;
+extern "C" obj* lean_name_mk_string(obj*, obj*);
+obj* l_Lean_protectedExt;
+obj* l_Lean_mkProtectedExtension___lambda__1___boxed(obj*, obj*, obj*);
+obj* l_Lean_protectedExt___elambda__2___rarg(obj*, obj*);
+obj* l_Lean_protectedExt___elambda__2(uint8);
+obj* l_Lean_PersistentEnvExtension_addEntry___rarg(obj*, obj*, obj*);
+namespace lean {
+uint8 is_protected_core(obj*, obj*);
+}
+obj* l_Lean_mkProtectedExtension(obj*);
+obj* l_Lean_registerPersistentEnvExtensionUnsafe___rarg(obj*, obj*, obj*, obj*, obj*, uint8, obj*);
+obj* l_Lean_protectedExt___elambda__2___boxed(obj*);
+obj* l_Lean_protectedExt___elambda__2___rarg___boxed(obj*, obj*);
+obj* l_Lean_mkProtectedExtension___lambda__1(uint8 x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; obj* x_4; 
+x_3 = lean::box(0);
+x_4 = l_RBNode_insert___at_Lean_NameSet_insert___spec__1(x_1, x_2, x_3);
+return x_4;
+}
+}
+obj* _init_l_Lean_mkProtectedExtension___closed__1() {
+_start:
+{
+obj* x_0; obj* x_1; obj* x_2; 
+x_0 = lean::box(0);
+x_1 = lean::mk_string("protected");
+x_2 = lean_name_mk_string(x_0, x_1);
+return x_2;
+}
+}
+obj* _init_l_Lean_mkProtectedExtension___closed__2() {
+_start:
+{
+obj* x_0; 
+x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_mkProtectedExtension___lambda__1___boxed), 3, 0);
+return x_0;
+}
+}
+obj* l_Lean_mkProtectedExtension(obj* x_0) {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; uint8 x_6; obj* x_7; 
+x_1 = lean::box(0);
+x_2 = l_Lean_mkProtectedExtension___closed__1;
+x_3 = lean::box(0);
+x_4 = l_Lean_mkProtectedExtension___closed__2;
+x_5 = l_Lean_PersistentEnvExtension_inhabited___rarg___closed__2;
+x_6 = 0;
+x_7 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg(x_2, x_1, x_3, x_4, x_5, x_6, x_0);
+return x_7;
+}
+}
+obj* l_Lean_mkProtectedExtension___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+uint8 x_3; obj* x_4; 
+x_3 = lean::unbox(x_0);
+x_4 = l_Lean_mkProtectedExtension___lambda__1(x_3, x_1, x_2);
+return x_4;
+}
+}
+obj* l_Lean_protectedExt___elambda__1(obj* x_0) {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_4; 
+x_1 = l_List_redLength___main___rarg(x_0);
+x_2 = lean::mk_empty_array(x_1);
+lean::dec(x_1);
+x_4 = l_List_toArrayAux___main___rarg(x_0, x_2);
+return x_4;
+}
+}
+obj* l_Lean_protectedExt___elambda__2___rarg(obj* x_0, obj* x_1) {
+_start:
+{
+lean::inc(x_0);
+return x_0;
+}
+}
+obj* l_Lean_protectedExt___elambda__2(uint8 x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_protectedExt___elambda__2___rarg___boxed), 2, 0);
+return x_1;
+}
+}
+obj* l_Lean_protectedExt___elambda__2___rarg___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Lean_protectedExt___elambda__2___rarg(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_Lean_protectedExt___elambda__2___boxed(obj* x_0) {
+_start:
+{
+uint8 x_1; obj* x_2; 
+x_1 = lean::unbox(x_0);
+x_2 = l_Lean_protectedExt___elambda__2(x_1);
+return x_2;
+}
+}
+namespace lean {
+obj* add_protected_core(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; 
+x_2 = l_Lean_protectedExt;
+x_3 = l_Lean_PersistentEnvExtension_addEntry___rarg(x_2, x_0, x_1);
+return x_3;
+}
+}
+}
+namespace lean {
+uint8 is_protected_core(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; uint8 x_5; 
+x_2 = l_Lean_protectedExt;
+x_3 = l_Lean_PersistentEnvExtension_getState___rarg(x_2, x_0);
+lean::dec(x_0);
+x_5 = l_Lean_NameSet_contains(x_3, x_1);
+lean::dec(x_1);
+return x_5;
+}
+}
+}
+obj* l_Lean_isProtected___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+uint8 x_2; obj* x_3; 
+x_2 = lean::is_protected_core(x_0, x_1);
+x_3 = lean::box(x_2);
+return x_3;
+}
+}
+obj* initialize_init_lean_environment(obj*);
+static bool _G_initialized = false;
+obj* initialize_init_lean_modifiers(obj* w) {
+ if (_G_initialized) return w;
+ _G_initialized = true;
+if (io_result_is_error(w)) return w;
+w = initialize_init_lean_environment(w);
+if (io_result_is_error(w)) return w;
+ l_Lean_mkProtectedExtension___closed__1 = _init_l_Lean_mkProtectedExtension___closed__1();
+lean::mark_persistent(l_Lean_mkProtectedExtension___closed__1);
+ l_Lean_mkProtectedExtension___closed__2 = _init_l_Lean_mkProtectedExtension___closed__2();
+lean::mark_persistent(l_Lean_mkProtectedExtension___closed__2);
+w = l_Lean_mkProtectedExtension(w);
+if (io_result_is_error(w)) return w;
+ l_Lean_protectedExt = io_result_get_value(w);
+lean::mark_persistent(l_Lean_protectedExt);
+return w;
+}