reflection - Get list of data constructors in Idris 2 - Stack Overflow

admin管理员组

文章数量:1122846

I want to get a list of data constructors in Idris 2. How is this done? This seems to work, but is there a better way to do this?

module GetConstructors

import Language.Reflection

%language ElabReflection

data Color = Red | Green | Blue

Show Color where
show Red = "Red"
show Green = "Green"
show Blue = "Blue"

colors : List Color
  colors = %runElab do
  let n = NS (MkNS ["GetConstructors"]) (UN $ Basic "Color")
  conNames <- getCons n
  logMsg "info" 1 $ "Got constructor names: " ++ show conNames
  -- Need to convert the constructor names into actual values
  let constructors = map (\n => IVar EmptyFC n) conNames
  check $ `(the (List Color) ~(foldr (\x, acc => `(~(x) :: ~(acc)))
  `([]) constructors))

main : IO () 
  main = do
  putStrLn "Colors:"
  traverse_ (\c => putStrLn $ "  " ++ show c) colors

本文标签： reflectionGet list of data constructors in Idris 2Stack Overflow