OCaml 中有返回特定类型值列表的函数吗？

Question

在 Haskell 中，使用

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

。

Coq 的 OCaml API 提供了

find_notation_printing_rule

，它接受

CNotation

中的值并返回符号的打印规则，但我也不明白返回的规则意味着什么。这促使我编写了一个打印规则转储器；一个程序，它将 Coq 代码作为输入，从代码中提取符号，并使用打印规则和其他有用信息转储符号。对于提取阶段，我需要像

listify

这样的函数来从代码中获取

CNotation

。

Answer 1

据我所知，您在 Haskell 中指向的通用编程工具尚未在 OCaml 中实现。

我从未听说过它们被用于 Coq 的开发。