chore(tests/playground/environment_ext): revert accidental commit

tests/playground/environment_ext.lean

@@ -1,34 +1,61 @@
 import init.Lean init.Lean.Parser.Syntax
 
 namespace Lean
-constant environmentExt (α σ : Type) : Type := Unit
-namespace environmentExt
-variables {α σ : Type}
-@[extern "lean_environment_ext_register"] constant register
-  (key : Option String)
-  (emptyState : σ)
-  (addEntry : Π (init : Bool), environment → σ → α → σ) :
-  IO (environmentExt α σ) := default _
+/-- An extension of the State held by an `environment` object. The new State
+    holds objects of Type `entryTy`, which optionally are persisted to the
+    .olean file and collected when loading imports. Objects can be retrieved
+    using an appropriate `stateTy` data structure, which is computed on-demand. -/
+constant environmentExt (entryTy stateTy : Type) : Type := Unit
 
-variables {β δ : Type}
+namespace environmentExt
+variables {entryTy stateTy : Type}
+/-- Register a new environment extension. The Result should usually be bound to
+    a top-Level definition, after which it can be used to access and modify the
+    extension State. -/
+@[extern "lean_environment_ext_register"] constant register
+  /- A unique String used for identifying persisted data of this extension. If
+     this key has already been used, the Lean process will halt with an error.
+     If the key is `none`, data of this extension will not be persisted, i.e. is
+     local to the current file. -/
+  (key : Option String)
+  /- initial cache value -/
+  (emptyState : stateTy)
+  /- Add an entry to the cache. `init` is `True` while building the initial
+     cache from the loaded imports, in which case the input cache may assumed to
+     be unshared and amenable to destructive updates. -/
+  (addEntry : Π (init : Bool), environment → stateTy → entryTy → stateTy) :
+  IO (environmentExt entryTy stateTy) := default _
+
+variables {entryTy' stateTy' : Type}
+
+/- Register a dependency between two environment extensions.
+   That is, whenever an entry `e` is added to `fromExt`,
+   Lean also adds an entry `convertEntry e` to `toExt`. -/
 @[extern "lean_environment_ext_register_dep"] constant registerDep
-   (fromExt : environmentExt α σ)
-   (toExt : environmentExt β δ)
-   (convertEntry : α → β)
+   (fromExt : environmentExt entryTy stateTy)
+   (toExt : environmentExt entryTy' stateTy')
+   (convertEntry : entryTy → entryTy')
    : IO Unit := default _
 
-@[extern "lean_environment_ext_add_entry"] constant addEntry (ext : environmentExt α σ) (persistent : Bool) (entry : α) : environment → environment := id
+@[extern "lean_environment_ext_add_entry"] constant addEntry (ext : environmentExt entryTy stateTy) (persistent : Bool) (entry : entryTy) : environment → environment := id
 
-@[extern "lean_environment_ext_get_state"] constant getState [Inhabited σ] : environmentExt α σ → environment → σ := default _
+/-- Retrieve the State of an environment extension. -/
+@[extern "lean_environment_ext_get_state"] constant getState [Inhabited stateTy] : environmentExt entryTy stateTy → environment → stateTy := default _
 end environmentExt
+
+/-- A datum as used by `attributeExt`. -/
 structure attributeEntry :=
 (Decl : Name)
 (args : Parser.Syntax)
 
-structure attributeExt (σ : Type) :=
-(activeExt : environmentExt attributeEntry σ)
+/-- The Result of registering an attribute in the global State. -/
+structure attributeExt (stateTy : Type) :=
+-- global and local attribute entries as well as "active" scoped entries
+(activeExt : environmentExt attributeEntry stateTy)
+-- all scoped entries
 (scopedExt : environmentExt attributeEntry (List attributeEntry))
 
+/-- `cacheTy`-oblivious attribute data available to the Elaborator. -/
 structure attributeInfo :=
 (attr : String)
 (addActiveEntry (persistent : Bool) : attributeEntry → environment → environment)
@@ -46,11 +73,11 @@ def attributesRef.init : IO (IO.ref (List attributeInfo)) := IO.mkRef []
 def attributes : IO (List attributeInfo) := attributesRef.read
 
 namespace attributeExt
-variable {σ : Type}
+variable {stateTy : Type}
 
-def register (attr : String) (emptyState : σ)
-  (addEntry : Π (init : Bool), environment → σ → attributeEntry → σ)
-  : IO (attributeExt σ) := do
+def register (attr : String) (emptyState : stateTy)
+  (addEntry : Π (init : Bool), environment → stateTy → attributeEntry → stateTy)
+  : IO (attributeExt stateTy) := do
   ext ← attributeExt.mk
     <$> environmentExt.register attr emptyState addEntry
     <*> environmentExt.register (some $ attr ++ ".scoped") [] (λ _ _ entries e, e::entries),