From 8138d9ca1a8543afbb0d2f8f2e67c961e0954fd5 Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Sat, 20 Jul 2024 14:53:37 +0200
Subject: [PATCH 1/9] draft

---
 lib/Haskell/Prim/Floating.agda   | 29 +++++++++++++++++++++++++++++
 lib/Haskell/Prim/Fractional.agda | 23 +++++++++++++++++++++++
 lib/Haskell/Prim/Integral.agda   | 25 +++++++++++++++++++++++++
 lib/Haskell/Prim/Real.agda       | 24 ++++++++++++++++++++++++
 lib/Haskell/Prim/RealFloat.agda  | 26 ++++++++++++++++++++++++++
 lib/Haskell/Prim/RealFrac.agda   | 14 ++++++++++++++
 6 files changed, 141 insertions(+)
 create mode 100644 lib/Haskell/Prim/Floating.agda
 create mode 100644 lib/Haskell/Prim/Fractional.agda
 create mode 100644 lib/Haskell/Prim/Integral.agda
 create mode 100644 lib/Haskell/Prim/Real.agda
 create mode 100644 lib/Haskell/Prim/RealFloat.agda
 create mode 100644 lib/Haskell/Prim/RealFrac.agda

diff --git a/lib/Haskell/Prim/Floating.agda b/lib/Haskell/Prim/Floating.agda
new file mode 100644
index 00000000..36318767
--- /dev/null
+++ b/lib/Haskell/Prim/Floating.agda
@@ -0,0 +1,29 @@
+module Haskell.Prim.Floating where
+
+open import Haskell.Prim
+
+postulate
+  pi      : Floating
+  exp     : Floating → Floating
+  log     : Floating → Floating
+  sqrt	  : Floating → Floating
+  _**_    : Floating → Floating → Floating
+  logBase : Floating → Floating → Floating
+  sin     : Floating → Floating
+  cos     : Floating → Floating
+  asin    : Floating → Floating
+  acos    : Floating → Floating
+  atan    : Floating → Floating
+  sinh    : Floating → Floating
+  cosh    : Floating → Floating
+  asinh   : Floating → Floating
+  acosh   : Floating → Floating
+  atanh   : Floating → Floating
+  log1p   : Floating → Floating
+  expm1   : Floating → Floating
+  log1pexp: Floating → Floating
+  log1mexp: Floating → Floating
+
+--------------------------------------------------
+-- Arithmetic
+
diff --git a/lib/Haskell/Prim/Fractional.agda b/lib/Haskell/Prim/Fractional.agda
new file mode 100644
index 00000000..5b18a91f
--- /dev/null
+++ b/lib/Haskell/Prim/Fractional.agda
@@ -0,0 +1,23 @@
+module Haskell.Prim.Fractional where
+
+open import Haskell.Prim
+
+--------------------------------------------------
+-- Definition
+
+data Fractional : Set where
+
+--------------------------------------------------
+-- Literals
+
+instance
+  iNumberFractional : Number Fractional
+  iNumberFractional .Number.Constraint _ = ⊤
+  iNumberFractional .fromNat n = pos n
+
+  iNegativeFractional : Negative Fractional
+  iNegativeFractional .Negative.Constraint _ = ⊤
+  iNegativeFractional .fromNeg n =
+  
+--------------------------------------------------
+-- Arithmetic
\ No newline at end of file
diff --git a/lib/Haskell/Prim/Integral.agda b/lib/Haskell/Prim/Integral.agda
new file mode 100644
index 00000000..12c7ba81
--- /dev/null
+++ b/lib/Haskell/Prim/Integral.agda
@@ -0,0 +1,25 @@
+module Haskell.Prim.Integral where
+
+open import Haskell.Prim
+
+--------------------------------------------------
+-- Definition
+
+data Integral : Set where
+
+--------------------------------------------------
+-- Literals
+
+instance
+  iNumberIntegral : Number Integral
+  iNumberIntegral .Number.Constraint _ = ⊤
+  iNumberIntegral .fromNat n = pos n
+
+  iNegativeIntegral : Negative Integral
+  iNegativeIntegral .Negative.Constraint _ = ⊤
+  iNegativeIntegral .fromNeg n =
+  
+  
+--------------------------------------------------
+-- Arithmetic
+
diff --git a/lib/Haskell/Prim/Real.agda b/lib/Haskell/Prim/Real.agda
new file mode 100644
index 00000000..b5fc0fb1
--- /dev/null
+++ b/lib/Haskell/Prim/Real.agda
@@ -0,0 +1,24 @@
+module Haskell.Prim.Real where
+
+open import Haskell.Prim
+
+--------------------------------------------------
+-- Definition
+
+data Real : Set where
+
+--------------------------------------------------
+-- Literals
+
+instance
+  iNumberReal : Number Real
+  iNumberReal .Number.Constraint _ = ⊤
+  iNumberReal .fromNat n = pos n
+
+  iNegativeReal : Negative Real
+  iNegativeReal .Negative.Constraint _ = ⊤
+  iNegativeReal .fromNeg n =
+  
+  
+--------------------------------------------------
+-- Arithmetic
\ No newline at end of file
diff --git a/lib/Haskell/Prim/RealFloat.agda b/lib/Haskell/Prim/RealFloat.agda
new file mode 100644
index 00000000..25cb5359
--- /dev/null
+++ b/lib/Haskell/Prim/RealFloat.agda
@@ -0,0 +1,26 @@
+module Haskell.Prim.RealFloat where
+
+open import Haskell.Prim
+open import Haskell.Prim.Int
+open import Haskell.Prim.Bool
+
+-- The RealFloat typeclass functions
+postulate
+  floatRadix       : RealFloat → Int
+  floatDigits      : RealFloat → Int
+  floatRange       : RealFloat → Σ Int (λ _ → Int)
+  decodeFloat      : RealFloat → Σ Int (λ _ → Int)
+  encodeFloat      : Int → Int → RealFloat
+  exponent         : RealFloat → Int
+  significand      : RealFloat → Float
+  scaleFloat       : Int → RealFloat → RealFloat
+  isNaN            : RealFloat → Bool
+  isInfinite       : RealFloat → Bool
+  isDenormalized   : RealFloat → Bool
+  isNegativeZero   : RealFloat → Bool
+  isIEEE           : RealFloat → Bool
+  atan2			   : RealFloat → RealFloat → RealFloat
+  
+--------------------------------------------------
+-- Arithmetic
+
diff --git a/lib/Haskell/Prim/RealFrac.agda b/lib/Haskell/Prim/RealFrac.agda
new file mode 100644
index 00000000..37bb1ba1
--- /dev/null
+++ b/lib/Haskell/Prim/RealFrac.agda
@@ -0,0 +1,14 @@
+module Haskell.Prim.RealFrac where
+
+open import Haskell.Prim
+
+postulate
+  properFraction : Float → Σ Int (λ _ → Float)
+  truncate       : Float → Int
+  round          : Float → Int
+  ceiling        : Float → Int
+  floor          : Float → Int
+
+--------------------------------------------------
+-- Arithmetic
+

From fba852a06a3b681196ca56852e5c2ef84468331d Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Sat, 20 Jul 2024 16:29:45 +0200
Subject: [PATCH 2/9] draft

---
 lib/Haskell/Prim/Floating.agda   | 28 ++++++++++++++++++++++++++
 lib/Haskell/Prim/Fractional.agda | 18 +++++++++++++++--
 lib/Haskell/Prim/Integral.agda   | 11 +++++++++++
 lib/Haskell/Prim/Real.agda       | 15 +++++++++++++-
 lib/Haskell/Prim/RealFloat.agda  | 24 ++++++++++++++++++++++
 lib/Haskell/Prim/RealFrac.agda   | 34 +++++++++++++++++++++++++++-----
 6 files changed, 122 insertions(+), 8 deletions(-)

diff --git a/lib/Haskell/Prim/Floating.agda b/lib/Haskell/Prim/Floating.agda
index 36318767..7817eaef 100644
--- a/lib/Haskell/Prim/Floating.agda
+++ b/lib/Haskell/Prim/Floating.agda
@@ -2,11 +2,27 @@ module Haskell.Prim.Floating where
 
 open import Haskell.Prim
 
+
+--------------------------------------------------
+-- Literals
+
+
+instance
+  iNumberFloating : Number Floating
+  iNumberFloating .Number.Constraint _ = ⊤
+  iNumberFloating .fromNat n = pos n
+
+  iNegativeFloating : Negative Floating
+  iNegativeFloating .Negative.Constraint _ = ⊤
+  iNegativeFloating .fromNeg n = negNat n
+
+
 postulate
   pi      : Floating
   exp     : Floating → Floating
   log     : Floating → Floating
   sqrt	  : Floating → Floating
+  infixr 8 _**_
   _**_    : Floating → Floating → Floating
   logBase : Floating → Floating → Floating
   sin     : Floating → Floating
@@ -27,3 +43,15 @@ postulate
 --------------------------------------------------
 -- Arithmetic
 
+
+--------------------------------------------------
+-- Constraints
+
+isNegativeFloating : Floating → Bool
+isNegativeFloating (pos _)    = False
+isNegativeFloating (negsuc _) = True
+
+IsNonNegativeFloating : Floating → Set
+IsNonNegativeFloating (pos _)      = ⊤
+IsNonNegativeFloating n@(negsuc _) =
+  TypeError (primStringAppend (primShowFloating n) (" is negative"))
\ No newline at end of file
diff --git a/lib/Haskell/Prim/Fractional.agda b/lib/Haskell/Prim/Fractional.agda
index 5b18a91f..136924e0 100644
--- a/lib/Haskell/Prim/Fractional.agda
+++ b/lib/Haskell/Prim/Fractional.agda
@@ -17,7 +17,21 @@ instance
 
   iNegativeFractional : Negative Fractional
   iNegativeFractional .Negative.Constraint _ = ⊤
-  iNegativeFractional .fromNeg n =
+  iNegativeFractional .fromNeg n = 
   
 --------------------------------------------------
--- Arithmetic
\ No newline at end of file
+-- Arithmetic
+
+
+
+--------------------------------------------------
+-- Constraints
+
+isNegativeFractional : Fractional → Bool
+isNegativeFractional (pos _)    = False
+isNegativeFractional (negsuc _) = True
+
+IsNonNegativeFractional : Fractional → Set
+IsNonNegativeFractional (pos _)      = ⊤
+IsNonNegativeFractional n@(negsuc _) =
+  TypeError (primStringAppend (primShowFractional n) (" is negative"))
\ No newline at end of file
diff --git a/lib/Haskell/Prim/Integral.agda b/lib/Haskell/Prim/Integral.agda
index 12c7ba81..b6216728 100644
--- a/lib/Haskell/Prim/Integral.agda
+++ b/lib/Haskell/Prim/Integral.agda
@@ -23,3 +23,14 @@ instance
 --------------------------------------------------
 -- Arithmetic
 
+--------------------------------------------------
+-- Constraints
+
+isNegativeIntegral : Integral → Bool
+isNegativeIntegral (pos _)    = False
+isNegativeIntegral (negsuc _) = True
+
+IsNonNegativeIntegral : Integral → Set
+IsNonNegativeIntegral (pos _)      = ⊤
+IsNonNegativeIntegral n@(negsuc _) =
+  TypeError (primStringAppend (primShowIntegral n) (" is negative"))
\ No newline at end of file
diff --git a/lib/Haskell/Prim/Real.agda b/lib/Haskell/Prim/Real.agda
index b5fc0fb1..c1ba7bdd 100644
--- a/lib/Haskell/Prim/Real.agda
+++ b/lib/Haskell/Prim/Real.agda
@@ -21,4 +21,17 @@ instance
   
   
 --------------------------------------------------
--- Arithmetic
\ No newline at end of file
+-- Arithmetic
+
+
+--------------------------------------------------
+-- Constraints
+
+isNegativeReal : Real → Bool
+isNegativeReal (pos _)    = False
+isNegativeReal (negsuc _) = True
+
+IsNonNegativeReal : Real → Set
+IsNonNegativeReal (pos _)      = ⊤
+IsNonNegativeReal n@(negsuc _) =
+  TypeError (primStringAppend (primShowReal n) (" is negative"))
\ No newline at end of file
diff --git a/lib/Haskell/Prim/RealFloat.agda b/lib/Haskell/Prim/RealFloat.agda
index 25cb5359..7ab6d22b 100644
--- a/lib/Haskell/Prim/RealFloat.agda
+++ b/lib/Haskell/Prim/RealFloat.agda
@@ -4,6 +4,18 @@ open import Haskell.Prim
 open import Haskell.Prim.Int
 open import Haskell.Prim.Bool
 
+--------------------------------------------------
+-- Literals
+
+instance
+  iNumberRealFloat : Number RealFloat
+  iNumberRealFloat .Number.Constraint _ = ⊤
+  iNumberRealFloat .fromNat n = pos n
+
+  iNegativeRealFloat : Negative RealFloat
+  iNegativeRealFloat .Negative.Constraint _ = ⊤
+  iNegativeRealFloat .fromNeg n = negNat n
+
 -- The RealFloat typeclass functions
 postulate
   floatRadix       : RealFloat → Int
@@ -24,3 +36,15 @@ postulate
 --------------------------------------------------
 -- Arithmetic
 
+
+--------------------------------------------------
+-- Constraints
+
+isNegativeRealFloat : RealFloat → Bool
+isNegativeRealFloat (pos _)    = False
+isNegativeRealFloat (negsuc _) = True
+
+IsNonNegativeRealFloat : RealFloat → Set
+IsNonNegativeRealFloat (pos _)      = ⊤
+IsNonNegativeRealFloat n@(negsuc _) =
+  TypeError (primStringAppend (primShowRealFloat n) (" is negative"))
\ No newline at end of file
diff --git a/lib/Haskell/Prim/RealFrac.agda b/lib/Haskell/Prim/RealFrac.agda
index 37bb1ba1..5e460b56 100644
--- a/lib/Haskell/Prim/RealFrac.agda
+++ b/lib/Haskell/Prim/RealFrac.agda
@@ -2,13 +2,37 @@ module Haskell.Prim.RealFrac where
 
 open import Haskell.Prim
 
+--------------------------------------------------
+-- Literals
+
+instance
+  iNumberRealFrac : Number RealFrac
+  iNumberRealFrac .Number.Constraint _ = ⊤
+  iNumberRealFrac .fromNat n = pos n
+
+  iNegativeRealFrac : Negative RealFrac
+  iNegativeRealFrac .Negative.Constraint _ = ⊤
+  iNegativeRealFrac .fromNeg n = negNat n
+
 postulate
-  properFraction : Float → Σ Int (λ _ → Float)
-  truncate       : Float → Int
-  round          : Float → Int
-  ceiling        : Float → Int
-  floor          : Float → Int
+  properFraction : RealFrac → Int 
+  truncate       : RealFrac → Int
+  round          : RealFrac → Int
+  ceiling        : RealFrac → Int
+  floor          : RealFrac → Int
 
 --------------------------------------------------
 -- Arithmetic
 
+
+--------------------------------------------------
+-- Constraints
+
+isNegativeRealFrac : RealFrac → Bool
+isNegativeRealFrac (pos _)    = False
+isNegativeRealFrac (negsuc _) = True
+
+IsNonNegativeRealFrac : Real → Set
+IsNonNegativeRealFrac (pos _)      = ⊤
+IsNonNegativeRealFrac n@(negsuc _) =
+  TypeError (primStringAppend (primShowRealFrac n) (" is negative"))
\ No newline at end of file

From f0ac510d2de6fef1b725199bd4b58476a455a61f Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Sat, 20 Jul 2024 16:33:34 +0200
Subject: [PATCH 3/9] draft

---
 lib/Haskell/Prim/RealFloat.agda | 4 ++--
 lib/Haskell/Prim/RealFrac.agda  | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lib/Haskell/Prim/RealFloat.agda b/lib/Haskell/Prim/RealFloat.agda
index 7ab6d22b..7b1ad21a 100644
--- a/lib/Haskell/Prim/RealFloat.agda
+++ b/lib/Haskell/Prim/RealFloat.agda
@@ -20,8 +20,8 @@ instance
 postulate
   floatRadix       : RealFloat → Int
   floatDigits      : RealFloat → Int
-  floatRange       : RealFloat → Σ Int (λ _ → Int)
-  decodeFloat      : RealFloat → Σ Int (λ _ → Int)
+  floatRange       : RealFloat → -- todo (Int, Int)
+  decodeFloat      : RealFloat → -- todo (Int, Int)
   encodeFloat      : Int → Int → RealFloat
   exponent         : RealFloat → Int
   significand      : RealFloat → Float
diff --git a/lib/Haskell/Prim/RealFrac.agda b/lib/Haskell/Prim/RealFrac.agda
index 5e460b56..6a71b37c 100644
--- a/lib/Haskell/Prim/RealFrac.agda
+++ b/lib/Haskell/Prim/RealFrac.agda
@@ -15,7 +15,7 @@ instance
   iNegativeRealFrac .fromNeg n = negNat n
 
 postulate
-  properFraction : RealFrac → Int 
+  properFraction : RealFrac → -- todo (Int, )
   truncate       : RealFrac → Int
   round          : RealFrac → Int
   ceiling        : RealFrac → Int

From b9caa9a65a35ffd7f538701c82aab0496e4eaa9c Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Sat, 20 Jul 2024 16:43:39 +0200
Subject: [PATCH 4/9] Realfrac properFraction

---
 lib/Haskell/Prim/RealFrac.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Haskell/Prim/RealFrac.agda b/lib/Haskell/Prim/RealFrac.agda
index 6a71b37c..2e034f1d 100644
--- a/lib/Haskell/Prim/RealFrac.agda
+++ b/lib/Haskell/Prim/RealFrac.agda
@@ -15,7 +15,7 @@ instance
   iNegativeRealFrac .fromNeg n = negNat n
 
 postulate
-  properFraction : RealFrac → -- todo (Int, )
+  properFraction : RealFrac → -- todo (Int, Realfrac)
   truncate       : RealFrac → Int
   round          : RealFrac → Int
   ceiling        : RealFrac → Int

From 48133b963c0f0df792163342e9eae3027028daed Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Mon, 22 Jul 2024 22:27:07 +0200
Subject: [PATCH 5/9] Rework draft, using typeclasses

---
 lib/Haskell/Prelude.agda         |  7 +++
 lib/Haskell/Prim/Floating.agda   | 73 +++++++++++---------------------
 lib/Haskell/Prim/Fractional.agda | 42 ++++++------------
 lib/Haskell/Prim/Integral.agda   | 71 +++++++++++++++++++------------
 lib/Haskell/Prim/Rational.agda   | 21 +++++++++
 lib/Haskell/Prim/Real.agda       | 41 ++++++++++++------
 lib/Haskell/Prim/RealFloat.agda  | 63 +++++++++------------------
 lib/Haskell/Prim/RealFrac.agda   | 41 +++++-------------
 8 files changed, 168 insertions(+), 191 deletions(-)
 create mode 100644 lib/Haskell/Prim/Rational.agda

diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda
index 70b6d560..f84875c1 100644
--- a/lib/Haskell/Prelude.agda
+++ b/lib/Haskell/Prelude.agda
@@ -25,10 +25,13 @@ 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
@@ -36,6 +39,10 @@ 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
diff --git a/lib/Haskell/Prim/Floating.agda b/lib/Haskell/Prim/Floating.agda
index 7817eaef..9c1dfdc8 100644
--- a/lib/Haskell/Prim/Floating.agda
+++ b/lib/Haskell/Prim/Floating.agda
@@ -2,56 +2,31 @@ module Haskell.Prim.Floating where
 
 open import Haskell.Prim
 
-
 --------------------------------------------------
--- Literals
-
-
-instance
-  iNumberFloating : Number Floating
-  iNumberFloating .Number.Constraint _ = ⊤
-  iNumberFloating .fromNat n = pos n
+-- Floating
 
-  iNegativeFloating : Negative Floating
-  iNegativeFloating .Negative.Constraint _ = ⊤
-  iNegativeFloating .fromNeg n = negNat n
-
-
-postulate
-  pi      : Floating
-  exp     : Floating → Floating
-  log     : Floating → Floating
-  sqrt	  : Floating → Floating
+record Floating (a : Set) : Set where
   infixr 8 _**_
-  _**_    : Floating → Floating → Floating
-  logBase : Floating → Floating → Floating
-  sin     : Floating → Floating
-  cos     : Floating → Floating
-  asin    : Floating → Floating
-  acos    : Floating → Floating
-  atan    : Floating → Floating
-  sinh    : Floating → Floating
-  cosh    : Floating → Floating
-  asinh   : Floating → Floating
-  acosh   : Floating → Floating
-  atanh   : Floating → Floating
-  log1p   : Floating → Floating
-  expm1   : Floating → Floating
-  log1pexp: Floating → Floating
-  log1mexp: Floating → Floating
-
---------------------------------------------------
--- Arithmetic
-
-
---------------------------------------------------
--- Constraints
-
-isNegativeFloating : Floating → Bool
-isNegativeFloating (pos _)    = False
-isNegativeFloating (negsuc _) = True
+  field
+	pi      : a
+	exp     : a → a
+	log     : a → a
+	sqrt	: a → a
+	_**_    : Floating → Floating → Floating
+	logBase : Floating → Floating → Floating
+	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 #-}
 
-IsNonNegativeFloating : Floating → Set
-IsNonNegativeFloating (pos _)      = ⊤
-IsNonNegativeFloating n@(negsuc _) =
-  TypeError (primStringAppend (primShowFloating n) (" is negative"))
\ No newline at end of file
diff --git a/lib/Haskell/Prim/Fractional.agda b/lib/Haskell/Prim/Fractional.agda
index 136924e0..09d18946 100644
--- a/lib/Haskell/Prim/Fractional.agda
+++ b/lib/Haskell/Prim/Fractional.agda
@@ -1,37 +1,21 @@
+{-# OPTIONS --no-auto-inline #-}
+
 module Haskell.Prim.Fractional where
 
 open import Haskell.Prim
+open import Haskell.Floating
+open import Haskell.Prim.RealFrac
 
 --------------------------------------------------
--- Definition
-
-data Fractional : Set where
-
---------------------------------------------------
--- Literals
-
-instance
-  iNumberFractional : Number Fractional
-  iNumberFractional .Number.Constraint _ = ⊤
-  iNumberFractional .fromNat n = pos n
-
-  iNegativeFractional : Negative Fractional
-  iNegativeFractional .Negative.Constraint _ = ⊤
-  iNegativeFractional .fromNeg n = 
-  
---------------------------------------------------
--- Arithmetic
-
+-- Fractional
 
+record Fractional (a : Set) : Set where
+  infixl 7 _/_
+  field
+    _/_ : a → a → a
+    recip : a → a
+    fromRational : Rational → a
+open Fractional ⦃... ⦄  public
 
---------------------------------------------------
--- Constraints
-
-isNegativeFractional : Fractional → Bool
-isNegativeFractional (pos _)    = False
-isNegativeFractional (negsuc _) = True
+{-# COMPILE AGDA2HS Fractional existing-class #-}
 
-IsNonNegativeFractional : Fractional → Set
-IsNonNegativeFractional (pos _)      = ⊤
-IsNonNegativeFractional n@(negsuc _) =
-  TypeError (primStringAppend (primShowFractional n) (" is negative"))
\ No newline at end of file
diff --git a/lib/Haskell/Prim/Integral.agda b/lib/Haskell/Prim/Integral.agda
index b6216728..a7aeb9b0 100644
--- a/lib/Haskell/Prim/Integral.agda
+++ b/lib/Haskell/Prim/Integral.agda
@@ -1,36 +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
 
 --------------------------------------------------
--- Definition
-
-data Integral : Set where
-
---------------------------------------------------
--- Literals
+-- 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
-  iNumberIntegral : Number Integral
-  iNumberIntegral .Number.Constraint _ = ⊤
-  iNumberIntegral .fromNat n = pos n
-
-  iNegativeIntegral : Negative Integral
-  iNegativeIntegral .Negative.Constraint _ = ⊤
-  iNegativeIntegral .fromNeg n =
+  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
   
---------------------------------------------------
--- Arithmetic
-
---------------------------------------------------
--- Constraints
-
-isNegativeIntegral : Integral → Bool
-isNegativeIntegral (pos _)    = False
-isNegativeIntegral (negsuc _) = True
-
-IsNonNegativeIntegral : Integral → Set
-IsNonNegativeIntegral (pos _)      = ⊤
-IsNonNegativeIntegral n@(negsuc _) =
-  TypeError (primStringAppend (primShowIntegral n) (" is negative"))
\ No newline at end of file
+  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
diff --git a/lib/Haskell/Prim/Rational.agda b/lib/Haskell/Prim/Rational.agda
new file mode 100644
index 00000000..34d53238
--- /dev/null
+++ b/lib/Haskell/Prim/Rational.agda
@@ -0,0 +1,21 @@
+{-# OPTIONS --no-auto-inline #-}
+
+module Haskell.Prim.Rational where
+
+open import Haskell.Prim.Integer
+
+--------------------------------------------------
+-- Definition
+
+-- | Rational numbers, with numerator and denominator of some 'Integral' type.
+data Ratio (a : Set) : Set where
+  :% : a → a → Ratio a
+  numerator : Ratio a → a
+  denominator : Ratio a → a
+
+-- | Arbitrary-precision rational numbers, represented as a ratio of
+-- two 'Integer' values.  A rational number may be constructed using
+-- the '%' operator.
+Rational : Set
+Rational = Ratio Integer
+
diff --git a/lib/Haskell/Prim/Real.agda b/lib/Haskell/Prim/Real.agda
index c1ba7bdd..9adf3c8a 100644
--- a/lib/Haskell/Prim/Real.agda
+++ b/lib/Haskell/Prim/Real.agda
@@ -1,24 +1,37 @@
+{-# 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
 
 --------------------------------------------------
--- Definition
+-- Real
 
-data Real : Set where
+record Real (a : Set) : Set where
+  field
+    toRational : a → Rational
+open Real ⦃... ⦄  public
 
---------------------------------------------------
--- Literals
+{-# COMPILE AGDA2HS Real existing-class #-}
 
 instance
-  iNumberReal : Number Real
-  iNumberReal .Number.Constraint _ = ⊤
-  iNumberReal .fromNat n = pos n
-
-  iNegativeReal : Negative Real
-  iNegativeReal .Negative.Constraint _ = ⊤
-  iNegativeReal .fromNeg n =
+  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  
   
 --------------------------------------------------
 -- Arithmetic
@@ -27,11 +40,11 @@ instance
 --------------------------------------------------
 -- Constraints
 
-isNegativeReal : Real → Bool
+isNegativeReal : a → Bool
 isNegativeReal (pos _)    = False
 isNegativeReal (negsuc _) = True
 
-IsNonNegativeReal : Real → Set
+IsNonNegativeReal : a → Set
 IsNonNegativeReal (pos _)      = ⊤
 IsNonNegativeReal n@(negsuc _) =
-  TypeError (primStringAppend (primShowReal n) (" is negative"))
\ No newline at end of file
+  TypeError (primStringAppend (primShowReal n) (" is negative"))
diff --git a/lib/Haskell/Prim/RealFloat.agda b/lib/Haskell/Prim/RealFloat.agda
index 7b1ad21a..6e7f788d 100644
--- a/lib/Haskell/Prim/RealFloat.agda
+++ b/lib/Haskell/Prim/RealFloat.agda
@@ -5,46 +5,25 @@ open import Haskell.Prim.Int
 open import Haskell.Prim.Bool
 
 --------------------------------------------------
--- Literals
+-- 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 #-}
 
-instance
-  iNumberRealFloat : Number RealFloat
-  iNumberRealFloat .Number.Constraint _ = ⊤
-  iNumberRealFloat .fromNat n = pos n
-
-  iNegativeRealFloat : Negative RealFloat
-  iNegativeRealFloat .Negative.Constraint _ = ⊤
-  iNegativeRealFloat .fromNeg n = negNat n
-
--- The RealFloat typeclass functions
-postulate
-  floatRadix       : RealFloat → Int
-  floatDigits      : RealFloat → Int
-  floatRange       : RealFloat → -- todo (Int, Int)
-  decodeFloat      : RealFloat → -- todo (Int, Int)
-  encodeFloat      : Int → Int → RealFloat
-  exponent         : RealFloat → Int
-  significand      : RealFloat → Float
-  scaleFloat       : Int → RealFloat → RealFloat
-  isNaN            : RealFloat → Bool
-  isInfinite       : RealFloat → Bool
-  isDenormalized   : RealFloat → Bool
-  isNegativeZero   : RealFloat → Bool
-  isIEEE           : RealFloat → Bool
-  atan2			   : RealFloat → RealFloat → RealFloat
-  
---------------------------------------------------
--- Arithmetic
-
-
---------------------------------------------------
--- Constraints
-
-isNegativeRealFloat : RealFloat → Bool
-isNegativeRealFloat (pos _)    = False
-isNegativeRealFloat (negsuc _) = True
-
-IsNonNegativeRealFloat : RealFloat → Set
-IsNonNegativeRealFloat (pos _)      = ⊤
-IsNonNegativeRealFloat n@(negsuc _) =
-  TypeError (primStringAppend (primShowRealFloat n) (" is negative"))
\ No newline at end of file
diff --git a/lib/Haskell/Prim/RealFrac.agda b/lib/Haskell/Prim/RealFrac.agda
index 2e034f1d..02c11323 100644
--- a/lib/Haskell/Prim/RealFrac.agda
+++ b/lib/Haskell/Prim/RealFrac.agda
@@ -1,38 +1,19 @@
 module Haskell.Prim.RealFrac where
 
 open import Haskell.Prim
+open import Haskell.Prim.Integral
 
 --------------------------------------------------
--- Literals
+-- RealFrac
 
-instance
-  iNumberRealFrac : Number RealFrac
-  iNumberRealFrac .Number.Constraint _ = ⊤
-  iNumberRealFrac .fromNat n = pos n
+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
 
-  iNegativeRealFrac : Negative RealFrac
-  iNegativeRealFrac .Negative.Constraint _ = ⊤
-  iNegativeRealFrac .fromNeg n = negNat n
+{-# COMPILE AGDA2HS RealFrac existing-class #-}
 
-postulate
-  properFraction : RealFrac → -- todo (Int, Realfrac)
-  truncate       : RealFrac → Int
-  round          : RealFrac → Int
-  ceiling        : RealFrac → Int
-  floor          : RealFrac → Int
-
---------------------------------------------------
--- Arithmetic
-
-
---------------------------------------------------
--- Constraints
-
-isNegativeRealFrac : RealFrac → Bool
-isNegativeRealFrac (pos _)    = False
-isNegativeRealFrac (negsuc _) = True
-
-IsNonNegativeRealFrac : Real → Set
-IsNonNegativeRealFrac (pos _)      = ⊤
-IsNonNegativeRealFrac n@(negsuc _) =
-  TypeError (primStringAppend (primShowRealFrac n) (" is negative"))
\ No newline at end of file

From c33dd78e15808630a61508c8b076d14bac669815 Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Mon, 22 Jul 2024 22:29:28 +0200
Subject: [PATCH 6/9] Removed unused code in Real.agda

---
 lib/Haskell/Prim/Real.agda | 15 ---------------
 1 file changed, 15 deletions(-)

diff --git a/lib/Haskell/Prim/Real.agda b/lib/Haskell/Prim/Real.agda
index 9adf3c8a..4955105b 100644
--- a/lib/Haskell/Prim/Real.agda
+++ b/lib/Haskell/Prim/Real.agda
@@ -32,19 +32,4 @@ instance
   
   iRealWord : Real Word
   iRealWord.toRational x = toInteger x :% 1  
-  
---------------------------------------------------
--- Arithmetic
-
-
---------------------------------------------------
--- Constraints
-
-isNegativeReal : a → Bool
-isNegativeReal (pos _)    = False
-isNegativeReal (negsuc _) = True
 
-IsNonNegativeReal : a → Set
-IsNonNegativeReal (pos _)      = ⊤
-IsNonNegativeReal n@(negsuc _) =
-  TypeError (primStringAppend (primShowReal n) (" is negative"))

From 32adcaeaa054c31527989e6debd5cc41aa3b96e1 Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Mon, 22 Jul 2024 23:08:00 +0200
Subject: [PATCH 7/9] Some corrections

---
 lib/Haskell/Prim/Floating.agda  | 4 ++--
 lib/Haskell/Prim/RealFloat.agda | 5 +++--
 lib/Haskell/Prim/RealFrac.agda  | 3 ++-
 3 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/lib/Haskell/Prim/Floating.agda b/lib/Haskell/Prim/Floating.agda
index 9c1dfdc8..24fbceb3 100644
--- a/lib/Haskell/Prim/Floating.agda
+++ b/lib/Haskell/Prim/Floating.agda
@@ -12,8 +12,8 @@ record Floating (a : Set) : Set where
 	exp     : a → a
 	log     : a → a
 	sqrt	: a → a
-	_**_    : Floating → Floating → Floating
-	logBase : Floating → Floating → Floating
+	_**_    : a → a → a
+	logBase : a → a → a
 	sin     : a → a
 	cos     : a → a
 	tan		: a → a
diff --git a/lib/Haskell/Prim/RealFloat.agda b/lib/Haskell/Prim/RealFloat.agda
index 6e7f788d..1078b863 100644
--- a/lib/Haskell/Prim/RealFloat.agda
+++ b/lib/Haskell/Prim/RealFloat.agda
@@ -2,6 +2,7 @@ module Haskell.Prim.RealFloat where
 
 open import Haskell.Prim
 open import Haskell.Prim.Int
+open import Haskell.Prim.Integer
 open import Haskell.Prim.Bool
 
 --------------------------------------------------
@@ -11,8 +12,8 @@ record RealFloat (a : Set) : Set where
   field
 	floatRadix       : a → Integer
 	floatDigits      : a → Int
-	floatRange       : a → (Int, Int)
-	decodeFloat      : a → (Integer, Int)
+	floatRange       : a → (Int × Int)
+	decodeFloat      : a → (Integer × Int)
 	encodeFloat      : Integer → Int → a
 	exponent         : a → Int
 	significand      : a → a
diff --git a/lib/Haskell/Prim/RealFrac.agda b/lib/Haskell/Prim/RealFrac.agda
index 02c11323..3be29426 100644
--- a/lib/Haskell/Prim/RealFrac.agda
+++ b/lib/Haskell/Prim/RealFrac.agda
@@ -1,6 +1,7 @@
 module Haskell.Prim.RealFrac where
 
 open import Haskell.Prim
+open import Haskell.Prim.Int
 open import Haskell.Prim.Integral
 
 --------------------------------------------------
@@ -8,7 +9,7 @@ open import Haskell.Prim.Integral
 
 record RealFrac (a : Set) : Set where
   field
-	properFraction : a → (Int, a)
+	properFraction : a → (Int × a)
 	truncate       : a → Integral
 	round          : a → Integral
 	ceiling        : a → Integral

From a1cedbd574a3be79428a960081b23351fe212655 Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Mon, 22 Jul 2024 23:13:56 +0200
Subject: [PATCH 8/9] Imports Haskell.Prim.Tuple

---
 lib/Haskell/Prim/RealFloat.agda | 29 +++++++++++++++--------------
 lib/Haskell/Prim/RealFrac.agda  | 11 ++++++-----
 2 files changed, 21 insertions(+), 19 deletions(-)

diff --git a/lib/Haskell/Prim/RealFloat.agda b/lib/Haskell/Prim/RealFloat.agda
index 1078b863..4543003a 100644
--- a/lib/Haskell/Prim/RealFloat.agda
+++ b/lib/Haskell/Prim/RealFloat.agda
@@ -4,26 +4,27 @@ 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
+    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 #-}
diff --git a/lib/Haskell/Prim/RealFrac.agda b/lib/Haskell/Prim/RealFrac.agda
index 3be29426..d6561953 100644
--- a/lib/Haskell/Prim/RealFrac.agda
+++ b/lib/Haskell/Prim/RealFrac.agda
@@ -3,17 +3,18 @@ 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
+    properFraction : a → (Int × a)
+    truncate       : a → Integral
+    round          : a → Integral
+    ceiling        : a → Integral
+    floor          : a → Integral
 open RealFrac ⦃... ⦄  public
 
 {-# COMPILE AGDA2HS RealFrac existing-class #-}

From 68c77f43a96496f519cbbbf23873b09d628840ed Mon Sep 17 00:00:00 2001
From: ndcroos <nick.decroos@gmail.com>
Date: Tue, 23 Jul 2024 11:06:30 +0200
Subject: [PATCH 9/9] Rework Ratio as record type and import Haskell.Prim

---
 lib/Haskell/Prim/Rational.agda | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/lib/Haskell/Prim/Rational.agda b/lib/Haskell/Prim/Rational.agda
index 34d53238..e7ab27f7 100644
--- a/lib/Haskell/Prim/Rational.agda
+++ b/lib/Haskell/Prim/Rational.agda
@@ -2,20 +2,22 @@
 
 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, with numerator and denominator of some 'Integral' type.
-data Ratio (a : Set) : Set where
-  :% : a → a → Ratio a
-  numerator : Ratio a → a
-  denominator : Ratio a → a
-
--- | Arbitrary-precision rational numbers, represented as a ratio of
--- two 'Integer' values.  A rational number may be constructed using
--- the '%' operator.
+-- Rational numbers, represented as a ratio of two 'Integer' values.
+-- A rational number may be constructed using the '%' operator.
 Rational : Set
 Rational = Ratio Integer