From f079d05fc2ce121f4f8c35db9d665e0385eda8a9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Jan 2017 19:08:41 -0800 Subject: [PATCH] chore(tests/lean): adjust tests to recent changes --- tests/lean/pp_all.lean.expected.out | 2 +- tests/lean/pp_beta.lean | 2 +- tests/lean/pp_beta.lean.expected.out | 2 +- tests/lean/quot_ind_bug.lean.expected.out | 2 +- tests/lean/tactic_state_pp.lean.expected.out | 5 +- tests/lean/whnf.lean.expected.out | 60 +++++++--- tests/lean/whnf_cache_bug.lean.expected.out | 30 +++-- tests/lean/whnf_core1.lean.expected.out | 120 +++++++++++++------ 8 files changed, 154 insertions(+), 69 deletions(-) diff --git a/tests/lean/pp_all.lean.expected.out b/tests/lean/pp_all.lean.expected.out index 1991b6fb61..da85ea18f5 100644 --- a/tests/lean/pp_all.lean.expected.out +++ b/tests/lean/pp_all.lean.expected.out @@ -1,4 +1,4 @@ -a + of_num b = 10 : Prop +(λ (x : ℕ), x) a + of_num b = 10 : Prop @eq.{1} nat (@add.{1} nat nat.has_add ((λ (x : nat), x) a) (nat.of_num b)) (@bit0.{1} nat nat.has_add (@bit1.{1} nat nat.has_one nat.has_add (@bit0.{1} nat nat.has_add (@one.{1} nat nat.has_one)))) : diff --git a/tests/lean/pp_beta.lean b/tests/lean/pp_beta.lean index 1ff93c06a2..a53fed304d 100644 --- a/tests/lean/pp_beta.lean +++ b/tests/lean/pp_beta.lean @@ -2,6 +2,6 @@ open nat check (λ x : nat, x) 1 -set_option pp.beta false +set_option pp.beta true check (λ x : nat, x) 1 diff --git a/tests/lean/pp_beta.lean.expected.out b/tests/lean/pp_beta.lean.expected.out index e214e6af9a..4104aed04c 100644 --- a/tests/lean/pp_beta.lean.expected.out +++ b/tests/lean/pp_beta.lean.expected.out @@ -1,2 +1,2 @@ -1 : ℕ (λ (x : ℕ), x) 1 : ℕ +1 : ℕ diff --git a/tests/lean/quot_ind_bug.lean.expected.out b/tests/lean/quot_ind_bug.lean.expected.out index f8d085512b..ea5f984b8e 100644 --- a/tests/lean/quot_ind_bug.lean.expected.out +++ b/tests/lean/quot_ind_bug.lean.expected.out @@ -1,3 +1,3 @@ -ind c ⟦a⟧ : B ⟦a⟧ +ind c ⟦a⟧ : (λ (_x : quot s), B _x) ⟦a⟧ c a : B ⟦a⟧ c a diff --git a/tests/lean/tactic_state_pp.lean.expected.out b/tests/lean/tactic_state_pp.lean.expected.out index f9eca5f3e4..0224248a42 100644 --- a/tests/lean/tactic_state_pp.lean.expected.out +++ b/tests/lean/tactic_state_pp.lean.expected.out @@ -1,8 +1,9 @@ tactic_state_pp.lean:31:0: error: tactic failed, there are unsolved goals state: My custom goal visualizer -Goal: ∀ {n_1 : ℕ} (a : α) (a_1 : Vec α n_1), n = nat.succ n_1 → v == Vec.cons a a_1 → f v ≠ 2 +Goal: ∀ {n_1 : ℕ} (a : α) (a_1 : Vec α n_1), + (λ (a : ℕ) (w : Vec α a), n = a → v == w → f v ≠ 2) (nat.succ n_1) (Vec.cons a a_1) tactic_state_pp.lean:39:0: error: tactic failed, there are unsolved goals state: My custom goal visualizer -Goal: ∀ (a : ℕ), n = succ a → 0 < n → succ (pred n) = n +Goal: ∀ (a : ℕ), (λ (w : ℕ), n = w → 0 < n → succ (pred n) = n) (succ a) diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out index a4a924faf4..f2636fa557 100644 --- a/tests/lean/whnf.lean.expected.out +++ b/tests/lean/whnf.lean.expected.out @@ -2,15 +2,27 @@ succ (prod.fst (prod.fst (nat.rec - (λ (a : ℕ), - nat.cases_on 0 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a)) - poly_unit.star, poly_unit.star) - (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a), - (λ (a_1 : ℕ), - nat.cases_on (succ a) (λ (_F : nat.below 0), a_1) - (λ (a : ℕ) (_F : nat.below (succ a)), succ (prod.fst (prod.fst _F) a_1)) - (ih_1, poly_unit.star), ih_1, poly_unit.star)) + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + 0 + poly_unit.star, poly_unit.star) + (λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a), + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + (succ a) + (ih_1, poly_unit.star), ih_1, poly_unit.star)) 0, poly_unit.star)) 2) 3 @@ -18,15 +30,27 @@ succ (prod.fst (prod.fst (nat.rec - (λ (a : ℕ), - nat.cases_on 0 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a)) - poly_unit.star, poly_unit.star) - (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a), - (λ (a_1 : ℕ), - nat.cases_on (succ a) (λ (_F : nat.below 0), a_1) - (λ (a : ℕ) (_F : nat.below (succ a)), succ (prod.fst (prod.fst _F) a_1)) - (ih_1, poly_unit.star), ih_1, poly_unit.star)) + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + 0 + poly_unit.star, poly_unit.star) + (λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a), + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + (succ a) + (ih_1, poly_unit.star), ih_1, poly_unit.star)) 0, poly_unit.star)) a) succ a diff --git a/tests/lean/whnf_cache_bug.lean.expected.out b/tests/lean/whnf_cache_bug.lean.expected.out index dcea7006b6..cdffb0371a 100644 --- a/tests/lean/whnf_cache_bug.lean.expected.out +++ b/tests/lean/whnf_cache_bug.lean.expected.out @@ -3,14 +3,26 @@ nat.succ (prod.fst (prod.fst (nat.rec - (λ (a : ℕ), - nat.cases_on 0 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) - poly_unit.star, poly_unit.star) - (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a), - (λ (a_1 : ℕ), - nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1) - (λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1)) - (ih_1, poly_unit.star), ih_1, poly_unit.star)) + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + 0 + poly_unit.star, poly_unit.star) + (λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a), + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + (nat.succ a) + (ih_1, poly_unit.star), ih_1, poly_unit.star)) 0, poly_unit.star)) 1) diff --git a/tests/lean/whnf_core1.lean.expected.out b/tests/lean/whnf_core1.lean.expected.out index 95ae6e5c04..2465ef7496 100644 --- a/tests/lean/whnf_core1.lean.expected.out +++ b/tests/lean/whnf_core1.lean.expected.out @@ -2,27 +2,51 @@ nat.succ (prod.fst (prod.fst (nat.rec - (λ (a : ℕ), - nat.cases_on 0 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) - poly_unit.star, poly_unit.star) - (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a), - (λ (a_1 : ℕ), - nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1) - (λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1)) - (ih_1, poly_unit.star), ih_1, poly_unit.star)) + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + 0 + poly_unit.star, poly_unit.star) + (λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a), + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + (nat.succ a) + (ih_1, poly_unit.star), ih_1, poly_unit.star)) (prod.fst (prod.fst (nat.rec - (λ (a : ℕ), - nat.cases_on 0 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) - poly_unit.star, poly_unit.star) - (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a), - (λ (a_1 : ℕ), - nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1) - (λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1)) - (ih_1, poly_unit.star), ih_1, poly_unit.star)) + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + 0 + poly_unit.star, poly_unit.star) + (λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a), + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + (nat.succ a) + (ih_1, poly_unit.star), ih_1, poly_unit.star)) 0, poly_unit.star)) 1), poly_unit.star)) a) @@ -30,27 +54,51 @@ nat.succ (prod.fst (prod.fst (nat.rec - (λ (a : ℕ), - nat.cases_on 0 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) - poly_unit.star, poly_unit.star) - (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a), - (λ (a_1 : ℕ), - nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1) - (λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1)) - (ih_1, poly_unit.star), ih_1, poly_unit.star)) + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + 0 + poly_unit.star, poly_unit.star) + (λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a), + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + (nat.succ a) + (ih_1, poly_unit.star), ih_1, poly_unit.star)) (prod.fst (prod.fst (nat.rec - (λ (a : ℕ), - nat.cases_on 0 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) - poly_unit.star, poly_unit.star) - (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a), - (λ (a_1 : ℕ), - nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1) - (λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1)) - (ih_1, poly_unit.star), ih_1, poly_unit.star)) + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + 0 + poly_unit.star, poly_unit.star) + (λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a), + ((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + (λ (a a_1 : ℕ) (_F : nat.below a_1), + nat.cases_on a_1 (λ (_F : nat.below 0), a) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a)) + _F) + a_1 + a + _F) + (nat.succ a) + (ih_1, poly_unit.star), ih_1, poly_unit.star)) 0, poly_unit.star)) 1), poly_unit.star)) a)