git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1438 from david-christiansen/reflection-updates
8d5c1feDavid Christiansen
libs/base/Language/Reflection.idr+172−3
compare with master
unifiedsplit
@@ -22,12 +22,20 @@ data TTUExp = UVar Int
22 -- ^ explicit universe variable
22 -- ^ explicit universe variable
23%name TTUExp uexp
23%name TTUExp uexp
24
24
25+data NativeTy = IT8 | IT16 | IT32 | IT64
26+
27+data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
28+ | ITVec NativeTy Int
29+
30+data ArithTy = ATInt Language.Reflection.IntTy | ATFloat
31+
25||| Primitive constants
32||| Primitive constants
26data Const = I Int | BI Integer | Fl Float | Ch Char | Str String
33data Const = I Int | BI Integer | Fl Float | Ch Char | Str String
27− | IType | BIType | FlType | ChType | StrType
28 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
34 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
29− | B8Type | B16Type | B32Type | B64Type
35+ | B8V Bits8x16 | B16V Bits16x8
36+ | B32V Bits32x4 | B64V Bits64x2
37+ | AType ArithTy | StrType
30− | PtrType | VoidType | Forgot
38+ | PtrType | ManagedPtrType | BufferType | VoidType | Forgot
31
39
32%name Const c, c'
40%name Const c, c'
33
41
@@ -213,3 +221,164 @@ data Tactic = Try Tactic Tactic
213 -- ^ do nothing
221 -- ^ do nothing
214 | Fail (List ErrorReportPart)
222 | Fail (List ErrorReportPart)
215%name Tactic tac, tac'
223%name Tactic tac, tac'
224+
225+
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+
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 ...)"
96− show B16Type = "B16Type"
93+ show (B16V xs) = "(B16V ...)"
97− show B32Type = "B32Type"
94+ show (B32V xs) = "(B32V ...)"
98− show B64Type = "B64Type"
95+ show (B64V xs) = "(B64V ...)"
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"
src/Idris/ElabTerm.hs+53−20
@@ -26,6 +26,8 @@ import qualified Data.Map as M
26import Data.Maybe (mapMaybe, fromMaybe)
26import Data.Maybe (mapMaybe, fromMaybe)
27import qualified Data.Set as S
27import qualified Data.Set as S
28import qualified Data.Text as T
28import qualified Data.Text as T
29+import Data.Vector.Unboxed (Vector)
30+import qualified Data.Vector.Unboxed as V
29
31
30import Debug.Trace
32import Debug.Trace
31
33
@@ -1559,15 +1561,7 @@ reifyTTBinderApp reif f [t]
1559reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
1561reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
1560
1562
1561reifyTTConst :: Term -> ElabD Const
1563reifyTTConst :: Term -> ElabD Const
1562−reifyTTConst (P _ n _) | n == reflm "IType" = return (AType (ATInt ITNative))
1563−reifyTTConst (P _ n _) | n == reflm "BIType" = return (AType (ATInt ITBig))
1564−reifyTTConst (P _ n _) | n == reflm "FlType" = return (AType ATFloat)
1565−reifyTTConst (P _ n _) | n == reflm "ChType" = return (AType (ATInt ITChar))
1566reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
1564reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
1567−reifyTTConst (P _ n _) | n == reflm "B8Type" = return (AType (ATInt (ITFixed IT8)))
1568−reifyTTConst (P _ n _) | n == reflm "B16Type" = return (AType (ATInt (ITFixed IT16)))
1569−reifyTTConst (P _ n _) | n == reflm "B32Type" = return (AType (ATInt (ITFixed IT32)))
1570−reifyTTConst (P _ n _) | n == reflm "B64Type" = return (AType (ATInt (ITFixed IT64)))
1571reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType
1565reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType
1572reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
1566reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
1573reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
1567reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
@@ -1576,6 +1570,8 @@ reifyTTConst t@(App _ _)
1576reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
1570reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
1577
1571
1578reifyTTConstApp :: Name -> Term -> ElabD Const
1572reifyTTConstApp :: Name -> Term -> ElabD Const
1573+reifyTTConstApp f aty
1574+ | f == reflm "AType" = fmap AType (reifyArithTy aty)
1579reifyTTConstApp f (Constant c@(I _))
1575reifyTTConstApp f (Constant c@(I _))
1580 | f == reflm "I" = return $ c
1576 | f == reflm "I" = return $ c
1581reifyTTConstApp f (Constant c@(BI _))
1577reifyTTConstApp f (Constant c@(BI _))
@@ -1596,6 +1592,26 @@ reifyTTConstApp f (Constant c@(B64 _))
1596 | f == reflm "B64" = return $ c
1592 | f == reflm "B64" = return $ c
1597reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
1593reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
1598
1594
1595+reifyArithTy :: Term -> ElabD ArithTy
1596+reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
1597+reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat
1598+reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
1599+
1600+reifyNativeTy :: Term -> ElabD NativeTy
1601+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
1602+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
1603+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
1604+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
1605+reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x
1606+
1607+reifyIntTy :: Term -> ElabD IntTy
1608+reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
1609+reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
1610+reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
1611+reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
1612+reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)
1613+ (reifyNativeTy nt)
1614+
1599reifyTTUExp :: Term -> ElabD UExp
1615reifyTTUExp :: Term -> ElabD UExp
1600reifyTTUExp t@(App _ _)
1616reifyTTUExp t@(App _ _)
1601 = case unApply t of
1617 = case unApply t of
@@ -1829,28 +1845,45 @@ reflectBinderQuote unq (PVar t)
1829reflectBinderQuote unq (PVTy t)
1845reflectBinderQuote unq (PVTy t)
1830 = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
1846 = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
1831
1847
1848+mkList :: Raw -> [Raw] -> Raw
1849+mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
1850+mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
1851+ x)
1852+ (mkList ty xs)
1853+
1832reflectConstant :: Const -> Raw
1854reflectConstant :: Const -> Raw
1833reflectConstant c@(I _) = reflCall "I" [RConstant c]
1855reflectConstant c@(I _) = reflCall "I" [RConstant c]
1834reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
1856reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
1835reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
1857reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
1836reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
1858reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
1837reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
1859reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
1838−reflectConstant (AType (ATInt ITNative)) = Var (reflm "IType")
1839−reflectConstant (AType (ATInt ITBig)) = Var (reflm "BIType")
1840−reflectConstant (AType ATFloat) = Var (reflm "FlType")
1841−reflectConstant (AType (ATInt ITChar)) = Var (reflm "ChType")
1842−reflectConstant (StrType) = Var (reflm "StrType")
1843reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
1860reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
1844reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
1861reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
1845reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
1862reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
1846reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
1863reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
1864+reflectConstant (B8V ws) = reflCall "B8V" [mkList (Var (sUN "Bits8")) . map (RConstant . B8) . V.toList $ ws]
1865+reflectConstant (B16V ws) = reflCall "B8V" [mkList (Var (sUN "Bits16")) . map (RConstant . B16) . V.toList $ ws]
1866+reflectConstant (B32V ws) = reflCall "B8V" [mkList (Var (sUN "Bits32")) . map (RConstant . B32) . V.toList $ ws]
1867+reflectConstant (B64V ws) = reflCall "B8V" [mkList (Var (sUN "Bits64")) . map (RConstant . B64) . V.toList $ ws]
1868+reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
1869+reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
1870+reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
1871+reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
1872+reflectConstant StrType = Var (reflm "StrType")
1847−reflectConstant (AType (ATInt (ITFixed IT8))) = Var (reflm "B8Type")
1873+reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
1848−reflectConstant (AType (ATInt (ITFixed IT16))) = Var (reflm "B16Type")
1874+reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
1849−reflectConstant (AType (ATInt (ITFixed IT32))) = Var (reflm "B32Type")
1875+reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
1850−reflectConstant (AType (ATInt (ITFixed IT64))) = Var (reflm "B64Type")
1876+reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
1851−reflectConstant (PtrType) = Var (reflm "PtrType")
1877+reflectConstant (AType (ATInt (ITVec IT8 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT8"), RConstant (I c)]]]
1878+reflectConstant (AType (ATInt (ITVec IT16 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT16"), RConstant (I c)]]]
1879+reflectConstant (AType (ATInt (ITVec IT32 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT32"), RConstant (I c)]]]
1880+reflectConstant (AType (ATInt (ITVec IT64 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT64"), RConstant (I c)]]]
1881+reflectConstant PtrType = Var (reflm "PtrType")
1882+reflectConstant ManagedPtrType = Var (reflm "ManagedPtrType")
1883+reflectConstant BufferType = Var (reflm "BufferType")
1852−reflectConstant (VoidType) = Var (reflm "VoidType")
1884+reflectConstant VoidType = Var (reflm "VoidType")
1853−reflectConstant (Forgot) = Var (reflm "Forgot")
1885+reflectConstant Forgot = Var (reflm "Forgot")
1886+
1854
1887
1855reflectUExp :: UExp -> Raw
1888reflectUExp :: UExp -> Raw
1856reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
1889reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]