diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Extensions.lean | 47 | ||||
| -rw-r--r-- | backends/lean/Base/Lookup/Base.lean | 70 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Base.lean | 26 |
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 |