From cc790505c5c8d57a4096f8309d5ad1255b512932 Mon Sep 17 00:00:00 2001 From: flupe Date: Mon, 4 Dec 2023 19:06:27 +0100 Subject: [PATCH] simplify tuples --- lib/Haskell/Law/Applicative/Def.agda | 4 ---- lib/Haskell/Law/Eq/Def.agda | 8 +++++-- lib/Haskell/Law/Functor/Def.agda | 3 --- lib/Haskell/Law/Monad/Def.agda | 4 ---- lib/Haskell/Law/Monoid/Def.agda | 10 ++++---- lib/Haskell/Law/Ord/Def.agda | 10 ++++++-- lib/Haskell/Law/Semigroup/Def.agda | 10 ++++---- lib/Haskell/Prim/Applicative.agda | 11 ++------- lib/Haskell/Prim/Bounded.agda | 28 +++++++++++++++------- lib/Haskell/Prim/Eq.agda | 8 +++---- lib/Haskell/Prim/Functor.agda | 9 +++---- lib/Haskell/Prim/Monad.agda | 10 ++------ lib/Haskell/Prim/Monoid.agda | 17 +++++++------- lib/Haskell/Prim/Ord.agda | 13 +++++++---- lib/Haskell/Prim/Show.agda | 17 +++++++------- lib/Haskell/Prim/Tuple.agda | 35 +++++++--------------------- src/Agda2Hs/Compile/Function.hs | 11 ++------- src/Agda2Hs/Compile/Term.hs | 12 +++------- src/Agda2Hs/Compile/Type.hs | 23 ++---------------- test/Fail/TuplePat.agda | 9 ------- test/Fail/TupleTerm.agda | 9 ------- test/Fail/TupleType.agda | 9 ------- test/Tuples.agda | 15 ++++++++---- test/golden/TuplePat.err | 2 -- test/golden/TupleTerm.err | 2 -- test/golden/TupleType.err | 2 -- test/golden/Tuples.hs | 9 ++++--- 27 files changed, 114 insertions(+), 186 deletions(-) delete mode 100644 test/Fail/TuplePat.agda delete mode 100644 test/Fail/TupleTerm.agda delete mode 100644 test/Fail/TupleType.agda delete mode 100644 test/golden/TuplePat.err delete mode 100644 test/golden/TupleTerm.err delete mode 100644 test/golden/TupleType.err diff --git a/lib/Haskell/Law/Applicative/Def.agda b/lib/Haskell/Law/Applicative/Def.agda index e1a4b162..9c93b9c0 100644 --- a/lib/Haskell/Law/Applicative/Def.agda +++ b/lib/Haskell/Law/Applicative/Def.agda @@ -39,7 +39,3 @@ instance postulate iLawfulApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_) iLawfulApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_) - - iLawfulApplicativeTuple₄ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → - Applicative (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ [])) - diff --git a/lib/Haskell/Law/Eq/Def.agda b/lib/Haskell/Law/Eq/Def.agda index 022712ca..f0876ca0 100644 --- a/lib/Haskell/Law/Eq/Def.agda +++ b/lib/Haskell/Law/Eq/Def.agda @@ -85,9 +85,13 @@ postulate instance iLawfulEqUnit : IsLawfulEq ⊤ - iLawfulEqTuple₀ : IsLawfulEq (Tuple []) + iLawfulEqTuple₂ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄ + → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ + → IsLawfulEq (a × b) - iLawfulEqTuple : ⦃ iEqA : Eq a ⦄ → ⦃ iEqAs : Eq (Tuple as) ⦄ → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq (Tuple as) ⦄ → IsLawfulEq (Tuple (a ∷ as)) + iLawfulEqTuple₃ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄ ⦃ iEqC : Eq c ⦄ + → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ → ⦃ IsLawfulEq c ⦄ + → IsLawfulEq (a × b × c) iLawfulEqList : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄ → IsLawfulEq (List a) diff --git a/lib/Haskell/Law/Functor/Def.agda b/lib/Haskell/Law/Functor/Def.agda index 173a6a57..6ba05fb8 100644 --- a/lib/Haskell/Law/Functor/Def.agda +++ b/lib/Haskell/Law/Functor/Def.agda @@ -22,6 +22,3 @@ instance postulate iLawfulFunctorTuple₂ : IsLawfulFunctor (a ×_) iLawfulFunctorTuple₃ : IsLawfulFunctor (a × b ×_) - - iLawfulFunctorTuple₄ : IsLawfulFunctor (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ [])) - diff --git a/lib/Haskell/Law/Monad/Def.agda b/lib/Haskell/Law/Monad/Def.agda index a7424816..4f939dbf 100644 --- a/lib/Haskell/Law/Monad/Def.agda +++ b/lib/Haskell/Law/Monad/Def.agda @@ -44,7 +44,3 @@ instance postulate iLawfulMonadTuple₂ : ⦃ Monoid a ⦄ → Monad (a ×_) iLawfulMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_) - - iLawfulMonadTuple₄ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → - Monad (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ [])) - diff --git a/lib/Haskell/Law/Monoid/Def.agda b/lib/Haskell/Law/Monoid/Def.agda index 4e617944..75383919 100644 --- a/lib/Haskell/Law/Monoid/Def.agda +++ b/lib/Haskell/Law/Monoid/Def.agda @@ -28,9 +28,11 @@ postulate instance iLawfulMonoidUnit : IsLawfulMonoid ⊤ - iLawfulMonoidTuple₀ : IsLawfulMonoid (Tuple []) + iLawfulMonoidTuple₂ : ⦃ iSemA : Monoid a ⦄ ⦃ iSemB : Monoid b ⦄ + → ⦃ IsLawfulMonoid a ⦄ → ⦃ IsLawfulMonoid b ⦄ + → IsLawfulMonoid (a × b) - iLawfulMonoidTuple : ⦃ iSemA : Monoid a ⦄ → ⦃ iSemA : Monoid (Tuple as) ⦄ - → ⦃ IsLawfulMonoid a ⦄ → ⦃ IsLawfulMonoid (Tuple as) ⦄ - → IsLawfulMonoid (Tuple (a ∷ as)) + iLawfulMonoidTuple₃ : ⦃ iSemA : Monoid a ⦄ ⦃ iSemB : Monoid b ⦄ ⦃ iSemC : Monoid c ⦄ + → ⦃ IsLawfulMonoid a ⦄ → ⦃ IsLawfulMonoid b ⦄ → ⦃ IsLawfulMonoid c ⦄ + → IsLawfulMonoid (a × b × c) diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda index cd6fd294..4da9149a 100644 --- a/lib/Haskell/Law/Ord/Def.agda +++ b/lib/Haskell/Law/Ord/Def.agda @@ -162,9 +162,15 @@ postulate instance iLawfulOrdChar : IsLawfulOrd Char - iLawfulOrdTuple₀ : IsLawfulOrd (Tuple []) + iLawfulOrdUnit : IsLawfulOrd ⊤ - iLawfulOrdTuple : ⦃ iOrdA : Ord a ⦄ → ⦃ iLawfulOrdA : Ord (Tuple as) ⦄ → ⦃ IsLawfulOrd a ⦄ → ⦃ IsLawfulOrd (Tuple as) ⦄ → IsLawfulOrd (Tuple (a ∷ as)) + iLawfulOrdTuple₂ : ⦃ iOrdA : Ord a ⦄ ⦃ iOrdB : Ord b ⦄ + → ⦃ IsLawfulOrd a ⦄ → ⦃ IsLawfulOrd b ⦄ + → IsLawfulOrd (a × b) + + iLawfulOrdTuple₃ : ⦃ iOrdA : Ord a ⦄ ⦃ iOrdB : Ord b ⦄ ⦃ iOrdC : Ord c ⦄ + → ⦃ IsLawfulOrd a ⦄ → ⦃ IsLawfulOrd b ⦄ → ⦃ IsLawfulOrd c ⦄ + → IsLawfulOrd (a × b × c) iLawfulOrdList : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → IsLawfulOrd (List a) diff --git a/lib/Haskell/Law/Semigroup/Def.agda b/lib/Haskell/Law/Semigroup/Def.agda index 769f33e9..ea91ead3 100644 --- a/lib/Haskell/Law/Semigroup/Def.agda +++ b/lib/Haskell/Law/Semigroup/Def.agda @@ -17,9 +17,11 @@ postulate instance iLawfulSemigroupUnit : IsLawfulSemigroup ⊤ - iLawfulSemigroupTuple₀ : IsLawfulSemigroup (Tuple []) + iLawfulSemigroupTuple₂ : ⦃ iSemA : Semigroup a ⦄ ⦃ iSemB : Semigroup b ⦄ + → ⦃ IsLawfulSemigroup a ⦄ → ⦃ IsLawfulSemigroup b ⦄ + → IsLawfulSemigroup (a × b) - iLawfulSemigroupTuple : ⦃ iSemA : Semigroup a ⦄ → ⦃ iSemA : Semigroup (Tuple as) ⦄ - → ⦃ IsLawfulSemigroup a ⦄ → ⦃ IsLawfulSemigroup (Tuple as) ⦄ - → IsLawfulSemigroup (Tuple (a ∷ as)) + iLawfulSemigroupTuple₃ : ⦃ iSemA : Semigroup a ⦄ ⦃ iSemB : Semigroup b ⦄ ⦃ iSemC : Semigroup c ⦄ + → ⦃ IsLawfulSemigroup a ⦄ → ⦃ IsLawfulSemigroup b ⦄ → ⦃ IsLawfulSemigroup c ⦄ + → IsLawfulSemigroup (a × b × c) diff --git a/lib/Haskell/Prim/Applicative.agda b/lib/Haskell/Prim/Applicative.agda index ff5aa275..e34dd75a 100644 --- a/lib/Haskell/Prim/Applicative.agda +++ b/lib/Haskell/Prim/Applicative.agda @@ -77,14 +77,7 @@ instance iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_) iApplicativeTuple₃ = mkApplicative λ where - .pure x → mempty , mempty , x - ._<*>_ (a , b , f) (a₁ , b₁ , x) → a <> a₁ , b <> b₁ , f x - - iApplicativeTuple₄ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → - Applicative (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ [])) - iApplicativeTuple₄ = mkApplicative λ where - .pure x → mempty ; mempty ; mempty ; x ; tt - ._<*>_ (a ; b ; c ; f ; tt) (a₁ ; b₁ ; c₁ ; x ; tt) → - a <> a₁ ; b <> b₁ ; c <> c₁ ; f x ; tt + .pure x → mempty , mempty , x + ._<*>_ (a , u , f) (b , v , x) → a <> b , u <> v , f x instance postulate iApplicativeIO : Applicative IO diff --git a/lib/Haskell/Prim/Bounded.agda b/lib/Haskell/Prim/Bounded.agda index 9c76a51a..402dbfea 100644 --- a/lib/Haskell/Prim/Bounded.agda +++ b/lib/Haskell/Prim/Bounded.agda @@ -59,15 +59,25 @@ instance iBoundedAboveChar : BoundedAbove Char iBoundedAboveChar .maxBound = '\1114111' - iBoundedBelowTuple₀ : BoundedBelow (Tuple []) - iBoundedBelowTuple₀ .minBound = tt - iBoundedAboveTuple₀ : BoundedAbove (Tuple []) - iBoundedAboveTuple₀ .maxBound = tt - - iBoundedBelowTuple : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow (Tuple as) ⦄ → BoundedBelow (Tuple (a ∷ as)) - iBoundedBelowTuple .minBound = minBound ; minBound - iBoundedAboveTuple : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove (Tuple as) ⦄ → BoundedAbove (Tuple (a ∷ as)) - iBoundedAboveTuple .maxBound = maxBound ; maxBound + iBoundedBelowUnit : BoundedBelow ⊤ + iBoundedBelowUnit .minBound = tt + + iBoundedAboveUnit : BoundedAbove ⊤ + iBoundedAboveUnit .maxBound = tt + + iBoundedBelowTuple₂ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄ + → BoundedBelow (a × b) + iBoundedBelowTuple₂ .minBound = minBound , minBound + iBoundedAboveTuple₂ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄ + → BoundedAbove (a × b) + iBoundedAboveTuple₂ .maxBound = maxBound , maxBound + + iBoundedBelowTuple₃ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄ → ⦃ BoundedBelow c ⦄ + → BoundedBelow (a × b × c) + iBoundedBelowTuple₃ .minBound = minBound , minBound , minBound + iBoundedAboveTuple₃ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄ → ⦃ BoundedAbove c ⦄ + → BoundedAbove (a × b × c) + iBoundedAboveTuple₃ .maxBound = maxBound , maxBound , maxBound iBoundedBelowOrdering : BoundedBelow Ordering iBoundedBelowOrdering .minBound = LT diff --git a/lib/Haskell/Prim/Eq.agda b/lib/Haskell/Prim/Eq.agda index 3dd3d99b..b17820ed 100644 --- a/lib/Haskell/Prim/Eq.agda +++ b/lib/Haskell/Prim/Eq.agda @@ -53,11 +53,11 @@ instance iEqUnit : Eq ⊤ iEqUnit ._==_ _ _ = True - iEqTuple₀ : Eq (Tuple []) - iEqTuple₀ ._==_ _ _ = True + iEqTuple₂ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (a × b) + iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₂ == y₂ - iEqTuple : ⦃ Eq a ⦄ → ⦃ Eq (Tuple as) ⦄ → Eq (Tuple (a ∷ as)) - iEqTuple ._==_ (x ; xs) (y ; ys) = x == y && xs == ys + iEqTuple₃ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → ⦃ Eq c ⦄ → Eq (a × b × c) + iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₂ == y₂ && z₁ == z₂ iEqList : ⦃ Eq a ⦄ → Eq (List a) iEqList {a} ._==_ = eqList diff --git a/lib/Haskell/Prim/Functor.agda b/lib/Haskell/Prim/Functor.agda index 28c90447..967ddd50 100644 --- a/lib/Haskell/Prim/Functor.agda +++ b/lib/Haskell/Prim/Functor.agda @@ -21,7 +21,7 @@ record Functor (f : Set → Set) : Set₁ where _<&>_ : f a → (a → b) → f b _<$_ : (@0 {{ b }} → a) → f b → f a _$>_ : f a → (@0 {{ a }} → b) → f b - void : f a → f (Tuple []) + void : f a → f ⊤ -- ** defaults record DefaultFunctor (f : Set → Set) : Set₁ where field fmap : (a → b) → f a → f b @@ -41,7 +41,7 @@ record DefaultFunctor (f : Set → Set) : Set₁ where _$>_ : f a → (@0 {{ a }} → b) → f b m $> x = x <$ m - void : f a → f (Tuple []) + void : f a → f ⊤ void = tt <$_ -- ** export open Functor ⦃...⦄ public @@ -74,9 +74,6 @@ instance iFunctorTuple₂ = fmap= λ f (x , y) → x , f y iFunctorTuple₃ : Functor (a × b ×_) - iFunctorTuple₃ = fmap= λ f (x , y , z) → x , y , f z - - iFunctorTuple₄ : Functor (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ [])) - iFunctorTuple₄ = fmap= λ f (x ; y ; z ; w ; tt) → x ; y ; z ; f w ; tt + iFunctorTuple₃ = fmap= λ where f (x , y , z) → x , y , f z instance postulate iFunctiorIO : Functor IO diff --git a/lib/Haskell/Prim/Monad.agda b/lib/Haskell/Prim/Monad.agda index f3d2d786..2b6e3c05 100644 --- a/lib/Haskell/Prim/Monad.agda +++ b/lib/Haskell/Prim/Monad.agda @@ -88,16 +88,10 @@ instance iMonadTuple₂ = bind= λ (a , x) k → first (a <>_) (k x) iMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_) - iMonadTuple₃ = bind= λ (a , b , x) k → - case k x of λ where + iMonadTuple₃ = bind= λ where + (a , b , x) k → case k x of λ where (a₁ , b₁ , y) → a <> a₁ , b <> b₁ , y - iMonadTuple₄ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → - Monad (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ [])) - iMonadTuple₄ = bind= λ (a ; b ; c ; x ; tt) k → - case k x of λ where - (a₁ ; b₁ ; c₁ ; y ; tt) → a <> a₁ ; b <> b₁ ; c <> c₁ ; y ; tt - instance postulate iMonadIO : Monad IO record MonadFail (m : Set → Set) : Set₁ where diff --git a/lib/Haskell/Prim/Monoid.agda b/lib/Haskell/Prim/Monoid.agda index a11430fb..09e71b3a 100644 --- a/lib/Haskell/Prim/Monoid.agda +++ b/lib/Haskell/Prim/Monoid.agda @@ -36,11 +36,12 @@ instance iSemigroupUnit : Semigroup ⊤ iSemigroupUnit ._<>_ _ _ = tt - iSemigroupTuple₀ : Semigroup (Tuple []) - iSemigroupTuple₀ ._<>_ _ _ = tt - iSemigroupTuple : ⦃ Semigroup a ⦄ → ⦃ Semigroup (Tuple as) ⦄ → Semigroup (Tuple (a ∷ as)) - iSemigroupTuple ._<>_ (x ; xs) (y ; ys) = x <> y ; xs <> ys + iSemigroupTuple₂ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → Semigroup (a × b) + iSemigroupTuple₂ ._<>_ (x₁ , y₁) (x₂ , y₂) = x₁ <> x₂ , y₁ <> y₂ + + iSemigroupTuple₃ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → ⦃ Semigroup c ⦄ → Semigroup (a × b × c) + iSemigroupTuple₃ ._<>_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ <> x₂ , y₁ <> y₂ , z₁ <> z₂ -------------------------------------------------- @@ -89,11 +90,11 @@ instance iMonoidUnit : Monoid ⊤ iMonoidUnit = mempty= tt - iMonoidTuple₀ : Monoid (Tuple []) - iMonoidTuple₀ = mempty= tt + iMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monoid (a × b) + iMonoidTuple₂ = mempty= (mempty , mempty) - iMonoidTuple : ⦃ Monoid a ⦄ → ⦃ Monoid (Tuple as) ⦄ → Monoid (Tuple (a ∷ as)) - iMonoidTuple = mempty= mempty ; mempty + iMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → Monoid (a × b × c) + iMonoidTuple₃ = mempty= (mempty , mempty , mempty) open DefaultMonoid diff --git a/lib/Haskell/Prim/Ord.agda b/lib/Haskell/Prim/Ord.agda index 6118b8bb..b6982ef8 100644 --- a/lib/Haskell/Prim/Ord.agda +++ b/lib/Haskell/Prim/Ord.agda @@ -125,11 +125,16 @@ instance True False → GT _ _ → EQ - iOrdTuple₀ : Ord (Tuple []) - iOrdTuple₀ = ordFromCompare λ _ _ → EQ + iOrdUnit : Ord ⊤ + iOrdUnit = ordFromCompare λ _ _ → EQ - iOrdTuple : ⦃ Ord a ⦄ → ⦃ Ord (Tuple as) ⦄ → Ord (Tuple (a ∷ as)) - iOrdTuple = ordFromCompare λ where (x ; xs) (y ; ys) → compare x y <> compare xs ys + iOrdTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (a × b) + iOrdTuple₂ = ordFromCompare λ where + (x₁ , y₁) (x₂ , y₂) → compare x₁ x₂ <> compare y₁ y₂ + + iOrdTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → Ord (a × b × c) + iOrdTuple₃ = ordFromCompare λ where + (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) → compare x₁ x₂ <> compare y₁ y₂ <> compare z₁ z₂ compareList : ⦃ Ord a ⦄ → List a → List a → Ordering compareList [] [] = EQ diff --git a/lib/Haskell/Prim/Show.agda b/lib/Haskell/Prim/Show.agda index 466d43f4..1d8a8c69 100644 --- a/lib/Haskell/Prim/Show.agda +++ b/lib/Haskell/Prim/Show.agda @@ -117,13 +117,12 @@ instance iShowEither = showsPrec= λ where p (Left x) → showApp₁ p "Left" x p (Right y) → showApp₁ p "Right" y -private - -- Minus the parens - showTuple : ⦃ All Show as ⦄ → Tuple as → ShowS - showTuple ⦃ allNil ⦄ _ = showString "" - showTuple ⦃ allCons ⦃ is = allNil ⦄ ⦄ (x ; tt) = shows x - showTuple ⦃ allCons ⦄ (x ; xs) = shows x - ∘ showString ", " ∘ showTuple xs + instance - iShowTuple : ⦃ All Show as ⦄ → Show (Tuple as) - iShowTuple = showsPrec= λ _ → showParen True ∘ showTuple + iShowTuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (a × b) + iShowTuple₂ = showsPrec= λ _ → λ where + (x , y) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ")" + + iShowTuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show (a × b × c) + iShowTuple₃ = showsPrec= λ _ → λ where + (x , y , z) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ", " ∘ shows z ∘ showString ")" diff --git a/lib/Haskell/Prim/Tuple.agda b/lib/Haskell/Prim/Tuple.agda index a2e73bac..71bb8624 100644 --- a/lib/Haskell/Prim/Tuple.agda +++ b/lib/Haskell/Prim/Tuple.agda @@ -3,33 +3,22 @@ module Haskell.Prim.Tuple where open import Haskell.Prim -variable - as : List Set - -------------------------------------------------- -- Tuples -infixr 5 _;_ -record Pair (A B : Set) : Set where - constructor _;_ - field fst : A ; snd : B - -Tuple : List Set → Set -Tuple [] = ⊤ -Tuple (A ∷ AS) = Pair A (Tuple AS) - infix 3 _×_ _×_×_ -_×_ : (a b : Set) → Set -a × b = Tuple (a ∷ b ∷ []) - -_×_×_ : (a b c : Set) → Set -a × b × c = Tuple (a ∷ b ∷ c ∷ []) - infix -1 _,_ _,_,_ -pattern _,_ x y = x ; y ; tt -pattern _,_,_ x y z = x ; y ; z ; tt +record _×_ (a b : Set) : Set where + constructor _,_ + field + fst : a + snd : b +open _×_ public + +data _×_×_ (a b c : Set) : Set where + _,_,_ : a → b → c → a × b × c uncurry : (a → b → c) → a × b → c uncurry f (x , y) = f x y @@ -37,12 +26,6 @@ uncurry f (x , y) = f x y curry : (a × b → c) → a → b → c curry f x y = f (x , y) -fst : a × b → a -fst (x , _) = x - -snd : a × b → b -snd (_ , y) = y - first : (a → b) → a × c → b × c first f (x , y) = f x , y diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs index 43caf157..752a2e87 100644 --- a/src/Agda2Hs/Compile/Function.hs +++ b/src/Agda2Hs/Compile/Function.hs @@ -44,7 +44,7 @@ import Agda.TypeChecking.Datatypes (isDataOrRecord) isSpecialPat :: QName -> Maybe (ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ())) isSpecialPat qn = case prettyShow qn of - "Haskell.Prim.Tuple._;_" -> Just tuplePat + "Haskell.Prim.Tuple._,_" -> Just tuplePat "Agda.Builtin.Int.Int.pos" -> Just posIntPat "Agda.Builtin.Int.Int.negsuc" -> Just negSucIntPat s | s `elem` badConstructors -> Just $ \ _ _ _ -> genericDocError =<< @@ -61,14 +61,7 @@ isUnboxCopattern (ProjP _ q) = isJust <$> isUnboxProjection q isUnboxCopattern _ = return False tuplePat :: ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ()) -tuplePat cons i ps = do - let p = ConP cons i ps - err = sep [ "Tuple pattern" - , nest 2 $ prettyTCM p - , "does not have a known size." ] - xs <- makeListP' "Agda.Builtin.Unit.tt" "Haskell.Prim.Tuple._;_" err p - qs <- mapM compilePat xs - return $ Hs.PTuple () Hs.Boxed qs +tuplePat cons i ps = mapM (compilePat . namedArg) ps <&> Hs.PTuple () Hs.Boxed -- Agda2Hs does not support natural number patterns directly (since -- they don't exist in Haskell), however they occur as part of diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs index 4dbe214a..e13e615b 100644 --- a/src/Agda2Hs/Compile/Term.hs +++ b/src/Agda2Hs/Compile/Term.hs @@ -53,18 +53,12 @@ isSpecialTerm q = case prettyShow q of isSpecialCon :: QName -> Maybe (ConHead -> ConInfo -> Elims -> C (Hs.Exp ())) isSpecialCon = prettyShow >>> \case - "Haskell.Prim.Tuple._;_" -> Just tupleTerm + "Haskell.Prim.Tuple._,_" -> Just tupleTerm + "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tupleTerm _ -> Nothing tupleTerm :: ConHead -> ConInfo -> Elims -> C (Hs.Exp ()) -tupleTerm cons i es = do - let v = Con cons i es - err = sep [ text "Tuple value" - , nest 2 $ prettyTCM v - , text "does not have a known size." ] - xs <- makeList' "Agda.Builtin.Unit.tt" "Haskell.Prim.Tuple._;_" err v - ts <- mapM compileTerm xs - return $ Hs.Tuple () Hs.Boxed ts +tupleTerm cons i es = compileElims es <&> Hs.Tuple () Hs.Boxed ifThenElse :: QName -> Elims -> C (Hs.Exp ()) ifThenElse _ es = compileElims es >>= \case diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs index 917cb625..07478c2c 100644 --- a/src/Agda2Hs/Compile/Type.hs +++ b/src/Agda2Hs/Compile/Type.hs @@ -40,33 +40,14 @@ import Agda2Hs.HsUtils isSpecialType :: QName -> Maybe (QName -> Elims -> C (Hs.Type ())) isSpecialType = prettyShow >>> \case - "Haskell.Prim.Tuple.Tuple" -> Just tupleType "Haskell.Prim.Tuple._×_" -> Just tupleType "Haskell.Prim.Tuple._×_×_" -> Just tupleType _ -> Nothing -tupleType' :: C Doc -> Term -> C [Term] -tupleType' err xs = - reduce xs >>= \case - Def q es - | [] <- vis es, q ~~ "Agda.Builtin.Unit.⊤" -> pure [] - | [_,_] <- vis es, q ~~ "Haskell.Prim.Tuple.Pair" -> pairToTuple es - _ -> genericDocError =<< err - where - vis es = [ unArg a | Apply a <- es, visible a ] - - pairToTuple :: Elims -> C [Term] - pairToTuple es - | Just [x, xs] <- allApplyElims es = (unArg x:) <$> tupleType' err (unArg xs) - | otherwise = genericDocError =<< text "Bad arguments for Pair: " text (show es) - tupleType :: QName -> Elims -> C (Hs.Type ()) tupleType q es = do - let err = sep [ prettyTCM (Def q es) - , text "is not a concrete sequence of types." - ] - xs <- reduce (Def q es) >>= tupleType' err - ts <- mapM compileType xs + let Just as = allApplyElims es + ts <- mapM (compileType . unArg) as return $ Hs.TyTuple () Hs.Boxed ts -- | Add a class constraint to a Haskell type. diff --git a/test/Fail/TuplePat.agda b/test/Fail/TuplePat.agda deleted file mode 100644 index c0ead4cb..00000000 --- a/test/Fail/TuplePat.agda +++ /dev/null @@ -1,9 +0,0 @@ - -module Fail.TuplePat where - -open import Haskell.Prelude - -fst₃ : a × b × c → a -fst₃ (x ; xs) = x - -{-# COMPILE AGDA2HS fst₃ #-} diff --git a/test/Fail/TupleTerm.agda b/test/Fail/TupleTerm.agda deleted file mode 100644 index 4ac30b0f..00000000 --- a/test/Fail/TupleTerm.agda +++ /dev/null @@ -1,9 +0,0 @@ - -module Fail.TupleTerm where - -open import Haskell.Prelude - -pair2trip : a → b × c → a × b × c -pair2trip x xs = x ; xs - -{-# COMPILE AGDA2HS pair2trip #-} diff --git a/test/Fail/TupleType.agda b/test/Fail/TupleType.agda deleted file mode 100644 index e294ebfa..00000000 --- a/test/Fail/TupleType.agda +++ /dev/null @@ -1,9 +0,0 @@ - -module Fail.TupleType where - -open import Haskell.Prelude - -idT : ∀ {@0 as} → Tuple as → Tuple as -idT x = x - -{-# COMPILE AGDA2HS idT #-} diff --git a/test/Tuples.agda b/test/Tuples.agda index 62674bc9..0288ddf2 100644 --- a/test/Tuples.agda +++ b/test/Tuples.agda @@ -8,11 +8,6 @@ swap (a , b) = b , a {-# COMPILE AGDA2HS swap #-} -unit2unit : ⊤ → Tuple [] -unit2unit tt = tt - -{-# COMPILE AGDA2HS unit2unit #-} - data TuplePos : Set where Test : TuplePos × Bool → TuplePos @@ -33,3 +28,13 @@ t3 : Bool × (Bool × Bool) t3 = True , (False , True) {-# COMPILE AGDA2HS t3 #-} + +pair : Int × Int +pair = 1 , 2 + +{-# COMPILE AGDA2HS pair #-} + +test : Int +test = let (x , y) = pair in x + y + +{-# COMPILE AGDA2HS test #-} diff --git a/test/golden/TuplePat.err b/test/golden/TuplePat.err deleted file mode 100644 index 9a83259d..00000000 --- a/test/golden/TuplePat.err +++ /dev/null @@ -1,2 +0,0 @@ -test/Fail/TuplePat.agda:6,1-5 -Tuple pattern (_;_ x xs) does not have a known size. diff --git a/test/golden/TupleTerm.err b/test/golden/TupleTerm.err deleted file mode 100644 index da0cf505..00000000 --- a/test/golden/TupleTerm.err +++ /dev/null @@ -1,2 +0,0 @@ -test/Fail/TupleTerm.agda:6,1-10 -Tuple value x ; xs does not have a known size. diff --git a/test/golden/TupleType.err b/test/golden/TupleType.err deleted file mode 100644 index 1bc97f5f..00000000 --- a/test/golden/TupleType.err +++ /dev/null @@ -1,2 +0,0 @@ -test/Fail/TupleType.agda:6,1-4 -Tuple as is not a concrete sequence of types. diff --git a/test/golden/Tuples.hs b/test/golden/Tuples.hs index 6d9a97c6..2cce6227 100644 --- a/test/golden/Tuples.hs +++ b/test/golden/Tuples.hs @@ -3,9 +3,6 @@ module Tuples where swap :: (a, b) -> (b, a) swap (a, b) = (b, a) -unit2unit :: () -> () -unit2unit () = () - data TuplePos = Test (TuplePos, Bool) t1 :: (Bool, Bool, Bool) @@ -17,3 +14,9 @@ t2 = ((True, False), True) t3 :: (Bool, (Bool, Bool)) t3 = (True, (False, True)) +pair :: (Int, Int) +pair = (1, 2) + +test :: Int +test = fst pair + snd pair +