Agda。字符的模式匹配

Question

我曾尝试实现我的"sprintf“函数(它从一个格式化字符串和许多不同类型的参数构造一个字符串)，但是失败了。同样的技术也适用于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

但是我在编译器中得到了这个错误：

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

在Agda中是否可以对“1”、“t”、“O”这样的字符进行模式匹配？

Answer 1

没有名为_::_的List的构造函数。您想使用的是_∷_。将所有出现的::替换为∷可解决此问题：

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