@@ -223,3 +223,162 @@ data Tactic = Try Tactic Tactic
223223%name Tactic tac, tac'
224224
225225
226+class Quotable a where
227+ quotedTy : TT
228+ quote : a -> TT
229+
230+instance Quotable Nat where
231+ quotedTy = `(Nat)
232+
233+ quote Z = `(Z)
234+ quote (S k) = `(S ~(quote k))
235+
236+instance Quotable Int where
237+ quotedTy = `(Int)
238+ quote x = TConst (I x)
239+
240+instance Quotable Float where
241+ quotedTy = `(Float)
242+ quote x = TConst (Fl x)
243+
244+instance Quotable Char where
245+ quotedTy = `(Char)
246+ quote x = TConst (Ch x)
247+
248+instance Quotable Bits8 where
249+ quotedTy = `(Bits8)
250+ quote x = TConst (B8 x)
251+
252+instance Quotable Bits16 where
253+ quotedTy = `(Bits16)
254+ quote x = TConst (B16 x)
255+
256+instance Quotable Bits32 where
257+ quotedTy = `(Bits32)
258+ quote x = TConst (B32 x)
259+
260+instance Quotable Bits64 where
261+ quotedTy = `(Bits64)
262+ quote x = TConst (B64 x)
263+
264+instance Quotable Integer where
265+ quotedTy = `(Integer)
266+ quote x = TConst (BI x)
267+
268+instance Quotable Bits8x16 where
269+ quotedTy = `(Bits8x16)
270+ quote x = TConst (B8V x)
271+
272+instance Quotable Bits16x8 where
273+ quotedTy = `(Bits16x8)
274+ quote x = TConst (B16V x)
275+
276+instance Quotable Bits32x4 where
277+ quotedTy = `(Bits32x4)
278+ quote x = TConst (B32V x)
279+
280+instance Quotable Bits64x2 where
281+ quotedTy = `(Bits64x2)
282+ quote x = TConst (B64V x)
283+
284+instance Quotable String where
285+ quotedTy = `(String)
286+ quote x = TConst (Str x)
287+
288+instance Quotable NameType where
289+ quotedTy = `(NameType)
290+ quote Bound = `(Bound)
291+ quote Ref = `(Ref)
292+ quote (DCon x y) = `(DCon ~(quote x) ~(quote y))
293+ quote (TCon x y) = `(TCon ~(quote x) ~(quote y))
294+
295+instance Quotable a => Quotable (List a) where
296+ quotedTy = `(List ~(quotedTy {a=a}))
297+ quote [] = `(List.Nil {a=~quotedTy})
298+ quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))
299+
300+instance Quotable TTName where
301+ quotedTy = `(TTName)
302+ quote (UN x) = `(UN ~(quote x))
303+ quote (NS n xs) = `(NS ~(quote n) ~(quote xs))
304+ quote (MN x y) = `(MN ~(quote x) ~(quote y))
305+ quote NErased = `(NErased)
306+
307+instance Quotable NativeTy where
308+ quotedTy = `(NativeTy)
309+ quote IT8 = `(Reflection.IT8)
310+ quote IT16 = `(Reflection.IT16)
311+ quote IT32 = `(Reflection.IT32)
312+ quote IT64 = `(Reflection.IT64)
313+
314+instance Quotable Reflection.IntTy where
315+ quotedTy = `(Reflection.IntTy)
316+ quote (ITFixed x) = `(ITFixed ~(quote x))
317+ quote ITNative = `(Reflection.ITNative)
318+ quote ITBig = `(ITBig)
319+ quote ITChar = `(Reflection.ITChar)
320+ quote (ITVec x y) = `(ITVec ~(quote x) ~(quote y))
321+
322+instance Quotable ArithTy where
323+ quotedTy = `(ArithTy)
324+ quote (ATInt x) = `(ATInt ~(quote x))
325+ quote ATFloat = `(ATFloat)
326+
327+instance Quotable Const where
328+ quotedTy = `(Const)
329+ quote (I x) = `(I ~(quote x))
330+ quote (BI x) = `(BI ~(quote x))
331+ quote (Fl x) = `(Fl ~(quote x))
332+ quote (Ch x) = `(Ch ~(quote x))
333+ quote (Str x) = `(Str ~(quote x))
334+ quote (B8 x) = `(B8 ~(quote x))
335+ quote (B16 x) = `(B16 ~(quote x))
336+ quote (B32 x) = `(B32 ~(quote x))
337+ quote (B64 x) = `(B64 ~(quote x))
338+ quote (B8V xs) = `(B8V ~(quote xs))
339+ quote (B16V xs) = `(B16V ~(quote xs))
340+ quote (B32V xs) = `(B32V ~(quote xs))
341+ quote (B64V xs) = `(B64V ~(quote xs))
342+ quote (AType x) = `(AType ~(quote x))
343+ quote StrType = `(StrType)
344+ quote PtrType = `(PtrType)
345+ quote ManagedPtrType = `(ManagedPtrType)
346+ quote BufferType = `(BufferType)
347+ quote VoidType = `(VoidType)
348+ quote Forgot = `(Forgot)
349+
350+
351+instance Quotable TTUExp where
352+ quotedTy = `(TTUExp)
353+ quote (UVar x) = `(UVar ~(quote x))
354+ quote (UVal x) = `(UVal ~(quote x))
355+
356+mutual
357+ instance Quotable TT where
358+ quotedTy = `(TT)
359+ quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm))
360+ quote (V x) = `(V ~(quote x))
361+ quote (Bind n b tm) = `(Bind ~(quote n) ~(assert_total (quote b)) ~(quote tm))
362+ quote (App f x) = `(App ~(quote f) ~(quote x))
363+ quote (TConst c) = `(TConst ~(quote c))
364+ quote (Proj tm x) = `(Proj ~(quote tm) ~(quote x))
365+ quote Erased = `(Erased)
366+ quote Impossible = `(Impossible)
367+ quote (TType uexp) = `(TType ~(quote uexp))
368+
369+ instance Quotable (Binder TT) where
370+ quotedTy = `(Binder TT)
371+ quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))
372+ quote (Pi x) = `(Pi {a=TT} ~(assert_total (quote x)))
373+ quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))
374+ ~(assert_total (quote y)))
375+ quote (NLet x y) = `(NLet {a=TT} ~(assert_total (quote x))
376+ ~(assert_total (quote y)))
377+ quote (Hole x) = `(Hole {a=TT} ~(assert_total (quote x)))
378+ quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x)))
379+ quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x))
380+ ~(assert_total (quote y)))
381+ quote (PVar x) = `(PVar {a=TT} ~(assert_total (quote x)))
382+ quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
383+
384+