diff --git a/tests/compiler/float_cases_bug.lean b/tests/compiler/float_cases_bug.lean index af8e76fbe8..14eb1fe19b 100644 --- a/tests/compiler/float_cases_bug.lean +++ b/tests/compiler/float_cases_bug.lean @@ -19,15 +19,15 @@ partial def foo : MyState -> Term -> Term -> List Term match t with | const _ => pure () - | app _ => emit (const 1) *> pure () ; + | app _ => emit (const 1); match t, u with - | app _, app _ => emit (app []) *> pure () + | app _, app _ => emit (app []) | _, _ => pure () ; match t, u with - | app _, app _ => emit (app []) *> pure () - | _, _ => emit (const 2) *> pure () + | app _, app _ => emit (app []) + | _, _ => emit (const 2) } ; diff --git a/tests/compiler/phashmap3.lean b/tests/compiler/phashmap3.lean index 6ad98d6f56..efbeb6a76b 100644 --- a/tests/compiler/phashmap3.lean +++ b/tests/compiler/phashmap3.lean @@ -25,8 +25,11 @@ partial def formatMap : Node Nat Nat → Format | Entry.entry k v => Format.paren (format k ++ " => " ++ format v)) Format.nil -def main : IO Unit := -do +def checkState (m : Map) : IO Unit := do +unless (m.stats.maxDepth == 1) (IO.println "unexpected max depth"); +unless (m.stats.numCollisions == 0) (IO.println "unexpected number of collisions") + +def main : IO Unit := do let m : Map := PersistentHashMap.empty; let m := m.insert 1 1; let m := m.insert (32^5 + 1) 2; @@ -42,6 +45,5 @@ let m := m.erase (32^(max+2) + 1); let m := m.erase (32^max + 1); unless (m.stats.maxDepth == PersistentHashMap.maxDepth.toNat - 1) (IO.println "unexpected max depth"); let m := m.erase (32^5 + 1); -unless (m.stats.maxDepth == 1) (IO.println "unexpected max depth"); -unless (m.stats.numCollisions == 0) (IO.println "unexpected number of collisions"); +checkState m; IO.println m.stats