阿格达。字符模式匹配

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

阿格达。字符模式匹配

Agda. Pattern matching on characters

syntax

pattern-matching

agda