Agda. Pattern matching on characters

Question

I've tried to implement my version of "sprintf" function (which constructs a string from a format string a number of arguments of different types), but failed. Same technique worked in Idris.

module Printf where
open import Agda.Builtin.List
open import Agda.Builtin.Char
open import Agda.Builtin.String
open import Agda.Builtin.Float
open import Agda.Builtin.Int

data Format : Set where
   TChar : Char → Format → Format
   TString : Format → Format
   TFloat : Format → Format
   TInt : Format → Format
   TEnd : Format

parseFormat : List Char → Format
parseFormat ('%' :: 's' :: rest) = TString (parseFormat rest)
parseFormat ('%' :: 'f' :: rest) = TFloat (parseFormat rest)
parseFormat ('%' :: 'd' :: rest) = TInt    (parseFormat rest)
parseFormat ('%' :: '%' :: rest) = TChar '%' (parseFormat rest)
parseFormat (x :: rest)          = TChar x (parseFormat rest)
parseFormat []                   = TEnd

But I get this error by the compiler:

Could not parse the left-hand side parseFormat ('%' :: 's' :: rest)
Operators used in the grammar:
  None
when scope checking the left-hand side
parseFormat ('%' :: 's' :: rest) in the definition of parseFormat

Is it possible to pattern-match on characters like '1', 't', 'O' in Agda?

Cactus Cactus · Accepted Answer · 2021-01-02T12:36:56

There is no constructor of List named _::_. What you meant to use is _∷_. Replacing all occurrences of :: with ∷ fixes the problem:

parseFormat : List Char → Format
parseFormat ('%' ∷ 's' ∷ rest) = TString (parseFormat rest)
parseFormat ('%' ∷ 'f' ∷ rest) = TFloat (parseFormat rest)
parseFormat ('%' ∷ 'd' ∷ rest) = TInt    (parseFormat rest)
parseFormat ('%' ∷ '%' ∷ rest) = TChar '%' (parseFormat rest)
parseFormat (x ∷ rest)         = TChar x (parseFormat rest)
parseFormat []                 = TEnd

Agda. Pattern matching on characters

1 Answers