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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-15 18:34:13 -08:00
parent 067dca5a65
commit a1aac9a98d
10 changed files with 49 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/compiler/phashmap.lean
View file

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

24
tests/compiler/phashmap2.lean
View file

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

4
tests/lean/mvar2.lean
View file

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

2
tests/lean/mvar3.lean
View file

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

2
tests/lean/phashmap_inst_coherence.lean
View file

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

2
tests/lean/phashmap_inst_coherence.lean.expected.out
View file

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

52
tests/lean/run/expr_maps.lean
View file

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

2
tests/lean/run/instuniv.lean
View file

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

2
tests/lean/run/meta2.lean
View file

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

2
tests/lean/run/meta3.lean
View file

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