0 | ||| Metadata about a data type's constructor and field names.
  1 | |||
  2 | ||| Since for the time being, record syntax is still under discussion,
  3 | ||| records are not yet treated any differently from other
  4 | ||| product types. This might well change in the future, once
  5 | ||| the issues about record syntax are resolved.
  6 | |||
  7 | ||| Also, it seems not yet to be possible to get access to an
  8 | ||| operator's fixity through elaborator reflection. We try to make
  9 | ||| this information available as soon as possible.
 10 | module Generics.Meta
 11 |
 12 | import Data.List
 13 | import Generics.SOP
 14 |
 15 | %default total
 16 |
 17 | ||| Name and integer index of constructor arguments
 18 | public export
 19 | data ArgName : Type where
 20 |
 21 |   ||| Name and index of a named argument
 22 |   NamedArg   : (index : Nat) -> (name : String) -> ArgName
 23 |
 24 |   ||| Index of an unnamed argument
 25 |   UnnamedArg : (index : Nat) -> ArgName
 26 |
 27 | ||| Tries to extract an argument's name.
 28 | public export
 29 | getName : ArgName -> Maybe String
 30 | getName (NamedArg _ name) = Just name
 31 | getName (UnnamedArg _)    = Nothing
 32 |
 33 | ||| Namespace, name and arguments of a single data constructor
 34 | |||
 35 | ||| The arguments are wrapped in an n-ary product
 36 | ||| parameterized by the constant functor, to make them
 37 | ||| accessible to the SOP combinators.
 38 | public export
 39 | record ConInfo_ (k : Type) (ks : List k) where
 40 |   constructor MkConInfo
 41 |
 42 |   ||| Namespace of the constructor
 43 |   conNS   : List String
 44 |
 45 |   ||| Name of the constructor
 46 |   conName : String
 47 |
 48 |   ||| Constructor arguments
 49 |   args    : NP_ k (K ArgName) ks
 50 |
 51 | ||| Alias for `ConInfo_` with the `k` parameter being implicit.
 52 | public export
 53 | ConInfo : {k : Type} -> (ks : List k) -> Type
 54 | ConInfo = ConInfo_ k
 55 |
 56 | ||| Tries to extract the set of argument names from
 57 | ||| a constructor.
 58 | public export
 59 | argNames : ConInfo ks -> Maybe (NP (K String) ks)
 60 | argNames = htraverse getName . args
 61 |
 62 | ||| Returns `True` if a constructor's `conName` consists
 63 | ||| only of non-alphanumeric characters.
 64 | public export
 65 | isOperator : String -> Bool
 66 | isOperator = all (not . isAlphaNum) . unpack
 67 |
 68 | ||| Wraps a function name in parentheses if it is an operator
 69 | public export
 70 | wrapOperator : String -> String
 71 | wrapOperator n = if isOperator n then "(" ++ n ++ ")" else n
 72 |
 73 | ||| Namespace, name and constructors of a data type.
 74 | |||
 75 | ||| The constructors are wrapped in an n-ary product
 76 | ||| parameterized by `ConInfo`, to make them
 77 | ||| accessible to the SOP combinators.
 78 | public export
 79 | record TypeInfo' (k : Type) (kss : List $ List k) where
 80 |   constructor MkTypeInfo
 81 |
 82 |   ||| Namespace of the data type
 83 |   typeNS       : List String
 84 |
 85 |   ||| Name of the data type
 86 |   typeName     : String
 87 |
 88 |   ||| n-ary product of the data type's constructors
 89 |   constructors : NP_ (List k) (ConInfo_ k) kss
 90 |
 91 | ||| Alias for `TypeInfo'` with the `k` parameter being implicit.
 92 | public export
 93 | TypeInfo : {k : Type} -> (kss : List $ List k) -> Type
 94 | TypeInfo = TypeInfo' k
 95 |
 96 | --------------------------------------------------------------------------------
 97 | --          Meta
 98 | --------------------------------------------------------------------------------
 99 |
100 | ||| Interface to make a data type's metadata available at runtime.
101 | |||
102 | ||| In order to get access to the meta data, it is often more convenient
103 | ||| to use function `metaFor`.
104 | public export
105 | interface Generic t code => Meta t code | t where
106 |   constructor MkMeta
107 |   meta : TypeInfo' Type code
108 |
109 | ||| Return's the `TypeInfo` of a data type. This is
110 | ||| an alias for `meta {t = t}`.
111 | public export
112 | metaFor : (0 t : Type) -> Meta t code => TypeInfo code
113 | metaFor t = meta {t = t}
114 |
115 | --------------------------------------------------------------------------------
116 | --          Show Implementations
117 | --------------------------------------------------------------------------------
118 |
119 | -- Displays a single applied constructor wrapping it in parens if necessary
120 | showC : NP (Show . f) ks => (p : Prec) -> ConInfo ks -> NP f ks -> String
121 |
122 | -- No need to wrap a constant in parens
123 | showC _ info []   = info.conName
124 |
125 | -- This uses `showCon` from the Prelude to wrap an applied
126 | -- constructor in parentheses depending on `p`.
127 | showC p info args =
128 |   let con := wrapOperator info.conName
129 |    in maybe (showOther con) (showRecord con) (argNames info)
130 |
131 |   where
132 |     showNamed : Show a => String -> a -> String
133 |     showNamed name v = name ++ " = " ++ show v
134 |
135 |     showRecord : (con : String) -> NP (K String) ks -> String
136 |     showRecord con names =
137 |       let applied := hcliftA2 (Show . f) showNamed names args
138 |           inner   := intersperse ", " (collapseNP applied)
139 |        in showCon p con (" { " ++ concat inner ++ " }")
140 |
141 |     showOther : (con : String) -> String
142 |     showOther con =
143 |       let argStr := hconcat $ hcmap (Show . f) showArg args
144 |        in showCon p con argStr
145 |
146 | showSOP :
147 |      {auto all : POP (Show . f) kss}
148 |   -> Prec
149 |   -> TypeInfo kss
150 |   -> SOP f kss
151 |   -> String
152 | showSOP {all = MkPOP _} p (MkTypeInfo _ _ cons) =
153 |   hconcat . hcliftA2 (NP $ Show . f) (showC p) cons . unSOP
154 |
155 | ||| Generic show function.
156 | |||
157 | ||| This is still quite basic. It uses prefix notation for operators
158 | ||| and data types with List constructors (`Nil` and `(::)`)
159 | ||| are not yet displayed using list syntax ("[a,b,c]").
160 | |||
161 | ||| However, constructors with only named arguments are displayed
162 | ||| in record syntax style.
163 | public export
164 | genShowPrec : Meta t code => POP Show code => Prec -> t -> String
165 | genShowPrec p = showSOP p (metaFor t) . from
166 |