feat: string literal support on recursors and kernel isDefEq

src/kernel/inductive.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "runtime/sstream.h"
+#include "runtime/utf8.h"
 #include "util/name_generator.h"
 #include "kernel/environment.h"
 #include "kernel/type_checker.h"
@@ -1108,8 +1109,12 @@ environment environment::add_inductive(declaration const & d) const {
     }
 }
 
-static expr * g_nat_zero = nullptr;
-static expr * g_nat_succ = nullptr;
+static expr * g_nat_zero       = nullptr;
+static expr * g_nat_succ       = nullptr;
+static expr * g_string_mk      = nullptr;
+static expr * g_list_cons_char = nullptr;
+static expr * g_list_nil_char  = nullptr;
+static expr * g_char_of_nat    = nullptr;
 
 expr nat_lit_to_constructor(expr const & e) {
     lean_assert(is_nat_lit(e));
@@ -1120,12 +1125,32 @@ expr nat_lit_to_constructor(expr const & e) {
         return mk_app(*g_nat_succ, mk_lit(literal(v - nat(1))));
 }
 
+expr string_lit_to_constructor(expr const & e) {
+    lean_assert(is_str_lit(e));
+    string_ref const & s = lit_value(e).get_string();
+    buffer<unsigned> cs;
+    utf8_decode(s.to_std_string(), cs);
+    expr r = *g_list_nil_char;
+    unsigned i = cs.size();
+    while (i > 0) {
+        i--;
+        r = mk_app(*g_list_cons_char, mk_app(*g_char_of_nat, mk_lit(literal(cs[i]))), r);
+    }
+    return mk_app(*g_string_mk, r);
+}
+
+
 void initialize_inductive() {
-    g_nested        = new name("_nested");
-    g_ind_fresh     = new name("_ind_fresh");
-    g_nested_fresh  = new name("_nested_fresh");
-    g_nat_zero      = new expr(mk_constant(name{"Nat", "zero"}));
-    g_nat_succ      = new expr(mk_constant(name{"Nat", "succ"}));
+    g_nested         = new name("_nested");
+    g_ind_fresh      = new name("_ind_fresh");
+    g_nested_fresh   = new name("_nested_fresh");
+    g_nat_zero       = new expr(mk_constant(name{"Nat", "zero"}));
+    g_nat_succ       = new expr(mk_constant(name{"Nat", "succ"}));
+    g_string_mk      = new expr(mk_constant(name{"String", "mk"}));
+    expr char_type   = mk_constant(name{"Char"});
+    g_list_cons_char = new expr(mk_app(mk_constant(name{"List", "cons"}, {level()}), char_type));
+    g_list_nil_char  = new expr(mk_app(mk_constant(name{"List", "nil"}, {level()}), char_type));
+    g_char_of_nat    = new expr(mk_constant(name{"Char", "ofNat"}));
     register_name_generator_prefix(*g_ind_fresh);
     register_name_generator_prefix(*g_nested_fresh);
 }
@@ -1136,5 +1161,8 @@ void finalize_inductive() {
     delete g_nested_fresh;
     delete g_nat_succ;
     delete g_nat_zero;
+    delete g_string_mk;
+    delete g_list_cons_char;
+    delete g_list_nil_char;
 }
 }

src/kernel/inductive.h

@@ -41,6 +41,7 @@ inline optional<expr> to_cnstr_when_K(environment const & env, recursor_val cons
 optional<recursor_rule> get_rec_rule_for(recursor_val const & rec_val, expr const & major);
 
 expr nat_lit_to_constructor(expr const & e);
+expr string_lit_to_constructor(expr const & e);
 
 template<typename WHNF, typename INFER, typename IS_DEF_EQ>
 inline optional<expr> inductive_reduce_rec(environment const & env, expr const & e,
@@ -63,6 +64,8 @@ inline optional<expr> inductive_reduce_rec(environment const & env, expr const &
     major = whnf(major);
     if (is_nat_lit(major))
         major = nat_lit_to_constructor(major);
+    if (is_string_lit(major))
+        major = string_lit_to_constructor(major);
     optional<recursor_rule> rule = get_rec_rule_for(rec_val, major);
     if (!rule) return none_expr();
     buffer<expr> major_args;

src/kernel/type_checker.cpp

@@ -927,6 +927,21 @@ lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
     }
 }
 
+static expr * g_string_mk = nullptr;
+
+lbool type_checker::try_string_lit_expansion_core(expr const & t, expr const & s) {
+    if (is_string_lit(t) && is_app(s) && app_fn(s) == *g_string_mk) {
+        return to_lbool(is_def_eq_core(string_lit_to_constructor(t), s));
+    }
+    return l_undef;
+}
+
+lbool type_checker::try_string_lit_expansion(expr const & t, expr const & s) {
+    lbool r = try_string_lit_expansion_core(t, s);
+    if (r != l_undef) return r;
+    return try_string_lit_expansion_core(s, t);
+}
+
 bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
     check_system("is_definitionally_equal");
     bool use_hash = true;
@@ -965,6 +980,9 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
     if (try_eta_expansion(t_n, s_n))
         return true;
 
+    r = try_string_lit_expansion(t_n, s_n);
+    if (r != l_undef) return r == l_true;
+
     return false;
 }
 
@@ -1040,6 +1058,7 @@ void initialize_type_checker() {
     g_nat_mod      = new expr(mk_constant(name{"Nat", "mod"}));
     g_nat_beq      = new expr(mk_constant(name{"Nat", "beq"}));
     g_nat_ble      = new expr(mk_constant(name{"Nat", "ble"}));
+    g_string_mk    = new expr(mk_constant(name{"String", "mk"}));
     g_lean_reduce_bool = new expr(mk_constant(name{"Lean", "reduceBool"}));
     g_lean_reduce_nat  = new expr(mk_constant(name{"Lean", "reduceNat"}));
     register_name_generator_prefix(*g_kernel_fresh);
@@ -1058,6 +1077,7 @@ void finalize_type_checker() {
     delete g_nat_mod;
     delete g_nat_beq;
     delete g_nat_ble;
+    delete g_string_mk;
     delete g_lean_reduce_bool;
     delete g_lean_reduce_nat;
 }

src/kernel/type_checker.h

@@ -78,6 +78,8 @@ private:
     bool try_eta_expansion(expr const & t, expr const & s) {
         return try_eta_expansion_core(t, s) || try_eta_expansion_core(s, t);
     }
+    lbool try_string_lit_expansion_core(expr const & t, expr const & s);
+    lbool try_string_lit_expansion(expr const & t, expr const & s);
     bool is_def_eq_app(expr const & t, expr const & s);
     bool is_def_eq_proof_irrel(expr const & t, expr const & s);
     bool failed_before(expr const & t, expr const & s) const;
@@ -91,7 +93,6 @@ private:
     template<typename F> optional<expr> reduce_bin_nat_op(F const & f, expr const & e);
     template<typename F> optional<expr> reduce_bin_nat_pred(F const & f, expr const & e);
     optional<expr> reduce_nat(expr const & e);
-
 public:
     type_checker(state & st, local_ctx const & lctx, bool safe_only = true);
     type_checker(state & st, bool safe_only = true):type_checker(st, local_ctx(), safe_only) {}

tests/lean/run/kernel2.lean

@@ -28,9 +28,26 @@ def v2  := 3628801
 #eval checkDefEq `c3 `v2
 #eval checkDefEq `c1 `c2
 
-set_option pp.all true
-
 def c4 := decide (100000000 < 20000000000)
 
 #eval whnf `c4
 #eval checkDefEq `c4 `Bool.true
+
+def c5 := "h".length
+def c6 := 1
+set_option pp.all true
+
+#eval whnf `c5
+#eval checkDefEq `c5 `c6
+
+def c7 := decide ("hello" = "world")
+#eval whnf `c7
+
+def c8 := "hello".length
+
+#eval whnf `c8
+
+def c9  : String := "hello" ++ "world"
+def c10 : String := "helloworld"
+
+#eval checkDefEq `c9 `c10