Is there a function that returns a list of values with specific type in OCaml?

Question

In Haskell, using listify with Data can extract values of a specific type from a deeply nested structure without lots of getters. For example, with the following code:

{-# 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 returns a list of Texts in john.

ghci> listStrings john
["John","Smith","1-2-3 Nantoka-kantoka-machi","Nishinomiya","Hyogo","Japan"]

Is there something like this in OCaml?

Context

I'm writing a Coq code formatter, and having difficulty pretty-printing notations (e.g., _ = _.) The node constructor for notations is CNotation in constr_expr_r.

Coq's OCaml API provides find_notation_printing_rule which takes a value in CNotation and returns the printing rule for the notation, but I also don't understand what the returned rule means. This led me to write a printing rule dumper; a program that takes a Coq code as an input, extracts notations from the code, and dumps the notations with printing rules and other useful information. For the extraction phase, I need a function like listify to get CNotations from the code.

Answer 1

After all, I converted an AST into an S-expression using functions in coq-serapi, filtered it, and converted them back to the concrete types

let extract_cnotations (ast : Vernacexpr.vernac_control) :
    Constrexpr.constr_expr_r list =
  let open Sexplib.Sexp in
  (* Traverse the given S-expression and return a list of S-expressions
     satisfying the given condition. *)
  let rec find_sexp_recursively cond = function
    | Atom x -> if cond (Atom x) then [ Atom x ] else []
    | List xs ->
        let tail = List.concat_map (find_sexp_recursively cond) xs in
        if cond (List xs) then List xs :: tail else tail
  in

  let cond = function
    | List
        [
          List [ Atom "v"; List (Atom "CNotation" :: _) ]; List (Atom "loc" :: _);
        ] ->
        true
    | _ -> false
  in

  Serlib.Ser_vernacexpr.sexp_of_vernac_control ast
  |> find_sexp_recursively cond
  |> List.map Serlib.Ser_constrexpr.constr_expr_of_sexp
  |> List.map (fun x -> x.CAst.v)

---

It turned out that sertop could dump printing rules for some notations with the Unparsing query.

$ rlwrap sertop --printer=human

...

(Query () (Unparsing "_ = _"))
(Answer 0 Ack)
(Answer 0
 (ObjList
  ((CoqUnparsing
    ((notation_printing_unparsing
      ((UnpBox (PpHOVB 0)
        ((()
          (UnpMetaVar
           ((notation_subentry InConstrEntry)
            (notation_relative_level (LevelLt 70))
            (notation_position (Left)))))
         (() (UnpTerminal " =")) (() (UnpCut (PpBrk 1 0)))
         (()
          (UnpMetaVar
           ((notation_subentry InConstrEntry)
            (notation_relative_level (LevelLt 70))
            (notation_position (Right)))))))))
     (notation_printing_level 70))
    (((notgram_level
       (((notation_entry InConstrEntry) (notation_level 70))
        ((LevelLt 70) (LevelLt 70))))
      (notgram_assoc ()) (notgram_notation (InConstrEntry "_ = _"))
      (notgram_prods
       (((GramConstrNonTerminal
          (ETProdConstr InConstrEntry
           ((NumLevel 70) (BorderProd Left (NonA))))
          ((Id x)))
         (GramConstrTerminal true =)
         (GramConstrNonTerminal
          (ETProdConstr InConstrEntry
           ((NumLevel 70) (BorderProd Right (NonA))))
          ((Id y))))))
      (notgram_typs
       ((ETConstr InConstrEntry () ((NumLevel 70) (BorderProd Left (NonA))))
        (ETConstr InConstrEntry () ((NumLevel 70) (BorderProd Right (NonA))))))))))))
(Answer 0 Completed)

Answer 2

As far as I can tell, the generic programming facilities that you are pointing to in Haskell have not been implemented in OCaml.

I never heard of them being used in the development of Coq.