From dcc314c109d54b43a1c12e8a4d8c453821e2db54 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Sep 2016 14:02:23 -0700 Subject: [PATCH] feat(library/noncomputable): improve is_noncomputable --- src/library/CMakeLists.txt | 2 +- src/library/constants.cpp | 12 ++++++++++ src/library/constants.h | 3 +++ src/library/constants.txt | 3 +++ src/library/library_system.cpp | 20 ++++++++++++++++ src/library/library_system.h | 13 ++++++++++ src/library/noncomputable.cpp | 24 +++++++++++++------ tests/lean/def_ite_value.lean | 2 +- tests/lean/defeq_simp_lemmas1.lean | 10 ++++---- tests/lean/defeq_simp_lemmas2.lean | 10 ++++---- tests/lean/inst.lean | 4 ++-- tests/lean/inst.lean.expected.out | 4 ---- tests/lean/nested1.lean | 2 +- tests/lean/nested1.lean.expected.out | 6 ++--- tests/lean/pattern_pp.lean | 2 +- tests/lean/pattern_pp.lean.expected.out | 2 -- tests/lean/pp_no_proofs.lean | 2 +- tests/lean/pp_no_proofs.lean.expected.out | 2 -- tests/lean/red.lean | 2 +- tests/lean/red.lean.expected.out | 2 -- tests/lean/run/basic.lean | 14 +++++------ tests/lean/run/class11.lean | 2 +- tests/lean/run/dsimp_at1.lean | 2 +- tests/lean/run/fun_info1.lean | 2 +- tests/lean/run/imp.lean | 18 +++++++------- tests/lean/run/impbug1.lean | 2 +- tests/lean/run/impbug2.lean | 2 +- tests/lean/run/impbug3.lean | 2 +- tests/lean/run/impbug4.lean | 2 +- tests/lean/run/kcomp.lean | 2 +- tests/lean/run/match_convoy.lean | 12 +++++----- tests/lean/run/occurs_check_bug1.lean | 2 +- tests/lean/run/over_subst.lean | 2 +- tests/lean/run/pack_unpack1.lean | 5 +++- tests/lean/run/pquot.lean | 6 ++--- tests/lean/run/section3.lean | 2 +- tests/lean/run/sigma_match.lean | 8 +++---- tests/lean/run/simp_ext_refl.lean | 2 +- .../run/simplifier_canonize_instances.lean | 4 ++-- tests/lean/run/simplifier_synth_congr.lean | 4 ++-- tests/lean/run/simplifier_topdown.lean | 2 +- tests/lean/run/sorry.lean | 2 +- tests/lean/run/unification_hints.lean | 4 ++-- tests/lean/run/unreachable_cases.lean | 6 ++--- tests/lean/t5.lean | 6 ++--- tests/lean/t5.lean.expected.out | 6 ----- tests/lean/unification_hints1.lean | 8 +++---- .../lean/unification_hints1.lean.expected.out | 8 ------- 48 files changed, 151 insertions(+), 113 deletions(-) create mode 100644 src/library/library_system.cpp create mode 100644 src/library/library_system.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 498a524120..7c16b0ed08 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -14,7 +14,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp inductive.cpp mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp - aux_definition.cpp inverse.cpp + aux_definition.cpp inverse.cpp library_system.cpp # Legacy -- The following files will be eventually deleted normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 50d861a650..d3c0eec155 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -77,6 +77,7 @@ name const * g_fin = nullptr; name const * g_fin_mk = nullptr; name const * g_funext = nullptr; name const * g_ge = nullptr; +name const * g_get_line = nullptr; name const * g_gt = nullptr; name const * g_has_add = nullptr; name const * g_has_div = nullptr; @@ -265,6 +266,8 @@ name const * g_prod_pr2 = nullptr; name const * g_propext = nullptr; name const * g_pexpr = nullptr; name const * g_pexpr_subst = nullptr; +name const * g_put_str = nullptr; +name const * g_put_nat = nullptr; name const * g_to_pexpr = nullptr; name const * g_quot_mk = nullptr; name const * g_quot_lift = nullptr; @@ -415,6 +418,7 @@ void initialize_constants() { g_fin_mk = new name{"fin", "mk"}; g_funext = new name{"funext"}; g_ge = new name{"ge"}; + g_get_line = new name{"get_line"}; g_gt = new name{"gt"}; g_has_add = new name{"has_add"}; g_has_div = new name{"has_div"}; @@ -603,6 +607,8 @@ void initialize_constants() { g_propext = new name{"propext"}; g_pexpr = new name{"pexpr"}; g_pexpr_subst = new name{"pexpr", "subst"}; + g_put_str = new name{"put_str"}; + g_put_nat = new name{"put_nat"}; g_to_pexpr = new name{"to_pexpr"}; g_quot_mk = new name{"quot", "mk"}; g_quot_lift = new name{"quot", "lift"}; @@ -754,6 +760,7 @@ void finalize_constants() { delete g_fin_mk; delete g_funext; delete g_ge; + delete g_get_line; delete g_gt; delete g_has_add; delete g_has_div; @@ -942,6 +949,8 @@ void finalize_constants() { delete g_propext; delete g_pexpr; delete g_pexpr_subst; + delete g_put_str; + delete g_put_nat; delete g_to_pexpr; delete g_quot_mk; delete g_quot_lift; @@ -1092,6 +1101,7 @@ name const & get_fin_name() { return *g_fin; } name const & get_fin_mk_name() { return *g_fin_mk; } name const & get_funext_name() { return *g_funext; } name const & get_ge_name() { return *g_ge; } +name const & get_get_line_name() { return *g_get_line; } name const & get_gt_name() { return *g_gt; } name const & get_has_add_name() { return *g_has_add; } name const & get_has_div_name() { return *g_has_div; } @@ -1280,6 +1290,8 @@ name const & get_prod_pr2_name() { return *g_prod_pr2; } name const & get_propext_name() { return *g_propext; } name const & get_pexpr_name() { return *g_pexpr; } name const & get_pexpr_subst_name() { return *g_pexpr_subst; } +name const & get_put_str_name() { return *g_put_str; } +name const & get_put_nat_name() { return *g_put_nat; } name const & get_to_pexpr_name() { return *g_to_pexpr; } name const & get_quot_mk_name() { return *g_quot_mk; } name const & get_quot_lift_name() { return *g_quot_lift; } diff --git a/src/library/constants.h b/src/library/constants.h index a3900106d3..59b5a17f9d 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -79,6 +79,7 @@ name const & get_fin_name(); name const & get_fin_mk_name(); name const & get_funext_name(); name const & get_ge_name(); +name const & get_get_line_name(); name const & get_gt_name(); name const & get_has_add_name(); name const & get_has_div_name(); @@ -267,6 +268,8 @@ name const & get_prod_pr2_name(); name const & get_propext_name(); name const & get_pexpr_name(); name const & get_pexpr_subst_name(); +name const & get_put_str_name(); +name const & get_put_nat_name(); name const & get_to_pexpr_name(); name const & get_quot_mk_name(); name const & get_quot_lift_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index a4ccf3ac83..5f32628974 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -72,6 +72,7 @@ fin fin.mk funext ge +get_line gt has_add has_div @@ -260,6 +261,8 @@ prod.pr2 propext pexpr pexpr.subst +put_str +put_nat to_pexpr quot.mk quot.lift diff --git a/src/library/library_system.cpp b/src/library/library_system.cpp new file mode 100644 index 0000000000..d9199eb8f8 --- /dev/null +++ b/src/library/library_system.cpp @@ -0,0 +1,20 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/name.h" +#include "library/constants.h" + +namespace lean { +bool is_system_builtin(name const & n) { + return + n == get_IO_name() || + n == get_functorIO_name() || + n == get_monadIO_name() || + n == get_put_str_name() || + n == get_put_nat_name() || + n == get_get_line_name(); +} +} diff --git a/src/library/library_system.h b/src/library/library_system.h new file mode 100644 index 0000000000..9cd202ef8b --- /dev/null +++ b/src/library/library_system.h @@ -0,0 +1,13 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/name.h" + +namespace lean { +/** \brief Return true iff \c n is the name of a builtin constant from the library.system folder. */ +bool is_system_builtin(name const & n); +} diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp index ba74cc91ad..5c045eb76b 100644 --- a/src/library/noncomputable.cpp +++ b/src/library/noncomputable.cpp @@ -8,10 +8,11 @@ Author: Leonardo de Moura #include #include "util/sstream.h" #include "kernel/for_each_fn.h" +#include "kernel/type_checker.h" #include "library/module.h" #include "library/util.h" #include "library/fingerprint.h" -#include "library/old_type_checker.h" +#include "library/library_system.h" namespace lean { struct noncomputable_ext : public environment_extension { @@ -49,15 +50,24 @@ static void noncomputable_reader(deserializer & d, shared_environment & senv, }); } -static bool is_noncomputable(old_type_checker & tc, noncomputable_ext const & ext, name const & n) { +static bool is_noncomputable(type_checker & tc, noncomputable_ext const & ext, name const & n) { + environment const & env = tc.env(); if (ext.m_noncomputable.contains(n)) return true; - declaration const & d = tc.env().get(n); - return d.is_axiom() && !tc.is_prop(d.get_type()).first; + declaration const & d = env.get(n); + if (!d.is_trusted()) { + return false; /* ignore nontrusted definitions */ + } else if (d.is_axiom() && !tc.is_prop(d.get_type())) { + return true; + } else if (d.is_constant_assumption()) { + return !env.is_builtin(d.get_name()) && !is_system_builtin(d.get_name()) && !tc.is_prop(d.get_type()); + } else { + return false; + } } bool is_noncomputable(environment const & env, name const & n) { - old_type_checker tc(env); + type_checker tc(env); auto ext = get_extension(env); return is_noncomputable(tc, ext, n); } @@ -80,8 +90,8 @@ optional get_noncomputable_reason(environment const & env, name const & n) declaration const & d = env.get(n); if (!d.is_definition()) return optional(); - old_type_checker tc(env); - if (tc.is_prop(d.get_type()).first) + type_checker tc(env); + if (tc.is_prop(d.get_type())) return optional(); // definition is a proposition, then do nothing expr const & v = d.get_value(); auto ext = get_extension(env); diff --git a/tests/lean/def_ite_value.lean b/tests/lean/def_ite_value.lean index 7575a65fdc..2274710a42 100644 --- a/tests/lean/def_ite_value.lean +++ b/tests/lean/def_ite_value.lean @@ -1,5 +1,5 @@ set_option new_elaborator true - +set_option eqn_compiler.lemmas false -- TODO(Leo): remove definition f : string → nat → nat | "hello world" 1 := 0 | "hello world" _ := 1 diff --git a/tests/lean/defeq_simp_lemmas1.lean b/tests/lean/defeq_simp_lemmas1.lean index b69080c86a..ece08b3b86 100644 --- a/tests/lean/defeq_simp_lemmas1.lean +++ b/tests/lean/defeq_simp_lemmas1.lean @@ -2,11 +2,11 @@ namespace foo universe l constants (A : Type.{l}) -definition q (x : A) := x -definition h (x : A) : A := q x -definition g (x y : A) := h y -definition f (x y z : A) := g (g x y) z -definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z) +noncomputable definition q (x : A) := x +noncomputable definition h (x : A) : A := q x +noncomputable definition g (x y : A) := h y +noncomputable definition f (x y z : A) := g (g x y) z +noncomputable definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z) attribute [defeq] definition h.def (x : A) : h x = q x := rfl diff --git a/tests/lean/defeq_simp_lemmas2.lean b/tests/lean/defeq_simp_lemmas2.lean index 0dec67f0ab..99f04490ef 100644 --- a/tests/lean/defeq_simp_lemmas2.lean +++ b/tests/lean/defeq_simp_lemmas2.lean @@ -2,11 +2,11 @@ namespace foo universe l constants (A : Type.{l}) -definition q (x : A) := x -definition h (x : A) : A := q x -definition g (x y : A) := h y -definition f (x y z : A) := g (g x y) z -definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z) +noncomputable definition q (x : A) := x +noncomputable definition h (x : A) : A := q x +noncomputable definition g (x y : A) := h y +noncomputable definition f (x y z : A) := g (g x y) z +noncomputable definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z) attribute [defeq] definition h.rfl (x : A) : h x = x := rfl diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean index 0c0d275211..38839d554a 100644 --- a/tests/lean/inst.lean +++ b/tests/lean/inst.lean @@ -9,7 +9,7 @@ C.rec (λa, a) c constant magic (A : Type) : A attribute [instance, priority std.priority.max] -definition C_magic (A : Type) : C A := +noncomputable definition C_magic (A : Type) : C A := C.mk (magic A) attribute [instance] @@ -21,6 +21,6 @@ definition C_prod {A B : Type} (Ha : C A) (Hb : C B) : C (prod A B) := C.mk (prod.mk (val Ha) (val Hb)) -- C_magic will be used because it has max priority -definition test : C (prod Prop Prop) := _ +noncomputable definition test : C (prod Prop Prop) := _ eval test diff --git a/tests/lean/inst.lean.expected.out b/tests/lean/inst.lean.expected.out index a043d28ac0..4c24c7b80a 100644 --- a/tests/lean/inst.lean.expected.out +++ b/tests/lean/inst.lean.expected.out @@ -1,5 +1 @@ -inst.lean:12:11:failed to generate bytecode for 'C_magic' -code generation failed, VM does not have code for 'magic' -inst.lean:24:11:failed to generate bytecode for 'test' -code generation failed, VM does not have code for 'magic' C.mk (magic (prod Prop Prop)) diff --git a/tests/lean/nested1.lean b/tests/lean/nested1.lean index 4303568fe7..ae81a009e1 100644 --- a/tests/lean/nested1.lean +++ b/tests/lean/nested1.lean @@ -5,7 +5,7 @@ namespace test constant foo (a : nat) : a > 0 → nat -definition bla (a : nat) := +noncomputable definition bla (a : nat) := foo (succ (succ a)) abstract as foo.prf lt.step (zero_lt_succ a) end diff --git a/tests/lean/nested1.lean.expected.out b/tests/lean/nested1.lean.expected.out index 0a8734d48c..5703c84221 100644 --- a/tests/lean/nested1.lean.expected.out +++ b/tests/lean/nested1.lean.expected.out @@ -1,11 +1,9 @@ -nested1.lean:8:11:failed to generate bytecode for 'test.bla' -code generation failed, VM does not have code for 'test.foo' attribute [irreducible] definition test.foo.prf : ∀ (x : ℕ), 0 < succ (succ x) := λ x, lt.step (zero_lt_succ x) -definition test.bla : ℕ → ℕ := +noncomputable definition test.bla : ℕ → ℕ := λ a, foo (succ (succ a)) (foo.prf a) -definition test.bla : ℕ → ℕ := +noncomputable definition test.bla : ℕ → ℕ := λ a, test.foo (succ (succ a)) (test.foo.prf a) attribute [irreducible] definition test.foo.prf : ∀ (x : ℕ), 0 < succ (succ x) := diff --git a/tests/lean/pattern_pp.lean b/tests/lean/pattern_pp.lean index ae7aec7af0..64977ca896 100644 --- a/tests/lean/pattern_pp.lean +++ b/tests/lean/pattern_pp.lean @@ -1,4 +1,4 @@ -definition Sum : nat → (nat → nat) → nat := sorry +noncomputable definition Sum : nat → (nat → nat) → nat := sorry attribute [forward] definition Sum_weird (f g h : nat → nat) (n : nat) : (Sum n (λ x, f (g (h x)))) = 1 := sorry print Sum_weird diff --git a/tests/lean/pattern_pp.lean.expected.out b/tests/lean/pattern_pp.lean.expected.out index 0b435e79c4..44952a01f8 100644 --- a/tests/lean/pattern_pp.lean.expected.out +++ b/tests/lean/pattern_pp.lean.expected.out @@ -1,5 +1,3 @@ -pattern_pp.lean:1:11:failed to generate bytecode for 'Sum' -code generation failed, VM does not have code for 'sorry' attribute [forward] definition Sum_weird : ∀ (f g h : ℕ → ℕ) (n : ℕ), Sum n (λ (x : ℕ), f (g (h x))) = 1 := λ f g h n, sorry diff --git a/tests/lean/pp_no_proofs.lean b/tests/lean/pp_no_proofs.lean index ad7d88004a..8eb0fefa70 100644 --- a/tests/lean/pp_no_proofs.lean +++ b/tests/lean/pp_no_proofs.lean @@ -5,7 +5,7 @@ constants (P : ∀ {t:true}, ℕ → Prop) (P0 : @P trivial 0) (Ps : ∀ {n}, @P trivial n → @P trivial (succ n)) (f : Π {n}, @P trivial n → ℕ) -definition messy := f (Ps (Ps (Ps (Ps (Ps (Ps P0)))))) +noncomputable definition messy := f (Ps (Ps (Ps (Ps (Ps (Ps P0)))))) eval messy set_option pp.proofs false diff --git a/tests/lean/pp_no_proofs.lean.expected.out b/tests/lean/pp_no_proofs.lean.expected.out index dd08979c42..b38300d0d0 100644 --- a/tests/lean/pp_no_proofs.lean.expected.out +++ b/tests/lean/pp_no_proofs.lean.expected.out @@ -1,5 +1,3 @@ -pp_no_proofs.lean:8:11:failed to generate bytecode for 'messy' -code generation failed, VM does not have code for 'f' f (Ps (Ps (Ps (Ps (Ps (Ps P0)))))) f ⌞P 6⌟ @f 6 ⌞@P ⌞true⌟ 6⌟ diff --git a/tests/lean/red.lean b/tests/lean/red.lean index 3db428b718..2943daddc3 100644 --- a/tests/lean/red.lean +++ b/tests/lean/red.lean @@ -1,6 +1,6 @@ constant g : nat → nat -definition f := g +noncomputable definition f := g example : f = g := rfl diff --git a/tests/lean/red.lean.expected.out b/tests/lean/red.lean.expected.out index 3162d87030..a2b3324ba2 100644 --- a/tests/lean/red.lean.expected.out +++ b/tests/lean/red.lean.expected.out @@ -1,5 +1,3 @@ -red.lean:3:11:failed to generate bytecode for 'f' -code generation failed, VM does not have code for 'g' red.lean:9:19: error: type mismatch at definition 'example', has type f = f but is expected to have type diff --git a/tests/lean/run/basic.lean b/tests/lean/run/basic.lean index ead66d56a8..e42fe5d09c 100644 --- a/tests/lean/run/basic.lean +++ b/tests/lean/run/basic.lean @@ -5,7 +5,7 @@ definition tst.{l} (A : Type) (B : Type) (C : Type.{l}) : Type := A → B → C check tst constant group.{l} : Type.{l+1} constant carrier.{l} : group.{l} → Type.{l} -definition to_carrier (g : group) := carrier g +noncomputable definition to_carrier (g : group) := carrier g check to_carrier.{1} @@ -44,8 +44,8 @@ section variable {T2 : Type.{l}} variable {T3 : Type.{u}} variable f : T1 → T2 → T2 - definition is_proj2 := ∀ x y, f x y = y - definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z + noncomputable definition is_proj2 := ∀ x y, f x y = y + noncomputable definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z end check @is_proj2.{1} @@ -56,8 +56,8 @@ section variables {T1 T2 : Type} variable {T3 : Type} variable f : T1 → T2 → T2 - definition is_proj2 := ∀ x y, f x y = y - definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z + noncomputable definition is_proj2 := ∀ x y, f x y = y + noncomputable definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z end check @foo.is_proj2.{1} check @foo.is_proj3.{1 2} @@ -69,8 +69,8 @@ section variable {T2 : Type} variable {T3 : Type} variable f : T1 → T2 → T2 - definition is_proj2 := ∀ x y, f x y = y - definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z + noncomputable definition is_proj2 := ∀ x y, f x y = y + noncomputable definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z end check @bla.is_proj2.{1 2} check @bla.is_proj3.{1 2 3} diff --git a/tests/lean/run/class11.lean b/tests/lean/run/class11.lean index 8e86eb595f..e45990c683 100644 --- a/tests/lean/run/class11.lean +++ b/tests/lean/run/class11.lean @@ -2,5 +2,5 @@ inductive [class] C {A : Type} : A → Prop constant f {A : Type} (a : A) [H : C a] : Prop -definition g {A : Type} (a b : A) {H1 : C a} {H2 : C b} : Prop := +noncomputable definition g {A : Type} (a b : A) {H1 : C a} {H2 : C b} : Prop := f a ∧ f b diff --git a/tests/lean/run/dsimp_at1.lean b/tests/lean/run/dsimp_at1.lean index 2396b3df7b..7cb34d7926 100644 --- a/tests/lean/run/dsimp_at1.lean +++ b/tests/lean/run/dsimp_at1.lean @@ -2,7 +2,7 @@ open tactic constants (A : Type.{1}) (x y : A) -definition f (z : A) : A := z +noncomputable definition f (z : A) : A := z attribute [defeq] definition f.def (z:A) : f z = z := rfl diff --git a/tests/lean/run/fun_info1.lean b/tests/lean/run/fun_info1.lean index 5fe4a31ad5..b7162f19f7 100644 --- a/tests/lean/run/fun_info1.lean +++ b/tests/lean/run/fun_info1.lean @@ -1,7 +1,7 @@ open tactic set_option pp.binder_types true -definition foo (A : Type) : A → A := +noncomputable definition foo (A : Type) : A → A := sorry example (a : nat) (H : foo unit () = ()) : true := diff --git a/tests/lean/run/imp.lean b/tests/lean/run/imp.lean index 0a9721f681..a3027e742d 100644 --- a/tests/lean/run/imp.lean +++ b/tests/lean/run/imp.lean @@ -8,10 +8,10 @@ check @f a check @f a b check @f a b c -definition l1 : N → N → N → N := @f -definition l2 : N → N → N := @f a -definition l3 : N → N := @f a b -definition l4 : N := @f a b c +noncomputable definition l1 : N → N → N → N := @f +noncomputable definition l2 : N → N → N := @f a +noncomputable definition l3 : N → N := @f a b +noncomputable definition l4 : N := @f a b c constant g : forall ⦃a b : N⦄, N → N @@ -22,8 +22,8 @@ check @g a check @g a b check @g a b c -definition l5 : N → N → N → N := @g -definition l6 : N → N → N := @g a -definition l7 : N → N := @g a b -definition l8 : N := @g a b c -definition l9 : N → N → N → N := g +noncomputable definition l5 : N → N → N → N := @g +noncomputable definition l6 : N → N → N := @g a +noncomputable definition l7 : N → N := @g a b +noncomputable definition l8 : N := @g a b c +noncomputable definition l9 : N → N → N → N := g diff --git a/tests/lean/run/impbug1.lean b/tests/lean/run/impbug1.lean index ce04acbc96..a0ca653d54 100644 --- a/tests/lean/run/impbug1.lean +++ b/tests/lean/run/impbug1.lean @@ -9,7 +9,7 @@ inductive category (ob : Type) (mor : ob → ob → Type) : Type | mk : Π (id : Π (A : ob), mor A A), (Π (A B : ob) (f : mor A A), id A = f) → category -definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat +noncomputable definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat attribute id [reducible] theorem id_left (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) (A : ob) (f : mor A A) : diff --git a/tests/lean/run/impbug2.lean b/tests/lean/run/impbug2.lean index d03b883f02..e3c7b06340 100644 --- a/tests/lean/run/impbug2.lean +++ b/tests/lean/run/impbug2.lean @@ -9,7 +9,7 @@ inductive category (ob : Type) (mor : ob → ob → Type) : Type | mk : Π (id : Π (A : ob), mor A A), (Π (A B : ob) (f : mor A A), id A = f) → category -definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat +noncomputable definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat constant ob : Type.{1} constant mor : ob → ob → Type.{1} constant Cat : category ob mor diff --git a/tests/lean/run/impbug3.lean b/tests/lean/run/impbug3.lean index 886225418d..51c800faad 100644 --- a/tests/lean/run/impbug3.lean +++ b/tests/lean/run/impbug3.lean @@ -12,7 +12,7 @@ inductive category : Type | mk : Π (id : Π (A : ob), mor A A), (Π (A B : ob) (f : mor A A), id A = f) → category -definition id (Cat : category) := category.rec (λ id idl, id) Cat +noncomputable definition id (Cat : category) := category.rec (λ id idl, id) Cat constant Cat : category attribute id [reducible] diff --git a/tests/lean/run/impbug4.lean b/tests/lean/run/impbug4.lean index 3a44e3bf93..e7d65a9b9d 100644 --- a/tests/lean/run/impbug4.lean +++ b/tests/lean/run/impbug4.lean @@ -12,7 +12,7 @@ inductive category : Type | mk : Π (id : Π (A : ob), mor A A), (Π (A B : ob) (f : mor A A), id A = f) → category -definition id (Cat : category) := category.rec (λ id idl, id) Cat +noncomputable definition id (Cat : category) := category.rec (λ id idl, id) Cat constant Cat : category print "-----------------" diff --git a/tests/lean/run/kcomp.lean b/tests/lean/run/kcomp.lean index 7530cac722..bada12ea11 100644 --- a/tests/lean/run/kcomp.lean +++ b/tests/lean/run/kcomp.lean @@ -16,7 +16,7 @@ check λ H : a = a, H₂ inductive to_type {B : Type} : B → Type | mk : Π (b : B), to_type b -definition tst1 : to_type (λ H : a = a, H₂) := to_type.mk (@eq.rec A a P H₂ a) +noncomputable definition tst1 : to_type (λ H : a = a, H₂) := to_type.mk (@eq.rec A a P H₂ a) check to_type.mk(λ H : a = a, H₂) check to_type.mk(@eq.rec A a P H₂ a) check to_type.mk(λ H : a = a, H₂) = to_type.mk(@eq.rec A a P H₂ a) diff --git a/tests/lean/run/match_convoy.lean b/tests/lean/run/match_convoy.lean index aac2e023de..d91d648a27 100644 --- a/tests/lean/run/match_convoy.lean +++ b/tests/lean/run/match_convoy.lean @@ -27,21 +27,21 @@ end constant bag_setoid : ∀ A, setoid (list A) attribute [instance] bag_setoid -definition bag (A : Type) : Type := +noncomputable definition bag (A : Type) : Type := quot (bag_setoid A) constant subcount : ∀ {A}, list A → list A → bool constant list.count : ∀ {A}, A → list A → nat constant all_of_subcount_eq_tt : ∀ {A} {l₁ l₂ : list A}, subcount l₁ l₂ = tt → ∀ a, list.count a l₁ ≤ list.count a l₂ constant ex_of_subcount_eq_ff : ∀ {A} {l₁ l₂ : list A}, subcount l₁ l₂ = ff → ∃ a, ¬ list.count a l₁ ≤ list.count a l₂ -definition count {A} (a : A) (b : bag A) : nat := +noncomputable definition count {A} (a : A) (b : bag A) : nat := quot.lift_on b (λ l, list.count a l) (λ l₁ l₂ h, sorry) -definition subbag {A} (b₁ b₂ : bag A) := ∀ a, count a b₁ ≤ count a b₂ +noncomputable definition subbag {A} (b₁ b₂ : bag A) := ∀ a, count a b₁ ≤ count a b₂ infix ⊆ := subbag attribute [instance] -definition decidable_subbag {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) := +noncomputable definition decidable_subbag {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) := quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂, match subcount l₁ l₂, rfl : ∀ (b : _), subcount l₁ l₂ = b → _ with | tt, H := decidable.tt (all_of_subcount_eq_tt H) @@ -51,7 +51,7 @@ quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂, end) attribute [instance] -definition decidable_subbag2 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) := +noncomputable definition decidable_subbag2 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) := quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂, match sigma.mk (subcount l₁ l₂) rfl : (Σ (b : _), subcount l₁ l₂ = b) → _ with | sigma.mk tt H := decidable.tt (all_of_subcount_eq_tt H) @@ -63,7 +63,7 @@ quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂, local notation ⟦ a , b ⟧ := sigma.mk a b attribute [instance] -definition decidable_subbag3 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) := +noncomputable definition decidable_subbag3 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) := quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂, match ⟦subcount l₁ l₂, rfl⟧ : (Σ (b : _), subcount l₁ l₂ = b) → _ with | ⟦tt, H⟧ := decidable.tt (all_of_subcount_eq_tt H) diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean index d8754e7db2..1dfb4040d3 100644 --- a/tests/lean/run/occurs_check_bug1.lean +++ b/tests/lean/run/occurs_check_bug1.lean @@ -6,7 +6,7 @@ infixl `mod`:70 := modulo1 constant gcd_aux : ℕ × ℕ → ℕ -definition gcd (x y : ℕ) : ℕ := gcd_aux (x, y) +noncomputable definition gcd (x y : ℕ) : ℕ := gcd_aux (x, y) theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (nat.has_decidable_eq (pr2 (x, y)) 0) nat x (gcd y (x mod y)) := sorry diff --git a/tests/lean/run/over_subst.lean b/tests/lean/run/over_subst.lean index 890c2bcc34..2ee32a308e 100644 --- a/tests/lean/run/over_subst.lean +++ b/tests/lean/run/over_subst.lean @@ -19,7 +19,7 @@ infixl `+` := add infix `≤` := le axiom add_assoc (a b c : int) : (a + b) + c = a + (b + c) axiom add_le_left {a b : int} (H : a ≤ b) (c : int) : c + a ≤ c + b -definition lt (a b : int) := a + one1 ≤ b +noncomputable definition lt (a b : int) := a + one1 ≤ b infix `<` := lt end int diff --git a/tests/lean/run/pack_unpack1.lean b/tests/lean/run/pack_unpack1.lean index 45de0e21fa..b19c66c587 100644 --- a/tests/lean/run/pack_unpack1.lean +++ b/tests/lean/run/pack_unpack1.lean @@ -61,10 +61,13 @@ constant P {A : Type} : tree A → Type₁ constant mk1 {A : Type} (a : A) : P (tree.leaf a) constant mk2 {A : Type} (l : list (tree A)) : P (tree.node l) -definition bla {A : Type} : ∀ n : tree A, P n +noncomputable definition bla {A : Type} : ∀ n : tree A, P n | (tree.leaf a) := mk1 a | (tree.node l) := mk2 l +check bla._main.equations.eqn_1 +check bla._main.equations.eqn_2 + definition foo {A : Type} : nat → tree A → nat | 0 _ := 0 | (n+1) (tree.leaf a) := 0 diff --git a/tests/lean/run/pquot.lean b/tests/lean/run/pquot.lean index 057dc41e4f..9c93bcc286 100644 --- a/tests/lean/run/pquot.lean +++ b/tests/lean/run/pquot.lean @@ -31,7 +31,7 @@ have aux : ∀ (P : pquot R → Prop), P (pquot.abs R a) → P (pquot.abs R b), pquot.eqv R H, aux (λ x : pquot R, pquot.abs R a = x) rfl -definition pquot.rec_on {A : Type} {R : A → A → Prop} {C : pquot R → Type} +noncomputable definition pquot.rec_on {A : Type} {R : A → A → Prop} {C : pquot R → Type} (q : pquot R) (f : Π a, C (pquot.abs R a)) (sound : ∀ (a b : A), R a b → f a == f b) @@ -48,7 +48,7 @@ pquot.rec f aux₄ (f a) (f b) aux₁ Ha) q -definition pquot.lift {A : Type} {R : A → A → Prop} {B : Type} +noncomputable definition pquot.lift {A : Type} {R : A → A → Prop} {B : Type} (f : A → B) (sound : ∀ (a b : A), R a b → f a = f b) (q : pquot R) @@ -69,7 +69,7 @@ pquot.rec_on q f (λ (a b : A) (H : R a b), theorem pquot.abs.surjective {A : Type} {R : A → A → Prop} : ∀ q : pquot R, ∃ x : A, pquot.abs R x = q := take q, pquot.induction_on q (take a, exists.intro a rfl) -definition pquot.exact {A : Type} (R : A → A → Prop) := +noncomputable definition pquot.exact {A : Type} (R : A → A → Prop) := ∀ a b : A, pquot.abs R a = pquot.abs R b → R a b -- Definable quotient diff --git a/tests/lean/run/section3.lean b/tests/lean/run/section3.lean index 0623525d24..36620ea715 100644 --- a/tests/lean/run/section3.lean +++ b/tests/lean/run/section3.lean @@ -1,6 +1,6 @@ section parameter (A : Type) definition foo := A - theorem bar {X : Type} {A : X} : foo := + noncomputable definition bar {X : Type} {A : X} : foo := sorry end diff --git a/tests/lean/run/sigma_match.lean b/tests/lean/run/sigma_match.lean index 74f3b5a0ba..a059538683 100644 --- a/tests/lean/run/sigma_match.lean +++ b/tests/lean/run/sigma_match.lean @@ -3,18 +3,18 @@ open sigma constant hom.{l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (a : A) (b : B) : Type.{max l₁ l₂} attribute [reducible] -definition arrow_ob (A B : Type) : Type := +noncomputable definition arrow_ob (A B : Type) : Type := Σ (a : A) (b : B), hom a b -definition src1 {A B : Type} (x : arrow_ob A B) : A := +noncomputable definition src1 {A B : Type} (x : arrow_ob A B) : A := match x with (sigma.mk a (sigma.mk b h)) := a end -definition src2 {A B : Type} : arrow_ob A B → A +noncomputable definition src2 {A B : Type} : arrow_ob A B → A | src2 (sigma.mk a (sigma.mk b c)) := a -definition src3 {A B : Type} (x : arrow_ob A B) : A := +noncomputable definition src3 {A B : Type} (x : arrow_ob A B) : A := match x with (sigma.mk a (sigma.mk b c)) := a end diff --git a/tests/lean/run/simp_ext_refl.lean b/tests/lean/run/simp_ext_refl.lean index b030d20ffd..00cb4f9ee3 100644 --- a/tests/lean/run/simp_ext_refl.lean +++ b/tests/lean/run/simp_ext_refl.lean @@ -3,7 +3,7 @@ open tactic constants (A : Type.{1}) (x y z : A) (g : A → A) (Hg : g y = z) attribute Hg [simp] -definition f (a : A) := y +noncomputable definition f (a : A) := y lemma f.def : ∀ (a), f a = y := λ a, rfl meta_definition simp_f_to_y : tactic unit := mk_eq_simp_ext $ diff --git a/tests/lean/run/simplifier_canonize_instances.lean b/tests/lean/run/simplifier_canonize_instances.lean index da1e073a05..541ed9bc1a 100644 --- a/tests/lean/run/simplifier_canonize_instances.lean +++ b/tests/lean/run/simplifier_canonize_instances.lean @@ -18,8 +18,8 @@ constants (f₁ : Π (X : Type) (X_grp : group X), X) constants (f₂ : Π (X : Type) [X_grp : group X], X) constants (A : Type.{l}) (A_grp₁ : group A) -attribute [irreducible] definition A_grp₂ : group A := A_grp₁ -attribute [irreducible] definition A_grp₃ (t : true) : group A := A_grp₁ +attribute [irreducible] noncomputable definition A_grp₂ : group A := A_grp₁ +attribute [irreducible] noncomputable definition A_grp₃ (t : true) : group A := A_grp₁ set_option simplify.canonize_instances_fixed_point true example : @f₂ A A_grp₁ = @f₂ A A_grp₂ := by simplify_goal_force diff --git a/tests/lean/run/simplifier_synth_congr.lean b/tests/lean/run/simplifier_synth_congr.lean index 9de57eb59c..4df7322f95 100644 --- a/tests/lean/run/simplifier_synth_congr.lean +++ b/tests/lean/run/simplifier_synth_congr.lean @@ -24,8 +24,8 @@ attribute H₂ [simp] example : f A ss_A a₁ a₂ ss_a₁ ss_a₂ = f A ss_A a₁' a₂' ss_a₁' ss_a₂' := by simp -attribute [reducible] definition c₁' := a₁' -attribute [reducible] definition c₂' := a₂' +attribute [reducible] noncomputable definition c₁' := a₁' +attribute [reducible] noncomputable definition c₂' := a₂' example : f A ss_A a₁' a₂' ss_a₁' ss_a₂' = f A ss_A c₁' c₂' ss_a₁' ss_a₂' := by simp example : f A ss_A a₁ a₂ ss_a₁ ss_a₂ = f A ss_A c₁' c₂' ss_a₁' ss_a₂' := by simp diff --git a/tests/lean/run/simplifier_topdown.lean b/tests/lean/run/simplifier_topdown.lean index b0839fec6d..60d7d78aa9 100644 --- a/tests/lean/run/simplifier_topdown.lean +++ b/tests/lean/run/simplifier_topdown.lean @@ -31,7 +31,7 @@ example : w = z := by simp set_option simplify.topdown false example : w = f y := by simp -attribute [reducible] definition u := f (f x) +attribute [reducible] noncomputable definition u := f (f x) set_option simplify.topdown true example : u = z := by simp diff --git a/tests/lean/run/sorry.lean b/tests/lean/run/sorry.lean index 8685e3a5af..395ad20fd9 100644 --- a/tests/lean/run/sorry.lean +++ b/tests/lean/run/sorry.lean @@ -1,4 +1,4 @@ -definition b : Prop := +noncomputable definition b : Prop := sorry theorem tst : true = false := diff --git a/tests/lean/run/unification_hints.lean b/tests/lean/run/unification_hints.lean index c1d302e5dc..2245d730aa 100644 --- a/tests/lean/run/unification_hints.lean +++ b/tests/lean/run/unification_hints.lean @@ -6,10 +6,10 @@ structure unification_hint := (pattern : unification_constraint) (constraints : namespace toy constants (A : Type.{1}) (f h : A → A) (x y z : A) attribute [irreducible] -definition g (x y : A) : A := f z +noncomputable definition g (x y : A) : A := f z attribute [unify] -definition toy_hint (x y : A) : unification_hint := +noncomputable definition toy_hint (x y : A) : unification_hint := unification_hint.mk (unification_constraint.mk (g x y) (f z)) [] open tactic diff --git a/tests/lean/run/unreachable_cases.lean b/tests/lean/run/unreachable_cases.lean index 66d49b9245..09606047a3 100644 --- a/tests/lean/run/unreachable_cases.lean +++ b/tests/lean/run/unreachable_cases.lean @@ -6,14 +6,14 @@ inductive ifin : ℕ → Type -- inductively defined fin-type open ifin -definition foo {N : Type} : Π{n : ℕ}, N → ifin n → (N × ifin n) +noncomputable definition foo {N : Type} : Π{n : ℕ}, N → ifin n → (N × ifin n) | (succ k) n (fz .k) := sorry | (succ k) n (fs x) := sorry -definition bar {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n) +noncomputable definition bar {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n) | (succ k) (n, fz .k) := sorry | (succ k) (n, fs x) := sorry -definition bar2 {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n) +noncomputable definition bar2 {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n) | (succ k) (n, fz .k) := sorry | (succ k) (n, fs x) := sorry diff --git a/tests/lean/t5.lean b/tests/lean/t5.lean index f53b330265..750632b64f 100644 --- a/tests/lean/t5.lean +++ b/tests/lean/t5.lean @@ -1,12 +1,12 @@ constant N : Type.{1} constant f : N → N constant a : N -definition g (a : N) : N := f a +noncomputable definition g (a : N) : N := f a check g namespace foo - definition h : N := f a + noncomputable definition h : N := f a check h - private definition q : N := f a + private noncomputable definition q : N := f a check q end foo check foo.h diff --git a/tests/lean/t5.lean.expected.out b/tests/lean/t5.lean.expected.out index 28f158b99a..479afd3739 100644 --- a/tests/lean/t5.lean.expected.out +++ b/tests/lean/t5.lean.expected.out @@ -1,11 +1,5 @@ -t5.lean:4:11:failed to generate bytecode for 'g' -code generation failed, VM does not have code for 'f' g : N → N -t5.lean:7:13:failed to generate bytecode for 'foo.h' -code generation failed, VM does not have code for 'f' h : N -t5.lean:9:21:failed to generate bytecode for 'private.106392691.q' -code generation failed, VM does not have code for 'f' q : N foo.h : N t5.lean:13:6: error: unknown identifier 'q' diff --git a/tests/lean/unification_hints1.lean b/tests/lean/unification_hints1.lean index 101425e5c0..4ecb6302aa 100644 --- a/tests/lean/unification_hints1.lean +++ b/tests/lean/unification_hints1.lean @@ -7,12 +7,12 @@ structure unification_hint := (pattern : unification_constraint) (constraints : namespace toy constants (A : Type.{1}) (f h : A → A) (x y z : A) attribute [irreducible] -definition g (x y : A) : A := f z +noncomputable definition g (x y : A) : A := f z #unify (g x y), (f z) attribute [unify] -definition toy_hint (x y : A) : unification_hint := +noncomputable definition toy_hint (x y : A) : unification_hint := unification_hint.mk (unification_constraint.mk (g x y) (f z)) [] #unify (g x y), (f z) @@ -44,12 +44,12 @@ definition Canonical.carrier (s : Canonical) : Type := Canonical.rec_on s (λ c op, c) constants (A : Type.{1}) (f : A → A) (x : A) -definition A_canonical : Canonical := Canonical.mk A f +noncomputable definition A_canonical : Canonical := Canonical.mk A f #unify (Canonical.carrier A_canonical), A attribute [unify] -definition Canonical_hint (C : Canonical) : unification_hint := +noncomputable definition Canonical_hint (C : Canonical) : unification_hint := unification_hint.mk (unification_constraint.mk (Canonical.carrier C) A) [unification_constraint.mk C A_canonical] -- TODO(dhs): we mark carrier as irreducible and prove A_canonical explicitly to work around the fact that diff --git a/tests/lean/unification_hints1.lean.expected.out b/tests/lean/unification_hints1.lean.expected.out index 07baddba10..66ed5ea9ef 100644 --- a/tests/lean/unification_hints1.lean.expected.out +++ b/tests/lean/unification_hints1.lean.expected.out @@ -1,9 +1,5 @@ -unification_hints1.lean:10:11:failed to generate bytecode for 'toy.g' -code generation failed, VM does not have code for 'toy.f' g x y =?= f z fail -unification_hints1.lean:15:11:failed to generate bytecode for 'toy.toy_hint' -code generation failed, VM does not have code for 'toy.f' g x y =?= f z g x y =?= f z success @@ -17,12 +13,8 @@ success unification hints: (add, nat.succ) #4 + 1 =?= succ #3 {#4 =?= #3} (toy.g, toy.f) toy.g #1 #0 =?= toy.f toy.z {} -unification_hints1.lean:47:11:failed to generate bytecode for 'canonical.A_canonical' -code generation failed, VM does not have code for 'canonical.f' Canonical.carrier A_canonical =?= A fail -unification_hints1.lean:52:11:failed to generate bytecode for 'canonical.Canonical_hint' -code generation failed, VM does not have code for 'canonical.f' Canonical.carrier A_canonical =?= A Canonical.carrier A_canonical =?= A success