feat: simprocs for Char

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean

@@ -8,3 +8,4 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 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

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean

@@ -0,0 +1,42 @@
+/-
+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.Nat
+
+namespace Char
+open Lean Meta Simp
+
+def fromExpr? (e : Expr) : SimpM (Option Char) := OptionT.run do
+  guard (e.isAppOfArity ``Char.ofNat 1)
+  let value ← Nat.fromExpr? e.appArg!
+  return Char.ofNat value
+
+@[inline] def reduceUnary [ToExpr α] (declName : Name) (op : Char → α) (arity : Nat := 1) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some c ← fromExpr? e.appArg! | return .continue
+  return .done { expr := toExpr (op c) }
+
+builtin_simproc [simp, seval] reduceToLower (Char.toLower _) := reduceUnary ``Char.toLower Char.toLower
+builtin_simproc [simp, seval] reduceToUpper (Char.toUpper _) := reduceUnary ``Char.toUpper Char.toUpper
+builtin_simproc [simp, seval] reduceToNat (Char.toNat _) := reduceUnary ``Char.toNat Char.toNat
+builtin_simproc [simp, seval] reduceIsWhitespace (Char.isWhitespace _) := reduceUnary ``Char.isWhitespace Char.isWhitespace
+builtin_simproc [simp, seval] reduceIsUpper (Char.isUpper _) := reduceUnary ``Char.isUpper Char.isUpper
+builtin_simproc [simp, seval] reduceIsLower (Char.isLower _) := reduceUnary ``Char.isLower Char.isLower
+builtin_simproc [simp, seval] reduceIsAlpha (Char.isAlpha _) := reduceUnary ``Char.isAlpha Char.isAlpha
+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
+
+/--
+Return `.done` for Char values. We don't want to unfold in the symbolic evaluator.
+In regular `simp`, we want to prevent the nested raw literal from being converted into
+a `OfNat.ofNat` application. TODO: cleanup
+-/
+builtin_simproc ↓ [simp, seval] isValue (Char.ofNat _ ) := fun e => do
+  unless (← fromExpr? e).isSome do return .continue
+  return .done { expr := e }
+
+end Char

tests/lean/simprocChar.lean

@@ -0,0 +1,56 @@
+example (h : x = 'a') : x = 'A'.toLower := by
+  simp
+  trace_state
+  assumption
+
+example (h : x = 'A') : x = 'a'.toUpper := by
+  simp
+  trace_state
+  assumption
+
+def f (c : Char) := c
+
+example (h : x = 'A') : x = f 'a'.toUpper := by
+  simp (config := { ground := true })
+  trace_state
+  assumption
+
+example (h : x = "a") : x = toString 'a' := by
+  simp
+  trace_state
+  assumption
+
+example (h : x = 65) : x = 'A'.toNat := by
+  simp
+  trace_state
+  assumption
+
+example (h : x = true) : x = ' '.isWhitespace := by
+  simp
+  trace_state
+  assumption
+
+example (h : x = true) : x = 'C'.isAlpha := by
+  simp
+  trace_state
+  assumption
+
+example (h : x = true) : x = '7'.isDigit := by
+  simp
+  trace_state
+  assumption
+
+example (h : x = true) : x = '7'.isAlphanum := by
+  simp
+  trace_state
+  assumption
+
+example (h : x = true) : x = 'a'.isLower := by
+  simp
+  trace_state
+  assumption
+
+example (h : x = true) : x = 'A'.isUpper := by
+  simp
+  trace_state
+  assumption

tests/lean/simprocChar.lean.expected.out

@@ -0,0 +1,33 @@
+x : Char
+h : x = 'a'
+⊢ x = 'a'
+x : Char
+h : x = 'A'
+⊢ x = 'A'
+x : Char
+h : x = 'A'
+⊢ x = 'A'
+x : String
+h : x = "a"
+⊢ x = "a"
+x : Nat
+h : x = 65
+⊢ x = 65
+x : Bool
+h : x = true
+⊢ x = true
+x : Bool
+h : x = true
+⊢ x = true
+x : Bool
+h : x = true
+⊢ x = true
+x : Bool
+h : x = true
+⊢ x = true
+x : Bool
+h : x = true
+⊢ x = true
+x : Bool
+h : x = true
+⊢ x = true