Grip.Ascii: named ASCII byte predicates, constants, and helpers

Pure byte layer: is-prefixed predicates over UInt8, the common delimiter bytes as named constants, and code : Char → UInt8 for ASCII character literals. No parsers and no grades live here; Grip.Combinators builds parsers on top. Batteries-only.

@[inline]

def Grip.Ascii.isWs (b : UInt8) : Bool

Whitespace: the union of space (0x20), line feed (0x0A), tab (0x09), and carriage return (0x0D). Use the named constants space/lf/tab/cr (below) to match one specific whitespace byte, or isBlank for just space and tab.

Equations

• Grip.Ascii.isWs b = (b == 32 || b == 10 || b == 9 || b == 13)

@[inline]

def Grip.Ascii.isBlank (b : UInt8) : Bool

Blank: space (0x20) or tab (0x09) only, excluding line breaks.

Equations

• Grip.Ascii.isBlank b = (b == 32 || b == 9)

@[inline]

def Grip.Ascii.isDigit (b : UInt8) : Bool

Decimal digit 0-9.

Equations

• Grip.Ascii.isDigit b = (decide (48 ≤ b) && decide (b ≤ 57))

@[inline]

def Grip.Ascii.isDigit19 (b : UInt8) : Bool

Nonzero decimal digit 1-9.

Equations

• Grip.Ascii.isDigit19 b = (decide (49 ≤ b) && decide (b ≤ 57))

@[inline]

def Grip.Ascii.isUpper (b : UInt8) : Bool

Uppercase ASCII letter A-Z.

Equations

• Grip.Ascii.isUpper b = (decide (65 ≤ b) && decide (b ≤ 90))

@[inline]

def Grip.Ascii.isLower (b : UInt8) : Bool

Lowercase ASCII letter a-z.

Equations

• Grip.Ascii.isLower b = (decide (97 ≤ b) && decide (b ≤ 122))

@[inline]

def Grip.Ascii.isAlpha (b : UInt8) : Bool

ASCII letter.

Equations

• Grip.Ascii.isAlpha b = (Grip.Ascii.isUpper b || Grip.Ascii.isLower b)

@[inline]

def Grip.Ascii.isAlphaNum (b : UInt8) : Bool

ASCII letter or decimal digit.

Equations

• Grip.Ascii.isAlphaNum b = (Grip.Ascii.isAlpha b || Grip.Ascii.isDigit b)

@[inline]

def Grip.Ascii.isHexDigit (b : UInt8) : Bool

Hexadecimal digit 0-9, a-f, A-F.

Equations

• Grip.Ascii.isHexDigit b = (Grip.Ascii.isDigit b || decide (97 ≤ b) && decide (b ≤ 102) || decide (65 ≤ b) && decide (b ≤ 70))

@[inline]

def Grip.Ascii.isOctDigit (b : UInt8) : Bool

Octal digit 0-7.

Equations

• Grip.Ascii.isOctDigit b = (decide (48 ≤ b) && decide (b ≤ 55))

@[inline]

def Grip.Ascii.isExp (b : UInt8) : Bool

Exponent marker e or E.

Equations

• Grip.Ascii.isExp b = (b == 101 || b == 69)

@[inline]

def Grip.Ascii.isSign (b : UInt8) : Bool

Sign byte + or -.

Equations

• Grip.Ascii.isSign b = (b == 43 || b == 45)

@[inline]

def Grip.Ascii.isControl (b : UInt8) : Bool

Control byte: 0x00-0x1F or 0x7F (DEL).

Equations

• Grip.Ascii.isControl b = (decide (b ≤ 31) || b == 127)

@[inline]

def Grip.Ascii.isPrint (b : UInt8) : Bool

Printable ASCII: space through ~.

Equations

• Grip.Ascii.isPrint b = (decide (32 ≤ b) && decide (b ≤ 126))

@[inline]

def Grip.Ascii.isPunct (b : UInt8) : Bool

Punctuation: printable, not alphanumeric, not space.

Equations

• Grip.Ascii.isPunct b = (Grip.Ascii.isPrint b && !Grip.Ascii.isAlphaNum b && b != 32)

@[inline]

def Grip.Ascii.digitValue (b : UInt8) : Nat

Numeric value of a decimal digit byte (meaningful only when isDigit).

Equations

• Grip.Ascii.digitValue b = b.toNat - 48

@[inline]

def Grip.Ascii.hexValue (b : UInt8) : Nat

Numeric value of a hex digit byte (0-15); 0 for non-hex bytes.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Grip.Ascii.code (c : Char) : UInt8

The low byte of a Char; ASCII-exact for c.toNat < 128.

Equations

• Grip.Ascii.code c = UInt8.ofNat c.toNat

@[inline]

def Grip.Ascii.space : UInt8

Space.

Equations

• Grip.Ascii.space = 32

@[inline]

def Grip.Ascii.tab : UInt8

Horizontal tab.

Equations

• Grip.Ascii.tab = 9

@[inline]

def Grip.Ascii.lf : UInt8

Line feed.

Equations

• Grip.Ascii.lf = 10

@[inline]

def Grip.Ascii.cr : UInt8

Carriage return.

Equations

• Grip.Ascii.cr = 13

@[inline]

def Grip.Ascii.quote : UInt8

Double quote ".

Equations

• Grip.Ascii.quote = 34

@[inline]

def Grip.Ascii.apostrophe : UInt8

Apostrophe '.

Equations

• Grip.Ascii.apostrophe = 39

@[inline]

def Grip.Ascii.backslash : UInt8

Backslash \.

Equations

• Grip.Ascii.backslash = 92

@[inline]

def Grip.Ascii.slash : UInt8

Forward slash /.

Equations

• Grip.Ascii.slash = 47

@[inline]

def Grip.Ascii.comma : UInt8

Comma ,.

Equations

• Grip.Ascii.comma = 44

@[inline]

def Grip.Ascii.dot : UInt8

Dot ..

Equations

• Grip.Ascii.dot = 46

@[inline]

def Grip.Ascii.colon : UInt8

Colon :.

Equations

• Grip.Ascii.colon = 58

@[inline]

def Grip.Ascii.semicolon : UInt8

Semicolon ;.

Equations

• Grip.Ascii.semicolon = 59

@[inline]

def Grip.Ascii.dash : UInt8

Hyphen-minus -.

Equations

• Grip.Ascii.dash = 45

@[inline]

def Grip.Ascii.plus : UInt8

Plus +.

Equations

• Grip.Ascii.plus = 43

@[inline]

def Grip.Ascii.equals : UInt8

Equals =.

Equations

• Grip.Ascii.equals = 61

@[inline]

def Grip.Ascii.star : UInt8

Asterisk *.

Equations

• Grip.Ascii.star = 42

@[inline]

def Grip.Ascii.hash : UInt8

Hash #.

Equations

• Grip.Ascii.hash = 35

@[inline]

def Grip.Ascii.atSign : UInt8

At sign @.

Equations

• Grip.Ascii.atSign = 64

@[inline]

def Grip.Ascii.lparen : UInt8

Left parenthesis (.

Equations

• Grip.Ascii.lparen = 40

@[inline]

def Grip.Ascii.rparen : UInt8

Right parenthesis ).

Equations

• Grip.Ascii.rparen = 41

@[inline]

def Grip.Ascii.lbracket : UInt8

Left bracket [.

Equations

• Grip.Ascii.lbracket = 91

@[inline]

def Grip.Ascii.rbracket : UInt8

Right bracket ].

Equations

• Grip.Ascii.rbracket = 93

@[inline]

def Grip.Ascii.lbrace : UInt8

Left brace {.

Equations

• Grip.Ascii.lbrace = 123

@[inline]

def Grip.Ascii.rbrace : UInt8

Right brace }.

Equations

• Grip.Ascii.rbrace = 125

Sanity guards.