From 38f66c580bec34b0d4b2efb9765892788aa96f09 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Oct 2019 15:57:02 -0700 Subject: [PATCH] chore: fix tests --- tests/compiler/array_test.lean.expected.out | 40 +++++++++---------- tests/compiler/qsortBadLt.lean.expected.out | 2 +- .../termparsertest1.lean.expected.out | 12 +++--- tests/lean/binsearch.lean.expected.out | 2 +- 4 files changed, 29 insertions(+), 27 deletions(-) diff --git a/tests/compiler/array_test.lean.expected.out b/tests/compiler/array_test.lean.expected.out index c0db8b4347..963e68449a 100644 --- a/tests/compiler/array_test.lean.expected.out +++ b/tests/compiler/array_test.lean.expected.out @@ -1,22 +1,22 @@ -[] +#[] 0 -[0, 1, 2, 3] -[10, 11, 12, 13] +#[0, 1, 2, 3] +#[10, 11, 12, 13] 4 -[10, 11, 12] -[10, 11, 12, 13, 100] -[10, 11, 12] -[3, 4, 5, 6] -[2, 3] -[] -[] -[3, 4] -[4, 3, 2, 1] -[] -[3, 2, 1] -[2, 4] -[2, 4] -[1, 3, 5] -[3, 4] -[] -[1, 2, 3, 4] +#[10, 11, 12] +#[10, 11, 12, 13, 100] +#[10, 11, 12] +#[3, 4, 5, 6] +#[2, 3] +#[] +#[] +#[3, 4] +#[4, 3, 2, 1] +#[] +#[3, 2, 1] +#[2, 4] +#[2, 4] +#[1, 3, 5] +#[3, 4] +#[] +#[1, 2, 3, 4] diff --git a/tests/compiler/qsortBadLt.lean.expected.out b/tests/compiler/qsortBadLt.lean.expected.out index 44e2ace7e5..6477d3bcbf 100644 --- a/tests/compiler/qsortBadLt.lean.expected.out +++ b/tests/compiler/qsortBadLt.lean.expected.out @@ -1 +1 @@ -[1, 2] +#[1, 2] diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out index edd3cb1ba1..62473338dc 100644 --- a/tests/compiler/termparsertest1.lean.expected.out +++ b/tests/compiler/termparsertest1.lean.expected.out @@ -166,11 +166,13 @@ fun (Prod.mk x y) => f y x (null (Term.structInstField `fst ":=" (numLit "10")) "," (Term.structInstSource ".." (null))) "}") a[i] -(Term.array (Term.id `a (null)) "[" (Term.id `i (null)) "]") +(Term.arrayRef (Term.id `a (null)) "[" (Term.id `i (null)) "]") f [10, 20] -(Term.app (Term.id `f (null)) (Term.list "[" (null (numLit "10") "," (numLit "20")) "]")) +(Term.app (Term.id `f (null)) (Term.listLit "[" (null (numLit "10") "," (numLit "20")) "]")) g a[x+2] -(Term.app (Term.id `g (null)) (Term.array (Term.id `a (null)) "[" (Term.add (Term.id `x (null)) "+" (numLit "2")) "]")) +(Term.app + (Term.id `g (null)) + (Term.arrayRef (Term.id `a (null)) "[" (Term.add (Term.id `x (null)) "+" (numLit "2")) "]")) g f.a.1.2.bla x.1.a (Term.app (Term.app @@ -384,7 +386,7 @@ let x[i].y := f 10; x (Term.let "let" (Term.letPatDecl - (Term.proj (Term.array (Term.id `x (null)) "[" (Term.id `i (null)) "]") "." `y) + (Term.proj (Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]") "." `y) (null) ":=" (Term.app (Term.id `f (null)) (numLit "10"))) @@ -394,7 +396,7 @@ let x[i] := f 20; x (Term.let "let" (Term.letPatDecl - (Term.array (Term.id `x (null)) "[" (Term.id `i (null)) "]") + (Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]") (null) ":=" (Term.app (Term.id `f (null)) (numLit "20"))) diff --git a/tests/lean/binsearch.lean.expected.out b/tests/lean/binsearch.lean.expected.out index 55a2237d2c..ad222b6164 100644 --- a/tests/lean/binsearch.lean.expected.out +++ b/tests/lean/binsearch.lean.expected.out @@ -1,4 +1,4 @@ -[(9, false), (8, true), (7, false), (6, true), (5, false), (4, true), (3, false), (2, true), (1, false), (0, true)] +#[(9, false), (8, true), (7, false), (6, true), (5, false), (4, true), (3, false), (2, true), (1, false), (0, true)] >> 0 ==> (some (0, true)) >> 1 ==> (some (1, false)) >> 2 ==> (some (2, true))