From c8236ccd4722e3a7951074de56369bf1f31616ec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 17 Feb 2024 17:16:42 -0800
Subject: [PATCH] chore: basic simprocs for `String`

---
 .../Meta/Tactic/Simp/BuiltinSimprocs.lean     |  1 +
 .../Tactic/Simp/BuiltinSimprocs/String.lean   | 36 +++++++++++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean
index f38bf790b4..cccd0fc86d 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean
@@ -9,3 +9,4 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean
new file mode 100644
index 0000000000..6c94b0b516
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.ToExpr
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
+
+namespace String
+open Lean Meta Simp
+
+def fromExpr? (e : Expr) : SimpM (Option String) := OptionT.run do
+  let .lit (.strVal s) := e | failure
+  return s
+
+builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : String)) := fun e => do
+  unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue
+  let some a ← fromExpr? e.appFn!.appArg! | return .continue
+  let some b ← fromExpr? e.appArg! | return .continue
+  return .done { expr := toExpr (a ++ b) }
+
+private partial def reduceListChar (e : Expr) (s : String) : SimpM Step := do
+  trace[Meta.debug] "reduceListChar {e}, {s}"
+  if e.isAppOfArity ``List.nil 1 then
+    return .done { expr := toExpr s }
+  else if e.isAppOfArity ``List.cons 3 then
+    let some c ← Char.fromExpr? e.appFn!.appArg! | return .continue
+    reduceListChar e.appArg! (s.push c)
+  else
+    return .continue
+
+builtin_simproc [simp, seval] reduceMk (String.mk _) := fun e => do
+  unless e.isAppOfArity ``String.mk 1 do return .continue
+  reduceListChar e.appArg! ""
+
+end String