From 5437ce9106b4d253b1cd48c08926f4b49ebfd8f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Apr 2020 11:32:39 -0700 Subject: [PATCH] chore: workaround bugs exposed by previous commit --- tests/compiler/float_cases_bug.lean | 8 ++++---- tests/compiler/phashmap3.lean | 10 ++++++---- 2 files changed, 10 insertions(+), 8 deletions(-) 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