4 | import Core.Normalise
9 | import Libraries.Data.WithDefault
14 | Reify BindMode where
15 | reify defs val@(NDCon _ n _ _ args)
16 | = case (dropAllNS !(full (gamma defs) n), args) of
17 | (UN (Basic "PI"), [(_, c)])
18 | => do c' <- reify defs !(evalClosure defs c)
20 | (UN (Basic "PATTERN"), _) => pure PATTERN
21 | (UN (Basic "COVERAGE"), _) => pure COVERAGE
22 | (UN (Basic "NONE"), _) => pure NONE
23 | _ => cantReify val "BindMode"
24 | reify deva val = cantReify val "BindMode"
27 | Reflect BindMode where
28 | reflect fc defs lhs env (PI c)
29 | = do c' <- reflect fc defs lhs env c
30 | appCon fc defs (reflectionttimp "PI") [c']
31 | reflect fc defs lhs env PATTERN
32 | = getCon fc defs (reflectionttimp "PATTERN")
33 | reflect fc defs lhs env COVERAGE
34 | = getCon fc defs (reflectionttimp "COVERAGE")
35 | reflect fc defs lhs env NONE
36 | = getCon fc defs (reflectionttimp "NONE")
40 | reify defs val@(NDCon _ n _ _ args)
41 | = case (dropAllNS !(full (gamma defs) n), args) of
42 | (UN (Basic "UseLeft"), _) => pure UseLeft
43 | (UN (Basic "UseRight"), _) => pure UseRight
44 | _ => cantReify val "UseSide"
45 | reify defs val = cantReify val "UseSide"
48 | Reflect UseSide where
49 | reflect fc defs lhs env UseLeft
50 | = getCon fc defs (reflectionttimp "UseLeft")
51 | reflect fc defs lhs env UseRight
52 | = getCon fc defs (reflectionttimp "UseRight")
55 | Reify DotReason where
56 | reify defs val@(NDCon _ n _ _ args)
57 | = case (dropAllNS !(full (gamma defs) n), args) of
58 | (UN (Basic "NonLinearVar"), _) => pure NonLinearVar
59 | (UN (Basic "VarApplied"), _) => pure VarApplied
60 | (UN (Basic "NotConstructor"), _) => pure NotConstructor
61 | (UN (Basic "ErasedArg"), _) => pure ErasedArg
62 | (UN (Basic "UserDotted"), _) => pure UserDotted
63 | (UN (Basic "UnknownDot"), _) => pure UnknownDot
64 | (UN (Basic "UnderAppliedCon"), _) => pure UnderAppliedCon
65 | _ => cantReify val "DotReason"
66 | reify defs val = cantReify val "DotReason"
69 | Reflect DotReason where
70 | reflect fc defs lhs env NonLinearVar
71 | = getCon fc defs (reflectionttimp "NonLinearVar")
72 | reflect fc defs lhs env VarApplied
73 | = getCon fc defs (reflectionttimp "VarApplied")
74 | reflect fc defs lhs env NotConstructor
75 | = getCon fc defs (reflectionttimp "NotConstructor")
76 | reflect fc defs lhs env ErasedArg
77 | = getCon fc defs (reflectionttimp "ErasedArg")
78 | reflect fc defs lhs env UserDotted
79 | = getCon fc defs (reflectionttimp "UserDotted")
80 | reflect fc defs lhs env UnknownDot
81 | = getCon fc defs (reflectionttimp "UnknownDot")
82 | reflect fc defs lhs env UnderAppliedCon
83 | = getCon fc defs (reflectionttimp "UnderAppliedCon")
89 | reify defs val@(NDCon _ n _ _ args)
90 | = case (dropAllNS !(full (gamma defs) n), map snd args) of
91 | (UN (Basic "IVar"), [fc, n])
92 | => do fc' <- reify defs !(evalClosure defs fc)
93 | n' <- reify defs !(evalClosure defs n)
95 | (UN (Basic "IPi"), [fc, c, p, mn, aty, rty])
96 | => do fc' <- reify defs !(evalClosure defs fc)
97 | c' <- reify defs !(evalClosure defs c)
98 | p' <- reify defs !(evalClosure defs p)
99 | mn' <- reify defs !(evalClosure defs mn)
100 | aty' <- reify defs !(evalClosure defs aty)
101 | rty' <- reify defs !(evalClosure defs rty)
102 | pure (IPi fc' c' p' mn' aty' rty')
103 | (UN (Basic "ILam"), [fc, c, p, mn, aty, lty])
104 | => do fc' <- reify defs !(evalClosure defs fc)
105 | c' <- reify defs !(evalClosure defs c)
106 | p' <- reify defs !(evalClosure defs p)
107 | mn' <- reify defs !(evalClosure defs mn)
108 | aty' <- reify defs !(evalClosure defs aty)
109 | lty' <- reify defs !(evalClosure defs lty)
110 | pure (ILam fc' c' p' mn' aty' lty')
111 | (UN (Basic "ILet"), [fc, lhsFC, c, n, ty, val, sc])
112 | => do fc' <- reify defs !(evalClosure defs fc)
113 | lhsFC' <- reify defs !(evalClosure defs lhsFC)
114 | c' <- reify defs !(evalClosure defs c)
115 | n' <- reify defs !(evalClosure defs n)
116 | ty' <- reify defs !(evalClosure defs ty)
117 | val' <- reify defs !(evalClosure defs val)
118 | sc' <- reify defs !(evalClosure defs sc)
119 | pure (ILet fc' lhsFC' c' n' ty' val' sc')
120 | (UN (Basic "ICase"), [fc, opts, sc, ty, cs])
121 | => do fc' <- reify defs !(evalClosure defs fc)
122 | opts' <- reify defs !(evalClosure defs opts)
123 | sc' <- reify defs !(evalClosure defs sc)
124 | ty' <- reify defs !(evalClosure defs ty)
125 | cs' <- reify defs !(evalClosure defs cs)
126 | pure (ICase fc' opts' sc' ty' cs')
127 | (UN (Basic "ILocal"), [fc, ds, sc])
128 | => do fc' <- reify defs !(evalClosure defs fc)
129 | ds' <- reify defs !(evalClosure defs ds)
130 | sc' <- reify defs !(evalClosure defs sc)
131 | pure (ILocal fc' ds' sc')
132 | (UN (Basic "IUpdate"), [fc, ds, sc])
133 | => do fc' <- reify defs !(evalClosure defs fc)
134 | ds' <- reify defs !(evalClosure defs ds)
135 | sc' <- reify defs !(evalClosure defs sc)
136 | pure (IUpdate fc' ds' sc')
137 | (UN (Basic "IApp"), [fc, f, a])
138 | => do fc' <- reify defs !(evalClosure defs fc)
139 | f' <- reify defs !(evalClosure defs f)
140 | a' <- reify defs !(evalClosure defs a)
141 | pure (IApp fc' f' a')
142 | (UN (Basic "INamedApp"), [fc, f, m, a])
143 | => do fc' <- reify defs !(evalClosure defs fc)
144 | f' <- reify defs !(evalClosure defs f)
145 | m' <- reify defs !(evalClosure defs m)
146 | a' <- reify defs !(evalClosure defs a)
147 | pure (INamedApp fc' f' m' a')
148 | (UN (Basic "IAutoApp"), [fc, f, a])
149 | => do fc' <- reify defs !(evalClosure defs fc)
150 | f' <- reify defs !(evalClosure defs f)
151 | a' <- reify defs !(evalClosure defs a)
152 | pure (IAutoApp fc' f' a')
153 | (UN (Basic "IWithApp"), [fc, f, a])
154 | => do fc' <- reify defs !(evalClosure defs fc)
155 | f' <- reify defs !(evalClosure defs f)
156 | a' <- reify defs !(evalClosure defs a)
157 | pure (IWithApp fc' f' a')
158 | (UN (Basic "ISearch"), [fc, d])
159 | => do fc' <- reify defs !(evalClosure defs fc)
160 | d' <- reify defs !(evalClosure defs d)
161 | pure (ISearch fc' d')
162 | (UN (Basic "IAlternative"), [fc, t, as])
163 | => do fc' <- reify defs !(evalClosure defs fc)
164 | t' <- reify defs !(evalClosure defs t)
165 | as' <- reify defs !(evalClosure defs as)
166 | pure (IAlternative fc' t' as')
167 | (UN (Basic "IRewrite"), [fc, t, sc])
168 | => do fc' <- reify defs !(evalClosure defs fc)
169 | t' <- reify defs !(evalClosure defs t)
170 | sc' <- reify defs !(evalClosure defs sc)
171 | pure (IRewrite fc' t' sc')
172 | (UN (Basic "IBindHere"), [fc, t, sc])
173 | => do fc' <- reify defs !(evalClosure defs fc)
174 | t' <- reify defs !(evalClosure defs t)
175 | sc' <- reify defs !(evalClosure defs sc)
176 | pure (IBindHere fc' t' sc')
177 | (UN (Basic "IBindVar"), [fc, n])
178 | => do fc' <- reify defs !(evalClosure defs fc)
179 | n' <- reify defs !(evalClosure defs n)
180 | pure (IBindVar fc' n')
181 | (UN (Basic "IAs"), [fc, nameFC, s, n, t])
182 | => do fc' <- reify defs !(evalClosure defs fc)
183 | nameFC' <- reify defs !(evalClosure defs nameFC)
184 | s' <- reify defs !(evalClosure defs s)
185 | n' <- reify defs !(evalClosure defs n)
186 | t' <- reify defs !(evalClosure defs t)
187 | pure (IAs fc' nameFC' s' n' t')
188 | (UN (Basic "IMustUnify"), [fc, r, t])
189 | => do fc' <- reify defs !(evalClosure defs fc)
190 | r' <- reify defs !(evalClosure defs r)
191 | t' <- reify defs !(evalClosure defs t)
192 | pure (IMustUnify fc' r' t')
193 | (UN (Basic "IDelayed"), [fc, r, t])
194 | => do fc' <- reify defs !(evalClosure defs fc)
195 | r' <- reify defs !(evalClosure defs r)
196 | t' <- reify defs !(evalClosure defs t)
197 | pure (IDelayed fc' r' t')
198 | (UN (Basic "IDelay"), [fc, t])
199 | => do fc' <- reify defs !(evalClosure defs fc)
200 | t' <- reify defs !(evalClosure defs t)
201 | pure (IDelay fc' t')
202 | (UN (Basic "IForce"), [fc, t])
203 | => do fc' <- reify defs !(evalClosure defs fc)
204 | t' <- reify defs !(evalClosure defs t)
205 | pure (IForce fc' t')
206 | (UN (Basic "IQuote"), [fc, t])
207 | => do fc' <- reify defs !(evalClosure defs fc)
208 | t' <- reify defs !(evalClosure defs t)
209 | pure (IQuote fc' t')
210 | (UN (Basic "IQuoteName"), [fc, t])
211 | => do fc' <- reify defs !(evalClosure defs fc)
212 | t' <- reify defs !(evalClosure defs t)
213 | pure (IQuoteName fc' t')
214 | (UN (Basic "IQuoteDecl"), [fc, t])
215 | => do fc' <- reify defs !(evalClosure defs fc)
216 | t' <- reify defs !(evalClosure defs t)
217 | pure (IQuoteDecl fc' t')
218 | (UN (Basic "IUnquote"), [fc, t])
219 | => do fc' <- reify defs !(evalClosure defs fc)
220 | t' <- reify defs !(evalClosure defs t)
221 | pure (IUnquote fc' t')
222 | (UN (Basic "IPrimVal"), [fc, t])
223 | => do fc' <- reify defs !(evalClosure defs fc)
224 | t' <- reify defs !(evalClosure defs t)
225 | pure (IPrimVal fc' t')
226 | (UN (Basic "IType"), [fc])
227 | => do fc' <- reify defs !(evalClosure defs fc)
229 | (UN (Basic "IHole"), [fc, n])
230 | => do fc' <- reify defs !(evalClosure defs fc)
231 | n' <- reify defs !(evalClosure defs n)
232 | pure (IHole fc' n')
233 | (UN (Basic "Implicit"), [fc, n])
234 | => do fc' <- reify defs !(evalClosure defs fc)
235 | n' <- reify defs !(evalClosure defs n)
236 | pure (Implicit fc' n')
237 | (UN (Basic "IWithUnambigNames"), [fc, ns, t])
238 | => do fc' <- reify defs !(evalClosure defs fc)
239 | ns' <- reify defs !(evalClosure defs ns)
240 | t' <- reify defs !(evalClosure defs t)
241 | pure (IWithUnambigNames fc' ns' t')
242 | _ => cantReify val "TTImp"
243 | reify defs val = cantReify val "TTImp"
246 | Reify IFieldUpdate where
247 | reify defs val@(NDCon _ n _ _ args)
248 | = case (dropAllNS !(full (gamma defs) n), args) of
249 | (UN (Basic "ISetField"), [(_, x), (_, y)])
250 | => do x' <- reify defs !(evalClosure defs x)
251 | y' <- reify defs !(evalClosure defs y)
252 | pure (ISetField x' y')
253 | (UN (Basic "ISetFieldApp"), [(_, x), (_, y)])
254 | => do x' <- reify defs !(evalClosure defs x)
255 | y' <- reify defs !(evalClosure defs y)
256 | pure (ISetFieldApp x' y')
257 | _ => cantReify val "IFieldUpdate"
258 | reify defs val = cantReify val "IFieldUpdate"
261 | Reify AltType where
262 | reify defs val@(NDCon _ n _ _ args)
263 | = case (dropAllNS !(full (gamma defs) n), args) of
264 | (UN (Basic "FirstSuccess"), _)
265 | => pure FirstSuccess
266 | (UN (Basic "Unique"), _)
268 | (UN (Basic "UniqueDefault"), [(_, x)])
269 | => do x' <- reify defs !(evalClosure defs x)
270 | pure (UniqueDefault x')
271 | _ => cantReify val "AltType"
272 | reify defs val = cantReify val "AltType"
276 | reify defs val@(NDCon _ n _ _ args)
277 | = case (dropAllNS !(full (gamma defs) n), args) of
278 | (UN (Basic "Inline"), _) => pure Inline
279 | (UN (Basic "Unsafe"), _) => pure Unsafe
280 | (UN (Basic "NoInline"), _) => pure NoInline
281 | (UN (Basic "Deprecate"), _) => pure Deprecate
282 | (UN (Basic "TCInline"), _) => pure TCInline
283 | (UN (Basic "Hint"), [(_, x)])
284 | => do x' <- reify defs !(evalClosure defs x)
286 | (UN (Basic "GlobalHint"), [(_, x)])
287 | => do x' <- reify defs !(evalClosure defs x)
288 | pure (GlobalHint x')
289 | (UN (Basic "ExternFn"), _) => pure ExternFn
290 | (UN (Basic "ForeignFn"), [(_, x)])
291 | => do x' <- reify defs !(evalClosure defs x)
292 | pure (ForeignFn x')
293 | (UN (Basic "ForeignExport"), [(_, x)])
294 | => do x' <- reify defs !(evalClosure defs x)
295 | pure (ForeignExport x')
296 | (UN (Basic "Invertible"), _) => pure Invertible
297 | (UN (Basic "Totality"), [(_, x)])
298 | => do x' <- reify defs !(evalClosure defs x)
300 | (UN (Basic "Macro"), _) => pure Macro
301 | (UN (Basic "SpecArgs"), [(_, x)])
302 | => do x' <- reify defs !(evalClosure defs x)
304 | _ => cantReify val "FnOpt"
305 | reify defs val = cantReify val "FnOpt"
309 | reify defs val@(NDCon _ n _ _ args)
310 | = case (dropAllNS !(full (gamma defs) n), map snd args) of
311 | (UN (Basic "MkTy"), [w, y, z])
312 | => do fc' <- reify defs !(evalClosure defs w)
313 | name' <- the (Core (WithFC Name)) (reify defs !(evalClosure defs y))
314 | term' <- reify defs !(evalClosure defs z)
315 | pure (Mk [fc', name'] term')
316 | _ => cantReify val "ITy"
317 | reify defs val = cantReify val "ITy"
320 | Reify DataOpt where
321 | reify defs val@(NDCon _ n _ _ args)
322 | = case (dropAllNS !(full (gamma defs) n), args) of
323 | (UN (Basic "SearchBy"), [(_, x)])
324 | => do x' <- reify defs !(evalClosure defs x)
326 | (UN (Basic "NoHints"), _) => pure NoHints
327 | (UN (Basic "UniqueSearch"), _) => pure UniqueSearch
328 | (UN (Basic "External"), _) => pure External
329 | (UN (Basic "NoNewtype"), _) => pure NoNewtype
330 | _ => cantReify val "DataOpt"
331 | reify defs val = cantReify val "DataOpt"
334 | Reify ImpData where
335 | reify defs val@(NDCon _ n _ _ args)
336 | = case (dropAllNS !(full (gamma defs) n), map snd args) of
337 | (UN (Basic "MkData"), [v,w,x,y,z])
338 | => do v' <- reify defs !(evalClosure defs v)
339 | w' <- reify defs !(evalClosure defs w)
340 | x' <- reify defs !(evalClosure defs x)
341 | y' <- reify defs !(evalClosure defs y)
342 | z' <- reify defs !(evalClosure defs z)
343 | pure (MkImpData v' w' x' y' z')
344 | (UN (Basic "MkLater"), [x,y,z])
345 | => do x' <- reify defs !(evalClosure defs x)
346 | y' <- reify defs !(evalClosure defs y)
347 | z' <- reify defs !(evalClosure defs z)
348 | pure (MkImpLater x' y' z')
349 | _ => cantReify val "Data"
350 | reify defs val = cantReify val "Data"
354 | reify defs val@(NDCon _ n _ _ args)
355 | = case (dropAllNS !(full (gamma defs) n), map snd args) of
356 | (UN (Basic "MkIField"), [v,w,x,y,z])
357 | => do fc <- reify defs !(evalClosure defs v)
358 | rig <- reify defs !(evalClosure defs w)
359 | info <- reify defs !(evalClosure defs x)
360 | name <- reify defs !(evalClosure defs y)
361 | type <- reify defs !(evalClosure defs z)
362 | pure (Mk [fc, rig, NoFC name] (MkPiBindData info type))
363 | _ => cantReify val "IField"
364 | reify defs val = cantReify val "IField"
367 | Reify ImpRecord where
368 | reify defs val@(NDCon _ n _ _ args)
369 | = case (dropAllNS !(full (gamma defs) n), map snd args) of
370 | (UN (Basic "MkRecord"), [v,w,x,y,z,a])
371 | => do fc <- reify defs !(evalClosure defs v)
372 | tyName <- reify defs !(evalClosure defs w)
373 | params <- reify defs !(evalClosure defs x)
374 | opts <- reify defs !(evalClosure defs y)
375 | conName <- reify defs !(evalClosure defs z)
376 | fields <- reify defs !(evalClosure defs a)
377 | pure (Mk [fc] $
MkImpRecord (Mk [NoFC tyName] (map fromOldParams params))
378 | (Mk [NoFC conName, opts] fields))
379 | _ => cantReify val "Record"
380 | reify defs val = cantReify val "Record"
383 | Reify WithFlag where
384 | reify defs val@(NDCon _ n _ _ args)
385 | = case (dropAllNS !(full (gamma defs) n), map snd args) of
386 | (UN (Basic "Syntactic"), [])
388 | _ => cantReify val "WithFlag"
389 | reify defs val = cantReify val "WithFlag"
392 | Reify ImpClause where
393 | reify defs val@(NDCon _ n _ _ args)
394 | = case (dropAllNS !(full (gamma defs) n), map snd args) of
395 | (UN (Basic "PatClause"), [x,y,z])
396 | => do x' <- reify defs !(evalClosure defs x)
397 | y' <- reify defs !(evalClosure defs y)
398 | z' <- reify defs !(evalClosure defs z)
399 | pure (PatClause x' y' z')
400 | (UN (Basic "WithClause"), [u,v,w,x,y,z,a])
401 | => do u' <- reify defs !(evalClosure defs u)
402 | v' <- reify defs !(evalClosure defs v)
403 | w' <- reify defs !(evalClosure defs w)
404 | x' <- reify defs !(evalClosure defs x)
405 | y' <- reify defs !(evalClosure defs y)
406 | z' <- reify defs !(evalClosure defs z)
407 | a' <- reify defs !(evalClosure defs a)
408 | pure (WithClause u' v' w' x' y' z' a')
409 | (UN (Basic "ImpossibleClause"), [x,y])
410 | => do x' <- reify defs !(evalClosure defs x)
411 | y' <- reify defs !(evalClosure defs y)
412 | pure (ImpossibleClause x' y')
413 | _ => cantReify val "Clause"
414 | reify defs val = cantReify val "Clause"
417 | Reify (IClaimData Name) where
418 | reify defs val@(NDCon _ n _ _ args)
419 | = case (dropAllNS !(full (gamma defs) n), map snd args) of
420 | (UN (Basic "MkIClaimData"), [w, x, y, z])
421 | => do w' <- reify defs !(evalClosure defs w)
422 | x' <- reify defs !(evalClosure defs x)
423 | y' <- reify defs !(evalClosure defs y)
424 | z' <- reify defs !(evalClosure defs z)
425 | pure (MkIClaimData w' x' y' z')
426 | _ => cantReify val "IClaimData"
427 | reify defs val = cantReify val "IClaimData"
430 | Reify ImpDecl where
431 | reify defs val@(NDCon _ n _ _ args)
432 | = case (dropAllNS !(full (gamma defs) n), map snd args) of
433 | (UN (Basic "IClaim"), [v])
434 | => do v' <- reify defs !(evalClosure defs v)
436 | (UN (Basic "IData"), [x,y,z,w])
437 | => do x' <- reify defs !(evalClosure defs x)
438 | y' <- reify defs !(evalClosure defs y)
439 | z' <- reify defs !(evalClosure defs z)
440 | w' <- reify defs !(evalClosure defs w)
441 | pure (IData x' y' z' w')
442 | (UN (Basic "IDef"), [x,y,z])
443 | => do x' <- reify defs !(evalClosure defs x)
444 | y' <- reify defs !(evalClosure defs y)
445 | z' <- reify defs !(evalClosure defs z)
446 | pure (IDef x' y' z')
447 | (UN (Basic "IParameters"), [x,y,z])
448 | => do x' <- reify defs !(evalClosure defs x)
449 | y' <- reify defs !(evalClosure defs y)
450 | z' <- reify defs !(evalClosure defs z)
451 | pure (IParameters x' (map fromOldParams y') z')
452 | (UN (Basic "IRecord"), [w,x,y,z,u])
453 | => do w' <- reify defs !(evalClosure defs w)
454 | x' <- reify defs !(evalClosure defs x)
455 | y' <- reify defs !(evalClosure defs y)
456 | z' <- reify defs !(evalClosure defs z)
457 | u' <- reify defs !(evalClosure defs u)
458 | pure (IRecord w' x' y' z' u')
459 | (UN (Basic "IFail"), [w,x,y])
460 | => do w' <- reify defs !(evalClosure defs w)
461 | x' <- reify defs !(evalClosure defs x)
462 | y' <- reify defs !(evalClosure defs y)
463 | pure (IFail w' x' y')
464 | (UN (Basic "INamespace"), [w,x,y])
465 | => do w' <- reify defs !(evalClosure defs w)
466 | x' <- reify defs !(evalClosure defs x)
467 | y' <- reify defs !(evalClosure defs y)
468 | pure (INamespace w' x' y')
469 | (UN (Basic "ITransform"), [w,x,y,z])
470 | => do w' <- reify defs !(evalClosure defs w)
471 | x' <- reify defs !(evalClosure defs x)
472 | y' <- reify defs !(evalClosure defs y)
473 | z' <- reify defs !(evalClosure defs z)
474 | pure (ITransform w' x' y' z')
475 | (UN (Basic "ILog"), [x])
476 | => do x' <- reify defs !(evalClosure defs x)
478 | _ => cantReify val "Decl"
479 | reify defs val = cantReify val "Decl"
483 | Reflect RawImp where
484 | reflect fc defs lhs env (IVar tfc n)
485 | = do fc' <- reflect fc defs lhs env tfc
486 | n' <- reflect fc defs lhs env n
487 | appCon fc defs (reflectionttimp "IVar") [fc', n']
488 | reflect fc defs lhs env (IPi tfc c p mn aty rty)
489 | = do fc' <- reflect fc defs lhs env tfc
490 | c' <- reflect fc defs lhs env c
491 | p' <- reflect fc defs lhs env p
492 | mn' <- reflect fc defs lhs env mn
493 | aty' <- reflect fc defs lhs env aty
494 | rty' <- reflect fc defs lhs env rty
495 | appCon fc defs (reflectionttimp "IPi") [fc', c', p', mn', aty', rty']
496 | reflect fc defs lhs env (ILam tfc c p mn aty rty)
497 | = do fc' <- reflect fc defs lhs env tfc
498 | c' <- reflect fc defs lhs env c
499 | p' <- reflect fc defs lhs env p
500 | mn' <- reflect fc defs lhs env mn
501 | aty' <- reflect fc defs lhs env aty
502 | rty' <- reflect fc defs lhs env rty
503 | appCon fc defs (reflectionttimp "ILam") [fc', c', p', mn', aty', rty']
504 | reflect fc defs lhs env (ILet tfc lhsFC c n aty aval sc)
505 | = do fc' <- reflect fc defs lhs env tfc
506 | lhsFC' <- reflect fc defs lhs env lhsFC
507 | c' <- reflect fc defs lhs env c
508 | n' <- reflect fc defs lhs env n
509 | aty' <- reflect fc defs lhs env aty
510 | aval' <- reflect fc defs lhs env aval
511 | sc' <- reflect fc defs lhs env sc
512 | appCon fc defs (reflectionttimp "ILet") [fc', lhsFC', c', n', aty', aval', sc']
513 | reflect fc defs lhs env (ICase tfc opts sc ty cs)
514 | = do fc' <- reflect fc defs lhs env tfc
515 | opts' <- reflect fc defs lhs env opts
516 | sc' <- reflect fc defs lhs env sc
517 | ty' <- reflect fc defs lhs env ty
518 | cs' <- reflect fc defs lhs env cs
519 | appCon fc defs (reflectionttimp "ICase") [fc', opts', sc', ty', cs']
520 | reflect fc defs lhs env (ILocal tfc ds sc)
521 | = do fc' <- reflect fc defs lhs env tfc
522 | ds' <- reflect fc defs lhs env ds
523 | sc' <- reflect fc defs lhs env sc
524 | appCon fc defs (reflectionttimp "ILocal") [fc', ds', sc']
525 | reflect fc defs lhs env (ICaseLocal tfc u i args t)
526 | = reflect fc defs lhs env t
527 | reflect fc defs lhs env (IUpdate tfc ds sc)
528 | = do fc' <- reflect fc defs lhs env tfc
529 | ds' <- reflect fc defs lhs env ds
530 | sc' <- reflect fc defs lhs env sc
531 | appCon fc defs (reflectionttimp "IUpdate") [fc', ds', sc']
532 | reflect fc defs lhs env (IApp tfc f a)
533 | = do fc' <- reflect fc defs lhs env tfc
534 | f' <- reflect fc defs lhs env f
535 | a' <- reflect fc defs lhs env a
536 | appCon fc defs (reflectionttimp "IApp") [fc', f', a']
537 | reflect fc defs lhs env (IAutoApp tfc f a)
538 | = do fc' <- reflect fc defs lhs env tfc
539 | f' <- reflect fc defs lhs env f
540 | a' <- reflect fc defs lhs env a
541 | appCon fc defs (reflectionttimp "IAutoApp") [fc', f', a']
542 | reflect fc defs lhs env (INamedApp tfc f m a)
543 | = do fc' <- reflect fc defs lhs env tfc
544 | f' <- reflect fc defs lhs env f
545 | m' <- reflect fc defs lhs env m
546 | a' <- reflect fc defs lhs env a
547 | appCon fc defs (reflectionttimp "INamedApp") [fc', f', m', a']
548 | reflect fc defs lhs env (IWithApp tfc f a)
549 | = do fc' <- reflect fc defs lhs env tfc
550 | f' <- reflect fc defs lhs env f
551 | a' <- reflect fc defs lhs env a
552 | appCon fc defs (reflectionttimp "IWithApp") [fc', f', a']
553 | reflect fc defs lhs env (ISearch tfc d)
554 | = do fc' <- reflect fc defs lhs env tfc
555 | d' <- reflect fc defs lhs env d
556 | appCon fc defs (reflectionttimp "ISearch") [fc', d']
557 | reflect fc defs lhs env (IAlternative tfc t as)
558 | = do fc' <- reflect fc defs lhs env tfc
559 | t' <- reflect fc defs lhs env t
560 | as' <- reflect fc defs lhs env as
561 | appCon fc defs (reflectionttimp "IAlternative") [fc', t', as']
562 | reflect fc defs lhs env (IRewrite tfc t sc)
563 | = do fc' <- reflect fc defs lhs env tfc
564 | t' <- reflect fc defs lhs env t
565 | sc' <- reflect fc defs lhs env sc
566 | appCon fc defs (reflectionttimp "IRewrite") [fc', t', sc']
567 | reflect fc defs lhs env (ICoerced tfc d) = reflect fc defs lhs env d
568 | reflect fc defs lhs env (IBindHere tfc n sc)
569 | = do fc' <- reflect fc defs lhs env tfc
570 | n' <- reflect fc defs lhs env n
571 | sc' <- reflect fc defs lhs env sc
572 | appCon fc defs (reflectionttimp "IBindHere") [fc', n', sc']
573 | reflect fc defs lhs env (IBindVar tfc n)
574 | = do fc' <- reflect fc defs lhs env tfc
575 | n' <- reflect fc defs lhs env n
576 | appCon fc defs (reflectionttimp "IBindVar") [fc', n']
577 | reflect fc defs lhs env (IAs tfc nameFC s n t)
578 | = do fc' <- reflect fc defs lhs env tfc
579 | nameFC' <- reflect fc defs lhs env nameFC
580 | s' <- reflect fc defs lhs env s
581 | n' <- reflect fc defs lhs env n
582 | t' <- reflect fc defs lhs env t
583 | appCon fc defs (reflectionttimp "IAs") [fc', nameFC', s', n', t']
584 | reflect fc defs lhs env (IMustUnify tfc r t)
585 | = do fc' <- reflect fc defs lhs env tfc
586 | r' <- reflect fc defs lhs env r
587 | t' <- reflect fc defs lhs env t
588 | appCon fc defs (reflectionttimp "IMustUnify") [fc', r', t']
589 | reflect fc defs lhs env (IDelayed tfc r t)
590 | = do fc' <- reflect fc defs lhs env tfc
591 | r' <- reflect fc defs lhs env r
592 | t' <- reflect fc defs lhs env t
593 | appCon fc defs (reflectionttimp "IDelayed") [fc', r', t']
594 | reflect fc defs lhs env (IDelay tfc t)
595 | = do fc' <- reflect fc defs lhs env tfc
596 | t' <- reflect fc defs lhs env t
597 | appCon fc defs (reflectionttimp "IDelay") [fc', t']
598 | reflect fc defs lhs env (IForce tfc t)
599 | = do fc' <- reflect fc defs lhs env tfc
600 | t' <- reflect fc defs lhs env t
601 | appCon fc defs (reflectionttimp "IForce") [fc', t']
602 | reflect fc defs lhs env (IQuote tfc t)
603 | = do fc' <- reflect fc defs lhs env tfc
604 | t' <- reflect fc defs lhs env t
605 | appCon fc defs (reflectionttimp "IQuote") [fc', t']
606 | reflect fc defs lhs env (IQuoteName tfc t)
607 | = do fc' <- reflect fc defs lhs env tfc
608 | t' <- reflect fc defs lhs env t
609 | appCon fc defs (reflectionttimp "IQuoteName") [fc', t']
610 | reflect fc defs lhs env (IQuoteDecl tfc t)
611 | = do fc' <- reflect fc defs lhs env tfc
612 | t' <- reflect fc defs lhs env t
613 | appCon fc defs (reflectionttimp "IQuoteDecl") [fc', t']
614 | reflect fc defs lhs env (IUnquote tfc (IVar _ t))
615 | = pure (Ref tfc Bound t)
616 | reflect fc defs lhs env (IUnquote tfc t)
617 | = throw (InternalError "Can't reflect an unquote: escapes should be lifted out")
618 | reflect fc defs lhs env (IRunElab tfc _ t)
619 | = throw (InternalError "Can't reflect a %runElab")
620 | reflect fc defs lhs env (IPrimVal tfc t)
621 | = do fc' <- reflect fc defs lhs env tfc
622 | t' <- reflect fc defs lhs env t
623 | appCon fc defs (reflectionttimp "IPrimVal") [fc', t']
624 | reflect fc defs lhs env (IType tfc)
625 | = do fc' <- reflect fc defs lhs env tfc
626 | appCon fc defs (reflectionttimp "IType") [fc']
627 | reflect fc defs lhs env (IHole tfc t)
628 | = do fc' <- reflect fc defs lhs env tfc
629 | t' <- reflect fc defs lhs env t
630 | appCon fc defs (reflectionttimp "IHole") [fc', t']
631 | reflect fc defs lhs env (IUnifyLog tfc _ t)
632 | = reflect fc defs lhs env t
633 | reflect fc defs True env (Implicit tfc t)
634 | = pure (Erased fc Placeholder)
635 | reflect fc defs lhs env (Implicit tfc t)
636 | = do fc' <- reflect fc defs lhs env tfc
637 | t' <- reflect fc defs lhs env t
638 | appCon fc defs (reflectionttimp "Implicit") [fc', t']
639 | reflect fc defs lhs env (IWithUnambigNames tfc ns t)
640 | = do fc' <- reflect fc defs lhs env tfc
641 | ns' <- reflect fc defs lhs env ns
642 | t' <- reflect fc defs lhs env t
643 | appCon fc defs (reflectionttimp "IWithUnambigNames") [fc', ns', t']
646 | Reflect IFieldUpdate where
647 | reflect fc defs lhs env (ISetField p t)
648 | = do p' <- reflect fc defs lhs env p
649 | t' <- reflect fc defs lhs env t
650 | appCon fc defs (reflectionttimp "ISetField") [p', t']
651 | reflect fc defs lhs env (ISetFieldApp p t)
652 | = do p' <- reflect fc defs lhs env p
653 | t' <- reflect fc defs lhs env t
654 | appCon fc defs (reflectionttimp "ISetFieldApp") [p', t']
657 | Reflect AltType where
658 | reflect fc defs lhs env FirstSuccess = getCon fc defs (reflectionttimp "FirstSuccess")
659 | reflect fc defs lhs env Unique = getCon fc defs (reflectionttimp "Unique")
660 | reflect fc defs lhs env (UniqueDefault x)
661 | = do x' <- reflect fc defs lhs env x
662 | appCon fc defs (reflectionttimp "UniqueDefault") [x']
665 | Reflect FnOpt where
666 | reflect fc defs lhs env Unsafe = getCon fc defs (reflectionttimp "Unsafe")
667 | reflect fc defs lhs env Inline = getCon fc defs (reflectionttimp "Inline")
668 | reflect fc defs lhs env NoInline = getCon fc defs (reflectionttimp "NoInline")
669 | reflect fc defs lhs env Deprecate = getCon fc defs (reflectionttimp "Deprecate")
670 | reflect fc defs lhs env TCInline = getCon fc defs (reflectionttimp "TCInline")
671 | reflect fc defs lhs env (Hint x)
672 | = do x' <- reflect fc defs lhs env x
673 | appCon fc defs (reflectionttimp "Hint") [x']
674 | reflect fc defs lhs env (GlobalHint x)
675 | = do x' <- reflect fc defs lhs env x
676 | appCon fc defs (reflectionttimp "GlobalHint") [x']
677 | reflect fc defs lhs env ExternFn = getCon fc defs (reflectionttimp "ExternFn")
678 | reflect fc defs lhs env (ForeignFn x)
679 | = do x' <- reflect fc defs lhs env x
680 | appCon fc defs (reflectionttimp "ForeignFn") [x']
681 | reflect fc defs lhs env (ForeignExport x)
682 | = do x' <- reflect fc defs lhs env x
683 | appCon fc defs (reflectionttimp "ForeignExport") [x']
684 | reflect fc defs lhs env Invertible = getCon fc defs (reflectionttimp "Invertible")
685 | reflect fc defs lhs env (Totality r)
686 | = do r' <- reflect fc defs lhs env r
687 | appCon fc defs (reflectionttimp "Totality") [r']
688 | reflect fc defs lhs env Macro = getCon fc defs (reflectionttimp "Macro")
689 | reflect fc defs lhs env (SpecArgs r)
690 | = do r' <- reflect fc defs lhs env r
691 | appCon fc defs (reflectionttimp "SpecArgs") [r']
694 | Reflect ImpTy where
695 | reflect fc defs lhs env ty
696 | = do w' <- reflect fc defs lhs env ty.fc
697 | x' <- reflect fc defs lhs env ty.tyName
698 | z' <- reflect fc defs lhs env ty.val
699 | appCon fc defs (reflectionttimp "MkTy") [w', x', z']
702 | Reflect DataOpt where
703 | reflect fc defs lhs env (SearchBy x)
704 | = do x' <- reflect fc defs lhs env x
705 | appCon fc defs (reflectionttimp "SearchBy") [x']
706 | reflect fc defs lhs env NoHints = getCon fc defs (reflectionttimp "NoHints")
707 | reflect fc defs lhs env UniqueSearch = getCon fc defs (reflectionttimp "UniqueSearch")
708 | reflect fc defs lhs env External = getCon fc defs (reflectionttimp "External")
709 | reflect fc defs lhs env NoNewtype = getCon fc defs (reflectionttimp "NoNewtype")
712 | Reflect ImpData where
713 | reflect fc defs lhs env (MkImpData v w x y z)
714 | = do v' <- reflect fc defs lhs env v
715 | w' <- reflect fc defs lhs env w
716 | x' <- reflect fc defs lhs env x
717 | y' <- reflect fc defs lhs env y
718 | z' <- reflect fc defs lhs env z
719 | appCon fc defs (reflectionttimp "MkData") [v', w', x', y', z']
720 | reflect fc defs lhs env (MkImpLater x y z)
721 | = do x' <- reflect fc defs lhs env x
722 | y' <- reflect fc defs lhs env y
723 | z' <- reflect fc defs lhs env z
724 | appCon fc defs (reflectionttimp "MkLater") [x', y', z']
727 | Reflect IField where
728 | reflect fc defs lhs env field
729 | = do v' <- reflect fc defs lhs env field.fc
730 | w' <- reflect fc defs lhs env field.rig
731 | x' <- reflect fc defs lhs env field.val.info
732 | y' <- reflect fc defs lhs env field.name.val
733 | z' <- reflect fc defs lhs env field.val.boundType
734 | appCon fc defs (reflectionttimp "MkIField") [v', w', x', y', z']
736 | Reflect ImpRecord where
737 | reflect fc defs lhs env r@(MkWithData _ $
MkImpRecord header body)
738 | = do v' <- reflect fc defs lhs env r.fc
739 | w' <- reflect fc defs lhs env header.name.val
740 | x' <- reflect fc defs lhs env (map toOldParams header.val)
741 | y' <- reflect fc defs lhs env body.opts
742 | z' <- reflect fc defs lhs env body.name.val
743 | a' <- reflect fc defs lhs env body.val
744 | appCon fc defs (reflectionttimp "MkRecord") [v', w', x', y', z', a']
747 | Reflect WithFlag where
748 | reflect fc defs lhs env Syntactic
749 | = getCon fc defs (reflectionttimp "Syntactic")
752 | Reflect ImpClause where
753 | reflect fc defs lhs env (PatClause x y z)
754 | = do x' <- reflect fc defs lhs env x
755 | y' <- reflect fc defs lhs env y
756 | z' <- reflect fc defs lhs env z
757 | appCon fc defs (reflectionttimp "PatClause") [x', y', z']
758 | reflect fc defs lhs env (WithClause u v w x y z a)
759 | = do u' <- reflect fc defs lhs env u
760 | v' <- reflect fc defs lhs env v
761 | w' <- reflect fc defs lhs env w
762 | x' <- reflect fc defs lhs env x
763 | y' <- reflect fc defs lhs env y
764 | z' <- reflect fc defs lhs env z
765 | a' <- reflect fc defs lhs env a
766 | appCon fc defs (reflectionttimp "WithClause") [u', v', w', x', y', z', a']
767 | reflect fc defs lhs env (ImpossibleClause x y)
768 | = do x' <- reflect fc defs lhs env x
769 | y' <- reflect fc defs lhs env y
770 | appCon fc defs (reflectionttimp "ImpossibleClause") [x', y']
773 | Reflect (IClaimData Name) where
774 | reflect fc defs lhs env (MkIClaimData w x y z)
775 | = do w' <- reflect fc defs lhs env w
776 | x' <- reflect fc defs lhs env x
777 | y' <- reflect fc defs lhs env y
778 | z' <- reflect fc defs lhs env z
779 | appCon fc defs (reflectionttimp "MkIClaimData") [w', x', y', z']
782 | Reflect ImpDecl where
783 | reflect fc defs lhs env (IClaim v)
784 | = do v' <- reflect fc defs lhs env v
785 | appCon fc defs (reflectionttimp "IClaim") [v']
786 | reflect fc defs lhs env (IData x y z w)
787 | = do x' <- reflect fc defs lhs env x
788 | y' <- reflect fc defs lhs env y
789 | z' <- reflect fc defs lhs env z
790 | w' <- reflect fc defs lhs env w
791 | appCon fc defs (reflectionttimp "IData") [x', y', z', w']
792 | reflect fc defs lhs env (IDef x y z)
793 | = do x' <- reflect fc defs lhs env x
794 | y' <- reflect fc defs lhs env y
795 | z' <- reflect fc defs lhs env z
796 | appCon fc defs (reflectionttimp "IDef") [x', y', z']
797 | reflect fc defs lhs env (IParameters x y z)
798 | = do x' <- reflect fc defs lhs env x
799 | y' <- reflect fc defs lhs env (map toOldParams y)
800 | z' <- reflect fc defs lhs env z
801 | appCon fc defs (reflectionttimp "IParameters") [x', y', z']
802 | reflect fc defs lhs env (IRecord w x y z u)
803 | = do w' <- reflect fc defs lhs env w
804 | x' <- reflect fc defs lhs env x
805 | y' <- reflect fc defs lhs env y
806 | z' <- reflect fc defs lhs env z
807 | u' <- reflect fc defs lhs env u
808 | appCon fc defs (reflectionttimp "IRecord") [w', x', y', z', u']
809 | reflect fc defs lhs env (IFail x y z)
810 | = do x' <- reflect fc defs lhs env x
811 | y' <- reflect fc defs lhs env y
812 | z' <- reflect fc defs lhs env z
813 | appCon fc defs (reflectionttimp "IFail") [x', y', z']
814 | reflect fc defs lhs env (INamespace x y z)
815 | = do x' <- reflect fc defs lhs env x
816 | y' <- reflect fc defs lhs env y
817 | z' <- reflect fc defs lhs env z
818 | appCon fc defs (reflectionttimp "INamespace") [x', y', z']
819 | reflect fc defs lhs env (ITransform w x y z)
820 | = do w' <- reflect fc defs lhs env w
821 | x' <- reflect fc defs lhs env x
822 | y' <- reflect fc defs lhs env y
823 | z' <- reflect fc defs lhs env z
824 | appCon fc defs (reflectionttimp "ITransform") [w', x', y', z']
825 | reflect fc defs lhs env (IRunElabDecl w x)
826 | = throw (GenericMsg fc "Can't reflect a %runElab")
827 | reflect fc defs lhs env (IPragma _ _ x)
828 | = throw (GenericMsg fc "Can't reflect a pragma")
829 | reflect fc defs lhs env (ILog x)
830 | = do x' <- reflect fc defs lhs env x
831 | appCon fc defs (reflectionttimp "ILog") [x']
832 | reflect fc defs lhs env (IBuiltin {})
833 | = throw (GenericMsg fc "Can't reflect a %builtin")