[Agda] equality on Char

[mechvel at scico.botik.ru]

On 2020-01-24 13:11, James Wood wrote:
> Hi Sergei,
> 
> These are now just safe [0], and can be found in Data.Char and 
> Data.String.
> [..]


I need the following functions for a certain parser to run not too slow:

--------------------------------------------------------------
delimiters :  List Char
delimiters =  ' ' ∷ ',' ∷ ';' ∷ '(' ∷ ')' ∷ '[' ∷ ']' ∷ '{' ∷ '}' ∷
               '<' ∷ '>' ∷ '/' ∷ []

open Membership CharProp.≈-setoid using (_∈_)

delimiter? :  Decidable (_∈ delimiters)
delimiter? c =  any (c ≈?_) delimiters

isRegularChar : Char → Set            -- a decimal digit  or  a latin 
letter  or  a
isRegularChar c =                     -- a punctuation sign
                 33 ≤ n × n ≤ 126  where
                                   n = Char.toℕ c

regularChar? : Decidable isRegularChar
regularChar? c =
                let n = Char.toℕ c
                in
                case ((33 ≤? n) ,′ (n ≤? 126)) of \
                                   { (yes le , yes le') → yes (le , le')
                                   ; (no nle , _      ) → no  (nle ∘ 
proj₁)
                                   ; (_ ,      no nle ) → no  (nle ∘ 
proj₂)
                                   }
--------------------------------------------------------------

Needs this ≈? on Char or ≟ ?
≈-setoid or ≡-setoid ?
Can "n ≤? 126" take about 126 match attempts at run-time?
May be to use ≡ᵇ, <ᵇ instead?

These things are listed in Data.Char.Base in lib-1.2:

open import Agda.Builtin.Char public using ( Char )
   renaming
   -- testing
   ( primIsLower    to isLower
   ; primIsDigit    to isDigit
   ; primIsAlpha    to isAlpha
   ; primIsSpace    to isSpace
   ; primIsAscii    to isAscii
   ; primIsLatin1   to isLatin1
   ; primIsPrint    to isPrint
   ; primIsHexDigit to isHexDigit
   -- transforming
   ; primToUpper to toUpper
   ; primToLower to toLower
   -- converting
   ; primCharToNat to toℕ
   ; primNatToChar to fromℕ
   )

May be to use some of them to avoid performance problems (if there are 
any) in the
above delimiter? and regularChar?
?

Thanks,

------
Sergei