on master help sign in
Update reflection for Float -> Double change
42eeb6eDavid Raymond Christiansen
libs/base/Data/Complex.idr+1−1
@@ -25,7 +25,7 @@ instance Show a => Show (Complex a) where
25 plus_i = User 6
25 plus_i = User 6
26
26
27
27
28−-- when we have a type class 'Fractional' (which contains Float and Double),
28+-- when we have a type class 'Fractional' (which contains Double),
29-- we can do:
29-- we can do:
30{-
30{-
31instance Fractional a => Fractional (Complex a) where
31instance Fractional a => Fractional (Complex a) where
libs/base/Language/Reflection/Utils.idr+2−2
@@ -129,7 +129,7 @@ instance Show IntTy where
129
129
130instance Show ArithTy where
130instance Show ArithTy where
131 showPrec d (ATInt t) = showCon d "ATInt" $ showArg t
131 showPrec d (ATInt t) = showCon d "ATInt" $ showArg t
132− showPrec d ATFloat = "ATFloat"
132+ showPrec d ATDouble = "ATDouble"
133
133
134instance Show Const where
134instance Show Const where
135 showPrec d (I i) = showCon d "I" $ showArg i
135 showPrec d (I i) = showCon d "I" $ showArg i
@@ -162,7 +162,7 @@ instance Eq Reflection.IntTy where
162
162
163instance Eq ArithTy where
163instance Eq ArithTy where
164 (ATInt x) == (ATInt y) = x == y
164 (ATInt x) == (ATInt y) = x == y
165− ATFloat == ATFloat = True
165+ ATDouble == ATDouble = True
166 _ == _ = False
166 _ == _ = False
167
167
168instance Eq Const where
168instance Eq Const where
libs/prelude/Language/Reflection.idr+9−9
@@ -70,10 +70,10 @@ data NativeTy = IT8 | IT16 | IT32 | IT64
70
70
71data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
71data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
72
72
73−data ArithTy = ATInt Language.Reflection.IntTy | ATFloat
73+data ArithTy = ATInt Language.Reflection.IntTy | ATDouble
74
74
75||| Primitive constants
75||| Primitive constants
76−data Const = I Int | BI Integer | Fl Float | Ch Char | Str String
76+data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
77 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
77 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
78 | AType ArithTy | StrType
78 | AType ArithTy | StrType
79 | VoidType | Forgot
79 | VoidType | Forgot
@@ -89,7 +89,7 @@ instance ReflConst Int where
89instance ReflConst Integer where
89instance ReflConst Integer where
90 toConst = BI
90 toConst = BI
91
91
92−instance ReflConst Float where
92+instance ReflConst Double where
93 toConst = Fl
93 toConst = Fl
94
94
95instance ReflConst Char where
95instance ReflConst Char where
@@ -366,12 +366,12 @@ instance Quotable Int Raw where
366 quotedTy = `(Int)
366 quotedTy = `(Int)
367 quote x = RConstant (I x)
367 quote x = RConstant (I x)
368
368
369−instance Quotable Float TT where
369+instance Quotable Double TT where
370− quotedTy = `(Float)
370+ quotedTy = `(Double)
371 quote x = TConst (Fl x)
371 quote x = TConst (Fl x)
372
372
373−instance Quotable Float Raw where
373+instance Quotable Double Raw where
374− quotedTy = `(Float)
374+ quotedTy = `(Double)
375 quote x = RConstant (Fl x)
375 quote x = RConstant (Fl x)
376
376
377instance Quotable Char TT where
377instance Quotable Char TT where
@@ -541,12 +541,12 @@ instance Quotable Reflection.IntTy Raw where
541instance Quotable ArithTy TT where
541instance Quotable ArithTy TT where
542 quotedTy = `(ArithTy)
542 quotedTy = `(ArithTy)
543 quote (ATInt x) = `(ATInt ~(quote x))
543 quote (ATInt x) = `(ATInt ~(quote x))
544− quote ATFloat = `(ATFloat)
544+ quote ATDouble = `(ATDouble)
545
545
546instance Quotable ArithTy Raw where
546instance Quotable ArithTy Raw where
547 quotedTy = `(ArithTy)
547 quotedTy = `(ArithTy)
548 quote (ATInt x) = `(ATInt ~(quote {t=Raw} x))
548 quote (ATInt x) = `(ATInt ~(quote {t=Raw} x))
549− quote ATFloat = `(ATFloat)
549+ quote ATDouble = `(ATDouble)
550
550
551instance Quotable Const TT where
551instance Quotable Const TT where
552 quotedTy = `(Const)
552 quotedTy = `(Const)
src/Idris/Reflection.hs+3−3
@@ -357,8 +357,8 @@ reifyTTConstApp f v@(P _ _ _) =
357reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
357reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
358
358
359reifyArithTy :: Term -> ElabD ArithTy
359reifyArithTy :: Term -> ElabD ArithTy
360−reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
360+reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
361−reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat
361+reifyArithTy (P _ n _) | n == reflm "ATDouble" = return ATFloat
362reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
362reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
363
363
364reifyNativeTy :: Term -> ElabD NativeTy
364reifyNativeTy :: Term -> ElabD NativeTy
@@ -768,7 +768,7 @@ reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
768reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
768reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
769reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
769reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
770reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
770reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
771−reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
771+reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATDouble")]
772reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
772reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
773reflectConstant StrType = Var (reflm "StrType")
773reflectConstant StrType = Var (reflm "StrType")
774reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
774reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]