From a1aac9a98dcf4197754eaffc9459b4040d8af870 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 15 Dec 2019 18:34:13 -0800 Subject: [PATCH] chore: fix tests --- tests/compiler/phashmap.lean | 6 +-- tests/compiler/phashmap2.lean | 24 ++++----- tests/lean/mvar2.lean | 4 +- tests/lean/mvar3.lean | 2 +- tests/lean/phashmap_inst_coherence.lean | 2 +- .../phashmap_inst_coherence.lean.expected.out | 2 +- tests/lean/run/expr_maps.lean | 52 +++++++++---------- tests/lean/run/instuniv.lean | 2 +- tests/lean/run/meta2.lean | 2 +- tests/lean/run/meta3.lean | 2 +- 10 files changed, 49 insertions(+), 49 deletions(-) diff --git a/tests/compiler/phashmap.lean b/tests/compiler/phashmap.lean index 608f579fd6..a429f11012 100644 --- a/tests/compiler/phashmap.lean +++ b/tests/compiler/phashmap.lean @@ -30,7 +30,7 @@ n.fold (fun i m => m.insert i (i*10)) PersistentHashMap.empty def check (n : Nat) (m : Map) : IO Unit := n.forM $ fun i => - match m.find i with + match m.find? i with | none => IO.println ("failed to find " ++ toString i) | some v => unless (v == i*10) (IO.println ("unexpected value " ++ toString i ++ " => " ++ toString v)) @@ -40,11 +40,11 @@ n.fold (fun i m => if i % 2 == 0 then m else m.erase i) m def check2 (n : Nat) (bot : Nat) (m : Map) : IO Unit := n.forM $ fun i => if i % 2 == 0 && i >= bot then - match m.find i with + match m.find? i with | none => IO.println ("failed to find " ++ toString i) | some v => unless (v == i*10) (IO.println ("unexpected value " ++ toString i ++ " => " ++ toString v)) else - unless (m.find i == none) (IO.println ("mapping still contains " ++ toString i)) + unless (m.find? i == none) (IO.println ("mapping still contains " ++ toString i)) def delLess (n : Nat) (m : Map) : Map := n.fold (fun i m => m.erase i) m diff --git a/tests/compiler/phashmap2.lean b/tests/compiler/phashmap2.lean index 2a20b4d2e2..c924b1389b 100644 --- a/tests/compiler/phashmap2.lean +++ b/tests/compiler/phashmap2.lean @@ -36,21 +36,21 @@ let m := m.insert 65 3; -- IO.println (formatMap m.root); IO.println m.stats; let m := m.erase 33; -IO.println (m.find 1); -IO.println (m.find 33); -IO.println (m.find 65); +IO.println (m.find? 1); +IO.println (m.find? 33); +IO.println (m.find? 65); IO.println m.stats; let m := m.erase 1; -IO.println (m.find 1); -IO.println (m.find 33); -IO.println (m.find 65); +IO.println (m.find? 1); +IO.println (m.find? 33); +IO.println (m.find? 65); IO.println m.stats; let m := m.erase 1; -IO.println (m.find 1); -IO.println (m.find 33); -IO.println (m.find 65); +IO.println (m.find? 1); +IO.println (m.find? 33); +IO.println (m.find? 65); let m := m.erase 65; -IO.println (m.find 1); -IO.println (m.find 33); -IO.println (m.find 65); +IO.println (m.find? 1); +IO.println (m.find? 33); +IO.println (m.find? 65); IO.println m.stats diff --git a/tests/lean/mvar2.lean b/tests/lean/mvar2.lean index 1bba9f0d3e..16d560d392 100644 --- a/tests/lean/mvar2.lean +++ b/tests/lean/mvar2.lean @@ -55,5 +55,5 @@ def t2 := lctx4.mkLambda #[α, x, y] $ mkAppN f #[mkAppN m3 #[α, x], x] #eval (mctx7.instantiateMVars t2).1 /- m3 is not prompoted to regular assignment until m1 is assigned. Reason: m1 occurs in the type of x, and m3 depends on x. This corner case in to correcly handled in the C++ code. -/ -#eval (mctx6.instantiateMVars t2).2.getExprAssignment `m3 -#eval (mctx7.instantiateMVars t2).2.getExprAssignment `m3 +#eval (mctx6.instantiateMVars t2).2.getExprAssignment? `m3 +#eval (mctx7.instantiateMVars t2).2.getExprAssignment? `m3 diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean index f230793feb..e7e1603bc8 100644 --- a/tests/lean/mvar3.lean +++ b/tests/lean/mvar3.lean @@ -92,5 +92,5 @@ def e3 := R3.1 def mctx7 := R3.2 #eval e3 -- The delayed assignment became a regular one. -#eval mctx7.getExprAssignment (mkNameNum `n 2) +#eval mctx7.getExprAssignment? (mkNameNum `n 2) #eval toString $ sortNames $ mctx7.dAssignment.toList.map Prod.fst diff --git a/tests/lean/phashmap_inst_coherence.lean b/tests/lean/phashmap_inst_coherence.lean index 284fdcbe68..c335013e27 100644 --- a/tests/lean/phashmap_inst_coherence.lean +++ b/tests/lean/phashmap_inst_coherence.lean @@ -8,4 +8,4 @@ def natDiffHash : Hashable Nat := ⟨fun n => USize.ofNat $ n+10⟩ -- The following example should fail since the `Hashable` instance used to create `m` is not `natDiffHash` -#eval @PersistentHashMap.find Nat Nat _ natDiffHash m 1 +#eval @PersistentHashMap.find? Nat Nat _ natDiffHash m 1 diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out index 6cf09f3e51..9870faee97 100644 --- a/tests/lean/phashmap_inst_coherence.lean.expected.out +++ b/tests/lean/phashmap_inst_coherence.lean.expected.out @@ -1,5 +1,5 @@ phashmap_inst_coherence.lean:11:0: error: type mismatch at application - PersistentHashMap.find m + PersistentHashMap.find? m term m has type diff --git a/tests/lean/run/expr_maps.lean b/tests/lean/run/expr_maps.lean index 406c6b418b..d098bc0dd2 100644 --- a/tests/lean/run/expr_maps.lean +++ b/tests/lean/run/expr_maps.lean @@ -41,13 +41,13 @@ do IO.println TypeArrowType; def tst2 : IO Unit := do let m1 : ExprMap Nat := {}; let m1 := m1.insert exprT1 10; - check (m1.find exprT1 == some 10); - check (m1.find exprT2 == some 10); - check (m1.find exprT3 == none); + check (m1.find? exprT1 == some 10); + check (m1.find? exprT2 == some 10); + check (m1.find? exprT3 == none); let m1 := m1.insert exprT4 20; - check (m1.find exprT1 == some 10); - check (m1.find exprT3 == some 20); - IO.println (m1.find exprT1); + check (m1.find? exprT1 == some 10); + check (m1.find? exprT3 == some 20); + IO.println (m1.find? exprT1); pure () #eval tst2 @@ -55,14 +55,14 @@ do let m1 : ExprMap Nat := {}; def tst3 : IO Unit := do let m1 : ExprStructMap Nat := {}; let m1 := m1.insert exprT1 10; - check (m1.find exprT1 == some 10); - check (m1.find exprT2 == none); - check (m1.find exprT3 == none); + check (m1.find? exprT1 == some 10); + check (m1.find? exprT2 == none); + check (m1.find? exprT3 == none); let m1 := m1.insert exprT4 20; - check (m1.find exprT1 == some 10); - check (m1.find exprT4 == some 20); - check (m1.find exprT3 == none); - IO.println (m1.find exprT1); + check (m1.find? exprT1 == some 10); + check (m1.find? exprT4 == some 20); + check (m1.find? exprT3 == none); + IO.println (m1.find? exprT1); pure () #eval tst3 @@ -70,13 +70,13 @@ do let m1 : ExprStructMap Nat := {}; def tst4 : IO Unit := do let m1 : PersistentExprMap Nat := {}; let m1 := m1.insert exprT1 10; - check (m1.find exprT1 == some 10); - check (m1.find exprT2 == some 10); - check (m1.find exprT3 == none); + check (m1.find? exprT1 == some 10); + check (m1.find? exprT2 == some 10); + check (m1.find? exprT3 == none); let m1 := m1.insert exprT4 20; - check (m1.find exprT1 == some 10); - check (m1.find exprT3 == some 20); - IO.println (m1.find exprT1); + check (m1.find? exprT1 == some 10); + check (m1.find? exprT3 == some 20); + IO.println (m1.find? exprT1); pure () #eval tst4 @@ -84,14 +84,14 @@ do let m1 : PersistentExprMap Nat := {}; def tst5 : IO Unit := do let m1 : PersistentExprStructMap Nat := {}; let m1 := m1.insert exprT1 10; - check (m1.find exprT1 == some 10); - check (m1.find exprT2 == none); - check (m1.find exprT3 == none); + check (m1.find? exprT1 == some 10); + check (m1.find? exprT2 == none); + check (m1.find? exprT3 == none); let m1 := m1.insert exprT4 20; - check (m1.find exprT1 == some 10); - check (m1.find exprT4 == some 20); - check (m1.find exprT3 == none); - IO.println (m1.find exprT1); + check (m1.find? exprT1 == some 10); + check (m1.find? exprT4 == some 20); + check (m1.find? exprT3 == none); + IO.println (m1.find? exprT1); pure () #eval tst5 diff --git a/tests/lean/run/instuniv.lean b/tests/lean/run/instuniv.lean index 0db30a1353..97e2be6c9e 100644 --- a/tests/lean/run/instuniv.lean +++ b/tests/lean/run/instuniv.lean @@ -3,7 +3,7 @@ open Lean def tst : IO Unit := do env ← importModules [{module := `Init.Data.Array}]; - match env.find `Array.foldl with + match env.find? `Array.foldl with | some info => do IO.println (info.instantiateTypeLevelParams [levelZero, levelZero]); IO.println (info.instantiateValueLevelParams [levelZero, levelZero]); diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean index 820aac3f31..6c8b481871 100644 --- a/tests/lean/run/meta2.lean +++ b/tests/lean/run/meta2.lean @@ -14,7 +14,7 @@ def check (x : MetaM Bool) : MetaM Unit := unlessM x $ throw $ Exception.other "check failed" def getAssignment (m : Expr) : MetaM Expr := -do v? ← getExprMVarAssignment m.mvarId!; +do v? ← getExprMVarAssignment? m.mvarId!; match v? with | some v => pure v | none => throw $ Exception.other "metavariable is not assigned" diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean index 6253e4b472..0db19b29bb 100644 --- a/tests/lean/run/meta3.lean +++ b/tests/lean/run/meta3.lean @@ -15,7 +15,7 @@ def check (x : MetaM Bool) : MetaM Unit := unlessM x $ throw $ Exception.other "check failed" def getAssignment (m : Expr) : MetaM Expr := -do v? ← getExprMVarAssignment m.mvarId!; +do v? ← getExprMVarAssignment? m.mvarId!; match v? with | some v => pure v | none => throw $ Exception.other "metavariable is not assigned"