@@ -26,6 +26,8 @@ import qualified Data.Map as M
2626import Data.Maybe (mapMaybe, fromMaybe)
2727import qualified Data.Set as S
2828import qualified Data.Text as T
29+import Data.Vector.Unboxed (Vector)
30+import qualified Data.Vector.Unboxed as V
2931
3032import Debug.Trace
3133
@@ -1559,15 +1561,7 @@ reifyTTBinderApp reif f [t]
15591561reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
15601562
15611563reifyTTConst :: 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))
15661564reifyTTConst (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)))
15711565reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType
15721566reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
15731567reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
@@ -1576,6 +1570,8 @@ reifyTTConst t@(App _ _)
15761570reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
15771571
15781572reifyTTConstApp :: Name -> Term -> ElabD Const
1573+reifyTTConstApp f aty
1574+ | f == reflm "AType" = fmap AType (reifyArithTy aty)
15791575reifyTTConstApp f (Constant c@(I _))
15801576 | f == reflm "I" = return $ c
15811577reifyTTConstApp f (Constant c@(BI _))
@@ -1596,6 +1592,26 @@ reifyTTConstApp f (Constant c@(B64 _))
15961592 | f == reflm "B64" = return $ c
15971593reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
15981594
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+
15991615reifyTTUExp :: Term -> ElabD UExp
16001616reifyTTUExp t@(App _ _)
16011617 = case unApply t of
@@ -1829,28 +1845,45 @@ reflectBinderQuote unq (PVar t)
18291845reflectBinderQuote unq (PVTy t)
18301846 = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
18311847
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+
18321854reflectConstant :: Const -> Raw
18331855reflectConstant c@(I _) = reflCall "I" [RConstant c]
18341856reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
18351857reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
18361858reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
18371859reflectConstant 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")
18431860reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
18441861reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
18451862reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
18461863reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
1847−reflectConstant (AType (ATInt (ITFixed IT8))) = Var (reflm "B8Type")
1848−reflectConstant (AType (ATInt (ITFixed IT16))) = Var (reflm "B16Type")
1849−reflectConstant (AType (ATInt (ITFixed IT32))) = Var (reflm "B32Type")
1850−reflectConstant (AType (ATInt (ITFixed IT64))) = Var (reflm "B64Type")
1851−reflectConstant (PtrType) = Var (reflm "PtrType")
1852−reflectConstant (VoidType) = Var (reflm "VoidType")
1853−reflectConstant (Forgot) = Var (reflm "Forgot")
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")
1873+reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
1874+reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
1875+reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
1876+reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
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")
1884+reflectConstant VoidType = Var (reflm "VoidType")
1885+reflectConstant Forgot = Var (reflm "Forgot")
1886+
18541887
18551888reflectUExp :: UExp -> Raw
18561889reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]