0 | module Core.WithData
  1 |
  2 | import Core.TT
  3 | import public Libraries.Data.WithData
  4 | import Libraries.Text.Bounded
  5 |
  6 | ------------------------------------------------------------------------------------------
  7 | -- Helpers for binding information
  8 | ------------------------------------------------------------------------------------------
  9 |
 10 | ||| The "bind" label containing binding information for metadata records
 11 | public export
 12 | Bind' : KeyVal
 13 | Bind' = "bind" :-: BindingModifier
 14 |
 15 | ||| Obtain binding information from the metadata
 16 | export
 17 | (.bind) :
 18 |     {n : Nat} ->
 19 |     (0 inRange : NameInRange "bind" fields === Just (n, BindingModifier)) =>
 20 |     WithData fields a -> BindingModifier
 21 | (.bind) = WithData.get "bind"
 22 | ------------------------------------------------------------------------------------------
 23 | -- Arity information
 24 | ------------------------------------------------------------------------------------------
 25 | ||| function arity
 26 | public export
 27 | Arity' : KeyVal
 28 | Arity' = "arity" :-: Nat
 29 |
 30 | public export
 31 | WithArity : Type -> Type
 32 | WithArity = AddMetadata Arity'
 33 |
 34 | ||| Obtain arity information from the metadata
 35 | export
 36 | (.arity) :
 37 |     {n : Nat} ->
 38 |     (0 inRange : NameInRange "arity" fields === Just (n, Nat)) =>
 39 |     WithData fields a -> Nat
 40 | (.arity) = WithData.get "arity"
 41 |
 42 | ------------------------------------------------------------------------------------------
 43 | -- Options information
 44 | ------------------------------------------------------------------------------------------
 45 | ||| data constructor options
 46 | public export
 47 | Opts' : KeyVal
 48 | Opts' = "opts" :-: List DataOpt
 49 |
 50 | public export
 51 | WithOpts : Type -> Type
 52 | WithOpts = AddMetadata Opts'
 53 |
 54 | ||| Obtain data options from the metadata
 55 | export
 56 | (.opts) :
 57 |     {n : Nat} ->
 58 |     (0 inRange : NameInRange "opts" fields === Just (n, List DataOpt)) =>
 59 |     WithData fields a -> List DataOpt
 60 | (.opts) = WithData.get "opts"
 61 |
 62 | ------------------------------------------------------------------------------------------
 63 | -- Totality information
 64 | ------------------------------------------------------------------------------------------
 65 |
 66 | ||| The "totalReq" label containing totality information for metadata records
 67 | public export
 68 | Tot' : KeyVal
 69 | Tot' = "totalReq" :-: Maybe TotalReq
 70 |
 71 | ||| Obtain totality information from the metadata
 72 | export
 73 | (.totReq) :
 74 |     {n : Nat} ->
 75 |     (0 inRange : NameInRange "totalReq" fields === Just (n, Maybe TotalReq)) =>
 76 |     WithData fields a -> Maybe TotalReq
 77 | (.totReq) = WithData.get "totalReq"
 78 |
 79 | ------------------------------------------------------------------------------------------
 80 | -- Helpers for FC information
 81 | ------------------------------------------------------------------------------------------
 82 |
 83 | ||| The "fc" label containing file context information for metadata records
 84 | public export
 85 | FC' : KeyVal
 86 | FC' = "fc" :-: FC
 87 |
 88 | ||| Attach FC information to a type
 89 | public export
 90 | WithFC : Type -> Type
 91 | WithFC = WithData [ FC' ]
 92 |
 93 | public export
 94 | AddFC : Type -> Type
 95 | AddFC = AddMetadata FC'
 96 |
 97 | ||| Obtain file context information from the metadata
 98 | export
 99 | (.fc) : {n : Nat} ->
100 |         (inRange : NameInRange "fc" fields === Just (n, FC)) => WithData fields a -> FC
101 | (.fc) = WithData.get "fc"
102 |
103 | export
104 | setFC : {n : Nat} ->
105 |         (inRange : NameInRange "fc" fields === Just (n, FC)) => FC ->
106 |         WithData fields a -> WithData fields a
107 | setFC fc = WithData.set "fc" fc @{inRange}
108 |
109 | ||| A wrapper for a value with a file context.
110 | public export
111 | MkFCVal : FC -> ty -> WithFC ty
112 | MkFCVal fc = Mk [fc]
113 |
114 | ||| Smart constructor for WithFC that uses EmptyFC as location
115 | %inline export
116 | NoFC : a -> WithFC a
117 | NoFC = MkFCVal EmptyFC
118 |
119 | export
120 | (.withFC) : (o : OriginDesc) => WithBounds t -> WithFC t
121 | x.withFC = MkFCVal x.toFC x.val
122 |
123 | export
124 | (.addFC) : (o : OriginDesc) => WithBounds (WithData ls t) -> WithData (FC' :: ls) t
125 | (.addFC) x = x.toFC :+ x.val
126 |
127 | ------------------------------------------------------------------------------------------
128 | -- Helpers for documentation information
129 | ------------------------------------------------------------------------------------------
130 |
131 | ||| The "doc" label containing documentation information for metadata records
132 | public export
133 | Doc' : KeyVal
134 | Doc' = "doc" :-: String
135 |
136 | public export
137 | WithDoc : Type -> Type
138 | WithDoc = AddMetadata Doc'
139 |
140 | ||| Obtain documentation information from the metadata
141 | export
142 | (.doc) : {n : Nat} ->
143 |          (inRange : NameInRange "doc" fields === Just (n, String)) =>
144 |          WithData fields a -> String
145 | (.doc) = WithData.get "doc"
146 |
147 | ------------------------------------------------------------------------------------------
148 | -- Helpers for quantity information
149 | ------------------------------------------------------------------------------------------
150 |
151 | ||| The "rig" label containing quantity information for metadata records
152 | public export
153 | Rig' : KeyVal
154 | Rig' = "rig" :-: RigCount
155 |
156 | public export
157 | WithRig : Type -> Type
158 | WithRig = AddMetadata Rig'
159 |
160 | ||| Obtain quantity information from the metadata
161 | export
162 | (.rig) : {n : Nat} ->
163 |          (inRange : NameInRange "rig" fields === Just (n, RigCount)) =>
164 |          WithData fields a -> RigCount
165 | (.rig) = WithData.get "rig"
166 |
167 | ------------------------------------------------------------------------------------------
168 | -- Helpers for name information
169 | ------------------------------------------------------------------------------------------
170 |
171 | ||| The "name" label containing a `Name` for metadata records
172 | public export
173 | Name' : KeyVal
174 | Name' = "name" :-: WithFC Name
175 |
176 |
177 | ||| Extract the name out of the metadata.
178 | export
179 | (.name) : {n : Nat} ->
180 |           (inRange : NameInRange "name" fields === Just (n, WithFC Name)) =>
181 |           WithData fields a -> WithFC Name
182 | (.name) = WithData.get "name" @{inRange}
183 |
184 | ||| Extract the name out of the metadata.
185 | export
186 | (.nameVal) : {n : Nat} ->
187 |           (inRange : NameInRange "name" fields === Just (n, WithFC Name)) =>
188 |           WithData fields a -> Name
189 | (.nameVal) x = x.name.val
190 |
191 | ||| Attach name and file context information to a type
192 | public export
193 | WithName : Type -> Type
194 | WithName = AddMetadata Name'
195 |
196 | ||| the "tyname" label containing a `WithFC Name` for metadata records. Typically used for type names.
197 | public export
198 | TyName' : KeyVal
199 | TyName' = "tyname" :-: WithFC Name
200 |
201 | ||| Extract the "tyname" value from the metadata record
202 | export
203 | (.tyName) : {n : Nat} ->
204 |             (inRange : NameInRange "tyname" fields === Just (n, WithFC Name)) =>
205 |             WithData fields a -> WithFC Name
206 | (.tyName) = WithData.get "tyname" @{inRange}
207 |
208 |
209 | ||| Attach documentation, binding and location information to a type
210 | public export
211 | DocBindFC : Type -> Type
212 | DocBindFC = WithData [ Doc', Bind', FC' ]
213 |
214 | ||| the "mname" label containing a `Maybe (WithFC Name)` for metadata records
215 | public export
216 | MName' : KeyVal
217 | MName' = "mname" :-: Maybe (WithFC Name)
218 |
219 | public export
220 | WithMName : Type -> Type
221 | WithMName = AddMetadata MName'
222 |
223 | export
224 | (.mName) : {n : Nat} ->
225 |             (inRange : NameInRange "mname" fields === Just (n, Maybe (WithFC Name))) =>
226 |             WithData fields a -> Maybe (WithFC Name)
227 | (.mName) = WithData.get "mname" @{inRange}
228 |
229 | ||| the "names" label containing a `List (WithFC Name)` for metadata records
230 | public export
231 | Names' : KeyVal
232 | Names' = "names" :-: List (WithFC Name)
233 |
234 | public export
235 | WithNames : Type -> Type
236 | WithNames = AddMetadata Names'
237 |
238 | export
239 | (.names) : {n : Nat} ->
240 |             (inRange : NameInRange "names" fields === Just (n, List (WithFC Name))) =>
241 |             WithData fields a -> List (WithFC Name)
242 | (.names) = WithData.get "names" @{inRange}
243 |
244 | ------------------------------------------------------------------------
245 | -- Default instances for metadata
246 | ------------------------------------------------------------------------
247 |
248 | -- When location is unavailable, use `EmptyFC`
249 | export
250 | HasDefault FC where
251 |   defValue = EmptyFC
252 |
253 | -- When binding is not provided, the default is not binding
254 | export
255 | HasDefault BindingModifier where
256 |   defValue = NotBinding
257 |
258 | -- default doc string
259 | export
260 | HasDefault String where
261 |   defValue = ""
262 |
263 | ------------------------------------------------------------------------
264 |
265 |