listify
和 Data
可以从深度嵌套结构中提取特定类型的值,而无需使用大量 getter。例如,使用以下代码:
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE OverloadedStrings #-}
module Lib
( john
, listStrings
) where
import Data.Data
import Data.Generics.Schemes
import Data.Text
data Person = Person
{ name :: Name
, address :: Address
} deriving (Data, Show)
data Name = Name
{ firstName :: Text
, lastName :: Text
} deriving (Data, Show)
data Address = Address
{ addressLine :: Text
, city :: Text
, province :: Text
, country :: Text
} deriving (Data, Show)
john :: Person
john =
Person
{ name = Name {firstName = "John", lastName = "Smith"}
, address =
Address
{ addressLine = "1-2-3 Nantoka-kantoka-machi"
, city = "Nishinomiya"
, province = "Hyogo"
, country = "Japan"
}
}
listStrings :: Person -> [Text]
listStrings = listify (const True)
listStrings john
返回 Text
中的 john
列表。
ghci> listStrings john
["John","Smith","1-2-3 Nantoka-kantoka-machi","Nishinomiya","Hyogo","Japan"]
OCaml 中有类似的东西吗?
我正在编写一个 Coq 代码格式化程序,并且很难漂亮地打印符号(例如,
_ = _
。)符号的节点构造函数是 CNotation
中的 constr_expr_r
。
find_notation_printing_rule
,它接受 CNotation
中的值并返回符号的打印规则,但我也不明白返回的规则意味着什么。这促使我编写了一个打印规则转储器;一个程序,它将 Coq 代码作为输入,从代码中提取符号,并使用打印规则和其他有用信息转储符号。对于提取阶段,我需要像 listify
这样的函数来从代码中获取 CNotation
。
据我所知,您在 Haskell 中指向的通用编程工具尚未在 OCaml 中实现。
我从未听说过它们被用于 Coq 的开发。