From 5acedcddbb5d2016ca87ea3ddfc8de16c9e6ee32 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Aug 2013 08:34:50 -0700 Subject: [PATCH] Remove useless is_* functions. We can use equality for that (more readable and similar performance). Signed-off-by: Leonardo de Moura --- src/kernel/arith/arith.h | 9 --------- src/kernel/builtin.h | 28 ---------------------------- src/kernel/type_check.cpp | 2 +- src/tests/kernel/arith.cpp | 6 ------ 4 files changed, 1 insertion(+), 44 deletions(-) diff --git a/src/kernel/arith/arith.h b/src/kernel/arith/arith.h index 1fc3b7c26..a30159c84 100644 --- a/src/kernel/arith/arith.h +++ b/src/kernel/arith/arith.h @@ -13,7 +13,6 @@ Author: Leonardo de Moura namespace lean { expr mk_int_type(); #define Int mk_int_type() -bool is_int_type(expr const & e); expr mk_int_value(mpz const & v); inline expr mk_int_value(int v) { return mk_int_value(mpz(v)); } @@ -22,35 +21,27 @@ bool is_int_value(expr const & e); mpz const & int_value_numeral(expr const & e); expr mk_int_add_fn(); -bool is_int_add_fn(expr const & e); inline expr iAdd(expr const & e1, expr const & e2) { return mk_app(mk_int_add_fn(), e1, e2); } expr mk_int_sub_fn(); -bool is_int_sub_fn(expr const & e); inline expr iSub(expr const & e1, expr const & e2) { return mk_app(mk_int_sub_fn(), e1, e2); } expr mk_int_mul_fn(); -bool is_int_mul_fn(expr const & e); inline expr iMul(expr const & e1, expr const & e2) { return mk_app(mk_int_mul_fn(), e1, e2); } expr mk_int_div_fn(); -bool is_int_div_fn(expr const & e); inline expr iDiv(expr const & e1, expr const & e2) { return mk_app(mk_int_div_fn(), e1, e2); } expr mk_int_le_fn(); -bool is_int_le_fn(expr const & e); inline expr iLe(expr const & e1, expr const & e2) { return mk_app(mk_int_le_fn(), e1, e2); } expr mk_int_ge_fn(); -bool is_int_ge_fn(expr const & e); inline expr iGe(expr const & e1, expr const & e2) { return mk_app(mk_int_ge_fn(), e1, e2); } expr mk_int_lt_fn(); -bool is_int_lt_fn(expr const & e); inline expr iLt(expr const & e1, expr const & e2) { return mk_app(mk_int_lt_fn(), e1, e2); } expr mk_int_gt_fn(); -bool is_int_gt_fn(expr const & e); inline expr iGt(expr const & e1, expr const & e2) { return mk_app(mk_int_gt_fn(), e1, e2); } inline expr iIf(expr const & c, expr const & t, expr const & e) { return mk_if(Int, c, t, e); } diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index 4667e9a8f..82c5fd0c3 100644 --- a/src/kernel/builtin.h +++ b/src/kernel/builtin.h @@ -26,8 +26,6 @@ expr mk_type_u(); /** \brief Return the Lean Boolean type. */ expr mk_bool_type(); #define Bool mk_bool_type() -/** \brief Return true iff \c e is the Lean Boolean type. */ -bool is_bool_type(expr const & e); /** \brief Create a Lean Boolean value (true/false) */ expr mk_bool_value(bool v); @@ -47,9 +45,6 @@ bool is_false(expr const & e); /** \brief Return the Lean If-Then-Else operator. It has type: pi (A : Type), bool -> A -> A -> A */ expr mk_if_fn(); -/** \brief Return true iff \c e is the Lean If-Then-Else operator */ -bool is_if_fn(expr const & e); - /** \brief Return the term (if A c t e) */ inline expr mk_if(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_app(mk_if_fn(), A, c, t, e); } inline expr If(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_if(A, c, t, e); } @@ -59,17 +54,12 @@ inline expr bIf(expr const & c, expr const & t, expr const & e) { return mk_bool /** \brief Return the Lean Implies operator */ expr mk_implies_fn(); -/** \brief Return true iff \c e is the Lean implies operator */ -bool is_implies_fn(expr const & e); /** \brief Return the term (e1 => e2) */ inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app(mk_implies_fn(), e1, e2); } inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); } /** \brief Return the Lean And operator */ expr mk_and_fn(); -/** \brief Return true iff \c e is the Lean and operator. */ -bool is_and_fn(expr const & e); - /** \brief Return (e1 and e2) */ inline expr mk_and(expr const & e1, expr const & e2) { return mk_app(mk_and_fn(), e1, e2); } inline expr mk_and(unsigned num_args, expr const * args) { return mk_bin_op(mk_and_fn(), True, num_args, args); } @@ -78,8 +68,6 @@ inline expr And(std::initializer_list const & l) { return mk_and(l.size(), /** \brief Return the Lean Or operator */ expr mk_or_fn(); -bool is_or_fn(expr const & e); - /** \brief Return (e1 Or e2) */ inline expr mk_or(expr const & e1, expr const & e2) { return mk_app(mk_or_fn(), e1, e2); } inline expr mk_or(unsigned num_args, expr const * args) { return mk_bin_op(mk_or_fn(), False, num_args, args); } @@ -88,68 +76,55 @@ inline expr Or(std::initializer_list const & l) { return mk_or(l.size(), l /** \brief Return the Lean not operator */ expr mk_not_fn(); -bool is_not_fn(expr const & e); - /** \brief Return (Not e) */ inline expr mk_not(expr const & e) { return mk_app(mk_not_fn(), e); } inline expr Not(expr const & e) { return mk_not(e); } /** \brief Return the Lean forall operator. It has type: Pi (A : Type), (A -> bool) -> Bool<\tt> */ expr mk_forall_fn(); -/** \brief Return true iff \c e is the Lean forall operator */ -bool is_forall_fn(expr const & e); /** \brief Return the term (Forall A P), where A is a type and P : A -> bool */ inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); } inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); } /** \brief Return the Lean exists operator. It has type: Pi (A : Type), (A -> Bool) -> Bool<\tt> */ expr mk_exists_fn(); -/** \brief Return true iff \c e is the Lean exists operator */ -bool is_exists_fn(expr const & e); /** \brief Return the term (exists A P), where A is a type and P : A -> bool */ inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); } inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); } /** \brief Modus Ponens axiom */ expr mk_mp_fn(); -bool is_mp_fn(const expr & e); /** \brief (Axiom) a : Bool, b : Bool, H1 : a => b, H2 : a |- MP(a, b, H1, H2) : b */ inline expr MP(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_mp_fn(), a, b, H1, H2); } /** \brief Discharge axiom */ expr mk_discharge_fn(); -bool is_discharge_fn(const expr & e); /** \brief (Axiom) a : Bool, b : Bool, H : a -> b |- Discharge(a, b, H) : a => b */ inline expr Discharge(expr const & a, expr const & b, expr const & H) { return mk_app(mk_discharge_fn(), a, b, H); } /** \brief Reflexivity axiom */ expr mk_refl_fn(); -bool is_refl_fn(expr const & e); /** \brief (Axiom) A : Type u, a : A |- Refl(A, a) : a = a */ inline expr Refl(expr const & A, expr const & a) { return mk_app(mk_refl_fn(), A, a); } #define Trivial Refl(Bool, True) /** \brief Case analysis axiom */ expr mk_case_fn(); -bool is_case_fn(expr const & e); /** \brief (Axiom) P : Bool -> Bool, H1 : P True, H2 : P False, a : Bool |- Case(P, H1, H2, a) : P a */ inline expr Case(expr const & P, expr const & H1, expr const & H2, expr const & a) { return mk_app(mk_case_fn(), P, H1, H2, a); } /** \brief Substitution axiom */ expr mk_subst_fn(); -bool is_subst_fn(expr const & e); /** \brief (Axiom) A : Type u, P : A -> Bool, a b : A, H1 : P a, H2 : a = b |- Subst(A, P, a, b, H1, H2) : P b */ inline expr Subst(expr const & A, expr const & P, expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app({mk_subst_fn(), A, P, a, b, H1, H2}); } /** \brief Eta conversion axiom */ expr mk_eta_fn(); -bool is_eta_fn(expr const & e); /** \brief (Axiom) A : Type u, B : A -> Type u, f : (Pi x : A, B x) |- Eta(A, B, f) : ((Fun x : A => f x) = f) */ inline expr Eta(expr const & A, expr const & B, expr const & f) { return mk_app(mk_eta_fn(), A, B, f); } /** \brief Implies Anti-symmetry */ expr mk_imp_antisym_fn(); -bool is_imp_antisym_fn(expr const & e); /** \brief (Axiom) a : Bool, b : Bool, H1 : a => b, H2 : b => a |- ImpAntisym(a, b, H1, H2) : a = b */ inline expr ImpAntisym(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_imp_antisym_fn(), a, b, H1, H2); } @@ -177,8 +152,5 @@ static name Name ## _name = NameObj; \ expr mk_##Name() { \ static thread_local expr r = mk_constant(Name ## _name); \ return r ; \ -} \ -bool is_##Name(expr const & e) { \ - return is_constant(e) && const_name(e) == Name ## _name; \ } } diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp index f402479a8..97baff3f4 100644 --- a/src/kernel/type_check.cpp +++ b/src/kernel/type_check.cpp @@ -57,7 +57,7 @@ struct infer_type_fn { expr u = normalize(infer_type(t, ctx), m_env, ctx); if (is_type(u)) return ty_level(u); - if (is_bool_type(u)) + if (u == Bool) return level(); std::ostringstream buffer; buffer << "type expected, "; diff --git a/src/tests/kernel/arith.cpp b/src/tests/kernel/arith.cpp index 55db67431..10981b7da 100644 --- a/src/tests/kernel/arith.cpp +++ b/src/tests/kernel/arith.cpp @@ -31,8 +31,6 @@ static void tst2() { std::cout << infer_type(mk_int_add_fn(), env) << "\n"; lean_assert(infer_type(e, env) == Int); lean_assert(infer_type(mk_app(mk_int_add_fn(), iVal(10)), env) == (Int >> Int)); - lean_assert(is_int_add_fn(mk_int_add_fn())); - lean_assert(!is_int_add_fn(mk_int_mul_fn())); lean_assert(is_int_value(normalize(e, env))); expr e2 = Fun("a", Int, iAdd(Const("a"), iAdd(iVal(10), iVal(30)))); std::cout << e2 << " --> " << normalize(e2, env) << "\n"; @@ -49,8 +47,6 @@ static void tst3() { std::cout << infer_type(mk_int_mul_fn(), env) << "\n"; lean_assert(infer_type(e, env) == Int); lean_assert(infer_type(mk_app(mk_int_mul_fn(), iVal(10)), env) == arrow(Int, Int)); - lean_assert(is_int_mul_fn(mk_int_mul_fn())); - lean_assert(!is_int_mul_fn(mk_int_add_fn())); lean_assert(is_int_value(normalize(e, env))); expr e2 = Fun("a", Int, iMul(Const("a"), iMul(iVal(10), iVal(30)))); std::cout << e2 << " --> " << normalize(e2, env) << "\n"; @@ -67,8 +63,6 @@ static void tst4() { std::cout << infer_type(mk_int_sub_fn(), env) << "\n"; lean_assert(infer_type(e, env) == Int); lean_assert(infer_type(mk_app(mk_int_sub_fn(), iVal(10)), env) == arrow(Int, Int)); - lean_assert(is_int_sub_fn(mk_int_sub_fn())); - lean_assert(!is_int_sub_fn(mk_int_add_fn())); lean_assert(is_int_value(normalize(e, env))); expr e2 = Fun("a", Int, iSub(Const("a"), iSub(iVal(10), iVal(30)))); std::cout << e2 << " --> " << normalize(e2, env) << "\n";