git.iko.soy/Idris-dev
on master help sign in
Update reflection code to current core language.
c41b605David Raymond Christiansen
libs/base/Language/Reflection.idr+13−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,5 @@ 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+
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)]