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/Progress/Base.lean | 26 ++------------------------
 1 file changed, 2 insertions(+), 24 deletions(-)

(limited to 'backends/lean/Base/Progress/Base.lean')

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index a72cd641..fd80db8c 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -2,42 +2,20 @@ import Lean
 import Std.Lean.HashSet
 import Base.Utils
 import Base.Primitives.Base
-import Base.Lookup.Base
-
+import Base.Extensions
 import Lean.Meta.DiscrTree
 import Lean.Meta.Tactic.Simp
 
 namespace Progress
 
 open Lean Elab Term Meta
-open Utils
+open Utils Extensions
 
 -- We can't define and use trace classes in the same file
 initialize registerTraceClass `Progress
 
 /- # Progress tactic -/
 
-/- Discrimination trees map expressions to values. When storing an expression
-   in a discrimination tree, the expression is first converted to an array
-   of `DiscrTree.Key`, which are the keys actually used by the discrimination
-   trees. The conversion operation is monadic, however, and extensions require
-   all the operations to be pure. For this reason, in the state extension, we
-   store the keys from *after* the transformation (i.e., the `DiscrTreeKey`
-   below).
- -/
-abbrev DiscrTreeKey (simpleReduce : Bool) := Array (DiscrTree.Key simpleReduce)
-
-abbrev DiscrTreeExtension (α : Type) (simpleReduce : Bool) :=
-  SimplePersistentEnvExtension (DiscrTreeKey simpleReduce × α) (DiscrTree α simpleReduce)
-
-def mkDiscrTreeExtention [Inhabited α] [BEq α] (name : Name := by exact decl_name%) (simpleReduce : Bool) :
-  IO (DiscrTreeExtension α simpleReduce) :=
-  registerSimplePersistentEnvExtension {
-    name          := name,
-    addImportedFn := fun a => a.foldl (fun s a => a.foldl (fun s (k, v) => s.insertCore k v) s) DiscrTree.empty,
-    addEntryFn    := fun s n => s.insertCore n.1 n.2 ,
-  }
-
 structure PSpecDesc where
   -- The universally quantified variables
   -- Can be fvars or mvars
-- 
cgit v1.2.3