@@ -382,3 +382,64 @@ mutual
382 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
382 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
385+instance Quotable ErrorReportPart where
386+ quotedTy = `(ErrorReportPart)
387+ quote (TextPart x) = `(TextPart ~(quote x))
388+ quote (NamePart n) = `(NamePart ~(quote n))
389+ quote (TermPart tm) = `(TermPart ~(quote tm))
390+ quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))
393+ quoteRaw : Raw -> TT
394+ quoteRaw (Var n) = `(Var ~(quote n))
395+ quoteRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinder b) ~(quoteRaw tm))
396+ quoteRaw (RApp tm tm') = `(RApp ~(quoteRaw tm) ~(quoteRaw tm'))
397+ quoteRaw RType = `(RType)
398+ quoteRaw (RForce tm) = `(RForce ~(quoteRaw tm))
399+ quoteRaw (RConstant c) = `(RConstant ~(quote c))
401+ quoteRawBinder : Binder Raw -> TT
402+ quoteRawBinder (Lam x) = `(Lam {a=Raw} ~(quoteRaw x))
403+ quoteRawBinder (Pi x) = `(Pi {a=Raw} ~(quoteRaw x))
404+ quoteRawBinder (Let x y) = `(Let {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
405+ quoteRawBinder (NLet x y) = `(NLet {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
406+ quoteRawBinder (Hole x) = `(Hole {a=Raw} ~(quoteRaw x))
407+ quoteRawBinder (GHole x) = `(GHole {a=Raw} ~(quoteRaw x))
408+ quoteRawBinder (Guess x y) = `(Guess {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
409+ quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))
410+ quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))
412+instance Quotable Raw where
416+instance Quotable (Binder Raw) where
417+ quotedTy = `(Binder Raw)
418+ quote = quoteRawBinder
420+instance Quotable Tactic where
421+ quotedTy = `(Tactic)
422+ quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))
423+ quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))
424+ quote (Refine n) = `(Refine ~(quote n))
425+ quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac'))
426+ quote Trivial = `(Trivial)
427+ quote (Search x) = `(Search ~(quote x))
428+ quote Instance = `(Instance)
429+ quote Solve = `(Solve)
430+ quote Intros = `(Intros)
431+ quote (Intro n) = `(Intro ~(quote n))
432+ quote (ApplyTactic tm) = `(ApplyTactic ~(quote tm))
433+ quote (Reflect tm) = `(Reflect ~(quote tm))
434+ quote (ByReflection tm) = `(ByReflection ~(quote tm))
435+ quote (Fill tm) = `(Fill ~(quote tm))
436+ quote (Exact tm) = `(Exact ~(quote tm))
437+ quote (Focus n) = `(Focus ~(quote n))
438+ quote (Rewrite tm) = `(Rewrite ~(quote tm))
439+ quote (Induction tm) = `(Induction ~(quote tm))
440+ quote (Case tm) = `(Case ~(quote tm))
441+ quote (LetTac n tm) = `(LetTac ~(quote n) ~(quote tm))
442+ quote (LetTacTy n tm tm') = `(LetTacTy ~(quote n) ~(quote tm) ~(quote tm'))
443+ quote Compute = `(Compute)
444+ quote Skip = `(Skip)
445+ quote (Fail xs) = `(Fail ~(quote xs))