@@ -1,6 +1,7 @@
1module Language.Reflection.Utils
1module Language.Reflection.Utils
3import Language.Reflection
3import Language.Reflection
4+import Language.Reflection.Elab
4import Language.Reflection.Errors
5import Language.Reflection.Errors
6--------------------------------------------------------
7--------------------------------------------------------
@@ -50,7 +51,7 @@ mkApp tm [] = tm
50mkApp tm (a::as) = mkApp (App tm a) as
51mkApp tm (a::as) = mkApp (App tm a) as
53−binderTy : (Eq t) => Binder t -> t
54+binderTy : Binder t -> t
54binderTy (Lam t) = t
55binderTy (Lam t) = t
55binderTy (Pi t _) = t
56binderTy (Pi t _) = t
56binderTy (Let t1 t2) = t1
57binderTy (Let t1 t2) = t1
@@ -75,7 +76,7 @@ mutual
75 show (MetaN parent meta) = "(MetaN " ++ show parent ++ " " ++ show meta ++ ")"
76 show (MetaN parent meta) = "(MetaN " ++ show parent ++ " " ++ show meta ++ ")"
77 instance Show TTName where
78 instance Show TTName where
78− show (UN str) = "(UN " ++ str ++ ")"
79+ show (UN str) = "(UN " ++ show str ++ ")"
79 show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
80 show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
80 show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"
81 show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"
81 show (SN sn) = "(SN " ++ assert_total (show sn) ++ ")"
82 show (SN sn) = "(SN " ++ assert_total (show sn) ++ ")"
@@ -252,12 +253,12 @@ forget tm = fe [] tm
252instance Show Raw where
253instance Show Raw where
253 show r = my_show r
254 show r = my_show r
254 where %assert_total my_show : Raw -> String
255 where %assert_total my_show : Raw -> String
255− my_show (Var n) = "Var " ++ show n
256+ 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 (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'
258+ my_show (RApp tm tm') = "(RApp " ++ my_show tm ++ " " ++ my_show tm' ++ ")"
258 my_show RType = "RType"
259 my_show RType = "RType"
259− my_show (RForce tm) = "RForce " ++ my_show tm
260+ my_show (RForce tm) = "(RForce " ++ my_show tm ++ ")"
260− my_show (RConstant c) = "RConstant " ++ show c
261+ my_show (RConstant c) = "(RConstant " ++ show c ++ ")"
262instance Show SourceLocation where
263instance Show SourceLocation where
263 show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col
264 show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col
@@ -306,3 +307,15 @@ instance Show Err where
307pure : Raw -> Raw
308pure : Raw -> Raw
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 ++ ")"
319+instance Show TyDecl where
320+ show (Declare fn args ret) = "(Declare " ++ show fn ++ " " ++
321+ show args ++ " " ++ show ret ++ ")"