summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress
diff options
context:
space:
mode:
authorSon Ho2023-12-11 11:37:03 +0100
committerSon Ho2023-12-11 11:37:03 +0100
commitcb332ffb55425e6e6bc3b0ef8da7e646b2174fdf (patch)
tree5b02bdac9ca9438d3c6084576aca788a336213ab /backends/lean/Base/Progress
parent10a77d17ea06b732106348588bedc6a89766d56f (diff)
Reorganize a bit
Diffstat (limited to 'backends/lean/Base/Progress')
-rw-r--r--backends/lean/Base/Progress/Base.lean26
1 files changed, 2 insertions, 24 deletions
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