阿格达字符模式匹配

问题描述

我尝试实现我的“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”之类的字符进行模式匹配？

解决方法

没有名为 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

agda pattern-matching