From 3dcc8cab3ed8d27d64fb3716a6941c1dbab5fb09 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 17 Feb 2024 16:06:50 -0800
Subject: [PATCH] feat: simprocs for `Char.val`, default char, and
 `Char.ofNatAux`

---
 .../Meta/Tactic/Simp/BuiltinSimprocs/Char.lean    | 15 ++++++++++++++-
 tests/lean/simprocChar.lean                       | 10 ++++++++++
 tests/lean/simprocChar.lean.expected.out          |  6 ++++++
 3 files changed, 30 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean
index 56823d47e8..ee6349bc58 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean
@@ -4,7 +4,7 @@ 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.Nat
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 
 namespace Char
 open Lean Meta Simp
@@ -29,6 +29,10 @@ builtin_simproc [simp, seval] reduceIsAlpha (Char.isAlpha _) := reduceUnary ``Ch
 builtin_simproc [simp, seval] reduceIsDigit (Char.isDigit _) := reduceUnary ``Char.isDigit Char.isDigit
 builtin_simproc [simp, seval] reduceIsAlphaNum (Char.isAlphanum _) := reduceUnary ``Char.isAlphanum Char.isAlphanum
 builtin_simproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnary ``toString toString 3
+builtin_simproc [simp, seval] reduceVal (Char.val _) := fun e => do
+  unless e.isAppOfArity ``Char.val 1 do return .continue
+  let some c ← fromExpr? e.appArg! | return .continue
+  return .done { expr := UInt32.toExprCore c.val }
 
 /--
 Return `.done` for Char values. We don't want to unfold in the symbolic evaluator.
@@ -39,4 +43,13 @@ builtin_simproc ↓ [simp, seval] isValue (Char.ofNat _ ) := fun e => do
   unless (← fromExpr? e).isSome do return .continue
   return .done { expr := e }
 
+builtin_simproc [simp, seval] reduceOfNatAux (Char.ofNatAux _ _) := fun e => do
+  unless e.isAppOfArity ``Char.ofNatAux 2 do return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  return .done { expr := toExpr (Char.ofNat n) }
+
+builtin_simproc [simp, seval] reduceDefault ((default : Char)) := fun e => do
+  unless e.isAppOfArity ``default 2 do return .continue
+  return .done { expr := toExpr (default : Char) }
+
 end Char
diff --git a/tests/lean/simprocChar.lean b/tests/lean/simprocChar.lean
index cd11fb5c54..190fe00fde 100644
--- a/tests/lean/simprocChar.lean
+++ b/tests/lean/simprocChar.lean
@@ -54,3 +54,13 @@ example (h : x = true) : x = 'A'.isUpper := by
   simp
   trace_state
   assumption
+
+example (h : x = 65) : x = 'A'.val := by
+  simp
+  trace_state
+  assumption
+
+example (h : x = 'A') : x = Char.ofNatAux 65 (by decide) := by
+  simp
+  trace_state
+  assumption
diff --git a/tests/lean/simprocChar.lean.expected.out b/tests/lean/simprocChar.lean.expected.out
index 2fc558faa9..c32ab38d4d 100644
--- a/tests/lean/simprocChar.lean.expected.out
+++ b/tests/lean/simprocChar.lean.expected.out
@@ -31,3 +31,9 @@ h : x = true
 x : Bool
 h : x = true
 ⊢ x = true
+x : UInt32
+h : x = 65
+⊢ x = 65
+x : Char
+h : x = 'A'
+⊢ x = 'A'