Remove special handling of tuple types in the prelude

agda · Jul 23, 2024 · 3ca7265 · 3ca7265
1 parent 44a82e2
commit 3ca7265
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 22 deletions.
diff --git a/lib/Haskell/Extra/Erase.agda b/lib/Haskell/Extra/Erase.agda
@@ -8,14 +8,15 @@ module Haskell.Extra.Erase where
   open import Haskell.Prim.List
   open import Haskell.Law.Equality
 
-  private variable 
+  private variable
     @0 x y : a
     @0 xs  : List a
 
   record Erase (@0 a : Set ℓ) : Set ℓ where
     constructor Erased
     field @0 get : a
   open Erase public
+  {-# COMPILE AGDA2HS Erase tuple #-}
 
   infixr 4 ⟨_⟩_
   record Σ0 (@0 a : Set) (b : @0 a → Set) : Set where

diff --git a/lib/Haskell/Extra/Sigma.agda b/lib/Haskell/Extra/Sigma.agda
@@ -6,6 +6,7 @@ record Σ (a : Set) (b : @0 a → Set) : Set where
     fst : a
     snd : b fst
 open Σ public
+{-# COMPILE AGDA2HS Σ tuple #-}
 
 infix 2 Σ-syntax
 

diff --git a/lib/Haskell/Law/Eq/Instances.agda b/lib/Haskell/Law/Eq/Instances.agda
@@ -25,6 +25,8 @@ open import Haskell.Law.List    using ( ∷-injective-left; ∷-injective-right
 open import Haskell.Law.Maybe
 open import Haskell.Law.Nat
 
+open _×_×_
+
 instance
   iLawfulEqNat : IsLawfulEq Nat
   iLawfulEqNat .isEquality zero    zero    = refl

diff --git a/lib/Haskell/Prim/Tuple.agda b/lib/Haskell/Prim/Tuple.agda
@@ -17,8 +17,17 @@ record _×_ (a b : Set) : Set where
     snd : b
 open _×_ public
 
-data _×_×_ (a b c : Set) : Set where
-  _,_,_ : a → b → c → a × b × c
+{-# COMPILE AGDA2HS _×_ tuple #-}
+
+record _×_×_ (a b c : Set) : Set where
+  no-eta-equality; pattern
+  constructor _,_,_
+  field
+    fst3 : a
+    snd3 : b
+    thd3 : c
+
+{-# COMPILE AGDA2HS _×_×_ tuple #-}
 
 uncurry : (a → b → c) → a × b → c
 uncurry f (x , y) = f x y
@@ -34,12 +43,3 @@ second f (x , y) = x , f y
 
 _***_ : (a → b) → (c → d) → a × c → b × d
 (f *** g) (x , y) = f x , g y
-
-fst₃ : (a × b × c) → a
-fst₃ (x , _ , _) = x 
-
-snd₃ : (a × b × c) → b
-snd₃ (_ , y , _) = y
-
-thd₃ : (a × b × c) → c
-thd₃ (_ , _ , z) = z
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
@@ -53,10 +53,6 @@ import Agda2Hs.HsUtils
 isSpecialCon :: QName -> Maybe (Type -> NAPs -> C (Hs.Pat ()))
 isSpecialCon qn = case prettyShow qn of
   s | s `elem` badConstructors     -> Just itsBad
-  "Haskell.Prim.Tuple._,_"         -> Just tuplePat
-  "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tuplePat
-  "Haskell.Extra.Erase.Erased"     -> Just tuplePat
-  "Haskell.Extra.Sigma._,_"        -> Just tuplePat
   "Agda.Builtin.Int.Int.pos"       -> Just posIntPat
   "Agda.Builtin.Int.Int.negsuc"    -> Just negSucIntPat
   _                                -> Nothing
@@ -71,12 +67,6 @@ isSpecialCon qn = case prettyShow qn of
     itsBad :: Type -> NAPs -> C (Hs.Pat ())
     itsBad _ _ = genericDocError =<< "constructor `" <> prettyTCM qn <> "` not supported in patterns"
 
--- | Translate list of patterns into a Haskell n-uple pattern.
-tuplePat :: Type -> NAPs -> C (Hs.Pat ())
-tuplePat ty ps =
-  compilePats ty ps
-  <&> Hs.PTuple () Hs.Boxed
-
 -- | Translate Int.pos pattern.
 posIntPat :: Type -> NAPs -> C (Hs.Pat ())
 posIntPat ty [p] = do