@@ -1,6 +1,7 @@
11module Language.Reflection.Utils
22
33import Language.Reflection
4+import Language.Reflection.Elab
45import Language.Reflection.Errors
56
67--------------------------------------------------------
@@ -50,7 +51,7 @@ mkApp tm [] = tm
5051mkApp tm (a::as) = mkApp (App tm a) as
5152
5253total
53−binderTy : (Eq t) => Binder t -> t
54+binderTy : Binder t -> t
5455binderTy (Lam t) = t
5556binderTy (Pi t _) = t
5657binderTy (Let t1 t2) = t1
@@ -75,7 +76,7 @@ mutual
7576 show (MetaN parent meta) = "(MetaN " ++ show parent ++ " " ++ show meta ++ ")"
7677
7778 instance Show TTName where
78− show (UN str) = "(UN " ++ str ++ ")"
79+ show (UN str) = "(UN " ++ show str ++ ")"
7980 show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
8081 show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"
8182 show (SN sn) = "(SN " ++ assert_total (show sn) ++ ")"
@@ -252,12 +253,12 @@ forget tm = fe [] tm
252253instance Show Raw where
253254 show r = my_show r
254255 where %assert_total my_show : Raw -> String
255− my_show (Var n) = "Var " ++ show n
256− my_show (RBind n b tm) = "RBind " ++ show n ++ " " ++ show b ++ " (" ++ my_show tm ++ ")"
257− my_show (RApp tm tm') = "RApp " ++ my_show tm ++ " " ++ my_show tm'
256+ my_show (Var n) = "(Var " ++ show n ++ ")"
257+ my_show (RBind n b tm) = "(RBind " ++ show n ++ " " ++ show b ++ " " ++ my_show tm ++ ")"
258+ my_show (RApp tm tm') = "(RApp " ++ my_show tm ++ " " ++ my_show tm' ++ ")"
258259 my_show RType = "RType"
259− my_show (RForce tm) = "RForce " ++ my_show tm
260− my_show (RConstant c) = "RConstant " ++ show c
260+ my_show (RForce tm) = "(RForce " ++ my_show tm ++ ")"
261+ my_show (RConstant c) = "(RConstant " ++ show c ++ ")"
261262
262263instance Show SourceLocation where
263264 show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col
@@ -306,3 +307,15 @@ instance Show Err where
306307
307308pure : Raw -> Raw
308309pure = id
310+
311+--------------------------------------
312+-- Instances for definition reflection
313+--------------------------------------
314+instance Show Arg where
315+ show (Explicit n t) = "(Explicit " ++ show n ++ " " ++ show t ++ ")"
316+ show (Implicit n t) = "(Implicit " ++ show n ++ " " ++ show t ++ ")"
317+ show (Constraint n t) = "(Constraint " ++ show n ++ " " ++ show t ++ ")"
318+
319+instance Show TyDecl where
320+ show (Declare fn args ret) = "(Declare " ++ show fn ++ " " ++
321+ show args ++ " " ++ show ret ++ ")"