From edd5e970459acdcfed73cd264ffb4a754c9f664d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Feb 2017 18:41:32 -0800 Subject: [PATCH] feat(frontends/lean/elaborator): coercion from (decidable) Prop to bool This is a hard coded extra case. It is not an instance of has_coe. Even if we change has_coe to accomodate this case, it will not be a satisfactory solution because this coercion depends on the element and not the type, and the element usually contains metavariables. We should eventually write a tactic for synthesizing coercions. --- library/init/meta/expr.lean | 4 ++-- library/init/meta/fun_info.lean | 2 +- library/init/meta/level.lean | 2 +- library/init/meta/occurrences.lean | 4 ++-- library/init/meta/simp_tactic.lean | 2 +- library/init/meta/smt/congruence_closure.lean | 2 +- library/init/meta/tactic.lean | 2 +- library/init/native/default.lean | 2 +- library/init/native/util.lean | 2 +- library/tools/debugger/cli.lean | 2 +- library/tools/super/lpo.lean | 4 ++-- library/tools/super/prover_state.lean | 2 +- src/frontends/lean/elaborator.cpp | 11 ++++++++++- src/frontends/lean/elaborator.h | 1 + src/library/constants.cpp | 4 ++++ src/library/constants.h | 1 + src/library/constants.txt | 1 + 17 files changed, 32 insertions(+), 16 deletions(-) diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index dfbaf77139..aa5bd181f6 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -183,14 +183,14 @@ meta def local_type : expr → expr | e := e meta def is_constant_of : expr → name → bool -| (const n₁ ls) n₂ := to_bool (n₁ = n₂) +| (const n₁ ls) n₂ := n₁ = n₂ | e n := ff meta def is_app_of (e : expr) (n : name) : bool := is_constant_of (get_app_fn e) n meta def is_napp_of (e : expr) (c : name) (n : nat) : bool := -to_bool (is_app_of e c ∧ get_app_num_args e = n) +is_app_of e c ∧ get_app_num_args e = n meta def is_false (e : expr) : bool := is_constant_of e `false diff --git a/library/init/meta/fun_info.lean b/library/init/meta/fun_info.lean index e92dfdb028..6626295b6d 100644 --- a/library/init/meta/fun_info.lean +++ b/library/init/meta/fun_info.lean @@ -32,7 +32,7 @@ group ∘ cbrace $ when ii "inst_implicit" +++ when p "prop" +++ when d "has_fwd_deps" +++ - when (to_bool (length ds > 0)) (to_fmt "back_deps := " ++ to_fmt ds) + when (length ds > 0) (to_fmt "back_deps := " ++ to_fmt ds) meta instance : has_to_format param_info := has_to_format.mk param_info.to_format diff --git a/library/init/meta/level.lean b/library/init/meta/level.lean index a64ea9b11c..8b3a4f0dfc 100644 --- a/library/init/meta/level.lean +++ b/library/init/meta/level.lean @@ -58,5 +58,5 @@ meta def level.has_param : level → name → bool | (level.succ l) n := level.has_param l n | (level.max l₁ l₂) n := level.has_param l₁ n || level.has_param l₂ n | (level.imax l₁ l₂) n := level.has_param l₁ n || level.has_param l₂ n -| (level.param n₁) n := to_bool (n₁ = n) +| (level.param n₁) n := n₁ = n | l n := ff diff --git a/library/init/meta/occurrences.lean b/library/init/meta/occurrences.lean index 675045f345..2a8da23514 100644 --- a/library/init/meta/occurrences.lean +++ b/library/init/meta/occurrences.lean @@ -27,8 +27,8 @@ open occurrences def occurrences.contains : occurrences → nat → bool | all p := tt -| (occurrences.pos ps) p := to_bool (p ∈ ps) -| (occurrences.neg ps) p := to_bool (p ∉ ps) +| (occurrences.pos ps) p := p ∈ ps +| (occurrences.neg ps) p := p ∉ ps instance : inhabited occurrences := ⟨all⟩ diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index fc8e8ed67a..f805a3c7ed 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -160,7 +160,7 @@ cs^.any (λ c, if e^.is_app_of c then tt /- Exact match -/ else let f := e^.get_app_fn in /- f is an auxiliary constant generated when compiling c -/ - f^.is_constant && f^.const_name^.is_internal && to_bool (f^.const_name^.get_prefix = c)) + f^.is_constant && f^.const_name^.is_internal && (f^.const_name^.get_prefix = c)) /- Delta reduce the given constant names -/ meta def delta_core (cfg : delta_config) (cs : list name) (e : expr) : tactic expr := diff --git a/library/init/meta/smt/congruence_closure.lean b/library/init/meta/smt/congruence_closure.lean index 1572d18c13..5a5a63f6e5 100644 --- a/library/init/meta/smt/congruence_closure.lean +++ b/library/init/meta/smt/congruence_closure.lean @@ -68,7 +68,7 @@ meta def eqc_of (s : cc_state) (e : expr) : list expr := s^.eqc_of_core e e [] meta def in_singlenton_eqc (s : cc_state) (e : expr) : bool := -to_bool (s^.next e = e) +s^.next e = e meta def eqc_size (s : cc_state) (e : expr) : nat := (s^.eqc_of e)^.length diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 88b42b1482..096f820939 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -532,7 +532,7 @@ meta def rstep {α : Type u} (line : nat) (col : nat) (t : tactic α) : tactic u meta def is_prop (e : expr) : tactic bool := do t ← infer_type e, - return (to_bool (t = expr.prop)) + return (t = expr.prop) /-- Return true iff n is the name of declaration that is a proposition. -/ meta def is_prop_decl (n : name) : tactic bool := diff --git a/library/init/native/default.lean b/library/init/native/default.lean index f72b79b426..0a5e8fe4c4 100644 --- a/library/init/native/default.lean +++ b/library/init/native/default.lean @@ -208,7 +208,7 @@ let fst' := list.map assert_name fst, ]) meta def is_return (n : name) : bool := -decidable.to_bool $ `native_compiler.return = n +`native_compiler.return = n meta def compile_call (head : name) (arity : nat) (args : list ir.expr) : ir_compiler ir.expr := do trace_ir $ "compile_call: " ++ (to_string head), diff --git a/library/init/native/util.lean b/library/init/native/util.lean index 3a539cbba6..38c47434b7 100644 --- a/library/init/native/util.lean +++ b/library/init/native/util.lean @@ -14,7 +14,7 @@ import init.native.internal import init.native.builtin meta def is_nat_cases_on (n : name) : bool := - decidable.to_bool $ `nat.cases_on = n +`nat.cases_on = n meta def is_cases_on (head : expr) : bool := if is_nat_cases_on (expr.const_name head) diff --git a/library/tools/debugger/cli.lean b/library/tools/debugger/cli.lean index fa4831f771..743729b360 100644 --- a/library/tools/debugger/cli.lean +++ b/library/tools/debugger/cli.lean @@ -206,7 +206,7 @@ meta def in_active_bps (s : state) : vm bool := do sz ← vm.call_stack_size, match s^.active_bps with | [] := return ff - | (csz, _)::_ := return $ to_bool (sz = csz) + | (csz, _)::_ := return (sz = csz) end meta def run_transition (s : state) : vm state := diff --git a/library/tools/super/lpo.lean b/library/tools/super/lpo.lean index 46584aa483..544d591369 100644 --- a/library/tools/super/lpo.lean +++ b/library/tools/super/lpo.lean @@ -19,7 +19,7 @@ def majo {T} (gt : T → T → bool) (s : T) : list T → bool meta def alpha (lpo : expr → expr → bool) : list expr → expr → bool | [] _ := ff -| (s::ss) t := to_bool (s = t) || lpo s t || alpha ss t +| (s::ss) t := (s = t) || lpo s t || alpha ss t meta def lex_ma (lpo : expr → expr → bool) (s t : expr) : list expr → list expr → bool | (si::ss) (ti::ts) := @@ -36,7 +36,7 @@ else alpha lpo (get_app_args s) t meta def prec_gt_of_name_list (ns : list name) : expr → expr → bool := let nis := rb_map.of_list ns^.zip_with_index in λs t, match (nis^.find (name_of_funsym s), nis^.find (name_of_funsym t)) with -| (some si, some ti) := to_bool (si > ti) +| (some si, some ti) := si > ti | _ := ff end diff --git a/library/tools/super/prover_state.lean b/library/tools/super/prover_state.lean index 526e852a21..ba43d34699 100644 --- a/library/tools/super/prover_state.lean +++ b/library/tools/super/prover_state.lean @@ -419,7 +419,7 @@ meta def empty (local_false : expr) : prover_state := meta def initial (local_false : expr) (clauses : list clause) : tactic prover_state := do after_setup ← for' clauses (λc, - let in_sos := decidable.to_bool $ ((contained_lconsts c^.proof)^.erase local_false^.local_uniq_name)^.size = 0 in + let in_sos := ((contained_lconsts c^.proof)^.erase local_false^.local_uniq_name)^.size = 0 in do mk_derived c { priority := score.prio.immediate, in_sos := in_sos, age := 0, cost := 0 } >>= add_inferred ) $ empty local_false, diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 4c9c75b2b7..6e0a67bd7b 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -510,8 +510,17 @@ void elaborator::trace_coercion_failure(expr const & e_type, expr const & type, }); } +optional elaborator::mk_Prop_to_bool_coercion(expr const & e, expr const & ref) { + expr dec = mk_app(mk_constant(get_decidable_name()), e); + expr inst = mk_instance(dec, ref); + expr r = mk_app(mk_constant(get_decidable_to_bool_name()), e, inst); + return some_expr(r); +} + optional elaborator::mk_coercion_core(expr const & e, expr const & e_type, expr const & type, expr const & ref) { - if (!has_expr_metavar(e_type) && !has_expr_metavar(type)) { + if (e_type == mk_Prop() && m_ctx.is_def_eq(type, mk_bool())) { + return mk_Prop_to_bool_coercion(e, ref); + } else if (!has_expr_metavar(e_type) && !has_expr_metavar(type)) { expr has_coe_t; try { has_coe_t = mk_app(m_ctx, get_has_coe_t_name(), e_type, type); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 2e0d820963..701eeb3080 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -133,6 +133,7 @@ private: level replace_univ_placeholder(level const & l); void trace_coercion_failure(expr const & e_type, expr const & type, expr const & ref, char const * error_msg); + optional mk_Prop_to_bool_coercion(expr const & e, expr const & ref); optional mk_coercion_core(expr const & e, expr const & e_type, expr const & type, expr const & ref); bool is_monad(expr const & e); bool is_monad_fail(expr const & e); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 0e2bf2468d..dcfb3dc0f4 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -48,6 +48,7 @@ name const * g_cyclic_numerals = nullptr; name const * g_cyclic_numerals_bound = nullptr; name const * g_decidable = nullptr; name const * g_decidable_by_contradiction = nullptr; +name const * g_decidable_to_bool = nullptr; name const * g_discrete_field = nullptr; name const * g_distinct = nullptr; name const * g_distrib = nullptr; @@ -535,6 +536,7 @@ void initialize_constants() { g_cyclic_numerals_bound = new name{"cyclic_numerals", "bound"}; g_decidable = new name{"decidable"}; g_decidable_by_contradiction = new name{"decidable", "by_contradiction"}; + g_decidable_to_bool = new name{"decidable", "to_bool"}; g_discrete_field = new name{"discrete_field"}; g_distinct = new name{"distinct"}; g_distrib = new name{"distrib"}; @@ -1023,6 +1025,7 @@ void finalize_constants() { delete g_cyclic_numerals_bound; delete g_decidable; delete g_decidable_by_contradiction; + delete g_decidable_to_bool; delete g_discrete_field; delete g_distinct; delete g_distrib; @@ -1510,6 +1513,7 @@ name const & get_cyclic_numerals_name() { return *g_cyclic_numerals; } name const & get_cyclic_numerals_bound_name() { return *g_cyclic_numerals_bound; } name const & get_decidable_name() { return *g_decidable; } name const & get_decidable_by_contradiction_name() { return *g_decidable_by_contradiction; } +name const & get_decidable_to_bool_name() { return *g_decidable_to_bool; } name const & get_discrete_field_name() { return *g_discrete_field; } name const & get_distinct_name() { return *g_distinct; } name const & get_distrib_name() { return *g_distrib; } diff --git a/src/library/constants.h b/src/library/constants.h index e8292445f7..fc56ee53c8 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -50,6 +50,7 @@ name const & get_cyclic_numerals_name(); name const & get_cyclic_numerals_bound_name(); name const & get_decidable_name(); name const & get_decidable_by_contradiction_name(); +name const & get_decidable_to_bool_name(); name const & get_discrete_field_name(); name const & get_distinct_name(); name const & get_distrib_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index eed0f16ed4..9f05741510 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -43,6 +43,7 @@ cyclic_numerals cyclic_numerals.bound decidable decidable.by_contradiction +decidable.to_bool discrete_field distinct distrib