Update reflection for Float -> Double change

libs/base/Data/Complex.idr

@@ -25,7 +25,7 @@ instance Show a => Show (Complex a) where
             plus_i = User 6
 
 
--- when we have a type class 'Fractional' (which contains Float and Double),
+-- when we have a type class 'Fractional' (which contains Double),
 -- we can do:
 {-
 instance Fractional a => Fractional (Complex a) where

libs/base/Language/Reflection/Utils.idr

@@ -129,7 +129,7 @@ instance Show IntTy where
 
 instance Show ArithTy where
   showPrec d (ATInt t) = showCon d "ATInt" $ showArg t
-  showPrec d ATFloat   = "ATFloat"
+  showPrec d ATDouble   = "ATDouble"
 
 instance Show Const where
   showPrec d (I i)      = showCon d "I" $ showArg i
@@ -162,7 +162,7 @@ instance Eq Reflection.IntTy where
 
 instance Eq ArithTy where
   (ATInt x) == (ATInt y) = x == y
-  ATFloat   == ATFloat   = True
+  ATDouble  == ATDouble   = True
   _         == _         = False
 
 instance Eq Const where

libs/prelude/Language/Reflection.idr

@@ -70,10 +70,10 @@ data NativeTy = IT8 | IT16 | IT32 | IT64
 
 data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
 
-data ArithTy = ATInt Language.Reflection.IntTy | ATFloat
+data ArithTy = ATInt Language.Reflection.IntTy | ATDouble
 
 ||| Primitive constants
-data Const = I Int | BI Integer | Fl Float | Ch Char | Str String
+data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
            | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
            | AType ArithTy | StrType
            | VoidType | Forgot
@@ -89,7 +89,7 @@ instance ReflConst Int where
 instance ReflConst Integer where
    toConst = BI
 
-instance ReflConst Float where
+instance ReflConst Double where
    toConst = Fl
 
 instance ReflConst Char where
@@ -366,12 +366,12 @@ instance Quotable Int Raw where
   quotedTy = `(Int)
   quote x = RConstant (I x)
 
-instance Quotable Float TT where
-  quotedTy = `(Float)
+instance Quotable Double TT where
+  quotedTy = `(Double)
   quote x = TConst (Fl x)
 
-instance Quotable Float Raw where
-  quotedTy = `(Float)
+instance Quotable Double Raw where
+  quotedTy = `(Double)
   quote x = RConstant (Fl x)
 
 instance Quotable Char TT where
@@ -541,12 +541,12 @@ instance Quotable Reflection.IntTy Raw where
 instance Quotable ArithTy TT where
   quotedTy = `(ArithTy)
   quote (ATInt x) = `(ATInt ~(quote x))
-  quote ATFloat = `(ATFloat)
+  quote ATDouble = `(ATDouble)
 
 instance Quotable ArithTy Raw where
   quotedTy = `(ArithTy)
   quote (ATInt x) = `(ATInt ~(quote {t=Raw} x))
-  quote ATFloat = `(ATFloat)
+  quote ATDouble = `(ATDouble)
 
 instance Quotable Const TT where
   quotedTy = `(Const)

src/Idris/Reflection.hs

@@ -357,8 +357,8 @@ reifyTTConstApp f v@(P _ _ _) =
 reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
 
 reifyArithTy :: Term -> ElabD ArithTy
-reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt"   = fmap ATInt (reifyIntTy intTy)
-reifyArithTy (P _ n _)             | n == reflm "ATFloat" = return ATFloat
+reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt"    = fmap ATInt (reifyIntTy intTy)
+reifyArithTy (P _ n _)               | n == reflm "ATDouble" = return ATFloat
 reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
 
 reifyNativeTy :: Term -> ElabD NativeTy
@@ -768,7 +768,7 @@ reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
 reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
 reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
 reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
-reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
+reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATDouble")]
 reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
 reflectConstant StrType = Var (reflm "StrType")
 reflectConstant (AType (ATInt (ITFixed IT8)))  = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]