chore: remove dead code at Class.lean used by old frontend

src/Lean/Class.lean

@@ -7,51 +7,37 @@ import Lean.Attributes
 
 namespace Lean
 
-inductive ClassEntry :=
-  | «class»    (name : Name) (hasOutParam : Bool)
-  | «instance» (name : Name) (ofClass : Name) -- TODO: remove after we remove old type class resolution
+structure ClassEntry :=
+  (name : Name)
+  (hasOutParam : Bool)
 
 namespace ClassEntry
 
-@[inline] def getName : ClassEntry → Name
-  | «class» n _ => n
-  | «instance» n _ => n
-
 def lt (a b : ClassEntry) : Bool :=
-  Name.quickLt a.getName b.getName
+  Name.quickLt a.name b.name
 
 end ClassEntry
 
 structure ClassState :=
-  (classToInstances : SMap Name (List Name) := SMap.empty) -- TODO: delete
-  (hasOutParam      : SMap Name Bool := SMap.empty)        -- We should keep only this one
-  (instances        : SMap Name Unit := SMap.empty)        -- TODO: delete
+  (hasOutParam : SMap Name Bool := SMap.empty)
 
 namespace ClassState
 
 instance : Inhabited ClassState := ⟨{}⟩
 
 def addEntry (s : ClassState) (entry : ClassEntry) : ClassState :=
-  match entry with
-  | ClassEntry.«class» clsName hasOutParam =>
-    { s with hasOutParam := s.hasOutParam.insert clsName hasOutParam }
-  | ClassEntry.«instance» instName clsName =>
-    { s with
-      instances        := s.instances.insert instName (),
-      classToInstances := match s.classToInstances.find? clsName with
-        | some insts => s.classToInstances.insert clsName (instName :: insts)
-        | none       => s.classToInstances.insert clsName [instName] }
+  { s with hasOutParam := s.hasOutParam.insert entry.name entry.hasOutParam }
 
-def switch : ClassState → ClassState
-  | ⟨m₁, m₂, m₃⟩ => ⟨m₁.switch, m₂.switch, m₃.switch⟩
+def switch (s : ClassState) : ClassState :=
+  { s with hasOutParam := s.hasOutParam.switch }
 
 end ClassState
 
 /- TODO: add support for scoped instances -/
 builtin_initialize classExtension : SimplePersistentEnvExtension ClassEntry ClassState ←
   registerSimplePersistentEnvExtension {
-    name          := `classExt,
-    addEntryFn    := ClassState.addEntry,
+    name          := `classExt
+    addEntryFn    := ClassState.addEntry
     addImportedFn := fun es => (mkStateFromImportedEntries ClassState.addEntry {} es).switch
   }
 
@@ -59,16 +45,6 @@ builtin_initialize classExtension : SimplePersistentEnvExtension ClassEntry Clas
 def isClass (env : Environment) (n : Name) : Bool :=
   (classExtension.getState env).hasOutParam.contains n
 
-@[export lean_is_instance]
-def isInstance (env : Environment) (n : Name) : Bool :=
-  (classExtension.getState env).instances.contains n
-
-@[export lean_get_class_instances]
-def getClassInstances (env : Environment) (n : Name) : List Name :=
-  match (classExtension.getState env).classToInstances.find? n with
-  | some insts => insts
-  | none       => []
-
 @[export lean_has_out_params]
 def hasOutParams (env : Environment) (n : Name) : Bool :=
   match (classExtension.getState env).hasOutParam.find? n with
@@ -112,7 +88,7 @@ def addClass (env : Environment) (clsName : Name) : Except String Environment :=
     | none      => Except.error ("unknown declaration '" ++ toString clsName ++ "'")
     | some decl@(ConstantInfo.inductInfo _) => do
       let b ← checkOutParam 1 #[] decl.type
-      Except.ok (classExtension.addEntry env (ClassEntry.«class» clsName b))
+      Except.ok (classExtension.addEntry env { name := clsName, hasOutParam := b })
     | some _    => Except.error ("invalid 'class', declaration '" ++ toString clsName ++ "' must be inductive datatype or structure")
 
 private def consumeNLambdas : Nat → Expr → Option Expr
@@ -145,14 +121,4 @@ builtin_initialize
       setEnv env
   }
 
--- TODO: delete
-@[export lean_add_instance_old]
-def addGlobalInstanceOld (env : Environment) (instName : Name) : Except String Environment :=
-  match env.find? instName with
-  | none      => Except.error ("unknown declaration '" ++ toString instName ++ "'")
-  | some decl =>
-    match getClassName env decl.type with
-    | none => Except.error ("invalid instance '" ++ toString instName ++ "', failed to retrieve class")
-    | some clsName => Except.ok (classExtension.addEntry env (ClassEntry.«instance» instName clsName))
-
 end Lean

src/Lean/Meta/Instances.lean

@@ -8,19 +8,31 @@ import Lean.Meta.DiscrTree
 namespace Lean.Meta
 
 structure InstanceEntry :=
-  (keys : Array DiscrTree.Key)
-  (val  : Expr)
+  (keys        : Array DiscrTree.Key)
+  (val         : Expr)
+  (globalName? : Option Name := none)
 
-abbrev Instances := DiscrTree Expr
+structure Instances :=
+  (discrTree       : DiscrTree Expr := DiscrTree.empty )
+  (globalInstances : NameSet := {})
+
+instance : Inhabited Instances := {
+  default := {}
+}
 
 def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances :=
-  d.insertCore e.keys e.val
+  { d with
+    discrTree := d.discrTree.insertCore e.keys e.val
+    globalInstances := match e.globalName? with
+      | some n => d.globalInstances.insert n
+      | none   => d.globalInstances
+  }
 
 builtin_initialize instanceExtension : SimplePersistentEnvExtension InstanceEntry Instances ←
   registerSimplePersistentEnvExtension {
     name          := `instanceExt,
     addEntryFn    := addInstanceEntry,
-    addImportedFn := fun es => (mkStateFromImportedEntries addInstanceEntry DiscrTree.empty es)
+    addImportedFn := fun es => (mkStateFromImportedEntries addInstanceEntry {} es)
   }
 
 private def mkInstanceKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
@@ -36,7 +48,7 @@ def addGlobalInstanceImp (env : Environment) (constName : Name) : IO Environment
   | some cinfo =>
     let c := mkConst constName (cinfo.lparams.map mkLevelParam)
     let (keys, s, _) ← (mkInstanceKey c).toIO {} { env := env } {} {}
-    pure $ instanceExtension.addEntry s.env { keys := keys, val := c }
+    pure $ instanceExtension.addEntry s.env { keys := keys, val := c, globalName? := constName }
 
 def addGlobalInstance {m} [Monad m] [MonadEnv m] [MonadLiftT IO m] (declName : Name) : m Unit := do
   let env ← getEnv
@@ -50,20 +62,14 @@ builtin_initialize
     add   := fun declName args persistent => do
       if args.hasArgs then throwError "invalid attribute 'instance', unexpected argument"
       unless persistent do throwError "invalid attribute 'instance', must be persistent"
-      let env ← getEnv
-      let env ← ofExcept (addGlobalInstanceOld env declName); setEnv env; -- TODO: delete after we remove old frontend
       addGlobalInstance declName
   }
 
-end Meta
+@[export lean_is_instance]
+def isGlobalInstance (env : Environment) (declName : Name) : Bool :=
+  Meta.instanceExtension.getState env |>.globalInstances.contains declName
 
-def Environment.getGlobalInstances (env : Environment) : Meta.Instances :=
-  Meta.instanceExtension.getState env
-
-namespace Meta
-
-def getGlobalInstances : MetaM Instances := do
-  let env ← getEnv
-  pure env.getGlobalInstances
+def getGlobalInstancesIndex : MetaM (DiscrTree Expr) :=
+  return Meta.instanceExtension.getState (← getEnv) |>.discrTree
 
 end Lean.Meta

src/Lean/Meta/SynthInstance.lean

@@ -170,7 +170,7 @@ def getInstances (type : Expr) : MetaM (Array Expr) := do
     match className? with
     | none   => throwError $ "type class instance expected" ++ indentExpr type
     | some className =>
-      let globalInstances ← getGlobalInstances
+      let globalInstances ← getGlobalInstancesIndex
       let result ← globalInstances.getUnify type
       let result ← result.mapM fun c => match c with
         | Expr.const constName us _ => return c.updateConst! (← us.mapM (fun _ => mkFreshLevelMVar))

src/library/class.cpp

@@ -11,24 +11,13 @@ Author: Leonardo de Moura
 namespace lean {
 extern "C" uint8 lean_is_class(object* env, object* n);
 extern "C" uint8 lean_is_instance(object* env, object* n);
-extern "C" object* lean_get_class_instances(object* env, object* n);
 extern "C" uint8 lean_is_out_param(object* e);
 extern "C" uint8 lean_has_out_params(object* env, object* n);
-extern "C" object* lean_add_instance(object* env, object* n, object* w);
-extern "C" object* lean_add_instance_old(object* env, object* n);
 
 bool is_class_out_param(expr const & e) { return lean_is_out_param(e.to_obj_arg()); }
 bool has_class_out_params(environment const & env, name const & c) { return lean_has_out_params(env.to_obj_arg(), c.to_obj_arg()); }
 bool is_class(environment const & env, name const & c) { return lean_is_class(env.to_obj_arg(), c.to_obj_arg()); }
 bool is_instance(environment const & env, name const & i) { return lean_is_instance(env.to_obj_arg(), i.to_obj_arg()); }
-names get_class_instances(environment const & env, name const & c) { return names(lean_get_class_instances(env.to_obj_arg(), c.to_obj_arg())); }
-
-environment add_instance(environment const & env, name const & n, bool persistent) {
-    if (!persistent) throw exception("local instances have been disabled");
-    environment new_env = get_except_value<environment>(lean_add_instance_old(env.to_obj_arg(), n.to_obj_arg()));
-    new_env = get_io_result<environment>(lean_add_instance(new_env.to_obj_arg(), n.to_obj_arg(), io_mk_world()));
-    return new_env;
-}
 
 static name * g_anonymous_inst_name_prefix = nullptr;
 

src/library/class.h

@@ -7,14 +7,10 @@ Author: Leonardo de Moura
 #pragma once
 #include "library/util.h"
 namespace lean {
-/** \brief Add a new 'class instance' to the environment. */
-environment add_instance(environment const & env, name const & n, bool persistent);
 /** \brief Return true iff \c c was declared with \c add_class. */
 bool is_class(environment const & env, name const & c);
 /** \brief Return true iff \c i was declared with \c add_instance. */
 bool is_instance(environment const & env, name const & i);
-/** \brief Return the instances of the given class. */
-names get_class_instances(environment const & env, name const & c);
 
 name const & get_anonymous_instance_prefix();
 name mk_anonymous_inst_name(unsigned idx);