chore: bump toolchain to v4.3.0-rc1 (#83)

Aesop/Builder/Cases.lean

@@ -22,7 +22,7 @@ def check (decl : Name) (p : CasesPattern) : MetaM Unit :=
 
 def toIndexingMode (p : CasesPattern) : MetaM IndexingMode :=
   withoutModifyingState do
-    .hyps <$> DiscrTree.mkPath (← p.toExpr)
+    .hyps <$> DiscrTree.mkPath (← p.toExpr) discrTreeConfig
 
 end CasesPattern
 

Aesop/Builder/Forward.lean

@@ -76,7 +76,7 @@ private def getIndexingMode (type : Expr) (immediate : UnorderedArraySet Nat)
       match args.get? i with
       | some arg =>
         let argT := (← arg.mvarId!.getDecl).type
-        let keys ← DiscrTree.mkPath argT
+        let keys ← DiscrTree.mkPath argT discrTreeConfig
         return .hyps keys
       | none => throwError
         "aesop: internal error: immediate arg for forward rule is out of range"

Aesop/Frontend/RuleExpr.lean

@@ -171,10 +171,10 @@ def elabSingleIndexingMode (stx : Syntax) : ElabM IndexingMode :=
     | `(indexing_mode| unindexed) => return .unindexed
     | _ => throwUnsupportedSyntax
   where
-    elabKeys {s} (stx : Syntax) : ElabM (Array (DiscrTree.Key s)) :=
+    elabKeys (stx : Syntax) : ElabM (Array DiscrTree.Key) :=
       show TermElabM _ from withoutModifyingState do
         let e ← elabPattern stx
-        DiscrTree.mkPath e
+        DiscrTree.mkPath e discrTreeConfig
 
 def IndexingMode.elab (stxs : Array Syntax) : ElabM IndexingMode :=
   .or <$> stxs.mapM elabSingleIndexingMode

Aesop/Index.lean

@@ -14,8 +14,8 @@ open Lean.Meta
 namespace Aesop
 
 structure Index (α : Type) [BEq α] [Hashable α] where
-  byTarget : DiscrTree α simpleReduce
-  byHyp : DiscrTree α simpleReduce
+  byTarget : DiscrTree α 
+  byHyp : DiscrTree α 
   unindexed : PHashSet α
   deriving Inhabited
 
@@ -56,9 +56,9 @@ partial def add (r : α) (imode : IndexingMode) (ri : Index α) :
   | IndexingMode.unindexed =>
     { ri with unindexed := ri.unindexed.insert r }
   | IndexingMode.target keys =>
-    { ri with byTarget := ri.byTarget.insertCore keys r }
+    { ri with byTarget := ri.byTarget.insertCore keys r discrTreeConfig }
   | IndexingMode.hyps keys =>
-    { ri with byHyp := ri.byHyp.insertCore keys r }
+    { ri with byHyp := ri.byHyp.insertCore keys r discrTreeConfig }
   | IndexingMode.or imodes =>
     imodes.foldl (init := ri) λ ri imode =>
       ri.add r imode
@@ -69,8 +69,8 @@ def unindex (ri : Index α) (p : α → Bool) : Index α :=
   { byTarget, byHyp, unindexed }
   where
     @[inline, always_inline]
-    filterDiscrTree' {s} (unindexed : PHashSet α) (t : DiscrTree α s) :
-        DiscrTree α s × PHashSet α :=
+    filterDiscrTree' (unindexed : PHashSet α) (t : DiscrTree α) :
+        DiscrTree α × PHashSet α :=
       filterDiscrTree (not ∘ p) (λ unindexed v => unindexed.insert v) unindexed
         t
 
@@ -95,7 +95,7 @@ def size : Index α → Nat
 private def applicableByTargetRules (ri : Index α) (goal : MVarId)
     (include? : α → Bool) : MetaM (Array (α × Array IndexMatchLocation)) :=
   goal.withContext do
-    let rules ← ri.byTarget.getUnify (← goal.getType)
+    let rules ← ri.byTarget.getUnify (← goal.getType) discrTreeConfig
     let mut rs := Array.mkEmpty rules.size
       -- Assumption: include? is true for most rules.
     for r in rules do
@@ -112,7 +112,7 @@ private def applicableByHypRules (ri : Index α) (goal : MVarId)
     for localDecl in ← getLCtx do
       if localDecl.isImplementationDetail then
         continue
-      let rules ← ri.byHyp.getUnify localDecl.type
+      let rules ← ri.byHyp.getUnify localDecl.type discrTreeConfig
       for r in rules do
         if include? r then
           rs := rs.push (r, #[.hyp localDecl])

Aesop/Index/Basic.lean

@@ -13,12 +13,12 @@ namespace Aesop
 
 -- This value controls whether we use 'powerful' reductions, e.g. iota, when
 -- indexing Aesop rules. See the `DiscrTree` docs for details.
-def simpleReduce := false
+def discrTreeConfig : WhnfCoreConfig := { iota := false }
 
 inductive IndexingMode : Type
   | unindexed
-  | target (keys : Array (DiscrTree.Key simpleReduce))
-  | hyps (keys : Array (DiscrTree.Key simpleReduce))
+  | target (keys : Array DiscrTree.Key)
+  | hyps (keys : Array DiscrTree.Key)
   | or (imodes : Array IndexingMode)
   deriving Inhabited
 
@@ -34,7 +34,7 @@ instance : ToFormat IndexingMode :=
   ⟨IndexingMode.format⟩
 
 def targetMatchingConclusion (type : Expr) : MetaM IndexingMode := do
-  let path ← getConclusionDiscrTreeKeys type
+  let path ← getConclusionDiscrTreeKeys type discrTreeConfig
   return target path
 
 def hypsMatchingConst (decl : Name) : MetaM IndexingMode := do

Aesop/Search/Main.lean

@@ -217,7 +217,7 @@ def handleFatalError (e : Exception) : SearchM Q α := do
 
 partial def searchLoop : SearchM Q (Array MVarId) :=
   withIncRecDepth do
-    checkMaxHeartbeats "aesop"
+    checkSystem "aesop"
     if let (some err) ← checkRootUnprovable then
       handleNonfatalError err
     else if ← finishIfProven then

Aesop/Util/Basic.lean

@@ -77,30 +77,30 @@ open DiscrTree
 
 -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with
 -- `n` stars).
-def getConclusionDiscrTreeKeys (type : Expr) :
-    MetaM (Array (Key s)) :=
+def getConclusionDiscrTreeKeys (type : Expr) (config : WhnfCoreConfig) :
+    MetaM (Array Key) :=
   withoutModifyingState do
     let (_, _, conclusion) ← forallMetaTelescope type
-    mkPath conclusion
+    mkPath conclusion config
     -- We use a meta telescope because `DiscrTree.mkPath` ignores metas (they
     -- turn into `Key.star`) but not fvars.
 
 -- For a constant `d` with type `∀ (x₁, ..., xₙ), T`, returns keys that
 -- match `d * ... *` (with `n` stars).
-def getConstDiscrTreeKeys (decl : Name) : MetaM (Array (Key s)) := do
+def getConstDiscrTreeKeys (decl : Name) : MetaM (Array Key) := do
   let arity := (← getConstInfo decl).type.forallArity
   let mut keys := Array.mkEmpty (arity + 1)
   keys := keys.push $ .const decl arity
   for _ in [0:arity] do
     keys := keys.push $ .star
   return keys
 
-def isEmptyTrie : Trie α s → Bool
+def isEmptyTrie : Trie α → Bool
   | .node vs children => vs.isEmpty && children.isEmpty
 
 @[specialize]
 private partial def filterTrieM [Monad m] [Inhabited σ] (f : σ → α → m σ)
-    (p : α → m (ULift Bool)) (init : σ) : Trie α s → m (Trie α s × σ)
+    (p : α → m (ULift Bool)) (init : σ) : Trie α → m (Trie α × σ)
   | .node vs children => do
     let (vs, acc) ← vs.foldlM (init := (#[], init)) λ (vs, acc) v => do
       if (← p v).down then
@@ -111,8 +111,8 @@ private partial def filterTrieM [Monad m] [Inhabited σ] (f : σ → α → m σ
     let children := children.filter λ (_, c) => ! isEmptyTrie c
     return (.node vs children, acc)
   where
-    go (acc : σ) (i : Nat) (children : Array (Key s × Trie α s)) :
-        m (Array (Key s × Trie α s) × σ) := do
+    go (acc : σ) (i : Nat) (children : Array (Key × Trie α)) :
+        m (Array (Key × Trie α) × σ) := do
       if h : i < children.size then
         let (key, t) := children[i]'h
         let (t, acc) ← filterTrieM f p acc t
@@ -128,8 +128,8 @@ returned.
 -/
 @[specialize]
 def filterDiscrTreeM [Monad m] [Inhabited σ] (p : α → m (ULift Bool))
-    (f : σ → α → m σ) (init : σ) (t : DiscrTree α s) :
-    m (DiscrTree α s × σ) := do
+    (f : σ → α → m σ) (init : σ) (t : DiscrTree α) :
+    m (DiscrTree α × σ) := do
   let (root, acc) ←
     t.root.foldlM (init := (.empty, init)) λ (root, acc) key t => do
       let (t, acc) ← filterTrieM f p acc t
@@ -143,7 +143,7 @@ The removed elements are folded over using `f` and `init`, so `f` is called
 once for each removed element and the final state of type `σ` is returned.
 -/
 def filterDiscrTree [Inhabited σ] (p : α → Bool) (f : σ → α → σ) (init : σ)
-    (t : DiscrTree α s) : DiscrTree α s × σ := Id.run $
+    (t : DiscrTree α) : DiscrTree α × σ := Id.run $
   filterDiscrTreeM (λ a => pure ⟨p a⟩) (λ s a => pure (f s a)) init t
 
 end DiscrTree

lake-manifest.json

@@ -4,9 +4,9 @@
  [{"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "409a644492aaff846b6b2963e221c7f1ceaf30cc",
+    "rev": "a71c160b1934814837d37f377efaf2964e55c433",
     "opts": {},
     "name": "std",
-    "inputRev?": "v4.2.0",
+    "inputRev?": "main",
     "inherited": false}}],
  "name": "aesop"}

lakefile.lean

@@ -13,4 +13,4 @@ lean_lib AesopTest {
   globs := #[.submodules "AesopTest"]
 }
 
-require std from git "https://github.com/leanprover/std4" @ "v4.2.0"
+require std from git "https://github.com/leanprover/std4" @ "main"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0
+leanprover/lean4:v4.3.0-rc1

tests/27.lean.expected

@@ -10,9 +10,7 @@
                           Eq.ndrec (motive := fun {xs_1} =>
                             ∀ (a_1 : All P xs_1), HEq h (All.cons (P := P) a a_1) → P x ∧ All P xs)
                             (fun a_1 h_1 =>
-                              Eq.ndrec (motive := fun h => P x ∧ All P xs)
-                                (of_eq_true (Eq.trans (congr (congrArg And (eq_true a)) (eq_true a_1)) (and_self True)))
-                                (Eq.symm (eq_of_heq h_1)))
+                              of_eq_true (Eq.trans (congr (congrArg And (eq_true a)) (eq_true a_1)) (and_self True)))
                             tail_eq a_1)
                         head_eq a :
                   x :: xs = x :: xs → HEq h h_2 → P x ∧ All P xs))