max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: workaround bugs exposed by previous commit

Browse source
This commit is contained in:
Leonardo de Moura 2020-04-23 11:32:39 -07:00
parent 8f67db0101
commit 5437ce9106
2 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
tests/compiler/float_cases_bug.lean
View file

@ -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)
} ;

10
tests/compiler/phashmap3.lean
View file

@ -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