on master help sign in
Update Eq and Show reflection for internals changes
9884992David Raymond Christiansen
libs/base/Language/Reflection/Utils.idr+55−34
@@ -3,6 +3,8 @@ module Language.Reflection.Utils
3import Language.Reflection
3import Language.Reflection
4import Language.Reflection.Errors
4import Language.Reflection.Errors
5
5
6+%default total
7+
6--------------------------------------------------------
8--------------------------------------------------------
7-- Tactic construction conveniences
9-- Tactic construction conveniences
8--------------------------------------------------------
10--------------------------------------------------------
@@ -83,46 +85,65 @@ instance Show Const where
83 show (Fl f) = "(Fl " ++ show f ++ ")"
85 show (Fl f) = "(Fl " ++ show f ++ ")"
84 show (Ch c) = "(Ch " ++ show c ++ ")"
86 show (Ch c) = "(Ch " ++ show c ++ ")"
85 show (Str str) = "(Str " ++ show str ++ ")"
87 show (Str str) = "(Str " ++ show str ++ ")"
86− show IType = "IType"
87− show BIType = "BIType"
88− show FlType = "FlType"
89− show ChType = "ChType"
90− show StrType = "StrType"
91 show (B8 b) = "(B8 ...)"
88 show (B8 b) = "(B8 ...)"
92 show (B16 b) = "(B16 ...)"
89 show (B16 b) = "(B16 ...)"
93 show (B32 b) = "(B32 ...)"
90 show (B32 b) = "(B32 ...)"
94 show (B64 b) = "(B64 ...)"
91 show (B64 b) = "(B64 ...)"
95− show B8Type = "B8Type"
92+ show (B8V xs) = "(B8V " ++ show xs ++ ")"
96− show B16Type = "B16Type"
93+ show (B16V xs) = "(B16V " ++ show xs ++")"
97− show B32Type = "B32Type"
94+ show (B32V xs) = "(B32V " ++ show xs ++ ")"
98− show B64Type = "B64Type"
95+ show (B64V xs) = "(B64V " ++ show xs ++ ")"
96+ show (AType x) = "(AType ...)"
97+ show StrType = "StrType"
99− show PtrType = "PtrType"
98+ show PtrType = "PtrType"
99+ show ManagedPtrType = "ManagedPtrType"
100+ show BufferType = "BufferType"
100− show VoidType = "VoidType"
101+ show VoidType = "VoidType"
101− show Forgot = "Forgot"
102+ show Forgot = "Forgot"
103+
104+instance Eq NativeTy where
105+ IT8 == IT8 = True
106+ IT16 == IT16 = True
107+ IT32 == IT32 = True
108+ IT64 == IT64 = True
109+ _ == _ = False
110+
111+instance Eq Reflection.IntTy where
112+ (ITFixed x) == (ITFixed y) = x == y
113+ ITNative == ITNative = True
114+ ITBig == ITBig = True
115+ ITChar == ITChar = True
116+ (ITVec x i) == (ITVec y j) = x == y && i == j
117+ _ == _ = False
118+
119+instance Eq ArithTy where
120+ (ATInt x) == (ATInt y) = x == y
121+ ATFloat == ATFloat = True
122+ _ == _ = False
102
123
103instance Eq Const where
124instance Eq Const where
104− (I i) == (I i') = i == i'
125+ (I x) == (I y) = x == y
105− (BI n) == (BI n') = n == n'
126+ (BI x) == (BI y) = x == y
106− (Fl f) == (Fl f') = f == f'
127+ (Fl x) == (Fl y) = x == y
107− (Ch c) == (Ch c') = c == c'
128+ (Ch x) == (Ch y) = x == y
108− (Str str) == (Str str') = str == str'
129+ (Str x) == (Str y) = x == y
109− IType == IType = True
130+ (B8 x) == (B8 y) = x == y
110− BIType == BIType = True
131+ (B16 x) == (B16 y) = x == y
111− FlType == FlType = True
132+ (B32 x) == (B32 y) = x == y
112− ChType == ChType = True
133+ (B64 x) == (B64 y) = x == y
113− StrType == StrType = True
134+ (B8V xs) == (B8V ys) = False -- TODO
114− (B8 b) == (B8 b') = False -- FIXME: b == b'
135+ (B16V xs) == (B16V ys) = False -- TODO
115− (B16 b) == (B16 b') = False -- FIXME: b == b'
136+ (B32V xs) == (B32V ys) = False -- TODO
116− (B32 b) == (B32 b') = False -- FIXME: b == b'
137+ (B64V xs) == (B64V ys) = False -- TODO
117− (B64 b) == (B64 b') = False -- FIXME: b == b'
138+ (AType x) == (AType y) = x == y
118− B8Type == B8Type = True
139+ StrType == StrType = True
119− B16Type == B16Type = True
140+ PtrType == PtrType = True
120− B32Type == B32Type = True
141+ ManagedPtrType == ManagedPtrType = True
121− B64Type == B64Type = True
142+ BufferType == BufferType = True
122− PtrType == PtrType = True
143+ VoidType == VoidType = True
123− VoidType == VoidType = True
144+ Forgot == Forgot = True
124− Forgot == Forgot = True
125− x == y = False
145+ _ == _ = False
146+
126
147
127instance Show NameType where
148instance Show NameType where
128 show Bound = "Bound"
149 show Bound = "Bound"