Draft for add bindings for numeric typeclasses

lib/Haskell/Prelude.agda

@@ -25,17 +25,24 @@ open import Haskell.Prim.Double      public
 open import Haskell.Prim.Either      public
 open import Haskell.Prim.Enum        public
 open import Haskell.Prim.Eq          public
+open import Haskell.Prim.Floating    public
 open import Haskell.Prim.Foldable    public
+open import Haskell.Prim.Fractional  public
 open import Haskell.Prim.Functor     public
 open import Haskell.Prim.Int         public
 open import Haskell.Prim.Integer     public
+open import Haskell.Prim.Integral    public
 open import Haskell.Prim.IO          public
 open import Haskell.Prim.List        public
 open import Haskell.Prim.Maybe       public
 open import Haskell.Prim.Monad       public
 open import Haskell.Prim.Monoid      public
 open import Haskell.Prim.Num         public
 open import Haskell.Prim.Ord         public
+open import Haskell.Prim.Rational    public
+open import Haskell.Prim.Real        public
+open import Haskell.Prim.RealFloat   public
+open import Haskell.Prim.RealFrac    public
 open import Haskell.Prim.Show        public
 open import Haskell.Prim.String      public
 open import Haskell.Prim.Traversable public

lib/Haskell/Prim/Floating.agda

@@ -0,0 +1,32 @@
+module Haskell.Prim.Floating where
+
+open import Haskell.Prim
+
+--------------------------------------------------
+-- Floating
+
+record Floating (a : Set) : Set where
+  infixr 8 _**_
+  field
+	pi      : a
+	exp     : a → a
+	log     : a → a
+	sqrt	: a → a
+	_**_    : a → a → a
+	logBase : a → a → a
+	sin     : a → a
+	cos     : a → a
+	tan		: a → a
+	asin    : a → a
+	acos    : a → a
+	atan    : a → a
+	sinh    : a → a
+	cosh    : a → a
+	tanh    : a → a
+	asinh   : a → a
+	acosh   : a → a
+	atanh   : a → a
+open Floating ⦃... ⦄  public
+
+{-# COMPILE AGDA2HS Floating existing-class #-}
+

lib/Haskell/Prim/Fractional.agda

@@ -0,0 +1,21 @@
+{-# OPTIONS --no-auto-inline #-}
+
+module Haskell.Prim.Fractional where
+
+open import Haskell.Prim
+open import Haskell.Floating
+open import Haskell.Prim.RealFrac
+
+--------------------------------------------------
+-- Fractional
+
+record Fractional (a : Set) : Set where
+  infixl 7 _/_
+  field
+    _/_ : a → a → a
+    recip : a → a
+    fromRational : Rational → a
+open Fractional ⦃... ⦄  public
+
+{-# COMPILE AGDA2HS Fractional existing-class #-}
+

lib/Haskell/Prim/Integral.agda

@@ -0,0 +1,53 @@
+{-# OPTIONS --no-auto-inline #-}
+
+module Haskell.Prim.Integral where
+
+open import Haskell.Prim
+open import Haskell.Prim.Integer
+open import Haskell.Prim.Tuple
+
+--------------------------------------------------
+-- Integral
+
+record Integral (a : Set) : Set where
+  infixl 7 _quot_ _rem_ _div_ _mod_
+  field
+    _quot_ : a → a → a
+    _rem_ : a → a → a
+    _div_ : a → a → a
+    _mod_ : a → a → a
+    quotRem : a → a → (a × a)
+    divMod : a → a → (a × a) 
+    toInteger : a → Integer
+open Integral ⦃...⦄ public
+
+{-# COMPILE AGDA2HS Integral existing-class #-}
+
+instance
+  iIntegralNat : Integral Nat
+  iIntegralNat._quot_ n d = ?
+  iIntegralNat._rem_ n d = ?
+  iIntegralNat._div_ n d = ?
+  iIntegralNat.quotRem n d = ?
+  iIntegralNat.toInteger x = toInteger x
+
+  iIntegralInt : Integral Int
+  iIntegralInt._quot_ n d = ?
+  iIntegralInt._rem_ n d = ?
+  iIntegralInt._div_ n d = ?
+  iIntegralInt.quotRem n d = ?
+  iIntegralInt.toInteger x = toInteger x
+
+  iIntegralInteger : Integral Integer
+  iIntegralInteger._quot_ n d = ?
+  iIntegralInteger._rem_ n d = ?
+  iIntegralInteger._div_ n d = ?
+  iIntegralInteger.quotRem n d = ?
+  iIntegralInteger.toInteger x = toInteger x
+
+  iIntegralWord : Integral Word
+  iIntegralWord._quot_ n d = ?
+  iIntegralWord._rem_ n d = ?
+  iIntegralWord._div_ n d =?
+  iIntegralWord.quotRem n d = ?
+  iIntegralWord.toInteger x = toInteger x

lib/Haskell/Prim/Rational.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --no-auto-inline #-}
+
+module Haskell.Prim.Rational where
+
+open import Haskell.Prim
+open import Haskell.Prim.Integer
+
+--------------------------------------------------
+-- Definition
+
+record Ratio (a : Set) : Set where
+  inductive
+  constructor _:%_
+  field
+    numerator : a
+    denominator : a
+open Ratio ⦃...⦄ public
+
+-- Rational numbers, represented as a ratio of two 'Integer' values.
+-- A rational number may be constructed using the '%' operator.
+Rational : Set
+Rational = Ratio Integer
+

lib/Haskell/Prim/Real.agda

@@ -0,0 +1,35 @@
+{-# OPTIONS --no-auto-inline #-}
+
+module Haskell.Prim.Real where
+
+open import Haskell.Prim
+open import Haskell.Prim.Rational
+open import Haskell.Prim.Int
+open import Haskell.Prim.Integer
+open import Haskell.Prim.RealFrac
+open import Haskell.Prim.Word
+open import Haskell.Prim.Double
+
+--------------------------------------------------
+-- Real
+
+record Real (a : Set) : Set where
+  field
+    toRational : a → Rational
+open Real ⦃... ⦄  public
+
+{-# COMPILE AGDA2HS Real existing-class #-}
+
+instance
+  iRealNat : Real Nat
+  iRealNat.toRational x = x :% 1
+
+  iRealInt : Real Int
+  iRealInt.toRational x = toInteger x :% 1
+
+  iRealInteger : Real Integer
+  iRealInteger.toRational x = x :% 1
+
+  iRealWord : Real Word
+  iRealWord.toRational x = toInteger x :% 1  
+

lib/Haskell/Prim/RealFloat.agda

@@ -0,0 +1,31 @@
+module Haskell.Prim.RealFloat where
+
+open import Haskell.Prim
+open import Haskell.Prim.Int
+open import Haskell.Prim.Integer
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Tuple
+
+--------------------------------------------------
+-- RealFloat
+
+record RealFloat (a : Set) : Set where
+  field
+    floatRadix       : a → Integer
+    floatDigits      : a → Int
+    floatRange       : a → (Int × Int)
+    decodeFloat      : a → (Integer × Int)
+    encodeFloat      : Integer → Int → a
+    exponent         : a → Int
+    significand      : a → a
+    scaleFloat       : Int → a → a
+    isNaN            : a → Bool
+    isInfinite       : a → Bool
+    isDenormalized   : a → Bool
+    isNegativeZero   : a → Bool
+    isIEEE           : a → Bool
+    atan2            : a → a → a
+open RealFloat ⦃... ⦄  public
+
+{-# COMPILE AGDA2HS RealFloat existing-class #-}
+

lib/Haskell/Prim/RealFrac.agda

@@ -0,0 +1,21 @@
+module Haskell.Prim.RealFrac where
+
+open import Haskell.Prim
+open import Haskell.Prim.Int
+open import Haskell.Prim.Integral
+open import Haskell.Prim.Tuple
+
+--------------------------------------------------
+-- RealFrac
+
+record RealFrac (a : Set) : Set where
+  field
+    properFraction : a → (Int × a)
+    truncate       : a → Integral
+    round          : a → Integral
+    ceiling        : a → Integral
+    floor          : a → Integral
+open RealFrac ⦃... ⦄  public
+
+{-# COMPILE AGDA2HS RealFrac existing-class #-}
+