feat: simprocs for Char.val, default char, and Char.ofNatAux

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

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

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'