From 9ddac04b40a278dcec409ae379ffdc3e165c505d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Aug 2020 10:17:51 -0700 Subject: [PATCH] fix: support for literals when compiling `noConfusion` --- src/library/compiler/lcnf.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index 4dc09c1885..9bd76f890c 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include "kernel/type_checker.h" #include "kernel/instantiate.h" +#include "kernel/inductive.h" #include "kernel/replace_fn.h" #include "library/expr_lt.h" #include "library/util.h" @@ -238,6 +239,15 @@ public: } } + expr lit_to_constructor(expr const & e) { + if (is_nat_lit(e)) + return nat_lit_to_constructor(e); + else if (is_string_lit(e)) + return string_lit_to_constructor(e); + else + return e; + } + expr visit_no_confusion(expr const & fn, buffer & args, bool root) { name const & no_confusion_name = const_name(fn); name const & I_name = no_confusion_name.get_prefix(); @@ -253,6 +263,8 @@ public: type_checker tc(m_st, m_lctx); expr lhs = tc.whnf(args[nparams + nindices + 1]); expr rhs = tc.whnf(args[nparams + nindices + 2]); + lhs = lit_to_constructor(lhs); + rhs = lit_to_constructor(rhs); optional lhs_constructor = is_constructor_app(env(), lhs); optional rhs_constructor = is_constructor_app(env(), rhs); if (!lhs_constructor || !rhs_constructor)