From cb332ffb55425e6e6bc3b0ef8da7e646b2174fdf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 11 Dec 2023 11:37:03 +0100
Subject: Reorganize a bit

---
 backends/lean/Base/Lookup/Base.lean | 70 -------------------------------------
 1 file changed, 70 deletions(-)
 delete mode 100644 backends/lean/Base/Lookup/Base.lean

(limited to 'backends/lean/Base/Lookup')

diff --git a/backends/lean/Base/Lookup/Base.lean b/backends/lean/Base/Lookup/Base.lean
deleted file mode 100644
index 54d242ea..00000000
--- a/backends/lean/Base/Lookup/Base.lean
+++ /dev/null
@@ -1,70 +0,0 @@
-/- Utilities to have databases of theorems -/
-import Lean
-import Std.Lean.HashSet
-import Base.Utils
-import Base.Primitives.Base
-
-namespace Lookup
-
-open Lean Elab Term Meta
-open Utils
-
--- TODO: the original function doesn't define correctly the `addImportedFn`. Do a PR?
-def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) :
-  IO (MapDeclarationExtension α) :=
-  registerSimplePersistentEnvExtension {
-    name          := name,
-    addImportedFn := fun a => a.foldl (fun s a => a.foldl (fun s (k, v) => s.insert k v) s) RBMap.empty,
-    addEntryFn    := fun s n => s.insert n.1 n.2 ,
-    toArrayFn     := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1)
-  }
-
--- Declare an extension of maps of maps (using [RBMap]).
--- The important point is that we need to merge the bound values (which are maps).
-def mkMapMapDeclarationExtension [Inhabited β] (ord : α → α → Ordering)
-  (name : Name := by exact decl_name%) :
-  IO (MapDeclarationExtension (RBMap α β ord)) :=
-  registerSimplePersistentEnvExtension {
-    name          := name,
-    addImportedFn := fun a =>
-      a.foldl (fun s a => a.foldl (
-        -- We need to merge the maps
-        fun s (k0, k1_to_v) =>
-        match s.find? k0 with
-        | none =>
-          -- No binding: insert one
-          s.insert k0 k1_to_v
-        | some m =>
-          -- There is already a binding: merge
-          let m := RBMap.fold (fun m k v => m.insert k v) m k1_to_v
-          s.insert k0 m)
-          s) RBMap.empty,
-    addEntryFn    := fun s n => s.insert n.1 n.2 ,
-    toArrayFn     := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1)
-  }
-
--- Declare an extension of maps of maps (using [HashMap]).
--- The important point is that we need to merge the bound values (which are maps).
-def mkMapHashMapDeclarationExtension [BEq α] [Hashable α] [Inhabited β]
-  (name : Name := by exact decl_name%) :
-  IO (MapDeclarationExtension (HashMap α β)) :=
-  registerSimplePersistentEnvExtension {
-    name          := name,
-    addImportedFn := fun a =>
-      a.foldl (fun s a => a.foldl (
-        -- We need to merge the maps
-        fun s (k0, k1_to_v) =>
-        match s.find? k0 with
-        | none =>
-          -- No binding: insert one
-          s.insert k0 k1_to_v
-        | some m =>
-          -- There is already a binding: merge
-          let m := HashMap.fold (fun m k v => m.insert k v) m k1_to_v
-          s.insert k0 m)
-          s) RBMap.empty,
-    addEntryFn    := fun s n => s.insert n.1 n.2 ,
-    toArrayFn     := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1)
-  }
-
-end Lookup
-- 
cgit v1.2.3