summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/Base/Extensions.lean47
-rw-r--r--backends/lean/Base/Lookup/Base.lean70
-rw-r--r--backends/lean/Base/Progress/Base.lean26
3 files changed, 49 insertions, 94 deletions
diff --git a/backends/lean/Base/Extensions.lean b/backends/lean/Base/Extensions.lean
new file mode 100644
index 00000000..b34f41dc
--- /dev/null
+++ b/backends/lean/Base/Extensions.lean
@@ -0,0 +1,47 @@
+import Lean
+import Std.Lean.HashSet
+import Base.Utils
+import Base.Primitives.Base
+
+import Lean.Meta.DiscrTree
+import Lean.Meta.Tactic.Simp
+
+/-! Various state extensions used in the library -/
+namespace Extensions
+
+open Lean Elab Term Meta
+open Utils
+
+-- This is not used anymore but we keep it here.
+-- 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)
+ }
+
+/- 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). The transformation itself can be done elsewhere.
+ -/
+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 ,
+ }
+
+end Extensions
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
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