From 68eab23c51859bfb3b3d5d0427572adae2c0b671 Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Thu, 22 Feb 2024 11:48:48 +0100
Subject: [PATCH] add Extra.Sigma

---
 lib/Haskell/Extra/Sigma.agda | 16 ++++++++++++++++
 src/Agda2Hs/Compile/Term.hs  |  1 +
 src/Agda2Hs/Compile/Type.hs  |  1 +
 test/Tuples.agda             |  9 +++++++++
 test/golden/Tuples.hs        |  5 +++++
 5 files changed, 32 insertions(+)
 create mode 100644 lib/Haskell/Extra/Sigma.agda

diff --git a/lib/Haskell/Extra/Sigma.agda b/lib/Haskell/Extra/Sigma.agda
new file mode 100644
index 00000000..0fb38fce
--- /dev/null
+++ b/lib/Haskell/Extra/Sigma.agda
@@ -0,0 +1,16 @@
+module Haskell.Extra.Sigma where
+
+record Σ (a : Set) (b : @0 a → Set) : Set where
+  constructor _,_
+  field
+    fst : a
+    snd : b fst
+open Σ public
+
+infix 2 Σ-syntax
+
+Σ-syntax : (a : Set) → (@0 a → Set) → Set
+Σ-syntax = Σ
+{-# COMPILE AGDA2HS Σ-syntax inline #-}
+
+syntax Σ-syntax a (λ x → b) = Σ[ x ∈ a ] b
diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
index 958b1fa1..9e965112 100644
--- a/src/Agda2Hs/Compile/Term.hs
+++ b/src/Agda2Hs/Compile/Term.hs
@@ -337,6 +337,7 @@ isSpecialCon :: QName -> Maybe ConCompileRule
 isSpecialCon = prettyShow >>> \case
   "Haskell.Prim.Tuple._,_"          -> Just tupleTerm
   "Haskell.Prim.Tuple._×_×_._,_,_"  -> Just tupleTerm
+  "Haskell.Extra.Sigma._,_"         -> Just tupleTerm
   "Haskell.Extra.Erase.Erased"      -> Just erasedTerm
   "Haskell.Extra.Delay.Delay.now"   -> Just compileErasedApp
   "Haskell.Extra.Delay.Delay.later" -> Just compileErasedApp
diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index ddbc35fb..ccebf30b 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -46,6 +46,7 @@ isSpecialType :: QName -> Maybe (Elims -> C (Hs.Type ()))
 isSpecialType = prettyShow >>> \case
   "Haskell.Prim.Tuple._×_"    -> Just tupleType
   "Haskell.Prim.Tuple._×_×_"  -> Just tupleType
+  "Haskell.Extra.Sigma.Σ"     -> Just tupleType
   "Haskell.Extra.Erase.Erase" -> Just unitType
   "Haskell.Extra.Delay.Delay" -> Just delayType
   _                           -> Nothing
diff --git a/test/Tuples.agda b/test/Tuples.agda
index 7b9cb29f..4c67555b 100644
--- a/test/Tuples.agda
+++ b/test/Tuples.agda
@@ -45,3 +45,12 @@ test2 = case t1 of \where
 
 {-# COMPILE AGDA2HS test2 #-}
 
+open import Haskell.Extra.Sigma as S using (Σ-syntax)
+open import Haskell.Extra.Dec
+open import Haskell.Prim using (itsTrue)
+open import Haskell.Extra.Refinement
+
+t4 : Σ[ n ∈ Nat ] (Dec (IsTrue (n <= 5)))
+t4 = 3 S., (True ⟨ itsTrue ⟩)
+
+{-# COMPILE AGDA2HS t4 #-}
diff --git a/test/golden/Tuples.hs b/test/golden/Tuples.hs
index 156bd6d4..ed6ba07b 100644
--- a/test/golden/Tuples.hs
+++ b/test/golden/Tuples.hs
@@ -1,5 +1,7 @@
 module Tuples where
 
+import Numeric.Natural (Natural)
+
 swap :: (a, b) -> (b, a)
 swap (a, b) = (b, a)
 
@@ -25,3 +27,6 @@ test2
   = case t1 of
         (a, b, c) -> c
 
+t4 :: (Natural, Bool)
+t4 = (3, True)
+